equal
deleted
inserted
replaced
18 begin |
18 begin |
19 |
19 |
20 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
20 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
21 INF_def: "INFI A f = \<Sqinter>(f ` A)" |
21 INF_def: "INFI A f = \<Sqinter>(f ` A)" |
22 |
22 |
|
23 lemma INF_image [simp]: "INFI (f`A) g = INFI A (\<lambda>x. g (f x))" |
|
24 by (simp add: INF_def image_image) |
|
25 |
|
26 lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFI A C = INFI B D" |
|
27 by (simp add: INF_def image_def) |
|
28 |
23 end |
29 end |
24 |
30 |
25 class Sup = |
31 class Sup = |
26 fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900) |
32 fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900) |
27 begin |
33 begin |
28 |
34 |
29 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
35 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
30 SUP_def: "SUPR A f = \<Squnion>(f ` A)" |
36 SUP_def: "SUPR A f = \<Squnion>(f ` A)" |
|
37 |
|
38 lemma SUP_image [simp]: "SUPR (f`A) g = SUPR A (%x. g (f x))" |
|
39 by (simp add: SUP_def image_image) |
|
40 |
|
41 lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPR A C = SUPR B D" |
|
42 by (simp add: SUP_def image_def) |
31 |
43 |
32 end |
44 end |
33 |
45 |
34 text {* |
46 text {* |
35 Note: must use names @{const INFI} and @{const SUPR} here instead of |
47 Note: must use names @{const INFI} and @{const SUPR} here instead of |
181 |
193 |
182 lemma Sup_UNIV [simp]: |
194 lemma Sup_UNIV [simp]: |
183 "\<Squnion>UNIV = \<top>" |
195 "\<Squnion>UNIV = \<top>" |
184 by (auto intro!: antisym Sup_upper) |
196 by (auto intro!: antisym Sup_upper) |
185 |
197 |
186 lemma INF_image [simp]: "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))" |
|
187 by (simp add: INF_def image_image) |
|
188 |
|
189 lemma SUP_image [simp]: "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))" |
|
190 by (simp add: SUP_def image_image) |
|
191 |
|
192 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}" |
198 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}" |
193 by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) |
199 by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) |
194 |
200 |
195 lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}" |
201 lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}" |
196 by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) |
202 by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) |
198 lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B" |
204 lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B" |
199 by (auto intro: Inf_greatest Inf_lower) |
205 by (auto intro: Inf_greatest Inf_lower) |
200 |
206 |
201 lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B" |
207 lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B" |
202 by (auto intro: Sup_least Sup_upper) |
208 by (auto intro: Sup_least Sup_upper) |
203 |
|
204 lemma INF_cong: |
|
205 "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Sqinter>x\<in>A. C x) = (\<Sqinter>x\<in>B. D x)" |
|
206 by (simp add: INF_def image_def) |
|
207 |
|
208 lemma SUP_cong: |
|
209 "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Squnion>x\<in>A. C x) = (\<Squnion>x\<in>B. D x)" |
|
210 by (simp add: SUP_def image_def) |
|
211 |
209 |
212 lemma Inf_mono: |
210 lemma Inf_mono: |
213 assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b" |
211 assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b" |
214 shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B" |
212 shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B" |
215 proof (rule Inf_greatest) |
213 proof (rule Inf_greatest) |