--- a/src/HOL/Auth/Message.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Auth/Message.ML Fri Apr 04 11:18:52 1997 +0200
@@ -37,20 +37,20 @@
(**** keysFor operator ****)
goalw thy [keysFor_def] "keysFor {} = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "keysFor_empty";
goalw thy [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "keysFor_Un";
goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "keysFor_UN";
(*Monotonicity*)
goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "keysFor_mono";
goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
@@ -83,7 +83,7 @@
keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Crypt_imp_invKey_keysFor";
@@ -108,7 +108,7 @@
proofs concern only atomic messages.*)
goal thy "H <= parts(H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "parts_increasing";
(*Monotonicity*)
@@ -122,7 +122,7 @@
goal thy "parts{} = {}";
by (Step_tac 1);
by (etac parts.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
qed "parts_empty";
Addsimps [parts_empty];
@@ -134,7 +134,7 @@
(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
goal thy "!!H. X: parts H ==> EX Y:H. X: parts {Y}";
by (etac parts.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
qed "parts_singleton";
@@ -147,7 +147,7 @@
goal thy "parts(G Un H) <= parts(G) Un parts(H)";
by (rtac subsetI 1);
by (etac parts.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
val parts_Un_subset2 = result();
goal thy "parts(G Un H) = parts(G) Un parts(H)";
@@ -173,7 +173,7 @@
goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
by (rtac subsetI 1);
by (etac parts.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
val parts_UN_subset2 = result();
goal thy "parts(UN x:A. H x) = (UN x:A. parts(H x))";
@@ -195,18 +195,18 @@
goal thy "!!H. X: parts (parts H) ==> X: parts H";
by (etac parts.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
qed "parts_partsE";
-AddSEs [parts_partsE];
+AddSDs [parts_partsE];
goal thy "parts (parts H) = parts H";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "parts_idem";
Addsimps [parts_idem];
goal thy "!!H. [| X: parts G; G <= parts H |] ==> X: parts H";
by (dtac parts_mono 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "parts_trans";
(*Cut*)
@@ -299,13 +299,13 @@
Addsimps [analz.Inj];
goal thy "H <= analz(H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "analz_increasing";
goal thy "analz H <= parts H";
by (rtac subsetI 1);
by (etac analz.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
qed "analz_subset_parts";
bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
@@ -315,7 +315,7 @@
by (rtac equalityI 1);
by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
by (Simp_tac 1);
-by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1);
+by (blast_tac (!claset addIs [analz_increasing RS parts_mono RS subsetD]) 1);
qed "parts_analz";
Addsimps [parts_analz];
@@ -339,7 +339,7 @@
goal thy "analz{} = {}";
by (Step_tac 1);
by (etac analz.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
qed "analz_empty";
Addsimps [analz_empty];
@@ -386,8 +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, analz.Decrypt]) 0));
+by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd]) 0));
qed "analz_insert_MPair";
(*Can pull out enCrypted message if the Key is not known*)
@@ -459,24 +458,24 @@
goal thy "!!H. X: analz (analz H) ==> X: analz H";
by (etac analz.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
qed "analz_analzE";
-AddSEs [analz_analzE];
+AddSDs [analz_analzE];
goal thy "analz (analz H) = analz H";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "analz_idem";
Addsimps [analz_idem];
goal thy "!!H. [| X: analz G; G <= analz H |] ==> X: analz H";
by (dtac analz_mono 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "analz_trans";
(*Cut; Lemma 2 of Lowe*)
goal thy "!!H. [| Y: analz (insert X H); X: analz H |] ==> Y: analz H";
by (etac analz_trans 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "analz_cut";
(*Cut can be proved easily by induction on
@@ -510,7 +509,7 @@
\ analz H = H";
by (Step_tac 1);
by (etac analz.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
qed "analz_trivial";
(*Helps to prove Fake cases*)
@@ -544,7 +543,7 @@
AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth];
goal thy "H <= synth(H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "synth_increasing";
(*Monotonicity*)
@@ -569,39 +568,39 @@
goal thy "!!H. X: synth (synth H) ==> X: synth H";
by (etac synth.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
qed "synth_synthE";
-AddSEs [synth_synthE];
+AddSDs [synth_synthE];
goal thy "synth (synth H) = synth H";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "synth_idem";
goal thy "!!H. [| X: synth G; G <= synth H |] ==> X: synth H";
by (dtac synth_mono 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "synth_trans";
(*Cut; Lemma 2 of Lowe*)
goal thy "!!H. [| Y: synth (insert X H); X: synth H |] ==> Y: synth H";
by (etac synth_trans 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "synth_cut";
goal thy "Agent A : synth H";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Agent_synth";
goal thy "(Nonce N : synth H) = (Nonce N : H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Nonce_synth_eq";
goal thy "(Key K : synth H) = (Key K : H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Key_synth_eq";
goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Crypt_synth_eq";
Addsimps [Agent_synth, Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
@@ -609,7 +608,7 @@
goalw thy [keysFor_def]
"keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "keysFor_synth";
Addsimps [keysFor_synth];
@@ -655,11 +654,10 @@
by (best_tac
(!claset addEs [impOfSubs synth_increasing,
impOfSubs analz_mono]) 5);
-by (Best_tac 1);
-by (deepen_tac (!claset addIs [analz.Fst]) 0 1);
-by (deepen_tac (!claset addIs [analz.Snd]) 0 1);
-by (deepen_tac (!claset addSEs [analz.Decrypt]
- addIs [analz.Decrypt]) 0 1);
+by (Blast_tac 1);
+by (blast_tac (!claset addIs [analz.Inj RS analz.Fst]) 1);
+by (blast_tac (!claset addIs [analz.Inj RS analz.Snd]) 1);
+by (blast_tac (!claset addIs [analz.Decrypt]) 1);
qed "analz_UN1_synth";
Addsimps [analz_UN1_synth];
@@ -668,7 +666,7 @@
goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "parts_insert_subset_Un";
(*More specifically for Fake*)
@@ -676,7 +674,7 @@
\ parts (insert X H) <= synth (analz G) Un parts G Un parts H";
by (dtac parts_insert_subset_Un 1);
by (Full_simp_tac 1);
-by (Deepen_tac 0 1);
+by (Blast_tac 1);
qed "Fake_parts_insert";
goal thy
@@ -696,15 +694,15 @@
by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
addSEs [impOfSubs analz_mono]) 2);
by (Full_simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Fake_analz_insert";
goal thy "(X: analz H & X: parts H) = (X: analz H)";
-by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
val analz_conj_parts = result();
goal thy "(X: analz H | X: parts H) = (X: parts H)";
-by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
val analz_disj_parts = result();
AddIffs [analz_conj_parts, analz_disj_parts];
@@ -713,20 +711,20 @@
redundant cases*)
goal thy "({|X,Y|} : synth (analz H)) = \
\ (X : synth (analz H) & Y : synth (analz H))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "MPair_synth_analz";
AddIffs [MPair_synth_analz];
goal thy "!!K. [| Key K : analz H; Key (invKey K) : analz H |] \
\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Crypt_synth_analz";
goal thy "!!K. X ~: synth (analz H) \
\ ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Hash_synth_analz";
Addsimps [Hash_synth_analz];
@@ -798,7 +796,7 @@
\ ==> (Hash[X] Y : synth (analz H)) = \
\ (Hash {|X, Y|} : analz H & Y : synth (analz H))";
by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "HPair_synth_analz";
Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair,
@@ -866,6 +864,6 @@
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
goal Set.thy "A Un (B Un A) = B Un A";
-by (Fast_tac 1);
+by (Blast_tac 1);
val Un_absorb3 = result();
Addsimps [Un_absorb3];
--- a/src/HOL/Auth/OtwayRees_AN.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Apr 04 11:18:52 1997 +0200
@@ -311,7 +311,7 @@
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (fast_tac (!claset addSEs [lemma]) 1);
+by (blast_tac (!claset addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -327,7 +327,7 @@
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
+by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
qed "Agent_not_see_encrypted_key";
--- a/src/HOL/Auth/Shared.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Auth/Shared.ML Fri Apr 04 11:18:52 1997 +0200
@@ -125,12 +125,12 @@
goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "sees_Says_subset_insert";
goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "sees_subset_sees_Says";
(*Pushing Unions into parts. One of the agents A is B, and thus sees Y.
@@ -141,7 +141,7 @@
by (etac rev_mp 1); (*split_tac does not work on assumptions*)
by (ALLGOALS
(fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons]
- setloop split_tac [expand_if]))));
+ setloop split_tac [expand_if]))));
qed "UN_parts_sees_Says";
goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
@@ -179,12 +179,12 @@
\ (EX A B. Says A B X : set_of_list evs) | (EX A. X = Key (shrK A))";
by (list.induct_tac "evs" 1);
by (ALLGOALS Asm_simp_tac);
-by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
+by (blast_tac (!claset addDs [impOfSubs initState_subset]) 1);
by (rtac conjI 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (event.induct_tac "a" 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if])));
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
qed_spec_mp "seesD";
Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
@@ -202,7 +202,7 @@
goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
by (etac (impOfSubs parts_mono) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "usedI";
AddIs [usedI];
@@ -222,7 +222,7 @@
(*A session key cannot clash with a long-term shared key*)
goal thy "!!K. K ~: range shrK ==> shrK B ~= K";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "shrK_neq";
Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
@@ -264,7 +264,7 @@
by (Step_tac 1);
(*MPair case*)
by (res_inst_tac [("x","Na+Nb")] exI 2);
-by (fast_tac (!claset addSEs [add_leE]) 2);
+by (blast_tac (!claset addSEs [add_leE]) 2);
(*Nonce case*)
by (res_inst_tac [("x","N + Suc nat")] exI 1);
by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
@@ -272,7 +272,7 @@
goal thy "EX N. Nonce N ~: used evs";
by (rtac (lemma RS exE) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Nonce_supply1";
goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
@@ -307,14 +307,14 @@
goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
by (rtac (lemma RS exE) 1);
by (rtac selectI 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Nonce_supply";
(*** Supply fresh keys for possibility theorems. ***)
goal thy "EX K. Key K ~: used evs";
by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Key_supply1";
val Fin_UNIV_insertI = UNIV_I RS Fin.insertI;
@@ -344,7 +344,7 @@
goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
by (rtac selectI 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Key_supply";
(*** Tactics for possibility theorems ***)
@@ -400,28 +400,23 @@
val pushKey_newK = insComm thy "Key (newK ?evs)" "Key (shrK ?C)";
goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "subset_Compl_range";
-goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
-\ Key `` (f `` (insert x E)) Un C";
-by (Fast_tac 1);
-qed "insert_Key_image";
-
goal thy "insert (Key K) H = Key `` {K} Un H";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "insert_Key_singleton";
goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
-by (Fast_tac 1);
-qed "insert_Key_image'";
+by (Blast_tac 1);
+qed "insert_Key_image";
val analz_image_freshK_ss =
!simpset delsimps [image_insert, image_Un]
addsimps ([image_insert RS sym, image_Un RS sym,
Key_not_used,
insert_Key_singleton, subset_Compl_range,
- insert_Key_image', Un_assoc RS sym]
+ insert_Key_image, Un_assoc RS sym]
@disj_comms)
setloop split_tac [expand_if];
--- a/src/HOL/Lambda/Eta.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Lambda/Eta.ML Fri Apr 04 11:18:52 1997 +0200
@@ -27,8 +27,8 @@
goal Eta.thy "!i t u. ~free s i --> s[t/i] = s[u/i]";
by (dB.induct_tac "s" 1);
by (ALLGOALS(simp_tac (addsplit (!simpset))));
-by (fast_tac HOL_cs 1);
-by (fast_tac HOL_cs 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "subst_not_free";
Addsimps [subst_not_free RS eqTrueI];
@@ -36,7 +36,7 @@
\ (i < k & free t i | k < i & free t (pred i))";
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
-by (fast_tac HOL_cs 2);
+by (Blast_tac 2);
by(simp_tac (!simpset addsimps [pred_def]
setloop (split_tac [expand_nat_case])) 1);
by (safe_tac HOL_cs);
@@ -48,7 +48,7 @@
\ (free s k & free t i | free s (if i<k then i else Suc i))";
by (dB.induct_tac "s" 1);
by (Asm_simp_tac 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (asm_full_simp_tac (addsplit (!simpset)) 2);
by(simp_tac (!simpset addsimps [pred_def,subst_Var]
setloop (split_tac [expand_if,expand_nat_case])) 1);
@@ -94,17 +94,17 @@
goal Eta.thy "!!s. s -e>> s' ==> Abs s -e>> Abs s'";
by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+by (ALLGOALS(blast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
qed "rtrancl_eta_Abs";
goal Eta.thy "!!s. s -e>> s' ==> s @ t -e>> s' @ t";
by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+by (ALLGOALS(blast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
qed "rtrancl_eta_AppL";
goal Eta.thy "!!s. t -e>> t' ==> s @ t -e>> s @ t'";
by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+by (ALLGOALS(blast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
qed "rtrancl_eta_AppR";
goal Eta.thy "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
@@ -142,9 +142,9 @@
goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
by (dB.induct_tac "u" 1);
by (ALLGOALS(asm_simp_tac (addsplit (!simpset))));
-by (fast_tac (!claset addIs [r_into_rtrancl]) 1);
-by (fast_tac (!claset addSIs [rtrancl_eta_App]) 1);
-by (fast_tac (!claset addSIs [rtrancl_eta_Abs,eta_lift]) 1);
+by (blast_tac (!claset addIs [r_into_rtrancl]) 1);
+by (blast_tac (!claset addSIs [rtrancl_eta_App]) 1);
+by (blast_tac (!claset addSIs [rtrancl_eta_Abs,eta_lift]) 1);
qed_spec_mp "rtrancl_eta_subst";
goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)";
@@ -179,7 +179,7 @@
by (etac thin_rl 1);
by (res_inst_tac [("dB","t")] dB_case_distinction 1);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
- by (fast_tac (HOL_cs addDs [less_not_refl2]) 1);
+ by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
@@ -196,7 +196,7 @@
by (res_inst_tac [("dB","t")] dB_case_distinction 1);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
by (Simp_tac 1);
- by (fast_tac HOL_cs 1);
+ by (Blast_tac 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
by (etac thin_rl 1);
@@ -211,7 +211,7 @@
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
by (Simp_tac 1);
by (Simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Blast_tac 1);
qed_spec_mp "not_free_iff_lifted";
goal Eta.thy "(!s u. (~free s 0) --> R(Abs(s @ Var 0))(s[u/0])) = \
--- a/src/HOL/Lambda/Lambda.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Lambda/Lambda.ML Fri Apr 04 11:18:52 1997 +0200
@@ -23,29 +23,30 @@
goal Lambda.thy "!!s. s ->> s' ==> Abs s ->> Abs s'";
by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
qed "rtrancl_beta_Abs";
AddSIs [rtrancl_beta_Abs];
goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t";
by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
qed "rtrancl_beta_AppL";
goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'";
by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
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]
+by (deepen_tac (!claset addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
addIs [rtrancl_trans]) 3 1);
qed "rtrancl_beta_App";
AddIs [rtrancl_beta_App];
(*** subst and lift ***)
-fun addsplit ss = ss addsimps [subst_Var] setloop (split_inside_tac [expand_if]);
+fun addsplit ss = ss addsimps [subst_Var]
+ setloop (split_inside_tac [expand_if]);
goal Lambda.thy "(Var k)[u/k] = u";
by (asm_full_simp_tac(addsplit(!simpset)) 1);
@@ -123,7 +124,7 @@
goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k";
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
-by (fast_tac (HOL_cs addDs [add_lessD1]) 1);
+by (blast_tac (!claset addDs [add_lessD1]) 1);
qed "liftn_lift";
Addsimps [liftn_lift];
--- a/src/HOL/Lambda/ParRed.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Lambda/ParRed.ML Fri Apr 04 11:18:52 1997 +0200
@@ -21,7 +21,7 @@
(*** beta <= par_beta <= beta^* ***)
goal ParRed.thy "(Var n => t) = (t = Var n)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "par_beta_varL";
Addsimps [par_beta_varL];
@@ -36,7 +36,7 @@
by (rtac subsetI 1);
by (split_all_tac 1);
by (etac beta.induct 1);
-by (ALLGOALS(fast_tac (!claset addSIs [par_beta_refl])));
+by (ALLGOALS(blast_tac (!claset addSIs [par_beta_refl])));
qed "beta_subset_par_beta";
goal ParRed.thy "par_beta <= beta^*";
@@ -72,7 +72,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(fast_tac (!claset addSIs [par_beta_subst])));
+by (ALLGOALS(Blast.depth_tac (!claset addSIs [par_beta_subst]) 7));
qed "diamond_par_beta";
@@ -83,16 +83,17 @@
by (Simp_tac 1);
by (etac rev_mp 1);
by (dB.induct_tac "dB1" 1);
- by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] unsafe_addss (!simpset))));
+ by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst]
+ unsafe_addss (!simpset))));
qed_spec_mp "par_beta_cd";
(*** Confluence (via cd) ***)
goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
-by (fast_tac (HOL_cs addIs [par_beta_cd]) 1);
+by (blast_tac (HOL_cs addIs [par_beta_cd]) 1);
qed "diamond_par_beta2";
goal ParRed.thy "confluent(beta)";
-by (fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence,
- par_beta_subset_beta,beta_subset_par_beta]) 1);
+by (blast_tac (HOL_cs addIs [diamond_par_beta2, diamond_to_confluence,
+ par_beta_subset_beta, beta_subset_par_beta]) 1);
qed"beta_confluent";
--- a/src/HOL/List.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/List.ML Fri Apr 04 11:18:52 1997 +0200
@@ -23,7 +23,6 @@
by (list.induct_tac "xs" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
-by (REPEAT(resolve_tac [exI,refl,conjI] 1));
qed "neq_Nil_conv";
@@ -31,10 +30,10 @@
goal List.thy
"P(list_case a f xs) = ((xs=[] --> P(a)) & \
-\ (!y ys. xs=y#ys --> P(f y ys)))";
+\ (!y ys. xs=y#ys --> P(f y ys)))";
by (list.induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "expand_list_case";
val prems = goal List.thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
@@ -44,8 +43,8 @@
goal List.thy "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
by (list.induct_tac "xs" 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
bind_thm("list_eq_cases",
impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
@@ -73,7 +72,7 @@
goal List.thy "([] = xs@ys) = (xs=[] & ys=[])";
by (list.induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
-by(Fast_tac 1);
+by(Blast_tac 1);
qed "Nil_is_append_conv";
AddIffs [Nil_is_append_conv];
@@ -175,19 +174,19 @@
goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
by (list.induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "set_of_list_append";
Addsimps[set_of_list_append];
goal thy "(x mem xs) = (x: set_of_list xs)";
by (list.induct_tac "xs" 1);
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "set_of_list_mem_eq";
goal List.thy "set_of_list l <= set_of_list (x#l)";
by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "set_of_list_subset_Cons";
goal List.thy "(set_of_list xs = {}) = (xs = [])";
@@ -199,7 +198,7 @@
goal List.thy "set_of_list(rev xs) = set_of_list(xs)";
by(list.induct_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
-by(Fast_tac 1);
+by(Blast_tac 1);
qed "set_of_list_rev";
Addsimps [set_of_list_rev];
@@ -227,7 +226,7 @@
goal List.thy "list_all P xs = (!x. x mem xs --> P(x))";
by (list.induct_tac "xs" 1);
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "list_all_mem_conv";
@@ -463,7 +462,7 @@
by(ALLGOALS Asm_simp_tac);
by(strip_tac 1);
by(res_inst_tac [("n","n")] natE 1);
- by(Fast_tac 1);
+ by(Blast_tac 1);
by(res_inst_tac [("n","i")] natE 1);
by(ALLGOALS (hyp_subst_tac THEN' Asm_full_simp_tac));
qed_spec_mp "nth_take";
@@ -486,7 +485,7 @@
by(list.induct_tac "xs" 1);
by(Simp_tac 1);
by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-by(Fast_tac 1);
+by(Blast_tac 1);
bind_thm("takeWhile_append1", conjI RS (result() RS mp));
Addsimps [takeWhile_append1];
@@ -503,7 +502,7 @@
by(list.induct_tac "xs" 1);
by(Simp_tac 1);
by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-by(Fast_tac 1);
+by(Blast_tac 1);
bind_thm("dropWhile_append1", conjI RS (result() RS mp));
Addsimps [dropWhile_append1];
--- a/src/HOL/NatDef.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/NatDef.ML Fri Apr 04 11:18:52 1997 +0200
@@ -28,7 +28,7 @@
"[| i: Nat; P(Zero_Rep); \
\ !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |] ==> P(i)";
by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
qed "Nat_induct";
val prems = goalw thy [Zero_def,Suc_def]
@@ -65,7 +65,7 @@
by (fast_tac (!claset addSEs prems) 1);
by (nat_ind_tac "n" 1);
by (rtac (refl RS disjI1) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "natE";
(*** Isomorphisms: Abs_Nat and Rep_Nat ***)
@@ -126,17 +126,17 @@
(*** nat_case -- the selection operator for nat ***)
goalw thy [nat_case_def] "nat_case a f 0 = a";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
qed "nat_case_0";
goalw thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
qed "nat_case_Suc";
(** Introduction rules for 'pred_nat' **)
goalw thy [pred_nat_def] "(n, Suc(n)) : pred_nat";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "pred_natI";
val major::prems = goalw thy [pred_nat_def]
@@ -149,8 +149,8 @@
goalw thy [wf_def] "wf(pred_nat)";
by (strip_tac 1);
by (nat_ind_tac "x" 1);
-by (fast_tac (!claset addSEs [mp, pred_natE]) 2);
-by (fast_tac (!claset addSEs [mp, pred_natE]) 1);
+by (blast_tac (!claset addSEs [mp, pred_natE]) 2);
+by (blast_tac (!claset addSEs [mp, pred_natE]) 1);
qed "wf_pred_nat";
@@ -228,7 +228,7 @@
(** Elimination properties **)
val prems = goalw thy [less_def] "n<m ==> ~ m<(n::nat)";
-by (fast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
+by (blast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
qed "less_not_sym";
(* [| n<m; m<n |] ==> R *)
@@ -243,7 +243,7 @@
bind_thm ("less_irrefl", (less_not_refl RS notE));
goal thy "!!m. n<m ==> m ~= (n::nat)";
-by (fast_tac (!claset addEs [less_irrefl]) 1);
+by (blast_tac (!claset addEs [less_irrefl]) 1);
qed "less_not_refl2";
@@ -272,14 +272,13 @@
"[| m < Suc(n); m<n ==> P; m=n ==> P |] ==> P";
by (rtac (major RS lessE) 1);
by (rtac eq 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (rtac less 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "less_SucE";
goal thy "(m < Suc(n)) = (m < n | m = n)";
-by (fast_tac (!claset addSIs [lessI]
- 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";
@@ -316,14 +315,13 @@
qed "Suc_lessE";
goal thy "!!m n. Suc(m) < Suc(n) ==> m<n";
-by (fast_tac (!claset addEs [lessE, Suc_lessD] addIs [lessI]) 1);
+by (blast_tac (!claset addEs [lessE, make_elim Suc_lessD]) 1);
qed "Suc_less_SucD";
goal thy "!!m n. m<n ==> Suc(m) < Suc(n)";
by (etac rev_mp 1);
by (nat_ind_tac "n" 1);
-by (ALLGOALS (fast_tac (!claset addSIs [lessI]
- addEs [less_trans, lessE])));
+by (ALLGOALS (fast_tac (!claset addEs [less_trans, lessE])));
qed "Suc_mono";
@@ -333,7 +331,7 @@
Addsimps [Suc_less_eq];
goal thy "~(Suc(n) < n)";
-by (fast_tac (!claset addEs [Suc_lessD RS less_irrefl]) 1);
+by (blast_tac (!claset addEs [Suc_lessD RS less_irrefl]) 1);
qed "not_Suc_n_less_n";
Addsimps [not_Suc_n_less_n];
@@ -341,7 +339,7 @@
by (nat_ind_tac "k" 1);
by (ALLGOALS (asm_simp_tac (!simpset)));
by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (fast_tac (!claset addDs [Suc_lessD]) 1);
+by (blast_tac (!claset addDs [Suc_lessD]) 1);
qed_spec_mp "less_trans_Suc";
(*"Less than" is a linear ordering*)
@@ -350,7 +348,7 @@
by (nat_ind_tac "n" 1);
by (rtac (refl RS disjI1 RS disjI2) 1);
by (rtac (zero_less_Suc RS disjI1) 1);
-by (fast_tac (!claset addIs [lessI, Suc_mono, less_SucI] addEs [lessE]) 1);
+by (fast_tac (!claset addIs [Suc_mono, less_SucI] addEs [lessE]) 1);
qed "less_linear";
qed_goal "nat_less_cases" thy
@@ -453,16 +451,16 @@
val leE = make_elim leD;
goal thy "(~n<m) = (m<=(n::nat))";
-by (fast_tac (!claset addIs [leI] addEs [leE]) 1);
+by (blast_tac (!claset addIs [leI] addEs [leE]) 1);
qed "not_less_iff_le";
goalw thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "not_leE";
goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n";
by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
+by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
qed "lessD";
goalw thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
@@ -474,32 +472,32 @@
"!!m. Suc m <= n ==> m < n";
by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
by (cut_facts_tac [less_linear] 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Suc_le_lessD";
goal thy "(Suc m <= n) = (m < n)";
-by (fast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
+by (blast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
qed "Suc_le_eq";
goalw thy [le_def] "!!m. m <= n ==> m <= Suc n";
-by (fast_tac (!claset addDs [Suc_lessD]) 1);
+by (blast_tac (!claset addDs [Suc_lessD]) 1);
qed "le_SucI";
Addsimps[le_SucI];
bind_thm ("le_Suc", not_Suc_n_less_n RS leI);
goalw thy [le_def] "!!m. m < n ==> m <= (n::nat)";
-by (fast_tac (!claset addEs [less_asym]) 1);
+by (blast_tac (!claset addEs [less_asym]) 1);
qed "less_imp_le";
goalw thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
by (cut_facts_tac [less_linear] 1);
-by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
+by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
qed "le_imp_less_or_eq";
goalw thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
by (cut_facts_tac [less_linear] 1);
-by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
+by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
by (flexflex_tac);
qed "less_or_eq_imp_le";
@@ -522,13 +520,16 @@
qed "less_le_trans";
goal thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
-by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
- rtac less_or_eq_imp_le, fast_tac (!claset addIs [less_trans])]);
+by (EVERY1[dtac le_imp_less_or_eq,
+ dtac le_imp_less_or_eq,
+ rtac less_or_eq_imp_le,
+ fast_tac (!claset addIs [less_trans])]);
qed "le_trans";
-val prems = goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
-by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
- fast_tac (!claset addEs [less_irrefl,less_asym])]);
+goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
+by (EVERY1[dtac le_imp_less_or_eq,
+ dtac le_imp_less_or_eq,
+ blast_tac (!claset addEs [less_irrefl,less_asym])]);
qed "le_anti_sym";
goal thy "(Suc(n) <= Suc(m)) = (n <= m)";
@@ -543,7 +544,7 @@
br conjI 1;
be less_imp_le 1;
be (less_not_refl2 RS not_sym) 1;
-by(fast_tac (!claset addSDs [le_imp_less_or_eq]) 1);
+by(blast_tac (!claset addSDs [le_imp_less_or_eq]) 1);
qed "nat_less_le";
(** LEAST -- the least number operator **)
@@ -551,9 +552,9 @@
val [prem1,prem2] = goalw thy [Least_def]
"[| P(k::nat); !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
by (rtac select_equality 1);
-by (fast_tac (!claset addSIs [prem1,prem2]) 1);
+by (blast_tac (!claset addSIs [prem1,prem2]) 1);
by (cut_facts_tac [less_linear] 1);
-by (fast_tac (!claset addSIs [prem1] addSDs [prem2]) 1);
+by (blast_tac (!claset addSIs [prem1] addSDs [prem2]) 1);
qed "Least_equality";
val [prem] = goal thy "P(k::nat) ==> P(LEAST x.P(x))";
@@ -564,7 +565,7 @@
by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
by (assume_tac 1);
by (assume_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "LeastI";
(*Proof is almost identical to the one above!*)
@@ -576,7 +577,7 @@
by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
by (assume_tac 1);
by (rtac le_refl 2);
-by (fast_tac (!claset addIs [less_imp_le,le_trans]) 1);
+by (blast_tac (!claset addIs [less_imp_le,le_trans]) 1);
qed "Least_le";
val [prem] = goal thy "k < (LEAST x.P(x)) ==> ~P(k::nat)";
@@ -593,23 +594,23 @@
safe_tac (!claset addSEs [LeastI]),
rename_tac "j" 1,
res_inst_tac [("n","j")] natE 1,
- Fast_tac 1,
- fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
+ Blast_tac 1,
+ blast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
rename_tac "k n" 1,
res_inst_tac [("n","k")] natE 1,
- Fast_tac 1,
+ Blast_tac 1,
hyp_subst_tac 1,
rewtac Least_def,
rtac (select_equality RS arg_cong RS sym) 1,
safe_tac (!claset),
dtac Suc_mono 1,
- Fast_tac 1,
+ Blast_tac 1,
cut_facts_tac [less_linear] 1,
safe_tac (!claset),
atac 2,
- Fast_tac 2,
+ Blast_tac 2,
dtac Suc_mono 1,
- Fast_tac 1]);
+ Blast_tac 1]);
(*** Instantiation of transitivity prover ***)
@@ -633,8 +634,8 @@
(fn _ => [etac swap2 1, etac leD 1]);
val eqI = prove_goal thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n"
(fn _ => [etac less_SucE 1,
- fast_tac (HOL_cs addSDs [Suc_less_SucD] addSEs [less_irrefl]
- addDs [less_trans_Suc]) 1,
+ fast_tac (!claset addSDs [Suc_less_SucD] addSEs [less_irrefl]
+ addDs [less_trans_Suc]) 1,
atac 1]);
val leD = le_eq_less_Suc RS iffD1;
val not_lessD = nat_leI RS leD;
--- a/src/HOL/Relation.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Relation.ML Fri Apr 04 11:18:52 1997 +0200
@@ -9,7 +9,7 @@
(** Identity relation **)
goalw Relation.thy [id_def] "(a,a) : id";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "idI";
val major::prems = goalw Relation.thy [id_def]
@@ -21,7 +21,7 @@
qed "idE";
goalw Relation.thy [id_def] "(a,b):id = (a=b)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "pair_in_id_conv";
Addsimps [pair_in_id_conv];
@@ -30,7 +30,7 @@
goalw Relation.thy [comp_def]
"!!r s. [| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "compI";
(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
@@ -55,12 +55,12 @@
AddSEs [compE, idE];
goal Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "comp_mono";
goal Relation.thy
"!!r s. [| s <= A Times B; r <= B Times C |] ==> (r O s) <= A Times C";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "comp_subset_Sigma";
(** Natural deduction for trans(r) **)
@@ -72,7 +72,7 @@
goalw Relation.thy [trans_def]
"!!r. [| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "transD";
(** Natural deduction for converse(r) **)
@@ -88,7 +88,7 @@
qed "converseI";
goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "converseD";
(*More general than converseD, as it "splits" the member of the relation*)
@@ -104,14 +104,14 @@
AddSEs [converseE];
goalw Relation.thy [converse_def] "converse(converse R) = R";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "converse_converse";
(** Domain **)
qed_goalw "Domain_iff" Relation.thy [Domain_def]
"a: Domain(r) = (EX y. (a,y): r)"
- (fn _=> [ (Fast_tac 1) ]);
+ (fn _=> [ (Blast_tac 1) ]);
qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)"
(fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
@@ -144,16 +144,16 @@
qed_goalw "Image_iff" Relation.thy [Image_def]
"b : r^^A = (? x:A. (x,b):r)"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
qed_goal "Image_singleton_iff" Relation.thy
"(b : r^^{a}) = ((a,b):r)"
(fn _ => [ rtac (Image_iff RS trans) 1,
- Fast_tac 1 ]);
+ Blast_tac 1 ]);
qed_goalw "ImageI" Relation.thy [Image_def]
"!!a b r. [| (a,b): r; a:A |] ==> b : r^^A"
- (fn _ => [ (Fast_tac 1)]);
+ (fn _ => [ (Blast_tac 1)]);
qed_goalw "ImageE" Relation.thy [Image_def]
"[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P"
--- a/src/HOL/Set.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Set.ML Fri Apr 04 11:18:52 1997 +0200
@@ -151,10 +151,10 @@
AddEs [subsetD, subsetCE];
qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
- (fn _=> [Fast_tac 1]);
+ (fn _=> [Blast_tac 1]);
val prems = goal Set.thy "!!B. [| A<=B; B<=C |] ==> A<=(C::'a set)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "subset_trans";
@@ -206,7 +206,7 @@
section "The empty set -- {}";
qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
Addsimps [empty_iff];
@@ -216,14 +216,14 @@
AddSEs [emptyE];
qed_goal "empty_subsetI" Set.thy "{} <= A"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
(fn [prem]=>
[ (fast_tac (!claset addIs [prem RS FalseE]) 1) ]);
qed_goal "equals0D" Set.thy "!!a. [| A={}; a:A |] ==> P"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
goal Set.thy "Ball {} P = True";
by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Ball_def, empty_def]) 1);
@@ -235,13 +235,13 @@
Addsimps [ball_empty, bex_empty];
goalw Set.thy [Ball_def] "(!x:A.False) = (A = {})";
-by(Fast_tac 1);
+by(Blast_tac 1);
qed "ball_False";
Addsimps [ball_False];
(* The dual is probably not helpful:
goal Set.thy "(? x:A.True) = (A ~= {})";
-by(Fast_tac 1);
+by(Blast_tac 1);
qed "bex_True";
Addsimps [bex_True];
*)
@@ -267,7 +267,7 @@
section "Set complement -- Compl";
qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : Compl(A)) = (c~:A)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
Addsimps [Compl_iff];
@@ -293,7 +293,7 @@
section "Binary union -- Un";
qed_goalw "Un_iff" Set.thy [Un_def] "(c : A Un B) = (c:A | c:B)"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
Addsimps [Un_iff];
@@ -324,7 +324,7 @@
section "Binary intersection -- Int";
qed_goalw "Int_iff" Set.thy [Int_def] "(c : A Int B) = (c:A & c:B)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
Addsimps [Int_iff];
@@ -353,7 +353,7 @@
section "Set difference";
qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : A-B) = (c:A & c~:B)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
Addsimps [Diff_iff];
@@ -378,7 +378,7 @@
section "Augmenting a set -- insert";
qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b | a:A)"
- (fn _ => [Fast_tac 1]);
+ (fn _ => [Blast_tac 1]);
Addsimps [insert_iff];
@@ -409,13 +409,13 @@
(fn _=> [ (rtac insertI1 1) ]);
goal Set.thy "!!a. b : {a} ==> b=a";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "singletonD";
bind_thm ("singletonE", make_elim singletonD);
qed_goal "singleton_iff" thy "(b : {a}) = (b=a)"
-(fn _ => [Fast_tac 1]);
+(fn _ => [Blast_tac 1]);
goal Set.thy "!!a b. {a}={b} ==> a=b";
by (fast_tac (!claset addEs [equalityE]) 1);
@@ -439,7 +439,7 @@
section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
goalw Set.thy [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "UN_iff";
Addsimps [UN_iff];
@@ -507,7 +507,7 @@
goalw Set.thy [UNION1_def] "(b: (UN x. B(x))) = (EX x. b: B(x))";
by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "UN1_iff";
Addsimps [UN1_iff];
@@ -531,7 +531,7 @@
goalw Set.thy [INTER1_def] "(b: (INT x. B(x))) = (ALL x. b: B(x))";
by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "INT1_iff";
Addsimps [INT1_iff];
@@ -552,7 +552,7 @@
section "Union";
goalw Set.thy [Union_def] "(A : Union(C)) = (EX X:C. A:X)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Union_iff";
Addsimps [Union_iff];
@@ -575,7 +575,7 @@
section "Inter";
goalw Set.thy [Inter_def] "(A : Inter(C)) = (ALL X:C. A:X)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Inter_iff";
Addsimps [Inter_iff];
--- a/src/HOL/Sum.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Sum.ML Fri Apr 04 11:18:52 1997 +0200
@@ -53,12 +53,12 @@
val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Inl_Rep_inject";
val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Inr_Rep_inject";
goalw Sum.thy [Inl_def] "inj(Inl)";
@@ -78,11 +78,11 @@
val Inr_inject = inj_Inr RS injD;
goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
-by (fast_tac (!claset addSEs [Inl_inject]) 1);
+by (blast_tac (!claset addSDs [Inl_inject]) 1);
qed "Inl_eq";
goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
-by (fast_tac (!claset addSEs [Inr_inject]) 1);
+by (blast_tac (!claset addSDs [Inr_inject]) 1);
qed "Inr_eq";
AddIffs [Inl_eq, Inr_eq];
@@ -92,11 +92,11 @@
(** Introduction rules for the injections **)
goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A Plus B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "InlI";
goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A Plus B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "InrI";
(** Elimination rules **)
@@ -119,7 +119,7 @@
(** sum_case -- the selection operator for sums **)
goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
qed "sum_case_Inl";
goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
@@ -163,7 +163,7 @@
goalw Sum.thy [Part_def]
"!!a b A h. [| a : A; a=h(b) |] ==> a : Part A h";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_eqI";
val PartI = refl RSN (2,Part_eqI);
@@ -177,12 +177,15 @@
by (REPEAT (ares_tac prems 1));
qed "PartE";
+AddIs [Part_eqI];
+AddSEs [PartE];
+
goalw Sum.thy [Part_def] "Part A h <= A";
by (rtac Int_lower1 1);
qed "Part_subset";
goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
-by (fast_tac (!claset addSIs [PartI] addSEs [PartE]) 1);
+by (Fast_tac 1);
qed "Part_mono";
val basic_monos = basic_monos @ [Part_mono];
@@ -192,14 +195,14 @@
qed "PartD1";
goal Sum.thy "Part A (%x.x) = A";
-by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
+by (Blast_tac 1);
qed "Part_id";
goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
-by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
+by (Fast_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 (!claset addIs [PartI] addSEs [PartE]) 1);
+by (Fast_tac 1);
qed "Part_Collect";
--- a/src/HOL/Trancl.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Trancl.ML Fri Apr 04 11:18:52 1997 +0200
@@ -20,7 +20,7 @@
(*Reflexivity of rtrancl*)
goal Trancl.thy "(a,a) : r^*";
by (stac rtrancl_unfold 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "rtrancl_refl";
Addsimps [rtrancl_refl];
@@ -30,7 +30,7 @@
(*Closure under composition with r*)
goal Trancl.thy "!!r. [| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*";
by (stac rtrancl_unfold 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "rtrancl_into_rtrancl";
(*rtrancl of r contains r*)
@@ -64,7 +64,7 @@
(*by induction on this formula*)
by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
(*now solve first subgoal: this formula is sufficient*)
-by (Fast_tac 1);
+by (Blast_tac 1);
(*now do the induction*)
by (resolve_tac [major RS rtrancl_full_induct] 1);
by (fast_tac (!claset addIs prems) 1);
@@ -124,7 +124,7 @@
by (dtac rtrancl_mono 1);
by (dtac rtrancl_mono 1);
by (Asm_full_simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "rtrancl_subset";
goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
@@ -165,7 +165,7 @@
\ ==> P(a)";
by (rtac ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1);
by (resolve_tac prems 1);
-by (fast_tac (!claset addIs prems addSEs[converseD]addSDs[rtrancl_converseD])1);
+by (fast_tac (!claset addIs prems addSDs[rtrancl_converseD])1);
qed "converse_rtrancl_induct";
val prems = goal Trancl.thy
@@ -225,7 +225,7 @@
(*by induction on this formula*)
by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
(*now solve first subgoal: this formula is sufficient*)
-by (Fast_tac 1);
+by (Blast_tac 1);
by (etac rtrancl_induct 1);
by (ALLGOALS (fast_tac (!claset addIs (rtrancl_into_trancl1::prems))));
qed "trancl_induct";
@@ -240,7 +240,7 @@
by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
by (etac rtranclE 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (fast_tac (!claset addSIs [rtrancl_into_trancl1]) 1);
qed "tranclE";
@@ -268,11 +268,11 @@
by (cut_facts_tac prems 1);
by (rtac (major RS rtrancl_induct) 1);
by (rtac (refl RS disjI1) 1);
-by (fast_tac (!claset addSEs [SigmaE2]) 1);
+by (Blast_tac 1);
val lemma = result();
goalw Trancl.thy [trancl_def]
"!!r. r <= A Times A ==> r^+ <= A Times A";
-by (fast_tac (!claset addSDs [lemma]) 1);
+by (blast_tac (!claset addSDs [lemma]) 1);
qed "trancl_subset_Sigma";
--- a/src/HOL/Univ.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/Univ.ML Fri Apr 04 11:18:52 1997 +0200
@@ -69,12 +69,12 @@
(*** Introduction rules for Node ***)
goalw Univ.thy [Node_def] "(%k. 0,a) : Node";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Node_K0_I";
goalw Univ.thy [Node_def,Push_def]
"!!p. p: Node ==> apfst (Push i) p : Node";
-by (fast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
+by (blast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
qed "Node_Push_I";
@@ -98,12 +98,12 @@
(** Atomic nodes **)
goalw Univ.thy [Atom_def, inj_def] "inj(Atom)";
-by (fast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
+by (blast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
qed "inj_Atom";
val Atom_inject = inj_Atom RS injD;
goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
-by (fast_tac (!claset addSEs [Atom_inject]) 1);
+by (blast_tac (!claset addSDs [Atom_inject]) 1);
qed "Atom_Atom_eq";
AddIffs [Atom_Atom_eq];
@@ -142,14 +142,12 @@
(** Injectiveness of Scons **)
-val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> M<=M'";
-by (cut_facts_tac [major] 1);
-by (fast_tac (!claset addSEs [Push_Node_inject]) 1);
+goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> M<=M'";
+by (blast_tac (!claset addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma1";
-val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> N<=N'";
-by (cut_facts_tac [major] 1);
-by (fast_tac (!claset addSEs [Push_Node_inject]) 1);
+goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
+by (fast_tac (!claset addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma2";
val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
@@ -171,7 +169,7 @@
AddSDs [Scons_inject];
goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
-by (fast_tac (!claset addSEs [Scons_inject]) 1);
+by (blast_tac (!claset addSEs [Scons_inject]) 1);
qed "Scons_Scons_eq";
(*** Distinctness involving Leaf and Numb ***)
@@ -244,7 +242,7 @@
(*** ntrunc applied to the various node sets ***)
goalw Univ.thy [ntrunc_def] "ntrunc 0 M = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "ntrunc_0";
goalw Univ.thy [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)";
@@ -261,7 +259,7 @@
goalw Univ.thy [Scons_def,ntrunc_def]
"ntrunc (Suc k) (M$N) = ntrunc k M $ ntrunc k N";
-by (safe_tac ((claset_of "Fun") addSIs [equalityI,imageI]));
+by (safe_tac (!claset addSIs [equalityI, imageI]));
by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
by (REPEAT (rtac Suc_less_SucD 1 THEN
rtac (ndepth_Push_Node RS subst) 1 THEN
@@ -273,7 +271,7 @@
goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
by (rewtac Scons_def);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "ntrunc_one_In0";
goalw Univ.thy [In0_def]
@@ -284,7 +282,7 @@
goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
by (rewtac Scons_def);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "ntrunc_one_In1";
goalw Univ.thy [In1_def]
@@ -321,11 +319,11 @@
(*** Disjoint Sum ***)
goalw Univ.thy [usum_def] "!!M. M:A ==> In0(M) : A<+>B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "usum_In0I";
goalw Univ.thy [usum_def] "!!N. N:B ==> In1(N) : A<+>B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "usum_In1I";
val major::prems = goalw Univ.thy [usum_def]
@@ -363,12 +361,12 @@
(*** proving equality of sets and functions using ntrunc ***)
goalw Univ.thy [ntrunc_def] "ntrunc k M <= M";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "ntrunc_subsetI";
val [major] = goalw Univ.thy [ntrunc_def]
"(!!k. ntrunc k M <= N) ==> M<=N";
-by (fast_tac (!claset addIs [less_add_Suc1, less_add_Suc2,
+by (blast_tac (!claset addIs [less_add_Suc1, less_add_Suc2,
major RS subsetD]) 1);
qed "ntrunc_subsetD";
@@ -390,15 +388,15 @@
(*** Monotonicity ***)
goalw Univ.thy [uprod_def] "!!A B. [| A<=A'; B<=B' |] ==> A<*>B <= A'<*>B'";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "uprod_mono";
goalw Univ.thy [usum_def] "!!A B. [| A<=A'; B<=B' |] ==> A<+>B <= A'<+>B'";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "usum_mono";
goalw Univ.thy [Scons_def] "!!M N. [| M<=M'; N<=N' |] ==> M$N <= M'$N'";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Scons_mono";
goalw Univ.thy [In0_def] "!!M N. M<=N ==> In0(M) <= In0(N)";
@@ -413,29 +411,29 @@
(*** Split and Case ***)
goalw Univ.thy [Split_def] "Split c (M$N) = c M N";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
qed "Split";
goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
qed "Case_In0";
goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
qed "Case_In1";
(**** UN x. B(x) rules ****)
goalw Univ.thy [ntrunc_def] "ntrunc k (UN x.f(x)) = (UN x. ntrunc k (f x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "ntrunc_UN1";
goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Scons_UN1_x";
goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Scons_UN1_y";
goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))";
@@ -450,7 +448,7 @@
(*** Equality : the diagonal relation ***)
goalw Univ.thy [diag_def] "!!a A. [| a=b; a:A |] ==> (a,b) : diag(A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "diag_eqI";
val diagI = refl RS diag_eqI |> standard;
@@ -468,7 +466,7 @@
goalw Univ.thy [dprod_def]
"!!r s. [| (M,M'):r; (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "dprodI";
(*The general elimination rule*)
@@ -485,11 +483,11 @@
(*** Equality for Disjoint Sum ***)
goalw Univ.thy [dsum_def] "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "dsum_In0I";
goalw Univ.thy [dsum_def] "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "dsum_In1I";
val major::prems = goalw Univ.thy [dsum_def]
@@ -510,22 +508,22 @@
(*** Monotonicity ***)
goal Univ.thy "!!r s. [| r<=r'; s<=s' |] ==> r<**>s <= r'<**>s'";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "dprod_mono";
goal Univ.thy "!!r s. [| r<=r'; s<=s' |] ==> r<++>s <= r'<++>s'";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "dsum_mono";
(*** Bounding theorems ***)
goal Univ.thy "diag(A) <= A Times A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "diag_subset_Sigma";
goal Univ.thy "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "dprod_Sigma";
val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
@@ -535,11 +533,11 @@
"(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
by (safe_tac (!claset));
by (stac Split 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "dprod_subset_Sigma2";
goal Univ.thy "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "dsum_Sigma";
val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
@@ -548,15 +546,15 @@
(*** Domain ***)
goal Univ.thy "fst `` diag(A) = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "fst_image_diag";
goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "fst_image_dprod";
goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "fst_image_dsum";
Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];
--- a/src/HOL/equalities.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/equalities.ML Fri Apr 04 11:18:52 1997 +0200
@@ -13,12 +13,12 @@
section "{}";
goal Set.thy "{x.False} = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Collect_False_empty";
Addsimps [Collect_False_empty];
goal Set.thy "(A <= {}) = (A = {})";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "subset_empty";
Addsimps [subset_empty];
@@ -26,7 +26,7 @@
(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
goal Set.thy "insert a A = {a} Un A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "insert_is_Un";
goal Set.thy "insert a A ~= {}";
@@ -38,55 +38,55 @@
Addsimps[empty_not_insert];
goal Set.thy "!!a. a:A ==> insert a A = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "insert_absorb";
goal Set.thy "insert x (insert x A) = insert x A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "insert_absorb2";
Addsimps [insert_absorb2];
goal Set.thy "insert x (insert y A) = insert y (insert x A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "insert_commute";
goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "insert_subset";
Addsimps[insert_subset];
(* use new B rather than (A-{a}) to avoid infinite unfolding *)
goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
by (res_inst_tac [("x","A-{a}")] exI 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "mk_disjoint_insert";
goal Set.thy
"!!A. A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "UN_insert_distrib";
goal Set.thy "(UN x. insert a (B x)) = insert a (UN x. B x)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "UN1_insert_distrib";
section "``";
goal Set.thy "f``{} = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "image_empty";
Addsimps[image_empty];
goal Set.thy "f``insert a B = insert (f a) (f``B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "image_insert";
Addsimps[image_insert];
qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
- (fn _ => [Fast_tac 1]);
+ (fn _ => [Blast_tac 1]);
goal Set.thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "insert_image";
Addsimps [insert_image];
@@ -94,7 +94,7 @@
"(%x. if P x then f x else g x) `` S \
\ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";
by (split_tac [expand_if] 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "if_image_distrib";
Addsimps[if_image_distrib];
@@ -102,53 +102,53 @@
section "range";
qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
- (fn _ => [Fast_tac 1]);
+ (fn _ => [Blast_tac 1]);
qed_goalw "image_range" Set.thy [image_def]
"f``range g = range (%x. f (g x))"
- (fn _ => [rtac Collect_cong 1, Fast_tac 1]);
+ (fn _ => [rtac Collect_cong 1, Blast_tac 1]);
section "Int";
goal Set.thy "A Int A = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_absorb";
Addsimps[Int_absorb];
goal Set.thy "A Int B = B Int A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_commute";
goal Set.thy "(A Int B) Int C = A Int (B Int C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_assoc";
goal Set.thy "{} Int B = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_empty_left";
Addsimps[Int_empty_left];
goal Set.thy "A Int {} = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_empty_right";
Addsimps[Int_empty_right];
goal Set.thy "UNIV Int B = B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_UNIV_left";
Addsimps[Int_UNIV_left];
goal Set.thy "A Int UNIV = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_UNIV_right";
Addsimps[Int_UNIV_right];
goal Set.thy "A Int (B Un C) = (A Int B) Un (A Int C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_Un_distrib";
goal Set.thy "(B Un C) Int A = (B Int A) Un (C Int A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_Un_distrib2";
goal Set.thy "(A<=B) = (A Int B = A)";
@@ -163,53 +163,53 @@
section "Un";
goal Set.thy "A Un A = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_absorb";
Addsimps[Un_absorb];
goal Set.thy "A Un B = B Un A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_commute";
goal Set.thy "(A Un B) Un C = A Un (B Un C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_assoc";
goal Set.thy "{} Un B = B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_empty_left";
Addsimps[Un_empty_left];
goal Set.thy "A Un {} = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_empty_right";
Addsimps[Un_empty_right];
goal Set.thy "UNIV Un B = UNIV";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_UNIV_left";
Addsimps[Un_UNIV_left];
goal Set.thy "A Un UNIV = UNIV";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_UNIV_right";
Addsimps[Un_UNIV_right];
goal Set.thy "(insert a B) Un C = insert a (B Un C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_insert_left";
goal Set.thy "A Un (insert a B) = insert a (A Un B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_insert_right";
goal Set.thy "(A Int B) Un C = (A Un C) Int (B Un C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_Int_distrib";
goal Set.thy
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_Int_crazy";
goal Set.thy "(A<=B) = (A Un B = B)";
@@ -217,7 +217,7 @@
qed "subset_Un_eq";
goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "subset_insert_iff";
goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
@@ -228,33 +228,33 @@
section "Compl";
goal Set.thy "A Int Compl(A) = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Compl_disjoint";
Addsimps[Compl_disjoint];
goal Set.thy "A Un Compl(A) = UNIV";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Compl_partition";
goal Set.thy "Compl(Compl(A)) = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "double_complement";
Addsimps[double_complement];
goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Compl_Un";
goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Compl_Int";
goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Compl_UN";
goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Compl_INT";
(*Halmos, Naive Set Theory, page 16.*)
@@ -267,27 +267,27 @@
section "Union";
goal Set.thy "Union({}) = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Union_empty";
Addsimps[Union_empty];
goal Set.thy "Union(UNIV) = UNIV";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Union_UNIV";
Addsimps[Union_UNIV];
goal Set.thy "Union(insert a B) = a Un Union(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Union_insert";
Addsimps[Union_insert];
goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Union_Un_distrib";
Addsimps[Union_Un_distrib];
goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Union_Int_subset";
val prems = goal Set.thy
@@ -298,26 +298,26 @@
section "Inter";
goal Set.thy "Inter({}) = UNIV";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Inter_empty";
Addsimps[Inter_empty];
goal Set.thy "Inter(UNIV) = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Inter_UNIV";
Addsimps[Inter_UNIV];
goal Set.thy "Inter(insert a B) = a Int Inter(B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Inter_insert";
Addsimps[Inter_insert];
goal Set.thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Inter_Un_subset";
goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
-by (best_tac (!claset) 1);
+by (Blast_tac 1);
qed "Inter_Un_distrib";
section "UN and INT";
@@ -325,134 +325,134 @@
(*Basic identities*)
goal Set.thy "(UN x:{}. B x) = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "UN_empty";
Addsimps[UN_empty];
goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "UN_UNIV";
Addsimps[UN_UNIV];
goal Set.thy "(INT x:{}. B x) = UNIV";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "INT_empty";
Addsimps[INT_empty];
goal Set.thy "(INT x:UNIV. B x) = (INT x. B x)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "INT_UNIV";
Addsimps[INT_UNIV];
goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "UN_insert";
Addsimps[UN_insert];
goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "INT_insert";
Addsimps[INT_insert];
goal Set.thy
"!!A. A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "INT_insert_distrib";
goal Set.thy "(INT x. insert a (B x)) = insert a (INT x. B x)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "INT1_insert_distrib";
goal Set.thy "Union(range(f)) = (UN x.f(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Union_range_eq";
goal Set.thy "Inter(range(f)) = (INT x.f(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Inter_range_eq";
goal Set.thy "Union(B``A) = (UN x:A. B(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Union_image_eq";
goal Set.thy "Inter(B``A) = (INT x:A. B(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Inter_image_eq";
goal Set.thy "!!A. a: A ==> (UN y:A. c) = c";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "UN_constant";
goal Set.thy "!!A. a: A ==> (INT y:A. c) = c";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "INT_constant";
goal Set.thy "(UN x.B) = B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "UN1_constant";
Addsimps[UN1_constant];
goal Set.thy "(INT x.B) = B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "INT1_constant";
Addsimps[INT1_constant];
goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "UN_eq";
(*Look: it has an EXISTENTIAL quantifier*)
goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "INT_eq";
(*Distributive laws...*)
goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_Union";
(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
Union of a family of unions **)
goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_Union_image";
(*Equivalent version*)
goal Set.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "UN_Un_distrib";
goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_Inter";
goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
-by (best_tac (!claset) 1);
+by (Blast_tac 1);
qed "Int_Inter_image";
(*Equivalent version*)
goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "INT_Int_distrib";
(*Halmos, Naive Set Theory, page 35.*)
goal Set.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_UN_distrib";
goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_INT_distrib";
goal Set.thy
"(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Int_UN_distrib2";
goal Set.thy
"(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Un_INT_distrib2";
@@ -462,58 +462,58 @@
body and (b) there are no similar rules for Int. **)
goal Set.thy "(ALL x:A Un B.P x) = ((ALL x:A.P x) & (ALL x:B.P x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "ball_Un";
goal Set.thy "(EX x:A Un B.P x) = ((EX x:A.P x) | (EX x:B.P x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "bex_Un";
section "-";
goal Set.thy "A-A = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Diff_cancel";
Addsimps[Diff_cancel];
goal Set.thy "{}-A = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "empty_Diff";
Addsimps[empty_Diff];
goal Set.thy "A-{} = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Diff_empty";
Addsimps[Diff_empty];
goal Set.thy "A-UNIV = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Diff_UNIV";
Addsimps[Diff_UNIV];
goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Diff_insert0";
Addsimps [Diff_insert0];
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
goal Set.thy "A - insert a B = A - B - {a}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Diff_insert";
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
goal Set.thy "A - insert a B = A - {a} - B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Diff_insert2";
goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "insert_Diff_if";
goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "insert_Diff1";
Addsimps [insert_Diff1];
@@ -522,24 +522,24 @@
qed "insert_Diff";
goal Set.thy "A Int (B-A) = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Diff_disjoint";
Addsimps[Diff_disjoint];
goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Diff_partition";
goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "double_diff";
goal Set.thy "A - (B Un C) = (A-B) Int (A-C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Diff_Un";
goal Set.thy "A - (B Int C) = (A-B) Un (A-C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Diff_Int";
Addsimps[subset_UNIV, empty_subsetI, subset_refl];
@@ -547,7 +547,7 @@
(** Miniscoping: pushing in big Unions and Intersections **)
local
- fun prover s = prove_goal Set.thy s (fn _ => [Fast_tac 1])
+ fun prover s = prove_goal Set.thy s (fn _ => [Blast_tac 1])
in
val UN1_simps = map prover
["(UN x. insert a (B x)) = insert a (UN x. B x)",
--- a/src/HOL/ex/Mutil.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/ex/Mutil.ML Fri Apr 04 11:18:52 1997 +0200
@@ -16,8 +16,8 @@
\ u: tiling A --> t <= Compl u --> t Un u : tiling A";
by (etac tiling.induct 1);
by (Simp_tac 1);
-by (fast_tac (!claset addIs tiling.intrs
- addss (!simpset addsimps [Un_assoc])) 1);
+by (simp_tac (!simpset addsimps [Un_assoc]) 1);
+by (blast_tac (!claset addIs tiling.intrs) 1);
qed_spec_mp "tiling_UnI";
@@ -29,19 +29,19 @@
goal thy "ALL i. (i: below k) = (i<k)";
by (nat_ind_tac "k" 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
-by (Fast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "below_less_iff";
Addsimps [below_less_iff];
goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Sigma_Suc1";
goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Sigma_Suc2";
(*Deletion is essential to allow use of Sigma_Suc1,2*)
@@ -55,17 +55,17 @@
by (subgoal_tac (*seems the easiest way of turning one to the other*)
"({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \
\ {(i, n1+n1), (i, Suc(n1+n1))}" 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
-by (fast_tac (!claset addEs [less_asym]
- addSDs [below_less_iff RS iffD1]) 1);
+by (blast_tac (!claset addEs [less_irrefl, less_asym]
+ addSDs [below_less_iff RS iffD1]) 1);
qed "dominoes_tile_row";
goal thy "(below m) Times below(n + n) : tiling domino";
by (nat_ind_tac "m" 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
-by (fast_tac (!claset addIs [equalityI, tiling_UnI, dominoes_tile_row]
- addEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
+by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row]
+ addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
qed "dominoes_tile_matrix";
@@ -83,11 +83,11 @@
bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "evnodd_Un";
goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "evnodd_Diff";
goalw thy [evnodd_def] "evnodd {} b = {}";
@@ -113,12 +113,12 @@
by (REPEAT (asm_full_simp_tac (!simpset addsimps
[less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc]
setloop split_tac [expand_if]) 1
- THEN Fast_tac 1));
+ THEN Blast_tac 1));
qed "domino_singleton";
goal thy "!!d. d:domino ==> finite d";
-by (fast_tac (!claset addSIs [finite_insertI, finite_emptyI]
- addEs [domino.elim]) 1);
+by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI]
+ addSEs [domino.elim]) 1);
qed "domino_finite";
@@ -127,7 +127,7 @@
goal thy "!!t. t:tiling domino ==> finite t";
by (eresolve_tac [tiling.induct] 1);
by (rtac finite_emptyI 1);
-by (fast_tac (!claset addIs [domino_finite, finite_UnI]) 1);
+by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
qed "tiling_domino_finite";
goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
@@ -143,7 +143,7 @@
tiling_domino_finite,
evnodd_subset RS finite_subset,
card_insert_disjoint]) 1);
-by (fast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
+by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
qed "tiling_domino_0_1";
goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n); \
--- a/src/HOL/ex/cla.ML Fri Apr 04 11:18:19 1997 +0200
+++ b/src/HOL/ex/cla.ML Fri Apr 04 11:18:52 1997 +0200
@@ -13,17 +13,17 @@
set_current_thy "HOL"; (*Boosts efficiency by omitting redundant rules*)
goal HOL.thy "(P --> Q | R) --> (P-->Q) | (P-->R)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*If and only if*)
goal HOL.thy "(P=Q) = (Q=P::bool)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
goal HOL.thy "~ (P = (~P))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
@@ -40,112 +40,112 @@
writeln"Pelletier's examples";
(*1*)
goal HOL.thy "(P-->Q) = (~Q --> ~P)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*2*)
goal HOL.thy "(~ ~ P) = P";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*3*)
goal HOL.thy "~(P-->Q) --> (Q-->P)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*4*)
goal HOL.thy "(~P-->Q) = (~Q --> P)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*5*)
goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*6*)
goal HOL.thy "P | ~ P";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*7*)
goal HOL.thy "P | ~ ~ ~ P";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*8. Peirce's law*)
goal HOL.thy "((P-->Q) --> P) --> P";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*9*)
goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*10*)
goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*11. Proved in each direction (incorrectly, says Pelletier!!) *)
goal HOL.thy "P=P::bool";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*12. "Dijkstra's law"*)
goal HOL.thy "((P = Q) = R) = (P = (Q = R))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*13. Distributive law*)
goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*14*)
goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*15*)
goal HOL.thy "(P --> Q) = (~P | Q)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*16*)
goal HOL.thy "(P-->Q) | (Q-->P)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*17*)
goal HOL.thy "((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Classical Logic: examples with quantifiers";
goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
goal HOL.thy "(? x. P-->Q(x)) = (P --> (? x.Q(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
goal HOL.thy "((! x.P(x)) | Q) = (! x. P(x) | Q)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*From Wishnu Prasetya*)
goal HOL.thy
"(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
\ --> p(t) | r(t)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
@@ -153,60 +153,60 @@
(*Needs multiple instantiation of the quantifier.*)
goal HOL.thy "(! x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
result();
(*Needs double instantiation of the quantifier*)
goal HOL.thy "? x. P(x) --> P(a) & P(b)";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
result();
goal HOL.thy "? z. P(z) --> (! x. P(x))";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
result();
goal HOL.thy "? x. (? y. P(y)) --> P(x)";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
result();
writeln"Hard examples with quantifiers";
writeln"Problem 18";
goal HOL.thy "? y. ! x. P(y)-->P(x)";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
result();
writeln"Problem 19";
goal HOL.thy "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
result();
writeln"Problem 20";
goal HOL.thy "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w))) \
\ --> (? x y. P(x) & Q(y)) --> (? z. R(z))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 21";
goal HOL.thy "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
result();
writeln"Problem 22";
goal HOL.thy "(! x. P = Q(x)) --> (P = (! x. Q(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 23";
goal HOL.thy "(! x. P | Q(x)) = (P | (! x. Q(x)))";
-by (Best_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 24";
goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) & \
\ (~(? x.P(x)) --> (? x.Q(x))) & (! x. Q(x)|R(x) --> S(x)) \
\ --> (? x. P(x)&R(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 25";
@@ -215,14 +215,14 @@
\ (! x. P(x) --> (M(x) & L(x))) & \
\ ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x))) \
\ --> (? x. Q(x)&P(x))";
-by (Best_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 26";
goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \
\ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \
\ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 27";
@@ -231,7 +231,7 @@
\ (! x. M(x) & L(x) --> P(x)) & \
\ ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x))) \
\ --> (! x. M(x) --> ~L(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 28. AMENDED";
@@ -239,21 +239,21 @@
\ ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) & \
\ ((? x.S(x)) --> (! x. L(x) --> M(x))) \
\ --> (! x. P(x) & L(x) --> M(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 29. Essentially the same as Principia Mathematica *11.71";
goal HOL.thy "(? x. F(x)) & (? y. G(y)) \
\ --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y))) = \
\ (! x y. F(x) & G(y) --> H(x) & J(y)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 30";
goal HOL.thy "(! x. P(x) | Q(x) --> ~ R(x)) & \
\ (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \
\ --> (! x. S(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 31";
@@ -261,7 +261,7 @@
\ (? x. L(x) & P(x)) & \
\ (! x. ~ R(x) --> M(x)) \
\ --> (? x. L(x) & M(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 32";
@@ -269,13 +269,13 @@
\ (! x. S(x) & R(x) --> L(x)) & \
\ (! x. M(x) --> R(x)) \
\ --> (! x. P(x) & M(x) --> L(x))";
-by (Best_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 33";
goal HOL.thy "(! x. P(a) & (P(x)-->P(b))-->P(c)) = \
\ (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
-by (Best_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 34 AMENDED (TWICE!!)";
@@ -284,13 +284,13 @@
\ ((? x. q(x)) = (! y. p(y)))) = \
\ ((? x. ! y. q(x) = q(y)) = \
\ ((? x. p(x)) = (! y. q(y))))";
-by (Deepen_tac 3 1);
+by (Blast_tac 1);
(*slower with smaller bounds*)
result();
writeln"Problem 35";
goal HOL.thy "? x y. P x y --> (! u v. P u v)";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
result();
writeln"Problem 36";
@@ -299,7 +299,7 @@
\ (! x y. J x y | G x y --> \
\ (! z. J y z | G y z --> H x z)) \
\ --> (! x. ? y. H x y)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 37";
@@ -308,7 +308,7 @@
\ (! x z. ~(P x z) --> (? y. Q y z)) & \
\ ((? x y. Q x y) --> (! x. R x x)) \
\ --> (! x. ? y. R x y)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 38";
@@ -318,35 +318,36 @@
\ (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) & \
\ (~p(a) | ~(? y. p(y) & r x y) | \
\ (? z. ? w. p(z) & r x w & r w z)))";
-by (Deepen_tac 0 1); (*beats fast_tac!*)
+by (Blast_tac 1); (*beats fast_tac!*)
result();
writeln"Problem 39";
goal HOL.thy "~ (? x. ! y. F y x = (~ F y y))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 40. AMENDED";
goal HOL.thy "(? y. ! x. F x y = F x x) \
\ --> ~ (! x. ? y. ! z. F z y = (~ F z x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 41";
goal HOL.thy "(! z. ? y. ! x. f x y = (f x z & ~ f x x)) \
\ --> ~ (? z. ! x. f x z)";
-by (Best_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 42";
goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))";
-by (Deepen_tac 3 1);
+by (Blast_tac 1);
result();
-writeln"Problem 43 NOT PROVED AUTOMATICALLY";
+writeln"Problem 43!!";
goal HOL.thy
"(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool))) \
\ --> (! x. (! y. q x y = (q y x::bool)))";
+by (Blast_tac 1);
writeln"Problem 44";
@@ -354,7 +355,7 @@
\ (? y. g(y) & h x y & (? y. g(y) & ~ h x y))) & \
\ (? x. j(x) & (! y. g(y) --> h x y)) \
\ --> (? x. j(x) & ~f(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 45";
@@ -365,7 +366,7 @@
\ (? x. f(x) & (! y. h x y --> l(y)) \
\ & (! y. g(y) & h x y --> j x y)) \
\ --> (? x. f(x) & ~ (? y. g(y) & h x y))";
-by (Best_tac 1);
+by (Blast_tac 1);
result();
@@ -373,7 +374,7 @@
writeln"Problem 48";
goal HOL.thy "(a=b | c=d) & (a=c | b=d) --> a=d | b=c";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 49 NOT PROVED AUTOMATICALLY";
@@ -386,20 +387,20 @@
by (assume_tac 1);
by (res_inst_tac [("x","b")] allE 1);
by (assume_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 50";
(*What has this to do with equality?*)
goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
result();
writeln"Problem 51";
goal HOL.thy
"(? z w. ! x y. P x y = (x=z & y=w)) --> \
\ (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))";
-by (Best_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 52";
@@ -407,7 +408,7 @@
goal HOL.thy
"(? z w. ! x y. P x y = (x=z & y=w)) --> \
\ (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))";
-by (Best_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 55";
@@ -423,20 +424,20 @@
\ (!x. hates agatha x --> hates butler x) & \
\ (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
\ killed ?who agatha";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 56";
goal HOL.thy
"(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 57";
goal HOL.thy
"P (f a b) (f b c) & P (f b c) (f a c) & \
\ (! x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 58 NOT PROVED AUTOMATICALLY";
@@ -447,13 +448,13 @@
writeln"Problem 59";
goal HOL.thy "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))";
-by (Deepen_tac 1 1);
+by (Blast_tac 1);
result();
writeln"Problem 60";
goal HOL.thy
"! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
@@ -461,7 +462,7 @@
"(ALL x. p a & (p x --> p(f x)) --> p(f(f x))) = \
\ (ALL x. (~ p a | p x | p(f(f x))) & \
\ (~ p a | ~ p(f x) | p(f(f x))))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
(*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
@@ -470,14 +471,14 @@
"(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
\ (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) & \
\ (ALL x. K(x) --> ~G(x)) --> (EX x. K(x) --> ~G(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();
goal Prod.thy
"(ALL x y. R(x,y) | R(y,x)) & \
\ (ALL x y. S(x,y) & S(y,x) --> x=y) & \
\ (ALL x y. R(x,y) --> S(x,y)) --> (ALL x y. S(x,y) --> R(x,y))";
-by (Fast_tac 1);
+by (Blast_tac 1);
result();