author  haftmann 
Fri, 05 Feb 2010 14:33:50 +0100  
changeset 35028  108662d50512 
parent 33364  2bd12592c5e8 
child 35216  7641e8d831d2 
permissions  rwrr 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

1 
(* Title: HOL/Power.thy 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

3 
Copyright 1997 University of Cambridge 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

4 
*) 
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

5 

30960  6 
header {* Exponentiation *} 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

7 

15131  8 
theory Power 
21413  9 
imports Nat 
15131  10 
begin 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

11 

30960  12 
subsection {* Powers for Arbitrary Monoids *} 
13 

30996  14 
class power = one + times 
30960  15 
begin 
24996  16 

30960  17 
primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) where 
18 
power_0: "a ^ 0 = 1" 

19 
 power_Suc: "a ^ Suc n = a * a ^ n" 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

20 

30996  21 
notation (latex output) 
22 
power ("(_\<^bsup>_\<^esup>)" [1000] 1000) 

23 

24 
notation (HTML output) 

25 
power ("(_\<^bsup>_\<^esup>)" [1000] 1000) 

26 

30960  27 
end 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

28 

30996  29 
context monoid_mult 
30 
begin 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

31 

30996  32 
subclass power .. 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

33 

30996  34 
lemma power_one [simp]: 
35 
"1 ^ n = 1" 

30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30242
diff
changeset

36 
by (induct n) simp_all 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

37 

30996  38 
lemma power_one_right [simp]: 
31001  39 
"a ^ 1 = a" 
30996  40 
by simp 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

41 

30996  42 
lemma power_commutes: 
43 
"a ^ n * a = a * a ^ n" 

30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30242
diff
changeset

44 
by (induct n) (simp_all add: mult_assoc) 
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
17149
diff
changeset

45 

30996  46 
lemma power_Suc2: 
47 
"a ^ Suc n = a ^ n * a" 

30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30242
diff
changeset

48 
by (simp add: power_commutes) 
28131
3130d7b3149d
add lemma power_Suc2; generalize power_minus from class comm_ring_1 to ring_1
huffman
parents:
25874
diff
changeset

49 

30996  50 
lemma power_add: 
51 
"a ^ (m + n) = a ^ m * a ^ n" 

52 
by (induct m) (simp_all add: algebra_simps) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

53 

30996  54 
lemma power_mult: 
55 
"a ^ (m * n) = (a ^ m) ^ n" 

30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30242
diff
changeset

56 
by (induct n) (simp_all add: power_add) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

57 

30996  58 
end 
59 

60 
context comm_monoid_mult 

61 
begin 

62 

63 
lemma power_mult_distrib: 

64 
"(a * b) ^ n = (a ^ n) * (b ^ n)" 

30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30242
diff
changeset

65 
by (induct n) (simp_all add: mult_ac) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

66 

30996  67 
end 
68 

69 
context semiring_1 

70 
begin 

71 

72 
lemma of_nat_power: 

73 
"of_nat (m ^ n) = of_nat m ^ n" 

74 
by (induct n) (simp_all add: of_nat_mult) 

75 

76 
end 

77 

78 
context comm_semiring_1 

79 
begin 

80 

81 
text {* The divides relation *} 

82 

83 
lemma le_imp_power_dvd: 

84 
assumes "m \<le> n" shows "a ^ m dvd a ^ n" 

85 
proof 

86 
have "a ^ n = a ^ (m + (n  m))" 

87 
using `m \<le> n` by simp 

88 
also have "\<dots> = a ^ m * a ^ (n  m)" 

89 
by (rule power_add) 

90 
finally show "a ^ n = a ^ m * a ^ (n  m)" . 

91 
qed 

92 

93 
lemma power_le_dvd: 

94 
"a ^ n dvd b \<Longrightarrow> m \<le> n \<Longrightarrow> a ^ m dvd b" 

95 
by (rule dvd_trans [OF le_imp_power_dvd]) 

96 

97 
lemma dvd_power_same: 

98 
"x dvd y \<Longrightarrow> x ^ n dvd y ^ n" 

99 
by (induct n) (auto simp add: mult_dvd_mono) 

100 

101 
lemma dvd_power_le: 

102 
"x dvd y \<Longrightarrow> m \<ge> n \<Longrightarrow> x ^ n dvd y ^ m" 

103 
by (rule power_le_dvd [OF dvd_power_same]) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

104 

