src/HOL/IMP/Hoare.ML

--- a/src/HOL/IMP/Hoare.ML	Mon Aug 19 11:15:44 1996 +0200
+++ b/src/HOL/IMP/Hoare.ML	Mon Aug 19 11:17:20 1996 +0200
@@ -13,7 +13,7 @@
 by (etac hoare.induct 1);
     by(ALLGOALS Asm_simp_tac);
   by(fast_tac rel_cs 1);
- by(fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (rtac allI 1);
 by (rtac allI 1);
 by (rtac impI 1);
@@ -23,26 +23,24 @@
 by(rename_tac "s t" 1);
 by (rewtac Gamma_def);  
 by(eres_inst_tac [("x","s")] allE 1);
-by (safe_tac comp_cs);
+by (Step_tac 1);
   by(ALLGOALS Asm_full_simp_tac);
 qed "hoare_sound";
 
 goalw Hoare.thy [swp_def] "swp SKIP Q = Q";
 by(Simp_tac 1);
 br ext 1;
-by(fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "swp_SKIP";
 
 goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[a s/x]))";
 by(Simp_tac 1);
-br ext 1;
-by(fast_tac HOL_cs 1);
 qed "swp_Ass";
 
 goalw Hoare.thy [swp_def] "swp (c;d) Q = swp c (swp d Q)";
 by(Simp_tac 1);
 br ext 1;
-by(fast_tac comp_cs 1);
+by (Fast_tac 1);
 qed "swp_Semi";
 
 goalw Hoare.thy [swp_def]
@@ -50,7 +48,7 @@
 \                                    (~b s --> swp d Q s))";
 by(Simp_tac 1);
 br ext 1;
-by(fast_tac comp_cs 1);
+by (Fast_tac 1);
 qed "swp_If";
 
 goalw Hoare.thy [swp_def]
@@ -62,38 +60,38 @@
 goalw Hoare.thy [swp_def] "!!s. ~b s ==> swp (WHILE b DO c) Q s = Q s";
 by(stac C_While_If 1);
 by(Asm_simp_tac 1);
-by(fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "swp_While_False";
 
 Addsimps [swp_SKIP,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False];
 
+(*Not suitable for rewriting: LOOPS!*)
+goal Hoare.thy "swp (WHILE b DO c) Q s = \
+\                 (if b s then swp (c;WHILE b DO c) Q s else Q s)";
+by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+qed "swp_While_if";
+
+
 Delsimps [C_while];
 
+AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
+
 goal Hoare.thy "!Q. |- {swp c Q} c {Q}";
 by(com.induct_tac "c" 1);
 by(ALLGOALS Simp_tac);
-    by(fast_tac (HOL_cs addIs [hoare.skip]) 1);
-   by(fast_tac (HOL_cs addIs [hoare.ass]) 1);
-  by(fast_tac (HOL_cs addIs [hoare.semi]) 1);
- by(safe_tac (HOL_cs addSIs [hoare.If]));
-  br hoare.conseq 1;
-    by(fast_tac HOL_cs 2);
-   by(fast_tac HOL_cs 2);
-  by(fast_tac HOL_cs 1);
- br hoare.conseq 1;
-   by(fast_tac HOL_cs 2);
-  by(fast_tac HOL_cs 2);
- by(fast_tac HOL_cs 1);
+by (REPEAT_FIRST Fast_tac);
+by (deepen_tac (!claset addIs [hoare.conseq]) 0 1);
+by (Step_tac 1);
 br hoare.conseq 1;
   be thin_rl 1;
-  by(fast_tac HOL_cs 1);
+  by (Fast_tac 1);
  br hoare.While 1;
  br hoare.conseq 1;
    be thin_rl 3;
    br allI 3;
    br impI 3;
    ba 3;
-  by(fast_tac HOL_cs 2);
+  by (Fast_tac 2);
  by(safe_tac HOL_cs);
  by(rotate_tac ~1 1);
  by(Asm_full_simp_tac 1);
@@ -103,7 +101,7 @@
 
 goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
 br (swp_is_pre RSN (2,hoare.conseq)) 1;
- by(fast_tac HOL_cs 2);
+ by (Fast_tac 2);
 by(rewrite_goals_tac [hoare_valid_def,swp_def]);
-by(fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "hoare_relative_complete";