Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 10 Dec 1993 11:45:25 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA03530;
          Fri, 10 Dec 1993 04:37:36 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA03526;
          Fri, 10 Dec 1993 04:37:32 -0700
Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA08352;
          Fri, 10 Dec 1993 03:34:10 -0800
Received: from ira.uka.de by iraun1.ira.uka.de id <25552-0@iraun1.ira.uka.de>;
          Fri, 10 Dec 1993 12:34:01 +0100
Received: from ira.uka.de by i80fs2.ira.uka.de id <16236-0@i80fs2.ira.uka.de>;
          Fri, 10 Dec 1993 12:33:21 +0100
Date: Fri, 10 Dec 93 12:33:20 EST
From: reetz <reetz@ira.uka.de>
To: info-hol@cs.uidaho.edu
Cc: schneide@ira.uka.de
Subject: RE: more strange rewrite
Message-Id: <"i80fs2.ira.238:10.11.93.11.33.23"@ira.uka.de>

I've taken Klaus' example and changed just the name
of --`l1--` within definition of BASIC_IMP to --`l0`--
and - look, it rewrites now the first occurrence of
BASIC_IMP, at least. So, something with renaming seems
to be strange?

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 =
                ?l0 l2 l3 l4 l5 l6.
                        INV(reset,l0) /\
                        AND(cin,enable,l2) /\
                        AND(l2,l0,l3) /\
                        AND(l3,out,cout) /\
                        XOR2(enable,out,l4) /\
                        MUX(cin,l4,out,l5) /\
                        AND(l0,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 "-")));
 
- OK..
1 subgoal:
(--`?l1 l2 l3 l4.
      (?l0 l2' l3 l4 l5 l6.
        (!t. l0 t = ~(reset t)) /\
        (!t. l2' t = enable t) /\
        (!t. l3 t = l2' t /\ l0 t) /\
        (!t. l1 t = l3 t /\ l2 t) /\
        (!t. l4 t = ~(enable t = l2 t)) /\
        (!t. l5 t = l4 t) /\
        (!t. l6 t = l0 t /\ l5 t) /\
        (!t. ~(l2 0) /\ (l2 (SUC t) = l6 t))) /\
      BASIC_IMP l1 reset enable l3 l4 /\
      (!t. out t = l2 t /\ l4 t)`--)
=============================
 
 
val it = () : unit