Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Lub_Glb.thy Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>Definitions of Least Upper Bounds and Greatest Lower Bounds\<close>

theory Lub_Glb
imports Complex_Main
begin

text \<open>Thanks to suggestions by James Margetson\<close>

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 \<open>Rules for the Relations \<open>*<=\<close> and \<open><=*\<close>\<close>

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 \<open>Rules about the Operators \<^term>\<open>leastP\<close>, \<^term>\<open>ub\<close> and \<^term>\<open>lub\<close>\<close>

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 \<open>Rules about the Operators \<^term>\<open>greatestP\<close>, \<^term>\<open>isLb\<close> and \<^term>\<open>isGlb\<close>\<close>

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'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\<open>Use completeness of reals (supremum property) to show that any bounded sequence has a least upper bound\<close>

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

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.