author  huffman 
Thu, 29 Mar 2012 11:47:30 +0200  
changeset 47191  ebd8c46d156b 
parent 45231  d85a2fdc586c 
child 47192  0c0501cb6da6 
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 
47191  9 
imports Num 
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 

39438
c5ece2a7a86e
Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example  amending lapse introduced in 9de4d64eee3b (April 2004);
wenzelm
parents:
36409
diff
changeset

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 

47191  69 
context semiring_numeral 
70 
begin 

71 

72 
lemma numeral_sqr: "numeral (Num.sqr k) = numeral k * numeral k" 

73 
by (simp only: sqr_conv_mult numeral_mult) 

74 

75 
lemma numeral_pow: "numeral (Num.pow k l) = numeral k ^ numeral l" 

76 
by (induct l, simp_all only: numeral_class.numeral.simps pow.simps 

77 
numeral_sqr numeral_mult power_add power_one_right) 

78 

79 
lemma power_numeral [simp]: "numeral k ^ numeral l = numeral (Num.pow k l)" 

80 
by (rule numeral_pow [symmetric]) 

81 

82 
end 

83 

30996  84 
context semiring_1 
85 
begin 

86 

87 
lemma of_nat_power: 

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

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

90 

47191  91 
lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0" 
92 
by (cases "numeral k :: nat", simp_all) 

93 

30996  94 
end 
95 

96 
context comm_semiring_1 

97 
begin 

98 

99 
text {* The divides relation *} 

100 

101 
lemma le_imp_power_dvd: 

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

103 
proof 

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

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

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

107 
by (rule power_add) 

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

109 
qed 

110 

111 
lemma power_le_dvd: 

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

113 
by (rule dvd_trans [OF le_imp_power_dvd]) 

114 

115 
lemma dvd_power_same: 

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

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

118 

119 
lemma dvd_power_le: 

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

121 
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

122 

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

125 
shows "x dvd (x ^ n)" 

126 
using assms proof 

127 
assume "0 < n" 

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

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

130 
next 

131 
assume "x = 1" 

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

133 
qed 

134 

135 
end 

136 

137 
context ring_1 

138 
begin 

139 

140 
lemma power_minus: 

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

142 
proof (induct n) 

143 
case 0 show ?case by simp 

144 
next 

145 
case (Suc n) then show ?case 

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

147 
qed 

148 

47191  149 
lemma power_minus_Bit0: 
150 
"( x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)" 

151 
by (induct k, simp_all only: numeral_class.numeral.simps power_add 

152 
power_one_right mult_minus_left mult_minus_right minus_minus) 

153 

154 
lemma power_minus_Bit1: 

155 
"( x) ^ numeral (Num.Bit1 k) =  (x ^ numeral (Num.Bit1 k))" 

156 
by (simp only: nat_number(4) power_Suc power_minus_Bit0 mult_minus_left) 

157 

158 
lemma power_neg_numeral_Bit0 [simp]: 

159 
"neg_numeral k ^ numeral (Num.Bit0 l) = numeral (Num.pow k (Num.Bit0 l))" 

160 
by (simp only: neg_numeral_def power_minus_Bit0 power_numeral) 

161 

162 
lemma power_neg_numeral_Bit1 [simp]: 

163 
"neg_numeral k ^ numeral (Num.Bit1 l) = neg_numeral (Num.pow k (Num.Bit1 l))" 

164 
by (simp only: neg_numeral_def power_minus_Bit1 power_numeral pow.simps) 

165 

30996  166 
end 
167 

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

168 
context linordered_semidom 
30996  169 
begin 
170 

171 
lemma zero_less_power [simp]: 

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

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

174 

175 
lemma zero_le_power [simp]: 

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

177 
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

178 

25874  179 
lemma one_le_power[simp]: 
30996  180 
"1 \<le> a \<Longrightarrow> 1 \<le> a ^ n" 
181 
apply (induct n) 

182 
apply simp_all 

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

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

185 
done 

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

186 

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

