author  paulson <lp15@cam.ac.uk> 
Tue, 31 Mar 2015 16:48:48 +0100  
changeset 59865  8a20dd967385 
parent 59741  5b762cd73a8e 
child 59867  58043346ca64 
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 

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

7 

15131  8 
theory Power 
55096  9 
imports Num Equiv_Relations 
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) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

30 
power2 :: "'a \<Rightarrow> 'a" ("(_\<^sup>2)" [1000] 999) where 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

31 
"x\<^sup>2 \<equiv> x ^ 2" 
47192
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) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

34 
power2 ("(_\<^sup>2)" [1000] 999) 
47192
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) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

37 
power2 ("(_\<^sup>2)" [1000] 999) 
47192
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 

59741
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset

54 
lemma power_Suc0_right [simp]: 
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset

55 
"a ^ Suc 0 = a" 
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset

56 
by simp 
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset

57 

30996  58 
lemma power_commutes: 
59 
"a ^ n * a = a * a ^ n" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

60 
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

61 

30996  62 
lemma power_Suc2: 
63 
"a ^ Suc n = a ^ n * a" 

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

64 
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

65 

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

68 
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

69 

30996  70 
lemma power_mult: 
71 
"a ^ (m * n) = (a ^ m) ^ n" 

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

72 
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

73 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

75 
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

76 

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

77 
lemma power3_eq_cube: "a ^ 3 = a * a * a" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

78 
by (simp add: numeral_3_eq_3 mult.assoc) 
47192
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_even_eq: 
53076  81 
"a ^ (2 * n) = (a ^ n)\<^sup>2" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

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

83 

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

84 
lemma power_odd_eq: 
53076  85 
"a ^ Suc (2*n) = a * (a ^ n)\<^sup>2" 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

86 
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

87 

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

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

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

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

91 

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

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

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

94 
unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

95 
unfolding power_Suc power_add Let_def mult.assoc .. 
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

96 

49824  97 
lemma funpow_times_power: 
98 
"(times x ^^ f x) = times (x ^ f x)" 

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

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

101 
next 

102 
case (Suc n) 

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

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

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

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

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

107 
ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult.assoc) 
49824  108 
qed 
109 

58656  110 
lemma power_commuting_commutes: 
111 
assumes "x * y = y * x" 

112 
shows "x ^ n * y = y * x ^n" 

113 
proof (induct n) 

114 
case (Suc n) 

115 
have "x ^ Suc n * y = x ^ n * y * x" 

116 
by (subst power_Suc2) (simp add: assms ac_simps) 

117 
also have "\<dots> = y * x ^ Suc n" 

118 
unfolding Suc power_Suc2 

119 
by (simp add: ac_simps) 

120 
finally show ?case . 

121 
qed simp 

122 

30996  123 
end 
124 

125 
context comm_monoid_mult 

126 
begin 

127 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
55811
diff
changeset

128 
lemma power_mult_distrib [field_simps]: 
30996  129 
"(a * b) ^ n = (a ^ n) * (b ^ n)" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

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

131 

30996  132 
end 
133 

59741
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset

134 
declare power_mult_distrib [where a = "numeral w" for w, simp] 
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset

135 
declare power_mult_distrib [where b = "numeral w" for w, simp] 
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset

136 

47191  137 
context semiring_numeral 
138 
begin 

139 

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

141 
by (simp only: sqr_conv_mult numeral_mult) 

142 

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

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

145 
numeral_sqr numeral_mult power_add power_one_right) 

146 

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

148 
by (rule numeral_pow [symmetric]) 

149 

150 
end 

151 

30996  152 
context semiring_1 
153 
begin 

154 

155 
lemma of_nat_power: 

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

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

158 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58889
diff
changeset

159 
lemma zero_power: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58889
diff
changeset

160 
"0 < n \<Longrightarrow> 0 ^ n = 0" 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58889
diff
changeset

161 
by (cases n) simp_all 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58889
diff
changeset

162 

348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58889
diff
changeset

163 
lemma power_zero_numeral [simp]: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58889
diff
changeset

164 
"0 ^ numeral k = 0" 
47209
4893907fe872
add constant pred_numeral k = numeral k  (1::nat);
huffman
parents:
47192
diff
changeset

165 
by (simp add: numeral_eq_Suc) 
47191  166 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

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

169 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

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

172 

30996  173 
end 
174 

175 
context comm_semiring_1 

176 
begin 

177 

178 
text {* The divides relation *} 

