equal
deleted
inserted
replaced
307 by (simp add: le_less less_linear) |
307 by (simp add: le_less less_linear) |
308 |
308 |
309 lemma le_cases [case_names le ge]: |
309 lemma le_cases [case_names le ge]: |
310 "(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P" |
310 "(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P" |
311 using linear by blast |
311 using linear by blast |
|
312 |
|
313 lemma (in linorder) le_cases3: |
|
314 "\<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; |
|
315 \<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" |
|
316 by (blast intro: le_cases) |
312 |
317 |
313 lemma linorder_cases [case_names less equal greater]: |
318 lemma linorder_cases [case_names less equal greater]: |
314 "(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P" |
319 "(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P" |
315 using less_linear by blast |
320 using less_linear by blast |
316 |
321 |