src/ZF/WF.ML
author lcp
Tue Jun 21 17:20:34 1994 +0200 (1994-06-21)
changeset 435 ca5356bd315a
parent 6 8ce8c4d13d4d
child 437 435875e4b21d
permissions -rw-r--r--
Addition of cardinals and order types, various tidying
     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 
    23 (*** Well-founded relations ***)
    24 
    25 (** Equivalences between wf and wf_on **)
    26 
    27 goalw WF.thy [wf_def, wf_on_def] "!!A r. wf(r) ==> wf[A](r)";
    28 by (fast_tac ZF_cs 1);
    29 val wf_imp_wf_on = result();
    30 
    31 goalw WF.thy [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)";
    32 by (fast_tac ZF_cs 1);
    33 val wf_on_field_imp_wf = result();
    34 
    35 goal WF.thy "wf(r) <-> wf[field(r)](r)";
    36 by (fast_tac (ZF_cs addSEs [wf_imp_wf_on, wf_on_field_imp_wf]) 1);
    37 val wf_iff_wf_on_field = result();
    38 
    39 goalw WF.thy [wf_on_def, wf_def] "!!A B r. [| wf[A](r);  B<=A |] ==> wf[B](r)";
    40 by (fast_tac ZF_cs 1);
    41 val wf_on_subset_A = result();
    42 
    43 goalw WF.thy [wf_on_def, wf_def] "!!A r s. [| wf[A](r);  s<=r |] ==> wf[A](s)";
    44 by (fast_tac ZF_cs 1);
    45 val wf_on_subset_r = result();
    46 
    47 (** Introduction rules for wf_on **)
    48 
    49 (*If every non-empty subset of A has an r-minimal element then wf[A](r).*)
    50 val [prem] = goalw WF.thy [wf_on_def, wf_def]
    51     "[| !!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \
    52 \    ==>  wf[A](r)";
    53 by (rtac (equals0I RS disjCI RS allI) 1);
    54 by (res_inst_tac [ ("Z", "Z") ] prem 1);
    55 by (ALLGOALS (fast_tac ZF_cs));
    56 val wf_onI = result();
    57 
    58 (*If r allows well-founded induction over A then wf[A](r)
    59   Premise is equivalent to 
    60   !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B  *)
    61 val [prem] = goal WF.thy
    62     "[| !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
    63 \              |] ==> y:B |] \
    64 \    ==>  wf[A](r)";
    65 br wf_onI 1;
    66 by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1);
    67 by (contr_tac 3);
    68 by (fast_tac ZF_cs 2);
    69 by (fast_tac ZF_cs 1);
    70 val wf_onI2 = result();
    71 
    72 
    73 (** Well-founded Induction **)
    74 
    75 (*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*)
    76 val major::prems = goalw WF.thy [wf_def]
    77     "[| wf(r);          \
    78 \       !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) \
    79 \    |]  ==>  P(a)";
    80 by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ]  (major RS allE) 1);
    81 by (etac disjE 1);
    82 by (rtac classical 1);
    83 by (etac equals0D 1);
    84 by (etac (singletonI RS UnI2 RS CollectI) 1);
    85 by (etac bexE 1);
    86 by (etac CollectE 1);
    87 by (etac swap 1);
    88 by (resolve_tac prems 1);
    89 by (fast_tac ZF_cs 1);
    90 val wf_induct = result();
    91 
    92 (*Perform induction on i, then prove the wf(r) subgoal using prems. *)
    93 fun wf_ind_tac a prems i = 
    94     EVERY [res_inst_tac [("a",a)] wf_induct i,
    95 	   rename_last_tac a ["1"] (i+1),
    96 	   ares_tac prems i];
    97 
    98 (*The form of this rule is designed to match wfI2*)
    99 val wfr::amem::prems = goal WF.thy
   100     "[| wf(r);  a:A;  field(r)<=A;  \
   101 \       !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) \
   102 \    |]  ==>  P(a)";
   103 by (rtac (amem RS rev_mp) 1);
   104 by (wf_ind_tac "a" [wfr] 1);
   105 by (rtac impI 1);
   106 by (eresolve_tac prems 1);
   107 by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1);
   108 val wf_induct2 = result();
   109 
   110 goal ZF.thy "!!r A. field(r Int A*A) <= A";
   111 by (fast_tac ZF_cs 1);
   112 val field_Int_square = result();
   113 
   114 val wfr::amem::prems = goalw WF.thy [wf_on_def]
   115     "[| wf[A](r);  a:A;  					\
   116 \       !!x.[| x: A;  ALL y:A. <y,x>: r --> P(y) |] ==> P(x) 	\
   117 \    |]  ==>  P(a)";
   118 by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1);
   119 by (REPEAT (ares_tac prems 1));
   120 by (fast_tac ZF_cs 1);
   121 val wf_on_induct = result();
   122 
   123 fun wf_on_ind_tac a prems i = 
   124     EVERY [res_inst_tac [("a",a)] wf_on_induct i,
   125 	   rename_last_tac a ["1"] (i+2),
   126 	   REPEAT (ares_tac prems i)];
   127 
   128 (*If r allows well-founded induction then wf(r)*)
   129 val [subs,indhyp] = goal WF.thy
   130     "[| field(r)<=A;  \
   131 \       !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
   132 \              |] ==> y:B |] \
   133 \    ==>  wf(r)";
   134 br ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1;
   135 by (REPEAT (ares_tac [indhyp] 1));
   136 val wfI2 = result();
   137 
   138 
   139 (*** Properties of well-founded relations ***)
   140 
   141 goal WF.thy "!!r. wf(r) ==> <a,a> ~: r";
   142 by (wf_ind_tac "a" [] 1);
   143 by (fast_tac ZF_cs 1);
   144 val wf_not_refl = result();
   145 
   146 goal WF.thy "!!r. [| wf(r);  <a,x>:r;  <x,a>:r |] ==> P";
   147 by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
   148 by (wf_ind_tac "a" [] 2);
   149 by (fast_tac ZF_cs 2);
   150 by (fast_tac FOL_cs 1);
   151 val wf_anti_sym = result();
   152 
   153 goal WF.thy "!!r. [| wf[A](r); a: A |] ==> <a,a> ~: r";
   154 by (wf_on_ind_tac "a" [] 1);
   155 by (fast_tac ZF_cs 1);
   156 val wf_on_not_refl = result();
   157 
   158 goal WF.thy "!!r. [| wf[A](r);  <a,b>:r;  <b,a>:r;  a:A;  b:A |] ==> P";
   159 by (subgoal_tac "ALL y:A. <a,y>:r --> <y,a>:r --> P" 1);
   160 by (wf_on_ind_tac "a" [] 2);
   161 by (fast_tac ZF_cs 2);
   162 by (fast_tac ZF_cs 1);
   163 val wf_on_anti_sym = result();
   164 
   165 (*Needed to prove well_ordI.  Could also reason that wf[A](r) means
   166   wf(r Int A*A);  thus wf( (r Int A*A)^+ ) and use wf_not_refl *)
   167 goal WF.thy
   168     "!!r. [| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P";
   169 by (subgoal_tac
   170     "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P" 1);
   171 by (wf_on_ind_tac "a" [] 2);
   172 by (fast_tac ZF_cs 2);
   173 by (fast_tac ZF_cs 1);
   174 val wf_on_chain3 = result();
   175 
   176 
   177 (*retains the universal formula for later use!*)
   178 val bchain_tac = EVERY' [rtac (bspec RS mp), assume_tac, assume_tac ];
   179 
   180 (*transitive closure of a WF relation is WF provided A is downwards closed*)
   181 val [wfr,subs] = goal WF.thy
   182     "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)";
   183 br wf_onI2 1;
   184 by (bchain_tac 1);
   185 by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1);
   186 by (rtac (impI RS ballI) 1);
   187 by (etac tranclE 1);
   188 by (etac (bspec RS mp) 1 THEN assume_tac 1);
   189 by (fast_tac ZF_cs 1);
   190 by (cut_facts_tac [subs] 1);
   191 (*astar_tac is slightly faster*)
   192 by (best_tac ZF_cs 1);
   193 val wf_on_trancl = result();
   194 
   195 goal WF.thy "!!r. wf(r) ==> wf(r^+)";
   196 by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1);
   197 br (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1;
   198 be wf_on_trancl 1;
   199 by (fast_tac ZF_cs 1);
   200 val wf_trancl = result();
   201 
   202 
   203 
   204 (** r-``{a} is the set of everything under a in r **)
   205 
   206 val underI = standard (vimage_singleton_iff RS iffD2);
   207 val underD = standard (vimage_singleton_iff RS iffD1);
   208 
   209 (** is_recfun **)
   210 
   211 val [major] = goalw WF.thy [is_recfun_def]
   212     "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
   213 by (rtac (major RS ssubst) 1);
   214 by (rtac (lamI RS rangeI RS lam_type) 1);
   215 by (assume_tac 1);
   216 val is_recfun_type = result();
   217 
   218 val [isrec,rel] = goalw WF.thy [is_recfun_def]
   219     "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))";
   220 by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (isrec RS ssubst) 1);
   221 by (rtac (rel RS underI RS beta) 1);
   222 val apply_recfun = result();
   223 
   224 (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
   225   spec RS mp  instantiates induction hypotheses*)
   226 fun indhyp_tac hyps =
   227     resolve_tac (TrueI::refl::hyps) ORELSE' 
   228     (cut_facts_tac hyps THEN'
   229        DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
   230 		        eresolve_tac [underD, transD, spec RS mp]));
   231 
   232 (*** NOTE! some simplifications need a different solver!! ***)
   233 val wf_super_ss = ZF_ss setsolver indhyp_tac;
   234 
   235 val prems = goalw WF.thy [is_recfun_def]
   236     "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
   237 \    <x,a>:r --> <x,b>:r --> f`x=g`x";
   238 by (cut_facts_tac prems 1);
   239 by (wf_ind_tac "x" prems 1);
   240 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
   241 by (rewtac restrict_def);
   242 by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
   243 val is_recfun_equal_lemma = result();
   244 val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
   245 
   246 val prems as [wfr,transr,recf,recg,_] = goal WF.thy
   247     "[| wf(r);  trans(r);       \
   248 \       is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |] ==> \
   249 \    restrict(f, r-``{b}) = g";
   250 by (cut_facts_tac prems 1);
   251 by (rtac (consI1 RS restrict_type RS fun_extension) 1);
   252 by (etac is_recfun_type 1);
   253 by (ALLGOALS
   254     (asm_simp_tac (wf_super_ss addsimps
   255 		   [ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
   256 val is_recfun_cut = result();
   257 
   258 (*** Main Existence Lemma ***)
   259 
   260 val prems = goal WF.thy
   261     "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g";
   262 by (cut_facts_tac prems 1);
   263 by (rtac fun_extension 1);
   264 by (REPEAT (ares_tac [is_recfun_equal] 1
   265      ORELSE eresolve_tac [is_recfun_type,underD] 1));
   266 val is_recfun_functional = result();
   267 
   268 (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
   269 val prems = goalw WF.thy [the_recfun_def]
   270     "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]  \
   271 \    ==> is_recfun(r, a, H, the_recfun(r,a,H))";
   272 by (rtac (ex1I RS theI) 1);
   273 by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1));
   274 val is_the_recfun = result();
   275 
   276 val prems = goal WF.thy
   277     "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))";
   278 by (cut_facts_tac prems 1);
   279 by (wf_ind_tac "a" prems 1);
   280 by (res_inst_tac [("f", "lam y: r-``{a1}. wftrec(r,y,H)")] is_the_recfun 1);
   281 by (REPEAT (assume_tac 2));
   282 by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
   283 (*Applying the substitution: must keep the quantified assumption!!*)
   284 by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
   285 by (fold_tac [is_recfun_def]);
   286 by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
   287 by (rtac is_recfun_type 1);
   288 by (ALLGOALS
   289     (asm_simp_tac
   290      (wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut])));
   291 val unfold_the_recfun = result();
   292 
   293 
   294 (*** Unfolding wftrec ***)
   295 
   296 val prems = goal WF.thy
   297     "[| wf(r);  trans(r);  <b,a>:r |] ==> \
   298 \    restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)";
   299 by (REPEAT (ares_tac (prems @ [is_recfun_cut, unfold_the_recfun]) 1));
   300 val the_recfun_cut = result();
   301 
   302 (*NOT SUITABLE FOR REWRITING since it is recursive!*)
   303 goalw WF.thy [wftrec_def]
   304     "!!r. [| wf(r);  trans(r) |] ==> \
   305 \         wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
   306 by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
   307 by (ALLGOALS (asm_simp_tac
   308 	(ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
   309 val wftrec = result();
   310 
   311 (** Removal of the premise trans(r) **)
   312 
   313 (*NOT SUITABLE FOR REWRITING since it is recursive!*)
   314 val [wfr] = goalw WF.thy [wfrec_def]
   315     "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
   316 by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
   317 by (rtac trans_trancl 1);
   318 by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
   319 by (etac r_into_trancl 1);
   320 by (rtac subset_refl 1);
   321 val wfrec = result();
   322 
   323 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   324 val rew::prems = goal WF.thy
   325     "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==> \
   326 \    h(a) = H(a, lam x: r-``{a}. h(x))";
   327 by (rewtac rew);
   328 by (REPEAT (resolve_tac (prems@[wfrec]) 1));
   329 val def_wfrec = result();
   330 
   331 val prems = goal WF.thy
   332     "[| wf(r);  a:A;  field(r)<=A;  \
   333 \       !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)   \
   334 \    |] ==> wfrec(r,a,H) : B(a)";
   335 by (res_inst_tac [("a","a")] wf_induct2 1);
   336 by (rtac (wfrec RS ssubst) 4);
   337 by (REPEAT (ares_tac (prems@[lam_type]) 1
   338      ORELSE eresolve_tac [spec RS mp, underD] 1));
   339 val wfrec_type = result();
   340 
   341 
   342 goalw WF.thy [wf_on_def, wfrec_on_def]
   343  "!!A r. [| wf[A](r);  a: A |] ==> \
   344 \        wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))";
   345 be (wfrec RS trans) 1;
   346 by (asm_simp_tac (ZF_ss addsimps [vimage_Int_square, cons_subset_iff]) 1);
   347 val wfrec_on = result();
   348