src/HOL/Parity.thy
 changeset 58681 a478a0742a8e parent 58680 6b2fa479945f child 58687 5469874b0228
```     1.1 --- a/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
1.2 +++ b/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
1.3 @@ -183,7 +183,7 @@
1.4  where
1.5    "odd a \<equiv> \<not> even a"
1.6
1.7 -lemma odd_dvdE [elim?]:
1.8 +lemma oddE [elim?]:
1.9    assumes "odd a"
1.10    obtains b where "a = 2 * b + 1"
1.11  proof -
1.12 @@ -291,26 +291,6 @@
1.13
1.14  subsubsection {* Legacy cruft *}
1.15
1.16 -lemma even_plus_even:
1.17 -  "even (x::int) ==> even y ==> even (x + y)"
1.18 -  by simp
1.19 -
1.20 -lemma odd_plus_odd:
1.21 -  "odd (x::int) ==> odd y ==> even (x + y)"
1.22 -  by simp
1.23 -
1.24 -lemma even_sum_nat:
1.25 -  "even ((x::nat) + y) = ((even x & even y) | (odd x & odd y))"
1.26 -  by auto
1.27 -
1.28 -lemma odd_pow:
1.29 -  "odd x ==> odd((x::int)^n)"
1.30 -  by simp
1.31 -
1.32 -lemma even_equiv_def:
1.33 -  "even (x::int) = (EX y. x = 2 * y)"
1.34 -  by presburger
1.35 -
1.36
1.37  subsubsection {* Equivalent definitions *}
1.38
1.39 @@ -361,9 +341,6 @@
1.40  lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==>
1.41      Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" by presburger
1.42
1.43 -lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))"
1.44 -  by presburger
1.45 -
1.46
1.47  subsubsection {* Parity and powers *}
1.48
1.49 @@ -386,11 +363,9 @@
1.50    apply (rule zero_le_square)
1.51    done
1.52
1.53 -lemma zero_le_odd_power: "odd n ==>
1.54 -    (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)"
1.55 -apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff)
1.56 -apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square)
1.57 -done
1.58 +lemma zero_le_odd_power:
1.59 +  "odd n \<Longrightarrow> 0 \<le> (x::'a::{linordered_idom}) ^ n \<longleftrightarrow> 0 \<le> x"
1.60 +  by (erule oddE) (auto simp: power_add zero_le_mult_iff mult_2 order_antisym_conv)
1.61
1.62  lemma zero_le_power_eq [presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
1.63      (even n | (odd n & 0 <= x))"
1.64 @@ -525,8 +500,7 @@
1.65    thus ?thesis by (simp add: zero_le_even_power even)
1.66  next
1.67    assume odd: "odd n"
1.68 -  then obtain k where "n = Suc(2*k)"
1.69 -    by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
1.70 +  then obtain k where "n = 2 * k + 1" ..
1.71    moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
1.72      by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
1.73    ultimately show ?thesis
```