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