src/ZF/WF.ML

--- a/src/ZF/WF.ML	Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/WF.ML	Wed Apr 23 10:54:22 1997 +0200
@@ -25,7 +25,7 @@
 (** Equivalences between wf and wf_on **)
 
 goalw WF.thy [wf_def, wf_on_def] "!!A r. wf(r) ==> wf[A](r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_imp_wf_on";
 
 goalw WF.thy [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)";
@@ -33,7 +33,7 @@
 qed "wf_on_field_imp_wf";
 
 goal WF.thy "wf(r) <-> wf[field(r)](r)";
-by (fast_tac (!claset addSEs [wf_imp_wf_on, wf_on_field_imp_wf]) 1);
+by (blast_tac (!claset addIs [wf_imp_wf_on, wf_on_field_imp_wf]) 1);
 qed "wf_iff_wf_on_field";
 
 goalw WF.thy [wf_on_def, wf_def] "!!A B r. [| wf[A](r);  B<=A |] ==> wf[B](r)";
@@ -52,7 +52,7 @@
 \    ==>  wf[A](r)";
 by (rtac (equals0I RS disjCI RS allI) 1);
 by (res_inst_tac [ ("Z", "Z") ] prem 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Blast_tac);
 qed "wf_onI";
 
 (*If r allows well-founded induction over A then wf[A](r)
@@ -65,7 +65,7 @@
 by (rtac wf_onI 1);
 by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1);
 by (contr_tac 3);
-by (Fast_tac 2);
+by (Blast_tac 2);
 by (Fast_tac 1);
 qed "wf_onI2";
 
@@ -79,9 +79,9 @@
 \    |]  ==>  P(a)";
 by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ]  (major RS allE) 1);
 by (etac disjE 1);
-by (fast_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
 by (asm_full_simp_tac (!simpset addsimps [domainI]) 1);
-by (fast_tac (!claset addSDs [minor]) 1);
+by (blast_tac (!claset addSDs [minor]) 1);
 qed "wf_induct";
 
 (*Perform induction on i, then prove the wf(r) subgoal using prems. *)
@@ -99,11 +99,11 @@
 by (wf_ind_tac "a" [wfr] 1);
 by (rtac impI 1);
 by (eresolve_tac prems 1);
-by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
+by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
 qed "wf_induct2";
 
 goal domrange.thy "!!r A. field(r Int A*A) <= A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "field_Int_square";
 
 val wfr::amem::prems = goalw WF.thy [wf_on_def]
@@ -112,7 +112,7 @@
 \    |]  ==>  P(a)";
 by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1);
 by (REPEAT (ares_tac prems 1));
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_on_induct";
 
 fun wf_on_ind_tac a prems i = 
@@ -135,26 +135,26 @@
 
 goal WF.thy "!!r. wf(r) ==> <a,a> ~: r";
 by (wf_ind_tac "a" [] 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_not_refl";
 
 goal WF.thy "!!r. [| wf(r);  <a,x>:r;  <x,a>:r |] ==> P";
 by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
 by (wf_ind_tac "a" [] 2);
-by (Fast_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 2);
+by (Blast_tac 1);
 qed "wf_asym";
 
 goal WF.thy "!!r. [| wf[A](r); a: A |] ==> <a,a> ~: r";
 by (wf_on_ind_tac "a" [] 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_on_not_refl";
 
 goal WF.thy "!!r. [| wf[A](r);  <a,b>:r;  <b,a>:r;  a:A;  b:A |] ==> P";
 by (subgoal_tac "ALL y:A. <a,y>:r --> <y,a>:r --> P" 1);
 by (wf_on_ind_tac "a" [] 2);
-by (Fast_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 2);
+by (Blast_tac 1);
 qed "wf_on_asym";
 
 (*Needed to prove well_ordI.  Could also reason that wf[A](r) means
@@ -164,8 +164,8 @@
 by (subgoal_tac
     "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P" 1);
 by (wf_on_ind_tac "a" [] 2);
-by (Fast_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 2);
+by (Blast_tac 1);
 qed "wf_on_chain3";
 
 
@@ -178,20 +178,15 @@
 by (rtac wf_onI2 1);
 by (bchain_tac 1);
 by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1);
-by (rtac (impI RS ballI) 1);
-by (etac tranclE 1);
-by (etac (bspec RS mp) 1 THEN assume_tac 1);
-by (Fast_tac 1);
 by (cut_facts_tac [subs] 1);
-(*astar_tac is slightly faster*)
-by (Best_tac 1);
+by (blast_tac (!claset addEs [tranclE]) 1);
 qed "wf_on_trancl";
 
 goal WF.thy "!!r. wf(r) ==> wf(r^+)";
 by (asm_full_simp_tac (!simpset addsimps [wf_iff_wf_on_field]) 1);
 by (rtac (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1);
 by (etac wf_on_trancl 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "wf_trancl";