30996  105 
lemma dvd_power [simp]: 
106 
assumes "n > (0::nat) \<or> x = 1" 

107 
shows "x dvd (x ^ n)" 

108 
using assms proof 

109 
assume "0 < n" 

110 
then have "x ^ n = x ^ Suc (n  1)" by simp 

111 
then show "x dvd (x ^ n)" by simp 

112 
next 

113 
assume "x = 1" 

114 
then show "x dvd (x ^ n)" by simp 

115 
qed 

116 

117 
end 

118 

119 
context ring_1 

120 
begin 

121 

122 
lemma power_minus: 

123 
"( a) ^ n = ( 1) ^ n * a ^ n" 

124 
proof (induct n) 

125 
case 0 show ?case by simp 

126 
next 

127 
case (Suc n) then show ?case 

128 
by (simp del: power_Suc add: power_Suc2 mult_assoc) 

129 
qed 

130 

131 
end 

132 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33364
diff
changeset

133 
context linordered_semidom 
30996  134 
begin 
135 

136 
lemma zero_less_power [simp]: 

137 
"0 < a \<Longrightarrow> 0 < a ^ n" 

138 
by (induct n) (simp_all add: mult_pos_pos) 

139 

140 
lemma zero_le_power [simp]: 

141 
"0 \<le> a \<Longrightarrow> 0 \<le> a ^ n" 

142 
by (induct n) (simp_all add: mult_nonneg_nonneg) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

143 

25874  144 
lemma one_le_power[simp]: 
30996  145 
"1 \<le> a \<Longrightarrow> 1 \<le> a ^ n" 
146 
apply (induct n) 

147 
apply simp_all 

148 
apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) 

149 
apply (simp_all add: order_trans [OF zero_le_one]) 

150 
done 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

151 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

152 
lemma power_gt1_lemma: 
30996  153 
assumes gt1: "1 < a" 
154 
shows "1 < a * a ^ n" 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

155 
proof  
30996  156 
from gt1 have "0 \<le> a" 
157 
by (fact order_trans [OF zero_le_one less_imp_le]) 

158 
have "1 * 1 < a * 1" using gt1 by simp 

159 
also have "\<dots> \<le> a * a ^ n" using gt1 

160 
by (simp only: mult_mono `0 \<le> a` one_le_power order_less_imp_le 

14577  161 
zero_le_one order_refl) 
162 
finally show ?thesis by simp 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

163 
qed 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

164 

30996  165 
lemma power_gt1: 
166 
"1 < a \<Longrightarrow> 1 < a ^ Suc n" 

167 
by (simp add: power_gt1_lemma) 

24376  168 

30996  169 
lemma one_less_power [simp]: 
170 
"1 < a \<Longrightarrow> 0 < n \<Longrightarrow> 1 < a ^ n" 

171 
by (cases n) (simp_all add: power_gt1_lemma) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

172 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

173 
lemma power_le_imp_le_exp: 
30996  174 
assumes gt1: "1 < a" 
175 
shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n" 

176 
proof (induct m arbitrary: n) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

177 
case 0 
14577  178 
show ?case by simp 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

179 
next 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

180 
case (Suc m) 
14577  181 
show ?case 
182 
proof (cases n) 

183 
case 0 

30996  184 
with Suc.prems Suc.hyps have "a * a ^ m \<le> 1" by simp 
14577  185 
with gt1 show ?thesis 
186 
by (force simp only: power_gt1_lemma 

30996  187 
not_less [symmetric]) 
14577  188 
next 
189 
case (Suc n) 

30996  190 
with Suc.prems Suc.hyps show ?thesis 
14577  191 
by (force dest: mult_left_le_imp_le 
30996  192 
simp add: less_trans [OF zero_less_one gt1]) 
14577  193 
qed 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

194 
qed 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

195 

14577  196 
text{*Surely we can strengthen this? It holds for @{text "0<a<1"} too.*} 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

197 
lemma power_inject_exp [simp]: 
30996  198 
"1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n" 
14577  199 
by (force simp add: order_antisym power_le_imp_le_exp) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

200 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

201 
text{*Can relax the first premise to @{term "0<a"} in the case of the 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

202 
natural numbers.*} 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

203 
lemma power_less_imp_less_exp: 
30996  204 
"1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n" 
205 
by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] 

206 
power_le_imp_le_exp) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

207 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

208 
lemma power_mono: 
30996  209 
"a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n" 
210 
by (induct n) 

