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