# HG changeset patch
# User nipkow
# Date 774793620 -7200
# Node ID 3a4e092ba69c6bfb1223bfdaaa747380fc4aedb2
# Parent  ac0568345f8878e2027d669fbf6750f621177b20
Initial revision

diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Aexp.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Aexp.ML	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,35 @@
+(*  Title: 	ZF/IMP/Aexp.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+structure Aexp = Datatype_Fun
+ (
+  val thy = Univ.thy |> add_consts [("loc", "i", NoSyn)]
+  val thy_name = "Aexp"
+  val rec_specs = 
+      [(
+        "aexp", "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )",
+          [
+           (["N","X"],	"i => i", NoSyn),
+           (["Op1"],    "[i,i] => i", NoSyn),
+           (["Op2"],    "[i,i,i] => i", NoSyn) 
+          ]
+       )];
+
+  val rec_styp = "i";
+  val ext = None;
+
+  val sintrs = 
+      [
+       "n:nat ==> N(n) : aexp", 
+       "x:loc ==> X(x) : aexp",
+       "[| f: nat -> nat; a : aexp |] ==> Op1(f,a) : aexp",
+       "[| f: (nat * nat) -> nat; a0 : aexp; a1: aexp |] \
+\          ==> Op2(f,a0,a1) : aexp"
+      ];
+  val monos = [];
+  val type_intrs = datatype_intrs;
+  val type_elims = datatype_elims;
+ );
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Aexp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Aexp.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,9 @@
+(*  Title: 	ZF/IMP/Aexp.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+
+Dummy theory merely recording dependence
+*)
+
+Aexp = Univ
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Assign.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Assign.ML	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,12 @@
+(*  Title: 	ZF/IMP/Assign.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+open Assign;
+
+val assign_type = prove_goalw Assign.thy [assign_def]
+	"[| sigma:loc -> nat; n:nat |] ==> sigma[n/x] : loc -> nat"
+    (fn prems => [(fast_tac  
+                   (ZF_cs addIs [apply_type,lam_type,if_type]@prems) 1)]);
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Assign.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Assign.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,13 @@
+(*  Title: 	ZF/IMP/Assign.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+Assign = Aexp +
+consts 
+	"assign" :: "[i,i,i] => i"	("_[_'/_]" [900,0,0] 900)
+
+rules 
+	assign_def	"sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
+end
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Bexp.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Bexp.ML	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,38 @@
+(*  Title: 	ZF/IMP/Bexp.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+structure Bexp = Datatype_Fun
+ (
+  val thy = Aexp.thy;
+  val thy_name = "Bexp"
+  val rec_specs = 
+      [
+       (
+        "bexp", "univ(aexp Un ((nat*nat)->bool) )",
+	  [
+           ( ["true","false"],	"i", NoSyn),
+	   ( ["noti"],		"i => i", NoSyn),
+	   ( ["andi"], 	"[i,i]=>i", Infixl 60),
+	   ( ["ori"], 	"[i,i]=>i", Infixl 60),
+           ( ["ROp"], "[i,i,i] => i", NoSyn)
+          ]
+       )
+      ];
+
+  val rec_styp = "i";
+  val sintrs = 
+       [
+        "true : bexp",
+	"false : bexp",
+	"[| a0 : aexp; a1 : aexp; f: (nat*nat)->bool |] ==> ROp(f,a0,a1) : bexp",
+	"b : bexp ==> noti(b) : bexp",
+	"[| b0 : bexp; b1 : bexp |] ==> b0 andi b1 : bexp",
+	"[| b0 : bexp; b1 : bexp |] ==> b0 ori b1 : bexp"
+       ];
+  val monos = [];
+  val type_intrs = datatype_intrs;
+  val type_elims = datatype_elims;
+ );
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Bexp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Bexp.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,9 @@
+(*  Title: 	ZF/IMP/Bexp.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+
+Dummy theory merely recording dependence
+*)
+
+Bexp = Aexp
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Com.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Com.ML	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,39 @@
+(*  Title: 	ZF/IMP/Com.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+structure Com = Datatype_Fun
+ (
+  val thy = Bexp.thy;
+  val thy_name = "Com";
+  val rec_specs = 
+      [
+       (
+        "com", "univ(aexp Un bexp)",
+	  [
+           (["skip"],		"i", NoSyn),
+	   ([":="],	"[i,i] => i", Infixl 60),
+	   ([";"],	"[i,i] => i", Infixl 60),
+	   (["whileC"], 	"[i,i] => i", Mixfix("while _ do _",[],60)),
+	   (["ifC"],		"[i,i,i] => i",
+              Mixfix("ifc _ then _ else _",[],60))
+          ]
+       )
+      ];
+
+  val rec_styp = "i";
+
+  val sintrs = 
+       [
+	"skip : com",
+	"[| x:loc; a:aexp|] ==> X(x) := a : com",
+	"[| c0:com; c1:com|] ==> c0 ; c1 : com",
+	"[| b:bexp; c:com|] ==> while b do c : com",
+	"[| b:bexp; c0:com; c1:com|] ==> ifc b then c0 else c1 : com"
+       ];
+  val monos = [];
+  val type_intrs = datatype_intrs@Aexp.intrs;
+  val type_elims = datatype_elims
+ );
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Com.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Com.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,9 @@
+(*  Title: 	ZF/IMP/Com.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+
+Dummy theory merely recording dependence
+*)
+
+Com = Bexp
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Denotation.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Denotation.ML	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,73 @@
+(*  Title: 	ZF/IMP/Denotation.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+open Denotation;
+
+(**** Rewrite Rules fuer A,B,C ****)
+
+val A_rewrite_rules =
+     [A_nat_def,A_loc_def,A_op1_def,A_op2_def];
+
+val B_rewrite_rules =
+     [B_true_def,B_false_def,B_op_def,B_not_def,B_and_def,B_or_def]
+
+val C_rewrite_rules = 
+     [C_skip_def,C_assign_def,C_comp_def,C_if_def,C_while_def]; 
+
+(**** Type_intr for A ****)
+
+val A_type = prove_goal Denotation.thy
+	"!!a.[|a:aexp; sigma:loc->nat|] ==> A(a,sigma):nat"
+   (fn _ => [(etac Aexp.induct 1),
+             (rewrite_goals_tac A_rewrite_rules),
+             (ALLGOALS (fast_tac (ZF_cs addSIs [apply_type])))]);
+
+(**** Type_intr for B ****)
+
+val B_type = prove_goal Denotation.thy
+	"!!b. [|b:bexp; sigma:loc->nat|] ==> B(b,sigma):bool"
+   (fn _ => [(etac Bexp.induct 1),
+             (rewrite_goals_tac B_rewrite_rules),
+             (ALLGOALS (fast_tac (ZF_cs 
+                          addSIs [apply_type,A_type]@bool_typechecks)))]);
+
+(**** C_subset ****)
+
+val C_subset = prove_goal Denotation.thy 
+	"!!c. c:com ==> C(c) <= (loc->nat)*(loc->nat)"
+   (fn _ => [(etac Com.induct 1),
+             (rewrite_tac C_rewrite_rules),
+             (ALLGOALS (fast_tac (comp_cs addDs [lfp_subset RS subsetD])))]);
+
+(**** Type_elims for C ****)
+
+val C_type = prove_goal Denotation.thy
+	"[| <x,y>:C(c); c:com; 					\
+\	     !!c. [| x:loc->nat; y:loc->nat |]  ==> R |]	\
+\	  ==> R"
+     (fn prems => [(cut_facts_tac prems 1),
+                   (fast_tac (ZF_cs addSIs prems 
+                                    addDs  [(C_subset RS subsetD)]) 1)]);
+
+val C_type_fst = prove_goal Denotation.thy
+	"[| x:C(c); c:com; 					\
+\	     !!c. [| fst(x):loc->nat |]  ==> R |]	\
+\	  ==> R"
+     (fn prems => [(cut_facts_tac prems 1),
+                   (resolve_tac prems 1),
+                   (dtac (C_subset RS subsetD) 1),
+                   (atac 1),
+                   (etac SigmaE 1),
+                   (asm_simp_tac ZF_ss 1)]);
+
+
+(**** bnd_mono (nat->nat*nat->nat,Gamma(b,c) ****)
+
+val Gamma_bnd_mono = prove_goalw Denotation.thy [bnd_mono_def,Gamma_def]
+	"!!c. c:com ==> bnd_mono ((loc->nat)*(loc->nat),Gamma(b,c))"
+     (fn prems => [(fast_tac (comp_cs addSIs [compI] addEs [C_type]) 1)]);
+
+(**** End ***)
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Denotation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Denotation.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,53 @@
+(*  Title: 	ZF/IMP/Denotation.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+Denotation = ZF + Assign + Aexp + Bexp + Com + 
+
+consts
+	A     :: "[i,i] => i"
+	B     :: "[i,i] => i"
+	C     :: "i => i"
+	Gamma :: "[i,i,i] => i"
+
+rules
+	A_nat_def	"A(N(n)) == (%sigma. n)"
+	A_loc_def	"A(X(x)) == (%sigma. sigma`x)" 
+	A_op1_def	"A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
+	A_op2_def	"A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
+
+
+	B_true_def	"B(true) == (%sigma. 1)"
+	B_false_def	"B(false) == (%sigma. 0)"
+	B_op_def	"B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)" 
+
+
+	B_not_def	"B(noti(b)) == (%sigma. not(B(b,sigma)))"
+	B_and_def	"B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
+	B_or_def	"B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
+
+
+	C_skip_def	"C(skip) == id(loc->nat)"
+	C_assign_def	"C(X(x) := a) == {io:(loc->nat)*(loc->nat). \
+\			 snd(io) = fst(io)[A(a,fst(io))/x]}"
+
+	C_comp_def	"C(c0 ; c1) == C(c1) O C(c0)"
+	C_if_def	"C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} \
+\			 			  Un {io:C(c1). B(b,fst(io))=0}"
+
+	Gamma_def	"Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un \
+\			 		     {io : id(loc->nat). B(b,fst(io))=0})"
+
+	C_while_def	"C(while b do c) == lfp((loc->nat)*(loc->nat), \
+\			                        Gamma(b,c))"
+
+
+end
+
+
+
+
+
+
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Equiv.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Equiv.ML	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,226 @@
+(*  Title: 	ZF/IMP/Equiv.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+val type_cs = ZF_cs addSEs [make_elim(Evala.dom_subset RS subsetD),
+                            make_elim(Evalb.dom_subset RS subsetD),
+                            make_elim(Evalc.dom_subset RS subsetD)];
+
+(**********     type_intrs fuer Evala     **********)
+
+val Evala_type_intrs = 
+ map (fn s => prove_goal Evala.thy s (fn _ => [(fast_tac type_cs 1)]))
+ ["!!a.<a,sigma> -a-> n ==> a:aexp","!!a.<a,sigma> -a-> n ==> sigma:loc->nat",
+  "!!a.<a,sigma> -a-> n ==> n:nat"];
+
+
+(**********     type_intrs fuer Evalb     **********)
+
+val Evalb_type_intrs = 
+ map (fn s => prove_goal Evalb.thy s (fn _ => [(fast_tac type_cs 1)]))
+ ["!!b.<b,sigma> -b-> w ==> b:bexp","!!b.<b,sigma> -b-> w ==> sigma:loc->nat",
+  "!!b.<b,sigma> -b-> w ==> w:bool"];
+
+
+(**********     type_intrs fuer Evalb     **********)
+
+val Evalc_type_intrs = 
+ map (fn s => prove_goal Evalc.thy s (fn _ => [(fast_tac type_cs 1)]))
+ ["!!c.<c,sigma> -c-> sigma' ==> c:com",
+  "!!c.<c,sigma> -c-> sigma' ==> sigma:loc->nat",
+  "!!c.<c,sigma> -c-> sigma' ==> sigma':loc->nat"];
+
+
+val op_type_intrs = Evala_type_intrs@Evalb_type_intrs@Evalc_type_intrs;
+
+val Aexp_elim_cases = 
+   [
+    Evala.mk_cases Aexp.con_defs "<N(n),sigma,i> : evala",
+    Evala.mk_cases Aexp.con_defs "<X(x),sigma,i> : evala",
+    Evala.mk_cases Aexp.con_defs "<Op1(f,e),sigma,i> : evala",
+    Evala.mk_cases Aexp.con_defs "<Op2(f,a1,a2),sigma,i> : evala"
+   ];
+
+
+val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \
+\ <a,sigma> -a-> n <-> n = A(a,sigma) ";
+
+by (res_inst_tac [("x","n")] spec 1);                       (* quantify n *)
+by (res_inst_tac [("x","a")] Aexp.induct 1);                (* struct. ind. *)
+by (resolve_tac prems 1);                                   (* type prem. *)
+by (safe_tac ZF_cs);                        		    (* allI,-->,<-- *)
+by (rewrite_goals_tac A_rewrite_rules);			    (* rewr. Den.   *)
+by (TRYALL (fast_tac (ZF_cs addSIs (Evala.intrs@prems)) )); (* <== *)
+by (TRYALL (fast_tac (ZF_cs addSEs Aexp_elim_cases)));      (* ==> *)
+
+val aexp_iff = result();
+
+
+val Aexp_rew_rules_cs = ZF_cs addIs  op_type_intrs@[aexp_iff RS iffD1 RS sym];
+
+val aexp1 = prove_goal Equiv.thy			    (* elim the prems *)
+        "<a,sigma> -a-> n ==> A(a,sigma) = n"		    (* destruction rule *)
+     (fn prems => [(fast_tac (Aexp_rew_rules_cs addSIs prems) 1)]);
+
+val aexp2 = aexp_iff RS iffD2;
+
+
+val Bexp_elim_cases = 
+   [
+    Evalb.mk_cases Bexp.con_defs "<true,sigma,x> : evalb",
+    Evalb.mk_cases Bexp.con_defs "<false,sigma,x> : evalb",
+    Evalb.mk_cases Bexp.con_defs "<ROp(f,a0,a1),sigma,x> : evalb",
+    Evalb.mk_cases Bexp.con_defs "<noti(b),sigma,x> : evalb",
+    Evalb.mk_cases Bexp.con_defs "<b0 andi b1,sigma,x> : evalb",
+    Evalb.mk_cases Bexp.con_defs "<b0 ori b1,sigma,x> : evalb"
+   ];
+
+
+val prems = goal Equiv.thy "[| b: bexp; sigma: loc -> nat |] ==> \
+\ <b,sigma> -b-> w <-> w = B(b,sigma) ";
+
+by (res_inst_tac [("x","w")] spec 1);				(* quantify w *)
+by (res_inst_tac [("x","b")] Bexp.induct 1);			(* struct. ind. *)
+by (resolve_tac prems 1);					(* type prem. *)
+by (safe_tac ZF_cs);                                  	        (* allI,-->,<-- *)
+by (rewrite_goals_tac B_rewrite_rules);				(* rewr. Den.   *)
+by (TRYALL (fast_tac 						(* <== *)
+            (ZF_cs addSIs (Evalb.intrs@prems@[aexp2])) ));
+by (TRYALL (fast_tac ((ZF_cs addSDs [aexp1]) addSEs Bexp_elim_cases)));
+								(* ==> *)
+
+val bexp_iff = result();
+
+
+val Bexp_rew_rules_cs = ZF_cs addIs  op_type_intrs@[bexp_iff RS iffD1 RS sym];
+
+val bexp1 = prove_goal Equiv.thy
+        "<b,sigma> -b-> w ==> B(b,sigma) = w"
+     (fn prems => [(fast_tac (Bexp_rew_rules_cs addSIs prems) 1)]);
+
+val bexp2 = prove_goal Equiv.thy 
+    "[| B(b,sigma) = w; b : bexp; sigma : loc -> nat |] ==> <b,sigma> -b-> w"
+    (fn prems => 
+    [(cut_facts_tac prems 1), 
+     (fast_tac (ZF_cs addIs ([bexp_iff RS iffD2])) 1)]);
+
+
+
+
+val prems = goal Equiv.thy
+	"<c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)";
+by (cut_facts_tac prems 1);
+
+by 
+(EVERY [(rtac (Evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1),
+(atac 1)]);
+
+by (rewrite_tac C_rewrite_rules);
+(* skip *)
+by (fast_tac (ZF_cs addSIs [idI]) 1);
+(* assign *)
+by (asm_full_simp_tac (ZF_ss addsimps [aexp1,assign_type] @
+                                      op_type_intrs) 1);
+(* comp *)
+by (fast_tac comp_cs 1);
+
+(* if *)
+by (fast_tac (ZF_cs addSIs [bexp1]
+                    addIs  [(fst_conv RS ssubst),UnI1]) 1);
+by (fast_tac (ZF_cs addSIs [bexp1]
+                    addIs  [(fst_conv RS ssubst),UnI2]) 1);
+
+(* while *)
+by (rtac (lfp_Tarski RS ssubst) 1);
+by (fast_tac (ZF_cs addSIs [Gamma_bnd_mono]) 1);
+by (rewrite_tac [Gamma_def]);
+by (fast_tac (ZF_cs addSIs [bexp1,idI]@Evalb_type_intrs
+                    addIs  [(fst_conv RS ssubst),UnI2]) 1);
+
+by (rtac (lfp_Tarski RS ssubst) 1);
+by (fold_tac [Gamma_def]);
+by (fast_tac (ZF_cs addSIs [Gamma_bnd_mono]@Evalc_type_intrs) 1);
+by (fast_tac (comp_cs addSIs [bexp1,compI]@Evalb_type_intrs
+                      addIs  [(fst_conv RS ssubst)]) 1);
+
+val Lemma_5_6 = result();
+
+
+
+
+
+val com_cs = ZF_cs addSIs [aexp2,bexp2,B_type,A_type]
+                   addIs Evalc.intrs
+                   addSEs [idE,compE]
+                   addEs [C_type,C_type_fst];
+
+val [prem] = goal Equiv.thy "c : com ==> ALL x. x:C(c) \
+\ --> <c,fst(x)> -c-> snd(x)";
+
+br (prem RS Com.induct) 1;
+by (rewrite_tac C_rewrite_rules);
+by (safe_tac com_cs);
+
+by (ALLGOALS (asm_full_simp_tac ZF_ss));
+(* skip *)
+by (fast_tac com_cs 1);
+(* assign *)
+by (fast_tac com_cs 1);
+(* comp *)
+by (REPEAT (EVERY [(etac allE 1),(etac impE 1),(atac 1)]));
+by (asm_full_simp_tac ZF_ss 1);
+by (fast_tac com_cs 1);
+(* while *)
+by (EVERY [(forward_tac [Gamma_bnd_mono] 1),(etac induct 1),(atac 1)]);
+
+by (rewrite_goals_tac [Gamma_def]);  
+by (safe_tac com_cs);
+
+by (EVERY [(etac allE 1),(etac impE 1),(atac 1)]);
+by (ALLGOALS (asm_full_simp_tac ZF_ss));
+
+(* while und if *)
+by (ALLGOALS (fast_tac com_cs));
+val com2 = result();
+
+
+
+(**** Beweis der Aequivalenz ****)
+
+
+val com_iff_cs = ZF_cs addIs [C_subset RS subsetD]
+                       addEs [com2 RS spec RS impE]
+                       addDs [Lemma_5_6];
+
+goal Equiv.thy "ALL c:com.\
+\           C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
+by (rtac ballI 1);
+by (rtac equalityI 1);
+by (fast_tac com_iff_cs 1);
+(* Gegenrichtung ! *)
+by (safe_tac com_iff_cs);
+bd Lemma_5_6 1;
+by (asm_full_simp_tac ZF_ss 1);
+
+val Com_equivalence = result();
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Equiv.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Equiv.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,7 @@
+(*  Title: 	ZF/IMP/Equiv.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+Equiv = Denotation + Evalc
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Evala.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Evala.ML	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,26 @@
+(*  Title: 	ZF/IMP/Evala.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+structure Evala = Inductive_Fun
+ (
+  val thy = Evala0.thy;
+  val thy_name="Evala";
+  val rec_doms = [("evala","aexp * (loc -> nat) * nat")];
+  val sintrs = 
+      [
+	"[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n",
+       	"[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x",
+       	"[| <e,sigma> -a-> n; f: nat -> nat |] \
+\           ==> <Op1(f,e),sigma> -a-> f`n" ,
+       	"[| <e0,sigma> -a-> n0; <e1,sigma>  -a-> n1; \
+\           f: (nat * nat) -> nat  |] \
+\           ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"  ];
+
+  val monos = [];
+  val con_defs = [];
+  val type_intrs = Aexp.intrs@[SigmaI,apply_funtype];
+  val type_elims = [SigmaE2]
+ );
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Evala.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Evala.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,9 @@
+(*  Title: 	ZF/IMP/Evala.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+
+Dummy theory merely recording dependence
+*)
+
+Evala = Evala0
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Evala0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Evala0.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,14 @@
+(*  Title: 	ZF/IMP/Evala0.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+Evala0 = Aexp +
+
+consts  evala    :: "i"
+       "@evala"  :: "[i,i,i] => o"	("<_,_>/ -a-> _")
+
+translations
+ "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
+end
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Evalb.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Evalb.ML	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,31 @@
+(*  Title: 	ZF/IMP/Evalb.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+structure Evalb = Inductive_Fun
+ (
+  val thy = Evalb0.thy;
+  val thy_name = "Evalb"
+  val rec_doms = [("evalb","bexp * (loc -> nat) * bool")];
+  val sintrs = 
+      [
+	"[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1",
+       	"[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0",
+       	"[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] \
+\	    ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> ",
+       	"[| <b,sigma> -b-> w |] \
+\	    ==> <noti(b),sigma> -b-> not(w)", 
+       	"[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
+\	    ==> <b0 andi b1,sigma> -b-> (w0 and w1)",
+       	"[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
+\	    ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
+      ];
+
+  val monos = [];
+  val con_defs = [];
+  val type_intrs = Bexp.intrs@[SigmaI,apply_funtype,and_type,or_type,
+		   bool_1I,bool_0I,not_type];
+  val type_elims = [SigmaE2,make_elim(Evala.dom_subset RS subsetD) ];
+ );
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Evalb.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Evalb.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,9 @@
+(*  Title: 	ZF/IMP/Evalb.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+
+Dummy theory merely recording dependence
+*)
+
+Evalb = Evalb0
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Evalb0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Evalb0.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,15 @@
+(*  Title: 	ZF/IMP/Evalb0.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+Evalb0 = Evala + Bexp +
+
+consts 
+        evalb	 :: "i"	
+        "@evalb" :: "[i,i,i] => o"	("<_,_>/ -b-> _")
+
+translations
+	"<be,sig> -b-> b" == "<be,sig,b> : evalb"
+end
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Evalc.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Evalc.ML	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,33 @@
+(*  Title: 	ZF/IMP/Evalc.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+structure Evalc = Inductive_Fun    
+ (
+  val thy = Evalc0.thy;
+  val thy_name = "Evalc"
+  val rec_doms = [("evalc","com * (loc -> nat) * (loc -> nat)")];
+  val sintrs =
+      [
+	"[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma",
+       	"[| m: nat; x: loc; <a,sigma> -a-> m |] ==> \
+\          <X(x) := a,sigma> -c-> sigma[m/x]" , 
+       "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> \
+\          <c0 ; c1, sigma> -c-> sigma1",
+       "[| c1: com; <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \
+\          <ifc b then c0 else c1, sigma> -c-> sigma1 ",
+       "[| c0 : com; <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \
+\          <ifc b then c0 else c1, sigma> -c-> sigma1 ",
+       "[| c: com; <b, sigma> -b-> 0 |] ==> \
+\          <while b do c,sigma> -c-> sigma ",
+       "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; \
+\          <while b do c, sigma2> -c-> sigma1 |] ==> \
+\          <while b do c, sigma> -c-> sigma1 "];
+
+  val monos = [];
+  val con_defs = [assign_def];
+  val type_intrs = Bexp.intrs@Com.intrs@[SigmaI,if_type,lam_type,apply_type];
+  val type_elims = [SigmaE2,make_elim(Evala.dom_subset RS subsetD),
+                            make_elim(Evalb.dom_subset RS subsetD) ]);
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Evalc.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Evalc.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,9 @@
+(*  Title: 	ZF/IMP/Evalc.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+
+Dummy theory merely recording dependence
+*)
+
+Evalc = Evalc0
diff -r ac0568345f88 -r 3a4e092ba69c src/ZF/IMP/Evalc0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Evalc0.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,15 @@
+(*  Title: 	ZF/IMP/Evalc0.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+Evalc0 = Evalb + Com + Assign +
+
+consts
+       evalc    :: "i"
+       "@evalc" :: "[i,i,i] => o"   ("<_,_>/ -c-> _")
+
+translations
+       "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
+end