author  haftmann 
Sun, 24 Feb 2013 20:29:13 +0100  
changeset 51263  31e786e0e6a7 
parent 49824  c26665a197dc 
child 52435  6646bb548c6b 
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 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

27 
text {* Special syntax for squares. *} 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

28 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

29 
abbreviation (xsymbols) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

30 
power2 :: "'a \<Rightarrow> 'a" ("(_\<twosuperior>)" [1000] 999) where 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

31 
"x\<twosuperior> \<equiv> x ^ 2" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

32 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

33 
notation (latex output) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

34 
power2 ("(_\<twosuperior>)" [1000] 999) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

35 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

36 
notation (HTML output) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

37 
power2 ("(_\<twosuperior>)" [1000] 999) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

38 

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

40 

30996  41 
context monoid_mult 
42 
begin 

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

43 

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

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

45 

30996  46 
lemma power_one [simp]: 
47 
"1 ^ n = 1" 

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

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

49 

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

53 

30996  54 
lemma power_commutes: 
55 
"a ^ n * a = a * a ^ 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: mult_assoc) 
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
17149
diff
changeset

57 

30996  58 
lemma power_Suc2: 
59 
"a ^ Suc n = a ^ n * a" 

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

60 
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

61 

30996  62 
lemma power_add: 
63 
"a ^ (m + n) = a ^ m * a ^ n" 

64 
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

65 

30996  66 
lemma power_mult: 
67 
"a ^ (m * n) = (a ^ m) ^ n" 

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

68 
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

69 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

70 
lemma power2_eq_square: "a\<twosuperior> = a * a" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

71 
by (simp add: numeral_2_eq_2) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

72 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

73 
lemma power3_eq_cube: "a ^ 3 = a * a * a" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

74 
by (simp add: numeral_3_eq_3 mult_assoc) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

75 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

76 
lemma power_even_eq: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

77 
"a ^ (2*n) = (a ^ n) ^ 2" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

78 
by (subst mult_commute) (simp add: power_mult) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

79 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

80 
lemma power_odd_eq: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

81 
"a ^ Suc (2*n) = a * (a ^ n) ^ 2" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

82 
by (simp add: power_even_eq) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

83 

47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

84 
lemma power_numeral_even: 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

85 
"z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)" 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

86 
unfolding numeral_Bit0 power_add Let_def .. 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

87 

30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

88 
lemma power_numeral_odd: 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

89 
"z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)" 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

90 
unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

91 
unfolding power_Suc power_add Let_def mult_assoc .. 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

92 

49824  93 
lemma funpow_times_power: 
94 
"(times x ^^ f x) = times (x ^ f x)" 

95 
proof (induct "f x" arbitrary: f) 

96 
case 0 then show ?case by (simp add: fun_eq_iff) 

97 
next 

98 
case (Suc n) 

99 
def g \<equiv> "\<lambda>x. f x  1" 

100 
with Suc have "n = g x" by simp 

101 
with Suc have "times x ^^ g x = times (x ^ g x)" by simp 

102 
moreover from Suc g_def have "f x = g x + 1" by simp 

103 
ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult_assoc) 

104 
qed 

105 

30996  106 
end 
107 

108 
context comm_monoid_mult 

109 
begin 

110 

111 
lemma power_mult_distrib: 

112 
"(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

113 
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

114 

30996  115 
end 
116 

47191  117 
context semiring_numeral 
118 
begin 

119 

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

121 
by (simp only: sqr_conv_mult numeral_mult) 

122 

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

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

125 
numeral_sqr numeral_mult power_add power_one_right) 

126 

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

128 
by (rule numeral_pow [symmetric]) 

129 

130 
end 

131 

30996  132 
context semiring_1 
133 
begin 

134 

135 
lemma of_nat_power: 

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

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

138 

47191  139 
lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0" 
47209
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47192
diff
changeset

140 
by (simp add: numeral_eq_Suc) 
47191  141 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

142 
lemma zero_power2: "0\<twosuperior> = 0" (* delete? *) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

143 
by (rule power_zero_numeral) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

144 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

145 
lemma one_power2: "1\<twosuperior> = 1" (* delete? *) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

146 
by (rule power_one) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

147 

30996  148 
end 
149 

150 
context comm_semiring_1 

151 
begin 

152 

153 
text {* The divides relation *} 

154 