179 

180 
lemma le_imp_power_dvd: 

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

182 
proof 

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

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

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

186 
by (rule power_add) 

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

188 
qed 

189 

190 
lemma power_le_dvd: 

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

192 
by (rule dvd_trans [OF le_imp_power_dvd]) 

193 

194 
lemma dvd_power_same: 

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

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

197 

198 
lemma dvd_power_le: 

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

200 
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

201 

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

204 
shows "x dvd (x ^ n)" 

205 
using assms proof 

206 
assume "0 < n" 

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

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

209 
next 

210 
assume "x = 1" 

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

212 
qed 

213 

214 
end 

215 

216 
context ring_1 

217 
begin 

218 

219 
lemma power_minus: 

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

221 
proof (induct n) 

222 
case 0 show ?case by simp 

223 
next 

224 
case (Suc n) then show ?case 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

225 
by (simp del: power_Suc add: power_Suc2 mult.assoc) 
30996  226 
qed 
227 

47191  228 
lemma power_minus_Bit0: 
229 
"( x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)" 

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

231 
power_one_right mult_minus_left mult_minus_right minus_minus) 

232 

233 
lemma power_minus_Bit1: 

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

235 
by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left) 
47191  236 

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

237 
lemma power2_minus [simp]: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

238 
"( a)\<^sup>2 = a\<^sup>2" 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

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

240 

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

241 
lemma power_minus1_even [simp]: 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58157
diff
changeset

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

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

244 
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

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

246 
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

247 
qed 
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 power_minus1_odd: 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58157
diff
changeset

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

251 
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 power_minus_even [simp]: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

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

255 
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

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 

58787  259 
lemma power_eq_0_nat_iff [simp]: 
260 
fixes m n :: nat 

261 
shows "m ^ n = 0 \<longleftrightarrow> m = 0 \<and> n > 0" 

262 
by (induct n) auto 

263 

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

264 
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

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

266 

58787  267 
lemma power_eq_0_iff [simp]: 
268 
"a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0" 

269 
by (induct n) auto 

270 

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

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

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

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

274 

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

275 
lemma zero_eq_power2 [simp]: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

276 
"a\<^sup>2 = 0 \<longleftrightarrow> a = 0" 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

277 
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

278 

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

279 
lemma power2_eq_1_iff: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

280 
"a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a =  1" 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

281 
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

282 

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

283 
end 
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 
context idom 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

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

287 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

289 
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

290 

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

291 
end 
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 
context division_ring 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

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

295 

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

296 
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

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

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

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

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

301 

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

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

303 

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

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

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

306 

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

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

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

309 
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

310 

59741
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset

311 
declare nonzero_power_divide [where b = "numeral w" for w, simp] 
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset

312 

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

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

314 

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

315 

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

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

317 

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

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

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

320 

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

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

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

323 
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

324 

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

325 
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

326 
"\<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

327 
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

328 

30996  329 
end 
330 

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

331 
context linordered_semidom 
30996  332 
begin 
333 

334 
lemma zero_less_power [simp]: 

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

56544  336 
by (induct n) simp_all 
30996  337 

338 
lemma zero_le_power [simp]: 

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

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

341 

47241  342 
lemma power_mono: 
343 
"a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n" 

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

345 

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

347 
using power_mono [of 1 a n] by simp 

348 

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

350 
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

351 

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

352 
lemma power_gt1_lemma: 
30996  353 
assumes gt1: "1 < a" 
354 
shows "1 < a * a ^ n" 

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

355 
proof  
30996  356 
from gt1 have "0 \<le> a" 
357 
by (fact order_trans [OF zero_le_one less_imp_le]) 

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

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

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

14577  361 
zero_le_one order_refl) 
362 
finally show ?thesis by simp 

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

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

364 

30996  365 
lemma power_gt1: 
366 
"1 < a \<Longrightarrow> 1 < a ^ Suc n" 

367 
by (simp add: power_gt1_lemma) 

24376  368 

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

371 
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

372 

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

373 
lemma power_le_imp_le_exp: 
30996  374 
assumes gt1: "1 < a" 
375 
shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n" 

376 
proof (induct m arbitrary: n) 

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

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

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

380 
case (Suc m) 
14577  381 
show ?case 
382 
proof (cases n) 

383 
case 0 

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

30996  387 
not_less [symmetric]) 
14577  388 
next 
389 
case (Suc n) 

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

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

395 

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

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

400 

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

401 
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

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

