src/HOL/Power.thy
changeset 15251 bb6f072c8d10
parent 15140 322485b816ac
child 16733 236dfafbeb63
     1.1 --- a/src/HOL/Power.thy	Mon Oct 18 13:40:45 2004 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue Oct 19 18:18:45 2004 +0200
     1.3 @@ -22,10 +22,10 @@
     1.4  
     1.5  text{*It looks plausible as a simprule, but its effect can be strange.*}
     1.6  lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::recpower))"
     1.7 -by (induct_tac "n", auto)
     1.8 +by (induct "n", auto)
     1.9  
    1.10  lemma power_one [simp]: "1^n = (1::'a::recpower)"
    1.11 -apply (induct_tac "n")
    1.12 +apply (induct "n")
    1.13  apply (auto simp add: power_Suc)
    1.14  done
    1.15  
    1.16 @@ -33,23 +33,23 @@
    1.17  by (simp add: power_Suc)
    1.18  
    1.19  lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)"
    1.20 -apply (induct_tac "n")
    1.21 +apply (induct "n")
    1.22  apply (simp_all add: power_Suc mult_ac)
    1.23  done
    1.24  
    1.25  lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n"
    1.26 -apply (induct_tac "n")
    1.27 +apply (induct "n")
    1.28  apply (simp_all add: power_Suc power_add)
    1.29  done
    1.30  
    1.31  lemma power_mult_distrib: "((a::'a::recpower) * b) ^ n = (a^n) * (b^n)"
    1.32 -apply (induct_tac "n")
    1.33 +apply (induct "n")
    1.34  apply (auto simp add: power_Suc mult_ac)
    1.35  done
    1.36  
    1.37  lemma zero_less_power:
    1.38       "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n"
    1.39 -apply (induct_tac "n")
    1.40 +apply (induct "n")
    1.41  apply (simp_all add: power_Suc zero_less_one mult_pos)
    1.42  done
    1.43  
    1.44 @@ -62,7 +62,7 @@
    1.45  
    1.46  lemma one_le_power:
    1.47       "1 \<le> (a::'a::{ordered_semidom,recpower}) ==> 1 \<le> a^n"
    1.48 -apply (induct_tac "n")
    1.49 +apply (induct "n")
    1.50  apply (simp_all add: power_Suc)
    1.51  apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
    1.52  apply (simp_all add: zero_le_one order_trans [OF zero_le_one])
    1.53 @@ -124,7 +124,7 @@
    1.54  
    1.55  lemma power_mono:
    1.56       "[|a \<le> b; (0::'a::{recpower,ordered_semidom}) \<le> a|] ==> a^n \<le> b^n"
    1.57 -apply (induct_tac "n")
    1.58 +apply (induct "n")
    1.59  apply (simp_all add: power_Suc)
    1.60  apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b])
    1.61  done
    1.62 @@ -132,20 +132,20 @@
    1.63  lemma power_strict_mono [rule_format]:
    1.64       "[|a < b; (0::'a::{recpower,ordered_semidom}) \<le> a|]
    1.65        ==> 0 < n --> a^n < b^n"
    1.66 -apply (induct_tac "n")
    1.67 +apply (induct "n")
    1.68  apply (auto simp add: mult_strict_mono zero_le_power power_Suc
    1.69                        order_le_less_trans [of 0 a b])
    1.70  done
    1.71  
    1.72  lemma power_eq_0_iff [simp]:
    1.73       "(a^n = 0) = (a = (0::'a::{ordered_idom,recpower}) & 0<n)"
    1.74 -apply (induct_tac "n")
    1.75 +apply (induct "n")
    1.76  apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
    1.77  done
    1.78  
    1.79  lemma field_power_eq_0_iff [simp]:
    1.80       "(a^n = 0) = (a = (0::'a::{field,recpower}) & 0<n)"
    1.81 -apply (induct_tac "n")
    1.82 +apply (induct "n")
    1.83  apply (auto simp add: power_Suc field_mult_eq_0_iff zero_neq_one[THEN not_sym])
    1.84  done
    1.85  
    1.86 @@ -154,14 +154,14 @@
    1.87  
    1.88  lemma nonzero_power_inverse:
    1.89    "a \<noteq> 0 ==> inverse ((a::'a::{field,recpower}) ^ n) = (inverse a) ^ n"
    1.90 -apply (induct_tac "n")
    1.91 +apply (induct "n")
    1.92  apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute)
    1.93  done
    1.94  
    1.95  text{*Perhaps these should be simprules.*}
    1.96  lemma power_inverse:
    1.97    "inverse ((a::'a::{field,division_by_zero,recpower}) ^ n) = (inverse a) ^ n"
    1.98 -apply (induct_tac "n")
    1.99 +apply (induct "n")
   1.100  apply (auto simp add: power_Suc inverse_mult_distrib)
   1.101  done
   1.102  
   1.103 @@ -177,7 +177,7 @@
   1.104  done
   1.105  
   1.106  lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,recpower}) ^ n"
   1.107 -apply (induct_tac "n")
   1.108 +apply (induct "n")
   1.109  apply (auto simp add: power_Suc abs_mult)
   1.110  done
   1.111  
   1.112 @@ -193,7 +193,7 @@
   1.113  
   1.114  lemma zero_le_power_abs [simp]:
   1.115       "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n"
   1.116 -apply (induct_tac "n")
   1.117 +apply (induct "n")
   1.118  apply (auto simp add: zero_le_one zero_le_power)
   1.119  done
   1.120  
   1.121 @@ -207,7 +207,7 @@
   1.122  lemma power_Suc_less:
   1.123       "[|(0::'a::{ordered_semidom,recpower}) < a; a < 1|]
   1.124        ==> a * a^n < a^n"
   1.125 -apply (induct_tac n)
   1.126 +apply (induct n)
   1.127  apply (auto simp add: power_Suc mult_strict_left_mono)
   1.128  done
   1.129  
   1.130 @@ -215,7 +215,7 @@
   1.131       "[|n < N; 0 < a; a < (1::'a::{ordered_semidom,recpower})|]
   1.132        ==> a^N < a^n"
   1.133  apply (erule rev_mp)
   1.134 -apply (induct_tac "N")
   1.135 +apply (induct "N")
   1.136  apply (auto simp add: power_Suc power_Suc_less less_Suc_eq)
   1.137  apply (rename_tac m)
   1.138  apply (subgoal_tac "a * a^m < 1 * a^n", simp)
   1.139 @@ -228,7 +228,7 @@
   1.140       "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semidom,recpower})|]
   1.141        ==> a^N \<le> a^n"
   1.142  apply (erule rev_mp)
   1.143 -apply (induct_tac "N")
   1.144 +apply (induct "N")
   1.145  apply (auto simp add: power_Suc  le_Suc_eq)
   1.146  apply (rename_tac m)
   1.147  apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
   1.148 @@ -245,7 +245,7 @@
   1.149  lemma power_increasing:
   1.150       "[|n \<le> N; (1::'a::{ordered_semidom,recpower}) \<le> a|] ==> a^n \<le> a^N"
   1.151  apply (erule rev_mp)
   1.152 -apply (induct_tac "N")
   1.153 +apply (induct "N")
   1.154  apply (auto simp add: power_Suc le_Suc_eq)
   1.155  apply (rename_tac m)
   1.156  apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
   1.157 @@ -256,14 +256,14 @@
   1.158  text{*Lemma for @{text power_strict_increasing}*}
   1.159  lemma power_less_power_Suc:
   1.160       "(1::'a::{ordered_semidom,recpower}) < a ==> a^n < a * a^n"
   1.161 -apply (induct_tac n)
   1.162 +apply (induct n)
   1.163  apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
   1.164  done
   1.165  
   1.166  lemma power_strict_increasing:
   1.167       "[|n < N; (1::'a::{ordered_semidom,recpower}) < a|] ==> a^n < a^N"
   1.168  apply (erule rev_mp)
   1.169 -apply (induct_tac "N")
   1.170 +apply (induct "N")
   1.171  apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
   1.172  apply (rename_tac m)
   1.173  apply (subgoal_tac "1 * a^n < a * a^m", simp)
   1.174 @@ -332,10 +332,10 @@
   1.175  done
   1.176  
   1.177  lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
   1.178 -by (induct_tac "n", auto)
   1.179 +by (induct "n", auto)
   1.180  
   1.181  lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
   1.182 -apply (induct_tac "j")
   1.183 +apply (induct "j")
   1.184  apply (simp_all add: le_Suc_eq)
   1.185  apply (blast dest!: dvd_mult_right)
   1.186  done
   1.187 @@ -371,7 +371,7 @@
   1.188  by simp
   1.189  
   1.190  lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
   1.191 -apply (induct_tac "n", auto)
   1.192 +apply (induct "n", auto)
   1.193  apply (erule allE)
   1.194  apply (erule mp, arith)
   1.195  done
   1.196 @@ -379,15 +379,15 @@
   1.197  declare binomial_0 [simp del] binomial_Suc [simp del]
   1.198  
   1.199  lemma binomial_n_n [simp]: "(n choose n) = 1"
   1.200 -apply (induct_tac "n")
   1.201 +apply (induct "n")
   1.202  apply (simp_all add: binomial_eq_0)
   1.203  done
   1.204  
   1.205  lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
   1.206 -by (induct_tac "n", simp_all)
   1.207 +by (induct "n", simp_all)
   1.208  
   1.209  lemma binomial_1 [simp]: "(n choose Suc 0) = n"
   1.210 -by (induct_tac "n", simp_all)
   1.211 +by (induct "n", simp_all)
   1.212  
   1.213  lemma zero_less_binomial [rule_format]: "k \<le> n --> 0 < (n choose k)"
   1.214  by (rule_tac m = n and n = k in diff_induct, simp_all)
   1.215 @@ -404,7 +404,7 @@
   1.216  (*Might be more useful if re-oriented*)
   1.217  lemma Suc_times_binomial_eq [rule_format]:
   1.218       "\<forall>k. k \<le> n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
   1.219 -apply (induct_tac "n")
   1.220 +apply (induct "n")
   1.221  apply (simp add: binomial_0, clarify)
   1.222  apply (case_tac "k")
   1.223  apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq