src/HOL/Parity.thy
changeset 58688 ddd124805260
parent 58687 5469874b0228
child 58689 ee5bf401cfa7
     1.1 --- a/src/HOL/Parity.thy	Thu Oct 16 19:26:13 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Thu Oct 16 19:26:14 2014 +0200
     1.3 @@ -340,10 +340,15 @@
     1.4    by presburger
     1.5  
     1.6  
     1.7 -subsubsection {* Legacy cruft *}
     1.8 +subsubsection {* Miscellaneous *}
     1.9  
    1.10 +lemma even_nat_plus_one_div_two:
    1.11 +  "even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
    1.12 +  by presburger
    1.13  
    1.14 -subsubsection {* Equivalent definitions *}
    1.15 +lemma odd_nat_plus_one_div_two:
    1.16 +  "odd (x::nat) ==> (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))"
    1.17 +  by presburger
    1.18  
    1.19  lemma even_nat_mod_two_eq_zero:
    1.20    "even (x::nat) ==> x mod Suc (Suc 0) = 0"
    1.21 @@ -369,6 +374,23 @@
    1.22    "odd (x::nat) ==> Suc (Suc (Suc 0) * (x div Suc (Suc 0))) = x"
    1.23    by presburger
    1.24  
    1.25 +lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)" by presburger
    1.26 +lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))" by presburger
    1.27 +
    1.28 +lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2"
    1.29 +  by presburger
    1.30 +
    1.31 +lemma lemma_odd_div2 [simp]: "odd n ==> (n + 1) div 2 = Suc (n div 2)"
    1.32 +  by presburger
    1.33 +
    1.34 +lemma even_num_iff: "0 < n ==> even n = (odd (n - 1 :: nat))" by presburger
    1.35 +lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" by presburger
    1.36 +
    1.37 +lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)" by presburger
    1.38 +
    1.39 +lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
    1.40 +  by presburger
    1.41 +
    1.42  
    1.43  subsubsection {* Parity and powers *}
    1.44  
    1.45 @@ -474,25 +496,21 @@
    1.46    qed
    1.47  qed
    1.48  
    1.49 -
    1.50 -subsubsection {* More Even/Odd Results *}
    1.51 - 
    1.52 -lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)" by presburger
    1.53 -lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))" by presburger
    1.54 -
    1.55 -lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2"
    1.56 -  by presburger
    1.57 -
    1.58 -lemma lemma_odd_div2 [simp]: "odd n ==> (n + 1) div 2 = Suc (n div 2)"
    1.59 -  by presburger
    1.60 -
    1.61 -lemma even_num_iff: "0 < n ==> even n = (odd (n - 1 :: nat))" by presburger
    1.62 -lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" by presburger
    1.63 -
    1.64 -lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)" by presburger
    1.65 -
    1.66 -lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
    1.67 -  by presburger
    1.68 +lemma (in linordered_idom) zero_le_power_iff [presburger]:
    1.69 +  "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
    1.70 +proof (cases "even n")
    1.71 +  case True
    1.72 +  then have "2 dvd n" by (simp add: even_def)
    1.73 +  then obtain k where "n = 2 * k" ..
    1.74 +  thus ?thesis by (simp add: zero_le_even_power True)
    1.75 +next
    1.76 +  case False
    1.77 +  then obtain k where "n = 2 * k + 1" ..
    1.78 +  moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
    1.79 +    by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
    1.80 +  ultimately show ?thesis
    1.81 +    by (auto simp add: zero_le_mult_iff zero_le_even_power)
    1.82 +qed
    1.83  
    1.84  text {* Simplify, when the exponent is a numeral *}
    1.85  
    1.86 @@ -517,35 +535,5 @@
    1.87  lemmas power_even_abs_numeral [simp] =
    1.88    power_even_abs [of "numeral w" _] for w
    1.89  
    1.90 -
    1.91 -subsubsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
    1.92 -
    1.93 -lemma zero_le_power_iff[presburger]:
    1.94 -  "(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom}) | even n)"
    1.95 -proof cases
    1.96 -  assume even: "even n"
    1.97 -  then have "2 dvd n" by (simp add: even_def)
    1.98 -  then obtain k where "n = 2 * k" ..
    1.99 -  thus ?thesis by (simp add: zero_le_even_power even)
   1.100 -next
   1.101 -  assume odd: "odd n"
   1.102 -  then obtain k where "n = 2 * k + 1" ..
   1.103 -  moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
   1.104 -    by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
   1.105 -  ultimately show ?thesis
   1.106 -    by (auto simp add: zero_le_mult_iff zero_le_even_power)
   1.107 -qed
   1.108 -
   1.109 -
   1.110 -subsubsection {* Miscellaneous *}
   1.111 -
   1.112 -lemma even_nat_plus_one_div_two:
   1.113 -  "even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
   1.114 -  by presburger
   1.115 -
   1.116 -lemma odd_nat_plus_one_div_two:
   1.117 -  "odd (x::nat) ==> (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))"
   1.118 -  by presburger
   1.119 -
   1.120  end
   1.121