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

Rewrite rules don't rewrite this equality.



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)         +