src/ZF/WF.thy
 author wenzelm Tue Sep 25 22:36:06 2012 +0200 (2012-09-25 ago) changeset 49566 66cbf8bb4693 parent 46993 7371429c527d child 58871 c399ae4b836f permissions -rw-r--r--
basic integration of graphview into document model;
updated Isabelle/jEdit authors and dependencies etc.;
```     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) == \<forall>Z. Z=0 | (\<exists>x\<in>Z. \<forall>y. <y,x>:r \<longrightarrow> ~ y \<in> 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 \<inter> A*A)"
```
```    30
```
```    31 definition
```
```    32   is_recfun    :: "[i, i, [i,i]=>i, i] =>o"  where
```
```    33     "is_recfun(r,a,H,f) == (f = (\<lambda>x\<in>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 \<inter> 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 \<subseteq> 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) \<longleftrightarrow> 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 \<in> Z;  \<forall>x\<in>Z. \<exists>y\<in>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. \<forall>x\<in>A. (\<forall>y. <y,x>: r \<longrightarrow> y \<in> B) \<longrightarrow> x \<in> B ==> A<=B"} *}
```
```    93 lemma wf_onI2:
```
```    94  assumes prem: "!!y B. [| \<forall>x\<in>A. (\<forall>y\<in>A. <y,x>:r \<longrightarrow> y \<in> B) \<longrightarrow> x \<in> B;   y \<in> A |]
```
```    95                        ==> y \<in> 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_raw:
```
```   109     "[| wf(r);
```
```   110         !!x.[| \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |]
```
```   111      ==> P(a)"
```
```   112 apply (unfold wf_def)
```
```   113 apply (erule_tac x = "{z \<in> domain(r). ~ P(z)}" in allE)
```
```   114 apply blast
```
```   115 done
```
```   116
```
```   117 lemmas wf_induct = wf_induct_raw [rule_format, consumes 1, case_names step, 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 \<in> A;  field(r)<=A;
```
```   122         !!x.[| x \<in> A;  \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |]
```
```   123      ==>  P(a)"
```
```   124 apply (erule_tac P="a \<in> A" in rev_mp)
```
```   125 apply (erule_tac a=a in wf_induct, blast)
```
```   126 done
```
```   127
```
```   128 lemma field_Int_square: "field(r \<inter> A*A) \<subseteq> A"
```
```   129 by blast
```
```   130
```
```   131 lemma wf_on_induct_raw [consumes 2, induct set: wf_on]:
```
```   132     "[| wf[A](r);  a \<in> A;
```
```   133         !!x.[| x \<in> A;  \<forall>y\<in>A. <y,x>: r \<longrightarrow> 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 =
```
```   141   wf_on_induct_raw [rule_format, consumes 2, case_names step, 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. [| \<forall>x\<in>A. (\<forall>y\<in>A. <y,x>:r \<longrightarrow> y \<in> B) \<longrightarrow> x \<in> B;  y \<in> A|]
```
```   149                ==> y \<in> 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> \<notin> r"
```
```   161 by (erule_tac a=a in wf_induct, blast)
```
```   162
```
```   163 lemma wf_not_sym [rule_format]: "wf(r) ==> \<forall>x. <a,x>:r \<longrightarrow> <x,a> \<notin> r"
```
```   164 by (erule_tac a=a in wf_induct, blast)
```
```   165
```
```   166 (* @{term"[| wf(r);  <a,x> \<in> r;  ~P ==> <x,a> \<in> r |] ==> P"} *)
```
```   167 lemmas wf_asym = wf_not_sym [THEN swap]
```
```   168
```
```   169 lemma wf_on_not_refl: "[| wf[A](r); a \<in> A |] ==> <a,a> \<notin> 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 \<in> A |] ==> \<forall>b\<in>A. <a,b>:r \<longrightarrow> <b,a>\<notin>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> \<in> r;
```
```   179          <b,a> \<notin> r ==> Z; ~Z ==> a \<in> A; ~Z ==> b \<in> 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 \<inter> A*A);  thus wf( (r \<inter> 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 \<in> A; b \<in> A; c \<in> A |] ==> P"
```
```   187 apply (subgoal_tac "\<forall>y\<in>A. \<forall>z\<in>A. <a,y>:r \<longrightarrow> <y,z>:r \<longrightarrow> <z,a>:r \<longrightarrow> 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 \<subseteq> 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]
```
```   216 lemmas underD = vimage_singleton_iff [THEN iffD1]
```
```   217
```
```   218
```
```   219 subsection{*The Predicate @{term is_recfun}*}
```
```   220
```
```   221 lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f \<in> 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 \<longrightarrow> <x,b>:r \<longrightarrow> 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 "\<forall>y\<in>r-``{x}. \<forall>z. <y,z>:f \<longleftrightarrow> <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 = "\<lambda>y\<in>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 atomize
```
```   301 apply (frule spec [THEN mp], assumption)
```
```   302 apply (subgoal_tac "<xa,a1> \<in> r")
```
```   303  apply (drule_tac x1 = xa in spec [THEN mp], assumption)
```
```   304 apply (simp add: vimage_singleton_iff
```
```   305                  apply_recfun is_recfun_cut)
```
```   306 apply (blast dest: transD)
```
```   307 done
```
```   308
```
```   309
```
```   310 subsection{*Unfolding @{term "wftrec(r,a,H)"}*}
```
```   311
```
```   312 lemma the_recfun_cut:
```
```   313      "[| wf(r);  trans(r);  <b,a>:r |]
```
```   314       ==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"
```
```   315 by (blast intro: is_recfun_cut unfold_the_recfun)
```
```   316
```
```   317 (*NOT SUITABLE FOR REWRITING: it is recursive!*)
```
```   318 lemma wftrec:
```
```   319     "[| wf(r);  trans(r) |] ==>
```
```   320           wftrec(r,a,H) = H(a, \<lambda>x\<in>r-``{a}. wftrec(r,x,H))"
```
```   321 apply (unfold wftrec_def)
```
```   322 apply (subst unfold_the_recfun [unfolded is_recfun_def])
```
```   323 apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut)
```
```   324 done
```
```   325
```
```   326
```
```   327 subsubsection{*Removal of the Premise @{term "trans(r)"}*}
```
```   328
```
```   329 (*NOT SUITABLE FOR REWRITING: it is recursive!*)
```
```   330 lemma wfrec:
```
```   331     "wf(r) ==> wfrec(r,a,H) = H(a, \<lambda>x\<in>r-``{a}. wfrec(r,x,H))"
```
```   332 apply (unfold wfrec_def)
```
```   333 apply (erule wf_trancl [THEN wftrec, THEN ssubst])
```
```   334  apply (rule trans_trancl)
```
```   335 apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context])
```
```   336  apply (erule r_into_trancl)
```
```   337 apply (rule subset_refl)
```
```   338 done
```
```   339
```
```   340 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
```
```   341 lemma def_wfrec:
```
```   342     "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==>
```
```   343      h(a) = H(a, \<lambda>x\<in>r-``{a}. h(x))"
```
```   344 apply simp
```
```   345 apply (elim wfrec)
```
```   346 done
```
```   347
```
```   348 lemma wfrec_type:
```
```   349     "[| wf(r);  a \<in> A;  field(r)<=A;
```
```   350         !!x u. [| x \<in> A;  u \<in> Pi(r-``{x}, B) |] ==> H(x,u) \<in> B(x)
```
```   351      |] ==> wfrec(r,a,H) \<in> B(a)"
```
```   352 apply (rule_tac a = a in wf_induct2, assumption+)
```
```   353 apply (subst wfrec, assumption)
```
```   354 apply (simp add: lam_type underD)
```
```   355 done
```
```   356
```
```   357
```
```   358 lemma wfrec_on:
```
```   359  "[| wf[A](r);  a \<in> A |] ==>
```
```   360          wfrec[A](r,a,H) = H(a, \<lambda>x\<in>(r-``{a}) \<inter> A. wfrec[A](r,x,H))"
```
```   361 apply (unfold wf_on_def wfrec_on_def)
```
```   362 apply (erule wfrec [THEN trans])
```
```   363 apply (simp add: vimage_Int_square cons_subset_iff)
```
```   364 done
```
```   365
```
```   366 text{*Minimal-element characterization of well-foundedness*}
```
```   367 lemma wf_eq_minimal:
```
```   368      "wf(r) \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. <y,z>:r \<longrightarrow> y\<notin>Q))"
```
```   369 by (unfold wf_def, blast)
```
```   370
```
```   371 end
```