--- a/src/HOL/Fun.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Fun.ML Fri Apr 11 15:21:36 1997 +0200
@@ -23,7 +23,7 @@
val prems = goalw Fun.thy [inj_def]
"[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
qed "injI";
val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)";
@@ -69,7 +69,7 @@
val prems = goalw Fun.thy [inj_onto_def]
"(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_onto f A";
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
qed "inj_ontoI";
val [major] = goal Fun.thy
@@ -86,7 +86,7 @@
qed "inj_ontoD";
goal Fun.thy "!!x y.[| inj_onto f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)";
-by (fast_tac (!claset addSEs [inj_ontoD]) 1);
+by (blast_tac (!claset addSDs [inj_ontoD]) 1);
qed "inj_onto_iff";
val major::prems = goal Fun.thy
@@ -105,7 +105,7 @@
qed "comp_inj";
val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
-by (fast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
+by (blast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
qed "inj_imp";
val [prem] = goalw Fun.thy [inv_def] "y : range(f) ==> f(inv f y) = y";
@@ -118,9 +118,7 @@
by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
qed "inv_injective";
-val prems = goal Fun.thy
- "[| inj(f); A<=range(f) |] ==> inj_onto (inv f) A";
-by (cut_facts_tac prems 1);
+goal Fun.thy "!!f. [| inj(f); A<=range(f) |] ==> inj_onto (inv f) A";
by (fast_tac (!claset addIs [inj_ontoI]
addEs [inv_injective,injD]) 1);
qed "inj_onto_inv";
--- a/src/HOL/NatDef.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/NatDef.ML Fri Apr 11 15:21:36 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 (blast_tac (!claset addSEs [less_SucE] addIs [less_trans]) 1);
qed "less_Suc_eq";
val prems = goal thy "m<n ==> n ~= 0";
@@ -348,18 +348,18 @@
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 [Suc_mono, less_SucI] addEs [lessE]) 1);
+by (blast_tac (!claset addIs [Suc_mono, less_SucI] addEs [lessE]) 1);
qed "less_linear";
qed_goal "nat_less_cases" thy
"[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m"
-( fn prems =>
+( fn [major,eqCase,lessCase] =>
[
- (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
+ (rtac (less_linear RS disjE) 1),
(etac disjE 2),
- (etac (hd (tl (tl prems))) 1),
- (etac (sym RS hd (tl prems)) 1),
- (etac (hd prems) 1)
+ (etac lessCase 1),
+ (etac (sym RS eqCase) 1),
+ (etac major 1)
]);
(*Can be used with less_Suc_eq to get n=m | n<m *)
@@ -511,19 +511,19 @@
val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
by (dtac le_imp_less_or_eq 1);
-by (fast_tac (!claset addIs [less_trans]) 1);
+by (blast_tac (!claset addIs [less_trans]) 1);
qed "le_less_trans";
goal thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
by (dtac le_imp_less_or_eq 1);
-by (fast_tac (!claset addIs [less_trans]) 1);
+by (blast_tac (!claset addIs [less_trans]) 1);
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])]);
+ blast_tac (!claset addIs [less_trans])]);
qed "le_trans";
goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
@@ -634,9 +634,9 @@
(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 (!claset addSDs [Suc_less_SucD] addSEs [less_irrefl]
+ blast_tac (!claset addSDs [Suc_less_SucD] addSEs [less_irrefl]
addDs [less_trans_Suc]) 1,
- atac 1]);
+ assume_tac 1]);
val leD = le_eq_less_Suc RS iffD1;
val not_lessD = nat_leI RS leD;
val not_leD = not_leE
--- a/src/HOL/Option.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Option.ML Fri Apr 11 15:21:36 1997 +0200
@@ -11,7 +11,7 @@
val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))";
br (prem RS rev_mp) 1;
by (option.induct_tac "opt" 1);
- by (ALLGOALS(Fast_tac));
+ by (ALLGOALS Blast_tac);
bind_thm("optionE", standard(result() RS disjE));
(*
goal Option.thy "opt=None | (? x.opt=Some(x))";
--- a/src/HOL/Ord.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Ord.ML Fri Apr 11 15:21:36 1997 +0200
@@ -25,26 +25,26 @@
AddIffs [order_refl];
goal Ord.thy "~ x < (x::'a::order)";
-by(simp_tac (!simpset addsimps [order_less_le]) 1);
+by (simp_tac (!simpset addsimps [order_less_le]) 1);
qed "order_less_irrefl";
AddIffs [order_less_irrefl];
goal thy "(x::'a::order) <= y = (x < y | x = y)";
-by(simp_tac (!simpset addsimps [order_less_le]) 1);
-by(Fast_tac 1);
+by (simp_tac (!simpset addsimps [order_less_le]) 1);
+by (Blast_tac 1);
qed "order_le_less";
(** min **)
goalw thy [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
-by(split_tac [expand_if] 1);
-by(Asm_simp_tac 1);
+by (split_tac [expand_if] 1);
+by (Asm_simp_tac 1);
qed "min_leastL";
val prems = goalw thy [min_def]
"(!!x::'a::order. least <= x) ==> min x least = least";
-by(cut_facts_tac prems 1);
-by(split_tac [expand_if] 1);
-by(Asm_simp_tac 1);
-by(fast_tac (!claset addEs [order_antisym]) 1);
+by (cut_facts_tac prems 1);
+by (split_tac [expand_if] 1);
+by (Asm_simp_tac 1);
+by (blast_tac (!claset addIs [order_antisym]) 1);
qed "min_leastR";
--- a/src/HOL/Prod.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Prod.ML Fri Apr 11 15:21:36 1997 +0200
@@ -33,15 +33,15 @@
AddSEs [Pair_inject];
goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Pair_eq";
goalw Prod.thy [fst_def] "fst((a,b)) = a";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
qed "fst_conv";
goalw Prod.thy [snd_def] "snd((a,b)) = b";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
qed "snd_conv";
goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
@@ -119,12 +119,12 @@
goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
by (stac surjective_pairing 1);
by (stac split 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "expand_split";
(** split used as a logical connective or set former **)
-(*These rules are for use with fast_tac.
+(*These rules are for use with blast_tac.
Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
@@ -193,8 +193,8 @@
by (rtac (major RS imageE) 1);
by (res_inst_tac [("p","x")] PairE 1);
by (resolve_tac prems 1);
-by (Fast_tac 2);
-by (fast_tac (!claset addIs [prod_fun]) 1);
+by (Blast_tac 2);
+by (blast_tac (!claset addIs [prod_fun]) 1);
qed "prod_fun_imageE";
(*** Disjoint union of a family of sets - Sigma ***)
@@ -239,19 +239,19 @@
val prems = goal Prod.thy
"[| A<=C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
by (cut_facts_tac prems 1);
-by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
+by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
qed "Sigma_mono";
qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
Addsimps [Sigma_empty1,Sigma_empty2];
goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "mem_Sigma_iff";
Addsimps [mem_Sigma_iff];
@@ -259,7 +259,7 @@
(*Suggested by Pierre Chartier*)
goal Prod.thy
"(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "UNION_Times_distrib";
(*** Domain of a relation ***)
--- a/src/HOL/RelPow.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/RelPow.ML Fri Apr 11 15:21:36 1997 +0200
@@ -35,7 +35,7 @@
"[| (x,z) : R^(Suc n); !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
by (cut_facts_tac [major] 1);
by (Asm_full_simp_tac 1);
-by (fast_tac (!claset addIs [minor]) 1);
+by (blast_tac (!claset addIs [minor]) 1);
qed "rel_pow_Suc_E";
val [p1,p2,p3] = goal RelPow.thy
@@ -102,7 +102,7 @@
qed "rel_pow_imp_rtrancl";
goal RelPow.thy "R^* = (UN n. R^n)";
-by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
+by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
qed "rtrancl_is_UN_rel_pow";
--- a/src/HOL/Set.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Set.ML Fri Apr 11 15:21:36 1997 +0200
@@ -220,7 +220,7 @@
qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
(fn [prem]=>
- [ (fast_tac (!claset addIs [prem RS FalseE]) 1) ]);
+ [ (blast_tac (!claset addIs [prem RS FalseE]) 1) ]);
qed_goal "equals0D" Set.thy "!!a. [| A={}; a:A |] ==> P"
(fn _ => [ (Blast_tac 1) ]);
@@ -418,7 +418,7 @@
(fn _ => [Blast_tac 1]);
goal Set.thy "!!a b. {a}={b} ==> a=b";
-by (fast_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
qed "singleton_inject";
(*Redundant? But unlike insertCI, it proves the subgoal immediately!*)
@@ -622,11 +622,11 @@
AddSEs [imageE];
goalw thy [o_def] "(f o g)``r = f``(g``r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "image_compose";
goal thy "f``(A Un B) = f``A Un f``B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "image_Un";
--- a/src/HOL/Trancl.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Trancl.ML Fri Apr 11 15:21:36 1997 +0200
@@ -52,7 +52,7 @@
\ !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |] ==> P((x,z)) |] \
\ ==> P((a,b))";
by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
qed "rtrancl_full_induct";
(*nice induction rule*)
@@ -67,8 +67,8 @@
by (Blast_tac 1);
(*now do the induction*)
by (resolve_tac [major RS rtrancl_full_induct] 1);
-by (fast_tac (!claset addIs prems) 1);
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
qed "rtrancl_induct";
bind_thm
@@ -93,8 +93,8 @@
\ |] ==> P";
by (subgoal_tac "(a::'a) = b | (? y. (a,y) : r^* & (y,b) : r)" 1);
by (rtac (major RS rtrancl_induct) 2);
-by (fast_tac (!claset addIs prems) 2);
-by (fast_tac (!claset addIs prems) 2);
+by (blast_tac (!claset addIs prems) 2);
+by (blast_tac (!claset addIs prems) 2);
by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
qed "rtranclE";
@@ -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 addSDs[rtrancl_converseD])1);
+by (blast_tac (!claset addIs prems addSDs[rtrancl_converseD])1);
qed "converse_rtrancl_induct";
val prems = goal Trancl.thy
@@ -227,7 +227,7 @@
(*now solve first subgoal: this formula is sufficient*)
by (Blast_tac 1);
by (etac rtrancl_induct 1);
-by (ALLGOALS (fast_tac (!claset addIs (rtrancl_into_trancl1::prems))));
+by (ALLGOALS (blast_tac (!claset addIs (rtrancl_into_trancl1::prems))));
qed "trancl_induct";
(*elimination of r^+ -- NOT an induction rule*)
--- a/src/HOL/Univ.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Univ.ML Fri Apr 11 15:21:36 1997 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/univ
+(* Title: HOL/Univ
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -147,7 +147,7 @@
qed "Scons_inject_lemma1";
goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
-by (fast_tac (!claset addSDs [Push_Node_inject]) 1);
+by (blast_tac (!claset addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma2";
val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
--- a/src/HOL/WF.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/WF.ML Fri Apr 11 15:21:36 1997 +0200
@@ -27,7 +27,7 @@
\ !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \
\ |] ==> P(a)";
by (rtac (major RS spec RS mp RS spec) 1);
-by (fast_tac (!claset addEs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
qed "wf_induct";
(*Perform induction on i, then prove the wf(r) subgoal using prems. *)
@@ -38,9 +38,9 @@
val prems = goal WF.thy "[| wf(r); (a,x):r; (x,a):r |] ==> P";
by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
by (wf_ind_tac "a" prems 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "wf_asym";
val prems = goal WF.thy "[| wf(r); (a,a): r |] ==> P";
@@ -58,8 +58,8 @@
by (res_inst_tac [("a","x")] (prem RS wf_induct) 1);
by (rtac (impI RS allI) 1);
by (etac tranclE 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
qed "wf_trancl";
--- a/src/HOL/ex/MT.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/ex/MT.ML Fri Apr 11 15:21:36 1997 +0200
@@ -17,30 +17,11 @@
open MT;
-(*Limit cyclic unifications during monotonicity proofs*)
-val orig_search_bound = !Unify.search_bound;
-Unify.search_bound := 8;
-
-val prems = goal MT.thy "~a:{b} ==> ~a=b";
-by (cut_facts_tac prems 1);
-by (rtac notI 1);
-by (dtac notE 1);
-by (hyp_subst_tac 1);
-by (rtac singletonI 1);
-by (assume_tac 1);
-qed "notsingletonI";
-
(* ############################################################ *)
(* Inference systems *)
(* ############################################################ *)
-val infsys_mono_tac =
- (rewtac subset_def) THEN (safe_tac (claset_of "HOL")) THEN (rtac ballI 1) THEN
- (rtac CollectI 1) THEN (dtac CollectD 1) THEN
- REPEAT
- ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN
- (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac ((claset_of "Fun")delrules [equalityI]) 1)
- );
+val infsys_mono_tac = (REPEAT (ares_tac (basic_monos@[allI,impI]) 1));
val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
by (simp_tac (!simpset addsimps prems) 1);
@@ -102,7 +83,7 @@
by (rtac (monoh RS monoD) 1);
by (rtac (UnE RS subsetI) 1);
by (assume_tac 1);
-by (fast_tac (!claset addSIs [cih]) 1);
+by (blast_tac (!claset addSIs [cih]) 1);
by (rtac (monoh RS monoD RS subsetD) 1);
by (rtac Un_upper2 1);
by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
@@ -169,7 +150,8 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (Fast_tac 1);
+ (*Naughty! But the quantifiers are nested VERY deeply...*)
+by (blast_tac (!claset addSIs [exI]) 1);
qed "eval_const";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -178,7 +160,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
qed "eval_var2";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -187,7 +169,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
qed "eval_fn";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -197,7 +179,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
qed "eval_fix";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -207,7 +189,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
qed "eval_app1";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -220,7 +202,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (fast_tac (!claset addSIs [disjI2]) 1);
+by (blast_tac (!claset addSIs [disjI2]) 1);
qed "eval_app2";
(* Strong elimination, induction on evaluations *)
@@ -250,7 +232,7 @@
by (dtac CollectD 1);
by (safe_tac (!claset));
by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS (Blast_tac));
qed "eval_ind0";
val prems = goal MT.thy
@@ -287,51 +269,46 @@
(* Introduction rules *)
-val prems = goalw MT.thy [elab_def, elab_rel_def]
- "c isof ty ==> te |- e_const(c) ===> ty";
-by (cut_facts_tac prems 1);
+goalw MT.thy [elab_def, elab_rel_def]
+ "!!te. c isof ty ==> te |- e_const(c) ===> ty";
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
qed "elab_const";
-val prems = goalw MT.thy [elab_def, elab_rel_def]
- "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
-by (cut_facts_tac prems 1);
+goalw MT.thy [elab_def, elab_rel_def]
+ "!!te. x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
qed "elab_var";
-val prems = goalw MT.thy [elab_def, elab_rel_def]
- "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
-by (cut_facts_tac prems 1);
+goalw MT.thy [elab_def, elab_rel_def]
+ "!!te. te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
qed "elab_fn";
-val prems = goalw MT.thy [elab_def, elab_rel_def]
- " te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
-\ te |- fix f(x) = e ===> ty1->ty2";
-by (cut_facts_tac prems 1);
+goalw MT.thy [elab_def, elab_rel_def]
+ "!!te. te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
+\ te |- fix f(x) = e ===> ty1->ty2";
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [exI]) 1);
qed "elab_fix";
-val prems = goalw MT.thy [elab_def, elab_rel_def]
- " [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
-\ te |- e1 @ e2 ===> ty2";
-by (cut_facts_tac prems 1);
+goalw MT.thy [elab_def, elab_rel_def]
+ "!!te. [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
+\ te |- e1 @ e2 ===> ty2";
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (fast_tac (!claset addSIs [disjI2]) 1);
+by (blast_tac (!claset addSIs [disjI2]) 1);
qed "elab_app";
(* Strong elimination, induction on elaborations *)
@@ -361,7 +338,7 @@
by (dtac CollectD 1);
by (safe_tac (!claset));
by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS (Blast_tac));
qed "elab_ind0";
val prems = goal MT.thy
@@ -412,7 +389,7 @@
by (dtac CollectD 1);
by (safe_tac (!claset));
by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS (Blast_tac));
qed "elab_elim0";
val prems = goal MT.thy
@@ -441,7 +418,7 @@
fun elab_e_elim_tac p =
( (rtac elab_elim 1) THEN
(resolve_tac p 1) THEN
- (REPEAT (fast_tac (e_ext_cs (claset_of "HOL")) 1))
+ (REPEAT (blast_tac (e_ext_cs HOL_cs) 1))
);
val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
@@ -451,7 +428,7 @@
val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
by (cut_facts_tac prems 1);
by (dtac elab_const_elim_lem 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "elab_const_elim";
val prems = goal MT.thy
@@ -463,7 +440,7 @@
"te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
by (cut_facts_tac prems 1);
by (dtac elab_var_elim_lem 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "elab_var_elim";
val prems = goal MT.thy
@@ -479,7 +456,7 @@
\ (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
by (cut_facts_tac prems 1);
by (dtac elab_fn_elim_lem 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "elab_fn_elim";
val prems = goal MT.thy
@@ -494,7 +471,7 @@
\ (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
by (cut_facts_tac prems 1);
by (dtac elab_fix_elim_lem 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "elab_fix_elim";
val prems = goal MT.thy
@@ -507,7 +484,7 @@
"te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)";
by (cut_facts_tac prems 1);
by (dtac elab_app_elim_lem 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "elab_app_elim";
(* ############################################################ *)
@@ -518,7 +495,8 @@
goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
by infsys_mono_tac;
-bind_thm("mono_hasty_fun", result());
+by (Blast_tac 1);
+qed "mono_hasty_fun";
(*
Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it
@@ -534,7 +512,7 @@
by (rewtac MT.hasty_fun_def);
by (rtac CollectI 1);
by (rtac disjI1 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (rtac mono_hasty_fun 1);
qed "hasty_rel_const_coind";
@@ -553,7 +531,7 @@
by (rewtac hasty_fun_def);
by (rtac CollectI 1);
by (rtac disjI2 1);
-by (fast_tac (claset_of "HOL") 1);
+by (blast_tac HOL_cs 1);
by (rtac mono_hasty_fun 1);
qed "hasty_rel_clos_coind";
@@ -575,8 +553,7 @@
by (dtac CollectD 1);
by (fold_goals_tac [hasty_fun_def]);
by (safe_tac (!claset));
-by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (Fast_tac));
+by (REPEAT (ares_tac prems 1));
qed "hasty_rel_elim0";
val prems = goal MT.thy
@@ -597,29 +574,27 @@
(* Introduction rules for hasty *)
-val prems = goalw MT.thy [hasty_def] "c isof t ==> v_const(c) hasty t";
-by (resolve_tac (prems RL [hasty_rel_const_coind]) 1);
+goalw MT.thy [hasty_def] "!!c. c isof t ==> v_const(c) hasty t";
+by (etac hasty_rel_const_coind 1);
qed "hasty_const";
-val prems = goalw MT.thy [hasty_def,hasty_env_def]
- "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
-by (cut_facts_tac prems 1);
+goalw MT.thy [hasty_def,hasty_env_def]
+ "!!t. te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
by (rtac hasty_rel_clos_coind 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS (blast_tac (!claset delrules [equalityI])));
qed "hasty_clos";
(* Elimination on constants for hasty *)
-val prems = goalw MT.thy [hasty_def]
- "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";
-by (cut_facts_tac prems 1);
+goalw MT.thy [hasty_def]
+ "!!v. v hasty t ==> (!c.(v = v_const(c) --> c isof t))";
by (rtac hasty_rel_elim 1);
-by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
+by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
qed "hasty_elim_const_lem";
-val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";
-by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);
-by (Fast_tac 1);
+goal MT.thy "!!c. v_const(c) hasty t ==> c isof t";
+by (dtac hasty_elim_const_lem 1);
+by (Blast_tac 1);
qed "hasty_elim_const";
(* Elimination on closures for hasty *)
@@ -630,14 +605,14 @@
\ v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
by (cut_facts_tac prems 1);
by (rtac hasty_rel_elim 1);
-by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
+by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
qed "hasty_elim_clos_lem";
-val prems = goal MT.thy
- "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===>\
- \t & ve hastyenv te ";
-by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
-by (Fast_tac 1);
+goal MT.thy
+ "!!t. v_clos(<|ev,e,ve|>) hasty t ==> \
+\ ? te.te |- fn ev => e ===> t & ve hastyenv te ";
+by (dtac hasty_elim_clos_lem 1);
+by (Blast_tac 1);
qed "hasty_elim_clos";
(* ############################################################ *)
@@ -650,10 +625,10 @@
by (rewtac hasty_env_def);
by (asm_full_simp_tac (!simpset delsimps mem_simps
addsimps [ve_dom_owr, te_dom_owr]) 1);
-by (safe_tac (claset_of "HOL"));
+by (safe_tac HOL_cs);
by (excluded_middle_tac "ev=x" 1);
by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (asm_simp_tac (!simpset addsimps [ve_app_owr1, te_app_owr1]) 1);
qed "hasty_env1";
@@ -661,38 +636,34 @@
(* The Consistency theorem *)
(* ############################################################ *)
-val prems = goal MT.thy
- "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
-by (cut_facts_tac prems 1);
+goal MT.thy
+ "!!t. [| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
by (dtac elab_const_elim 1);
by (etac hasty_const 1);
qed "consistency_const";
-val prems = goalw MT.thy [hasty_env_def]
- " [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
-\ ve_app ve ev hasty t";
-by (cut_facts_tac prems 1);
+goalw MT.thy [hasty_env_def]
+ "!!t. [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
+\ ve_app ve ev hasty t";
by (dtac elab_var_elim 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "consistency_var";
-val prems = goal MT.thy
- " [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
-\ v_clos(<| ev, e, ve |>) hasty t";
-by (cut_facts_tac prems 1);
+goal MT.thy
+ "!!t. [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
+\ v_clos(<| ev, e, ve |>) hasty t";
by (rtac hasty_clos 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "consistency_fn";
-val prems = goalw MT.thy [hasty_env_def,hasty_def]
- " [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
+goalw MT.thy [hasty_env_def,hasty_def]
+ "!!t. [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
\ ve hastyenv te ; \
\ te |- fix ev2 ev1 = e ===> t \
\ |] ==> \
\ v_clos(cl) hasty t";
-by (cut_facts_tac prems 1);
by (dtac elab_fix_elim 1);
-by (safe_tac (claset_of "HOL"));
+by (safe_tac HOL_cs);
(*Do a single unfolding of cl*)
by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
by (rtac hasty_rel_clos_coind 1);
@@ -700,37 +671,36 @@
by (asm_simp_tac (!simpset addsimps [ve_dom_owr, te_dom_owr]) 1);
by (asm_simp_tac (!simpset delsimps mem_simps addsimps [ve_dom_owr]) 1);
-by (safe_tac (claset_of "HOL"));
+by (safe_tac HOL_cs);
by (excluded_middle_tac "ev2=ev1a" 1);
by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (asm_simp_tac (!simpset delsimps mem_simps
addsimps [ve_app_owr1, te_app_owr1]) 1);
by (hyp_subst_tac 1);
by (etac subst 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "consistency_fix";
-val prems = goal MT.thy
- " [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t; \
+goal MT.thy
+ "!!t. [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v_const(c2) hasty t; \
\ ve hastyenv te ; te |- e1 @ e2 ===> t \
\ |] ==> \
\ v_const(c_app c1 c2) hasty t";
-by (cut_facts_tac prems 1);
by (dtac elab_app_elim 1);
by (safe_tac (!claset));
by (rtac hasty_const 1);
by (rtac isof_app 1);
by (rtac hasty_elim_const 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (rtac hasty_elim_const 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "consistency_app1";
-val prems = goal MT.thy
- " [| ! t te. \
+goal MT.thy
+ "!!t. [| ! t te. \
\ ve hastyenv te --> \
\ te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v2 hasty t; \
@@ -740,7 +710,6 @@
\ te |- e1 @ e2 ===> t \
\ |] ==> \
\ v hasty t";
-by (cut_facts_tac prems 1);
by (dtac elab_app_elim 1);
by (safe_tac (!claset));
by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
@@ -754,10 +723,7 @@
by (dtac hasty_elim_clos 1);
by (safe_tac (!claset));
by (dtac elab_fn_elim 1);
-by (safe_tac (!claset));
-by (dtac t_fun_inj 1);
-by (safe_tac (!claset));
-by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (Fast_tac 1));
+by (blast_tac (!claset addIs [hasty_env1] addSDs [t_fun_inj]) 1);
qed "consistency_app2";
val [major] = goal MT.thy
@@ -795,10 +761,7 @@
by (cut_facts_tac prems 1);
by (rtac hasty_elim_const 1);
by (dtac consistency 1);
-by (fast_tac (!claset addSIs [basic_consistency_lem]) 1);
+by (blast_tac (!claset addSIs [basic_consistency_lem]) 1);
qed "basic_consistency";
-
-Unify.search_bound := orig_search_bound;
-
writeln"Reached end of file.";
--- a/src/HOL/ex/Simult.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/ex/Simult.ML Fri Apr 11 15:21:36 1997 +0200
@@ -29,7 +29,7 @@
goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
by (rtac lfp_lowerbound 1);
-by (fast_tac (!claset addIs sexp.intrs@[sexp_In0I, sexp_In1I]
+by (blast_tac (!claset addIs sexp.intrs@[sexp_In0I, sexp_In1I]
addSEs [PartE]) 1);
qed "TF_sexp";
@@ -50,7 +50,7 @@
\ |] ==> R(FCONS M N) \
\ |] ==> R(i)";
by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
-by (fast_tac (!claset addIs (prems@[PartI])
+by (blast_tac (!claset addIs (prems@[PartI])
addEs [usumE, uprodE, PartE]) 1);
qed "TF_induct";
@@ -59,13 +59,9 @@
"!!A. ! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
\ (M: Part (TF A) In1 --> Q(M)) \
\ ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "TF_induct_lemma";
-AddSIs [PartI];
-AddSDs [In0_inject, In1_inject];
-AddSEs [PartE];
-
(*Could prove ~ TCONS M N : Part (TF A) In1 etc. *)
(*Induction on TF with separate predicates P, Q*)
@@ -93,12 +89,12 @@
(Tree_Forest_induct RS conjE) 1);
(*Instantiates ?A1 to range(Leaf). *)
by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst,
- Rep_Forest_inverse RS subst]
- addSIs [Rep_Tree,Rep_Forest]) 4);
+ Rep_Forest_inverse RS subst]
+ addSIs [Rep_Tree,Rep_Forest]) 4);
(*Cannot use simplifier: the rewrites work in the wrong direction!*)
by (ALLGOALS (fast_tac (!claset addSEs [Abs_Tree_inverse RS subst,
- Abs_Forest_inverse RS subst]
- addSIs prems)));
+ Abs_Forest_inverse RS subst]
+ addSIs prems)));
qed "tree_forest_induct";
@@ -135,38 +131,38 @@
AddIs [TF_I, uprodI, usum_In0I, usum_In1I];
AddSEs [Scons_inject];
-val prems = goalw Simult.thy TF_Rep_defs
- "[| a: A; M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
-by (fast_tac (!claset addIs prems) 1);
+goalw Simult.thy TF_Rep_defs
+ "!!A. [| a: A; M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
+by (Blast_tac 1);
qed "TCONS_I";
(* FNIL is a TF(A) -- this also justifies the type definition*)
goalw Simult.thy TF_Rep_defs "FNIL: Part (TF A) In1";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "FNIL_I";
-val prems = goalw Simult.thy TF_Rep_defs
- "[| M: Part (TF A) In0; N: Part (TF A) In1 |] ==> \
-\ FCONS M N : Part (TF A) In1";
-by (fast_tac (!claset addIs prems) 1);
+goalw Simult.thy TF_Rep_defs
+ "!!A. [| M: Part (TF A) In0; N: Part (TF A) In1 |] ==> \
+\ FCONS M N : Part (TF A) In1";
+by (Blast_tac 1);
qed "FCONS_I";
(** Injectiveness of TCONS and FCONS **)
goalw Simult.thy TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "TCONS_TCONS_eq";
bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
goalw Simult.thy TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "FCONS_FCONS_eq";
bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
(** Distinctness of TCONS, FNIL and FCONS **)
goalw Simult.thy TF_Rep_defs "TCONS M N ~= FNIL";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "TCONS_not_FNIL";
bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
@@ -174,7 +170,7 @@
val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
goalw Simult.thy TF_Rep_defs "FCONS M N ~= FNIL";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "FCONS_not_FNIL";
bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
@@ -182,7 +178,7 @@
val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
goalw Simult.thy TF_Rep_defs "TCONS M N ~= FCONS K L";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "TCONS_not_FCONS";
bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
@@ -206,12 +202,12 @@
Leaf_inject];
goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Tcons_Tcons_eq";
bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
goalw Simult.thy [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Fcons_not_Fnil";
bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
@@ -221,7 +217,7 @@
(** Injectiveness of Fcons **)
goalw Simult.thy [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Fcons_Fcons_eq";
bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
--- a/src/HOL/ex/set.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/ex/set.ML Fri Apr 11 15:21:36 1997 +0200
@@ -43,19 +43,18 @@
(*** The Schroder-Berstein Theorem ***)
-val prems = goalw Lfp.thy [image_def] "inj(f) ==> inv(f)``(f``X) = X";
-by (cut_facts_tac prems 1);
+goalw Lfp.thy [image_def] "!!f. inj(f) ==> inv(f)``(f``X) = X";
by (rtac equalityI 1);
by (fast_tac (!claset addEs [inv_f_f RS ssubst]) 1);
by (fast_tac (!claset addEs [inv_f_f RS ssubst]) 1);
qed "inv_image_comp";
goal Set.thy "!!f. f(a) ~: (f``X) ==> a~:X";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "contra_imageI";
goal Lfp.thy "(a ~: Compl(X)) = (a:X)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "not_Compl";
(*Lots of backtracking in this proof...*)
@@ -69,11 +68,11 @@
goalw Lfp.thy [image_def]
"range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "range_if_then_else";
goal Lfp.thy "a : X Un Compl(X)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "X_Un_Compl";
goalw Lfp.thy [surj_def] "surj(f) = (!a. a : range(f))";
--- a/src/HOL/simpdata.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/simpdata.ML Fri Apr 11 15:21:36 1997 +0200
@@ -55,7 +55,7 @@
local
- fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
+ fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
val P_imp_P_iff_True = prover "P --> (P = True)" RS mp;
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
@@ -118,7 +118,7 @@
val imp_cong = impI RSN
(2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
- (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
+ (fn _=> [blast_tac HOL_cs 1]) RS mp RS mp);
(*Miniscoping: pushing in existential quantifiers*)
val ex_simps = map prover
@@ -153,7 +153,7 @@
end;
-fun prove nm thm = qed_goal nm HOL.thy thm (fn _ => [fast_tac HOL_cs 1]);
+fun prove nm thm = qed_goal nm HOL.thy thm (fn _ => [blast_tac HOL_cs 1]);
prove "conj_commute" "(P&Q) = (Q&P)";
prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
@@ -196,19 +196,19 @@
let val th = prove_goal HOL.thy
"(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
- (fn _=> [fast_tac HOL_cs 1])
+ (fn _=> [blast_tac HOL_cs 1])
in bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp))) end;
let val th = prove_goal HOL.thy
"(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
- (fn _=> [fast_tac HOL_cs 1])
+ (fn _=> [blast_tac HOL_cs 1])
in bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp))) end;
(* '|' congruence rule: not included by default! *)
let val th = prove_goal HOL.thy
"(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
- (fn _=> [fast_tac HOL_cs 1])
+ (fn _=> [blast_tac HOL_cs 1])
in bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp))) end;
prove "eq_sym_conv" "(x=y) = (y=x)";
@@ -220,10 +220,10 @@
(fn [prem] => [rewtac prem, rtac refl 1]);
qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
- (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
+ (fn _=>[blast_tac (HOL_cs addIs [select_equality]) 1]);
qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y"
- (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
+ (fn _=>[blast_tac (HOL_cs addIs [select_equality]) 1]);
qed_goal "if_P" HOL.thy "P ==> (if P then x else y) = x"
(fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
@@ -232,14 +232,14 @@
(fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);
*)
qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
- (fn _ => [fast_tac (HOL_cs addIs [select_equality]) 1]);
+ (fn _ => [blast_tac (HOL_cs addIs [select_equality]) 1]);
qed_goal "expand_if" HOL.thy
"P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
(fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
stac if_P 2,
stac if_not_P 1,
- REPEAT(fast_tac HOL_cs 1) ]);
+ REPEAT(blast_tac HOL_cs 1) ]);
qed_goal "if_bool_eq" HOL.thy
"(if P then Q else R) = ((P-->Q) & (~P-->R))"
@@ -257,7 +257,7 @@
qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
- (fn _ => [split_tac [expand_if] 1, fast_tac HOL_cs 1]);
+ (fn _ => [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
(** 'if' congruence rules: neither included by default! *)
@@ -267,7 +267,7 @@
\ (if b then x else y) = (if c then u else v)"
(fn rew::prems =>
[stac rew 1, stac expand_if 1, stac expand_if 1,
- fast_tac (HOL_cs addDs prems) 1]);
+ blast_tac (HOL_cs addDs prems) 1]);
(*Prevents simplification of x and y: much faster*)
qed_goal "if_weak_cong" HOL.thy