Theory Complete_Non_Orders.Continuity

theory Continuity
  imports Complete_Relations
begin

subsection ‹Scott Continuity, $\omega$-Continuity›

text ‹In this Section, we formalize Scott continuity and $\omega$-continuity.
We then prove that a Scott continuous map is $\omega$-continuous and that an $\omega$-continuous 
map is ``nearly'' monotone.›

definition continuous (‹_-continuous› [1000]1000) where
  "𝒞-continuous A (⊑) B (⊴) f ≡
   f ` A ⊆ B ∧
   (∀X s. 𝒞 X (⊑) ⟶ X ≠ {} ⟶ X ⊆ A ⟶ extreme_bound A (⊑) X s ⟶ extreme_bound B (⊴) (f`X) (f s))"
  for leA (infix ‹⊑› 50) and leB (infix ‹⊴› 50)

lemmas continuousI[intro?] =
  continuous_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp, rule_format]

lemmas continuousE =
  continuous_def[unfolded atomize_eq, THEN iffD1, elim_format, unfolded conj_imp_eq_imp_imp, rule_format]

lemma
  fixes prec_eq (infix ‹≼› 50) and less_eq (infix ‹⊑› 50)
  assumes "𝒞-continuous I (≼) A (⊑) f"
  shows continuous_carrierD[dest]: "f ` I ⊆ A"
    and continuousD: "𝒞 X (≼) ⟹ X ≠ {} ⟹ X ⊆ I ⟹ extreme_bound I (≼) X b ⟹ extreme_bound A (⊑) (f ` X) (f b)"
  using assms by (auto elim!: continuousE)

lemma continuous_comp:
  fixes leA (infix ‹⊑⇩A› 50) and leB (infix ‹⊑⇩B› 50) and leC (infix ‹⊑⇩C› 50)
  assumes KfL: "∀X ⊆ A. 𝒦 X (⊑⇩A) ⟶ ℒ (f ` X) (⊑⇩B)"
  assumes f: "𝒦-continuous A (⊑⇩A) B (⊑⇩B) f" and g: "ℒ-continuous B (⊑⇩B) C (⊑⇩C) g"
  shows "𝒦-continuous A (⊑⇩A) C (⊑⇩C) (g ∘ f)"
  apply (intro continuousI)
proof -
  from f g have fAB: "f ` A ⊆ B" and gBC: "g ` B ⊆ C" by auto
  then show "(g ∘ f) ` A ⊆ C" by auto
  fix X s
  assume XA: "X ⊆ A" and X0: "X ≠ {}" and XK: "𝒦 X (⊑⇩A)" and Xs: "extreme_bound A (⊑⇩A) X s"
  from fAB XA have fXB: "f ` X ⊆ B" by auto
  from X0 have fX0: "f ` X ≠ {}" by auto
  from KfL XA XK have fXL: "ℒ (f ` X) (⊑⇩B)" by auto
  from continuousD[OF f XK X0 XA Xs]
  have "extreme_bound B (⊑⇩B) (f ` X) (f s)".
  from continuousD[OF g fXL fX0 fXB this]
  show "extreme_bound C (⊑⇩C) ((g∘f)`X) ((g∘f) s)" by (auto simp: image_comp)
qed

lemma continuous_comp_top:
  fixes leA (infix ‹⊑⇩A› 50) and leB (infix ‹⊑⇩B› 50) and leC (infix ‹⊑⇩C› 50)
  assumes f: "𝒦-continuous A (⊑⇩A) B (⊑⇩B) f" and g: "⊤-continuous B (⊑⇩B) C (⊑⇩C) g"
  shows "𝒦-continuous A (⊑⇩A) C (⊑⇩C) (g ∘ f)"
  by (rule continuous_comp[OF _ f g], auto)

lemma id_continuous:
  fixes leA (infix ‹⊑⇩A› 50)
  shows "𝒦-continuous A (⊑⇩A) A (⊑⇩A) (λx. x)"
  by (auto intro: continuousI)

lemma cst_continuous:
  fixes leA (infix ‹⊑⇩A› 50) and leB (infix ‹⊑⇩B› 50)
  assumes "b ∈ B" and bb: "b ⊑⇩B b"
  shows "𝒦-continuous A (⊑⇩A) B (⊑⇩B) (λx. b)"
  apply (intro continuousI)
  using assms(1) apply auto
  using assms extreme_bound_singleton_refl[of B "(⊑⇩B)" b] by blast


lemma continuous_cmono:
  assumes CD: "𝒞 ≤ 𝒟" shows "𝒟-continuous ≤ 𝒞-continuous"
