src/HOL/Parity.thy
 author wenzelm Tue Sep 26 20:54:40 2017 +0200 (22 months ago) changeset 66695 91500c024c7f parent 66582 2b49d4888cb8 child 66808 1907167b6038 permissions -rw-r--r--
tuned;
 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@58710 ` 104` wenzelm@60758 ` 105` ```subsection \Instances for @{typ nat} and @{typ int}\ ``` haftmann@58787 ` 106` wenzelm@63654 ` 107` ```lemma even_Suc_Suc_iff [simp]: "2 dvd Suc (Suc n) \ 2 dvd n" ``` haftmann@58787 ` 108` ``` using dvd_add_triv_right_iff [of 2 n] by simp ``` haftmann@58687 ` 109` wenzelm@63654 ` 110` ```lemma even_Suc [simp]: "2 dvd Suc n \ \ 2 dvd n" ``` haftmann@58787 ` 111` ``` by (induct n) auto ``` haftmann@58787 ` 112` wenzelm@63654 ` 113` ```lemma even_diff_nat [simp]: "2 dvd (m - n) \ m < n \ 2 dvd (m + n)" ``` wenzelm@63654 ` 114` ``` for m n :: nat ``` haftmann@58787 ` 115` ```proof (cases "n \ m") ``` haftmann@58787 ` 116` ``` case True ``` haftmann@58787 ` 117` ``` then have "m - n + n * 2 = m + n" by (simp add: mult_2_right) ``` haftmann@60343 ` 118` ``` moreover have "2 dvd (m - n) \ 2 dvd (m - n + n * 2)" by simp ``` haftmann@60343 ` 119` ``` ultimately have "2 dvd (m - n) \ 2 dvd (m + n)" by (simp only:) ``` haftmann@58787 ` 120` ``` then show ?thesis by auto ``` haftmann@58787 ` 121` ```next ``` haftmann@58787 ` 122` ``` case False ``` haftmann@58787 ` 123` ``` then show ?thesis by simp ``` wenzelm@63654 ` 124` ```qed ``` wenzelm@63654 ` 125` haftmann@58787 ` 126` ```instance nat :: semiring_parity ``` haftmann@58787 ` 127` ```proof ``` haftmann@60343 ` 128` ``` show "\ 2 dvd (1 :: nat)" ``` haftmann@58787 ` 129` ``` by (rule notI, erule dvdE) simp ``` haftmann@58787 ` 130` ```next ``` haftmann@58787 ` 131` ``` fix m n :: nat ``` haftmann@60343 ` 132` ``` assume "\ 2 dvd m" ``` haftmann@60343 ` 133` ``` moreover assume "\ 2 dvd n" ``` haftmann@60343 ` 134` ``` ultimately have *: "2 dvd Suc m \ 2 dvd Suc n" ``` haftmann@58787 ` 135` ``` by simp ``` haftmann@60343 ` 136` ``` then have "2 dvd (Suc m + Suc n)" ``` haftmann@58787 ` 137` ``` by (blast intro: dvd_add) ``` haftmann@58787 ` 138` ``` also have "Suc m + Suc n = m + n + 2" ``` haftmann@58787 ` 139` ``` by simp ``` haftmann@60343 ` 140` ``` finally show "2 dvd (m + n)" ``` haftmann@58787 ` 141` ``` using dvd_add_triv_right_iff [of 2 "m + n"] by simp ``` haftmann@58787 ` 142` ```next ``` haftmann@58787 ` 143` ``` fix m n :: nat ``` haftmann@60343 ` 144` ``` assume *: "2 dvd (m * n)" ``` haftmann@60343 ` 145` ``` show "2 dvd m \ 2 dvd n" ``` haftmann@58787 ` 146` ``` proof (rule disjCI) ``` haftmann@60343 ` 147` ``` assume "\ 2 dvd n" ``` haftmann@60343 ` 148` ``` then have "2 dvd (Suc n)" by simp ``` haftmann@58787 ` 149` ``` then obtain r where "Suc n = 2 * r" .. ``` haftmann@58787 ` 150` ``` moreover from * obtain s where "m * n = 2 * s" .. ``` haftmann@58787 ` 151` ``` then have "2 * s + m = m * Suc n" by simp ``` wenzelm@63654 ` 152` ``` ultimately have " 2 * s + m = 2 * (m * r)" ``` wenzelm@63654 ` 153` ``` by (simp add: algebra_simps) ``` haftmann@58787 ` 154` ``` then have "m = 2 * (m * r - s)" by simp ``` haftmann@60343 ` 155` ``` then show "2 dvd m" .. ``` haftmann@58787 ` 156` ``` qed ``` haftmann@58787 ` 157` ```next ``` haftmann@58787 ` 158` ``` fix n :: nat ``` haftmann@60343 ` 159` ``` assume "\ 2 dvd n" ``` haftmann@58787 ` 160` ``` then show "\m. n = m + 1" ``` haftmann@58787 ` 161` ``` by (cases n) simp_all ``` haftmann@58787 ` 162` ```qed ``` haftmann@58687 ` 163` wenzelm@63654 ` 164` ```lemma odd_pos: "odd n \ 0 < n" ``` wenzelm@63654 ` 165` ``` for n :: nat ``` haftmann@58690 ` 166` ``` by (auto elim: oddE) ``` haftmann@60343 ` 167` wenzelm@63654 ` 168` ```lemma Suc_double_not_eq_double: "Suc (2 * m) \ 2 * n" ``` wenzelm@63654 ` 169` ``` for m n :: nat ``` haftmann@62597 ` 170` ```proof ``` haftmann@62597 ` 171` ``` assume "Suc (2 * m) = 2 * n" ``` haftmann@62597 ` 172` ``` moreover have "odd (Suc (2 * m))" and "even (2 * n)" ``` haftmann@62597 ` 173` ``` by simp_all ``` haftmann@62597 ` 174` ``` ultimately show False by simp ``` haftmann@62597 ` 175` ```qed ``` haftmann@62597 ` 176` wenzelm@63654 ` 177` ```lemma double_not_eq_Suc_double: "2 * m \ Suc (2 * n)" ``` wenzelm@63654 ` 178` ``` for m n :: nat ``` haftmann@62597 ` 179` ``` using Suc_double_not_eq_double [of n m] by simp ``` haftmann@62597 ` 180` wenzelm@63654 ` 181` ```lemma even_diff_iff [simp]: "2 dvd (k - l) \ 2 dvd (k + l)" ``` wenzelm@63654 ` 182` ``` for k l :: int ``` haftmann@60343 ` 183` ``` using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right) ``` haftmann@60343 ` 184` wenzelm@63654 ` 185` ```lemma even_abs_add_iff [simp]: "2 dvd (\k\ + l) \ 2 dvd (k + l)" ``` wenzelm@63654 ` 186` ``` for k l :: int ``` haftmann@60343 ` 187` ``` by (cases "k \ 0") (simp_all add: ac_simps) ``` haftmann@60343 ` 188` wenzelm@63654 ` 189` ```lemma even_add_abs_iff [simp]: "2 dvd (k + \l\) \ 2 dvd (k + l)" ``` wenzelm@63654 ` 190` ``` for k l :: int ``` haftmann@60343 ` 191` ``` using even_abs_add_iff [of l k] by (simp add: ac_simps) ``` haftmann@60343 ` 192` wenzelm@63654 ` 193` ```lemma odd_Suc_minus_one [simp]: "odd n \ Suc (n - Suc 0) = n" ``` haftmann@60867 ` 194` ``` by (auto elim: oddE) ``` haftmann@60867 ` 195` haftmann@58787 ` 196` ```instance int :: ring_parity ``` haftmann@58787 ` 197` ```proof ``` wenzelm@63654 ` 198` ``` show "\ 2 dvd (1 :: int)" ``` wenzelm@63654 ` 199` ``` by (simp add: dvd_int_unfold_dvd_nat) ``` wenzelm@63654 ` 200` ```next ``` haftmann@58787 ` 201` ``` fix k l :: int ``` haftmann@60343 ` 202` ``` assume "\ 2 dvd k" ``` haftmann@60343 ` 203` ``` moreover assume "\ 2 dvd l" ``` wenzelm@63654 ` 204` ``` ultimately have "2 dvd (nat \k\ + nat \l\)" ``` haftmann@58787 ` 205` ``` by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add) ``` haftmann@60343 ` 206` ``` then have "2 dvd (\k\ + \l\)" ``` haftmann@58787 ` 207` ``` by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib) ``` haftmann@60343 ` 208` ``` then show "2 dvd (k + l)" ``` haftmann@58787 ` 209` ``` by simp ``` haftmann@58787 ` 210` ```next ``` haftmann@58787 ` 211` ``` fix k l :: int ``` haftmann@60343 ` 212` ``` assume "2 dvd (k * l)" ``` haftmann@60343 ` 213` ``` then show "2 dvd k \ 2 dvd l" ``` haftmann@58787 ` 214` ``` by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib) ``` haftmann@58787 ` 215` ```next ``` haftmann@58787 ` 216` ``` fix k :: int ``` haftmann@58787 ` 217` ``` have "k = (k - 1) + 1" by simp ``` haftmann@58787 ` 218` ``` then show "\l. k = l + 1" .. ``` haftmann@58787 ` 219` ```qed ``` haftmann@58680 ` 220` wenzelm@63654 ` 221` ```lemma even_int_iff [simp]: "even (int n) \ even n" ``` haftmann@58740 ` 222` ``` by (simp add: dvd_int_iff) ``` haftmann@33318 ` 223` wenzelm@63654 ` 224` ```lemma even_nat_iff: "0 \ k \ even (nat k) \ even k" ``` haftmann@58687 ` 225` ``` by (simp add: even_int_iff [symmetric]) ``` haftmann@58687 ` 226` haftmann@58687 ` 227` wenzelm@60758 ` 228` ```subsection \Parity and powers\ ``` haftmann@58689 ` 229` eberlm@61531 ` 230` ```context ring_1 ``` haftmann@58689 ` 231` ```begin ``` haftmann@58689 ` 232` wenzelm@63654 ` 233` ```lemma power_minus_even [simp]: "even n \ (- a) ^ n = a ^ n" ``` haftmann@58690 ` 234` ``` by (auto elim: evenE) ``` haftmann@58689 ` 235` wenzelm@63654 ` 236` ```lemma power_minus_odd [simp]: "odd n \ (- a) ^ n = - (a ^ n)" ``` haftmann@58690 ` 237` ``` by (auto elim: oddE) ``` haftmann@58690 ` 238` wenzelm@63654 ` 239` ```lemma neg_one_even_power [simp]: "even n \ (- 1) ^ n = 1" ``` haftmann@58690 ` 240` ``` by simp ``` haftmann@58689 ` 241` wenzelm@63654 ` 242` ```lemma neg_one_odd_power [simp]: "odd n \ (- 1) ^ n = - 1" ``` haftmann@58690 ` 243` ``` by simp ``` haftmann@58689 ` 244` bulwahn@66582 ` 245` ```lemma neg_one_power_add_eq_neg_one_power_diff: "k \ n \ (- 1) ^ (n + k) = (- 1) ^ (n - k)" ``` bulwahn@66582 ` 246` ``` by (cases "even (n + k)") auto ``` bulwahn@66582 ` 247` wenzelm@63654 ` 248` ```end ``` haftmann@58689 ` 249` haftmann@58689 ` 250` ```context linordered_idom ``` haftmann@58689 ` 251` ```begin ``` haftmann@58689 ` 252` wenzelm@63654 ` 253` ```lemma zero_le_even_power: "even n \ 0 \ a ^ n" ``` haftmann@58690 ` 254` ``` by (auto elim: evenE) ``` haftmann@58689 ` 255` wenzelm@63654 ` 256` ```lemma zero_le_odd_power: "odd n \ 0 \ a ^ n \ 0 \ a" ``` haftmann@58689 ` 257` ``` by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) ``` haftmann@58689 ` 258` wenzelm@63654 ` 259` ```lemma zero_le_power_eq: "0 \ a ^ n \ even n \ odd n \ 0 \ a" ``` haftmann@58787 ` 260` ``` by (auto simp add: zero_le_even_power zero_le_odd_power) ``` wenzelm@63654 ` 261` wenzelm@63654 ` 262` ```lemma zero_less_power_eq: "0 < a ^ n \ n = 0 \ even n \ a \ 0 \ odd n \ 0 < a" ``` haftmann@58689 ` 263` ```proof - ``` haftmann@58689 ` 264` ``` have [simp]: "0 = a ^ n \ a = 0 \ n > 0" ``` haftmann@58787 ` 265` ``` unfolding power_eq_0_iff [of a n, symmetric] by blast ``` haftmann@58689 ` 266` ``` show ?thesis ``` wenzelm@63654 ` 267` ``` unfolding less_le zero_le_power_eq by auto ``` haftmann@58689 ` 268` ```qed ``` haftmann@58689 ` 269` wenzelm@63654 ` 270` ```lemma power_less_zero_eq [simp]: "a ^ n < 0 \ odd n \ a < 0" ``` haftmann@58689 ` 271` ``` unfolding not_le [symmetric] zero_le_power_eq by auto ``` haftmann@58689 ` 272` wenzelm@63654 ` 273` ```lemma power_le_zero_eq: "a ^ n \ 0 \ n > 0 \ (odd n \ a \ 0 \ even n \ a = 0)" ``` wenzelm@63654 ` 274` ``` unfolding not_less [symmetric] zero_less_power_eq by auto ``` wenzelm@63654 ` 275` wenzelm@63654 ` 276` ```lemma power_even_abs: "even n \ \a\ ^ n = a ^ n" ``` haftmann@58689 ` 277` ``` using power_abs [of a n] by (simp add: zero_le_even_power) ``` haftmann@58689 ` 278` haftmann@58689 ` 279` ```lemma power_mono_even: ``` haftmann@58689 ` 280` ``` assumes "even n" and "\a\ \ \b\" ``` haftmann@58689 ` 281` ``` shows "a ^ n \ b ^ n" ``` haftmann@58689 ` 282` ```proof - ``` haftmann@58689 ` 283` ``` have "0 \ \a\" by auto ``` wenzelm@63654 ` 284` ``` with \\a\ \ \b\\ have "\a\ ^ n \ \b\ ^ n" ``` wenzelm@63654 ` 285` ``` by (rule power_mono) ``` wenzelm@63654 ` 286` ``` with \even n\ show ?thesis ``` wenzelm@63654 ` 287` ``` by (simp add: power_even_abs) ``` haftmann@58689 ` 288` ```qed ``` haftmann@58689 ` 289` haftmann@58689 ` 290` ```lemma power_mono_odd: ``` haftmann@58689 ` 291` ``` assumes "odd n" and "a \ b" ``` haftmann@58689 ` 292` ``` shows "a ^ n \ b ^ n" ``` haftmann@58689 ` 293` ```proof (cases "b < 0") ``` wenzelm@63654 ` 294` ``` case True ``` wenzelm@63654 ` 295` ``` with \a \ b\ have "- b \ - a" and "0 \ - b" by auto ``` wenzelm@63654 ` 296` ``` then have "(- b) ^ n \ (- a) ^ n" by (rule power_mono) ``` wenzelm@60758 ` 297` ``` with \odd n\ show ?thesis by simp ``` haftmann@58689 ` 298` ```next ``` wenzelm@63654 ` 299` ``` case False ``` wenzelm@63654 ` 300` ``` then have "0 \ b" by auto ``` haftmann@58689 ` 301` ``` show ?thesis ``` haftmann@58689 ` 302` ``` proof (cases "a < 0") ``` wenzelm@63654 ` 303` ``` case True ``` wenzelm@63654 ` 304` ``` then have "n \ 0" and "a \ 0" using \odd n\ [THEN odd_pos] by auto ``` wenzelm@60758 ` 305` ``` then have "a ^ n \ 0" unfolding power_le_zero_eq using \odd n\ by auto ``` wenzelm@63654 ` 306` ``` moreover from \0 \ b\ have "0 \ b ^ n" by auto ``` haftmann@58689 ` 307` ``` ultimately show ?thesis by auto ``` haftmann@58689 ` 308` ``` next ``` wenzelm@63654 ` 309` ``` case False ``` wenzelm@63654 ` 310` ``` then have "0 \ a" by auto ``` wenzelm@63654 ` 311` ``` with \a \ b\ show ?thesis ``` wenzelm@63654 ` 312` ``` using power_mono by auto ``` haftmann@58689 ` 313` ``` qed ``` haftmann@58689 ` 314` ```qed ``` hoelzl@62083 ` 315` hoelzl@62083 ` 316` ```lemma (in comm_ring_1) uminus_power_if: "(- x) ^ n = (if even n then x^n else - (x ^ n))" ``` hoelzl@62083 ` 317` ``` by auto ``` hoelzl@62083 ` 318` wenzelm@60758 ` 319` ```text \Simplify, when the exponent is a numeral\ ``` haftmann@58689 ` 320` haftmann@58689 ` 321` ```lemma zero_le_power_eq_numeral [simp]: ``` haftmann@58689 ` 322` ``` "0 \ a ^ numeral w \ even (numeral w :: nat) \ odd (numeral w :: nat) \ 0 \ a" ``` haftmann@58689 ` 323` ``` by (fact zero_le_power_eq) ``` haftmann@58689 ` 324` haftmann@58689 ` 325` ```lemma zero_less_power_eq_numeral [simp]: ``` wenzelm@63654 ` 326` ``` "0 < a ^ numeral w \ ``` wenzelm@63654 ` 327` ``` numeral w = (0 :: nat) \ ``` wenzelm@63654 ` 328` ``` even (numeral w :: nat) \ a \ 0 \ ``` wenzelm@63654 ` 329` ``` odd (numeral w :: nat) \ 0 < a" ``` haftmann@58689 ` 330` ``` by (fact zero_less_power_eq) ``` haftmann@58689 ` 331` haftmann@58689 ` 332` ```lemma power_le_zero_eq_numeral [simp]: ``` wenzelm@63654 ` 333` ``` "a ^ numeral w \ 0 \ ``` wenzelm@63654 ` 334` ``` (0 :: nat) < numeral w \ ``` wenzelm@63654 ` 335` ``` (odd (numeral w :: nat) \ a \ 0 \ even (numeral w :: nat) \ a = 0)" ``` haftmann@58689 ` 336` ``` by (fact power_le_zero_eq) ``` haftmann@58689 ` 337` haftmann@58689 ` 338` ```lemma power_less_zero_eq_numeral [simp]: ``` haftmann@58689 ` 339` ``` "a ^ numeral w < 0 \ odd (numeral w :: nat) \ a < 0" ``` haftmann@58689 ` 340` ``` by (fact power_less_zero_eq) ``` haftmann@58689 ` 341` haftmann@58689 ` 342` ```lemma power_even_abs_numeral [simp]: ``` haftmann@58689 ` 343` ``` "even (numeral w :: nat) \ \a\ ^ numeral w = a ^ numeral w" ``` haftmann@58689 ` 344` ``` by (fact power_even_abs) ``` haftmann@58689 ` 345` haftmann@58689 ` 346` ```end ``` haftmann@58689 ` 347` haftmann@58689 ` 348` wenzelm@63654 ` 349` ```subsubsection \Tool setup\ ``` haftmann@58687 ` 350` wenzelm@63654 ` 351` ```declare transfer_morphism_int_nat [transfer add return: even_int_iff] ``` wenzelm@21256 ` 352` haftmann@58770 ` 353` ```end ```