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 17:39:06 2013 +0100
     1.3 @@ -743,6 +743,24 @@
     1.4    "max x y < z \<longleftrightarrow> x < z \<and> y < z"
     1.5    unfolding max_def le_less using less_linear by (auto intro: less_trans)
     1.6  
     1.7 +lemma min_max_distrib1:
     1.8 +  "min (max b c) a = max (min b a) (min c a)"
     1.9 +  by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
    1.10 +
    1.11 +lemma min_max_distrib2:
    1.12 +  "min a (max b c) = max (min a b) (min a c)"
    1.13 +  by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
    1.14 +
    1.15 +lemma max_min_distrib1:
    1.16 +  "max (min b c) a = min (max b a) (max c a)"
    1.17 +  by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
    1.18 +
    1.19 +lemma max_min_distrib2:
    1.20 +  "max a (min b c) = min (max a b) (max a c)"
    1.21 +  by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
    1.22 +
    1.23 +lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2
    1.24 +
    1.25  lemma split_min [no_atp]:
    1.26    "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
    1.27    by (simp add: min_def)