155 
lemma le_imp_power_dvd: 

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

157 
proof 

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

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

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

161 
by (rule power_add) 

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

163 
qed 

164 

165 
lemma power_le_dvd: 

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

167 
by (rule dvd_trans [OF le_imp_power_dvd]) 

168 

169 
lemma dvd_power_same: 

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

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

172 

173 
lemma dvd_power_le: 

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

175 
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

176 

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

179 
shows "x dvd (x ^ n)" 

180 
using assms proof 

181 
assume "0 < n" 

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

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

184 
next 

185 
assume "x = 1" 

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

187 
qed 

188 

189 
end 

190 

191 
context ring_1 

192 
begin 

193 

194 
lemma power_minus: 

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

196 
proof (induct n) 

197 
case 0 show ?case by simp 

198 
next 

199 
case (Suc n) then show ?case 

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

201 
qed 

202 

47191  203 
lemma power_minus_Bit0: 
204 
"( x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)" 

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

206 
power_one_right mult_minus_left mult_minus_right minus_minus) 

207 

208 
lemma power_minus_Bit1: 

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

47220
52426c62b5d0
replace lemmas eval_nat_numeral with a simpler reformulation
huffman
parents:
47209
diff
changeset

210 
by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left) 
47191  211 

212 
lemma power_neg_numeral_Bit0 [simp]: 

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

214 
by (simp only: neg_numeral_def power_minus_Bit0 power_numeral) 

215 

216 
lemma power_neg_numeral_Bit1 [simp]: 

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

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

219 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

220 
lemma power2_minus [simp]: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

221 
"( a)\<twosuperior> = a\<twosuperior>" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

222 
by (rule power_minus_Bit0) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

223 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

224 
lemma power_minus1_even [simp]: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

225 
"1 ^ (2*n) = 1" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

226 
proof (induct n) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

227 
case 0 show ?case by simp 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

228 
next 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

229 
case (Suc n) then show ?case by (simp add: power_add power2_eq_square) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

230 
qed 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

231 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

232 
lemma power_minus1_odd: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

233 
"1 ^ Suc (2*n) = 1" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

234 
by simp 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

235 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

236 
lemma power_minus_even [simp]: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

237 
"(a) ^ (2*n) = a ^ (2*n)" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

238 
by (simp add: power_minus [of a]) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

239 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

240 
end 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

241 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

242 
context ring_1_no_zero_divisors 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

243 
begin 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

244 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

245 
lemma field_power_not_zero: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

246 
"a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

247 
by (induct n) auto 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

248 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

249 
lemma zero_eq_power2 [simp]: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

250 
"a\<twosuperior> = 0 \<longleftrightarrow> a = 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

251 
unfolding power2_eq_square by simp 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

252 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

253 
lemma power2_eq_1_iff: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

254 
"a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> a =  1" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

255 
unfolding power2_eq_square by (rule square_eq_1_iff) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

256 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

257 
end 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

258 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

259 
context idom 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

260 
begin 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

261 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

262 
lemma power2_eq_iff: "x\<twosuperior> = y\<twosuperior> \<longleftrightarrow> x = y \<or> x =  y" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

263 
unfolding power2_eq_square by (rule square_eq_iff) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

264 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

265 
end 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

266 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

267 
context division_ring 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

268 
begin 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

269 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

270 
text {* FIXME reorient or rename to @{text nonzero_inverse_power} *} 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

271 
lemma nonzero_power_inverse: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

272 
"a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

273 
by (induct n) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

274 
(simp_all add: nonzero_inverse_mult_distrib power_commutes field_power_not_zero) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

275 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

276 
end 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

277 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

278 
context field 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

279 
begin 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

280 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

281 
lemma nonzero_power_divide: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

282 
"b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

283 
by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

284 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

285 
end 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

286 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

287 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

288 
subsection {* Exponentiation on ordered types *} 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

289 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

290 
context linordered_ring (* TODO: move *) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

291 
begin 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

292 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

293 
lemma sum_squares_ge_zero: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

294 
"0 \<le> x * x + y * y" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

295 
by (intro add_nonneg_nonneg zero_le_square) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

296 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

297 
lemma not_sum_squares_lt_zero: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

298 
"\<not> x * x + y * y < 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

299 
by (simp add: not_less sum_squares_ge_zero) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

300 

30996  301 
end 
302 

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

