src/HOL/Orderings.thy
changeset 57447 87429bdecad5
parent 56545 8f1e7596deb7
child 58826 2ed2eaabe3df
     1.1 --- a/src/HOL/Orderings.thy	Mon Jun 30 15:45:03 2014 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Mon Jun 30 15:45:21 2014 +0200
     1.3 @@ -319,6 +319,10 @@
     1.4    "(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P"
     1.5  using less_linear by blast
     1.6  
     1.7 +lemma linorder_wlog[case_names le sym]:
     1.8 +  "(\<And>a b. a \<le> b \<Longrightarrow> P a b) \<Longrightarrow> (\<And>a b. P b a \<Longrightarrow> P a b) \<Longrightarrow> P a b"
     1.9 +  by (cases rule: le_cases[of a b]) blast+
    1.10 +
    1.11  lemma not_less: "\<not> x < y \<longleftrightarrow> y \<le> x"
    1.12  apply (simp add: less_le)
    1.13  using linear apply (blast intro: antisym)
    1.14 @@ -360,7 +364,6 @@
    1.15  lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y"
    1.16  unfolding not_le .
    1.17  
    1.18 -
    1.19  text {* Dual order *}
    1.20  
    1.21  lemma dual_linorder: