741 |
741 |
742 lemma max_less_iff_conj [simp]: |
742 lemma max_less_iff_conj [simp]: |
743 "max x y < z \<longleftrightarrow> x < z \<and> y < z" |
743 "max x y < z \<longleftrightarrow> x < z \<and> y < z" |
744 unfolding max_def le_less using less_linear by (auto intro: less_trans) |
744 unfolding max_def le_less using less_linear by (auto intro: less_trans) |
745 |
745 |
|
746 lemma min_max_distrib1: |
|
747 "min (max b c) a = max (min b a) (min c a)" |
|
748 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
|
749 |
|
750 lemma min_max_distrib2: |
|
751 "min a (max b c) = max (min a b) (min a c)" |
|
752 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
|
753 |
|
754 lemma max_min_distrib1: |
|
755 "max (min b c) a = min (max b a) (max c a)" |
|
756 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
|
757 |
|
758 lemma max_min_distrib2: |
|
759 "max a (min b c) = min (max a b) (max a c)" |
|
760 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
|
761 |
|
762 lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2 |
|
763 |
746 lemma split_min [no_atp]: |
764 lemma split_min [no_atp]: |
747 "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)" |
765 "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)" |
748 by (simp add: min_def) |
766 by (simp add: min_def) |
749 |
767 |
750 lemma split_max [no_atp]: |
768 lemma split_max [no_atp]: |