src/HOL/Power.thy
 author haftmann Wed Sep 24 19:11:21 2014 +0200 (2014-09-24) changeset 58437 8d124c73c37a parent 58410 6d46ad54a2ab child 58656 7f14d5d9b933 permissions -rw-r--r--
 paulson@3390 ` 1` ```(* Title: HOL/Power.thy ``` paulson@3390 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` paulson@3390 ` 3` ``` Copyright 1997 University of Cambridge ``` paulson@3390 ` 4` ```*) ``` paulson@3390 ` 5` haftmann@30960 ` 6` ```header {* Exponentiation *} ``` paulson@14348 ` 7` nipkow@15131 ` 8` ```theory Power ``` traytel@55096 ` 9` ```imports Num Equiv_Relations ``` nipkow@15131 ` 10` ```begin ``` paulson@14348 ` 11` haftmann@30960 ` 12` ```subsection {* Powers for Arbitrary Monoids *} ``` haftmann@30960 ` 13` haftmann@30996 ` 14` ```class power = one + times ``` haftmann@30960 ` 15` ```begin ``` haftmann@24996 ` 16` haftmann@30960 ` 17` ```primrec power :: "'a \ nat \ 'a" (infixr "^" 80) where ``` haftmann@30960 ` 18` ``` power_0: "a ^ 0 = 1" ``` haftmann@30960 ` 19` ``` | power_Suc: "a ^ Suc n = a * a ^ n" ``` paulson@14348 ` 20` haftmann@30996 ` 21` ```notation (latex output) ``` haftmann@30996 ` 22` ``` power ("(_\<^bsup>_\<^esup>)" [1000] 1000) ``` haftmann@30996 ` 23` haftmann@30996 ` 24` ```notation (HTML output) ``` haftmann@30996 ` 25` ``` power ("(_\<^bsup>_\<^esup>)" [1000] 1000) ``` haftmann@30996 ` 26` huffman@47192 ` 27` ```text {* Special syntax for squares. *} ``` huffman@47192 ` 28` huffman@47192 ` 29` ```abbreviation (xsymbols) ``` wenzelm@53015 ` 30` ``` power2 :: "'a \ 'a" ("(_\<^sup>2)" [1000] 999) where ``` wenzelm@53015 ` 31` ``` "x\<^sup>2 \ x ^ 2" ``` huffman@47192 ` 32` huffman@47192 ` 33` ```notation (latex output) ``` wenzelm@53015 ` 34` ``` power2 ("(_\<^sup>2)" [1000] 999) ``` huffman@47192 ` 35` huffman@47192 ` 36` ```notation (HTML output) ``` wenzelm@53015 ` 37` ``` power2 ("(_\<^sup>2)" [1000] 999) ``` huffman@47192 ` 38` haftmann@30960 ` 39` ```end ``` paulson@14348 ` 40` haftmann@30996 ` 41` ```context monoid_mult ``` haftmann@30996 ` 42` ```begin ``` paulson@14348 ` 43` wenzelm@39438 ` 44` ```subclass power . ``` paulson@14348 ` 45` haftmann@30996 ` 46` ```lemma power_one [simp]: ``` haftmann@30996 ` 47` ``` "1 ^ n = 1" ``` huffman@30273 ` 48` ``` by (induct n) simp_all ``` paulson@14348 ` 49` haftmann@30996 ` 50` ```lemma power_one_right [simp]: ``` haftmann@31001 ` 51` ``` "a ^ 1 = a" ``` haftmann@30996 ` 52` ``` by simp ``` paulson@14348 ` 53` haftmann@30996 ` 54` ```lemma power_commutes: ``` haftmann@30996 ` 55` ``` "a ^ n * a = a * a ^ n" ``` haftmann@57512 ` 56` ``` by (induct n) (simp_all add: mult.assoc) ``` krauss@21199 ` 57` haftmann@30996 ` 58` ```lemma power_Suc2: ``` haftmann@30996 ` 59` ``` "a ^ Suc n = a ^ n * a" ``` huffman@30273 ` 60` ``` by (simp add: power_commutes) ``` huffman@28131 ` 61` haftmann@30996 ` 62` ```lemma power_add: ``` haftmann@30996 ` 63` ``` "a ^ (m + n) = a ^ m * a ^ n" ``` haftmann@30996 ` 64` ``` by (induct m) (simp_all add: algebra_simps) ``` paulson@14348 ` 65` haftmann@30996 ` 66` ```lemma power_mult: ``` haftmann@30996 ` 67` ``` "a ^ (m * n) = (a ^ m) ^ n" ``` huffman@30273 ` 68` ``` by (induct n) (simp_all add: power_add) ``` paulson@14348 ` 69` wenzelm@53015 ` 70` ```lemma power2_eq_square: "a\<^sup>2 = a * a" ``` huffman@47192 ` 71` ``` by (simp add: numeral_2_eq_2) ``` huffman@47192 ` 72` huffman@47192 ` 73` ```lemma power3_eq_cube: "a ^ 3 = a * a * a" ``` haftmann@57512 ` 74` ``` by (simp add: numeral_3_eq_3 mult.assoc) ``` huffman@47192 ` 75` huffman@47192 ` 76` ```lemma power_even_eq: ``` wenzelm@53076 ` 77` ``` "a ^ (2 * n) = (a ^ n)\<^sup>2" ``` haftmann@57512 ` 78` ``` by (subst mult.commute) (simp add: power_mult) ``` huffman@47192 ` 79` huffman@47192 ` 80` ```lemma power_odd_eq: ``` wenzelm@53076 ` 81` ``` "a ^ Suc (2*n) = a * (a ^ n)\<^sup>2" ``` huffman@47192 ` 82` ``` by (simp add: power_even_eq) ``` huffman@47192 ` 83` huffman@47255 ` 84` ```lemma power_numeral_even: ``` huffman@47255 ` 85` ``` "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)" ``` huffman@47255 ` 86` ``` unfolding numeral_Bit0 power_add Let_def .. ``` huffman@47255 ` 87` huffman@47255 ` 88` ```lemma power_numeral_odd: ``` huffman@47255 ` 89` ``` "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)" ``` huffman@47255 ` 90` ``` unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right ``` haftmann@57512 ` 91` ``` unfolding power_Suc power_add Let_def mult.assoc .. ``` huffman@47255 ` 92` haftmann@49824 ` 93` ```lemma funpow_times_power: ``` haftmann@49824 ` 94` ``` "(times x ^^ f x) = times (x ^ f x)" ``` haftmann@49824 ` 95` ```proof (induct "f x" arbitrary: f) ``` haftmann@49824 ` 96` ``` case 0 then show ?case by (simp add: fun_eq_iff) ``` haftmann@49824 ` 97` ```next ``` haftmann@49824 ` 98` ``` case (Suc n) ``` haftmann@49824 ` 99` ``` def g \ "\x. f x - 1" ``` haftmann@49824 ` 100` ``` with Suc have "n = g x" by simp ``` haftmann@49824 ` 101` ``` with Suc have "times x ^^ g x = times (x ^ g x)" by simp ``` haftmann@49824 ` 102` ``` moreover from Suc g_def have "f x = g x + 1" by simp ``` haftmann@57512 ` 103` ``` ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult.assoc) ``` haftmann@49824 ` 104` ```qed ``` haftmann@49824 ` 105` haftmann@30996 ` 106` ```end ``` haftmann@30996 ` 107` haftmann@30996 ` 108` ```context comm_monoid_mult ``` haftmann@30996 ` 109` ```begin ``` haftmann@30996 ` 110` hoelzl@56480 ` 111` ```lemma power_mult_distrib [field_simps]: ``` haftmann@30996 ` 112` ``` "(a * b) ^ n = (a ^ n) * (b ^ n)" ``` haftmann@57514 ` 113` ``` by (induct n) (simp_all add: ac_simps) ``` paulson@14348 ` 114` haftmann@30996 ` 115` ```end ``` haftmann@30996 ` 116` huffman@47191 ` 117` ```context semiring_numeral ``` huffman@47191 ` 118` ```begin ``` huffman@47191 ` 119` huffman@47191 ` 120` ```lemma numeral_sqr: "numeral (Num.sqr k) = numeral k * numeral k" ``` huffman@47191 ` 121` ``` by (simp only: sqr_conv_mult numeral_mult) ``` huffman@47191 ` 122` huffman@47191 ` 123` ```lemma numeral_pow: "numeral (Num.pow k l) = numeral k ^ numeral l" ``` huffman@47191 ` 124` ``` by (induct l, simp_all only: numeral_class.numeral.simps pow.simps ``` huffman@47191 ` 125` ``` numeral_sqr numeral_mult power_add power_one_right) ``` huffman@47191 ` 126` huffman@47191 ` 127` ```lemma power_numeral [simp]: "numeral k ^ numeral l = numeral (Num.pow k l)" ``` huffman@47191 ` 128` ``` by (rule numeral_pow [symmetric]) ``` huffman@47191 ` 129` huffman@47191 ` 130` ```end ``` huffman@47191 ` 131` haftmann@30996 ` 132` ```context semiring_1 ``` haftmann@30996 ` 133` ```begin ``` haftmann@30996 ` 134` haftmann@30996 ` 135` ```lemma of_nat_power: ``` haftmann@30996 ` 136` ``` "of_nat (m ^ n) = of_nat m ^ n" ``` haftmann@30996 ` 137` ``` by (induct n) (simp_all add: of_nat_mult) ``` haftmann@30996 ` 138` huffman@47191 ` 139` ```lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0" ``` huffman@47209 ` 140` ``` by (simp add: numeral_eq_Suc) ``` huffman@47191 ` 141` wenzelm@53015 ` 142` ```lemma zero_power2: "0\<^sup>2 = 0" (* delete? *) ``` huffman@47192 ` 143` ``` by (rule power_zero_numeral) ``` huffman@47192 ` 144` wenzelm@53015 ` 145` ```lemma one_power2: "1\<^sup>2 = 1" (* delete? *) ``` huffman@47192 ` 146` ``` by (rule power_one) ``` huffman@47192 ` 147` haftmann@30996 ` 148` ```end ``` haftmann@30996 ` 149` haftmann@30996 ` 150` ```context comm_semiring_1 ``` haftmann@30996 ` 151` ```begin ``` haftmann@30996 ` 152` haftmann@30996 ` 153` ```text {* The divides relation *} ``` haftmann@30996 ` 154` haftmann@30996 ` 155` ```lemma le_imp_power_dvd: ``` haftmann@30996 ` 156` ``` assumes "m \ n" shows "a ^ m dvd a ^ n" ``` haftmann@30996 ` 157` ```proof ``` haftmann@30996 ` 158` ``` have "a ^ n = a ^ (m + (n - m))" ``` haftmann@30996 ` 159` ``` using `m \ n` by simp ``` haftmann@30996 ` 160` ``` also have "\ = a ^ m * a ^ (n - m)" ``` haftmann@30996 ` 161` ``` by (rule power_add) ``` haftmann@30996 ` 162` ``` finally show "a ^ n = a ^ m * a ^ (n - m)" . ``` haftmann@30996 ` 163` ```qed ``` haftmann@30996 ` 164` haftmann@30996 ` 165` ```lemma power_le_dvd: ``` haftmann@30996 ` 166` ``` "a ^ n dvd b \ m \ n \ a ^ m dvd b" ``` haftmann@30996 ` 167` ``` by (rule dvd_trans [OF le_imp_power_dvd]) ``` haftmann@30996 ` 168` haftmann@30996 ` 169` ```lemma dvd_power_same: ``` haftmann@30996 ` 170` ``` "x dvd y \ x ^ n dvd y ^ n" ``` haftmann@30996 ` 171` ``` by (induct n) (auto simp add: mult_dvd_mono) ``` haftmann@30996 ` 172` haftmann@30996 ` 173` ```lemma dvd_power_le: ``` haftmann@30996 ` 174` ``` "x dvd y \ m \ n \ x ^ n dvd y ^ m" ``` haftmann@30996 ` 175` ``` by (rule power_le_dvd [OF dvd_power_same]) ``` paulson@14348 ` 176` haftmann@30996 ` 177` ```lemma dvd_power [simp]: ``` haftmann@30996 ` 178` ``` assumes "n > (0::nat) \ x = 1" ``` haftmann@30996 ` 179` ``` shows "x dvd (x ^ n)" ``` haftmann@30996 ` 180` ```using assms proof ``` haftmann@30996 ` 181` ``` assume "0 < n" ``` haftmann@30996 ` 182` ``` then have "x ^ n = x ^ Suc (n - 1)" by simp ``` haftmann@30996 ` 183` ``` then show "x dvd (x ^ n)" by simp ``` haftmann@30996 ` 184` ```next ``` haftmann@30996 ` 185` ``` assume "x = 1" ``` haftmann@30996 ` 186` ``` then show "x dvd (x ^ n)" by simp ``` haftmann@30996 ` 187` ```qed ``` haftmann@30996 ` 188` haftmann@30996 ` 189` ```end ``` haftmann@30996 ` 190` haftmann@30996 ` 191` ```context ring_1 ``` haftmann@30996 ` 192` ```begin ``` haftmann@30996 ` 193` haftmann@30996 ` 194` ```lemma power_minus: ``` haftmann@30996 ` 195` ``` "(- a) ^ n = (- 1) ^ n * a ^ n" ``` haftmann@30996 ` 196` ```proof (induct n) ``` haftmann@30996 ` 197` ``` case 0 show ?case by simp ``` haftmann@30996 ` 198` ```next ``` haftmann@30996 ` 199` ``` case (Suc n) then show ?case ``` haftmann@57512 ` 200` ``` by (simp del: power_Suc add: power_Suc2 mult.assoc) ``` haftmann@30996 ` 201` ```qed ``` haftmann@30996 ` 202` huffman@47191 ` 203` ```lemma power_minus_Bit0: ``` huffman@47191 ` 204` ``` "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)" ``` huffman@47191 ` 205` ``` by (induct k, simp_all only: numeral_class.numeral.simps power_add ``` huffman@47191 ` 206` ``` power_one_right mult_minus_left mult_minus_right minus_minus) ``` huffman@47191 ` 207` huffman@47191 ` 208` ```lemma power_minus_Bit1: ``` huffman@47191 ` 209` ``` "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))" ``` huffman@47220 ` 210` ``` by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left) ``` huffman@47191 ` 211` huffman@47192 ` 212` ```lemma power2_minus [simp]: ``` wenzelm@53015 ` 213` ``` "(- a)\<^sup>2 = a\<^sup>2" ``` huffman@47192 ` 214` ``` by (rule power_minus_Bit0) ``` huffman@47192 ` 215` huffman@47192 ` 216` ```lemma power_minus1_even [simp]: ``` haftmann@58410 ` 217` ``` "(- 1) ^ (2*n) = 1" ``` huffman@47192 ` 218` ```proof (induct n) ``` huffman@47192 ` 219` ``` case 0 show ?case by simp ``` huffman@47192 ` 220` ```next ``` huffman@47192 ` 221` ``` case (Suc n) then show ?case by (simp add: power_add power2_eq_square) ``` huffman@47192 ` 222` ```qed ``` huffman@47192 ` 223` huffman@47192 ` 224` ```lemma power_minus1_odd: ``` haftmann@58410 ` 225` ``` "(- 1) ^ Suc (2*n) = -1" ``` huffman@47192 ` 226` ``` by simp ``` huffman@47192 ` 227` huffman@47192 ` 228` ```lemma power_minus_even [simp]: ``` huffman@47192 ` 229` ``` "(-a) ^ (2*n) = a ^ (2*n)" ``` huffman@47192 ` 230` ``` by (simp add: power_minus [of a]) ``` huffman@47192 ` 231` huffman@47192 ` 232` ```end ``` huffman@47192 ` 233` huffman@47192 ` 234` ```context ring_1_no_zero_divisors ``` huffman@47192 ` 235` ```begin ``` huffman@47192 ` 236` huffman@47192 ` 237` ```lemma field_power_not_zero: ``` huffman@47192 ` 238` ``` "a \ 0 \ a ^ n \ 0" ``` huffman@47192 ` 239` ``` by (induct n) auto ``` huffman@47192 ` 240` huffman@47192 ` 241` ```lemma zero_eq_power2 [simp]: ``` wenzelm@53015 ` 242` ``` "a\<^sup>2 = 0 \ a = 0" ``` huffman@47192 ` 243` ``` unfolding power2_eq_square by simp ``` huffman@47192 ` 244` huffman@47192 ` 245` ```lemma power2_eq_1_iff: ``` wenzelm@53015 ` 246` ``` "a\<^sup>2 = 1 \ a = 1 \ a = - 1" ``` huffman@47192 ` 247` ``` unfolding power2_eq_square by (rule square_eq_1_iff) ``` huffman@47192 ` 248` huffman@47192 ` 249` ```end ``` huffman@47192 ` 250` huffman@47192 ` 251` ```context idom ``` huffman@47192 ` 252` ```begin ``` huffman@47192 ` 253` wenzelm@53015 ` 254` ```lemma power2_eq_iff: "x\<^sup>2 = y\<^sup>2 \ x = y \ x = - y" ``` huffman@47192 ` 255` ``` unfolding power2_eq_square by (rule square_eq_iff) ``` huffman@47192 ` 256` huffman@47192 ` 257` ```end ``` huffman@47192 ` 258` huffman@47192 ` 259` ```context division_ring ``` huffman@47192 ` 260` ```begin ``` huffman@47192 ` 261` huffman@47192 ` 262` ```text {* FIXME reorient or rename to @{text nonzero_inverse_power} *} ``` huffman@47192 ` 263` ```lemma nonzero_power_inverse: ``` huffman@47192 ` 264` ``` "a \ 0 \ inverse (a ^ n) = (inverse a) ^ n" ``` huffman@47192 ` 265` ``` by (induct n) ``` huffman@47192 ` 266` ``` (simp_all add: nonzero_inverse_mult_distrib power_commutes field_power_not_zero) ``` huffman@47192 ` 267` huffman@47192 ` 268` ```end ``` huffman@47192 ` 269` huffman@47192 ` 270` ```context field ``` huffman@47192 ` 271` ```begin ``` huffman@47192 ` 272` huffman@47192 ` 273` ```lemma nonzero_power_divide: ``` huffman@47192 ` 274` ``` "b \ 0 \ (a / b) ^ n = a ^ n / b ^ n" ``` huffman@47192 ` 275` ``` by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse) ``` huffman@47192 ` 276` huffman@47192 ` 277` ```end ``` huffman@47192 ` 278` huffman@47192 ` 279` huffman@47192 ` 280` ```subsection {* Exponentiation on ordered types *} ``` huffman@47192 ` 281` huffman@47192 ` 282` ```context linordered_ring (* TODO: move *) ``` huffman@47192 ` 283` ```begin ``` huffman@47192 ` 284` huffman@47192 ` 285` ```lemma sum_squares_ge_zero: ``` huffman@47192 ` 286` ``` "0 \ x * x + y * y" ``` huffman@47192 ` 287` ``` by (intro add_nonneg_nonneg zero_le_square) ``` huffman@47192 ` 288` huffman@47192 ` 289` ```lemma not_sum_squares_lt_zero: ``` huffman@47192 ` 290` ``` "\ x * x + y * y < 0" ``` huffman@47192 ` 291` ``` by (simp add: not_less sum_squares_ge_zero) ``` huffman@47192 ` 292` haftmann@30996 ` 293` ```end ``` haftmann@30996 ` 294` haftmann@35028 ` 295` ```context linordered_semidom ``` haftmann@30996 ` 296` ```begin ``` haftmann@30996 ` 297` haftmann@30996 ` 298` ```lemma zero_less_power [simp]: ``` haftmann@30996 ` 299` ``` "0 < a \ 0 < a ^ n" ``` nipkow@56544 ` 300` ``` by (induct n) simp_all ``` haftmann@30996 ` 301` haftmann@30996 ` 302` ```lemma zero_le_power [simp]: ``` haftmann@30996 ` 303` ``` "0 \ a \ 0 \ a ^ n" ``` nipkow@56536 ` 304` ``` by (induct n) simp_all ``` paulson@14348 ` 305` huffman@47241 ` 306` ```lemma power_mono: ``` huffman@47241 ` 307` ``` "a \ b \ 0 \ a \ a ^ n \ b ^ n" ``` huffman@47241 ` 308` ``` by (induct n) (auto intro: mult_mono order_trans [of 0 a b]) ``` huffman@47241 ` 309` huffman@47241 ` 310` ```lemma one_le_power [simp]: "1 \ a \ 1 \ a ^ n" ``` huffman@47241 ` 311` ``` using power_mono [of 1 a n] by simp ``` huffman@47241 ` 312` huffman@47241 ` 313` ```lemma power_le_one: "\0 \ a; a \ 1\ \ a ^ n \ 1" ``` huffman@47241 ` 314` ``` using power_mono [of a 1 n] by simp ``` paulson@14348 ` 315` paulson@14348 ` 316` ```lemma power_gt1_lemma: ``` haftmann@30996 ` 317` ``` assumes gt1: "1 < a" ``` haftmann@30996 ` 318` ``` shows "1 < a * a ^ n" ``` paulson@14348 ` 319` ```proof - ``` haftmann@30996 ` 320` ``` from gt1 have "0 \ a" ``` haftmann@30996 ` 321` ``` by (fact order_trans [OF zero_le_one less_imp_le]) ``` haftmann@30996 ` 322` ``` have "1 * 1 < a * 1" using gt1 by simp ``` haftmann@30996 ` 323` ``` also have "\ \ a * a ^ n" using gt1 ``` haftmann@30996 ` 324` ``` by (simp only: mult_mono `0 \ a` one_le_power order_less_imp_le ``` wenzelm@14577 ` 325` ``` zero_le_one order_refl) ``` wenzelm@14577 ` 326` ``` finally show ?thesis by simp ``` paulson@14348 ` 327` ```qed ``` paulson@14348 ` 328` haftmann@30996 ` 329` ```lemma power_gt1: ``` haftmann@30996 ` 330` ``` "1 < a \ 1 < a ^ Suc n" ``` haftmann@30996 ` 331` ``` by (simp add: power_gt1_lemma) ``` huffman@24376 ` 332` haftmann@30996 ` 333` ```lemma one_less_power [simp]: ``` haftmann@30996 ` 334` ``` "1 < a \ 0 < n \ 1 < a ^ n" ``` haftmann@30996 ` 335` ``` by (cases n) (simp_all add: power_gt1_lemma) ``` paulson@14348 ` 336` paulson@14348 ` 337` ```lemma power_le_imp_le_exp: ``` haftmann@30996 ` 338` ``` assumes gt1: "1 < a" ``` haftmann@30996 ` 339` ``` shows "a ^ m \ a ^ n \ m \ n" ``` haftmann@30996 ` 340` ```proof (induct m arbitrary: n) ``` paulson@14348 ` 341` ``` case 0 ``` wenzelm@14577 ` 342` ``` show ?case by simp ``` paulson@14348 ` 343` ```next ``` paulson@14348 ` 344` ``` case (Suc m) ``` wenzelm@14577 ` 345` ``` show ?case ``` wenzelm@14577 ` 346` ``` proof (cases n) ``` wenzelm@14577 ` 347` ``` case 0 ``` haftmann@30996 ` 348` ``` with Suc.prems Suc.hyps have "a * a ^ m \ 1" by simp ``` wenzelm@14577 ` 349` ``` with gt1 show ?thesis ``` wenzelm@14577 ` 350` ``` by (force simp only: power_gt1_lemma ``` haftmann@30996 ` 351` ``` not_less [symmetric]) ``` wenzelm@14577 ` 352` ``` next ``` wenzelm@14577 ` 353` ``` case (Suc n) ``` haftmann@30996 ` 354` ``` with Suc.prems Suc.hyps show ?thesis ``` wenzelm@14577 ` 355` ``` by (force dest: mult_left_le_imp_le ``` haftmann@30996 ` 356` ``` simp add: less_trans [OF zero_less_one gt1]) ``` wenzelm@14577 ` 357` ``` qed ``` paulson@14348 ` 358` ```qed ``` paulson@14348 ` 359` wenzelm@14577 ` 360` ```text{*Surely we can strengthen this? It holds for @{text "0 a ^ m = a ^ n \ m = n" ``` wenzelm@14577 ` 363` ``` by (force simp add: order_antisym power_le_imp_le_exp) ``` paulson@14348 ` 364` paulson@14348 ` 365` ```text{*Can relax the first premise to @{term "0 a ^ m < a ^ n \ m < n" ``` haftmann@30996 ` 369` ``` by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] ``` haftmann@30996 ` 370` ``` power_le_imp_le_exp) ``` paulson@14348 ` 371` paulson@14348 ` 372` ```lemma power_strict_mono [rule_format]: ``` haftmann@30996 ` 373` ``` "a < b \ 0 \ a \ 0 < n \ a ^ n < b ^ n" ``` haftmann@30996 ` 374` ``` by (induct n) ``` haftmann@30996 ` 375` ``` (auto simp add: mult_strict_mono le_less_trans [of 0 a b]) ``` paulson@14348 ` 376` paulson@14348 ` 377` ```text{*Lemma for @{text power_strict_decreasing}*} ``` paulson@14348 ` 378` ```lemma power_Suc_less: ``` haftmann@30996 ` 379` ``` "0 < a \ a < 1 \ a * a ^ n < a ^ n" ``` haftmann@30996 ` 380` ``` by (induct n) ``` haftmann@30996 ` 381` ``` (auto simp add: mult_strict_left_mono) ``` paulson@14348 ` 382` haftmann@30996 ` 383` ```lemma power_strict_decreasing [rule_format]: ``` haftmann@30996 ` 384` ``` "n < N \ 0 < a \ a < 1 \ a ^ N < a ^ n" ``` haftmann@30996 ` 385` ```proof (induct N) ``` haftmann@30996 ` 386` ``` case 0 then show ?case by simp ``` haftmann@30996 ` 387` ```next ``` haftmann@30996 ` 388` ``` case (Suc N) then show ?case ``` haftmann@30996 ` 389` ``` apply (auto simp add: power_Suc_less less_Suc_eq) ``` haftmann@30996 ` 390` ``` apply (subgoal_tac "a * a^N < 1 * a^n") ``` haftmann@30996 ` 391` ``` apply simp ``` haftmann@30996 ` 392` ``` apply (rule mult_strict_mono) apply auto ``` haftmann@30996 ` 393` ``` done ``` haftmann@30996 ` 394` ```qed ``` paulson@14348 ` 395` paulson@14348 ` 396` ```text{*Proof resembles that of @{text power_strict_decreasing}*} ``` haftmann@30996 ` 397` ```lemma power_decreasing [rule_format]: ``` haftmann@30996 ` 398` ``` "n \ N \ 0 \ a \ a \ 1 \ a ^ N \ a ^ n" ``` haftmann@30996 ` 399` ```proof (induct N) ``` haftmann@30996 ` 400` ``` case 0 then show ?case by simp ``` haftmann@30996 ` 401` ```next ``` haftmann@30996 ` 402` ``` case (Suc N) then show ?case ``` haftmann@30996 ` 403` ``` apply (auto simp add: le_Suc_eq) ``` haftmann@30996 ` 404` ``` apply (subgoal_tac "a * a^N \ 1 * a^n", simp) ``` haftmann@30996 ` 405` ``` apply (rule mult_mono) apply auto ``` haftmann@30996 ` 406` ``` done ``` haftmann@30996 ` 407` ```qed ``` paulson@14348 ` 408` paulson@14348 ` 409` ```lemma power_Suc_less_one: ``` haftmann@30996 ` 410` ``` "0 < a \ a < 1 \ a ^ Suc n < 1" ``` haftmann@30996 ` 411` ``` using power_strict_decreasing [of 0 "Suc n" a] by simp ``` paulson@14348 ` 412` paulson@14348 ` 413` ```text{*Proof again resembles that of @{text power_strict_decreasing}*} ``` haftmann@30996 ` 414` ```lemma power_increasing [rule_format]: ``` haftmann@30996 ` 415` ``` "n \ N \ 1 \ a \ a ^ n \ a ^ N" ``` haftmann@30996 ` 416` ```proof (induct N) ``` haftmann@30996 ` 417` ``` case 0 then show ?case by simp ``` haftmann@30996 ` 418` ```next ``` haftmann@30996 ` 419` ``` case (Suc N) then show ?case ``` haftmann@30996 ` 420` ``` apply (auto simp add: le_Suc_eq) ``` haftmann@30996 ` 421` ``` apply (subgoal_tac "1 * a^n \ a * a^N", simp) ``` haftmann@30996 ` 422` ``` apply (rule mult_mono) apply (auto simp add: order_trans [OF zero_le_one]) ``` haftmann@30996 ` 423` ``` done ``` haftmann@30996 ` 424` ```qed ``` paulson@14348 ` 425` paulson@14348 ` 426` ```text{*Lemma for @{text power_strict_increasing}*} ``` paulson@14348 ` 427` ```lemma power_less_power_Suc: ``` haftmann@30996 ` 428` ``` "1 < a \ a ^ n < a * a ^ n" ``` haftmann@30996 ` 429` ``` by (induct n) (auto simp add: mult_strict_left_mono less_trans [OF zero_less_one]) ``` paulson@14348 ` 430` haftmann@30996 ` 431` ```lemma power_strict_increasing [rule_format]: ``` haftmann@30996 ` 432` ``` "n < N \ 1 < a \ a ^ n < a ^ N" ``` haftmann@30996 ` 433` ```proof (induct N) ``` haftmann@30996 ` 434` ``` case 0 then show ?case by simp ``` haftmann@30996 ` 435` ```next ``` haftmann@30996 ` 436` ``` case (Suc N) then show ?case ``` haftmann@30996 ` 437` ``` apply (auto simp add: power_less_power_Suc less_Suc_eq) ``` haftmann@30996 ` 438` ``` apply (subgoal_tac "1 * a^n < a * a^N", simp) ``` haftmann@30996 ` 439` ``` apply (rule mult_strict_mono) apply (auto simp add: less_trans [OF zero_less_one] less_imp_le) ``` haftmann@30996 ` 440` ``` done ``` haftmann@30996 ` 441` ```qed ``` paulson@14348 ` 442` nipkow@25134 ` 443` ```lemma power_increasing_iff [simp]: ``` haftmann@30996 ` 444` ``` "1 < b \ b ^ x \ b ^ y \ x \ y" ``` haftmann@30996 ` 445` ``` by (blast intro: power_le_imp_le_exp power_increasing less_imp_le) ``` paulson@15066 ` 446` paulson@15066 ` 447` ```lemma power_strict_increasing_iff [simp]: ``` haftmann@30996 ` 448` ``` "1 < b \ b ^ x < b ^ y \ x < y" ``` nipkow@25134 ` 449` ```by (blast intro: power_less_imp_less_exp power_strict_increasing) ``` paulson@15066 ` 450` paulson@14348 ` 451` ```lemma power_le_imp_le_base: ``` haftmann@30996 ` 452` ``` assumes le: "a ^ Suc n \ b ^ Suc n" ``` haftmann@30996 ` 453` ``` and ynonneg: "0 \ b" ``` haftmann@30996 ` 454` ``` shows "a \ b" ``` nipkow@25134 ` 455` ```proof (rule ccontr) ``` nipkow@25134 ` 456` ``` assume "~ a \ b" ``` nipkow@25134 ` 457` ``` then have "b < a" by (simp only: linorder_not_le) ``` nipkow@25134 ` 458` ``` then have "b ^ Suc n < a ^ Suc n" ``` wenzelm@41550 ` 459` ``` by (simp only: assms power_strict_mono) ``` haftmann@30996 ` 460` ``` from le and this show False ``` nipkow@25134 ` 461` ``` by (simp add: linorder_not_less [symmetric]) ``` nipkow@25134 ` 462` ```qed ``` wenzelm@14577 ` 463` huffman@22853 ` 464` ```lemma power_less_imp_less_base: ``` huffman@22853 ` 465` ``` assumes less: "a ^ n < b ^ n" ``` huffman@22853 ` 466` ``` assumes nonneg: "0 \ b" ``` huffman@22853 ` 467` ``` shows "a < b" ``` huffman@22853 ` 468` ```proof (rule contrapos_pp [OF less]) ``` huffman@22853 ` 469` ``` assume "~ a < b" ``` huffman@22853 ` 470` ``` hence "b \ a" by (simp only: linorder_not_less) ``` huffman@22853 ` 471` ``` hence "b ^ n \ a ^ n" using nonneg by (rule power_mono) ``` haftmann@30996 ` 472` ``` thus "\ a ^ n < b ^ n" by (simp only: linorder_not_less) ``` huffman@22853 ` 473` ```qed ``` huffman@22853 ` 474` paulson@14348 ` 475` ```lemma power_inject_base: ``` haftmann@30996 ` 476` ``` "a ^ Suc n = b ^ Suc n \ 0 \ a \ 0 \ b \ a = b" ``` haftmann@30996 ` 477` ```by (blast intro: power_le_imp_le_base antisym eq_refl sym) ``` paulson@14348 ` 478` huffman@22955 ` 479` ```lemma power_eq_imp_eq_base: ``` haftmann@30996 ` 480` ``` "a ^ n = b ^ n \ 0 \ a \ 0 \ b \ 0 < n \ a = b" ``` haftmann@30996 ` 481` ``` by (cases n) (simp_all del: power_Suc, rule power_inject_base) ``` huffman@22955 ` 482` huffman@47192 ` 483` ```lemma power2_le_imp_le: ``` wenzelm@53015 ` 484` ``` "x\<^sup>2 \ y\<^sup>2 \ 0 \ y \ x \ y" ``` huffman@47192 ` 485` ``` unfolding numeral_2_eq_2 by (rule power_le_imp_le_base) ``` huffman@47192 ` 486` huffman@47192 ` 487` ```lemma power2_less_imp_less: ``` wenzelm@53015 ` 488` ``` "x\<^sup>2 < y\<^sup>2 \ 0 \ y \ x < y" ``` huffman@47192 ` 489` ``` by (rule power_less_imp_less_base) ``` huffman@47192 ` 490` huffman@47192 ` 491` ```lemma power2_eq_imp_eq: ``` wenzelm@53015 ` 492` ``` "x\<^sup>2 = y\<^sup>2 \ 0 \ x \ 0 \ y \ x = y" ``` huffman@47192 ` 493` ``` unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp ``` huffman@47192 ` 494` huffman@47192 ` 495` ```end ``` huffman@47192 ` 496` huffman@47192 ` 497` ```context linordered_ring_strict ``` huffman@47192 ` 498` ```begin ``` huffman@47192 ` 499` huffman@47192 ` 500` ```lemma sum_squares_eq_zero_iff: ``` huffman@47192 ` 501` ``` "x * x + y * y = 0 \ x = 0 \ y = 0" ``` huffman@47192 ` 502` ``` by (simp add: add_nonneg_eq_0_iff) ``` huffman@47192 ` 503` huffman@47192 ` 504` ```lemma sum_squares_le_zero_iff: ``` huffman@47192 ` 505` ``` "x * x + y * y \ 0 \ x = 0 \ y = 0" ``` huffman@47192 ` 506` ``` by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff) ``` huffman@47192 ` 507` huffman@47192 ` 508` ```lemma sum_squares_gt_zero_iff: ``` huffman@47192 ` 509` ``` "0 < x * x + y * y \ x \ 0 \ y \ 0" ``` huffman@47192 ` 510` ``` by (simp add: not_le [symmetric] sum_squares_le_zero_iff) ``` huffman@47192 ` 511` haftmann@30996 ` 512` ```end ``` haftmann@30996 ` 513` haftmann@35028 ` 514` ```context linordered_idom ``` haftmann@30996 ` 515` ```begin ``` huffman@29978 ` 516` haftmann@30996 ` 517` ```lemma power_abs: ``` haftmann@30996 ` 518` ``` "abs (a ^ n) = abs a ^ n" ``` haftmann@30996 ` 519` ``` by (induct n) (auto simp add: abs_mult) ``` haftmann@30996 ` 520` haftmann@30996 ` 521` ```lemma abs_power_minus [simp]: ``` haftmann@30996 ` 522` ``` "abs ((-a) ^ n) = abs (a ^ n)" ``` huffman@35216 ` 523` ``` by (simp add: power_abs) ``` haftmann@30996 ` 524` blanchet@54147 ` 525` ```lemma zero_less_power_abs_iff [simp]: ``` haftmann@30996 ` 526` ``` "0 < abs a ^ n \ a \ 0 \ n = 0" ``` haftmann@30996 ` 527` ```proof (induct n) ``` haftmann@30996 ` 528` ``` case 0 show ?case by simp ``` haftmann@30996 ` 529` ```next ``` haftmann@30996 ` 530` ``` case (Suc n) show ?case by (auto simp add: Suc zero_less_mult_iff) ``` huffman@29978 ` 531` ```qed ``` huffman@29978 ` 532` haftmann@30996 ` 533` ```lemma zero_le_power_abs [simp]: ``` haftmann@30996 ` 534` ``` "0 \ abs a ^ n" ``` haftmann@30996 ` 535` ``` by (rule zero_le_power [OF abs_ge_zero]) ``` haftmann@30996 ` 536` huffman@47192 ` 537` ```lemma zero_le_power2 [simp]: ``` wenzelm@53015 ` 538` ``` "0 \ a\<^sup>2" ``` huffman@47192 ` 539` ``` by (simp add: power2_eq_square) ``` huffman@47192 ` 540` huffman@47192 ` 541` ```lemma zero_less_power2 [simp]: ``` wenzelm@53015 ` 542` ``` "0 < a\<^sup>2 \ a \ 0" ``` huffman@47192 ` 543` ``` by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) ``` huffman@47192 ` 544` huffman@47192 ` 545` ```lemma power2_less_0 [simp]: ``` wenzelm@53015 ` 546` ``` "\ a\<^sup>2 < 0" ``` huffman@47192 ` 547` ``` by (force simp add: power2_eq_square mult_less_0_iff) ``` huffman@47192 ` 548` huffman@47192 ` 549` ```lemma abs_power2 [simp]: ``` wenzelm@53015 ` 550` ``` "abs (a\<^sup>2) = a\<^sup>2" ``` huffman@47192 ` 551` ``` by (simp add: power2_eq_square abs_mult abs_mult_self) ``` huffman@47192 ` 552` huffman@47192 ` 553` ```lemma power2_abs [simp]: ``` wenzelm@53015 ` 554` ``` "(abs a)\<^sup>2 = a\<^sup>2" ``` huffman@47192 ` 555` ``` by (simp add: power2_eq_square abs_mult_self) ``` huffman@47192 ` 556` huffman@47192 ` 557` ```lemma odd_power_less_zero: ``` huffman@47192 ` 558` ``` "a < 0 \ a ^ Suc (2*n) < 0" ``` huffman@47192 ` 559` ```proof (induct n) ``` huffman@47192 ` 560` ``` case 0 ``` huffman@47192 ` 561` ``` then show ?case by simp ``` huffman@47192 ` 562` ```next ``` huffman@47192 ` 563` ``` case (Suc n) ``` huffman@47192 ` 564` ``` have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" ``` haftmann@57514 ` 565` ``` by (simp add: ac_simps power_add power2_eq_square) ``` huffman@47192 ` 566` ``` thus ?case ``` huffman@47192 ` 567` ``` by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg) ``` huffman@47192 ` 568` ```qed ``` haftmann@30996 ` 569` huffman@47192 ` 570` ```lemma odd_0_le_power_imp_0_le: ``` huffman@47192 ` 571` ``` "0 \ a ^ Suc (2*n) \ 0 \ a" ``` huffman@47192 ` 572` ``` using odd_power_less_zero [of a n] ``` huffman@47192 ` 573` ``` by (force simp add: linorder_not_less [symmetric]) ``` huffman@47192 ` 574` huffman@47192 ` 575` ```lemma zero_le_even_power'[simp]: ``` huffman@47192 ` 576` ``` "0 \ a ^ (2*n)" ``` huffman@47192 ` 577` ```proof (induct n) ``` huffman@47192 ` 578` ``` case 0 ``` huffman@47192 ` 579` ``` show ?case by simp ``` huffman@47192 ` 580` ```next ``` huffman@47192 ` 581` ``` case (Suc n) ``` huffman@47192 ` 582` ``` have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" ``` haftmann@57514 ` 583` ``` by (simp add: ac_simps power_add power2_eq_square) ``` huffman@47192 ` 584` ``` thus ?case ``` huffman@47192 ` 585` ``` by (simp add: Suc zero_le_mult_iff) ``` huffman@47192 ` 586` ```qed ``` haftmann@30996 ` 587` huffman@47192 ` 588` ```lemma sum_power2_ge_zero: ``` wenzelm@53015 ` 589` ``` "0 \ x\<^sup>2 + y\<^sup>2" ``` huffman@47192 ` 590` ``` by (intro add_nonneg_nonneg zero_le_power2) ``` huffman@47192 ` 591` huffman@47192 ` 592` ```lemma not_sum_power2_lt_zero: ``` wenzelm@53015 ` 593` ``` "\ x\<^sup>2 + y\<^sup>2 < 0" ``` huffman@47192 ` 594` ``` unfolding not_less by (rule sum_power2_ge_zero) ``` huffman@47192 ` 595` huffman@47192 ` 596` ```lemma sum_power2_eq_zero_iff: ``` wenzelm@53015 ` 597` ``` "x\<^sup>2 + y\<^sup>2 = 0 \ x = 0 \ y = 0" ``` huffman@47192 ` 598` ``` unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff) ``` huffman@47192 ` 599` huffman@47192 ` 600` ```lemma sum_power2_le_zero_iff: ``` wenzelm@53015 ` 601` ``` "x\<^sup>2 + y\<^sup>2 \ 0 \ x = 0 \ y = 0" ``` huffman@47192 ` 602` ``` by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero) ``` huffman@47192 ` 603` huffman@47192 ` 604` ```lemma sum_power2_gt_zero_iff: ``` wenzelm@53015 ` 605` ``` "0 < x\<^sup>2 + y\<^sup>2 \ x \ 0 \ y \ 0" ``` huffman@47192 ` 606` ``` unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) ``` haftmann@30996 ` 607` haftmann@30996 ` 608` ```end ``` haftmann@30996 ` 609` huffman@29978 ` 610` huffman@47192 ` 611` ```subsection {* Miscellaneous rules *} ``` paulson@14348 ` 612` lp15@55718 ` 613` ```lemma self_le_power: ``` lp15@55718 ` 614` ``` fixes x::"'a::linordered_semidom" ``` lp15@55718 ` 615` ``` shows "1 \ x \ 0 < n \ x \ x ^ n" ``` traytel@55811 ` 616` ``` using power_increasing[of 1 n x] power_one_right[of x] by auto ``` lp15@55718 ` 617` huffman@47255 ` 618` ```lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))" ``` huffman@47255 ` 619` ``` unfolding One_nat_def by (cases m) simp_all ``` huffman@47255 ` 620` huffman@47192 ` 621` ```lemma power2_sum: ``` huffman@47192 ` 622` ``` fixes x y :: "'a::comm_semiring_1" ``` wenzelm@53015 ` 623` ``` shows "(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y" ``` huffman@47192 ` 624` ``` by (simp add: algebra_simps power2_eq_square mult_2_right) ``` haftmann@30996 ` 625` huffman@47192 ` 626` ```lemma power2_diff: ``` huffman@47192 ` 627` ``` fixes x y :: "'a::comm_ring_1" ``` wenzelm@53015 ` 628` ``` shows "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y" ``` haftmann@57512 ` 629` ``` by (simp add: ring_distribs power2_eq_square mult_2) (rule mult.commute) ``` haftmann@30996 ` 630` haftmann@30996 ` 631` ```lemma power_0_Suc [simp]: ``` haftmann@30996 ` 632` ``` "(0::'a::{power, semiring_0}) ^ Suc n = 0" ``` haftmann@30996 ` 633` ``` by simp ``` nipkow@30313 ` 634` haftmann@30996 ` 635` ```text{*It looks plausible as a simprule, but its effect can be strange.*} ``` haftmann@30996 ` 636` ```lemma power_0_left: ``` haftmann@30996 ` 637` ``` "0 ^ n = (if n = 0 then 1 else (0::'a::{power, semiring_0}))" ``` haftmann@30996 ` 638` ``` by (induct n) simp_all ``` haftmann@30996 ` 639` haftmann@30996 ` 640` ```lemma power_eq_0_iff [simp]: ``` haftmann@30996 ` 641` ``` "a ^ n = 0 \ ``` haftmann@30996 ` 642` ``` a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,power}) \ n \ 0" ``` haftmann@30996 ` 643` ``` by (induct n) ``` haftmann@30996 ` 644` ``` (auto simp add: no_zero_divisors elim: contrapos_pp) ``` haftmann@30996 ` 645` haftmann@36409 ` 646` ```lemma (in field) power_diff: ``` haftmann@30996 ` 647` ``` assumes nz: "a \ 0" ``` haftmann@30996 ` 648` ``` shows "n \ m \ a ^ (m - n) = a ^ m / a ^ n" ``` haftmann@36409 ` 649` ``` by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero) ``` nipkow@30313 ` 650` haftmann@30996 ` 651` ```text{*Perhaps these should be simprules.*} ``` haftmann@30996 ` 652` ```lemma power_inverse: ``` haftmann@36409 ` 653` ``` fixes a :: "'a::division_ring_inverse_zero" ``` haftmann@36409 ` 654` ``` shows "inverse (a ^ n) = inverse a ^ n" ``` haftmann@30996 ` 655` ```apply (cases "a = 0") ``` haftmann@30996 ` 656` ```apply (simp add: power_0_left) ``` haftmann@30996 ` 657` ```apply (simp add: nonzero_power_inverse) ``` haftmann@30996 ` 658` ```done (* TODO: reorient or rename to inverse_power *) ``` haftmann@30996 ` 659` haftmann@30996 ` 660` ```lemma power_one_over: ``` haftmann@36409 ` 661` ``` "1 / (a::'a::{field_inverse_zero, power}) ^ n = (1 / a) ^ n" ``` haftmann@30996 ` 662` ``` by (simp add: divide_inverse) (rule power_inverse) ``` haftmann@30996 ` 663` hoelzl@56481 ` 664` ```lemma power_divide [field_simps, divide_simps]: ``` haftmann@36409 ` 665` ``` "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n" ``` haftmann@30996 ` 666` ```apply (cases "b = 0") ``` haftmann@30996 ` 667` ```apply (simp add: power_0_left) ``` haftmann@30996 ` 668` ```apply (rule nonzero_power_divide) ``` haftmann@30996 ` 669` ```apply assumption ``` nipkow@30313 ` 670` ```done ``` nipkow@30313 ` 671` huffman@47255 ` 672` ```text {* Simprules for comparisons where common factors can be cancelled. *} ``` huffman@47255 ` 673` huffman@47255 ` 674` ```lemmas zero_compare_simps = ``` huffman@47255 ` 675` ``` add_strict_increasing add_strict_increasing2 add_increasing ``` huffman@47255 ` 676` ``` zero_le_mult_iff zero_le_divide_iff ``` huffman@47255 ` 677` ``` zero_less_mult_iff zero_less_divide_iff ``` huffman@47255 ` 678` ``` mult_le_0_iff divide_le_0_iff ``` huffman@47255 ` 679` ``` mult_less_0_iff divide_less_0_iff ``` huffman@47255 ` 680` ``` zero_le_power2 power2_less_0 ``` huffman@47255 ` 681` nipkow@30313 ` 682` haftmann@30960 ` 683` ```subsection {* Exponentiation for the Natural Numbers *} ``` wenzelm@14577 ` 684` haftmann@30996 ` 685` ```lemma nat_one_le_power [simp]: ``` haftmann@30996 ` 686` ``` "Suc 0 \ i \ Suc 0 \ i ^ n" ``` haftmann@30996 ` 687` ``` by (rule one_le_power [of i n, unfolded One_nat_def]) ``` huffman@23305 ` 688` haftmann@30996 ` 689` ```lemma nat_zero_less_power_iff [simp]: ``` haftmann@30996 ` 690` ``` "x ^ n > 0 \ x > (0::nat) \ n = 0" ``` haftmann@30996 ` 691` ``` by (induct n) auto ``` paulson@14348 ` 692` nipkow@30056 ` 693` ```lemma nat_power_eq_Suc_0_iff [simp]: ``` haftmann@30996 ` 694` ``` "x ^ m = Suc 0 \ m = 0 \ x = Suc 0" ``` haftmann@30996 ` 695` ``` by (induct m) auto ``` nipkow@30056 ` 696` haftmann@30996 ` 697` ```lemma power_Suc_0 [simp]: ``` haftmann@30996 ` 698` ``` "Suc 0 ^ n = Suc 0" ``` haftmann@30996 ` 699` ``` by simp ``` nipkow@30056 ` 700` paulson@14348 ` 701` ```text{*Valid for the naturals, but what if @{text"0nat)" ``` haftmann@30996 ` 706` ``` assumes less: "i ^ m < i ^ n" ``` haftmann@21413 ` 707` ``` shows "m < n" ``` haftmann@21413 ` 708` ```proof (cases "i = 1") ``` haftmann@21413 ` 709` ``` case True with less power_one [where 'a = nat] show ?thesis by simp ``` haftmann@21413 ` 710` ```next ``` haftmann@21413 ` 711` ``` case False with nonneg have "1 < i" by auto ``` haftmann@21413 ` 712` ``` from power_strict_increasing_iff [OF this] less show ?thesis .. ``` haftmann@21413 ` 713` ```qed ``` paulson@14348 ` 714` haftmann@33274 ` 715` ```lemma power_dvd_imp_le: ``` haftmann@33274 ` 716` ``` "i ^ m dvd i ^ n \ (1::nat) < i \ m \ n" ``` haftmann@33274 ` 717` ``` apply (rule power_le_imp_le_exp, assumption) ``` haftmann@33274 ` 718` ``` apply (erule dvd_imp_le, simp) ``` haftmann@33274 ` 719` ``` done ``` haftmann@33274 ` 720` haftmann@51263 ` 721` ```lemma power2_nat_le_eq_le: ``` haftmann@51263 ` 722` ``` fixes m n :: nat ``` wenzelm@53015 ` 723` ``` shows "m\<^sup>2 \ n\<^sup>2 \ m \ n" ``` haftmann@51263 ` 724` ``` by (auto intro: power2_le_imp_le power_mono) ``` haftmann@51263 ` 725` haftmann@51263 ` 726` ```lemma power2_nat_le_imp_le: ``` haftmann@51263 ` 727` ``` fixes m n :: nat ``` wenzelm@53015 ` 728` ``` assumes "m\<^sup>2 \ n" ``` haftmann@51263 ` 729` ``` shows "m \ n" ``` haftmann@54249 ` 730` ```proof (cases m) ``` haftmann@54249 ` 731` ``` case 0 then show ?thesis by simp ``` haftmann@54249 ` 732` ```next ``` haftmann@54249 ` 733` ``` case (Suc k) ``` haftmann@54249 ` 734` ``` show ?thesis ``` haftmann@54249 ` 735` ``` proof (rule ccontr) ``` haftmann@54249 ` 736` ``` assume "\ m \ n" ``` haftmann@54249 ` 737` ``` then have "n < m" by simp ``` haftmann@54249 ` 738` ``` with assms Suc show False ``` haftmann@54249 ` 739` ``` by (auto simp add: algebra_simps) (simp add: power2_eq_square) ``` haftmann@54249 ` 740` ``` qed ``` haftmann@54249 ` 741` ```qed ``` haftmann@51263 ` 742` traytel@55096 ` 743` ```subsubsection {* Cardinality of the Powerset *} ``` traytel@55096 ` 744` traytel@55096 ` 745` ```lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2" ``` traytel@55096 ` 746` ``` unfolding UNIV_bool by simp ``` traytel@55096 ` 747` traytel@55096 ` 748` ```lemma card_Pow: "finite A \ card (Pow A) = 2 ^ card A" ``` traytel@55096 ` 749` ```proof (induct rule: finite_induct) ``` traytel@55096 ` 750` ``` case empty ``` traytel@55096 ` 751` ``` show ?case by auto ``` traytel@55096 ` 752` ```next ``` traytel@55096 ` 753` ``` case (insert x A) ``` traytel@55096 ` 754` ``` then have "inj_on (insert x) (Pow A)" ``` traytel@55096 ` 755` ``` unfolding inj_on_def by (blast elim!: equalityE) ``` traytel@55096 ` 756` ``` then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A" ``` traytel@55096 ` 757` ``` by (simp add: mult_2 card_image Pow_insert insert.hyps) ``` traytel@55096 ` 758` ``` then show ?case using insert ``` traytel@55096 ` 759` ``` apply (simp add: Pow_insert) ``` traytel@55096 ` 760` ``` apply (subst card_Un_disjoint, auto) ``` traytel@55096 ` 761` ``` done ``` traytel@55096 ` 762` ```qed ``` traytel@55096 ` 763` haftmann@57418 ` 764` haftmann@57418 ` 765` ```subsubsection {* Generalized sum over a set *} ``` haftmann@57418 ` 766` haftmann@57418 ` 767` ```lemma setsum_zero_power [simp]: ``` haftmann@57418 ` 768` ``` fixes c :: "nat \ 'a::division_ring" ``` haftmann@57418 ` 769` ``` shows "(\i\A. c i * 0^i) = (if finite A \ 0 \ A then c 0 else 0)" ``` haftmann@57418 ` 770` ```apply (cases "finite A") ``` haftmann@57418 ` 771` ``` by (induction A rule: finite_induct) auto ``` haftmann@57418 ` 772` haftmann@57418 ` 773` ```lemma setsum_zero_power' [simp]: ``` haftmann@57418 ` 774` ``` fixes c :: "nat \ 'a::field" ``` haftmann@57418 ` 775` ``` shows "(\i\A. c i * 0^i / d i) = (if finite A \ 0 \ A then c 0 / d 0 else 0)" ``` haftmann@57418 ` 776` ``` using setsum_zero_power [of "\i. c i / d i" A] ``` haftmann@57418 ` 777` ``` by auto ``` haftmann@57418 ` 778` haftmann@57418 ` 779` traytel@55096 ` 780` ```subsubsection {* Generalized product over a set *} ``` traytel@55096 ` 781` traytel@55096 ` 782` ```lemma setprod_constant: "finite A ==> (\x\ A. (y::'a::{comm_monoid_mult})) = y^(card A)" ``` traytel@55096 ` 783` ```apply (erule finite_induct) ``` traytel@55096 ` 784` ```apply auto ``` traytel@55096 ` 785` ```done ``` traytel@55096 ` 786` haftmann@57418 ` 787` ```lemma setprod_power_distrib: ``` haftmann@57418 ` 788` ``` fixes f :: "'a \ 'b::comm_semiring_1" ``` haftmann@57418 ` 789` ``` shows "setprod f A ^ n = setprod (\x. (f x) ^ n) A" ``` haftmann@57418 ` 790` ```proof (cases "finite A") ``` haftmann@57418 ` 791` ``` case True then show ?thesis ``` haftmann@57418 ` 792` ``` by (induct A rule: finite_induct) (auto simp add: power_mult_distrib) ``` haftmann@57418 ` 793` ```next ``` haftmann@57418 ` 794` ``` case False then show ?thesis ``` haftmann@57418 ` 795` ``` by simp ``` haftmann@57418 ` 796` ```qed ``` haftmann@57418 ` 797` haftmann@58437 ` 798` ```lemma power_setsum: ``` haftmann@58437 ` 799` ``` "c ^ (\a\A. f a) = (\a\A. c ^ f a)" ``` haftmann@58437 ` 800` ``` by (induct A rule: infinite_finite_induct) (simp_all add: power_add) ``` haftmann@58437 ` 801` traytel@55096 ` 802` ```lemma setprod_gen_delta: ``` traytel@55096 ` 803` ``` assumes fS: "finite S" ``` traytel@55096 ` 804` ``` shows "setprod (\k. if k=a then b k else c) S = (if a \ S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)" ``` traytel@55096 ` 805` ```proof- ``` traytel@55096 ` 806` ``` let ?f = "(\k. if k=a then b k else c)" ``` traytel@55096 ` 807` ``` {assume a: "a \ S" ``` traytel@55096 ` 808` ``` hence "\ k\ S. ?f k = c" by simp ``` traytel@55096 ` 809` ``` hence ?thesis using a setprod_constant[OF fS, of c] by simp } ``` traytel@55096 ` 810` ``` moreover ``` traytel@55096 ` 811` ``` {assume a: "a \ S" ``` traytel@55096 ` 812` ``` let ?A = "S - {a}" ``` traytel@55096 ` 813` ``` let ?B = "{a}" ``` traytel@55096 ` 814` ``` have eq: "S = ?A \ ?B" using a by blast ``` traytel@55096 ` 815` ``` have dj: "?A \ ?B = {}" by simp ``` traytel@55096 ` 816` ``` from fS have fAB: "finite ?A" "finite ?B" by auto ``` traytel@55096 ` 817` ``` have fA0:"setprod ?f ?A = setprod (\i. c) ?A" ``` haftmann@57418 ` 818` ``` apply (rule setprod.cong) by auto ``` traytel@55096 ` 819` ``` have cA: "card ?A = card S - 1" using fS a by auto ``` traytel@55096 ` 820` ``` have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto ``` traytel@55096 ` 821` ``` have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" ``` haftmann@57418 ` 822` ``` using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] ``` traytel@55096 ` 823` ``` by simp ``` traytel@55096 ` 824` ``` then have ?thesis using a cA ``` haftmann@57418 ` 825` ``` by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)} ``` traytel@55096 ` 826` ``` ultimately show ?thesis by blast ``` traytel@55096 ` 827` ```qed ``` traytel@55096 ` 828` haftmann@31155 ` 829` ```subsection {* Code generator tweak *} ``` haftmann@31155 ` 830` bulwahn@45231 ` 831` ```lemma power_power_power [code]: ``` haftmann@31155 ` 832` ``` "power = power.power (1::'a::{power}) (op *)" ``` haftmann@31155 ` 833` ``` unfolding power_def power.power_def .. ``` haftmann@31155 ` 834` haftmann@31155 ` 835` ```declare power.power.simps [code] ``` haftmann@31155 ` 836` haftmann@52435 ` 837` ```code_identifier ``` haftmann@52435 ` 838` ``` code_module Power \ (SML) Arith and (OCaml) Arith and (Haskell) Arith ``` haftmann@33364 ` 839` paulson@3390 ` 840` ```end ``` haftmann@49824 ` 841`