# HG changeset patch
# User haftmann
# Date 1413480387 -7200
# Node ID 5c5c148447384525045938bfe5ab2ed16355cd83
# Parent  ee5bf401cfa7f55b0ff7f7e3c2e8421f16163afe
standard elimination rule for even

diff -r ee5bf401cfa7 -r 5c5c14844738 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu Oct 16 19:26:26 2014 +0200
+++ b/src/HOL/Parity.thy	Thu Oct 16 19:26:27 2014 +0200
@@ -197,6 +197,14 @@
 where
   "odd a \<equiv> \<not> even a"
 
+lemma evenE [elim?]:
+  assumes "even a"
+  obtains b where "a = 2 * b"
+proof -
+  from assms have "2 dvd a" by (simp add: even_def)
+  then show thesis using that ..
+qed
+
 lemma oddE [elim?]:
   assumes "odd a"
   obtains b where "a = 2 * b + 1"
@@ -289,7 +297,7 @@
 
 lemma odd_pos: 
   "odd (n :: nat) \<Longrightarrow> 0 < n"
-  by (auto simp add: even_def intro: classical)
+  by (auto elim: oddE)
   
 lemma even_diff_nat [simp]:
   fixes m n :: nat
@@ -310,25 +318,25 @@
 context comm_ring_1
 begin
 
-lemma neg_power_if:
-  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
-  by (induct n) simp_all
-
 lemma power_minus_even [simp]:
   "even n \<Longrightarrow> (- a) ^ n = a ^ n"
-  by (simp add: neg_power_if)
+  by (auto elim: evenE)
 
 lemma power_minus_odd [simp]:
   "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
-  by (simp add: neg_power_if)
+  by (auto elim: oddE)
+
+lemma neg_power_if:
+  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
+  by simp
 
 lemma neg_one_even_power [simp]:
   "even n \<Longrightarrow> (- 1) ^ n = 1"
-  by (simp add: neg_power_if)
+  by simp
 
 lemma neg_one_odd_power [simp]:
   "odd n \<Longrightarrow> (- 1) ^ n = - 1"
-  by (simp_all add: neg_power_if)
+  by simp
 
 end  
 
@@ -356,7 +364,7 @@
 
 lemma zero_le_even_power:
   "even n \<Longrightarrow> 0 \<le> a ^ n"
-  by (auto simp add: even_def elim: dvd_class.dvdE)
+  by (auto elim: evenE)
 
 lemma zero_le_odd_power:
   "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
@@ -366,9 +374,8 @@
   "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
 proof (cases "even n")
   case True
-  then have "2 dvd n" by (simp add: even_def)
   then obtain k where "n = 2 * k" ..
-  thus ?thesis by (simp add: zero_le_even_power True)
+  then show ?thesis by simp
 next
   case False
   then obtain k where "n = 2 * k + 1" ..