src/HOL/Orderings.thy
changeset 61762 d50b993b4fb9
parent 61699 a81dc5c4d6a9
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Orderings.thy	Mon Nov 30 14:24:51 2015 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Tue Dec 01 14:09:10 2015 +0000
     1.3 @@ -310,6 +310,11 @@
     1.4    "(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P"
     1.5  using linear by blast
     1.6  
     1.7 +lemma (in linorder) le_cases3:
     1.8 +  "\<lbrakk>\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> P; \<lbrakk>y \<le> x; x \<le> z\<rbrakk> \<Longrightarrow> P; \<lbrakk>x \<le> z; z \<le> y\<rbrakk> \<Longrightarrow> P;
     1.9 +    \<lbrakk>z \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> P; \<lbrakk>y \<le> z; z \<le> x\<rbrakk> \<Longrightarrow> P; \<lbrakk>z \<le> x; x \<le> y\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.10 +by (blast intro: le_cases)
    1.11 +
    1.12  lemma linorder_cases [case_names less equal greater]:
    1.13    "(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P"
    1.14  using less_linear by blast