src/HOL/Parity.thy
changeset 58787 af9eb5e566dd
parent 58778 e29cae8eab1f
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Parity.thy	Sat Oct 25 19:20:28 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Sun Oct 26 19:11:16 2014 +0100
     1.3 @@ -3,148 +3,19 @@
     1.4      Author:     Jacques D. Fleuriot
     1.5  *)
     1.6  
     1.7 -header {* Even and Odd for int and nat *}
     1.8 +header {* Parity in rings and semirings *}
     1.9  
    1.10  theory Parity
    1.11  imports Nat_Transfer
    1.12  begin
    1.13  
    1.14 -subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
    1.15 -
    1.16 -lemma two_dvd_Suc_Suc_iff [simp]:
    1.17 -  "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
    1.18 -  using dvd_add_triv_right_iff [of 2 n] by simp
    1.19 -
    1.20 -lemma two_dvd_Suc_iff:
    1.21 -  "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
    1.22 -  by (induct n) auto
    1.23 -
    1.24 -lemma two_dvd_diff_nat_iff:
    1.25 -  fixes m n :: nat
    1.26 -  shows "2 dvd m - n \<longleftrightarrow> m < n \<or> 2 dvd m + n"
    1.27 -proof (cases "n \<le> m")
    1.28 -  case True
    1.29 -  then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
    1.30 -  moreover have "2 dvd m - n \<longleftrightarrow> 2 dvd m - n + n * 2" by simp
    1.31 -  ultimately have "2 dvd m - n \<longleftrightarrow> 2 dvd m + n" by (simp only:)
    1.32 -  then show ?thesis by auto
    1.33 -next
    1.34 -  case False
    1.35 -  then show ?thesis by simp
    1.36 -qed 
    1.37 -  
    1.38 -lemma two_dvd_diff_iff:
    1.39 -  fixes k l :: int
    1.40 -  shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l"
    1.41 -  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
    1.42 -
    1.43 -lemma two_dvd_abs_add_iff:
    1.44 -  fixes k l :: int
    1.45 -  shows "2 dvd \<bar>k\<bar> + l \<longleftrightarrow> 2 dvd k + l"
    1.46 -  by (cases "k \<ge> 0") (simp_all add: two_dvd_diff_iff ac_simps)
    1.47 -
    1.48 -lemma two_dvd_add_abs_iff:
    1.49 -  fixes k l :: int
    1.50 -  shows "2 dvd k + \<bar>l\<bar> \<longleftrightarrow> 2 dvd k + l"
    1.51 -  using two_dvd_abs_add_iff [of l k] by (simp add: ac_simps)
    1.52 -
    1.53 -
    1.54 -subsection {* Ring structures with parity *}
    1.55 +subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *}
    1.56  
    1.57  class semiring_parity = semiring_dvd + semiring_numeral +
    1.58 -  assumes two_not_dvd_one [simp]: "\<not> 2 dvd 1"
    1.59 -  assumes not_dvd_not_dvd_dvd_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
    1.60 -  assumes two_is_prime: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
    1.61 -  assumes not_dvd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
    1.62 -begin
    1.63 -
    1.64 -lemma two_dvd_plus_one_iff [simp]:
    1.65 -  "2 dvd a + 1 \<longleftrightarrow> \<not> 2 dvd a"
    1.66 -  by (auto simp add: dvd_add_right_iff intro: not_dvd_not_dvd_dvd_add)
    1.67 -
    1.68 -lemma not_two_dvdE [elim?]:
    1.69 -  assumes "\<not> 2 dvd a"
    1.70 -  obtains b where "a = 2 * b + 1"
    1.71 -proof -
    1.72 -  from assms obtain b where *: "a = b + 1"
    1.73 -    by (blast dest: not_dvd_ex_decrement)
    1.74 -  with assms have "2 dvd b + 2" by simp
    1.75 -  then have "2 dvd b" by simp
    1.76 -  then obtain c where "b = 2 * c" ..
    1.77 -  with * have "a = 2 * c + 1" by simp
    1.78 -  with that show thesis .
    1.79 -qed
    1.80 -
    1.81 -end
    1.82 -
    1.83 -instance nat :: semiring_parity
    1.84 -proof
    1.85 -  show "\<not> (2 :: nat) dvd 1"
    1.86 -    by (rule notI, erule dvdE) simp
    1.87 -next
    1.88 -  fix m n :: nat
    1.89 -  assume "\<not> 2 dvd m"
    1.90 -  moreover assume "\<not> 2 dvd n"
    1.91 -  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
    1.92 -    by (simp add: two_dvd_Suc_iff)
    1.93 -  then have "2 dvd Suc m + Suc n"
    1.94 -    by (blast intro: dvd_add)
    1.95 -  also have "Suc m + Suc n = m + n + 2"
    1.96 -    by simp
    1.97 -  finally show "2 dvd m + n"
    1.98 -    using dvd_add_triv_right_iff [of 2 "m + n"] by simp
    1.99 -next
   1.100 -  fix m n :: nat
   1.101 -  assume *: "2 dvd m * n"
   1.102 -  show "2 dvd m \<or> 2 dvd n"
   1.103 -  proof (rule disjCI)
   1.104 -    assume "\<not> 2 dvd n"
   1.105 -    then have "2 dvd Suc n" by (simp add: two_dvd_Suc_iff)
   1.106 -    then obtain r where "Suc n = 2 * r" ..
   1.107 -    moreover from * obtain s where "m * n = 2 * s" ..
   1.108 -    then have "2 * s + m = m * Suc n" by simp
   1.109 -    ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
   1.110 -    then have "m = 2 * (m * r - s)" by simp
   1.111 -    then show "2 dvd m" ..
   1.112 -  qed
   1.113 -next
   1.114 -  fix n :: nat
   1.115 -  assume "\<not> 2 dvd n"
   1.116 -  then show "\<exists>m. n = m + 1"
   1.117 -    by (cases n) simp_all
   1.118 -qed
   1.119 -
   1.120 -class ring_parity = comm_ring_1 + semiring_parity
   1.121 -
   1.122 -instance int :: ring_parity
   1.123 -proof
   1.124 -  show "\<not> (2 :: int) dvd 1" by (simp add: dvd_int_unfold_dvd_nat)
   1.125 -  fix k l :: int
   1.126 -  assume "\<not> 2 dvd k"
   1.127 -  moreover assume "\<not> 2 dvd l"
   1.128 -  ultimately have "2 dvd nat \<bar>k\<bar> + nat \<bar>l\<bar>" 
   1.129 -    by (auto simp add: dvd_int_unfold_dvd_nat intro: not_dvd_not_dvd_dvd_add)
   1.130 -  then have "2 dvd \<bar>k\<bar> + \<bar>l\<bar>"
   1.131 -    by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
   1.132 -  then show "2 dvd k + l"
   1.133 -    by (simp add: two_dvd_abs_add_iff two_dvd_add_abs_iff)
   1.134 -next
   1.135 -  fix k l :: int
   1.136 -  assume "2 dvd k * l"
   1.137 -  then show "2 dvd k \<or> 2 dvd l"
   1.138 -    by (simp add: dvd_int_unfold_dvd_nat two_is_prime nat_abs_mult_distrib)
   1.139 -next
   1.140 -  fix k :: int
   1.141 -  have "k = (k - 1) + 1" by simp
   1.142 -  then show "\<exists>l. k = l + 1" ..
   1.143 -qed
   1.144 -
   1.145 -
   1.146 -subsection {* Dedicated @{text even}/@{text odd} predicate *}
   1.147 -
   1.148 -subsubsection {* Properties *}
   1.149 -
   1.150 -context semiring_parity
   1.151 +  assumes odd_one [simp]: "\<not> 2 dvd 1"
   1.152 +  assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
   1.153 +  assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
   1.154 +  assumes odd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
   1.155  begin
   1.156  
   1.157  abbreviation even :: "'a \<Rightarrow> bool"
   1.158 @@ -155,6 +26,14 @@
   1.159  where
   1.160    "odd a \<equiv> \<not> 2 dvd a"
   1.161  
   1.162 +lemma even_zero [simp]:
   1.163 +  "even 0"
   1.164 +  by (fact dvd_0_right)
   1.165 +
   1.166 +lemma even_plus_one_iff [simp]:
   1.167 +  "even (a + 1) \<longleftrightarrow> odd a"
   1.168 +  by (auto simp add: dvd_add_right_iff intro: odd_even_add)
   1.169 +
   1.170  lemma evenE [elim?]:
   1.171    assumes "even a"
   1.172    obtains b where "a = 2 * b"
   1.173 @@ -163,19 +42,19 @@
   1.174  lemma oddE [elim?]:
   1.175    assumes "odd a"
   1.176    obtains b where "a = 2 * b + 1"
   1.177 -  using assms by (rule not_two_dvdE)
   1.178 -  
   1.179 +proof -
   1.180 +  from assms obtain b where *: "a = b + 1"
   1.181 +    by (blast dest: odd_ex_decrement)
   1.182 +  with assms have "even (b + 2)" by simp
   1.183 +  then have "even b" by simp
   1.184 +  then obtain c where "b = 2 * c" ..
   1.185 +  with * have "a = 2 * c + 1" by simp
   1.186 +  with that show thesis .
   1.187 +qed
   1.188 + 
   1.189  lemma even_times_iff [simp]:
   1.190    "even (a * b) \<longleftrightarrow> even a \<or> even b"
   1.191 -  by (auto simp add: dest: two_is_prime)
   1.192 -
   1.193 -lemma even_zero [simp]:
   1.194 -  "even 0"
   1.195 -  by simp
   1.196 -
   1.197 -lemma odd_one [simp]:
   1.198 -  "odd 1"
   1.199 -  by simp
   1.200 +  by (auto dest: even_multD)
   1.201  
   1.202  lemma even_numeral [simp]:
   1.203    "even (numeral (Num.Bit0 n))"
   1.204 @@ -206,7 +85,7 @@
   1.205  
   1.206  lemma even_add [simp]:
   1.207    "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
   1.208 -  by (auto simp add: dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add)
   1.209 +  by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
   1.210  
   1.211  lemma odd_add [simp]:
   1.212    "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
   1.213 @@ -218,7 +97,7 @@
   1.214  
   1.215  end
   1.216  
   1.217 -context ring_parity
   1.218 +class ring_parity = comm_ring_1 + semiring_parity
   1.219  begin
   1.220  
   1.221  lemma even_minus [simp]:
   1.222 @@ -232,22 +111,110 @@
   1.223  end
   1.224  
   1.225  
   1.226 -subsubsection {* Particularities for @{typ nat} and @{typ int} *}
   1.227 +subsection {* Instances for @{typ nat} and @{typ int} *}
   1.228 +
   1.229 +lemma even_Suc_Suc_iff [simp]:
   1.230 +  "even (Suc (Suc n)) \<longleftrightarrow> even n"
   1.231 +  using dvd_add_triv_right_iff [of 2 n] by simp
   1.232  
   1.233  lemma even_Suc [simp]:
   1.234 -  "even (Suc n) = odd n"
   1.235 -  by (fact two_dvd_Suc_iff)
   1.236 +  "even (Suc n) \<longleftrightarrow> odd n"
   1.237 +  by (induct n) auto
   1.238 +
   1.239 +lemma even_diff_nat [simp]:
   1.240 +  fixes m n :: nat
   1.241 +  shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
   1.242 +proof (cases "n \<le> m")
   1.243 +  case True
   1.244 +  then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
   1.245 +  moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
   1.246 +  ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
   1.247 +  then show ?thesis by auto
   1.248 +next
   1.249 +  case False
   1.250 +  then show ?thesis by simp
   1.251 +qed 
   1.252 +  
   1.253 +lemma even_diff_iff [simp]:
   1.254 +  fixes k l :: int
   1.255 +  shows "even (k - l) \<longleftrightarrow> even (k + l)"
   1.256 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
   1.257 +
   1.258 +lemma even_abs_add_iff [simp]:
   1.259 +  fixes k l :: int
   1.260 +  shows "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)"
   1.261 +  by (cases "k \<ge> 0") (simp_all add: ac_simps)
   1.262 +
   1.263 +lemma even_add_abs_iff [simp]:
   1.264 +  fixes k l :: int
   1.265 +  shows "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)"
   1.266 +  using even_abs_add_iff [of l k] by (simp add: ac_simps)
   1.267 +
   1.268 +instance nat :: semiring_parity
   1.269 +proof
   1.270 +  show "odd (1 :: nat)"
   1.271 +    by (rule notI, erule dvdE) simp
   1.272 +next
   1.273 +  fix m n :: nat
   1.274 +  assume "odd m"
   1.275 +  moreover assume "odd n"
   1.276 +  ultimately have *: "even (Suc m) \<and> even (Suc n)"
   1.277 +    by simp
   1.278 +  then have "even (Suc m + Suc n)"
   1.279 +    by (blast intro: dvd_add)
   1.280 +  also have "Suc m + Suc n = m + n + 2"
   1.281 +    by simp
   1.282 +  finally show "even (m + n)"
   1.283 +    using dvd_add_triv_right_iff [of 2 "m + n"] by simp
   1.284 +next
   1.285 +  fix m n :: nat
   1.286 +  assume *: "even (m * n)"
   1.287 +  show "even m \<or> even n"
   1.288 +  proof (rule disjCI)
   1.289 +    assume "odd n"
   1.290 +    then have "even (Suc n)" by simp
   1.291 +    then obtain r where "Suc n = 2 * r" ..
   1.292 +    moreover from * obtain s where "m * n = 2 * s" ..
   1.293 +    then have "2 * s + m = m * Suc n" by simp
   1.294 +    ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
   1.295 +    then have "m = 2 * (m * r - s)" by simp
   1.296 +    then show "even m" ..
   1.297 +  qed
   1.298 +next
   1.299 +  fix n :: nat
   1.300 +  assume "odd n"
   1.301 +  then show "\<exists>m. n = m + 1"
   1.302 +    by (cases n) simp_all
   1.303 +qed
   1.304  
   1.305  lemma odd_pos: 
   1.306    "odd (n :: nat) \<Longrightarrow> 0 < n"
   1.307    by (auto elim: oddE)
   1.308    
   1.309 -lemma even_diff_nat [simp]:
   1.310 -  fixes m n :: nat
   1.311 -  shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
   1.312 -  by (fact two_dvd_diff_nat_iff)
   1.313 +instance int :: ring_parity
   1.314 +proof
   1.315 +  show "odd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
   1.316 +  fix k l :: int
   1.317 +  assume "odd k"
   1.318 +  moreover assume "odd l"
   1.319 +  ultimately have "even (nat \<bar>k\<bar> + nat \<bar>l\<bar>)" 
   1.320 +    by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add)
   1.321 +  then have "even (\<bar>k\<bar> + \<bar>l\<bar>)"
   1.322 +    by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
   1.323 +  then show "even (k + l)"
   1.324 +    by simp
   1.325 +next
   1.326 +  fix k l :: int
   1.327 +  assume "even (k * l)"
   1.328 +  then show "even k \<or> even l"
   1.329 +    by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib)
   1.330 +next
   1.331 +  fix k :: int
   1.332 +  have "k = (k - 1) + 1" by simp
   1.333 +  then show "\<exists>l. k = l + 1" ..
   1.334 +qed
   1.335  
   1.336 -lemma even_int_iff:
   1.337 +lemma even_int_iff [simp]:
   1.338    "even (int n) \<longleftrightarrow> even n"
   1.339    by (simp add: dvd_int_iff)
   1.340  
   1.341 @@ -255,11 +222,8 @@
   1.342    "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
   1.343    by (simp add: even_int_iff [symmetric])
   1.344  
   1.345 -lemma even_num_iff:
   1.346 -  "0 < n \<Longrightarrow> even n = odd (n - 1 :: nat)"
   1.347 -  by simp
   1.348  
   1.349 -text {* Parity and powers *}
   1.350 +subsection {* Parity and powers *}
   1.351  
   1.352  context comm_ring_1
   1.353  begin
   1.354 @@ -272,10 +236,6 @@
   1.355    "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
   1.356    by (auto elim: oddE)
   1.357  
   1.358 -lemma neg_power_if:
   1.359 -  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
   1.360 -  by simp
   1.361 -
   1.362  lemma neg_one_even_power [simp]:
   1.363    "even n \<Longrightarrow> (- 1) ^ n = 1"
   1.364    by simp
   1.365 @@ -286,28 +246,9 @@
   1.366  
   1.367  end  
   1.368  
   1.369 -lemma zero_less_power_nat_eq_numeral [simp]: -- \<open>FIXME move\<close>
   1.370 -  "0 < (n :: nat) ^ numeral w \<longleftrightarrow> 0 < n \<or> numeral w = (0 :: nat)"
   1.371 -  by (fact nat_zero_less_power_iff)
   1.372 -
   1.373  context linordered_idom
   1.374  begin
   1.375  
   1.376 -lemma power_eq_0_iff' [simp]: -- \<open>FIXME move\<close>
   1.377 -  "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
   1.378 -  by (induct n) auto
   1.379 -
   1.380 -lemma power2_less_eq_zero_iff [simp]: -- \<open>FIXME move\<close>
   1.381 -  "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
   1.382 -proof (cases "a = 0")
   1.383 -  case True then show ?thesis by simp
   1.384 -next
   1.385 -  case False then have "a < 0 \<or> a > 0" by auto
   1.386 -  then have "a\<^sup>2 > 0" by auto
   1.387 -  then have "\<not> a\<^sup>2 \<le> 0" by (simp add: not_le)
   1.388 -  with False show ?thesis by simp
   1.389 -qed
   1.390 -
   1.391  lemma zero_le_even_power:
   1.392    "even n \<Longrightarrow> 0 \<le> a ^ n"
   1.393    by (auto elim: evenE)
   1.394 @@ -316,35 +257,20 @@
   1.395    "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
   1.396    by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
   1.397  
   1.398 -lemma zero_le_power_iff: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
   1.399 -  "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
   1.400 -proof (cases "even n")
   1.401 -  case True
   1.402 -  then obtain k where "n = 2 * k" ..
   1.403 -  then show ?thesis by simp
   1.404 -next
   1.405 -  case False
   1.406 -  then obtain k where "n = 2 * k + 1" ..
   1.407 -  moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
   1.408 -    by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
   1.409 -  ultimately show ?thesis
   1.410 -    by (auto simp add: zero_le_mult_iff zero_le_even_power)
   1.411 -qed
   1.412 -
   1.413  lemma zero_le_power_eq:
   1.414    "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
   1.415 -  using zero_le_power_iff [of a n] by auto
   1.416 -
   1.417 +  by (auto simp add: zero_le_even_power zero_le_odd_power)
   1.418 +  
   1.419  lemma zero_less_power_eq:
   1.420    "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
   1.421  proof -
   1.422    have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
   1.423 -    unfolding power_eq_0_iff' [of a n, symmetric] by blast
   1.424 +    unfolding power_eq_0_iff [of a n, symmetric] by blast
   1.425    show ?thesis
   1.426    unfolding less_le zero_le_power_eq by auto
   1.427  qed
   1.428  
   1.429 -lemma power_less_zero_eq:
   1.430 +lemma power_less_zero_eq [simp]:
   1.431    "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
   1.432    unfolding not_le [symmetric] zero_le_power_eq by auto
   1.433    
   1.434 @@ -408,10 +334,6 @@
   1.435    "a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0"
   1.436    by (fact power_less_zero_eq)
   1.437  
   1.438 -lemma power_eq_0_iff_numeral [simp]:
   1.439 -  "a ^ numeral w = (0 :: nat) \<longleftrightarrow> a = 0 \<and> numeral w \<noteq> (0 :: nat)"
   1.440 -  by (fact power_eq_0_iff)
   1.441 -
   1.442  lemma power_even_abs_numeral [simp]:
   1.443    "even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w"
   1.444    by (fact power_even_abs)