874 |
874 |
875 lemma max_linorder: |
875 lemma max_linorder: |
876 "linorder.max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = max" |
876 "linorder.max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = max" |
877 by (rule+) (simp add: max_def order.max_def) |
877 by (rule+) (simp add: max_def order.max_def) |
878 |
878 |
879 lemmas min_le_iff_disj = order.min_le_iff_disj [where 'b = "?'a::linorder", simplified min_linorder] |
879 lemmas min_le_iff_disj = order.min_le_iff_disj [where 'b = "?'a::linorder", unfolded min_linorder] |
880 lemmas le_max_iff_disj = order.le_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder] |
880 lemmas le_max_iff_disj = order.le_max_iff_disj [where 'b = "?'a::linorder", unfolded max_linorder] |
881 lemmas min_less_iff_disj = order.min_less_iff_disj [where 'b = "?'a::linorder", simplified min_linorder] |
881 lemmas min_less_iff_disj = order.min_less_iff_disj [where 'b = "?'a::linorder", unfolded min_linorder] |
882 lemmas less_max_iff_disj = order.less_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder] |
882 lemmas less_max_iff_disj = order.less_max_iff_disj [where 'b = "?'a::linorder", unfolded max_linorder] |
883 lemmas min_less_iff_conj [simp] = order.min_less_iff_conj [where 'b = "?'a::linorder", simplified min_linorder] |
883 lemmas min_less_iff_conj [simp] = order.min_less_iff_conj [where 'b = "?'a::linorder", unfolded min_linorder] |
884 lemmas max_less_iff_conj [simp] = order.max_less_iff_conj [where 'b = "?'a::linorder", simplified max_linorder] |
884 lemmas max_less_iff_conj [simp] = order.max_less_iff_conj [where 'b = "?'a::linorder", unfolded max_linorder] |
885 lemmas split_min = order.split_min [where 'b = "?'a::linorder", simplified min_linorder] |
885 lemmas split_min = order.split_min [where 'b = "?'a::linorder", unfolded min_linorder] |
886 lemmas split_max = order.split_max [where 'b = "?'a::linorder", simplified max_linorder] |
886 lemmas split_max = order.split_max [where 'b = "?'a::linorder", unfolded max_linorder] |
887 |
887 |
888 lemma min_leastL: "(!!x. least <= x) ==> min least x = least" |
888 lemma min_leastL: "(!!x. least <= x) ==> min least x = least" |
889 by (simp add: min_def) |
889 by (simp add: min_def) |
890 |
890 |
891 lemma max_leastL: "(!!x. least <= x) ==> max least x = x" |
891 lemma max_leastL: "(!!x. least <= x) ==> max least x = x" |