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.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.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.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.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.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.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")