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) text ‹For natural numbers, having a maximum is the same as being bounded from above and non-empty, or being finite and non-empty.› lemma has_Maximum_nat_iff_bdd_above: "has_Maximum (A :: nat set) ⟷ bdd_above A ∧ A ≠ {}" unfolding has_Maximum_def by (metis bdd_above.I bdd_above_nat emptyE finite_has_maximal nat_le_linear) lemma has_Maximum_nat_iff_finite: "has_Maximum (A :: nat set) ⟷ finite A ∧ A ≠ {}" unfolding has_Maximum_nat_iff_bdd_above bdd_above_nat .. lemma bdd_above_Maximum_nat: "(x :: nat) ∈ A ⟹ bdd_above A ⟹ x ≤ Maximum A" by (rule has_MaximumD, auto simp: has_Maximum_nat_iff_bdd_above) end