Theory CCPO_Topology

(*  Title:       CCPO_Topology.thy
    Author:      Johannes Hölzl, TU Munich
*)

section ‹CCPO topologies›

theory CCPO_Topology
imports
  "HOL-Analysis.Extended_Real_Limits"
  "../Coinductive_Nat"
begin

lemma dropWhile_append:
  "dropWhile P (xs @ ys) = (if xset 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 "cC. 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 cC 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 *: "DK. 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