author  wenzelm 
Sat, 18 Jul 2015 22:58:50 +0200  
changeset 60758  d8d85a8172b5 
parent 60685  cb21b7022b00 
child 60866  7f562aa4eb4b 
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 

60758  6 
section \<open>Exponentiation\<close> 
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 

60758  12 
subsection \<open>Powers for Arbitrary Monoids\<close> 
30960  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 

60758  27 
text \<open>Special syntax for squares.\<close> 
47192
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 

60758  134 
text\<open>Extract constant factors from powers\<close> 
59741
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 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

136 
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

137 

60155
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

138 
lemma power_add_numeral [simp]: 
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

139 
fixes a :: "'a :: monoid_mult" 
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

140 
shows "a^numeral m * a^numeral n = a^numeral (m + n)" 
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

141 
by (simp add: power_add [symmetric]) 
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

142 

91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

143 
lemma power_add_numeral2 [simp]: 
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

144 
fixes a :: "'a :: monoid_mult" 
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

145 
shows "a^numeral m * (a^numeral n * b) = a^numeral (m + n) * b" 
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

146 
by (simp add: mult.assoc [symmetric]) 
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

147 

91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

148 
lemma power_mult_numeral [simp]: 
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

149 
fixes a :: "'a :: monoid_mult" 
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

150 
shows"(a^numeral m)^numeral n = a^numeral (m * n)" 
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

151 
by (simp only: numeral_mult power_mult) 
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

152 

47191  153 
context semiring_numeral 
154 
begin 

155 

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

157 
by (simp only: sqr_conv_mult numeral_mult) 

158 

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

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

161 
numeral_sqr numeral_mult power_add power_one_right) 

162 

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

164 
by (rule numeral_pow [symmetric]) 

165 

166 
end 

167 

30996  168 
context semiring_1 
169 
begin 

170 

171 
lemma of_nat_power: 

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

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

174 

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

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

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

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

178 

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

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

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

181 
by (simp add: numeral_eq_Suc) 
47191  182 

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

183 
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

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

185 

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

186 
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

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

188 

30996  189 
end 
190 

191 
context comm_semiring_1 

192 
begin 

193 

60758  194 
text \<open>The divides relation\<close> 
30996  195 

196 
lemma le_imp_power_dvd: 

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

198 
proof 

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

60758  200 
using \<open>m \<le> n\<close> by simp 
30996  201 
also have "\<dots> = a ^ m * a ^ (n  m)" 
202 
by (rule power_add) 

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

204 
qed 

205 

206 
lemma power_le_dvd: 

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

208 
by (rule dvd_trans [OF le_imp_power_dvd]) 

209 

210 
lemma dvd_power_same: 

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

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

213 

214 
lemma dvd_power_le: 

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

216 
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

217 

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

220 
shows "x dvd (x ^ n)" 

221 
using assms proof 

222 
assume "0 < n" 

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

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

225 
next 

226 
assume "x = 1" 

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

228 
qed 

229 

230 
end 

231 

232 
context ring_1 

233 
begin 

234 

235 
lemma power_minus: 

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

237 
proof (induct n) 

238 
case 0 show ?case by simp 

239 
next 

240 
case (Suc n) then show ?case 

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

241 
by (simp del: power_Suc add: power_Suc2 mult.assoc) 
30996  242 
qed 
243 

47191  244 
lemma power_minus_Bit0: 
245 
"( x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)" 

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

247 
power_one_right mult_minus_left mult_minus_right minus_minus) 

248 

249 
lemma power_minus_Bit1: 

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

251 
by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left) 
47191  252 

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

253 
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

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

255 
by (rule power_minus_Bit0) 
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 
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

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

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

260 
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

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

262 
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

263 
qed 
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 
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

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

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

268 

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

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

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

271 
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

272 

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

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

274 

58787  275 
lemma power_eq_0_nat_iff [simp]: 
276 
fixes m n :: nat 

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

278 
by (induct n) auto 

279 

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

280 
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

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

282 

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

285 
by (induct n) auto 

286 

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

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

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

289 
by (induct n) auto 
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 
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

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

293 
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

294 

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

295 
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

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

297 
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

298 

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

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

300 

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

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

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

303 

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

304 
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

305 
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

306 

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

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

308 

60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

309 
context normalization_semidom 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

310 
begin 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

311 

cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

312 
lemma normalize_power: 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

313 
"normalize (a ^ n) = normalize a ^ n" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

