(* Title : Lubs.thy ID : $Id: Lubs.thy,v 1.8 2004/08/18 09:10:05 nipkow Exp $ Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge *) header{*Definitions of Upper Bounds and Least Upper Bounds*} theory Lubs imports Main begin text{*Thanks to suggestions by James Margetson*} constdefs setle :: "['a set, 'a::ord] => bool" (infixl "*<=" 70) "S *<= x == (ALL y: S. y <= x)" setge :: "['a::ord, 'a set] => bool" (infixl "<=*" 70) "x <=* S == (ALL y: S. x <= y)" leastP :: "['a =>bool,'a::ord] => bool" "leastP P x == (P x & x <=* Collect P)" isUb :: "['a set, 'a set, 'a::ord] => bool" "isUb R S x == S *<= x & x: R" isLub :: "['a set, 'a set, 'a::ord] => bool" "isLub R S x == leastP (isUb R S) x" ubs :: "['a set, 'a::ord set] => 'a set" "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" apply (simp add: isUb_def) apply (blast dest: isLubD1 isLubD1a) done 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" apply (simp add: isLub_def) apply (blast intro!: leastPD3) done lemma isLub_ubs: "isLub R S x ==> x <=* ubs R S" apply (simp add: ubs_def isLub_def) apply (erule leastPD2) done ML {* val setle_def = thm "setle_def"; val setge_def = thm "setge_def"; val leastP_def = thm "leastP_def"; val isLub_def = thm "isLub_def"; val isUb_def = thm "isUb_def"; val ubs_def = thm "ubs_def"; val setleI = thm "setleI"; val setleD = thm "setleD"; val setgeI = thm "setgeI"; val setgeD = thm "setgeD"; val leastPD1 = thm "leastPD1"; val leastPD2 = thm "leastPD2"; val leastPD3 = thm "leastPD3"; val isLubD1 = thm "isLubD1"; val isLubD1a = thm "isLubD1a"; val isLub_isUb = thm "isLub_isUb"; val isLubD2 = thm "isLubD2"; val isLubD3 = thm "isLubD3"; val isLubI1 = thm "isLubI1"; val isLubI2 = thm "isLubI2"; val isUbD = thm "isUbD"; val isUbD2 = thm "isUbD2"; val isUbD2a = thm "isUbD2a"; val isUbI = thm "isUbI"; val isLub_le_isUb = thm "isLub_le_isUb"; val isLub_ubs = thm "isLub_ubs"; *} end
lemma setleI:
∀y∈S. y ≤ x ==> S *<= x
lemma setleD:
[| S *<= x; y ∈ S |] ==> y ≤ x
lemma setgeI:
∀y∈S. x ≤ y ==> x <=* S
lemma setgeD:
[| x <=* S; y ∈ S |] ==> x ≤ y
lemma leastPD1:
leastP P x ==> P x
lemma leastPD2:
leastP P x ==> x <=* Collect P
lemma leastPD3:
[| leastP P x; y ∈ Collect P |] ==> x ≤ y
lemma isLubD1:
isLub R S x ==> S *<= x
lemma isLubD1a:
isLub R S x ==> x ∈ R
lemma isLub_isUb:
isLub R S x ==> isUb R S x
lemma isLubD2:
[| isLub R S x; y ∈ S |] ==> y ≤ x
lemma isLubD3:
isLub R S x ==> leastP (isUb R S) x
lemma isLubI1:
leastP (isUb R S) x ==> isLub R S x
lemma isLubI2:
[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x
lemma isUbD:
[| isUb R S x; y ∈ S |] ==> y ≤ x
lemma isUbD2:
isUb R S x ==> S *<= x
lemma isUbD2a:
isUb R S x ==> x ∈ R
lemma isUbI:
[| S *<= x; x ∈ R |] ==> isUb R S x
lemma isLub_le_isUb:
[| isLub R S x; isUb R S y |] ==> x ≤ y
lemma isLub_ubs:
isLub R S x ==> x <=* ubs R S