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.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();
```