1(* Title: HOL/Power.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1997 University of Cambridge 4*) 5 6section \<open>Exponentiation\<close> 7 8theory Power 9 imports Num 10begin 11 12subsection \<open>Powers for Arbitrary Monoids\<close> 13 14class power = one + times 15begin 16 17primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) 18 where 19 power_0: "a ^ 0 = 1" 20 | power_Suc: "a ^ Suc n = a * a ^ n" 21 22notation (latex output) 23 power ("(_\<^bsup>_\<^esup>)" [1000] 1000) 24 25text \<open>Special syntax for squares.\<close> 26abbreviation power2 :: "'a \<Rightarrow> 'a" ("(_\<^sup>2)" [1000] 999) 27 where "x\<^sup>2 \<equiv> x ^ 2" 28 29end 30 31context monoid_mult 32begin 33 34subclass power . 35 36lemma power_one [simp]: "1 ^ n = 1" 37 by (induct n) simp_all 38 39lemma power_one_right [simp]: "a ^ 1 = a" 40 by simp 41 42lemma power_Suc0_right [simp]: "a ^ Suc 0 = a" 43 by simp 44 45lemma power_commutes: "a ^ n * a = a * a ^ n" 46 by (induct n) (simp_all add: mult.assoc) 47 48lemma power_Suc2: "a ^ Suc n = a ^ n * a" 49 by (simp add: power_commutes) 50 51lemma power_add: "a ^ (m + n) = a ^ m * a ^ n" 52 by (induct m) (simp_all add: algebra_simps) 53 54lemma power_mult: "a ^ (m * n) = (a ^ m) ^ n" 55 by (induct n) (simp_all add: power_add) 56 57lemma power2_eq_square: "a\<^sup>2 = a * a" 58 by (simp add: numeral_2_eq_2) 59 60lemma power3_eq_cube: "a ^ 3 = a * a * a" 61 by (simp add: numeral_3_eq_3 mult.assoc) 62 63lemma power_even_eq: "a ^ (2 * n) = (a ^ n)\<^sup>2" 64 by (subst mult.commute) (simp add: power_mult) 65 66lemma power_odd_eq: "a ^ Suc (2*n) = a * (a ^ n)\<^sup>2" 67 by (simp add: power_even_eq) 68 69lemma power_numeral_even: "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)" 70 by (simp only: numeral_Bit0 power_add Let_def) 71 72lemma power_numeral_odd: "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)" 73 by (simp only: numeral_Bit1 One_nat_def add_Suc_right add_0_right 74 power_Suc power_add Let_def mult.assoc) 75 76lemma funpow_times_power: "(times x ^^ f x) = times (x ^ f x)" 77proof (induct "f x" arbitrary: f) 78 case 0 79 then show ?case by (simp add: fun_eq_iff) 80next 81 case (Suc n) 82 define g where "g x = f x - 1" for x 83 with Suc have "n = g x" by simp 84 with Suc have "times x ^^ g x = times (x ^ g x)" by simp 85 moreover from Suc g_def have "f x = g x + 1" by simp 86 ultimately show ?case 87 by (simp add: power_add funpow_add fun_eq_iff mult.assoc) 88qed 89 90lemma power_commuting_commutes: 91 assumes "x * y = y * x" 92 shows "x ^ n * y = y * x ^n" 93proof (induct n) 94 case 0 95 then show ?case by simp 96next 97 case (Suc n) 98 have "x ^ Suc n * y = x ^ n * y * x" 99 by (subst power_Suc2) (simp add: assms ac_simps) 100 also have "\<dots> = y * x ^ Suc n" 101 by (simp only: Suc power_Suc2) (simp add: ac_simps) 102 finally show ?case . 103qed 104 105lemma power_minus_mult: "0 < n \<Longrightarrow> a ^ (n - 1) * a = a ^ n" 106 by (simp add: power_commutes split: nat_diff_split) 107 108end 109 110context comm_monoid_mult 111begin 112 113lemma power_mult_distrib [field_simps]: "(a * b) ^ n = (a ^ n) * (b ^ n)" 114 by (induct n) (simp_all add: ac_simps) 115 116end 117 118text \<open>Extract constant factors from powers.\<close> 119declare power_mult_distrib [where a = "numeral w" for w, simp] 120declare power_mult_distrib [where b = "numeral w" for w, simp] 121 122lemma power_add_numeral [simp]: "a^numeral m * a^numeral n = a^numeral (m + n)" 123 for a :: "'a::monoid_mult" 124 by (simp add: power_add [symmetric]) 125 126lemma power_add_numeral2 [simp]: "a^numeral m * (a^numeral n * b) = a^numeral (m + n) * b" 127 for a :: "'a::monoid_mult" 128 by (simp add: mult.assoc [symmetric]) 129 130lemma power_mult_numeral [simp]: "(a^numeral m)^numeral n = a^numeral (m * n)" 131 for a :: "'a::monoid_mult" 132 by (simp only: numeral_mult power_mult) 133 134context semiring_numeral 135begin 136 137lemma numeral_sqr: "numeral (Num.sqr k) = numeral k * numeral k" 138 by (simp only: sqr_conv_mult numeral_mult) 139 140lemma numeral_pow: "numeral (Num.pow k l) = numeral k ^ numeral l" 141 by (induct l) 142 (simp_all only: numeral_class.numeral.simps pow.simps 143 numeral_sqr numeral_mult power_add power_one_right) 144 145lemma power_numeral [simp]: "numeral k ^ numeral l = numeral (Num.pow k l)" 146 by (rule numeral_pow [symmetric]) 147 148end 149 150context semiring_1 151begin 152 153lemma of_nat_power [simp]: "of_nat (m ^ n) = of_nat m ^ n" 154 by (induct n) simp_all 155 156lemma zero_power: "0 < n \<Longrightarrow> 0 ^ n = 0" 157 by (cases n) simp_all 158 159lemma power_zero_numeral [simp]: "0 ^ numeral k = 0" 160 by (simp add: numeral_eq_Suc) 161 162lemma zero_power2: "0\<^sup>2 = 0" (* delete? *) 163 by (rule power_zero_numeral) 164 165lemma one_power2: "1\<^sup>2 = 1" (* delete? *) 166 by (rule power_one) 167 168lemma power_0_Suc [simp]: "0 ^ Suc n = 0" 169 by simp 170 171text \<open>It looks plausible as a simprule, but its effect can be strange.\<close> 172lemma power_0_left: "0 ^ n = (if n = 0 then 1 else 0)" 173 by (cases n) simp_all 174 175end 176 177context semiring_char_0 begin 178 179lemma numeral_power_eq_of_nat_cancel_iff [simp]: 180 "numeral x ^ n = of_nat y \<longleftrightarrow> numeral x ^ n = y" 181 using of_nat_eq_iff by fastforce 182 183lemma real_of_nat_eq_numeral_power_cancel_iff [simp]: 184 "of_nat y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n" 185 using numeral_power_eq_of_nat_cancel_iff [of x n y] by (metis (mono_tags)) 186 187lemma of_nat_eq_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w = of_nat x \<longleftrightarrow> b ^ w = x" 188 by (metis of_nat_power of_nat_eq_iff) 189 190lemma of_nat_power_eq_of_nat_cancel_iff[simp]: "of_nat x = (of_nat b) ^ w \<longleftrightarrow> x = b ^ w" 191 by (metis of_nat_eq_of_nat_power_cancel_iff) 192 193end 194 195context comm_semiring_1 196begin 197 198text \<open>The divides relation.\<close> 199 200lemma le_imp_power_dvd: 201 assumes "m \<le> n" 202 shows "a ^ m dvd a ^ n" 203proof 204 from assms have "a ^ n = a ^ (m + (n - m))" by simp 205 also have "\<dots> = a ^ m * a ^ (n - m)" by (rule power_add) 206 finally show "a ^ n = a ^ m * a ^ (n - m)" . 207qed 208 209lemma power_le_dvd: "a ^ n dvd b \<Longrightarrow> m \<le> n \<Longrightarrow> a ^ m dvd b" 210 by (rule dvd_trans [OF le_imp_power_dvd]) 211 212lemma dvd_power_same: "x dvd y \<Longrightarrow> x ^ n dvd y ^ n" 213 by (induct n) (auto simp add: mult_dvd_mono) 214 215lemma dvd_power_le: "x dvd y \<Longrightarrow> m \<ge> n \<Longrightarrow> x ^ n dvd y ^ m" 216 by (rule power_le_dvd [OF dvd_power_same]) 217 218lemma dvd_power [simp]: 219 fixes n :: nat 220 assumes "n > 0 \<or> x = 1" 221 shows "x dvd (x ^ n)" 222 using assms 223proof 224 assume "0 < n" 225 then have "x ^ n = x ^ Suc (n - 1)" by simp 226 then show "x dvd (x ^ n)" by simp 227next 228 assume "x = 1" 229 then show "x dvd (x ^ n)" by simp 230qed 231 232end 233 234context semiring_1_no_zero_divisors 235begin 236 237subclass power . 238 239lemma power_eq_0_iff [simp]: "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0" 240 by (induct n) auto 241 242lemma power_not_zero: "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0" 243 by (induct n) auto 244 245lemma zero_eq_power2 [simp]: "a\<^sup>2 = 0 \<longleftrightarrow> a = 0" 246 unfolding power2_eq_square by simp 247 248end 249 250context ring_1 251begin 252 253lemma power_minus: "(- a) ^ n = (- 1) ^ n * a ^ n" 254proof (induct n) 255 case 0 256 show ?case by simp 257next 258 case (Suc n) 259 then show ?case 260 by (simp del: power_Suc add: power_Suc2 mult.assoc) 261qed 262 263lemma power_minus': "NO_MATCH 1 x \<Longrightarrow> (-x) ^ n = (-1)^n * x ^ n" 264 by (rule power_minus) 265 266lemma power_minus_Bit0: "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)" 267 by (induct k, simp_all only: numeral_class.numeral.simps power_add 268 power_one_right mult_minus_left mult_minus_right minus_minus) 269 270lemma power_minus_Bit1: "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))" 271 by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left) 272 273lemma power2_minus [simp]: "(- a)\<^sup>2 = a\<^sup>2" 274 by (fact power_minus_Bit0) 275 276lemma power_minus1_even [simp]: "(- 1) ^ (2*n) = 1" 277proof (induct n) 278 case 0 279 show ?case by simp 280next 281 case (Suc n) 282 then show ?case by (simp add: power_add power2_eq_square) 283qed 284 285lemma power_minus1_odd: "(- 1) ^ Suc (2*n) = -1" 286 by simp 287 288lemma power_minus_even [simp]: "(-a) ^ (2*n) = a ^ (2*n)" 289 by (simp add: power_minus [of a]) 290 291end 292 293context ring_1_no_zero_divisors 294begin 295 296lemma power2_eq_1_iff: "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1" 297 using square_eq_1_iff [of a] by (simp add: power2_eq_square) 298 299end 300 301context idom 302begin 303 304lemma power2_eq_iff: "x\<^sup>2 = y\<^sup>2 \<longleftrightarrow> x = y \<or> x = - y" 305 unfolding power2_eq_square by (rule square_eq_iff) 306 307end 308 309context semidom_divide 310begin 311 312lemma power_diff: 313 "a ^ (m - n) = (a ^ m) div (a ^ n)" if "a \<noteq> 0" and "n \<le> m" 314proof - 315 define q where "q = m - n" 316 with \<open>n \<le> m\<close> have "m = q + n" by simp 317 with \<open>a \<noteq> 0\<close> q_def show ?thesis 318 by (simp add: power_add) 319qed 320 321end 322 323context algebraic_semidom 324begin 325 326lemma div_power: "b dvd a \<Longrightarrow> (a div b) ^ n = a ^ n div b ^ n" 327 by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same) 328 329lemma is_unit_power_iff: "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0" 330 by (induct n) (auto simp add: is_unit_mult_iff) 331 332lemma dvd_power_iff: 333 assumes "x \<noteq> 0" 334 shows "x ^ m dvd x ^ n \<longleftrightarrow> is_unit x \<or> m \<le> n" 335proof 336 assume *: "x ^ m dvd x ^ n" 337 { 338 assume "m > n" 339 note * 340 also have "x ^ n = x ^ n * 1" by simp 341 also from \<open>m > n\<close> have "m = n + (m - n)" by simp 342 also have "x ^ \<dots> = x ^ n * x ^ (m - n)" by (rule power_add) 343 finally have "x ^ (m - n) dvd 1" 344 by (subst (asm) dvd_times_left_cancel_iff) (insert assms, simp_all) 345 with \<open>m > n\<close> have "is_unit x" by (simp add: is_unit_power_iff) 346 } 347 thus "is_unit x \<or> m \<le> n" by force 348qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd) 349 350 351end 352 353context normalization_semidom 354begin 355 356lemma normalize_power: "normalize (a ^ n) = normalize a ^ n" 357 by (induct n) (simp_all add: normalize_mult) 358 359lemma unit_factor_power: "unit_factor (a ^ n) = unit_factor a ^ n" 360 by (induct n) (simp_all add: unit_factor_mult) 361 362end 363 364context division_ring 365begin 366 367text \<open>Perhaps these should be simprules.\<close> 368lemma power_inverse [field_simps, divide_simps]: "inverse a ^ n = inverse (a ^ n)" 369proof (cases "a = 0") 370 case True 371 then show ?thesis by (simp add: power_0_left) 372next 373 case False 374 then have "inverse (a ^ n) = inverse a ^ n" 375 by (induct n) (simp_all add: nonzero_inverse_mult_distrib power_commutes) 376 then show ?thesis by simp 377qed 378 379lemma power_one_over [field_simps, divide_simps]: "(1 / a) ^ n = 1 / a ^ n" 380 using power_inverse [of a] by (simp add: divide_inverse) 381 382end 383 384context field 385begin 386 387lemma power_divide [field_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n" 388 by (induct n) simp_all 389 390end 391 392 393subsection \<open>Exponentiation on ordered types\<close> 394 395context linordered_semidom 396begin 397 398lemma zero_less_power [simp]: "0 < a \<Longrightarrow> 0 < a ^ n" 399 by (induct n) simp_all 400 401lemma zero_le_power [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n" 402 by (induct n) simp_all 403 404lemma power_mono: "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n" 405 by (induct n) (auto intro: mult_mono order_trans [of 0 a b]) 406 407lemma one_le_power [simp]: "1 \<le> a \<Longrightarrow> 1 \<le> a ^ n" 408 using power_mono [of 1 a n] by simp 409 410lemma power_le_one: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ n \<le> 1" 411 using power_mono [of a 1 n] by simp 412 413lemma power_gt1_lemma: 414 assumes gt1: "1 < a" 415 shows "1 < a * a ^ n" 416proof - 417 from gt1 have "0 \<le> a" 418 by (fact order_trans [OF zero_le_one less_imp_le]) 419 from gt1 have "1 * 1 < a * 1" by simp 420 also from gt1 have "\<dots> \<le> a * a ^ n" 421 by (simp only: mult_mono \<open>0 \<le> a\<close> one_le_power order_less_imp_le zero_le_one order_refl) 422 finally show ?thesis by simp 423qed 424 425lemma power_gt1: "1 < a \<Longrightarrow> 1 < a ^ Suc n" 426 by (simp add: power_gt1_lemma) 427 428lemma one_less_power [simp]: "1 < a \<Longrightarrow> 0 < n \<Longrightarrow> 1 < a ^ n" 429 by (cases n) (simp_all add: power_gt1_lemma) 430 431lemma power_le_imp_le_exp: 432 assumes gt1: "1 < a" 433 shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n" 434proof (induct m arbitrary: n) 435 case 0 436 show ?case by simp 437next 438 case (Suc m) 439 show ?case 440 proof (cases n) 441 case 0 442 with Suc have "a * a ^ m \<le> 1" by simp 443 with gt1 show ?thesis 444 by (force simp only: power_gt1_lemma not_less [symmetric]) 445 next 446 case (Suc n) 447 with Suc.prems Suc.hyps show ?thesis 448 by (force dest: mult_left_le_imp_le simp add: less_trans [OF zero_less_one gt1]) 449 qed 450qed 451 452lemma of_nat_zero_less_power_iff [simp]: "of_nat x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0" 453 by (induct n) auto 454 455text \<open>Surely we can strengthen this? It holds for \<open>0<a<1\<close> too.\<close> 456lemma power_inject_exp [simp]: "1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n" 457 by (force simp add: order_antisym power_le_imp_le_exp) 458 459text \<open> 460 Can relax the first premise to @{term "0<a"} in the case of the 461 natural numbers. 462\<close> 463lemma power_less_imp_less_exp: "1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n" 464 by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] power_le_imp_le_exp) 465 466lemma power_strict_mono [rule_format]: "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n" 467 by (induct n) (auto simp: mult_strict_mono le_less_trans [of 0 a b]) 468 469text\<open>Lemma for \<open>power_strict_decreasing\<close>\<close> 470lemma power_Suc_less: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n" 471 by (induct n) (auto simp: mult_strict_left_mono) 472 473lemma power_strict_decreasing [rule_format]: "n < N \<Longrightarrow> 0 < a \<Longrightarrow> a < 1 \<longrightarrow> a ^ N < a ^ n" 474proof (induct N) 475 case 0 476 then show ?case by simp 477next 478 case (Suc N) 479 then show ?case 480 apply (auto simp add: power_Suc_less less_Suc_eq) 481 apply (subgoal_tac "a * a^N < 1 * a^n") 482 apply simp 483 apply (rule mult_strict_mono) 484 apply auto 485 done 486qed 487 488text \<open>Proof resembles that of \<open>power_strict_decreasing\<close>.\<close> 489lemma power_decreasing: "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ N \<le> a ^ n" 490proof (induct N) 491 case 0 492 then show ?case by simp 493next 494 case (Suc N) 495 then show ?case 496 apply (auto simp add: le_Suc_eq) 497 apply (subgoal_tac "a * a^N \<le> 1 * a^n") 498 apply simp 499 apply (rule mult_mono) 500 apply auto 501 done 502qed 503 504lemma power_Suc_less_one: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1" 505 using power_strict_decreasing [of 0 "Suc n" a] by simp 506 507text \<open>Proof again resembles that of \<open>power_strict_decreasing\<close>.\<close> 508lemma power_increasing: "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N" 509proof (induct N) 510 case 0 511 then show ?case by simp 512next 513 case (Suc N) 514 then show ?case 515 apply (auto simp add: le_Suc_eq) 516 apply (subgoal_tac "1 * a^n \<le> a * a^N") 517 apply simp 518 apply (rule mult_mono) 519 apply (auto simp add: order_trans [OF zero_le_one]) 520 done 521qed 522 523text \<open>Lemma for \<open>power_strict_increasing\<close>.\<close> 524lemma power_less_power_Suc: "1 < a \<Longrightarrow> a ^ n < a * a ^ n" 525 by (induct n) (auto simp: mult_strict_left_mono less_trans [OF zero_less_one]) 526 527lemma power_strict_increasing: "n < N \<Longrightarrow> 1 < a \<Longrightarrow> a ^ n < a ^ N" 528proof (induct N) 529 case 0 530 then show ?case by simp 531next 532 case (Suc N) 533 then show ?case 534 apply (auto simp add: power_less_power_Suc less_Suc_eq) 535 apply (subgoal_tac "1 * a^n < a * a^N") 536 apply simp 537 apply (rule mult_strict_mono) 538 apply (auto simp add: less_trans [OF zero_less_one] less_imp_le) 539 done 540qed 541 542lemma power_increasing_iff [simp]: "1 < b \<Longrightarrow> b ^ x \<le> b ^ y \<longleftrightarrow> x \<le> y" 543 by (blast intro: power_le_imp_le_exp power_increasing less_imp_le) 544 545lemma power_strict_increasing_iff [simp]: "1 < b \<Longrightarrow> b ^ x < b ^ y \<longleftrightarrow> x < y" 546 by (blast intro: power_less_imp_less_exp power_strict_increasing) 547 548lemma power_le_imp_le_base: 549 assumes le: "a ^ Suc n \<le> b ^ Suc n" 550 and "0 \<le> b" 551 shows "a \<le> b" 552proof (rule ccontr) 553 assume "\<not> ?thesis" 554 then have "b < a" by (simp only: linorder_not_le) 555 then have "b ^ Suc n < a ^ Suc n" 556 by (simp only: assms(2) power_strict_mono) 557 with le show False 558 by (simp add: linorder_not_less [symmetric]) 559qed 560 561lemma power_less_imp_less_base: 562 assumes less: "a ^ n < b ^ n" 563 assumes nonneg: "0 \<le> b" 564 shows "a < b" 565proof (rule contrapos_pp [OF less]) 566 assume "\<not> ?thesis" 567 then have "b \<le> a" by (simp only: linorder_not_less) 568 from this nonneg have "b ^ n \<le> a ^ n" by (rule power_mono) 569 then show "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less) 570qed 571 572lemma power_inject_base: "a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b" 573 by (blast intro: power_le_imp_le_base antisym eq_refl sym) 574 575lemma power_eq_imp_eq_base: "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b" 576 by (cases n) (simp_all del: power_Suc, rule power_inject_base) 577 578lemma power_eq_iff_eq_base: "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b" 579 using power_eq_imp_eq_base [of a n b] by auto 580 581lemma power2_le_imp_le: "x\<^sup>2 \<le> y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y" 582 unfolding numeral_2_eq_2 by (rule power_le_imp_le_base) 583 584lemma power2_less_imp_less: "x\<^sup>2 < y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y" 585 by (rule power_less_imp_less_base) 586 587lemma power2_eq_imp_eq: "x\<^sup>2 = y\<^sup>2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y" 588 unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp 589 590lemma power_Suc_le_self: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a" 591 using power_decreasing [of 1 "Suc n" a] by simp 592 593lemma power2_eq_iff_nonneg [simp]: 594 assumes "0 \<le> x" "0 \<le> y" 595 shows "(x ^ 2 = y ^ 2) \<longleftrightarrow> x = y" 596using assms power2_eq_imp_eq by blast 597 598lemma of_nat_less_numeral_power_cancel_iff[simp]: 599 "of_nat x < numeral i ^ n \<longleftrightarrow> x < numeral i ^ n" 600 using of_nat_less_iff[of x "numeral i ^ n", unfolded of_nat_numeral of_nat_power] . 601 602lemma of_nat_le_numeral_power_cancel_iff[simp]: 603 "of_nat x \<le> numeral i ^ n \<longleftrightarrow> x \<le> numeral i ^ n" 604 using of_nat_le_iff[of x "numeral i ^ n", unfolded of_nat_numeral of_nat_power] . 605 606lemma numeral_power_less_of_nat_cancel_iff[simp]: 607 "numeral i ^ n < of_nat x \<longleftrightarrow> numeral i ^ n < x" 608 using of_nat_less_iff[of "numeral i ^ n" x, unfolded of_nat_numeral of_nat_power] . 609 610lemma numeral_power_le_of_nat_cancel_iff[simp]: 611 "numeral i ^ n \<le> of_nat x \<longleftrightarrow> numeral i ^ n \<le> x" 612 using of_nat_le_iff[of "numeral i ^ n" x, unfolded of_nat_numeral of_nat_power] . 613 614lemma of_nat_le_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w \<le> of_nat x \<longleftrightarrow> b ^ w \<le> x" 615 by (metis of_nat_le_iff of_nat_power) 616 617lemma of_nat_power_le_of_nat_cancel_iff[simp]: "of_nat x \<le> (of_nat b) ^ w \<longleftrightarrow> x \<le> b ^ w" 618 by (metis of_nat_le_iff of_nat_power) 619 620lemma of_nat_less_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w < of_nat x \<longleftrightarrow> b ^ w < x" 621 by (metis of_nat_less_iff of_nat_power) 622 623lemma of_nat_power_less_of_nat_cancel_iff[simp]: "of_nat x < (of_nat b) ^ w \<longleftrightarrow> x < b ^ w" 624 by (metis of_nat_less_iff of_nat_power) 625 626end 627 628context linordered_ring_strict 629begin 630 631lemma sum_squares_eq_zero_iff: "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 632 by (simp add: add_nonneg_eq_0_iff) 633 634lemma sum_squares_le_zero_iff: "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0" 635 by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff) 636 637lemma sum_squares_gt_zero_iff: "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0" 638 by (simp add: not_le [symmetric] sum_squares_le_zero_iff) 639 640end 641 642context linordered_idom 643begin 644 645lemma zero_le_power2 [simp]: "0 \<le> a\<^sup>2" 646 by (simp add: power2_eq_square) 647 648lemma zero_less_power2 [simp]: "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0" 649 by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) 650 651lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0" 652 by (force simp add: power2_eq_square mult_less_0_iff) 653 654lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" \<comment> \<open>FIXME simp?\<close> 655 by (induct n) (simp_all add: abs_mult) 656 657lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n" 658 by (induct n) (simp_all add: sgn_mult) 659 660lemma abs_power_minus [simp]: "\<bar>(- a) ^ n\<bar> = \<bar>a ^ n\<bar>" 661 by (simp add: power_abs) 662 663lemma zero_less_power_abs_iff [simp]: "0 < \<bar>a\<bar> ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0" 664proof (induct n) 665 case 0 666 show ?case by simp 667next 668 case Suc 669 then show ?case by (auto simp: zero_less_mult_iff) 670qed 671 672lemma zero_le_power_abs [simp]: "0 \<le> \<bar>a\<bar> ^ n" 673 by (rule zero_le_power [OF abs_ge_zero]) 674 675lemma power2_less_eq_zero_iff [simp]: "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0" 676 by (simp add: le_less) 677 678lemma abs_power2 [simp]: "\<bar>a\<^sup>2\<bar> = a\<^sup>2" 679 by (simp add: power2_eq_square) 680 681lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2" 682 by (simp add: power2_eq_square) 683 684lemma odd_power_less_zero: "a < 0 \<Longrightarrow> a ^ Suc (2 * n) < 0" 685proof (induct n) 686 case 0 687 then show ?case by simp 688next 689 case (Suc n) 690 have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 691 by (simp add: ac_simps power_add power2_eq_square) 692 then show ?case 693 by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg) 694qed 695 696lemma odd_0_le_power_imp_0_le: "0 \<le> a ^ Suc (2 * n) \<Longrightarrow> 0 \<le> a" 697 using odd_power_less_zero [of a n] 698 by (force simp add: linorder_not_less [symmetric]) 699 700lemma zero_le_even_power'[simp]: "0 \<le> a ^ (2 * n)" 701proof (induct n) 702 case 0 703 show ?case by simp 704next 705 case (Suc n) 706 have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 707 by (simp add: ac_simps power_add power2_eq_square) 708 then show ?case 709 by (simp add: Suc zero_le_mult_iff) 710qed 711 712lemma sum_power2_ge_zero: "0 \<le> x\<^sup>2 + y\<^sup>2" 713 by (intro add_nonneg_nonneg zero_le_power2) 714 715lemma not_sum_power2_lt_zero: "\<not> x\<^sup>2 + y\<^sup>2 < 0" 716 unfolding not_less by (rule sum_power2_ge_zero) 717 718lemma sum_power2_eq_zero_iff: "x\<^sup>2 + y\<^sup>2 = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 719 unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff) 720 721lemma sum_power2_le_zero_iff: "x\<^sup>2 + y\<^sup>2 \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0" 722 by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero) 723 724lemma sum_power2_gt_zero_iff: "0 < x\<^sup>2 + y\<^sup>2 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0" 725 unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) 726 727lemma abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> x\<^sup>2 \<le> y\<^sup>2" 728 (is "?lhs \<longleftrightarrow> ?rhs") 729proof 730 assume ?lhs 731 then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono) simp 732 then show ?rhs by simp 733next 734 assume ?rhs 735 then show ?lhs 736 by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero]) 737qed 738 739lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> \<bar>x\<bar> \<le> 1" 740 using abs_le_square_iff [of x 1] by simp 741 742lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> \<bar>x\<bar> = 1" 743 by (auto simp add: abs_if power2_eq_1_iff) 744 745lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> \<bar>x\<bar> < 1" 746 using abs_square_eq_1 [of x] abs_square_le_1 [of x] by (auto simp add: le_less) 747 748lemma square_le_1: 749 assumes "- 1 \<le> x" "x \<le> 1" 750 shows "x\<^sup>2 \<le> 1" 751 using assms 752 by (metis add.inverse_inverse linear mult_le_one neg_equal_0_iff_equal neg_le_iff_le power2_eq_square power_minus_Bit0) 753 754end 755 756 757subsection \<open>Miscellaneous rules\<close> 758 759lemma (in linordered_semidom) self_le_power: "1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n" 760 using power_increasing [of 1 n a] power_one_right [of a] by auto 761 762lemma (in power) power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))" 763 unfolding One_nat_def by (cases m) simp_all 764 765lemma (in comm_semiring_1) power2_sum: "(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y" 766 by (simp add: algebra_simps power2_eq_square mult_2_right) 767 768context comm_ring_1 769begin 770 771lemma power2_diff: "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y" 772 by (simp add: algebra_simps power2_eq_square mult_2_right) 773 774lemma power2_commute: "(x - y)\<^sup>2 = (y - x)\<^sup>2" 775 by (simp add: algebra_simps power2_eq_square) 776 777lemma minus_power_mult_self: "(- a) ^ n * (- a) ^ n = a ^ (2 * n)" 778 by (simp add: power_mult_distrib [symmetric]) 779 (simp add: power2_eq_square [symmetric] power_mult [symmetric]) 780 781lemma minus_one_mult_self [simp]: "(- 1) ^ n * (- 1) ^ n = 1" 782 using minus_power_mult_self [of 1 n] by simp 783 784lemma left_minus_one_mult_self [simp]: "(- 1) ^ n * ((- 1) ^ n * a) = a" 785 by (simp add: mult.assoc [symmetric]) 786 787end 788 789text \<open>Simprules for comparisons where common factors can be cancelled.\<close> 790 791lemmas zero_compare_simps = 792 add_strict_increasing add_strict_increasing2 add_increasing 793 zero_le_mult_iff zero_le_divide_iff 794 zero_less_mult_iff zero_less_divide_iff 795 mult_le_0_iff divide_le_0_iff 796 mult_less_0_iff divide_less_0_iff 797 zero_le_power2 power2_less_0 798 799 800subsection \<open>Exponentiation for the Natural Numbers\<close> 801 802lemma nat_one_le_power [simp]: "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n" 803 by (rule one_le_power [of i n, unfolded One_nat_def]) 804 805lemma nat_zero_less_power_iff [simp]: "x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0" 806 for x :: nat 807 by (induct n) auto 808 809lemma nat_power_eq_Suc_0_iff [simp]: "x ^ m = Suc 0 \<longleftrightarrow> m = 0 \<or> x = Suc 0" 810 by (induct m) auto 811 812lemma power_Suc_0 [simp]: "Suc 0 ^ n = Suc 0" 813 by simp 814 815text \<open> 816 Valid for the naturals, but what if \<open>0 < i < 1\<close>? Premises cannot be 817 weakened: consider the case where \<open>i = 0\<close>, \<open>m = 1\<close> and \<open>n = 0\<close>. 818\<close> 819 820lemma nat_power_less_imp_less: 821 fixes i :: nat 822 assumes nonneg: "0 < i" 823 assumes less: "i ^ m < i ^ n" 824 shows "m < n" 825proof (cases "i = 1") 826 case True 827 with less power_one [where 'a = nat] show ?thesis by simp 828next 829 case False 830 with nonneg have "1 < i" by auto 831 from power_strict_increasing_iff [OF this] less show ?thesis .. 832qed 833 834lemma power_dvd_imp_le: "i ^ m dvd i ^ n \<Longrightarrow> 1 < i \<Longrightarrow> m \<le> n" 835 for i m n :: nat 836 apply (rule power_le_imp_le_exp) 837 apply assumption 838 apply (erule dvd_imp_le) 839 apply simp 840 done 841 842lemma power2_nat_le_eq_le: "m\<^sup>2 \<le> n\<^sup>2 \<longleftrightarrow> m \<le> n" 843 for m n :: nat 844 by (auto intro: power2_le_imp_le power_mono) 845 846lemma power2_nat_le_imp_le: 847 fixes m n :: nat 848 assumes "m\<^sup>2 \<le> n" 849 shows "m \<le> n" 850proof (cases m) 851 case 0 852 then show ?thesis by simp 853next 854 case (Suc k) 855 show ?thesis 856 proof (rule ccontr) 857 assume "\<not> ?thesis" 858 then have "n < m" by simp 859 with assms Suc show False 860 by (simp add: power2_eq_square) 861 qed 862qed 863 864lemma ex_power_ivl1: fixes b k :: nat assumes "b \<ge> 2" 865shows "k \<ge> 1 \<Longrightarrow> \<exists>n. b^n \<le> k \<and> k < b^(n+1)" (is "_ \<Longrightarrow> \<exists>n. ?P k n") 866proof(induction k) 867 case 0 thus ?case by simp 868next 869 case (Suc k) 870 show ?case 871 proof cases 872 assume "k=0" 873 hence "?P (Suc k) 0" using assms by simp 874 thus ?case .. 875 next 876 assume "k\<noteq>0" 877 with Suc obtain n where IH: "?P k n" by auto 878 show ?case 879 proof (cases "k = b^(n+1) - 1") 880 case True 881 hence "?P (Suc k) (n+1)" using assms 882 by (simp add: power_less_power_Suc) 883 thus ?thesis .. 884 next 885 case False 886 hence "?P (Suc k) n" using IH by auto 887 thus ?thesis .. 888 qed 889 qed 890qed 891 892lemma ex_power_ivl2: fixes b k :: nat assumes "b \<ge> 2" "k \<ge> 2" 893shows "\<exists>n. b^n < k \<and> k \<le> b^(n+1)" 894proof - 895 have "1 \<le> k - 1" using assms(2) by arith 896 from ex_power_ivl1[OF assms(1) this] 897 obtain n where "b ^ n \<le> k - 1 \<and> k - 1 < b ^ (n + 1)" .. 898 hence "b^n < k \<and> k \<le> b^(n+1)" using assms by auto 899 thus ?thesis .. 900qed 901 902 903subsubsection \<open>Cardinality of the Powerset\<close> 904 905lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2" 906 unfolding UNIV_bool by simp 907 908lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A" 909proof (induct rule: finite_induct) 910 case empty 911 show ?case by simp 912next 913 case (insert x A) 914 from \<open>x \<notin> A\<close> have disjoint: "Pow A \<inter> insert x ` Pow A = {}" by blast 915 from \<open>x \<notin> A\<close> have inj_on: "inj_on (insert x) (Pow A)" 916 unfolding inj_on_def by auto 917 918 have "card (Pow (insert x A)) = card (Pow A \<union> insert x ` Pow A)" 919 by (simp only: Pow_insert) 920 also have "\<dots> = card (Pow A) + card (insert x ` Pow A)" 921 by (rule card_Un_disjoint) (use \<open>finite A\<close> disjoint in simp_all) 922 also from inj_on have "card (insert x ` Pow A) = card (Pow A)" 923 by (rule card_image) 924 also have "\<dots> + \<dots> = 2 * \<dots>" by (simp add: mult_2) 925 also from insert(3) have "\<dots> = 2 ^ Suc (card A)" by simp 926 also from insert(1,2) have "Suc (card A) = card (insert x A)" 927 by (rule card_insert_disjoint [symmetric]) 928 finally show ?case . 929qed 930 931 932subsection \<open>Code generator tweak\<close> 933 934code_identifier 935 code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 936 937end 938