src/HOL/Lattices.thy
changeset 54861 00d551179872
parent 54859 64ff7f16d5b7
child 54862 c65e5cbdbc97
     1.1 --- a/src/HOL/Lattices.thy	Wed Dec 25 15:52:25 2013 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Wed Dec 25 15:52:25 2013 +0100
     1.3 @@ -712,10 +712,57 @@
     1.4  
     1.5  subsection {* @{text "min/max"} as special case of lattice *}
     1.6  
     1.7 -sublocale linorder < min!: semilattice_order min less_eq less
     1.8 +context linorder
     1.9 +begin
    1.10 +
    1.11 +sublocale min!: semilattice_order min less_eq less
    1.12    + max!: semilattice_order max greater_eq greater
    1.13    by default (auto simp add: min_def max_def)
    1.14  
    1.15 +lemma min_le_iff_disj:
    1.16 +  "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
    1.17 +  unfolding min_def using linear by (auto intro: order_trans)
    1.18 +
    1.19 +lemma le_max_iff_disj:
    1.20 +  "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
    1.21 +  unfolding max_def using linear by (auto intro: order_trans)
    1.22 +
    1.23 +lemma min_less_iff_disj:
    1.24 +  "min x y < z \<longleftrightarrow> x < z \<or> y < z"
    1.25 +  unfolding min_def le_less using less_linear by (auto intro: less_trans)
    1.26 +
    1.27 +lemma less_max_iff_disj:
    1.28 +  "z < max x y \<longleftrightarrow> z < x \<or> z < y"
    1.29 +  unfolding max_def le_less using less_linear by (auto intro: less_trans)
    1.30 +
    1.31 +lemma min_less_iff_conj [simp]:
    1.32 +  "z < min x y \<longleftrightarrow> z < x \<and> z < y"
    1.33 +  unfolding min_def le_less using less_linear by (auto intro: less_trans)
    1.34 +
    1.35 +lemma max_less_iff_conj [simp]:
    1.36 +  "max x y < z \<longleftrightarrow> x < z \<and> y < z"
    1.37 +  unfolding max_def le_less using less_linear by (auto intro: less_trans)
    1.38 +
    1.39 +lemma split_min [no_atp]:
    1.40 +  "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
    1.41 +  by (simp add: min_def)
    1.42 +
    1.43 +lemma split_max [no_atp]:
    1.44 +  "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
    1.45 +  by (simp add: max_def)
    1.46 +
    1.47 +lemma min_of_mono:
    1.48 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
    1.49 +  shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
    1.50 +  by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
    1.51 +
    1.52 +lemma max_of_mono:
    1.53 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
    1.54 +  shows "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)"
    1.55 +  by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
    1.56 +
    1.57 +end
    1.58 +
    1.59  lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.60    by (auto intro: antisym simp add: min_def fun_eq_iff)
    1.61