(* 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.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
