src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
 author wenzelm Wed Mar 08 10:50:59 2017 +0100 (2017-03-08) changeset 65151 a7394aa4d21c parent 64911 f0e07600de47 child 67408 4a4c14b24800 permissions -rw-r--r--
tuned proofs;
```     1 (*  Title:      HOL/Library/Bourbaki_Witt_Fixpoint.thy
```
```     2     Author:     Andreas Lochbihler, ETH Zurich
```
```     3
```
```     4   Follows G. Smolka, S. SchÃ¤fer and C. Doczkal: Transfinite Constructions in
```
```     5   Classical Type Theory. ITP 2015
```
```     6 *)
```
```     7
```
```     8 section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
```
```     9
```
```    10 theory Bourbaki_Witt_Fixpoint
```
```    11   imports While_Combinator
```
```    12 begin
```
```    13
```
```    14 lemma ChainsI [intro?]:
```
```    15   "(\<And>a b. \<lbrakk> a \<in> Y; b \<in> Y \<rbrakk> \<Longrightarrow> (a, b) \<in> r \<or> (b, a) \<in> r) \<Longrightarrow> Y \<in> Chains r"
```
```    16 unfolding Chains_def by blast
```
```    17
```
```    18 lemma in_Chains_subset: "\<lbrakk> M \<in> Chains r; M' \<subseteq> M \<rbrakk> \<Longrightarrow> M' \<in> Chains r"
```
```    19 by(auto simp add: Chains_def)
```
```    20
```
```    21 lemma in_ChainsD: "\<lbrakk> M \<in> Chains r; x \<in> M; y \<in> M \<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r"
```
```    22 unfolding Chains_def by fast
```
```    23
```
```    24 lemma Chains_FieldD: "\<lbrakk> M \<in> Chains r; x \<in> M \<rbrakk> \<Longrightarrow> x \<in> Field r"
```
```    25 by(auto simp add: Chains_def intro: FieldI1 FieldI2)
```
```    26
```
```    27 lemma in_Chains_conv_chain: "M \<in> Chains r \<longleftrightarrow> Complete_Partial_Order.chain (\<lambda>x y. (x, y) \<in> r) M"
```
```    28 by(simp add: Chains_def chain_def)
```
```    29
```
```    30 lemma partial_order_on_trans:
```
```    31   "\<lbrakk> partial_order_on A r; (x, y) \<in> r; (y, z) \<in> r \<rbrakk> \<Longrightarrow> (x, z) \<in> r"
```
```    32 by(auto simp add: order_on_defs dest: transD)
```
```    33
```
```    34 locale bourbaki_witt_fixpoint =
```
```    35   fixes lub :: "'a set \<Rightarrow> 'a"
```
```    36   and leq :: "('a \<times> 'a) set"
```
```    37   and f :: "'a \<Rightarrow> 'a"
```
```    38   assumes po: "Partial_order leq"
```
```    39   and lub_least: "\<lbrakk> M \<in> Chains leq; M \<noteq> {}; \<And>x. x \<in> M \<Longrightarrow> (x, z) \<in> leq \<rbrakk> \<Longrightarrow> (lub M, z) \<in> leq"
```
```    40   and lub_upper: "\<lbrakk> M \<in> Chains leq; x \<in> M \<rbrakk> \<Longrightarrow> (x, lub M) \<in> leq"
```
```    41   and lub_in_Field: "\<lbrakk> M \<in> Chains leq; M \<noteq> {} \<rbrakk> \<Longrightarrow> lub M \<in> Field leq"
```
```    42   and increasing: "\<And>x. x \<in> Field leq \<Longrightarrow> (x, f x) \<in> leq"
```
```    43 begin
```
```    44
```
```    45 lemma leq_trans: "\<lbrakk> (x, y) \<in> leq; (y, z) \<in> leq \<rbrakk> \<Longrightarrow> (x, z) \<in> leq"
```
```    46 by(rule partial_order_on_trans[OF po])
```
```    47
```
```    48 lemma leq_refl: "x \<in> Field leq \<Longrightarrow> (x, x) \<in> leq"
```
```    49 using po by(simp add: order_on_defs refl_on_def)
```
```    50
```
```    51 lemma leq_antisym: "\<lbrakk> (x, y) \<in> leq; (y, x) \<in> leq \<rbrakk> \<Longrightarrow> x = y"
```
```    52 using po by(simp add: order_on_defs antisym_def)
```
```    53
```
```    54 inductive_set iterates_above :: "'a \<Rightarrow> 'a set"
```
```    55   for a
```
```    56 where
```
```    57   base: "a \<in> iterates_above a"
```
```    58 | step: "x \<in> iterates_above a \<Longrightarrow> f x \<in> iterates_above a"
```
```    59 | Sup: "\<lbrakk> M \<in> Chains leq; M \<noteq> {}; \<And>x. x \<in> M \<Longrightarrow> x \<in> iterates_above a \<rbrakk> \<Longrightarrow> lub M \<in> iterates_above a"
```
```    60
```
```    61 definition fixp_above :: "'a \<Rightarrow> 'a"
```
```    62 where "fixp_above a = (if a \<in> Field leq then lub (iterates_above a) else a)"
```
```    63
```
```    64 lemma fixp_above_outside: "a \<notin> Field leq \<Longrightarrow> fixp_above a = a"
```
```    65 by(simp add: fixp_above_def)
```
```    66
```
```    67 lemma fixp_above_inside: "a \<in> Field leq \<Longrightarrow> fixp_above a = lub (iterates_above a)"
```
```    68 by(simp add: fixp_above_def)
```
```    69
```
```    70 context
```
```    71   notes leq_refl [intro!, simp]
```
```    72   and base [intro]
```
```    73   and step [intro]
```
```    74   and Sup [intro]
```
```    75   and leq_trans [trans]
```
```    76 begin
```
```    77
```
```    78 lemma iterates_above_le_f: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> (x, f x) \<in> leq"
```
```    79 by(induction x rule: iterates_above.induct)(blast intro: increasing FieldI2 lub_in_Field)+
```
```    80
```
```    81 lemma iterates_above_Field: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> x \<in> Field leq"
```
```    82 by(drule (1) iterates_above_le_f)(rule FieldI1)
```
```    83
```
```    84 lemma iterates_above_ge:
```
```    85   assumes y: "y \<in> iterates_above a"
```
```    86   and a: "a \<in> Field leq"
```
```    87   shows "(a, y) \<in> leq"
```
```    88 using y by(induction)(auto intro: a increasing iterates_above_le_f leq_trans leq_trans[OF _ lub_upper])
```
```    89
```
```    90 lemma iterates_above_lub:
```
```    91   assumes M: "M \<in> Chains leq"
```
```    92   and nempty: "M \<noteq> {}"
```
```    93   and upper: "\<And>y. y \<in> M \<Longrightarrow> \<exists>z \<in> M. (y, z) \<in> leq \<and> z \<in> iterates_above a"
```
```    94   shows "lub M \<in> iterates_above a"
```
```    95 proof -
```
```    96   let ?M = "M \<inter> iterates_above a"
```
```    97   from M have M': "?M \<in> Chains leq" by(rule in_Chains_subset)simp
```
```    98   have "?M \<noteq> {}" using nempty by(auto dest: upper)
```
```    99   with M' have "lub ?M \<in> iterates_above a" by(rule Sup) blast
```
```   100   also have "lub ?M = lub M" using nempty
```
```   101     by(intro leq_antisym)(blast intro!: lub_least[OF M] lub_least[OF M'] intro: lub_upper[OF M'] lub_upper[OF M] leq_trans dest: upper)+
```
```   102   finally show ?thesis .
```
```   103 qed
```
```   104
```
```   105 lemma iterates_above_successor:
```
```   106   assumes y: "y \<in> iterates_above a"
```
```   107   and a: "a \<in> Field leq"
```
```   108   shows "y = a \<or> y \<in> iterates_above (f a)"
```
```   109 using y
```
```   110 proof induction
```
```   111   case base thus ?case by simp
```
```   112 next
```
```   113   case (step x) thus ?case by auto
```
```   114 next
```
```   115   case (Sup M)
```
```   116   show ?case
```
```   117   proof(cases "\<exists>x. M \<subseteq> {x}")
```
```   118     case True
```
```   119     with \<open>M \<noteq> {}\<close> obtain y where M: "M = {y}" by auto
```
```   120     have "lub M = y"
```
```   121       by(rule leq_antisym)(auto intro!: lub_upper Sup lub_least ChainsI simp add: a M Sup.hyps(3)[of y, THEN iterates_above_Field] dest: iterates_above_Field)
```
```   122     with Sup.IH[of y] M show ?thesis by simp
```
```   123   next
```
```   124     case False
```
```   125     from Sup(1-2) have "lub M \<in> iterates_above (f a)"
```
```   126     proof(rule iterates_above_lub)
```
```   127       fix y
```
```   128       assume y: "y \<in> M"
```
```   129       from Sup.IH[OF this] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (f a)"
```
```   130       proof
```
```   131         assume "y = a"
```
```   132         from y False obtain z where z: "z \<in> M" and neq: "y \<noteq> z" by (metis insertI1 subsetI)
```
```   133         with Sup.IH[OF z] \<open>y = a\<close> Sup.hyps(3)[OF z]
```
```   134         show ?thesis by(auto dest: iterates_above_ge intro: a)
```
```   135       next
```
```   136         assume *: "y \<in> iterates_above (f a)"
```
```   137         with increasing[OF a] have "y \<in> Field leq"
```
```   138           by(auto dest!: iterates_above_Field intro: FieldI2)
```
```   139         with * show ?thesis using y by auto
```
```   140       qed
```
```   141     qed
```
```   142     thus ?thesis by simp
```
```   143   qed
```
```   144 qed
```
```   145
```
```   146 lemma iterates_above_Sup_aux:
```
```   147   assumes M: "M \<in> Chains leq" "M \<noteq> {}"
```
```   148   and M': "M' \<in> Chains leq" "M' \<noteq> {}"
```
```   149   and comp: "\<And>x. x \<in> M \<Longrightarrow> x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x"
```
```   150   shows "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')"
```
```   151 proof(cases "\<exists>x \<in> M. x \<in> iterates_above (lub M')")
```
```   152   case True
```
```   153   then obtain x where x: "x \<in> M" "x \<in> iterates_above (lub M')" by blast
```
```   154   have lub_M': "lub M' \<in> Field leq" using M' by(rule lub_in_Field)
```
```   155   have "lub M \<in> iterates_above (lub M')" using M
```
```   156   proof(rule iterates_above_lub)
```
```   157     fix y
```
```   158     assume y: "y \<in> M"
```
```   159     from comp[OF y] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (lub M')"
```
```   160     proof
```
```   161       assume "y \<in> iterates_above (lub M')"
```
```   162       from this iterates_above_Field[OF this] y lub_M' show ?thesis by blast
```
```   163     next
```
```   164       assume "lub M' \<in> iterates_above y"
```
```   165       hence "(y, lub M') \<in> leq" using Chains_FieldD[OF M(1) y] by(rule iterates_above_ge)
```
```   166       also have "(lub M', x) \<in> leq" using x(2) lub_M' by(rule iterates_above_ge)
```
```   167       finally show ?thesis using x by blast
```
```   168     qed
```
```   169   qed
```
```   170   thus ?thesis ..
```
```   171 next
```
```   172   case False
```
```   173   have "(lub M, lub M') \<in> leq" using M
```
```   174   proof(rule lub_least)
```
```   175     fix x
```
```   176     assume x: "x \<in> M"
```
```   177     from comp[OF x] x False have "lub M' \<in> iterates_above x" by auto
```
```   178     moreover from M(1) x have "x \<in> Field leq" by(rule Chains_FieldD)
```
```   179     ultimately show "(x, lub M') \<in> leq" by(rule iterates_above_ge)
```
```   180   qed
```
```   181   thus ?thesis ..
```
```   182 qed
```
```   183
```
```   184 lemma iterates_above_triangle:
```
```   185   assumes x: "x \<in> iterates_above a"
```
```   186   and y: "y \<in> iterates_above a"
```
```   187   and a: "a \<in> Field leq"
```
```   188   shows "x \<in> iterates_above y \<or> y \<in> iterates_above x"
```
```   189 using x y
```
```   190 proof(induction arbitrary: y)
```
```   191   case base then show ?case by simp
```
```   192 next
```
```   193   case (step x) thus ?case using a
```
```   194     by(auto dest: iterates_above_successor intro: iterates_above_Field)
```
```   195 next
```
```   196   case x: (Sup M)
```
```   197   hence lub: "lub M \<in> iterates_above a" by blast
```
```   198   from \<open>y \<in> iterates_above a\<close> show ?case
```
```   199   proof(induction)
```
```   200     case base show ?case using lub by simp
```
```   201   next
```
```   202     case (step y) thus ?case using a
```
```   203       by(auto dest: iterates_above_successor intro: iterates_above_Field)
```
```   204   next
```
```   205     case y: (Sup M')
```
```   206     hence lub': "lub M' \<in> iterates_above a" by blast
```
```   207     have *: "x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x" if "x \<in> M" for x
```
```   208       using that lub' by(rule x.IH)
```
```   209     with x(1-2) y(1-2) have "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')"
```
```   210       by(rule iterates_above_Sup_aux)
```
```   211     moreover from y(1-2) x(1-2) have "(lub M', lub M) \<in> leq \<or> lub M' \<in> iterates_above (lub M)"
```
```   212       by(rule iterates_above_Sup_aux)(blast dest: y.IH)
```
```   213     ultimately show ?case by(auto 4 3 dest: leq_antisym)
```
```   214   qed
```
```   215 qed
```
```   216
```
```   217 lemma chain_iterates_above:
```
```   218   assumes a: "a \<in> Field leq"
```
```   219   shows "iterates_above a \<in> Chains leq" (is "?C \<in> _")
```
```   220 proof (rule ChainsI)
```
```   221   fix x y
```
```   222   assume "x \<in> ?C" "y \<in> ?C"
```
```   223   hence "x \<in> iterates_above y \<or> y \<in> iterates_above x" using a by(rule iterates_above_triangle)
```
```   224   moreover from \<open>x \<in> ?C\<close> a have "x \<in> Field leq" by(rule iterates_above_Field)
```
```   225   moreover from \<open>y \<in> ?C\<close> a have "y \<in> Field leq" by(rule iterates_above_Field)
```
```   226   ultimately show "(x, y) \<in> leq \<or> (y, x) \<in> leq" by(auto dest: iterates_above_ge)
```
```   227 qed
```
```   228
```
```   229 lemma fixp_iterates_above: "fixp_above a \<in> iterates_above a"
```
```   230 by(auto intro: chain_iterates_above simp add: fixp_above_def)
```
```   231
```
```   232 lemma fixp_above_Field: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> Field leq"
```
```   233 using fixp_iterates_above by(rule iterates_above_Field)
```
```   234
```
```   235 lemma fixp_above_unfold:
```
```   236   assumes a: "a \<in> Field leq"
```
```   237   shows "fixp_above a = f (fixp_above a)" (is "?a = f ?a")
```
```   238 proof(rule leq_antisym)
```
```   239   show "(?a, f ?a) \<in> leq" using fixp_above_Field[OF a] by(rule increasing)
```
```   240
```
```   241   have "f ?a \<in> iterates_above a" using fixp_iterates_above by(rule iterates_above.step)
```
```   242   with chain_iterates_above[OF a] show "(f ?a, ?a) \<in> leq"
```
```   243     by(simp add: fixp_above_inside assms lub_upper)
```
```   244 qed
```
```   245
```
```   246 end
```
```   247
```
```   248 lemma fixp_above_induct [case_names adm base step]:
```
```   249   assumes adm: "ccpo.admissible lub (\<lambda>x y. (x, y) \<in> leq) P"
```
```   250   and base: "P a"
```
```   251   and step: "\<And>x. P x \<Longrightarrow> P (f x)"
```
```   252   shows "P (fixp_above a)"
```
```   253 proof(cases "a \<in> Field leq")
```
```   254   case True
```
```   255   from adm chain_iterates_above[OF True]
```
```   256   show ?thesis unfolding fixp_above_inside[OF True] in_Chains_conv_chain
```
```   257   proof(rule ccpo.admissibleD)
```
```   258     have "a \<in> iterates_above a" ..
```
```   259     then show "iterates_above a \<noteq> {}" by(auto)
```
```   260     show "P x" if "x \<in> iterates_above a" for x using that
```
```   261       by induction(auto intro: base step simp add: in_Chains_conv_chain dest: ccpo.admissibleD[OF adm])
```
```   262   qed
```
```   263 qed(simp add: fixp_above_outside base)
```
```   264
```
```   265 end
```
```   266
```
```   267 subsection \<open>Connect with the while combinator for executability on chain-finite lattices.\<close>
```
```   268
```
```   269 context bourbaki_witt_fixpoint begin
```
```   270
```
```   271 lemma in_Chains_finite: \<comment> \<open>Translation from @{thm in_chain_finite}.\<close>
```
```   272   assumes "M \<in> Chains leq"
```
```   273   and "M \<noteq> {}"
```
```   274   and "finite M"
```
```   275   shows "lub M \<in> M"
```
```   276 using assms(3,1,2)
```
```   277 proof induction
```
```   278   case empty thus ?case by simp
```
```   279 next
```
```   280   case (insert x M)
```
```   281   note chain = \<open>insert x M \<in> Chains leq\<close>
```
```   282   show ?case
```
```   283   proof(cases "M = {}")
```
```   284     case True thus ?thesis
```
```   285       using chain in_ChainsD leq_antisym lub_least lub_upper by fastforce
```
```   286   next
```
```   287     case False
```
```   288     from chain have chain': "M \<in> Chains leq"
```
```   289       using in_Chains_subset subset_insertI by blast
```
```   290     hence "lub M \<in> M" using False by(rule insert.IH)
```
```   291     show ?thesis
```
```   292     proof(cases "(x, lub M) \<in> leq")
```
```   293       case True
```
```   294       have "(lub (insert x M), lub M) \<in> leq" using chain
```
```   295         by (rule lub_least) (auto simp: True intro: lub_upper[OF chain'])
```
```   296       with False have "lub (insert x M) = lub M"
```
```   297         using lub_upper[OF chain] lub_least[OF chain'] by (blast intro: leq_antisym)
```
```   298       with \<open>lub M \<in> M\<close> show ?thesis by simp
```
```   299     next
```
```   300       case False
```
```   301       with in_ChainsD[OF chain, of x "lub M"] \<open>lub M \<in> M\<close>
```
```   302       have "lub (insert x M) = x"
```
```   303         by - (rule leq_antisym, (blast intro: FieldI2 chain chain' insert.prems(2) leq_refl leq_trans lub_least lub_upper)+)
```
```   304       thus ?thesis by simp
```
```   305     qed
```
```   306   qed
```
```   307 qed
```
```   308
```
```   309 lemma fun_pow_iterates_above: "(f ^^ k) a \<in> iterates_above a"
```
```   310 using iterates_above.base iterates_above.step by (induct k) simp_all
```
```   311
```
```   312 lemma chfin_iterates_above_fun_pow:
```
```   313   assumes "x \<in> iterates_above a"
```
```   314   assumes "\<forall>M \<in> Chains leq. finite M"
```
```   315   shows "\<exists>j. x = (f ^^ j) a"
```
```   316 using assms(1)
```
```   317 proof induct
```
```   318   case base then show ?case by (simp add: exI[where x=0])
```
```   319 next
```
```   320   case (step x) then obtain j where "x = (f ^^ j) a" by blast
```
```   321   with step(1) show ?case by (simp add: exI[where x="Suc j"])
```
```   322 next
```
```   323   case (Sup M) with in_Chains_finite assms(2) show ?case by blast
```
```   324 qed
```
```   325
```
```   326 lemma Chain_finite_iterates_above_fun_pow_iff:
```
```   327   assumes "\<forall>M \<in> Chains leq. finite M"
```
```   328   shows "x \<in> iterates_above a \<longleftrightarrow> (\<exists>j. x = (f ^^ j) a)"
```
```   329 using chfin_iterates_above_fun_pow fun_pow_iterates_above assms by blast
```
```   330
```
```   331 lemma fixp_above_Kleene_iter_ex:
```
```   332   assumes "(\<forall>M \<in> Chains leq. finite M)"
```
```   333   obtains k where "fixp_above a = (f ^^ k) a"
```
```   334 using assms by atomize_elim (simp add: chfin_iterates_above_fun_pow fixp_iterates_above)
```
```   335
```
```   336 context fixes a assumes a: "a \<in> Field leq" begin
```
```   337
```
```   338 lemma funpow_Field_leq: "(f ^^ k) a \<in> Field leq"
```
```   339 using a by (induct k) (auto intro: increasing FieldI2)
```
```   340
```
```   341 lemma funpow_prefix: "j < k \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq"
```
```   342 proof(induct k)
```
```   343   case (Suc k)
```
```   344   with leq_trans[OF _ increasing[OF funpow_Field_leq]] funpow_Field_leq increasing a
```
```   345   show ?case by simp (metis less_antisym)
```
```   346 qed simp
```
```   347
```
```   348 lemma funpow_suffix: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ (j + k)) a, (f ^^ k) a) \<in> leq"
```
```   349 using funpow_Field_leq
```
```   350 by (induct j) (simp_all del: funpow.simps add: funpow_Suc_right funpow_add leq_refl)
```
```   351
```
```   352 lemma funpow_stability: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq"
```
```   353 using funpow_prefix funpow_suffix[where j="j - k" and k=k] by (cases "j < k") simp_all
```
```   354
```
```   355 lemma funpow_in_Chains: "{(f ^^ k) a |k. True} \<in> Chains leq"
```
```   356 using chain_iterates_above[OF a] fun_pow_iterates_above
```
```   357 by (blast intro: ChainsI dest: in_ChainsD)
```
```   358
```
```   359 lemma fixp_above_Kleene_iter:
```
```   360   assumes "\<forall>M \<in> Chains leq. finite M" (* convenient but surely not necessary *)
```
```   361   assumes "(f ^^ Suc k) a = (f ^^ k) a"
```
```   362   shows "fixp_above a = (f ^^ k) a"
```
```   363 proof(rule leq_antisym)
```
```   364   show "(fixp_above a, (f ^^ k) a) \<in> leq" using assms a
```
```   365     by(auto simp add: fixp_above_def chain_iterates_above Chain_finite_iterates_above_fun_pow_iff funpow_stability[OF assms(2)] intro!: lub_least intro: iterates_above.base)
```
```   366   show "((f ^^ k) a, fixp_above a) \<in> leq" using a
```
```   367     by(auto simp add: fixp_above_def chain_iterates_above fun_pow_iterates_above intro!: lub_upper)
```
```   368 qed
```
```   369
```
```   370 context assumes chfin: "\<forall>M \<in> Chains leq. finite M" begin
```
```   371
```
```   372 lemma Chain_finite_wf: "wf {(f ((f ^^ k) a), (f ^^ k) a) |k. f ((f ^^ k) a) \<noteq> (f ^^ k) a}"
```
```   373 apply(rule wf_measure[where f="\<lambda>b. card {(f ^^ j) a |j. (b, (f ^^ j) a) \<in> leq}", THEN wf_subset])
```
```   374 apply(auto simp: set_eq_iff intro!: psubset_card_mono[OF finite_subset[OF _ bspec[OF chfin funpow_in_Chains]]])
```
```   375 apply(metis funpow_Field_leq increasing leq_antisym leq_trans leq_refl)+
```
```   376 done
```
```   377
```
```   378 lemma while_option_finite_increasing: "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f a = Some P"
```
```   379 by(rule wf_rel_while_option_Some[OF Chain_finite_wf, where P="\<lambda>A. (\<exists>k. A = (f ^^ k) a) \<and> (A, f A) \<in> leq" and s="a"])
```
```   380   (auto simp: a increasing chfin FieldI2 chfin_iterates_above_fun_pow fun_pow_iterates_above iterates_above.step intro: exI[where x=0])
```
```   381
```
```   382 lemma fixp_above_the_while_option: "fixp_above a = the (while_option (\<lambda>A. f A \<noteq> A) f a)"
```
```   383 proof -
```
```   384   obtain P where "while_option (\<lambda>A. f A \<noteq> A) f a = Some P"
```
```   385     using while_option_finite_increasing by blast
```
```   386   with while_option_stop2[OF this] fixp_above_Kleene_iter[OF chfin]
```
```   387   show ?thesis by fastforce
```
```   388 qed
```
```   389
```
```   390 lemma fixp_above_conv_while: "fixp_above a = while (\<lambda>A. f A \<noteq> A) f a"
```
```   391 unfolding while_def by (rule fixp_above_the_while_option)
```
```   392
```
```   393 end
```
```   394
```
```   395 end
```
```   396
```
```   397 end
```
```   398
```
```   399 lemma bourbaki_witt_fixpoint_complete_latticeI:
```
```   400   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
```
```   401   assumes "\<And>x. x \<le> f x"
```
```   402   shows "bourbaki_witt_fixpoint Sup {(x, y). x \<le> y} f"
```
```   403 by unfold_locales (auto simp: assms Sup_upper order_on_defs Field_def intro: refl_onI transI antisymI Sup_least)
```
```   404
```
```   405 end
```