src/HOL/IMPP/EvenOdd.ML

--- a/src/HOL/IMPP/EvenOdd.ML	Mon Jan 22 11:46:25 2001 +0100
+++ b/src/HOL/IMPP/EvenOdd.ML	Mon Jan 22 17:26:19 2001 +0100
@@ -13,7 +13,7 @@
 
 Goalw [even_def] "even 1 = False";
 by (Clarsimp_tac 1);
-bd dvd_imp_le 1;
+by (dtac dvd_imp_le 1);
 by Auto_tac;
 qed "not_even_1";
 Addsimps [not_even_1];
@@ -21,8 +21,8 @@
 Goalw [even_def] "even (Suc (Suc n)) = even n";
 by (subgoal_tac "Suc (Suc n) = n+#2" 1);
 by  (Simp_tac 2);
-be ssubst 1;
-br dvd_reduce 1;
+by (etac ssubst 1);
+by (rtac dvd_reduce 1);
 qed "even_step";
 Addsimps[even_step];
 
@@ -33,11 +33,11 @@
 Addsimps[Even_neq_Odd, Even_neq_Odd RS not_sym];
 
 Goalw [Z_eq_Arg_plus_def] "(Z=Arg+n) Z s = (Z = s<Arg>+n)";
-br refl 1;
+by (rtac refl 1);
 qed "Z_eq_Arg_plus_def2";
 
 Goalw [Res_ok_def] "Res_ok Z s = (even Z = (s<Res> = 0))";
-br refl 1;
+by (rtac refl 1);
 qed "Res_ok_def2";
 
 val Arg_Res_css = (claset(),simpset()addsimps[Z_eq_Arg_plus_def2,Res_ok_def2]);
@@ -53,59 +53,59 @@
 section "verification";
 
 Goalw [odd_def] "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+1}. odd .{Res_ok}";
-br hoare_derivs.If 1;
-br  (hoare_derivs.Ass RS conseq1) 1;
+by (rtac hoare_derivs.If 1);
+by (rtac (hoare_derivs.Ass RS conseq1) 1);
 by  (clarsimp_tac Arg_Res_css 1);
-br export_s 1;
-br (hoare_derivs.Call RS conseq1) 1;
+by (rtac export_s 1);
+by (rtac (hoare_derivs.Call RS conseq1) 1);
 by  (res_inst_tac [("P","Z=Arg+2")] conseq12 1);
-br   single_asm 1;
+by (rtac single_asm 1);
 by (auto_tac Arg_Res_css);
 qed "Odd_lemma";
 
 Goalw [evn_def] "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}";
-br hoare_derivs.If 1;
-br  (hoare_derivs.Ass RS conseq1) 1;
+by (rtac hoare_derivs.If 1);
+by (rtac (hoare_derivs.Ass RS conseq1) 1);
 by  (clarsimp_tac Arg_Res_css 1);
-br hoare_derivs.Comp 1;
-br  hoare_derivs.Ass 2;
+by (rtac hoare_derivs.Comp 1);
+by (rtac hoare_derivs.Ass 2);
 by (Clarsimp_tac 1);
 by (res_inst_tac [("Q","%Z s. ?P Z s & Res_ok Z s")] hoare_derivs.Comp 1);
-br  export_s 1;
+by (rtac export_s 1);
 by  (res_inst_tac [("I1","%Z l. Z = l Arg & 0 < Z"),
 		   ("Q1","Res_ok")] (Call_invariant RS conseq12) 1);
-br   (single_asm RS conseq2) 1;
+by (rtac (single_asm RS conseq2) 1);
 by   (clarsimp_tac Arg_Res_css 1);
 by  (force_tac Arg_Res_css 1);
-br export_s 1;
+by (rtac export_s 1);
 by (res_inst_tac [("I1","%Z l. even Z = (l Res = 0)"),
 		  ("Q1","%Z s. even Z = (s<Arg>=0)")]
 		 (Call_invariant RS conseq12) 1);
-br  (single_asm RS conseq2) 1;
+by (rtac (single_asm RS conseq2) 1);
 by  (clarsimp_tac Arg_Res_css 1);
 by (force_tac Arg_Res_css 1);
 qed "Even_lemma";
 
 
 Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
-br BodyN 1;
+by (rtac BodyN 1);
 by (Simp_tac 1);
-br (Even_lemma RS hoare_derivs.cut) 1;
-br BodyN 1;
+by (rtac (Even_lemma RS hoare_derivs.cut) 1);
+by (rtac BodyN 1);
 by (Simp_tac 1);
-br (Odd_lemma RS thin) 1;
+by (rtac (Odd_lemma RS thin) 1);
 by (Simp_tac 1);
 qed "Even_ok_N";
 
 Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
-br conseq1 1;
+by (rtac conseq1 1);
 by  (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"), 
       ("P","%pn. Z=Arg+(if pn = Odd then 1 else 0)"),
       ("Q","%pn. Res_ok")] Body1 1);
 by    Auto_tac;
-br hoare_derivs.insert 1;
-br  (Odd_lemma RS thin) 1;
+by (rtac hoare_derivs.insert 1);
+by (rtac (Odd_lemma RS thin) 1);
 by  (Simp_tac 1);
-br (Even_lemma RS thin) 1;
+by (rtac (Even_lemma RS thin) 1);
 by (Simp_tac 1);
 qed "Even_ok_S";