src/HOL/Lubs.thy
changeset 28952 15a4b2cf8c34
parent 27368 9f90ac19e32b
child 29654 24e73987bfe2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Lubs.thy	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -0,0 +1,113 @@
     1.4 +(*  Title       : Lubs.thy
     1.5 +    ID          : $Id$
     1.6 +    Author      : Jacques D. Fleuriot
     1.7 +    Copyright   : 1998  University of Cambridge
     1.8 +*)
     1.9 +
    1.10 +header{*Definitions of Upper Bounds and Least Upper Bounds*}
    1.11 +
    1.12 +theory Lubs
    1.13 +imports Plain
    1.14 +begin
    1.15 +
    1.16 +text{*Thanks to suggestions by James Margetson*}
    1.17 +
    1.18 +definition
    1.19 +  setle :: "['a set, 'a::ord] => bool"  (infixl "*<=" 70) where
    1.20 +  "S *<= x = (ALL y: S. y <= x)"
    1.21 +
    1.22 +definition
    1.23 +  setge :: "['a::ord, 'a set] => bool"  (infixl "<=*" 70) where
    1.24 +  "x <=* S = (ALL y: S. x <= y)"
    1.25 +
    1.26 +definition
    1.27 +  leastP      :: "['a =>bool,'a::ord] => bool" where
    1.28 +  "leastP P x = (P x & x <=* Collect P)"
    1.29 +
    1.30 +definition
    1.31 +  isUb        :: "['a set, 'a set, 'a::ord] => bool" where
    1.32 +  "isUb R S x = (S *<= x & x: R)"
    1.33 +
    1.34 +definition
    1.35 +  isLub       :: "['a set, 'a set, 'a::ord] => bool" where
    1.36 +  "isLub R S x = leastP (isUb R S) x"
    1.37 +
    1.38 +definition
    1.39 +  ubs         :: "['a set, 'a::ord set] => 'a set" where
    1.40 +  "ubs R S = Collect (isUb R S)"
    1.41 +
    1.42 +
    1.43 +
    1.44 +subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*}
    1.45 +
    1.46 +lemma setleI: "ALL y: S. y <= x ==> S *<= x"
    1.47 +by (simp add: setle_def)
    1.48 +
    1.49 +lemma setleD: "[| S *<= x; y: S |] ==> y <= x"
    1.50 +by (simp add: setle_def)
    1.51 +
    1.52 +lemma setgeI: "ALL y: S. x<= y ==> x <=* S"
    1.53 +by (simp add: setge_def)
    1.54 +
    1.55 +lemma setgeD: "[| x <=* S; y: S |] ==> x <= y"
    1.56 +by (simp add: setge_def)
    1.57 +
    1.58 +
    1.59 +subsection{*Rules about the Operators @{term leastP}, @{term ub}
    1.60 +    and @{term lub}*}
    1.61 +
    1.62 +lemma leastPD1: "leastP P x ==> P x"
    1.63 +by (simp add: leastP_def)
    1.64 +
    1.65 +lemma leastPD2: "leastP P x ==> x <=* Collect P"
    1.66 +by (simp add: leastP_def)
    1.67 +
    1.68 +lemma leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y"
    1.69 +by (blast dest!: leastPD2 setgeD)
    1.70 +
    1.71 +lemma isLubD1: "isLub R S x ==> S *<= x"
    1.72 +by (simp add: isLub_def isUb_def leastP_def)
    1.73 +
    1.74 +lemma isLubD1a: "isLub R S x ==> x: R"
    1.75 +by (simp add: isLub_def isUb_def leastP_def)
    1.76 +
    1.77 +lemma isLub_isUb: "isLub R S x ==> isUb R S x"
    1.78 +apply (simp add: isUb_def)
    1.79 +apply (blast dest: isLubD1 isLubD1a)
    1.80 +done
    1.81 +
    1.82 +lemma isLubD2: "[| isLub R S x; y : S |] ==> y <= x"
    1.83 +by (blast dest!: isLubD1 setleD)
    1.84 +
    1.85 +lemma isLubD3: "isLub R S x ==> leastP(isUb R S) x"
    1.86 +by (simp add: isLub_def)
    1.87 +
    1.88 +lemma isLubI1: "leastP(isUb R S) x ==> isLub R S x"
    1.89 +by (simp add: isLub_def)
    1.90 +
    1.91 +lemma isLubI2: "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"
    1.92 +by (simp add: isLub_def leastP_def)
    1.93 +
    1.94 +lemma isUbD: "[| isUb R S x; y : S |] ==> y <= x"
    1.95 +by (simp add: isUb_def setle_def)
    1.96 +
    1.97 +lemma isUbD2: "isUb R S x ==> S *<= x"
    1.98 +by (simp add: isUb_def)
    1.99 +
   1.100 +lemma isUbD2a: "isUb R S x ==> x: R"
   1.101 +by (simp add: isUb_def)
   1.102 +
   1.103 +lemma isUbI: "[| S *<= x; x: R |] ==> isUb R S x"
   1.104 +by (simp add: isUb_def)
   1.105 +
   1.106 +lemma isLub_le_isUb: "[| isLub R S x; isUb R S y |] ==> x <= y"
   1.107 +apply (simp add: isLub_def)
   1.108 +apply (blast intro!: leastPD3)
   1.109 +done
   1.110 +
   1.111 +lemma isLub_ubs: "isLub R S x ==> x <=* ubs R S"
   1.112 +apply (simp add: ubs_def isLub_def)
   1.113 +apply (erule leastPD2)
   1.114 +done
   1.115 +
   1.116 +end