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