src/HOL/Power.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 66936 cf8d8fc23891
child 67226 ec32cdaab97b
permissions -rw-r--r--
more robust sorted_entries;
     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 semidom_divide
   310 begin
   311 
   312 lemma power_diff:
   313   "a ^ (m - n) = (a ^ m) div (a ^ n)" if "a \<noteq> 0" and "n \<le> m"
   314 proof -
   315   define q where "q = m - n"
   316   with \<open>n \<le> m\<close> have "m = q + n" by simp
   317   with \<open>a \<noteq> 0\<close> q_def show ?thesis
   318     by (simp add: power_add)
   319 qed
   320 
   321 end
   322 
   323 context algebraic_semidom
   324 begin
   325 
   326 lemma div_power: "b dvd a \<Longrightarrow> (a div b) ^ n = a ^ n div b ^ n"
   327   by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same)
   328 
   329 lemma is_unit_power_iff: "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
   330   by (induct n) (auto simp add: is_unit_mult_iff)
   331 
   332 lemma dvd_power_iff:
   333   assumes "x \<noteq> 0"
   334   shows   "x ^ m dvd x ^ n \<longleftrightarrow> is_unit x \<or> m \<le> n"
   335 proof
   336   assume *: "x ^ m dvd x ^ n"
   337   {
   338     assume "m > n"
   339     note *
   340     also have "x ^ n = x ^ n * 1" by simp
   341     also from \<open>m > n\<close> have "m = n + (m - n)" by simp
   342     also have "x ^ \<dots> = x ^ n * x ^ (m - n)" by (rule power_add)
   343     finally have "x ^ (m - n) dvd 1"
   344       by (subst (asm) dvd_times_left_cancel_iff) (insert assms, simp_all)
   345     with \<open>m > n\<close> have "is_unit x" by (simp add: is_unit_power_iff)
   346   }
   347   thus "is_unit x \<or> m \<le> n" by force
   348 qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd)
   349 
   350 
   351 end
   352 
   353 context normalization_semidom
   354 begin
   355 
   356 lemma normalize_power: "normalize (a ^ n) = normalize a ^ n"
   357   by (induct n) (simp_all add: normalize_mult)
   358 
   359 lemma unit_factor_power: "unit_factor (a ^ n) = unit_factor a ^ n"
   360   by (induct n) (simp_all add: unit_factor_mult)
   361 
   362 end
   363 
   364 context division_ring
   365 begin
   366 
   367 text \<open>Perhaps these should be simprules.\<close>
   368 lemma power_inverse [field_simps, divide_simps]: "inverse a ^ n = inverse (a ^ n)"
   369 proof (cases "a = 0")
   370   case True
   371   then show ?thesis by (simp add: power_0_left)
   372 next
   373   case False
   374   then have "inverse (a ^ n) = inverse a ^ n"
   375     by (induct n) (simp_all add: nonzero_inverse_mult_distrib power_commutes)
   376   then show ?thesis by simp
   377 qed
   378 
   379 lemma power_one_over [field_simps, divide_simps]: "(1 / a) ^ n = 1 / a ^ n"
   380   using power_inverse [of a] by (simp add: divide_inverse)
   381 
   382 end
   383 
   384 context field
   385 begin
   386 
   387 lemma power_divide [field_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n"
   388   by (induct n) simp_all
   389 
   390 end
   391 
   392 
   393 subsection \<open>Exponentiation on ordered types\<close>
   394 
   395 context linordered_semidom
   396 begin
   397 
   398 lemma zero_less_power [simp]: "0 < a \<Longrightarrow> 0 < a ^ n"
   399   by (induct n) simp_all
   400 
   401 lemma zero_le_power [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
   402   by (induct n) simp_all
   403 
   404 lemma power_mono: "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n"
   405   by (induct n) (auto intro: mult_mono order_trans [of 0 a b])
   406 
   407 lemma one_le_power [simp]: "1 \<le> a \<Longrightarrow> 1 \<le> a ^ n"
   408   using power_mono [of 1 a n] by simp
   409 
   410 lemma power_le_one: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ n \<le> 1"
   411   using power_mono [of a 1 n] by simp
   412 
   413 lemma power_gt1_lemma:
   414   assumes gt1: "1 < a"
   415   shows "1 < a * a ^ n"
   416 proof -
   417   from gt1 have "0 \<le> a"
   418     by (fact order_trans [OF zero_le_one less_imp_le])
   419   from gt1 have "1 * 1 < a * 1" by simp
   420   also from gt1 have "\<dots> \<le> a * a ^ n"
   421     by (simp only: mult_mono \<open>0 \<le> a\<close> one_le_power order_less_imp_le zero_le_one order_refl)
   422   finally show ?thesis by simp
   423 qed
   424 
   425 lemma power_gt1: "1 < a \<Longrightarrow> 1 < a ^ Suc n"
   426   by (simp add: power_gt1_lemma)
   427 
   428 lemma one_less_power [simp]: "1 < a \<Longrightarrow> 0 < n \<Longrightarrow> 1 < a ^ n"
   429   by (cases n) (simp_all add: power_gt1_lemma)
   430 
   431 lemma power_le_imp_le_exp:
   432   assumes gt1: "1 < a"
   433   shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n"
   434 proof (induct m arbitrary: n)
   435   case 0
   436   show ?case by simp
   437 next
   438   case (Suc m)
   439   show ?case
   440   proof (cases n)
   441     case 0
   442     with Suc have "a * a ^ m \<le> 1" by simp
   443     with gt1 show ?thesis
   444       by (force simp only: power_gt1_lemma not_less [symmetric])
   445   next
   446     case (Suc n)
   447     with Suc.prems Suc.hyps show ?thesis
   448       by (force dest: mult_left_le_imp_le simp add: less_trans [OF zero_less_one gt1])
   449   qed
   450 qed
   451 
   452 lemma of_nat_zero_less_power_iff [simp]: "of_nat x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
   453   by (induct n) auto
   454 
   455 text \<open>Surely we can strengthen this? It holds for \<open>0<a<1\<close> too.\<close>
   456 lemma power_inject_exp [simp]: "1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
   457   by (force simp add: order_antisym power_le_imp_le_exp)
   458 
   459 text \<open>
   460   Can relax the first premise to @{term "0<a"} in the case of the
   461   natural numbers.
   462 \<close>
   463 lemma power_less_imp_less_exp: "1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n"
   464   by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] power_le_imp_le_exp)
   465 
   466 lemma power_strict_mono [rule_format]: "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n"
   467   by (induct n) (auto simp: mult_strict_mono le_less_trans [of 0 a b])
   468 
   469 text\<open>Lemma for \<open>power_strict_decreasing\<close>\<close>
   470 lemma power_Suc_less: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n"
   471   by (induct n) (auto simp: mult_strict_left_mono)
   472 
   473 lemma power_strict_decreasing [rule_format]: "n < N \<Longrightarrow> 0 < a \<Longrightarrow> a < 1 \<longrightarrow> a ^ N < a ^ n"
   474 proof (induct N)
   475   case 0
   476   then show ?case by simp
   477 next
   478   case (Suc N)
   479   then show ?case
   480     apply (auto simp add: power_Suc_less less_Suc_eq)
   481     apply (subgoal_tac "a * a^N < 1 * a^n")
   482      apply simp
   483     apply (rule mult_strict_mono)
   484        apply auto
   485     done
   486 qed
   487 
   488 text \<open>Proof resembles that of \<open>power_strict_decreasing\<close>.\<close>
   489 lemma power_decreasing: "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ N \<le> a ^ n"
   490 proof (induct N)
   491   case 0
   492   then show ?case by simp
   493 next
   494   case (Suc N)
   495   then show ?case
   496     apply (auto simp add: le_Suc_eq)
   497     apply (subgoal_tac "a * a^N \<le> 1 * a^n")
   498      apply simp
   499     apply (rule mult_mono)
   500        apply auto
   501     done
   502 qed
   503 
   504 lemma power_Suc_less_one: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1"
   505   using power_strict_decreasing [of 0 "Suc n" a] by simp
   506 
   507 text \<open>Proof again resembles that of \<open>power_strict_decreasing\<close>.\<close>
   508 lemma power_increasing: "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
   509 proof (induct N)
   510   case 0
   511   then show ?case by simp
   512 next
   513   case (Suc N)
   514   then show ?case
   515     apply (auto simp add: le_Suc_eq)
   516     apply (subgoal_tac "1 * a^n \<le> a * a^N")
   517      apply simp
   518     apply (rule mult_mono)
   519        apply (auto simp add: order_trans [OF zero_le_one])
   520     done
   521 qed
   522 
   523 text \<open>Lemma for \<open>power_strict_increasing\<close>.\<close>
   524 lemma power_less_power_Suc: "1 < a \<Longrightarrow> a ^ n < a * a ^ n"
   525   by (induct n) (auto simp: mult_strict_left_mono less_trans [OF zero_less_one])
   526 
   527 lemma power_strict_increasing: "n < N \<Longrightarrow> 1 < a \<Longrightarrow> a ^ n < a ^ N"
   528 proof (induct N)
   529   case 0
   530   then show ?case by simp
   531 next
   532   case (Suc N)
   533   then show ?case
   534     apply (auto simp add: power_less_power_Suc less_Suc_eq)
   535     apply (subgoal_tac "1 * a^n < a * a^N")
   536      apply simp
   537     apply (rule mult_strict_mono)
   538     apply (auto simp add: less_trans [OF zero_less_one] less_imp_le)
   539     done
   540 qed
   541 
   542 lemma power_increasing_iff [simp]: "1 < b \<Longrightarrow> b ^ x \<le> b ^ y \<longleftrightarrow> x \<le> y"
   543   by (blast intro: power_le_imp_le_exp power_increasing less_imp_le)
   544 
   545 lemma power_strict_increasing_iff [simp]: "1 < b \<Longrightarrow> b ^ x < b ^ y \<longleftrightarrow> x < y"
   546   by (blast intro: power_less_imp_less_exp power_strict_increasing)
   547 
   548 lemma power_le_imp_le_base:
   549   assumes le: "a ^ Suc n \<le> b ^ Suc n"
   550     and "0 \<le> b"
   551   shows "a \<le> b"
   552 proof (rule ccontr)
   553   assume "\<not> ?thesis"
   554   then have "b < a" by (simp only: linorder_not_le)
   555   then have "b ^ Suc n < a ^ Suc n"
   556     by (simp only: assms(2) power_strict_mono)
   557   with le show False
   558     by (simp add: linorder_not_less [symmetric])
   559 qed
   560 
   561 lemma power_less_imp_less_base:
   562   assumes less: "a ^ n < b ^ n"
   563   assumes nonneg: "0 \<le> b"
   564   shows "a < b"
   565 proof (rule contrapos_pp [OF less])
   566   assume "\<not> ?thesis"
   567   then have "b \<le> a" by (simp only: linorder_not_less)
   568   from this nonneg have "b ^ n \<le> a ^ n" by (rule power_mono)
   569   then show "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less)
   570 qed
   571 
   572 lemma power_inject_base: "a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b"
   573   by (blast intro: power_le_imp_le_base antisym eq_refl sym)
   574 
   575 lemma power_eq_imp_eq_base: "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b"
   576   by (cases n) (simp_all del: power_Suc, rule power_inject_base)
   577 
   578 lemma power_eq_iff_eq_base: "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b"
   579   using power_eq_imp_eq_base [of a n b] by auto
   580 
   581 lemma power2_le_imp_le: "x\<^sup>2 \<le> y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
   582   unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
   583 
   584 lemma power2_less_imp_less: "x\<^sup>2 < y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
   585   by (rule power_less_imp_less_base)
   586 
   587 lemma power2_eq_imp_eq: "x\<^sup>2 = y\<^sup>2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
   588   unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
   589 
   590 lemma power_Suc_le_self: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
   591   using power_decreasing [of 1 "Suc n" a] by simp
   592 
   593 lemma power2_eq_iff_nonneg [simp]:
   594   assumes "0 \<le> x" "0 \<le> y"
   595   shows "(x ^ 2 = y ^ 2) \<longleftrightarrow> x = y"
   596 using assms power2_eq_imp_eq by blast
   597 
   598 lemma of_nat_less_numeral_power_cancel_iff[simp]:
   599   "of_nat x < numeral i ^ n \<longleftrightarrow> x < numeral i ^ n"
   600   using of_nat_less_iff[of x "numeral i ^ n", unfolded of_nat_numeral of_nat_power] .
   601 
   602 lemma of_nat_le_numeral_power_cancel_iff[simp]:
   603   "of_nat x \<le> numeral i ^ n \<longleftrightarrow> x \<le> numeral i ^ n"
   604   using of_nat_le_iff[of x "numeral i ^ n", unfolded of_nat_numeral of_nat_power] .
   605 
   606 lemma numeral_power_less_of_nat_cancel_iff[simp]:
   607   "numeral i ^ n < of_nat x \<longleftrightarrow> numeral i ^ n < x"
   608   using of_nat_less_iff[of "numeral i ^ n" x, unfolded of_nat_numeral of_nat_power] .
   609 
   610 lemma numeral_power_le_of_nat_cancel_iff[simp]:
   611   "numeral i ^ n \<le> of_nat x \<longleftrightarrow> numeral i ^ n \<le> x"
   612   using of_nat_le_iff[of "numeral i ^ n" x, unfolded of_nat_numeral of_nat_power] .
   613 
   614 lemma of_nat_le_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w \<le> of_nat x \<longleftrightarrow> b ^ w \<le> x"
   615   by (metis of_nat_le_iff of_nat_power)
   616 
   617 lemma of_nat_power_le_of_nat_cancel_iff[simp]: "of_nat x \<le> (of_nat b) ^ w \<longleftrightarrow> x \<le> b ^ w"
   618   by (metis of_nat_le_iff of_nat_power)
   619 
   620 lemma of_nat_less_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w < of_nat x \<longleftrightarrow> b ^ w < x"
   621   by (metis of_nat_less_iff of_nat_power)
   622 
   623 lemma of_nat_power_less_of_nat_cancel_iff[simp]: "of_nat x < (of_nat b) ^ w \<longleftrightarrow> x < b ^ w"
   624   by (metis of_nat_less_iff of_nat_power)
   625 
   626 end
   627 
   628 context linordered_ring_strict
   629 begin
   630 
   631 lemma sum_squares_eq_zero_iff: "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   632   by (simp add: add_nonneg_eq_0_iff)
   633 
   634 lemma sum_squares_le_zero_iff: "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   635   by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
   636 
   637 lemma sum_squares_gt_zero_iff: "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   638   by (simp add: not_le [symmetric] sum_squares_le_zero_iff)
   639 
   640 end
   641 
   642 context linordered_idom
   643 begin
   644 
   645 lemma zero_le_power2 [simp]: "0 \<le> a\<^sup>2"
   646   by (simp add: power2_eq_square)
   647 
   648 lemma zero_less_power2 [simp]: "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0"
   649   by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   650 
   651 lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
   652   by (force simp add: power2_eq_square mult_less_0_iff)
   653 
   654 lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" -- \<open>FIXME simp?\<close>
   655   by (induct n) (simp_all add: abs_mult)
   656 
   657 lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n"
   658   by (induct n) (simp_all add: sgn_mult)
   659 
   660 lemma abs_power_minus [simp]: "\<bar>(- a) ^ n\<bar> = \<bar>a ^ n\<bar>"
   661   by (simp add: power_abs)
   662 
   663 lemma zero_less_power_abs_iff [simp]: "0 < \<bar>a\<bar> ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
   664 proof (induct n)
   665   case 0
   666   show ?case by simp
   667 next
   668   case Suc
   669   then show ?case by (auto simp: zero_less_mult_iff)
   670 qed
   671 
   672 lemma zero_le_power_abs [simp]: "0 \<le> \<bar>a\<bar> ^ n"
   673   by (rule zero_le_power [OF abs_ge_zero])
   674 
   675 lemma power2_less_eq_zero_iff [simp]: "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
   676   by (simp add: le_less)
   677 
   678 lemma abs_power2 [simp]: "\<bar>a\<^sup>2\<bar> = a\<^sup>2"
   679   by (simp add: power2_eq_square)
   680 
   681 lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2"
   682   by (simp add: power2_eq_square)
   683 
   684 lemma odd_power_less_zero: "a < 0 \<Longrightarrow> a ^ Suc (2 * n) < 0"
   685 proof (induct n)
   686   case 0
   687   then show ?case by simp
   688 next
   689   case (Suc n)
   690   have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
   691     by (simp add: ac_simps power_add power2_eq_square)
   692   then show ?case
   693     by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
   694 qed
   695 
   696 lemma odd_0_le_power_imp_0_le: "0 \<le> a ^ Suc (2 * n) \<Longrightarrow> 0 \<le> a"
   697   using odd_power_less_zero [of a n]
   698   by (force simp add: linorder_not_less [symmetric])
   699 
   700 lemma zero_le_even_power'[simp]: "0 \<le> a ^ (2 * n)"
   701 proof (induct n)
   702   case 0
   703   show ?case by simp
   704 next
   705   case (Suc n)
   706   have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
   707     by (simp add: ac_simps power_add power2_eq_square)
   708   then show ?case
   709     by (simp add: Suc zero_le_mult_iff)
   710 qed
   711 
   712 lemma sum_power2_ge_zero: "0 \<le> x\<^sup>2 + y\<^sup>2"
   713   by (intro add_nonneg_nonneg zero_le_power2)
   714 
   715 lemma not_sum_power2_lt_zero: "\<not> x\<^sup>2 + y\<^sup>2 < 0"
   716   unfolding not_less by (rule sum_power2_ge_zero)
   717 
   718 lemma sum_power2_eq_zero_iff: "x\<^sup>2 + y\<^sup>2 = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   719   unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff)
   720 
   721 lemma sum_power2_le_zero_iff: "x\<^sup>2 + y\<^sup>2 \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   722   by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero)
   723 
   724 lemma sum_power2_gt_zero_iff: "0 < x\<^sup>2 + y\<^sup>2 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   725   unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff)
   726 
   727 lemma abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> x\<^sup>2 \<le> y\<^sup>2"
   728   (is "?lhs \<longleftrightarrow> ?rhs")
   729 proof
   730   assume ?lhs
   731   then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono) simp
   732   then show ?rhs by simp
   733 next
   734   assume ?rhs
   735   then show ?lhs
   736     by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
   737 qed
   738 
   739 lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> \<bar>x\<bar> \<le> 1"
   740   using abs_le_square_iff [of x 1] by simp
   741 
   742 lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> \<bar>x\<bar> = 1"
   743   by (auto simp add: abs_if power2_eq_1_iff)
   744 
   745 lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> \<bar>x\<bar> < 1"
   746   using  abs_square_eq_1 [of x] abs_square_le_1 [of x] by (auto simp add: le_less)
   747 
   748 end
   749 
   750 
   751 subsection \<open>Miscellaneous rules\<close>
   752 
   753 lemma (in linordered_semidom) self_le_power: "1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n"
   754   using power_increasing [of 1 n a] power_one_right [of a] by auto
   755 
   756 lemma (in power) power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
   757   unfolding One_nat_def by (cases m) simp_all
   758 
   759 lemma (in comm_semiring_1) power2_sum: "(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y"
   760   by (simp add: algebra_simps power2_eq_square mult_2_right)
   761 
   762 context comm_ring_1
   763 begin
   764 
   765 lemma power2_diff: "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
   766   by (simp add: algebra_simps power2_eq_square mult_2_right)
   767 
   768 lemma power2_commute: "(x - y)\<^sup>2 = (y - x)\<^sup>2"
   769   by (simp add: algebra_simps power2_eq_square)
   770 
   771 lemma minus_power_mult_self: "(- a) ^ n * (- a) ^ n = a ^ (2 * n)"
   772   by (simp add: power_mult_distrib [symmetric])
   773     (simp add: power2_eq_square [symmetric] power_mult [symmetric])
   774 
   775 lemma minus_one_mult_self [simp]: "(- 1) ^ n * (- 1) ^ n = 1"
   776   using minus_power_mult_self [of 1 n] by simp
   777 
   778 lemma left_minus_one_mult_self [simp]: "(- 1) ^ n * ((- 1) ^ n * a) = a"
   779   by (simp add: mult.assoc [symmetric])
   780 
   781 end
   782 
   783 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
   784 
   785 lemmas zero_compare_simps =
   786   add_strict_increasing add_strict_increasing2 add_increasing
   787   zero_le_mult_iff zero_le_divide_iff
   788   zero_less_mult_iff zero_less_divide_iff
   789   mult_le_0_iff divide_le_0_iff
   790   mult_less_0_iff divide_less_0_iff
   791   zero_le_power2 power2_less_0
   792 
   793 
   794 subsection \<open>Exponentiation for the Natural Numbers\<close>
   795 
   796 lemma nat_one_le_power [simp]: "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n"
   797   by (rule one_le_power [of i n, unfolded One_nat_def])
   798 
   799 lemma nat_zero_less_power_iff [simp]: "x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
   800   for x :: nat
   801   by (induct n) auto
   802 
   803 lemma nat_power_eq_Suc_0_iff [simp]: "x ^ m = Suc 0 \<longleftrightarrow> m = 0 \<or> x = Suc 0"
   804   by (induct m) auto
   805 
   806 lemma power_Suc_0 [simp]: "Suc 0 ^ n = Suc 0"
   807   by simp
   808 
   809 text \<open>
   810   Valid for the naturals, but what if \<open>0 < i < 1\<close>? Premises cannot be
   811   weakened: consider the case where \<open>i = 0\<close>, \<open>m = 1\<close> and \<open>n = 0\<close>.
   812 \<close>
   813 
   814 lemma nat_power_less_imp_less:
   815   fixes i :: nat
   816   assumes nonneg: "0 < i"
   817   assumes less: "i ^ m < i ^ n"
   818   shows "m < n"
   819 proof (cases "i = 1")
   820   case True
   821   with less power_one [where 'a = nat] show ?thesis by simp
   822 next
   823   case False
   824   with nonneg have "1 < i" by auto
   825   from power_strict_increasing_iff [OF this] less show ?thesis ..
   826 qed
   827 
   828 lemma power_dvd_imp_le: "i ^ m dvd i ^ n \<Longrightarrow> 1 < i \<Longrightarrow> m \<le> n"
   829   for i m n :: nat
   830   apply (rule power_le_imp_le_exp)
   831    apply assumption
   832   apply (erule dvd_imp_le)
   833   apply simp
   834   done
   835 
   836 lemma power2_nat_le_eq_le: "m\<^sup>2 \<le> n\<^sup>2 \<longleftrightarrow> m \<le> n"
   837   for m n :: nat
   838   by (auto intro: power2_le_imp_le power_mono)
   839 
   840 lemma power2_nat_le_imp_le:
   841   fixes m n :: nat
   842   assumes "m\<^sup>2 \<le> n"
   843   shows "m \<le> n"
   844 proof (cases m)
   845   case 0
   846   then show ?thesis by simp
   847 next
   848   case (Suc k)
   849   show ?thesis
   850   proof (rule ccontr)
   851     assume "\<not> ?thesis"
   852     then have "n < m" by simp
   853     with assms Suc show False
   854       by (simp add: power2_eq_square)
   855   qed
   856 qed
   857 
   858 lemma ex_power_ivl1: fixes b k :: nat assumes "b \<ge> 2"
   859 shows "k \<ge> 1 \<Longrightarrow> \<exists>n. b^n \<le> k \<and> k < b^(n+1)" (is "_ \<Longrightarrow> \<exists>n. ?P k n")
   860 proof(induction k)
   861   case 0 thus ?case by simp
   862 next
   863   case (Suc k)
   864   show ?case
   865   proof cases
   866     assume "k=0"
   867     hence "?P (Suc k) 0" using assms by simp
   868     thus ?case ..
   869   next
   870     assume "k\<noteq>0"
   871     with Suc obtain n where IH: "?P k n" by auto
   872     show ?case
   873     proof (cases "k = b^(n+1) - 1")
   874       case True
   875       hence "?P (Suc k) (n+1)" using assms
   876         by (simp add: power_less_power_Suc)
   877       thus ?thesis ..
   878     next
   879       case False
   880       hence "?P (Suc k) n" using IH by auto
   881       thus ?thesis ..
   882     qed
   883   qed
   884 qed
   885 
   886 lemma ex_power_ivl2: fixes b k :: nat assumes "b \<ge> 2" "k \<ge> 2"
   887 shows "\<exists>n. b^n < k \<and> k \<le> b^(n+1)"
   888 proof -
   889   have "1 \<le> k - 1" using assms(2) by arith
   890   from ex_power_ivl1[OF assms(1) this]
   891   obtain n where "b ^ n \<le> k - 1 \<and> k - 1 < b ^ (n + 1)" ..
   892   hence "b^n < k \<and> k \<le> b^(n+1)" using assms by auto
   893   thus ?thesis ..
   894 qed
   895 
   896 
   897 subsubsection \<open>Cardinality of the Powerset\<close>
   898 
   899 lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
   900   unfolding UNIV_bool by simp
   901 
   902 lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
   903 proof (induct rule: finite_induct)
   904   case empty
   905   show ?case by simp
   906 next
   907   case (insert x A)
   908   from \<open>x \<notin> A\<close> have disjoint: "Pow A \<inter> insert x ` Pow A = {}" by blast
   909   from \<open>x \<notin> A\<close> have inj_on: "inj_on (insert x) (Pow A)"
   910     unfolding inj_on_def by auto
   911 
   912   have "card (Pow (insert x A)) = card (Pow A \<union> insert x ` Pow A)"
   913     by (simp only: Pow_insert)
   914   also have "\<dots> = card (Pow A) + card (insert x ` Pow A)"
   915     by (rule card_Un_disjoint) (use \<open>finite A\<close> disjoint in simp_all)
   916   also from inj_on have "card (insert x ` Pow A) = card (Pow A)"
   917     by (rule card_image)
   918   also have "\<dots> + \<dots> = 2 * \<dots>" by (simp add: mult_2)
   919   also from insert(3) have "\<dots> = 2 ^ Suc (card A)" by simp
   920   also from insert(1,2) have "Suc (card A) = card (insert x A)"
   921     by (rule card_insert_disjoint [symmetric])
   922   finally show ?case .
   923 qed
   924 
   925 
   926 subsection \<open>Code generator tweak\<close>
   927 
   928 code_identifier
   929   code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   930 
   931 end