# HG changeset patch
# User nipkow
# Date 775488737 -7200
# Node ID 0842a38074e72d00e29465ea2be91967402898d3
# Parent  5a54c796b80881a91f06dcd2951ad0b820aa3389
some small simplifications

diff -r 5a54c796b808 -r 0842a38074e7 src/ZF/IMP/Denotation.ML
--- a/src/ZF/IMP/Denotation.ML	Fri Jul 29 13:30:48 1994 +0200
+++ b/src/ZF/IMP/Denotation.ML	Fri Jul 29 15:32:17 1994 +0200
@@ -68,6 +68,6 @@
 
 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)]);
+     (fn prems => [(best_tac (comp_cs addEs [C_type]) 1)]);
 
 (**** End ***)
diff -r 5a54c796b808 -r 0842a38074e7 src/ZF/IMP/Denotation.thy
--- a/src/ZF/IMP/Denotation.thy	Fri Jul 29 13:30:48 1994 +0200
+++ b/src/ZF/IMP/Denotation.thy	Fri Jul 29 15:32:17 1994 +0200
@@ -7,8 +7,8 @@
 Denotation = ZF + Assign + Aexp + Bexp + Com + 
 
 consts
-	A     :: "[i,i] => i"
-	B     :: "[i,i] => i"
+	A     :: "i => i => i"
+	B     :: "i => i => i"
 	C     :: "i => i"
 	Gamma :: "[i,i,i] => i"
 
diff -r 5a54c796b808 -r 0842a38074e7 src/ZF/IMP/Equiv.ML
--- a/src/ZF/IMP/Equiv.ML	Fri Jul 29 13:30:48 1994 +0200
+++ b/src/ZF/IMP/Equiv.ML	Fri Jul 29 15:32:17 1994 +0200
@@ -37,10 +37,10 @@
 
 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"
+    Evala.mk_cases Aexp.con_defs "<N(n),sigma> -a-> i",
+    Evala.mk_cases Aexp.con_defs "<X(x),sigma> -a-> i",
+    Evala.mk_cases Aexp.con_defs "<Op1(f,e),sigma> -a-> i",
+    Evala.mk_cases Aexp.con_defs "<Op2(f,a1,a2),sigma>  -a-> i"
    ];
 
 
@@ -69,12 +69,12 @@
 
 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"
+    Evalb.mk_cases Bexp.con_defs "<true,sigma> -b-> x",
+    Evalb.mk_cases Bexp.con_defs "<false,sigma> -b-> x",
+    Evalb.mk_cases Bexp.con_defs "<ROp(f,a0,a1),sigma> -b-> x",
+    Evalb.mk_cases Bexp.con_defs "<noti(b),sigma> -b-> x",
+    Evalb.mk_cases Bexp.con_defs "<b0 andi b1,sigma> -b-> x",
+    Evalb.mk_cases Bexp.con_defs "<b0 ori b1,sigma> -b-> x"
    ];
 
 
@@ -108,18 +108,17 @@
 
 
 
-
 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)]);
+(* start with rule induction *)
+be (Evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
 
-by (rewrite_tac C_rewrite_rules);
+by (rewrite_tac (Gamma_def::C_rewrite_rules));
 (* skip *)
-by (fast_tac (ZF_cs addSIs [idI]) 1);
+by (fast_tac comp_cs 1);
+
 (* assign *)
 by (asm_full_simp_tac (ZF_ss addsimps [aexp1,assign_type] @
                                       op_type_intrs) 1);
@@ -127,28 +126,19 @@
 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);
+by (fast_tac (ZF_cs addSIs [bexp1] addIs  [(fst_conv RS ssubst)]) 1);
+by (fast_tac (ZF_cs addSIs [bexp1] addIs  [(fst_conv RS ssubst)]) 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 (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
+by (fast_tac (comp_cs addSIs [bexp1,idI]@Evalb_type_intrs
+                      addIs  [(fst_conv RS ssubst)]) 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 (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
 by (fast_tac (comp_cs addSIs [bexp1,compI]@Evalb_type_intrs
                       addIs  [(fst_conv RS ssubst)]) 1);
 
-val Lemma_5_6 = result();
-
-
-
+val com1 = result();
 
 
 val com_cs = ZF_cs addSIs [aexp2,bexp2,B_type,A_type]
@@ -162,22 +152,23 @@
 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));
 
-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));
 
@@ -186,22 +177,22 @@
 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];
+                       addDs [com1];
 
 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 (REPEAT (step_tac com_iff_cs 1));
 by (asm_full_simp_tac ZF_ss 1);
 
 val Com_equivalence = result();