Simplified some proofs. Added some type assumptions to the introduction rules.

--- a/src/ZF/IMP/Equiv.ML	Thu Aug 04 12:39:28 1994 +0200
+++ b/src/ZF/IMP/Equiv.ML	Mon Aug 08 16:45:08 1994 +0200
@@ -45,24 +45,20 @@
 
 
 val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \
-\ <a,sigma> -a-> n <-> n = A(a,sigma) ";
+\ <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 (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)));      (* ==> *)
+by (ALLGOALS (fast_tac (ZF_cs addSIs (Evala.intrs@prems)
+                              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 aexp1 = prove_goal Equiv.thy			    (* destr. rule *)
+    "[| <a,sigma> -a-> n; a: aexp; sigma: loc -> nat |] ==> A(a,sigma) = n"
+     (fn prems => [fast_tac (ZF_cs addSIs ((aexp_iff RS iffD1)::prems)) 1]);
 
 val aexp2 = aexp_iff RS iffD2;
 
@@ -79,38 +75,25 @@
 
 
 val prems = goal Equiv.thy "[| b: bexp; sigma: loc -> nat |] ==> \
-\ <b,sigma> -b-> w <-> w = B(b,sigma) ";
+\                           <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 (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)));
-								(* ==> *)
+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 (ALLGOALS (fast_tac (ZF_cs addSIs (Evalb.intrs@prems@[aexp2])
+                              addSEs Bexp_elim_cases addSDs [aexp1])));
 
 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 bexp1 = prove_goal Equiv.thy 
+    "[| <b,sigma> -b-> w; b : bexp; sigma : loc -> nat |] ==> B(b,sigma) = w"
+    (fn prems => [fast_tac (ZF_cs addIs ((bexp_iff RS iffD1)::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 bexp2 = bexp_iff RS iffD2;
 
-
-
-val prems = goal Equiv.thy
-	"<c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)";
-by (cut_facts_tac prems 1);
+goal Equiv.thy "!!c. <c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)";
 
 (* start with rule induction *)
 be (Evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
@@ -130,11 +113,11 @@
 by (fast_tac (ZF_cs addSIs [bexp1] addIs  [(fst_conv RS ssubst)]) 1);
 
 (* while *)
-by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 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 (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 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);
 
@@ -146,10 +129,9 @@
                    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)";
+goal Equiv.thy "!!c. c : com ==> ALL io:C(c). <c,fst(io)> -c-> snd(io)";
 
-br (prem RS Com.induct) 1;
+be Com.induct 1;
 by (rewrite_tac C_rewrite_rules);
 by (safe_tac com_cs);
 by (ALLGOALS (asm_full_simp_tac ZF_ss));
@@ -161,15 +143,15 @@
 by (fast_tac com_cs 1);
 
 (* comp *)
-by (REPEAT (EVERY [(etac allE 1),(etac impE 1),(atac 1)]));
+by (REPEAT (EVERY [dtac bspec 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 (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 (EVERY [dtac bspec 1, atac 1]);
 by (ALLGOALS (asm_full_simp_tac ZF_ss));
 
 (* while und if *)
@@ -180,7 +162,7 @@
 (**** Beweis der Aequivalenz ****)
 
 val com_iff_cs = ZF_cs addIs [C_subset RS subsetD]
-                       addEs [com2 RS spec RS impE]
+                       addEs [com2 RS bspec]
                        addDs [com1];
 
 goal Equiv.thy "ALL c:com.\
@@ -196,22 +178,3 @@
 by (asm_full_simp_tac ZF_ss 1);
 
 val Com_equivalence = result();
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-

--- a/src/ZF/IMP/Evalc.ML	Thu Aug 04 12:39:28 1994 +0200
+++ b/src/ZF/IMP/Evalc.ML	Mon Aug 08 16:45:08 1994 +0200
@@ -12,17 +12,19 @@
   val sintrs =
       [
 	"[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma",
-       	"[| m: nat; x: loc; <a,sigma> -a-> m |] ==> \
+       	"[| m: nat; x: loc; a:aexp; <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 |] ==> \
+       "[| b:bexp; c1:com; sigma:loc->nat;\
+\          <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \
+\       <ifc b then c0 else c1, sigma> -c-> sigma1 ",
+       "[| b:bexp; c0:com; sigma:loc->nat;\
+\          <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \
+\       <ifc b then c0 else c1, sigma> -c-> sigma1 ",
+       "[| b:bexp; c:com; <b, sigma> -b-> 0 |] ==> \
 \          <while b do c,sigma> -c-> sigma ",
-       "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; \
+       "[| b:bexp; c:com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; \
 \          <while b do c, sigma2> -c-> sigma1 |] ==> \
 \          <while b do c, sigma> -c-> sigma1 "];