3 *) |
3 *) |
4 |
4 |
5 section \<open>Countable Complete Lattices\<close> |
5 section \<open>Countable Complete Lattices\<close> |
6 |
6 |
7 theory Countable_Complete_Lattices |
7 theory Countable_Complete_Lattices |
8 imports Main Lattice_Syntax Countable_Set |
8 imports Main Countable_Set |
9 begin |
9 begin |
10 |
10 |
11 lemma UNIV_nat_eq: "UNIV = insert 0 (range Suc)" |
11 lemma UNIV_nat_eq: "UNIV = insert 0 (range Suc)" |
12 by (metis UNIV_eq_I nat.nchotomy insertCI rangeI) |
12 by (metis UNIV_eq_I nat.nchotomy insertCI rangeI) |
13 |
13 |
14 class countable_complete_lattice = lattice + Inf + Sup + bot + top + |
14 class countable_complete_lattice = lattice + Inf + Sup + bot + top + |
15 assumes ccInf_lower: "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x" |
15 assumes ccInf_lower: "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> Inf A \<le> x" |
16 assumes ccInf_greatest: "countable A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A" |
16 assumes ccInf_greatest: "countable A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf A" |
17 assumes ccSup_upper: "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> x \<le> \<Squnion>A" |
17 assumes ccSup_upper: "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> x \<le> Sup A" |
18 assumes ccSup_least: "countable A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z" |
18 assumes ccSup_least: "countable A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup A \<le> z" |
19 assumes ccInf_empty [simp]: "\<Sqinter>{} = \<top>" |
19 assumes ccInf_empty [simp]: "Inf {} = top" |
20 assumes ccSup_empty [simp]: "\<Squnion>{} = \<bottom>" |
20 assumes ccSup_empty [simp]: "Sup {} = bot" |
21 begin |
21 begin |
22 |
22 |
23 subclass bounded_lattice |
23 subclass bounded_lattice |
24 proof |
24 proof |
25 fix a |
25 fix a |
26 show "\<bottom> \<le> a" by (auto intro: ccSup_least simp only: ccSup_empty [symmetric]) |
26 show "bot \<le> a" by (auto intro: ccSup_least simp only: ccSup_empty [symmetric]) |
27 show "a \<le> \<top>" by (auto intro: ccInf_greatest simp only: ccInf_empty [symmetric]) |
27 show "a \<le> top" by (auto intro: ccInf_greatest simp only: ccInf_empty [symmetric]) |
28 qed |
28 qed |
29 |
29 |
30 lemma ccINF_lower: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> f i" |
30 lemma ccINF_lower: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> (INF i :A. f i) \<le> f i" |
31 using ccInf_lower [of "f ` A"] by simp |
31 using ccInf_lower [of "f ` A"] by simp |
32 |
32 |
33 lemma ccINF_greatest: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> u \<le> f i) \<Longrightarrow> u \<le> (\<Sqinter>i\<in>A. f i)" |
33 lemma ccINF_greatest: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> u \<le> f i) \<Longrightarrow> u \<le> (INF i :A. f i)" |
34 using ccInf_greatest [of "f ` A"] by auto |
34 using ccInf_greatest [of "f ` A"] by auto |
35 |
35 |
36 lemma ccSUP_upper: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> (\<Squnion>i\<in>A. f i)" |
36 lemma ccSUP_upper: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> (SUP i :A. f i)" |
37 using ccSup_upper [of "f ` A"] by simp |
37 using ccSup_upper [of "f ` A"] by simp |
38 |
38 |
39 lemma ccSUP_least: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> f i \<le> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<le> u" |
39 lemma ccSUP_least: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> f i \<le> u) \<Longrightarrow> (SUP i :A. f i) \<le> u" |
40 using ccSup_least [of "f ` A"] by auto |
40 using ccSup_least [of "f ` A"] by auto |
41 |
41 |
42 lemma ccInf_lower2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> u \<le> v \<Longrightarrow> \<Sqinter>A \<le> v" |
42 lemma ccInf_lower2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> u \<le> v \<Longrightarrow> Inf A \<le> v" |
43 using ccInf_lower [of A u] by auto |
43 using ccInf_lower [of A u] by auto |
44 |
44 |
45 lemma ccINF_lower2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> u" |
45 lemma ccINF_lower2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (INF i :A. f i) \<le> u" |
46 using ccINF_lower [of A i f] by auto |
46 using ccINF_lower [of A i f] by auto |
47 |
47 |
48 lemma ccSup_upper2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> v \<le> u \<Longrightarrow> v \<le> \<Squnion>A" |
48 lemma ccSup_upper2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> v \<le> u \<Longrightarrow> v \<le> Sup A" |
49 using ccSup_upper [of A u] by auto |
49 using ccSup_upper [of A u] by auto |
50 |
50 |
51 lemma ccSUP_upper2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (\<Squnion>i\<in>A. f i)" |
51 lemma ccSUP_upper2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (SUP i :A. f i)" |
52 using ccSUP_upper [of A i f] by auto |
52 using ccSUP_upper [of A i f] by auto |
53 |
53 |
54 lemma le_ccInf_iff: "countable A \<Longrightarrow> b \<le> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<le> a)" |
54 lemma le_ccInf_iff: "countable A \<Longrightarrow> b \<le> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<le> a)" |
55 by (auto intro: ccInf_greatest dest: ccInf_lower) |
55 by (auto intro: ccInf_greatest dest: ccInf_lower) |
56 |
56 |
57 lemma le_ccINF_iff: "countable A \<Longrightarrow> u \<le> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)" |
57 lemma le_ccINF_iff: "countable A \<Longrightarrow> u \<le> (INF i :A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)" |
58 using le_ccInf_iff [of "f ` A"] by simp |
58 using le_ccInf_iff [of "f ` A"] by simp |
59 |
59 |
60 lemma ccSup_le_iff: "countable A \<Longrightarrow> \<Squnion>A \<le> b \<longleftrightarrow> (\<forall>a\<in>A. a \<le> b)" |
60 lemma ccSup_le_iff: "countable A \<Longrightarrow> Sup A \<le> b \<longleftrightarrow> (\<forall>a\<in>A. a \<le> b)" |
61 by (auto intro: ccSup_least dest: ccSup_upper) |
61 by (auto intro: ccSup_least dest: ccSup_upper) |
62 |
62 |
63 lemma ccSUP_le_iff: "countable A \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)" |
63 lemma ccSUP_le_iff: "countable A \<Longrightarrow> (SUP i :A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)" |
64 using ccSup_le_iff [of "f ` A"] by simp |
64 using ccSup_le_iff [of "f ` A"] by simp |
65 |
65 |
66 lemma ccInf_insert [simp]: "countable A \<Longrightarrow> \<Sqinter>insert a A = a \<sqinter> \<Sqinter>A" |
66 lemma ccInf_insert [simp]: "countable A \<Longrightarrow> Inf (insert a A) = inf a (Inf A)" |
67 by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower) |
67 by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower) |
68 |
68 |
69 lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFIMUM A f" |
69 lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (INF x:insert a A. f x) = inf (f a) (INFIMUM A f)" |
70 unfolding image_insert by simp |
70 unfolding image_insert by simp |
71 |
71 |
72 lemma ccSup_insert [simp]: "countable A \<Longrightarrow> \<Squnion>insert a A = a \<squnion> \<Squnion>A" |
72 lemma ccSup_insert [simp]: "countable A \<Longrightarrow> Sup (insert a A) = sup a (Sup A)" |
73 by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper) |
73 by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper) |
74 |
74 |
75 lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPREMUM A f" |
75 lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (SUP x:insert a A. f x) = sup (f a) (SUPREMUM A f)" |
76 unfolding image_insert by simp |
76 unfolding image_insert by simp |
77 |
77 |
78 lemma ccINF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>" |
78 lemma ccINF_empty [simp]: "(INF x:{}. f x) = top" |
79 unfolding image_empty by simp |
79 unfolding image_empty by simp |
80 |
80 |
81 lemma ccSUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>" |
81 lemma ccSUP_empty [simp]: "(SUP x:{}. f x) = bot" |
82 unfolding image_empty by simp |
82 unfolding image_empty by simp |
83 |
83 |
84 lemma ccInf_superset_mono: "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<le> \<Sqinter>B" |
84 lemma ccInf_superset_mono: "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> Inf A \<le> Inf B" |
85 by (auto intro: ccInf_greatest ccInf_lower countable_subset) |
85 by (auto intro: ccInf_greatest ccInf_lower countable_subset) |
86 |
86 |
87 lemma ccSup_subset_mono: "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> \<Squnion>A \<le> \<Squnion>B" |
87 lemma ccSup_subset_mono: "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> Sup A \<le> Sup B" |
88 by (auto intro: ccSup_least ccSup_upper countable_subset) |
88 by (auto intro: ccSup_least ccSup_upper countable_subset) |
89 |
89 |
90 lemma ccInf_mono: |
90 lemma ccInf_mono: |
91 assumes [intro]: "countable B" "countable A" |
91 assumes [intro]: "countable B" "countable A" |
92 assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b" |
92 assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b" |
93 shows "\<Sqinter>A \<le> \<Sqinter>B" |
93 shows "Inf A \<le> Inf B" |
94 proof (rule ccInf_greatest) |
94 proof (rule ccInf_greatest) |
95 fix b assume "b \<in> B" |
95 fix b assume "b \<in> B" |
96 with assms obtain a where "a \<in> A" and "a \<le> b" by blast |
96 with assms obtain a where "a \<in> A" and "a \<le> b" by blast |
97 from \<open>a \<in> A\<close> have "\<Sqinter>A \<le> a" by (rule ccInf_lower[rotated]) auto |
97 from \<open>a \<in> A\<close> have "Inf A \<le> a" by (rule ccInf_lower[rotated]) auto |
98 with \<open>a \<le> b\<close> show "\<Sqinter>A \<le> b" by auto |
98 with \<open>a \<le> b\<close> show "Inf A \<le> b" by auto |
99 qed auto |
99 qed auto |
100 |
100 |
101 lemma ccINF_mono: |
101 lemma ccINF_mono: |
102 "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<le> (\<Sqinter>n\<in>B. g n)" |
102 "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)" |
103 using ccInf_mono [of "g ` B" "f ` A"] by auto |
103 using ccInf_mono [of "g ` B" "f ` A"] by auto |
104 |
104 |
105 lemma ccSup_mono: |
105 lemma ccSup_mono: |
106 assumes [intro]: "countable B" "countable A" |
106 assumes [intro]: "countable B" "countable A" |
107 assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b" |
107 assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b" |
108 shows "\<Squnion>A \<le> \<Squnion>B" |
108 shows "Sup A \<le> Sup B" |
109 proof (rule ccSup_least) |
109 proof (rule ccSup_least) |
110 fix a assume "a \<in> A" |
110 fix a assume "a \<in> A" |
111 with assms obtain b where "b \<in> B" and "a \<le> b" by blast |
111 with assms obtain b where "b \<in> B" and "a \<le> b" by blast |
112 from \<open>b \<in> B\<close> have "b \<le> \<Squnion>B" by (rule ccSup_upper[rotated]) auto |
112 from \<open>b \<in> B\<close> have "b \<le> Sup B" by (rule ccSup_upper[rotated]) auto |
113 with \<open>a \<le> b\<close> show "a \<le> \<Squnion>B" by auto |
113 with \<open>a \<le> b\<close> show "a \<le> Sup B" by auto |
114 qed auto |
114 qed auto |
115 |
115 |
116 lemma ccSUP_mono: |
116 lemma ccSUP_mono: |
117 "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<le> (\<Squnion>n\<in>B. g n)" |
117 "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)" |
118 using ccSup_mono [of "g ` B" "f ` A"] by auto |
118 using ccSup_mono [of "g ` B" "f ` A"] by auto |
119 |
119 |
120 lemma ccINF_superset_mono: |
120 lemma ccINF_superset_mono: |
121 "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<le> (\<Sqinter>x\<in>B. g x)" |
121 "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (INF x:A. f x) \<le> (INF x:B. g x)" |
122 by (blast intro: ccINF_mono countable_subset dest: subsetD) |
122 by (blast intro: ccINF_mono countable_subset dest: subsetD) |
123 |
123 |
124 lemma ccSUP_subset_mono: |
124 lemma ccSUP_subset_mono: |
125 "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<le> (\<Squnion>x\<in>B. g x)" |
125 "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (SUP x:A. f x) \<le> (SUP x:B. g x)" |
126 by (blast intro: ccSUP_mono countable_subset dest: subsetD) |
126 by (blast intro: ccSUP_mono countable_subset dest: subsetD) |
127 |
127 |
128 |
128 |
129 lemma less_eq_ccInf_inter: "countable A \<Longrightarrow> countable B \<Longrightarrow> \<Sqinter>A \<squnion> \<Sqinter>B \<le> \<Sqinter>(A \<inter> B)" |
129 lemma less_eq_ccInf_inter: "countable A \<Longrightarrow> countable B \<Longrightarrow> sup (Inf A) (Inf B) \<le> Inf (A \<inter> B)" |
130 by (auto intro: ccInf_greatest ccInf_lower) |
130 by (auto intro: ccInf_greatest ccInf_lower) |
131 |
131 |
132 lemma ccSup_inter_less_eq: "countable A \<Longrightarrow> countable B \<Longrightarrow> \<Squnion>(A \<inter> B) \<le> \<Squnion>A \<sqinter> \<Squnion>B " |
132 lemma ccSup_inter_less_eq: "countable A \<Longrightarrow> countable B \<Longrightarrow> Sup (A \<inter> B) \<le> inf (Sup A) (Sup B)" |
133 by (auto intro: ccSup_least ccSup_upper) |
133 by (auto intro: ccSup_least ccSup_upper) |
134 |
134 |
135 lemma ccInf_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> \<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B" |
135 lemma ccInf_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> Inf (A \<union> B) = inf (Inf A) (Inf B)" |
136 by (rule antisym) (auto intro: ccInf_greatest ccInf_lower le_infI1 le_infI2) |
136 by (rule antisym) (auto intro: ccInf_greatest ccInf_lower le_infI1 le_infI2) |
137 |
137 |
138 lemma ccINF_union: |
138 lemma ccINF_union: |
139 "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)" |
139 "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i:A \<union> B. M i) = inf (INF i:A. M i) (INF i:B. M i)" |
140 by (auto intro!: antisym ccINF_mono intro: le_infI1 le_infI2 ccINF_greatest ccINF_lower) |
140 by (auto intro!: antisym ccINF_mono intro: le_infI1 le_infI2 ccINF_greatest ccINF_lower) |
141 |
141 |
142 lemma ccSup_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> \<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B" |
142 lemma ccSup_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)" |
143 by (rule antisym) (auto intro: ccSup_least ccSup_upper le_supI1 le_supI2) |
143 by (rule antisym) (auto intro: ccSup_least ccSup_upper le_supI1 le_supI2) |
144 |
144 |
145 lemma ccSUP_union: |
145 lemma ccSUP_union: |
146 "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)" |
146 "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i:A \<union> B. M i) = sup (SUP i:A. M i) (SUP i:B. M i)" |
147 by (auto intro!: antisym ccSUP_mono intro: le_supI1 le_supI2 ccSUP_least ccSUP_upper) |
147 by (auto intro!: antisym ccSUP_mono intro: le_supI1 le_supI2 ccSUP_least ccSUP_upper) |
148 |
148 |
149 lemma ccINF_inf_distrib: "countable A \<Longrightarrow> (\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)" |
149 lemma ccINF_inf_distrib: "countable A \<Longrightarrow> inf (INF a:A. f a) (INF a:A. g a) = (INF a:A. inf (f a) (g a))" |
150 by (rule antisym) (rule ccINF_greatest, auto intro: le_infI1 le_infI2 ccINF_lower ccINF_mono) |
150 by (rule antisym) (rule ccINF_greatest, auto intro: le_infI1 le_infI2 ccINF_lower ccINF_mono) |
151 |
151 |
152 lemma ccSUP_sup_distrib: "countable A \<Longrightarrow> (\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)" |
152 lemma ccSUP_sup_distrib: "countable A \<Longrightarrow> sup (SUP a:A. f a) (SUP a:A. g a) = (SUP a:A. sup (f a) (g a))" |
153 by (rule antisym[rotated]) (rule ccSUP_least, auto intro: le_supI1 le_supI2 ccSUP_upper ccSUP_mono) |
153 by (rule antisym[rotated]) (rule ccSUP_least, auto intro: le_supI1 le_supI2 ccSUP_upper ccSUP_mono) |
154 |
154 |
155 lemma ccINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f" |
155 lemma ccINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (INF i :A. f) = f" |
156 unfolding image_constant_conv by auto |
156 unfolding image_constant_conv by auto |
157 |
157 |
158 lemma ccSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f" |
158 lemma ccSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (SUP i :A. f) = f" |
159 unfolding image_constant_conv by auto |
159 unfolding image_constant_conv by auto |
160 |
160 |
161 lemma ccINF_top [simp]: "(\<Sqinter>x\<in>A. \<top>) = \<top>" |
161 lemma ccINF_top [simp]: "(INF x:A. top) = top" |
162 by (cases "A = {}") simp_all |
162 by (cases "A = {}") simp_all |
163 |
163 |
164 lemma ccSUP_bot [simp]: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>" |
164 lemma ccSUP_bot [simp]: "(SUP x:A. bot) = bot" |
165 by (cases "A = {}") simp_all |
165 by (cases "A = {}") simp_all |
166 |
166 |
167 lemma ccINF_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)" |
167 lemma ccINF_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)" |
168 by (iprover intro: ccINF_lower ccINF_greatest order_trans antisym) |
168 by (iprover intro: ccINF_lower ccINF_greatest order_trans antisym) |
169 |
169 |
170 lemma ccSUP_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)" |
170 lemma ccSUP_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)" |
171 by (iprover intro: ccSUP_upper ccSUP_least order_trans antisym) |
171 by (iprover intro: ccSUP_upper ccSUP_least order_trans antisym) |
172 |
172 |
173 end |
173 end |
174 |
174 |
175 context |
175 context |
176 fixes a :: "'a::{countable_complete_lattice, linorder}" |
176 fixes a :: "'a::{countable_complete_lattice, linorder}" |
177 begin |
177 begin |
178 |
178 |
179 lemma less_ccSup_iff: "countable S \<Longrightarrow> a < \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a < x)" |
179 lemma less_ccSup_iff: "countable S \<Longrightarrow> a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)" |
180 unfolding not_le [symmetric] by (subst ccSup_le_iff) auto |
180 unfolding not_le [symmetric] by (subst ccSup_le_iff) auto |
181 |
181 |
182 lemma less_ccSUP_iff: "countable A \<Longrightarrow> a < (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)" |
182 lemma less_ccSUP_iff: "countable A \<Longrightarrow> a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)" |
183 using less_ccSup_iff [of "f ` A"] by simp |
183 using less_ccSup_iff [of "f ` A"] by simp |
184 |
184 |
185 lemma ccInf_less_iff: "countable S \<Longrightarrow> \<Sqinter>S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)" |
185 lemma ccInf_less_iff: "countable S \<Longrightarrow> Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)" |
186 unfolding not_le [symmetric] by (subst le_ccInf_iff) auto |
186 unfolding not_le [symmetric] by (subst le_ccInf_iff) auto |
187 |
187 |
188 lemma ccINF_less_iff: "countable A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)" |
188 lemma ccINF_less_iff: "countable A \<Longrightarrow> (INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)" |
189 using ccInf_less_iff [of "f ` A"] by simp |
189 using ccInf_less_iff [of "f ` A"] by simp |
190 |
190 |
191 end |
191 end |
192 |
192 |
193 class countable_complete_distrib_lattice = countable_complete_lattice + |
193 class countable_complete_distrib_lattice = countable_complete_lattice + |
194 assumes sup_ccInf: "countable B \<Longrightarrow> a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)" |
194 assumes sup_ccInf: "countable B \<Longrightarrow> sup a (Inf B) = (INF b:B. sup a b)" |
195 assumes inf_ccSup: "countable B \<Longrightarrow> a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)" |
195 assumes inf_ccSup: "countable B \<Longrightarrow> inf a (Sup B) = (SUP b:B. inf a b)" |
196 begin |
196 begin |
197 |
197 |
198 lemma sup_ccINF: |
198 lemma sup_ccINF: |
199 "countable B \<Longrightarrow> a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)" |
199 "countable B \<Longrightarrow> sup a (INF b:B. f b) = (INF b:B. sup a (f b))" |
200 by (simp only: sup_ccInf image_image countable_image) |
200 by (simp only: sup_ccInf image_image countable_image) |
201 |
201 |
202 lemma inf_ccSUP: |
202 lemma inf_ccSUP: |
203 "countable B \<Longrightarrow> a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)" |
203 "countable B \<Longrightarrow> inf a (SUP b:B. f b) = (SUP b:B. inf a (f b))" |
204 by (simp only: inf_ccSup image_image countable_image) |
204 by (simp only: inf_ccSup image_image countable_image) |
205 |
205 |
206 subclass distrib_lattice proof |
206 subclass distrib_lattice |
|
207 proof |
207 fix a b c |
208 fix a b c |
208 from sup_ccInf[of "{b, c}" a] have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" |
209 from sup_ccInf[of "{b, c}" a] have "sup a (Inf {b, c}) = (INF d:{b, c}. sup a d)" |
209 by simp |
210 by simp |
210 then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by simp |
211 then show "sup a (inf b c) = inf (sup a b) (sup a c)" |
|
212 by simp |
211 qed |
213 qed |
212 |
214 |
213 lemma ccInf_sup: |
215 lemma ccInf_sup: |
214 "countable B \<Longrightarrow> \<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)" |
216 "countable B \<Longrightarrow> sup (Inf B) a = (INF b:B. sup b a)" |
215 by (simp add: sup_ccInf sup_commute) |
217 by (simp add: sup_ccInf sup_commute) |
216 |
218 |
217 lemma ccSup_inf: |
219 lemma ccSup_inf: |
218 "countable B \<Longrightarrow> \<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)" |
220 "countable B \<Longrightarrow> inf (Sup B) a = (SUP b:B. inf b a)" |
219 by (simp add: inf_ccSup inf_commute) |
221 by (simp add: inf_ccSup inf_commute) |
220 |
222 |
221 lemma ccINF_sup: |
223 lemma ccINF_sup: |
222 "countable B \<Longrightarrow> (\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)" |
224 "countable B \<Longrightarrow> sup (INF b:B. f b) a = (INF b:B. sup (f b) a)" |
223 by (simp add: sup_ccINF sup_commute) |
225 by (simp add: sup_ccINF sup_commute) |
224 |
226 |
225 lemma ccSUP_inf: |
227 lemma ccSUP_inf: |
226 "countable B \<Longrightarrow> (\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)" |
228 "countable B \<Longrightarrow> inf (SUP b:B. f b) a = (SUP b:B. inf (f b) a)" |
227 by (simp add: inf_ccSUP inf_commute) |
229 by (simp add: inf_ccSUP inf_commute) |
228 |
230 |
229 lemma ccINF_sup_distrib2: |
231 lemma ccINF_sup_distrib2: |
230 "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<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)" |
232 "countable A \<Longrightarrow> countable B \<Longrightarrow> sup (INF a:A. f a) (INF b:B. g b) = (INF a:A. INF b:B. sup (f a) (g b))" |
231 by (subst ccINF_commute) (simp_all add: sup_ccINF ccINF_sup) |
233 by (subst ccINF_commute) (simp_all add: sup_ccINF ccINF_sup) |
232 |
234 |
233 lemma ccSUP_inf_distrib2: |
235 lemma ccSUP_inf_distrib2: |
234 "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<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)" |
236 "countable A \<Longrightarrow> countable B \<Longrightarrow> inf (SUP a:A. f a) (SUP b:B. g b) = (SUP a:A. SUP b:B. inf (f a) (g b))" |
235 by (subst ccSUP_commute) (simp_all add: inf_ccSUP ccSUP_inf) |
237 by (subst ccSUP_commute) (simp_all add: inf_ccSUP ccSUP_inf) |
236 |
238 |
237 context |
239 context |
238 fixes f :: "'a \<Rightarrow> 'b::countable_complete_lattice" |
240 fixes f :: "'a \<Rightarrow> 'b::countable_complete_lattice" |
239 assumes "mono f" |
241 assumes "mono f" |
240 begin |
242 begin |
241 |
243 |
242 lemma mono_ccInf: |
244 lemma mono_ccInf: |
243 "countable A \<Longrightarrow> f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)" |
245 "countable A \<Longrightarrow> f (Inf A) \<le> (INF x:A. f x)" |
244 using \<open>mono f\<close> |
246 using \<open>mono f\<close> |
245 by (auto intro!: countable_complete_lattice_class.ccINF_greatest intro: ccInf_lower dest: monoD) |
247 by (auto intro!: countable_complete_lattice_class.ccINF_greatest intro: ccInf_lower dest: monoD) |
246 |
248 |
247 lemma mono_ccSup: |
249 lemma mono_ccSup: |
248 "countable A \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)" |
250 "countable A \<Longrightarrow> (SUP x:A. f x) \<le> f (Sup A)" |
249 using \<open>mono f\<close> by (auto intro: countable_complete_lattice_class.ccSUP_least ccSup_upper dest: monoD) |
251 using \<open>mono f\<close> by (auto intro: countable_complete_lattice_class.ccSUP_least ccSup_upper dest: monoD) |
250 |
252 |
251 lemma mono_ccINF: |
253 lemma mono_ccINF: |
252 "countable I \<Longrightarrow> f (INF i : I. A i) \<le> (INF x : I. f (A x))" |
254 "countable I \<Longrightarrow> f (INF i : I. A i) \<le> (INF x : I. f (A x))" |
253 by (intro countable_complete_lattice_class.ccINF_greatest monoD[OF \<open>mono f\<close>] ccINF_lower) |
255 by (intro countable_complete_lattice_class.ccINF_greatest monoD[OF \<open>mono f\<close>] ccINF_lower) |