403 
lemma power_less_imp_less_exp: 
30996  404 
"1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n" 
405 
by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] 

406 
power_le_imp_le_exp) 

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

407 

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

408 
lemma power_strict_mono [rule_format]: 
30996  409 
"a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n" 
410 
by (induct n) 

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

412 

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

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

414 
lemma power_Suc_less: 
30996  415 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n" 
416 
by (induct n) 

417 
(auto simp add: mult_strict_left_mono) 

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

418 

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

421 
proof (induct N) 

422 
case 0 then show ?case by simp 

423 
next 

424 
case (Suc N) then show ?case 

425 
apply (auto simp add: power_Suc_less less_Suc_eq) 

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

427 
apply simp 

428 
apply (rule mult_strict_mono) apply auto 

429 
done 

430 
qed 

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

431 

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

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

435 
proof (induct N) 

436 
case 0 then show ?case by simp 

437 
next 

438 
case (Suc N) then show ?case 

439 
apply (auto simp add: le_Suc_eq) 

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

441 
apply (rule mult_mono) apply auto 

442 
done 

443 
qed 

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

444 

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

445 
lemma power_Suc_less_one: 
30996  446 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1" 
447 
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

448 

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

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

452 
proof (induct N) 

453 
case 0 then show ?case by simp 

454 
next 

455 
case (Suc N) then show ?case 

456 
apply (auto simp add: le_Suc_eq) 

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

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

459 
done 

460 
qed 

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

461 

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

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

463 
lemma power_less_power_Suc: 
30996  464 
"1 < a \<Longrightarrow> a ^ n < a * a ^ n" 
465 
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

466 

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

469 
proof (induct N) 

470 
case 0 then show ?case by simp 

471 
next 

472 
case (Suc N) then show ?case 

473 
apply (auto simp add: power_less_power_Suc less_Suc_eq) 

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

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

476 
done 

477 
qed 

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

478 

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

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

15066  482 

483 
lemma power_strict_increasing_iff [simp]: 

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

485 
by (blast intro: power_less_imp_less_exp power_strict_increasing) 
15066  486 

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

487 
lemma power_le_imp_le_base: 
30996  488 
assumes le: "a ^ Suc n \<le> b ^ Suc n" 
489 
and ynonneg: "0 \<le> b" 

490 
shows "a \<le> b" 

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

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

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

493 
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

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

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

498 
qed 
14577  499 

22853  500 
lemma power_less_imp_less_base: 
501 
assumes less: "a ^ n < b ^ n" 

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

503 
shows "a < b" 

504 
proof (rule contrapos_pp [OF less]) 

505 
assume "~ a < b" 

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

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

30996  508 
thus "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less) 
22853  509 
qed 
510 

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

511 
lemma power_inject_base: 
30996  512 
"a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b" 
513 
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

514 

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

22955  518 

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

519 
lemma power2_le_imp_le: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

520 
"x\<^sup>2 \<le> y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y" 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

521 
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

522 

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

523 
lemma power2_less_imp_less: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

524 
"x\<^sup>2 < y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y" 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

525 
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

526 

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

527 
lemma power2_eq_imp_eq: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

529 
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

530 

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

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

532 

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

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

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

535 

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

536 
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

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

538 
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

539 

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

540 
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

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

542 
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

543 

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

544 
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

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

546 
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

547 

30996  548 
end 
549 

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

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

552 

30996  553 
lemma power_abs: 
554 
"abs (a ^ n) = abs a ^ n" 

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

556 

557 
lemma abs_power_minus [simp]: 

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

35216  559 
by (simp add: power_abs) 
30996  560 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53076
diff
changeset

561 
lemma zero_less_power_abs_iff [simp]: 
30996  562 
"0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0" 
563 
proof (induct n) 

564 
case 0 show ?case by simp 

565 
next 

566 
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

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

568 

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

571 
by (rule zero_le_power [OF abs_ge_zero]) 

572 

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

573 
lemma zero_le_power2 [simp]: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

574 
"0 \<le> a\<^sup>2" 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

575 
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

576 

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

577 
lemma zero_less_power2 [simp]: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

578 
"0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0" 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

579 
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

580 

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

581 
lemma power2_less_0 [simp]: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

582 
"\<not> a\<^sup>2 < 0" 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

583 
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

584 

58787  585 
lemma power2_less_eq_zero_iff [simp]: 
586 
"a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0" 

587 
by (simp add: le_less) 

588 

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

589 
lemma abs_power2 [simp]: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