211 
(auto intro: mult_mono order_trans [of 0 a b]) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

212 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

213 
lemma power_strict_mono [rule_format]: 
30996  214 
"a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n" 
215 
by (induct n) 

216 
(auto simp add: mult_strict_mono le_less_trans [of 0 a b]) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

217 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

218 
text{*Lemma for @{text power_strict_decreasing}*} 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

219 
lemma power_Suc_less: 
30996  220 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n" 
221 
by (induct n) 

222 
(auto simp add: mult_strict_left_mono) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

223 

30996  224 
lemma power_strict_decreasing [rule_format]: 
225 
"n < N \<Longrightarrow> 0 < a \<Longrightarrow> a < 1 \<longrightarrow> a ^ N < a ^ n" 

226 
proof (induct N) 

227 
case 0 then show ?case by simp 

228 
next 

229 
case (Suc N) then show ?case 

230 
apply (auto simp add: power_Suc_less less_Suc_eq) 

231 
apply (subgoal_tac "a * a^N < 1 * a^n") 

232 
apply simp 

233 
apply (rule mult_strict_mono) apply auto 

234 
done 

235 
qed 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

236 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

237 
text{*Proof resembles that of @{text power_strict_decreasing}*} 
30996  238 
lemma power_decreasing [rule_format]: 
239 
"n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<longrightarrow> a ^ N \<le> a ^ n" 

240 
proof (induct N) 

241 
case 0 then show ?case by simp 

242 
next 

243 
case (Suc N) then show ?case 

244 
apply (auto simp add: le_Suc_eq) 

245 
apply (subgoal_tac "a * a^N \<le> 1 * a^n", simp) 

246 
apply (rule mult_mono) apply auto 

247 
done 

248 
qed 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

249 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

250 
lemma power_Suc_less_one: 
30996  251 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1" 
252 
using power_strict_decreasing [of 0 "Suc n" a] by simp 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

253 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

254 
text{*Proof again resembles that of @{text power_strict_decreasing}*} 
30996  255 
lemma power_increasing [rule_format]: 
256 
"n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N" 

257 
proof (induct N) 

258 
case 0 then show ?case by simp 

259 
next 

260 
case (Suc N) then show ?case 

261 
apply (auto simp add: le_Suc_eq) 

262 
apply (subgoal_tac "1 * a^n \<le> a * a^N", simp) 

263 
apply (rule mult_mono) apply (auto simp add: order_trans [OF zero_le_one]) 

264 
done 

265 
qed 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

266 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

267 
text{*Lemma for @{text power_strict_increasing}*} 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

268 
lemma power_less_power_Suc: 
30996  269 
"1 < a \<Longrightarrow> a ^ n < a * a ^ n" 
270 
by (induct n) (auto simp add: mult_strict_left_mono less_trans [OF zero_less_one]) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

271 

30996  272 
lemma power_strict_increasing [rule_format]: 
273 
"n < N \<Longrightarrow> 1 < a \<longrightarrow> a ^ n < a ^ N" 

274 
proof (induct N) 

275 
case 0 then show ?case by simp 

276 
next 

277 
case (Suc N) then show ?case 

278 
apply (auto simp add: power_less_power_Suc less_Suc_eq) 

279 
apply (subgoal_tac "1 * a^n < a * a^N", simp) 

280 
apply (rule mult_strict_mono) apply (auto simp add: less_trans [OF zero_less_one] less_imp_le) 

281 
done 

282 
qed 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

283 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset

284 
lemma power_increasing_iff [simp]: 
30996  285 
"1 < b \<Longrightarrow> b ^ x \<le> b ^ y \<longleftrightarrow> x \<le> y" 
286 
by (blast intro: power_le_imp_le_exp power_increasing less_imp_le) 

15066  287 

288 
lemma power_strict_increasing_iff [simp]: 

30996  289 
"1 < b \<Longrightarrow> b ^ x < b ^ y \<longleftrightarrow> x < y" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset

290 
by (blast intro: power_less_imp_less_exp power_strict_increasing) 
15066  291 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

292 
lemma power_le_imp_le_base: 
30996  293 
assumes le: "a ^ Suc n \<le> b ^ Suc n" 
294 
and ynonneg: "0 \<le> b" 

295 
shows "a \<le> b" 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset

296 
proof (rule ccontr) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset

297 
assume "~ a \<le> b" 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset

298 
then have "b < a" by (simp only: linorder_not_le) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset

