src/ZF/WF.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	ZF/wf.ML
     2     ID:         $Id$
     3     Author: 	Tobias Nipkow and Lawrence C Paulson
     4     Copyright   1992  University of Cambridge
     5 
     6 For wf.thy.  Well-founded Recursion
     7 
     8 Derived first for transitive relations, and finally for arbitrary WF relations
     9 via wf_trancl and trans_trancl.
    10 
    11 It is difficult to derive this general case directly, using r^+ instead of
    12 r.  In is_recfun, the two occurrences of the relation must have the same
    13 form.  Inserting r^+ in the_recfun or wftrec yields a recursion rule with
    14 r^+ -`` {a} instead of r-``{a}.  This recursion rule is stronger in
    15 principle, but harder to use, especially to prove wfrec_eclose_eq in
    16 epsilon.ML.  Expanding out the definition of wftrec in wfrec would yield
    17 a mess.
    18 *)
    19 
    20 open WF;
    21 
    22 val [H_cong] = mk_typed_congs WF.thy[("H","[i,i]=>i")];
    23 
    24 val wf_ss = ZF_ss addcongs [H_cong];
    25 
    26 
    27 (*** Well-founded relations ***)
    28 
    29 (*Are these two theorems at all useful??*)
    30 
    31 (*If every subset of field(r) possesses an r-minimal element then wf(r).
    32   Seems impossible to prove this for domain(r) or range(r) instead...
    33   Consider in particular finite wf relations!*)
    34 val [prem1,prem2] = goalw WF.thy [wf_def]
    35     "[| field(r)<=A;  \
    36 \       !!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \
    37 \    ==>  wf(r)";
    38 by (rtac (equals0I RS disjCI RS allI) 1);
    39 by (rtac prem2 1);
    40 by (res_inst_tac [ ("B1", "Z") ] (prem1 RS (Int_lower1 RS subset_trans)) 1);
    41 by (fast_tac ZF_cs 1);
    42 by (fast_tac ZF_cs 1);
    43 val wfI = result();
    44 
    45 (*If r allows well-founded induction then wf(r)*)
    46 val [prem1,prem2] = goal WF.thy
    47     "[| field(r)<=A;  \
    48 \       !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B |]  \
    49 \    ==>  wf(r)";
    50 by (rtac (prem1 RS wfI) 1);
    51 by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);
    52 by (fast_tac ZF_cs 3);
    53 by (fast_tac ZF_cs 2);
    54 by (fast_tac ZF_cs 1);
    55 val wfI2 = result();
    56 
    57 
    58 (** Well-founded Induction **)
    59 
    60 (*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*)
    61 val major::prems = goalw WF.thy [wf_def]
    62     "[| wf(r);          \
    63 \       !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) \
    64 \    |]  ==>  P(a)";
    65 by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ]  (major RS allE) 1);
    66 by (etac disjE 1);
    67 by (rtac classical 1);
    68 by (etac equals0D 1);
    69 by (etac (singletonI RS UnI2 RS CollectI) 1);
    70 by (etac bexE 1);
    71 by (etac CollectE 1);
    72 by (etac swap 1);
    73 by (resolve_tac prems 1);
    74 by (fast_tac ZF_cs 1);
    75 val wf_induct = result();
    76 
    77 (*Perform induction on i, then prove the wf(r) subgoal using prems. *)
    78 fun wf_ind_tac a prems i = 
    79     EVERY [res_inst_tac [("a",a)] wf_induct i,
    80 	   rename_last_tac a ["1"] (i+1),
    81 	   ares_tac prems i];
    82 
    83 (*The form of this rule is designed to match wfI2*)
    84 val wfr::amem::prems = goal WF.thy
    85     "[| wf(r);  a:A;  field(r)<=A;  \
    86 \       !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) \
    87 \    |]  ==>  P(a)";
    88 by (rtac (amem RS rev_mp) 1);
    89 by (wf_ind_tac "a" [wfr] 1);
    90 by (rtac impI 1);
    91 by (eresolve_tac prems 1);
    92 by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1);
    93 val wf_induct2 = result();
    94 
    95 val prems = goal WF.thy "[| wf(r);  <a,x>:r;  <x,a>:r |] ==> False";
    96 by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> False" 1);
    97 by (wf_ind_tac "a" prems 2);
    98 by (fast_tac ZF_cs 2);
    99 by (fast_tac (FOL_cs addIs prems) 1);
   100 val wf_anti_sym = result();
   101 
   102 (*transitive closure of a WF relation is WF!*)
   103 val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
   104 by (rtac (trancl_type RS field_rel_subset RS wfI2) 1);
   105 by (rtac subsetI 1);
   106 (*must retain the universal formula for later use!*)
   107 by (rtac (bspec RS mp) 1 THEN assume_tac 1 THEN assume_tac 1);
   108 by (eres_inst_tac [("a","x")] (prem RS wf_induct2) 1);
   109 by (rtac subset_refl 1);
   110 by (rtac (impI RS allI) 1);
   111 by (etac tranclE 1);
   112 by (etac (bspec RS mp) 1);
   113 by (etac fieldI1 1);
   114 by (fast_tac ZF_cs 1);
   115 by (fast_tac ZF_cs 1);
   116 val wf_trancl = result();
   117 
   118 (** r-``{a} is the set of everything under a in r **)
   119 
   120 val underI = standard (vimage_singleton_iff RS iffD2);
   121 val underD = standard (vimage_singleton_iff RS iffD1);
   122 
   123 (** is_recfun **)
   124 
   125 val [major] = goalw WF.thy [is_recfun_def]
   126     "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
   127 by (rtac (major RS ssubst) 1);
   128 by (rtac (lamI RS rangeI RS lam_type) 1);
   129 by (assume_tac 1);
   130 val is_recfun_type = result();
   131 
   132 val [isrec,rel] = goalw WF.thy [is_recfun_def]
   133     "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))";
   134 by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (isrec RS ssubst) 1);
   135 by (rtac (rel RS underI RS beta) 1);
   136 val apply_recfun = result();
   137 
   138 (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
   139   spec RS mp  instantiates induction hypotheses*)
   140 fun indhyp_tac hyps =
   141     ares_tac (TrueI::hyps) ORELSE' 
   142     (cut_facts_tac hyps THEN'
   143        DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
   144 		        eresolve_tac [underD, transD, spec RS mp]));
   145 
   146 (*** NOTE! some simplifications need a different auto_tac!! ***)
   147 val wf_super_ss = wf_ss setauto indhyp_tac;
   148 
   149 val prems = goalw WF.thy [is_recfun_def]
   150     "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
   151 \    <x,a>:r --> <x,b>:r --> f`x=g`x";
   152 by (cut_facts_tac prems 1);
   153 by (wf_ind_tac "x" prems 1);
   154 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
   155 by (rewtac restrict_def);
   156 by (ASM_SIMP_TAC (wf_super_ss addrews [vimage_singleton_iff]) 1);
   157 val is_recfun_equal_lemma = result();
   158 val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
   159 
   160 val prems as [wfr,transr,recf,recg,_] = goal WF.thy
   161     "[| wf(r);  trans(r);       \
   162 \       is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |] ==> \
   163 \    restrict(f, r-``{b}) = g";
   164 by (cut_facts_tac prems 1);
   165 by (rtac (consI1 RS restrict_type RS fun_extension) 1);
   166 by (etac is_recfun_type 1);
   167 by (ALLGOALS
   168     (ASM_SIMP_TAC (wf_super_ss addrews
   169 		   [ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
   170 val is_recfun_cut = result();
   171 
   172 (*** Main Existence Lemma ***)
   173 
   174 val prems = goal WF.thy
   175     "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g";
   176 by (cut_facts_tac prems 1);
   177 by (rtac fun_extension 1);
   178 by (REPEAT (ares_tac [is_recfun_equal] 1
   179      ORELSE eresolve_tac [is_recfun_type,underD] 1));
   180 val is_recfun_functional = result();
   181 
   182 (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
   183 val prems = goalw WF.thy [the_recfun_def]
   184     "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]  \
   185 \    ==> is_recfun(r, a, H, the_recfun(r,a,H))";
   186 by (rtac (ex1I RS theI) 1);
   187 by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1));
   188 val is_the_recfun = result();
   189 
   190 val prems = goal WF.thy
   191     "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))";
   192 by (cut_facts_tac prems 1);
   193 by (wf_ind_tac "a" prems 1);
   194 by (res_inst_tac [("f", "lam y: r-``{a1}. wftrec(r,y,H)")] is_the_recfun 1);
   195 by (REPEAT (assume_tac 2));
   196 by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
   197 (*Applying the substitution: must keep the quantified assumption!!*)
   198 by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong, H_cong] 1));
   199 by (fold_tac [is_recfun_def]);
   200 by (rtac (consI1 RS restrict_type RSN (2,fun_extension)) 1);
   201 by (rtac is_recfun_type 1);
   202 by (ALLGOALS
   203     (ASM_SIMP_TAC
   204      (wf_super_ss addrews [underI RS beta, apply_recfun, is_recfun_cut])));
   205 val unfold_the_recfun = result();
   206 
   207 
   208 (*** Unfolding wftrec ***)
   209 
   210 val prems = goal WF.thy
   211     "[| wf(r);  trans(r);  <b,a>:r |] ==> \
   212 \    restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)";
   213 by (REPEAT (ares_tac (prems @ [is_recfun_cut, unfold_the_recfun]) 1));
   214 val the_recfun_cut = result();
   215 
   216 (*NOT SUITABLE FOR REWRITING since it is recursive!*)
   217 val prems = goalw WF.thy [wftrec_def]
   218     "[| wf(r);  trans(r) |] ==> \
   219 \    wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
   220 by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
   221 by (ALLGOALS (ASM_SIMP_TAC
   222 	      (wf_ss addrews (prems@[vimage_singleton_iff RS iff_sym, 
   223 				     the_recfun_cut]))));
   224 val wftrec = result();
   225 
   226 (** Removal of the premise trans(r) **)
   227 
   228 (*NOT SUITABLE FOR REWRITING since it is recursive!*)
   229 val [wfr] = goalw WF.thy [wfrec_def]
   230     "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
   231 by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
   232 by (rtac trans_trancl 1);
   233 by (rtac (refl RS H_cong) 1);
   234 by (rtac (vimage_pair_mono RS restrict_lam_eq) 1);
   235 by (etac r_into_trancl 1);
   236 by (rtac subset_refl 1);
   237 val wfrec = result();
   238 
   239 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   240 val rew::prems = goal WF.thy
   241     "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==> \
   242 \    h(a) = H(a, lam x: r-``{a}. h(x))";
   243 by (rewtac rew);
   244 by (REPEAT (resolve_tac (prems@[wfrec]) 1));
   245 val def_wfrec = result();
   246 
   247 val prems = goal WF.thy
   248     "[| wf(r);  a:A;  field(r)<=A;  \
   249 \       !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)   \
   250 \    |] ==> wfrec(r,a,H) : B(a)";
   251 by (res_inst_tac [("a","a")] wf_induct2 1);
   252 by (rtac (wfrec RS ssubst) 4);
   253 by (REPEAT (ares_tac (prems@[lam_type]) 1
   254      ORELSE eresolve_tac [spec RS mp, underD] 1));
   255 val wfrec_type = result();
   256 
   257 val prems = goalw WF.thy [wfrec_def,wftrec_def,the_recfun_def,is_recfun_def]
   258     "[| r=r';  !!x u. H(x,u)=H'(x,u);  a=a' |] \
   259 \    ==> wfrec(r,a,H)=wfrec(r',a',H')";
   260 by (EVERY1 (map rtac (prems RL [subst])));
   261 by (SIMP_TAC (wf_ss addrews (prems RL [sym])) 1);
   262 val wfrec_cong = result();