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