Theory Util_MinMax

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


header {* Order and linear order: min and max *}

theory Util_MinMax
imports Lattices
begin

subsection {* Additional lemmata about @{term min} and @{term max} *}

thm min_less_iff_conj
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_max.le_inf_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_max.le_infI


thm min_max.inf_absorb1
(*lemma min_eqL:"[| (x::('a::linorder)) ≤ y |] ==> min x y = x"*)
lemmas min_eqL = min_max.inf_absorb1
(*lemma min_eqR:"[| (y::('a::linorder)) ≤ x |] ==> min x y = y"*)
lemmas min_eqR = min_max.inf_absorb2
lemmas min_eq = min_eqL min_eqR
thm min_eq

thm max_less_iff_conj
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 = min_max.le_sup_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 =  min_max.le_supI

thm min_max.sup_absorb1
(*lemma max_eqL:"[| (y::('a::linorder)) ≤ x |] ==> max x y = x"*)
lemmas max_eqL = min_max.sup_absorb1
(*lemma max_eqR:"[| (x::('a::linorder)) ≤ y |] ==> max x y = y"*)
lemmas max_eqR =  min_max.sup_absorb2
lemmas max_eq = max_eqL max_eqR
thm max_eq



thm 
  le_maxI1
  le_maxI2
(*lemma le_minI1:"min x y ≤ (x::('a::linorder))"*)
lemmas le_minI1 = min_max.inf_le1
(*lemma le_minI2:"min x y ≤ (y::('a::linorder))"*)
lemmas le_minI2 = min_max.inf_le2


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 (fastsimp simp: min_max.inf_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 (fastsimp simp: min_max.sup_mono max_def)+

end