# Re: Rewrite rules don't rewrite this equality.

reduce is the core part of grind.  grind basically applies rewrite
rules, then calls reduce, which easily dispenses your theorem.

John

p.s. anyone know why the file "strategies.lisp" is no longer part of
the distribution?  I miss it....

>
> 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,
>