src/HOL/Library/Glbs.thy
 author bulwahn Tue Apr 05 09:38:28 2011 +0200 (2011-04-05) changeset 42231 bc1891226d00 parent 30661 54858c8ad226 child 46509 c4b2ec379fdd permissions -rw-r--r--
removing bounded_forall code equation for characters when loading Code_Char
1 (* Author: Amine Chaieb, University of Cambridge *)
3 header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}
5 theory Glbs
6 imports Lubs
7 begin
9 definition
10   greatestP      :: "['a =>bool,'a::ord] => bool" where
11   "greatestP P x = (P x & Collect P *<=  x)"
13 definition
14   isLb        :: "['a set, 'a set, 'a::ord] => bool" where
15   "isLb R S x = (x <=* S & x: R)"
17 definition
18   isGlb       :: "['a set, 'a set, 'a::ord] => bool" where
19   "isGlb R S x = greatestP (isLb R S) x"
21 definition
22   lbs         :: "['a set, 'a::ord set] => 'a set" where
23   "lbs R S = Collect (isLb R S)"
25 subsection{*Rules about the Operators @{term greatestP}, @{term isLb}
26     and @{term isGlb}*}
28 lemma leastPD1: "greatestP P x ==> P x"
29 by (simp add: greatestP_def)
31 lemma greatestPD2: "greatestP P x ==> Collect P *<= x"
32 by (simp add: greatestP_def)
34 lemma greatestPD3: "[| greatestP P x; y: Collect P |] ==> x >= y"
35 by (blast dest!: greatestPD2 setleD)
37 lemma isGlbD1: "isGlb R S x ==> x <=* S"
38 by (simp add: isGlb_def isLb_def greatestP_def)
40 lemma isGlbD1a: "isGlb R S x ==> x: R"
41 by (simp add: isGlb_def isLb_def greatestP_def)
43 lemma isGlb_isLb: "isGlb R S x ==> isLb R S x"
44 apply (simp add: isLb_def)
45 apply (blast dest: isGlbD1 isGlbD1a)
46 done
48 lemma isGlbD2: "[| isGlb R S x; y : S |] ==> y >= x"
49 by (blast dest!: isGlbD1 setgeD)
51 lemma isGlbD3: "isGlb R S x ==> greatestP(isLb R S) x"
52 by (simp add: isGlb_def)
54 lemma isGlbI1: "greatestP(isLb R S) x ==> isGlb R S x"
55 by (simp add: isGlb_def)
57 lemma isGlbI2: "[| isLb R S x; Collect (isLb R S) *<= x |] ==> isGlb R S x"
58 by (simp add: isGlb_def greatestP_def)
60 lemma isLbD: "[| isLb R S x; y : S |] ==> y >= x"
61 by (simp add: isLb_def setge_def)
63 lemma isLbD2: "isLb R S x ==> x <=* S "
64 by (simp add: isLb_def)
66 lemma isLbD2a: "isLb R S x ==> x: R"
67 by (simp add: isLb_def)
69 lemma isLbI: "[| x <=* S ; x: R |] ==> isLb R S x"
70 by (simp add: isLb_def)
72 lemma isGlb_le_isLb: "[| isGlb R S x; isLb R S y |] ==> x >= y"
73 apply (simp add: isGlb_def)
74 apply (blast intro!: greatestPD3)
75 done
77 lemma isGlb_ubs: "isGlb R S x ==> lbs R S *<= x"
78 apply (simp add: lbs_def isGlb_def)
79 apply (erule greatestPD2)
80 done
82 end