303 
context linordered_semidom 
30996  304 
begin 
305 

306 
lemma zero_less_power [simp]: 

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

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

309 

310 
lemma zero_le_power [simp]: 

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

312 
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

313 

47241  314 
lemma power_mono: 
315 
"a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n" 

316 
by (induct n) (auto intro: mult_mono order_trans [of 0 a b]) 

317 

318 
lemma one_le_power [simp]: "1 \<le> a \<Longrightarrow> 1 \<le> a ^ n" 

319 
using power_mono [of 1 a n] by simp 

320 

321 
lemma power_le_one: "\<lbrakk>0 \<le> a; a \<le> 1\<rbrakk> \<Longrightarrow> a ^ n \<le> 1" 

322 
using power_mono [of a 1 n] by simp 

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

323 

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

324 
lemma power_gt1_lemma: 
30996  325 
assumes gt1: "1 < a" 
326 
shows "1 < a * a ^ n" 

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

327 
proof  
30996  328 
from gt1 have "0 \<le> a" 
329 
by (fact order_trans [OF zero_le_one less_imp_le]) 

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

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

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

14577  333 
zero_le_one order_refl) 
334 
finally show ?thesis by simp 

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

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

336 

30996  337 
lemma power_gt1: 
338 
"1 < a \<Longrightarrow> 1 < a ^ Suc n" 

339 
by (simp add: power_gt1_lemma) 

24376  340 

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

343 
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

344 

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

345 
lemma power_le_imp_le_exp: 
30996  346 
assumes gt1: "1 < a" 
347 
shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n" 

348 
proof (induct m arbitrary: n) 

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

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

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

352 
case (Suc m) 
14577  353 
show ?case 
354 
proof (cases n) 

355 
case 0 

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

30996  359 
not_less [symmetric]) 
14577  360 
next 
361 
case (Suc n) 

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

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

367 

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

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

372 

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

373 
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

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

375 
lemma power_less_imp_less_exp: 
30996  376 
"1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n" 
377 
by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] 

378 
power_le_imp_le_exp) 

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

379 

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

380 
lemma power_strict_mono [rule_format]: 
30996  381 
"a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n" 
382 
by (induct n) 

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

384 

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

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

386 
lemma power_Suc_less: 
30996  387 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n" 
388 
by (induct n) 

389 
(auto simp add: mult_strict_left_mono) 

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

390 

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

393 
proof (induct N) 

394 
case 0 then show ?case by simp 

395 
next 

396 
case (Suc N) then show ?case 

397 
apply (auto simp add: power_Suc_less less_Suc_eq) 

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

399 
apply simp 

400 
apply (rule mult_strict_mono) apply auto 

401 
done 

402 
qed 

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

403 

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

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

407 
proof (induct N) 

408 
case 0 then show ?case by simp 

409 
next 

410 
case (Suc N) then show ?case 

411 
apply (auto simp add: le_Suc_eq) 

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

413 
apply (rule mult_mono) apply auto 

414 
done 

415 
qed 

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

416 

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

417 
lemma power_Suc_less_one: 
30996  418 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1" 
419 
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

420 

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

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

424 
proof (induct N) 

425 
case 0 then show ?case by simp 

426 
next 

427 
case (Suc N) then show ?case 

428 
apply (auto simp add: le_Suc_eq) 

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

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

431 
done 

432 
qed 

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

433 

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

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

435 
lemma power_less_power_Suc: 
30996  436 
"1 < a \<Longrightarrow> a ^ n < a * a ^ n" 
437 
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

438 

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

441 
proof (induct N) 

442 
case 0 then show ?case by simp 

443 
next 

444 
case (Suc N) then show ?case 

445 
apply (auto simp add: power_less_power_Suc less_Suc_eq) 

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

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

448 
done 

449 
qed 

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

450 

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

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

15066  454 

455 
lemma power_strict_increasing_iff [simp]: 

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

457 
by (blast intro: power_less_imp_less_exp power_strict_increasing) 
15066  458 

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

459 
lemma power_le_imp_le_base: 
30996  460 
assumes le: "a ^ Suc n \<le> b ^ Suc n" 
461 
and ynonneg: "0 \<le> b" 

462 
shows "a \<le> b" 

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

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

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

465 
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

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

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

470 
qed 
14577  471 

