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