(* Title: HOL/Library/Order_Continuity.thy Author: David von Oheimb, TU München Author: Johannes Hölzl, TU München *) section ‹Continuity and iterations› theory Order_Continuity imports Complex_Main Countable_Complete_Lattices begin (* TODO: Generalize theory to chain-complete partial orders *) lemma SUP_nat_binary: "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::countable_complete_lattice)" apply (auto intro!: antisym ccSUP_least) apply (rule ccSUP_upper2[where i=0]) apply simp_all apply (rule ccSUP_upper2[where i=1]) apply simp_all done lemma INF_nat_binary: "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::countable_complete_lattice)" apply (auto intro!: antisym ccINF_greatest) apply (rule ccINF_lower2[where i=0]) apply simp_all apply (rule ccINF_lower2[where i=1]) apply simp_all done text ‹ The name ‹continuous› is already taken in ‹Complex_Main›, so we use ‹sup_continuous› and ‹inf_continuous›. These names appear sometimes in literature and have the advantage that these names are duals. › named_theorems order_continuous_intros subsection ‹Continuity for complete lattices› definition sup_continuous :: "('a::countable_complete_lattice ⇒ 'b::countable_complete_lattice) ⇒ bool" where "sup_continuous F ⟷ (∀M::nat ⇒ 'a. mono M ⟶ F (SUP i. M i) = (SUP i. F (M i)))" lemma sup_continuousD: "sup_continuous F ⟹ mono M ⟹ F (SUP i::nat. M i) = (SUP i. F (M i))" by (auto simp: sup_continuous_def) lemma sup_continuous_mono: assumes [simp]: "sup_continuous F" shows "mono F" proof fix A B :: "'a" assume [simp]: "A ≤ B" have "F B = F (SUP n::nat. if n = 0 then A else B)" by (simp add: sup_absorb2 SUP_nat_binary) also have "… = (SUP n::nat. if n = 0 then F A else F B)" by (auto simp: sup_continuousD mono_def intro!: SUP_cong) finally show "F A ≤ F B" by (simp add: SUP_nat_binary le_iff_sup) qed lemma [order_continuous_intros]: shows sup_continuous_const: "sup_continuous (λx. c)" and sup_continuous_id: "sup_continuous (λx. x)" and sup_continuous_apply: "sup_continuous (λf. f x)" and sup_continuous_fun: "(⋀s. sup_continuous (λx. P x s)) ⟹ sup_continuous P" and sup_continuous_If: "sup_continuous F ⟹ sup_continuous G ⟹ sup_continuous (λf. if C then F f else G f)" by (auto simp: sup_continuous_def) lemma sup_continuous_compose: assumes f: "sup_continuous f" and g: "sup_continuous g" shows "sup_continuous (λx. f (g x))" unfolding sup_continuous_def proof safe fix M :: "nat ⇒ 'c" assume M: "mono M" then have "mono (λi. g (M i))" using sup_continuous_mono[OF g] by (auto simp: mono_def) with M show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))" by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD]) qed lemma sup_continuous_sup[order_continuous_intros]: "sup_continuous f ⟹ sup_continuous g ⟹ sup_continuous (λx. sup (f x) (g x))" by (simp add: sup_continuous_def ccSUP_sup_distrib) lemma sup_continuous_inf[order_continuous_intros]: fixes P Q :: "'a :: countable_complete_lattice ⇒ 'b :: countable_complete_distrib_lattice" assumes P: "sup_continuous P" and Q: "sup_continuous Q" shows "sup_continuous (λx. inf (P x) (Q x))" unfolding sup_continuous_def proof (safe intro!: antisym) fix M :: "nat ⇒ 'a" assume M: "incseq M" have "inf (P (SUP i. M i)) (Q (SUP i. M i)) ≤ (SUP j i. inf (P (M i)) (Q (M j)))" by (simp add: sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_ccSUP ccSUP_inf) also have "… ≤ (SUP i. inf (P (M i)) (Q (M i)))" proof (intro ccSUP_least) fix i j from M assms[THEN sup_continuous_mono] show "inf (P (M i)) (Q (M j)) ≤ (SUP i. inf (P (M i)) (Q (M i)))" by (intro ccSUP_upper2[of _ "sup i j"] inf_mono) (auto simp: mono_def) qed auto finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) ≤ (SUP i. inf (P (M i)) (Q (M i)))" . show "(SUP i. inf (P (M i)) (Q (M i))) ≤ inf (P (SUP i. M i)) (Q (SUP i. M i))" unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro ccSUP_least inf_mono ccSUP_upper) auto qed lemma sup_continuous_and[order_continuous_intros]: "sup_continuous P ⟹ sup_continuous Q ⟹ sup_continuous (λx. P x ∧ Q x)" using sup_continuous_inf[of P Q] by simp lemma sup_continuous_or[order_continuous_intros]: "sup_continuous P ⟹ sup_continuous Q ⟹ sup_continuous (λx. P x ∨ Q x)" by (auto simp: sup_continuous_def) lemma sup_continuous_lfp: assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U") proof (rule antisym) note mono = sup_continuous_mono[OF ‹sup_continuous F›] show "?U ≤ lfp F" proof (rule SUP_least) fix i show "(F ^^ i) bot ≤ lfp F" proof (induct i) case (Suc i) have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp also have "… ≤ F (lfp F)" by (rule monoD[OF mono Suc]) also have "… = lfp F" by (simp add: lfp_fixpoint[OF mono]) finally show ?case . qed simp qed show "lfp F ≤ ?U" proof (rule lfp_lowerbound) have "mono (λi::nat. (F ^^ i) bot)" proof - { fix i::nat have "(F ^^ i) bot ≤ (F ^^ (Suc i)) bot" proof (induct i) case 0 show ?case by simp next case Suc thus ?case using monoD[OF mono Suc] by auto qed } thus ?thesis by (auto simp add: mono_iff_le_Suc) qed hence "F ?U = (SUP i. (F ^^ Suc i) bot)" using ‹sup_continuous F› by (simp add: sup_continuous_def) also have "… ≤ ?U" by (fast intro: SUP_least SUP_upper) finally show "F ?U ≤ ?U" . qed qed lemma lfp_transfer_bounded: assumes P: "P bot" "⋀x. P x ⟹ P (f x)" "⋀M. (⋀i. P (M i)) ⟹ P (SUP i::nat. M i)" assumes α: "⋀M. mono M ⟹ (⋀i::nat. P (M i)) ⟹ α (SUP i. M i) = (SUP i. α (M i))" assumes f: "sup_continuous f" and g: "sup_continuous g" assumes [simp]: "⋀x. P x ⟹ x ≤ lfp f ⟹ α (f x) = g (α x)" assumes g_bound: "⋀x. α bot ≤ g x" shows "α (lfp f) = lfp g" proof (rule antisym) note mono_g = sup_continuous_mono[OF g] note mono_f = sup_continuous_mono[OF f] have lfp_bound: "α bot ≤ lfp g" by (subst lfp_unfold[OF mono_g]) (rule g_bound) have P_pow: "P ((f ^^ i) bot)" for i by (induction i) (auto intro!: P) have incseq_pow: "mono (λi. (f ^^ i) bot)" unfolding mono_iff_le_Suc proof fix i show "(f ^^ i) bot ≤ (f ^^ (Suc i)) bot" proof (induct i) case Suc thus ?case using monoD[OF sup_continuous_mono[OF f] Suc] by auto qed (simp add: le_fun_def) qed have P_lfp: "P (lfp f)" using P_pow unfolding sup_continuous_lfp[OF f] by (auto intro!: P) have iter_le_lfp: "(f ^^ n) bot ≤ lfp f" for n apply (induction n) apply simp apply (subst lfp_unfold[OF mono_f]) apply (auto intro!: monoD[OF mono_f]) done have "α (lfp f) = (SUP i. α ((f^^i) bot))" unfolding sup_continuous_lfp[OF f] using incseq_pow P_pow by (rule α) also have "… ≤ lfp g" proof (rule SUP_least) fix i show "α ((f^^i) bot) ≤ lfp g" proof (induction i) case (Suc n) then show ?case by (subst lfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow iter_le_lfp) qed (simp add: lfp_bound) qed finally show "α (lfp f) ≤ lfp g" . show "lfp g ≤ α (lfp f)" proof (induction rule: lfp_ordinal_induct[OF mono_g]) case (1 S) then show ?case by (subst lfp_unfold[OF sup_continuous_mono[OF f]]) (simp add: monoD[OF mono_g] P_lfp) qed (auto intro: Sup_least) qed lemma lfp_transfer: "sup_continuous α ⟹ sup_continuous f ⟹ sup_continuous g ⟹ (⋀x. α bot ≤ g x) ⟹ (⋀x. x ≤ lfp f ⟹ α (f x) = g (α x)) ⟹ α (lfp f) = lfp g" by (rule lfp_transfer_bounded[where P=top]) (auto dest: sup_continuousD) definition inf_continuous :: "('a::countable_complete_lattice ⇒ 'b::countable_complete_lattice) ⇒ bool" where "inf_continuous F ⟷ (∀M::nat ⇒ 'a. antimono M ⟶ F (INF i. M i) = (INF i. F (M i)))" lemma inf_continuousD: "inf_continuous F ⟹ antimono M ⟹ F (INF i::nat. M i) = (INF i. F (M i))" by (auto simp: inf_continuous_def) lemma inf_continuous_mono: assumes [simp]: "inf_continuous F" shows "mono F" proof fix A B :: "'a" assume [simp]: "A ≤ B" have "F A = F (INF n::nat. if n = 0 then B else A)" by (simp add: inf_absorb2 INF_nat_binary) also have "… = (INF n::nat. if n = 0 then F B else F A)" by (auto simp: inf_continuousD antimono_def intro!: INF_cong) finally show "F A ≤ F B" by (simp add: INF_nat_binary le_iff_inf inf_commute) qed lemma [order_continuous_intros]: shows inf_continuous_const: "inf_continuous (λx. c)" and inf_continuous_id: "inf_continuous (λx. x)" and inf_continuous_apply: "inf_continuous (λf. f x)" and inf_continuous_fun: "(⋀s. inf_continuous (λx. P x s)) ⟹ inf_continuous P" and inf_continuous_If: "inf_continuous F ⟹ inf_continuous G ⟹ inf_continuous (λf. if C then F f else G f)" by (auto simp: inf_continuous_def) lemma inf_continuous_inf[order_continuous_intros]: "inf_continuous f ⟹ inf_continuous g ⟹ inf_continuous (λx. inf (f x) (g x))" by (simp add: inf_continuous_def ccINF_inf_distrib) lemma inf_continuous_sup[order_continuous_intros]: fixes P Q :: "'a :: countable_complete_lattice ⇒ 'b :: countable_complete_distrib_lattice" assumes P: "inf_continuous P" and Q: "inf_continuous Q" shows "inf_continuous (λx. sup (P x) (Q x))" unfolding inf_continuous_def proof (safe intro!: antisym) fix M :: "nat ⇒ 'a" assume M: "decseq M" show "sup (P (INF i. M i)) (Q (INF i. M i)) ≤ (INF i. sup (P (M i)) (Q (M i)))" unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro ccINF_greatest sup_mono ccINF_lower) auto have "(INF i. sup (P (M i)) (Q (M i))) ≤ (INF j i. sup (P (M i)) (Q (M j)))" proof (intro ccINF_greatest) fix i j from M assms[THEN inf_continuous_mono] show "sup (P (M i)) (Q (M j)) ≥ (INF i. sup (P (M i)) (Q (M i)))" by (intro ccINF_lower2[of _ "sup i j"] sup_mono) (auto simp: mono_def antimono_def) qed auto also have "… ≤ sup (P (INF i. M i)) (Q (INF i. M i))" by (simp add: inf_continuousD[OF P M] inf_continuousD[OF Q M] ccINF_sup sup_ccINF) finally show "sup (P (INF i. M i)) (Q (INF i. M i)) ≥ (INF i. sup (P (M i)) (Q (M i)))" . qed lemma inf_continuous_and[order_continuous_intros]: "inf_continuous P ⟹ inf_continuous Q ⟹ inf_continuous (λx. P x ∧ Q x)" using inf_continuous_inf[of P Q] by simp lemma inf_continuous_or[order_continuous_intros]: "inf_continuous P ⟹ inf_continuous Q ⟹ inf_continuous (λx. P x ∨ Q x)" using inf_continuous_sup[of P Q] by simp lemma inf_continuous_compose: assumes f: "inf_continuous f" and g: "inf_continuous g" shows "inf_continuous (λx. f (g x))" unfolding inf_continuous_def proof safe fix M :: "nat ⇒ 'c" assume M: "antimono M" then have "antimono (λi. g (M i))" using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def) with M show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))" by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD]) qed lemma inf_continuous_gfp: assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U") proof (rule antisym) note mono = inf_continuous_mono[OF ‹inf_continuous F›] show "gfp F ≤ ?U" proof (rule INF_greatest) fix i show "gfp F ≤ (F ^^ i) top" proof (induct i) case (Suc i) have "gfp F = F (gfp F)" by (simp add: gfp_fixpoint[OF mono]) also have "… ≤ F ((F ^^ i) top)" by (rule monoD[OF mono Suc]) also have "… = (F ^^ Suc i) top" by simp finally show ?case . qed simp qed show "?U ≤ gfp F" proof (rule gfp_upperbound) have *: "antimono (λi::nat. (F ^^ i) top)" proof - { fix i::nat have "(F ^^ Suc i) top ≤ (F ^^ i) top" proof (induct i) case 0 show ?case by simp next case Suc thus ?case using monoD[OF mono Suc] by auto qed } thus ?thesis by (auto simp add: antimono_iff_le_Suc) qed have "?U ≤ (INF i. (F ^^ Suc i) top)" by (fast intro: INF_greatest INF_lower) also have "… ≤ F ?U" by (simp add: inf_continuousD ‹inf_continuous F› *) finally show "?U ≤ F ?U" . qed qed lemma gfp_transfer: assumes α: "inf_continuous α" and f: "inf_continuous f" and g: "inf_continuous g" assumes [simp]: "α top = top" "⋀x. α (f x) = g (α x)" shows "α (gfp f) = gfp g" proof - have "α (gfp f) = (INF i. α ((f^^i) top))" unfolding inf_continuous_gfp[OF f] by (intro f α inf_continuousD antimono_funpow inf_continuous_mono) moreover have "α ((f^^i) top) = (g^^i) top" for i by (induction i; simp) ultimately show ?thesis unfolding inf_continuous_gfp[OF g] by simp qed lemma gfp_transfer_bounded: assumes P: "P (f top)" "⋀x. P x ⟹ P (f x)" "⋀M. antimono M ⟹ (⋀i. P (M i)) ⟹ P (INF i::nat. M i)" assumes α: "⋀M. antimono M ⟹ (⋀i::nat. P (M i)) ⟹ α (INF i. M i) = (INF i. α (M i))" assumes f: "inf_continuous f" and g: "inf_continuous g" assumes [simp]: "⋀x. P x ⟹ α (f x) = g (α x)" assumes g_bound: "⋀x. g x ≤ α (f top)" shows "α (gfp f) = gfp g" proof (rule antisym) note mono_g = inf_continuous_mono[OF g] have P_pow: "P ((f ^^ i) (f top))" for i by (induction i) (auto intro!: P) have antimono_pow: "antimono (λi. (f ^^ i) top)" unfolding antimono_iff_le_Suc proof fix i show "(f ^^ Suc i) top ≤ (f ^^ i) top" proof (induct i) case Suc thus ?case using monoD[OF inf_continuous_mono[OF f] Suc] by auto qed (simp add: le_fun_def) qed have antimono_pow2: "antimono (λi. (f ^^ i) (f top))" proof show "x ≤ y ⟹ (f ^^ y) (f top) ≤ (f ^^ x) (f top)" for x y using antimono_pow[THEN antimonoD, of "Suc x" "Suc y"] unfolding funpow_Suc_right by simp qed have gfp_f: "gfp f = (INF i. (f ^^ i) (f top))" unfolding inf_continuous_gfp[OF f] proof (rule INF_eq) show "∃j∈UNIV. (f ^^ j) (f top) ≤ (f ^^ i) top" for i by (intro bexI[of _ "i - 1"]) (auto simp: diff_Suc funpow_Suc_right simp del: funpow.simps(2) split: nat.split) show "∃j∈UNIV. (f ^^ j) top ≤ (f ^^ i) (f top)" for i by (intro bexI[of _ "Suc i"]) (auto simp: funpow_Suc_right simp del: funpow.simps(2)) qed have P_lfp: "P (gfp f)" unfolding gfp_f by (auto intro!: P P_pow antimono_pow2) have "α (gfp f) = (INF i. α ((f^^i) (f top)))" unfolding gfp_f by (rule α) (auto intro!: P_pow antimono_pow2) also have "… ≥ gfp g" proof (rule INF_greatest) fix i show "gfp g ≤ α ((f^^i) (f top))" proof (induction i) case (Suc n) then show ?case by (subst gfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow) next case 0 have "gfp g ≤ α (f top)" by (subst gfp_unfold[OF mono_g]) (rule g_bound) then show ?case by simp qed qed finally show "gfp g ≤ α (gfp f)" . show "α (gfp f) ≤ gfp g" proof (induction rule: gfp_ordinal_induct[OF mono_g]) case (1 S) then show ?case by (subst gfp_unfold[OF inf_continuous_mono[OF f]]) (simp add: monoD[OF mono_g] P_lfp) qed (auto intro: Inf_greatest) qed subsubsection ‹Least fixed points in countable complete lattices› definition (in countable_complete_lattice) cclfp :: "('a ⇒ 'a) ⇒ 'a" where "cclfp f = (SUP i. (f ^^ i) bot)" lemma cclfp_unfold: assumes "sup_continuous F" shows "cclfp F = F (cclfp F)" proof - have "cclfp F = (SUP i. F ((F ^^ i) bot))" unfolding cclfp_def by (subst UNIV_nat_eq) auto also have "… = F (cclfp F)" unfolding cclfp_def by (intro sup_continuousD[symmetric] assms mono_funpow sup_continuous_mono) finally show ?thesis . qed lemma cclfp_lowerbound: assumes f: "mono f" and A: "f A ≤ A" shows "cclfp f ≤ A" unfolding cclfp_def proof (intro ccSUP_least) fix i show "(f ^^ i) bot ≤ A" proof (induction i) case (Suc i) from monoD[OF f this] A show ?case by auto qed simp qed simp lemma cclfp_transfer: assumes "sup_continuous α" "mono f" assumes "α bot = bot" "⋀x. α (f x) = g (α x)" shows "α (cclfp f) = cclfp g" proof - have "α (cclfp f) = (SUP i. α ((f ^^ i) bot))" unfolding cclfp_def by (intro sup_continuousD assms mono_funpow sup_continuous_mono) moreover have "α ((f ^^ i) bot) = (g ^^ i) bot" for i by (induction i) (simp_all add: assms) ultimately show ?thesis by (simp add: cclfp_def) qed end