Tidying and modification to cope with iffCE

--- a/src/ZF/IMP/Denotation.ML	Wed Nov 26 16:45:54 1997 +0100
+++ b/src/ZF/IMP/Denotation.ML	Wed Nov 26 16:48:11 1997 +0100
@@ -6,43 +6,37 @@
 
 open Denotation;
 
-(**** Rewrite Rules for A,B,C ****)
-
-val A_rewrite_rules =
-     [A_nat_def,A_loc_def,A_op1_def,A_op2_def];
+(** Rewrite Rules for A,B,C **)
+Addsimps [A_nat_def,A_loc_def,A_op1_def,A_op2_def];
+Addsimps [B_true_def,B_false_def,B_op_def,B_not_def,B_and_def,B_or_def];
+Addsimps [C_skip_def,C_assign_def,C_comp_def,C_if_def,C_while_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 ****)
+(** 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 Asm_simp_tac),
              (ALLGOALS (fast_tac (claset() addSIs [apply_type])))]);
 
-(**** Type_intr for B ****)
+(** 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 Asm_simp_tac),
              (ALLGOALS (fast_tac (claset() 
                           addSIs [apply_type,A_type]@bool_typechecks)))]);
 
-(**** C_subset ****)
+(** 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 Asm_simp_tac),
              (ALLGOALS (fast_tac (claset() addDs [lfp_subset RS subsetD])))]);
 
-(**** Type_elims for C ****)
+(** Type_elims for C **)
 
 val C_type = prove_goal Denotation.thy
         "[| <x,y>:C(c); c:com;                                  \
@@ -64,10 +58,10 @@
                    (Asm_simp_tac 1)]);
 
 
-(**** bnd_mono (nat->nat*nat->nat,Gamma(b,c) ****)
+(** 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 => [(best_tac (claset() addEs [C_type]) 1)]);
 
-(**** End ***)
+(** End ***)

--- a/src/ZF/IMP/Equiv.ML	Wed Nov 26 16:45:54 1997 +0100
+++ b/src/ZF/IMP/Equiv.ML	Wed Nov 26 16:48:11 1997 +0100
@@ -4,21 +4,18 @@
     Copyright   1994 TUM
 *)
 
-val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \
-\ <a,sigma> -a-> n <-> A(a,sigma) = n";
+val prems = goal Equiv.thy
+   "!!a. [| a: aexp; sigma: loc -> nat |] ==> \
+\        <a,sigma> -a-> n <-> A(a,sigma) = n";
 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 (rewrite_goals_tac A_rewrite_rules);                     (* rewr. Den.   *)
-by (TRYALL (fast_tac (claset() addSIs (evala.intrs@prems)
-                              addSEs aexp_elim_cases)));
+by (etac aexp.induct 1);
+by (ALLGOALS (fast_tac (claset() addSIs evala.intrs
+                                 addSEs aexp_elim_cases 
+                                 addss (simpset()))));
 qed "aexp_iff";
 
 
-val aexp1 = prove_goal Equiv.thy
-        "[| <a,sigma> -a-> n; a: aexp; sigma: loc -> nat |] \
-        \ ==> A(a,sigma) = n"       (* destruction rule *)
-     (fn prems => [(fast_tac (claset() addSIs ((aexp_iff RS iffD1)::prems)) 1)]);
+val aexp1 = aexp_iff RS iffD1;
 val aexp2 = aexp_iff RS iffD2;
 
 
@@ -33,86 +30,64 @@
    ];
 
 
-val prems = goal Equiv.thy "[| b: bexp; sigma: loc -> nat |] ==> \
-\ <b,sigma> -b-> w <-> B(b,sigma) = w";
-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 (rewrite_goals_tac B_rewrite_rules);                 (* rewr. Den.   *)
-by (TRYALL (fast_tac (claset() addSIs (evalb.intrs@prems@[aexp2])
-                            addSDs [aexp1] addSEs bexp_elim_cases)));
+val prems = goal Equiv.thy
+   "!!b. [| b: bexp; sigma: loc -> nat |] ==> \
+\        <b,sigma> -b-> w <-> B(b,sigma) = w";
+by (res_inst_tac [("x","w")] spec 1);
+by (etac bexp.induct 1);
+by (ALLGOALS (fast_tac (claset() addSIs evalb.intrs
+                                 addSEs bexp_elim_cases 
+                                 addss (simpset() addsimps [aexp_iff]))));
 qed "bexp_iff";
 
