[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: thkim@salmosa.kaist.ac.kr (Tae Ho Kim)*Subject*: Re: Questions on conversion/coercion.*From*: John Hoffman <hoffman@securecomputing.com>*Date*: Thu, 21 Aug 1997 09:54:09 -0500 (CDT)*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <199708211414.XAA20492@hydra.kaist.ac.kr> from "Tae Ho Kim" at Aug 21, 97 11:14:39 pm

a of type aset is not the same as a of type bset they are different entities, of different types. Here's something that will do what you want. (grind) proves the theorem. comp % [ parameters ] : THEORY BEGIN % ASSUMING % assuming declarations % ENDASSUMING bset : TYPE = {a, b, c, d, e, f} aset_set : setof [bset] = {x : bset | x = a or x = b or x = c} aset : TYPE = (aset_set) t : THEOREM FORALL (e1:aset): EXISTS (e2:bset): e1 = e2 END comp > > Hi. > > I have a question about conversion/coercion. > > 1. > I specified two enumerated types. Every member of A type > is the member of B type. And I want to verify every member > of A is the member of B (theorem t). But I cannot do it. > Because the set A type and the set B type is different. > How can I prove it? > > comp : THEORY > BEGIN > aset : TYPE = {a, b} > bset : TYPE = {a, b, c, d, e, f} > > t : THEOREM FORALL (e1:aset): EXISTS (e2:bset): e1 = e2 > END comp > > 2. > I tried to define and use a conversion funtion. It is > incorrect. What is the false? How can I modify it? > I know that conv function is incorrect (skipping g), > but I cannot find theorem t is incorrect. Theorem t is fine, if conv typechecks correctly. But you'll notice that there's a TCC that gets generated for the definition of conv. You need to show that g is in the domain of conv. It's not, so the proof of the TCC fails. If you look at the proof status screen, you'll find that the proof status of theorem t is incomplete (or something like that) that's because the TCC for conv is false, and t can't be known to be true until conv is typechecked. If you changed your definition of conv to conv(aele:aset): bset = cases aele OF a : a:bset, b : b:bset, g : c:bset endcases you'll be fine. > comp1 : THEORY > BEGIN > aset : TYPE = {a, b, g} > bset : TYPE = {a, b, c, d, e, f} > > conv(aele:aset): bset = > cases aele OF > a : a:bset, > b : b:bset > endcases > > t : THEOREM FORALL(e1:aset):EXISTS (e2:bset): conv(e1) = e2 > END comp1 > > -- > Kim, Tae-ho > thkim@salmosa.kaist.ac.kr > http://salmosa.kaist.ac.kr/~thkim > >

**References**:**Questions on conversion/coercion.***From:*Tae Ho Kim <thkim@salmosa.kaist.ac.kr>

- Prev by Date:
**Questions on conversion/coercion.** - Next by Date:
**Two trivial questions during proof..** - Prev by thread:
**Questions on conversion/coercion.** - Next by thread:
**regarding status-proof-theory** - Index(es):