Theory LP_Duality.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