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

*To*: pvs-help@csl.sri.com*Subject*: Rewrite rules don't rewrite this equality.*From*: Adriaan de Groot <adridg@sci.kun.nl>*Date*: Tue, 16 Sep 1997 15:31:33 +0200 (MET DST)

Dear volunteers, I'm trying to prove a theorem in which I compute a result inside an if, and then add that result to something else. PVS revision 2.408, on a regular Sun running Solaris. Here's my test theory: %%% test : THEORY BEGIN struct : TYPE = [# ins:nat, outs:nat #] f(a:struct) : nat = outs(a) ; alemma : LEMMA (forall (a:struct) : (if ins(a)>0 then f(a) else outs(a) endif)=outs(a) ) dilemma : THEOREM (forall (a:struct, b:struct) : (if ins(a)>0 then f(a) else outs(a) endif)+ (if ins(b)>0 then f(b) else outs(b) endif)= outs(a)+outs(b) ) END test %%% The idea is that I can apply alemma twice with different instantiations (ie. a<-a!1, a<-b!1) to prove dilemma. %%% (skolem!)(lemma "alemma" ("a" "a!1"))(lemma "alemma" ("a" "b!1")) %%% However, once I've done that, I end up with this: %%% dilemma : [-1] (IF ins(b!1) > 0 THEN f(b!1) ELSE outs(b!1) ENDIF) = outs(b!1) [-2] (IF ins(a!1) > 0 THEN f(a!1) ELSE outs(a!1) ENDIF) = outs(a!1) |------- [1] (IF ins(a!1) > 0 THEN f(a!1) ELSE outs(a!1) ENDIF) + (IF ins(b!1) > 0 THEN f(b!1) ELSE outs(b!1) ENDIF) = outs(a!1) + outs(b!1) Rule? (assert) No change on: (ASSERT) dilemma : %%% It seems to me that not enough is being rewritten here; running (grind) rewrites the f() calls and then simplifies, which doesn't work for the theory I'm really interested in, since it's more complicated. Am I missing some prover command to do this, or what? My thanks for your help, ade -- +-----------------------------------+-------------------+ + My brother went to London and all + adridg@sci.kun.nl + + I got was this lousy .sig. + (Ade) +

- Prev by Date:
**Re: Instantiating datatypes with subtype of nat** - Next by Date:
**Re: Rewrite rules don't rewrite this equality.** - Prev by thread:
**Re: How can we extend type bool with a "bottom" element?** - Next by thread:
**Re: Rewrite rules don't rewrite this equality.** - Index(es):