Theory Util_MinMax

(*  Title:      Util_MinMax.thy
    Date:       Oct 2006
    Author:     David Trachtenherz
*)

section ‹Order and linear order: min and max›

theory Util_MinMax
imports Main
begin

subsection ‹Additional lemmata about @{term min} and @{term max}›

lemma min_less_imp_conj: "(z::'a::linorder) < min x y ⟹ z < x ∧ z < y" by simp
lemma conj_less_imp_min: "⟦ z < x; z < y ⟧ ⟹ (z::'a::linorder) < min x y" by simp

(*lemma min_le_iff_conj: "((z::'a::linorder) ≤ min x y) = (z ≤ x ∧ z ≤ y)"*)
lemmas min_le_iff_conj = min.bounded_iff
lemma min_le_imp_conj: "(z::'a::linorder) ≤ min x y ⟹ z ≤ x ∧ z ≤ y" by simp
(*lemma conj_le_imp_min: "⟦ z ≤ x; z ≤ y ⟧ ⟹ (z::'a::linorder) ≤ min x y"*)
lemmas conj_le_imp_min = min.boundedI

(*lemma min_eqL:"⟦ (x::('a::linorder)) ≤ y ⟧ ⟹ min x y = x"*)
lemmas min_eqL = min.absorb1
(*lemma min_eqR:"⟦ (y::('a::linorder)) ≤ x ⟧ ⟹ min x y = y"*)
lemmas min_eqR = min.absorb2
lemmas min_eq = min_eqL min_eqR

lemma max_less_imp_conj:"max x y < b ⟹ x < (b::('a::linorder)) ∧ y < b" by simp
lemma conj_less_imp_max:"⟦ x < (b::('a::linorder)); y < b ⟧ ⟹ max x y < b" by simp

(*lemma max_le_iff_conj: "(max x y ≤ b) = (x ≤ (b::('a::linorder)) ∧ y ≤ b)"*)
lemmas max_le_iff_conj = max.bounded_iff
lemma max_le_imp_conj:"max x y ≤ b ⟹ x ≤ (b::('a::linorder)) ∧ y ≤ b" by simp
(*lemma conj_le_imp_max:"⟦ x ≤ (b::('a::linorder)); y ≤ b ⟧ ⟹ max x y ≤ b"*)
lemmas conj_le_imp_max =  max.boundedI

(*lemma max_eqL:"⟦ (y::('a::linorder)) ≤ x ⟧ ⟹ max x y = x"*)
lemmas max_eqL = max.absorb1
(*lemma max_eqR:"⟦ (x::('a::linorder)) ≤ y ⟧ ⟹ max x y = y"*)
lemmas max_eqR =  max.absorb2
lemmas max_eq = max_eqL max_eqR

(*lemma le_minI1:"min x y ≤ (x::('a::linorder))"*)
lemmas le_minI1 = min.cobounded1
(*lemma le_minI2:"min x y ≤ (y::('a::linorder))"*)
lemmas le_minI2 = min.cobounded2


lemma
  min_le_monoR: "(a::'a::linorder) ≤ b ⟹ min x a ≤ min x b" and
  min_le_monoL: "(a::'a::linorder) ≤ b ⟹ min a x ≤ min b x"
by (fastforce simp: min.mono min_def)+
lemma
  max_le_monoR: "(a::'a::linorder) ≤ b ⟹ max x a ≤ max x b" and
  max_le_monoL: "(a::'a::linorder) ≤ b ⟹ max a x ≤ max b x"
by (fastforce simp: max.mono max_def)+

end