src/ZF/WF.ML

--- a/src/ZF/WF.ML	Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/WF.ML	Fri Jan 03 15:01:55 1997 +0100
@@ -25,23 +25,23 @@
 (** Equivalences between wf and wf_on **)
 
 goalw WF.thy [wf_def, wf_on_def] "!!A r. wf(r) ==> wf[A](r)";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
 qed "wf_imp_wf_on";
 
 goalw WF.thy [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
 qed "wf_on_field_imp_wf";
 
 goal WF.thy "wf(r) <-> wf[field(r)](r)";
-by (fast_tac (ZF_cs addSEs [wf_imp_wf_on, wf_on_field_imp_wf]) 1);
+by (fast_tac (!claset addSEs [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)";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
 qed "wf_on_subset_A";
 
 goalw WF.thy [wf_on_def, wf_def] "!!A r s. [| wf[A](r);  s<=r |] ==> wf[A](s)";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
 qed "wf_on_subset_r";
 
 (** Introduction rules for wf_on **)
@@ -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 ZF_cs));
+by (ALLGOALS (Fast_tac));
 qed "wf_onI";
 
 (*If r allows well-founded induction over A then wf[A](r)
@@ -65,8 +65,8 @@
 by (rtac wf_onI 1);
 by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1);
 by (contr_tac 3);
-by (fast_tac ZF_cs 2);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 2);
+by (Fast_tac 1);
 qed "wf_onI2";
 
 
@@ -79,11 +79,11 @@
 \    |]  ==>  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 (ZF_cs addEs [equalityE]) 1);
-by (asm_full_simp_tac (ZF_ss addsimps [domainI]) 1);
+by (fast_tac (!claset addEs [equalityE]) 1);
+by (asm_full_simp_tac (!simpset addsimps [domainI]) 1);
 by (etac bexE 1);
 by (dtac minor 1);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
 qed "wf_induct";
 
 (*Perform induction on i, then prove the wf(r) subgoal using prems. *)
@@ -101,11 +101,11 @@
 by (wf_ind_tac "a" [wfr] 1);
 by (rtac impI 1);
 by (eresolve_tac prems 1);
-by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1);
+by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
 qed "wf_induct2";
 
-goal ZF.thy "!!r A. field(r Int A*A) <= A";
-by (fast_tac ZF_cs 1);
+goal domrange.thy "!!r A. field(r Int A*A) <= A";
+by (Fast_tac 1);
 qed "field_Int_square";
 
 val wfr::amem::prems = goalw WF.thy [wf_on_def]
@@ -114,7 +114,7 @@
 \    |]  ==>  P(a)";
 by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1);
 by (REPEAT (ares_tac prems 1));
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
 qed "wf_on_induct";
 
 fun wf_on_ind_tac a prems i = 
@@ -137,26 +137,26 @@
 
 goal WF.thy "!!r. wf(r) ==> <a,a> ~: r";
 by (wf_ind_tac "a" [] 1);
-by (fast_tac ZF_cs 1);
+by (Fast_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 ZF_cs 2);
-by (fast_tac FOL_cs 1);
+by (Fast_tac 2);
+by (Fast_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 ZF_cs 1);
+by (Fast_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 ZF_cs 2);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 2);
+by (Fast_tac 1);
 qed "wf_on_asym";
 
 (*Needed to prove well_ordI.  Could also reason that wf[A](r) means
@@ -166,8 +166,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 ZF_cs 2);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 2);
+by (Fast_tac 1);
 qed "wf_on_chain3";
 
 
@@ -183,17 +183,17 @@
 by (rtac (impI RS ballI) 1);
 by (etac tranclE 1);
 by (etac (bspec RS mp) 1 THEN assume_tac 1);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
 by (cut_facts_tac [subs] 1);
 (*astar_tac is slightly faster*)
-by (best_tac ZF_cs 1);
+by (Best_tac 1);
 qed "wf_on_trancl";
 
 goal WF.thy "!!r. wf(r) ==> wf(r^+)";
-by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1);
+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 ZF_cs 1);
+by (Fast_tac 1);
 qed "wf_trancl";
 
 
@@ -227,7 +227,7 @@
                         eresolve_tac [underD, transD, spec RS mp]));
 
 (*** NOTE! some simplifications need a different solver!! ***)
-val wf_super_ss = ZF_ss setsolver indhyp_tac;
+val wf_super_ss = !simpset setsolver indhyp_tac;
 
 val prems = goalw WF.thy [is_recfun_def]
     "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
@@ -302,7 +302,7 @@
 \         wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
 by (stac (rewrite_rule [is_recfun_def] unfold_the_recfun) 1);
 by (ALLGOALS (asm_simp_tac
-        (ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
+        (!simpset addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
 qed "wftrec";
 
 (** Removal of the premise trans(r) **)
@@ -340,6 +340,6 @@
  "!!A r. [| wf[A](r);  a: A |] ==> \
 \        wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))";
 by (etac (wfrec RS trans) 1);
-by (asm_simp_tac (ZF_ss addsimps [vimage_Int_square, cons_subset_iff]) 1);
+by (asm_simp_tac (!simpset addsimps [vimage_Int_square, cons_subset_iff]) 1);
 qed "wfrec_on";