22853  472 
lemma power_less_imp_less_base: 
473 
assumes less: "a ^ n < b ^ n" 

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

475 
shows "a < b" 

476 
proof (rule contrapos_pp [OF less]) 

477 
assume "~ a < b" 

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

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

30996  480 
thus "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less) 
22853  481 
qed 
482 

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

483 
lemma power_inject_base: 
30996  484 
"a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b" 
485 
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

486 

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

22955  490 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

491 
lemma power2_le_imp_le: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

492 
"x\<twosuperior> \<le> y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

493 
unfolding numeral_2_eq_2 by (rule power_le_imp_le_base) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

494 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

495 
lemma power2_less_imp_less: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

496 
"x\<twosuperior> < y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

497 
by (rule power_less_imp_less_base) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

498 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

499 
lemma power2_eq_imp_eq: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

500 
"x\<twosuperior> = y\<twosuperior> \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

501 
unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

502 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

503 
end 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

504 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

505 
context linordered_ring_strict 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

506 
begin 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

507 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

508 
lemma sum_squares_eq_zero_iff: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

509 
"x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

510 
by (simp add: add_nonneg_eq_0_iff) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

511 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

512 
lemma sum_squares_le_zero_iff: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

513 
"x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

514 
by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

515 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

516 
lemma sum_squares_gt_zero_iff: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

517 
"0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

518 
by (simp add: not_le [symmetric] sum_squares_le_zero_iff) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

519 

30996  520 
end 
521 

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

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

524 

30996  525 
lemma power_abs: 
526 
"abs (a ^ n) = abs a ^ n" 

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

528 

529 
lemma abs_power_minus [simp]: 

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

35216  531 
by (simp add: power_abs) 
30996  532 

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

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

536 
case 0 show ?case by simp 

537 
next 

538 
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

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

540 

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

543 
by (rule zero_le_power [OF abs_ge_zero]) 

544 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

545 
lemma zero_le_power2 [simp]: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

546 
"0 \<le> a\<twosuperior>" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

547 
by (simp add: power2_eq_square) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

548 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

549 
lemma zero_less_power2 [simp]: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

550 
"0 < a\<twosuperior> \<longleftrightarrow> a \<noteq> 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

551 
by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

552 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

553 
lemma power2_less_0 [simp]: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

554 
"\<not> a\<twosuperior> < 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

555 
by (force simp add: power2_eq_square mult_less_0_iff) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

556 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

557 
lemma abs_power2 [simp]: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

558 
"abs (a\<twosuperior>) = a\<twosuperior>" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

559 
by (simp add: power2_eq_square abs_mult abs_mult_self) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

560 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

561 
lemma power2_abs [simp]: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

562 
"(abs a)\<twosuperior> = a\<twosuperior>" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

563 
by (simp add: power2_eq_square abs_mult_self) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

564 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

565 
lemma odd_power_less_zero: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

566 
"a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

567 
proof (induct n) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

568 
case 0 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

569 
then show ?case by simp 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

570 
next 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

571 
case (Suc n) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

572 
have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

573 
by (simp add: mult_ac power_add power2_eq_square) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

574 
thus ?case 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

575 
by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

576 
qed 
30996  577 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

578 
lemma odd_0_le_power_imp_0_le: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

579 
"0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

580 
using odd_power_less_zero [of a n] 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

581 
by (force simp add: linorder_not_less [symmetric]) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

582 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

583 
lemma zero_le_even_power'[simp]: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

584 
"0 \<le> a ^ (2*n)" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

585 
proof (induct n) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

586 
case 0 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

587 
show ?case by simp 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

588 
next 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

589 
case (Suc n) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

590 
have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

591 
by (simp add: mult_ac power_add power2_eq_square) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

592 
thus ?case 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

593 
by (simp add: Suc zero_le_mult_iff) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

594 
qed 
30996  595 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

596 
lemma sum_power2_ge_zero: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

597 
"0 \<le> x\<twosuperior> + y\<twosuperior>" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

598 
by (intro add_nonneg_nonneg zero_le_power2) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

599 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

600 
lemma not_sum_power2_lt_zero: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

601 
"\<not> x\<twosuperior> + y\<twosuperior> < 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

602 
unfolding not_less by (rule sum_power2_ge_zero) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

603 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

604 
lemma sum_power2_eq_zero_iff: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