299 
then have "b ^ Suc n < a ^ Suc n" 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset

300 
by (simp only: prems power_strict_mono) 
30996  301 
from le and this show False 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset

302 
by (simp add: linorder_not_less [symmetric]) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset

303 
qed 
14577  304 

22853  305 
lemma power_less_imp_less_base: 
306 
assumes less: "a ^ n < b ^ n" 

307 
assumes nonneg: "0 \<le> b" 

308 
shows "a < b" 

309 
proof (rule contrapos_pp [OF less]) 

310 
assume "~ a < b" 

311 
hence "b \<le> a" by (simp only: linorder_not_less) 

312 
hence "b ^ n \<le> a ^ n" using nonneg by (rule power_mono) 

30996  313 
thus "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less) 
22853  314 
qed 
315 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

316 
lemma power_inject_base: 
30996  317 
"a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b" 
318 
by (blast intro: power_le_imp_le_base antisym eq_refl sym) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

319 

22955  320 
lemma power_eq_imp_eq_base: 
30996  321 
"a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b" 
322 
by (cases n) (simp_all del: power_Suc, rule power_inject_base) 

22955  323 

30996  324 
end 
325 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33364
diff
changeset

326 
context linordered_idom 
30996  327 
begin 
29978
33df3c4eb629
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
huffman
parents:
29608
diff
changeset

328 

30996  329 
lemma power_abs: 
330 
"abs (a ^ n) = abs a ^ n" 

331 
by (induct n) (auto simp add: abs_mult) 

332 

333 
lemma abs_power_minus [simp]: 

334 
"abs ((a) ^ n) = abs (a ^ n)" 

335 
by (simp add: abs_minus_cancel power_abs) 

336 

337 
lemma zero_less_power_abs_iff [simp, noatp]: 

338 
"0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0" 

339 
proof (induct n) 

340 
case 0 show ?case by simp 

341 
next 

342 
case (Suc n) show ?case by (auto simp add: Suc zero_less_mult_iff) 

29978
33df3c4eb629
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
huffman
parents:
29608
diff
changeset

343 
qed 
33df3c4eb629
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
huffman
parents:
29608
diff
changeset

344 

30996  345 
lemma zero_le_power_abs [simp]: 
346 
"0 \<le> abs a ^ n" 

347 
by (rule zero_le_power [OF abs_ge_zero]) 

348 

349 
end 

350 

351 
context ring_1_no_zero_divisors 

352 
begin 

353 

354 
lemma field_power_not_zero: 

355 
"a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0" 

356 
by (induct n) auto 

357 

358 
end 

359 

360 
context division_ring 

361 
begin 

29978
33df3c4eb629
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
huffman
parents:
29608
diff
changeset

362 

30997  363 
text {* FIXME reorient or rename to @{text nonzero_inverse_power} *} 
30996  364 
lemma nonzero_power_inverse: 
365 
"a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n" 

366 
by (induct n) 

367 
(simp_all add: nonzero_inverse_mult_distrib power_commutes field_power_not_zero) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

368 

30996  369 
end 
370 

371 
context field 

372 
begin 

373 

374 
lemma nonzero_power_divide: 

375 
"b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n" 

376 
by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse) 

377 

378 
end 

379 

380 
lemma power_0_Suc [simp]: 

381 
"(0::'a::{power, semiring_0}) ^ Suc n = 0" 

382 
by simp 

30313  383 

30996  384 
text{*It looks plausible as a simprule, but its effect can be strange.*} 
385 
lemma power_0_left: 

386 
"0 ^ n = (if n = 0 then 1 else (0::'a::{power, semiring_0}))" 

387 
by (induct n) simp_all 

388 

389 
lemma power_eq_0_iff [simp]: 

390 
"a ^ n = 0 \<longleftrightarrow> 

391 
a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,power}) \<and> n \<noteq> 0" 

392 
by (induct n) 

393 
(auto simp add: no_zero_divisors elim: contrapos_pp) 

394 

395 
lemma power_diff: 

396 
fixes a :: "'a::field" 

397 
assumes nz: "a \<noteq> 0" 

398 
shows "n \<le> m \<Longrightarrow> a ^ (m  n) = a ^ m / a ^ n" 

399 
by (induct m n rule: diff_induct) (simp_all add: nz) 

30313  400 

30996  401 
text{*Perhaps these should be simprules.*} 
402 
lemma power_inverse: 