314 
by (induct n) (simp_all add: normalize_mult) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

315 

cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

316 
lemma unit_factor_power: 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

317 
"unit_factor (a ^ n) = unit_factor a ^ n" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

318 
by (induct n) (simp_all add: unit_factor_mult) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

319 

cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

320 
end 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset

321 

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

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

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

324 

60758  325 
text \<open>FIXME reorient or rename to @{text nonzero_inverse_power}\<close> 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

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

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

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

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

330 

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

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

332 

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

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

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

335 

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

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

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

338 
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

339 

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

340 
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

341 

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

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

343 

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

344 

60758  345 
subsection \<open>Exponentiation on ordered types\<close> 
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

346 

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

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

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

349 

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

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

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

352 
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

353 

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

354 
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

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

356 
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

357 

30996  358 
end 
359 

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

360 
context linordered_semidom 
30996  361 
begin 
362 

363 
lemma zero_less_power [simp]: 

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

56544  365 
by (induct n) simp_all 
30996  366 

367 
lemma zero_le_power [simp]: 

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

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

370 

47241  371 
lemma power_mono: 
372 
"a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n" 

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

374 

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

376 
using power_mono [of 1 a n] by simp 

377 

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

379 
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

380 

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

381 
lemma power_gt1_lemma: 
30996  382 
assumes gt1: "1 < a" 
383 
shows "1 < a * a ^ n" 

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

384 
proof  
30996  385 
from gt1 have "0 \<le> a" 
386 
by (fact order_trans [OF zero_le_one less_imp_le]) 

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

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

60758  389 
by (simp only: mult_mono \<open>0 \<le> a\<close> one_le_power order_less_imp_le 
14577  390 
zero_le_one order_refl) 
391 
finally show ?thesis by simp 

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

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

393 

30996  394 
lemma power_gt1: 
395 
"1 < a \<Longrightarrow> 1 < a ^ Suc n" 

396 
by (simp add: power_gt1_lemma) 

24376  397 

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

400 
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

401 

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

402 
lemma power_le_imp_le_exp: 
30996  403 
assumes gt1: "1 < a" 
404 
shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n" 

405 
proof (induct m arbitrary: n) 

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

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

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

409 
case (Suc m) 
14577  410 
show ?case 
411 
proof (cases n) 

412 
case 0 

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

30996  416 
not_less [symmetric]) 
14577  417 
next 
418 
case (Suc n) 

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

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

424 

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

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

429 

60758  430 
text\<open>Can relax the first premise to @{term "0<a"} in the case of the 
431 
natural numbers.\<close> 

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

432 
lemma power_less_imp_less_exp: 
30996  433 
"1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n" 
434 
by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] 

435 
power_le_imp_le_exp) 

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

436 

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

437 
lemma power_strict_mono [rule_format]: 
30996  438 
"a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n" 
439 
by (induct n) 

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

441 

60758  442 
text\<open>Lemma for @{text power_strict_decreasing}\<close> 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

443 
lemma power_Suc_less: 
30996  444 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n" 
445 
by (induct n) 

446 
(auto simp add: mult_strict_left_mono) 

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

447 

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

450 
proof (induct N) 

451 
case 0 then show ?case by simp 

452 
next 

453 
case (Suc N) then show ?case 

454 
apply (auto simp add: power_Suc_less less_Suc_eq) 

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

456 
apply simp 

457 
apply (rule mult_strict_mono) apply auto 

458 
done 

459 
qed 

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

460 

60758  461 
text\<open>Proof resembles that of @{text power_strict_decreasing}\<close> 
30996  462 
lemma power_decreasing [rule_format]: 
463 
"n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<longrightarrow> a ^ N \<le> a ^ n" 

464 
proof (induct N) 

465 
case 0 then show ?case by simp 

466 
next 

467 
case (Suc N) then show ?case 

468 
apply (auto simp add: le_Suc_eq) 

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

470 
apply (rule mult_mono) apply auto 

471 
done 

472 
qed 

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

473 

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

474 
lemma power_Suc_less_one: 
30996  475 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1" 
476 
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

477 

60758  478 
text\<open>Proof again resembles that of @{text power_strict_decreasing}\<close> 
30996  479 
lemma power_increasing [rule_format]: 
480 
"n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N" 

481 
proof (induct N) 

482 
case 0 then show ?case by simp 

483 
next 

484 
case (Suc N) then show ?case 

485 
apply (auto simp add: le_Suc_eq) 

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

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

