src/HOL/Lattices_Big.thy
 author paulson Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) changeset 62379 340738057c8c parent 61776 57bb7da5c867 child 63290 9ac558ab0906 permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
1 (*  Title:      HOL/Lattices_Big.thy
2     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
3                 with contributions by Jeremy Avigad
4 *)
6 section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close>
8 theory Lattices_Big
9 imports Finite_Set Option
10 begin
12 subsection \<open>Generic lattice operations over a set\<close>
14 no_notation times (infixl "*" 70)
15 no_notation Groups.one ("1")
18 subsubsection \<open>Without neutral element\<close>
20 locale semilattice_set = semilattice
21 begin
23 interpretation comp_fun_idem f
24   by standard (simp_all add: fun_eq_iff left_commute)
26 definition F :: "'a set \<Rightarrow> 'a"
27 where
28   eq_fold': "F A = the (Finite_Set.fold (\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)) None A)"
30 lemma eq_fold:
31   assumes "finite A"
32   shows "F (insert x A) = Finite_Set.fold f x A"
33 proof (rule sym)
34   let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
35   interpret comp_fun_idem "?f"
36     by standard (simp_all add: fun_eq_iff commute left_commute split: option.split)
37   from assms show "Finite_Set.fold f x A = F (insert x A)"
38   proof induct
39     case empty then show ?case by (simp add: eq_fold')
40   next
41     case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold')
42   qed
43 qed
45 lemma singleton [simp]:
46   "F {x} = x"
47   by (simp add: eq_fold)
49 lemma insert_not_elem:
50   assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
51   shows "F (insert x A) = x * F A"
52 proof -
53   from \<open>A \<noteq> {}\<close> obtain b where "b \<in> A" by blast
54   then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
55   with \<open>finite A\<close> and \<open>x \<notin> A\<close>
56     have "finite (insert x B)" and "b \<notin> insert x B" by auto
57   then have "F (insert b (insert x B)) = x * F (insert b B)"
58     by (simp add: eq_fold)
59   then show ?thesis by (simp add: * insert_commute)
60 qed
62 lemma in_idem:
63   assumes "finite A" and "x \<in> A"
64   shows "x * F A = F A"
65 proof -
66   from assms have "A \<noteq> {}" by auto
67   with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
68     by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
69 qed
71 lemma insert [simp]:
72   assumes "finite A" and "A \<noteq> {}"
73   shows "F (insert x A) = x * F A"
74   using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
76 lemma union:
77   assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
78   shows "F (A \<union> B) = F A * F B"
79   using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
81 lemma remove:
82   assumes "finite A" and "x \<in> A"
83   shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
84 proof -
85   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
86   with assms show ?thesis by simp
87 qed
89 lemma insert_remove:
90   assumes "finite A"
91   shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
92   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
94 lemma subset:
95   assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
96   shows "F B * F A = F A"
97 proof -
98   from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
99   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
100 qed
102 lemma closed:
103   assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
104   shows "F A \<in> A"
105 using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
106   case singleton then show ?case by simp
107 next
108   case insert with elem show ?case by force
109 qed
111 lemma hom_commute:
112   assumes hom: "\<And>x y. h (x * y) = h x * h y"
113   and N: "finite N" "N \<noteq> {}"
114   shows "h (F N) = F (h ` N)"
115 using N proof (induct rule: finite_ne_induct)
116   case singleton thus ?case by simp
117 next
118   case (insert n N)
119   then have "h (F (insert n N)) = h (n * F N)" by simp
120   also have "\<dots> = h n * h (F N)" by (rule hom)
121   also have "h (F N) = F (h ` N)" by (rule insert)
122   also have "h n * \<dots> = F (insert (h n) (h ` N))"
123     using insert by simp
124   also have "insert (h n) (h ` N) = h ` insert n N" by simp
125   finally show ?case .
126 qed
128 lemma infinite: "\<not> finite A \<Longrightarrow> F A = the None"
129   unfolding eq_fold' by (cases "finite (UNIV::'a set)") (auto intro: finite_subset fold_infinite)
131 end
133 locale semilattice_order_set = binary?: semilattice_order + semilattice_set
134 begin
136 lemma bounded_iff:
137   assumes "finite A" and "A \<noteq> {}"
138   shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
139   using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
141 lemma boundedI:
142   assumes "finite A"
143   assumes "A \<noteq> {}"
144   assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
145   shows "x \<preceq> F A"
146   using assms by (simp add: bounded_iff)
148 lemma boundedE:
149   assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
150   obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
151   using assms by (simp add: bounded_iff)
153 lemma coboundedI:
154   assumes "finite A"
155     and "a \<in> A"
156   shows "F A \<preceq> a"
157 proof -
158   from assms have "A \<noteq> {}" by auto
159   from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
160   proof (induct rule: finite_ne_induct)
161     case singleton thus ?case by (simp add: refl)
162   next
163     case (insert x B)
164     from insert have "a = x \<or> a \<in> B" by simp
165     then show ?case using insert by (auto intro: coboundedI2)
166   qed
167 qed
169 lemma antimono:
170   assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
171   shows "F B \<preceq> F A"
172 proof (cases "A = B")
173   case True then show ?thesis by (simp add: refl)
174 next
175   case False
176   have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
177   then have "F B = F (A \<union> (B - A))" by simp
178   also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
179   also have "\<dots> \<preceq> F A" by simp
180   finally show ?thesis .
181 qed
183 end
186 subsubsection \<open>With neutral element\<close>
188 locale semilattice_neutr_set = semilattice_neutr
189 begin
191 interpretation comp_fun_idem f
192   by standard (simp_all add: fun_eq_iff left_commute)
194 definition F :: "'a set \<Rightarrow> 'a"
195 where
196   eq_fold: "F A = Finite_Set.fold f 1 A"
198 lemma infinite [simp]:
199   "\<not> finite A \<Longrightarrow> F A = 1"
200   by (simp add: eq_fold)
202 lemma empty [simp]:
203   "F {} = 1"
204   by (simp add: eq_fold)
206 lemma insert [simp]:
207   assumes "finite A"
208   shows "F (insert x A) = x * F A"
209   using assms by (simp add: eq_fold)
211 lemma in_idem:
212   assumes "finite A" and "x \<in> A"
213   shows "x * F A = F A"
214 proof -
215   from assms have "A \<noteq> {}" by auto
216   with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
217     by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
218 qed
220 lemma union:
221   assumes "finite A" and "finite B"
222   shows "F (A \<union> B) = F A * F B"
223   using assms by (induct A) (simp_all add: ac_simps)
225 lemma remove:
226   assumes "finite A" and "x \<in> A"
227   shows "F A = x * F (A - {x})"
228 proof -
229   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
230   with assms show ?thesis by simp
231 qed
233 lemma insert_remove:
234   assumes "finite A"
235   shows "F (insert x A) = x * F (A - {x})"
236   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
238 lemma subset:
239   assumes "finite A" and "B \<subseteq> A"
240   shows "F B * F A = F A"
241 proof -
242   from assms have "finite B" by (auto dest: finite_subset)
243   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
244 qed
246 lemma closed:
247   assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
248   shows "F A \<in> A"
249 using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
250   case singleton then show ?case by simp
251 next
252   case insert with elem show ?case by force
253 qed
255 end
257 locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set
258 begin
260 lemma bounded_iff:
261   assumes "finite A"
262   shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
263   using assms by (induct A) (simp_all add: bounded_iff)
265 lemma boundedI:
266   assumes "finite A"
267   assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
268   shows "x \<preceq> F A"
269   using assms by (simp add: bounded_iff)
271 lemma boundedE:
272   assumes "finite A" and "x \<preceq> F A"
273   obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
274   using assms by (simp add: bounded_iff)
276 lemma coboundedI:
277   assumes "finite A"
278     and "a \<in> A"
279   shows "F A \<preceq> a"
280 proof -
281   from assms have "A \<noteq> {}" by auto
282   from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
283   proof (induct rule: finite_ne_induct)
284     case singleton thus ?case by (simp add: refl)
285   next
286     case (insert x B)
287     from insert have "a = x \<or> a \<in> B" by simp
288     then show ?case using insert by (auto intro: coboundedI2)
289   qed
290 qed
292 lemma antimono:
293   assumes "A \<subseteq> B" and "finite B"
294   shows "F B \<preceq> F A"
295 proof (cases "A = B")
296   case True then show ?thesis by (simp add: refl)
297 next
298   case False
299   have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
300   then have "F B = F (A \<union> (B - A))" by simp
301   also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
302   also have "\<dots> \<preceq> F A" by simp
303   finally show ?thesis .
304 qed
306 end
308 notation times (infixl "*" 70)
309 notation Groups.one ("1")
312 subsection \<open>Lattice operations on finite sets\<close>
314 context semilattice_inf
315 begin
317 sublocale Inf_fin: semilattice_order_set inf less_eq less
318 defines
319   Inf_fin ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_"  900) = Inf_fin.F ..
321 end
323 context semilattice_sup
324 begin
326 sublocale Sup_fin: semilattice_order_set sup greater_eq greater
327 defines
328   Sup_fin ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_"  900) = Sup_fin.F ..
330 end
333 subsection \<open>Infimum and Supremum over non-empty sets\<close>
335 context lattice
336 begin
338 lemma Inf_fin_le_Sup_fin [simp]:
339   assumes "finite A" and "A \<noteq> {}"
340   shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
341 proof -
342   from \<open>A \<noteq> {}\<close> obtain a where "a \<in> A" by blast
343   with \<open>finite A\<close> have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI)
344   moreover from \<open>finite A\<close> \<open>a \<in> A\<close> have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI)
345   ultimately show ?thesis by (rule order_trans)
346 qed
348 lemma sup_Inf_absorb [simp]:
349   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<squnion> a = a"
350   by (rule sup_absorb2) (rule Inf_fin.coboundedI)
352 lemma inf_Sup_absorb [simp]:
353   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> a \<sqinter> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA = a"
354   by (rule inf_absorb1) (rule Sup_fin.coboundedI)
356 end
358 context distrib_lattice
359 begin
361 lemma sup_Inf1_distrib:
362   assumes "finite A"
363     and "A \<noteq> {}"
364   shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}"
365 using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
366   (rule arg_cong [where f="Inf_fin"], blast)
368 lemma sup_Inf2_distrib:
369   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
370   shows "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B}"
371 using A proof (induct rule: finite_ne_induct)
372   case singleton then show ?case
373     by (simp add: sup_Inf1_distrib [OF B])
374 next
375   case (insert x A)
376   have finB: "finite {sup x b |b. b \<in> B}"
377     by (rule finite_surj [where f = "sup x", OF B(1)], auto)
378   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
379   proof -
380     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
381       by blast
382     thus ?thesis by(simp add: insert(1) B(1))
383   qed
384   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
385   have "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = sup (inf x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)"
386     using insert by simp
387   also have "\<dots> = inf (sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)) (sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB))" by(rule sup_inf_distrib2)
388   also have "\<dots> = inf (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x b|b. b \<in> B}) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B})"
389     using insert by(simp add:sup_Inf1_distrib[OF B])
390   also have "\<dots> = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
391     (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
392     using B insert
393     by (simp add: Inf_fin.union [OF finB _ finAB ne])
394   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
395     by blast
396   finally show ?case .
397 qed
399 lemma inf_Sup1_distrib:
400   assumes "finite A" and "A \<noteq> {}"
401   shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}"
402 using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
403   (rule arg_cong [where f="Sup_fin"], blast)
405 lemma inf_Sup2_distrib:
406   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
407   shows "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B}"
408 using A proof (induct rule: finite_ne_induct)
409   case singleton thus ?case
410     by(simp add: inf_Sup1_distrib [OF B])
411 next
412   case (insert x A)
413   have finB: "finite {inf x b |b. b \<in> B}"
414     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
415   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
416   proof -
417     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
418       by blast
419     thus ?thesis by(simp add: insert(1) B(1))
420   qed
421   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
422   have "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = inf (sup x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)"
423     using insert by simp
424   also have "\<dots> = sup (inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)) (inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB))" by(rule inf_sup_distrib2)
425   also have "\<dots> = sup (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x b|b. b \<in> B}) (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B})"
426     using insert by(simp add:inf_Sup1_distrib[OF B])
427   also have "\<dots> = \<Squnion>\<^sub>f\<^sub>i\<^sub>n({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
428     (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
429     using B insert
430     by (simp add: Sup_fin.union [OF finB _ finAB ne])
431   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
432     by blast
433   finally show ?case .
434 qed
436 end
438 context complete_lattice
439 begin
441 lemma Inf_fin_Inf:
442   assumes "finite A" and "A \<noteq> {}"
443   shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = \<Sqinter>A"
444 proof -
445   from assms obtain b B where "A = insert b B" and "finite B" by auto
446   then show ?thesis
447     by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
448 qed
450 lemma Sup_fin_Sup:
451   assumes "finite A" and "A \<noteq> {}"
452   shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = \<Squnion>A"
453 proof -
454   from assms obtain b B where "A = insert b B" and "finite B" by auto
455   then show ?thesis
456     by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
457 qed
459 end
462 subsection \<open>Minimum and Maximum over non-empty sets\<close>
464 context linorder
465 begin
467 sublocale Min: semilattice_order_set min less_eq less
468   + Max: semilattice_order_set max greater_eq greater
469 defines
470   Min = Min.F and Max = Max.F ..
472 end
474 text \<open>An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin}\<close>
476 lemma Inf_fin_Min:
477   "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
478   by (simp add: Inf_fin_def Min_def inf_min)
480 lemma Sup_fin_Max:
481   "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
482   by (simp add: Sup_fin_def Max_def sup_max)
484 context linorder
485 begin
487 lemma dual_min:
488   "ord.min greater_eq = max"
489   by (auto simp add: ord.min_def max_def fun_eq_iff)
491 lemma dual_max:
492   "ord.max greater_eq = min"
493   by (auto simp add: ord.max_def min_def fun_eq_iff)
495 lemma dual_Min:
496   "linorder.Min greater_eq = Max"
497 proof -
498   interpret dual: linorder greater_eq greater by (fact dual_linorder)
499   show ?thesis by (simp add: dual.Min_def dual_min Max_def)
500 qed
502 lemma dual_Max:
503   "linorder.Max greater_eq = Min"
504 proof -
505   interpret dual: linorder greater_eq greater by (fact dual_linorder)
506   show ?thesis by (simp add: dual.Max_def dual_max Min_def)
507 qed
509 lemmas Min_singleton = Min.singleton
510 lemmas Max_singleton = Max.singleton
511 lemmas Min_insert = Min.insert
512 lemmas Max_insert = Max.insert
513 lemmas Min_Un = Min.union
514 lemmas Max_Un = Max.union
515 lemmas hom_Min_commute = Min.hom_commute
516 lemmas hom_Max_commute = Max.hom_commute
518 lemma Min_in [simp]:
519   assumes "finite A" and "A \<noteq> {}"
520   shows "Min A \<in> A"
521   using assms by (auto simp add: min_def Min.closed)
523 lemma Max_in [simp]:
524   assumes "finite A" and "A \<noteq> {}"
525   shows "Max A \<in> A"
526   using assms by (auto simp add: max_def Max.closed)
528 lemma Min_insert2:
529   assumes "finite A" and min: "\<And>b. b \<in> A \<Longrightarrow> a \<le> b"
530   shows "Min (insert a A) = a"
531 proof (cases "A = {}")
532   case True then show ?thesis by simp
533 next
534   case False with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)"
535     by simp
536   moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> min have "a \<le> Min A" by simp
537   ultimately show ?thesis by (simp add: min.absorb1)
538 qed
540 lemma Max_insert2:
541   assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> a"
542   shows "Max (insert a A) = a"
543 proof (cases "A = {}")
544   case True then show ?thesis by simp
545 next
546   case False with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)"
547     by simp
548   moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> max have "Max A \<le> a" by simp
549   ultimately show ?thesis by (simp add: max.absorb1)
550 qed
552 lemma Min_le [simp]:
553   assumes "finite A" and "x \<in> A"
554   shows "Min A \<le> x"
555   using assms by (fact Min.coboundedI)
557 lemma Max_ge [simp]:
558   assumes "finite A" and "x \<in> A"
559   shows "x \<le> Max A"
560   using assms by (fact Max.coboundedI)
562 lemma Min_eqI:
563   assumes "finite A"
564   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
565     and "x \<in> A"
566   shows "Min A = x"
567 proof (rule antisym)
568   from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto
569   with assms show "Min A \<ge> x" by simp
570 next
571   from assms show "x \<ge> Min A" by simp
572 qed
574 lemma Max_eqI:
575   assumes "finite A"
576   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
577     and "x \<in> A"
578   shows "Max A = x"
579 proof (rule antisym)
580   from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto
581   with assms show "Max A \<le> x" by simp
582 next
583   from assms show "x \<le> Max A" by simp
584 qed
586 context
587   fixes A :: "'a set"
588   assumes fin_nonempty: "finite A" "A \<noteq> {}"
589 begin
591 lemma Min_ge_iff [simp]:
592   "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
593   using fin_nonempty by (fact Min.bounded_iff)
595 lemma Max_le_iff [simp]:
596   "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
597   using fin_nonempty by (fact Max.bounded_iff)
599 lemma Min_gr_iff [simp]:
600   "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
601   using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
603 lemma Max_less_iff [simp]:
604   "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
605   using fin_nonempty by (induct rule: finite_ne_induct) simp_all
607 lemma Min_le_iff:
608   "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
609   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
611 lemma Max_ge_iff:
612   "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
613   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
615 lemma Min_less_iff:
616   "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
617   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
619 lemma Max_gr_iff:
620   "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
621   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
623 end
625 lemma Max_eq_if:
626   assumes "finite A"  "finite B"  "\<forall>a\<in>A. \<exists>b\<in>B. a \<le> b"  "\<forall>b\<in>B. \<exists>a\<in>A. b \<le> a"
627   shows "Max A = Max B"
628 proof cases
629   assume "A = {}" thus ?thesis using assms by simp
630 next
631   assume "A \<noteq> {}" thus ?thesis using assms
632     by(blast intro: antisym Max_in Max_ge_iff[THEN iffD2])
633 qed
635 lemma Min_antimono:
636   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
637   shows "Min N \<le> Min M"
638   using assms by (fact Min.antimono)
640 lemma Max_mono:
641   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
642   shows "Max M \<le> Max N"
643   using assms by (fact Max.antimono)
645 end
647 context linorder  (* FIXME *)
648 begin
650 lemma mono_Min_commute:
651   assumes "mono f"
652   assumes "finite A" and "A \<noteq> {}"
653   shows "f (Min A) = Min (f ` A)"
654 proof (rule linorder_class.Min_eqI [symmetric])
655   from \<open>finite A\<close> show "finite (f ` A)" by simp
656   from assms show "f (Min A) \<in> f ` A" by simp
657   fix x
658   assume "x \<in> f ` A"
659   then obtain y where "y \<in> A" and "x = f y" ..
660   with assms have "Min A \<le> y" by auto
661   with \<open>mono f\<close> have "f (Min A) \<le> f y" by (rule monoE)
662   with \<open>x = f y\<close> show "f (Min A) \<le> x" by simp
663 qed
665 lemma mono_Max_commute:
666   assumes "mono f"
667   assumes "finite A" and "A \<noteq> {}"
668   shows "f (Max A) = Max (f ` A)"
669 proof (rule linorder_class.Max_eqI [symmetric])
670   from \<open>finite A\<close> show "finite (f ` A)" by simp
671   from assms show "f (Max A) \<in> f ` A" by simp
672   fix x
673   assume "x \<in> f ` A"
674   then obtain y where "y \<in> A" and "x = f y" ..
675   with assms have "y \<le> Max A" by auto
676   with \<open>mono f\<close> have "f y \<le> f (Max A)" by (rule monoE)
677   with \<open>x = f y\<close> show "x \<le> f (Max A)" by simp
678 qed
680 lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
681   assumes fin: "finite A"
682   and empty: "P {}"
683   and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
684   shows "P A"
685 using fin empty insert
686 proof (induct rule: finite_psubset_induct)
687   case (psubset A)
688   have IH: "\<And>B. \<lbrakk>B < A; P {}; (\<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. a<b; P A\<rbrakk> \<Longrightarrow> P (insert b A))\<rbrakk> \<Longrightarrow> P B" by fact
689   have fin: "finite A" by fact
690   have empty: "P {}" by fact
691   have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
692   show "P A"
693   proof (cases "A = {}")
694     assume "A = {}"
695     then show "P A" using \<open>P {}\<close> by simp
696   next
697     let ?B = "A - {Max A}"
698     let ?A = "insert (Max A) ?B"
699     have "finite ?B" using \<open>finite A\<close> by simp
700     assume "A \<noteq> {}"
701     with \<open>finite A\<close> have "Max A : A" by auto
702     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
703     then have "P ?B" using \<open>P {}\<close> step IH [of ?B] by blast
704     moreover
705     have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF \<open>finite A\<close>] by fastforce
706     ultimately show "P A" using A insert_Diff_single step [OF \<open>finite ?B\<close>] by fastforce
707   qed
708 qed
710 lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
711   "\<lbrakk>finite A; P {}; \<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A"
712   by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
714 lemma Least_Min:
715   assumes "finite {a. P a}" and "\<exists>a. P a"
716   shows "(LEAST a. P a) = Min {a. P a}"
717 proof -
718   { fix A :: "'a set"
719     assume A: "finite A" "A \<noteq> {}"
720     have "(LEAST a. a \<in> A) = Min A"
721     using A proof (induct A rule: finite_ne_induct)
722       case singleton show ?case by (rule Least_equality) simp_all
723     next
724       case (insert a A)
725       have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
726         by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
727       with insert show ?case by simp
728     qed
729   } from this [of "{a. P a}"] assms show ?thesis by simp
730 qed
732 lemma infinite_growing:
733   assumes "X \<noteq> {}"
734   assumes *: "\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>X. y > x"
735   shows "\<not> finite X"
736 proof
737   assume "finite X"
738   with \<open>X \<noteq> {}\<close> have "Max X \<in> X" "\<forall>x\<in>X. x \<le> Max X"
739     by auto
740   with *[of "Max X"] show False
741     by auto
742 qed
744 end
747 begin
750   fixes k
751   assumes "finite N" and "N \<noteq> {}"
752   shows "k + Min N = Min {k + m | m. m \<in> N}"
753 proof -
754   have "\<And>x y. k + min x y = min (k + x) (k + y)"
755     by (simp add: min_def not_le)
756       (blast intro: antisym less_imp_le add_left_mono)
757   with assms show ?thesis
758     using hom_Min_commute [of "plus k" N]
759     by simp (blast intro: arg_cong [where f = Min])
760 qed
763   fixes k
764   assumes "finite N" and "N \<noteq> {}"
765   shows "k + Max N = Max {k + m | m. m \<in> N}"
766 proof -
767   have "\<And>x y. k + max x y = max (k + x) (k + y)"
768     by (simp add: max_def not_le)
769       (blast intro: antisym less_imp_le add_left_mono)
770   with assms show ?thesis
771     using hom_Max_commute [of "plus k" N]
772     by simp (blast intro: arg_cong [where f = Max])
773 qed
775 end
778 begin
780 lemma minus_Max_eq_Min [simp]:
781   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
782   by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
784 lemma minus_Min_eq_Max [simp]:
785   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
786   by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
788 end
790 context complete_linorder
791 begin
793 lemma Min_Inf:
794   assumes "finite A" and "A \<noteq> {}"
795   shows "Min A = Inf A"
796 proof -
797   from assms obtain b B where "A = insert b B" and "finite B" by auto
798   then show ?thesis
799     by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
800 qed
802 lemma Max_Sup:
803   assumes "finite A" and "A \<noteq> {}"
804   shows "Max A = Sup A"
805 proof -
806   from assms obtain b B where "A = insert b B" and "finite B" by auto
807   then show ?thesis
808     by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
809 qed
811 end
813 end