# Theory Minimum_Maximum

section ‹Minimum and Maximum of Potentially Infinite Sets›
theory Minimum_Maximum
imports Main
begin
text ‹We define minima and maxima of sets. In contrast
to the existing @{const Min} and @{const Max} operators,
these operators are not restricted to finite sets ›
definition Maximum :: "'a :: linorder set ⇒ 'a" where
"Maximum S = (THE x. x ∈ S ∧ (∀ y ∈ S. y ≤ x))"
definition Minimum :: "'a :: linorder set ⇒ 'a" where
"Minimum S = (THE x. x ∈ S ∧ (∀ y ∈ S. x ≤ y))"
definition has_Maximum where "has_Maximum S = (∃ x. x ∈ S ∧ (∀ y ∈ S. y ≤ x))"
definition has_Minimum where "has_Minimum S = (∃ x. x ∈ S ∧ (∀ y ∈ S. x ≤ y))"
lemma eqMaximumI:
assumes "x ∈ S"
and "⋀ y. y ∈ S ⟹ y ≤ x"
shows "Maximum S = x"
unfolding Maximum_def
by (standard, insert assms, auto, fastforce)
lemma eqMinimumI:
assumes "x ∈ S"
and "⋀ y. y ∈ S ⟹ x ≤ y"
shows "Minimum S = x"
unfolding Minimum_def
by (standard, insert assms, auto, fastforce)
lemma has_MaximumD:
assumes "has_Maximum S"
shows "Maximum S ∈ S"
"x ∈ S ⟹ x ≤ Maximum S"
proof -
from assms[unfolded has_Maximum_def]
obtain m where *: "m ∈ S" "⋀ y. y ∈ S ⟹ y ≤ m" by auto
have id: "Maximum S = m"
by (rule eqMaximumI, insert *, auto)
from * id show "Maximum S ∈ S" "x ∈ S ⟹ x ≤ Maximum S" by auto
qed
lemma has_MinimumD:
assumes "has_Minimum S"
shows "Minimum S ∈ S"
"x ∈ S ⟹ Minimum S ≤ x"
proof -
from assms[unfolded has_Minimum_def]
obtain m where *: "m ∈ S" "⋀ y. y ∈ S ⟹ m ≤ y" by auto
have id: "Minimum S = m"
by (rule eqMinimumI, insert *, auto)
from * id show "Minimum S ∈ S" "x ∈ S ⟹ Minimum S ≤ x" by auto
qed
text ‹On non-empty finite sets, @{const Minimum} and @{const Min}
coincide, and similarly @{const Maximum} and @{const Max}.›
lemma Minimum_Min: assumes "finite S" "S ≠ {}"
shows "Minimum S = Min S"
by (rule eqMinimumI, insert assms, auto)
lemma Maximum_Max: assumes "finite S" "S ≠ {}"
shows "Maximum S = Max S"
by (rule eqMaximumI, insert assms, auto)
end