# HG changeset patch
# User paulson
# Date 844676760 -7200
# Node ID cc274e47f607521d2e6698054249dc8f96817cf7
# Parent  bf3891343aa57ea093cee10dd99a78ae6e00108c
Ran expandshort

diff -r bf3891343aa5 -r cc274e47f607 src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Mon Oct 07 10:23:35 1996 +0200
+++ b/src/HOL/IMP/Hoare.ML	Mon Oct 07 10:26:00 1996 +0200
@@ -11,22 +11,20 @@
 
 goalw Hoare.thy [hoare_valid_def] "!!P c Q. |- {P}c{Q} ==> |= {P}c{Q}";
 by (etac hoare.induct 1);
-    by(ALLGOALS Asm_simp_tac);
+    by (ALLGOALS Asm_simp_tac);
   by (Fast_tac 1);
  by (Fast_tac 1);
 by (rtac allI 1);
 by (rtac allI 1);
 by (rtac impI 1);
 by (etac induct2 1);
- br Gamma_mono 1;
+ by (rtac Gamma_mono 1);
 by (rewtac Gamma_def);  
 by (Fast_tac 1);
 qed "hoare_sound";
 
 goalw Hoare.thy [swp_def] "swp SKIP Q = Q";
 by (Simp_tac 1);
-by (rtac ext 1);
-by (Fast_tac 1);
 qed "swp_SKIP";
 
 goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[a s/x]))";
@@ -56,7 +54,6 @@
 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 1);
 qed "swp_While_False";
 
 Addsimps [swp_SKIP,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False];
@@ -79,18 +76,18 @@
 by (deepen_tac (!claset addIs [hoare.conseq]) 0 1);
 by (Step_tac 1);
 by (rtac hoare.conseq 1);
-  be thin_rl 1;
+  by (etac thin_rl 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 (rtac hoare.While 1);
+ by (rtac hoare.conseq 1);
+   by (etac thin_rl 3);
+   by (rtac allI 3);
+   by (rtac impI 3);
+   by (assume_tac 3);
   by (Fast_tac 2);
- by(safe_tac HOL_cs);
- by(rotate_tac ~1 1);
- by(Asm_full_simp_tac 1);
+ by (safe_tac HOL_cs);
+ by (rotate_tac ~1 1);
+ by (Asm_full_simp_tac 1);
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac 1);
 qed_spec_mp "swp_is_pre";
diff -r bf3891343aa5 -r cc274e47f607 src/HOL/IMP/Transition.ML
--- a/src/HOL/IMP/Transition.ML	Mon Oct 07 10:23:35 1996 +0200
+++ b/src/HOL/IMP/Transition.ML	Mon Oct 07 10:26:00 1996 +0200
@@ -34,7 +34,7 @@
 \              (c;d, s) -*-> (SKIP, u)";
 by (nat_ind_tac "n" 1);
  (* case n = 0 *)
- by(fast_tac (!claset addIs [rtrancl_into_rtrancl2])1);
+ by (fast_tac (!claset addIs [rtrancl_into_rtrancl2])1);
 (* induction step *)
 by (safe_tac (!claset addSDs [rel_pow_Suc_D2]));
 by (split_all_tac 1);
diff -r bf3891343aa5 -r cc274e47f607 src/HOL/IMP/VC.ML
--- a/src/HOL/IMP/VC.ML	Mon Oct 07 10:23:35 1996 +0200
+++ b/src/HOL/IMP/VC.ML	Mon Oct 07 10:26:00 1996 +0200
@@ -14,24 +14,24 @@
 
 goal VC.thy "!Q. (!s. vc c Q s) --> |- {wp c Q} astrip c {Q}";
 by (acom.induct_tac "c" 1);
-    by(ALLGOALS Simp_tac);
-    by(Fast_tac 1);
-   by(Fast_tac 1);
-  by(Fast_tac 1);
+    by (ALLGOALS Simp_tac);
+    by (Fast_tac 1);
+   by (Fast_tac 1);
+  by (Fast_tac 1);
  (* if *)
- by(Deepen_tac 4 1);
+ by (Deepen_tac 4 1);
 (* while *)
 by (safe_tac HOL_cs);
 by (resolve_tac hoare.intrs 1);
-  br lemma 1;
- brs hoare.intrs 1;
- brs hoare.intrs 1;
-   by(ALLGOALS(fast_tac HOL_cs));
+  by (rtac lemma 1);
+ by (resolve_tac hoare.intrs 1);
+ by (resolve_tac hoare.intrs 1);
+   by (ALLGOALS(fast_tac HOL_cs));
 qed "vc_sound";
 
 goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)";
 by (acom.induct_tac "c" 1);
-    by(ALLGOALS Asm_simp_tac);
+    by (ALLGOALS Asm_simp_tac);
 by (EVERY1[rtac allI, rtac allI, rtac impI]);
 by (EVERY1[etac allE, etac allE, etac mp]);
 by (EVERY1[etac allE, etac allE, etac mp, atac]);
@@ -39,7 +39,7 @@
 
 goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
 by (acom.induct_tac "c" 1);
-    by(ALLGOALS Asm_simp_tac);
+    by (ALLGOALS Asm_simp_tac);
 by (safe_tac HOL_cs);
 by (EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
 by (fast_tac (HOL_cs addEs [wp_mono]) 1);
@@ -49,20 +49,20 @@
   "!!P c Q. |- {P}c{Q} ==> \
 \          (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> wp ac Q s))";
 by (etac hoare.induct 1);
-     by(res_inst_tac [("x","Askip")] exI 1);
-     by(Simp_tac 1);
-    by(res_inst_tac [("x","Aass x a")] exI 1);
-    by(Simp_tac 1);
-   by(SELECT_GOAL(safe_tac HOL_cs)1);
-   by(res_inst_tac [("x","Asemi ac aca")] exI 1);
-   by(Asm_simp_tac 1);
-   by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
-  by(SELECT_GOAL(safe_tac HOL_cs)1);
-  by(res_inst_tac [("x","Aif b ac aca")] exI 1);
-  by(Asm_simp_tac 1);
- by(SELECT_GOAL(safe_tac HOL_cs)1);
- by(res_inst_tac [("x","Awhile b Pa ac")] exI 1);
- by(Asm_simp_tac 1);
+     by (res_inst_tac [("x","Askip")] exI 1);
+     by (Simp_tac 1);
+    by (res_inst_tac [("x","Aass x a")] exI 1);
+    by (Simp_tac 1);
+   by (SELECT_GOAL(safe_tac HOL_cs)1);
+   by (res_inst_tac [("x","Asemi ac aca")] exI 1);
+   by (Asm_simp_tac 1);
+   by (fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
+  by (SELECT_GOAL(safe_tac HOL_cs)1);
+  by (res_inst_tac [("x","Aif b ac aca")] exI 1);
+  by (Asm_simp_tac 1);
+ by (SELECT_GOAL(safe_tac HOL_cs)1);
+ by (res_inst_tac [("x","Awhile b Pa ac")] exI 1);
+ by (Asm_simp_tac 1);
 by (safe_tac HOL_cs);
 by (res_inst_tac [("x","ac")] exI 1);
 by (Asm_simp_tac 1);