591 
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

592 

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

593 
lemma power2_abs [simp]: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

595 
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

596 

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

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

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

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

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

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

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

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

604 
have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

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

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

607 
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

608 
qed 
30996  609 

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

610 
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

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

612 
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

613 
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

614 

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

615 
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

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

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

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

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

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

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

622 
have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

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

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

625 
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

626 
qed 
30996  627 

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

628 
lemma sum_power2_ge_zero: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

629 
"0 \<le> x\<^sup>2 + y\<^sup>2" 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

630 
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

631 

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

632 
lemma not_sum_power2_lt_zero: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

633 
"\<not> x\<^sup>2 + y\<^sup>2 < 0" 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

634 
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

635 

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

636 
lemma sum_power2_eq_zero_iff: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

638 
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

639 

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

640 
lemma sum_power2_le_zero_iff: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

642 
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

643 

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

644 
lemma sum_power2_gt_zero_iff: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

646 
unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) 
30996  647 

59865
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

648 
lemma abs_le_square_iff: 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

649 
"\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> x\<^sup>2 \<le> y\<^sup>2" 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

650 
proof 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

651 
assume "\<bar>x\<bar> \<le> \<bar>y\<bar>" 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

652 
then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono, simp) 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

653 
then show "x\<^sup>2 \<le> y\<^sup>2" by simp 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

654 
next 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

655 
assume "x\<^sup>2 \<le> y\<^sup>2" 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

656 
then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

657 
by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero]) 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

658 
qed 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

659 

8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

660 
lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> abs(x) \<le> 1" 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

661 
using abs_le_square_iff [of x 1] 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

662 
by simp 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

663 

8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

664 
lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> abs(x) = 1" 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

665 
by (auto simp add: abs_if power2_eq_1_iff) 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

666 

8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

667 
lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> abs(x) < 1" 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

668 
using abs_square_eq_1 [of x] abs_square_le_1 [of x] 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

669 
by (auto simp add: le_less) 
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset

670 

30996  671 
end 
672 

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

673 

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

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

675 

55718
34618f031ba9
A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents:
55096
diff
changeset

676 
lemma self_le_power: 
34618f031ba9
A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents:
55096
diff
changeset

677 
fixes x::"'a::linordered_semidom" 
34618f031ba9
A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents:
55096
diff
changeset

678 
shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n" 
55811  679 
using power_increasing[of 1 n x] power_one_right[of x] by auto 
55718
34618f031ba9
A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents:
55096
diff
changeset

680 

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

681 
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

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

683 

58787  684 
lemma (in comm_semiring_1) power2_sum: 
685 
"(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y" 

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

686 
by (simp add: algebra_simps power2_eq_square mult_2_right) 
30996  687 

58787  688 
lemma (in comm_ring_1) power2_diff: 
689 
"(x  y)\<^sup>2 = x\<^sup>2 + y\<^sup>2  2 * x * y" 

690 
by (simp add: algebra_simps power2_eq_square mult_2_right) 

30996  691 

692 
lemma power_0_Suc [simp]: 

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

694 
by simp 

30313  695 

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

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

699 
by (induct n) simp_all 

700 

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

36409  704 
by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero) 
30313  705 

30996  706 
text{*Perhaps these should be simprules.*} 
707 
lemma power_inverse: 

36409  708 
fixes a :: "'a::division_ring_inverse_zero" 
709 
shows "inverse (a ^ n) = inverse a ^ n" 

30996  710 
apply (cases "a = 0") 
711 
apply (simp add: power_0_left) 

712 
apply (simp add: nonzero_power_inverse) 

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

714 

715 
lemma power_one_over: 

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

56481  719 
lemma power_divide [field_simps, divide_simps]: 
36409  720 
"(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n" 
30996  721 
apply (cases "b = 0") 
722 
apply (simp add: power_0_left) 

723 
apply (rule nonzero_power_divide) 

724 
apply assumption 

30313  725 
done 
726 

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

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

728 

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

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

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

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

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

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

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

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

736 

30313  737 

30960  738 
subsection {* Exponentiation for the Natural Numbers *} 
14577  739 

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

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

23305  743 

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

746 
by (induct n) auto 

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

747 

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

30056  751 

30996  752 
lemma power_Suc_0 [simp]: 
753 
"Suc 0 ^ n = Suc 0" 

754 
by simp 

30056  755 

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

756 
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

757 
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

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

