Yet more fast_tac->blast_tac, and other tidying
authorpaulson
Fri Apr 11 15:21:36 1997 +0200 (1997-04-11)
changeset 2935998cb95fdd43
parent 2934 bd922fc9001b
child 2936 bd33e7aae062
Yet more fast_tac->blast_tac, and other tidying
src/HOL/Fun.ML
src/HOL/NatDef.ML
src/HOL/Option.ML
src/HOL/Ord.ML
src/HOL/Prod.ML
src/HOL/RelPow.ML
src/HOL/Set.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/WF.ML
src/HOL/ex/MT.ML
src/HOL/ex/Simult.ML
src/HOL/ex/set.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Fun.ML	Fri Apr 11 11:33:51 1997 +0200
     1.2 +++ b/src/HOL/Fun.ML	Fri Apr 11 15:21:36 1997 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5  val prems = goalw Fun.thy [inj_def]
     1.6      "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
     1.7 -by (fast_tac (!claset addIs prems) 1);
     1.8 +by (blast_tac (!claset addIs prems) 1);
     1.9  qed "injI";
    1.10  
    1.11  val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)";
    1.12 @@ -69,7 +69,7 @@
    1.13  
    1.14  val prems = goalw Fun.thy [inj_onto_def]
    1.15      "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
    1.16 -by (fast_tac (!claset addIs prems) 1);
    1.17 +by (blast_tac (!claset addIs prems) 1);
    1.18  qed "inj_ontoI";
    1.19  
    1.20  val [major] = goal Fun.thy 
    1.21 @@ -86,7 +86,7 @@
    1.22  qed "inj_ontoD";
    1.23  
    1.24  goal Fun.thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
    1.25 -by (fast_tac (!claset addSEs [inj_ontoD]) 1);
    1.26 +by (blast_tac (!claset addSDs [inj_ontoD]) 1);
    1.27  qed "inj_onto_iff";
    1.28  
    1.29  val major::prems = goal Fun.thy
    1.30 @@ -105,7 +105,7 @@
    1.31  qed "comp_inj";
    1.32  
    1.33  val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
    1.34 -by (fast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
    1.35 +by (blast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
    1.36  qed "inj_imp";
    1.37  
    1.38  val [prem] = goalw Fun.thy [inv_def] "y : range(f) ==> f(inv f y) = y";
    1.39 @@ -118,9 +118,7 @@
    1.40  by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
    1.41  qed "inv_injective";
    1.42  
    1.43 -val prems = goal Fun.thy
    1.44 -    "[| inj(f);  A<=range(f) |] ==> inj_onto (inv f) A";
    1.45 -by (cut_facts_tac prems 1);
    1.46 +goal Fun.thy "!!f. [| inj(f);  A<=range(f) |] ==> inj_onto (inv f) A";
    1.47  by (fast_tac (!claset addIs [inj_ontoI] 
    1.48                        addEs [inv_injective,injD]) 1);
    1.49  qed "inj_onto_inv";
     2.1 --- a/src/HOL/NatDef.ML	Fri Apr 11 11:33:51 1997 +0200
     2.2 +++ b/src/HOL/NatDef.ML	Fri Apr 11 15:21:36 1997 +0200
     2.3 @@ -278,7 +278,7 @@
     2.4  qed "less_SucE";
     2.5  
     2.6  goal thy "(m < Suc(n)) = (m < n | m = n)";
     2.7 -by (fast_tac (!claset addEs [less_trans, less_SucE]) 1);
     2.8 +by (blast_tac (!claset addSEs [less_SucE] addIs [less_trans]) 1);
     2.9  qed "less_Suc_eq";
    2.10  
    2.11  val prems = goal thy "m<n ==> n ~= 0";
    2.12 @@ -348,18 +348,18 @@
    2.13  by (nat_ind_tac "n" 1);
    2.14  by (rtac (refl RS disjI1 RS disjI2) 1);
    2.15  by (rtac (zero_less_Suc RS disjI1) 1);
    2.16 -by (fast_tac (!claset addIs [Suc_mono, less_SucI] addEs [lessE]) 1);
    2.17 +by (blast_tac (!claset addIs [Suc_mono, less_SucI] addEs [lessE]) 1);
    2.18  qed "less_linear";
    2.19  
    2.20  qed_goal "nat_less_cases" thy 
    2.21     "[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m"
    2.22 -( fn prems =>
    2.23 +( fn [major,eqCase,lessCase] =>
    2.24          [
    2.25 -        (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
    2.26 +        (rtac (less_linear RS disjE) 1),
    2.27          (etac disjE 2),
    2.28 -        (etac (hd (tl (tl prems))) 1),
    2.29 -        (etac (sym RS hd (tl prems)) 1),
    2.30 -        (etac (hd prems) 1)
    2.31 +        (etac lessCase 1),
    2.32 +        (etac (sym RS eqCase) 1),
    2.33 +        (etac major 1)
    2.34          ]);
    2.35  
    2.36  (*Can be used with less_Suc_eq to get n=m | n<m *)
    2.37 @@ -511,19 +511,19 @@
    2.38  
    2.39  val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
    2.40  by (dtac le_imp_less_or_eq 1);
    2.41 -by (fast_tac (!claset addIs [less_trans]) 1);
    2.42 +by (blast_tac (!claset addIs [less_trans]) 1);
    2.43  qed "le_less_trans";
    2.44  
    2.45  goal thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
    2.46  by (dtac le_imp_less_or_eq 1);
    2.47 -by (fast_tac (!claset addIs [less_trans]) 1);
    2.48 +by (blast_tac (!claset addIs [less_trans]) 1);
    2.49  qed "less_le_trans";
    2.50  
    2.51  goal thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
    2.52  by (EVERY1[dtac le_imp_less_or_eq, 
    2.53  	   dtac le_imp_less_or_eq,
    2.54  	   rtac less_or_eq_imp_le, 
    2.55 -	   fast_tac (!claset addIs [less_trans])]);
    2.56 +	   blast_tac (!claset addIs [less_trans])]);
    2.57  qed "le_trans";
    2.58  
    2.59  goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
    2.60 @@ -634,9 +634,9 @@
    2.61    (fn _ => [etac swap2 1, etac leD 1]);
    2.62  val eqI = prove_goal thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n"
    2.63    (fn _ => [etac less_SucE 1,
    2.64 -            fast_tac (!claset addSDs [Suc_less_SucD] addSEs [less_irrefl]
    2.65 +            blast_tac (!claset addSDs [Suc_less_SucD] addSEs [less_irrefl]
    2.66                                addDs [less_trans_Suc]) 1,
    2.67 -            atac 1]);
    2.68 +            assume_tac 1]);
    2.69  val leD = le_eq_less_Suc RS iffD1;
    2.70  val not_lessD = nat_leI RS leD;
    2.71  val not_leD = not_leE
     3.1 --- a/src/HOL/Option.ML	Fri Apr 11 11:33:51 1997 +0200
     3.2 +++ b/src/HOL/Option.ML	Fri Apr 11 15:21:36 1997 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))";
     3.5   br (prem RS rev_mp) 1;
     3.6   by (option.induct_tac "opt" 1);
     3.7 - by (ALLGOALS(Fast_tac));
     3.8 + by (ALLGOALS Blast_tac);
     3.9  bind_thm("optionE", standard(result() RS disjE));
    3.10  (*
    3.11  goal Option.thy "opt=None | (? x.opt=Some(x))"; 
     4.1 --- a/src/HOL/Ord.ML	Fri Apr 11 11:33:51 1997 +0200
     4.2 +++ b/src/HOL/Ord.ML	Fri Apr 11 15:21:36 1997 +0200
     4.3 @@ -25,26 +25,26 @@
     4.4  AddIffs [order_refl];
     4.5  
     4.6  goal Ord.thy "~ x < (x::'a::order)";
     4.7 -by(simp_tac (!simpset addsimps [order_less_le]) 1);
     4.8 +by (simp_tac (!simpset addsimps [order_less_le]) 1);
     4.9  qed "order_less_irrefl";
    4.10  AddIffs [order_less_irrefl];
    4.11  
    4.12  goal thy "(x::'a::order) <= y = (x < y | x = y)";
    4.13 -by(simp_tac (!simpset addsimps [order_less_le]) 1);
    4.14 -by(Fast_tac 1);
    4.15 +by (simp_tac (!simpset addsimps [order_less_le]) 1);
    4.16 +by (Blast_tac 1);
    4.17  qed "order_le_less";
    4.18  
    4.19  (** min **)
    4.20  
    4.21  goalw thy [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
    4.22 -by(split_tac [expand_if] 1);
    4.23 -by(Asm_simp_tac 1);
    4.24 +by (split_tac [expand_if] 1);
    4.25 +by (Asm_simp_tac 1);
    4.26  qed "min_leastL";
    4.27  
    4.28  val prems = goalw thy [min_def]
    4.29   "(!!x::'a::order. least <= x) ==> min x least = least";
    4.30 -by(cut_facts_tac prems 1);
    4.31 -by(split_tac [expand_if] 1);
    4.32 -by(Asm_simp_tac 1);
    4.33 -by(fast_tac (!claset addEs [order_antisym]) 1);
    4.34 +by (cut_facts_tac prems 1);
    4.35 +by (split_tac [expand_if] 1);
    4.36 +by (Asm_simp_tac 1);
    4.37 +by (blast_tac (!claset addIs [order_antisym]) 1);
    4.38  qed "min_leastR";
     5.1 --- a/src/HOL/Prod.ML	Fri Apr 11 11:33:51 1997 +0200
     5.2 +++ b/src/HOL/Prod.ML	Fri Apr 11 15:21:36 1997 +0200
     5.3 @@ -33,15 +33,15 @@
     5.4  AddSEs [Pair_inject];
     5.5  
     5.6  goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
     5.7 -by (Fast_tac 1);
     5.8 +by (Blast_tac 1);
     5.9  qed "Pair_eq";
    5.10  
    5.11  goalw Prod.thy [fst_def] "fst((a,b)) = a";
    5.12 -by (fast_tac (!claset addIs [select_equality]) 1);
    5.13 +by (blast_tac (!claset addIs [select_equality]) 1);
    5.14  qed "fst_conv";
    5.15  
    5.16  goalw Prod.thy [snd_def] "snd((a,b)) = b";
    5.17 -by (fast_tac (!claset addIs [select_equality]) 1);
    5.18 +by (blast_tac (!claset addIs [select_equality]) 1);
    5.19  qed "snd_conv";
    5.20  
    5.21  goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
    5.22 @@ -119,12 +119,12 @@
    5.23  goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
    5.24  by (stac surjective_pairing 1);
    5.25  by (stac split 1);
    5.26 -by (Fast_tac 1);
    5.27 +by (Blast_tac 1);
    5.28  qed "expand_split";
    5.29  
    5.30  (** split used as a logical connective or set former **)
    5.31  
    5.32 -(*These rules are for use with fast_tac.
    5.33 +(*These rules are for use with blast_tac.
    5.34    Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
    5.35  
    5.36  goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
    5.37 @@ -193,8 +193,8 @@
    5.38  by (rtac (major RS imageE) 1);
    5.39  by (res_inst_tac [("p","x")] PairE 1);
    5.40  by (resolve_tac prems 1);
    5.41 -by (Fast_tac 2);
    5.42 -by (fast_tac (!claset addIs [prod_fun]) 1);
    5.43 +by (Blast_tac 2);
    5.44 +by (blast_tac (!claset addIs [prod_fun]) 1);
    5.45  qed "prod_fun_imageE";
    5.46  
    5.47  (*** Disjoint union of a family of sets - Sigma ***)
    5.48 @@ -239,19 +239,19 @@
    5.49  val prems = goal Prod.thy
    5.50      "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
    5.51  by (cut_facts_tac prems 1);
    5.52 -by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
    5.53 +by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
    5.54  qed "Sigma_mono";
    5.55  
    5.56  qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
    5.57 - (fn _ => [ (Fast_tac 1) ]);
    5.58 + (fn _ => [ (Blast_tac 1) ]);
    5.59  
    5.60  qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
    5.61 - (fn _ => [ (Fast_tac 1) ]);
    5.62 + (fn _ => [ (Blast_tac 1) ]);
    5.63  
    5.64  Addsimps [Sigma_empty1,Sigma_empty2]; 
    5.65  
    5.66  goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
    5.67 -by (Fast_tac 1);
    5.68 +by (Blast_tac 1);
    5.69  qed "mem_Sigma_iff";
    5.70  Addsimps [mem_Sigma_iff]; 
    5.71  
    5.72 @@ -259,7 +259,7 @@
    5.73  (*Suggested by Pierre Chartier*)
    5.74  goal Prod.thy
    5.75       "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
    5.76 -by (Fast_tac 1);
    5.77 +by (Blast_tac 1);
    5.78  qed "UNION_Times_distrib";
    5.79  
    5.80  (*** Domain of a relation ***)
     6.1 --- a/src/HOL/RelPow.ML	Fri Apr 11 11:33:51 1997 +0200
     6.2 +++ b/src/HOL/RelPow.ML	Fri Apr 11 15:21:36 1997 +0200
     6.3 @@ -35,7 +35,7 @@
     6.4    "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
     6.5  by (cut_facts_tac [major] 1);
     6.6  by (Asm_full_simp_tac  1);
     6.7 -by (fast_tac (!claset addIs [minor]) 1);
     6.8 +by (blast_tac (!claset addIs [minor]) 1);
     6.9  qed "rel_pow_Suc_E";
    6.10  
    6.11  val [p1,p2,p3] = goal RelPow.thy
    6.12 @@ -102,7 +102,7 @@
    6.13  qed "rel_pow_imp_rtrancl";
    6.14  
    6.15  goal RelPow.thy "R^* = (UN n. R^n)";
    6.16 -by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
    6.17 +by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
    6.18  qed "rtrancl_is_UN_rel_pow";
    6.19  
    6.20  
     7.1 --- a/src/HOL/Set.ML	Fri Apr 11 11:33:51 1997 +0200
     7.2 +++ b/src/HOL/Set.ML	Fri Apr 11 15:21:36 1997 +0200
     7.3 @@ -220,7 +220,7 @@
     7.4  
     7.5  qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
     7.6   (fn [prem]=>
     7.7 -  [ (fast_tac (!claset addIs [prem RS FalseE]) 1) ]);
     7.8 +  [ (blast_tac (!claset addIs [prem RS FalseE]) 1) ]);
     7.9  
    7.10  qed_goal "equals0D" Set.thy "!!a. [| A={};  a:A |] ==> P"
    7.11   (fn _ => [ (Blast_tac 1) ]);
    7.12 @@ -418,7 +418,7 @@
    7.13  (fn _ => [Blast_tac 1]);
    7.14  
    7.15  goal Set.thy "!!a b. {a}={b} ==> a=b";
    7.16 -by (fast_tac (!claset addEs [equalityE]) 1);
    7.17 +by (blast_tac (!claset addEs [equalityE]) 1);
    7.18  qed "singleton_inject";
    7.19  
    7.20  (*Redundant? But unlike insertCI, it proves the subgoal immediately!*)
    7.21 @@ -622,11 +622,11 @@
    7.22  AddSEs [imageE]; 
    7.23  
    7.24  goalw thy [o_def] "(f o g)``r = f``(g``r)";
    7.25 -by (Fast_tac 1);
    7.26 +by (Blast_tac 1);
    7.27  qed "image_compose";
    7.28  
    7.29  goal thy "f``(A Un B) = f``A Un f``B";
    7.30 -by (Fast_tac 1);
    7.31 +by (Blast_tac 1);
    7.32  qed "image_Un";
    7.33  
    7.34  
     8.1 --- a/src/HOL/Trancl.ML	Fri Apr 11 11:33:51 1997 +0200
     8.2 +++ b/src/HOL/Trancl.ML	Fri Apr 11 15:21:36 1997 +0200
     8.3 @@ -52,7 +52,7 @@
     8.4  \     !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |]  ==>  P((x,z)) |] \
     8.5  \  ==>  P((a,b))";
     8.6  by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
     8.7 -by (fast_tac (!claset addIs prems) 1);
     8.8 +by (blast_tac (!claset addIs prems) 1);
     8.9  qed "rtrancl_full_induct";
    8.10  
    8.11  (*nice induction rule*)
    8.12 @@ -67,8 +67,8 @@
    8.13  by (Blast_tac 1);
    8.14  (*now do the induction*)
    8.15  by (resolve_tac [major RS rtrancl_full_induct] 1);
    8.16 -by (fast_tac (!claset addIs prems) 1);
    8.17 -by (fast_tac (!claset addIs prems) 1);
    8.18 +by (blast_tac (!claset addIs prems) 1);
    8.19 +by (blast_tac (!claset addIs prems) 1);
    8.20  qed "rtrancl_induct";
    8.21  
    8.22  bind_thm
    8.23 @@ -93,8 +93,8 @@
    8.24  \    |] ==> P";
    8.25  by (subgoal_tac "(a::'a) = b  | (? y. (a,y) : r^* & (y,b) : r)" 1);
    8.26  by (rtac (major RS rtrancl_induct) 2);
    8.27 -by (fast_tac (!claset addIs prems) 2);
    8.28 -by (fast_tac (!claset addIs prems) 2);
    8.29 +by (blast_tac (!claset addIs prems) 2);
    8.30 +by (blast_tac (!claset addIs prems) 2);
    8.31  by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
    8.32  qed "rtranclE";
    8.33  
    8.34 @@ -165,7 +165,7 @@
    8.35  \     ==> P(a)";
    8.36  by (rtac ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1);
    8.37  by (resolve_tac prems 1);
    8.38 -by (fast_tac (!claset addIs prems addSDs[rtrancl_converseD])1);
    8.39 +by (blast_tac (!claset addIs prems addSDs[rtrancl_converseD])1);
    8.40  qed "converse_rtrancl_induct";
    8.41  
    8.42  val prems = goal Trancl.thy
    8.43 @@ -227,7 +227,7 @@
    8.44  (*now solve first subgoal: this formula is sufficient*)
    8.45  by (Blast_tac 1);
    8.46  by (etac rtrancl_induct 1);
    8.47 -by (ALLGOALS (fast_tac (!claset addIs (rtrancl_into_trancl1::prems))));
    8.48 +by (ALLGOALS (blast_tac (!claset addIs (rtrancl_into_trancl1::prems))));
    8.49  qed "trancl_induct";
    8.50  
    8.51  (*elimination of r^+ -- NOT an induction rule*)
     9.1 --- a/src/HOL/Univ.ML	Fri Apr 11 11:33:51 1997 +0200
     9.2 +++ b/src/HOL/Univ.ML	Fri Apr 11 15:21:36 1997 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOL/univ
     9.5 +(*  Title:      HOL/Univ
     9.6      ID:         $Id$
     9.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.8      Copyright   1991  University of Cambridge
     9.9 @@ -147,7 +147,7 @@
    9.10  qed "Scons_inject_lemma1";
    9.11  
    9.12  goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
    9.13 -by (fast_tac (!claset addSDs [Push_Node_inject]) 1);
    9.14 +by (blast_tac (!claset addSDs [Push_Node_inject]) 1);
    9.15  qed "Scons_inject_lemma2";
    9.16  
    9.17  val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
    10.1 --- a/src/HOL/WF.ML	Fri Apr 11 11:33:51 1997 +0200
    10.2 +++ b/src/HOL/WF.ML	Fri Apr 11 15:21:36 1997 +0200
    10.3 @@ -27,7 +27,7 @@
    10.4  \       !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \
    10.5  \    |]  ==>  P(a)";
    10.6  by (rtac (major RS spec RS mp RS spec) 1);
    10.7 -by (fast_tac (!claset addEs prems) 1);
    10.8 +by (blast_tac (!claset addIs prems) 1);
    10.9  qed "wf_induct";
   10.10  
   10.11  (*Perform induction on i, then prove the wf(r) subgoal using prems. *)
   10.12 @@ -38,9 +38,9 @@
   10.13  
   10.14  val prems = goal WF.thy "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
   10.15  by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
   10.16 -by (fast_tac (!claset addIs prems) 1);
   10.17 +by (blast_tac (!claset addIs prems) 1);
   10.18  by (wf_ind_tac "a" prems 1);
   10.19 -by (Fast_tac 1);
   10.20 +by (Blast_tac 1);
   10.21  qed "wf_asym";
   10.22  
   10.23  val prems = goal WF.thy "[| wf(r);  (a,a): r |] ==> P";
   10.24 @@ -58,8 +58,8 @@
   10.25  by (res_inst_tac [("a","x")] (prem RS wf_induct) 1);
   10.26  by (rtac (impI RS allI) 1);
   10.27  by (etac tranclE 1);
   10.28 -by (Fast_tac 1);
   10.29 -by (Fast_tac 1);
   10.30 +by (Blast_tac 1);
   10.31 +by (Blast_tac 1);
   10.32  qed "wf_trancl";
   10.33  
   10.34  
    11.1 --- a/src/HOL/ex/MT.ML	Fri Apr 11 11:33:51 1997 +0200
    11.2 +++ b/src/HOL/ex/MT.ML	Fri Apr 11 15:21:36 1997 +0200
    11.3 @@ -17,30 +17,11 @@
    11.4  
    11.5  open MT;
    11.6  
    11.7 -(*Limit cyclic unifications during monotonicity proofs*)
    11.8 -val orig_search_bound = !Unify.search_bound;
    11.9 -Unify.search_bound := 8;
   11.10 -
   11.11 -val prems = goal MT.thy "~a:{b} ==> ~a=b";
   11.12 -by (cut_facts_tac prems 1);
   11.13 -by (rtac notI 1);
   11.14 -by (dtac notE 1);
   11.15 -by (hyp_subst_tac 1);
   11.16 -by (rtac singletonI 1);
   11.17 -by (assume_tac 1);
   11.18 -qed "notsingletonI";
   11.19 -
   11.20  (* ############################################################ *)
   11.21  (* Inference systems                                            *)
   11.22  (* ############################################################ *)
   11.23  
   11.24 -val infsys_mono_tac =
   11.25 -  (rewtac subset_def) THEN (safe_tac (claset_of "HOL")) THEN (rtac ballI 1) THEN
   11.26 -  (rtac CollectI 1) THEN (dtac CollectD 1) THEN
   11.27 -  REPEAT 
   11.28 -    ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN
   11.29 -      (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac ((claset_of "Fun")delrules [equalityI]) 1)
   11.30 -    );
   11.31 +val infsys_mono_tac = (REPEAT (ares_tac (basic_monos@[allI,impI]) 1));
   11.32  
   11.33  val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
   11.34  by (simp_tac (!simpset addsimps prems) 1);
   11.35 @@ -102,7 +83,7 @@
   11.36  by (rtac (monoh RS monoD) 1);
   11.37  by (rtac (UnE RS subsetI) 1);
   11.38  by (assume_tac 1);
   11.39 -by (fast_tac (!claset addSIs [cih]) 1);
   11.40 +by (blast_tac (!claset addSIs [cih]) 1);
   11.41  by (rtac (monoh RS monoD RS subsetD) 1);
   11.42  by (rtac Un_upper2 1);
   11.43  by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
   11.44 @@ -169,7 +150,8 @@
   11.45  by (rtac lfp_intro2 1);
   11.46  by (rtac eval_fun_mono 1);
   11.47  by (rewtac eval_fun_def);
   11.48 -by (Fast_tac 1);
   11.49 +	(*Naughty!  But the quantifiers are nested VERY deeply...*)
   11.50 +by (blast_tac (!claset addSIs [exI]) 1);
   11.51  qed "eval_const";
   11.52  
   11.53  val prems = goalw MT.thy [eval_def, eval_rel_def] 
   11.54 @@ -178,7 +160,7 @@
   11.55  by (rtac lfp_intro2 1);
   11.56  by (rtac eval_fun_mono 1);
   11.57  by (rewtac eval_fun_def);
   11.58 -by (Fast_tac 1);
   11.59 +by (blast_tac (!claset addSIs [exI]) 1);
   11.60  qed "eval_var2";
   11.61  
   11.62  val prems = goalw MT.thy [eval_def, eval_rel_def] 
   11.63 @@ -187,7 +169,7 @@
   11.64  by (rtac lfp_intro2 1);
   11.65  by (rtac eval_fun_mono 1);
   11.66  by (rewtac eval_fun_def);
   11.67 -by (Fast_tac 1);
   11.68 +by (blast_tac (!claset addSIs [exI]) 1);
   11.69  qed "eval_fn";
   11.70  
   11.71  val prems = goalw MT.thy [eval_def, eval_rel_def] 
   11.72 @@ -197,7 +179,7 @@
   11.73  by (rtac lfp_intro2 1);
   11.74  by (rtac eval_fun_mono 1);
   11.75  by (rewtac eval_fun_def);
   11.76 -by (Fast_tac 1);
   11.77 +by (blast_tac (!claset addSIs [exI]) 1);
   11.78  qed "eval_fix";
   11.79  
   11.80  val prems = goalw MT.thy [eval_def, eval_rel_def]
   11.81 @@ -207,7 +189,7 @@
   11.82  by (rtac lfp_intro2 1);
   11.83  by (rtac eval_fun_mono 1);
   11.84  by (rewtac eval_fun_def);
   11.85 -by (Fast_tac 1);
   11.86 +by (blast_tac (!claset addSIs [exI]) 1);
   11.87  qed "eval_app1";
   11.88  
   11.89  val prems = goalw MT.thy [eval_def, eval_rel_def] 
   11.90 @@ -220,7 +202,7 @@
   11.91  by (rtac lfp_intro2 1);
   11.92  by (rtac eval_fun_mono 1);
   11.93  by (rewtac eval_fun_def);
   11.94 -by (fast_tac (!claset addSIs [disjI2]) 1);
   11.95 +by (blast_tac (!claset addSIs [disjI2]) 1);
   11.96  qed "eval_app2";
   11.97  
   11.98  (* Strong elimination, induction on evaluations *)
   11.99 @@ -250,7 +232,7 @@
  11.100  by (dtac CollectD 1);
  11.101  by (safe_tac (!claset));
  11.102  by (ALLGOALS (resolve_tac prems));
  11.103 -by (ALLGOALS (Fast_tac));
  11.104 +by (ALLGOALS (Blast_tac));
  11.105  qed "eval_ind0";
  11.106  
  11.107  val prems = goal MT.thy 
  11.108 @@ -287,51 +269,46 @@
  11.109  
  11.110  (* Introduction rules *)
  11.111  
  11.112 -val prems = goalw MT.thy [elab_def, elab_rel_def] 
  11.113 -  "c isof ty ==> te |- e_const(c) ===> ty";
  11.114 -by (cut_facts_tac prems 1);
  11.115 +goalw MT.thy [elab_def, elab_rel_def] 
  11.116 +  "!!te. c isof ty ==> te |- e_const(c) ===> ty";
  11.117  by (rtac lfp_intro2 1);
  11.118  by (rtac elab_fun_mono 1);
  11.119  by (rewtac elab_fun_def);
  11.120 -by (Fast_tac 1);
  11.121 +by (blast_tac (!claset addSIs [exI]) 1);
  11.122  qed "elab_const";
  11.123  
  11.124 -val prems = goalw MT.thy [elab_def, elab_rel_def] 
  11.125 -  "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
  11.126 -by (cut_facts_tac prems 1);
  11.127 +goalw MT.thy [elab_def, elab_rel_def] 
  11.128 +  "!!te. x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
  11.129  by (rtac lfp_intro2 1);
  11.130  by (rtac elab_fun_mono 1);
  11.131  by (rewtac elab_fun_def);
  11.132 -by (Fast_tac 1);
  11.133 +by (blast_tac (!claset addSIs [exI]) 1);
  11.134  qed "elab_var";
  11.135  
  11.136 -val prems = goalw MT.thy [elab_def, elab_rel_def] 
  11.137 -  "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
  11.138 -by (cut_facts_tac prems 1);
  11.139 +goalw MT.thy [elab_def, elab_rel_def] 
  11.140 +  "!!te. te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
  11.141  by (rtac lfp_intro2 1);
  11.142  by (rtac elab_fun_mono 1);
  11.143  by (rewtac elab_fun_def);
  11.144 -by (Fast_tac 1);
  11.145 +by (blast_tac (!claset addSIs [exI]) 1);
  11.146  qed "elab_fn";
  11.147  
  11.148 -val prems = goalw MT.thy [elab_def, elab_rel_def]
  11.149 -  " te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
  11.150 -\   te |- fix f(x) = e ===> ty1->ty2";
  11.151 -by (cut_facts_tac prems 1);
  11.152 +goalw MT.thy [elab_def, elab_rel_def]
  11.153 +  "!!te. te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
  11.154 +\        te |- fix f(x) = e ===> ty1->ty2";
  11.155  by (rtac lfp_intro2 1);
  11.156  by (rtac elab_fun_mono 1);
  11.157  by (rewtac elab_fun_def);
  11.158 -by (Fast_tac 1);
  11.159 +by (blast_tac (!claset addSIs [exI]) 1);
  11.160  qed "elab_fix";
  11.161  
  11.162 -val prems = goalw MT.thy [elab_def, elab_rel_def] 
  11.163 -  " [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
  11.164 -\   te |- e1 @ e2 ===> ty2";
  11.165 -by (cut_facts_tac prems 1);
  11.166 +goalw MT.thy [elab_def, elab_rel_def] 
  11.167 +  "!!te. [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
  11.168 +\        te |- e1 @ e2 ===> ty2";
  11.169  by (rtac lfp_intro2 1);
  11.170  by (rtac elab_fun_mono 1);
  11.171  by (rewtac elab_fun_def);
  11.172 -by (fast_tac (!claset addSIs [disjI2]) 1);
  11.173 +by (blast_tac (!claset addSIs [disjI2]) 1);
  11.174  qed "elab_app";
  11.175  
  11.176  (* Strong elimination, induction on elaborations *)
  11.177 @@ -361,7 +338,7 @@
  11.178  by (dtac CollectD 1);
  11.179  by (safe_tac (!claset));
  11.180  by (ALLGOALS (resolve_tac prems));
  11.181 -by (ALLGOALS (Fast_tac));
  11.182 +by (ALLGOALS (Blast_tac));
  11.183  qed "elab_ind0";
  11.184  
  11.185  val prems = goal MT.thy
  11.186 @@ -412,7 +389,7 @@
  11.187  by (dtac CollectD 1);
  11.188  by (safe_tac (!claset));
  11.189  by (ALLGOALS (resolve_tac prems));
  11.190 -by (ALLGOALS (Fast_tac));
  11.191 +by (ALLGOALS (Blast_tac));
  11.192  qed "elab_elim0";
  11.193  
  11.194  val prems = goal MT.thy
  11.195 @@ -441,7 +418,7 @@
  11.196  fun elab_e_elim_tac p = 
  11.197    ( (rtac elab_elim 1) THEN 
  11.198      (resolve_tac p 1) THEN 
  11.199 -    (REPEAT (fast_tac (e_ext_cs (claset_of "HOL")) 1))
  11.200 +    (REPEAT (blast_tac (e_ext_cs HOL_cs) 1))
  11.201    );
  11.202  
  11.203  val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
  11.204 @@ -451,7 +428,7 @@
  11.205  val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
  11.206  by (cut_facts_tac prems 1);
  11.207  by (dtac elab_const_elim_lem 1);
  11.208 -by (Fast_tac 1);
  11.209 +by (Blast_tac 1);
  11.210  qed "elab_const_elim";
  11.211  
  11.212  val prems = goal MT.thy 
  11.213 @@ -463,7 +440,7 @@
  11.214    "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
  11.215  by (cut_facts_tac prems 1);
  11.216  by (dtac elab_var_elim_lem 1);
  11.217 -by (Fast_tac 1);
  11.218 +by (Blast_tac 1);
  11.219  qed "elab_var_elim";
  11.220  
  11.221  val prems = goal MT.thy 
  11.222 @@ -479,7 +456,7 @@
  11.223  \   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
  11.224  by (cut_facts_tac prems 1);
  11.225  by (dtac elab_fn_elim_lem 1);
  11.226 -by (Fast_tac 1);
  11.227 +by (Blast_tac 1);
  11.228  qed "elab_fn_elim";
  11.229  
  11.230  val prems = goal MT.thy 
  11.231 @@ -494,7 +471,7 @@
  11.232  \   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
  11.233  by (cut_facts_tac prems 1);
  11.234  by (dtac elab_fix_elim_lem 1);
  11.235 -by (Fast_tac 1);
  11.236 +by (Blast_tac 1);
  11.237  qed "elab_fix_elim";
  11.238  
  11.239  val prems = goal MT.thy 
  11.240 @@ -507,7 +484,7 @@
  11.241   "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
  11.242  by (cut_facts_tac prems 1);
  11.243  by (dtac elab_app_elim_lem 1);
  11.244 -by (Fast_tac 1);
  11.245 +by (Blast_tac 1);
  11.246  qed "elab_app_elim";
  11.247  
  11.248  (* ############################################################ *)
  11.249 @@ -518,7 +495,8 @@
  11.250  
  11.251  goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
  11.252  by infsys_mono_tac;
  11.253 -bind_thm("mono_hasty_fun",  result());
  11.254 +by (Blast_tac 1);
  11.255 +qed "mono_hasty_fun";
  11.256  
  11.257  (* 
  11.258    Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it 
  11.259 @@ -534,7 +512,7 @@
  11.260  by (rewtac MT.hasty_fun_def);
  11.261  by (rtac CollectI 1);
  11.262  by (rtac disjI1 1);
  11.263 -by (Fast_tac 1);
  11.264 +by (Blast_tac 1);
  11.265  by (rtac mono_hasty_fun 1);
  11.266  qed "hasty_rel_const_coind";
  11.267  
  11.268 @@ -553,7 +531,7 @@
  11.269  by (rewtac hasty_fun_def);
  11.270  by (rtac CollectI 1);
  11.271  by (rtac disjI2 1);
  11.272 -by (fast_tac (claset_of "HOL") 1);
  11.273 +by (blast_tac HOL_cs 1);
  11.274  by (rtac mono_hasty_fun 1);
  11.275  qed "hasty_rel_clos_coind";
  11.276  
  11.277 @@ -575,8 +553,7 @@
  11.278  by (dtac CollectD 1);
  11.279  by (fold_goals_tac [hasty_fun_def]);
  11.280  by (safe_tac (!claset));
  11.281 -by (ALLGOALS (resolve_tac prems));
  11.282 -by (ALLGOALS (Fast_tac));
  11.283 +by (REPEAT (ares_tac prems 1));
  11.284  qed "hasty_rel_elim0";
  11.285  
  11.286  val prems = goal MT.thy 
  11.287 @@ -597,29 +574,27 @@
  11.288  
  11.289  (* Introduction rules for hasty *)
  11.290  
  11.291 -val prems = goalw MT.thy [hasty_def] "c isof t ==> v_const(c) hasty t";
  11.292 -by (resolve_tac (prems RL [hasty_rel_const_coind]) 1);
  11.293 +goalw MT.thy [hasty_def] "!!c. c isof t ==> v_const(c) hasty t";
  11.294 +by (etac hasty_rel_const_coind 1);
  11.295  qed "hasty_const";
  11.296  
  11.297 -val prems = goalw MT.thy [hasty_def,hasty_env_def] 
  11.298 -  "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
  11.299 -by (cut_facts_tac prems 1);
  11.300 +goalw MT.thy [hasty_def,hasty_env_def] 
  11.301 + "!!t. te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
  11.302  by (rtac hasty_rel_clos_coind 1);
  11.303 -by (ALLGOALS (Fast_tac));
  11.304 +by (ALLGOALS (blast_tac (!claset delrules [equalityI])));
  11.305  qed "hasty_clos";
  11.306  
  11.307  (* Elimination on constants for hasty *)
  11.308  
  11.309 -val prems = goalw MT.thy [hasty_def] 
  11.310 -  "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
  11.311 -by (cut_facts_tac prems 1);
  11.312 +goalw MT.thy [hasty_def] 
  11.313 +  "!!v. v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
  11.314  by (rtac hasty_rel_elim 1);
  11.315 -by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
  11.316 +by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
  11.317  qed "hasty_elim_const_lem";
  11.318  
  11.319 -val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";
  11.320 -by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);
  11.321 -by (Fast_tac 1);
  11.322 +goal MT.thy "!!c. v_const(c) hasty t ==> c isof t";
  11.323 +by (dtac hasty_elim_const_lem 1);
  11.324 +by (Blast_tac 1);
  11.325  qed "hasty_elim_const";
  11.326  
  11.327  (* Elimination on closures for hasty *)
  11.328 @@ -630,14 +605,14 @@
  11.329  \     v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
  11.330  by (cut_facts_tac prems 1);
  11.331  by (rtac hasty_rel_elim 1);
  11.332 -by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
  11.333 +by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
  11.334  qed "hasty_elim_clos_lem";
  11.335  
  11.336 -val prems = goal MT.thy 
  11.337 -  "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===>\
  11.338 -  \t & ve hastyenv te ";
  11.339 -by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
  11.340 -by (Fast_tac 1);
  11.341 +goal MT.thy 
  11.342 +  "!!t. v_clos(<|ev,e,ve|>) hasty t ==>  \
  11.343 +\       ? te.te |- fn ev => e ===> t & ve hastyenv te ";
  11.344 +by (dtac hasty_elim_clos_lem 1);
  11.345 +by (Blast_tac 1);
  11.346  qed "hasty_elim_clos";
  11.347  
  11.348  (* ############################################################ *)
  11.349 @@ -650,10 +625,10 @@
  11.350  by (rewtac hasty_env_def);
  11.351  by (asm_full_simp_tac (!simpset delsimps mem_simps
  11.352                                  addsimps [ve_dom_owr, te_dom_owr]) 1);
  11.353 -by (safe_tac (claset_of "HOL"));
  11.354 +by (safe_tac HOL_cs);
  11.355  by (excluded_middle_tac "ev=x" 1);
  11.356  by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
  11.357 -by (Fast_tac 1);
  11.358 +by (Blast_tac 1);
  11.359  by (asm_simp_tac (!simpset addsimps [ve_app_owr1, te_app_owr1]) 1);
  11.360  qed "hasty_env1";
  11.361  
  11.362 @@ -661,38 +636,34 @@
  11.363  (* The Consistency theorem                                      *)
  11.364  (* ############################################################ *)
  11.365  
  11.366 -val prems = goal MT.thy 
  11.367 -  "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
  11.368 -by (cut_facts_tac prems 1);
  11.369 +goal MT.thy 
  11.370 +  "!!t. [| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
  11.371  by (dtac elab_const_elim 1);
  11.372  by (etac hasty_const 1);
  11.373  qed "consistency_const";
  11.374  
  11.375 -val prems = goalw MT.thy [hasty_env_def]
  11.376 -  " [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
  11.377 -\   ve_app ve ev hasty t";
  11.378 -by (cut_facts_tac prems 1);
  11.379 +goalw MT.thy [hasty_env_def]
  11.380 +  "!!t. [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
  11.381 +\       ve_app ve ev hasty t";
  11.382  by (dtac elab_var_elim 1);
  11.383 -by (Fast_tac 1);
  11.384 +by (Blast_tac 1);
  11.385  qed "consistency_var";
  11.386  
  11.387 -val prems = goal MT.thy
  11.388 -  " [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
  11.389 -\   v_clos(<| ev, e, ve |>) hasty t";
  11.390 -by (cut_facts_tac prems 1);
  11.391 +goal MT.thy
  11.392 +  "!!t. [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
  11.393 +\       v_clos(<| ev, e, ve |>) hasty t";
  11.394  by (rtac hasty_clos 1);
  11.395 -by (Fast_tac 1);
  11.396 +by (Blast_tac 1);
  11.397  qed "consistency_fn";
  11.398  
  11.399 -val prems = goalw MT.thy [hasty_env_def,hasty_def]
  11.400 -  " [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
  11.401 +goalw MT.thy [hasty_env_def,hasty_def]
  11.402 +  "!!t. [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
  11.403  \      ve hastyenv te ; \
  11.404  \      te |- fix ev2  ev1  = e ===> t \
  11.405  \   |] ==> \
  11.406  \   v_clos(cl) hasty t";
  11.407 -by (cut_facts_tac prems 1);
  11.408  by (dtac elab_fix_elim 1);
  11.409 -by (safe_tac (claset_of "HOL"));
  11.410 +by (safe_tac HOL_cs);
  11.411  (*Do a single unfolding of cl*)
  11.412  by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
  11.413  by (rtac hasty_rel_clos_coind 1);
  11.414 @@ -700,37 +671,36 @@
  11.415  by (asm_simp_tac (!simpset addsimps [ve_dom_owr, te_dom_owr]) 1);
  11.416  
  11.417  by (asm_simp_tac (!simpset delsimps mem_simps addsimps [ve_dom_owr]) 1);
  11.418 -by (safe_tac (claset_of "HOL"));
  11.419 +by (safe_tac HOL_cs);
  11.420  by (excluded_middle_tac "ev2=ev1a" 1);
  11.421  by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
  11.422 -by (Fast_tac 1);
  11.423 +by (Blast_tac 1);
  11.424  
  11.425  by (asm_simp_tac (!simpset delsimps mem_simps
  11.426                             addsimps [ve_app_owr1, te_app_owr1]) 1);
  11.427  by (hyp_subst_tac 1);
  11.428  by (etac subst 1);
  11.429 -by (Fast_tac 1);
  11.430 +by (Blast_tac 1);
  11.431  qed "consistency_fix";
  11.432  
  11.433 -val prems = goal MT.thy 
  11.434 -  " [| ! t te. ve hastyenv te  --> te |- e1 ===> t --> v_const(c1) hasty t; \
  11.435 +goal MT.thy 
  11.436 +  "!!t. [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
  11.437  \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
  11.438  \      ve hastyenv te ; te |- e1 @ e2 ===> t \
  11.439  \   |] ==> \
  11.440  \   v_const(c_app c1 c2) hasty t";
  11.441 -by (cut_facts_tac prems 1);
  11.442  by (dtac elab_app_elim 1);
  11.443  by (safe_tac (!claset));
  11.444  by (rtac hasty_const 1);
  11.445  by (rtac isof_app 1);
  11.446  by (rtac hasty_elim_const 1);
  11.447 -by (Fast_tac 1);
  11.448 +by (Blast_tac 1);
  11.449  by (rtac hasty_elim_const 1);
  11.450 -by (Fast_tac 1);
  11.451 +by (Blast_tac 1);
  11.452  qed "consistency_app1";
  11.453  
  11.454 -val prems = goal MT.thy 
  11.455 -  " [| ! t te. \
  11.456 +goal MT.thy 
  11.457 +  "!!t.  [| ! t te. \
  11.458  \        ve hastyenv te  --> \
  11.459  \        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
  11.460  \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
  11.461 @@ -740,7 +710,6 @@
  11.462  \      te |- e1 @ e2 ===> t \
  11.463  \   |] ==> \
  11.464  \   v hasty t";
  11.465 -by (cut_facts_tac prems 1);
  11.466  by (dtac elab_app_elim 1);
  11.467  by (safe_tac (!claset));
  11.468  by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
  11.469 @@ -754,10 +723,7 @@
  11.470  by (dtac hasty_elim_clos 1);
  11.471  by (safe_tac (!claset));
  11.472  by (dtac elab_fn_elim 1);
  11.473 -by (safe_tac (!claset));
  11.474 -by (dtac t_fun_inj 1);
  11.475 -by (safe_tac (!claset));
  11.476 -by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (Fast_tac 1));
  11.477 +by (blast_tac (!claset addIs [hasty_env1] addSDs [t_fun_inj]) 1);
  11.478  qed "consistency_app2";
  11.479  
  11.480  val [major] = goal MT.thy 
  11.481 @@ -795,10 +761,7 @@
  11.482  by (cut_facts_tac prems 1);
  11.483  by (rtac hasty_elim_const 1);
  11.484  by (dtac consistency 1);
  11.485 -by (fast_tac (!claset addSIs [basic_consistency_lem]) 1);
  11.486 +by (blast_tac (!claset addSIs [basic_consistency_lem]) 1);
  11.487  qed "basic_consistency";
  11.488  
  11.489 -
  11.490 -Unify.search_bound := orig_search_bound;
  11.491 -
  11.492  writeln"Reached end of file.";
    12.1 --- a/src/HOL/ex/Simult.ML	Fri Apr 11 11:33:51 1997 +0200
    12.2 +++ b/src/HOL/ex/Simult.ML	Fri Apr 11 15:21:36 1997 +0200
    12.3 @@ -29,7 +29,7 @@
    12.4  
    12.5  goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
    12.6  by (rtac lfp_lowerbound 1);
    12.7 -by (fast_tac (!claset addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
    12.8 +by (blast_tac (!claset addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
    12.9                        addSEs [PartE]) 1);
   12.10  qed "TF_sexp";
   12.11  
   12.12 @@ -50,7 +50,7 @@
   12.13  \            |] ==> R(FCONS M N)    \
   12.14  \    |] ==> R(i)";
   12.15  by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
   12.16 -by (fast_tac (!claset addIs (prems@[PartI])
   12.17 +by (blast_tac (!claset addIs (prems@[PartI])
   12.18                         addEs [usumE, uprodE, PartE]) 1);
   12.19  qed "TF_induct";
   12.20  
   12.21 @@ -59,13 +59,9 @@
   12.22   "!!A.  ! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
   12.23  \                   (M: Part (TF A) In1 --> Q(M)) \
   12.24  \  ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
   12.25 -by (Fast_tac 1);
   12.26 +by (Blast_tac 1);
   12.27  qed "TF_induct_lemma";
   12.28  
   12.29 -AddSIs [PartI];
   12.30 -AddSDs [In0_inject, In1_inject];
   12.31 -AddSEs [PartE];
   12.32 -
   12.33  (*Could prove  ~ TCONS M N : Part (TF A) In1  etc. *)
   12.34  
   12.35  (*Induction on TF with separate predicates P, Q*)
   12.36 @@ -93,12 +89,12 @@
   12.37      (Tree_Forest_induct RS conjE) 1);
   12.38  (*Instantiates ?A1 to range(Leaf). *)
   12.39  by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst, 
   12.40 -                             Rep_Forest_inverse RS subst] 
   12.41 -                     addSIs [Rep_Tree,Rep_Forest]) 4);
   12.42 +			      Rep_Forest_inverse RS subst] 
   12.43 +                       addSIs [Rep_Tree,Rep_Forest]) 4);
   12.44  (*Cannot use simplifier: the rewrites work in the wrong direction!*)
   12.45  by (ALLGOALS (fast_tac (!claset addSEs [Abs_Tree_inverse RS subst,
   12.46 -                          Abs_Forest_inverse RS subst] 
   12.47 -                     addSIs prems)));
   12.48 +					Abs_Forest_inverse RS subst] 
   12.49 +                                addSIs prems)));
   12.50  qed "tree_forest_induct";
   12.51  
   12.52  
   12.53 @@ -135,38 +131,38 @@
   12.54  AddIs [TF_I, uprodI, usum_In0I, usum_In1I];
   12.55  AddSEs [Scons_inject];
   12.56  
   12.57 -val prems = goalw Simult.thy TF_Rep_defs
   12.58 -    "[| a: A;  M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
   12.59 -by (fast_tac (!claset addIs prems) 1);
   12.60 +goalw Simult.thy TF_Rep_defs
   12.61 +    "!!A. [| a: A;  M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
   12.62 +by (Blast_tac 1);
   12.63  qed "TCONS_I";
   12.64  
   12.65  (* FNIL is a TF(A) -- this also justifies the type definition*)
   12.66  goalw Simult.thy TF_Rep_defs "FNIL: Part (TF A) In1";
   12.67 -by (Fast_tac 1);
   12.68 +by (Blast_tac 1);
   12.69  qed "FNIL_I";
   12.70  
   12.71 -val prems = goalw Simult.thy TF_Rep_defs
   12.72 -    "[| M: Part (TF A) In0;  N: Part (TF A) In1 |] ==> \
   12.73 -\    FCONS M N : Part (TF A) In1";
   12.74 -by (fast_tac (!claset addIs prems) 1);
   12.75 +goalw Simult.thy TF_Rep_defs
   12.76 +    "!!A. [| M: Part (TF A) In0;  N: Part (TF A) In1 |] ==> \
   12.77 +\         FCONS M N : Part (TF A) In1";
   12.78 +by (Blast_tac 1);
   12.79  qed "FCONS_I";
   12.80  
   12.81  (** Injectiveness of TCONS and FCONS **)
   12.82  
   12.83  goalw Simult.thy TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)";
   12.84 -by (Fast_tac 1);
   12.85 +by (Blast_tac 1);
   12.86  qed "TCONS_TCONS_eq";
   12.87  bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
   12.88  
   12.89  goalw Simult.thy TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)";
   12.90 -by (Fast_tac 1);
   12.91 +by (Blast_tac 1);
   12.92  qed "FCONS_FCONS_eq";
   12.93  bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
   12.94  
   12.95  (** Distinctness of TCONS, FNIL and FCONS **)
   12.96  
   12.97  goalw Simult.thy TF_Rep_defs "TCONS M N ~= FNIL";
   12.98 -by (Fast_tac 1);
   12.99 +by (Blast_tac 1);
  12.100  qed "TCONS_not_FNIL";
  12.101  bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
  12.102  
  12.103 @@ -174,7 +170,7 @@
  12.104  val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
  12.105  
  12.106  goalw Simult.thy TF_Rep_defs "FCONS M N ~= FNIL";
  12.107 -by (Fast_tac 1);
  12.108 +by (Blast_tac 1);
  12.109  qed "FCONS_not_FNIL";
  12.110  bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
  12.111  
  12.112 @@ -182,7 +178,7 @@
  12.113  val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
  12.114  
  12.115  goalw Simult.thy TF_Rep_defs "TCONS M N ~= FCONS K L";
  12.116 -by (Fast_tac 1);
  12.117 +by (Blast_tac 1);
  12.118  qed "TCONS_not_FCONS";
  12.119  bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
  12.120  
  12.121 @@ -206,12 +202,12 @@
  12.122                             Leaf_inject];
  12.123  
  12.124  goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)";
  12.125 -by (Fast_tac 1);
  12.126 +by (Blast_tac 1);
  12.127  qed "Tcons_Tcons_eq";
  12.128  bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
  12.129  
  12.130  goalw Simult.thy [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil";
  12.131 -by (Fast_tac 1);
  12.132 +by (Blast_tac 1);
  12.133  qed "Fcons_not_Fnil";
  12.134  
  12.135  bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
  12.136 @@ -221,7 +217,7 @@
  12.137  (** Injectiveness of Fcons **)
  12.138  
  12.139  goalw Simult.thy [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)";
  12.140 -by (Fast_tac 1);
  12.141 +by (Blast_tac 1);
  12.142  qed "Fcons_Fcons_eq";
  12.143  bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
  12.144  
    13.1 --- a/src/HOL/ex/set.ML	Fri Apr 11 11:33:51 1997 +0200
    13.2 +++ b/src/HOL/ex/set.ML	Fri Apr 11 15:21:36 1997 +0200
    13.3 @@ -43,19 +43,18 @@
    13.4  
    13.5  (*** The Schroder-Berstein Theorem ***)
    13.6  
    13.7 -val prems = goalw Lfp.thy [image_def] "inj(f) ==> inv(f)``(f``X) = X";
    13.8 -by (cut_facts_tac prems 1);
    13.9 +goalw Lfp.thy [image_def] "!!f. inj(f) ==> inv(f)``(f``X) = X";
   13.10  by (rtac equalityI 1);
   13.11  by (fast_tac (!claset addEs [inv_f_f RS ssubst]) 1);
   13.12  by (fast_tac (!claset addEs [inv_f_f RS ssubst]) 1);
   13.13  qed "inv_image_comp";
   13.14  
   13.15  goal Set.thy "!!f. f(a) ~: (f``X) ==> a~:X";
   13.16 -by (Fast_tac 1);
   13.17 +by (Blast_tac 1);
   13.18  qed "contra_imageI";
   13.19  
   13.20  goal Lfp.thy "(a ~: Compl(X)) = (a:X)";
   13.21 -by (Fast_tac 1);
   13.22 +by (Blast_tac 1);
   13.23  qed "not_Compl";
   13.24  
   13.25  (*Lots of backtracking in this proof...*)
   13.26 @@ -69,11 +68,11 @@
   13.27  goalw Lfp.thy [image_def]
   13.28      "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
   13.29  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   13.30 -by (Fast_tac 1);
   13.31 +by (Blast_tac 1);
   13.32  qed "range_if_then_else";
   13.33  
   13.34  goal Lfp.thy "a : X Un Compl(X)";
   13.35 -by (Fast_tac 1);
   13.36 +by (Blast_tac 1);
   13.37  qed "X_Un_Compl";
   13.38  
   13.39  goalw Lfp.thy [surj_def] "surj(f) = (!a. a : range(f))";
    14.1 --- a/src/HOL/simpdata.ML	Fri Apr 11 11:33:51 1997 +0200
    14.2 +++ b/src/HOL/simpdata.ML	Fri Apr 11 15:21:36 1997 +0200
    14.3 @@ -55,7 +55,7 @@
    14.4  
    14.5  local
    14.6  
    14.7 -  fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
    14.8 +  fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
    14.9  
   14.10    val P_imp_P_iff_True = prover "P --> (P = True)" RS mp;
   14.11    val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
   14.12 @@ -118,7 +118,7 @@
   14.13  
   14.14  val imp_cong = impI RSN
   14.15      (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
   14.16 -        (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
   14.17 +        (fn _=> [blast_tac HOL_cs 1]) RS mp RS mp);
   14.18  
   14.19  (*Miniscoping: pushing in existential quantifiers*)
   14.20  val ex_simps = map prover 
   14.21 @@ -153,7 +153,7 @@
   14.22  
   14.23  end;
   14.24  
   14.25 -fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [fast_tac HOL_cs 1]);
   14.26 +fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [blast_tac HOL_cs 1]);
   14.27  
   14.28  prove "conj_commute" "(P&Q) = (Q&P)";
   14.29  prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
   14.30 @@ -196,19 +196,19 @@
   14.31  
   14.32  let val th = prove_goal HOL.thy 
   14.33                  "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
   14.34 -                (fn _=> [fast_tac HOL_cs 1])
   14.35 +                (fn _=> [blast_tac HOL_cs 1])
   14.36  in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   14.37  
   14.38  let val th = prove_goal HOL.thy 
   14.39                  "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
   14.40 -                (fn _=> [fast_tac HOL_cs 1])
   14.41 +                (fn _=> [blast_tac HOL_cs 1])
   14.42  in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   14.43  
   14.44  (* '|' congruence rule: not included by default! *)
   14.45  
   14.46  let val th = prove_goal HOL.thy 
   14.47                  "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
   14.48 -                (fn _=> [fast_tac HOL_cs 1])
   14.49 +                (fn _=> [blast_tac HOL_cs 1])
   14.50  in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   14.51  
   14.52  prove "eq_sym_conv" "(x=y) = (y=x)";
   14.53 @@ -220,10 +220,10 @@
   14.54    (fn [prem] => [rewtac prem, rtac refl 1]);
   14.55  
   14.56  qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
   14.57 - (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
   14.58 + (fn _=>[blast_tac (HOL_cs addIs [select_equality]) 1]);
   14.59  
   14.60  qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y"
   14.61 - (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
   14.62 + (fn _=>[blast_tac (HOL_cs addIs [select_equality]) 1]);
   14.63  
   14.64  qed_goal "if_P" HOL.thy "P ==> (if P then x else y) = x"
   14.65   (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
   14.66 @@ -232,14 +232,14 @@
   14.67   (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);
   14.68  *)
   14.69  qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
   14.70 - (fn _ => [fast_tac (HOL_cs addIs [select_equality]) 1]);
   14.71 + (fn _ => [blast_tac (HOL_cs addIs [select_equality]) 1]);
   14.72  
   14.73  qed_goal "expand_if" HOL.thy
   14.74      "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
   14.75   (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
   14.76           stac if_P 2,
   14.77           stac if_not_P 1,
   14.78 -         REPEAT(fast_tac HOL_cs 1) ]);
   14.79 +         REPEAT(blast_tac HOL_cs 1) ]);
   14.80  
   14.81  qed_goal "if_bool_eq" HOL.thy
   14.82                     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
   14.83 @@ -257,7 +257,7 @@
   14.84  
   14.85  
   14.86  qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   14.87 -  (fn _ => [split_tac [expand_if] 1, fast_tac HOL_cs 1]);
   14.88 +  (fn _ => [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
   14.89  
   14.90  (** 'if' congruence rules: neither included by default! *)
   14.91  
   14.92 @@ -267,7 +267,7 @@
   14.93  \  (if b then x else y) = (if c then u else v)"
   14.94    (fn rew::prems =>
   14.95     [stac rew 1, stac expand_if 1, stac expand_if 1,
   14.96 -    fast_tac (HOL_cs addDs prems) 1]);
   14.97 +    blast_tac (HOL_cs addDs prems) 1]);
   14.98  
   14.99  (*Prevents simplification of x and y: much faster*)
  14.100  qed_goal "if_weak_cong" HOL.thy