--- a/IMP/Equiv.ML Tue Sep 06 16:46:27 1994 +0200
+++ b/IMP/Equiv.ML Wed Sep 07 13:17:34 1994 +0200
@@ -16,20 +16,25 @@
val aexp2 = aexp_iff RS iffD2;
+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 Equiv.thy "!w. (B(b,s) = w) --> (<b,s> -b-> w)";
+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();
+
+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 (res_inst_tac [("x","w")] spec 1); (* quantify w *)
-by (bexp.induct_tac "b" 1); (* struct. ind. *)
-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));
-
+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);
val BfstD = read_instantiate_sg (sign_of Equiv.thy)