IMP/Equiv.ML

--- a/IMP/Equiv.ML	Wed Nov 02 15:26:13 1994 +0100
+++ b/IMP/Equiv.ML	Thu Nov 03 11:36:54 1994 +0100
@@ -4,36 +4,26 @@
     Copyright   1994 TUM
 *)
 
-goal Equiv.thy "(<a,s> -a-> n) = (A(a,s) = n)";
-by (res_inst_tac [("x","n")] spec 1);                     (* quantify n *)
+goal Equiv.thy "!n. (<a,s> -a-> n) = (n = A(a,s))";
 by (aexp.induct_tac "a" 1);                		  (* struct. ind. *)
 by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps)));	  (* rewr. Den.   *)
 by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
-                             addSEs aexp_elim_cases)));
-val aexp_iff = result();
-
-val aexp1 = aexp_iff RS iffD1;
-val aexp2 = aexp_iff RS iffD2;
+                             addSEs evala_elim_cases)));
+val aexp_iff = result() RS spec;
 
 
-goal Equiv.thy "!w. (<b,s> -b-> w) --> (B(b,s) = w)";
-by (bexp.induct_tac "b" 1);
-by (rewrite_goals_tac B_simps);		(*denotational semantics*)
-by (ALLGOALS (fast_tac (HOL_cs addSDs [aexp1] addSEs bexp_elim_cases)));
-val bexp_imp1 = result();
+goal HOL.thy "(? x. x=t & P) = P";
+by(fast_tac HOL_cs 1);
+val elim_ex_conv = result();
 
-goal Equiv.thy "!w. (B(b,s) = w) --> (<b,s> -b-> w)";
+goal Equiv.thy "!w. (<b,s> -b-> w) = (w = B(b,s))";
 by (bexp.induct_tac "b" 1);
-by (rewrite_goals_tac B_simps);		(*denotational semantics*)
-by (ALLGOALS (best_tac (HOL_cs addSIs (aexp2::evalb.intrs))));
-val bexp_imp2 = result();
+by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong]
+              addsimps (aexp_iff::elim_ex_conv::B_simps@evalb_simps))));
+val bexp_iff = result() RS spec;
 
-val bexp1 = bexp_imp1 RS spec RS mp |> standard;
-val bexp2 = bexp_imp2 RS spec RS mp |> standard;
-
-goal Equiv.thy "(<b,s> -b-> w) = (B(b,s) = w)";
-by (fast_tac (HOL_cs addSEs [bexp1,bexp2]) 1);
-val bexp_iff = result();
+val bexp1 = bexp_iff RS iffD1;
+val bexp2 = bexp_iff RS iffD2;
 
 val BfstI = read_instantiate_sg (sign_of Equiv.thy)
               [("P","%x.B(?b,x)")] (fst_conv RS ssubst);
@@ -49,7 +39,7 @@
 (* skip *)
 by (fast_tac comp_cs 1);
 (* assign *)
-by (asm_full_simp_tac (prod_ss addsimps [aexp1]) 1);
+by (asm_full_simp_tac (prod_ss addsimps [aexp_iff]) 1);
 (* comp *)
 by (fast_tac comp_cs 1);
 (* if *)
@@ -64,41 +54,31 @@
 val com1 = result();
 
 
-val com_cs = comp_cs addSIs [aexp2,bexp2] addIs evalc.intrs;
+val com_ss = prod_ss addsimps (aexp_iff::bexp_iff::evalc.intrs);
 
 goal Equiv.thy "!io:C(c). <c,fst(io)> -c-> snd(io)";
 by (com.induct_tac "c" 1);
 by (rewrite_tac C_simps);
-by (safe_tac com_cs);
-by (ALLGOALS (asm_full_simp_tac prod_ss));
-
-(* skip *)
-by (fast_tac com_cs 1);
-
-(* assign *)
-by (fast_tac com_cs 1);
+by (safe_tac comp_cs);
+by (ALLGOALS (asm_full_simp_tac com_ss));
 
 (* comp *)
 by (REPEAT (EVERY [(dtac bspec 1),(atac 1)]));
-by (asm_full_simp_tac prod_ss 1);
-by (fast_tac com_cs 1);
+by (asm_full_simp_tac com_ss 1);
 
 (* while *)
 by (etac (Gamma_mono RSN (2,induct)) 1);
 by (rewrite_goals_tac [Gamma_def]);  
-by (safe_tac com_cs);
+by (safe_tac comp_cs);
 by (EVERY1 [dtac bspec, atac]);
-by (ALLGOALS (asm_full_simp_tac prod_ss));
+by (ALLGOALS (asm_full_simp_tac com_ss));
 
-(* while, if *)
-by (ALLGOALS (fast_tac com_cs));
 val com2 = result();
 
 
 (**** Proof of Equivalence ****)
 
-val com_iff_cs = set_cs addEs [com2 RS bspec]
-                        addDs [com1];
+val com_iff_cs = set_cs addEs [com2 RS bspec] addDs [com1];
 
 goal Equiv.thy "C(c) = {io . <c,fst(io)> -c-> snd(io)}";
 by (rtac equalityI 1);