src/HOL/Power.thy
changeset 63654 f90e3926e627
parent 63648 f9f3006a5579
child 63924 f91766530e13
     1.1 --- a/src/HOL/Power.thy	Wed Aug 10 22:05:00 2016 +0200
     1.2 +++ b/src/HOL/Power.thy	Wed Aug 10 22:05:36 2016 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  section \<open>Exponentiation\<close>
     1.5  
     1.6  theory Power
     1.7 -imports Num
     1.8 +  imports Num
     1.9  begin
    1.10  
    1.11  subsection \<open>Powers for Arbitrary Monoids\<close>
    1.12 @@ -15,9 +15,9 @@
    1.13  begin
    1.14  
    1.15  primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixr "^" 80)
    1.16 -where
    1.17 -  power_0: "a ^ 0 = 1"
    1.18 -| power_Suc: "a ^ Suc n = a * a ^ n"
    1.19 +  where
    1.20 +    power_0: "a ^ 0 = 1"
    1.21 +  | power_Suc: "a ^ Suc n = a * a ^ n"
    1.22  
    1.23  notation (latex output)
    1.24    power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    1.25 @@ -33,32 +33,25 @@
    1.26  
    1.27  subclass power .
    1.28  
    1.29 -lemma power_one [simp]:
    1.30 -  "1 ^ n = 1"
    1.31 +lemma power_one [simp]: "1 ^ n = 1"
    1.32    by (induct n) simp_all
    1.33  
    1.34 -lemma power_one_right [simp]:
    1.35 -  "a ^ 1 = a"
    1.36 +lemma power_one_right [simp]: "a ^ 1 = a"
    1.37    by simp
    1.38  
    1.39 -lemma power_Suc0_right [simp]:
    1.40 -  "a ^ Suc 0 = a"
    1.41 +lemma power_Suc0_right [simp]: "a ^ Suc 0 = a"
    1.42    by simp
    1.43  
    1.44 -lemma power_commutes:
    1.45 -  "a ^ n * a = a * a ^ n"
    1.46 +lemma power_commutes: "a ^ n * a = a * a ^ n"
    1.47    by (induct n) (simp_all add: mult.assoc)
    1.48  
    1.49 -lemma power_Suc2:
    1.50 -  "a ^ Suc n = a ^ n * a"
    1.51 +lemma power_Suc2: "a ^ Suc n = a ^ n * a"
    1.52    by (simp add: power_commutes)
    1.53  
    1.54 -lemma power_add:
    1.55 -  "a ^ (m + n) = a ^ m * a ^ n"
    1.56 +lemma power_add: "a ^ (m + n) = a ^ m * a ^ n"
    1.57    by (induct m) (simp_all add: algebra_simps)
    1.58  
    1.59 -lemma power_mult:
    1.60 -  "a ^ (m * n) = (a ^ m) ^ n"
    1.61 +lemma power_mult: "a ^ (m * n) = (a ^ m) ^ n"
    1.62    by (induct n) (simp_all add: power_add)
    1.63  
    1.64  lemma power2_eq_square: "a\<^sup>2 = a * a"
    1.65 @@ -67,51 +60,49 @@
    1.66  lemma power3_eq_cube: "a ^ 3 = a * a * a"
    1.67    by (simp add: numeral_3_eq_3 mult.assoc)
    1.68  
    1.69 -lemma power_even_eq:
    1.70 -  "a ^ (2 * n) = (a ^ n)\<^sup>2"
    1.71 +lemma power_even_eq: "a ^ (2 * n) = (a ^ n)\<^sup>2"
    1.72    by (subst mult.commute) (simp add: power_mult)
    1.73  
    1.74 -lemma power_odd_eq:
    1.75 -  "a ^ Suc (2*n) = a * (a ^ n)\<^sup>2"
    1.76 +lemma power_odd_eq: "a ^ Suc (2*n) = a * (a ^ n)\<^sup>2"
    1.77    by (simp add: power_even_eq)
    1.78  
    1.79 -lemma power_numeral_even:
    1.80 -  "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)"
    1.81 -  unfolding numeral_Bit0 power_add Let_def ..
    1.82 +lemma power_numeral_even: "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)"
    1.83 +  by (simp only: numeral_Bit0 power_add Let_def)
    1.84  
    1.85 -lemma power_numeral_odd:
    1.86 -  "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)"
    1.87 -  unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right
    1.88 -  unfolding power_Suc power_add Let_def mult.assoc ..
    1.89 +lemma power_numeral_odd: "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)"
    1.90 +  by (simp only: numeral_Bit1 One_nat_def add_Suc_right add_0_right
    1.91 +      power_Suc power_add Let_def mult.assoc)
    1.92  
    1.93 -lemma funpow_times_power:
    1.94 -  "(times x ^^ f x) = times (x ^ f x)"
    1.95 +lemma funpow_times_power: "(times x ^^ f x) = times (x ^ f x)"
    1.96  proof (induct "f x" arbitrary: f)
    1.97 -  case 0 then show ?case by (simp add: fun_eq_iff)
    1.98 +  case 0
    1.99 +  then show ?case by (simp add: fun_eq_iff)
   1.100  next
   1.101    case (Suc n)
   1.102    define g where "g x = f x - 1" for x
   1.103    with Suc have "n = g x" by simp
   1.104    with Suc have "times x ^^ g x = times (x ^ g x)" by simp
   1.105    moreover from Suc g_def have "f x = g x + 1" by simp
   1.106 -  ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult.assoc)
   1.107 +  ultimately show ?case
   1.108 +    by (simp add: power_add funpow_add fun_eq_iff mult.assoc)
   1.109  qed
   1.110  
   1.111  lemma power_commuting_commutes:
   1.112    assumes "x * y = y * x"
   1.113    shows "x ^ n * y = y * x ^n"
   1.114  proof (induct n)
   1.115 +  case 0
   1.116 +  then show ?case by simp
   1.117 +next
   1.118    case (Suc n)
   1.119    have "x ^ Suc n * y = x ^ n * y * x"
   1.120      by (subst power_Suc2) (simp add: assms ac_simps)
   1.121    also have "\<dots> = y * x ^ Suc n"
   1.122 -    unfolding Suc power_Suc2
   1.123 -    by (simp add: ac_simps)
   1.124 +    by (simp only: Suc power_Suc2) (simp add: ac_simps)
   1.125    finally show ?case .
   1.126 -qed simp
   1.127 +qed
   1.128  
   1.129 -lemma power_minus_mult:
   1.130 -  "0 < n \<Longrightarrow> a ^ (n - 1) * a = a ^ n"
   1.131 +lemma power_minus_mult: "0 < n \<Longrightarrow> a ^ (n - 1) * a = a ^ n"
   1.132    by (simp add: power_commutes split: nat_diff_split)
   1.133  
   1.134  end
   1.135 @@ -119,29 +110,25 @@
   1.136  context comm_monoid_mult
   1.137  begin
   1.138  
   1.139 -lemma power_mult_distrib [field_simps]:
   1.140 -  "(a * b) ^ n = (a ^ n) * (b ^ n)"
   1.141 +lemma power_mult_distrib [field_simps]: "(a * b) ^ n = (a ^ n) * (b ^ n)"
   1.142    by (induct n) (simp_all add: ac_simps)
   1.143  
   1.144  end
   1.145  
   1.146 -text\<open>Extract constant factors from powers\<close>
   1.147 +text \<open>Extract constant factors from powers.\<close>
   1.148  declare power_mult_distrib [where a = "numeral w" for w, simp]
   1.149  declare power_mult_distrib [where b = "numeral w" for w, simp]
   1.150  
   1.151 -lemma power_add_numeral [simp]:
   1.152 -  fixes a :: "'a :: monoid_mult"
   1.153 -  shows "a^numeral m * a^numeral n = a^numeral (m + n)"
   1.154 +lemma power_add_numeral [simp]: "a^numeral m * a^numeral n = a^numeral (m + n)"
   1.155 +  for a :: "'a::monoid_mult"
   1.156    by (simp add: power_add [symmetric])
   1.157  
   1.158 -lemma power_add_numeral2 [simp]:
   1.159 -  fixes a :: "'a :: monoid_mult"
   1.160 -  shows "a^numeral m * (a^numeral n * b) = a^numeral (m + n) * b"
   1.161 +lemma power_add_numeral2 [simp]: "a^numeral m * (a^numeral n * b) = a^numeral (m + n) * b"
   1.162 +  for a :: "'a::monoid_mult"
   1.163    by (simp add: mult.assoc [symmetric])
   1.164  
   1.165 -lemma power_mult_numeral [simp]:
   1.166 -  fixes a :: "'a :: monoid_mult"
   1.167 -  shows"(a^numeral m)^numeral n = a^numeral (m * n)"
   1.168 +lemma power_mult_numeral [simp]: "(a^numeral m)^numeral n = a^numeral (m * n)"
   1.169 +  for a :: "'a::monoid_mult"
   1.170    by (simp only: numeral_mult power_mult)
   1.171  
   1.172  context semiring_numeral
   1.173 @@ -151,8 +138,9 @@
   1.174    by (simp only: sqr_conv_mult numeral_mult)
   1.175  
   1.176  lemma numeral_pow: "numeral (Num.pow k l) = numeral k ^ numeral l"
   1.177 -  by (induct l, simp_all only: numeral_class.numeral.simps pow.simps
   1.178 -    numeral_sqr numeral_mult power_add power_one_right)
   1.179 +  by (induct l)
   1.180 +    (simp_all only: numeral_class.numeral.simps pow.simps
   1.181 +      numeral_sqr numeral_mult power_add power_one_right)
   1.182  
   1.183  lemma power_numeral [simp]: "numeral k ^ numeral l = numeral (Num.pow k l)"
   1.184    by (rule numeral_pow [symmetric])
   1.185 @@ -162,16 +150,13 @@
   1.186  context semiring_1
   1.187  begin
   1.188  
   1.189 -lemma of_nat_power [simp]:
   1.190 -  "of_nat (m ^ n) = of_nat m ^ n"
   1.191 +lemma of_nat_power [simp]: "of_nat (m ^ n) = of_nat m ^ n"
   1.192    by (induct n) simp_all
   1.193  
   1.194 -lemma zero_power:
   1.195 -  "0 < n \<Longrightarrow> 0 ^ n = 0"
   1.196 +lemma zero_power: "0 < n \<Longrightarrow> 0 ^ n = 0"
   1.197    by (cases n) simp_all
   1.198  
   1.199 -lemma power_zero_numeral [simp]:
   1.200 -  "0 ^ numeral k = 0"
   1.201 +lemma power_zero_numeral [simp]: "0 ^ numeral k = 0"
   1.202    by (simp add: numeral_eq_Suc)
   1.203  
   1.204  lemma zero_power2: "0\<^sup>2 = 0" (* delete? *)
   1.205 @@ -180,13 +165,11 @@
   1.206  lemma one_power2: "1\<^sup>2 = 1" (* delete? *)
   1.207    by (rule power_one)
   1.208  
   1.209 -lemma power_0_Suc [simp]:
   1.210 -  "0 ^ Suc n = 0"
   1.211 +lemma power_0_Suc [simp]: "0 ^ Suc n = 0"
   1.212    by simp
   1.213  
   1.214 -text\<open>It looks plausible as a simprule, but its effect can be strange.\<close>
   1.215 -lemma power_0_left:
   1.216 -  "0 ^ n = (if n = 0 then 1 else 0)"
   1.217 +text \<open>It looks plausible as a simprule, but its effect can be strange.\<close>
   1.218 +lemma power_0_left: "0 ^ n = (if n = 0 then 1 else 0)"
   1.219    by (cases n) simp_all
   1.220  
   1.221  end
   1.222 @@ -194,34 +177,32 @@
   1.223  context comm_semiring_1
   1.224  begin
   1.225  
   1.226 -text \<open>The divides relation\<close>
   1.227 +text \<open>The divides relation.\<close>
   1.228  
   1.229  lemma le_imp_power_dvd:
   1.230 -  assumes "m \<le> n" shows "a ^ m dvd a ^ n"
   1.231 +  assumes "m \<le> n"
   1.232 +  shows "a ^ m dvd a ^ n"
   1.233  proof
   1.234 -  have "a ^ n = a ^ (m + (n - m))"
   1.235 -    using \<open>m \<le> n\<close> by simp
   1.236 -  also have "\<dots> = a ^ m * a ^ (n - m)"
   1.237 -    by (rule power_add)
   1.238 +  from assms have "a ^ n = a ^ (m + (n - m))" by simp
   1.239 +  also have "\<dots> = a ^ m * a ^ (n - m)" by (rule power_add)
   1.240    finally show "a ^ n = a ^ m * a ^ (n - m)" .
   1.241  qed
   1.242  
   1.243 -lemma power_le_dvd:
   1.244 -  "a ^ n dvd b \<Longrightarrow> m \<le> n \<Longrightarrow> a ^ m dvd b"
   1.245 +lemma power_le_dvd: "a ^ n dvd b \<Longrightarrow> m \<le> n \<Longrightarrow> a ^ m dvd b"
   1.246    by (rule dvd_trans [OF le_imp_power_dvd])
   1.247  
   1.248 -lemma dvd_power_same:
   1.249 -  "x dvd y \<Longrightarrow> x ^ n dvd y ^ n"
   1.250 +lemma dvd_power_same: "x dvd y \<Longrightarrow> x ^ n dvd y ^ n"
   1.251    by (induct n) (auto simp add: mult_dvd_mono)
   1.252  
   1.253 -lemma dvd_power_le:
   1.254 -  "x dvd y \<Longrightarrow> m \<ge> n \<Longrightarrow> x ^ n dvd y ^ m"
   1.255 +lemma dvd_power_le: "x dvd y \<Longrightarrow> m \<ge> n \<Longrightarrow> x ^ n dvd y ^ m"
   1.256    by (rule power_le_dvd [OF dvd_power_same])
   1.257  
   1.258  lemma dvd_power [simp]:
   1.259 -  assumes "n > (0::nat) \<or> x = 1"
   1.260 +  fixes n :: nat
   1.261 +  assumes "n > 0 \<or> x = 1"
   1.262    shows "x dvd (x ^ n)"
   1.263 -using assms proof
   1.264 +  using assms
   1.265 +proof
   1.266    assume "0 < n"
   1.267    then have "x ^ n = x ^ Suc (n - 1)" by simp
   1.268    then show "x dvd (x ^ n)" by simp
   1.269 @@ -237,16 +218,13 @@
   1.270  
   1.271  subclass power .
   1.272  
   1.273 -lemma power_eq_0_iff [simp]:
   1.274 -  "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
   1.275 +lemma power_eq_0_iff [simp]: "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
   1.276    by (induct n) auto
   1.277  
   1.278 -lemma power_not_zero:
   1.279 -  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
   1.280 +lemma power_not_zero: "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
   1.281    by (induct n) auto
   1.282  
   1.283 -lemma zero_eq_power2 [simp]:
   1.284 -  "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"
   1.285 +lemma zero_eq_power2 [simp]: "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"
   1.286    unfolding power2_eq_square by simp
   1.287  
   1.288  end
   1.289 @@ -254,45 +232,42 @@
   1.290  context ring_1
   1.291  begin
   1.292  
   1.293 -lemma power_minus:
   1.294 -  "(- a) ^ n = (- 1) ^ n * a ^ n"
   1.295 +lemma power_minus: "(- a) ^ n = (- 1) ^ n * a ^ n"
   1.296  proof (induct n)
   1.297 -  case 0 show ?case by simp
   1.298 +  case 0
   1.299 +  show ?case by simp
   1.300  next
   1.301 -  case (Suc n) then show ?case
   1.302 +  case (Suc n)
   1.303 +  then show ?case
   1.304      by (simp del: power_Suc add: power_Suc2 mult.assoc)
   1.305  qed
   1.306  
   1.307  lemma power_minus': "NO_MATCH 1 x \<Longrightarrow> (-x) ^ n = (-1)^n * x ^ n"
   1.308    by (rule power_minus)
   1.309  
   1.310 -lemma power_minus_Bit0:
   1.311 -  "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)"
   1.312 +lemma power_minus_Bit0: "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)"
   1.313    by (induct k, simp_all only: numeral_class.numeral.simps power_add
   1.314      power_one_right mult_minus_left mult_minus_right minus_minus)
   1.315  
   1.316 -lemma power_minus_Bit1:
   1.317 -  "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))"
   1.318 +lemma power_minus_Bit1: "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))"
   1.319    by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left)
   1.320  
   1.321 -lemma power2_minus [simp]:
   1.322 -  "(- a)\<^sup>2 = a\<^sup>2"
   1.323 +lemma power2_minus [simp]: "(- a)\<^sup>2 = a\<^sup>2"
   1.324    by (fact power_minus_Bit0)
   1.325  
   1.326 -lemma power_minus1_even [simp]:
   1.327 -  "(- 1) ^ (2*n) = 1"
   1.328 +lemma power_minus1_even [simp]: "(- 1) ^ (2*n) = 1"
   1.329  proof (induct n)
   1.330 -  case 0 show ?case by simp
   1.331 +  case 0
   1.332 +  show ?case by simp
   1.333  next
   1.334 -  case (Suc n) then show ?case by (simp add: power_add power2_eq_square)
   1.335 +  case (Suc n)
   1.336 +  then show ?case by (simp add: power_add power2_eq_square)
   1.337  qed
   1.338  
   1.339 -lemma power_minus1_odd:
   1.340 -  "(- 1) ^ Suc (2*n) = -1"
   1.341 +lemma power_minus1_odd: "(- 1) ^ Suc (2*n) = -1"
   1.342    by simp
   1.343  
   1.344 -lemma power_minus_even [simp]:
   1.345 -  "(-a) ^ (2*n) = a ^ (2*n)"
   1.346 +lemma power_minus_even [simp]: "(-a) ^ (2*n) = a ^ (2*n)"
   1.347    by (simp add: power_minus [of a])
   1.348  
   1.349  end
   1.350 @@ -300,8 +275,7 @@
   1.351  context ring_1_no_zero_divisors
   1.352  begin
   1.353  
   1.354 -lemma power2_eq_1_iff:
   1.355 -  "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
   1.356 +lemma power2_eq_1_iff: "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
   1.357    using square_eq_1_iff [of a] by (simp add: power2_eq_square)
   1.358  
   1.359  end
   1.360 @@ -317,13 +291,10 @@
   1.361  context algebraic_semidom
   1.362  begin
   1.363  
   1.364 -lemma div_power:
   1.365 -  assumes "b dvd a"
   1.366 -  shows "(a div b) ^ n = a ^ n div b ^ n"
   1.367 -  using assms by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same)
   1.368 +lemma div_power: "b dvd a \<Longrightarrow> (a div b) ^ n = a ^ n div b ^ n"
   1.369 +  by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same)
   1.370  
   1.371 -lemma is_unit_power_iff:
   1.372 -  "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
   1.373 +lemma is_unit_power_iff: "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
   1.374    by (induct n) (auto simp add: is_unit_mult_iff)
   1.375  
   1.376  end
   1.377 @@ -331,12 +302,10 @@
   1.378  context normalization_semidom
   1.379  begin
   1.380  
   1.381 -lemma normalize_power:
   1.382 -  "normalize (a ^ n) = normalize a ^ n"
   1.383 +lemma normalize_power: "normalize (a ^ n) = normalize a ^ n"
   1.384    by (induct n) (simp_all add: normalize_mult)
   1.385  
   1.386 -lemma unit_factor_power:
   1.387 -  "unit_factor (a ^ n) = unit_factor a ^ n"
   1.388 +lemma unit_factor_power: "unit_factor (a ^ n) = unit_factor a ^ n"
   1.389    by (induct n) (simp_all add: unit_factor_mult)
   1.390  
   1.391  end
   1.392 @@ -344,19 +313,19 @@
   1.393  context division_ring
   1.394  begin
   1.395  
   1.396 -text\<open>Perhaps these should be simprules.\<close>
   1.397 -lemma power_inverse [field_simps, divide_simps]:
   1.398 -  "inverse a ^ n = inverse (a ^ n)"
   1.399 +text \<open>Perhaps these should be simprules.\<close>
   1.400 +lemma power_inverse [field_simps, divide_simps]: "inverse a ^ n = inverse (a ^ n)"
   1.401  proof (cases "a = 0")
   1.402 -  case True then show ?thesis by (simp add: power_0_left)
   1.403 +  case True
   1.404 +  then show ?thesis by (simp add: power_0_left)
   1.405  next
   1.406 -  case False then have "inverse (a ^ n) = inverse a ^ n"
   1.407 +  case False
   1.408 +  then have "inverse (a ^ n) = inverse a ^ n"
   1.409      by (induct n) (simp_all add: nonzero_inverse_mult_distrib power_commutes)
   1.410    then show ?thesis by simp
   1.411  qed
   1.412  
   1.413 -lemma power_one_over [field_simps, divide_simps]:
   1.414 -  "(1 / a) ^ n = 1 / a ^ n"
   1.415 +lemma power_one_over [field_simps, divide_simps]: "(1 / a) ^ n = 1 / a ^ n"
   1.416    using power_inverse [of a] by (simp add: divide_inverse)
   1.417  
   1.418  end
   1.419 @@ -365,12 +334,11 @@
   1.420  begin
   1.421  
   1.422  lemma power_diff:
   1.423 -  assumes nz: "a \<noteq> 0"
   1.424 +  assumes "a \<noteq> 0"
   1.425    shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
   1.426 -  by (induct m n rule: diff_induct) (simp_all add: nz power_not_zero)
   1.427 +  by (induct m n rule: diff_induct) (simp_all add: assms power_not_zero)
   1.428  
   1.429 -lemma power_divide [field_simps, divide_simps]:
   1.430 -  "(a / b) ^ n = a ^ n / b ^ n"
   1.431 +lemma power_divide [field_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n"
   1.432    by (induct n) simp_all
   1.433  
   1.434  end
   1.435 @@ -381,22 +349,19 @@
   1.436  context linordered_semidom
   1.437  begin
   1.438  
   1.439 -lemma zero_less_power [simp]:
   1.440 -  "0 < a \<Longrightarrow> 0 < a ^ n"
   1.441 +lemma zero_less_power [simp]: "0 < a \<Longrightarrow> 0 < a ^ n"
   1.442    by (induct n) simp_all
   1.443  
   1.444 -lemma zero_le_power [simp]:
   1.445 -  "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
   1.446 +lemma zero_le_power [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
   1.447    by (induct n) simp_all
   1.448  
   1.449 -lemma power_mono:
   1.450 -  "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n"
   1.451 +lemma power_mono: "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n"
   1.452    by (induct n) (auto intro: mult_mono order_trans [of 0 a b])
   1.453  
   1.454  lemma one_le_power [simp]: "1 \<le> a \<Longrightarrow> 1 \<le> a ^ n"
   1.455    using power_mono [of 1 a n] by simp
   1.456  
   1.457 -lemma power_le_one: "\<lbrakk>0 \<le> a; a \<le> 1\<rbrakk> \<Longrightarrow> a ^ n \<le> 1"
   1.458 +lemma power_le_one: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ n \<le> 1"
   1.459    using power_mono [of a 1 n] by simp
   1.460  
   1.461  lemma power_gt1_lemma:
   1.462 @@ -405,19 +370,16 @@
   1.463  proof -
   1.464    from gt1 have "0 \<le> a"
   1.465      by (fact order_trans [OF zero_le_one less_imp_le])
   1.466 -  have "1 * 1 < a * 1" using gt1 by simp
   1.467 -  also have "\<dots> \<le> a * a ^ n" using gt1
   1.468 -    by (simp only: mult_mono \<open>0 \<le> a\<close> one_le_power order_less_imp_le
   1.469 -        zero_le_one order_refl)
   1.470 +  from gt1 have "1 * 1 < a * 1" by simp
   1.471 +  also from gt1 have "\<dots> \<le> a * a ^ n"
   1.472 +    by (simp only: mult_mono \<open>0 \<le> a\<close> one_le_power order_less_imp_le zero_le_one order_refl)
   1.473    finally show ?thesis by simp
   1.474  qed
   1.475  
   1.476 -lemma power_gt1:
   1.477 -  "1 < a \<Longrightarrow> 1 < a ^ Suc n"
   1.478 +lemma power_gt1: "1 < a \<Longrightarrow> 1 < a ^ Suc n"
   1.479    by (simp add: power_gt1_lemma)
   1.480  
   1.481 -lemma one_less_power [simp]:
   1.482 -  "1 < a \<Longrightarrow> 0 < n \<Longrightarrow> 1 < a ^ n"
   1.483 +lemma one_less_power [simp]: "1 < a \<Longrightarrow> 0 < n \<Longrightarrow> 1 < a ^ n"
   1.484    by (cases n) (simp_all add: power_gt1_lemma)
   1.485  
   1.486  lemma power_le_imp_le_exp:
   1.487 @@ -431,123 +393,122 @@
   1.488    show ?case
   1.489    proof (cases n)
   1.490      case 0
   1.491 -    with Suc.prems Suc.hyps have "a * a ^ m \<le> 1" by simp
   1.492 +    with Suc have "a * a ^ m \<le> 1" by simp
   1.493      with gt1 show ?thesis
   1.494 -      by (force simp only: power_gt1_lemma
   1.495 -          not_less [symmetric])
   1.496 +      by (force simp only: power_gt1_lemma not_less [symmetric])
   1.497    next
   1.498      case (Suc n)
   1.499      with Suc.prems Suc.hyps show ?thesis
   1.500 -      by (force dest: mult_left_le_imp_le
   1.501 -          simp add: less_trans [OF zero_less_one gt1])
   1.502 +      by (force dest: mult_left_le_imp_le simp add: less_trans [OF zero_less_one gt1])
   1.503    qed
   1.504  qed
   1.505  
   1.506 -lemma of_nat_zero_less_power_iff [simp]:
   1.507 -  "of_nat x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
   1.508 +lemma of_nat_zero_less_power_iff [simp]: "of_nat x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
   1.509    by (induct n) auto
   1.510  
   1.511 -text\<open>Surely we can strengthen this? It holds for \<open>0<a<1\<close> too.\<close>
   1.512 -lemma power_inject_exp [simp]:
   1.513 -  "1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
   1.514 +text \<open>Surely we can strengthen this? It holds for \<open>0<a<1\<close> too.\<close>
   1.515 +lemma power_inject_exp [simp]: "1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
   1.516    by (force simp add: order_antisym power_le_imp_le_exp)
   1.517  
   1.518 -text\<open>Can relax the first premise to @{term "0<a"} in the case of the
   1.519 -natural numbers.\<close>
   1.520 -lemma power_less_imp_less_exp:
   1.521 -  "1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n"
   1.522 -  by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"]
   1.523 -    power_le_imp_le_exp)
   1.524 +text \<open>
   1.525 +  Can relax the first premise to @{term "0<a"} in the case of the
   1.526 +  natural numbers.
   1.527 +\<close>
   1.528 +lemma power_less_imp_less_exp: "1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n"
   1.529 +  by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] power_le_imp_le_exp)
   1.530  
   1.531 -lemma power_strict_mono [rule_format]:
   1.532 -  "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n"
   1.533 -  by (induct n)
   1.534 -   (auto simp add: mult_strict_mono le_less_trans [of 0 a b])
   1.535 +lemma power_strict_mono [rule_format]: "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n"
   1.536 +  by (induct n) (auto simp: mult_strict_mono le_less_trans [of 0 a b])
   1.537  
   1.538  text\<open>Lemma for \<open>power_strict_decreasing\<close>\<close>
   1.539 -lemma power_Suc_less:
   1.540 -  "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n"
   1.541 -  by (induct n)
   1.542 -    (auto simp add: mult_strict_left_mono)
   1.543 +lemma power_Suc_less: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n"
   1.544 +  by (induct n) (auto simp: mult_strict_left_mono)
   1.545  
   1.546 -lemma power_strict_decreasing [rule_format]:
   1.547 -  "n < N \<Longrightarrow> 0 < a \<Longrightarrow> a < 1 \<longrightarrow> a ^ N < a ^ n"
   1.548 +lemma power_strict_decreasing [rule_format]: "n < N \<Longrightarrow> 0 < a \<Longrightarrow> a < 1 \<longrightarrow> a ^ N < a ^ n"
   1.549  proof (induct N)
   1.550 -  case 0 then show ?case by simp
   1.551 +  case 0
   1.552 +  then show ?case by simp
   1.553  next
   1.554 -  case (Suc N) then show ?case
   1.555 -  apply (auto simp add: power_Suc_less less_Suc_eq)
   1.556 -  apply (subgoal_tac "a * a^N < 1 * a^n")
   1.557 -  apply simp
   1.558 -  apply (rule mult_strict_mono) apply auto
   1.559 -  done
   1.560 +  case (Suc N)
   1.561 +  then show ?case
   1.562 +    apply (auto simp add: power_Suc_less less_Suc_eq)
   1.563 +    apply (subgoal_tac "a * a^N < 1 * a^n")
   1.564 +     apply simp
   1.565 +    apply (rule mult_strict_mono)
   1.566 +       apply auto
   1.567 +    done
   1.568  qed
   1.569  
   1.570 -text\<open>Proof resembles that of \<open>power_strict_decreasing\<close>\<close>
   1.571 -lemma power_decreasing [rule_format]:
   1.572 -  "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<longrightarrow> a ^ N \<le> a ^ n"
   1.573 +text \<open>Proof resembles that of \<open>power_strict_decreasing\<close>.\<close>
   1.574 +lemma power_decreasing: "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ N \<le> a ^ n"
   1.575  proof (induct N)
   1.576 -  case 0 then show ?case by simp
   1.577 +  case 0
   1.578 +  then show ?case by simp
   1.579  next
   1.580 -  case (Suc N) then show ?case
   1.581 -  apply (auto simp add: le_Suc_eq)
   1.582 -  apply (subgoal_tac "a * a^N \<le> 1 * a^n", simp)
   1.583 -  apply (rule mult_mono) apply auto
   1.584 -  done
   1.585 +  case (Suc N)
   1.586 +  then show ?case
   1.587 +    apply (auto simp add: le_Suc_eq)
   1.588 +    apply (subgoal_tac "a * a^N \<le> 1 * a^n")
   1.589 +     apply simp
   1.590 +    apply (rule mult_mono)
   1.591 +       apply auto
   1.592 +    done
   1.593  qed
   1.594  
   1.595 -lemma power_Suc_less_one:
   1.596 -  "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1"
   1.597 +lemma power_Suc_less_one: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1"
   1.598    using power_strict_decreasing [of 0 "Suc n" a] by simp
   1.599  
   1.600 -text\<open>Proof again resembles that of \<open>power_strict_decreasing\<close>\<close>
   1.601 -lemma power_increasing [rule_format]:
   1.602 -  "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
   1.603 +text \<open>Proof again resembles that of \<open>power_strict_decreasing\<close>.\<close>
   1.604 +lemma power_increasing: "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
   1.605  proof (induct N)
   1.606 -  case 0 then show ?case by simp
   1.607 +  case 0
   1.608 +  then show ?case by simp
   1.609  next
   1.610 -  case (Suc N) then show ?case
   1.611 -  apply (auto simp add: le_Suc_eq)
   1.612 -  apply (subgoal_tac "1 * a^n \<le> a * a^N", simp)
   1.613 -  apply (rule mult_mono) apply (auto simp add: order_trans [OF zero_le_one])
   1.614 -  done
   1.615 +  case (Suc N)
   1.616 +  then show ?case
   1.617 +    apply (auto simp add: le_Suc_eq)
   1.618 +    apply (subgoal_tac "1 * a^n \<le> a * a^N")
   1.619 +     apply simp
   1.620 +    apply (rule mult_mono)
   1.621 +       apply (auto simp add: order_trans [OF zero_le_one])
   1.622 +    done
   1.623  qed
   1.624  
   1.625 -text\<open>Lemma for \<open>power_strict_increasing\<close>\<close>
   1.626 -lemma power_less_power_Suc:
   1.627 -  "1 < a \<Longrightarrow> a ^ n < a * a ^ n"
   1.628 -  by (induct n) (auto simp add: mult_strict_left_mono less_trans [OF zero_less_one])
   1.629 +text \<open>Lemma for \<open>power_strict_increasing\<close>.\<close>
   1.630 +lemma power_less_power_Suc: "1 < a \<Longrightarrow> a ^ n < a * a ^ n"
   1.631 +  by (induct n) (auto simp: mult_strict_left_mono less_trans [OF zero_less_one])
   1.632  
   1.633 -lemma power_strict_increasing [rule_format]:
   1.634 -  "n < N \<Longrightarrow> 1 < a \<longrightarrow> a ^ n < a ^ N"
   1.635 +lemma power_strict_increasing: "n < N \<Longrightarrow> 1 < a \<Longrightarrow> a ^ n < a ^ N"
   1.636  proof (induct N)
   1.637 -  case 0 then show ?case by simp
   1.638 +  case 0
   1.639 +  then show ?case by simp
   1.640  next
   1.641 -  case (Suc N) then show ?case
   1.642 -  apply (auto simp add: power_less_power_Suc less_Suc_eq)
   1.643 -  apply (subgoal_tac "1 * a^n < a * a^N", simp)
   1.644 -  apply (rule mult_strict_mono) apply (auto simp add: less_trans [OF zero_less_one] less_imp_le)
   1.645 -  done
   1.646 +  case (Suc N)
   1.647 +  then show ?case
   1.648 +    apply (auto simp add: power_less_power_Suc less_Suc_eq)
   1.649 +    apply (subgoal_tac "1 * a^n < a * a^N")
   1.650 +     apply simp
   1.651 +    apply (rule mult_strict_mono)
   1.652 +    apply (auto simp add: less_trans [OF zero_less_one] less_imp_le)
   1.653 +    done
   1.654  qed
   1.655  
   1.656 -lemma power_increasing_iff [simp]:
   1.657 -  "1 < b \<Longrightarrow> b ^ x \<le> b ^ y \<longleftrightarrow> x \<le> y"
   1.658 +lemma power_increasing_iff [simp]: "1 < b \<Longrightarrow> b ^ x \<le> b ^ y \<longleftrightarrow> x \<le> y"
   1.659    by (blast intro: power_le_imp_le_exp power_increasing less_imp_le)
   1.660  
   1.661 -lemma power_strict_increasing_iff [simp]:
   1.662 -  "1 < b \<Longrightarrow> b ^ x < b ^ y \<longleftrightarrow> x < y"
   1.663 -by (blast intro: power_less_imp_less_exp power_strict_increasing)
   1.664 +lemma power_strict_increasing_iff [simp]: "1 < b \<Longrightarrow> b ^ x < b ^ y \<longleftrightarrow> x < y"
   1.665 +  by (blast intro: power_less_imp_less_exp power_strict_increasing)
   1.666  
   1.667  lemma power_le_imp_le_base:
   1.668    assumes le: "a ^ Suc n \<le> b ^ Suc n"
   1.669 -    and ynonneg: "0 \<le> b"
   1.670 +    and "0 \<le> b"
   1.671    shows "a \<le> b"
   1.672  proof (rule ccontr)
   1.673 -  assume "~ a \<le> b"
   1.674 +  assume "\<not> ?thesis"
   1.675    then have "b < a" by (simp only: linorder_not_le)
   1.676    then have "b ^ Suc n < a ^ Suc n"
   1.677 -    by (simp only: assms power_strict_mono)
   1.678 -  from le and this show False
   1.679 +    by (simp only: assms(2) power_strict_mono)
   1.680 +  with le show False
   1.681      by (simp add: linorder_not_less [symmetric])
   1.682  qed
   1.683  
   1.684 @@ -556,38 +517,31 @@
   1.685    assumes nonneg: "0 \<le> b"
   1.686    shows "a < b"
   1.687  proof (rule contrapos_pp [OF less])
   1.688 -  assume "~ a < b"
   1.689 -  hence "b \<le> a" by (simp only: linorder_not_less)
   1.690 -  hence "b ^ n \<le> a ^ n" using nonneg by (rule power_mono)
   1.691 -  thus "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less)
   1.692 +  assume "\<not> ?thesis"
   1.693 +  then have "b \<le> a" by (simp only: linorder_not_less)
   1.694 +  from this nonneg have "b ^ n \<le> a ^ n" by (rule power_mono)
   1.695 +  then show "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less)
   1.696  qed
   1.697  
   1.698 -lemma power_inject_base:
   1.699 -  "a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b"
   1.700 -by (blast intro: power_le_imp_le_base antisym eq_refl sym)
   1.701 +lemma power_inject_base: "a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b"
   1.702 +  by (blast intro: power_le_imp_le_base antisym eq_refl sym)
   1.703  
   1.704 -lemma power_eq_imp_eq_base:
   1.705 -  "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b"
   1.706 +lemma power_eq_imp_eq_base: "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b"
   1.707    by (cases n) (simp_all del: power_Suc, rule power_inject_base)
   1.708  
   1.709 -lemma power_eq_iff_eq_base:
   1.710 -  "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b"
   1.711 +lemma power_eq_iff_eq_base: "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b"
   1.712    using power_eq_imp_eq_base [of a n b] by auto
   1.713  
   1.714 -lemma power2_le_imp_le:
   1.715 -  "x\<^sup>2 \<le> y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
   1.716 +lemma power2_le_imp_le: "x\<^sup>2 \<le> y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
   1.717    unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
   1.718  
   1.719 -lemma power2_less_imp_less:
   1.720 -  "x\<^sup>2 < y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
   1.721 +lemma power2_less_imp_less: "x\<^sup>2 < y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
   1.722    by (rule power_less_imp_less_base)
   1.723  
   1.724 -lemma power2_eq_imp_eq:
   1.725 -  "x\<^sup>2 = y\<^sup>2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
   1.726 +lemma power2_eq_imp_eq: "x\<^sup>2 = y\<^sup>2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
   1.727    unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
   1.728  
   1.729 -lemma power_Suc_le_self:
   1.730 -  shows "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
   1.731 +lemma power_Suc_le_self: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
   1.732    using power_decreasing [of 1 "Suc n" a] by simp
   1.733  
   1.734  end
   1.735 @@ -595,16 +549,13 @@
   1.736  context linordered_ring_strict
   1.737  begin
   1.738  
   1.739 -lemma sum_squares_eq_zero_iff:
   1.740 -  "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.741 +lemma sum_squares_eq_zero_iff: "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.742    by (simp add: add_nonneg_eq_0_iff)
   1.743  
   1.744 -lemma sum_squares_le_zero_iff:
   1.745 -  "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.746 +lemma sum_squares_le_zero_iff: "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.747    by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
   1.748  
   1.749 -lemma sum_squares_gt_zero_iff:
   1.750 -  "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   1.751 +lemma sum_squares_gt_zero_iff: "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   1.752    by (simp add: not_le [symmetric] sum_squares_le_zero_iff)
   1.753  
   1.754  end
   1.755 @@ -620,28 +571,26 @@
   1.756  
   1.757  lemma zero_less_power_abs_iff [simp]: "0 < \<bar>a\<bar> ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
   1.758  proof (induct n)
   1.759 -  case 0 show ?case by simp
   1.760 +  case 0
   1.761 +  show ?case by simp
   1.762  next
   1.763 -  case (Suc n) show ?case by (auto simp add: Suc zero_less_mult_iff)
   1.764 +  case Suc
   1.765 +  then show ?case by (auto simp: zero_less_mult_iff)
   1.766  qed
   1.767  
   1.768  lemma zero_le_power_abs [simp]: "0 \<le> \<bar>a\<bar> ^ n"
   1.769    by (rule zero_le_power [OF abs_ge_zero])
   1.770  
   1.771 -lemma zero_le_power2 [simp]:
   1.772 -  "0 \<le> a\<^sup>2"
   1.773 +lemma zero_le_power2 [simp]: "0 \<le> a\<^sup>2"
   1.774    by (simp add: power2_eq_square)
   1.775  
   1.776 -lemma zero_less_power2 [simp]:
   1.777 -  "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0"
   1.778 +lemma zero_less_power2 [simp]: "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0"
   1.779    by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   1.780  
   1.781 -lemma power2_less_0 [simp]:
   1.782 -  "\<not> a\<^sup>2 < 0"
   1.783 +lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
   1.784    by (force simp add: power2_eq_square mult_less_0_iff)
   1.785  
   1.786 -lemma power2_less_eq_zero_iff [simp]:
   1.787 -  "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
   1.788 +lemma power2_less_eq_zero_iff [simp]: "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
   1.789    by (simp add: le_less)
   1.790  
   1.791  lemma abs_power2 [simp]: "\<bar>a\<^sup>2\<bar> = a\<^sup>2"
   1.792 @@ -650,8 +599,7 @@
   1.793  lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2"
   1.794    by (simp add: power2_eq_square)
   1.795  
   1.796 -lemma odd_power_less_zero:
   1.797 -  "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
   1.798 +lemma odd_power_less_zero: "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
   1.799  proof (induct n)
   1.800    case 0
   1.801    then show ?case by simp
   1.802 @@ -659,160 +607,152 @@
   1.803    case (Suc n)
   1.804    have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
   1.805      by (simp add: ac_simps power_add power2_eq_square)
   1.806 -  thus ?case
   1.807 +  then show ?case
   1.808      by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
   1.809  qed
   1.810  
   1.811 -lemma odd_0_le_power_imp_0_le:
   1.812 -  "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
   1.813 +lemma odd_0_le_power_imp_0_le: "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
   1.814    using odd_power_less_zero [of a n]
   1.815 -    by (force simp add: linorder_not_less [symmetric])
   1.816 +  by (force simp add: linorder_not_less [symmetric])
   1.817  
   1.818 -lemma zero_le_even_power'[simp]:
   1.819 -  "0 \<le> a ^ (2*n)"
   1.820 +lemma zero_le_even_power'[simp]: "0 \<le> a ^ (2*n)"
   1.821  proof (induct n)
   1.822    case 0
   1.823 -    show ?case by simp
   1.824 +  show ?case by simp
   1.825  next
   1.826    case (Suc n)
   1.827 -    have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
   1.828 -      by (simp add: ac_simps power_add power2_eq_square)
   1.829 -    thus ?case
   1.830 -      by (simp add: Suc zero_le_mult_iff)
   1.831 +  have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
   1.832 +    by (simp add: ac_simps power_add power2_eq_square)
   1.833 +  then show ?case
   1.834 +    by (simp add: Suc zero_le_mult_iff)
   1.835  qed
   1.836  
   1.837 -lemma sum_power2_ge_zero:
   1.838 -  "0 \<le> x\<^sup>2 + y\<^sup>2"
   1.839 +lemma sum_power2_ge_zero: "0 \<le> x\<^sup>2 + y\<^sup>2"
   1.840    by (intro add_nonneg_nonneg zero_le_power2)
   1.841  
   1.842 -lemma not_sum_power2_lt_zero:
   1.843 -  "\<not> x\<^sup>2 + y\<^sup>2 < 0"
   1.844 +lemma not_sum_power2_lt_zero: "\<not> x\<^sup>2 + y\<^sup>2 < 0"
   1.845    unfolding not_less by (rule sum_power2_ge_zero)
   1.846  
   1.847 -lemma sum_power2_eq_zero_iff:
   1.848 -  "x\<^sup>2 + y\<^sup>2 = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.849 +lemma sum_power2_eq_zero_iff: "x\<^sup>2 + y\<^sup>2 = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.850    unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff)
   1.851  
   1.852 -lemma sum_power2_le_zero_iff:
   1.853 -  "x\<^sup>2 + y\<^sup>2 \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.854 +lemma sum_power2_le_zero_iff: "x\<^sup>2 + y\<^sup>2 \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.855    by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero)
   1.856  
   1.857 -lemma sum_power2_gt_zero_iff:
   1.858 -  "0 < x\<^sup>2 + y\<^sup>2 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   1.859 +lemma sum_power2_gt_zero_iff: "0 < x\<^sup>2 + y\<^sup>2 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   1.860    unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff)
   1.861  
   1.862 -lemma abs_le_square_iff:
   1.863 -   "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> x\<^sup>2 \<le> y\<^sup>2"
   1.864 +lemma abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> x\<^sup>2 \<le> y\<^sup>2"
   1.865 +  (is "?lhs \<longleftrightarrow> ?rhs")
   1.866  proof
   1.867 -  assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
   1.868 -  then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono, simp)
   1.869 -  then show "x\<^sup>2 \<le> y\<^sup>2" by simp
   1.870 +  assume ?lhs
   1.871 +  then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono) simp
   1.872 +  then show ?rhs by simp
   1.873  next
   1.874 -  assume "x\<^sup>2 \<le> y\<^sup>2"
   1.875 -  then show "\<bar>x\<bar> \<le> \<bar>y\<bar>"
   1.876 +  assume ?rhs
   1.877 +  then show ?lhs
   1.878      by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
   1.879  qed
   1.880  
   1.881  lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> \<bar>x\<bar> \<le> 1"
   1.882 -  using abs_le_square_iff [of x 1]
   1.883 -  by simp
   1.884 +  using abs_le_square_iff [of x 1] by simp
   1.885  
   1.886  lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> \<bar>x\<bar> = 1"
   1.887    by (auto simp add: abs_if power2_eq_1_iff)
   1.888  
   1.889  lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> \<bar>x\<bar> < 1"
   1.890 -  using  abs_square_eq_1 [of x] abs_square_le_1 [of x]
   1.891 -  by (auto simp add: le_less)
   1.892 +  using  abs_square_eq_1 [of x] abs_square_le_1 [of x] by (auto simp add: le_less)
   1.893  
   1.894  end
   1.895  
   1.896  
   1.897  subsection \<open>Miscellaneous rules\<close>
   1.898  
   1.899 -lemma (in linordered_semidom) self_le_power:
   1.900 -  "1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n"
   1.901 +lemma (in linordered_semidom) self_le_power: "1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n"
   1.902    using power_increasing [of 1 n a] power_one_right [of a] by auto
   1.903  
   1.904 -lemma (in power) power_eq_if:
   1.905 -  "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
   1.906 +lemma (in power) power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
   1.907    unfolding One_nat_def by (cases m) simp_all
   1.908  
   1.909 -lemma (in comm_semiring_1) power2_sum:
   1.910 -  "(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y"
   1.911 +lemma (in comm_semiring_1) power2_sum: "(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y"
   1.912    by (simp add: algebra_simps power2_eq_square mult_2_right)
   1.913  
   1.914 -lemma (in comm_ring_1) power2_diff:
   1.915 -  "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
   1.916 +context comm_ring_1
   1.917 +begin
   1.918 +
   1.919 +lemma power2_diff: "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
   1.920    by (simp add: algebra_simps power2_eq_square mult_2_right)
   1.921  
   1.922 -lemma (in comm_ring_1) power2_commute:
   1.923 -  "(x - y)\<^sup>2 = (y - x)\<^sup>2"
   1.924 +lemma power2_commute: "(x - y)\<^sup>2 = (y - x)\<^sup>2"
   1.925    by (simp add: algebra_simps power2_eq_square)
   1.926  
   1.927 -lemma (in comm_ring_1) minus_power_mult_self:
   1.928 -  "(- a) ^ n * (- a) ^ n = a ^ (2 * n)"
   1.929 -  by (simp add: power_mult_distrib [symmetric]) (simp add: power2_eq_square [symmetric] power_mult [symmetric])
   1.930 -  
   1.931 -lemma (in comm_ring_1) minus_one_mult_self [simp]:
   1.932 -  "(- 1) ^ n * (- 1) ^ n = 1"
   1.933 +lemma minus_power_mult_self: "(- a) ^ n * (- a) ^ n = a ^ (2 * n)"
   1.934 +  by (simp add: power_mult_distrib [symmetric])
   1.935 +    (simp add: power2_eq_square [symmetric] power_mult [symmetric])
   1.936 +
   1.937 +lemma minus_one_mult_self [simp]: "(- 1) ^ n * (- 1) ^ n = 1"
   1.938    using minus_power_mult_self [of 1 n] by simp
   1.939  
   1.940 -lemma (in comm_ring_1) left_minus_one_mult_self [simp]:
   1.941 -  "(- 1) ^ n * ((- 1) ^ n * a) = a"
   1.942 +lemma left_minus_one_mult_self [simp]: "(- 1) ^ n * ((- 1) ^ n * a) = a"
   1.943    by (simp add: mult.assoc [symmetric])
   1.944  
   1.945 +end
   1.946 +
   1.947  text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
   1.948  
   1.949  lemmas zero_compare_simps =
   1.950 -    add_strict_increasing add_strict_increasing2 add_increasing
   1.951 -    zero_le_mult_iff zero_le_divide_iff
   1.952 -    zero_less_mult_iff zero_less_divide_iff
   1.953 -    mult_le_0_iff divide_le_0_iff
   1.954 -    mult_less_0_iff divide_less_0_iff
   1.955 -    zero_le_power2 power2_less_0
   1.956 +  add_strict_increasing add_strict_increasing2 add_increasing
   1.957 +  zero_le_mult_iff zero_le_divide_iff
   1.958 +  zero_less_mult_iff zero_less_divide_iff
   1.959 +  mult_le_0_iff divide_le_0_iff
   1.960 +  mult_less_0_iff divide_less_0_iff
   1.961 +  zero_le_power2 power2_less_0
   1.962  
   1.963  
   1.964  subsection \<open>Exponentiation for the Natural Numbers\<close>
   1.965  
   1.966 -lemma nat_one_le_power [simp]:
   1.967 -  "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n"
   1.968 +lemma nat_one_le_power [simp]: "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n"
   1.969    by (rule one_le_power [of i n, unfolded One_nat_def])
   1.970  
   1.971 -lemma nat_zero_less_power_iff [simp]:
   1.972 -  "x ^ n > 0 \<longleftrightarrow> x > (0::nat) \<or> n = 0"
   1.973 +lemma nat_zero_less_power_iff [simp]: "x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
   1.974 +  for x :: nat
   1.975    by (induct n) auto
   1.976  
   1.977 -lemma nat_power_eq_Suc_0_iff [simp]:
   1.978 -  "x ^ m = Suc 0 \<longleftrightarrow> m = 0 \<or> x = Suc 0"
   1.979 +lemma nat_power_eq_Suc_0_iff [simp]: "x ^ m = Suc 0 \<longleftrightarrow> m = 0 \<or> x = Suc 0"
   1.980    by (induct m) auto
   1.981  
   1.982 -lemma power_Suc_0 [simp]:
   1.983 -  "Suc 0 ^ n = Suc 0"
   1.984 +lemma power_Suc_0 [simp]: "Suc 0 ^ n = Suc 0"
   1.985    by simp
   1.986  
   1.987 -text\<open>Valid for the naturals, but what if \<open>0<i<1\<close>?
   1.988 -Premises cannot be weakened: consider the case where @{term "i=0"},
   1.989 -@{term "m=1"} and @{term "n=0"}.\<close>
   1.990 +text \<open>
   1.991 +  Valid for the naturals, but what if \<open>0 < i < 1\<close>? Premises cannot be
   1.992 +  weakened: consider the case where \<open>i = 0\<close>, \<open>m = 1\<close> and \<open>n = 0\<close>.
   1.993 +\<close>
   1.994 +
   1.995  lemma nat_power_less_imp_less:
   1.996 -  assumes nonneg: "0 < (i::nat)"
   1.997 +  fixes i :: nat
   1.998 +  assumes nonneg: "0 < i"
   1.999    assumes less: "i ^ m < i ^ n"
  1.1000    shows "m < n"
  1.1001  proof (cases "i = 1")
  1.1002 -  case True with less power_one [where 'a = nat] show ?thesis by simp
  1.1003 +  case True
  1.1004 +  with less power_one [where 'a = nat] show ?thesis by simp
  1.1005  next
  1.1006 -  case False with nonneg have "1 < i" by auto
  1.1007 +  case False
  1.1008 +  with nonneg have "1 < i" by auto
  1.1009    from power_strict_increasing_iff [OF this] less show ?thesis ..
  1.1010  qed
  1.1011  
  1.1012 -lemma power_dvd_imp_le:
  1.1013 -  "i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n"
  1.1014 -  apply (rule power_le_imp_le_exp, assumption)
  1.1015 -  apply (erule dvd_imp_le, simp)
  1.1016 +lemma power_dvd_imp_le: "i ^ m dvd i ^ n \<Longrightarrow> 1 < i \<Longrightarrow> m \<le> n"
  1.1017 +  for i m n :: nat
  1.1018 +  apply (rule power_le_imp_le_exp)
  1.1019 +   apply assumption
  1.1020 +  apply (erule dvd_imp_le)
  1.1021 +  apply simp
  1.1022    done
  1.1023  
  1.1024 -lemma power2_nat_le_eq_le:
  1.1025 -  fixes m n :: nat
  1.1026 -  shows "m\<^sup>2 \<le> n\<^sup>2 \<longleftrightarrow> m \<le> n"
  1.1027 +lemma power2_nat_le_eq_le: "m\<^sup>2 \<le> n\<^sup>2 \<longleftrightarrow> m \<le> n"
  1.1028 +  for m n :: nat
  1.1029    by (auto intro: power2_le_imp_le power_mono)
  1.1030  
  1.1031  lemma power2_nat_le_imp_le:
  1.1032 @@ -820,18 +760,20 @@
  1.1033    assumes "m\<^sup>2 \<le> n"
  1.1034    shows "m \<le> n"
  1.1035  proof (cases m)
  1.1036 -  case 0 then show ?thesis by simp
  1.1037 +  case 0
  1.1038 +  then show ?thesis by simp
  1.1039  next
  1.1040    case (Suc k)
  1.1041    show ?thesis
  1.1042    proof (rule ccontr)
  1.1043 -    assume "\<not> m \<le> n"
  1.1044 +    assume "\<not> ?thesis"
  1.1045      then have "n < m" by simp
  1.1046      with assms Suc show False
  1.1047        by (simp add: power2_eq_square)
  1.1048    qed
  1.1049  qed
  1.1050  
  1.1051 +
  1.1052  subsubsection \<open>Cardinality of the Powerset\<close>
  1.1053  
  1.1054  lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
  1.1055 @@ -840,16 +782,17 @@
  1.1056  lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
  1.1057  proof (induct rule: finite_induct)
  1.1058    case empty
  1.1059 -    show ?case by auto
  1.1060 +  show ?case by auto
  1.1061  next
  1.1062    case (insert x A)
  1.1063    then have "inj_on (insert x) (Pow A)"
  1.1064      unfolding inj_on_def by (blast elim!: equalityE)
  1.1065    then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A"
  1.1066      by (simp add: mult_2 card_image Pow_insert insert.hyps)
  1.1067 -  then show ?case using insert
  1.1068 +  with insert show ?case
  1.1069      apply (simp add: Pow_insert)
  1.1070 -    apply (subst card_Un_disjoint, auto)
  1.1071 +    apply (subst card_Un_disjoint)
  1.1072 +       apply auto
  1.1073      done
  1.1074  qed
  1.1075