# 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 \ \ 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) \ 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 \ (- a) ^ n = a ^ n" - by (simp add: neg_power_if) + by (auto elim: evenE) lemma power_minus_odd [simp]: "odd n \ (- 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 \ (- 1) ^ n = 1" - by (simp add: neg_power_if) + by simp lemma neg_one_odd_power [simp]: "odd n \ (- 1) ^ n = - 1" - by (simp_all add: neg_power_if) + by simp end @@ -356,7 +364,7 @@ lemma zero_le_even_power: "even n \ 0 \ a ^ n" - by (auto simp add: even_def elim: dvd_class.dvdE) + by (auto elim: evenE) lemma zero_le_odd_power: "odd n \ 0 \ a ^ n \ 0 \ a" @@ -366,9 +374,8 @@ "0 \ a ^ n \ 0 \ a \ 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" ..