src/HOL/Parity.thy
 author wenzelm Sat Nov 04 15:24:40 2017 +0100 (19 months ago) changeset 67003 49850a679c2c parent 66840 0d689d71dbdc child 67051 e7e54a0b9197 permissions -rw-r--r--
more robust sorted_entries;
```     1 (*  Title:      HOL/Parity.thy
```
```     2     Author:     Jeremy Avigad
```
```     3     Author:     Jacques D. Fleuriot
```
```     4 *)
```
```     5
```
```     6 section \<open>Parity in rings and semirings\<close>
```
```     7
```
```     8 theory Parity
```
```     9   imports Euclidean_Division
```
```    10 begin
```
```    11
```
```    12 subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
```
```    13
```
```    14 class semiring_parity = linordered_semidom + unique_euclidean_semiring +
```
```    15   assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
```
```    16     and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
```
```    17     and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"
```
```    18 begin
```
```    19
```
```    20 lemma division_segment_eq_iff:
```
```    21   "a = b" if "division_segment a = division_segment b"
```
```    22     and "euclidean_size a = euclidean_size b"
```
```    23   using that division_segment_euclidean_size [of a] by simp
```
```    24
```
```    25 lemma euclidean_size_of_nat [simp]:
```
```    26   "euclidean_size (of_nat n) = n"
```
```    27 proof -
```
```    28   have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n"
```
```    29     by (fact division_segment_euclidean_size)
```
```    30   then show ?thesis by simp
```
```    31 qed
```
```    32
```
```    33 lemma of_nat_euclidean_size:
```
```    34   "of_nat (euclidean_size a) = a div division_segment a"
```
```    35 proof -
```
```    36   have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a"
```
```    37     by (subst nonzero_mult_div_cancel_left) simp_all
```
```    38   also have "\<dots> = a div division_segment a"
```
```    39     by simp
```
```    40   finally show ?thesis .
```
```    41 qed
```
```    42
```
```    43 lemma division_segment_1 [simp]:
```
```    44   "division_segment 1 = 1"
```
```    45   using division_segment_of_nat [of 1] by simp
```
```    46
```
```    47 lemma division_segment_numeral [simp]:
```
```    48   "division_segment (numeral k) = 1"
```
```    49   using division_segment_of_nat [of "numeral k"] by simp
```
```    50
```
```    51 lemma euclidean_size_1 [simp]:
```
```    52   "euclidean_size 1 = 1"
```
```    53   using euclidean_size_of_nat [of 1] by simp
```
```    54
```
```    55 lemma euclidean_size_numeral [simp]:
```
```    56   "euclidean_size (numeral k) = numeral k"
```
```    57   using euclidean_size_of_nat [of "numeral k"] by simp
```
```    58
```
```    59 lemma of_nat_dvd_iff:
```
```    60   "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
```
```    61 proof (cases "m = 0")
```
```    62   case True
```
```    63   then show ?thesis
```
```    64     by simp
```
```    65 next
```
```    66   case False
```
```    67   show ?thesis
```
```    68   proof
```
```    69     assume ?Q
```
```    70     then show ?P
```
```    71       by (auto elim: dvd_class.dvdE)
```
```    72   next
```
```    73     assume ?P
```
```    74     with False have "of_nat n = of_nat n div of_nat m * of_nat m"
```
```    75       by simp
```
```    76     then have "of_nat n = of_nat (n div m * m)"
```
```    77       by (simp add: of_nat_div)
```
```    78     then have "n = n div m * m"
```
```    79       by (simp only: of_nat_eq_iff)
```
```    80     then have "n = m * (n div m)"
```
```    81       by (simp add: ac_simps)
```
```    82     then show ?Q ..
```
```    83   qed
```
```    84 qed
```
```    85
```
```    86 lemma of_nat_mod:
```
```    87   "of_nat (m mod n) = of_nat m mod of_nat n"
```
```    88 proof -
```
```    89   have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m"
```
```    90     by (simp add: div_mult_mod_eq)
```
```    91   also have "of_nat m = of_nat (m div n * n + m mod n)"
```
```    92     by simp
```
```    93   finally show ?thesis
```
```    94     by (simp only: of_nat_div of_nat_mult of_nat_add) simp
```
```    95 qed
```
```    96
```
```    97 lemma one_div_two_eq_zero [simp]:
```
```    98   "1 div 2 = 0"
```
```    99 proof -
```
```   100   from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0"
```
```   101     by (simp only:) simp
```
```   102   then show ?thesis
```
```   103     by simp
```
```   104 qed
```
```   105
```
```   106 lemma one_mod_two_eq_one [simp]:
```
```   107   "1 mod 2 = 1"
```
```   108 proof -
```
```   109   from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
```
```   110     by (simp only:) simp
```
```   111   then show ?thesis
```
```   112     by simp
```
```   113 qed
```
```   114
```
```   115 abbreviation even :: "'a \<Rightarrow> bool"
```
```   116   where "even a \<equiv> 2 dvd a"
```
```   117
```
```   118 abbreviation odd :: "'a \<Rightarrow> bool"
```
```   119   where "odd a \<equiv> \<not> 2 dvd a"
```
```   120
```
```   121 lemma even_iff_mod_2_eq_zero:
```
```   122   "even a \<longleftrightarrow> a mod 2 = 0"
```
```   123   by (fact dvd_eq_mod_eq_0)
```
```   124
```
```   125 lemma odd_iff_mod_2_eq_one:
```
```   126   "odd a \<longleftrightarrow> a mod 2 = 1"
```
```   127 proof
```
```   128   assume "a mod 2 = 1"
```
```   129   then show "odd a"
```
```   130     by auto
```
```   131 next
```
```   132   assume "odd a"
```
```   133   have eucl: "euclidean_size (a mod 2) = 1"
```
```   134   proof (rule order_antisym)
```
```   135     show "euclidean_size (a mod 2) \<le> 1"
```
```   136       using mod_size_less [of 2 a] by simp
```
```   137     show "1 \<le> euclidean_size (a mod 2)"
```
```   138       using \<open>odd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0)
```
```   139   qed
```
```   140   from \<open>odd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)"
```
```   141     by simp
```
```   142   then have "\<not> of_nat 2 dvd of_nat (euclidean_size a)"
```
```   143     by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment)
```
```   144   then have "\<not> 2 dvd euclidean_size a"
```
```   145     using of_nat_dvd_iff [of 2] by simp
```
```   146   then have "euclidean_size a mod 2 = 1"
```
```   147     by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0)
```
```   148   then have "of_nat (euclidean_size a mod 2) = of_nat 1"
```
```   149     by simp
```
```   150   then have "of_nat (euclidean_size a) mod 2 = 1"
```
```   151     by (simp add: of_nat_mod)
```
```   152   from \<open>odd a\<close> eucl
```
```   153   show "a mod 2 = 1"
```
```   154     by (auto intro: division_segment_eq_iff simp add: division_segment_mod)
```
```   155 qed
```
```   156
```
```   157 lemma parity_cases [case_names even odd]:
```
```   158   assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P"
```
```   159   assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P"
```
```   160   shows P
```
```   161   using assms by (cases "even a") (simp_all add: odd_iff_mod_2_eq_one)
```
```   162
```
```   163 lemma not_mod_2_eq_1_eq_0 [simp]:
```
```   164   "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
```
```   165   by (cases a rule: parity_cases) simp_all
```
```   166
```
```   167 lemma not_mod_2_eq_0_eq_1 [simp]:
```
```   168   "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
```
```   169   by (cases a rule: parity_cases) simp_all
```
```   170
```
```   171 lemma evenE [elim?]:
```
```   172   assumes "even a"
```
```   173   obtains b where "a = 2 * b"
```
```   174   using assms by (rule dvdE)
```
```   175
```
```   176 lemma oddE [elim?]:
```
```   177   assumes "odd a"
```
```   178   obtains b where "a = 2 * b + 1"
```
```   179 proof -
```
```   180   have "a = 2 * (a div 2) + a mod 2"
```
```   181     by (simp add: mult_div_mod_eq)
```
```   182   with assms have "a = 2 * (a div 2) + 1"
```
```   183     by (simp add: odd_iff_mod_2_eq_one)
```
```   184   then show ?thesis ..
```
```   185 qed
```
```   186
```
```   187 lemma mod_2_eq_odd:
```
```   188   "a mod 2 = of_bool (odd a)"
```
```   189   by (auto elim: oddE)
```
```   190
```
```   191 lemma one_mod_2_pow_eq [simp]:
```
```   192   "1 mod (2 ^ n) = of_bool (n > 0)"
```
```   193 proof -
```
```   194   have "1 mod (2 ^ n) = (of_bool (n > 0) :: nat)"
```
```   195     by (induct n) (simp_all add: mod_mult2_eq)
```
```   196   then have "of_nat (1 mod (2 ^ n)) = of_bool (n > 0)"
```
```   197     by simp
```
```   198   then show ?thesis
```
```   199     by (simp add: of_nat_mod)
```
```   200 qed
```
```   201
```
```   202 lemma even_of_nat [simp]:
```
```   203   "even (of_nat a) \<longleftrightarrow> even a"
```
```   204 proof -
```
```   205   have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a"
```
```   206     by simp
```
```   207   also have "\<dots> \<longleftrightarrow> even a"
```
```   208     by (simp only: of_nat_dvd_iff)
```
```   209   finally show ?thesis .
```
```   210 qed
```
```   211
```
```   212 lemma even_zero [simp]:
```
```   213   "even 0"
```
```   214   by (fact dvd_0_right)
```
```   215
```
```   216 lemma odd_one [simp]:
```
```   217   "odd 1"
```
```   218 proof -
```
```   219   have "\<not> (2 :: nat) dvd 1"
```
```   220     by simp
```
```   221   then have "\<not> of_nat 2 dvd of_nat 1"
```
```   222     unfolding of_nat_dvd_iff by simp
```
```   223   then show ?thesis
```
```   224     by simp
```
```   225 qed
```
```   226
```
```   227 lemma odd_even_add:
```
```   228   "even (a + b)" if "odd a" and "odd b"
```
```   229 proof -
```
```   230   from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1"
```
```   231     by (blast elim: oddE)
```
```   232   then have "a + b = 2 * c + 2 * d + (1 + 1)"
```
```   233     by (simp only: ac_simps)
```
```   234   also have "\<dots> = 2 * (c + d + 1)"
```
```   235     by (simp add: algebra_simps)
```
```   236   finally show ?thesis ..
```
```   237 qed
```
```   238
```
```   239 lemma even_add [simp]:
```
```   240   "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
```
```   241   by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
```
```   242
```
```   243 lemma odd_add [simp]:
```
```   244   "odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)"
```
```   245   by simp
```
```   246
```
```   247 lemma even_plus_one_iff [simp]:
```
```   248   "even (a + 1) \<longleftrightarrow> odd a"
```
```   249   by (auto simp add: dvd_add_right_iff intro: odd_even_add)
```
```   250
```
```   251 lemma even_mult_iff [simp]:
```
```   252   "even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q")
```
```   253 proof
```
```   254   assume ?Q
```
```   255   then show ?P
```
```   256     by auto
```
```   257 next
```
```   258   assume ?P
```
```   259   show ?Q
```
```   260   proof (rule ccontr)
```
```   261     assume "\<not> (even a \<or> even b)"
```
```   262     then have "odd a" and "odd b"
```
```   263       by auto
```
```   264     then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1"
```
```   265       by (blast elim: oddE)
```
```   266     then have "a * b = (2 * r + 1) * (2 * s + 1)"
```
```   267       by simp
```
```   268     also have "\<dots> = 2 * (2 * r * s + r + s) + 1"
```
```   269       by (simp add: algebra_simps)
```
```   270     finally have "odd (a * b)"
```
```   271       by simp
```
```   272     with \<open>?P\<close> show False
```
```   273       by auto
```
```   274   qed
```
```   275 qed
```
```   276
```
```   277 lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))"
```
```   278 proof -
```
```   279   have "even (2 * numeral n)"
```
```   280     unfolding even_mult_iff by simp
```
```   281   then have "even (numeral n + numeral n)"
```
```   282     unfolding mult_2 .
```
```   283   then show ?thesis
```
```   284     unfolding numeral.simps .
```
```   285 qed
```
```   286
```
```   287 lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))"
```
```   288 proof
```
```   289   assume "even (numeral (num.Bit1 n))"
```
```   290   then have "even (numeral n + numeral n + 1)"
```
```   291     unfolding numeral.simps .
```
```   292   then have "even (2 * numeral n + 1)"
```
```   293     unfolding mult_2 .
```
```   294   then have "2 dvd numeral n * 2 + 1"
```
```   295     by (simp add: ac_simps)
```
```   296   then have "2 dvd 1"
```
```   297     using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp
```
```   298   then show False by simp
```
```   299 qed
```
```   300
```
```   301 lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
```
```   302   by (induct n) auto
```
```   303
```
```   304 lemma even_succ_div_two [simp]:
```
```   305   "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
```
```   306   by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
```
```   307
```
```   308 lemma odd_succ_div_two [simp]:
```
```   309   "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
```
```   310   by (auto elim!: oddE simp add: add.assoc)
```
```   311
```
```   312 lemma even_two_times_div_two:
```
```   313   "even a \<Longrightarrow> 2 * (a div 2) = a"
```
```   314   by (fact dvd_mult_div_cancel)
```
```   315
```
```   316 lemma odd_two_times_div_two_succ [simp]:
```
```   317   "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
```
```   318   using mult_div_mod_eq [of 2 a]
```
```   319   by (simp add: even_iff_mod_2_eq_zero)
```
```   320
```
```   321 end
```
```   322
```
```   323 class ring_parity = ring + semiring_parity
```
```   324 begin
```
```   325
```
```   326 subclass comm_ring_1 ..
```
```   327
```
```   328 lemma even_minus [simp]:
```
```   329   "even (- a) \<longleftrightarrow> even a"
```
```   330   by (fact dvd_minus_iff)
```
```   331
```
```   332 lemma even_diff [simp]:
```
```   333   "even (a - b) \<longleftrightarrow> even (a + b)"
```
```   334   using even_add [of a "- b"] by simp
```
```   335
```
```   336 end
```
```   337
```
```   338
```
```   339 subsection \<open>Instance for @{typ nat}\<close>
```
```   340
```
```   341 instance nat :: semiring_parity
```
```   342   by standard (simp_all add: dvd_eq_mod_eq_0)
```
```   343
```
```   344 lemma even_Suc_Suc_iff [simp]:
```
```   345   "even (Suc (Suc n)) \<longleftrightarrow> even n"
```
```   346   using dvd_add_triv_right_iff [of 2 n] by simp
```
```   347
```
```   348 lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n"
```
```   349   using even_plus_one_iff [of n] by simp
```
```   350
```
```   351 lemma even_diff_nat [simp]:
```
```   352   "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat
```
```   353 proof (cases "n \<le> m")
```
```   354   case True
```
```   355   then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
```
```   356   moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
```
```   357   ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
```
```   358   then show ?thesis by auto
```
```   359 next
```
```   360   case False
```
```   361   then show ?thesis by simp
```
```   362 qed
```
```   363
```
```   364 lemma odd_pos:
```
```   365   "odd n \<Longrightarrow> 0 < n" for n :: nat
```
```   366   by (auto elim: oddE)
```
```   367
```
```   368 lemma Suc_double_not_eq_double:
```
```   369   "Suc (2 * m) \<noteq> 2 * n"
```
```   370 proof
```
```   371   assume "Suc (2 * m) = 2 * n"
```
```   372   moreover have "odd (Suc (2 * m))" and "even (2 * n)"
```
```   373     by simp_all
```
```   374   ultimately show False by simp
```
```   375 qed
```
```   376
```
```   377 lemma double_not_eq_Suc_double:
```
```   378   "2 * m \<noteq> Suc (2 * n)"
```
```   379   using Suc_double_not_eq_double [of n m] by simp
```
```   380
```
```   381 lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
```
```   382   by (auto elim: oddE)
```
```   383
```
```   384 lemma even_Suc_div_two [simp]:
```
```   385   "even n \<Longrightarrow> Suc n div 2 = n div 2"
```
```   386   using even_succ_div_two [of n] by simp
```
```   387
```
```   388 lemma odd_Suc_div_two [simp]:
```
```   389   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
```
```   390   using odd_succ_div_two [of n] by simp
```
```   391
```
```   392 lemma odd_two_times_div_two_nat [simp]:
```
```   393   assumes "odd n"
```
```   394   shows "2 * (n div 2) = n - (1 :: nat)"
```
```   395 proof -
```
```   396   from assms have "2 * (n div 2) + 1 = n"
```
```   397     by (rule odd_two_times_div_two_succ)
```
```   398   then have "Suc (2 * (n div 2)) - 1 = n - 1"
```
```   399     by simp
```
```   400   then show ?thesis
```
```   401     by simp
```
```   402 qed
```
```   403
```
```   404 lemma parity_induct [case_names zero even odd]:
```
```   405   assumes zero: "P 0"
```
```   406   assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
```
```   407   assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
```
```   408   shows "P n"
```
```   409 proof (induct n rule: less_induct)
```
```   410   case (less n)
```
```   411   show "P n"
```
```   412   proof (cases "n = 0")
```
```   413     case True with zero show ?thesis by simp
```
```   414   next
```
```   415     case False
```
```   416     with less have hyp: "P (n div 2)" by simp
```
```   417     show ?thesis
```
```   418     proof (cases "even n")
```
```   419       case True
```
```   420       with hyp even [of "n div 2"] show ?thesis
```
```   421         by simp
```
```   422     next
```
```   423       case False
```
```   424       with hyp odd [of "n div 2"] show ?thesis
```
```   425         by simp
```
```   426     qed
```
```   427   qed
```
```   428 qed
```
```   429
```
```   430
```
```   431 subsection \<open>Parity and powers\<close>
```
```   432
```
```   433 context ring_1
```
```   434 begin
```
```   435
```
```   436 lemma power_minus_even [simp]: "even n \<Longrightarrow> (- a) ^ n = a ^ n"
```
```   437   by (auto elim: evenE)
```
```   438
```
```   439 lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
```
```   440   by (auto elim: oddE)
```
```   441
```
```   442 lemma uminus_power_if:
```
```   443   "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
```
```   444   by auto
```
```   445
```
```   446 lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
```
```   447   by simp
```
```   448
```
```   449 lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
```
```   450   by simp
```
```   451
```
```   452 lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)"
```
```   453   by (cases "even (n + k)") auto
```
```   454
```
```   455 end
```
```   456
```
```   457 context linordered_idom
```
```   458 begin
```
```   459
```
```   460 lemma zero_le_even_power: "even n \<Longrightarrow> 0 \<le> a ^ n"
```
```   461   by (auto elim: evenE)
```
```   462
```
```   463 lemma zero_le_odd_power: "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
```
```   464   by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
```
```   465
```
```   466 lemma zero_le_power_eq: "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
```
```   467   by (auto simp add: zero_le_even_power zero_le_odd_power)
```
```   468
```
```   469 lemma zero_less_power_eq: "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
```
```   470 proof -
```
```   471   have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
```
```   472     unfolding power_eq_0_iff [of a n, symmetric] by blast
```
```   473   show ?thesis
```
```   474     unfolding less_le zero_le_power_eq by auto
```
```   475 qed
```
```   476
```
```   477 lemma power_less_zero_eq [simp]: "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
```
```   478   unfolding not_le [symmetric] zero_le_power_eq by auto
```
```   479
```
```   480 lemma power_le_zero_eq: "a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)"
```
```   481   unfolding not_less [symmetric] zero_less_power_eq by auto
```
```   482
```
```   483 lemma power_even_abs: "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n"
```
```   484   using power_abs [of a n] by (simp add: zero_le_even_power)
```
```   485
```
```   486 lemma power_mono_even:
```
```   487   assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>"
```
```   488   shows "a ^ n \<le> b ^ n"
```
```   489 proof -
```
```   490   have "0 \<le> \<bar>a\<bar>" by auto
```
```   491   with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close> have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n"
```
```   492     by (rule power_mono)
```
```   493   with \<open>even n\<close> show ?thesis
```
```   494     by (simp add: power_even_abs)
```
```   495 qed
```
```   496
```
```   497 lemma power_mono_odd:
```
```   498   assumes "odd n" and "a \<le> b"
```
```   499   shows "a ^ n \<le> b ^ n"
```
```   500 proof (cases "b < 0")
```
```   501   case True
```
```   502   with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto
```
```   503   then have "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono)
```
```   504   with \<open>odd n\<close> show ?thesis by simp
```
```   505 next
```
```   506   case False
```
```   507   then have "0 \<le> b" by auto
```
```   508   show ?thesis
```
```   509   proof (cases "a < 0")
```
```   510     case True
```
```   511     then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto
```
```   512     then have "a ^ n \<le> 0" unfolding power_le_zero_eq using \<open>odd n\<close> by auto
```
```   513     moreover from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto
```
```   514     ultimately show ?thesis by auto
```
```   515   next
```
```   516     case False
```
```   517     then have "0 \<le> a" by auto
```
```   518     with \<open>a \<le> b\<close> show ?thesis
```
```   519       using power_mono by auto
```
```   520   qed
```
```   521 qed
```
```   522
```
```   523 text \<open>Simplify, when the exponent is a numeral\<close>
```
```   524
```
```   525 lemma zero_le_power_eq_numeral [simp]:
```
```   526   "0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a"
```
```   527   by (fact zero_le_power_eq)
```
```   528
```
```   529 lemma zero_less_power_eq_numeral [simp]:
```
```   530   "0 < a ^ numeral w \<longleftrightarrow>
```
```   531     numeral w = (0 :: nat) \<or>
```
```   532     even (numeral w :: nat) \<and> a \<noteq> 0 \<or>
```
```   533     odd (numeral w :: nat) \<and> 0 < a"
```
```   534   by (fact zero_less_power_eq)
```
```   535
```
```   536 lemma power_le_zero_eq_numeral [simp]:
```
```   537   "a ^ numeral w \<le> 0 \<longleftrightarrow>
```
```   538     (0 :: nat) < numeral w \<and>
```
```   539     (odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)"
```
```   540   by (fact power_le_zero_eq)
```
```   541
```
```   542 lemma power_less_zero_eq_numeral [simp]:
```
```   543   "a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0"
```
```   544   by (fact power_less_zero_eq)
```
```   545
```
```   546 lemma power_even_abs_numeral [simp]:
```
```   547   "even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w"
```
```   548   by (fact power_even_abs)
```
```   549
```
```   550 end
```
```   551
```
```   552
```
```   553 subsection \<open>Instance for @{typ int}\<close>
```
```   554
```
```   555 instance int :: ring_parity
```
```   556   by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
```
```   557
```
```   558 lemma even_diff_iff [simp]:
```
```   559   "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
```
```   560   using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
```
```   561
```
```   562 lemma even_abs_add_iff [simp]:
```
```   563   "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
```
```   564   by (cases "k \<ge> 0") (simp_all add: ac_simps)
```
```   565
```
```   566 lemma even_add_abs_iff [simp]:
```
```   567   "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
```
```   568   using even_abs_add_iff [of l k] by (simp add: ac_simps)
```
```   569
```
```   570 lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
```
```   571   by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
```
```   572
```
```   573 end
```