9 begin |
9 begin |
10 |
10 |
11 text \<open>Thanks to suggestions by James Margetson\<close> |
11 text \<open>Thanks to suggestions by James Margetson\<close> |
12 |
12 |
13 definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" (infixl "*<=" 70) |
13 definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" (infixl "*<=" 70) |
14 where "S *<= x = (ALL y: S. y \<le> x)" |
14 where "S *<= x = (\<forall>y\<in>S. y \<le> x)" |
15 |
15 |
16 definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "<=*" 70) |
16 definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "<=*" 70) |
17 where "x <=* S = (ALL y: S. x \<le> y)" |
17 where "x <=* S = (\<forall>y\<in>S. x \<le> y)" |
18 |
18 |
19 |
19 |
20 subsection \<open>Rules for the Relations \<open>*<=\<close> and \<open><=*\<close>\<close> |
20 subsection \<open>Rules for the Relations \<open>*<=\<close> and \<open><=*\<close>\<close> |
21 |
21 |
22 lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x" |
22 lemma setleI: "\<forall>y\<in>S. y \<le> x \<Longrightarrow> S *<= x" |
23 by (simp add: setle_def) |
23 by (simp add: setle_def) |
24 |
24 |
25 lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x" |
25 lemma setleD: "S *<= x \<Longrightarrow> y\<in>S \<Longrightarrow> y \<le> x" |
26 by (simp add: setle_def) |
26 by (simp add: setle_def) |
27 |
27 |
28 lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S" |
28 lemma setgeI: "\<forall>y\<in>S. x \<le> y \<Longrightarrow> x <=* S" |
29 by (simp add: setge_def) |
29 by (simp add: setge_def) |
30 |
30 |
31 lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y" |
31 lemma setgeD: "x <=* S \<Longrightarrow> y\<in>S \<Longrightarrow> x \<le> y" |
32 by (simp add: setge_def) |
32 by (simp add: setge_def) |
33 |
33 |
34 |
34 |
35 definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool" |
35 definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool" |
36 where "leastP P x = (P x \<and> x <=* Collect P)" |
36 where "leastP P x = (P x \<and> x <=* Collect P)" |
37 |
37 |
38 definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
38 definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
39 where "isUb R S x = (S *<= x \<and> x: R)" |
39 where "isUb R S x = (S *<= x \<and> x \<in> R)" |
40 |
40 |
41 definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
41 definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
42 where "isLub R S x = leastP (isUb R S) x" |
42 where "isLub R S x = leastP (isUb R S) x" |
43 |
43 |
44 definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set" |
44 definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set" |
51 by (simp add: leastP_def) |
51 by (simp add: leastP_def) |
52 |
52 |
53 lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P" |
53 lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P" |
54 by (simp add: leastP_def) |
54 by (simp add: leastP_def) |
55 |
55 |
56 lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y" |
56 lemma leastPD3: "leastP P x \<Longrightarrow> y \<in> Collect P \<Longrightarrow> x \<le> y" |
57 by (blast dest!: leastPD2 setgeD) |
57 by (blast dest!: leastPD2 setgeD) |
58 |
58 |
59 lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x" |
59 lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x" |
60 by (simp add: isLub_def isUb_def leastP_def) |
60 by (simp add: isLub_def isUb_def leastP_def) |
61 |
61 |
62 lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R" |
62 lemma isLubD1a: "isLub R S x \<Longrightarrow> x \<in> R" |
63 by (simp add: isLub_def isUb_def leastP_def) |
63 by (simp add: isLub_def isUb_def leastP_def) |
64 |
64 |
65 lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x" |
65 lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x" |
66 unfolding isUb_def by (blast dest: isLubD1 isLubD1a) |
66 unfolding isUb_def by (blast dest: isLubD1 isLubD1a) |
67 |
67 |
68 lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x" |
68 lemma isLubD2: "isLub R S x \<Longrightarrow> y \<in> S \<Longrightarrow> y \<le> x" |
69 by (blast dest!: isLubD1 setleD) |
69 by (blast dest!: isLubD1 setleD) |
70 |
70 |
71 lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x" |
71 lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x" |
72 by (simp add: isLub_def) |
72 by (simp add: isLub_def) |
73 |
73 |
75 by (simp add: isLub_def) |
75 by (simp add: isLub_def) |
76 |
76 |
77 lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x" |
77 lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x" |
78 by (simp add: isLub_def leastP_def) |
78 by (simp add: isLub_def leastP_def) |
79 |
79 |
80 lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x" |
80 lemma isUbD: "isUb R S x \<Longrightarrow> y \<in> S \<Longrightarrow> y \<le> x" |
81 by (simp add: isUb_def setle_def) |
81 by (simp add: isUb_def setle_def) |
82 |
82 |
83 lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x" |
83 lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x" |
84 by (simp add: isUb_def) |
84 by (simp add: isUb_def) |
85 |
85 |
86 lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R" |
86 lemma isUbD2a: "isUb R S x \<Longrightarrow> x \<in> R" |
87 by (simp add: isUb_def) |
87 by (simp add: isUb_def) |
88 |
88 |
89 lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x" |
89 lemma isUbI: "S *<= x \<Longrightarrow> x \<in> R \<Longrightarrow> isUb R S x" |
90 by (simp add: isUb_def) |
90 by (simp add: isUb_def) |
91 |
91 |
92 lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y" |
92 lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y" |
93 unfolding isLub_def by (blast intro!: leastPD3) |
93 unfolding isLub_def by (blast intro!: leastPD3) |
94 |
94 |
107 |
107 |
108 definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool" |
108 definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool" |
109 where "greatestP P x = (P x \<and> Collect P *<= x)" |
109 where "greatestP P x = (P x \<and> Collect P *<= x)" |
110 |
110 |
111 definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
111 definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
112 where "isLb R S x = (x <=* S \<and> x: R)" |
112 where "isLb R S x = (x <=* S \<and> x \<in> R)" |
113 |
113 |
114 definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
114 definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
115 where "isGlb R S x = greatestP (isLb R S) x" |
115 where "isGlb R S x = greatestP (isLb R S) x" |
116 |
116 |
117 definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set" |
117 definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set" |
124 by (simp add: greatestP_def) |
124 by (simp add: greatestP_def) |
125 |
125 |
126 lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x" |
126 lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x" |
127 by (simp add: greatestP_def) |
127 by (simp add: greatestP_def) |
128 |
128 |
129 lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y" |
129 lemma greatestPD3: "greatestP P x \<Longrightarrow> y \<in> Collect P \<Longrightarrow> x \<ge> y" |
130 by (blast dest!: greatestPD2 setleD) |
130 by (blast dest!: greatestPD2 setleD) |
131 |
131 |
132 lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S" |
132 lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S" |
133 by (simp add: isGlb_def isLb_def greatestP_def) |
133 by (simp add: isGlb_def isLb_def greatestP_def) |
134 |
134 |
135 lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R" |
135 lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x \<in> R" |
136 by (simp add: isGlb_def isLb_def greatestP_def) |
136 by (simp add: isGlb_def isLb_def greatestP_def) |
137 |
137 |
138 lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x" |
138 lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x" |
139 unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a) |
139 unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a) |
140 |
140 |
141 lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x" |
141 lemma isGlbD2: "isGlb R S x \<Longrightarrow> y \<in> S \<Longrightarrow> y \<ge> x" |
142 by (blast dest!: isGlbD1 setgeD) |
142 by (blast dest!: isGlbD1 setgeD) |
143 |
143 |
144 lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x" |
144 lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x" |
145 by (simp add: isGlb_def) |
145 by (simp add: isGlb_def) |
146 |
146 |
148 by (simp add: isGlb_def) |
148 by (simp add: isGlb_def) |
149 |
149 |
150 lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x" |
150 lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x" |
151 by (simp add: isGlb_def greatestP_def) |
151 by (simp add: isGlb_def greatestP_def) |
152 |
152 |
153 lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x" |
153 lemma isLbD: "isLb R S x \<Longrightarrow> y \<in> S \<Longrightarrow> y \<ge> x" |
154 by (simp add: isLb_def setge_def) |
154 by (simp add: isLb_def setge_def) |
155 |
155 |
156 lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S " |
156 lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S " |
157 by (simp add: isLb_def) |
157 by (simp add: isLb_def) |
158 |
158 |
159 lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R" |
159 lemma isLbD2a: "isLb R S x \<Longrightarrow> x \<in> R" |
160 by (simp add: isLb_def) |
160 by (simp add: isLb_def) |
161 |
161 |
162 lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x" |
162 lemma isLbI: "x <=* S \<Longrightarrow> x \<in> R \<Longrightarrow> isLb R S x" |
163 by (simp add: isLb_def) |
163 by (simp add: isLb_def) |
164 |
164 |
165 lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y" |
165 lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y" |
166 unfolding isGlb_def by (blast intro!: greatestPD3) |
166 unfolding isGlb_def by (blast intro!: greatestPD3) |
167 |
167 |