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" ..