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)

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