(* Title: HOL/Lattices_Big.thy Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel with contributions by Jeremy Avigad *) section ‹Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets› theory Lattices_Big imports Option begin subsection ‹Generic lattice operations over a set› subsubsection ‹Without neutral element› locale semilattice_set = semilattice begin interpretation comp_fun_idem f by standard (simp_all add: fun_eq_iff left_commute) definition F :: "'a set ⇒ 'a" where eq_fold': "F A = the (Finite_Set.fold (λx y. Some (case y of None ⇒ x | Some z ⇒ f x z)) None A)" lemma eq_fold: assumes "finite A" shows "F (insert x A) = Finite_Set.fold f x A" proof (rule sym) let ?f = "λx y. Some (case y of None ⇒ x | Some z ⇒ f x z)" interpret comp_fun_idem "?f" by standard (simp_all add: fun_eq_iff commute left_commute split: option.split) from assms show "Finite_Set.fold f x A = F (insert x A)" proof induct case empty then show ?case by (simp add: eq_fold') next case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold') qed qed lemma singleton [simp]: "F {x} = x" by (simp add: eq_fold) lemma insert_not_elem: assumes "finite A" and "x ∉ A" and "A ≠ {}" shows "F (insert x A) = x ❙* F A" proof - from ‹A ≠ {}› obtain b where "b ∈ A" by blast then obtain B where *: "A = insert b B" "b ∉ B" by (blast dest: mk_disjoint_insert) with ‹finite A› and ‹x ∉ A› have "finite (insert x B)" and "b ∉ insert x B" by auto then have "F (insert b (insert x B)) = x ❙* F (insert b B)" by (simp add: eq_fold) then show ?thesis by (simp add: * insert_commute) qed lemma in_idem: assumes "finite A" and "x ∈ A" shows "x ❙* F A = F A" proof - from assms have "A ≠ {}" by auto with ‹finite A› show ?thesis using ‹x ∈ A› by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem) qed lemma insert [simp]: assumes "finite A" and "A ≠ {}" shows "F (insert x A) = x ❙* F A" using assms by (cases "x ∈ A") (simp_all add: insert_absorb in_idem insert_not_elem) lemma union: assumes "finite A" "A ≠ {}" and "finite B" "B ≠ {}" shows "F (A ∪ B) = F A ❙* F B" using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps) lemma remove: assumes "finite A" and "x ∈ A" shows "F A = (if A - {x} = {} then x else x ❙* F (A - {x}))" proof - from assms obtain B where "A = insert x B" and "x ∉ B" by (blast dest: mk_disjoint_insert) with assms show ?thesis by simp qed lemma insert_remove: assumes "finite A" shows "F (insert x A) = (if A - {x} = {} then x else x ❙* F (A - {x}))" using assms by (cases "x ∈ A") (simp_all add: insert_absorb remove) lemma subset: assumes "finite A" "B ≠ {}" and "B ⊆ A" shows "F B ❙* F A = F A" proof - from assms have "A ≠ {}" and "finite B" by (auto dest: finite_subset) with assms show ?thesis by (simp add: union [symmetric] Un_absorb1) qed lemma closed: assumes "finite A" "A ≠ {}" and elem: "⋀x y. x ❙* y ∈ {x, y}" shows "F A ∈ A" using ‹finite A› ‹A ≠ {}› proof (induct rule: finite_ne_induct) case singleton then show ?case by simp next case insert with elem show ?case by force qed lemma hom_commute: assumes hom: "⋀x y. h (x ❙* y) = h x ❙* h y" and N: "finite N" "N ≠ {}" shows "h (F N) = F (h ` N)" using N proof (induct rule: finite_ne_induct) case singleton thus ?case by simp next case (insert n N) then have "h (F (insert n N)) = h (n ❙* F N)" by simp also have "… = h n ❙* h (F N)" by (rule hom) also have "h (F N) = F (h ` N)" by (rule insert) also have "h n ❙* … = F (insert (h n) (h ` N))" using insert by simp also have "insert (h n) (h ` N) = h ` insert n N" by simp finally show ?case . qed lemma infinite: "¬ finite A ⟹ F A = the None" unfolding eq_fold' by (cases "finite (UNIV::'a set)") (auto intro: finite_subset fold_infinite) end locale semilattice_order_set = binary?: semilattice_order + semilattice_set begin lemma bounded_iff: assumes "finite A" and "A ≠ {}" shows "x ❙≤ F A ⟷ (∀a∈A. x ❙≤ a)" using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff) lemma boundedI: assumes "finite A" assumes "A ≠ {}" assumes "⋀a. a ∈ A ⟹ x ❙≤ a" shows "x ❙≤ F A" using assms by (simp add: bounded_iff) lemma boundedE: assumes "finite A" and "A ≠ {}" and "x ❙≤ F A" obtains "⋀a. a ∈ A ⟹ x ❙≤ a" using assms by (simp add: bounded_iff) lemma coboundedI: assumes "finite A" and "a ∈ A" shows "F A ❙≤ a" proof - from assms have "A ≠ {}" by auto from ‹finite A› ‹A ≠ {}› ‹a ∈ A› show ?thesis proof (induct rule: finite_ne_induct) case singleton thus ?case by (simp add: refl) next case (insert x B) from insert have "a = x ∨ a ∈ B" by simp then show ?case using insert by (auto intro: coboundedI2) qed qed lemma antimono: assumes "A ⊆ B" and "A ≠ {}" and "finite B" shows "F B ❙≤ F A" proof (cases "A = B") case True then show ?thesis by (simp add: refl) next case False have B: "B = A ∪ (B - A)" using ‹A ⊆ B› by blast then have "F B = F (A ∪ (B - A))" by simp also have "… = F A ❙* F (B - A)" using False assms by (subst union) (auto intro: finite_subset) also have "… ❙≤ F A" by simp finally show ?thesis . qed end subsubsection ‹With neutral element› locale semilattice_neutr_set = semilattice_neutr begin interpretation comp_fun_idem f by standard (simp_all add: fun_eq_iff left_commute) definition F :: "'a set ⇒ 'a" where eq_fold: "F A = Finite_Set.fold f ❙1 A" lemma infinite [simp]: "¬ finite A ⟹ F A = ❙1" by (simp add: eq_fold) lemma empty [simp]: "F {} = ❙1" by (simp add: eq_fold) lemma insert [simp]: assumes "finite A" shows "F (insert x A) = x ❙* F A" using assms by (simp add: eq_fold) lemma in_idem: assumes "finite A" and "x ∈ A" shows "x ❙* F A = F A" proof - from assms have "A ≠ {}" by auto with ‹finite A› show ?thesis using ‹x ∈ A› by (induct A rule: finite_ne_induct) (auto simp add: ac_simps) qed lemma union: assumes "finite A" and "finite B" shows "F (A ∪ B) = F A ❙* F B" using assms by (induct A) (simp_all add: ac_simps) lemma remove: assumes "finite A" and "x ∈ A" shows "F A = x ❙* F (A - {x})" proof - from assms obtain B where "A = insert x B" and "x ∉ B" by (blast dest: mk_disjoint_insert) with assms show ?thesis by simp qed lemma insert_remove: assumes "finite A" shows "F (insert x A) = x ❙* F (A - {x})" using assms by (cases "x ∈ A") (simp_all add: insert_absorb remove) lemma subset: assumes "finite A" and "B ⊆ A" shows "F B ❙* F A = F A" proof - from assms have "finite B" by (auto dest: finite_subset) with assms show ?thesis by (simp add: union [symmetric] Un_absorb1) qed lemma closed: assumes "finite A" "A ≠ {}" and elem: "⋀x y. x ❙* y ∈ {x, y}" shows "F A ∈ A" using ‹finite A› ‹A ≠ {}› proof (induct rule: finite_ne_induct) case singleton then show ?case by simp next case insert with elem show ?case by force qed end locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set begin lemma bounded_iff: assumes "finite A" shows "x ❙≤ F A ⟷ (∀a∈A. x ❙≤ a)" using assms by (induct A) (simp_all add: bounded_iff) lemma boundedI: assumes "finite A" assumes "⋀a. a ∈ A ⟹ x ❙≤ a" shows "x ❙≤ F A" using assms by (simp add: bounded_iff) lemma boundedE: assumes "finite A" and "x ❙≤ F A" obtains "⋀a. a ∈ A ⟹ x ❙≤ a" using assms by (simp add: bounded_iff) lemma coboundedI: assumes "finite A" and "a ∈ A" shows "F A ❙≤ a" proof - from assms have "A ≠ {}" by auto from ‹finite A› ‹A ≠ {}› ‹a ∈ A› show ?thesis proof (induct rule: finite_ne_induct) case singleton thus ?case by (simp add: refl) next case (insert x B) from insert have "a = x ∨ a ∈ B" by simp then show ?case using insert by (auto intro: coboundedI2) qed qed lemma antimono: assumes "A ⊆ B" and "finite B" shows "F B ❙≤ F A" proof (cases "A = B") case True then show ?thesis by (simp add: refl) next case False have B: "B = A ∪ (B - A)" using ‹A ⊆ B› by blast then have "F B = F (A ∪ (B - A))" by simp also have "… = F A ❙* F (B - A)" using False assms by (subst union) (auto intro: finite_subset) also have "… ❙≤ F A" by simp finally show ?thesis . qed end subsection ‹Lattice operations on finite sets› context semilattice_inf begin sublocale Inf_fin: semilattice_order_set inf less_eq less defines Inf_fin ("⨅⇩_{f}⇩_{i}⇩_{n}_" [900] 900) = Inf_fin.F .. end context semilattice_sup begin sublocale Sup_fin: semilattice_order_set sup greater_eq greater defines Sup_fin ("⨆⇩_{f}⇩_{i}⇩_{n}_" [900] 900) = Sup_fin.F .. end subsection ‹Infimum and Supremum over non-empty sets› context lattice begin lemma Inf_fin_le_Sup_fin [simp]: assumes "finite A" and "A ≠ {}" shows "⨅⇩_{f}⇩_{i}⇩_{n}A ≤ ⨆⇩_{f}⇩_{i}⇩_{n}A" proof - from ‹A ≠ {}› obtain a where "a ∈ A" by blast with ‹finite A› have "⨅⇩_{f}⇩_{i}⇩_{n}A ≤ a" by (rule Inf_fin.coboundedI) moreover from ‹finite A› ‹a ∈ A› have "a ≤ ⨆⇩_{f}⇩_{i}⇩_{n}A" by (rule Sup_fin.coboundedI) ultimately show ?thesis by (rule order_trans) qed lemma sup_Inf_absorb [simp]: "finite A ⟹ a ∈ A ⟹ ⨅⇩_{f}⇩_{i}⇩_{n}A ⊔ a = a" by (rule sup_absorb2) (rule Inf_fin.coboundedI) lemma inf_Sup_absorb [simp]: "finite A ⟹ a ∈ A ⟹ a ⊓ ⨆⇩_{f}⇩_{i}⇩_{n}A = a" by (rule inf_absorb1) (rule Sup_fin.coboundedI) end context distrib_lattice begin lemma sup_Inf1_distrib: assumes "finite A" and "A ≠ {}" shows "sup x (⨅⇩_{f}⇩_{i}⇩_{n}A) = ⨅⇩_{f}⇩_{i}⇩_{n}{sup x a|a. a ∈ A}" using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1]) (rule arg_cong [where f="Inf_fin"], blast) lemma sup_Inf2_distrib: assumes A: "finite A" "A ≠ {}" and B: "finite B" "B ≠ {}" shows "sup (⨅⇩_{f}⇩_{i}⇩_{n}A) (⨅⇩_{f}⇩_{i}⇩_{n}B) = ⨅⇩_{f}⇩_{i}⇩_{n}{sup a b|a b. a ∈ A ∧ b ∈ B}" using A proof (induct rule: finite_ne_induct) case singleton then show ?case by (simp add: sup_Inf1_distrib [OF B]) next case (insert x A) have finB: "finite {sup x b |b. b ∈ B}" by (rule finite_surj [where f = "sup x", OF B(1)], auto) have finAB: "finite {sup a b |a b. a ∈ A ∧ b ∈ B}" proof - have "{sup a b |a b. a ∈ A ∧ b ∈ B} = (UN a:A. UN b:B. {sup a b})" by blast thus ?thesis by(simp add: insert(1) B(1)) qed have ne: "{sup a b |a b. a ∈ A ∧ b ∈ B} ≠ {}" using insert B by blast have "sup (⨅⇩_{f}⇩_{i}⇩_{n}(insert x A)) (⨅⇩_{f}⇩_{i}⇩_{n}B) = sup (inf x (⨅⇩_{f}⇩_{i}⇩_{n}A)) (⨅⇩_{f}⇩_{i}⇩_{n}B)" using insert by simp also have "… = inf (sup x (⨅⇩_{f}⇩_{i}⇩_{n}B)) (sup (⨅⇩_{f}⇩_{i}⇩_{n}A) (⨅⇩_{f}⇩_{i}⇩_{n}B))" by(rule sup_inf_distrib2) also have "… = inf (⨅⇩_{f}⇩_{i}⇩_{n}{sup x b|b. b ∈ B}) (⨅⇩_{f}⇩_{i}⇩_{n}{sup a b|a b. a ∈ A ∧ b ∈ B})" using insert by(simp add:sup_Inf1_distrib[OF B]) also have "… = ⨅⇩_{f}⇩_{i}⇩_{n}({sup x b |b. b ∈ B} ∪ {sup a b |a b. a ∈ A ∧ b ∈ B})" (is "_ = ⨅⇩_{f}⇩_{i}⇩_{n}?M") using B insert by (simp add: Inf_fin.union [OF finB _ finAB ne]) also have "?M = {sup a b |a b. a ∈ insert x A ∧ b ∈ B}" by blast finally show ?case . qed lemma inf_Sup1_distrib: assumes "finite A" and "A ≠ {}" shows "inf x (⨆⇩_{f}⇩_{i}⇩_{n}A) = ⨆⇩_{f}⇩_{i}⇩_{n}{inf x a|a. a ∈ A}" using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1]) (rule arg_cong [where f="Sup_fin"], blast) lemma inf_Sup2_distrib: assumes A: "finite A" "A ≠ {}" and B: "finite B" "B ≠ {}" shows "inf (⨆⇩_{f}⇩_{i}⇩_{n}A) (⨆⇩_{f}⇩_{i}⇩_{n}B) = ⨆⇩_{f}⇩_{i}⇩_{n}{inf a b|a b. a ∈ A ∧ b ∈ B}" using A proof (induct rule: finite_ne_induct) case singleton thus ?case by(simp add: inf_Sup1_distrib [OF B]) next case (insert x A) have finB: "finite {inf x b |b. b ∈ B}" by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto) have finAB: "finite {inf a b |a b. a ∈ A ∧ b ∈ B}" proof - have "{inf a b |a b. a ∈ A ∧ b ∈ B} = (UN a:A. UN b:B. {inf a b})" by blast thus ?thesis by(simp add: insert(1) B(1)) qed have ne: "{inf a b |a b. a ∈ A ∧ b ∈ B} ≠ {}" using insert B by blast have "inf (⨆⇩_{f}⇩_{i}⇩_{n}(insert x A)) (⨆⇩_{f}⇩_{i}⇩_{n}B) = inf (sup x (⨆⇩_{f}⇩_{i}⇩_{n}A)) (⨆⇩_{f}⇩_{i}⇩_{n}B)" using insert by simp also have "… = sup (inf x (⨆⇩_{f}⇩_{i}⇩_{n}B)) (inf (⨆⇩_{f}⇩_{i}⇩_{n}A) (⨆⇩_{f}⇩_{i}⇩_{n}B))" by(rule inf_sup_distrib2) also have "… = sup (⨆⇩_{f}⇩_{i}⇩_{n}{inf x b|b. b ∈ B}) (⨆⇩_{f}⇩_{i}⇩_{n}{inf a b|a b. a ∈ A ∧ b ∈ B})" using insert by(simp add:inf_Sup1_distrib[OF B]) also have "… = ⨆⇩_{f}⇩_{i}⇩_{n}({inf x b |b. b ∈ B} ∪ {inf a b |a b. a ∈ A ∧ b ∈ B})" (is "_ = ⨆⇩_{f}⇩_{i}⇩_{n}?M") using B insert by (simp add: Sup_fin.union [OF finB _ finAB ne]) also have "?M = {inf a b |a b. a ∈ insert x A ∧ b ∈ B}" by blast finally show ?case . qed end context complete_lattice begin lemma Inf_fin_Inf: assumes "finite A" and "A ≠ {}" shows "⨅⇩_{f}⇩_{i}⇩_{n}A = ⨅A" proof - from assms obtain b B where "A = insert b B" and "finite B" by auto then show ?thesis by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b]) qed lemma Sup_fin_Sup: assumes "finite A" and "A ≠ {}" shows "⨆⇩_{f}⇩_{i}⇩_{n}A = ⨆A" proof - from assms obtain b B where "A = insert b B" and "finite B" by auto then show ?thesis by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b]) qed end subsection ‹Minimum and Maximum over non-empty sets› context linorder begin sublocale Min: semilattice_order_set min less_eq less + Max: semilattice_order_set max greater_eq greater defines Min = Min.F and Max = Max.F .. end text ‹An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin}› lemma Inf_fin_Min: "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set ⇒ 'a)" by (simp add: Inf_fin_def Min_def inf_min) lemma Sup_fin_Max: "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set ⇒ 'a)" by (simp add: Sup_fin_def Max_def sup_max) context linorder begin lemma dual_min: "ord.min greater_eq = max" by (auto simp add: ord.min_def max_def fun_eq_iff) lemma dual_max: "ord.max greater_eq = min" by (auto simp add: ord.max_def min_def fun_eq_iff) lemma dual_Min: "linorder.Min greater_eq = Max" proof - interpret dual: linorder greater_eq greater by (fact dual_linorder) show ?thesis by (simp add: dual.Min_def dual_min Max_def) qed lemma dual_Max: "linorder.Max greater_eq = Min" proof - interpret dual: linorder greater_eq greater by (fact dual_linorder) show ?thesis by (simp add: dual.Max_def dual_max Min_def) qed lemmas Min_singleton = Min.singleton lemmas Max_singleton = Max.singleton lemmas Min_insert = Min.insert lemmas Max_insert = Max.insert lemmas Min_Un = Min.union lemmas Max_Un = Max.union lemmas hom_Min_commute = Min.hom_commute lemmas hom_Max_commute = Max.hom_commute lemma Min_in [simp]: assumes "finite A" and "A ≠ {}" shows "Min A ∈ A" using assms by (auto simp add: min_def Min.closed) lemma Max_in [simp]: assumes "finite A" and "A ≠ {}" shows "Max A ∈ A" using assms by (auto simp add: max_def Max.closed) lemma Min_insert2: assumes "finite A" and min: "⋀b. b ∈ A ⟹ a ≤ b" shows "Min (insert a A) = a" proof (cases "A = {}") case True then show ?thesis by simp next case False with ‹finite A› have "Min (insert a A) = min a (Min A)" by simp moreover from ‹finite A› ‹A ≠ {}› min have "a ≤ Min A" by simp ultimately show ?thesis by (simp add: min.absorb1) qed lemma Max_insert2: assumes "finite A" and max: "⋀b. b ∈ A ⟹ b ≤ a" shows "Max (insert a A) = a" proof (cases "A = {}") case True then show ?thesis by simp next case False with ‹finite A› have "Max (insert a A) = max a (Max A)" by simp moreover from ‹finite A› ‹A ≠ {}› max have "Max A ≤ a" by simp ultimately show ?thesis by (simp add: max.absorb1) qed lemma Min_le [simp]: assumes "finite A" and "x ∈ A" shows "Min A ≤ x" using assms by (fact Min.coboundedI) lemma Max_ge [simp]: assumes "finite A" and "x ∈ A" shows "x ≤ Max A" using assms by (fact Max.coboundedI) lemma Min_eqI: assumes "finite A" assumes "⋀y. y ∈ A ⟹ y ≥ x" and "x ∈ A" shows "Min A = x" proof (rule antisym) from ‹x ∈ A› have "A ≠ {}" by auto with assms show "Min A ≥ x" by simp next from assms show "x ≥ Min A" by simp qed lemma Max_eqI: assumes "finite A" assumes "⋀y. y ∈ A ⟹ y ≤ x" and "x ∈ A" shows "Max A = x" proof (rule antisym) from ‹x ∈ A› have "A ≠ {}" by auto with assms show "Max A ≤ x" by simp next from assms show "x ≤ Max A" by simp qed lemma eq_Min_iff: "⟦ finite A; A ≠ {} ⟧ ⟹ m = Min A ⟷ m ∈ A ∧ (∀a ∈ A. m ≤ a)" by (meson Min_in Min_le antisym) lemma Min_eq_iff: "⟦ finite A; A ≠ {} ⟧ ⟹ Min A = m ⟷ m ∈ A ∧ (∀a ∈ A. m ≤ a)" by (meson Min_in Min_le antisym) lemma eq_Max_iff: "⟦ finite A; A ≠ {} ⟧ ⟹ m = Max A ⟷ m ∈ A ∧ (∀a ∈ A. a ≤ m)" by (meson Max_in Max_ge antisym) lemma Max_eq_iff: "⟦ finite A; A ≠ {} ⟧ ⟹ Max A = m ⟷ m ∈ A ∧ (∀a ∈ A. a ≤ m)" by (meson Max_in Max_ge antisym) context fixes A :: "'a set" assumes fin_nonempty: "finite A" "A ≠ {}" begin lemma Min_ge_iff [simp]: "x ≤ Min A ⟷ (∀a∈A. x ≤ a)" using fin_nonempty by (fact Min.bounded_iff) lemma Max_le_iff [simp]: "Max A ≤ x ⟷ (∀a∈A. a ≤ x)" using fin_nonempty by (fact Max.bounded_iff) lemma Min_gr_iff [simp]: "x < Min A ⟷ (∀a∈A. x < a)" using fin_nonempty by (induct rule: finite_ne_induct) simp_all lemma Max_less_iff [simp]: "Max A < x ⟷ (∀a∈A. a < x)" using fin_nonempty by (induct rule: finite_ne_induct) simp_all lemma Min_le_iff: "Min A ≤ x ⟷ (∃a∈A. a ≤ x)" using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj) lemma Max_ge_iff: "x ≤ Max A ⟷ (∃a∈A. x ≤ a)" using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj) lemma Min_less_iff: "Min A < x ⟷ (∃a∈A. a < x)" using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj) lemma Max_gr_iff: "x < Max A ⟷ (∃a∈A. x < a)" using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj) end lemma Max_eq_if: assumes "finite A" "finite B" "∀a∈A. ∃b∈B. a ≤ b" "∀b∈B. ∃a∈A. b ≤ a" shows "Max A = Max B" proof cases assume "A = {}" thus ?thesis using assms by simp next assume "A ≠ {}" thus ?thesis using assms by(blast intro: antisym Max_in Max_ge_iff[THEN iffD2]) qed lemma Min_antimono: assumes "M ⊆ N" and "M ≠ {}" and "finite N" shows "Min N ≤ Min M" using assms by (fact Min.antimono) lemma Max_mono: assumes "M ⊆ N" and "M ≠ {}" and "finite N" shows "Max M ≤ Max N" using assms by (fact Max.antimono) end context linorder (* FIXME *) begin lemma mono_Min_commute: assumes "mono f" assumes "finite A" and "A ≠ {}" shows "f (Min A) = Min (f ` A)" proof (rule linorder_class.Min_eqI [symmetric]) from ‹finite A› show "finite (f ` A)" by simp from assms show "f (Min A) ∈ f ` A" by simp fix x assume "x ∈ f ` A" then obtain y where "y ∈ A" and "x = f y" .. with assms have "Min A ≤ y" by auto with ‹mono f› have "f (Min A) ≤ f y" by (rule monoE) with ‹x = f y› show "f (Min A) ≤ x" by simp qed lemma mono_Max_commute: assumes "mono f" assumes "finite A" and "A ≠ {}" shows "f (Max A) = Max (f ` A)" proof (rule linorder_class.Max_eqI [symmetric]) from ‹finite A› show "finite (f ` A)" by simp from assms show "f (Max A) ∈ f ` A" by simp fix x assume "x ∈ f ` A" then obtain y where "y ∈ A" and "x = f y" .. with assms have "y ≤ Max A" by auto with ‹mono f› have "f y ≤ f (Max A)" by (rule monoE) with ‹x = f y› show "x ≤ f (Max A)" by simp qed lemma finite_linorder_max_induct [consumes 1, case_names empty insert]: assumes fin: "finite A" and empty: "P {}" and insert: "⋀b A. finite A ⟹ ∀a∈A. a < b ⟹ P A ⟹ P (insert b A)" shows "P A" using fin empty insert proof (induct rule: finite_psubset_induct) case (psubset A) have IH: "⋀B. ⟦B < A; P {}; (⋀A b. ⟦finite A; ∀a∈A. a<b; P A⟧ ⟹ P (insert b A))⟧ ⟹ P B" by fact have fin: "finite A" by fact have empty: "P {}" by fact have step: "⋀b A. ⟦finite A; ∀a∈A. a < b; P A⟧ ⟹ P (insert b A)" by fact show "P A" proof (cases "A = {}") assume "A = {}" then show "P A" using ‹P {}› by simp next let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B" have "finite ?B" using ‹finite A› by simp assume "A ≠ {}" with ‹finite A› have "Max A : A" by auto then have A: "?A = A" using insert_Diff_single insert_absorb by auto then have "P ?B" using ‹P {}› step IH [of ?B] by blast moreover have "∀a∈?B. a < Max A" using Max_ge [OF ‹finite A›] by fastforce ultimately show "P A" using A insert_Diff_single step [OF ‹finite ?B›] by fastforce qed qed lemma finite_linorder_min_induct [consumes 1, case_names empty insert]: "⟦finite A; P {}; ⋀b A. ⟦finite A; ∀a∈A. b < a; P A⟧ ⟹ P (insert b A)⟧ ⟹ P A" by (rule linorder.finite_linorder_max_induct [OF dual_linorder]) lemma Least_Min: assumes "finite {a. P a}" and "∃a. P a" shows "(LEAST a. P a) = Min {a. P a}" proof - { fix A :: "'a set" assume A: "finite A" "A ≠ {}" have "(LEAST a. a ∈ A) = Min A" using A proof (induct A rule: finite_ne_induct) case singleton show ?case by (rule Least_equality) simp_all next case (insert a A) have "(LEAST b. b = a ∨ b ∈ A) = min a (LEAST a. a ∈ A)" by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le) with insert show ?case by simp qed } from this [of "{a. P a}"] assms show ?thesis by simp qed lemma infinite_growing: assumes "X ≠ {}" assumes *: "⋀x. x ∈ X ⟹ ∃y∈X. y > x" shows "¬ finite X" proof assume "finite X" with ‹X ≠ {}› have "Max X ∈ X" "∀x∈X. x ≤ Max X" by auto with *[of "Max X"] show False by auto qed end context linordered_ab_semigroup_add begin lemma add_Min_commute: fixes k assumes "finite N" and "N ≠ {}" shows "k + Min N = Min {k + m | m. m ∈ N}" proof - have "⋀x y. k + min x y = min (k + x) (k + y)" by (simp add: min_def not_le) (blast intro: antisym less_imp_le add_left_mono) with assms show ?thesis using hom_Min_commute [of "plus k" N] by simp (blast intro: arg_cong [where f = Min]) qed lemma add_Max_commute: fixes k assumes "finite N" and "N ≠ {}" shows "k + Max N = Max {k + m | m. m ∈ N}" proof - have "⋀x y. k + max x y = max (k + x) (k + y)" by (simp add: max_def not_le) (blast intro: antisym less_imp_le add_left_mono) with assms show ?thesis using hom_Max_commute [of "plus k" N] by simp (blast intro: arg_cong [where f = Max]) qed end context linordered_ab_group_add begin lemma minus_Max_eq_Min [simp]: "finite S ⟹ S ≠ {} ⟹ - Max S = Min (uminus ` S)" by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min) lemma minus_Min_eq_Max [simp]: "finite S ⟹ S ≠ {} ⟹ - Min S = Max (uminus ` S)" by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max) end context complete_linorder begin lemma Min_Inf: assumes "finite A" and "A ≠ {}" shows "Min A = Inf A" proof - from assms obtain b B where "A = insert b B" and "finite B" by auto then show ?thesis by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b]) qed lemma Max_Sup: assumes "finite A" and "A ≠ {}" shows "Max A = Sup A" proof - from assms obtain b B where "A = insert b B" and "finite B" by auto then show ?thesis by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b]) qed end subsection ‹Arg Min› definition is_arg_min :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool" where "is_arg_min f P x = (P x ∧ ¬(∃y. P y ∧ f y < f x))" definition arg_min :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ bool) ⇒ 'a" where "arg_min f P = (SOME x. is_arg_min f P x)" abbreviation arg_min_on :: "('a ⇒ 'b::ord) ⇒ 'a set ⇒ 'a" where "arg_min_on f S ≡ arg_min f (λx. x ∈ S)" syntax "_arg_min" :: "('a ⇒ 'b) ⇒ pttrn ⇒ bool ⇒ 'a" ("(3ARG'_MIN _ _./ _)" [0, 0, 10] 10) translations "ARG_MIN f x. P" ⇌ "CONST arg_min f (λx. P)" lemma is_arg_min_linorder: fixes f :: "'a ⇒ 'b :: linorder" shows "is_arg_min f P x = (P x ∧ (∀y. P y ⟶ f x ≤ f y))" by(auto simp add: is_arg_min_def) lemma arg_minI: "⟦ P x; ⋀y. P y ⟹ ¬ f y < f x; ⋀x. ⟦ P x; ∀y. P y ⟶ ¬ f y < f x ⟧ ⟹ Q x ⟧ ⟹ Q (arg_min f P)" apply (simp add: arg_min_def is_arg_min_def) apply (rule someI2_ex) apply blast apply blast done lemma arg_min_equality: "⟦ P k; ⋀x. P x ⟹ f k ≤ f x ⟧ ⟹ f (arg_min f P) = f k" for f :: "_ ⇒ 'a::order" apply (rule arg_minI) apply assumption apply (simp add: less_le_not_le) by (metis le_less) lemma wf_linord_ex_has_least: "⟦ wf r; ∀x y. (x, y) ∈ r⇧^{+}⟷ (y, x) ∉ r⇧^{*}; P k ⟧ ⟹ ∃x. P x ∧ (∀y. P y ⟶ (m x, m y) ∈ r⇧^{*})" apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]]) apply (drule_tac x = "m ` Collect P" in spec) by force lemma ex_has_least_nat: "P k ⟹ ∃x. P x ∧ (∀y. P y ⟶ m x ≤ m y)" for m :: "'a ⇒ nat" apply (simp only: pred_nat_trancl_eq_le [symmetric]) apply (rule wf_pred_nat [THEN wf_linord_ex_has_least]) apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le) by assumption lemma arg_min_nat_lemma: "P k ⟹ P(arg_min m P) ∧ (∀y. P y ⟶ m (arg_min m P) ≤ m y)" for m :: "'a ⇒ nat" apply (simp add: arg_min_def is_arg_min_linorder) apply (rule someI_ex) apply (erule ex_has_least_nat) done lemmas arg_min_natI = arg_min_nat_lemma [THEN conjunct1] lemma is_arg_min_arg_min_nat: fixes m :: "'a ⇒ nat" shows "P x ⟹ is_arg_min m P (arg_min m P)" by (metis arg_min_nat_lemma is_arg_min_linorder) lemma arg_min_nat_le: "P x ⟹ m (arg_min m P) ≤ m x" for m :: "'a ⇒ nat" by (rule arg_min_nat_lemma [THEN conjunct2, THEN spec, THEN mp]) lemma ex_min_if_finite: "⟦ finite S; S ≠ {} ⟧ ⟹ ∃m∈S. ¬(∃x∈S. x < (m::'a::order))" by(induction rule: finite.induct) (auto intro: order.strict_trans) lemma ex_is_arg_min_if_finite: fixes f :: "'a ⇒ 'b :: order" shows "⟦ finite S; S ≠ {} ⟧ ⟹ ∃x. is_arg_min f (λx. x : S) x" unfolding is_arg_min_def using ex_min_if_finite[of "f ` S"] by auto lemma arg_min_SOME_Min: "finite S ⟹ arg_min_on f S = (SOME y. y ∈ S ∧ f y = Min(f ` S))" unfolding arg_min_def is_arg_min_linorder apply(rule arg_cong[where f = Eps]) apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric]) done lemma arg_min_if_finite: fixes f :: "'a ⇒ 'b :: order" assumes "finite S" "S ≠ {}" shows "arg_min_on f S ∈ S" and "¬(∃x∈S. f x < f (arg_min_on f S))" using ex_is_arg_min_if_finite[OF assms, of f] unfolding arg_min_def is_arg_min_def by(auto dest!: someI_ex) lemma arg_min_least: fixes f :: "'a ⇒ 'b :: linorder" shows "⟦ finite S; S ≠ {}; y ∈ S ⟧ ⟹ f(arg_min_on f S) ≤ f y" by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f) lemma arg_min_inj_eq: fixes f :: "'a ⇒ 'b :: order" shows "⟦ inj_on f {x. P x}; P a; ∀y. P y ⟶ f a ≤ f y ⟧ ⟹ arg_min f P = a" apply(simp add: arg_min_def is_arg_min_def) apply(rule someI2[of _ a]) apply (simp add: less_le_not_le) by (metis inj_on_eq_iff less_le mem_Collect_eq) subsection ‹Arg Max› definition is_arg_max :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool" where "is_arg_max f P x = (P x ∧ ¬(∃y. P y ∧ f y > f x))" definition arg_max :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ bool) ⇒ 'a" where "arg_max f P = (SOME x. is_arg_max f P x)" abbreviation arg_max_on :: "('a ⇒ 'b::ord) ⇒ 'a set ⇒ 'a" where "arg_max_on f S ≡ arg_max f (λx. x ∈ S)" syntax "_arg_max" :: "('a ⇒ 'b) ⇒ pttrn ⇒ bool ⇒ 'a" ("(3ARG'_MAX _ _./ _)" [0, 0, 10] 10) translations "ARG_MAX f x. P" ⇌ "CONST arg_max f (λx. P)" lemma is_arg_max_linorder: fixes f :: "'a ⇒ 'b :: linorder" shows "is_arg_max f P x = (P x ∧ (∀y. P y ⟶ f x ≥ f y))" by(auto simp add: is_arg_max_def) lemma arg_maxI: "P x ⟹ (⋀y. P y ⟹ ¬ f y > f x) ⟹ (⋀x. P x ⟹ ∀y. P y ⟶ ¬ f y > f x ⟹ Q x) ⟹ Q (arg_max f P)" apply (simp add: arg_max_def is_arg_max_def) apply (rule someI2_ex) apply blast apply blast done lemma arg_max_equality: "⟦ P k; ⋀x. P x ⟹ f x ≤ f k ⟧ ⟹ f (arg_max f P) = f k" for f :: "_ ⇒ 'a::order" apply (rule arg_maxI [where f = f]) apply assumption apply (simp add: less_le_not_le) by (metis le_less) lemma ex_has_greatest_nat_lemma: "P k ⟹ ∀x. P x ⟶ (∃y. P y ∧ ¬ f y ≤ f x) ⟹ ∃y. P y ∧ ¬ f y < f k + n" for f :: "'a ⇒ nat" by (induct n) (force simp: le_Suc_eq)+ lemma ex_has_greatest_nat: "P k ⟹ ∀y. P y ⟶ f y < b ⟹ ∃x. P x ∧ (∀y. P y ⟶ f y ≤ f x)" for f :: "'a ⇒ nat" apply (rule ccontr) apply (cut_tac P = P and n = "b - f k" in ex_has_greatest_nat_lemma) apply (subgoal_tac [3] "f k ≤ b") apply auto done lemma arg_max_nat_lemma: "⟦ P k; ∀y. P y ⟶ f y < b ⟧ ⟹ P (arg_max f P) ∧ (∀y. P y ⟶ f y ≤ f (arg_max f P))" for f :: "'a ⇒ nat" apply (simp add: arg_max_def is_arg_max_linorder) apply (rule someI_ex) apply (erule (1) ex_has_greatest_nat) done lemmas arg_max_natI = arg_max_nat_lemma [THEN conjunct1] lemma arg_max_nat_le: "P x ⟹ ∀y. P y ⟶ f y < b ⟹ f x ≤ f (arg_max f P)" for f :: "'a ⇒ nat" by (blast dest: arg_max_nat_lemma [THEN conjunct2, THEN spec, of P]) end