--- a/src/HOL/Arith.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Arith.ML Wed Apr 09 12:32:04 1997 +0200
@@ -50,7 +50,7 @@
by (etac rev_mp 1);
by (nat_ind_tac "k" 1);
by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
val lemma = result();
(* [| 0 < k; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
@@ -247,7 +247,7 @@
(*In ordinary notation: if 0<n and n<=m then m-n < m *)
goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc])));
qed "diff_less";
@@ -335,7 +335,7 @@
goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
-by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Fast_tac));
+by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Blast_tac));
qed "zero_induct_lemma";
val prems = goal Arith.thy "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
@@ -385,7 +385,7 @@
by (subgoal_tac "k mod 2 < 2" 1);
by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "mod2_cases";
goal thy "Suc(Suc(m)) mod 2 = m mod 2";
@@ -452,7 +452,7 @@
by (etac rev_mp 1);
by (nat_ind_tac "j" 1);
by (ALLGOALS Asm_simp_tac);
-by (fast_tac (!claset addDs [Suc_lessD]) 1);
+by (blast_tac (!claset addDs [Suc_lessD]) 1);
qed "add_lessD1";
goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
@@ -468,7 +468,7 @@
goal Arith.thy "m+k<=n --> m<=(n::nat)";
by (nat_ind_tac "k" 1);
by (ALLGOALS Asm_simp_tac);
-by (fast_tac (!claset addDs [Suc_leD]) 1);
+by (blast_tac (!claset addDs [Suc_leD]) 1);
qed_spec_mp "add_leD1";
goal Arith.thy "!!n::nat. m+k<=n ==> k<=n";
@@ -477,7 +477,7 @@
qed_spec_mp "add_leD2";
goal Arith.thy "!!n::nat. m+k<=n ==> m<=n & k<=n";
-by (fast_tac (!claset addDs [add_leD1, add_leD2]) 1);
+by (blast_tac (!claset addDs [add_leD1, add_leD2]) 1);
bind_thm ("add_leE", result() RS conjE);
goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
@@ -513,7 +513,7 @@
\ |] ==> f(i) <= (f(j)::nat)";
by (cut_facts_tac [le] 1);
by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
-by (fast_tac (!claset addSIs [lt_mono]) 1);
+by (blast_tac (!claset addSIs [lt_mono]) 1);
qed "less_mono_imp_le_mono";
(*non-strict, in 1st argument*)
--- a/src/HOL/Auth/Message.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Auth/Message.ML Wed Apr 09 12:32:04 1997 +0200
@@ -188,7 +188,7 @@
Addsimps [parts_Un, parts_UN, parts_UN1];
goal thy "insert X (parts H) <= parts(insert X H)";
-by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1);
+by (blast_tac (!claset addIs [impOfSubs parts_mono]) 1);
qed "parts_insert_subset";
(** Idempotence and transitivity **)
@@ -196,8 +196,8 @@
goal thy "!!H. X: parts (parts H) ==> X: parts H";
by (etac parts.induct 1);
by (ALLGOALS Blast_tac);
-qed "parts_partsE";
-AddSDs [parts_partsE];
+qed "parts_partsD";
+AddSDs [parts_partsD];
goal thy "parts (parts H) = parts H";
by (Blast_tac 1);
@@ -255,7 +255,7 @@
by (etac parts.induct 1);
by (Auto_tac());
by (etac parts.induct 1);
-by (ALLGOALS (best_tac (!claset addIs [parts.Body])));
+by (ALLGOALS (blast_tac (!claset addIs [parts.Body])));
qed "parts_insert_Crypt";
goal thy "parts (insert {|X,Y|} H) = \
@@ -265,7 +265,7 @@
by (etac parts.induct 1);
by (Auto_tac());
by (etac parts.induct 1);
-by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd])));
+by (ALLGOALS (blast_tac (!claset addIs [parts.Fst, parts.Snd])));
qed "parts_insert_MPair";
Addsimps [parts_insert_Agent, parts_insert_Nonce, parts_insert_Key,
@@ -350,7 +350,7 @@
qed "analz_Un";
goal thy "insert X (analz H) <= analz(insert X H)";
-by (fast_tac (!claset addEs [impOfSubs analz_mono]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
qed "analz_insert";
(** Rewrite rules for pulling out atomic messages **)
@@ -386,7 +386,7 @@
by (etac analz.induct 1);
by (Auto_tac());
by (etac analz.induct 1);
-by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd]) 0));
+by (ALLGOALS (blast_tac (!claset addIs [analz.Fst, analz.Snd])));
qed "analz_insert_MPair";
(*Can pull out enCrypted message if the Key is not known*)
@@ -410,7 +410,7 @@
by (Auto_tac());
by (eres_inst_tac [("za","x")] analz.induct 1);
by (Auto_tac());
-by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD,
+by (blast_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD,
analz.Decrypt]) 1);
val lemma2 = result();
@@ -459,8 +459,8 @@
goal thy "!!H. X: analz (analz H) ==> X: analz H";
by (etac analz.induct 1);
by (ALLGOALS Blast_tac);
-qed "analz_analzE";
-AddSDs [analz_analzE];
+qed "analz_analzD";
+AddSDs [analz_analzD];
goal thy "analz (analz H) = analz H";
by (Blast_tac 1);
@@ -515,12 +515,11 @@
(*Helps to prove Fake cases*)
goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)";
by (etac analz.induct 1);
-by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono])));
+by (ALLGOALS (blast_tac (!claset addIs [impOfSubs analz_mono])));
val lemma = result();
goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)";
-by (fast_tac (!claset addIs [lemma]
- addEs [impOfSubs analz_mono]) 1);
+by (blast_tac (!claset addIs [lemma, impOfSubs analz_mono]) 1);
qed "analz_UN_analz";
Addsimps [analz_UN_analz];
@@ -561,7 +560,7 @@
qed "synth_Un";
goal thy "insert X (synth H) <= synth(insert X H)";
-by (fast_tac (!claset addEs [impOfSubs synth_mono]) 1);
+by (blast_tac (!claset addIs [impOfSubs synth_mono]) 1);
qed "synth_insert";
(** Idempotence and transitivity **)
@@ -569,8 +568,8 @@
goal thy "!!H. X: synth (synth H) ==> X: synth H";
by (etac synth.induct 1);
by (ALLGOALS Blast_tac);
-qed "synth_synthE";
-AddSDs [synth_synthE];
+qed "synth_synthD";
+AddSDs [synth_synthD];
goal thy "synth (synth H) = synth H";
by (Blast_tac 1);
@@ -620,7 +619,7 @@
by (rtac subsetI 1);
by (etac parts.induct 1);
by (ALLGOALS
- (best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD)
+ (blast_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD)
::parts.intrs))));
qed "parts_synth";
Addsimps [parts_synth];
@@ -634,9 +633,8 @@
by (rtac equalityI 1);
by (rtac subsetI 1);
by (etac analz.induct 1);
-by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 5);
-(*Strange that best_tac just can't hack this one...*)
-by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0));
+by (blast_tac (!claset addIs [impOfSubs analz_mono]) 5);
+by (ALLGOALS (blast_tac (!claset addIs analz.intrs)));
qed "analz_synth_Un";
goal thy "analz (synth H) = analz H Un synth H";
@@ -651,8 +649,8 @@
by (rtac equalityI 1);
by (rtac subsetI 1);
by (etac analz.induct 1);
-by (best_tac
- (!claset addEs [impOfSubs synth_increasing,
+by (blast_tac
+ (!claset addIs [impOfSubs synth_increasing,
impOfSubs analz_mono]) 5);
by (Blast_tac 1);
by (blast_tac (!claset addIs [analz.Inj RS analz.Fst]) 1);
@@ -691,8 +689,8 @@
\ analz (insert X H) <= synth (analz G) Un analz (G Un H)";
by (rtac subsetI 1);
by (subgoal_tac "x : analz (synth (analz G) Un H)" 1);
-by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
- addSEs [impOfSubs analz_mono]) 2);
+by (blast_tac (!claset addIs [impOfSubs analz_mono,
+ impOfSubs (analz_mono RS synth_mono)]) 2);
by (Full_simp_tac 1);
by (Blast_tac 1);
qed "Fake_analz_insert";
--- a/src/HOL/Auth/Shared.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Auth/Shared.ML Wed Apr 09 12:32:04 1997 +0200
@@ -424,5 +424,5 @@
goal thy
"!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H) ==> \
\ (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
-by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
qed "analz_image_freshK_lemma";
--- a/src/HOL/Finite.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Finite.ML Wed Apr 09 12:32:04 1997 +0200
@@ -16,7 +16,7 @@
qed "Fin_mono";
goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
-by (fast_tac (!claset addSIs [lfp_lowerbound]) 1);
+by (blast_tac (!claset addSIs [lfp_lowerbound]) 1);
qed "Fin_subset_Pow";
(* A : Fin(B) ==> A <= B *)
@@ -55,7 +55,7 @@
qed "Fin_subset";
goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
-by (fast_tac (!claset addIs [Fin_UnI] addDs
+by (blast_tac (!claset addIs [Fin_UnI] addDs
[Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
qed "subset_Fin";
Addsimps[subset_Fin];
@@ -63,7 +63,7 @@
goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
by (stac insert_is_Un 1);
by (Simp_tac 1);
-by (fast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
+by (blast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
qed "insert_Fin";
Addsimps[insert_Fin];
@@ -163,7 +163,7 @@
section "Finite cardinality -- 'card'";
goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
-by (Fast_tac 1);
+by (Blast_tac 1);
val Collect_conv_insert = result();
goalw Finite.thy [card_def] "card {} = 0";
@@ -197,7 +197,7 @@
by (case_tac "? a. a:A" 1);
by (res_inst_tac [("x","0")] exI 2);
by (Simp_tac 2);
- by (Fast_tac 2);
+ by (Blast_tac 2);
by (etac exE 1);
by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
by (rtac exI 1);
@@ -205,47 +205,47 @@
by (etac equalityE 1);
by (asm_full_simp_tac
(!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
-by (SELECT_GOAL(safe_tac (!claset))1);
+by (safe_tac (!claset));
by (Asm_full_simp_tac 1);
by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
by (SELECT_GOAL(safe_tac (!claset))1);
by (subgoal_tac "x ~= f m" 1);
- by (Fast_tac 2);
+ by (Blast_tac 2);
by (subgoal_tac "? k. f k = x & k<m" 1);
- by (best_tac (!claset) 2);
+ by (Blast_tac 2);
by (SELECT_GOAL(safe_tac (!claset))1);
by (res_inst_tac [("x","k")] exI 1);
by (Asm_simp_tac 1);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
- by (best_tac (!claset) 1);
+ by (Blast_tac 1);
bd sym 1;
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
by (SELECT_GOAL(safe_tac (!claset))1);
by (subgoal_tac "x ~= f m" 1);
- by (Fast_tac 2);
+ by (Blast_tac 2);
by (subgoal_tac "? k. f k = x & k<m" 1);
- by (best_tac (!claset) 2);
+ by (Blast_tac 2);
by (SELECT_GOAL(safe_tac (!claset))1);
by (res_inst_tac [("x","k")] exI 1);
by (Asm_simp_tac 1);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
- by (best_tac (!claset) 1);
+ by (Blast_tac 1);
by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
by (SELECT_GOAL(safe_tac (!claset))1);
by (subgoal_tac "x ~= f i" 1);
- by (Fast_tac 2);
+ by (Blast_tac 2);
by (case_tac "x = f m" 1);
by (res_inst_tac [("x","i")] exI 1);
by (Asm_simp_tac 1);
by (subgoal_tac "? k. f k = x & k<m" 1);
- by (best_tac (!claset) 2);
+ by (Blast_tac 2);
by (SELECT_GOAL(safe_tac (!claset))1);
by (res_inst_tac [("x","k")] exI 1);
by (Asm_simp_tac 1);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (best_tac (!claset) 1);
+by (Blast_tac 1);
val lemma = result();
goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
@@ -303,8 +303,8 @@
by (Asm_simp_tac 1);
by (rtac card_insert_disjoint 1);
by (rtac (major RSN (2,finite_subset)) 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
qed "card_insert";
Addsimps [card_insert];
--- a/src/HOL/Fun.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Fun.ML Wed Apr 09 12:32:04 1997 +0200
@@ -99,11 +99,9 @@
(*** Lemmas about inj ***)
-val prems = goalw Fun.thy [o_def]
- "[| inj(f); inj_onto g (range f) |] ==> inj(g o f)";
-by (cut_facts_tac prems 1);
-by (fast_tac (!claset addIs [injI]
- addEs [injD,inj_ontoD]) 1);
+goalw Fun.thy [o_def]
+ "!!f g. [| inj(f); inj_onto g (range f) |] ==> inj(g o f)";
+by (fast_tac (!claset addIs [injI] addEs [injD, inj_ontoD]) 1);
qed "comp_inj";
val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
--- a/src/HOL/Lambda/Commutation.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Lambda/Commutation.ML Wed Apr 09 12:32:04 1997 +0200
@@ -94,6 +94,6 @@
rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
by (etac rtrancl_induct 1);
by (Blast_tac 1);
-by (slow_best_tac (!claset addIs [r_into_rtrancl]
- addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
+by (blast_tac (!claset delrules [rtrancl_refl]
+ addIs [r_into_rtrancl, rtrancl_trans]) 1);
qed "Church_Rosser_confluent";
--- a/src/HOL/Lambda/Eta.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Lambda/Eta.ML Wed Apr 09 12:32:04 1997 +0200
@@ -80,10 +80,9 @@
by (etac eta.induct 1);
by (slow_tac (!claset addIs [subst_not_free,eta_subst]
addIs [free_eta RS iffD1] addss !simpset) 1);
-by (slow_tac (!claset) 1);
-by (slow_tac (!claset) 1);
-by (slow_tac (!claset addSIs [eta_subst]
- addIs [free_eta RS iffD1]) 1);
+by (safe_tac (!claset));
+by (blast_tac (!claset addSIs [eta_subst] addIs [free_eta RS iffD1]) 5);
+by (ALLGOALS Blast_tac);
qed "square_eta";
goal Eta.thy "confluent(eta)";
@@ -108,8 +107,8 @@
qed "rtrancl_eta_AppR";
goal Eta.thy "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
-by (deepen_tac (!claset addSIs [rtrancl_eta_AppL,rtrancl_eta_AppR]
- addIs [rtrancl_trans]) 2 1);
+by (blast_tac (!claset addSIs [rtrancl_eta_AppL, rtrancl_eta_AppR]
+ addIs [rtrancl_trans]) 1);
qed "rtrancl_eta_App";
section "Commutation of -> and -e>";
@@ -152,8 +151,9 @@
by (etac beta.induct 1);
by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_subst,eta_subst]
addss !simpset) 1);
-by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
-by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
+by (Blast.depth_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 6 1);
+by (Blast.depth_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 6 1);
+(*23 seconds?*)
by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Abs,free_beta]
addss !simpset) 1);
qed "square_beta_eta";
--- a/src/HOL/Lambda/Lambda.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Lambda/Lambda.ML Wed Apr 09 12:32:04 1997 +0200
@@ -38,8 +38,8 @@
qed "rtrancl_beta_AppR";
goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
-by (deepen_tac (!claset addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
- addIs [rtrancl_trans]) 3 1);
+by (blast_tac (!claset addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
+ addIs [rtrancl_trans]) 1);
qed "rtrancl_beta_App";
AddIs [rtrancl_beta_App];
@@ -90,8 +90,8 @@
by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
setloop (split_tac [expand_if])
addSolver cut_trans_tac)));
-by(safe_tac (HOL_cs addSEs [nat_neqE]));
-by(ALLGOALS trans_tac);
+by (safe_tac (HOL_cs addSEs [nat_neqE]));
+by (ALLGOALS trans_tac);
qed "lift_subst_lt";
goal Lambda.thy "!k s. (lift t k)[s/k] = t";
@@ -108,8 +108,8 @@
(!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
setloop (split_tac [expand_if,expand_nat_case])
addSolver cut_trans_tac)));
-by(safe_tac (HOL_cs addSEs [nat_neqE]));
-by(ALLGOALS trans_tac);
+by (safe_tac (HOL_cs addSEs [nat_neqE]));
+by (ALLGOALS trans_tac);
qed_spec_mp "subst_subst";
--- a/src/HOL/Lambda/ParRed.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Lambda/ParRed.ML Wed Apr 09 12:32:04 1997 +0200
@@ -43,8 +43,10 @@
by (rtac subsetI 1);
by (split_all_tac 1);
by (etac par_beta.induct 1);
-by (ALLGOALS (slow_best_tac (!claset addIs [rtrancl_into_rtrancl]
- addEs [rtrancl_trans])));
+by (Blast_tac 1);
+(* rtrancl_refl complicates the proof by increasing the branching factor*)
+by (ALLGOALS (blast_tac (!claset delrules [rtrancl_refl]
+ addIs [rtrancl_into_rtrancl])));
qed "par_beta_subset_beta";
(*** => ***)
@@ -72,7 +74,7 @@
goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
by (rtac (impI RS allI RS allI) 1);
by (etac par_beta.induct 1);
-by (ALLGOALS(Blast.depth_tac (!claset addSIs [par_beta_subst]) 7));
+by (ALLGOALS(blast_tac (!claset addSIs [par_beta_subst])));
qed "diamond_par_beta";
@@ -90,7 +92,7 @@
(*** Confluence (via cd) ***)
goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
-by (blast_tac (HOL_cs addIs [par_beta_cd]) 1);
+by (blast_tac (!claset addIs [par_beta_cd]) 1);
qed "diamond_par_beta2";
goal ParRed.thy "confluent(beta)";
--- a/src/HOL/NatDef.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/NatDef.ML Wed Apr 09 12:32:04 1997 +0200
@@ -278,7 +278,7 @@
qed "less_SucE";
goal thy "(m < Suc(n)) = (m < n | m = n)";
-by (fast_tac (!claset addEs [less_trans, less_SucE]) 1);
+by (fast_tac (!claset addEs [less_trans, less_SucE]) 1);
qed "less_Suc_eq";
val prems = goal thy "m<n ==> n ~= 0";
--- a/src/HOL/RelPow.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/RelPow.ML Wed Apr 09 12:32:04 1997 +0200
@@ -17,14 +17,14 @@
goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "rel_pow_Suc_I";
goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n --> (x,z):R^(Suc n)";
by (nat_ind_tac "n" 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "rel_pow_Suc_I2";
goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
@@ -53,8 +53,8 @@
goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
by (nat_ind_tac "n" 1);
-by (fast_tac (!claset addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
-by (fast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (blast_tac (!claset addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (blast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
qed_spec_mp "rel_pow_Suc_D2";
@@ -86,13 +86,14 @@
goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
by (split_all_tac 1);
by (etac rtrancl_induct 1);
-by (ALLGOALS (fast_tac (!claset addIs [rel_pow_0_I,rel_pow_Suc_I])));
+by (ALLGOALS (blast_tac (!claset addIs [rel_pow_0_I,rel_pow_Suc_I])));
qed "rtrancl_imp_UN_rel_pow";
goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
by (nat_ind_tac "n" 1);
-by (fast_tac (!claset addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
-by (fast_tac (!claset addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
+by (blast_tac (!claset addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
+by (blast_tac (!claset addEs [rel_pow_Suc_E]
+ addIs [rtrancl_into_rtrancl]) 1);
val lemma = result() RS spec RS mp;
goal RelPow.thy "!!p. p:R^n ==> p:R^*";
--- a/src/HOL/Sum.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Sum.ML Wed Apr 09 12:32:04 1997 +0200
@@ -185,7 +185,7 @@
qed "Part_subset";
goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_mono";
val basic_monos = basic_monos @ [Part_mono];
@@ -199,10 +199,10 @@
qed "Part_id";
goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_Int";
(*For inductive definitions*)
goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_Collect";
--- a/src/HOL/Trancl.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Trancl.ML Wed Apr 09 12:32:04 1997 +0200
@@ -80,7 +80,7 @@
goalw Trancl.thy [trans_def] "trans(r^*)";
by (safe_tac (!claset));
by (eres_inst_tac [("b","z")] rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS(blast_tac (!claset addIs [rtrancl_into_rtrancl])));
qed "trans_rtrancl";
bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
@@ -110,7 +110,7 @@
by (rtac iffI 1);
by (etac rtrancl_induct 1);
by (rtac rtrancl_refl 1);
-by (fast_tac (!claset addEs [rtrancl_trans]) 1);
+by (blast_tac (!claset addIs [rtrancl_trans]) 1);
by (etac r_into_rtrancl 1);
qed "rtrancl_idemp";
Addsimps [rtrancl_idemp];
@@ -128,13 +128,13 @@
qed "rtrancl_subset";
goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
-by (best_tac (!claset addSIs [rtrancl_subset]
- addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
+by (blast_tac (!claset addSIs [rtrancl_subset]
+ addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
qed "rtrancl_Un_rtrancl";
goal Trancl.thy "(R^=)^* = R^*";
-by (fast_tac (!claset addSIs [rtrancl_refl,rtrancl_subset]
- addIs [r_into_rtrancl]) 1);
+by (blast_tac (!claset addSIs [rtrancl_subset]
+ addIs [rtrancl_refl, r_into_rtrancl]) 1);
qed "rtrancl_reflcl";
Addsimps [rtrancl_reflcl];
@@ -142,14 +142,14 @@
by (rtac converseI 1);
by (etac rtrancl_induct 1);
by (rtac rtrancl_refl 1);
-by (deepen_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 0 1);
+by (blast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
qed "rtrancl_converseD";
goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
by (dtac converseD 1);
by (etac rtrancl_induct 1);
by (rtac rtrancl_refl 1);
-by (deepen_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 0 1);
+by (blast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
qed "rtrancl_converseI";
goal Trancl.thy "(converse r)^* = converse(r^*)";
@@ -241,7 +241,7 @@
by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
by (etac rtranclE 1);
by (Blast_tac 1);
-by (fast_tac (!claset addSIs [rtrancl_into_trancl1]) 1);
+by (blast_tac (!claset addSIs [rtrancl_into_trancl1]) 1);
qed "tranclE";
(*Transitivity of r^+.
--- a/src/HOL/equalities.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/equalities.ML Wed Apr 09 12:32:04 1997 +0200
@@ -30,7 +30,7 @@
qed "insert_is_Un";
goal Set.thy "insert a A ~= {}";
-by (fast_tac (!claset addEs [equalityCE]) 1);
+by (blast_tac (!claset addEs [equalityCE]) 1);
qed"insert_not_empty";
Addsimps[insert_not_empty];
@@ -152,11 +152,11 @@
qed "Int_Un_distrib2";
goal Set.thy "(A<=B) = (A Int B = A)";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
qed "subset_Int_eq";
goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
-by (fast_tac (!claset addEs [equalityCE]) 1);
+by (blast_tac (!claset addEs [equalityCE]) 1);
qed "Int_UNIV";
Addsimps[Int_UNIV];
@@ -213,7 +213,7 @@
qed "Un_Int_crazy";
goal Set.thy "(A<=B) = (A Un B = B)";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
qed "subset_Un_eq";
goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
@@ -221,7 +221,7 @@
qed "subset_insert_iff";
goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
-by (fast_tac (!claset addEs [equalityCE]) 1);
+by (blast_tac (!claset addEs [equalityCE]) 1);
qed "Un_empty";
Addsimps[Un_empty];
@@ -260,7 +260,7 @@
(*Halmos, Naive Set Theory, page 16.*)
goal Set.thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
qed "Un_Int_assoc_eq";
@@ -292,7 +292,7 @@
val prems = goal Set.thy
"(Union(C) Int A = {}) = (! B:C. B Int A = {})";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
qed "Union_disjoint";
section "Inter";
@@ -517,8 +517,8 @@
qed "insert_Diff1";
Addsimps [insert_Diff1];
-val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A";
-by (fast_tac (!claset addSIs prems) 1);
+goal Set.thy "!!a. a:A ==> insert a (A-{a}) = A";
+by (Blast_tac 1);
qed "insert_Diff";
goal Set.thy "A Int (B-A) = {}";
--- a/src/HOL/ex/cla.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/ex/cla.ML Wed Apr 09 12:32:04 1997 +0200
@@ -424,7 +424,7 @@
\ (!x. hates agatha x --> hates butler x) & \
\ (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
\ killed ?who agatha";
-by (Blast_tac 1);
+by (Fast_tac 1);
result();
writeln"Problem 56";
--- a/src/HOL/mono.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/mono.ML Wed Apr 09 12:32:04 1997 +0200
@@ -7,62 +7,62 @@
*)
goal Set.thy "!!A B. A<=B ==> f``A <= f``B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "image_mono";
goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Pow_mono";
goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Union_mono";
goal Set.thy "!!A B. B<=A ==> Inter(A) <= Inter(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Inter_anti_mono";
val prems = goal Set.thy
"[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \
\ (UN x:A. f(x)) <= (UN x:B. g(x))";
-by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
+by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
qed "UN_mono";
val [prem] = goal Set.thy
"[| !!x. f(x)<=g(x) |] ==> (UN x. f(x)) <= (UN x. g(x))";
-by (fast_tac (!claset addIs [prem RS subsetD]) 1);
+by (blast_tac (!claset addIs [prem RS subsetD]) 1);
qed "UN1_mono";
val prems = goal Set.thy
"[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \
\ (INT x:A. f(x)) <= (INT x:A. g(x))";
-by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
+by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
qed "INT_anti_mono";
(*The inclusion is POSITIVE! *)
val [prem] = goal Set.thy
"[| !!x. f(x)<=g(x) |] ==> (INT x. f(x)) <= (INT x. g(x))";
-by (fast_tac (!claset addIs [prem RS subsetD]) 1);
+by (blast_tac (!claset addIs [prem RS subsetD]) 1);
qed "INT1_mono";
goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "insert_mono";
goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Un B <= C Un D";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_mono";
goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Int B <= C Int D";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_mono";
goal Set.thy "!!A::'a set. [| A<=C; D<=B |] ==> A-B <= C-D";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Diff_mono";
goal Set.thy "!!A B. A<=B ==> Compl(B) <= Compl(A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Compl_anti_mono";
(** Monotonicity of implications. For inductive definitions **)
@@ -74,15 +74,15 @@
qed "in_mono";
goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "conj_mono";
goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "disj_mono";
goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "imp_mono";
goal HOL.thy "P-->P";
@@ -92,24 +92,24 @@
val [PQimp] = goal HOL.thy
"[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
-by (fast_tac (!claset addIs [PQimp RS mp]) 1);
+by (blast_tac (!claset addIs [PQimp RS mp]) 1);
qed "ex_mono";
val [PQimp] = goal HOL.thy
"[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
-by (fast_tac (!claset addIs [PQimp RS mp]) 1);
+by (blast_tac (!claset addIs [PQimp RS mp]) 1);
qed "all_mono";
val [PQimp] = goal Set.thy
"[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
-by (fast_tac (!claset addIs [PQimp RS mp]) 1);
+by (blast_tac (!claset addIs [PQimp RS mp]) 1);
qed "Collect_mono";
(*Used in indrule.ML*)
val [subs,PQimp] = goal Set.thy
"[| A<=B; !!x. x:A ==> P(x) --> Q(x) \
\ |] ==> A Int Collect(P) <= B Int Collect(Q)";
-by (fast_tac (!claset addIs [subs RS subsetD, PQimp RS mp]) 1);
+by (blast_tac (!claset addIs [subs RS subsetD, PQimp RS mp]) 1);
qed "Int_Collect_mono";
(*Used in intr_elim.ML and in individual datatype definitions*)
--- a/src/HOL/thy_syntax.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/thy_syntax.ML Wed Apr 09 12:32:04 1997 +0200
@@ -120,7 +120,8 @@
fun mk_params ((ts, tname), cons) =
("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n"
^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
- \val thy = thy",
+ \val thy = thy"
+ ,
"structure " ^ tname ^ " =\n\
\struct\n\
\ val inject = map (get_axiom thy) " ^
@@ -172,6 +173,7 @@
(** primrec **)
+(*recursion equations have user-supplied names*)
fun mk_primrec_decl_1 ((fname, tname), axms) =
let
(*Isolate type name from the structure's identifier it may be stored in*)
@@ -184,10 +186,13 @@
\ (fn _ => [Simp_tac 1]));";
val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
- in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)
+ in ("|> " ^ tname ^ "_add_primrec " ^ axs
+ ,
+ cat_lines (map mk_prove axms)
^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
end;
+(*recursion equations have no names*)
fun mk_primrec_decl_2 ((fname, tname), axms) =
let
(*Isolate type name from the structure's identifier it may be stored in*)
@@ -199,17 +204,44 @@
\(fn _ => [Simp_tac 1])";
val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
- in ("|> " ^ tname ^ "_add_primrec " ^ axs,
+ in ("|> " ^ tname ^ "_add_primrec " ^ axs
+ ,
"val dummy = Addsimps " ^
brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
end;
+(*function name, argument type and either (name,axiom) pairs or just axioms*)
val primrec_decl =
(name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
(name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
+
+(** rec: interface to Slind's TFL **)
+
+
+fun mk_rec_decl ((fname, rel), axms) =
+ let val fid = trim fname
+ in
+ (";\n\n\
+ \structure " ^ fid ^ " =\n\
+ \ struct\n\
+ \ val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
+ \ val {induct,eqns,thy,tcs} = Tfl.RfuncStringList " ^
+ rel ^ "\n" ^ mk_big_list axms ^ " thy;\n\
+ \ end;\n\n\
+ \val thy = thy"
+ ,
+ "")
+ end;
+
+val rec_decl = (name -- string -- repeat1 string >> mk_rec_decl) ;
+
+
+
+
+
(** sections **)
val user_keywords = ["intrs", "monos", "con_defs", "|"];
@@ -219,7 +251,8 @@
("inductive", inductive_decl ""),
("coinductive", inductive_decl "Co"),
("datatype", datatype_decl),
- ("primrec", primrec_decl)];
+ ("primrec", primrec_decl),
+ ("recdef", rec_decl)];
end;