--- a/src/HOL/Algebra/abstract/NatSum.ML Mon Jan 22 11:46:25 2001 +0100
+++ b/src/HOL/Algebra/abstract/NatSum.ML Mon Jan 22 17:26:19 2001 +0100
@@ -17,8 +17,7 @@
Addsimps [SUM_0, SUM_Suc];
-Goal
- "SUM (Suc n) f = (SUM n (%i. f (Suc i)) + f 0::'a::ring)";
+Goal "SUM (Suc n) f = (SUM n (%i. f (Suc i)) + f 0::'a::ring)";
by (induct_tac "n" 1);
(* Base case *)
by (Simp_tac 1);
@@ -28,18 +27,11 @@
(* Congruence rules *)
-val [p_equal, p_context] = goal NatSum.thy
- "[| m = n; !!i. i <= n ==> f i = g i |] ==> SUM m f = (SUM n g::'a::ring)";
-by (simp_tac (simpset() addsimps [p_equal]) 1);
-by (cut_inst_tac [("n", "n")] le_refl 1);
-by (etac rev_mp 1);
-by (res_inst_tac [("P", "%k. k <= n --> SUM k f = SUM k g")] nat_induct 1);
-(* Base case *)
-by (simp_tac (simpset() addsimps [p_context]) 1);
-(* Induction step *)
-by (asm_simp_tac (simpset() addsimps [p_context]) 1);
-qed "SUM_cong";
-
+Goal "ALL j'. j=j' --> (ALL i. i<=j' --> f i = (f' i :: 'a :: ring)) \
+\ --> SUM j f = SUM j' f'";
+by (induct_tac "j" 1);
+by Auto_tac;
+bind_thm ("SUM_cong", (impI RS allI) RSN (2, result() RS spec RS mp RS mp));
Addcongs [SUM_cong];
(* Results needed for the development of polynomials *)
@@ -72,8 +64,7 @@
by (asm_simp_tac (simpset() addsimps [l_distr]) 1);
qed "SUM_ldistr";
-Goal
- "!!a::'a::ring. a * SUM n f = SUM n (%i. a * f i)";
+Goal "!!a::'a::ring. a * SUM n f = SUM n (%i. a * f i)";
by (induct_tac "n" 1);
(* Base case *)
by (Simp_tac 1);
@@ -110,12 +101,13 @@
Goal
"!! a::nat=>'a::ring. j <= n --> \
\ SUM j (%i. a i * b (n-i)) = SUM j (%i. a (n-i-(n-j)) * b (i+(n-j)))";
+by (Simp_tac 1);
by (induct_tac "j" 1);
(* Base case *)
by (Simp_tac 1);
(* Induction step *)
by (stac SUM_Suc2 1);
-by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, a_comm]) 1);
+by (asm_simp_tac (simpset() addsimps [a_comm]) 1);
qed "poly_comm_lemma1";
Goal
--- a/src/HOL/Algebra/poly/LongDiv.ML Mon Jan 22 11:46:25 2001 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.ML Mon Jan 22 17:26:19 2001 +0100
@@ -10,14 +10,13 @@
\ coeff (deg r) p = - (coeff (deg r) q); deg r ~= 0 |] ==> \
\ deg (p + q) < deg r";
by (res_inst_tac [("j", "deg r - 1")] le_less_trans 1);
+by (arith_tac 2);
by (rtac deg_aboveI 1);
by (strip_tac 1);
-by (dtac pred_less_imp_le 1);
by (case_tac "deg r = m" 1);
by (Clarify_tac 1);
by (Asm_full_simp_tac 1);
(* case "deg q ~= m" *)
-by (arith_tac 2);
by (subgoal_tac "deg p < m & deg q < m" 1);
by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
by (arith_tac 1);
--- a/src/HOL/Hoare/Examples.ML Mon Jan 22 11:46:25 2001 +0100
+++ b/src/HOL/Hoare/Examples.ML Mon Jan 22 17:26:19 2001 +0100
@@ -175,6 +175,10 @@
Ambiguity warnings of parser are due to := being used
both for assignment and list update.
*)
+Goal "m - 1 < n ==> m < Suc n";
+by (arith_tac 1);
+qed "lemma";
+
Goal
"[| leq == %A i. !k. k<i --> A!k <= pivot; \
\ geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==> \
@@ -198,8 +202,8 @@
by (hoare_tac Asm_full_simp_tac 1);
by (force_tac (claset(), simpset() addsimps [neq_Nil_conv]) 1);
by (blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
- by (blast_tac (claset() addSEs [less_SucE] addIs [less_imp_diff_less]
- addDs [pred_less_imp_le RS le_imp_less_Suc] ) 1);
+ by (blast_tac (claset() addSEs [less_SucE]
+ addIs [less_imp_diff_less] addDs [lemma]) 1);
by (force_tac (claset(), simpset() addsimps [nth_list_update]) 1);
by (auto_tac (claset() addIs [order_antisym], simpset()));
qed "Partition";
--- a/src/HOL/IMPP/Com.ML Mon Jan 22 11:46:25 2001 +0100
+++ b/src/HOL/IMPP/Com.ML Mon Jan 22 17:26:19 2001 +0100
@@ -1,11 +1,11 @@
val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
Goalw [body_def] "finite (dom body)";
-br finite_dom_map_of 1;
+by (rtac finite_dom_map_of 1);
qed "finite_dom_body";
Goalw [WT_bodies_def, body_def] "[| WT_bodies; body pn = Some b |] ==> WT b";
-bd map_of_SomeD 1;
+by (dtac map_of_SomeD 1);
by (Fast_tac 1);
qed "WT_bodiesD";
--- 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";
--- a/src/HOL/IMPP/Hoare.ML Mon Jan 22 11:46:25 2001 +0100
+++ b/src/HOL/IMPP/Hoare.ML Mon Jan 22 17:26:19 2001 +0100
@@ -50,62 +50,62 @@
Goal "[| G|-{P'}.c.{Q'}; !Z s. P Z s --> \
\ (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s') |] \
\ ==> G|-{P}.c.{Q}";
-br hoare_derivs.conseq 1;
+by (rtac hoare_derivs.conseq 1);
by (Blast_tac 1);
qed "conseq12";
Goal "[| G|-{P'}.c.{Q}; !Z s. P Z s --> P' Z s |] ==> G|-{P}.c.{Q}";
-be conseq12 1;
+by (etac conseq12 1);
by (Fast_tac 1);
qed "conseq1";
Goal "[| G|-{P}.c.{Q'}; !Z s. Q' Z s --> Q Z s |] ==> G|-{P}.c.{Q}";
-be conseq12 1;
+by (etac conseq12 1);
by (Fast_tac 1);
qed "conseq2";
Goal "[| G Un (%p. {P p}. BODY p .{Q p})`Procs \
\ ||- (%p. {P p}. the (body p) .{Q p})`Procs; \
\ pn:Procs |] ==> G|-{P pn}. BODY pn .{Q pn}";
-bd hoare_derivs.Body 1;
-be hoare_derivs.weaken 1;
+by (dtac hoare_derivs.Body 1);
+by (etac hoare_derivs.weaken 1);
by (Fast_tac 1);
qed "Body1";
Goal "(insert ({P}. BODY pn .{Q}) G) |-{P}. the (body pn) .{Q} ==> \
\ G|-{P}. BODY pn .{Q}";
-br Body1 1;
-br singletonI 2;
+by (rtac Body1 1);
+by (rtac singletonI 2);
by (Clarsimp_tac 1);
qed "BodyN";
Goal "[| !Z s. P Z s --> G|-{%Z s'. s'=s}.c.{%Z'. Q Z} |] ==> G|-{P}.c.{Q}";
-br hoare_derivs.conseq 1;
+by (rtac hoare_derivs.conseq 1);
by (Fast_tac 1);
qed "escape";
Goal "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}";
-br hoare_derivs.conseq 1;
+by (rtac hoare_derivs.conseq 1);
by (fast_tac (claset() addDs (premises())) 1);
qed "constant";
Goal "G|-{%Z s. P Z s & ~b s}.WHILE b DO c.{P}";
-br (hoare_derivs.Loop RS conseq2) 1;
+by (rtac (hoare_derivs.Loop RS conseq2) 1);
by (ALLGOALS Simp_tac);
-br hoare_derivs.conseq 1;
+by (rtac hoare_derivs.conseq 1);
by (Fast_tac 1);
qed "LoopF";
(*
Goal "[| G'||-ts; G' <= G |] ==> G||-ts";
-be hoare_derivs.cut 1;
-be hoare_derivs.asm 1;
+by (etac hoare_derivs.cut 1);
+by (etac hoare_derivs.asm 1);
qed "thin";
*)
Goal "G'||-ts ==> !G. G' <= G --> G||-ts";
by (etac hoare_derivs.induct 1);
by (ALLGOALS (EVERY'[Clarify_tac, REPEAT o smp_tac 1]));
-br hoare_derivs.empty 1;
+by (rtac hoare_derivs.empty 1);
by (eatac hoare_derivs.insert 1 1);
by (fast_tac (claset() addIs [hoare_derivs.asm]) 1);
by (fast_tac (claset() addIs [hoare_derivs.cut]) 1);
@@ -118,8 +118,8 @@
qed_spec_mp "thin";
Goal "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}";
-br BodyN 1;
-be thin 1;
+by (rtac BodyN 1);
+by (etac thin 1);
by Auto_tac;
qed "weak_Body";
@@ -130,10 +130,10 @@
Goal "[| finite U; \
\ !p. G |- {P' p}.c0 p.{Q' p} --> G |- {P p}.c0 p.{Q p} |] ==> \
\ G||-(%p. {P' p}.c0 p.{Q' p}) ` U --> G||-(%p. {P p}.c0 p.{Q p}) ` U";
-be finite_induct 1;
+by (etac finite_induct 1);
by (ALLGOALS Clarsimp_tac);
-bd derivs_insertD 1;
-br hoare_derivs.insert 1;
+by (dtac derivs_insertD 1);
+by (rtac hoare_derivs.insert 1);
by Auto_tac;
qed_spec_mp "finite_pointwise";
@@ -144,7 +144,7 @@
"G|={P &> b}. c .{P} ==> \
\ G|={P}. WHILE b DO c .{P &> (Not o b)}";
by (full_simp_tac (simpset() addsimps [triple_valid_def2]) 1);
-br allI 1;
+by (rtac allI 1);
by (subgoal_tac "!d s s'. <d,s> -n-> s' --> \
\ d = WHILE b DO c --> ||=n:G --> (!Z. P Z s --> P Z s' & ~b s')" 1);
by (EVERY'[etac thin_rl, Fast_tac] 1);
@@ -157,11 +157,11 @@
"[| G Un (%pn. {P pn}. BODY pn .{Q pn})`Procs \
\ ||=(%pn. {P pn}. the (body pn) .{Q pn})`Procs |] ==> \
\ G||=(%pn. {P pn}. BODY pn .{Q pn})`Procs";
-br allI 1;
+by (rtac allI 1);
by (induct_tac "n" 1);
by (fast_tac (claset() addIs [Body_triple_valid_0]) 1);
by (Clarsimp_tac 1);
-bd triples_valid_Suc 1;
+by (dtac triples_valid_Suc 1);
by (mp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
by (EVERY'[dtac spec, etac impE, etac conjI, atac] 1);
@@ -169,7 +169,7 @@
qed "Body_sound_lemma";
Goal "G||-ts ==> G||=ts";
-be hoare_derivs.induct 1;
+by (etac hoare_derivs.induct 1);
by (TRYALL (eresolve_tac [Loop_sound_lemma, Body_sound_lemma]
THEN_ALL_NEW atac));
by (rewtac hoare_valids_def);
@@ -196,25 +196,25 @@
(*unused*)
Goalw [MGT_def] "G|-MGT c ==> \
\ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1}";
-be conseq12 1;
+by (etac conseq12 1);
by Auto_tac;
qed "MGT_alternI";
(* requires com_det *)
Goalw [MGT_def] "state_not_singleton ==> \
\ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1} ==> G|-MGT c";
-be conseq12 1;
+by (etac conseq12 1);
by Auto_tac;
by (case_tac "? t. <c,?s> -c-> t" 1);
by (fast_tac (claset() addEs [com_det]) 1);
by (Clarsimp_tac 1);
-bd single_stateE 1;
+by (dtac single_stateE 1);
by (Blast_tac 1);
qed "MGT_alternD";
Goalw [MGT_def]
"{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}";
-be conseq12 1;
+by (etac conseq12 1);
by (clarsimp_tac (claset(), simpset() addsimps
[hoare_valids_def,eval_eq,triple_valid_def2]) 1);
qed "MGF_complete";
@@ -231,15 +231,15 @@
by (induct_tac "c" 1);
by (ALLGOALS Clarsimp_tac);
by (fast_tac (claset() addIs [domI]) 7);
-be MGT_alternD 6;
+by (etac MGT_alternD 6);
by (rewtac MGT_def);
by (EVERY'[dtac bspec, etac domI] 7);
by (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac
[("P1","%Z' s. s=(setlocs Z newlocs)[Loc Arg ::= fun Z]")]
(hoare_derivs.Call RS conseq1), etac conseq12] 7);
by (ALLGOALS (etac thin_rl));
-br (hoare_derivs.Skip RS conseq2) 1;
-br (hoare_derivs.Ass RS conseq1) 2;
+by (rtac (hoare_derivs.Skip RS conseq2) 1);
+by (rtac (hoare_derivs.Ass RS conseq1) 2);
by (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac
[("P1","%Z' s. s=(Z[Loc loc::=fun Z])")]
(hoare_derivs.Local RS conseq1), etac conseq12] 3);
@@ -264,11 +264,11 @@
by (asm_simp_tac (simpset() addsimps [card_seteq, finite_imageI]) 2);
by (Asm_full_simp_tac 1);
by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
-br ballI 1;
+by (rtac ballI 1);
by (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
by (Fast_tac 1);
by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
-br ballI 1;
+by (rtac ballI 1);
by (case_tac "mgt_call pn : G" 1);
by (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
by (Fast_tac 1);
@@ -276,31 +276,32 @@
byev[dtac spec 1, etac impE 1, etac impE 2, etac impE 3, dtac spec 4,etac mp 4];
by (eresolve_tac (tl(tl(tl(premises())))) 4);
by (Fast_tac 1);
-be Suc_leD 1;
-bd finite_subset 1;
-be finite_imageI 1;
-by (force_tac (claset() addEs [Suc_diff_Suc], simpset()) 1);
+by (etac Suc_leD 1);
+by (dtac finite_subset 1);
+by (etac finite_imageI 1);
+by (Asm_simp_tac 1);
+by (arith_tac 1);
qed_spec_mp "nesting_lemma";
Goalw [MGT_def] "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==> \
\ G|-{=}.BODY pn.{->}";
-br BodyN 1;
-be conseq2 1;
+by (rtac BodyN 1);
+by (etac conseq2 1);
by (Force_tac 1);
qed "MGT_BodyN";
(* requires BodyN, com_det *)
Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c";
by (res_inst_tac [("P","%G ts. G||-ts"),("U","dom body")] nesting_lemma 1);
-be hoare_derivs.asm 1;
-be MGT_BodyN 1;
-br finite_dom_body 3;
-be MGF_lemma1 1;
-ba 2;
+by (etac hoare_derivs.asm 1);
+by (etac MGT_BodyN 1);
+by (rtac finite_dom_body 3);
+by (etac MGF_lemma1 1);
+by (assume_tac 2);
by (Blast_tac 1);
by (Clarsimp_tac 1);
by (eatac WT_bodiesD 1 1);
-br le_refl 3;
+by (rtac le_refl 3);
by Auto_tac;
qed "MGF";
@@ -311,11 +312,11 @@
Goalw [MGT_def] "[| G Un (%pn. {=}. BODY pn .{->})`Procs \
\ ||-(%pn. {=}. the (body pn) .{->})`Procs; \
\ finite Procs |] ==> G ||-(%pn. {=}. BODY pn .{->})`Procs";
-br hoare_derivs.Body 1;
-be finite_pointwise 1;
-ba 2;
+by (rtac hoare_derivs.Body 1);
+by (etac finite_pointwise 1);
+by (assume_tac 2);
by (Clarify_tac 1);
-be conseq2 1;
+by (etac conseq2 1);
by Auto_tac;
qed "MGT_Body";
@@ -324,33 +325,33 @@
\ F<=(%pn. {=}.the (body pn).{->})`dom body |] ==> \
\ (%pn. {=}. BODY pn .{->})`dom body||-F";
by (ftac finite_subset 1);
-br (finite_dom_body RS finite_imageI) 1;
+by (rtac (finite_dom_body RS finite_imageI) 1);
by (rotate_tac 2 1);
by (make_imp_tac 1);
-be finite_induct 1;
+by (etac finite_induct 1);
by (ALLGOALS (clarsimp_tac (
claset() addSIs [hoare_derivs.empty,hoare_derivs.insert],
simpset() delsimps [range_composition])));
-be MGF_lemma1 1;
+by (etac MGF_lemma1 1);
by (fast_tac (claset() addDs [WT_bodiesD]) 2);
by (Clarsimp_tac 1);
-br hoare_derivs.asm 1;
+by (rtac hoare_derivs.asm 1);
by (fast_tac (claset() addIs [domI]) 1);
qed_spec_mp "MGF_lemma2_simult";
(* requires Body, empty, insert, com_det *)
Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c";
-br MGF_lemma1 1;
-ba 1;
-ba 2;
+by (rtac MGF_lemma1 1);
+by (assume_tac 1);
+by (assume_tac 2);
by (Clarsimp_tac 1);
by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})`dom body" 1);
-be hoare_derivs.weaken 1;
+by (etac hoare_derivs.weaken 1);
by (fast_tac (claset() addIs [domI]) 1);
-br (finite_dom_body RSN (2,MGT_Body)) 1;
+by (rtac (finite_dom_body RSN (2,MGT_Body)) 1);
by (Simp_tac 1);
by (eatac MGF_lemma2_simult 1 1);
-br subset_refl 1;
+by (rtac subset_refl 1);
qed "MGF";
(* requires Body+empty+insert / BodyN, com_det *)
@@ -359,24 +360,24 @@
section "unused derived rules";
Goal "G|-{%Z s. False}.c.{Q}";
-br hoare_derivs.conseq 1;
+by (rtac hoare_derivs.conseq 1);
by (Fast_tac 1);
qed "falseE";
Goal "G|-{P}.c.{%Z s. True}";
-br hoare_derivs.conseq 1;
+by (rtac hoare_derivs.conseq 1);
by (fast_tac (claset() addSIs [falseE]) 1);
qed "trueI";
Goal "[| G|-{P}.c.{Q}; G|-{P'}.c.{Q'} |] \
\ ==> G|-{%Z s. P Z s | P' Z s}.c.{%Z s. Q Z s | Q' Z s}";
-br hoare_derivs.conseq 1;
+by (rtac hoare_derivs.conseq 1);
by (fast_tac (claset() addEs [conseq12]) 1);
qed "disj"; (* analogue conj non-derivable *)
Goal "(!Z s. P Z s --> Q Z s) ==> G|-{P}. SKIP .{Q}";
-br conseq12 1;
-br hoare_derivs.Skip 1;
+by (rtac conseq12 1);
+by (rtac hoare_derivs.Skip 1);
by (Fast_tac 1);
qed "hoare_SkipI";
@@ -384,12 +385,12 @@
section "useful derived rules";
Goal "{t}|-t";
-br hoare_derivs.asm 1;
-br subset_refl 1;
+by (rtac hoare_derivs.asm 1);
+by (rtac subset_refl 1);
qed "single_asm";
Goal "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}";
-br hoare_derivs.conseq 1;
+by (rtac hoare_derivs.conseq 1);
by (Clarsimp_tac 1);
by (cut_facts_tac (premises()) 1);
by (Fast_tac 1);
@@ -398,9 +399,9 @@
Goal "[| G|-{P}. c .{Q}; !k Z s. Q Z s --> Q Z (s[Loc Y::=k]) |] ==> \
\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{Q}";
-br export_s 1;
-br hoare_derivs.Local 1;
-be conseq2 1;
-be spec 1;
+by (rtac export_s 1);
+by (rtac hoare_derivs.Local 1);
+by (etac conseq2 1);
+by (etac spec 1);
qed "weak_Local";
--- a/src/HOL/IMPP/Misc.ML Mon Jan 22 11:46:25 2001 +0100
+++ b/src/HOL/IMPP/Misc.ML Mon Jan 22 17:26:19 2001 +0100
@@ -47,7 +47,7 @@
Goal "getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])";
by (induct_tac "Y" 1);
-br ext 2;
+by (rtac ext 2);
by Auto_tac;
qed "getlocs_setlocs_lemma";
@@ -59,7 +59,7 @@
by (Clarsimp_tac 1);
by (dres_inst_tac [("x","s<Y>")] spec 1);
by (smp_tac 1 1);
-bd spec 1;
+by (dtac spec 1);
by (dres_inst_tac [("x","s[Loc Y::=a s]")] spec 1);
by (Full_simp_tac 1);
by (mp_tac 1);
@@ -69,56 +69,56 @@
Goal "!v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. \
\ c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}";
-br export_s 1;
+by (rtac export_s 1);
(*variant 1*)
-br (hoare_derivs.Local RS conseq1) 1;
-be spec 1;
+by (rtac (hoare_derivs.Local RS conseq1) 1);
+by (etac spec 1);
by (Force_tac 1);
(*variant 2
by (res_inst_tac [("P'","%Z s. s' = s & P Z (s[Loc Y::=a s][Loc Y::=s'<Y>]) & (s[Loc Y::=a s])<Y> = a (s[Loc Y::=a s][Loc Y::=s'<Y>])")] conseq1 1);
by (Clarsimp_tac 2);
-br hoare_derivs.Local 1;
-be spec 1;
+by (rtac hoare_derivs.Local 1);
+by (etac spec 1);
*)
qed "classic_Local";
Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'>=d} |] ==> \
\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'>=d}";
-br classic_Local 1;
+by (rtac classic_Local 1);
by (ALLGOALS Clarsimp_tac);
-be conseq12 1;
+by (etac conseq12 1);
by (Clarsimp_tac 1);
-bd sym 1;
+by (dtac sym 1);
by (Asm_full_simp_tac 1);
qed "classic_Local_indep";
Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'>=d} |] ==> \
\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'>=d}";
-br export_s 1;
-br hoare_derivs.Local 1;
+by (rtac export_s 1);
+by (rtac hoare_derivs.Local 1);
by (Clarsimp_tac 1);
qed "Local_indep";
Goal "[| Y'~=Y; G|-{P}. c .{%Z s. s<Y'>=d} |] ==> \
\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'>=d}";
-br weak_Local 1;
+by (rtac weak_Local 1);
by (ALLGOALS Clarsimp_tac);
qed "weak_Local_indep";
Goal "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}";
-br export_s 1;
+by (rtac export_s 1);
by (res_inst_tac [("P'","%Z s. s'=s & True"), ("Q'","%Z s. s'<Y> = s<Y>")] (conseq12) 1);
by (Clarsimp_tac 2);
-br hoare_derivs.Local 1;
+by (rtac hoare_derivs.Local 1);
by (Clarsimp_tac 1);
-br trueI 1;
+by (rtac trueI 1);
qed "export_Local_invariant";
Goal "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}";
-br classic_Local 1;
+by (rtac classic_Local 1);
by (Clarsimp_tac 1);
-br (trueI RS conseq12) 1;
+by (rtac (trueI RS conseq12) 1);
by (Clarsimp_tac 1);
qed "classic_Local_invariant";
--- a/src/HOL/IMPP/Natural.ML Mon Jan 22 11:46:25 2001 +0100
+++ b/src/HOL/IMPP/Natural.ML Mon Jan 22 17:26:19 2001 +0100
@@ -25,14 +25,14 @@
(* evaluation of com is deterministic *)
Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
-be evalc.induct 1;
+by (etac evalc.induct 1);
by (thin_tac "<?c,s1> -c-> s2" 8);
(*blast_tac needs Unify.search_bound := 40*)
by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
qed_spec_mp "com_det";
Goal "<c,s> -n-> t ==> <c,s> -c-> t";
-be evaln.induct 1;
+by (etac evaln.induct 1);
by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac));
qed "evaln_evalc";
@@ -49,13 +49,13 @@
qed "Suc_le_D_lemma";
Goal "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t";
-be evaln.induct 1;
+by (etac evaln.induct 1);
by (ALLGOALS (EVERY'[strip_tac,TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1]));
by (ALLGOALS (resolve_tac evaln.intrs THEN_ALL_NEW atac));
qed_spec_mp "evaln_nonstrict";
Goal "<c,s> -n-> s' ==> <c,s> -Suc n-> s'";
-be evaln_nonstrict 1;
+by (etac evaln_nonstrict 1);
by Auto_tac;
qed "evaln_Suc";
@@ -66,7 +66,7 @@
qed "evaln_max2";
Goal "<c,s> -c-> t ==> ? n. <c,s> -n-> t";
-be evalc.induct 1;
+by (etac evalc.induct 1);
by (ALLGOALS (REPEAT o etac exE));
by (TRYALL(EVERY'[datac evaln_max2 1, REPEAT o eresolve_tac [exE, conjE]]));
by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intrs THEN_ALL_NEW atac));
--- a/src/HOL/NatArith.ML Mon Jan 22 11:46:25 2001 +0100
+++ b/src/HOL/NatArith.ML Mon Jan 22 17:26:19 2001 +0100
@@ -40,10 +40,6 @@
by (arith_tac 1);
qed "le_diff_conv2";
-Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
-by (arith_tac 1);
-qed "Suc_diff_Suc";
-
Goal "i <= (n::nat) ==> n - (n - i) = i";
by (arith_tac 1);
qed "diff_diff_cancel";
@@ -53,60 +49,12 @@
by (arith_tac 1);
qed "le_add_diff";
-Goal "m-1 < n ==> m <= n";
-by (arith_tac 1);
-qed "pred_less_imp_le";
-
-Goal "j<=i ==> i - j < Suc i - j";
-by (arith_tac 1);
-qed "diff_less_Suc_diff";
-
-Goal "i - j <= Suc i - j";
-by (arith_tac 1);
-qed "diff_le_Suc_diff";
-AddIffs [diff_le_Suc_diff];
-
-Goal "n - Suc i <= n - i";
-by (arith_tac 1);
-qed "diff_Suc_le_diff";
-AddIffs [diff_Suc_le_diff];
-
-Goal "!!m::nat. 0 < n ==> (m <= n-1) = (m<n)";
-by (arith_tac 1);
-qed "le_pred_eq";
-
-Goal "!!m::nat. 0 < n ==> (m-1 < n) = (m<=n)";
-by (arith_tac 1);
-qed "less_pred_eq";
-
(*Replaces the previous diff_less and le_diff_less, which had the stronger
second premise n<=m*)
Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m";
by (arith_tac 1);
qed "diff_less";
-Goal "j <= (k::nat) ==> (j+i)-k = i-(k-j)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_add_assoc_diff";
-
-
-(*** Reducing subtraction to addition ***)
-
-Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
-by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed_spec_mp "Suc_diff_add_le";
-
-Goal "i<n ==> n - Suc i < n - i";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_Suc_less_diff";
-
-Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
-by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "if_Suc_diff_le";
-
-Goal "Suc(m)-n <= Suc(m-n)";
-by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_Suc_le_Suc_diff";
(** Simplification of relational expressions involving subtraction **)