--- a/IMP/Equiv.ML Tue Sep 06 13:24:29 1994 +0200
+++ b/IMP/Equiv.ML Tue Sep 06 16:15:59 1994 +0200
@@ -7,7 +7,7 @@
goal Equiv.thy "(<a,s> -a-> n) = (A(a,s) = n)";
by (res_inst_tac [("x","n")] spec 1); (* quantify n *)
by (aexp.induct_tac "a" 1); (* struct. ind. *)
-by (rewrite_goals_tac A_rewrite_rules); (* rewr. Den. *)
+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();
@@ -19,7 +19,8 @@
goal Equiv.thy "(<b,s> -b-> w) = (B(b,s) = w)";
by (res_inst_tac [("x","w")] spec 1); (* quantify w *)
by (bexp.induct_tac "b" 1); (* struct. ind. *)
-by (rewrite_goals_tac B_rewrite_rules); (* rewr. Den. *)
+by(rewrite_goals_tac B_simps);
+ (* simplification with HOL_ss too agressive: (True=x) == True *)
by (safe_tac (HOL_cs addSIs (aexp2::evalb.intrs)
addSDs [aexp1] addSEs bexp_elim_cases)
THEN ALLGOALS(best_tac HOL_cs));
@@ -38,8 +39,8 @@
(* start with rule induction *)
be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
-
-by (rewrite_tac (Gamma_def::C_rewrite_rules));
+by (rewrite_tac (Gamma_def::C_simps));
+ (* simplification with HOL_ss again too agressive *)
(* skip *)
by (fast_tac comp_cs 1);
(* assign *)
@@ -62,7 +63,7 @@
goal Equiv.thy "!io:C(c). <c,fst(io)> -c-> snd(io)";
by (com.induct_tac "c" 1);
-by (rewrite_tac C_rewrite_rules);
+by (rewrite_tac C_simps);
by (safe_tac com_cs);
by (ALLGOALS (asm_full_simp_tac prod_ss));