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