src/HOL/Parity.thy
 changeset 58690 5c5c14844738 parent 58689 ee5bf401cfa7 child 58691 68f8d22a6867
```     1.1 --- a/src/HOL/Parity.thy	Thu Oct 16 19:26:26 2014 +0200
1.2 +++ b/src/HOL/Parity.thy	Thu Oct 16 19:26:27 2014 +0200
1.3 @@ -197,6 +197,14 @@
1.4  where
1.5    "odd a \<equiv> \<not> even a"
1.6
1.7 +lemma evenE [elim?]:
1.8 +  assumes "even a"
1.9 +  obtains b where "a = 2 * b"
1.10 +proof -
1.11 +  from assms have "2 dvd a" by (simp add: even_def)
1.12 +  then show thesis using that ..
1.13 +qed
1.14 +
1.15  lemma oddE [elim?]:
1.16    assumes "odd a"
1.17    obtains b where "a = 2 * b + 1"
1.18 @@ -289,7 +297,7 @@
1.19
1.20  lemma odd_pos:
1.21    "odd (n :: nat) \<Longrightarrow> 0 < n"
1.22 -  by (auto simp add: even_def intro: classical)
1.23 +  by (auto elim: oddE)
1.24
1.25  lemma even_diff_nat [simp]:
1.26    fixes m n :: nat
1.27 @@ -310,25 +318,25 @@
1.28  context comm_ring_1
1.29  begin
1.30
1.31 -lemma neg_power_if:
1.32 -  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
1.33 -  by (induct n) simp_all
1.34 -
1.35  lemma power_minus_even [simp]:
1.36    "even n \<Longrightarrow> (- a) ^ n = a ^ n"
1.37 -  by (simp add: neg_power_if)
1.38 +  by (auto elim: evenE)
1.39
1.40  lemma power_minus_odd [simp]:
1.41    "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
1.42 -  by (simp add: neg_power_if)
1.43 +  by (auto elim: oddE)
1.44 +
1.45 +lemma neg_power_if:
1.46 +  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
1.47 +  by simp
1.48
1.49  lemma neg_one_even_power [simp]:
1.50    "even n \<Longrightarrow> (- 1) ^ n = 1"
1.51 -  by (simp add: neg_power_if)
1.52 +  by simp
1.53
1.54  lemma neg_one_odd_power [simp]:
1.55    "odd n \<Longrightarrow> (- 1) ^ n = - 1"
1.56 -  by (simp_all add: neg_power_if)
1.57 +  by simp
1.58
1.59  end
1.60
1.61 @@ -356,7 +364,7 @@
1.62
1.63  lemma zero_le_even_power:
1.64    "even n \<Longrightarrow> 0 \<le> a ^ n"
1.65 -  by (auto simp add: even_def elim: dvd_class.dvdE)
1.66 +  by (auto elim: evenE)
1.67
1.68  lemma zero_le_odd_power:
1.69    "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
1.70 @@ -366,9 +374,8 @@
1.71    "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
1.72  proof (cases "even n")
1.73    case True
1.74 -  then have "2 dvd n" by (simp add: even_def)
1.75    then obtain k where "n = 2 * k" ..
1.76 -  thus ?thesis by (simp add: zero_le_even_power True)
1.77 +  then show ?thesis by simp
1.78  next
1.79    case False
1.80    then obtain k where "n = 2 * k + 1" ..
```