6 *) |
6 *) |
7 |
7 |
8 header {* Fixed Points and the Knaster-Tarski Theorem*} |
8 header {* Fixed Points and the Knaster-Tarski Theorem*} |
9 |
9 |
10 theory FixedPoint |
10 theory FixedPoint |
11 imports Fun |
11 imports Lattices |
12 begin |
12 begin |
13 |
|
14 subsection {* Complete lattices *} |
|
15 |
|
16 class complete_lattice = lattice + |
|
17 fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900) |
|
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> \<Sqinter>A" |
|
20 begin |
|
21 |
|
22 definition |
|
23 Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900) |
|
24 where |
|
25 "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}" |
|
26 |
|
27 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<^loc>\<le> a}" |
|
28 unfolding Sup_def by (auto intro: Inf_greatest Inf_lower) |
|
29 |
|
30 lemma Sup_upper: "x \<in> A \<Longrightarrow> x \<^loc>\<le> \<Squnion>A" |
|
31 by (auto simp: Sup_def intro: Inf_greatest) |
|
32 |
|
33 lemma Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<^loc>\<le> z) \<Longrightarrow> \<Squnion>A \<^loc>\<le> z" |
|
34 by (auto simp: Sup_def intro: Inf_lower) |
|
35 |
|
36 lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}" |
|
37 unfolding Sup_def by auto |
|
38 |
|
39 lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}" |
|
40 unfolding Inf_Sup by auto |
|
41 |
|
42 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A" |
|
43 apply (rule antisym) |
|
44 apply (rule le_infI) |
|
45 apply (rule Inf_lower) |
|
46 apply simp |
|
47 apply (rule Inf_greatest) |
|
48 apply (rule Inf_lower) |
|
49 apply simp |
|
50 apply (rule Inf_greatest) |
|
51 apply (erule insertE) |
|
52 apply (rule le_infI1) |
|
53 apply simp |
|
54 apply (rule le_infI2) |
|
55 apply (erule Inf_lower) |
|
56 done |
|
57 |
|
58 lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A" |
|
59 apply (rule antisym) |
|
60 apply (rule Sup_least) |
|
61 apply (erule insertE) |
|
62 apply (rule le_supI1) |
|
63 apply simp |
|
64 apply (rule le_supI2) |
|
65 apply (erule Sup_upper) |
|
66 apply (rule le_supI) |
|
67 apply (rule Sup_upper) |
|
68 apply simp |
|
69 apply (rule Sup_least) |
|
70 apply (rule Sup_upper) |
|
71 apply simp |
|
72 done |
|
73 |
|
74 lemma Inf_singleton [simp]: |
|
75 "\<Sqinter>{a} = a" |
|
76 by (auto intro: antisym Inf_lower Inf_greatest) |
|
77 |
|
78 lemma Sup_singleton [simp]: |
|
79 "\<Squnion>{a} = a" |
|
80 by (auto intro: antisym Sup_upper Sup_least) |
|
81 |
|
82 lemma Inf_insert_simp: |
|
83 "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)" |
|
84 by (cases "A = {}") (simp_all, simp add: Inf_insert) |
|
85 |
|
86 lemma Sup_insert_simp: |
|
87 "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)" |
|
88 by (cases "A = {}") (simp_all, simp add: Sup_insert) |
|
89 |
|
90 lemma Inf_binary: |
|
91 "\<Sqinter>{a, b} = a \<sqinter> b" |
|
92 by (simp add: Inf_insert_simp) |
|
93 |
|
94 lemma Sup_binary: |
|
95 "\<Squnion>{a, b} = a \<squnion> b" |
|
96 by (simp add: Sup_insert_simp) |
|
97 |
|
98 end |
|
99 |
|
100 lemmas Sup_def = Sup_def [folded complete_lattice_class.Sup] |
|
101 lemmas Sup_upper = Sup_upper [folded complete_lattice_class.Sup] |
|
102 lemmas Sup_least = Sup_least [folded complete_lattice_class.Sup] |
|
103 |
|
104 lemmas Sup_insert [code func] = Sup_insert [folded complete_lattice_class.Sup] |
|
105 lemmas Sup_singleton [simp, code func] = Sup_singleton [folded complete_lattice_class.Sup] |
|
106 lemmas Sup_insert_simp = Sup_insert_simp [folded complete_lattice_class.Sup] |
|
107 lemmas Sup_binary = Sup_binary [folded complete_lattice_class.Sup] |
|
108 |
|
109 (* FIXME: definition inside class does not work *) |
|
110 definition |
|
111 top :: "'a::complete_lattice" |
|
112 where |
|
113 "top = Inf {}" |
|
114 |
|
115 definition |
|
116 bot :: "'a::complete_lattice" |
|
117 where |
|
118 "bot = Sup {}" |
|
119 |
|
120 lemma top_greatest [simp]: "x \<le> top" |
|
121 by (unfold top_def, rule Inf_greatest, simp) |
|
122 |
|
123 lemma bot_least [simp]: "bot \<le> x" |
|
124 by (unfold bot_def, rule Sup_least, simp) |
|
125 |
|
126 definition |
|
127 SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where |
|
128 "SUPR A f == Sup (f ` A)" |
|
129 |
|
130 definition |
|
131 INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where |
|
132 "INFI A f == Inf (f ` A)" |
|
133 |
|
134 syntax |
|
135 "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10) |
|
136 "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 10] 10) |
|
137 "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10) |
|
138 "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 10] 10) |
|
139 |
|
140 translations |
|
141 "SUP x y. B" == "SUP x. SUP y. B" |
|
142 "SUP x. B" == "CONST SUPR UNIV (%x. B)" |
|
143 "SUP x. B" == "SUP x:UNIV. B" |
|
144 "SUP x:A. B" == "CONST SUPR A (%x. B)" |
|
145 "INF x y. B" == "INF x. INF y. B" |
|
146 "INF x. B" == "CONST INFI UNIV (%x. B)" |
|
147 "INF x. B" == "INF x:UNIV. B" |
|
148 "INF x:A. B" == "CONST INFI A (%x. B)" |
|
149 |
|
150 (* To avoid eta-contraction of body: *) |
|
151 print_translation {* |
|
152 let |
|
153 fun btr' syn (A :: Abs abs :: ts) = |
|
154 let val (x,t) = atomic_abs_tr' abs |
|
155 in list_comb (Syntax.const syn $ x $ A $ t, ts) end |
|
156 val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const |
|
157 in |
|
158 [(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")] |
|
159 end |
|
160 *} |
|
161 |
|
162 lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)" |
|
163 by (auto simp add: SUPR_def intro: Sup_upper) |
|
164 |
|
165 lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u" |
|
166 by (auto simp add: SUPR_def intro: Sup_least) |
|
167 |
|
168 lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i" |
|
169 by (auto simp add: INFI_def intro: Inf_lower) |
|
170 |
|
171 lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)" |
|
172 by (auto simp add: INFI_def intro: Inf_greatest) |
|
173 |
|
174 lemma mono_inf: "mono f \<Longrightarrow> f (inf A B) <= inf (f A) (f B)" |
|
175 by (auto simp add: mono_def) |
|
176 |
|
177 lemma mono_sup: "mono f \<Longrightarrow> sup (f A) (f B) <= f (sup A B)" |
|
178 by (auto simp add: mono_def) |
|
179 |
|
180 lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M" |
|
181 by (auto intro: order_antisym SUP_leI le_SUPI) |
|
182 |
|
183 lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M" |
|
184 by (auto intro: order_antisym INF_leI le_INFI) |
|
185 |
|
186 |
|
187 subsection {* Some instances of the type class of complete lattices *} |
|
188 |
|
189 subsubsection {* Booleans *} |
|
190 |
|
191 instance bool :: complete_lattice |
|
192 Inf_bool_def: "Inf A \<equiv> \<forall>x\<in>A. x" |
|
193 apply intro_classes |
|
194 apply (unfold Inf_bool_def) |
|
195 apply (iprover intro!: le_boolI elim: ballE) |
|
196 apply (iprover intro!: ballI le_boolI elim: ballE le_boolE) |
|
197 done |
|
198 |
|
199 theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)" |
|
200 apply (rule order_antisym) |
|
201 apply (rule Sup_least) |
|
202 apply (rule le_boolI) |
|
203 apply (erule bexI, assumption) |
|
204 apply (rule le_boolI) |
|
205 apply (erule bexE) |
|
206 apply (rule le_boolE) |
|
207 apply (rule Sup_upper) |
|
208 apply assumption+ |
|
209 done |
|
210 |
|
211 lemma Inf_empty_bool [simp]: |
|
212 "Inf {}" |
|
213 unfolding Inf_bool_def by auto |
|
214 |
|
215 lemma not_Sup_empty_bool [simp]: |
|
216 "\<not> Sup {}" |
|
217 unfolding Sup_def Inf_bool_def by auto |
|
218 |
|
219 lemma top_bool_eq: "top = True" |
|
220 by (iprover intro!: order_antisym le_boolI top_greatest) |
|
221 |
|
222 lemma bot_bool_eq: "bot = False" |
|
223 by (iprover intro!: order_antisym le_boolI bot_least) |
|
224 |
|
225 |
|
226 subsubsection {* Functions *} |
|
227 |
|
228 instance "fun" :: (type, complete_lattice) complete_lattice |
|
229 Inf_fun_def: "Inf A \<equiv> (\<lambda>x. Inf {y. \<exists>f\<in>A. y = f x})" |
|
230 apply intro_classes |
|
231 apply (unfold Inf_fun_def) |
|
232 apply (rule le_funI) |
|
233 apply (rule Inf_lower) |
|
234 apply (rule CollectI) |
|
235 apply (rule bexI) |
|
236 apply (rule refl) |
|
237 apply assumption |
|
238 apply (rule le_funI) |
|
239 apply (rule Inf_greatest) |
|
240 apply (erule CollectE) |
|
241 apply (erule bexE) |
|
242 apply (iprover elim: le_funE) |
|
243 done |
|
244 |
|
245 lemmas [code func del] = Inf_fun_def |
|
246 |
|
247 theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})" |
|
248 apply (rule order_antisym) |
|
249 apply (rule Sup_least) |
|
250 apply (rule le_funI) |
|
251 apply (rule Sup_upper) |
|
252 apply fast |
|
253 apply (rule le_funI) |
|
254 apply (rule Sup_least) |
|
255 apply (erule CollectE) |
|
256 apply (erule bexE) |
|
257 apply (drule le_funD [OF Sup_upper]) |
|
258 apply simp |
|
259 done |
|
260 |
|
261 lemma Inf_empty_fun: |
|
262 "Inf {} = (\<lambda>_. Inf {})" |
|
263 by rule (auto simp add: Inf_fun_def) |
|
264 |
|
265 lemma Sup_empty_fun: |
|
266 "Sup {} = (\<lambda>_. Sup {})" |
|
267 proof - |
|
268 have aux: "\<And>x. {y. \<exists>f. y = f x} = UNIV" by auto |
|
269 show ?thesis |
|
270 by (auto simp add: Sup_def Inf_fun_def Inf_binary inf_bool_eq aux) |
|
271 qed |
|
272 |
|
273 lemma top_fun_eq: "top = (\<lambda>x. top)" |
|
274 by (iprover intro!: order_antisym le_funI top_greatest) |
|
275 |
|
276 lemma bot_fun_eq: "bot = (\<lambda>x. bot)" |
|
277 by (iprover intro!: order_antisym le_funI bot_least) |
|
278 |
|
279 |
|
280 subsubsection {* Sets *} |
|
281 |
|
282 instance set :: (type) complete_lattice |
|
283 Inf_set_def: "Inf S \<equiv> \<Inter>S" |
|
284 by intro_classes (auto simp add: Inf_set_def) |
|
285 |
|
286 lemmas [code func del] = Inf_set_def |
|
287 |
|
288 theorem Sup_set_eq: "Sup S = \<Union>S" |
|
289 apply (rule subset_antisym) |
|
290 apply (rule Sup_least) |
|
291 apply (erule Union_upper) |
|
292 apply (rule Union_least) |
|
293 apply (erule Sup_upper) |
|
294 done |
|
295 |
|
296 lemma top_set_eq: "top = UNIV" |
|
297 by (iprover intro!: subset_antisym subset_UNIV top_greatest) |
|
298 |
|
299 lemma bot_set_eq: "bot = {}" |
|
300 by (iprover intro!: subset_antisym empty_subsetI bot_least) |
|
301 |
|
302 |
13 |
303 subsection {* Least and greatest fixed points *} |
14 subsection {* Least and greatest fixed points *} |
304 |
15 |
305 definition |
16 definition |
306 lfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where |
17 lfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where |