src/HOL/Library/Order_Continuity.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (3 months ago) changeset 69946 494934c30f38 parent 69872 bb16c0bb7520 permissions -rw-r--r--
improved code equations taken over from AFP
```     1 (*  Title:      HOL/Library/Order_Continuity.thy
```
```     2     Author:     David von Oheimb, TU München
```
```     3     Author:     Johannes Hölzl, TU München
```
```     4 *)
```
```     5
```
```     6 section \<open>Continuity and iterations\<close>
```
```     7
```
```     8 theory Order_Continuity
```
```     9 imports Complex_Main Countable_Complete_Lattices
```
```    10 begin
```
```    11
```
```    12 (* TODO: Generalize theory to chain-complete partial orders *)
```
```    13
```
```    14 lemma SUP_nat_binary:
```
```    15   "(sup A (SUP x\<in>Collect ((<) (0::nat)). B)) = (sup A B::'a::countable_complete_lattice)"
```
```    16   apply (subst image_constant)
```
```    17    apply auto
```
```    18   done
```
```    19
```
```    20 lemma INF_nat_binary:
```
```    21   "inf A (INF x\<in>Collect ((<) (0::nat)). B) = (inf A B::'a::countable_complete_lattice)"
```
```    22   apply (subst image_constant)
```
```    23    apply auto
```
```    24   done
```
```    25
```
```    26 text \<open>
```
```    27   The name \<open>continuous\<close> is already taken in \<open>Complex_Main\<close>, so we use
```
```    28   \<open>sup_continuous\<close> and \<open>inf_continuous\<close>. These names appear sometimes in literature
```
```    29   and have the advantage that these names are duals.
```
```    30 \<close>
```
```    31
```
```    32 named_theorems order_continuous_intros
```
```    33
```
```    34 subsection \<open>Continuity for complete lattices\<close>
```
```    35
```
```    36 definition
```
```    37   sup_continuous :: "('a::countable_complete_lattice \<Rightarrow> 'b::countable_complete_lattice) \<Rightarrow> bool"
```
```    38 where
```
```    39   "sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
```
```    40
```
```    41 lemma sup_continuousD: "sup_continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
```
```    42   by (auto simp: sup_continuous_def)
```
```    43
```
```    44 lemma sup_continuous_mono:
```
```    45   "mono F" if "sup_continuous F"
```
```    46 proof
```
```    47   fix A B :: "'a"
```
```    48   assume "A \<le> B"
```
```    49   let ?f = "\<lambda>n::nat. if n = 0 then A else B"
```
```    50   from \<open>A \<le> B\<close> have "incseq ?f"
```
```    51     by (auto intro: monoI)
```
```    52   with \<open>sup_continuous F\<close> have *: "F (SUP i. ?f i) = (SUP i. F (?f i))"
```
```    53     by (auto dest: sup_continuousD)
```
```    54   from \<open>A \<le> B\<close> have "B = sup A B"
```
```    55     by (simp add: le_iff_sup)
```
```    56   then have "F B = F (sup A B)"
```
```    57     by simp
```
```    58   also have "\<dots> = sup (F A) (F B)"
```
```    59     using * by (simp add: if_distrib SUP_nat_binary cong del: SUP_cong)
```
```    60   finally show "F A \<le> F B"
```
```    61     by (simp add: le_iff_sup)
```
```    62 qed
```
```    63
```
```    64 lemma [order_continuous_intros]:
```
```    65   shows sup_continuous_const: "sup_continuous (\<lambda>x. c)"
```
```    66     and sup_continuous_id: "sup_continuous (\<lambda>x. x)"
```
```    67     and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)"
```
```    68     and sup_continuous_fun: "(\<And>s. sup_continuous (\<lambda>x. P x s)) \<Longrightarrow> sup_continuous P"
```
```    69     and sup_continuous_If: "sup_continuous F \<Longrightarrow> sup_continuous G \<Longrightarrow> sup_continuous (\<lambda>f. if C then F f else G f)"
```
```    70   by (auto simp: sup_continuous_def image_comp)
```
```    71
```
```    72 lemma sup_continuous_compose:
```
```    73   assumes f: "sup_continuous f" and g: "sup_continuous g"
```
```    74   shows "sup_continuous (\<lambda>x. f (g x))"
```
```    75   unfolding sup_continuous_def
```
```    76 proof safe
```
```    77   fix M :: "nat \<Rightarrow> 'c"
```
```    78   assume M: "mono M"
```
```    79   then have "mono (\<lambda>i. g (M i))"
```
```    80     using sup_continuous_mono[OF g] by (auto simp: mono_def)
```
```    81   with M show "f (g (Sup (M ` UNIV))) = (SUP i. f (g (M i)))"
```
```    82     by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
```
```    83 qed
```
```    84
```
```    85 lemma sup_continuous_sup[order_continuous_intros]:
```
```    86   "sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. sup (f x) (g x))"
```
```    87   by (simp add: sup_continuous_def ccSUP_sup_distrib)
```
```    88
```
```    89 lemma sup_continuous_inf[order_continuous_intros]:
```
```    90   fixes P Q :: "'a :: countable_complete_lattice \<Rightarrow> 'b :: countable_complete_distrib_lattice"
```
```    91   assumes P: "sup_continuous P" and Q: "sup_continuous Q"
```
```    92   shows "sup_continuous (\<lambda>x. inf (P x) (Q x))"
```
```    93   unfolding sup_continuous_def
```
```    94 proof (safe intro!: antisym)
```
```    95   fix M :: "nat \<Rightarrow> 'a" assume M: "incseq M"
```
```    96   have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP j i. inf (P (M i)) (Q (M j)))"
```
```    97     by (simp add: sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_ccSUP ccSUP_inf)
```
```    98   also have "\<dots> \<le> (SUP i. inf (P (M i)) (Q (M i)))"
```
```    99   proof (intro ccSUP_least)
```
```   100     fix i j from M assms[THEN sup_continuous_mono] show "inf (P (M i)) (Q (M j)) \<le> (SUP i. inf (P (M i)) (Q (M i)))"
```
```   101       by (intro ccSUP_upper2[of _ "sup i j"] inf_mono) (auto simp: mono_def)
```
```   102   qed auto
```
```   103   finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP i. inf (P (M i)) (Q (M i)))" .
```
```   104
```
```   105   show "(SUP i. inf (P (M i)) (Q (M i))) \<le> inf (P (SUP i. M i)) (Q (SUP i. M i))"
```
```   106     unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro ccSUP_least inf_mono ccSUP_upper) auto
```
```   107 qed
```
```   108
```
```   109 lemma sup_continuous_and[order_continuous_intros]:
```
```   110   "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<and> Q x)"
```
```   111   using sup_continuous_inf[of P Q] by simp
```
```   112
```
```   113 lemma sup_continuous_or[order_continuous_intros]:
```
```   114   "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<or> Q x)"
```
```   115   by (auto simp: sup_continuous_def)
```
```   116
```
```   117 lemma sup_continuous_lfp:
```
```   118   assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
```
```   119 proof (rule antisym)
```
```   120   note mono = sup_continuous_mono[OF \<open>sup_continuous F\<close>]
```
```   121   show "?U \<le> lfp F"
```
```   122   proof (rule SUP_least)
```
```   123     fix i show "(F ^^ i) bot \<le> lfp F"
```
```   124     proof (induct i)
```
```   125       case (Suc i)
```
```   126       have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
```
```   127       also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
```
```   128       also have "\<dots> = lfp F" by (simp add: lfp_fixpoint[OF mono])
```
```   129       finally show ?case .
```
```   130     qed simp
```
```   131   qed
```
```   132   show "lfp F \<le> ?U"
```
```   133   proof (rule lfp_lowerbound)
```
```   134     have "mono (\<lambda>i::nat. (F ^^ i) bot)"
```
```   135     proof -
```
```   136       { fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
```
```   137         proof (induct i)
```
```   138           case 0 show ?case by simp
```
```   139         next
```
```   140           case Suc thus ?case using monoD[OF mono Suc] by auto
```
```   141         qed }
```
```   142       thus ?thesis by (auto simp add: mono_iff_le_Suc)
```
```   143     qed
```
```   144     hence "F ?U = (SUP i. (F ^^ Suc i) bot)"
```
```   145       using \<open>sup_continuous F\<close> by (simp add: sup_continuous_def)
```
```   146     also have "\<dots> \<le> ?U"
```
```   147       by (fast intro: SUP_least SUP_upper)
```
```   148     finally show "F ?U \<le> ?U" .
```
```   149   qed
```
```   150 qed
```
```   151
```
```   152 lemma lfp_transfer_bounded:
```
```   153   assumes P: "P bot" "\<And>x. P x \<Longrightarrow> P (f x)" "\<And>M. (\<And>i. P (M i)) \<Longrightarrow> P (SUP i::nat. M i)"
```
```   154   assumes \<alpha>: "\<And>M. mono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (SUP i. M i) = (SUP i. \<alpha> (M i))"
```
```   155   assumes f: "sup_continuous f" and g: "sup_continuous g"
```
```   156   assumes [simp]: "\<And>x. P x \<Longrightarrow> x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
```
```   157   assumes g_bound: "\<And>x. \<alpha> bot \<le> g x"
```
```   158   shows "\<alpha> (lfp f) = lfp g"
```
```   159 proof (rule antisym)
```
```   160   note mono_g = sup_continuous_mono[OF g]
```
```   161   note mono_f = sup_continuous_mono[OF f]
```
```   162   have lfp_bound: "\<alpha> bot \<le> lfp g"
```
```   163     by (subst lfp_unfold[OF mono_g]) (rule g_bound)
```
```   164
```
```   165   have P_pow: "P ((f ^^ i) bot)" for i
```
```   166     by (induction i) (auto intro!: P)
```
```   167   have incseq_pow: "mono (\<lambda>i. (f ^^ i) bot)"
```
```   168     unfolding mono_iff_le_Suc
```
```   169   proof
```
```   170     fix i show "(f ^^ i) bot \<le> (f ^^ (Suc i)) bot"
```
```   171     proof (induct i)
```
```   172       case Suc thus ?case using monoD[OF sup_continuous_mono[OF f] Suc] by auto
```
```   173     qed (simp add: le_fun_def)
```
```   174   qed
```
```   175   have P_lfp: "P (lfp f)"
```
```   176     using P_pow unfolding sup_continuous_lfp[OF f] by (auto intro!: P)
```
```   177
```
```   178   have iter_le_lfp: "(f ^^ n) bot \<le> lfp f" for n
```
```   179     apply (induction n)
```
```   180     apply simp
```
```   181     apply (subst lfp_unfold[OF mono_f])
```
```   182     apply (auto intro!: monoD[OF mono_f])
```
```   183     done
```
```   184
```
```   185   have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
```
```   186     unfolding sup_continuous_lfp[OF f] using incseq_pow P_pow by (rule \<alpha>)
```
```   187   also have "\<dots> \<le> lfp g"
```
```   188   proof (rule SUP_least)
```
```   189     fix i show "\<alpha> ((f^^i) bot) \<le> lfp g"
```
```   190     proof (induction i)
```
```   191       case (Suc n) then show ?case
```
```   192         by (subst lfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow iter_le_lfp)
```
```   193     qed (simp add: lfp_bound)
```
```   194   qed
```
```   195   finally show "\<alpha> (lfp f) \<le> lfp g" .
```
```   196
```
```   197   show "lfp g \<le> \<alpha> (lfp f)"
```
```   198   proof (induction rule: lfp_ordinal_induct[OF mono_g])
```
```   199     case (1 S) then show ?case
```
```   200       by (subst lfp_unfold[OF sup_continuous_mono[OF f]])
```
```   201          (simp add: monoD[OF mono_g] P_lfp)
```
```   202   qed (auto intro: Sup_least)
```
```   203 qed
```
```   204
```
```   205 lemma lfp_transfer:
```
```   206   "sup_continuous \<alpha> \<Longrightarrow> sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow>
```
```   207     (\<And>x. \<alpha> bot \<le> g x) \<Longrightarrow> (\<And>x. x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)) \<Longrightarrow> \<alpha> (lfp f) = lfp g"
```
```   208   by (rule lfp_transfer_bounded[where P=top]) (auto dest: sup_continuousD)
```
```   209
```
```   210 definition
```
```   211   inf_continuous :: "('a::countable_complete_lattice \<Rightarrow> 'b::countable_complete_lattice) \<Rightarrow> bool"
```
```   212 where
```
```   213   "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
```
```   214
```
```   215 lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
```
```   216   by (auto simp: inf_continuous_def)
```
```   217
```
```   218 lemma inf_continuous_mono:
```
```   219   "mono F" if "inf_continuous F"
```
```   220 proof
```
```   221   fix A B :: "'a"
```
```   222   assume "A \<le> B"
```
```   223   let ?f = "\<lambda>n::nat. if n = 0 then B else A"
```
```   224   from \<open>A \<le> B\<close> have "decseq ?f"
```
```   225     by (auto intro: antimonoI)
```
```   226   with \<open>inf_continuous F\<close> have *: "F (INF i. ?f i) = (INF i. F (?f i))"
```
```   227     by (auto dest: inf_continuousD)
```
```   228   from \<open>A \<le> B\<close> have "A = inf B A"
```
```   229     by (simp add: inf.absorb_iff2)
```
```   230   then have "F A = F (inf B A)"
```
```   231     by simp
```
```   232   also have "\<dots> = inf (F B) (F A)"
```
```   233     using * by (simp add: if_distrib INF_nat_binary cong del: INF_cong)
```
```   234   finally show "F A \<le> F B"
```
```   235     by (simp add: inf.absorb_iff2)
```
```   236 qed
```
```   237
```
```   238 lemma [order_continuous_intros]:
```
```   239   shows inf_continuous_const: "inf_continuous (\<lambda>x. c)"
```
```   240     and inf_continuous_id: "inf_continuous (\<lambda>x. x)"
```
```   241     and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)"
```
```   242     and inf_continuous_fun: "(\<And>s. inf_continuous (\<lambda>x. P x s)) \<Longrightarrow> inf_continuous P"
```
```   243     and inf_continuous_If: "inf_continuous F \<Longrightarrow> inf_continuous G \<Longrightarrow> inf_continuous (\<lambda>f. if C then F f else G f)"
```
```   244   by (auto simp: inf_continuous_def image_comp)
```
```   245
```
```   246 lemma inf_continuous_inf[order_continuous_intros]:
```
```   247   "inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))"
```
```   248   by (simp add: inf_continuous_def ccINF_inf_distrib)
```
```   249
```
```   250 lemma inf_continuous_sup[order_continuous_intros]:
```
```   251   fixes P Q :: "'a :: countable_complete_lattice \<Rightarrow> 'b :: countable_complete_distrib_lattice"
```
```   252   assumes P: "inf_continuous P" and Q: "inf_continuous Q"
```
```   253   shows "inf_continuous (\<lambda>x. sup (P x) (Q x))"
```
```   254   unfolding inf_continuous_def
```
```   255 proof (safe intro!: antisym)
```
```   256   fix M :: "nat \<Rightarrow> 'a" assume M: "decseq M"
```
```   257   show "sup (P (INF i. M i)) (Q (INF i. M i)) \<le> (INF i. sup (P (M i)) (Q (M i)))"
```
```   258     unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro ccINF_greatest sup_mono ccINF_lower) auto
```
```   259
```
```   260   have "(INF i. sup (P (M i)) (Q (M i))) \<le> (INF j i. sup (P (M i)) (Q (M j)))"
```
```   261   proof (intro ccINF_greatest)
```
```   262     fix i j from M assms[THEN inf_continuous_mono] show "sup (P (M i)) (Q (M j)) \<ge> (INF i. sup (P (M i)) (Q (M i)))"
```
```   263       by (intro ccINF_lower2[of _ "sup i j"] sup_mono) (auto simp: mono_def antimono_def)
```
```   264   qed auto
```
```   265   also have "\<dots> \<le> sup (P (INF i. M i)) (Q (INF i. M i))"
```
```   266     by (simp add: inf_continuousD[OF P M] inf_continuousD[OF Q M] ccINF_sup sup_ccINF)
```
```   267   finally show "sup (P (INF i. M i)) (Q (INF i. M i)) \<ge> (INF i. sup (P (M i)) (Q (M i)))" .
```
```   268 qed
```
```   269
```
```   270 lemma inf_continuous_and[order_continuous_intros]:
```
```   271   "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<and> Q x)"
```
```   272   using inf_continuous_inf[of P Q] by simp
```
```   273
```
```   274 lemma inf_continuous_or[order_continuous_intros]:
```
```   275   "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<or> Q x)"
```
```   276   using inf_continuous_sup[of P Q] by simp
```
```   277
```
```   278 lemma inf_continuous_compose:
```
```   279   assumes f: "inf_continuous f" and g: "inf_continuous g"
```
```   280   shows "inf_continuous (\<lambda>x. f (g x))"
```
```   281   unfolding inf_continuous_def
```
```   282 proof safe
```
```   283   fix M :: "nat \<Rightarrow> 'c"
```
```   284   assume M: "antimono M"
```
```   285   then have "antimono (\<lambda>i. g (M i))"
```
```   286     using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
```
```   287   with M show "f (g (Inf (M ` UNIV))) = (INF i. f (g (M i)))"
```
```   288     by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
```
```   289 qed
```
```   290
```
```   291 lemma inf_continuous_gfp:
```
```   292   assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
```
```   293 proof (rule antisym)
```
```   294   note mono = inf_continuous_mono[OF \<open>inf_continuous F\<close>]
```
```   295   show "gfp F \<le> ?U"
```
```   296   proof (rule INF_greatest)
```
```   297     fix i show "gfp F \<le> (F ^^ i) top"
```
```   298     proof (induct i)
```
```   299       case (Suc i)
```
```   300       have "gfp F = F (gfp F)" by (simp add: gfp_fixpoint[OF mono])
```
```   301       also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
```
```   302       also have "\<dots> = (F ^^ Suc i) top" by simp
```
```   303       finally show ?case .
```
```   304     qed simp
```
```   305   qed
```
```   306   show "?U \<le> gfp F"
```
```   307   proof (rule gfp_upperbound)
```
```   308     have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
```
```   309     proof -
```
```   310       { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
```
```   311         proof (induct i)
```
```   312           case 0 show ?case by simp
```
```   313         next
```
```   314           case Suc thus ?case using monoD[OF mono Suc] by auto
```
```   315         qed }
```
```   316       thus ?thesis by (auto simp add: antimono_iff_le_Suc)
```
```   317     qed
```
```   318     have "?U \<le> (INF i. (F ^^ Suc i) top)"
```
```   319       by (fast intro: INF_greatest INF_lower)
```
```   320     also have "\<dots> \<le> F ?U"
```
```   321       by (simp add: inf_continuousD \<open>inf_continuous F\<close> *)
```
```   322     finally show "?U \<le> F ?U" .
```
```   323   qed
```
```   324 qed
```
```   325
```
```   326 lemma gfp_transfer:
```
```   327   assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g"
```
```   328   assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
```
```   329   shows "\<alpha> (gfp f) = gfp g"
```
```   330 proof -
```
```   331   have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))"
```
```   332     unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono)
```
```   333   moreover have "\<alpha> ((f^^i) top) = (g^^i) top" for i
```
```   334     by (induction i; simp)
```
```   335   ultimately show ?thesis
```
```   336     unfolding inf_continuous_gfp[OF g] by simp
```
```   337 qed
```
```   338
```
```   339 lemma gfp_transfer_bounded:
```
```   340   assumes P: "P (f top)" "\<And>x. P x \<Longrightarrow> P (f x)" "\<And>M. antimono M \<Longrightarrow> (\<And>i. P (M i)) \<Longrightarrow> P (INF i::nat. M i)"
```
```   341   assumes \<alpha>: "\<And>M. antimono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (INF i. M i) = (INF i. \<alpha> (M i))"
```
```   342   assumes f: "inf_continuous f" and g: "inf_continuous g"
```
```   343   assumes [simp]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
```
```   344   assumes g_bound: "\<And>x. g x \<le> \<alpha> (f top)"
```
```   345   shows "\<alpha> (gfp f) = gfp g"
```
```   346 proof (rule antisym)
```
```   347   note mono_g = inf_continuous_mono[OF g]
```
```   348
```
```   349   have P_pow: "P ((f ^^ i) (f top))" for i
```
```   350     by (induction i) (auto intro!: P)
```
```   351
```
```   352   have antimono_pow: "antimono (\<lambda>i. (f ^^ i) top)"
```
```   353     unfolding antimono_iff_le_Suc
```
```   354   proof
```
```   355     fix i show "(f ^^ Suc i) top \<le> (f ^^ i) top"
```
```   356     proof (induct i)
```
```   357       case Suc thus ?case using monoD[OF inf_continuous_mono[OF f] Suc] by auto
```
```   358     qed (simp add: le_fun_def)
```
```   359   qed
```
```   360   have antimono_pow2: "antimono (\<lambda>i. (f ^^ i) (f top))"
```
```   361   proof
```
```   362     show "x \<le> y \<Longrightarrow> (f ^^ y) (f top) \<le> (f ^^ x) (f top)" for x y
```
```   363       using antimono_pow[THEN antimonoD, of "Suc x" "Suc y"]
```
```   364       unfolding funpow_Suc_right by simp
```
```   365   qed
```
```   366
```
```   367   have gfp_f: "gfp f = (INF i. (f ^^ i) (f top))"
```
```   368     unfolding inf_continuous_gfp[OF f]
```
```   369   proof (rule INF_eq)
```
```   370     show "\<exists>j\<in>UNIV. (f ^^ j) (f top) \<le> (f ^^ i) top" for i
```
```   371       by (intro bexI[of _ "i - 1"]) (auto simp: diff_Suc funpow_Suc_right simp del: funpow.simps(2) split: nat.split)
```
```   372     show "\<exists>j\<in>UNIV. (f ^^ j) top \<le> (f ^^ i) (f top)" for i
```
```   373       by (intro bexI[of _ "Suc i"]) (auto simp: funpow_Suc_right simp del: funpow.simps(2))
```
```   374   qed
```
```   375
```
```   376   have P_lfp: "P (gfp f)"
```
```   377     unfolding gfp_f by (auto intro!: P P_pow antimono_pow2)
```
```   378
```
```   379   have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) (f top)))"
```
```   380     unfolding gfp_f by (rule \<alpha>) (auto intro!: P_pow antimono_pow2)
```
```   381   also have "\<dots> \<ge> gfp g"
```
```   382   proof (rule INF_greatest)
```
```   383     fix i show "gfp g \<le> \<alpha> ((f^^i) (f top))"
```
```   384     proof (induction i)
```
```   385       case (Suc n) then show ?case
```
```   386         by (subst gfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow)
```
```   387     next
```
```   388       case 0
```
```   389       have "gfp g \<le> \<alpha> (f top)"
```
```   390         by (subst gfp_unfold[OF mono_g]) (rule g_bound)
```
```   391       then show ?case
```
```   392         by simp
```
```   393     qed
```
```   394   qed
```
```   395   finally show "gfp g \<le> \<alpha> (gfp f)" .
```
```   396
```
```   397   show "\<alpha> (gfp f) \<le> gfp g"
```
```   398   proof (induction rule: gfp_ordinal_induct[OF mono_g])
```
```   399     case (1 S) then show ?case
```
```   400       by (subst gfp_unfold[OF inf_continuous_mono[OF f]])
```
```   401          (simp add: monoD[OF mono_g] P_lfp)
```
```   402   qed (auto intro: Inf_greatest)
```
```   403 qed
```
```   404
```
```   405 subsubsection \<open>Least fixed points in countable complete lattices\<close>
```
```   406
```
```   407 definition (in countable_complete_lattice) cclfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
```
```   408   where "cclfp f = (SUP i. (f ^^ i) bot)"
```
```   409
```
```   410 lemma cclfp_unfold:
```
```   411   assumes "sup_continuous F" shows "cclfp F = F (cclfp F)"
```
```   412 proof -
```
```   413   have "cclfp F = (SUP i. F ((F ^^ i) bot))"
```
```   414     unfolding cclfp_def
```
```   415     by (subst UNIV_nat_eq) (simp add: image_comp)
```
```   416   also have "\<dots> = F (cclfp F)"
```
```   417     unfolding cclfp_def
```
```   418     by (intro sup_continuousD[symmetric] assms mono_funpow sup_continuous_mono)
```
```   419   finally show ?thesis .
```
```   420 qed
```
```   421
```
```   422 lemma cclfp_lowerbound: assumes f: "mono f" and A: "f A \<le> A" shows "cclfp f \<le> A"
```
```   423   unfolding cclfp_def
```
```   424 proof (intro ccSUP_least)
```
```   425   fix i show "(f ^^ i) bot \<le> A"
```
```   426   proof (induction i)
```
```   427     case (Suc i) from monoD[OF f this] A show ?case
```
```   428       by auto
```
```   429   qed simp
```
```   430 qed simp
```
```   431
```
```   432 lemma cclfp_transfer:
```
```   433   assumes "sup_continuous \<alpha>" "mono f"
```
```   434   assumes "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
```
```   435   shows "\<alpha> (cclfp f) = cclfp g"
```
```   436 proof -
```
```   437   have "\<alpha> (cclfp f) = (SUP i. \<alpha> ((f ^^ i) bot))"
```
```   438     unfolding cclfp_def by (intro sup_continuousD assms mono_funpow sup_continuous_mono)
```
```   439   moreover have "\<alpha> ((f ^^ i) bot) = (g ^^ i) bot" for i
```
```   440     by (induction i) (simp_all add: assms)
```
```   441   ultimately show ?thesis
```
```   442     by (simp add: cclfp_def)
```
```   443 qed
```
```   444
```
```   445 end
```