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.39 -  by (induct n) (simp_all add: power_Suc power_add)
    1.40 +  by (induct n) (simp_all add: power_add)
    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.55 -apply (simp add: order_le_less)
    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.64 -apply (simp_all add: power_Suc)
    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.82 +by (simp add: power_gt1_lemma)
    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.108 -apply (simp_all add: power_Suc)
   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*}