src/ZF/wf.ML
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/wf.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,262 @@
     1.4 +(*  Title: 	ZF/wf.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Tobias Nipkow and Lawrence C Paulson
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +For wf.thy.  Well-founded Recursion
    1.10 +
    1.11 +Derived first for transitive relations, and finally for arbitrary WF relations
    1.12 +via wf_trancl and trans_trancl.
    1.13 +
    1.14 +It is difficult to derive this general case directly, using r^+ instead of
    1.15 +r.  In is_recfun, the two occurrences of the relation must have the same
    1.16 +form.  Inserting r^+ in the_recfun or wftrec yields a recursion rule with
    1.17 +r^+ -`` {a} instead of r-``{a}.  This recursion rule is stronger in
    1.18 +principle, but harder to use, especially to prove wfrec_eclose_eq in
    1.19 +epsilon.ML.  Expanding out the definition of wftrec in wfrec would yield
    1.20 +a mess.
    1.21 +*)
    1.22 +
    1.23 +open WF;
    1.24 +
    1.25 +val [H_cong] = mk_typed_congs WF.thy[("H","[i,i]=>i")];
    1.26 +
    1.27 +val wf_ss = ZF_ss addcongs [H_cong];
    1.28 +
    1.29 +
    1.30 +(*** Well-founded relations ***)
    1.31 +
    1.32 +(*Are these two theorems at all useful??*)
    1.33 +
    1.34 +(*If every subset of field(r) possesses an r-minimal element then wf(r).
    1.35 +  Seems impossible to prove this for domain(r) or range(r) instead...
    1.36 +  Consider in particular finite wf relations!*)
    1.37 +val [prem1,prem2] = goalw WF.thy [wf_def]
    1.38 +    "[| field(r)<=A;  \
    1.39 +\       !!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \
    1.40 +\    ==>  wf(r)";
    1.41 +by (rtac (equals0I RS disjCI RS allI) 1);
    1.42 +by (rtac prem2 1);
    1.43 +by (res_inst_tac [ ("B1", "Z") ] (prem1 RS (Int_lower1 RS subset_trans)) 1);
    1.44 +by (fast_tac ZF_cs 1);
    1.45 +by (fast_tac ZF_cs 1);
    1.46 +val wfI = result();
    1.47 +
    1.48 +(*If r allows well-founded induction then wf(r)*)
    1.49 +val [prem1,prem2] = goal WF.thy
    1.50 +    "[| field(r)<=A;  \
    1.51 +\       !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B |]  \
    1.52 +\    ==>  wf(r)";
    1.53 +by (rtac (prem1 RS wfI) 1);
    1.54 +by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);
    1.55 +by (fast_tac ZF_cs 3);
    1.56 +by (fast_tac ZF_cs 2);
    1.57 +by (fast_tac ZF_cs 1);
    1.58 +val wfI2 = result();
    1.59 +
    1.60 +
    1.61 +(** Well-founded Induction **)
    1.62 +
    1.63 +(*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*)
    1.64 +val major::prems = goalw WF.thy [wf_def]
    1.65 +    "[| wf(r);          \
    1.66 +\       !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) \
    1.67 +\    |]  ==>  P(a)";
    1.68 +by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ]  (major RS allE) 1);
    1.69 +by (etac disjE 1);
    1.70 +by (rtac classical 1);
    1.71 +by (etac equals0D 1);
    1.72 +by (etac (singletonI RS UnI2 RS CollectI) 1);
    1.73 +by (etac bexE 1);
    1.74 +by (etac CollectE 1);
    1.75 +by (etac swap 1);
    1.76 +by (resolve_tac prems 1);
    1.77 +by (fast_tac ZF_cs 1);
    1.78 +val wf_induct = result();
    1.79 +
    1.80 +(*Perform induction on i, then prove the wf(r) subgoal using prems. *)
    1.81 +fun wf_ind_tac a prems i = 
    1.82 +    EVERY [res_inst_tac [("a",a)] wf_induct i,
    1.83 +	   rename_last_tac a ["1"] (i+1),
    1.84 +	   ares_tac prems i];
    1.85 +
    1.86 +(*The form of this rule is designed to match wfI2*)
    1.87 +val wfr::amem::prems = goal WF.thy
    1.88 +    "[| wf(r);  a:A;  field(r)<=A;  \
    1.89 +\       !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) \
    1.90 +\    |]  ==>  P(a)";
    1.91 +by (rtac (amem RS rev_mp) 1);
    1.92 +by (wf_ind_tac "a" [wfr] 1);
    1.93 +by (rtac impI 1);
    1.94 +by (eresolve_tac prems 1);
    1.95 +by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1);
    1.96 +val wf_induct2 = result();
    1.97 +
    1.98 +val prems = goal WF.thy "[| wf(r);  <a,x>:r;  <x,a>:r |] ==> False";
    1.99 +by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> False" 1);
   1.100 +by (wf_ind_tac "a" prems 2);
   1.101 +by (fast_tac ZF_cs 2);
   1.102 +by (fast_tac (FOL_cs addIs prems) 1);
   1.103 +val wf_anti_sym = result();
   1.104 +
   1.105 +(*transitive closure of a WF relation is WF!*)
   1.106 +val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
   1.107 +by (rtac (trancl_type RS field_rel_subset RS wfI2) 1);
   1.108 +by (rtac subsetI 1);
   1.109 +(*must retain the universal formula for later use!*)
   1.110 +by (rtac (bspec RS mp) 1 THEN assume_tac 1 THEN assume_tac 1);
   1.111 +by (eres_inst_tac [("a","x")] (prem RS wf_induct2) 1);
   1.112 +by (rtac subset_refl 1);
   1.113 +by (rtac (impI RS allI) 1);
   1.114 +by (etac tranclE 1);
   1.115 +by (etac (bspec RS mp) 1);
   1.116 +by (etac fieldI1 1);
   1.117 +by (fast_tac ZF_cs 1);
   1.118 +by (fast_tac ZF_cs 1);
   1.119 +val wf_trancl = result();
   1.120 +
   1.121 +(** r-``{a} is the set of everything under a in r **)
   1.122 +
   1.123 +val underI = standard (vimage_singleton_iff RS iffD2);
   1.124 +val underD = standard (vimage_singleton_iff RS iffD1);
   1.125 +
   1.126 +(** is_recfun **)
   1.127 +
   1.128 +val [major] = goalw WF.thy [is_recfun_def]
   1.129 +    "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
   1.130 +by (rtac (major RS ssubst) 1);
   1.131 +by (rtac (lamI RS rangeI RS lam_type) 1);
   1.132 +by (assume_tac 1);
   1.133 +val is_recfun_type = result();
   1.134 +
   1.135 +val [isrec,rel] = goalw WF.thy [is_recfun_def]
   1.136 +    "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))";
   1.137 +by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (isrec RS ssubst) 1);
   1.138 +by (rtac (rel RS underI RS beta) 1);
   1.139 +val apply_recfun = result();
   1.140 +
   1.141 +(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
   1.142 +  spec RS mp  instantiates induction hypotheses*)
   1.143 +fun indhyp_tac hyps =
   1.144 +    ares_tac (TrueI::hyps) ORELSE' 
   1.145 +    (cut_facts_tac hyps THEN'
   1.146 +       DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
   1.147 +		        eresolve_tac [underD, transD, spec RS mp]));
   1.148 +
   1.149 +(*** NOTE! some simplifications need a different auto_tac!! ***)
   1.150 +val wf_super_ss = wf_ss setauto indhyp_tac;
   1.151 +
   1.152 +val prems = goalw WF.thy [is_recfun_def]
   1.153 +    "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
   1.154 +\    <x,a>:r --> <x,b>:r --> f`x=g`x";
   1.155 +by (cut_facts_tac prems 1);
   1.156 +by (wf_ind_tac "x" prems 1);
   1.157 +by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
   1.158 +by (rewtac restrict_def);
   1.159 +by (ASM_SIMP_TAC (wf_super_ss addrews [vimage_singleton_iff]) 1);
   1.160 +val is_recfun_equal_lemma = result();
   1.161 +val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
   1.162 +
   1.163 +val prems as [wfr,transr,recf,recg,_] = goal WF.thy
   1.164 +    "[| wf(r);  trans(r);       \
   1.165 +\       is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |] ==> \
   1.166 +\    restrict(f, r-``{b}) = g";
   1.167 +by (cut_facts_tac prems 1);
   1.168 +by (rtac (consI1 RS restrict_type RS fun_extension) 1);
   1.169 +by (etac is_recfun_type 1);
   1.170 +by (ALLGOALS
   1.171 +    (ASM_SIMP_TAC (wf_super_ss addrews
   1.172 +		   [ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
   1.173 +val is_recfun_cut = result();
   1.174 +
   1.175 +(*** Main Existence Lemma ***)
   1.176 +
   1.177 +val prems = goal WF.thy
   1.178 +    "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g";
   1.179 +by (cut_facts_tac prems 1);
   1.180 +by (rtac fun_extension 1);
   1.181 +by (REPEAT (ares_tac [is_recfun_equal] 1
   1.182 +     ORELSE eresolve_tac [is_recfun_type,underD] 1));
   1.183 +val is_recfun_functional = result();
   1.184 +
   1.185 +(*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
   1.186 +val prems = goalw WF.thy [the_recfun_def]
   1.187 +    "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]  \
   1.188 +\    ==> is_recfun(r, a, H, the_recfun(r,a,H))";
   1.189 +by (rtac (ex1I RS theI) 1);
   1.190 +by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1));
   1.191 +val is_the_recfun = result();
   1.192 +
   1.193 +val prems = goal WF.thy
   1.194 +    "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))";
   1.195 +by (cut_facts_tac prems 1);
   1.196 +by (wf_ind_tac "a" prems 1);
   1.197 +by (res_inst_tac [("f", "lam y: r-``{a1}. wftrec(r,y,H)")] is_the_recfun 1);
   1.198 +by (REPEAT (assume_tac 2));
   1.199 +by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
   1.200 +(*Applying the substitution: must keep the quantified assumption!!*)
   1.201 +by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong, H_cong] 1));
   1.202 +by (fold_tac [is_recfun_def]);
   1.203 +by (rtac (consI1 RS restrict_type RSN (2,fun_extension)) 1);
   1.204 +by (rtac is_recfun_type 1);
   1.205 +by (ALLGOALS
   1.206 +    (ASM_SIMP_TAC
   1.207 +     (wf_super_ss addrews [underI RS beta, apply_recfun, is_recfun_cut])));
   1.208 +val unfold_the_recfun = result();
   1.209 +
   1.210 +
   1.211 +(*** Unfolding wftrec ***)
   1.212 +
   1.213 +val prems = goal WF.thy
   1.214 +    "[| wf(r);  trans(r);  <b,a>:r |] ==> \
   1.215 +\    restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)";
   1.216 +by (REPEAT (ares_tac (prems @ [is_recfun_cut, unfold_the_recfun]) 1));
   1.217 +val the_recfun_cut = result();
   1.218 +
   1.219 +(*NOT SUITABLE FOR REWRITING since it is recursive!*)
   1.220 +val prems = goalw WF.thy [wftrec_def]
   1.221 +    "[| wf(r);  trans(r) |] ==> \
   1.222 +\    wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
   1.223 +by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
   1.224 +by (ALLGOALS (ASM_SIMP_TAC
   1.225 +	      (wf_ss addrews (prems@[vimage_singleton_iff RS iff_sym, 
   1.226 +				     the_recfun_cut]))));
   1.227 +val wftrec = result();
   1.228 +
   1.229 +(** Removal of the premise trans(r) **)
   1.230 +
   1.231 +(*NOT SUITABLE FOR REWRITING since it is recursive!*)
   1.232 +val [wfr] = goalw WF.thy [wfrec_def]
   1.233 +    "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
   1.234 +by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
   1.235 +by (rtac trans_trancl 1);
   1.236 +by (rtac (refl RS H_cong) 1);
   1.237 +by (rtac (vimage_pair_mono RS restrict_lam_eq) 1);
   1.238 +by (etac r_into_trancl 1);
   1.239 +by (rtac subset_refl 1);
   1.240 +val wfrec = result();
   1.241 +
   1.242 +(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   1.243 +val rew::prems = goal WF.thy
   1.244 +    "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==> \
   1.245 +\    h(a) = H(a, lam x: r-``{a}. h(x))";
   1.246 +by (rewtac rew);
   1.247 +by (REPEAT (resolve_tac (prems@[wfrec]) 1));
   1.248 +val def_wfrec = result();
   1.249 +
   1.250 +val prems = goal WF.thy
   1.251 +    "[| wf(r);  a:A;  field(r)<=A;  \
   1.252 +\       !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)   \
   1.253 +\    |] ==> wfrec(r,a,H) : B(a)";
   1.254 +by (res_inst_tac [("a","a")] wf_induct2 1);
   1.255 +by (rtac (wfrec RS ssubst) 4);
   1.256 +by (REPEAT (ares_tac (prems@[lam_type]) 1
   1.257 +     ORELSE eresolve_tac [spec RS mp, underD] 1));
   1.258 +val wfrec_type = result();
   1.259 +
   1.260 +val prems = goalw WF.thy [wfrec_def,wftrec_def,the_recfun_def,is_recfun_def]
   1.261 +    "[| r=r';  !!x u. H(x,u)=H'(x,u);  a=a' |] \
   1.262 +\    ==> wfrec(r,a,H)=wfrec(r',a',H')";
   1.263 +by (EVERY1 (map rtac (prems RL [subst])));
   1.264 +by (SIMP_TAC (wf_ss addrews (prems RL [sym])) 1);
   1.265 +val wfrec_cong = result();