Theory Lub_Glb

(*  Title:      HOL/Library/Lub_Glb.thy
    Author:     Jacques D. Fleuriot, University of Cambridge
    Author:     Amine Chaieb, University of Cambridge *)

section ‹Definitions of Least Upper Bounds and Greatest Lower Bounds›

theory Lub_Glb
imports Complex_Main
begin

text ‹Thanks to suggestions by James Margetson›

definition setle :: "'a set ⇒ 'a::ord ⇒ bool"  (infixl ‹*<=› 70)
  where "S *<= x = (∀y∈S. y ≤ x)"

definition setge :: "'a::ord ⇒ 'a set ⇒ bool"  (infixl ‹<=*› 70)
  where "x <=* S = (∀y∈S. x ≤ y)"


subsection ‹Rules for the Relations ‹*<=› and ‹<=*››

lemma setleI: "∀y∈S. y ≤ x ⟹ S *<= x"
  by (simp add: setle_def)

lemma setleD: "S *<= x ⟹ y∈S ⟹ y ≤ x"
  by (simp add: setle_def)

lemma setgeI: "∀y∈S. x ≤ y ⟹ x <=* S"
  by (simp add: setge_def)

lemma setgeD: "x <=* S ⟹ y∈S ⟹ x ≤ y"
  by (simp add: setge_def)


definition leastP :: "('a ⇒ bool) ⇒ 'a::ord ⇒ bool"
  where "leastP P x = (P x ∧ x <=* Collect P)"

definition isUb :: "'a set ⇒ 'a set ⇒ 'a::ord ⇒ bool"
  where "isUb R S x = (S *<= x ∧ x ∈ R)"

definition isLub :: "'a set ⇒ 'a set ⇒ 'a::ord ⇒ bool"
  where "isLub R S x = leastP (isUb R S) x"

definition ubs :: "'a set ⇒ 'a::ord set ⇒ 'a set"
  where "ubs R S = Collect (isUb R S)"


subsection ‹Rules about the Operators \<^term>‹leastP›, \<^term>‹ub› and \<^term>‹lub››

lemma leastPD1: "leastP P x ⟹ P x"
  by (simp add: leastP_def)

lemma leastPD2: "leastP P x ⟹ x <=* Collect P"
  by (simp add: leastP_def)

lemma leastPD3: "leastP P x ⟹ y ∈ Collect P ⟹ x ≤ y"
  by (blast dest!: leastPD2 setgeD)

lemma isLubD1: "isLub R S x ⟹ S *<= x"
  by (simp add: isLub_def isUb_def leastP_def)

lemma isLubD1a: "isLub R S x ⟹ x ∈ R"
  by (simp add: isLub_def isUb_def leastP_def)

lemma isLub_isUb: "isLub R S x ⟹ isUb R S x"
  unfolding isUb_def by (blast dest: isLubD1 isLubD1a)

lemma isLubD2: "isLub R S x ⟹ y ∈ S ⟹ y ≤ x"
  by (blast dest!: isLubD1 setleD)

lemma isLubD3: "isLub R S x ⟹ leastP (isUb R S) x"
  by (simp add: isLub_def)

lemma isLubI1: "leastP(isUb R S) x ⟹ isLub R S x"
  by (simp add: isLub_def)

lemma isLubI2: "isUb R S x ⟹ x <=* Collect (isUb R S) ⟹ isLub R S x"
  by (simp add: isLub_def leastP_def)

lemma isUbD: "isUb R S x ⟹ y ∈ S ⟹ y ≤ x"
  by (simp add: isUb_def setle_def)

lemma isUbD2: "isUb R S x ⟹ S *<= x"
  by (simp add: isUb_def)

lemma isUbD2a: "isUb R S x ⟹ x ∈ R"
  by (simp add: isUb_def)

lemma isUbI: "S *<= x ⟹ x ∈ R ⟹ isUb R S x"
  by (simp add: isUb_def)

lemma isLub_le_isUb: "isLub R S x ⟹ isUb R S y ⟹ x ≤ y"
  unfolding isLub_def by (blast intro!: leastPD3)

lemma isLub_ubs: "isLub R S x ⟹ x <=* ubs R S"
  unfolding ubs_def isLub_def by (rule leastPD2)

lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
  apply (frule isLub_isUb)
  apply (frule_tac x = y in isLub_isUb)
  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
  done

lemma isUb_UNIV_I: "(⋀y. y ∈ S ⟹ y ≤ u) ⟹ isUb UNIV S u"
  by (simp add: isUbI setleI)


definition greatestP :: "('a ⇒ bool) ⇒ 'a::ord ⇒ bool"
  where "greatestP P x = (P x ∧ Collect P *<=  x)"

definition isLb :: "'a set ⇒ 'a set ⇒ 'a::ord ⇒ bool"
  where "isLb R S x = (x <=* S ∧ x ∈ R)"

definition isGlb :: "'a set ⇒ 'a set ⇒ 'a::ord ⇒ bool"
  where "isGlb R S x = greatestP (isLb R S) x"

definition lbs :: "'a set ⇒ 'a::ord set ⇒ 'a set"
  where "lbs R S = Collect (isLb R S)"


subsection ‹Rules about the Operators \<^term>‹greatestP›, \<^term>‹isLb› and \<^term>‹isGlb››

lemma greatestPD1: "greatestP P x ⟹ P x"
  by (simp add: greatestP_def)

lemma greatestPD2: "greatestP P x ⟹ Collect P *<= x"
  by (simp add: greatestP_def)

lemma greatestPD3: "greatestP P x ⟹ y ∈ Collect P ⟹ x ≥ y"
  by (blast dest!: greatestPD2 setleD)

