src/ZF/Fixedpt.thy
 author wenzelm Tue Jul 31 19:40:22 2007 +0200 (2007-07-31) changeset 24091 109f19a13872 parent 16417 9bc16273c2d4 child 24893 b8ef7afe3a6b permissions -rw-r--r--
```     1 (*  Title:      ZF/fixedpt.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1992  University of Cambridge
```
```     5 *)
```
```     6
```
```     7 header{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*}
```
```     8
```
```     9 theory Fixedpt imports equalities begin
```
```    10
```
```    11 constdefs
```
```    12
```
```    13   (*monotone operator from Pow(D) to itself*)
```
```    14   bnd_mono :: "[i,i=>i]=>o"
```
```    15      "bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))"
```
```    16
```
```    17   lfp      :: "[i,i=>i]=>i"
```
```    18      "lfp(D,h) == Inter({X: Pow(D). h(X) <= X})"
```
```    19
```
```    20   gfp      :: "[i,i=>i]=>i"
```
```    21      "gfp(D,h) == Union({X: Pow(D). X <= h(X)})"
```
```    22
```
```    23 text{*The theorem is proved in the lattice of subsets of @{term D},
```
```    24       namely @{term "Pow(D)"}, with Inter as the greatest lower bound.*}
```
```    25
```
```    26 subsection{*Monotone Operators*}
```
```    27
```
```    28 lemma bnd_monoI:
```
```    29     "[| h(D)<=D;
```
```    30         !!W X. [| W<=D;  X<=D;  W<=X |] ==> h(W) <= h(X)
```
```    31      |] ==> bnd_mono(D,h)"
```
```    32 by (unfold bnd_mono_def, clarify, blast)
```
```    33
```
```    34 lemma bnd_monoD1: "bnd_mono(D,h) ==> h(D) <= D"
```
```    35 apply (unfold bnd_mono_def)
```
```    36 apply (erule conjunct1)
```
```    37 done
```
```    38
```
```    39 lemma bnd_monoD2: "[| bnd_mono(D,h);  W<=X;  X<=D |] ==> h(W) <= h(X)"
```
```    40 by (unfold bnd_mono_def, blast)
```
```    41
```
```    42 lemma bnd_mono_subset:
```
```    43     "[| bnd_mono(D,h);  X<=D |] ==> h(X) <= D"
```
```    44 by (unfold bnd_mono_def, clarify, blast)
```
```    45
```
```    46 lemma bnd_mono_Un:
```
```    47      "[| bnd_mono(D,h);  A <= D;  B <= D |] ==> h(A) Un h(B) <= h(A Un B)"
```
```    48 apply (unfold bnd_mono_def)
```
```    49 apply (rule Un_least, blast+)
```
```    50 done
```
```    51
```
```    52 (*unused*)
```
```    53 lemma bnd_mono_UN:
```
```    54      "[| bnd_mono(D,h);  \<forall>i\<in>I. A(i) <= D |]
```
```    55       ==> (\<Union>i\<in>I. h(A(i))) <= h((\<Union>i\<in>I. A(i)))"
```
```    56 apply (unfold bnd_mono_def)
```
```    57 apply (rule UN_least)
```
```    58 apply (elim conjE)
```
```    59 apply (drule_tac x="A(i)" in spec)
```
```    60 apply (drule_tac x="(\<Union>i\<in>I. A(i))" in spec)
```
```    61 apply blast
```
```    62 done
```
```    63
```
```    64 (*Useful??*)
```
```    65 lemma bnd_mono_Int:
```
```    66      "[| bnd_mono(D,h);  A <= D;  B <= D |] ==> h(A Int B) <= h(A) Int h(B)"
```
```    67 apply (rule Int_greatest)
```
```    68 apply (erule bnd_monoD2, rule Int_lower1, assumption)
```
```    69 apply (erule bnd_monoD2, rule Int_lower2, assumption)
```
```    70 done
```
```    71
```
```    72 subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*}
```
```    73
```
```    74 (*lfp is contained in each pre-fixedpoint*)
```
```    75 lemma lfp_lowerbound:
```
```    76     "[| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A"
```
```    77 by (unfold lfp_def, blast)
```
```    78
```
```    79 (*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)
```
```    80 lemma lfp_subset: "lfp(D,h) <= D"
```
```    81 by (unfold lfp_def Inter_def, blast)
```
```    82
```
```    83 (*Used in datatype package*)
```
```    84 lemma def_lfp_subset:  "A == lfp(D,h) ==> A <= D"
```
```    85 apply simp
```
```    86 apply (rule lfp_subset)
```
```    87 done
```
```    88
```
```    89 lemma lfp_greatest:
```
```    90     "[| h(D) <= D;  !!X. [| h(X) <= X;  X<=D |] ==> A<=X |] ==> A <= lfp(D,h)"
```
```    91 by (unfold lfp_def, blast)
```
```    92
```
```    93 lemma lfp_lemma1:
```
```    94     "[| bnd_mono(D,h);  h(A)<=A;  A<=D |] ==> h(lfp(D,h)) <= A"
```
```    95 apply (erule bnd_monoD2 [THEN subset_trans])
```
```    96 apply (rule lfp_lowerbound, assumption+)
```
```    97 done
```
```    98
```
```    99 lemma lfp_lemma2: "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)"
```
```   100 apply (rule bnd_monoD1 [THEN lfp_greatest])
```
```   101 apply (rule_tac [2] lfp_lemma1)
```
```   102 apply (assumption+)
```
```   103 done
```
```   104
```
```   105 lemma lfp_lemma3:
```
```   106     "bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))"
```
```   107 apply (rule lfp_lowerbound)
```
```   108 apply (rule bnd_monoD2, assumption)
```
```   109 apply (rule lfp_lemma2, assumption)
```
```   110 apply (erule_tac [2] bnd_mono_subset)
```
```   111 apply (rule lfp_subset)+
```
```   112 done
```
```   113
```
```   114 lemma lfp_unfold: "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))"
```
```   115 apply (rule equalityI)
```
```   116 apply (erule lfp_lemma3)
```
```   117 apply (erule lfp_lemma2)
```
```   118 done
```
```   119
```
```   120 (*Definition form, to control unfolding*)
```
```   121 lemma def_lfp_unfold:
```
```   122     "[| A==lfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)"
```
```   123 apply simp
```
```   124 apply (erule lfp_unfold)
```
```   125 done
```
```   126
```
```   127 subsection{*General Induction Rule for Least Fixedpoints*}
```
```   128
```
```   129 lemma Collect_is_pre_fixedpt:
```
```   130     "[| bnd_mono(D,h);  !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) |]
```
```   131      ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)"
```
```   132 by (blast intro: lfp_lemma2 [THEN subsetD] bnd_monoD2 [THEN subsetD]
```
```   133                  lfp_subset [THEN subsetD])
```
```   134
```
```   135 (*This rule yields an induction hypothesis in which the components of a
```
```   136   data structure may be assumed to be elements of lfp(D,h)*)
```
```   137 lemma induct:
```
```   138     "[| bnd_mono(D,h);  a : lfp(D,h);
```
```   139         !!x. x : h(Collect(lfp(D,h),P)) ==> P(x)
```
```   140      |] ==> P(a)"
```
```   141 apply (rule Collect_is_pre_fixedpt
```
```   142               [THEN lfp_lowerbound, THEN subsetD, THEN CollectD2])
```
```   143 apply (rule_tac [3] lfp_subset [THEN Collect_subset [THEN subset_trans]],
```
```   144        blast+)
```
```   145 done
```
```   146
```
```   147 (*Definition form, to control unfolding*)
```
```   148 lemma def_induct:
```
```   149     "[| A == lfp(D,h);  bnd_mono(D,h);  a:A;
```
```   150         !!x. x : h(Collect(A,P)) ==> P(x)
```
```   151      |] ==> P(a)"
```
```   152 by (rule induct, blast+)
```
```   153
```
```   154 (*This version is useful when "A" is not a subset of D
```
```   155   second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *)
```
```   156 lemma lfp_Int_lowerbound:
```
```   157     "[| h(D Int A) <= A;  bnd_mono(D,h) |] ==> lfp(D,h) <= A"
```
```   158 apply (rule lfp_lowerbound [THEN subset_trans])
```
```   159 apply (erule bnd_mono_subset [THEN Int_greatest], blast+)
```
```   160 done
```
```   161
```
```   162 (*Monotonicity of lfp, where h precedes i under a domain-like partial order
```
```   163   monotonicity of h is not strictly necessary; h must be bounded by D*)
```
```   164 lemma lfp_mono:
```
```   165   assumes hmono: "bnd_mono(D,h)"
```
```   166       and imono: "bnd_mono(E,i)"
```
```   167       and subhi: "!!X. X<=D ==> h(X) <= i(X)"
```
```   168     shows "lfp(D,h) <= lfp(E,i)"
```
```   169 apply (rule bnd_monoD1 [THEN lfp_greatest])
```
```   170 apply (rule imono)
```
```   171 apply (rule hmono [THEN [2] lfp_Int_lowerbound])
```
```   172 apply (rule Int_lower1 [THEN subhi, THEN subset_trans])
```
```   173 apply (rule imono [THEN bnd_monoD2, THEN subset_trans], auto)
```
```   174 done
```
```   175
```
```   176 (*This (unused) version illustrates that monotonicity is not really needed,
```
```   177   but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)
```
```   178 lemma lfp_mono2:
```
```   179     "[| i(D) <= D;  !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(D,i)"
```
```   180 apply (rule lfp_greatest, assumption)
```
```   181 apply (rule lfp_lowerbound, blast, assumption)
```
```   182 done
```
```   183
```
```   184 lemma lfp_cong:
```
```   185      "[|D=D'; !!X. X <= D' ==> h(X) = h'(X)|] ==> lfp(D,h) = lfp(D',h')"
```
```   186 apply (simp add: lfp_def)
```
```   187 apply (rule_tac t=Inter in subst_context)
```
```   188 apply (rule Collect_cong, simp_all)
```
```   189 done
```
```   190
```
```   191
```
```   192 subsection{*Proof of Knaster-Tarski Theorem using @{term gfp}*}
```
```   193
```
```   194 (*gfp contains each post-fixedpoint that is contained in D*)
```
```   195 lemma gfp_upperbound: "[| A <= h(A);  A<=D |] ==> A <= gfp(D,h)"
```
```   196 apply (unfold gfp_def)
```
```   197 apply (rule PowI [THEN CollectI, THEN Union_upper])
```
```   198 apply (assumption+)
```
```   199 done
```
```   200
```
```   201 lemma gfp_subset: "gfp(D,h) <= D"
```
```   202 by (unfold gfp_def, blast)
```
```   203
```
```   204 (*Used in datatype package*)
```
```   205 lemma def_gfp_subset: "A==gfp(D,h) ==> A <= D"
```
```   206 apply simp
```
```   207 apply (rule gfp_subset)
```
```   208 done
```
```   209
```
```   210 lemma gfp_least:
```
```   211     "[| bnd_mono(D,h);  !!X. [| X <= h(X);  X<=D |] ==> X<=A |] ==>
```
```   212      gfp(D,h) <= A"
```
```   213 apply (unfold gfp_def)
```
```   214 apply (blast dest: bnd_monoD1)
```
```   215 done
```
```   216
```
```   217 lemma gfp_lemma1:
```
```   218     "[| bnd_mono(D,h);  A<=h(A);  A<=D |] ==> A <= h(gfp(D,h))"
```
```   219 apply (rule subset_trans, assumption)
```
```   220 apply (erule bnd_monoD2)
```
```   221 apply (rule_tac [2] gfp_subset)
```
```   222 apply (simp add: gfp_upperbound)
```
```   223 done
```
```   224
```
```   225 lemma gfp_lemma2: "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))"
```
```   226 apply (rule gfp_least)
```
```   227 apply (rule_tac [2] gfp_lemma1)
```
```   228 apply (assumption+)
```
```   229 done
```
```   230
```
```   231 lemma gfp_lemma3:
```
```   232     "bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)"
```
```   233 apply (rule gfp_upperbound)
```
```   234 apply (rule bnd_monoD2, assumption)
```
```   235 apply (rule gfp_lemma2, assumption)
```
```   236 apply (erule bnd_mono_subset, rule gfp_subset)+
```
```   237 done
```
```   238
```
```   239 lemma gfp_unfold: "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))"
```
```   240 apply (rule equalityI)
```
```   241 apply (erule gfp_lemma2)
```
```   242 apply (erule gfp_lemma3)
```
```   243 done
```
```   244
```
```   245 (*Definition form, to control unfolding*)
```
```   246 lemma def_gfp_unfold:
```
```   247     "[| A==gfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)"
```
```   248 apply simp
```
```   249 apply (erule gfp_unfold)
```
```   250 done
```
```   251
```
```   252
```
```   253 subsection{*Coinduction Rules for Greatest Fixed Points*}
```
```   254
```
```   255 (*weak version*)
```
```   256 lemma weak_coinduct: "[| a: X;  X <= h(X);  X <= D |] ==> a : gfp(D,h)"
```
```   257 by (blast intro: gfp_upperbound [THEN subsetD])
```
```   258
```
```   259 lemma coinduct_lemma:
```
```   260     "[| X <= h(X Un gfp(D,h));  X <= D;  bnd_mono(D,h) |] ==>
```
```   261      X Un gfp(D,h) <= h(X Un gfp(D,h))"
```
```   262 apply (erule Un_least)
```
```   263 apply (rule gfp_lemma2 [THEN subset_trans], assumption)
```
```   264 apply (rule Un_upper2 [THEN subset_trans])
```
```   265 apply (rule bnd_mono_Un, assumption+)
```
```   266 apply (rule gfp_subset)
```
```   267 done
```
```   268
```
```   269 (*strong version*)
```
```   270 lemma coinduct:
```
```   271      "[| bnd_mono(D,h);  a: X;  X <= h(X Un gfp(D,h));  X <= D |]
```
```   272       ==> a : gfp(D,h)"
```
```   273 apply (rule weak_coinduct)
```
```   274 apply (erule_tac [2] coinduct_lemma)
```
```   275 apply (simp_all add: gfp_subset Un_subset_iff)
```
```   276 done
```
```   277
```
```   278 (*Definition form, to control unfolding*)
```
```   279 lemma def_coinduct:
```
```   280     "[| A == gfp(D,h);  bnd_mono(D,h);  a: X;  X <= h(X Un A);  X <= D |] ==>
```
```   281      a : A"
```
```   282 apply simp
```
```   283 apply (rule coinduct, assumption+)
```
```   284 done
```
```   285
```
```   286 (*The version used in the induction/coinduction package*)
```
```   287 lemma def_Collect_coinduct:
```
```   288     "[| A == gfp(D, %w. Collect(D,P(w)));  bnd_mono(D, %w. Collect(D,P(w)));
```
```   289         a: X;  X <= D;  !!z. z: X ==> P(X Un A, z) |] ==>
```
```   290      a : A"
```
```   291 apply (rule def_coinduct, assumption+, blast+)
```
```   292 done
```
```   293
```
```   294 (*Monotonicity of gfp!*)
```
```   295 lemma gfp_mono:
```
```   296     "[| bnd_mono(D,h);  D <= E;
```
```   297         !!X. X<=D ==> h(X) <= i(X)  |] ==> gfp(D,h) <= gfp(E,i)"
```
```   298 apply (rule gfp_upperbound)
```
```   299 apply (rule gfp_lemma2 [THEN subset_trans], assumption)
```
```   300 apply (blast del: subsetI intro: gfp_subset)
```
```   301 apply (blast del: subsetI intro: subset_trans gfp_subset)
```
```   302 done
```
```   303
```
```   304 ML
```
```   305 {*
```
```   306 val bnd_mono_def = thm "bnd_mono_def";
```
```   307 val lfp_def = thm "lfp_def";
```
```   308 val gfp_def = thm "gfp_def";
```
```   309
```
```   310 val bnd_monoI = thm "bnd_monoI";
```
```   311 val bnd_monoD1 = thm "bnd_monoD1";
```
```   312 val bnd_monoD2 = thm "bnd_monoD2";
```
```   313 val bnd_mono_subset = thm "bnd_mono_subset";
```
```   314 val bnd_mono_Un = thm "bnd_mono_Un";
```
```   315 val bnd_mono_Int = thm "bnd_mono_Int";
```
```   316 val lfp_lowerbound = thm "lfp_lowerbound";
```
```   317 val lfp_subset = thm "lfp_subset";
```
```   318 val def_lfp_subset = thm "def_lfp_subset";
```
```   319 val lfp_greatest = thm "lfp_greatest";
```
```   320 val lfp_unfold = thm "lfp_unfold";
```
```   321 val def_lfp_unfold = thm "def_lfp_unfold";
```
```   322 val Collect_is_pre_fixedpt = thm "Collect_is_pre_fixedpt";
```
```   323 val induct = thm "induct";
```
```   324 val def_induct = thm "def_induct";
```
```   325 val lfp_Int_lowerbound = thm "lfp_Int_lowerbound";
```
```   326 val lfp_mono = thm "lfp_mono";
```
```   327 val lfp_mono2 = thm "lfp_mono2";
```
```   328 val gfp_upperbound = thm "gfp_upperbound";
```
```   329 val gfp_subset = thm "gfp_subset";
```
```   330 val def_gfp_subset = thm "def_gfp_subset";
```
```   331 val gfp_least = thm "gfp_least";
```
```   332 val gfp_unfold = thm "gfp_unfold";
```
```   333 val def_gfp_unfold = thm "def_gfp_unfold";
```
```   334 val weak_coinduct = thm "weak_coinduct";
```
```   335 val coinduct = thm "coinduct";
```
```   336 val def_coinduct = thm "def_coinduct";
```
```   337 val def_Collect_coinduct = thm "def_Collect_coinduct";
```
```   338 val gfp_mono = thm "gfp_mono";
```
```   339 *}
```
```   340
```
```   341
```
```   342 end
```