605 
"x\<twosuperior> + y\<twosuperior> = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

606 
unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

607 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

608 
lemma sum_power2_le_zero_iff: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

609 
"x\<twosuperior> + y\<twosuperior> \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

610 
by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero) 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

611 

0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

612 
lemma sum_power2_gt_zero_iff: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

613 
"0 < x\<twosuperior> + y\<twosuperior> \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

614 
unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) 
30996  615 

616 
end 

617 

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

618 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

619 
subsection {* Miscellaneous rules *} 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

620 

47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

621 
lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m  1)))" 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

622 
unfolding One_nat_def by (cases m) simp_all 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

623 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

624 
lemma power2_sum: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

625 
fixes x y :: "'a::comm_semiring_1" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

626 
shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

627 
by (simp add: algebra_simps power2_eq_square mult_2_right) 
30996  628 

47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

629 
lemma power2_diff: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

630 
fixes x y :: "'a::comm_ring_1" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

631 
shows "(x  y)\<twosuperior> = x\<twosuperior> + y\<twosuperior>  2 * x * y" 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

632 
by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute) 
30996  633 

634 
lemma power_0_Suc [simp]: 

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

636 
by simp 

30313  637 

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

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

641 
by (induct n) simp_all 

642 

643 
lemma power_eq_0_iff [simp]: 

644 
"a ^ n = 0 \<longleftrightarrow> 

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

646 
by (induct n) 

647 
(auto simp add: no_zero_divisors elim: contrapos_pp) 

648 

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

36409  652 
by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero) 
30313  653 

30996  654 
text{*Perhaps these should be simprules.*} 
655 
lemma power_inverse: 

36409  656 
fixes a :: "'a::division_ring_inverse_zero" 
657 
shows "inverse (a ^ n) = inverse a ^ n" 

30996  658 
apply (cases "a = 0") 
659 
apply (simp add: power_0_left) 

660 
apply (simp add: nonzero_power_inverse) 

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

662 

663 
lemma power_one_over: 

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

667 
lemma power_divide: 

36409  668 
"(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n" 
30996  669 
apply (cases "b = 0") 
670 
apply (simp add: power_0_left) 

671 
apply (rule nonzero_power_divide) 

672 
apply assumption 

30313  673 
done 
674 

47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

675 
text {* Simprules for comparisons where common factors can be cancelled. *} 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

676 

30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

677 
lemmas zero_compare_simps = 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

678 
add_strict_increasing add_strict_increasing2 add_increasing 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

679 
zero_le_mult_iff zero_le_divide_iff 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

680 
zero_less_mult_iff zero_less_divide_iff 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

681 
mult_le_0_iff divide_le_0_iff 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

682 
mult_less_0_iff divide_less_0_iff 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

683 
zero_le_power2 power2_less_0 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

684 

30313  685 

30960  686 
subsection {* Exponentiation for the Natural Numbers *} 
14577  687 

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

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

23305  691 

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

694 
by (induct n) auto 

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

695 

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

30056  699 

30996  700 
lemma power_Suc_0 [simp]: 
701 
"Suc 0 ^ n = Suc 0" 

702 
by simp 

30056  703 

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

704 
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

705 
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

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

30996  709 
assumes less: "i ^ m < i ^ n" 
21413  710 
shows "m < n" 
711 
proof (cases "i = 1") 

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

713 
next 

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

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

716 
qed 

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

717 

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

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

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

720 
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

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

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

723 

51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

724 
lemma power2_nat_le_eq_le: 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

725 
fixes m n :: nat 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

726 
shows "m\<twosuperior> \<le> n\<twosuperior> \<longleftrightarrow> m \<le> n" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

727 
by (auto intro: power2_le_imp_le power_mono) 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

728 

31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

729 
lemma power2_nat_le_imp_le: 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

730 
fixes m n :: nat 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

731 
assumes "m\<twosuperior> \<le> n" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

732 
shows "m \<le> n" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

733 
using assms by (cases m) (simp_all add: power2_eq_square) 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

734 

31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

735 

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

736 

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

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

738 

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

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

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

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

742 

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

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

744 

33364  745 
code_modulename SML 
746 
Power Arith 

747 

748 
code_modulename OCaml 

749 
Power Arith 

750 

751 
code_modulename Haskell 

752 
Power Arith 

753 

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

754 
end 
49824  755 