Theory CCPO_Topology
section ‹CCPO topologies›
theory CCPO_Topology
imports
"HOL-Analysis.Extended_Real_Limits"
"../Coinductive_Nat"
begin
lemma dropWhile_append:
"dropWhile P (xs @ ys) = (if ∀x∈set xs. P x then dropWhile P ys else dropWhile P xs @ ys)"
by auto
lemma dropWhile_False: "(⋀x. x ∈ set xs ⟹ P x) ⟹ dropWhile P xs = []"
by simp
abbreviation (in order) "chain ≡ Complete_Partial_Order.chain (≤)"
lemma (in linorder) chain_linorder: "chain C"
by (simp add: chain_def linear)
lemma continuous_add_ereal:
assumes "0 ≤ t"
shows "continuous_on {-∞::ereal <..} (λx. t + x)"
proof (subst continuous_on_open_vimage, (intro open_greaterThan allI impI)+)
fix B :: "ereal set" assume "open B"
show "open ((λx. t + x) -` B ∩ {- ∞<..})"
proof (cases t)
case (real t')
then have *: "(λx. t + x) -` B ∩ {- ∞<..} = (λx. 1 * x + (-t)) ` (B ∩ {-∞ <..})"
apply (simp add: set_eq_iff image_iff Bex_def)
apply (intro allI iffI)
apply (rule_tac x= "x + ereal t'" in exI)
apply (case_tac x)
apply (auto simp: ac_simps)
done
show ?thesis
unfolding *
apply (rule ereal_open_affinity_pos)
using ‹open B›
apply (auto simp: real)
done
qed (insert ‹0 ≤ t›, auto)
qed
lemma tendsto_add_ereal:
"0 ≤ x ⟹ 0 ≤ y ⟹ (f ⤏ y) F ⟹ ((λz. x + f z :: ereal) ⤏ x + y) F"
apply (rule tendsto_compose[where f=f])
using continuous_add_ereal[where t=x]
unfolding continuous_on_def
apply (auto simp add: at_within_open[where S="{- ∞ <..}"])
done
lemma tendsto_LimI: "(f ⤏ y) F ⟹ (f ⤏ Lim F f) F"
by (metis tendsto_Lim tendsto_bot)
subsection ‹The filter ‹at'››
abbreviation (in ccpo) "compact_element ≡ ccpo.compact Sup (≤)"
lemma tendsto_unique_eventually:
fixes x x' :: "'a :: t2_space"
shows "F ≠ bot ⟹ eventually (λx. f x = g x) F ⟹ (f ⤏ x) F ⟹ (g ⤏ x') F ⟹ x = x'"
by (metis tendsto_unique filterlim_cong)
lemma (in ccpo) ccpo_Sup_upper2: "chain C ⟹ x ∈ C ⟹ y ≤ x ⟹ y ≤ Sup C"
by (blast intro: ccpo_Sup_upper order_trans)
lemma tendsto_open_vimage: "(⋀B. open B ⟹ open (f -` B)) ⟹ f ─l→ f l"
using continuous_on_open_vimage[of UNIV f] continuous_on_def[of UNIV f] by simp
lemma open_vimageI: "(⋀x. f ─x→ f x) ⟹ open A ⟹ open (f -` A)"
using continuous_on_open_vimage[of UNIV f] continuous_on_def[of UNIV f] by simp
lemma principal_bot: "principal x = bot ⟷ x = {}"
by (auto simp: filter_eq_iff eventually_principal)
definition "at' x = (if open {x} then principal {x} else at x)"
lemma at'_bot: "at' x ≠ bot"
by (simp add: at'_def at_eq_bot_iff principal_bot)
lemma tendsto_id_at'[simp, intro]: "((λx. x) ⤏ x) (at' x)"
by (simp add: at'_def topological_tendstoI eventually_principal tendsto_ident_at)
lemma cont_at': "(f ⤏ f x) (at' x) ⟷ f ─x→ f x"
using at_eq_bot_iff[of x] by (auto split: if_split_asm intro!: topological_tendstoI simp: eventually_principal at'_def)
subsection ‹The type class ‹ccpo_topology››
text ‹Temporarily relax type constraints for @{term "open"}.›
setup ‹Sign.add_const_constraint
(@{const_name "open"}, SOME @{typ "'a::open set ⇒ bool"})›
class ccpo_topology = "open" + ccpo +
assumes open_ccpo: "open A ⟷ (∀C. chain C ⟶ C ≠ {} ⟶ Sup C ∈ A ⟶ C ∩ A ≠ {})"
begin
lemma open_ccpoD:
assumes "open A" "chain C" "C ≠ {}" "Sup C ∈ A"
shows "∃c∈C. ∀c'∈C. c ≤ c' ⟶ c' ∈ A"
proof (rule ccontr)
assume "¬ ?thesis"
then have *: "⋀c. c ∈ C ⟹ ∃c'∈C. c ≤ c' ∧ c' ∉ A"
by auto
with ‹chain C› ‹C ≠ {}› have "chain (C - A)" "C - A ≠ {}"
by (auto intro: chain_Diff)
moreover have "Sup C = Sup (C - A)"
proof (safe intro!: order.antisym ccpo_Sup_least ‹chain C› chain_Diff)
fix c assume "c ∈ C"
with * obtain c' where "c' ∈ C" "c ≤ c'" "c' ∉ A"
by auto
with ‹c∈C› show "c ≤ ⨆(C - A)"
by (intro ccpo_Sup_upper2 ‹chain (C - A)›) auto
qed (auto intro: ‹chain C› ccpo_Sup_upper)
ultimately show False
using ‹open A› ‹Sup C ∈ A› by (auto simp: open_ccpo)
qed
lemma open_ccpo_Iic: "open {.. b}"
by (auto simp: open_ccpo) (metis Int_iff atMost_iff ccpo_Sup_upper empty_iff order_trans)
subclass topological_space
proof
show "open (UNIV::'a set)"
unfolding open_ccpo by auto
next
fix S T :: "'a set" assume "open S" "open T"
show "open (S ∩ T)"
unfolding open_ccpo
proof (intro allI impI)
fix C assume C: "chain C" "C ≠ {}" and "⨆C ∈ S ∩ T"
with open_ccpoD[OF ‹open S› C] open_ccpoD[OF ‹open T› C]
show "C ∩ (S ∩ T) ≠ {}"
unfolding chain_def by blast
qed
next
fix K :: "'a set set" assume *: "∀D∈K. open D"
show "open (⋃K)"
unfolding open_ccpo
proof (intro allI impI)
fix C assume "chain C" "C ≠ {}" "⨆C ∈ (⋃K)"
with * obtain D where "D ∈ K" "⨆C ∈ D" "C ∩ D ≠ {}"
by (auto simp: open_ccpo)
then show "C ∩ (⋃K) ≠ {}"
by auto
qed
qed
lemma closed_ccpo: "closed A ⟷ (∀C. chain C ⟶ C ≠ {} ⟶ C ⊆ A ⟶ Sup C ∈ A)"
unfolding closed_def open_ccpo by auto
lemma closed_admissible: "closed {x. P x} ⟷ ccpo.admissible Sup (≤) P"
unfolding closed_ccpo ccpo.admissible_def by auto
lemma open_singletonI_compact: "compact_element x ⟹ open {x}"
using admissible_compact_neq[of Sup "(≤)" x]
by (simp add: closed_admissible[symmetric] open_closed Collect_neg_eq)
lemma closed_Ici: "closed {.. b}"
by (auto simp: closed_ccpo intro: ccpo_Sup_least)
lemma closed_Iic: "closed {b ..}"
by (auto simp: closed_ccpo intro: ccpo_Sup_upper2)
text ‹
@{class ccpo_topology}s are also @{class t2_space}s.
This is necessary to have a unique continuous extension.
›
subclass t2_space
proof
fix x y :: 'a assume "x ≠ y"
show "∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}"
proof cases
{ fix x y assume "x ≠ y" "x ≤ y"
then have "open {..x} ∧ open (- {..x}) ∧ x ∈ {..x} ∧ y ∈ - {..x} ∧ {..x} ∩ - {..x} = {}"
by (auto intro: open_ccpo_Iic closed_Ici) }
moreover assume "x ≤ y ∨ y ≤ x"
ultimately show ?thesis
using ‹x ≠ y› by (metis Int_commute)
next
assume "¬ (x ≤ y ∨ y ≤ x)"
then have "open ({..x} ∩ - {..y}) ∧ open ({..y} ∩ - {..x}) ∧
x ∈ {..x} ∩ - {..y} ∧ y ∈ {..y} ∩ - {..x} ∧ ({..x} ∩ - {..y}) ∩ ({..y} ∩ - {..x}) = {}"
by (auto intro: open_ccpo_Iic closed_Ici)
then show ?thesis by auto
qed
qed
end
lemma tendsto_le_ccpo:
fixes f g :: "'a ⇒ 'b::ccpo_topology"
assumes F: "¬ trivial_limit F"
assumes x: "(f ⤏ x) F" and y: "(g ⤏ y) F"
assumes ev: "eventually (λx. g x ≤ f x) F"
shows "y ≤ x"
proof (rule ccontr)
assume "¬ y ≤ x"
show False
proof cases
assume "x ≤ y"
with ‹¬ y ≤ x›
have "open {..x}" "open (- {..x})" "x ∈ {..x}" "y ∈ - {..x}" "{..x} ∩ - {..x} = {}"
by (auto intro: open_ccpo_Iic closed_Ici)
with topological_tendstoD[OF x, of "{..x}"] topological_tendstoD[OF y, of "- {..x}"]
have "eventually (λz. f z ≤ x) F" "eventually (λz. ¬ g z ≤ x) F"
by auto
with ev have "eventually (λx. False) F" by eventually_elim (auto intro: order_trans)
with F show False by (auto simp: eventually_False)
next
assume "¬ x ≤ y"
with ‹¬ y ≤ x› have "open ({..x} ∩ - {..y})" "open ({..y} ∩ - {..x})"
"x ∈ {..x} ∩ - {..y}" "y ∈ {..y} ∩ - {..x}" "({..x} ∩ - {..y}) ∩ ({..y} ∩ - {..x}) = {}"
by (auto intro: open_ccpo_Iic closed_Ici)
with topological_tendstoD[OF x, of "{..x} ∩ - {..y}"]
topological_tendstoD[OF y, of "{..y} ∩ - {..x}"]
have "eventually (λz. f z ≤ x ∧ ¬ f z ≤ y) F" "eventually (λz. g z ≤ y ∧ ¬ g z ≤ x) F"
by auto
with ev have "eventually (λx. False) F" by eventually_elim (auto intro: order_trans)
with F show False by (auto simp: eventually_False)
qed
qed
lemma tendsto_ccpoI:
fixes f :: "'a::ccpo_topology ⇒ 'b::ccpo_topology"
shows "(⋀C. chain C ⟹ C ≠ {} ⟹ chain (f ` C) ∧ f (Sup C) = Sup (f`C)) ⟹ f ─x→ f x"
by (intro tendsto_open_vimage) (auto simp: open_ccpo)
lemma tendsto_mcont:
assumes mcont: "mcont Sup (≤) Sup (≤) (f :: 'a :: ccpo_topology ⇒ 'b :: ccpo_topology)"
shows "f ─l→ f l"
proof (intro tendsto_ccpoI conjI)
fix C :: "'a set" assume C: "chain C" "C ≠ {}"
show "chain (f`C)"
using mcont
by (intro chain_imageI[where le_a="(≤)"] C) (simp add: mcont_def monotone_def)
show "f (⨆C) = ⨆(f ` C)"
using mcont C by (simp add: mcont_def cont_def)
qed
subsection ‹Instances for @{class ccpo_topology}s and continuity theorems›
instantiation set :: (type) ccpo_topology
begin
definition open_set :: "'a set set ⇒ bool" where
"open_set A ⟷ (∀C. chain C ⟶ C ≠ {} ⟶ Sup C ∈ A ⟶ C ∩ A ≠ {})"
instance
by intro_classes (simp add: open_set_def)
end
instantiation enat :: ccpo_topology
begin
instance
proof
fix A :: "enat set"
show "open A = (∀C. chain C ⟶ C ≠ {} ⟶ ⨆C ∈ A ⟶ C ∩ A ≠ {})"
proof (intro iffI allI impI)
fix C x assume "open A" "chain C" "C ≠ {}" "⨆C ∈ A"
show "C ∩ A ≠ {}"
proof cases
assume "⨆C = ∞"
with ‹⨆C ∈ A› ‹open A› obtain n where "{enat n <..} ⊆ A"
unfolding open_enat_iff by auto
with ‹⨆C = ∞› Sup_eq_top_iff[of C] show ?thesis
by (auto simp: top_enat_def)
next
assume "⨆C ≠ ∞"
then obtain n where "C ⊆ {.. enat n}"
unfolding Sup_eq_top_iff top_enat_def[symmetric] by (auto simp: not_less top_enat_def)
moreover have "finite {.. enat n}"
by (auto intro: finite_enat_bounded)
ultimately have "finite C"
by (auto intro: finite_subset)
from in_chain_finite[OF ‹chain C› ‹finite C› ‹C ≠ {}›] ‹⨆C ∈ A› show ?thesis
by auto
qed
next
assume C: "∀C. chain C ⟶ C ≠ {} ⟶ ⨆C ∈ A ⟶ C ∩ A ≠ {}"
show "open A"
unfolding open_enat_iff
proof safe
assume "∞ ∈ A"
{ fix C :: "enat set" assume "infinite C"
then have "⨆C = ∞"
by (auto simp: Sup_enat_def)
with ‹infinite C› C[THEN spec, of C] ‹∞ ∈ A› have "C ∩ A ≠ {}"
by auto }
note inf_C = this
show "∃x. {enat x<..} ⊆ A"
proof (rule ccontr)
assume "¬ (∃x. {enat x<..} ⊆ A)"
with ‹∞ ∈ A› have "⋀x. ∃y>x. enat y ∉ A"
by (simp add: subset_eq Bex_def) (metis enat.exhaust enat_ord_simps(2))
then have "infinite {n. enat n ∉ A}"
unfolding infinite_nat_iff_unbounded by auto
then have "infinite (enat ` {n. enat n ∉ A})"
by (auto dest!: finite_imageD)
from inf_C[OF this] show False
by auto
qed
qed
qed
qed
end
lemmas tendsto_inf2[THEN tendsto_compose, tendsto_intros] =
tendsto_mcont[OF mcont_inf2]
lemma isCont_inf2[THEN isCont_o2[rotated]]:
"isCont (λx. x ⊓ y) (z :: _ :: {ccpo_topology, complete_distrib_lattice})"
by(simp add: isCont_def tendsto_inf2 tendsto_ident_at)
lemmas tendsto_sup1[THEN tendsto_compose, tendsto_intros] =
tendsto_mcont[OF mcont_sup1]
lemma isCont_If: "isCont f x ⟹ isCont g x ⟹ isCont (λx. if Q then f x else g x) x"
by (cases Q) auto
lemma isCont_enat_case: "isCont (f (epred n)) x ⟹ isCont g x ⟹ isCont (λx. co.case_enat (g x) (λn. f n x) n) x"
by (cases n rule: enat_coexhaust) auto
end