Quellcode-Bibliothek Lattices_Big.thy

(*  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 Groups_Big 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

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 subset_imp:
  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

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 subset_imp:
  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🪙nA ≤ ⊔🪙f🪙i🪙nA"
proof -
  from ‹A ≠ {}› obtain a where "a ∈ A" by blast
  with ‹finite A› have "⊓🪙f🪙i🪙nA ≤ a" by (rule Inf_fin.coboundedI)
  moreover from ‹finite A› ‹a ∈ A› have "a ≤ ⊔🪙f🪙i🪙nA" by (rule Sup_fin.coboundedI)
  ultimately show ?thesis by (rule order_trans)
qed

lemma sup_Inf_absorb [simp]:
  "finite A ==> a ∈ A ==> ⊓🪙f🪙i🪙nA ⊔ a = a"
  by (rule sup_absorb2) (rule Inf_fin.coboundedI)

lemma inf_Sup_absorb [simp]:
  "finite A ==> a ∈ A ==> a ⊓ ⊔🪙f🪙i🪙nA = 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🪙nA) = ⊓🪙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🪙nA) (⊓🪙f🪙i🪙nB) = ⊓🪙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} = (∪a∈A. ∪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🪙nB) = sup (inf x (⊓🪙f🪙i🪙nA)) (⊓🪙f🪙i🪙nB)"
    using insert by simp
  also have "… = inf (sup x (⊓🪙f🪙i🪙nB)) (sup (⊓🪙f🪙i🪙nA) (⊓🪙f🪙i🪙nB))" 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🪙nA) = ⊔🪙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🪙nA) (⊔🪙f🪙i🪙nB) = ⊔🪙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} = (∪a∈A. ∪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🪙nB) = inf (sup x (⊔🪙f🪙i🪙nA)) (⊔🪙f🪙i🪙nB)"
    using insert by simp
  also have "… = sup (inf x (⊔🪙f🪙i🪙nB)) (inf (⊔🪙f🪙i🪙nA) (⊔🪙f🪙i🪙nB))" 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🪙nA = ⊓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🪙nA = ⊔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

syntax
  "_MIN1"     :: "pttrns ==> 'b ==> 'b"           (‹(‹indent=3 notation=‹binder MIN›\›MIN _./ _)› [0, 10] 10)
  "_MIN"      :: "pttrn ==> 'a set ==> 'b ==> 'b"  (‹(‹indent=3 notation=‹binder MIN›\›MIN _∈_./ _)› [0, 0, 10] 10)
  "_MAX1"     :: "pttrns ==> 'b ==> 'b"           (‹(‹indent=3 notation=‹binder MAX›\›MAX _./ _)› [0, 10] 10)
  "_MAX"      :: "pttrn ==> 'a set ==> 'b ==> 'b"  (‹(‹indent=3 notation=‹binder MAX›\›MAX _∈_./ _)› [0, 0, 10] 10)

syntax_consts
  "_MIN1" "_MIN" ⇌ Min and
  "_MAX1" "_MAX" ⇌ Max

translations
  "MIN x y. f"   ⇌ "MIN x. MIN y. f"
  "MIN x. f"     ⇌ "CONST Min (CONST range (λx. f))"
  "MIN x∈A. f"   ⇌ "CONST Min ((λx. f) ` A)"
  "MAX x y. f"   ⇌ "MAX x. MAX y. f"
  "MAX x. f"     ⇌ "CONST Max (CONST range (λx. f))"
  "MAX x∈A. f"   ⇌ "CONST Max ((λx. f) ` A)"


text ‹An aside: 🍋‹Min›/🍋‹Max› on linear orders as special case of 🍋‹Inf_fin›/??‹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 Max_const[simp]: "[ finite A; A ≠ {} ] ==> Max ((λ_. c) ` A) = c"
using Max_in image_is_empty by blast

lemma Min_const[simp]: "[ finite A; A ≠ {} ] ==> Min ((λ_. c) ` A) = c"
using Min_in image_is_empty by blast

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 order.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 order.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 order.antisym)

lemma Min_eq_iff:
  "[ finite A; A ≠ {} ] ==> Min A = m ⟷ m ∈ A ∧ (∀a ∈ A. m ≤ a)"
by (meson Min_in Min_le order.antisym)

lemma eq_Max_iff:
  "[ finite A; A ≠ {} ] ==> m = Max A ⟷ m ∈ A ∧ (∀a ∈ A. a ≤ m)"
by (meson Max_in Max_ge order.antisym)

lemma Max_eq_iff:
  "[ finite A; A ≠ {} ] ==> Max A = m ⟷ m ∈ A ∧ (∀a ∈ A. a ≤ m)"
