1 (* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *) |
1 (* Title: HOL/Complete_Lattices.thy |
|
2 Author: Tobias Nipkow |
|
3 Author: Lawrence C Paulson |
|
4 Author: Markus Wenzel |
|
5 Author: Florian Haftmann |
|
6 *) |
2 |
7 |
3 section \<open>Complete lattices\<close> |
8 section \<open>Complete lattices\<close> |
4 |
9 |
5 theory Complete_Lattices |
10 theory Complete_Lattices |
6 imports Fun |
11 imports Fun |
7 begin |
12 begin |
8 |
13 |
9 notation |
14 notation |
10 less_eq (infix "\<sqsubseteq>" 50) and |
15 less_eq (infix "\<sqsubseteq>" 50) and |
11 less (infix "\<sqsubset>" 50) |
16 less (infix "\<sqsubset>" 50) |
12 |
17 |
13 |
18 |
14 subsection \<open>Syntactic infimum and supremum operations\<close> |
19 subsection \<open>Syntactic infimum and supremum operations\<close> |
15 |
20 |
16 class Inf = |
21 class Inf = |
17 fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900) |
22 fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900) |
18 begin |
23 begin |
19 |
24 |
20 abbreviation INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" |
25 abbreviation INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" |
21 where |
26 where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)" |
22 "INFIMUM A f \<equiv> \<Sqinter>(f ` A)" |
27 |
23 |
28 lemma INF_image [simp]: "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)" |
24 lemma INF_image [simp]: |
|
25 "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)" |
|
26 by (simp add: image_comp) |
29 by (simp add: image_comp) |
27 |
30 |
28 lemma INF_identity_eq [simp]: |
31 lemma INF_identity_eq [simp]: "INFIMUM A (\<lambda>x. x) = \<Sqinter>A" |
29 "INFIMUM A (\<lambda>x. x) = \<Sqinter>A" |
|
30 by simp |
32 by simp |
31 |
33 |
32 lemma INF_id_eq [simp]: |
34 lemma INF_id_eq [simp]: "INFIMUM A id = \<Sqinter>A" |
33 "INFIMUM A id = \<Sqinter>A" |
|
34 by simp |
35 by simp |
35 |
36 |
36 lemma INF_cong: |
37 lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D" |
37 "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D" |
|
38 by (simp add: image_def) |
38 by (simp add: image_def) |
39 |
39 |
40 lemma strong_INF_cong [cong]: |
40 lemma strong_INF_cong [cong]: |
41 "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D" |
41 "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D" |
42 unfolding simp_implies_def by (fact INF_cong) |
42 unfolding simp_implies_def by (fact INF_cong) |
43 |
43 |
44 end |
44 end |
45 |
45 |
46 class Sup = |
46 class Sup = |
47 fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900) |
47 fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900) |
48 begin |
48 begin |
49 |
49 |
50 abbreviation SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" |
50 abbreviation SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" |
51 where |
51 where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)" |
52 "SUPREMUM A f \<equiv> \<Squnion>(f ` A)" |
52 |
53 |
53 lemma SUP_image [simp]: "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)" |
54 lemma SUP_image [simp]: |
|
55 "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)" |
|
56 by (simp add: image_comp) |
54 by (simp add: image_comp) |
57 |
55 |
58 lemma SUP_identity_eq [simp]: |
56 lemma SUP_identity_eq [simp]: "SUPREMUM A (\<lambda>x. x) = \<Squnion>A" |
59 "SUPREMUM A (\<lambda>x. x) = \<Squnion>A" |
|
60 by simp |
57 by simp |
61 |
58 |
62 lemma SUP_id_eq [simp]: |
59 lemma SUP_id_eq [simp]: "SUPREMUM A id = \<Squnion>A" |
63 "SUPREMUM A id = \<Squnion>A" |
|
64 by (simp add: id_def) |
60 by (simp add: id_def) |
65 |
61 |
66 lemma SUP_cong: |
62 lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D" |
67 "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D" |
|
68 by (simp add: image_def) |
63 by (simp add: image_def) |
69 |
64 |
70 lemma strong_SUP_cong [cong]: |
65 lemma strong_SUP_cong [cong]: |
71 "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D" |
66 "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D" |
72 unfolding simp_implies_def by (fact SUP_cong) |
67 unfolding simp_implies_def by (fact SUP_cong) |
120 along with assumptions that define bottom and top |
115 along with assumptions that define bottom and top |
121 in terms of infimum and supremum.\<close> |
116 in terms of infimum and supremum.\<close> |
122 |
117 |
123 class complete_lattice = lattice + Inf + Sup + bot + top + |
118 class complete_lattice = lattice + Inf + Sup + bot + top + |
124 assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x" |
119 assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x" |
125 and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A" |
120 and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A" |
126 assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A" |
121 and Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A" |
127 and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z" |
122 and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z" |
128 assumes Inf_empty [simp]: "\<Sqinter>{} = \<top>" |
123 and Inf_empty [simp]: "\<Sqinter>{} = \<top>" |
129 assumes Sup_empty [simp]: "\<Squnion>{} = \<bottom>" |
124 and Sup_empty [simp]: "\<Squnion>{} = \<bottom>" |
130 begin |
125 begin |
131 |
126 |
132 subclass bounded_lattice |
127 subclass bounded_lattice |
133 proof |
128 proof |
134 fix a |
129 fix a |
135 show "\<bottom> \<le> a" by (auto intro: Sup_least simp only: Sup_empty [symmetric]) |
130 show "\<bottom> \<le> a" |
136 show "a \<le> \<top>" by (auto intro: Inf_greatest simp only: Inf_empty [symmetric]) |
131 by (auto intro: Sup_least simp only: Sup_empty [symmetric]) |
137 qed |
132 show "a \<le> \<top>" |
138 |
133 by (auto intro: Inf_greatest simp only: Inf_empty [symmetric]) |
139 lemma dual_complete_lattice: |
134 qed |
140 "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>" |
135 |
|
136 lemma dual_complete_lattice: "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>" |
141 by (auto intro!: class.complete_lattice.intro dual_lattice) |
137 by (auto intro!: class.complete_lattice.intro dual_lattice) |
142 (unfold_locales, (fact Inf_empty Sup_empty |
138 (unfold_locales, (fact Inf_empty Sup_empty Sup_upper Sup_least Inf_lower Inf_greatest)+) |
143 Sup_upper Sup_least Inf_lower Inf_greatest)+) |
|
144 |
139 |
145 end |
140 end |
146 |
141 |
147 context complete_lattice |
142 context complete_lattice |
148 begin |
143 begin |
313 by (auto intro: Sup_least Sup_upper) |
302 by (auto intro: Sup_least Sup_upper) |
314 |
303 |
315 lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B" |
304 lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B" |
316 by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2) |
305 by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2) |
317 |
306 |
318 lemma INF_union: |
307 lemma INF_union: "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)" |
319 "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)" |
|
320 by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower) |
308 by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower) |
321 |
309 |
322 lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B" |
310 lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B" |
323 by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2) |
311 by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2) |
324 |
312 |
325 lemma SUP_union: |
313 lemma SUP_union: "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)" |
326 "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)" |
|
327 by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper) |
314 by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper) |
328 |
315 |
329 lemma INF_inf_distrib: "(\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)" |
316 lemma INF_inf_distrib: "(\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)" |
330 by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono) |
317 by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono) |
331 |
318 |
332 lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)" (is "?L = ?R") |
319 lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)" |
|
320 (is "?L = ?R") |
333 proof (rule antisym) |
321 proof (rule antisym) |
334 show "?L \<le> ?R" by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono) |
322 show "?L \<le> ?R" |
335 next |
323 by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono) |
336 show "?R \<le> ?L" by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper) |
324 show "?R \<le> ?L" |
|
325 by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper) |
337 qed |
326 qed |
338 |
327 |
339 lemma Inf_top_conv [simp]: |
328 lemma Inf_top_conv [simp]: |
340 "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" |
329 "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" |
341 "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" |
330 "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" |
406 proof - |
395 proof - |
407 from assms obtain J where "I = insert k J" by blast |
396 from assms obtain J where "I = insert k J" by blast |
408 then show ?thesis by simp |
397 then show ?thesis by simp |
409 qed |
398 qed |
410 |
399 |
411 lemma INF_inf_const1: |
400 lemma INF_inf_const1: "I \<noteq> {} \<Longrightarrow> (INF i:I. inf x (f i)) = inf x (INF i:I. f i)" |
412 "I \<noteq> {} \<Longrightarrow> (INF i:I. inf x (f i)) = inf x (INF i:I. f i)" |
|
413 by (intro antisym INF_greatest inf_mono order_refl INF_lower) |
401 by (intro antisym INF_greatest inf_mono order_refl INF_lower) |
414 (auto intro: INF_lower2 le_infI2 intro!: INF_mono) |
402 (auto intro: INF_lower2 le_infI2 intro!: INF_mono) |
415 |
403 |
416 lemma INF_inf_const2: |
404 lemma INF_inf_const2: "I \<noteq> {} \<Longrightarrow> (INF i:I. inf (f i) x) = inf (INF i:I. f i) x" |
417 "I \<noteq> {} \<Longrightarrow> (INF i:I. inf (f i) x) = inf (INF i:I. f i) x" |
|
418 using INF_inf_const1[of I x f] by (simp add: inf_commute) |
405 using INF_inf_const1[of I x f] by (simp add: inf_commute) |
419 |
406 |
420 lemma INF_constant: |
407 lemma INF_constant: "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)" |
421 "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)" |
|
422 by simp |
408 by simp |
423 |
409 |
424 lemma SUP_constant: |
410 lemma SUP_constant: "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)" |
425 "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)" |
|
426 by simp |
411 by simp |
427 |
412 |
428 lemma less_INF_D: |
413 lemma less_INF_D: |
429 assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i" |
414 assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" |
|
415 shows "y < f i" |
430 proof - |
416 proof - |
431 note \<open>y < (\<Sqinter>i\<in>A. f i)\<close> |
417 note \<open>y < (\<Sqinter>i\<in>A. f i)\<close> |
432 also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using \<open>i \<in> A\<close> |
418 also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using \<open>i \<in> A\<close> |
433 by (rule INF_lower) |
419 by (rule INF_lower) |
434 finally show "y < f i" . |
420 finally show "y < f i" . |
435 qed |
421 qed |
436 |
422 |
437 lemma SUP_lessD: |
423 lemma SUP_lessD: |
438 assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y" |
424 assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" |
|
425 shows "f i < y" |
439 proof - |
426 proof - |
440 have "f i \<le> (\<Squnion>i\<in>A. f i)" using \<open>i \<in> A\<close> |
427 have "f i \<le> (\<Squnion>i\<in>A. f i)" |
441 by (rule SUP_upper) |
428 using \<open>i \<in> A\<close> by (rule SUP_upper) |
442 also note \<open>(\<Squnion>i\<in>A. f i) < y\<close> |
429 also note \<open>(\<Squnion>i\<in>A. f i) < y\<close> |
443 finally show "f i < y" . |
430 finally show "f i < y" . |
444 qed |
431 qed |
445 |
432 |
446 lemma INF_UNIV_bool_expand: |
433 lemma INF_UNIV_bool_expand: "(\<Sqinter>b. A b) = A True \<sqinter> A False" |
447 "(\<Sqinter>b. A b) = A True \<sqinter> A False" |
|
448 by (simp add: UNIV_bool inf_commute) |
434 by (simp add: UNIV_bool inf_commute) |
449 |
435 |
450 lemma SUP_UNIV_bool_expand: |
436 lemma SUP_UNIV_bool_expand: "(\<Squnion>b. A b) = A True \<squnion> A False" |
451 "(\<Squnion>b. A b) = A True \<squnion> A False" |
|
452 by (simp add: UNIV_bool sup_commute) |
437 by (simp add: UNIV_bool sup_commute) |
453 |
438 |
454 lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A" |
439 lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A" |
455 by (blast intro: Sup_upper2 Inf_lower ex_in_conv) |
440 by (blast intro: Sup_upper2 Inf_lower ex_in_conv) |
456 |
441 |
457 lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFIMUM A f \<le> SUPREMUM A f" |
442 lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFIMUM A f \<le> SUPREMUM A f" |
458 using Inf_le_Sup [of "f ` A"] by simp |
443 using Inf_le_Sup [of "f ` A"] by simp |
459 |
444 |
460 lemma INF_eq_const: |
445 lemma INF_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x" |
461 "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x" |
|
462 by (auto intro: INF_eqI) |
446 by (auto intro: INF_eqI) |
463 |
447 |
464 lemma SUP_eq_const: |
448 lemma SUP_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x" |
465 "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x" |
|
466 by (auto intro: SUP_eqI) |
449 by (auto intro: SUP_eqI) |
467 |
450 |
468 lemma INF_eq_iff: |
451 lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> INFIMUM I f = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)" |
469 "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> (INFIMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)" |
|
470 using INF_eq_const [of I f c] INF_lower [of _ I f] |
452 using INF_eq_const [of I f c] INF_lower [of _ I f] |
471 by (auto intro: antisym cong del: strong_INF_cong) |
453 by (auto intro: antisym cong del: strong_INF_cong) |
472 |
454 |
473 lemma SUP_eq_iff: |
455 lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> SUPREMUM I f = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)" |
474 "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPREMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)" |
|
475 using SUP_eq_const [of I f c] SUP_upper [of _ I f] |
456 using SUP_eq_const [of I f c] SUP_upper [of _ I f] |
476 by (auto intro: antisym cong del: strong_SUP_cong) |
457 by (auto intro: antisym cong del: strong_SUP_cong) |
477 |
458 |
478 end |
459 end |
479 |
460 |
480 class complete_distrib_lattice = complete_lattice + |
461 class complete_distrib_lattice = complete_lattice + |
481 assumes sup_Inf: "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)" |
462 assumes sup_Inf: "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)" |
482 assumes inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)" |
463 and inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)" |
483 begin |
464 begin |
484 |
465 |
485 lemma sup_INF: |
466 lemma sup_INF: "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)" |
486 "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)" |
|
487 by (simp add: sup_Inf) |
467 by (simp add: sup_Inf) |
488 |
468 |
489 lemma inf_SUP: |
469 lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)" |
490 "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)" |
|
491 by (simp add: inf_Sup) |
470 by (simp add: inf_Sup) |
492 |
471 |
493 lemma dual_complete_distrib_lattice: |
472 lemma dual_complete_distrib_lattice: |
494 "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>" |
473 "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>" |
495 apply (rule class.complete_distrib_lattice.intro) |
474 apply (rule class.complete_distrib_lattice.intro) |
496 apply (fact dual_complete_lattice) |
475 apply (fact dual_complete_lattice) |
497 apply (rule class.complete_distrib_lattice_axioms.intro) |
476 apply (rule class.complete_distrib_lattice_axioms.intro) |
498 apply (simp_all add: inf_Sup sup_Inf) |
477 apply (simp_all add: inf_Sup sup_Inf) |
499 done |
478 done |
500 |
479 |
501 subclass distrib_lattice proof |
480 subclass distrib_lattice |
|
481 proof |
502 fix a b c |
482 fix a b c |
503 from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" . |
483 have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" by (rule sup_Inf) |
504 then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by simp |
484 then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by simp |
505 qed |
485 qed |
506 |
486 |
507 lemma Inf_sup: |
487 lemma Inf_sup: "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)" |
508 "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)" |
|
509 by (simp add: sup_Inf sup_commute) |
488 by (simp add: sup_Inf sup_commute) |
510 |
489 |
511 lemma Sup_inf: |
490 lemma Sup_inf: "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)" |
512 "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)" |
|
513 by (simp add: inf_Sup inf_commute) |
491 by (simp add: inf_Sup inf_commute) |
514 |
492 |
515 lemma INF_sup: |
493 lemma INF_sup: "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)" |
516 "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)" |
|
517 by (simp add: sup_INF sup_commute) |
494 by (simp add: sup_INF sup_commute) |
518 |
495 |
519 lemma SUP_inf: |
496 lemma SUP_inf: "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)" |
520 "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)" |
|
521 by (simp add: inf_SUP inf_commute) |
497 by (simp add: inf_SUP inf_commute) |
522 |
498 |
523 lemma Inf_sup_eq_top_iff: |
499 lemma Inf_sup_eq_top_iff: "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)" |
524 "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)" |
|
525 by (simp only: Inf_sup INF_top_conv) |
500 by (simp only: Inf_sup INF_top_conv) |
526 |
501 |
527 lemma Sup_inf_eq_bot_iff: |
502 lemma Sup_inf_eq_bot_iff: "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)" |
528 "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)" |
|
529 by (simp only: Sup_inf SUP_bot_conv) |
503 by (simp only: Sup_inf SUP_bot_conv) |
530 |
504 |
531 lemma INF_sup_distrib2: |
505 lemma INF_sup_distrib2: "(\<Sqinter>a\<in>A. f a) \<squnion> (\<Sqinter>b\<in>B. g b) = (\<Sqinter>a\<in>A. \<Sqinter>b\<in>B. f a \<squnion> g b)" |
532 "(\<Sqinter>a\<in>A. f a) \<squnion> (\<Sqinter>b\<in>B. g b) = (\<Sqinter>a\<in>A. \<Sqinter>b\<in>B. f a \<squnion> g b)" |
|
533 by (subst INF_commute) (simp add: sup_INF INF_sup) |
506 by (subst INF_commute) (simp add: sup_INF INF_sup) |
534 |
507 |
535 lemma SUP_inf_distrib2: |
508 lemma SUP_inf_distrib2: "(\<Squnion>a\<in>A. f a) \<sqinter> (\<Squnion>b\<in>B. g b) = (\<Squnion>a\<in>A. \<Squnion>b\<in>B. f a \<sqinter> g b)" |
536 "(\<Squnion>a\<in>A. f a) \<sqinter> (\<Squnion>b\<in>B. g b) = (\<Squnion>a\<in>A. \<Squnion>b\<in>B. f a \<sqinter> g b)" |
|
537 by (subst SUP_commute) (simp add: inf_SUP SUP_inf) |
509 by (subst SUP_commute) (simp add: inf_SUP SUP_inf) |
538 |
510 |
539 context |
511 context |
540 fixes f :: "'a \<Rightarrow> 'b::complete_lattice" |
512 fixes f :: "'a \<Rightarrow> 'b::complete_lattice" |
541 assumes "mono f" |
513 assumes "mono f" |
542 begin |
514 begin |
543 |
515 |
544 lemma mono_Inf: |
516 lemma mono_Inf: "f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)" |
545 shows "f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)" |
|
546 using \<open>mono f\<close> by (auto intro: complete_lattice_class.INF_greatest Inf_lower dest: monoD) |
517 using \<open>mono f\<close> by (auto intro: complete_lattice_class.INF_greatest Inf_lower dest: monoD) |
547 |
518 |
548 lemma mono_Sup: |
519 lemma mono_Sup: "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)" |
549 shows "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)" |
|
550 using \<open>mono f\<close> by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD) |
520 using \<open>mono f\<close> by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD) |
551 |
521 |
552 lemma mono_INF: |
522 lemma mono_INF: "f (INF i : I. A i) \<le> (INF x : I. f (A x))" |
553 "f (INF i : I. A i) \<le> (INF x : I. f (A x))" |
|
554 by (intro complete_lattice_class.INF_greatest monoD[OF \<open>mono f\<close>] INF_lower) |
523 by (intro complete_lattice_class.INF_greatest monoD[OF \<open>mono f\<close>] INF_lower) |
555 |
524 |
556 lemma mono_SUP: |
525 lemma mono_SUP: "(SUP x : I. f (A x)) \<le> f (SUP i : I. A i)" |
557 "(SUP x : I. f (A x)) \<le> f (SUP i : I. A i)" |
|
558 by (intro complete_lattice_class.SUP_least monoD[OF \<open>mono f\<close>] SUP_upper) |
526 by (intro complete_lattice_class.SUP_least monoD[OF \<open>mono f\<close>] SUP_upper) |
559 |
527 |
560 end |
528 end |
561 |
529 |
562 end |
530 end |
564 class complete_boolean_algebra = boolean_algebra + complete_distrib_lattice |
532 class complete_boolean_algebra = boolean_algebra + complete_distrib_lattice |
565 begin |
533 begin |
566 |
534 |
567 lemma dual_complete_boolean_algebra: |
535 lemma dual_complete_boolean_algebra: |
568 "class.complete_boolean_algebra Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus" |
536 "class.complete_boolean_algebra Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus" |
569 by (rule class.complete_boolean_algebra.intro, rule dual_complete_distrib_lattice, rule dual_boolean_algebra) |
537 by (rule class.complete_boolean_algebra.intro, |
570 |
538 rule dual_complete_distrib_lattice, |
571 lemma uminus_Inf: |
539 rule dual_boolean_algebra) |
572 "- (\<Sqinter>A) = \<Squnion>(uminus ` A)" |
540 |
|
541 lemma uminus_Inf: "- (\<Sqinter>A) = \<Squnion>(uminus ` A)" |
573 proof (rule antisym) |
542 proof (rule antisym) |
574 show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)" |
543 show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)" |
575 by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp |
544 by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp |
576 show "\<Squnion>(uminus ` A) \<le> - \<Sqinter>A" |
545 show "\<Squnion>(uminus ` A) \<le> - \<Sqinter>A" |
577 by (rule Sup_least, rule compl_le_swap1, rule Inf_lower) auto |
546 by (rule Sup_least, rule compl_le_swap1, rule Inf_lower) auto |
578 qed |
547 qed |
579 |
548 |
580 lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)" |
549 lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)" |
581 by (simp add: uminus_Inf image_image) |
550 by (simp add: uminus_Inf image_image) |
582 |
551 |
583 lemma uminus_Sup: |
552 lemma uminus_Sup: "- (\<Squnion>A) = \<Sqinter>(uminus ` A)" |
584 "- (\<Squnion>A) = \<Sqinter>(uminus ` A)" |
|
585 proof - |
553 proof - |
586 have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_INF) |
554 have "\<Squnion>A = - \<Sqinter>(uminus ` A)" |
|
555 by (simp add: image_image uminus_INF) |
587 then show ?thesis by simp |
556 then show ?thesis by simp |
588 qed |
557 qed |
589 |
558 |
590 lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)" |
559 lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)" |
591 by (simp add: uminus_Sup image_image) |
560 by (simp add: uminus_Sup image_image) |
592 |
561 |
593 end |
562 end |
594 |
563 |
603 by (auto intro: antisym simp add: min_def fun_eq_iff) |
572 by (auto intro: antisym simp add: min_def fun_eq_iff) |
604 |
573 |
605 lemma complete_linorder_sup_max: "sup = max" |
574 lemma complete_linorder_sup_max: "sup = max" |
606 by (auto intro: antisym simp add: max_def fun_eq_iff) |
575 by (auto intro: antisym simp add: max_def fun_eq_iff) |
607 |
576 |
608 lemma Inf_less_iff: |
577 lemma Inf_less_iff: "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)" |
609 "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)" |
|
610 by (simp add: not_le [symmetric] le_Inf_iff) |
578 by (simp add: not_le [symmetric] le_Inf_iff) |
611 |
579 |
612 lemma INF_less_iff: |
580 lemma INF_less_iff: "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)" |
613 "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)" |
|
614 by (simp add: Inf_less_iff [of "f ` A"]) |
581 by (simp add: Inf_less_iff [of "f ` A"]) |
615 |
582 |
616 lemma less_Sup_iff: |
583 lemma less_Sup_iff: "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)" |
617 "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)" |
|
618 by (simp add: not_le [symmetric] Sup_le_iff) |
584 by (simp add: not_le [symmetric] Sup_le_iff) |
619 |
585 |
620 lemma less_SUP_iff: |
586 lemma less_SUP_iff: "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)" |
621 "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)" |
|
622 by (simp add: less_Sup_iff [of _ "f ` A"]) |
587 by (simp add: less_Sup_iff [of _ "f ` A"]) |
623 |
588 |
624 lemma Sup_eq_top_iff [simp]: |
589 lemma Sup_eq_top_iff [simp]: "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)" |
625 "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)" |
|
626 proof |
590 proof |
627 assume *: "\<Squnion>A = \<top>" |
591 assume *: "\<Squnion>A = \<top>" |
628 show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric] |
592 show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" |
|
593 unfolding * [symmetric] |
629 proof (intro allI impI) |
594 proof (intro allI impI) |
630 fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i" |
595 fix x |
|
596 assume "x < \<Squnion>A" |
|
597 then show "\<exists>i\<in>A. x < i" |
631 by (simp add: less_Sup_iff) |
598 by (simp add: less_Sup_iff) |
632 qed |
599 qed |
633 next |
600 next |
634 assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i" |
601 assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i" |
635 show "\<Squnion>A = \<top>" |
602 show "\<Squnion>A = \<top>" |
636 proof (rule ccontr) |
603 proof (rule ccontr) |
637 assume "\<Squnion>A \<noteq> \<top>" |
604 assume "\<Squnion>A \<noteq> \<top>" |
638 with top_greatest [of "\<Squnion>A"] |
605 with top_greatest [of "\<Squnion>A"] have "\<Squnion>A < \<top>" |
639 have "\<Squnion>A < \<top>" unfolding le_less by auto |
606 unfolding le_less by auto |
640 then have "\<Squnion>A < \<Squnion>A" |
607 with * have "\<Squnion>A < \<Squnion>A" |
641 using * unfolding less_Sup_iff by auto |
608 unfolding less_Sup_iff by auto |
642 then show False by auto |
609 then show False by auto |
643 qed |
610 qed |
644 qed |
611 qed |
645 |
612 |
646 lemma SUP_eq_top_iff [simp]: |
613 lemma SUP_eq_top_iff [simp]: "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)" |
647 "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)" |
|
648 using Sup_eq_top_iff [of "f ` A"] by simp |
614 using Sup_eq_top_iff [of "f ` A"] by simp |
649 |
615 |
650 lemma Inf_eq_bot_iff [simp]: |
616 lemma Inf_eq_bot_iff [simp]: "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)" |
651 "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)" |
|
652 using dual_complete_linorder |
617 using dual_complete_linorder |
653 by (rule complete_linorder.Sup_eq_top_iff) |
618 by (rule complete_linorder.Sup_eq_top_iff) |
654 |
619 |
655 lemma INF_eq_bot_iff [simp]: |
620 lemma INF_eq_bot_iff [simp]: "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)" |
656 "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)" |
|
657 using Inf_eq_bot_iff [of "f ` A"] by simp |
621 using Inf_eq_bot_iff [of "f ` A"] by simp |
658 |
622 |
659 lemma Inf_le_iff: "\<Sqinter>A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)" |
623 lemma Inf_le_iff: "\<Sqinter>A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)" |
660 proof safe |
624 proof safe |
661 fix y assume "x \<ge> \<Sqinter>A" "y > x" |
625 fix y |
|
626 assume "x \<ge> \<Sqinter>A" "y > x" |
662 then have "y > \<Sqinter>A" by auto |
627 then have "y > \<Sqinter>A" by auto |
663 then show "\<exists>a\<in>A. y > a" |
628 then show "\<exists>a\<in>A. y > a" |
664 unfolding Inf_less_iff . |
629 unfolding Inf_less_iff . |
665 qed (auto elim!: allE[of _ "\<Sqinter>A"] simp add: not_le[symmetric] Inf_lower) |
630 qed (auto elim!: allE[of _ "\<Sqinter>A"] simp add: not_le[symmetric] Inf_lower) |
666 |
631 |
667 lemma INF_le_iff: |
632 lemma INF_le_iff: "INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)" |
668 "INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)" |
|
669 using Inf_le_iff [of "f ` A"] by simp |
633 using Inf_le_iff [of "f ` A"] by simp |
670 |
634 |
671 lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)" |
635 lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)" |
672 proof safe |
636 proof safe |
673 fix y assume "x \<le> \<Squnion>A" "y < x" |
637 fix y |
|
638 assume "x \<le> \<Squnion>A" "y < x" |
674 then have "y < \<Squnion>A" by auto |
639 then have "y < \<Squnion>A" by auto |
675 then show "\<exists>a\<in>A. y < a" |
640 then show "\<exists>a\<in>A. y < a" |
676 unfolding less_Sup_iff . |
641 unfolding less_Sup_iff . |
677 qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper) |
642 qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper) |
678 |
643 |
694 subsection \<open>Complete lattice on @{typ bool}\<close> |
659 subsection \<open>Complete lattice on @{typ bool}\<close> |
695 |
660 |
696 instantiation bool :: complete_lattice |
661 instantiation bool :: complete_lattice |
697 begin |
662 begin |
698 |
663 |
699 definition |
664 definition [simp, code]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A" |
700 [simp, code]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A" |
665 |
701 |
666 definition [simp, code]: "\<Squnion>A \<longleftrightarrow> True \<in> A" |
702 definition |
667 |
703 [simp, code]: "\<Squnion>A \<longleftrightarrow> True \<in> A" |
668 instance |
704 |
669 by standard (auto intro: bool_induct) |
705 instance proof |
|
706 qed (auto intro: bool_induct) |
|
707 |
670 |
708 end |
671 end |
709 |
672 |
710 lemma not_False_in_image_Ball [simp]: |
673 lemma not_False_in_image_Ball [simp]: "False \<notin> P ` A \<longleftrightarrow> Ball A P" |
711 "False \<notin> P ` A \<longleftrightarrow> Ball A P" |
674 by auto |
712 by auto |
675 |
713 |
676 lemma True_in_image_Bex [simp]: "True \<in> P ` A \<longleftrightarrow> Bex A P" |
714 lemma True_in_image_Bex [simp]: |
677 by auto |
715 "True \<in> P ` A \<longleftrightarrow> Bex A P" |
678 |
716 by auto |
679 lemma INF_bool_eq [simp]: "INFIMUM = Ball" |
717 |
|
718 lemma INF_bool_eq [simp]: |
|
719 "INFIMUM = Ball" |
|
720 by (simp add: fun_eq_iff) |
680 by (simp add: fun_eq_iff) |
721 |
681 |
722 lemma SUP_bool_eq [simp]: |
682 lemma SUP_bool_eq [simp]: "SUPREMUM = Bex" |
723 "SUPREMUM = Bex" |
|
724 by (simp add: fun_eq_iff) |
683 by (simp add: fun_eq_iff) |
725 |
684 |
726 instance bool :: complete_boolean_algebra proof |
685 instance bool :: complete_boolean_algebra |
727 qed (auto intro: bool_induct) |
686 by standard (auto intro: bool_induct) |
728 |
687 |
729 |
688 |
730 subsection \<open>Complete lattice on @{typ "_ \<Rightarrow> _"}\<close> |
689 subsection \<open>Complete lattice on @{typ "_ \<Rightarrow> _"}\<close> |
731 |
690 |
732 instantiation "fun" :: (type, Inf) Inf |
691 instantiation "fun" :: (type, Inf) Inf |
733 begin |
692 begin |
734 |
693 |
735 definition |
694 definition "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)" |
736 "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)" |
695 |
737 |
696 lemma Inf_apply [simp, code]: "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)" |
738 lemma Inf_apply [simp, code]: |
|
739 "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)" |
|
740 by (simp add: Inf_fun_def) |
697 by (simp add: Inf_fun_def) |
741 |
698 |
742 instance .. |
699 instance .. |
743 |
700 |
744 end |
701 end |
745 |
702 |
746 instantiation "fun" :: (type, Sup) Sup |
703 instantiation "fun" :: (type, Sup) Sup |
747 begin |
704 begin |
748 |
705 |
749 definition |
706 definition "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)" |
750 "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)" |
707 |
751 |
708 lemma Sup_apply [simp, code]: "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)" |
752 lemma Sup_apply [simp, code]: |
|
753 "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)" |
|
754 by (simp add: Sup_fun_def) |
709 by (simp add: Sup_fun_def) |
755 |
710 |
756 instance .. |
711 instance .. |
757 |
712 |
758 end |
713 end |
759 |
714 |
760 instantiation "fun" :: (type, complete_lattice) complete_lattice |
715 instantiation "fun" :: (type, complete_lattice) complete_lattice |
761 begin |
716 begin |
762 |
717 |
763 instance proof |
718 instance |
764 qed (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least) |
719 by standard (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least) |
765 |
720 |
766 end |
721 end |
767 |
722 |
768 lemma INF_apply [simp]: |
723 lemma INF_apply [simp]: "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)" |
769 "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)" |
|
770 using Inf_apply [of "f ` A"] by (simp add: comp_def) |
724 using Inf_apply [of "f ` A"] by (simp add: comp_def) |
771 |
725 |
772 lemma SUP_apply [simp]: |
726 lemma SUP_apply [simp]: "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)" |
773 "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)" |
|
774 using Sup_apply [of "f ` A"] by (simp add: comp_def) |
727 using Sup_apply [of "f ` A"] by (simp add: comp_def) |
775 |
728 |
776 instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof |
729 instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice |
777 qed (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image) |
730 by standard (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image) |
778 |
731 |
779 instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra .. |
732 instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra .. |
780 |
733 |
781 |
734 |
782 subsection \<open>Complete lattice on unary and binary predicates\<close> |
735 subsection \<open>Complete lattice on unary and binary predicates\<close> |
783 |
736 |
784 lemma Inf1_I: |
737 lemma Inf1_I: "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a" |
785 "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a" |
738 by auto |
786 by auto |
739 |
787 |
740 lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b" |
788 lemma INF1_I: |
|
789 "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b" |
|
790 by simp |
741 by simp |
791 |
742 |
792 lemma INF2_I: |
743 lemma INF2_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c" |
793 "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c" |
|
794 by simp |
744 by simp |
795 |
745 |
796 lemma Inf2_I: |
746 lemma Inf2_I: "(\<And>r. r \<in> A \<Longrightarrow> r a b) \<Longrightarrow> (\<Sqinter>A) a b" |
797 "(\<And>r. r \<in> A \<Longrightarrow> r a b) \<Longrightarrow> (\<Sqinter>A) a b" |
747 by auto |
798 by auto |
748 |
799 |
749 lemma Inf1_D: "(\<Sqinter>A) a \<Longrightarrow> P \<in> A \<Longrightarrow> P a" |
800 lemma Inf1_D: |
750 by auto |
801 "(\<Sqinter>A) a \<Longrightarrow> P \<in> A \<Longrightarrow> P a" |
751 |
802 by auto |
752 lemma INF1_D: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b" |
803 |
|
804 lemma INF1_D: |
|
805 "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b" |
|
806 by simp |
753 by simp |
807 |
754 |
808 lemma Inf2_D: |
755 lemma Inf2_D: "(\<Sqinter>A) a b \<Longrightarrow> r \<in> A \<Longrightarrow> r a b" |
809 "(\<Sqinter>A) a b \<Longrightarrow> r \<in> A \<Longrightarrow> r a b" |
756 by auto |
810 by auto |
757 |
811 |
758 lemma INF2_D: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c" |
812 lemma INF2_D: |
|
813 "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c" |
|
814 by simp |
759 by simp |
815 |
760 |
816 lemma Inf1_E: |
761 lemma Inf1_E: |
817 assumes "(\<Sqinter>A) a" |
762 assumes "(\<Sqinter>A) a" |
818 obtains "P a" | "P \<notin> A" |
763 obtains "P a" | "P \<notin> A" |
911 |
848 |
912 lemma InterI [intro!]: "(\<And>X. X \<in> C \<Longrightarrow> A \<in> X) \<Longrightarrow> A \<in> \<Inter>C" |
849 lemma InterI [intro!]: "(\<And>X. X \<in> C \<Longrightarrow> A \<in> X) \<Longrightarrow> A \<in> \<Inter>C" |
913 by (simp add: Inter_eq) |
850 by (simp add: Inter_eq) |
914 |
851 |
915 text \<open> |
852 text \<open> |
916 \medskip A ``destruct'' rule -- every @{term X} in @{term C} |
853 \<^medskip> A ``destruct'' rule -- every @{term X} in @{term C} |
917 contains @{term A} as an element, but @{prop "A \<in> X"} can hold when |
854 contains @{term A} as an element, but @{prop "A \<in> X"} can hold when |
918 @{prop "X \<in> C"} does not! This rule is analogous to \<open>spec\<close>. |
855 @{prop "X \<in> C"} does not! This rule is analogous to \<open>spec\<close>. |
919 \<close> |
856 \<close> |
920 |
857 |
921 lemma InterD [elim, Pure.elim]: "A \<in> \<Inter>C \<Longrightarrow> X \<in> C \<Longrightarrow> A \<in> X" |
858 lemma InterD [elim, Pure.elim]: "A \<in> \<Inter>C \<Longrightarrow> X \<in> C \<Longrightarrow> A \<in> X" |
922 by auto |
859 by auto |
923 |
860 |
924 lemma InterE [elim]: "A \<in> \<Inter>C \<Longrightarrow> (X \<notin> C \<Longrightarrow> R) \<Longrightarrow> (A \<in> X \<Longrightarrow> R) \<Longrightarrow> R" |
861 lemma InterE [elim]: "A \<in> \<Inter>C \<Longrightarrow> (X \<notin> C \<Longrightarrow> R) \<Longrightarrow> (A \<in> X \<Longrightarrow> R) \<Longrightarrow> R" |
925 \<comment> \<open>``Classical'' elimination rule -- does not require proving |
862 \<comment> \<open>``Classical'' elimination rule -- does not require proving |
926 @{prop "X \<in> C"}.\<close> |
863 @{prop "X \<in> C"}.\<close> |
927 by (unfold Inter_eq) blast |
864 unfolding Inter_eq by blast |
928 |
865 |
929 lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B" |
866 lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B" |
930 by (fact Inf_lower) |
867 by (fact Inf_lower) |
931 |
868 |
932 lemma Inter_subset: |
869 lemma Inter_subset: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B" |
933 "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B" |
|
934 by (fact Inf_less_eq) |
870 by (fact Inf_less_eq) |
935 |
871 |
936 lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> \<Inter>A" |
872 lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> \<Inter>A" |
937 by (fact Inf_greatest) |
873 by (fact Inf_greatest) |
938 |
874 |
1321 |
1249 |
1322 lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})" |
1250 lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})" |
1323 by (fact Sup_inf_eq_bot_iff) |
1251 by (fact Sup_inf_eq_bot_iff) |
1324 |
1252 |
1325 lemma SUP_UNION: "(SUP x:(UN y:A. g y). f x) = (SUP y:A. SUP x:g y. f x :: _ :: complete_lattice)" |
1253 lemma SUP_UNION: "(SUP x:(UN y:A. g y). f x) = (SUP y:A. SUP x:g y. f x :: _ :: complete_lattice)" |
1326 by(rule order_antisym)(blast intro: SUP_least SUP_upper2)+ |
1254 by (rule order_antisym) (blast intro: SUP_least SUP_upper2)+ |
|
1255 |
1327 |
1256 |
1328 subsection \<open>Injections and bijections\<close> |
1257 subsection \<open>Injections and bijections\<close> |
1329 |
1258 |
1330 lemma inj_on_Inter: |
1259 lemma inj_on_Inter: "S \<noteq> {} \<Longrightarrow> (\<And>A. A \<in> S \<Longrightarrow> inj_on f A) \<Longrightarrow> inj_on f (\<Inter>S)" |
1331 "S \<noteq> {} \<Longrightarrow> (\<And>A. A \<in> S \<Longrightarrow> inj_on f A) \<Longrightarrow> inj_on f (\<Inter>S)" |
|
1332 unfolding inj_on_def by blast |
1260 unfolding inj_on_def by blast |
1333 |
1261 |
1334 lemma inj_on_INTER: |
1262 lemma inj_on_INTER: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)) \<Longrightarrow> inj_on f (\<Inter>i \<in> I. A i)" |
1335 "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)) \<Longrightarrow> inj_on f (\<Inter>i \<in> I. A i)" |
|
1336 unfolding inj_on_def by safe simp |
1263 unfolding inj_on_def by safe simp |
1337 |
1264 |
1338 lemma inj_on_UNION_chain: |
1265 lemma inj_on_UNION_chain: |
1339 assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and |
1266 assumes chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" |
1340 INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)" |
1267 and inj: "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)" |
1341 shows "inj_on f (\<Union>i \<in> I. A i)" |
1268 shows "inj_on f (\<Union>i \<in> I. A i)" |
1342 proof - |
1269 proof - |
1343 { |
1270 have "x = y" |
1344 fix i j x y |
1271 if *: "i \<in> I" "j \<in> I" |
1345 assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j" |
1272 and **: "x \<in> A i" "y \<in> A j" |
1346 and ***: "f x = f y" |
1273 and ***: "f x = f y" |
1347 have "x = y" |
1274 for i j x y |
1348 proof - |
1275 using chain [OF *] |
1349 { |
1276 proof |
1350 assume "A i \<le> A j" |
1277 assume "A i \<le> A j" |
1351 with ** have "x \<in> A j" by auto |
1278 with ** have "x \<in> A j" by auto |
1352 with INJ * ** *** have ?thesis |
1279 with inj * ** *** show ?thesis |
1353 by(auto simp add: inj_on_def) |
1280 by (auto simp add: inj_on_def) |
1354 } |
1281 next |
1355 moreover |
1282 assume "A j \<le> A i" |
1356 { |
1283 with ** have "y \<in> A i" by auto |
1357 assume "A j \<le> A i" |
1284 with inj * ** *** show ?thesis |
1358 with ** have "y \<in> A i" by auto |
1285 by (auto simp add: inj_on_def) |
1359 with INJ * ** *** have ?thesis |
1286 qed |
1360 by(auto simp add: inj_on_def) |
1287 then show ?thesis |
1361 } |
1288 by (unfold inj_on_def UNION_eq) auto |
1362 ultimately show ?thesis using CH * by blast |
|
1363 qed |
|
1364 } |
|
1365 then show ?thesis by (unfold inj_on_def UNION_eq) auto |
|
1366 qed |
1289 qed |
1367 |
1290 |
1368 lemma bij_betw_UNION_chain: |
1291 lemma bij_betw_UNION_chain: |
1369 assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and |
1292 assumes chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" |
1370 BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)" |
1293 and bij: "\<And>i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)" |
1371 shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)" |
1294 shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)" |
1372 proof (unfold bij_betw_def, auto) |
1295 unfolding bij_betw_def |
1373 have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)" |
1296 proof auto (* slow *) |
1374 using BIJ bij_betw_def[of f] by auto |
1297 have "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)" |
1375 thus "inj_on f (\<Union>i \<in> I. A i)" |
1298 using bij bij_betw_def[of f] by auto |
1376 using CH inj_on_UNION_chain[of I A f] by auto |
1299 then show "inj_on f (\<Union>i \<in> I. A i)" |
|
1300 using chain inj_on_UNION_chain[of I A f] by auto |
1377 next |
1301 next |
1378 fix i x |
1302 fix i x |
1379 assume *: "i \<in> I" "x \<in> A i" |
1303 assume *: "i \<in> I" "x \<in> A i" |
1380 hence "f x \<in> A' i" using BIJ bij_betw_def[of f] by auto |
1304 then have "f x \<in> A' i" |
1381 thus "\<exists>j \<in> I. f x \<in> A' j" using * by blast |
1305 using bij bij_betw_def[of f] by auto |
|
1306 with * show "\<exists>j \<in> I. f x \<in> A' j" by blast |
1382 next |
1307 next |
1383 fix i x' |
1308 fix i x' |
1384 assume *: "i \<in> I" "x' \<in> A' i" |
1309 assume *: "i \<in> I" "x' \<in> A' i" |
1385 hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast |
1310 then have "\<exists>x \<in> A i. x' = f x" |
1386 then have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x" |
1311 using bij bij_betw_def[of f] by blast |
1387 using * by blast |
1312 with * have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x" |
1388 then show "x' \<in> f ` (\<Union>x\<in>I. A x)" by blast |
1313 by blast |
|
1314 then show "x' \<in> f ` (\<Union>x\<in>I. A x)" |
|
1315 by blast |
1389 qed |
1316 qed |
1390 |
1317 |
1391 (*injectivity's required. Left-to-right inclusion holds even if A is empty*) |
1318 (*injectivity's required. Left-to-right inclusion holds even if A is empty*) |
1392 lemma image_INT: |
1319 lemma image_INT: "inj_on f C \<Longrightarrow> \<forall>x\<in>A. B x \<subseteq> C \<Longrightarrow> j \<in> A \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)" |
1393 "[| inj_on f C; ALL x:A. B x <= C; j:A |] |
1320 by (auto simp add: inj_on_def) blast |
1394 ==> f ` (INTER A B) = (INT x:A. f ` B x)" |
1321 |
1395 by (simp add: inj_on_def, auto) blast |
1322 lemma bij_image_INT: "bij f \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)" |
1396 |
1323 apply (simp only: bij_def) |
1397 lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)" |
1324 apply (simp only: inj_on_def surj_def) |
1398 apply (simp add: bij_def) |
|
1399 apply (simp add: inj_on_def surj_def) |
|
1400 apply auto |
1325 apply auto |
1401 apply blast |
1326 apply blast |
1402 done |
1327 done |
1403 |
1328 |
1404 lemma UNION_fun_upd: |
1329 lemma UNION_fun_upd: "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})" |
1405 "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})" |
|
1406 by (auto simp add: set_eq_iff) |
1330 by (auto simp add: set_eq_iff) |
1407 |
1331 |
1408 lemma bij_betw_Pow: |
1332 lemma bij_betw_Pow: |
1409 assumes "bij_betw f A B" |
1333 assumes "bij_betw f A B" |
1410 shows "bij_betw (image f) (Pow A) (Pow B)" |
1334 shows "bij_betw (image f) (Pow A) (Pow B)" |