488 
done 

489 
qed 

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

490 

60758  491 
text\<open>Lemma for @{text power_strict_increasing}\<close> 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

492 
lemma power_less_power_Suc: 
30996  493 
"1 < a \<Longrightarrow> a ^ n < a * a ^ n" 
494 
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

495 

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

498 
proof (induct N) 

499 
case 0 then show ?case by simp 

500 
next 

501 
case (Suc N) then show ?case 

502 
apply (auto simp add: power_less_power_Suc less_Suc_eq) 

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

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

505 
done 

506 
qed 

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

507 

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

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

15066  511 

512 
lemma power_strict_increasing_iff [simp]: 

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

514 
by (blast intro: power_less_imp_less_exp power_strict_increasing) 
15066  515 

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

516 
lemma power_le_imp_le_base: 
30996  517 
assumes le: "a ^ Suc n \<le> b ^ Suc n" 
518 
and ynonneg: "0 \<le> b" 

519 
shows "a \<le> b" 

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

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

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

522 
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

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

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

527 
qed 
14577  528 

22853  529 
lemma power_less_imp_less_base: 
530 
assumes less: "a ^ n < b ^ n" 

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

532 
shows "a < b" 

533 
proof (rule contrapos_pp [OF less]) 

534 
assume "~ a < b" 

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

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

30996  537 
thus "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less) 
22853  538 
qed 
539 

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

540 
lemma power_inject_base: 
30996  541 
"a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b" 
542 
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

543 

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

22955  547 

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

548 
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

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

550 
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

551 

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

552 
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

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

554 
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

555 

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

556 
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

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

558 
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

559 

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

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

561 

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

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

563 
begin 
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 sum_squares_eq_zero_iff: 
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset

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

567 
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

568 

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

569 
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

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

571 
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

572 

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

573 
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

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

575 
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

576 

30996  577 
end 
578 

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

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

581 

30996  582 
lemma power_abs: 
583 
"abs (a ^ n) = abs a ^ n" 

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

585 

586 
lemma abs_power_minus [simp]: 

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

35216  588 
by (simp add: power_abs) 
30996  589 

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

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

593 
case 0 show ?case by simp 

594 
next 

595 
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

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

597 

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

600 
by (rule zero_le_power [OF abs_ge_zero]) 

601 

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

602 
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

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

604 
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

605 

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

606 
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

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

608 
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

609 

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

610 
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

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

612 
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

613 

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

616 
by (simp add: le_less) 

617 

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

618 
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

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

620 
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

621 

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

622 
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

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

624 
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

625 

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

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

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

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

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

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

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

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

633 
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

634 
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

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

636 
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

637 
qed 
30996  638 

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

639 
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

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

641 
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

642 
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

643 

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

644 
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

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

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

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

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

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

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

651 
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

652 
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

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

654 
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

655 
qed 
30996  656 

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

657 
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

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

659 
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

660 

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

661 
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

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

663 
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

664 

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

665 
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

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

667 
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

668 

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

669 
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

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

671 
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

672 

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

673 
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

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

675 
unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) 
30996  676 

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

677 
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

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

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

680 
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

681 
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

682 
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

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

684 
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

685 
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

686 
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

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

688 

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

689 
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

690 
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

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

692 

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

693 
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

694 
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

695 

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

696 
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

697 
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

698 
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

699 

30996  700 
end 
701 

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

702 

60758  703 
subsection \<open>Miscellaneous rules\<close> 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

704 

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

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

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

707 
shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n" 
55811  708 
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

709 

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

710 
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

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

712 

58787  713 
lemma (in comm_semiring_1) power2_sum: 
714 
"(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

715 
by (simp add: algebra_simps power2_eq_square mult_2_right) 
30996  716 

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

719 
by (simp add: algebra_simps power2_eq_square mult_2_right) 

30996  720 

721 
lemma power_0_Suc [simp]: 

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

723 
by simp 

30313  724 

60758  725 
text\<open>It looks plausible as a simprule, but its effect can be strange.\<close> 
30996  726 
lemma power_0_left: 
727 
"0 ^ n = (if n = 0 then 1 else (0::'a::{power, semiring_0}))" 

728 
by (induct n) simp_all 

729 

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

36409  733 
by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero) 
30313  734 

60758  735 
text\<open>Perhaps these should be simprules.\<close> 
30996  736 
lemma power_inverse: 
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59865
diff
changeset

