Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Date: Fri, 10 Dec 93 10:38:34 EST
From: schneide <schneide@ira.uka.de>
To: info-hol@cs.uidaho.edu
Subject: Strange REWRITE_TAC
Message-Id: <"i80fs2.ira.943:10.11.93.10.00.23"@ira.uka.de>


Hello all,
  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 INV_DEF=new_definition("INV_DEF",
	--`!inp out.INV(inp,out) = !t:num.(out t= ~inp t) `--);
val AND_DEF=new_definition("AND_DEF",
	--`!in1 in2 out.AND(in1,in2,out) = !t:num.out t=(in1 t /\ in2 t )`--);
val XOR2_DEF=new_definition("XOR2_DEF",
	--`!(in1:num->bool) in2 out.XOR2(in1,in2,out) = !t:num. out t=~(in1 t = in2 t)`--);
val MUX_DEF=new_definition("MUX_DEF",
	--`!(in1:num->bool) in2  sel out.
			MUX(sel,in1,in2,out) = !t:num. out t=(sel t =>in1 t|in2 t )`--);
val DELAY_DEF=new_definition("DELAY_DEF",
	--`!inp out.DELAY(inp,out) = !t. (out 0=F) /\(out (SUC t)= inp t)`--);


val BASIC_IMP = new_definition("BASIC_IMP",
	--`BASIC_IMP cin reset enable cout out =
		?l1 l2 l3 l4 l5 l6.
			INV(reset,l1) /\
			AND(cin,enable,l2) /\
			AND(l2,l1,l3) /\
			AND(l3,out,cout) /\
			XOR2(enable,out,l4) /\
			MUX(cin,l4,out,l5) /\	
			AND(l1,l5,l6) /\
			DELAY(l6,out) `--);


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)`--)
=============================


Why did HOL not rewrite with the definition of BASIC_IMP ?????
***************************************************************************
And even more surprising: It is straightforward to prove the following:
	val lemma =
	  |- BASIC_IMP =
	     (\cin reset enable cout out.
	       ?l1 l2 l3 l4 l5 l6.
	         INV (reset,l1) /\
	         AND (cin,enable,l2) /\
	         AND (l2,l1,l3) /\
	         AND (l3,out,cout) /\
	         XOR2 (enable,out,l4) /\
	         MUX (cin,l4,out,l5) /\
	         AND (l1,l5,l6) /\
	         DELAY (l6,out)) : thm

Rewriting with this theorem is then successful. 
***************************************************************************
And now the worst: If the definition of BASIC_IMP is specialised, then 
the rewriting is successful with several instantiations, but not for all.
Just try to rewrite with:

val th1 = SPECL[(--`l1:num->bool`--),(--`reset:num->bool`--),(--`enable:num->bool`--),
	        (--`l3:num->bool`--),(--`l4:num->bool`--)]BASIC_IMP;

and 
val th2 = SPEC_ALL BASIC_IMP
***************************************************************************

Can anyone explain this strange behaviour of REWRITE_TAC??


Klaus