equal
deleted
inserted
replaced
816 lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x" |
816 lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x" |
817 apply (simp add: order_less_le) |
817 apply (simp add: order_less_le) |
818 apply (insert linorder_linear, blast) |
818 apply (insert linorder_linear, blast) |
819 done |
819 done |
820 |
820 |
|
821 lemma linorder_le_less_linear: "!!x::'a::linorder. x\<le>y | y<x" |
|
822 by (simp add: order_le_less linorder_less_linear) |
|
823 |
821 lemma linorder_le_cases [case_names le ge]: |
824 lemma linorder_le_cases [case_names le ge]: |
822 "((x::'a::linorder) \<le> y ==> P) ==> (y \<le> x ==> P) ==> P" |
825 "((x::'a::linorder) \<le> y ==> P) ==> (y \<le> x ==> P) ==> P" |
823 by (insert linorder_linear, blast) |
826 by (insert linorder_linear, blast) |
824 |
827 |
825 lemma linorder_cases [case_names less equal greater]: |
828 lemma linorder_cases [case_names less equal greater]: |