by (meson Max_in Max_ge order.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

text ‹Handy results about @{term Max} and @{term Min} by Chelsea Edmonds›
lemma obtains_Max:
  assumes "finite A" and "A ≠ {}"
  obtains x where "x ∈ A" and "Max A = x"
  using assms Max_in by blast

lemma obtains_MAX:
  assumes "finite A" and "A ≠ {}"
  obtains x where "x ∈ A" and "Max (f ` A) = f x"
  using obtains_Max
  by (metis (mono_tags, opaque_lifting) assms(1) assms(2) empty_is_image finite_imageI image_iff) 

lemma obtains_Min:
  assumes "finite A" and "A ≠ {}"
  obtains x where "x ∈ A" and "Min A = x"
  using assms Min_in by blast

lemma obtains_MIN:
  assumes "finite A" and "A ≠ {}"
  obtains x where "x ∈ A" and "Min (f ` A) = f x"
  using obtains_Min assms empty_is_image finite_imageI image_iff
  by (metis (mono_tags, opaque_lifting)) 

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: order.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.subset_imp)

lemma Max_mono:
  assumes "M ⊆ N" and "M ≠ {}" and "finite N"
  shows "Max M ≤ Max N"
  using assms by (fact Max.subset_imp)

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] ==> 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 finite_ranking_induct[consumes 1, case_names empty insert]:
  fixes f :: "'b ==> 'a"
  assumes "finite S"
  assumes "P {}" 
  assumes "∧x S. finite S ==> (∧y. y ∈ S ==> f y ≤ f x) ==> P S ==> P (insert x S)"
  shows "P S"
  using ‹finite S›
proof (induction rule: finite_psubset_induct)
  case (psubset A)
  {
    assume "A ≠ {}"
    hence "f ` A ≠ {}" and "finite (f ` A)"
      using psubset finite_image_iff by simp+ 
    then obtain a where "f a = Max (f ` A)" and "a ∈ A"
      by (metis Max_in[of "f ` A"] imageE)
    then have "P (A - {a})"
      using psubset(2) [of ‹A - {a}›] by auto
    moreover 
    have "∧y. y ∈ A ==> f y ≤ f a"
      using ‹f a = Max (f ` A)› ‹finite (f ` A)› by simp
    ultimately
    have ?case
      by (metis ‹a ∈ A› DiffD1 insert_Diff assms(3) finite_Diff psubset.hyps)
  }
  thus ?case
    using assms(2) by blast
qed

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 Greatest_Max:
  assumes "finite {a. P a}" and "∃a. P a"
  shows "(GREATEST a. P a) = Max {a. P a}"
