1.1 --- a/src/ZF/WF.ML	Wed Feb 13 10:44:07 2002 +0100
     1.2 +++ b/src/ZF/WF.ML	Wed Feb 13 10:44:39 2002 +0100
     1.3 @@ -58,8 +58,8 @@
     1.4    Premise is equivalent to 
     1.5    !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B  *)
     1.6  val [prem] = Goal
     1.7 -    "[| !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
     1.8 -\              |] ==> y:B |] \
     1.9 +    "[| !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A |]   \
    1.10 +\              ==> y:B |] \
    1.11  \    ==>  wf[A](r)";
    1.12  by (rtac wf_onI 1);
    1.13  by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1);
    1.14 @@ -122,8 +122,8 @@
    1.15  (*If r allows well-founded induction then wf(r)*)
    1.16  val [subs,indhyp] = Goal
    1.17      "[| field(r)<=A;  \
    1.18 -\       !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
    1.19 -\              |] ==> y:B |] \
    1.20 +\       !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;  y:A|]  \
    1.21 +\              ==> y:B |] \
    1.22  \    ==>  wf(r)";
    1.23  by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1);
    1.24  by (REPEAT (ares_tac [indhyp] 1));
    1.25 @@ -212,36 +212,25 @@
    1.26  by (rtac (rel RS underI RS beta) 1);
    1.27  qed "apply_recfun";
    1.28  
    1.29 -(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
    1.30 -  spec RS mp  instantiates induction hypotheses*)
    1.31 -fun indhyp_tac hyps =
    1.32 -    resolve_tac (TrueI::refl::reflexive_thm::hyps) ORELSE' 
    1.33 -    (cut_facts_tac hyps THEN'
    1.34 -       DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
    1.35 -                        eresolve_tac [underD, transD, spec RS mp]));
    1.36 -
    1.37 -(*** NOTE! some simplifications need a different solver!! ***)
    1.38 -val wf_super_ss = simpset() setSolver (mk_solver "WF" indhyp_tac);
    1.39 -
    1.40  Goalw [is_recfun_def]
    1.41      "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
    1.42  \    <x,a>:r --> <x,b>:r --> f`x=g`x";
    1.43  by (wf_ind_tac "x" [] 1);
    1.44  by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
    1.45 -by (rewtac restrict_def);
    1.46 -by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
    1.47 +by (asm_simp_tac (simpset() addsimps [vimage_singleton_iff, restrict_def]) 1); 
    1.48 +by (subgoal_tac "ALL y. y : r-``{x1} --> f`y = g`y" 1);
    1.49 + by (Asm_simp_tac 1);
    1.50 +by (blast_tac (claset() addDs [transD]) 1); 
    1.51  qed_spec_mp "is_recfun_equal";
    1.52  
    1.53 -val prems as [wfr,transr,recf,recg,_] = goal (the_context ())
    1.54 -    "[| wf(r);  trans(r);       \
    1.55 -\       is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |] ==> \
    1.56 -\    restrict(f, r-``{b}) = g";
    1.57 -by (cut_facts_tac prems 1);
    1.58 +Goal "[| wf(r);  trans(r);       \
    1.59 +\        is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |]  \
    1.60 +\     ==> restrict(f, r-``{b}) = g";
    1.61  by (rtac (consI1 RS restrict_type RS fun_extension) 1);
    1.62  by (etac is_recfun_type 1);
    1.63 -by (ALLGOALS
    1.64 -    (asm_simp_tac (wf_super_ss addsimps
    1.65 -                   [ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
    1.66 +by (asm_full_simp_tac (simpset() addsimps [vimage_singleton_iff]) 1);
    1.67 +by (blast_tac (claset() addDs [transD]
    1.68 +			addIs [is_recfun_equal]) 1);
    1.69  qed "is_recfun_cut";
    1.70  
    1.71  (*** Main Existence Lemma ***)
    1.72 @@ -269,10 +258,14 @@
    1.73  by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
    1.74  by (fold_tac [is_recfun_def]);
    1.75  by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
    1.76 -by (rtac is_recfun_type 1);
    1.77 -by (ALLGOALS
    1.78 -    (asm_simp_tac
    1.79 -     (wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut])));
    1.80 + by (blast_tac (claset() addIs [is_recfun_type]) 1);
    1.81 +by (ftac (spec RS mp) 1 THEN assume_tac 1);
    1.82 +by (subgoal_tac "<xa,a1> : r" 1);
    1.83 +by (dres_inst_tac [("x1","xa")] (spec RS mp) 1 THEN assume_tac 1);
    1.84 +by (asm_full_simp_tac
    1.85 +     (simpset() addsimps [vimage_singleton_iff, underI RS beta, apply_recfun, 
    1.86 +                          is_recfun_cut]) 1);
    1.87 +by (blast_tac (claset() addDs [transD]) 1);
    1.88  qed "unfold_the_recfun";
    1.89  
    1.90  
    1.91 @@ -331,22 +324,9 @@
    1.92  by (asm_simp_tac (simpset() addsimps [vimage_Int_square, cons_subset_iff]) 1);
    1.93  qed "wfrec_on";
    1.94  
    1.95 -(*----------------------------------------------------------------------------
    1.96 - * Minimal-element characterization of well-foundedness
    1.97 - *---------------------------------------------------------------------------*)
    1.98 -
    1.99 -Goalw [wf_def] "wf(r) ==> x:Q --> (EX z:Q. ALL y. <y,z>:r --> y~:Q)";
   1.100 -by (dtac spec 1);
   1.101 +(*Minimal-element characterization of well-foundedness*)
   1.102 +Goalw [wf_def] 
   1.103 +     "wf(r) <-> (ALL Q x. x:Q --> (EX z:Q. ALL y. <y,z>:r --> y~:Q))";
   1.104  by (Blast_tac 1);
   1.105 -val lemma1 = result();
   1.106 -
   1.107 -Goalw [wf_def]
   1.108 -     "(ALL Q x. x:Q --> (EX z:Q. ALL y. <y,z>:r --> y~:Q)) ==> wf(r)";
   1.109 -by (Clarify_tac 1);
   1.110 -by (Blast_tac 1);
   1.111 -val lemma2 = result();
   1.112 -
   1.113 -Goal "wf(r) <-> (ALL Q x. x:Q --> (EX z:Q. ALL y. <y,z>:r --> y~:Q))";
   1.114 -by (blast_tac (claset() addSIs [lemma1, lemma2]) 1);
   1.115  qed "wf_eq_minimal";
   1.116