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