737 
fixes a :: "'a::division_ring" 
36409  738 
shows "inverse (a ^ n) = inverse a ^ n" 
30996  739 
apply (cases "a = 0") 
740 
apply (simp add: power_0_left) 

741 
apply (simp add: nonzero_power_inverse) 

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

743 

744 
lemma power_one_over: 

59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59865
diff
changeset

745 
"1 / (a::'a::{field, power}) ^ n = (1 / a) ^ n" 
30996  746 
by (simp add: divide_inverse) (rule power_inverse) 
747 

56481  748 
lemma power_divide [field_simps, divide_simps]: 
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59865
diff
changeset

749 
"(a / b) ^ n = (a::'a::field) ^ n / b ^ n" 
30996  750 
apply (cases "b = 0") 
751 
apply (simp add: power_0_left) 

752 
apply (rule nonzero_power_divide) 

753 
apply assumption 

30313  754 
done 
755 

60758  756 
text \<open>Simprules for comparisons where common factors can be cancelled.\<close> 
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset

757 

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

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

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

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

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

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

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

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

765 

30313  766 

60758  767 
subsection \<open>Exponentiation for the Natural Numbers\<close> 
14577  768 

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

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

23305  772 

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

775 
by (induct n) auto 

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

776 

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

30056  780 

30996  781 
lemma power_Suc_0 [simp]: 
782 
"Suc 0 ^ n = Suc 0" 

783 
by simp 

30056  784 

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

786 
Premises cannot be weakened: consider the case where @{term "i=0"}, 
60758  787 
@{term "m=1"} and @{term "n=0"}.\<close> 
21413  788 
lemma nat_power_less_imp_less: 
789 
assumes nonneg: "0 < (i\<Colon>nat)" 

30996  790 
assumes less: "i ^ m < i ^ n" 
21413  791 
shows "m < n" 
792 
proof (cases "i = 1") 

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

794 
next 

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

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

797 
qed 

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

798 

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

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

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

801 
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

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

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

804 

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

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

806 
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

807 
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

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

809 

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

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

811 
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

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

813 
shows "m \<le> n" 
54249  814 
proof (cases m) 
815 
case 0 then show ?thesis by simp 

816 
next 

817 
case (Suc k) 

818 
show ?thesis 

819 
proof (rule ccontr) 

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

821 
then have "n < m" by simp 

822 
with assms Suc show False 

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

824 
qed 

825 
qed 

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

826 

60758  827 
subsubsection \<open>Cardinality of the Powerset\<close> 
55096  828 

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

830 
unfolding UNIV_bool by simp 

831 

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

833 
proof (induct rule: finite_induct) 

834 
case empty 

835 
show ?case by auto 

836 
next 

837 
case (insert x A) 

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

839 
unfolding inj_on_def by (blast elim!: equalityE) 

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

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

842 
then show ?case using insert 

843 
apply (simp add: Pow_insert) 

844 
apply (subst card_Un_disjoint, auto) 

845 
done 

846 
qed 

847 

57418  848 

60758  849 
subsubsection \<open>Generalized sum over a set\<close> 
57418  850 

851 
lemma setsum_zero_power [simp]: 

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

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

854 
apply (cases "finite A") 

855 
by (induction A rule: finite_induct) auto 

856 

857 
lemma setsum_zero_power' [simp]: 

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

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

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

861 
by auto 

862 

863 

60758  864 
subsubsection \<open>Generalized product over a set\<close> 
55096  865 

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

867 
apply (erule finite_induct) 

868 
apply auto 

869 
done 

870 

57418  871 
lemma setprod_power_distrib: 
872 
fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1" 

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

874 
proof (cases "finite A") 

875 
case True then show ?thesis 

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

877 
next 

878 
case False then show ?thesis 

879 
by simp 

880 
qed 

881 

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

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

885 

55096  886 
lemma setprod_gen_delta: 
887 
assumes fS: "finite S" 

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

889 
proof 

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

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

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

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

894 
moreover 

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

896 
let ?A = "S  {a}" 

897 
let ?B = "{a}" 

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

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

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

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

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

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

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

57418  909 
by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)} 
55096  910 
ultimately show ?thesis by blast 
911 
qed 

912 

60758  913 
subsection \<open>Code generator tweak\<close> 
31155
92d8ff6af82c
monomorphic code generation for power operations
haftmann
parents:
31021
diff
changeset

914 

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

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

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

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

918 

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

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

920 

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

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

922 
code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 
33364  923 

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

924 
end 
49824  925 