equal
deleted
inserted
replaced
855 apply (simp add: min_def order_le_less) |
855 apply (simp add: min_def order_le_less) |
856 apply (insert linorder_less_linear) |
856 apply (insert linorder_less_linear) |
857 apply (blast intro: order_less_trans) |
857 apply (blast intro: order_less_trans) |
858 done |
858 done |
859 |
859 |
860 declare order_less_irrefl [iff] |
|
861 |
|
862 lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)" |
860 lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)" |
863 apply(simp add:max_def) |
861 apply(simp add:max_def) |
864 apply(rule conjI) |
862 apply(rule conjI) |
865 apply(blast intro:order_trans) |
863 apply(blast intro:order_trans) |
866 apply(simp add:linorder_not_le) |
864 apply(simp add:linorder_not_le) |
895 done |
893 done |
896 |
894 |
897 lemmas min_ac = min_assoc min_commute |
895 lemmas min_ac = min_assoc min_commute |
898 mk_left_commute[of min,OF min_assoc min_commute] |
896 mk_left_commute[of min,OF min_assoc min_commute] |
899 |
897 |
900 declare order_less_irrefl [iff del] |
|
901 declare order_less_irrefl [simp] |
|
902 |
|
903 lemma split_min: |
898 lemma split_min: |
904 "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))" |
899 "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))" |
905 by (simp add: min_def) |
900 by (simp add: min_def) |
906 |
901 |
907 lemma split_max: |
902 lemma split_max: |