src/HOL/Parity.thy
 author haftmann Sun Oct 08 22:28:21 2017 +0200 (21 months ago) changeset 66808 1907167b6038 parent 66582 2b49d4888cb8 child 66815 93c6632ddf44 permissions -rw-r--r--
elementary definition of division on natural numbers
 wenzelm@41959 ` 1` ```(* Title: HOL/Parity.thy ``` wenzelm@41959 ` 2` ``` Author: Jeremy Avigad ``` wenzelm@41959 ` 3` ``` Author: Jacques D. Fleuriot ``` wenzelm@21256 ` 4` ```*) ``` wenzelm@21256 ` 5` wenzelm@60758 ` 6` ```section \Parity in rings and semirings\ ``` wenzelm@21256 ` 7` wenzelm@21256 ` 8` ```theory Parity ``` haftmann@64785 ` 9` ``` imports Nat_Transfer Euclidean_Division ``` wenzelm@21256 ` 10` ```begin ``` wenzelm@21256 ` 11` wenzelm@61799 ` 12` ```subsection \Ring structures with parity and \even\/\odd\ predicates\ ``` haftmann@58678 ` 13` lp15@60562 ` 14` ```class semiring_parity = comm_semiring_1_cancel + numeral + ``` haftmann@58787 ` 15` ``` assumes odd_one [simp]: "\ 2 dvd 1" ``` haftmann@58787 ` 16` ``` assumes odd_even_add: "\ 2 dvd a \ \ 2 dvd b \ 2 dvd a + b" ``` haftmann@58787 ` 17` ``` assumes even_multD: "2 dvd a * b \ 2 dvd a \ 2 dvd b" ``` haftmann@58787 ` 18` ``` assumes odd_ex_decrement: "\ 2 dvd a \ \b. a = b + 1" ``` haftmann@54227 ` 19` ```begin ``` wenzelm@21256 ` 20` haftmann@59816 ` 21` ```subclass semiring_numeral .. ``` haftmann@59816 ` 22` haftmann@58740 ` 23` ```abbreviation even :: "'a \ bool" ``` wenzelm@63654 ` 24` ``` where "even a \ 2 dvd a" ``` haftmann@54228 ` 25` haftmann@58678 ` 26` ```abbreviation odd :: "'a \ bool" ``` wenzelm@63654 ` 27` ``` where "odd a \ \ 2 dvd a" ``` haftmann@58678 ` 28` wenzelm@63654 ` 29` ```lemma even_zero [simp]: "even 0" ``` haftmann@58787 ` 30` ``` by (fact dvd_0_right) ``` haftmann@58787 ` 31` wenzelm@63654 ` 32` ```lemma even_plus_one_iff [simp]: "even (a + 1) \ odd a" ``` haftmann@58787 ` 33` ``` by (auto simp add: dvd_add_right_iff intro: odd_even_add) ``` haftmann@58787 ` 34` haftmann@58690 ` 35` ```lemma evenE [elim?]: ``` haftmann@58690 ` 36` ``` assumes "even a" ``` haftmann@58690 ` 37` ``` obtains b where "a = 2 * b" ``` haftmann@58740 ` 38` ``` using assms by (rule dvdE) ``` haftmann@58690 ` 39` haftmann@58681 ` 40` ```lemma oddE [elim?]: ``` haftmann@58680 ` 41` ``` assumes "odd a" ``` haftmann@58680 ` 42` ``` obtains b where "a = 2 * b + 1" ``` haftmann@58787 ` 43` ```proof - ``` haftmann@58787 ` 44` ``` from assms obtain b where *: "a = b + 1" ``` haftmann@58787 ` 45` ``` by (blast dest: odd_ex_decrement) ``` haftmann@58787 ` 46` ``` with assms have "even (b + 2)" by simp ``` haftmann@58787 ` 47` ``` then have "even b" by simp ``` haftmann@58787 ` 48` ``` then obtain c where "b = 2 * c" .. ``` haftmann@58787 ` 49` ``` with * have "a = 2 * c + 1" by simp ``` haftmann@58787 ` 50` ``` with that show thesis . ``` haftmann@58787 ` 51` ```qed ``` wenzelm@63654 ` 52` wenzelm@63654 ` 53` ```lemma even_times_iff [simp]: "even (a * b) \ even a \ even b" ``` haftmann@58787 ` 54` ``` by (auto dest: even_multD) ``` haftmann@58678 ` 55` wenzelm@63654 ` 56` ```lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))" ``` haftmann@58678 ` 57` ```proof - ``` haftmann@58678 ` 58` ``` have "even (2 * numeral n)" ``` haftmann@58740 ` 59` ``` unfolding even_times_iff by simp ``` haftmann@58678 ` 60` ``` then have "even (numeral n + numeral n)" ``` haftmann@58678 ` 61` ``` unfolding mult_2 . ``` haftmann@58678 ` 62` ``` then show ?thesis ``` haftmann@58678 ` 63` ``` unfolding numeral.simps . ``` haftmann@58678 ` 64` ```qed ``` haftmann@58678 ` 65` wenzelm@63654 ` 66` ```lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))" ``` haftmann@58678 ` 67` ```proof ``` haftmann@58678 ` 68` ``` assume "even (numeral (num.Bit1 n))" ``` haftmann@58678 ` 69` ``` then have "even (numeral n + numeral n + 1)" ``` haftmann@58678 ` 70` ``` unfolding numeral.simps . ``` haftmann@58678 ` 71` ``` then have "even (2 * numeral n + 1)" ``` haftmann@58678 ` 72` ``` unfolding mult_2 . ``` haftmann@58678 ` 73` ``` then have "2 dvd numeral n * 2 + 1" ``` haftmann@58740 ` 74` ``` by (simp add: ac_simps) ``` wenzelm@63654 ` 75` ``` then have "2 dvd 1" ``` wenzelm@63654 ` 76` ``` using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp ``` haftmann@58678 ` 77` ``` then show False by simp ``` haftmann@58678 ` 78` ```qed ``` haftmann@58678 ` 79` wenzelm@63654 ` 80` ```lemma even_add [simp]: "even (a + b) \ (even a \ even b)" ``` haftmann@58787 ` 81` ``` by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add) ``` haftmann@58680 ` 82` wenzelm@63654 ` 83` ```lemma odd_add [simp]: "odd (a + b) \ (\ (odd a \ odd b))" ``` haftmann@58680 ` 84` ``` by simp ``` haftmann@58680 ` 85` wenzelm@63654 ` 86` ```lemma even_power [simp]: "even (a ^ n) \ even a \ n > 0" ``` haftmann@58680 ` 87` ``` by (induct n) auto ``` haftmann@58680 ` 88` haftmann@58678 ` 89` ```end ``` haftmann@58678 ` 90` haftmann@59816 ` 91` ```class ring_parity = ring + semiring_parity ``` haftmann@58679 ` 92` ```begin ``` haftmann@58679 ` 93` haftmann@59816 ` 94` ```subclass comm_ring_1 .. ``` haftmann@59816 ` 95` wenzelm@63654 ` 96` ```lemma even_minus [simp]: "even (- a) \ even a" ``` haftmann@58740 ` 97` ``` by (fact dvd_minus_iff) ``` haftmann@58679 ` 98` wenzelm@63654 ` 99` ```lemma even_diff [simp]: "even (a - b) \ even (a + b)" ``` haftmann@58680 ` 100` ``` using even_add [of a "- b"] by simp ``` haftmann@58680 ` 101` haftmann@58679 ` 102` ```end ``` haftmann@58679 ` 103` haftmann@66808 ` 104` ```class unique_euclidean_semiring_parity = unique_euclidean_semiring + ``` haftmann@66808 ` 105` ``` assumes parity: "a mod 2 = 0 \ a mod 2 = 1" ``` haftmann@66808 ` 106` ``` assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1" ``` haftmann@66808 ` 107` ``` assumes zero_not_eq_two: "0 \ 2" ``` haftmann@66808 ` 108` ```begin ``` haftmann@66808 ` 109` haftmann@66808 ` 110` ```lemma parity_cases [case_names even odd]: ``` haftmann@66808 ` 111` ``` assumes "a mod 2 = 0 \ P" ``` haftmann@66808 ` 112` ``` assumes "a mod 2 = 1 \ P" ``` haftmann@66808 ` 113` ``` shows P ``` haftmann@66808 ` 114` ``` using assms parity by blast ``` haftmann@66808 ` 115` haftmann@66808 ` 116` ```lemma one_div_two_eq_zero [simp]: ``` haftmann@66808 ` 117` ``` "1 div 2 = 0" ``` haftmann@66808 ` 118` ```proof (cases "2 = 0") ``` haftmann@66808 ` 119` ``` case True then show ?thesis by simp ``` haftmann@66808 ` 120` ```next ``` haftmann@66808 ` 121` ``` case False ``` haftmann@66808 ` 122` ``` from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" . ``` haftmann@66808 ` 123` ``` with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp ``` haftmann@66808 ` 124` ``` then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff) ``` haftmann@66808 ` 125` ``` then have "1 div 2 = 0 \ 2 = 0" by simp ``` haftmann@66808 ` 126` ``` with False show ?thesis by auto ``` haftmann@66808 ` 127` ```qed ``` haftmann@66808 ` 128` haftmann@66808 ` 129` ```lemma not_mod_2_eq_0_eq_1 [simp]: ``` haftmann@66808 ` 130` ``` "a mod 2 \ 0 \ a mod 2 = 1" ``` haftmann@66808 ` 131` ``` by (cases a rule: parity_cases) simp_all ``` haftmann@66808 ` 132` haftmann@66808 ` 133` ```lemma not_mod_2_eq_1_eq_0 [simp]: ``` haftmann@66808 ` 134` ``` "a mod 2 \ 1 \ a mod 2 = 0" ``` haftmann@66808 ` 135` ``` by (cases a rule: parity_cases) simp_all ``` haftmann@66808 ` 136` haftmann@66808 ` 137` ```subclass semiring_parity ``` haftmann@66808 ` 138` ```proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1) ``` haftmann@66808 ` 139` ``` show "1 mod 2 = 1" ``` haftmann@66808 ` 140` ``` by (fact one_mod_two_eq_one) ``` haftmann@66808 ` 141` ```next ``` haftmann@66808 ` 142` ``` fix a b ``` haftmann@66808 ` 143` ``` assume "a mod 2 = 1" ``` haftmann@66808 ` 144` ``` moreover assume "b mod 2 = 1" ``` haftmann@66808 ` 145` ``` ultimately show "(a + b) mod 2 = 0" ``` haftmann@66808 ` 146` ``` using mod_add_eq [of a 2 b] by simp ``` haftmann@66808 ` 147` ```next ``` haftmann@66808 ` 148` ``` fix a b ``` haftmann@66808 ` 149` ``` assume "(a * b) mod 2 = 0" ``` haftmann@66808 ` 150` ``` then have "(a mod 2) * (b mod 2) mod 2 = 0" ``` haftmann@66808 ` 151` ``` by (simp add: mod_mult_eq) ``` haftmann@66808 ` 152` ``` then have "(a mod 2) * (b mod 2) = 0" ``` haftmann@66808 ` 153` ``` by (cases "a mod 2 = 0") simp_all ``` haftmann@66808 ` 154` ``` then show "a mod 2 = 0 \ b mod 2 = 0" ``` haftmann@66808 ` 155` ``` by (rule divisors_zero) ``` haftmann@66808 ` 156` ```next ``` haftmann@66808 ` 157` ``` fix a ``` haftmann@66808 ` 158` ``` assume "a mod 2 = 1" ``` haftmann@66808 ` 159` ``` then have "a = a div 2 * 2 + 1" ``` haftmann@66808 ` 160` ``` using div_mult_mod_eq [of a 2] by simp ``` haftmann@66808 ` 161` ``` then show "\b. a = b + 1" .. ``` haftmann@66808 ` 162` ```qed ``` haftmann@66808 ` 163` haftmann@66808 ` 164` ```lemma even_iff_mod_2_eq_zero: ``` haftmann@66808 ` 165` ``` "even a \ a mod 2 = 0" ``` haftmann@66808 ` 166` ``` by (fact dvd_eq_mod_eq_0) ``` haftmann@66808 ` 167` haftmann@66808 ` 168` ```lemma odd_iff_mod_2_eq_one: ``` haftmann@66808 ` 169` ``` "odd a \ a mod 2 = 1" ``` haftmann@66808 ` 170` ``` by (simp add: even_iff_mod_2_eq_zero) ``` haftmann@66808 ` 171` haftmann@66808 ` 172` ```lemma even_succ_div_two [simp]: ``` haftmann@66808 ` 173` ``` "even a \ (a + 1) div 2 = a div 2" ``` haftmann@66808 ` 174` ``` by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero) ``` haftmann@66808 ` 175` haftmann@66808 ` 176` ```lemma odd_succ_div_two [simp]: ``` haftmann@66808 ` 177` ``` "odd a \ (a + 1) div 2 = a div 2 + 1" ``` haftmann@66808 ` 178` ``` by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc) ``` haftmann@66808 ` 179` haftmann@66808 ` 180` ```lemma even_two_times_div_two: ``` haftmann@66808 ` 181` ``` "even a \ 2 * (a div 2) = a" ``` haftmann@66808 ` 182` ``` by (fact dvd_mult_div_cancel) ``` haftmann@66808 ` 183` haftmann@66808 ` 184` ```lemma odd_two_times_div_two_succ [simp]: ``` haftmann@66808 ` 185` ``` "odd a \ 2 * (a div 2) + 1 = a" ``` haftmann@66808 ` 186` ``` using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero) ``` haftmann@66808 ` 187` ``` ``` haftmann@66808 ` 188` ```end ``` haftmann@66808 ` 189` haftmann@58710 ` 190` wenzelm@60758 ` 191` ```subsection \Instances for @{typ nat} and @{typ int}\ ``` haftmann@58787 ` 192` wenzelm@63654 ` 193` ```lemma even_Suc_Suc_iff [simp]: "2 dvd Suc (Suc n) \ 2 dvd n" ``` haftmann@58787 ` 194` ``` using dvd_add_triv_right_iff [of 2 n] by simp ``` haftmann@58687 ` 195` wenzelm@63654 ` 196` ```lemma even_Suc [simp]: "2 dvd Suc n \ \ 2 dvd n" ``` haftmann@58787 ` 197` ``` by (induct n) auto ``` haftmann@58787 ` 198` wenzelm@63654 ` 199` ```lemma even_diff_nat [simp]: "2 dvd (m - n) \ m < n \ 2 dvd (m + n)" ``` wenzelm@63654 ` 200` ``` for m n :: nat ``` haftmann@58787 ` 201` ```proof (cases "n \ m") ``` haftmann@58787 ` 202` ``` case True ``` haftmann@58787 ` 203` ``` then have "m - n + n * 2 = m + n" by (simp add: mult_2_right) ``` haftmann@60343 ` 204` ``` moreover have "2 dvd (m - n) \ 2 dvd (m - n + n * 2)" by simp ``` haftmann@60343 ` 205` ``` ultimately have "2 dvd (m - n) \ 2 dvd (m + n)" by (simp only:) ``` haftmann@58787 ` 206` ``` then show ?thesis by auto ``` haftmann@58787 ` 207` ```next ``` haftmann@58787 ` 208` ``` case False ``` haftmann@58787 ` 209` ``` then show ?thesis by simp ``` wenzelm@63654 ` 210` ```qed ``` wenzelm@63654 ` 211` haftmann@58787 ` 212` ```instance nat :: semiring_parity ``` haftmann@58787 ` 213` ```proof ``` haftmann@60343 ` 214` ``` show "\ 2 dvd (1 :: nat)" ``` haftmann@58787 ` 215` ``` by (rule notI, erule dvdE) simp ``` haftmann@58787 ` 216` ```next ``` haftmann@58787 ` 217` ``` fix m n :: nat ``` haftmann@60343 ` 218` ``` assume "\ 2 dvd m" ``` haftmann@60343 ` 219` ``` moreover assume "\ 2 dvd n" ``` haftmann@60343 ` 220` ``` ultimately have *: "2 dvd Suc m \ 2 dvd Suc n" ``` haftmann@58787 ` 221` ``` by simp ``` haftmann@60343 ` 222` ``` then have "2 dvd (Suc m + Suc n)" ``` haftmann@58787 ` 223` ``` by (blast intro: dvd_add) ``` haftmann@58787 ` 224` ``` also have "Suc m + Suc n = m + n + 2" ``` haftmann@58787 ` 225` ``` by simp ``` haftmann@60343 ` 226` ``` finally show "2 dvd (m + n)" ``` haftmann@58787 ` 227` ``` using dvd_add_triv_right_iff [of 2 "m + n"] by simp ``` haftmann@58787 ` 228` ```next ``` haftmann@58787 ` 229` ``` fix m n :: nat ``` haftmann@60343 ` 230` ``` assume *: "2 dvd (m * n)" ``` haftmann@60343 ` 231` ``` show "2 dvd m \ 2 dvd n" ``` haftmann@58787 ` 232` ``` proof (rule disjCI) ``` haftmann@60343 ` 233` ``` assume "\ 2 dvd n" ``` haftmann@60343 ` 234` ``` then have "2 dvd (Suc n)" by simp ``` haftmann@58787 ` 235` ``` then obtain r where "Suc n = 2 * r" .. ``` haftmann@58787 ` 236` ``` moreover from * obtain s where "m * n = 2 * s" .. ``` haftmann@58787 ` 237` ``` then have "2 * s + m = m * Suc n" by simp ``` wenzelm@63654 ` 238` ``` ultimately have " 2 * s + m = 2 * (m * r)" ``` wenzelm@63654 ` 239` ``` by (simp add: algebra_simps) ``` haftmann@58787 ` 240` ``` then have "m = 2 * (m * r - s)" by simp ``` haftmann@60343 ` 241` ``` then show "2 dvd m" .. ``` haftmann@58787 ` 242` ``` qed ``` haftmann@58787 ` 243` ```next ``` haftmann@58787 ` 244` ``` fix n :: nat ``` haftmann@60343 ` 245` ``` assume "\ 2 dvd n" ``` haftmann@58787 ` 246` ``` then show "\m. n = m + 1" ``` haftmann@58787 ` 247` ``` by (cases n) simp_all ``` haftmann@58787 ` 248` ```qed ``` haftmann@58687 ` 249` wenzelm@63654 ` 250` ```lemma odd_pos: "odd n \ 0 < n" ``` wenzelm@63654 ` 251` ``` for n :: nat ``` haftmann@58690 ` 252` ``` by (auto elim: oddE) ``` haftmann@60343 ` 253` wenzelm@63654 ` 254` ```lemma Suc_double_not_eq_double: "Suc (2 * m) \ 2 * n" ``` wenzelm@63654 ` 255` ``` for m n :: nat ``` haftmann@62597 ` 256` ```proof ``` haftmann@62597 ` 257` ``` assume "Suc (2 * m) = 2 * n" ``` haftmann@62597 ` 258` ``` moreover have "odd (Suc (2 * m))" and "even (2 * n)" ``` haftmann@62597 ` 259` ``` by simp_all ``` haftmann@62597 ` 260` ``` ultimately show False by simp ``` haftmann@62597 ` 261` ```qed ``` haftmann@62597 ` 262` wenzelm@63654 ` 263` ```lemma double_not_eq_Suc_double: "2 * m \ Suc (2 * n)" ``` wenzelm@63654 ` 264` ``` for m n :: nat ``` haftmann@62597 ` 265` ``` using Suc_double_not_eq_double [of n m] by simp ``` haftmann@62597 ` 266` wenzelm@63654 ` 267` ```lemma even_diff_iff [simp]: "2 dvd (k - l) \ 2 dvd (k + l)" ``` wenzelm@63654 ` 268` ``` for k l :: int ``` haftmann@60343 ` 269` ``` using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right) ``` haftmann@60343 ` 270` wenzelm@63654 ` 271` ```lemma even_abs_add_iff [simp]: "2 dvd (\k\ + l) \ 2 dvd (k + l)" ``` wenzelm@63654 ` 272` ``` for k l :: int ``` haftmann@60343 ` 273` ``` by (cases "k \ 0") (simp_all add: ac_simps) ``` haftmann@60343 ` 274` wenzelm@63654 ` 275` ```lemma even_add_abs_iff [simp]: "2 dvd (k + \l\) \ 2 dvd (k + l)" ``` wenzelm@63654 ` 276` ``` for k l :: int ``` haftmann@60343 ` 277` ``` using even_abs_add_iff [of l k] by (simp add: ac_simps) ``` haftmann@60343 ` 278` haftmann@58787 ` 279` ```instance int :: ring_parity ``` haftmann@58787 ` 280` ```proof ``` wenzelm@63654 ` 281` ``` show "\ 2 dvd (1 :: int)" ``` wenzelm@63654 ` 282` ``` by (simp add: dvd_int_unfold_dvd_nat) ``` wenzelm@63654 ` 283` ```next ``` haftmann@58787 ` 284` ``` fix k l :: int ``` haftmann@60343 ` 285` ``` assume "\ 2 dvd k" ``` haftmann@60343 ` 286` ``` moreover assume "\ 2 dvd l" ``` wenzelm@63654 ` 287` ``` ultimately have "2 dvd (nat \k\ + nat \l\)" ``` haftmann@58787 ` 288` ``` by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add) ``` haftmann@60343 ` 289` ``` then have "2 dvd (\k\ + \l\)" ``` haftmann@58787 ` 290` ``` by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib) ``` haftmann@60343 ` 291` ``` then show "2 dvd (k + l)" ``` haftmann@58787 ` 292` ``` by simp ``` haftmann@58787 ` 293` ```next ``` haftmann@58787 ` 294` ``` fix k l :: int ``` haftmann@60343 ` 295` ``` assume "2 dvd (k * l)" ``` haftmann@60343 ` 296` ``` then show "2 dvd k \ 2 dvd l" ``` haftmann@58787 ` 297` ``` by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib) ``` haftmann@58787 ` 298` ```next ``` haftmann@58787 ` 299` ``` fix k :: int ``` haftmann@58787 ` 300` ``` have "k = (k - 1) + 1" by simp ``` haftmann@58787 ` 301` ``` then show "\l. k = l + 1" .. ``` haftmann@58787 ` 302` ```qed ``` haftmann@58680 ` 303` wenzelm@63654 ` 304` ```lemma even_int_iff [simp]: "even (int n) \ even n" ``` haftmann@58740 ` 305` ``` by (simp add: dvd_int_iff) ``` haftmann@33318 ` 306` wenzelm@63654 ` 307` ```lemma even_nat_iff: "0 \ k \ even (nat k) \ even k" ``` haftmann@58687 ` 308` ``` by (simp add: even_int_iff [symmetric]) ``` haftmann@58687 ` 309` haftmann@58687 ` 310` wenzelm@60758 ` 311` ```subsection \Parity and powers\ ``` haftmann@58689 ` 312` eberlm@61531 ` 313` ```context ring_1 ``` haftmann@58689 ` 314` ```begin ``` haftmann@58689 ` 315` wenzelm@63654 ` 316` ```lemma power_minus_even [simp]: "even n \ (- a) ^ n = a ^ n" ``` haftmann@58690 ` 317` ``` by (auto elim: evenE) ``` haftmann@58689 ` 318` wenzelm@63654 ` 319` ```lemma power_minus_odd [simp]: "odd n \ (- a) ^ n = - (a ^ n)" ``` haftmann@58690 ` 320` ``` by (auto elim: oddE) ``` haftmann@58690 ` 321` wenzelm@63654 ` 322` ```lemma neg_one_even_power [simp]: "even n \ (- 1) ^ n = 1" ``` haftmann@58690 ` 323` ``` by simp ``` haftmann@58689 ` 324` wenzelm@63654 ` 325` ```lemma neg_one_odd_power [simp]: "odd n \ (- 1) ^ n = - 1" ``` haftmann@58690 ` 326` ``` by simp ``` haftmann@58689 ` 327` bulwahn@66582 ` 328` ```lemma neg_one_power_add_eq_neg_one_power_diff: "k \ n \ (- 1) ^ (n + k) = (- 1) ^ (n - k)" ``` bulwahn@66582 ` 329` ``` by (cases "even (n + k)") auto ``` bulwahn@66582 ` 330` wenzelm@63654 ` 331` ```end ``` haftmann@58689 ` 332` haftmann@58689 ` 333` ```context linordered_idom ``` haftmann@58689 ` 334` ```begin ``` haftmann@58689 ` 335` wenzelm@63654 ` 336` ```lemma zero_le_even_power: "even n \ 0 \ a ^ n" ``` haftmann@58690 ` 337` ``` by (auto elim: evenE) ``` haftmann@58689 ` 338` wenzelm@63654 ` 339` ```lemma zero_le_odd_power: "odd n \ 0 \ a ^ n \ 0 \ a" ``` haftmann@58689 ` 340` ``` by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) ``` haftmann@58689 ` 341` wenzelm@63654 ` 342` ```lemma zero_le_power_eq: "0 \ a ^ n \ even n \ odd n \ 0 \ a" ``` haftmann@58787 ` 343` ``` by (auto simp add: zero_le_even_power zero_le_odd_power) ``` wenzelm@63654 ` 344` wenzelm@63654 ` 345` ```lemma zero_less_power_eq: "0 < a ^ n \ n = 0 \ even n \ a \ 0 \ odd n \ 0 < a" ``` haftmann@58689 ` 346` ```proof - ``` haftmann@58689 ` 347` ``` have [simp]: "0 = a ^ n \ a = 0 \ n > 0" ``` haftmann@58787 ` 348` ``` unfolding power_eq_0_iff [of a n, symmetric] by blast ``` haftmann@58689 ` 349` ``` show ?thesis ``` wenzelm@63654 ` 350` ``` unfolding less_le zero_le_power_eq by auto ``` haftmann@58689 ` 351` ```qed ``` haftmann@58689 ` 352` wenzelm@63654 ` 353` ```lemma power_less_zero_eq [simp]: "a ^ n < 0 \ odd n \ a < 0" ``` haftmann@58689 ` 354` ``` unfolding not_le [symmetric] zero_le_power_eq by auto ``` haftmann@58689 ` 355` wenzelm@63654 ` 356` ```lemma power_le_zero_eq: "a ^ n \ 0 \ n > 0 \ (odd n \ a \ 0 \ even n \ a = 0)" ``` wenzelm@63654 ` 357` ``` unfolding not_less [symmetric] zero_less_power_eq by auto ``` wenzelm@63654 ` 358` wenzelm@63654 ` 359` ```lemma power_even_abs: "even n \ \a\ ^ n = a ^ n" ``` haftmann@58689 ` 360` ``` using power_abs [of a n] by (simp add: zero_le_even_power) ``` haftmann@58689 ` 361` haftmann@58689 ` 362` ```lemma power_mono_even: ``` haftmann@58689 ` 363` ``` assumes "even n" and "\a\ \ \b\" ``` haftmann@58689 ` 364` ``` shows "a ^ n \ b ^ n" ``` haftmann@58689 ` 365` ```proof - ``` haftmann@58689 ` 366` ``` have "0 \ \a\" by auto ``` wenzelm@63654 ` 367` ``` with \\a\ \ \b\\ have "\a\ ^ n \ \b\ ^ n" ``` wenzelm@63654 ` 368` ``` by (rule power_mono) ``` wenzelm@63654 ` 369` ``` with \even n\ show ?thesis ``` wenzelm@63654 ` 370` ``` by (simp add: power_even_abs) ``` haftmann@58689 ` 371` ```qed ``` haftmann@58689 ` 372` haftmann@58689 ` 373` ```lemma power_mono_odd: ``` haftmann@58689 ` 374` ``` assumes "odd n" and "a \ b" ``` haftmann@58689 ` 375` ``` shows "a ^ n \ b ^ n" ``` haftmann@58689 ` 376` ```proof (cases "b < 0") ``` wenzelm@63654 ` 377` ``` case True ``` wenzelm@63654 ` 378` ``` with \a \ b\ have "- b \ - a" and "0 \ - b" by auto ``` wenzelm@63654 ` 379` ``` then have "(- b) ^ n \ (- a) ^ n" by (rule power_mono) ``` wenzelm@60758 ` 380` ``` with \odd n\ show ?thesis by simp ``` haftmann@58689 ` 381` ```next ``` wenzelm@63654 ` 382` ``` case False ``` wenzelm@63654 ` 383` ``` then have "0 \ b" by auto ``` haftmann@58689 ` 384` ``` show ?thesis ``` haftmann@58689 ` 385` ``` proof (cases "a < 0") ``` wenzelm@63654 ` 386` ``` case True ``` wenzelm@63654 ` 387` ``` then have "n \ 0" and "a \ 0" using \odd n\ [THEN odd_pos] by auto ``` wenzelm@60758 ` 388` ``` then have "a ^ n \ 0" unfolding power_le_zero_eq using \odd n\ by auto ``` wenzelm@63654 ` 389` ``` moreover from \0 \ b\ have "0 \ b ^ n" by auto ``` haftmann@58689 ` 390` ``` ultimately show ?thesis by auto ``` haftmann@58689 ` 391` ``` next ``` wenzelm@63654 ` 392` ``` case False ``` wenzelm@63654 ` 393` ``` then have "0 \ a" by auto ``` wenzelm@63654 ` 394` ``` with \a \ b\ show ?thesis ``` wenzelm@63654 ` 395` ``` using power_mono by auto ``` haftmann@58689 ` 396` ``` qed ``` haftmann@58689 ` 397` ```qed ``` hoelzl@62083 ` 398` hoelzl@62083 ` 399` ```lemma (in comm_ring_1) uminus_power_if: "(- x) ^ n = (if even n then x^n else - (x ^ n))" ``` hoelzl@62083 ` 400` ``` by auto ``` hoelzl@62083 ` 401` wenzelm@60758 ` 402` ```text \Simplify, when the exponent is a numeral\ ``` haftmann@58689 ` 403` haftmann@58689 ` 404` ```lemma zero_le_power_eq_numeral [simp]: ``` haftmann@58689 ` 405` ``` "0 \ a ^ numeral w \ even (numeral w :: nat) \ odd (numeral w :: nat) \ 0 \ a" ``` haftmann@58689 ` 406` ``` by (fact zero_le_power_eq) ``` haftmann@58689 ` 407` haftmann@58689 ` 408` ```lemma zero_less_power_eq_numeral [simp]: ``` wenzelm@63654 ` 409` ``` "0 < a ^ numeral w \ ``` wenzelm@63654 ` 410` ``` numeral w = (0 :: nat) \ ``` wenzelm@63654 ` 411` ``` even (numeral w :: nat) \ a \ 0 \ ``` wenzelm@63654 ` 412` ``` odd (numeral w :: nat) \ 0 < a" ``` haftmann@58689 ` 413` ``` by (fact zero_less_power_eq) ``` haftmann@58689 ` 414` haftmann@58689 ` 415` ```lemma power_le_zero_eq_numeral [simp]: ``` wenzelm@63654 ` 416` ``` "a ^ numeral w \ 0 \ ``` wenzelm@63654 ` 417` ``` (0 :: nat) < numeral w \ ``` wenzelm@63654 ` 418` ``` (odd (numeral w :: nat) \ a \ 0 \ even (numeral w :: nat) \ a = 0)" ``` haftmann@58689 ` 419` ``` by (fact power_le_zero_eq) ``` haftmann@58689 ` 420` haftmann@58689 ` 421` ```lemma power_less_zero_eq_numeral [simp]: ``` haftmann@58689 ` 422` ``` "a ^ numeral w < 0 \ odd (numeral w :: nat) \ a < 0" ``` haftmann@58689 ` 423` ``` by (fact power_less_zero_eq) ``` haftmann@58689 ` 424` haftmann@58689 ` 425` ```lemma power_even_abs_numeral [simp]: ``` haftmann@58689 ` 426` ``` "even (numeral w :: nat) \ \a\ ^ numeral w = a ^ numeral w" ``` haftmann@58689 ` 427` ``` by (fact power_even_abs) ``` haftmann@58689 ` 428` haftmann@58689 ` 429` ```end ``` haftmann@58689 ` 430` haftmann@58689 ` 431` wenzelm@63654 ` 432` ```subsubsection \Tool setup\ ``` haftmann@58687 ` 433` wenzelm@63654 ` 434` ```declare transfer_morphism_int_nat [transfer add return: even_int_iff] ``` wenzelm@21256 ` 435` haftmann@58770 ` 436` ```end ```