# Theory Lattices_Big

(*  Title:      HOL/Lattices_Big.thy
Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
*)

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"

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)"
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  (aA. 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"

lemma empty [simp]:
"F {} = 1"

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  (aA. 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 ("fin _" [900] 900) = Inf_fin.F ..

end

context semilattice_sup
begin

sublocale Sup_fin: semilattice_order_set sup greater_eq greater
defines
Sup_fin ("fin _" [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 "finA  finA"
proof -
from A  {} obtain a where "a  A" by blast
with finite A have "finA  a" by (rule Inf_fin.coboundedI)
moreover from finite A a  A have "a  finA" by (rule Sup_fin.coboundedI)
ultimately show ?thesis by (rule order_trans)
qed

lemma sup_Inf_absorb [simp]:
"finite A  a  A  finA  a = a"
by (rule sup_absorb2) (rule Inf_fin.coboundedI)

lemma inf_Sup_absorb [simp]:
"finite A  a  A  a  finA = 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 (finA) = fin{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 (finA) (finB) = fin{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} = (aA. bB. {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 (fin(insert x A)) (finB) = sup (inf x (finA)) (finB)"
using insert by simp
also have " = inf (sup x (finB)) (sup (finA) (finB))" by(rule sup_inf_distrib2)
also have " = inf (fin{sup x b|b. b  B}) (fin{sup a b|a b. a  A  b  B})"
also have " = fin({sup x b |b. b  B}  {sup a b |a b. a  A  b  B})"
(is "_ = fin?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 (finA) = fin{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 (finA) (finB) = fin{inf a b|a b. a  A  b  B}"
using A proof (induct rule: finite_ne_induct)
case singleton thus ?case
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} = (aA. bB. {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 (fin(insert x A)) (finB) = inf (sup x (finA)) (finB)"
using insert by simp
also have " = sup (inf x (finB)) (inf (finA) (finB))" by(rule inf_sup_distrib2)
also have " = sup (fin{inf x b|b. b  B}) (fin{inf a b|a b. a  A  b  B})"
also have " = fin({inf x b |b. b  B}  {inf a b |a b. a  A  b  B})"
(is "_ = fin?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 "finA = 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 "finA = 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"           ("(3MIN _./ _)" [0, 10] 10)
"_MIN"      :: "pttrn  'a set  'b  'b"  ("(3MIN __./ _)" [0, 0, 10] 10)
"_MAX1"     :: "pttrns  'b  'b"           ("(3MAX _./ _)" [0, 10] 10)
"_MAX"      :: "pttrn  'a set  'b  'b"  ("(3MAX __./ _)" [0, 0, 10] 10)

translations
"MIN x y. f"    "MIN x. MIN y. f"
"MIN x. f"      "CONST Min (CONST range (λx. f))"
"MIN xA. 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 xA. f"    "CONST Max ((λx. f) ` A)"

text ‹An aside: constMin/constMax on linear orders as special case of constInf_fin/constSup_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:

by (auto simp add: ord.min_def max_def fun_eq_iff)

lemma dual_max:

by (auto simp add: ord.max_def min_def fun_eq_iff)

lemma dual_Min:

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:

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  (aA. x  a)"
using fin_nonempty by (fact Min.bounded_iff)

lemma Max_le_iff [simp]:
"Max A  x  (aA. a  x)"
using fin_nonempty by (fact Max.bounded_iff)

lemma Min_gr_iff [simp]:
"x < Min A  (aA. x < a)"
using fin_nonempty  by (induct rule: finite_ne_induct) simp_all

lemma Max_less_iff [simp]:
"Max A < x  (aA. a < x)"
using fin_nonempty by (induct rule: finite_ne_induct) simp_all

lemma Min_le_iff:
"Min A  x  (aA. 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  (aA. 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  (aA. 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  (aA. 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"  "aA. bB. a  b"  "bB. aA. 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  aA. 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; aA. 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; aA. 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; aA. 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 member_remove by blast
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 infinite_growing:
assumes "X  {}"
assumes *: "x. x  X  yX. y > x"
shows "¬ finite X"
proof
assume "finite X"
with X  {} have "Max X  X" "xX. 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

begin

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)"
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

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)"
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

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 ‹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"
("(3ARG'_MIN _ _./ _)" [1000, 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))"

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"

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 (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
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 (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  {}   mS. ¬(xS. 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 = ])
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 "¬(xS. 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"

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(rule someI2[of _ a])
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"
("(3ARG'_MAX _ _./ _)" [1000, 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))"

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 (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
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"