tuned facts on even and power
authorhaftmann
Thu Oct 16 19:26:26 2014 +0200 (2014-10-16)
changeset 58689ee5bf401cfa7
parent 58688 ddd124805260
child 58690 5c5c14844738
tuned facts on even and power
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Parity.thy	Thu Oct 16 19:26:14 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Thu Oct 16 19:26:26 2014 +0200
     1.3 @@ -287,6 +287,10 @@
     1.4    "even (Suc n) = odd n"
     1.5    by (simp add: even_def two_dvd_Suc_iff)
     1.6  
     1.7 +lemma odd_pos: 
     1.8 +  "odd (n :: nat) \<Longrightarrow> 0 < n"
     1.9 +  by (auto simp add: even_def intro: classical)
    1.10 +  
    1.11  lemma even_diff_nat [simp]:
    1.12    fixes m n :: nat
    1.13    shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
    1.14 @@ -301,6 +305,167 @@
    1.15    by (simp add: even_int_iff [symmetric])
    1.16  
    1.17  
    1.18 +subsubsection {* Parity and powers *}
    1.19 +
    1.20 +context comm_ring_1
    1.21 +begin
    1.22 +
    1.23 +lemma neg_power_if:
    1.24 +  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
    1.25 +  by (induct n) simp_all
    1.26 +
    1.27 +lemma power_minus_even [simp]:
    1.28 +  "even n \<Longrightarrow> (- a) ^ n = a ^ n"
    1.29 +  by (simp add: neg_power_if)
    1.30 +
    1.31 +lemma power_minus_odd [simp]:
    1.32 +  "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
    1.33 +  by (simp add: neg_power_if)
    1.34 +
    1.35 +lemma neg_one_even_power [simp]:
    1.36 +  "even n \<Longrightarrow> (- 1) ^ n = 1"
    1.37 +  by (simp add: neg_power_if)
    1.38 +
    1.39 +lemma neg_one_odd_power [simp]:
    1.40 +  "odd n \<Longrightarrow> (- 1) ^ n = - 1"
    1.41 +  by (simp_all add: neg_power_if)
    1.42 +
    1.43 +end  
    1.44 +
    1.45 +lemma zero_less_power_nat_eq_numeral [simp]: -- \<open>FIXME move\<close>
    1.46 +  "0 < (n :: nat) ^ numeral w \<longleftrightarrow> 0 < n \<or> numeral w = (0 :: nat)"
    1.47 +  by (fact nat_zero_less_power_iff)
    1.48 +
    1.49 +context linordered_idom
    1.50 +begin
    1.51 +
    1.52 +lemma power_eq_0_iff' [simp]: -- \<open>FIXME move\<close>
    1.53 +  "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
    1.54 +  by (induct n) auto
    1.55 +
    1.56 +lemma power2_less_eq_zero_iff [simp]: -- \<open>FIXME move\<close>
    1.57 +  "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
    1.58 +proof (cases "a = 0")
    1.59 +  case True then show ?thesis by simp
    1.60 +next
    1.61 +  case False then have "a < 0 \<or> a > 0" by auto
    1.62 +  then have "a\<^sup>2 > 0" by auto
    1.63 +  then have "\<not> a\<^sup>2 \<le> 0" by (simp add: not_le)
    1.64 +  with False show ?thesis by simp
    1.65 +qed
    1.66 +
    1.67 +lemma zero_le_even_power:
    1.68 +  "even n \<Longrightarrow> 0 \<le> a ^ n"
    1.69 +  by (auto simp add: even_def elim: dvd_class.dvdE)
    1.70 +
    1.71 +lemma zero_le_odd_power:
    1.72 +  "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
    1.73 +  by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
    1.74 +
    1.75 +lemma zero_le_power_iff [presburger]:
    1.76 +  "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
    1.77 +proof (cases "even n")
    1.78 +  case True
    1.79 +  then have "2 dvd n" by (simp add: even_def)
    1.80 +  then obtain k where "n = 2 * k" ..
    1.81 +  thus ?thesis by (simp add: zero_le_even_power True)
    1.82 +next
    1.83 +  case False
    1.84 +  then obtain k where "n = 2 * k + 1" ..
    1.85 +  moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
    1.86 +    by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
    1.87 +  ultimately show ?thesis
    1.88 +    by (auto simp add: zero_le_mult_iff zero_le_even_power)
    1.89 +qed
    1.90 +
    1.91 +lemma zero_le_power_eq [presburger]: -- \<open>FIXME weaker version of @{text zero_le_power_iff}\<close>
    1.92 +  "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
    1.93 +  using zero_le_power_iff [of a n] by auto
    1.94 +
    1.95 +lemma zero_less_power_eq [presburger]:
    1.96 +  "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
    1.97 +proof -
    1.98 +  have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
    1.99 +    unfolding power_eq_0_iff' [of a n, symmetric] by blast
   1.100 +  show ?thesis
   1.101 +  unfolding less_le zero_le_power_iff by auto
   1.102 +qed
   1.103 +
   1.104 +lemma power_less_zero_eq [presburger]:
   1.105 +  "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
   1.106 +  unfolding not_le [symmetric] zero_le_power_eq by auto
   1.107 +  
   1.108 +lemma power_le_zero_eq [presburger]:
   1.109 +  "a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)"
   1.110 +  unfolding not_less [symmetric] zero_less_power_eq by auto 
   1.111 +
   1.112 +lemma power_even_abs:
   1.113 +  "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n"
   1.114 +  using power_abs [of a n] by (simp add: zero_le_even_power)
   1.115 +
   1.116 +lemma power_mono_even:
   1.117 +  assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>"
   1.118 +  shows "a ^ n \<le> b ^ n"
   1.119 +proof -
   1.120 +  have "0 \<le> \<bar>a\<bar>" by auto
   1.121 +  with `\<bar>a\<bar> \<le> \<bar>b\<bar>`
   1.122 +  have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n" by (rule power_mono)
   1.123 +  with `even n` show ?thesis by (simp add: power_even_abs)  
   1.124 +qed
   1.125 +
   1.126 +lemma power_mono_odd:
   1.127 +  assumes "odd n" and "a \<le> b"
   1.128 +  shows "a ^ n \<le> b ^ n"
   1.129 +proof (cases "b < 0")
   1.130 +  case True with `a \<le> b` have "- b \<le> - a" and "0 \<le> - b" by auto
   1.131 +  hence "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono)
   1.132 +  with `odd n` show ?thesis by simp
   1.133 +next
   1.134 +  case False then have "0 \<le> b" by auto
   1.135 +  show ?thesis
   1.136 +  proof (cases "a < 0")
   1.137 +    case True then have "n \<noteq> 0" and "a \<le> 0" using `odd n` [THEN odd_pos] by auto
   1.138 +    then have "a ^ n \<le> 0" unfolding power_le_zero_eq using `odd n` by auto
   1.139 +    moreover
   1.140 +    from `0 \<le> b` have "0 \<le> b ^ n" by auto
   1.141 +    ultimately show ?thesis by auto
   1.142 +  next
   1.143 +    case False then have "0 \<le> a" by auto
   1.144 +    with `a \<le> b` show ?thesis using power_mono by auto
   1.145 +  qed
   1.146 +qed
   1.147 + 
   1.148 +text {* Simplify, when the exponent is a numeral *}
   1.149 +
   1.150 +lemma zero_le_power_eq_numeral [simp]:
   1.151 +  "0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a"
   1.152 +  by (fact zero_le_power_eq)
   1.153 +
   1.154 +lemma zero_less_power_eq_numeral [simp]:
   1.155 +  "0 < a ^ numeral w \<longleftrightarrow> numeral w = (0 :: nat)
   1.156 +    \<or> even (numeral w :: nat) \<and> a \<noteq> 0 \<or> odd (numeral w :: nat) \<and> 0 < a"
   1.157 +  by (fact zero_less_power_eq)
   1.158 +
   1.159 +lemma power_le_zero_eq_numeral [simp]:
   1.160 +  "a ^ numeral w \<le> 0 \<longleftrightarrow> (0 :: nat) < numeral w
   1.161 +    \<and> (odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)"
   1.162 +  by (fact power_le_zero_eq)
   1.163 +
   1.164 +lemma power_less_zero_eq_numeral [simp]:
   1.165 +  "a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0"
   1.166 +  by (fact power_less_zero_eq)
   1.167 +
   1.168 +lemma power_eq_0_iff_numeral [simp]:
   1.169 +  "a ^ numeral w = (0 :: nat) \<longleftrightarrow> a = 0 \<and> numeral w \<noteq> (0 :: nat)"
   1.170 +  by (fact power_eq_0_iff)
   1.171 +
   1.172 +lemma power_even_abs_numeral [simp]:
   1.173 +  "even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w"
   1.174 +  by (fact power_even_abs)
   1.175 +
   1.176 +end
   1.177 +
   1.178 +
   1.179  subsubsection {* Tools setup *}
   1.180  
   1.181  declare transfer_morphism_int_nat [transfer add return:
   1.182 @@ -391,149 +556,5 @@
   1.183  lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
   1.184    by presburger
   1.185  
   1.186 -
   1.187 -subsubsection {* Parity and powers *}
   1.188 -
   1.189 -lemma (in comm_ring_1) neg_power_if:
   1.190 -  "(- a) ^ n = (if even n then (a ^ n) else - (a ^ n))"
   1.191 -  by (induct n) simp_all
   1.192 -
   1.193 -lemma (in comm_ring_1)
   1.194 -  shows neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
   1.195 -  and neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
   1.196 -  by (simp_all add: neg_power_if)
   1.197 -
   1.198 -lemma zero_le_even_power: "even n ==>
   1.199 -    0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
   1.200 -  apply (simp add: even_def)
   1.201 -  apply (erule dvdE)
   1.202 -  apply (erule ssubst)
   1.203 -  unfolding mult.commute [of 2]
   1.204 -  unfolding power_mult power2_eq_square
   1.205 -  apply (rule zero_le_square)
   1.206 -  done
   1.207 -
   1.208 -lemma zero_le_odd_power:
   1.209 -  "odd n \<Longrightarrow> 0 \<le> (x::'a::{linordered_idom}) ^ n \<longleftrightarrow> 0 \<le> x"
   1.210 -  by (erule oddE) (auto simp: power_add zero_le_mult_iff mult_2 order_antisym_conv)
   1.211 -
   1.212 -lemma zero_le_power_eq [presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
   1.213 -    (even n | (odd n & 0 <= x))"
   1.214 -  apply auto
   1.215 -  apply (subst zero_le_odd_power [symmetric])
   1.216 -  apply assumption+
   1.217 -  apply (erule zero_le_even_power)
   1.218 -  done
   1.219 -
   1.220 -lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{linordered_idom}) ^ n) =
   1.221 -    (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))"
   1.222 -  unfolding order_less_le zero_le_power_eq by auto
   1.223 -
   1.224 -lemma power_less_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n < 0) =
   1.225 -    (odd n & x < 0)"
   1.226 -  apply (subst linorder_not_le [symmetric])+
   1.227 -  apply (subst zero_le_power_eq)
   1.228 -  apply auto
   1.229 -  done
   1.230 -
   1.231 -lemma power_le_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n <= 0) =
   1.232 -    (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))"
   1.233 -  apply (subst linorder_not_less [symmetric])+
   1.234 -  apply (subst zero_less_power_eq)
   1.235 -  apply auto
   1.236 -  done
   1.237 -
   1.238 -lemma power_even_abs: "even n ==>
   1.239 -    (abs (x::'a::{linordered_idom}))^n = x^n"
   1.240 -  apply (subst power_abs [symmetric])
   1.241 -  apply (simp add: zero_le_even_power)
   1.242 -  done
   1.243 -
   1.244 -lemma power_minus_even [simp]: "even n ==>
   1.245 -    (- x)^n = (x^n::'a::{comm_ring_1})"
   1.246 -  apply (subst power_minus)
   1.247 -  apply simp
   1.248 -  done
   1.249 -
   1.250 -lemma power_minus_odd [simp]: "odd n ==>
   1.251 -    (- x)^n = - (x^n::'a::{comm_ring_1})"
   1.252 -  apply (subst power_minus)
   1.253 -  apply simp
   1.254 -  done
   1.255 -
   1.256 -lemma power_mono_even: fixes x y :: "'a :: {linordered_idom}"
   1.257 -  assumes "even n" and "\<bar>x\<bar> \<le> \<bar>y\<bar>"
   1.258 -  shows "x^n \<le> y^n"
   1.259 -proof -
   1.260 -  have "0 \<le> \<bar>x\<bar>" by auto
   1.261 -  with `\<bar>x\<bar> \<le> \<bar>y\<bar>`
   1.262 -  have "\<bar>x\<bar>^n \<le> \<bar>y\<bar>^n" by (rule power_mono)
   1.263 -  thus ?thesis unfolding power_even_abs[OF `even n`] .
   1.264 -qed
   1.265 -
   1.266 -lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger
   1.267 -
   1.268 -lemma power_mono_odd: fixes x y :: "'a :: {linordered_idom}"
   1.269 -  assumes "odd n" and "x \<le> y"
   1.270 -  shows "x^n \<le> y^n"
   1.271 -proof (cases "y < 0")
   1.272 -  case True with `x \<le> y` have "-y \<le> -x" and "0 \<le> -y" by auto
   1.273 -  hence "(-y)^n \<le> (-x)^n" by (rule power_mono)
   1.274 -  thus ?thesis unfolding power_minus_odd[OF `odd n`] by auto
   1.275 -next
   1.276 -  case False
   1.277 -  show ?thesis
   1.278 -  proof (cases "x < 0")
   1.279 -    case True hence "n \<noteq> 0" and "x \<le> 0" using `odd n`[THEN odd_pos] by auto
   1.280 -    hence "x^n \<le> 0" unfolding power_le_zero_eq using `odd n` by auto
   1.281 -    moreover
   1.282 -    from `\<not> y < 0` have "0 \<le> y" by auto
   1.283 -    hence "0 \<le> y^n" by auto
   1.284 -    ultimately show ?thesis by auto
   1.285 -  next
   1.286 -    case False hence "0 \<le> x" by auto
   1.287 -    with `x \<le> y` show ?thesis using power_mono by auto
   1.288 -  qed
   1.289 -qed
   1.290 -
   1.291 -lemma (in linordered_idom) zero_le_power_iff [presburger]:
   1.292 -  "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
   1.293 -proof (cases "even n")
   1.294 -  case True
   1.295 -  then have "2 dvd n" by (simp add: even_def)
   1.296 -  then obtain k where "n = 2 * k" ..
   1.297 -  thus ?thesis by (simp add: zero_le_even_power True)
   1.298 -next
   1.299 -  case False
   1.300 -  then obtain k where "n = 2 * k + 1" ..
   1.301 -  moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
   1.302 -    by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
   1.303 -  ultimately show ?thesis
   1.304 -    by (auto simp add: zero_le_mult_iff zero_le_even_power)
   1.305 -qed
   1.306 -
   1.307 -text {* Simplify, when the exponent is a numeral *}
   1.308 -
   1.309 -lemmas zero_le_power_eq_numeral [simp] =
   1.310 -  zero_le_power_eq [of _ "numeral w"] for w
   1.311 -
   1.312 -lemmas zero_less_power_eq_numeral [simp] =
   1.313 -  zero_less_power_eq [of _ "numeral w"] for w
   1.314 -
   1.315 -lemmas power_le_zero_eq_numeral [simp] =
   1.316 -  power_le_zero_eq [of _ "numeral w"] for w
   1.317 -
   1.318 -lemmas power_less_zero_eq_numeral [simp] =
   1.319 -  power_less_zero_eq [of _ "numeral w"] for w
   1.320 -
   1.321 -lemmas zero_less_power_nat_eq_numeral [simp] =
   1.322 -  nat_zero_less_power_iff [of _ "numeral w"] for w
   1.323 -
   1.324 -lemmas power_eq_0_iff_numeral [simp] =
   1.325 -  power_eq_0_iff [of _ "numeral w"] for w
   1.326 -
   1.327 -lemmas power_even_abs_numeral [simp] =
   1.328 -  power_even_abs [of "numeral w" _] for w
   1.329 -
   1.330  end
   1.331