12 begin |
12 begin |
13 |
13 |
14 subsection {* Complete lattices *} |
14 subsection {* Complete lattices *} |
15 |
15 |
16 class complete_lattice = lattice + |
16 class complete_lattice = lattice + |
17 fixes Inf :: "'a set \<Rightarrow> 'a" |
17 fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90) |
18 assumes Inf_lower: "x \<in> A \<Longrightarrow> Inf A \<sqsubseteq> x" |
18 assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x" |
19 assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Inf A" |
19 assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A" |
20 |
20 |
21 definition |
21 definition |
22 Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a" where |
22 Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a" |
|
23 where |
23 "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}" |
24 "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}" |
24 |
25 |
25 theorem Sup_upper: "(x::'a::complete_lattice) \<in> A \<Longrightarrow> x <= Sup A" |
26 theorem Sup_upper: "(x::'a::complete_lattice) \<in> A \<Longrightarrow> x \<le> Sup A" |
26 by (auto simp: Sup_def intro: Inf_greatest) |
27 by (auto simp: Sup_def intro: Inf_greatest) |
27 |
28 |
28 theorem Sup_least: "(\<And>x::'a::complete_lattice. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z" |
29 theorem Sup_least: "(\<And>x::'a::complete_lattice. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup A \<le> z" |
29 by (auto simp: Sup_def intro: Inf_lower) |
30 by (auto simp: Sup_def intro: Inf_lower) |
30 |
31 |
31 definition |
32 definition |
32 SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where |
33 SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where |
33 "SUPR A f == Sup (f ` A)" |
34 "SUPR A f == Sup (f ` A)" |
196 apply (erule CollectE) |
197 apply (erule CollectE) |
197 apply (erule bexE) |
198 apply (erule bexE) |
198 apply (iprover elim: le_funE) |
199 apply (iprover elim: le_funE) |
199 done |
200 done |
200 |
201 |
201 lemmas [code nofunc] = Inf_fun_def |
202 lemmas [code func del] = Inf_fun_def |
202 |
203 |
203 theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})" |
204 theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})" |
204 apply (rule order_antisym) |
205 apply (rule order_antisym) |
205 apply (rule Sup_least) |
206 apply (rule Sup_least) |
206 apply (rule le_funI) |
207 apply (rule le_funI) |
219 |
220 |
220 instance set :: (type) complete_lattice |
221 instance set :: (type) complete_lattice |
221 Inf_set_def: "Inf S \<equiv> \<Inter>S" |
222 Inf_set_def: "Inf S \<equiv> \<Inter>S" |
222 by intro_classes (auto simp add: Inf_set_def) |
223 by intro_classes (auto simp add: Inf_set_def) |
223 |
224 |
224 lemmas [code nofunc] = Inf_set_def |
225 lemmas [code func del] = Inf_set_def |
225 |
226 |
226 theorem Sup_set_eq: "Sup S = \<Union>S" |
227 theorem Sup_set_eq: "Sup S = \<Union>S" |
227 apply (rule subset_antisym) |
228 apply (rule subset_antisym) |
228 apply (rule Sup_least) |
229 apply (rule Sup_least) |
229 apply (erule Union_upper) |
230 apply (erule Union_upper) |