src/HOL/Power.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (22 months ago)
changeset 66695 91500c024c7f
parent 65057 799bbbb3a395
child 66912 a99a7cbf0fb5
permissions -rw-r--r--
tuned;
     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 comm_semiring_1
   178 begin
   179 
   180 text \<open>The divides relation.\<close>
   181 
   182 lemma le_imp_power_dvd:
   183   assumes "m \<le> n"
   184   shows "a ^ m dvd a ^ n"
   185 proof
   186   from assms have "a ^ n = a ^ (m + (n - m))" by simp
   187   also have "\<dots> = a ^ m * a ^ (n - m)" by (rule power_add)
   188   finally show "a ^ n = a ^ m * a ^ (n - m)" .
   189 qed
   190 
   191 lemma power_le_dvd: "a ^ n dvd b \<Longrightarrow> m \<le> n \<Longrightarrow> a ^ m dvd b"
   192   by (rule dvd_trans [OF le_imp_power_dvd])
   193 
   194 lemma dvd_power_same: "x dvd y \<Longrightarrow> x ^ n dvd y ^ n"
   195   by (induct n) (auto simp add: mult_dvd_mono)
   196 
   197 lemma dvd_power_le: "x dvd y \<Longrightarrow> m \<ge> n \<Longrightarrow> x ^ n dvd y ^ m"
   198   by (rule power_le_dvd [OF dvd_power_same])
   199 
   200 lemma dvd_power [simp]:
   201   fixes n :: nat
   202   assumes "n > 0 \<or> x = 1"
   203   shows "x dvd (x ^ n)"
   204   using assms
   205 proof
   206   assume "0 < n"
   207   then have "x ^ n = x ^ Suc (n - 1)" by simp
   208   then show "x dvd (x ^ n)" by simp
   209 next
   210   assume "x = 1"
   211   then show "x dvd (x ^ n)" by simp
   212 qed
   213 
   214 end
   215 
   216 context semiring_1_no_zero_divisors
   217 begin
   218 
   219 subclass power .
   220 
   221 lemma power_eq_0_iff [simp]: "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
   222   by (induct n) auto
   223 
   224 lemma power_not_zero: "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
   225   by (induct n) auto
   226 
   227 lemma zero_eq_power2 [simp]: "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"
   228   unfolding power2_eq_square by simp
   229 
   230 end
   231 
   232 context ring_1
   233 begin
   234 
   235 lemma power_minus: "(- a) ^ n = (- 1) ^ n * a ^ n"
   236 proof (induct n)
   237   case 0
   238   show ?case by simp
   239 next
   240   case (Suc n)
   241   then show ?case
   242     by (simp del: power_Suc add: power_Suc2 mult.assoc)
   243 qed
   244 
   245 lemma power_minus': "NO_MATCH 1 x \<Longrightarrow> (-x) ^ n = (-1)^n * x ^ n"
   246   by (rule power_minus)
   247 
   248 lemma power_minus_Bit0: "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)"
   249   by (induct k, simp_all only: numeral_class.numeral.simps power_add
   250     power_one_right mult_minus_left mult_minus_right minus_minus)
   251 
   252 lemma power_minus_Bit1: "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))"
   253   by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left)
   254 
   255 lemma power2_minus [simp]: "(- a)\<^sup>2 = a\<^sup>2"
   256   by (fact power_minus_Bit0)
   257 
   258 lemma power_minus1_even [simp]: "(- 1) ^ (2*n) = 1"
   259 proof (induct n)
   260   case 0
   261   show ?case by simp
   262 next
   263   case (Suc n)
   264   then show ?case by (simp add: power_add power2_eq_square)
   265 qed
   266 
   267 lemma power_minus1_odd: "(- 1) ^ Suc (2*n) = -1"
   268   by simp
   269 
   270 lemma power_minus_even [simp]: "(-a) ^ (2*n) = a ^ (2*n)"
   271   by (simp add: power_minus [of a])
   272 
   273 end
   274 
   275 context ring_1_no_zero_divisors
   276 begin
   277 
   278 lemma power2_eq_1_iff: "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
   279   using square_eq_1_iff [of a] by (simp add: power2_eq_square)
   280 
   281 end
   282 
   283 context idom
   284 begin
   285 
   286 lemma power2_eq_iff: "x\<^sup>2 = y\<^sup>2 \<longleftrightarrow> x = y \<or> x = - y"
   287   unfolding power2_eq_square by (rule square_eq_iff)
   288 
   289 end
   290 
   291 context algebraic_semidom
   292 begin
   293 
   294 lemma div_power: "b dvd a \<Longrightarrow> (a div b) ^ n = a ^ n div b ^ n"
   295   by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same)
   296 
   297 lemma is_unit_power_iff: "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
   298   by (induct n) (auto simp add: is_unit_mult_iff)
   299 
   300 lemma dvd_power_iff:
   301   assumes "x \<noteq> 0"
   302   shows   "x ^ m dvd x ^ n \<longleftrightarrow> is_unit x \<or> m \<le> n"
   303 proof
   304   assume *: "x ^ m dvd x ^ n"
   305   {
   306     assume "m > n"
   307     note *
   308     also have "x ^ n = x ^ n * 1" by simp
   309     also from \<open>m > n\<close> have "m = n + (m - n)" by simp
   310     also have "x ^ \<dots> = x ^ n * x ^ (m - n)" by (rule power_add)
   311     finally have "x ^ (m - n) dvd 1"
   312       by (subst (asm) dvd_times_left_cancel_iff) (insert assms, simp_all)
   313     with \<open>m > n\<close> have "is_unit x" by (simp add: is_unit_power_iff)
   314   }
   315   thus "is_unit x \<or> m \<le> n" by force
   316 qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd)
   317 
   318 
   319 end
   320 
   321 context normalization_semidom
   322 begin
   323 
   324 lemma normalize_power: "normalize (a ^ n) = normalize a ^ n"
   325   by (induct n) (simp_all add: normalize_mult)
   326 
   327 lemma unit_factor_power: "unit_factor (a ^ n) = unit_factor a ^ n"
   328   by (induct n) (simp_all add: unit_factor_mult)
   329 
   330 end
   331 
   332 context division_ring
   333 begin
   334 
   335 text \<open>Perhaps these should be simprules.\<close>
   336 lemma power_inverse [field_simps, divide_simps]: "inverse a ^ n = inverse (a ^ n)"
   337 proof (cases "a = 0")
   338   case True
   339   then show ?thesis by (simp add: power_0_left)
   340 next
   341   case False
   342   then have "inverse (a ^ n) = inverse a ^ n"
   343     by (induct n) (simp_all add: nonzero_inverse_mult_distrib power_commutes)
   344   then show ?thesis by simp
   345 qed
   346 
   347 lemma power_one_over [field_simps, divide_simps]: "(1 / a) ^ n = 1 / a ^ n"
   348   using power_inverse [of a] by (simp add: divide_inverse)
   349 
   350 end
   351 
   352 context field
   353 begin
   354 
   355 lemma power_diff:
   356   assumes "a \<noteq> 0"
   357   shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
   358   by (induct m n rule: diff_induct) (simp_all add: assms power_not_zero)
   359 
   360 lemma power_divide [field_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n"
   361   by (induct n) simp_all
   362 
   363 end
   364 
   365 
   366 subsection \<open>Exponentiation on ordered types\<close>
   367 
   368 context linordered_semidom
   369 begin
   370 
   371 lemma zero_less_power [simp]: "0 < a \<Longrightarrow> 0 < a ^ n"
   372   by (induct n) simp_all
   373 
   374 lemma zero_le_power [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
   375   by (induct n) simp_all
   376 
   377 lemma power_mono: "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n"
   378   by (induct n) (auto intro: mult_mono order_trans [of 0 a b])
   379 
   380 lemma one_le_power [simp]: "1 \<le> a \<Longrightarrow> 1 \<le> a ^ n"
   381   using power_mono [of 1 a n] by simp
   382 
   383 lemma power_le_one: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ n \<le> 1"
   384   using power_mono [of a 1 n] by simp
   385 
   386 lemma power_gt1_lemma:
   387   assumes gt1: "1 < a"
   388   shows "1 < a * a ^ n"
   389 proof -
   390   from gt1 have "0 \<le> a"
   391     by (fact order_trans [OF zero_le_one less_imp_le])
   392   from gt1 have "1 * 1 < a * 1" by simp
   393   also from gt1 have "\<dots> \<le> a * a ^ n"
   394     by (simp only: mult_mono \<open>0 \<le> a\<close> one_le_power order_less_imp_le zero_le_one order_refl)
   395   finally show ?thesis by simp
   396 qed
   397 
   398 lemma power_gt1: "1 < a \<Longrightarrow> 1 < a ^ Suc n"
   399   by (simp add: power_gt1_lemma)
   400 
   401 lemma one_less_power [simp]: "1 < a \<Longrightarrow> 0 < n \<Longrightarrow> 1 < a ^ n"
   402   by (cases n) (simp_all add: power_gt1_lemma)
   403 
   404 lemma power_le_imp_le_exp:
   405   assumes gt1: "1 < a"
   406   shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n"
   407 proof (induct m arbitrary: n)
   408   case 0
   409   show ?case by simp
   410 next
   411   case (Suc m)
   412   show ?case
   413   proof (cases n)
   414     case 0
   415     with Suc have "a * a ^ m \<le> 1" by simp
   416     with gt1 show ?thesis
   417       by (force simp only: power_gt1_lemma not_less [symmetric])
   418   next
   419     case (Suc n)
   420     with Suc.prems Suc.hyps show ?thesis
   421       by (force dest: mult_left_le_imp_le simp add: less_trans [OF zero_less_one gt1])
   422   qed
   423 qed
   424 
   425 lemma of_nat_zero_less_power_iff [simp]: "of_nat x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
   426   by (induct n) auto
   427 
   428 text \<open>Surely we can strengthen this? It holds for \<open>0<a<1\<close> too.\<close>
   429 lemma power_inject_exp [simp]: "1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
   430   by (force simp add: order_antisym power_le_imp_le_exp)
   431 
   432 text \<open>
   433   Can relax the first premise to @{term "0<a"} in the case of the
   434   natural numbers.
   435 \<close>
   436 lemma power_less_imp_less_exp: "1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n"
   437   by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] power_le_imp_le_exp)
   438 
   439 lemma power_strict_mono [rule_format]: "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n"
   440   by (induct n) (auto simp: mult_strict_mono le_less_trans [of 0 a b])
   441 
   442 text\<open>Lemma for \<open>power_strict_decreasing\<close>\<close>
   443 lemma power_Suc_less: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n"
   444   by (induct n) (auto simp: mult_strict_left_mono)
   445 
   446 lemma power_strict_decreasing [rule_format]: "n < N \<Longrightarrow> 0 < a \<Longrightarrow> a < 1 \<longrightarrow> a ^ N < a ^ n"
   447 proof (induct N)
   448   case 0
   449   then show ?case by simp
   450 next
   451   case (Suc N)
   452   then show ?case
   453     apply (auto simp add: power_Suc_less less_Suc_eq)
   454     apply (subgoal_tac "a * a^N < 1 * a^n")
   455      apply simp
   456     apply (rule mult_strict_mono)
   457        apply auto
   458     done
   459 qed
   460 
   461 text \<open>Proof resembles that of \<open>power_strict_decreasing\<close>.\<close>
   462 lemma power_decreasing: "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ N \<le> a ^ n"
   463 proof (induct N)
   464   case 0
   465   then show ?case by simp
   466 next
   467   case (Suc N)
   468   then show ?case
   469     apply (auto simp add: le_Suc_eq)
   470     apply (subgoal_tac "a * a^N \<le> 1 * a^n")
   471      apply simp
   472     apply (rule mult_mono)
   473        apply auto
   474     done
   475 qed
   476 
   477 lemma power_Suc_less_one: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1"
   478   using power_strict_decreasing [of 0 "Suc n" a] by simp
   479 
   480 text \<open>Proof again resembles that of \<open>power_strict_decreasing\<close>.\<close>
   481 lemma power_increasing: "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
   482 proof (induct N)
   483   case 0
   484   then show ?case by simp
   485 next
   486   case (Suc N)
   487   then show ?case
   488     apply (auto simp add: le_Suc_eq)
   489     apply (subgoal_tac "1 * a^n \<le> a * a^N")
   490      apply simp
   491     apply (rule mult_mono)
   492        apply (auto simp add: order_trans [OF zero_le_one])
   493     done
   494 qed
   495 
   496 text \<open>Lemma for \<open>power_strict_increasing\<close>.\<close>
   497 lemma power_less_power_Suc: "1 < a \<Longrightarrow> a ^ n < a * a ^ n"
   498   by (induct n) (auto simp: mult_strict_left_mono less_trans [OF zero_less_one])
   499 
   500 lemma power_strict_increasing: "n < N \<Longrightarrow> 1 < a \<Longrightarrow> a ^ n < a ^ N"
   501 proof (induct N)
   502   case 0
   503   then show ?case by simp
   504 next
   505   case (Suc N)
   506   then show ?case
   507     apply (auto simp add: power_less_power_Suc less_Suc_eq)
   508     apply (subgoal_tac "1 * a^n < a * a^N")
   509      apply simp
   510     apply (rule mult_strict_mono)
   511     apply (auto simp add: less_trans [OF zero_less_one] less_imp_le)
   512     done
   513 qed
   514 
   515 lemma power_increasing_iff [simp]: "1 < b \<Longrightarrow> b ^ x \<le> b ^ y \<longleftrightarrow> x \<le> y"
   516   by (blast intro: power_le_imp_le_exp power_increasing less_imp_le)
   517 
   518 lemma power_strict_increasing_iff [simp]: "1 < b \<Longrightarrow> b ^ x < b ^ y \<longleftrightarrow> x < y"
   519   by (blast intro: power_less_imp_less_exp power_strict_increasing)
   520 
   521 lemma power_le_imp_le_base:
   522   assumes le: "a ^ Suc n \<le> b ^ Suc n"
   523     and "0 \<le> b"
   524   shows "a \<le> b"
   525 proof (rule ccontr)
   526   assume "\<not> ?thesis"
   527   then have "b < a" by (simp only: linorder_not_le)
   528   then have "b ^ Suc n < a ^ Suc n"
   529     by (simp only: assms(2) power_strict_mono)
   530   with le show False
   531     by (simp add: linorder_not_less [symmetric])
   532 qed
   533 
   534 lemma power_less_imp_less_base:
   535   assumes less: "a ^ n < b ^ n"
   536   assumes nonneg: "0 \<le> b"
   537   shows "a < b"
   538 proof (rule contrapos_pp [OF less])
   539   assume "\<not> ?thesis"
   540   then have "b \<le> a" by (simp only: linorder_not_less)
   541   from this nonneg have "b ^ n \<le> a ^ n" by (rule power_mono)
   542   then show "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less)
   543 qed
   544 
   545 lemma power_inject_base: "a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b"
   546   by (blast intro: power_le_imp_le_base antisym eq_refl sym)
   547 
   548 lemma power_eq_imp_eq_base: "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b"
   549   by (cases n) (simp_all del: power_Suc, rule power_inject_base)
   550 
   551 lemma power_eq_iff_eq_base: "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b"
   552   using power_eq_imp_eq_base [of a n b] by auto
   553 
   554 lemma power2_le_imp_le: "x\<^sup>2 \<le> y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
   555   unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
   556 
   557 lemma power2_less_imp_less: "x\<^sup>2 < y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
   558   by (rule power_less_imp_less_base)
   559 
   560 lemma power2_eq_imp_eq: "x\<^sup>2 = y\<^sup>2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
   561   unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
   562 
   563 lemma power_Suc_le_self: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
   564   using power_decreasing [of 1 "Suc n" a] by simp
   565 
   566 lemma power2_eq_iff_nonneg [simp]:
   567   assumes "0 \<le> x" "0 \<le> y"
   568   shows "(x ^ 2 = y ^ 2) \<longleftrightarrow> x = y"
   569 using assms power2_eq_imp_eq by blast
   570 
   571 end
   572 
   573 context linordered_ring_strict
   574 begin
   575 
   576 lemma sum_squares_eq_zero_iff: "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   577   by (simp add: add_nonneg_eq_0_iff)
   578 
   579 lemma sum_squares_le_zero_iff: "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   580   by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
   581 
   582 lemma sum_squares_gt_zero_iff: "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   583   by (simp add: not_le [symmetric] sum_squares_le_zero_iff)
   584 
   585 end
   586 
   587 context linordered_idom
   588 begin
   589 
   590 lemma zero_le_power2 [simp]: "0 \<le> a\<^sup>2"
   591   by (simp add: power2_eq_square)
   592 
   593 lemma zero_less_power2 [simp]: "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0"
   594   by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   595 
   596 lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
   597   by (force simp add: power2_eq_square mult_less_0_iff)
   598 
   599 lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" -- \<open>FIXME simp?\<close>
   600   by (induct n) (simp_all add: abs_mult)
   601 
   602 lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n"
   603   by (induct n) (simp_all add: sgn_mult)
   604 
   605 lemma abs_power_minus [simp]: "\<bar>(- a) ^ n\<bar> = \<bar>a ^ n\<bar>"
   606   by (simp add: power_abs)
   607 
   608 lemma zero_less_power_abs_iff [simp]: "0 < \<bar>a\<bar> ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
   609 proof (induct n)
   610   case 0
   611   show ?case by simp
   612 next
   613   case Suc
   614   then show ?case by (auto simp: zero_less_mult_iff)
   615 qed
   616 
   617 lemma zero_le_power_abs [simp]: "0 \<le> \<bar>a\<bar> ^ n"
   618   by (rule zero_le_power [OF abs_ge_zero])
   619 
   620 lemma power2_less_eq_zero_iff [simp]: "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
   621   by (simp add: le_less)
   622 
   623 lemma abs_power2 [simp]: "\<bar>a\<^sup>2\<bar> = a\<^sup>2"
   624   by (simp add: power2_eq_square)
   625 
   626 lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2"
   627   by (simp add: power2_eq_square)
   628 
   629 lemma odd_power_less_zero: "a < 0 \<Longrightarrow> a ^ Suc (2 * n) < 0"
   630 proof (induct n)
   631   case 0
   632   then show ?case by simp
   633 next
   634   case (Suc n)
   635   have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
   636     by (simp add: ac_simps power_add power2_eq_square)
   637   then show ?case
   638     by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
   639 qed
   640 
   641 lemma odd_0_le_power_imp_0_le: "0 \<le> a ^ Suc (2 * n) \<Longrightarrow> 0 \<le> a"
   642   using odd_power_less_zero [of a n]
   643   by (force simp add: linorder_not_less [symmetric])
   644 
   645 lemma zero_le_even_power'[simp]: "0 \<le> a ^ (2 * n)"
   646 proof (induct n)
   647   case 0
   648   show ?case by simp
   649 next
   650   case (Suc n)
   651   have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
   652     by (simp add: ac_simps power_add power2_eq_square)
   653   then show ?case
   654     by (simp add: Suc zero_le_mult_iff)
   655 qed
   656 
   657 lemma sum_power2_ge_zero: "0 \<le> x\<^sup>2 + y\<^sup>2"
   658   by (intro add_nonneg_nonneg zero_le_power2)
   659 
   660 lemma not_sum_power2_lt_zero: "\<not> x\<^sup>2 + y\<^sup>2 < 0"
   661   unfolding not_less by (rule sum_power2_ge_zero)
   662 
   663 lemma sum_power2_eq_zero_iff: "x\<^sup>2 + y\<^sup>2 = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   664   unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff)
   665 
   666 lemma sum_power2_le_zero_iff: "x\<^sup>2 + y\<^sup>2 \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   667   by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero)
   668 
   669 lemma sum_power2_gt_zero_iff: "0 < x\<^sup>2 + y\<^sup>2 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   670   unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff)
   671 
   672 lemma abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> x\<^sup>2 \<le> y\<^sup>2"
   673   (is "?lhs \<longleftrightarrow> ?rhs")
   674 proof
   675   assume ?lhs
   676   then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono) simp
   677   then show ?rhs by simp
   678 next
   679   assume ?rhs
   680   then show ?lhs
   681     by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
   682 qed
   683 
   684 lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> \<bar>x\<bar> \<le> 1"
   685   using abs_le_square_iff [of x 1] by simp
   686 
   687 lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> \<bar>x\<bar> = 1"
   688   by (auto simp add: abs_if power2_eq_1_iff)
   689 
   690 lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> \<bar>x\<bar> < 1"
   691   using  abs_square_eq_1 [of x] abs_square_le_1 [of x] by (auto simp add: le_less)
   692 
   693 end
   694 
   695 
   696 subsection \<open>Miscellaneous rules\<close>
   697 
   698 lemma (in linordered_semidom) self_le_power: "1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n"
   699   using power_increasing [of 1 n a] power_one_right [of a] by auto
   700 
   701 lemma (in power) power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
   702   unfolding One_nat_def by (cases m) simp_all
   703 
   704 lemma (in comm_semiring_1) power2_sum: "(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y"
   705   by (simp add: algebra_simps power2_eq_square mult_2_right)
   706 
   707 context comm_ring_1
   708 begin
   709 
   710 lemma power2_diff: "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
   711   by (simp add: algebra_simps power2_eq_square mult_2_right)
   712 
   713 lemma power2_commute: "(x - y)\<^sup>2 = (y - x)\<^sup>2"
   714   by (simp add: algebra_simps power2_eq_square)
   715 
   716 lemma minus_power_mult_self: "(- a) ^ n * (- a) ^ n = a ^ (2 * n)"
   717   by (simp add: power_mult_distrib [symmetric])
   718     (simp add: power2_eq_square [symmetric] power_mult [symmetric])
   719 
   720 lemma minus_one_mult_self [simp]: "(- 1) ^ n * (- 1) ^ n = 1"
   721   using minus_power_mult_self [of 1 n] by simp
   722 
   723 lemma left_minus_one_mult_self [simp]: "(- 1) ^ n * ((- 1) ^ n * a) = a"
   724   by (simp add: mult.assoc [symmetric])
   725 
   726 end
   727 
   728 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
   729 
   730 lemmas zero_compare_simps =
   731   add_strict_increasing add_strict_increasing2 add_increasing
   732   zero_le_mult_iff zero_le_divide_iff
   733   zero_less_mult_iff zero_less_divide_iff
   734   mult_le_0_iff divide_le_0_iff
   735   mult_less_0_iff divide_less_0_iff
   736   zero_le_power2 power2_less_0
   737 
   738 
   739 subsection \<open>Exponentiation for the Natural Numbers\<close>
   740 
   741 lemma nat_one_le_power [simp]: "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n"
   742   by (rule one_le_power [of i n, unfolded One_nat_def])
   743 
   744 lemma nat_zero_less_power_iff [simp]: "x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
   745   for x :: nat
   746   by (induct n) auto
   747 
   748 lemma nat_power_eq_Suc_0_iff [simp]: "x ^ m = Suc 0 \<longleftrightarrow> m = 0 \<or> x = Suc 0"
   749   by (induct m) auto
   750 
   751 lemma power_Suc_0 [simp]: "Suc 0 ^ n = Suc 0"
   752   by simp
   753 
   754 text \<open>
   755   Valid for the naturals, but what if \<open>0 < i < 1\<close>? Premises cannot be
   756   weakened: consider the case where \<open>i = 0\<close>, \<open>m = 1\<close> and \<open>n = 0\<close>.
   757 \<close>
   758 
   759 lemma nat_power_less_imp_less:
   760   fixes i :: nat
   761   assumes nonneg: "0 < i"
   762   assumes less: "i ^ m < i ^ n"
   763   shows "m < n"
   764 proof (cases "i = 1")
   765   case True
   766   with less power_one [where 'a = nat] show ?thesis by simp
   767 next
   768   case False
   769   with nonneg have "1 < i" by auto
   770   from power_strict_increasing_iff [OF this] less show ?thesis ..
   771 qed
   772 
   773 lemma power_dvd_imp_le: "i ^ m dvd i ^ n \<Longrightarrow> 1 < i \<Longrightarrow> m \<le> n"
   774   for i m n :: nat
   775   apply (rule power_le_imp_le_exp)
   776    apply assumption
   777   apply (erule dvd_imp_le)
   778   apply simp
   779   done
   780 
   781 lemma power2_nat_le_eq_le: "m\<^sup>2 \<le> n\<^sup>2 \<longleftrightarrow> m \<le> n"
   782   for m n :: nat
   783   by (auto intro: power2_le_imp_le power_mono)
   784 
   785 lemma power2_nat_le_imp_le:
   786   fixes m n :: nat
   787   assumes "m\<^sup>2 \<le> n"
   788   shows "m \<le> n"
   789 proof (cases m)
   790   case 0
   791   then show ?thesis by simp
   792 next
   793   case (Suc k)
   794   show ?thesis
   795   proof (rule ccontr)
   796     assume "\<not> ?thesis"
   797     then have "n < m" by simp
   798     with assms Suc show False
   799       by (simp add: power2_eq_square)
   800   qed
   801 qed
   802 
   803 lemma ex_power_ivl1: fixes b k :: nat assumes "b \<ge> 2"
   804 shows "k \<ge> 1 \<Longrightarrow> \<exists>n. b^n \<le> k \<and> k < b^(n+1)" (is "_ \<Longrightarrow> \<exists>n. ?P k n")
   805 proof(induction k)
   806   case 0 thus ?case by simp
   807 next
   808   case (Suc k)
   809   show ?case
   810   proof cases
   811     assume "k=0"
   812     hence "?P (Suc k) 0" using assms by simp
   813     thus ?case ..
   814   next
   815     assume "k\<noteq>0"
   816     with Suc obtain n where IH: "?P k n" by auto
   817     show ?case
   818     proof (cases "k = b^(n+1) - 1")
   819       case True
   820       hence "?P (Suc k) (n+1)" using assms
   821         by (simp add: power_less_power_Suc)
   822       thus ?thesis ..
   823     next
   824       case False
   825       hence "?P (Suc k) n" using IH by auto
   826       thus ?thesis ..
   827     qed
   828   qed
   829 qed
   830 
   831 lemma ex_power_ivl2: fixes b k :: nat assumes "b \<ge> 2" "k \<ge> 2"
   832 shows "\<exists>n. b^n < k \<and> k \<le> b^(n+1)"
   833 proof -
   834   have "1 \<le> k - 1" using assms(2) by arith
   835   from ex_power_ivl1[OF assms(1) this]
   836   obtain n where "b ^ n \<le> k - 1 \<and> k - 1 < b ^ (n + 1)" ..
   837   hence "b^n < k \<and> k \<le> b^(n+1)" using assms by auto
   838   thus ?thesis ..
   839 qed
   840 
   841 
   842 subsubsection \<open>Cardinality of the Powerset\<close>
   843 
   844 lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
   845   unfolding UNIV_bool by simp
   846 
   847 lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
   848 proof (induct rule: finite_induct)
   849   case empty
   850   show ?case by simp
   851 next
   852   case (insert x A)
   853   from \<open>x \<notin> A\<close> have disjoint: "Pow A \<inter> insert x ` Pow A = {}" by blast
   854   from \<open>x \<notin> A\<close> have inj_on: "inj_on (insert x) (Pow A)"
   855     unfolding inj_on_def by auto
   856 
   857   have "card (Pow (insert x A)) = card (Pow A \<union> insert x ` Pow A)"
   858     by (simp only: Pow_insert)
   859   also have "\<dots> = card (Pow A) + card (insert x ` Pow A)"
   860     by (rule card_Un_disjoint) (use \<open>finite A\<close> disjoint in simp_all)
   861   also from inj_on have "card (insert x ` Pow A) = card (Pow A)"
   862     by (rule card_image)
   863   also have "\<dots> + \<dots> = 2 * \<dots>" by (simp add: mult_2)
   864   also from insert(3) have "\<dots> = 2 ^ Suc (card A)" by simp
   865   also from insert(1,2) have "Suc (card A) = card (insert x A)"
   866     by (rule card_insert_disjoint [symmetric])
   867   finally show ?case .
   868 qed
   869 
   870 
   871 subsection \<open>Code generator tweak\<close>
   872 
   873 code_identifier
   874   code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   875 
   876 end