src/HOL/Power.thy
 changeset 30273 ecd6f0ca62ea parent 30242 aea5d7fa7ef5 child 30313 b2441b0c8d38
```     1.1 --- a/src/HOL/Power.thy	Thu Mar 05 00:16:28 2009 +0100
1.2 +++ b/src/HOL/Power.thy	Wed Mar 04 17:12:23 2009 -0800
1.3 @@ -18,55 +18,50 @@
1.4
1.5  class recpower = monoid_mult + power +
1.6    assumes power_0 [simp]: "a ^ 0       = 1"
1.7 -  assumes power_Suc:      "a ^ Suc n = a * (a ^ n)"
1.8 +  assumes power_Suc [simp]: "a ^ Suc n = a * (a ^ n)"
1.9
1.10  lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
1.11 -  by (simp add: power_Suc)
1.12 +  by simp
1.13
1.14  text{*It looks plausible as a simprule, but its effect can be strange.*}
1.15  lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::{recpower,semiring_0}))"
1.16    by (induct n) simp_all
1.17
1.18  lemma power_one [simp]: "1^n = (1::'a::recpower)"
1.19 -  by (induct n) (simp_all add: power_Suc)
1.20 +  by (induct n) simp_all
1.21
1.22  lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
1.23 -  unfolding One_nat_def by (simp add: power_Suc)
1.24 +  unfolding One_nat_def by simp
1.25
1.26  lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
1.27 -  by (induct n) (simp_all add: power_Suc mult_assoc)
1.28 +  by (induct n) (simp_all add: mult_assoc)
1.29
1.30  lemma power_Suc2: "(a::'a::recpower) ^ Suc n = a ^ n * a"
1.31 -  by (simp add: power_Suc power_commutes)
1.32 +  by (simp add: power_commutes)
1.33
1.34  lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)"
1.35 -  by (induct m) (simp_all add: power_Suc mult_ac)
1.36 +  by (induct m) (simp_all add: mult_ac)
1.37
1.38  lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n"
1.41
1.42  lemma power_mult_distrib: "((a::'a::{recpower,comm_monoid_mult}) * b) ^ n = (a^n) * (b^n)"
1.43 -  by (induct n) (simp_all add: power_Suc mult_ac)
1.44 +  by (induct n) (simp_all add: mult_ac)
1.45
1.46  lemma zero_less_power[simp]:
1.47       "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n"
1.48 -apply (induct "n")
1.49 -apply (simp_all add: power_Suc zero_less_one mult_pos_pos)
1.50 -done
1.51 +by (induct n) (simp_all add: mult_pos_pos)
1.52
1.53  lemma zero_le_power[simp]:
1.54       "0 \<le> (a::'a::{ordered_semidom,recpower}) ==> 0 \<le> a^n"
1.56 -apply (erule disjE)
1.57 -apply (simp_all add: zero_less_one power_0_left)
1.58 -done
1.59 +by (induct n) (simp_all add: mult_nonneg_nonneg)
1.60
1.61  lemma one_le_power[simp]:
1.62       "1 \<le> (a::'a::{ordered_semidom,recpower}) ==> 1 \<le> a^n"
1.63  apply (induct "n")
1.65 +apply simp_all
1.66  apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
1.67 -apply (simp_all add: zero_le_one order_trans [OF zero_le_one])
1.68 +apply (simp_all add: order_trans [OF zero_le_one])
1.69  done
1.70
1.71  lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semidom)"
1.72 @@ -85,11 +80,11 @@
1.73
1.74  lemma one_less_power[simp]:
1.75    "\<lbrakk>1 < (a::'a::{ordered_semidom,recpower}); 0 < n\<rbrakk> \<Longrightarrow> 1 < a ^ n"
1.76 -by (cases n, simp_all add: power_gt1_lemma power_Suc)
1.77 +by (cases n, simp_all add: power_gt1_lemma)
1.78
1.79  lemma power_gt1:
1.80       "1 < (a::'a::{ordered_semidom,recpower}) ==> 1 < a ^ (Suc n)"
1.81 -by (simp add: power_gt1_lemma power_Suc)
1.83
1.84  lemma power_le_imp_le_exp:
1.85    assumes gt1: "(1::'a::{recpower,ordered_semidom}) < a"
1.86 @@ -102,7 +97,7 @@
1.87    show ?case
1.88    proof (cases n)
1.89      case 0
1.90 -    from prems have "a * a^m \<le> 1" by (simp add: power_Suc)
1.91 +    from prems have "a * a^m \<le> 1" by simp
1.92      with gt1 show ?thesis
1.93        by (force simp only: power_gt1_lemma
1.94            linorder_not_less [symmetric])
1.95 @@ -110,7 +105,7 @@
1.96      case (Suc n)
1.97      from prems show ?thesis
1.98        by (force dest: mult_left_le_imp_le
1.99 -          simp add: power_Suc order_less_trans [OF zero_less_one gt1])
1.100 +          simp add: order_less_trans [OF zero_less_one gt1])
1.101    qed
1.102  qed
1.103
1.104 @@ -130,7 +125,7 @@
1.105  lemma power_mono:
1.106       "[|a \<le> b; (0::'a::{recpower,ordered_semidom}) \<le> a|] ==> a^n \<le> b^n"
1.107  apply (induct "n")
1.109 +apply simp_all
1.110  apply (auto intro: mult_mono order_trans [of 0 a b])
1.111  done
1.112
1.113 @@ -138,15 +133,14 @@
1.114       "[|a < b; (0::'a::{recpower,ordered_semidom}) \<le> a|]
1.115        ==> 0 < n --> a^n < b^n"
1.116  apply (induct "n")
1.117 -apply (auto simp add: mult_strict_mono power_Suc
1.118 -                      order_le_less_trans [of 0 a b])
1.119 +apply (auto simp add: mult_strict_mono order_le_less_trans [of 0 a b])
1.120  done
1.121
1.122  lemma power_eq_0_iff [simp]:
1.123    "(a^n = 0) \<longleftrightarrow>
1.124     (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\<noteq>0)"
1.125  apply (induct "n")
1.126 -apply (auto simp add: power_Suc zero_neq_one [THEN not_sym] no_zero_divisors)
1.127 +apply (auto simp add: no_zero_divisors)
1.128  done
1.129
1.130
1.131 @@ -158,7 +152,7 @@
1.132    fixes a :: "'a::{division_ring,recpower}"
1.133    shows "a \<noteq> 0 ==> inverse (a ^ n) = (inverse a) ^ n"
1.134  apply (induct "n")
1.135 -apply (auto simp add: power_Suc nonzero_inverse_mult_distrib power_commutes)
1.136 +apply (auto simp add: nonzero_inverse_mult_distrib power_commutes)
1.137  done (* TODO: reorient or rename to nonzero_inverse_power *)
1.138
1.139  text{*Perhaps these should be simprules.*}
1.140 @@ -189,18 +183,17 @@
1.141
1.142  lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,recpower}) ^ n"
1.143  apply (induct "n")
1.144 -apply (auto simp add: power_Suc abs_mult)
1.145 +apply (auto simp add: abs_mult)
1.146  done
1.147
1.148  lemma zero_less_power_abs_iff [simp,noatp]:
1.149       "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)"
1.150  proof (induct "n")
1.151    case 0
1.152 -    show ?case by (simp add: zero_less_one)
1.153 +    show ?case by simp
1.154  next
1.155    case (Suc n)
1.156 -    show ?case by (auto simp add: prems power_Suc zero_less_mult_iff
1.157 -      abs_zero)
1.158 +    show ?case by (auto simp add: prems zero_less_mult_iff)
1.159  qed
1.160
1.161  lemma zero_le_power_abs [simp]:
1.162 @@ -212,7 +205,7 @@
1.163    case 0 show ?case by simp
1.164  next
1.165    case (Suc n) then show ?case
1.166 -    by (simp add: power_Suc2 mult_assoc)
1.167 +    by (simp del: power_Suc add: power_Suc2 mult_assoc)
1.168  qed
1.169
1.170  text{*Lemma for @{text power_strict_decreasing}*}
1.171 @@ -220,7 +213,7 @@
1.172       "[|(0::'a::{ordered_semidom,recpower}) < a; a < 1|]
1.173        ==> a * a^n < a^n"
1.174  apply (induct n)
1.175 -apply (auto simp add: power_Suc mult_strict_left_mono)
1.176 +apply (auto simp add: mult_strict_left_mono)
1.177  done
1.178
1.179  lemma power_strict_decreasing:
1.180 @@ -228,11 +221,11 @@
1.181        ==> a^N < a^n"
1.182  apply (erule rev_mp)
1.183  apply (induct "N")
1.184 -apply (auto simp add: power_Suc power_Suc_less less_Suc_eq)
1.185 +apply (auto simp add: power_Suc_less less_Suc_eq)
1.186  apply (rename_tac m)
1.187  apply (subgoal_tac "a * a^m < 1 * a^n", simp)
1.188  apply (rule mult_strict_mono)
1.189 -apply (auto simp add: zero_less_one order_less_imp_le)
1.190 +apply (auto simp add: order_less_imp_le)
1.191  done
1.192
1.193  text{*Proof resembles that of @{text power_strict_decreasing}*}
1.194 @@ -241,11 +234,11 @@
1.195        ==> a^N \<le> a^n"
1.196  apply (erule rev_mp)
1.197  apply (induct "N")
1.198 -apply (auto simp add: power_Suc  le_Suc_eq)
1.199 +apply (auto simp add: le_Suc_eq)
1.200  apply (rename_tac m)
1.201  apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
1.202  apply (rule mult_mono)
1.203 -apply (auto simp add: zero_le_one)
1.204 +apply auto
1.205  done
1.206
1.207  lemma power_Suc_less_one:
1.208 @@ -258,7 +251,7 @@
1.209       "[|n \<le> N; (1::'a::{ordered_semidom,recpower}) \<le> a|] ==> a^n \<le> a^N"
1.210  apply (erule rev_mp)
1.211  apply (induct "N")
1.212 -apply (auto simp add: power_Suc le_Suc_eq)
1.213 +apply (auto simp add: le_Suc_eq)
1.214  apply (rename_tac m)
1.215  apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
1.216  apply (rule mult_mono)
1.217 @@ -269,14 +262,14 @@
1.218  lemma power_less_power_Suc:
1.219       "(1::'a::{ordered_semidom,recpower}) < a ==> a^n < a * a^n"
1.220  apply (induct n)
1.221 -apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
1.222 +apply (auto simp add: mult_strict_left_mono order_less_trans [OF zero_less_one])
1.223  done
1.224
1.225  lemma power_strict_increasing:
1.226       "[|n < N; (1::'a::{ordered_semidom,recpower}) < a|] ==> a^n < a^N"
1.227  apply (erule rev_mp)
1.228  apply (induct "N")
1.229 -apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
1.230 +apply (auto simp add: power_less_power_Suc less_Suc_eq)
1.231  apply (rename_tac m)
1.232  apply (subgoal_tac "1 * a^n < a * a^m", simp)
1.233  apply (rule mult_strict_mono)
1.234 @@ -324,7 +317,7 @@
1.235  lemma power_eq_imp_eq_base:
1.236    fixes a b :: "'a::{ordered_semidom,recpower}"
1.237    shows "\<lbrakk>a ^ n = b ^ n; 0 \<le> a; 0 \<le> b; 0 < n\<rbrakk> \<Longrightarrow> a = b"
1.238 -by (cases n, simp_all, rule power_inject_base)
1.239 +by (cases n, simp_all del: power_Suc, rule power_inject_base)
1.240
1.241  text {* The divides relation *}
1.242
1.243 @@ -360,11 +353,13 @@
1.244    show "z^(Suc n) = z * (z^n)" by simp
1.245  qed
1.246
1.247 +declare power_nat.simps [simp del]
1.248 +
1.249  end
1.250
1.251  lemma of_nat_power:
1.252    "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
1.253 -by (induct n, simp_all add: power_Suc of_nat_mult)
1.254 +by (induct n, simp_all add: of_nat_mult)
1.255
1.256  lemma nat_one_le_power [simp]: "Suc 0 \<le> i ==> Suc 0 \<le> i^n"
1.257  by (rule one_le_power [of i n, unfolded One_nat_def])
1.258 @@ -397,7 +392,7 @@
1.259    assumes nz: "a ~= 0"
1.260    shows "n <= m ==> (a::'a::{recpower, field}) ^ (m-n) = (a^m) / (a^n)"
1.261    by (induct m n rule: diff_induct)
1.262 -    (simp_all add: power_Suc nonzero_mult_divide_cancel_left nz)
1.263 +    (simp_all add: nonzero_mult_divide_cancel_left nz)
1.264
1.265
1.266  text{*ML bindings for the general exponentiation theorems*}
```