proof -
  { fix A :: "'a set"
    assume A: "finite A" "A ≠ {}"
    have "(GREATEST a. a ∈ A) = Max A"
    using A proof (induct A rule: finite_ne_induct)
      case singleton show ?case by (rule Greatest_equality) simp_all
    next
      case (insert a A)
      have "(GREATEST b. b = a ∨ b ∈ A) = max a (GREATEST a. a ∈ A)"
        by (auto intro!: Greatest_equality simp add: max_def not_le insert.hyps)
      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

lemma sum_le_card_Max: "finite A ==> sum f A ≤ card A * Max (f ` A)"
using sum_bounded_above[of A f "Max (f ` A)"] by simp

lemma card_Min_le_sum: "finite A ==> card A * Min (f ` A) ≤ sum f A"
using sum_bounded_below[of A "Min (f ` A)" f] by simp

context linordered_ab_semigroup_add
begin

lemma Min_add_commute:
  fixes k
  assumes "finite S" and "S ≠ {}"
  shows "Min ((λx. f x + k) ` S) = Min(f ` S) + k"
proof -
  have m: "∧x y. min x y + k = min (x+k) (y+k)"
    by (simp add: min_def order.antisym add_right_mono)
  have "(λx. f x + k) ` S = (λy. y + k) ` (f ` S)" by auto
  also have "Min … = Min (f ` S) + k"
    using assms hom_Min_commute [of "λy. y+k" "f ` S", OF m, symmetric] by simp
  finally show ?thesis by simp
qed

lemma Max_add_commute:
  fixes k
  assumes "finite S" and "S ≠ {}"
  shows "Max ((λx. f x + k) ` S) = Max(f ` S) + k"
proof -
  have m: "∧x y. max x y + k = max (x+k) (y+k)"
    by (simp add: max_def order.antisym add_right_mono)
  have "(λx. f x + k) ` S = (λy. y + k) ` (f ` S)" by auto
  also have "Max … = Max (f ` S) + k"
    using assms hom_Max_commute [of "λy. y+k" "f ` S", OF m, symmetric] by simp
  finally show ?thesis by simp
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

lemma disjnt_ge_max: 🍋‹contributor ‹Lars Hupel›\›
  ‹disjnt X Y› if ‹finite Y› ‹∧x. x ∈ X ==> x > Max Y›
  using that by (auto simp add: disjnt_def) (use Max_less_iff in blast)


subsection ‹An aside: code generation for ‹LEAST› and ‹GREATEST›\›

context
begin

qualified definition Least :: ‹'a::linorder set ==> 'a› 🍋 ‹only for code generation›
  where Least_eq [code_abbrev, simp]: ‹Least S = (LEAST x. x ∈ S)›

qualified lemma Least_filter_eq [code_abbrev]:
  ‹Least (Set.filter P S) = (LEAST x. x ∈ S ∧ P x)›
  by simp

qualified definition Least_abort :: ‹'a set ==> 'a::linorder›
  where ‹Least_abort = Least›

qualified lemma Least_code [code abort: Lattices_Big.Least_abort, code]:
  ‹Least A = (if finite A ⟶ Set.is_empty A then Least_abort A else Min A)›
  using Least_Min [of ‹λx. x ∈ A›] by (auto simp add: Least_abort_def)

qualified definition Greatest :: ‹'a::linorder set ==> 'a› 🍋 ‹only for code generation›
  where Greatest_eq [code_abbrev, simp]: ‹Greatest S = (GREATEST x. x ∈ S)›

qualified lemma Greatest_filter_eq [code_abbrev]:
  ‹Greatest (Set.filter P S) = (GREATEST x. x ∈ S ∧ P x)›
  by simp

qualified definition Greatest_abort :: ‹'a set ==> 'a::linorder›
  where ‹Greatest_abort = Greatest›

qualified lemma Greatest_code [code abort: Lattices_Big.Greatest_abort, code]:
  ‹Greatest A = (if finite A ⟶ Set.is_empty A then Greatest_abort A else Max A)›
  using Greatest_Max [of ‹λx. x ∈ A›] by (auto simp add: Greatest_abort_def)

end


subsection ‹Arg Min›

context ord
begin

definition is_arg_min :: "('b ==> 'a) ==> ('b ==> bool) ==> 'b ==> bool" where
"is_arg_min f P x = (P x ∧ ¬(∃y. P y ∧ f y < f x))"

definition arg_min :: "('b ==> 'a) ==> ('b ==> bool) ==> 'b" where
"arg_min f P = (SOME x. is_arg_min f P x)"

definition arg_min_on :: "('b ==> 'a) ==> 'b set ==> 'b" where
"arg_min_on f S = arg_min f (λx. x ∈ S)"

end

syntax
  "_arg_min" :: "('b ==> 'a) ==> pttrn ==> bool ==> 'b"
    (‹(‹indent=3 notation=‹binder ARG_MIN›\›ARG'_MIN _ _./ _)› [1000, 0, 10] 10)
syntax_consts
  "_arg_min" ⇌ arg_min
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 is_arg_min_antimono: fixes f :: "'a ==> ('b::order)"
shows "[ is_arg_min f P x; f y ≤ f x; P y ] ==> is_arg_min f P y"
by (simp add: order.order_iff_strict 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)"
  unfolding arg_min_def is_arg_min_def
  by (blast intro!: someI2_ex)

lemma arg_min_equality:
  "[ P k; ∧x. P x ==> f k ≤ f x ] ==> f (arg_min f P) = f k"
  for f :: "_ ==> 'a::order"
  by (rule arg_minI; force simp: not_less less_le_not_le)

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🪙*)"
  by (force dest!:  wf_trancl [THEN wf_eq_minimal [THEN iffD1, THEN spec], where x = "m ` Collect P"])

lemma ex_has_least_nat: "P k ==> ∃x. P x ∧ (∀y. P y ⟶ m x ≤ m y)"
  for m :: "'a ==> nat"
  unfolding 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"
  unfolding 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_on_def 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_on_def 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›

context ord
begin

definition is_arg_max :: "('b ==> 'a) ==> ('b ==> bool) ==> 'b ==> bool" where
"is_arg_max f P x = (P x ∧ ¬(∃y. P y ∧ f y > f x))"

definition arg_max :: "('b ==> 'a) ==> ('b ==> bool) ==> 'b" where
"arg_max f P = (SOME x. is_arg_max f P x)"

definition arg_max_on :: "('b ==> 'a) ==> 'b set ==> 'b" where
"arg_max_on f S = arg_max f (λx. x ∈ S)"

end

syntax
  "_arg_max" :: "('b ==> 'a) ==> pttrn ==> bool ==> 'a"
    (‹(‹indent=3 notation=‹binder ARG_MAX›\›ARG'_MAX _ _./ _)› [1000, 0, 10] 10)
syntax_consts
  "_arg_max" ⇌ arg_max
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)"
  unfolding arg_max_def is_arg_max_def
  by (blast intro!: someI2_ex elim: )

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:
  assumes "P k"
    and "∀y. P y ⟶ (f:: 'a ==> nat) y < b"
shows "∃x. P x ∧ (∀y. P y ⟶ f y ≤ f x)"
proof (rule ccontr)
  assume "∄x. P x ∧ (∀y. P y ⟶ f y ≤ f x)"
  then have "∀x. P x ⟶ (∃y. P y ∧ ¬ f y ≤ f x)"
    by auto
  then have "∃y. P y ∧ ¬ f y < f k + (b - f k)"
    using assms ex_has_greatest_nat_lemma[of P k f "b - f k"]
    by blast
  then show "False"
    using assms by auto
qed

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"
  unfolding arg_max_def is_arg_max_linorder
  by (rule someI_ex) (metis ex_has_greatest_nat)

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"
  using arg_max_nat_lemma by metis

end