src/ZF/wf.ML
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
     1.1 --- a/src/ZF/wf.ML	Fri Sep 17 12:53:53 1993 +0200
     1.2 +++ b/src/ZF/wf.ML	Fri Sep 17 16:16:38 1993 +0200
     1.3 @@ -19,10 +19,6 @@
     1.4  
     1.5  open WF;
     1.6  
     1.7 -val [H_cong] = mk_typed_congs WF.thy[("H","[i,i]=>i")];
     1.8 -
     1.9 -val wf_ss = ZF_ss addcongs [H_cong];
    1.10 -
    1.11  
    1.12  (*** Well-founded relations ***)
    1.13  
    1.14 @@ -138,13 +134,13 @@
    1.15  (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
    1.16    spec RS mp  instantiates induction hypotheses*)
    1.17  fun indhyp_tac hyps =
    1.18 -    ares_tac (TrueI::hyps) ORELSE' 
    1.19 +    resolve_tac (TrueI::refl::hyps) ORELSE' 
    1.20      (cut_facts_tac hyps THEN'
    1.21         DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
    1.22  		        eresolve_tac [underD, transD, spec RS mp]));
    1.23  
    1.24 -(*** NOTE! some simplifications need a different auto_tac!! ***)
    1.25 -val wf_super_ss = wf_ss setauto indhyp_tac;
    1.26 +(*** NOTE! some simplifications need a different solver!! ***)
    1.27 +val wf_super_ss = ZF_ss setsolver indhyp_tac;
    1.28  
    1.29  val prems = goalw WF.thy [is_recfun_def]
    1.30      "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
    1.31 @@ -153,7 +149,7 @@
    1.32  by (wf_ind_tac "x" prems 1);
    1.33  by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
    1.34  by (rewtac restrict_def);
    1.35 -by (ASM_SIMP_TAC (wf_super_ss addrews [vimage_singleton_iff]) 1);
    1.36 +by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
    1.37  val is_recfun_equal_lemma = result();
    1.38  val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
    1.39  
    1.40 @@ -165,7 +161,7 @@
    1.41  by (rtac (consI1 RS restrict_type RS fun_extension) 1);
    1.42  by (etac is_recfun_type 1);
    1.43  by (ALLGOALS
    1.44 -    (ASM_SIMP_TAC (wf_super_ss addrews
    1.45 +    (asm_simp_tac (wf_super_ss addsimps
    1.46  		   [ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
    1.47  val is_recfun_cut = result();
    1.48  
    1.49 @@ -195,13 +191,13 @@
    1.50  by (REPEAT (assume_tac 2));
    1.51  by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
    1.52  (*Applying the substitution: must keep the quantified assumption!!*)
    1.53 -by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong, H_cong] 1));
    1.54 +by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
    1.55  by (fold_tac [is_recfun_def]);
    1.56 -by (rtac (consI1 RS restrict_type RSN (2,fun_extension)) 1);
    1.57 +by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
    1.58  by (rtac is_recfun_type 1);
    1.59  by (ALLGOALS
    1.60 -    (ASM_SIMP_TAC
    1.61 -     (wf_super_ss addrews [underI RS beta, apply_recfun, is_recfun_cut])));
    1.62 +    (asm_simp_tac
    1.63 +     (wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut])));
    1.64  val unfold_the_recfun = result();
    1.65  
    1.66  
    1.67 @@ -214,13 +210,12 @@
    1.68  val the_recfun_cut = result();
    1.69  
    1.70  (*NOT SUITABLE FOR REWRITING since it is recursive!*)
    1.71 -val prems = goalw WF.thy [wftrec_def]
    1.72 -    "[| wf(r);  trans(r) |] ==> \
    1.73 -\    wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
    1.74 +goalw WF.thy [wftrec_def]
    1.75 +    "!!r. [| wf(r);  trans(r) |] ==> \
    1.76 +\         wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
    1.77  by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
    1.78 -by (ALLGOALS (ASM_SIMP_TAC
    1.79 -	      (wf_ss addrews (prems@[vimage_singleton_iff RS iff_sym, 
    1.80 -				     the_recfun_cut]))));
    1.81 +by (ALLGOALS (asm_simp_tac
    1.82 +	(ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
    1.83  val wftrec = result();
    1.84  
    1.85  (** Removal of the premise trans(r) **)
    1.86 @@ -230,8 +225,7 @@
    1.87      "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
    1.88  by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
    1.89  by (rtac trans_trancl 1);
    1.90 -by (rtac (refl RS H_cong) 1);
    1.91 -by (rtac (vimage_pair_mono RS restrict_lam_eq) 1);
    1.92 +by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
    1.93  by (etac r_into_trancl 1);
    1.94  by (rtac subset_refl 1);
    1.95  val wfrec = result();
    1.96 @@ -253,10 +247,3 @@
    1.97  by (REPEAT (ares_tac (prems@[lam_type]) 1
    1.98       ORELSE eresolve_tac [spec RS mp, underD] 1));
    1.99  val wfrec_type = result();
   1.100 -
   1.101 -val prems = goalw WF.thy [wfrec_def,wftrec_def,the_recfun_def,is_recfun_def]
   1.102 -    "[| r=r';  !!x u. H(x,u)=H'(x,u);  a=a' |] \
   1.103 -\    ==> wfrec(r,a,H)=wfrec(r',a',H')";
   1.104 -by (EVERY1 (map rtac (prems RL [subst])));
   1.105 -by (SIMP_TAC (wf_ss addrews (prems RL [sym])) 1);
   1.106 -val wfrec_cong = result();