104 then show ?case by simp |
121 then show ?case by simp |
105 qed |
122 qed |
106 qed |
123 qed |
107 qed |
124 qed |
108 |
125 |
109 end |
126 instantiation option :: (inf) inf |
|
127 begin |
|
128 |
|
129 definition inf_option where |
|
130 "x \<sqinter> y = (case x of None \<Rightarrow> None | Some x \<Rightarrow> (case y of None \<Rightarrow> None | Some y \<Rightarrow> Some (x \<sqinter> y)))" |
|
131 |
|
132 lemma inf_None_1 [simp, code]: |
|
133 "None \<sqinter> y = None" |
|
134 by (simp add: inf_option_def) |
|
135 |
|
136 lemma inf_None_2 [simp, code]: |
|
137 "x \<sqinter> None = None" |
|
138 by (cases x) (simp_all add: inf_option_def) |
|
139 |
|
140 lemma inf_Some [simp, code]: |
|
141 "Some x \<sqinter> Some y = Some (x \<sqinter> y)" |
|
142 by (simp add: inf_option_def) |
|
143 |
|
144 instance .. |
|
145 |
|
146 end |
|
147 |
|
148 instantiation option :: (sup) sup |
|
149 begin |
|
150 |
|
151 definition sup_option where |
|
152 "x \<squnion> y = (case x of None \<Rightarrow> y | Some x' \<Rightarrow> (case y of None \<Rightarrow> x | Some y \<Rightarrow> Some (x' \<squnion> y)))" |
|
153 |
|
154 lemma sup_None_1 [simp, code]: |
|
155 "None \<squnion> y = y" |
|
156 by (simp add: sup_option_def) |
|
157 |
|
158 lemma sup_None_2 [simp, code]: |
|
159 "x \<squnion> None = x" |
|
160 by (cases x) (simp_all add: sup_option_def) |
|
161 |
|
162 lemma sup_Some [simp, code]: |
|
163 "Some x \<squnion> Some y = Some (x \<squnion> y)" |
|
164 by (simp add: sup_option_def) |
|
165 |
|
166 instance .. |
|
167 |
|
168 end |
|
169 |
|
170 instantiation option :: (semilattice_inf) semilattice_inf |
|
171 begin |
|
172 |
|
173 instance proof |
|
174 fix x y z :: "'a option" |
|
175 show "x \<sqinter> y \<le> x" |
|
176 by - (cases x, simp_all, cases y, simp_all) |
|
177 show "x \<sqinter> y \<le> y" |
|
178 by - (cases x, simp_all, cases y, simp_all) |
|
179 show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z" |
|
180 by - (cases x, simp_all, cases y, simp_all, cases z, simp_all) |
|
181 qed |
|
182 |
|
183 end |
|
184 |
|
185 instantiation option :: (semilattice_sup) semilattice_sup |
|
186 begin |
|
187 |
|
188 instance proof |
|
189 fix x y z :: "'a option" |
|
190 show "x \<le> x \<squnion> y" |
|
191 by - (cases x, simp_all, cases y, simp_all) |
|
192 show "y \<le> x \<squnion> y" |
|
193 by - (cases x, simp_all, cases y, simp_all) |
|
194 fix x y z :: "'a option" |
|
195 show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x" |
|
196 by - (cases y, simp_all, cases z, simp_all, cases x, simp_all) |
|
197 qed |
|
198 |
|
199 end |
|
200 |
|
201 instance option :: (lattice) lattice .. |
|
202 |
|
203 instance option :: (lattice) bounded_lattice_bot .. |
|
204 |
|
205 instance option :: (bounded_lattice_top) bounded_lattice_top .. |
|
206 |
|
207 instance option :: (bounded_lattice_top) bounded_lattice .. |
|
208 |
|
209 instance option :: (distrib_lattice) distrib_lattice |
|
210 proof |
|
211 fix x y z :: "'a option" |
|
212 show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
|
213 by - (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute) |
|
214 qed |
|
215 |
|
216 instantiation option :: (complete_lattice) complete_lattice |
|
217 begin |
|
218 |
|
219 definition Inf_option :: "'a option set \<Rightarrow> 'a option" where |
|
220 "\<Sqinter>A = (if None \<in> A then None else Some (\<Sqinter>Option.these A))" |
|
221 |
|
222 lemma None_in_Inf [simp]: |
|
223 "None \<in> A \<Longrightarrow> \<Sqinter>A = None" |
|
224 by (simp add: Inf_option_def) |
|
225 |
|
226 definition Sup_option :: "'a option set \<Rightarrow> 'a option" where |
|
227 "\<Squnion>A = (if A = {} \<or> A = {None} then None else Some (\<Squnion>Option.these A))" |
|
228 |
|
229 lemma empty_Sup [simp]: |
|
230 "\<Squnion>{} = None" |
|
231 by (simp add: Sup_option_def) |
|
232 |
|
233 lemma singleton_None_Sup [simp]: |
|
234 "\<Squnion>{None} = None" |
|
235 by (simp add: Sup_option_def) |
|
236 |
|
237 instance proof |
|
238 fix x :: "'a option" and A |
|
239 assume "x \<in> A" |
|
240 then show "\<Sqinter>A \<le> x" |
|
241 by (cases x) (auto simp add: Inf_option_def in_these_eq intro: Inf_lower) |
|
242 next |
|
243 fix z :: "'a option" and A |
|
244 assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" |
|
245 show "z \<le> \<Sqinter>A" |
|
246 proof (cases z) |
|
247 case None then show ?thesis by simp |
|
248 next |
|
249 case (Some y) |
|
250 show ?thesis |
|
251 by (auto simp add: Inf_option_def in_these_eq Some intro!: Inf_greatest dest!: *) |
|
252 qed |
|
253 next |
|
254 fix x :: "'a option" and A |
|
255 assume "x \<in> A" |
|
256 then show "x \<le> \<Squnion>A" |
|
257 by (cases x) (auto simp add: Sup_option_def in_these_eq intro: Sup_upper) |
|
258 next |
|
259 fix z :: "'a option" and A |
|
260 assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z" |
|
261 show "\<Squnion>A \<le> z " |
|
262 proof (cases z) |
|
263 case None |
|
264 with * have "\<And>x. x \<in> A \<Longrightarrow> x = None" by (auto dest: less_eq_option_None_is_None) |
|
265 then have "A = {} \<or> A = {None}" by blast |
|
266 then show ?thesis by (simp add: Sup_option_def) |
|
267 next |
|
268 case (Some y) |
|
269 from * have "\<And>w. Some w \<in> A \<Longrightarrow> Some w \<le> z" . |
|
270 with Some have "\<And>w. w \<in> Option.these A \<Longrightarrow> w \<le> y" |
|
271 by (simp add: in_these_eq) |
|
272 then have "\<Squnion>Option.these A \<le> y" by (rule Sup_least) |
|
273 with Some show ?thesis by (simp add: Sup_option_def) |
|
274 qed |
|
275 qed |
|
276 |
|
277 end |
|
278 |
|
279 lemma Some_Inf: |
|
280 "Some (\<Sqinter>A) = \<Sqinter>(Some ` A)" |
|
281 by (auto simp add: Inf_option_def) |
|
282 |
|
283 lemma Some_Sup: |
|
284 "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>A) = \<Squnion>(Some ` A)" |
|
285 by (auto simp add: Sup_option_def) |
|
286 |
|
287 lemma Some_INF: |
|
288 "Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))" |
|
289 by (simp add: INF_def Some_Inf image_image) |
|
290 |
|
291 lemma Some_SUP: |
|
292 "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))" |
|
293 by (simp add: SUP_def Some_Sup image_image) |
|
294 |
|
295 instantiation option :: (complete_distrib_lattice) complete_distrib_lattice |
|
296 begin |
|
297 |
|
298 instance proof |
|
299 fix a :: "'a option" and B |
|
300 show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)" |
|
301 proof (cases a) |
|
302 case None |
|
303 then show ?thesis by (simp add: INF_def) |
|
304 next |
|
305 case (Some c) |
|
306 show ?thesis |
|
307 proof (cases "None \<in> B") |
|
308 case True |
|
309 then have "Some c = (\<Sqinter>b\<in>B. Some c \<squnion> b)" |
|
310 by (auto intro!: antisym INF_lower2 INF_greatest) |
|
311 with True Some show ?thesis by simp |
|
312 next |
|
313 case False then have B: "{x \<in> B. \<exists>y. x = Some y} = B" by auto (metis not_Some_eq) |
|
314 from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b\<in>Option.these B. c \<squnion> b)" by simp |
|
315 then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x\<in>Some ` Option.these B. Some c \<squnion> x)" |
|
316 by (simp add: Some_INF Some_Inf) |
|
317 with Some B show ?thesis by (simp add: Some_image_these_eq) |
|
318 qed |
|
319 qed |
|
320 show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)" |
|
321 proof (cases a) |
|
322 case None |
|
323 then show ?thesis by (simp add: SUP_def image_constant_conv bot_option_def) |
|
324 next |
|
325 case (Some c) |
|
326 show ?thesis |
|
327 proof (cases "B = {} \<or> B = {None}") |
|
328 case True |
|
329 then show ?thesis by (auto simp add: SUP_def) |
|
330 next |
|
331 have B: "B = {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}" |
|
332 by auto |
|
333 then have Sup_B: "\<Squnion>B = \<Squnion>({x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None})" |
|
334 and SUP_B: "\<And>f. (\<Squnion>x \<in> B. f x) = (\<Squnion>x \<in> {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}. f x)" |
|
335 by simp_all |
|
336 have Sup_None: "\<Squnion>{x. x = None \<and> x \<in> B} = None" |
|
337 by (simp add: bot_option_def [symmetric]) |
|
338 have SUP_None: "(\<Squnion>x\<in>{x. x = None \<and> x \<in> B}. Some c \<sqinter> x) = None" |
|
339 by (simp add: bot_option_def [symmetric]) |
|
340 case False then have "Option.these B \<noteq> {}" by (simp add: these_not_empty_eq) |
|
341 moreover from inf_Sup have "Some c \<sqinter> Some (\<Squnion>Option.these B) = Some (\<Squnion>b\<in>Option.these B. c \<sqinter> b)" |
|
342 by simp |
|
343 ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x\<in>Some ` Option.these B. Some c \<sqinter> x)" |
|
344 by (simp add: Some_SUP Some_Sup) |
|
345 with Some show ?thesis |
|
346 by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib) |
|
347 qed |
|
348 qed |
|
349 qed |
|
350 |
|
351 end |
|
352 |
|
353 instantiation option :: (complete_linorder) complete_linorder |
|
354 begin |
|
355 |
|
356 instance .. |
|
357 |
|
358 end |
|
359 |
|
360 |
|
361 no_notation |
|
362 bot ("\<bottom>") and |
|
363 top ("\<top>") and |
|
364 inf (infixl "\<sqinter>" 70) and |
|
365 sup (infixl "\<squnion>" 65) and |
|
366 Inf ("\<Sqinter>_" [900] 900) and |
|
367 Sup ("\<Squnion>_" [900] 900) |
|
368 |
|
369 no_syntax (xsymbols) |
|
370 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
|
371 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
|
372 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
|
373 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
|
374 |
|
375 end |
|
376 |