src/ZF/WF.thy
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 35762 af3ff2ba4c54
child 45602 2a858377c3d2
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     1 (*  Title:      ZF/WF.thy
     2     Author:     Tobias Nipkow and Lawrence C Paulson
     3     Copyright   1994  University of Cambridge
     4 
     5 Derived first for transitive relations, and finally for arbitrary WF relations
     6 via wf_trancl and trans_trancl.
     7 
     8 It is difficult to derive this general case directly, using r^+ instead of
     9 r.  In is_recfun, the two occurrences of the relation must have the same
    10 form.  Inserting r^+ in the_recfun or wftrec yields a recursion rule with
    11 r^+ -`` {a} instead of r-``{a}.  This recursion rule is stronger in
    12 principle, but harder to use, especially to prove wfrec_eclose_eq in
    13 epsilon.ML.  Expanding out the definition of wftrec in wfrec would yield
    14 a mess.
    15 *)
    16 
    17 header{*Well-Founded Recursion*}
    18 
    19 theory WF imports Trancl begin
    20 
    21 definition
    22   wf           :: "i=>o"  where
    23     (*r is a well-founded relation*)
    24     "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
    25 
    26 definition
    27   wf_on        :: "[i,i]=>o"                      ("wf[_]'(_')")  where
    28     (*r is well-founded on A*)
    29     "wf_on(A,r) == wf(r Int A*A)"
    30 
    31 definition
    32   is_recfun    :: "[i, i, [i,i]=>i, i] =>o"  where
    33     "is_recfun(r,a,H,f) == (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
    34 
    35 definition
    36   the_recfun   :: "[i, i, [i,i]=>i] =>i"  where
    37     "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))"
    38 
    39 definition
    40   wftrec :: "[i, i, [i,i]=>i] =>i"  where
    41     "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
    42 
    43 definition
    44   wfrec :: "[i, i, [i,i]=>i] =>i"  where
    45     (*public version.  Does not require r to be transitive*)
    46     "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
    47 
    48 definition
    49   wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"       ("wfrec[_]'(_,_,_')")  where
    50     "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)"
    51 
    52 
    53 subsection{*Well-Founded Relations*}
    54 
    55 subsubsection{*Equivalences between @{term wf} and @{term wf_on}*}
    56 
    57 lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)"
    58 by (unfold wf_def wf_on_def, force) 
    59 
    60 lemma wf_on_imp_wf: "[|wf[A](r); r <= A*A|] ==> wf(r)";
    61 by (simp add: wf_on_def subset_Int_iff)
    62 
    63 lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
    64 by (unfold wf_def wf_on_def, fast)
    65 
    66 lemma wf_iff_wf_on_field: "wf(r) <-> wf[field(r)](r)"
    67 by (blast intro: wf_imp_wf_on wf_on_field_imp_wf)
    68 
    69 lemma wf_on_subset_A: "[| wf[A](r);  B<=A |] ==> wf[B](r)"
    70 by (unfold wf_on_def wf_def, fast)
    71 
    72 lemma wf_on_subset_r: "[| wf[A](r); s<=r |] ==> wf[A](s)"
    73 by (unfold wf_on_def wf_def, fast)
    74 
    75 lemma wf_subset: "[|wf(s); r<=s|] ==> wf(r)"
    76 by (simp add: wf_def, fast)
    77 
    78 subsubsection{*Introduction Rules for @{term wf_on}*}
    79 
    80 text{*If every non-empty subset of @{term A} has an @{term r}-minimal element
    81    then we have @{term "wf[A](r)"}.*}
    82 lemma wf_onI:
    83  assumes prem: "!!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False"
    84  shows         "wf[A](r)"
    85 apply (unfold wf_on_def wf_def)
    86 apply (rule equals0I [THEN disjCI, THEN allI])
    87 apply (rule_tac Z = Z in prem, blast+)
    88 done
    89 
    90 text{*If @{term r} allows well-founded induction over @{term A}
    91    then we have @{term "wf[A](r)"}.   Premise is equivalent to
    92   @{prop "!!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B"} *}
    93 lemma wf_onI2:
    94  assumes prem: "!!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A |]
    95                        ==> y:B"
    96  shows         "wf[A](r)"
    97 apply (rule wf_onI)
    98 apply (rule_tac c=u in prem [THEN DiffE])
    99   prefer 3 apply blast 
   100  apply fast+
   101 done
   102 
   103 
   104 subsubsection{*Well-founded Induction*}
   105 
   106 text{*Consider the least @{term z} in @{term "domain(r)"} such that
   107   @{term "P(z)"} does not hold...*}
   108 lemma wf_induct [induct set: wf]:
   109     "[| wf(r);
   110         !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) |]  
   111      ==> P(a)"
   112 apply (unfold wf_def) 
   113 apply (erule_tac x = "{z : domain(r). ~ P(z)}" in allE)
   114 apply blast 
   115 done
   116 
   117 lemmas wf_induct_rule = wf_induct [rule_format, induct set: wf]
   118 
   119 text{*The form of this rule is designed to match @{text wfI}*}
   120 lemma wf_induct2:
   121     "[| wf(r);  a:A;  field(r)<=A;
   122         !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) |]
   123      ==>  P(a)"
   124 apply (erule_tac P="a:A" in rev_mp)
   125 apply (erule_tac a=a in wf_induct, blast) 
   126 done
   127 
   128 lemma field_Int_square: "field(r Int A*A) <= A"
   129 by blast
   130 
   131 lemma wf_on_induct [consumes 2, induct set: wf_on]:
   132     "[| wf[A](r);  a:A;
   133         !!x.[| x: A;  ALL y:A. <y,x>: r --> P(y) |] ==> P(x)
   134      |]  ==>  P(a)"
   135 apply (unfold wf_on_def) 
   136 apply (erule wf_induct2, assumption)
   137 apply (rule field_Int_square, blast)
   138 done
   139 
   140 lemmas wf_on_induct_rule =
   141   wf_on_induct [rule_format, consumes 2, induct set: wf_on]
   142 
   143 
   144 text{*If @{term r} allows well-founded induction 
   145    then we have @{term "wf(r)"}.*}
   146 lemma wfI:
   147     "[| field(r)<=A;
   148         !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;  y:A|]
   149                ==> y:B |]
   150      ==>  wf(r)"
   151 apply (rule wf_on_subset_A [THEN wf_on_field_imp_wf])
   152 apply (rule wf_onI2)
   153  prefer 2 apply blast  
   154 apply blast 
   155 done
   156 
   157 
   158 subsection{*Basic Properties of Well-Founded Relations*}
   159 
   160 lemma wf_not_refl: "wf(r) ==> <a,a> ~: r"
   161 by (erule_tac a=a in wf_induct, blast)
   162 
   163 lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. <a,x>:r --> <x,a> ~: r"
   164 by (erule_tac a=a in wf_induct, blast)
   165 
   166 (* [| wf(r);  <a,x> : r;  ~P ==> <x,a> : r |] ==> P *)
   167 lemmas wf_asym = wf_not_sym [THEN swap, standard]
   168 
   169 lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> <a,a> ~: r"
   170 by (erule_tac a=a in wf_on_induct, assumption, blast)
   171 
   172 lemma wf_on_not_sym [rule_format]:
   173      "[| wf[A](r);  a:A |] ==> ALL b:A. <a,b>:r --> <b,a>~:r"
   174 apply (erule_tac a=a in wf_on_induct, assumption, blast)
   175 done
   176 
   177 lemma wf_on_asym:
   178      "[| wf[A](r);  ~Z ==> <a,b> : r;
   179          <b,a> ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z"
   180 by (blast dest: wf_on_not_sym) 
   181 
   182 
   183 (*Needed to prove well_ordI.  Could also reason that wf[A](r) means
   184   wf(r Int A*A);  thus wf( (r Int A*A)^+ ) and use wf_not_refl *)
   185 lemma wf_on_chain3:
   186      "[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P"
   187 apply (subgoal_tac "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P",
   188        blast) 
   189 apply (erule_tac a=a in wf_on_induct, assumption, blast)
   190 done
   191 
   192 
   193 
   194 text{*transitive closure of a WF relation is WF provided 
   195   @{term A} is downward closed*}
   196 lemma wf_on_trancl:
   197     "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)"
   198 apply (rule wf_onI2)
   199 apply (frule bspec [THEN mp], assumption+)
   200 apply (erule_tac a = y in wf_on_induct, assumption)
   201 apply (blast elim: tranclE, blast) 
   202 done
   203 
   204 lemma wf_trancl: "wf(r) ==> wf(r^+)"
   205 apply (simp add: wf_iff_wf_on_field)
   206 apply (rule wf_on_subset_A) 
   207  apply (erule wf_on_trancl)
   208  apply blast 
   209 apply (rule trancl_type [THEN field_rel_subset])
   210 done
   211 
   212 
   213 text{*@{term "r-``{a}"} is the set of everything under @{term a} in @{term r}*}
   214 
   215 lemmas underI = vimage_singleton_iff [THEN iffD2, standard]
   216 lemmas underD = vimage_singleton_iff [THEN iffD1, standard]
   217 
   218 
   219 subsection{*The Predicate @{term is_recfun}*}
   220 
   221 lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)"
   222 apply (unfold is_recfun_def)
   223 apply (erule ssubst)
   224 apply (rule lamI [THEN rangeI, THEN lam_type], assumption)
   225 done
   226 
   227 lemmas is_recfun_imp_function = is_recfun_type [THEN fun_is_function]
   228 
   229 lemma apply_recfun:
   230     "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
   231 apply (unfold is_recfun_def) 
   232   txt{*replace f only on the left-hand side*}
   233 apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
   234 apply (simp add: underI) 
   235 done
   236 
   237 lemma is_recfun_equal [rule_format]:
   238      "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |]
   239       ==> <x,a>:r --> <x,b>:r --> f`x=g`x"
   240 apply (frule_tac f = f in is_recfun_type)
   241 apply (frule_tac f = g in is_recfun_type)
   242 apply (simp add: is_recfun_def)
   243 apply (erule_tac a=x in wf_induct)
   244 apply (intro impI)
   245 apply (elim ssubst)
   246 apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
   247 apply (rule_tac t = "%z. H (?x,z) " in subst_context)
   248 apply (subgoal_tac "ALL y : r-``{x}. ALL z. <y,z>:f <-> <y,z>:g")
   249  apply (blast dest: transD)
   250 apply (simp add: apply_iff)
   251 apply (blast dest: transD intro: sym)
   252 done
   253 
   254 lemma is_recfun_cut:
   255      "[| wf(r);  trans(r);
   256          is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |]
   257       ==> restrict(f, r-``{b}) = g"
   258 apply (frule_tac f = f in is_recfun_type)
   259 apply (rule fun_extension)
   260   apply (blast dest: transD intro: restrict_type2)
   261  apply (erule is_recfun_type, simp)
   262 apply (blast dest: transD intro: is_recfun_equal)
   263 done
   264 
   265 subsection{*Recursion: Main Existence Lemma*}
   266 
   267 lemma is_recfun_functional:
   268      "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g"
   269 by (blast intro: fun_extension is_recfun_type is_recfun_equal)
   270 
   271 lemma the_recfun_eq:
   272     "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |] ==> the_recfun(r,a,H) = f"
   273 apply (unfold the_recfun_def)
   274 apply (blast intro: is_recfun_functional)
   275 done
   276 
   277 (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
   278 lemma is_the_recfun:
   279     "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]
   280      ==> is_recfun(r, a, H, the_recfun(r,a,H))"
   281 by (simp add: the_recfun_eq)
   282 
   283 lemma unfold_the_recfun:
   284      "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))"
   285 apply (rule_tac a=a in wf_induct, assumption)
   286 apply (rename_tac a1) 
   287 apply (rule_tac f = "lam y: r-``{a1}. wftrec (r,y,H)" in is_the_recfun)
   288   apply typecheck
   289 apply (unfold is_recfun_def wftrec_def)
   290   --{*Applying the substitution: must keep the quantified assumption!*}
   291 apply (rule lam_cong [OF refl]) 
   292 apply (drule underD) 
   293 apply (fold is_recfun_def)
   294 apply (rule_tac t = "%z. H(?x,z)" in subst_context)
   295 apply (rule fun_extension)
   296   apply (blast intro: is_recfun_type)
   297  apply (rule lam_type [THEN restrict_type2])
   298   apply blast
   299  apply (blast dest: transD)
   300 apply (frule spec [THEN mp], assumption)
   301 apply (subgoal_tac "<xa,a1> : r")
   302  apply (drule_tac x1 = xa in spec [THEN mp], assumption)
   303 apply (simp add: vimage_singleton_iff 
   304                  apply_recfun is_recfun_cut)
   305 apply (blast dest: transD)
   306 done
   307 
   308 
   309 subsection{*Unfolding @{term "wftrec(r,a,H)"}*}
   310 
   311 lemma the_recfun_cut:
   312      "[| wf(r);  trans(r);  <b,a>:r |]
   313       ==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"
   314 by (blast intro: is_recfun_cut unfold_the_recfun)
   315 
   316 (*NOT SUITABLE FOR REWRITING: it is recursive!*)
   317 lemma wftrec:
   318     "[| wf(r);  trans(r) |] ==>
   319           wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))"
   320 apply (unfold wftrec_def)
   321 apply (subst unfold_the_recfun [unfolded is_recfun_def])
   322 apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut)
   323 done
   324 
   325 
   326 subsubsection{*Removal of the Premise @{term "trans(r)"}*}
   327 
   328 (*NOT SUITABLE FOR REWRITING: it is recursive!*)
   329 lemma wfrec:
   330     "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))"
   331 apply (unfold wfrec_def) 
   332 apply (erule wf_trancl [THEN wftrec, THEN ssubst])
   333  apply (rule trans_trancl)
   334 apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context])
   335  apply (erule r_into_trancl)
   336 apply (rule subset_refl)
   337 done
   338 
   339 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   340 lemma def_wfrec:
   341     "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==>
   342      h(a) = H(a, lam x: r-``{a}. h(x))"
   343 apply simp
   344 apply (elim wfrec) 
   345 done
   346 
   347 lemma wfrec_type:
   348     "[| wf(r);  a:A;  field(r)<=A;
   349         !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)
   350      |] ==> wfrec(r,a,H) : B(a)"
   351 apply (rule_tac a = a in wf_induct2, assumption+)
   352 apply (subst wfrec, assumption)
   353 apply (simp add: lam_type underD)  
   354 done
   355 
   356 
   357 lemma wfrec_on:
   358  "[| wf[A](r);  a: A |] ==>
   359          wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))"
   360 apply (unfold wf_on_def wfrec_on_def)
   361 apply (erule wfrec [THEN trans])
   362 apply (simp add: vimage_Int_square cons_subset_iff)
   363 done
   364 
   365 text{*Minimal-element characterization of well-foundedness*}
   366 lemma wf_eq_minimal:
   367      "wf(r) <-> (ALL Q x. x:Q --> (EX z:Q. ALL y. <y,z>:r --> y~:Q))"
   368 by (unfold wf_def, blast)
   369 
   370 end