# Theory Lubs

Up to index of Isabelle/HOL

theory Lubs
imports Main
`(*  Title:      HOL/Lubs.thy    Author:     Jacques D. Fleuriot, University of Cambridge*)header {* Definitions of Upper Bounds and Least Upper Bounds *}theory Lubsimports Mainbegintext {* Thanks to suggestions by James Margetson *}definition setle :: "'a set => 'a::ord => bool"  (infixl "*<=" 70)  where "S *<= x = (ALL y: S. y ≤ x)"definition setge :: "'a::ord => 'a set => bool"  (infixl "<=*" 70)  where "x <=* S = (ALL y: S. x ≤ y)"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 for the Relations @{text "*<="} and @{text "<=*"} *}lemma setleI: "ALL 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: "ALL y: S. x ≤ y ==> x <=* S"  by (simp add: setge_def)lemma setgeD: "x <=* S ==> y: S ==> x ≤ y"  by (simp add: setge_def)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)end`