proof (safe intro!: le_funI le_boolI)
  fix I A f and prec_eq (infix ‹≼› 50) and less_eq (infix ‹⊑› 50)
  assume cont: "𝒟-continuous I (≼) A (⊑) f"
  show "𝒞-continuous I (≼) A (⊑) f"
  proof (rule continuousI)
    from cont show "f ` I ⊆ A" by auto
    fix X s assume X: "𝒞 X (≼)" and X0: "X ≠ {}" and XI: "X ⊆ I" and Xs: "extreme_bound I (≼) X s"
    from CD X have "𝒟 X (≼)" by auto
    from continuousD[OF cont, OF this X0 XI Xs]
    show "extreme_bound A (⊑) (f ` X) (f s)".
  qed
qed

context
  fixes prec_eq :: "'i ⇒ 'i ⇒ bool" (infix ‹≼› 50) and less_eq :: "'a ⇒ 'a ⇒ bool" (infix ‹⊑› 50)
begin

lemma continuous_subclass:
  assumes CD: "∀X⊆I. X ≠ {} ⟶ 𝒞 X (≼) ⟶ 𝒟 X (≼)" and cont: "𝒟-continuous I (≼) A (⊑) f"
  shows "𝒞-continuous I (≼) A (⊑) f"
  using cont by (auto simp: continuous_def CD[rule_format])

lemma chain_continuous_imp_well_continuous:
  assumes cont: "connex-continuous I (≼) A (⊑) f"
  shows "well_related_set-continuous I (≼) A (⊑) f"
  by (rule continuous_subclass[OF _ cont], auto simp: well_related_set.connex)

lemma well_continuous_imp_omega_continous:
  assumes cont: "well_related_set-continuous I (≼) A (⊑) f"
  shows "omega_chain-continuous I (≼) A (⊑) f"
  by (rule continuous_subclass[OF _ cont], auto simp: omega_chain_imp_well_related)

end

abbreviation "scott_continuous I (≼) ≡ directed_set-continuous I (≼)"
  for prec_eq (infix ‹≼› 50)

lemma scott_continuous_imp_well_continuous:
  fixes prec_eq :: "'i ⇒ 'i ⇒ bool" (infix ‹≼› 50) and less_eq :: "'a ⇒ 'a ⇒ bool" (infix ‹⊑› 50)
  assumes cont: "scott_continuous I (≼) A (⊑) f"
  shows "well_related_set-continuous I (≼) A (⊑) f"
  by (rule continuous_subclass[OF _ cont], auto simp: well_related_set.directed_set)

lemmas scott_continuous_imp_omega_continuous =
  scott_continuous_imp_well_continuous[THEN well_continuous_imp_omega_continous]


subsubsection ‹Continuity implies monotonicity›

lemma continuous_imp_mono_refl:
  fixes prec_eq (infix ‹≼› 50) and less_eq (infix ‹⊑› 50)
  assumes cont: "𝒞-continuous I (≼) A (⊑) f" and xyC: "𝒞 {x,y} (≼)"
    and xy: "x ≼ y" and yy: "y ≼ y"
    and x: "x ∈ I" and y: "y ∈ I"
  shows "f x ⊑ f y"
proof-
  have fboy: "extreme_bound A (⊑) (f ` {x,y}) (f y)"
  proof (intro continuousD[OF cont] xyC)
    from x y show CI: "{x,y} ⊆ I" by auto
    show Cy: "extreme_bound I (≼) {x,y} y" using xy yy x y by auto
  qed auto
  then show ?thesis by auto
qed

lemma omega_continuous_imp_mono_refl:
  fixes prec_eq (infix ‹≼› 50) and less_eq (infix ‹⊑› 50)
  assumes cont: "omega_chain-continuous I (≼) A (⊑) f"
    and xx: "x ≼ x" and xy: "x ≼ y" and yy: "y ≼ y"
    and x: "x ∈ I" and y: "y ∈ I"
  shows "f x ⊑ f y"
  apply (rule continuous_imp_mono_refl[OF cont, OF pair_omega_chain])
  using assms by auto

context reflexive begin

lemma continuous_imp_monotone_on:
  fixes leB (infix ‹⊴› 50)
  assumes cont: "𝒞-continuous A (⊑) B (⊴) f"
    and II: "∀i ∈ A. ∀ j ∈ A. i ⊑ j ⟶ 𝒞 {i,j} (⊑)"
  shows "monotone_on A (⊑) (⊴) f"
proof-
  show ?thesis
    apply (intro monotone_onI continuous_imp_mono_refl[OF cont])
    using II by auto
qed

lemma well_complete_imp_monotone_on:
  fixes leB (infix ‹⊴› 50)
  assumes cont: "well_related_set-continuous A (⊑) B (⊴) f"
  shows "monotone_on A (⊑) (⊴) f"                       
  by (auto intro!: continuous_imp_monotone_on cont pair_well_related)

end

end