src/HOL/Power.thy
author haftmann
Sat Dec 31 08:12:31 2016 +0100 (2016-12-31)
changeset 64715 33d5fa0ce6e5
parent 64065 40d440b75b00
child 64964 a0c985a57f7e
permissions -rw-r--r--
more elementary rules about div / mod on int
     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 end
   567 
   568 context linordered_ring_strict
   569 begin
   570 
   571 lemma sum_squares_eq_zero_iff: "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   572   by (simp add: add_nonneg_eq_0_iff)
   573 
   574 lemma sum_squares_le_zero_iff: "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   575   by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
   576 
   577 lemma sum_squares_gt_zero_iff: "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   578   by (simp add: not_le [symmetric] sum_squares_le_zero_iff)
   579 
   580 end
   581 
   582 context linordered_idom
   583 begin
   584 
   585 lemma zero_le_power2 [simp]: "0 \<le> a\<^sup>2"
   586   by (simp add: power2_eq_square)
   587 
   588 lemma zero_less_power2 [simp]: "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0"
   589   by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   590 
   591 lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
   592   by (force simp add: power2_eq_square mult_less_0_iff)
   593 
   594 lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" -- \<open>FIXME simp?\<close>
   595   by (induct n) (simp_all add: abs_mult)
   596 
   597 lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n"
   598   by (induct n) (simp_all add: sgn_mult)
   599     
   600 lemma abs_power_minus [simp]: "\<bar>(- a) ^ n\<bar> = \<bar>a ^ n\<bar>"
   601   by (simp add: power_abs)
   602 
   603 lemma zero_less_power_abs_iff [simp]: "0 < \<bar>a\<bar> ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
   604 proof (induct n)
   605   case 0
   606   show ?case by simp
   607 next
   608   case Suc
   609   then show ?case by (auto simp: zero_less_mult_iff)
   610 qed
   611 
   612 lemma zero_le_power_abs [simp]: "0 \<le> \<bar>a\<bar> ^ n"
   613   by (rule zero_le_power [OF abs_ge_zero])
   614 
   615 lemma power2_less_eq_zero_iff [simp]: "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
   616   by (simp add: le_less)
   617 
   618 lemma abs_power2 [simp]: "\<bar>a\<^sup>2\<bar> = a\<^sup>2"
   619   by (simp add: power2_eq_square)
   620 
   621 lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2"
   622   by (simp add: power2_eq_square)
   623 
   624 lemma odd_power_less_zero: "a < 0 \<Longrightarrow> a ^ Suc (2 * n) < 0"
   625 proof (induct n)
   626   case 0
   627   then show ?case by simp
   628 next
   629   case (Suc n)
   630   have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
   631     by (simp add: ac_simps power_add power2_eq_square)
   632   then show ?case
   633     by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
   634 qed
   635 
   636 lemma odd_0_le_power_imp_0_le: "0 \<le> a ^ Suc (2 * n) \<Longrightarrow> 0 \<le> a"
   637   using odd_power_less_zero [of a n]
   638   by (force simp add: linorder_not_less [symmetric])
   639 
   640 lemma zero_le_even_power'[simp]: "0 \<le> a ^ (2 * n)"
   641 proof (induct n)
   642   case 0
   643   show ?case by simp
   644 next
   645   case (Suc n)
   646   have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
   647     by (simp add: ac_simps power_add power2_eq_square)
   648   then show ?case
   649     by (simp add: Suc zero_le_mult_iff)
   650 qed
   651 
   652 lemma sum_power2_ge_zero: "0 \<le> x\<^sup>2 + y\<^sup>2"
   653   by (intro add_nonneg_nonneg zero_le_power2)
   654 
   655 lemma not_sum_power2_lt_zero: "\<not> x\<^sup>2 + y\<^sup>2 < 0"
   656   unfolding not_less by (rule sum_power2_ge_zero)
   657 
   658 lemma sum_power2_eq_zero_iff: "x\<^sup>2 + y\<^sup>2 = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   659   unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff)
   660 
   661 lemma sum_power2_le_zero_iff: "x\<^sup>2 + y\<^sup>2 \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   662   by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero)
   663 
   664 lemma sum_power2_gt_zero_iff: "0 < x\<^sup>2 + y\<^sup>2 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   665   unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff)
   666 
   667 lemma abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> x\<^sup>2 \<le> y\<^sup>2"
   668   (is "?lhs \<longleftrightarrow> ?rhs")
   669 proof
   670   assume ?lhs
   671   then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono) simp
   672   then show ?rhs by simp
   673 next
   674   assume ?rhs
   675   then show ?lhs
   676     by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
   677 qed
   678 
   679 lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> \<bar>x\<bar> \<le> 1"
   680   using abs_le_square_iff [of x 1] by simp
   681 
   682 lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> \<bar>x\<bar> = 1"
   683   by (auto simp add: abs_if power2_eq_1_iff)
   684 
   685 lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> \<bar>x\<bar> < 1"
   686   using  abs_square_eq_1 [of x] abs_square_le_1 [of x] by (auto simp add: le_less)
   687 
   688 end
   689 
   690 
   691 subsection \<open>Miscellaneous rules\<close>
   692 
   693 lemma (in linordered_semidom) self_le_power: "1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n"
   694   using power_increasing [of 1 n a] power_one_right [of a] by auto
   695 
   696 lemma (in power) power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
   697   unfolding One_nat_def by (cases m) simp_all
   698 
   699 lemma (in comm_semiring_1) power2_sum: "(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y"
   700   by (simp add: algebra_simps power2_eq_square mult_2_right)
   701 
   702 context comm_ring_1
   703 begin
   704 
   705 lemma power2_diff: "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
   706   by (simp add: algebra_simps power2_eq_square mult_2_right)
   707 
   708 lemma power2_commute: "(x - y)\<^sup>2 = (y - x)\<^sup>2"
   709   by (simp add: algebra_simps power2_eq_square)
   710 
   711 lemma minus_power_mult_self: "(- a) ^ n * (- a) ^ n = a ^ (2 * n)"
   712   by (simp add: power_mult_distrib [symmetric])
   713     (simp add: power2_eq_square [symmetric] power_mult [symmetric])
   714 
   715 lemma minus_one_mult_self [simp]: "(- 1) ^ n * (- 1) ^ n = 1"
   716   using minus_power_mult_self [of 1 n] by simp
   717 
   718 lemma left_minus_one_mult_self [simp]: "(- 1) ^ n * ((- 1) ^ n * a) = a"
   719   by (simp add: mult.assoc [symmetric])
   720 
   721 end
   722 
   723 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
   724 
   725 lemmas zero_compare_simps =
   726   add_strict_increasing add_strict_increasing2 add_increasing
   727   zero_le_mult_iff zero_le_divide_iff
   728   zero_less_mult_iff zero_less_divide_iff
   729   mult_le_0_iff divide_le_0_iff
   730   mult_less_0_iff divide_less_0_iff
   731   zero_le_power2 power2_less_0
   732 
   733 
   734 subsection \<open>Exponentiation for the Natural Numbers\<close>
   735 
   736 lemma nat_one_le_power [simp]: "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n"
   737   by (rule one_le_power [of i n, unfolded One_nat_def])
   738 
   739 lemma nat_zero_less_power_iff [simp]: "x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
   740   for x :: nat
   741   by (induct n) auto
   742 
   743 lemma nat_power_eq_Suc_0_iff [simp]: "x ^ m = Suc 0 \<longleftrightarrow> m = 0 \<or> x = Suc 0"
   744   by (induct m) auto
   745 
   746 lemma power_Suc_0 [simp]: "Suc 0 ^ n = Suc 0"
   747   by simp
   748 
   749 text \<open>
   750   Valid for the naturals, but what if \<open>0 < i < 1\<close>? Premises cannot be
   751   weakened: consider the case where \<open>i = 0\<close>, \<open>m = 1\<close> and \<open>n = 0\<close>.
   752 \<close>
   753 
   754 lemma nat_power_less_imp_less:
   755   fixes i :: nat
   756   assumes nonneg: "0 < i"
   757   assumes less: "i ^ m < i ^ n"
   758   shows "m < n"
   759 proof (cases "i = 1")
   760   case True
   761   with less power_one [where 'a = nat] show ?thesis by simp
   762 next
   763   case False
   764   with nonneg have "1 < i" by auto
   765   from power_strict_increasing_iff [OF this] less show ?thesis ..
   766 qed
   767 
   768 lemma power_dvd_imp_le: "i ^ m dvd i ^ n \<Longrightarrow> 1 < i \<Longrightarrow> m \<le> n"
   769   for i m n :: nat
   770   apply (rule power_le_imp_le_exp)
   771    apply assumption
   772   apply (erule dvd_imp_le)
   773   apply simp
   774   done
   775 
   776 lemma power2_nat_le_eq_le: "m\<^sup>2 \<le> n\<^sup>2 \<longleftrightarrow> m \<le> n"
   777   for m n :: nat
   778   by (auto intro: power2_le_imp_le power_mono)
   779 
   780 lemma power2_nat_le_imp_le:
   781   fixes m n :: nat
   782   assumes "m\<^sup>2 \<le> n"
   783   shows "m \<le> n"
   784 proof (cases m)
   785   case 0
   786   then show ?thesis by simp
   787 next
   788   case (Suc k)
   789   show ?thesis
   790   proof (rule ccontr)
   791     assume "\<not> ?thesis"
   792     then have "n < m" by simp
   793     with assms Suc show False
   794       by (simp add: power2_eq_square)
   795   qed
   796 qed
   797 
   798 lemma ex_power_ivl1: fixes b k :: nat assumes "b \<ge> 2"
   799 shows "k \<ge> 1 \<Longrightarrow> \<exists>n. b^n \<le> k \<and> k < b^(n+1)" (is "_ \<Longrightarrow> \<exists>n. ?P k n")
   800 proof(induction k)
   801   case 0 thus ?case by simp
   802 next
   803   case (Suc k)
   804   show ?case
   805   proof cases
   806     assume "k=0"
   807     hence "?P (Suc k) 0" using assms by simp
   808     thus ?case ..
   809   next
   810     assume "k\<noteq>0"
   811     with Suc obtain n where IH: "?P k n" by auto
   812     show ?case
   813     proof (cases "k = b^(n+1) - 1")
   814       case True
   815       hence "?P (Suc k) (n+1)" using assms
   816         by (simp add: power_less_power_Suc)
   817       thus ?thesis ..
   818     next
   819       case False
   820       hence "?P (Suc k) n" using IH by auto
   821       thus ?thesis ..
   822     qed
   823   qed
   824 qed
   825 
   826 lemma ex_power_ivl2: fixes b k :: nat assumes "b \<ge> 2" "k \<ge> 2"
   827 shows "\<exists>n. b^n < k \<and> k \<le> b^(n+1)"
   828 proof -
   829   have "1 \<le> k - 1" using assms(2) by arith
   830   from ex_power_ivl1[OF assms(1) this]
   831   obtain n where "b ^ n \<le> k - 1 \<and> k - 1 < b ^ (n + 1)" ..
   832   hence "b^n < k \<and> k \<le> b^(n+1)" using assms by auto
   833   thus ?thesis ..
   834 qed
   835 
   836 
   837 subsubsection \<open>Cardinality of the Powerset\<close>
   838 
   839 lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
   840   unfolding UNIV_bool by simp
   841 
   842 lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
   843 proof (induct rule: finite_induct)
   844   case empty
   845   show ?case by auto
   846 next
   847   case (insert x A)
   848   then have "inj_on (insert x) (Pow A)"
   849     unfolding inj_on_def by (blast elim!: equalityE)
   850   then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A"
   851     by (simp add: mult_2 card_image Pow_insert insert.hyps)
   852   with insert show ?case
   853     apply (simp add: Pow_insert)
   854     apply (subst card_Un_disjoint)
   855        apply auto
   856     done
   857 qed
   858 
   859 
   860 subsection \<open>Code generator tweak\<close>
   861 
   862 code_identifier
   863   code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   864 
   865 end