-val bexp1 = prove_goal Equiv.thy
-        "[| <b,sigma> -b-> w; b: bexp; sigma: loc -> nat |]\
-        \ ==> B(b,sigma) = w"
-     (fn prems => [(fast_tac (claset() addSIs ((bexp_iff RS iffD1)::prems)) 1)]);
+val bexp1 = bexp_iff RS iffD1;
 val bexp2 = bexp_iff RS iffD2;
 
+
 goal Equiv.thy "!!c. <c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)";
-
-(* start with rule induction *)
 by (etac evalc.induct 1);
-
-by (rewrite_tac (Gamma_def::C_rewrite_rules));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [bexp1])));
 (* skip *)
 by (Fast_tac 1);
-
 (* assign *)
-by (asm_full_simp_tac (simpset() addsimps [aexp1,assign_type] @ op_type_intrs) 1);
-
+by (asm_full_simp_tac (simpset() addsimps 
+		       [aexp1, assign_type] @ op_type_intrs) 1);
 (* comp *)
 by (Fast_tac 1);
-
-(* if *)
-by (asm_simp_tac (simpset() addsimps [bexp1]) 1);
-by (asm_simp_tac (simpset() addsimps [bexp1]) 1);
-
 (* while *)
-by (etac (rewrite_rule [Gamma_def]
-          (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
-by (asm_simp_tac (simpset() addsimps [bexp1]) 1);
-by (fast_tac (claset() addSIs [bexp1,idI]@evalb_type_intrs) 1);
-
-by (etac (rewrite_rule [Gamma_def]
-          (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
-by (asm_simp_tac (simpset() addsimps [bexp1]) 1);
-by (fast_tac (claset() addSIs [bexp1,compI]@evalb_type_intrs) 1);
-
+by (etac (Gamma_bnd_mono RS lfp_Tarski RS ssubst) 1);
+by (asm_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
+by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
+(* recursive case of while *)
+by (etac (Gamma_bnd_mono RS lfp_Tarski RS ssubst) 1);
+by (asm_full_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
+by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
 val com1 = result();
 
 
 AddSIs [aexp2,bexp2,B_type,A_type];
-AddIs evalc.intrs;
-AddEs [C_type,C_type_fst];
+AddIs  evalc.intrs;
+AddEs  [C_type,C_type_fst];
+
 
-val [prem] = goal Equiv.thy
-    "c : com ==> ALL x:C(c). <c,fst(x)> -c-> snd(x)";
-by (rtac (prem RS com.induct) 1);
-by (rewrite_tac C_rewrite_rules);
+goal Equiv.thy "!!c. c : com ==> ALL x:C(c). <c,fst(x)> -c-> snd(x)";
+by (etac com.induct 1);
+(* skip *)
+by (fast_tac (claset() addss (simpset())) 1);
+(* assign *)
+by (fast_tac (claset() addss (simpset())) 1);
+(* comp *)
+by (best_tac (claset() addss (simpset())) 1);
+(* while *)
 by Safe_tac;
 by (ALLGOALS Asm_full_simp_tac);
-
-(* skip *)
-by (Fast_tac 1);
-
-(* assign *)
-by (Fast_tac 1);
-
-(* comp *)
-by (REPEAT (EVERY [(dtac bspec 1),(atac 1)]));
-by (Asm_full_simp_tac 1);
-by (Fast_tac 1);
-
-(* while *)
 by (EVERY1 [forward_tac [Gamma_bnd_mono], etac induct, atac]);
 by (rewtac Gamma_def);  
 by Safe_tac;
 by (EVERY1 [dtac bspec, atac]);
 by (ALLGOALS Asm_full_simp_tac);
-
 (* while, if *)
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 val com2 = result();
 
 
@@ -121,7 +96,7 @@
 goal Equiv.thy
     "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
 by (fast_tac (claset() addIs [C_subset RS subsetD]
-	              addEs [com2 RS bspec]
-		      addDs [com1]
-		      addss (simpset())) 1);
+		       addEs [com2 RS bspec]
+		       addDs [com1]
+		       addss (simpset())) 1);
 val com_equivalence = result();