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