30996  761 
assumes less: "i ^ m < i ^ n" 
21413  762 
shows "m < n" 
763 
proof (cases "i = 1") 

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

765 
next 

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

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

768 
qed 

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

769 

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

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

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

772 
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

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

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

775 

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

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

777 
fixes m n :: nat 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

778 
shows "m\<^sup>2 \<le> n\<^sup>2 \<longleftrightarrow> m \<le> n" 
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

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

780 

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

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

782 
fixes m n :: nat 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

783 
assumes "m\<^sup>2 \<le> n" 
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset

784 
shows "m \<le> n" 
54249  785 
proof (cases m) 
786 
case 0 then show ?thesis by simp 

787 
next 

788 
case (Suc k) 

789 
show ?thesis 

790 
proof (rule ccontr) 

791 
assume "\<not> m \<le> n" 

792 
then have "n < m" by simp 

793 
with assms Suc show False 

794 
by (auto simp add: algebra_simps) (simp add: power2_eq_square) 

795 
qed 

796 
qed 

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

797 

55096  798 
subsubsection {* Cardinality of the Powerset *} 
799 

800 
lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2" 

801 
unfolding UNIV_bool by simp 

802 

803 
lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A" 

804 
proof (induct rule: finite_induct) 

805 
case empty 

806 
show ?case by auto 

807 
next 

808 
case (insert x A) 

809 
then have "inj_on (insert x) (Pow A)" 

810 
unfolding inj_on_def by (blast elim!: equalityE) 

811 
then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A" 

812 
by (simp add: mult_2 card_image Pow_insert insert.hyps) 

813 
then show ?case using insert 

814 
apply (simp add: Pow_insert) 

815 
apply (subst card_Un_disjoint, auto) 

816 
done 

817 
qed 

818 

57418  819 

820 
subsubsection {* Generalized sum over a set *} 

821 

822 
lemma setsum_zero_power [simp]: 

823 
fixes c :: "nat \<Rightarrow> 'a::division_ring" 

824 
shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)" 

825 
apply (cases "finite A") 

826 
by (induction A rule: finite_induct) auto 

827 

828 
lemma setsum_zero_power' [simp]: 

829 
fixes c :: "nat \<Rightarrow> 'a::field" 

830 
shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)" 

831 
using setsum_zero_power [of "\<lambda>i. c i / d i" A] 

832 
by auto 

833 

834 

55096  835 
subsubsection {* Generalized product over a set *} 
836 

837 
lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)" 

838 
apply (erule finite_induct) 

839 
apply auto 

840 
done 

841 

57418  842 
lemma setprod_power_distrib: 
843 
fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1" 

844 
shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A" 

845 
proof (cases "finite A") 

846 
case True then show ?thesis 

847 
by (induct A rule: finite_induct) (auto simp add: power_mult_distrib) 

848 
next 

849 
case False then show ?thesis 

850 
by simp 

851 
qed 

852 

58437  853 
lemma power_setsum: 
854 
"c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)" 

855 
by (induct A rule: infinite_finite_induct) (simp_all add: power_add) 

856 

55096  857 
lemma setprod_gen_delta: 
858 
assumes fS: "finite S" 

859 
shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S  1) else c^ card S)" 

860 
proof 

861 
let ?f = "(\<lambda>k. if k=a then b k else c)" 

862 
{assume a: "a \<notin> S" 

863 
hence "\<forall> k\<in> S. ?f k = c" by simp 

864 
hence ?thesis using a setprod_constant[OF fS, of c] by simp } 

865 
moreover 

866 
{assume a: "a \<in> S" 

867 
let ?A = "S  {a}" 

868 
let ?B = "{a}" 

869 
have eq: "S = ?A \<union> ?B" using a by blast 

870 
have dj: "?A \<inter> ?B = {}" by simp 

871 
from fS have fAB: "finite ?A" "finite ?B" by auto 

872 
have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A" 

57418  873 
apply (rule setprod.cong) by auto 
55096  874 
have cA: "card ?A = card S  1" using fS a by auto 
875 
have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto 

876 
have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" 

57418  877 
using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] 
55096  878 
by simp 
879 
then have ?thesis using a cA 

57418  880 
by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)} 
55096  881 
ultimately show ?thesis by blast 
882 
qed 

883 

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

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

885 

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

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

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

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

889 

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

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

891 

52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51263
diff
changeset

892 
code_identifier 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51263
diff
changeset

893 
code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 
33364  894 

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

895 
end 
49824  896 