187 
lemma power_gt1_lemma: 
30996  188 
assumes gt1: "1 < a" 
189 
shows "1 < a * a ^ n" 

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

190 
proof  
30996  191 
from gt1 have "0 \<le> a" 
192 
by (fact order_trans [OF zero_le_one less_imp_le]) 

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

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

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

14577  196 
zero_le_one order_refl) 
197 
finally show ?thesis by simp 

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

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

199 

30996  200 
lemma power_gt1: 
201 
"1 < a \<Longrightarrow> 1 < a ^ Suc n" 

202 
by (simp add: power_gt1_lemma) 

24376  203 

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

206 
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

207 

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

208 
lemma power_le_imp_le_exp: 
30996  209 
assumes gt1: "1 < a" 
210 
shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n" 

211 
proof (induct m arbitrary: n) 

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

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

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

215 
case (Suc m) 
14577  216 
show ?case 
217 
proof (cases n) 

218 
case 0 

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

30996  222 
not_less [symmetric]) 
14577  223 
next 
224 
case (Suc n) 

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

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

230 

14577  231 
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

232 
lemma power_inject_exp [simp]: 
30996  233 
"1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n" 
14577  234 
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

235 

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

236 
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

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

238 
lemma power_less_imp_less_exp: 
30996  239 
"1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n" 
240 
by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] 

241 
power_le_imp_le_exp) 

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

242 

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

243 
lemma power_mono: 
30996  244 
"a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n" 
245 
by (induct n) 