lemma isGlbD1: "isGlb R S x ⟹ x <=* S"
  by (simp add: isGlb_def isLb_def greatestP_def)

lemma isGlbD1a: "isGlb R S x ⟹ x ∈ R"
  by (simp add: isGlb_def isLb_def greatestP_def)

lemma isGlb_isLb: "isGlb R S x ⟹ isLb R S x"
  unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)

lemma isGlbD2: "isGlb R S x ⟹ y ∈ S ⟹ y ≥ x"
  by (blast dest!: isGlbD1 setgeD)

lemma isGlbD3: "isGlb R S x ⟹ greatestP (isLb R S) x"
  by (simp add: isGlb_def)

lemma isGlbI1: "greatestP (isLb R S) x ⟹ isGlb R S x"
  by (simp add: isGlb_def)

lemma isGlbI2: "isLb R S x ⟹ Collect (isLb R S) *<= x ⟹ isGlb R S x"
  by (simp add: isGlb_def greatestP_def)

lemma isLbD: "isLb R S x ⟹ y ∈ S ⟹ y ≥ x"
  by (simp add: isLb_def setge_def)

lemma isLbD2: "isLb R S x ⟹ x <=* S "
  by (simp add: isLb_def)

lemma isLbD2a: "isLb R S x ⟹ x ∈ R"
  by (simp add: isLb_def)

lemma isLbI: "x <=* S ⟹ x ∈ R ⟹ isLb R S x"
  by (simp add: isLb_def)

lemma isGlb_le_isLb: "isGlb R S x ⟹ isLb R S y ⟹ x ≥ y"
  unfolding isGlb_def by (blast intro!: greatestPD3)

lemma isGlb_ubs: "isGlb R S x ⟹ lbs R S *<= x"
  unfolding lbs_def isGlb_def by (rule greatestPD2)

lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
  apply (frule isGlb_isLb)
  apply (frule_tac x = y in isGlb_isLb)
  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
  done

lemma bdd_above_setle: "bdd_above A ⟷ (∃a. A *<= a)"
  by (auto simp: bdd_above_def setle_def)

lemma bdd_below_setge: "bdd_below A ⟷ (∃a. a <=* A)"
  by (auto simp: bdd_below_def setge_def)

lemma isLub_cSup: 
  "(S::'a :: conditionally_complete_lattice set) ≠ {} ⟹ (∃b. S *<= b) ⟹ isLub UNIV S (Sup S)"
  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
            intro!: setgeI cSup_upper cSup_least)

lemma isGlb_cInf: 
  "(S::'a :: conditionally_complete_lattice set) ≠ {} ⟹ (∃b. b <=* S) ⟹ isGlb UNIV S (Inf S)"
  by  (auto simp add: isGlb_def setge_def greatestP_def isLb_def
            intro!: setleI cInf_lower cInf_greatest)

lemma cSup_le: "(S::'a::conditionally_complete_lattice set) ≠ {} ⟹ S *<= b ⟹ Sup S ≤ b"
  by (metis cSup_least setle_def)

lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) ≠ {} ⟹ b <=* S ⟹ Inf S ≥ b"
  by (metis cInf_greatest setge_def)

lemma cSup_bounds:
  fixes S :: "'a :: conditionally_complete_lattice set"
  shows "S ≠ {} ⟹ a <=* S ⟹ S *<= b ⟹ a ≤ Sup S ∧ Sup S ≤ b"
  using cSup_least[of S b] cSup_upper2[of _ S a]
  by (auto simp: bdd_above_setle setge_def setle_def)

lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b ⟹ (∀b'<b. ∃x∈S. b' < x) ⟹ Sup S = b"
  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)

lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) ⟹ (∀b'>b. ∃x∈S. b' > x) ⟹ Inf S = b"
  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)

text‹Use completeness of reals (supremum property) to show that any bounded sequence has a least upper bound›

lemma reals_complete: "∃X. X ∈ S ⟹ ∃Y. isUb (UNIV::real set) S Y ⟹ ∃t. isLub (UNIV :: real set) S t"
  by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)

lemma Bseq_isUb: "⋀X :: nat ⇒ real. Bseq X ⟹ ∃U. isUb (UNIV::real set) {x. ∃n. X n = x} U"
  by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)

lemma Bseq_isLub: "⋀X :: nat ⇒ real. Bseq X ⟹ ∃U. isLub (UNIV::real set) {x. ∃n. X n = x} U"
  by (blast intro: reals_complete Bseq_isUb)

lemma isLub_mono_imp_LIMSEQ:
  fixes X :: "nat ⇒ real"
  assumes u: "isLub UNIV {x. ∃n. X n = x} u" (* FIXME: use ‹range X› *)
  assumes X: "∀m n. m ≤ n ⟶ X m ≤ X n"
  shows "X ⇢ u"
proof -
  have "X ⇢ (SUP i. X i)"
    using u[THEN isLubD1] X
    by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle)
  also have "(SUP i. X i) = u"
    using isLub_cSup[of "range X"] u[THEN isLubD1]
    by (intro isLub_unique[OF _ u]) (auto simp add: image_def eq_commute)
  finally show ?thesis .
qed

lemmas real_isGlb_unique = isGlb_unique[where 'a=real]

lemma real_le_inf_subset: "t ≠ {} ⟹ t ⊆ s ⟹ ∃b. b <=* s ⟹ Inf s ≤ Inf (t::real set)"
  by (rule cInf_superset_mono) (auto simp: bdd_below_setge)

lemma real_ge_sup_subset: "t ≠ {} ⟹ t ⊆ s ⟹ ∃b. s *<= b ⟹ Sup s ≥ Sup (t::real set)"
  by (rule cSup_subset_mono) (auto simp: bdd_above_setle)

end