Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <24788.9312101146@frogland.inmos.co.uk>
Subject: Re: Strange REWRITE_TAC
To: schneide@ira.uka.de (schneide)
Date: Fri, 10 Dec 1993 11:46:01 +0000 (GMT)
Cc: info-hol@cs.uidaho.edu (info-hol mailing list)
In-Reply-To: <"i80fs2.ira.943:10.11.93.10.00.23"@ira.uka.de> from "schneide" at Dec 10, 93 10:38:34 am
Content-Type: text
Content-Length: 2851

schneide has said:
>   I tried to verify a very small circuit and I found that HOL (i.e. HOL90) 
> didn't behave as I expected. I defined a ciruit which has been implemented
> by a base module, which is again implemented by given modules. If I tried
> to rewrite with the definitions, nothing happend. 
> 
> Here's the code:
> new_theory "count2";
...
> val BASIC_IMP = new_definition("BASIC_IMP",
> 	--`BASIC_IMP cin reset enable cout out =
> 		?l1 l2 l3 l4 l5 l6.
> 			...`--);
> 
> 
> val TWO_SIGN = new_definition("TWO_SIGN",
> 	--`TWO_SIGN reset enable out =
> 		? l1 l2 l3 l4.
> 			(BASIC_IMP (\t:num.T) reset enable l1 l2) /\
> 			(BASIC_IMP   l1   reset enable l3 l4) /\
> 			AND(l2,l4,out)`--);
> 
> 
> (* --------------------------------------------------------------------- *)
> (* The goal I actually wanted to prove is more complicated, but	the 	 *)
> (* curiosity can be demonstrated here although the goal below is not	 *)
> (* provable.								 *)
> (* --------------------------------------------------------------------- *)
> 
> val g2 = ([],--`TWO_SIGN reset enable out`--);
> 
> set_goal g2;
> e(REWRITE_TAC(map snd (definitions "-")));
> 
> 
> The result is the following subgoal:
> 1 subgoal:
> (--`?l1 l2 l3 l4.
>       BASIC_IMP (\t. T) reset enable l1 l2 /\
>       BASIC_IMP l1 reset enable l3 l4 /\
>       (!t. out t = l2 t /\ l4 t)`--)

The problem is that if the first BASIC_IMP gets rewritten then term
that is instatiated contains some `l1`'s that are from the argument
that that replaces `cout` while there are also occurrence of `l1` from
the internal existentially quantified `l1`, hence the rewrite fails.

HOL handles the universally quantified variables to a rewrite term by
first specialising then the genvar's - i.e. unique variable names - so 
that there can be no clashes. You could do the same here, except that
you would get lots of gen%var%nnn's around that you didn't need.

One method of alieviating this would be to have a naming convention on
"local wires" which incorporated the name of the "module" they are
local to. E.g.

--`TWO_SIGN reset enable out =
   ? TWO_SIGN_l1 TWO_SIGN_l2 TWO_SIGN_l3 TWO_SIGN_l4.
     ....`

but this looks messy.

Another solution is to write a rewrite conversion/rule/tactic that
alpha converts any quatification in the rhs of rewrites so that names
do not clash with free variables in the term being rewritten.
(As I assume you are (a) doing this in the context of hardware unfolding
and (b) using your restricted hardware equation form, then this should
be fairly trivial to do).

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"you might think that   ---   I couldn't possibly comment"