246 
(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

247 

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

248 
lemma power_strict_mono [rule_format]: 
30996  249 
"a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n" 
250 
by (induct n) 

251 
(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

252 

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

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

254 
lemma power_Suc_less: 
30996  255 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n" 
256 
by (induct n) 

257 
(auto simp add: mult_strict_left_mono) 

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

258 

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

261 
proof (induct N) 

262 
case 0 then show ?case by simp 

263 
next 

264 
case (Suc N) then show ?case 

265 
apply (auto simp add: power_Suc_less less_Suc_eq) 

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

267 
apply simp 

268 
apply (rule mult_strict_mono) apply auto 

269 
done 

270 
qed 

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

271 

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

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

275 
proof (induct N) 

276 
case 0 then show ?case by simp 

277 
next 

278 
case (Suc N) then show ?case 

279 
apply (auto simp add: le_Suc_eq) 

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

281 
apply (rule mult_mono) apply auto 

282 
done 

283 
qed 

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

284 

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

285 
lemma power_Suc_less_one: 
30996  286 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1" 
287 
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

288 

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

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

292 
proof (induct N) 

293 
case 0 then show ?case by simp 

294 
next 

295 
case (Suc N) then show ?case 

296 
apply (auto simp add: le_Suc_eq) 

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

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

299 
done 

300 
qed 

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

301 

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

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

303 
lemma power_less_power_Suc: 
30996  304 
"1 < a \<Longrightarrow> a ^ n < a * a ^ n" 
305 
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

306 

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

309 
proof (induct N) 

310 
case 0 then show ?case by simp 

311 
next 

312 
case (Suc N) then show ?case 

313 
apply (auto simp add: power_less_power_Suc less_Suc_eq) 

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

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

316 
done 

317 
qed 

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

318 

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

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

15066  322 

323 
lemma power_strict_increasing_iff [simp]: 

30996  324 
"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

325 
by (blast intro: power_less_imp_less_exp power_strict_increasing) 
15066  326 

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

327 
lemma power_le_imp_le_base: 
30996  328 
assumes le: "a ^ Suc n \<le> b ^ Suc n" 
329 
and ynonneg: "0 \<le> b" 

330 
shows "a \<le> b" 

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

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

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

333 
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

334 
then have "b ^ Suc n < a ^ Suc n" 
41550  335 
by (simp only: assms power_strict_mono) 
30996  336 
from le and this show False 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset

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

338 
qed 
14577  339 

22853  340 
lemma power_less_imp_less_base: 
341 
assumes less: "a ^ n < b ^ n" 

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

343 
shows "a < b" 

344 
proof (rule contrapos_pp [OF less]) 

345 
assume "~ a < b" 

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

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

30996  348 
thus "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less) 
22853  349 
qed 
350 

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

351 
lemma power_inject_base: 
30996  352 
"a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b" 
353 
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

354 

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

22955  358 

30996  359 
end 
360 

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

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

363 

30996  364 
lemma power_abs: 
365 
"abs (a ^ n) = abs a ^ n" 

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

367 

368 
lemma abs_power_minus [simp]: 

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

35216  370 
by (simp add: power_abs) 
30996  371 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35216
diff
changeset

372 
lemma zero_less_power_abs_iff [simp, no_atp]: 
30996  373 
"0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0" 
374 
proof (induct n) 

375 
case 0 show ?case by simp 

376 
next 

377 
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

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

379 

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

382 
by (rule zero_le_power [OF abs_ge_zero]) 

383 

384 
end 

385 

386 
context ring_1_no_zero_divisors 

387 
begin 

388 

389 
lemma field_power_not_zero: 

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

391 
by (induct n) auto 

392 

393 
end 

394 

395 
context division_ring 

396 
begin 

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

397 

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

401 
by (induct n) 

402 
(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

403 

30996  404 
end 
405 

406 
context field 

407 
begin 

408 

409 
lemma nonzero_power_divide: 

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

411 
by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse) 

412 

413 
end 

414 

415 
lemma power_0_Suc [simp]: 

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

417 
by simp 

30313  418 

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

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

422 
by (induct n) simp_all 

423 

424 
lemma power_eq_0_iff [simp]: 

425 
"a ^ n = 0 \<longleftrightarrow> 

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

427 
by (induct n) 

428 
(auto simp add: no_zero_divisors elim: contrapos_pp) 

429 

36409  430 
lemma (in field) power_diff: 
30996  431 
assumes nz: "a \<noteq> 0" 
432 
shows "n \<le> m \<Longrightarrow> a ^ (m  n) = a ^ m / a ^ n" 

36409  433 
by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero) 
30313  434 

30996  435 
text{*Perhaps these should be simprules.*} 
436 
lemma power_inverse: 

36409  437 
fixes a :: "'a::division_ring_inverse_zero" 
438 
shows "inverse (a ^ n) = inverse a ^ n" 

30996  439 
apply (cases "a = 0") 
440 
apply (simp add: power_0_left) 

441 
apply (simp add: nonzero_power_inverse) 

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

443 

444 
lemma power_one_over: 

36409  445 
"1 / (a::'a::{field_inverse_zero, power}) ^ n = (1 / a) ^ n" 
30996  446 
by (simp add: divide_inverse) (rule power_inverse) 
447 

448 
lemma power_divide: 

36409  449 
"(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n" 
30996  450 
apply (cases "b = 0") 
451 
apply (simp add: power_0_left) 

452 
apply (rule nonzero_power_divide) 

453 
apply assumption 

30313  454 
done 
455 

456 

30960  457 
subsection {* Exponentiation for the Natural Numbers *} 
14577  458 

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

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

23305  462 

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

465 
by (induct n) auto 

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

466 

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

30056  470 

30996  471 
lemma power_Suc_0 [simp]: 
472 
"Suc 0 ^ n = Suc 0" 

473 
by simp 

30056  474 

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

475 
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

476 
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

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

30996  480 
assumes less: "i ^ m < i ^ n" 
21413  481 
shows "m < n" 
482 
proof (cases "i = 1") 

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

484 
next 

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

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

487 
qed 

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

488 

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

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

490 
"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

491 
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

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

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

494 

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

495 

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

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

497 

45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
41550
diff
changeset

498 
lemma power_power_power [code]: 
31155
92d8ff6af82c
monomorphic code generation for power operations
haftmann
parents:
31021
diff
changeset

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

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

501 

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

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

503 

33364  504 
code_modulename SML 
505 
Power Arith 

506 

507 
code_modulename OCaml 

508 
Power Arith 

509 

510 
code_modulename Haskell 

511 
Power Arith 

512 

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

513 
end 