403 
fixes a :: "'a::{division_ring,division_by_zero,power}" 

404 
shows "inverse (a ^ n) = (inverse a) ^ n" 

405 
apply (cases "a = 0") 

406 
apply (simp add: power_0_left) 

407 
apply (simp add: nonzero_power_inverse) 

408 
done (* TODO: reorient or rename to inverse_power *) 

409 

410 
lemma power_one_over: 

411 
"1 / (a::'a::{field,division_by_zero, power}) ^ n = (1 / a) ^ n" 

412 
by (simp add: divide_inverse) (rule power_inverse) 

413 

414 
lemma power_divide: 

415 
"(a / b) ^ n = (a::'a::{field,division_by_zero}) ^ n / b ^ n" 

416 
apply (cases "b = 0") 

417 
apply (simp add: power_0_left) 

418 
apply (rule nonzero_power_divide) 

419 
apply assumption 

30313  420 
done 
421 

422 

30960  423 
subsection {* Exponentiation for the Natural Numbers *} 
14577  424 

30996  425 
lemma nat_one_le_power [simp]: 
426 
"Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n" 

427 
by (rule one_le_power [of i n, unfolded One_nat_def]) 

23305  428 

30996  429 
lemma nat_zero_less_power_iff [simp]: 
430 
"x ^ n > 0 \<longleftrightarrow> x > (0::nat) \<or> n = 0" 

431 
by (induct n) auto 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

432 

30056  433 
lemma nat_power_eq_Suc_0_iff [simp]: 
30996  434 
"x ^ m = Suc 0 \<longleftrightarrow> m = 0 \<or> x = Suc 0" 
435 
by (induct m) auto 

30056  436 

30996  437 
lemma power_Suc_0 [simp]: 
438 
"Suc 0 ^ n = Suc 0" 

439 
by simp 

30056  440 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

441 
text{*Valid for the naturals, but what if @{text"0<i<1"}? 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

442 
Premises cannot be weakened: consider the case where @{term "i=0"}, 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

443 
@{term "m=1"} and @{term "n=0"}.*} 
21413  444 
lemma nat_power_less_imp_less: 
445 
assumes nonneg: "0 < (i\<Colon>nat)" 

30996  446 
assumes less: "i ^ m < i ^ n" 
21413  447 
shows "m < n" 
448 
proof (cases "i = 1") 

449 
case True with less power_one [where 'a = nat] show ?thesis by simp 

450 
next 

451 
case False with nonneg have "1 < i" by auto 

452 
from power_strict_increasing_iff [OF this] less show ?thesis .. 

453 
qed 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

454 

33274
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
31998
diff
changeset

455 
lemma power_dvd_imp_le: 
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
31998
diff
changeset

456 
"i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n" 
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
31998
diff
changeset

457 
apply (rule power_le_imp_le_exp, assumption) 
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
31998
diff
changeset

458 
apply (erule dvd_imp_le, simp) 
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
31998
diff
changeset

459 
done 
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
31998
diff
changeset

460 

31155
92d8ff6af82c
monomorphic code generation for power operations
haftmann
parents:
31021
diff
changeset

461 

92d8ff6af82c
monomorphic code generation for power operations
haftmann
parents:
31021
diff
changeset

462 
subsection {* Code generator tweak *} 
92d8ff6af82c
monomorphic code generation for power operations
haftmann
parents:
31021
diff
changeset

463 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31155
diff
changeset

464 
lemma power_power_power [code, code_unfold, code_inline del]: 
31155
92d8ff6af82c
monomorphic code generation for power operations
haftmann
parents:
31021
diff
changeset

465 
"power = power.power (1::'a::{power}) (op *)" 
92d8ff6af82c
monomorphic code generation for power operations
haftmann
parents:
31021
diff
changeset

466 
unfolding power_def power.power_def .. 
92d8ff6af82c
monomorphic code generation for power operations
haftmann
parents:
31021
diff
changeset

467 

92d8ff6af82c
monomorphic code generation for power operations
haftmann
parents:
31021
diff
changeset

468 
declare power.power.simps [code] 
92d8ff6af82c
monomorphic code generation for power operations
haftmann
parents:
31021
diff
changeset

469 

33364  470 
code_modulename SML 
471 
Power Arith 

472 

473 
code_modulename OCaml 

474 
Power Arith 

475 

476 
code_modulename Haskell 

477 
Power Arith 

478 

3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

479 
end 