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