author  huffman 
Thu, 29 Mar 2012 14:09:10 +0200  
changeset 47192  0c0501cb6da6 
parent 47191  ebd8c46d156b 
child 47209  4893907fe872 
permissions  rwrr 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset

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

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

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

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

5 

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

7 

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

11 

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

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

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

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

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

20 

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

23 

24 
notation (HTML output) 

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

26 

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

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

28 

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

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

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

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

32 

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

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

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

35 

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

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

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

38 

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

40 

30996  41 
context monoid_mult 
42 
begin 

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

43 

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

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

45 

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

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

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

49 

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

53 

30996  54 
lemma power_commutes: 
55 
"a ^ n * a = a * a ^ n" 

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

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

57 

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

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

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

61 

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

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

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

65 

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

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

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

69 

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

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

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

72 

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

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

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

75 

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

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

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

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

79 

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

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

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

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

83 

30996  84 
end 
85 

86 
context comm_monoid_mult 

87 
begin 

88 

89 
lemma power_mult_distrib: 

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

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

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

92 

30996  93 
end 
94 

47191  95 
context semiring_numeral 
96 
begin 

97 

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

99 
by (simp only: sqr_conv_mult numeral_mult) 

100 

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

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

103 
numeral_sqr numeral_mult power_add power_one_right) 

104 

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

106 
by (rule numeral_pow [symmetric]) 

107 

108 
end 

109 

30996  110 
context semiring_1 
111 
begin 

112 

113 
lemma of_nat_power: 

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

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

116 

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

119 

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

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

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

122 

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

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

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

125 

30996  126 
end 
127 

128 
context comm_semiring_1 

129 
begin 

130 

131 
text {* The divides relation *} 

132 

133 
lemma le_imp_power_dvd: 

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

135 
proof 

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

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

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

139 
by (rule power_add) 

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

141 
qed 

142 

143 
lemma power_le_dvd: 

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

145 
by (rule dvd_trans [OF le_imp_power_dvd]) 

146 

147 
lemma dvd_power_same: 

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

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

150 

151 
lemma dvd_power_le: 

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

153 
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

154 

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

157 
shows "x dvd (x ^ n)" 

158 
using assms proof 

159 
assume "0 < n" 

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

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

162 
next 

163 
assume "x = 1" 

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

165 
qed 

166 

167 
end 

168 

169 
context ring_1 

170 
begin 

171 

172 
lemma power_minus: 

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

174 
proof (induct n) 

175 
case 0 show ?case by simp 

176 
next 

177 
case (Suc n) then show ?case 

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

179 
qed 

180 

47191  181 
lemma power_minus_Bit0: 
182 
"( x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)" 

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

184 
power_one_right mult_minus_left mult_minus_right minus_minus) 

185 

186 
lemma power_minus_Bit1: 

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

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

189 

190 
lemma power_neg_numeral_Bit0 [simp]: 

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

192 
by (simp only: neg_numeral_def power_minus_Bit0 power_numeral) 

193 

194 
lemma power_neg_numeral_Bit1 [simp]: 

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

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

197 

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

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

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

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

201 

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

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

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

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

205 
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

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

207 
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

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

209 

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

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

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

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

213 

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

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

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

216 
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

217 

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

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

219 

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

220 
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

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

222 

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

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

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

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

226 

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

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

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

229 
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

230 

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

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

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

233 
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

234 

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

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

236 

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

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

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

239 

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

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

241 
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

242 

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

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

244 

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

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

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

247 

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

248 
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

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

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

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

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

253 

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

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

255 

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

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

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

258 

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

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

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

261 
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

262 

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

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

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

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

267 

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

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

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

270 

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

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

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

273 
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

274 

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

275 
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

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

277 
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

278 

30996  279 
end 
280 

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

281 
context linordered_semidom 
30996  282 
begin 
283 

284 
lemma zero_less_power [simp]: 

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

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

287 

288 
lemma zero_le_power [simp]: 

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

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

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

291 

25874  292 
lemma one_le_power[simp]: 
30996  293 
"1 \<le> a \<Longrightarrow> 1 \<le> a ^ n" 
294 
apply (induct n) 

295 
apply simp_all 

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

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

298 
done 

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

299 

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

300 
lemma power_gt1_lemma: 
30996  301 
assumes gt1: "1 < a" 
302 
shows "1 < a * a ^ n" 

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

303 
proof  
30996  304 
from gt1 have "0 \<le> a" 
305 
by (fact order_trans [OF zero_le_one less_imp_le]) 

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

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

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

14577  309 
zero_le_one order_refl) 
310 
finally show ?thesis by simp 

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

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

312 

30996  313 
lemma power_gt1: 
314 
"1 < a \<Longrightarrow> 1 < a ^ Suc n" 

315 
by (simp add: power_gt1_lemma) 

24376  316 

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

319 
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

320 

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

321 
lemma power_le_imp_le_exp: 
30996  322 
assumes gt1: "1 < a" 
323 
shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n" 

324 
proof (induct m arbitrary: n) 

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

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

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

328 
case (Suc m) 
14577  329 
show ?case 
330 
proof (cases n) 

331 
case 0 

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

30996  335 
not_less [symmetric]) 
14577  336 
next 
337 
case (Suc n) 

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

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

343 

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

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

348 

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

349 
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

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

351 
lemma power_less_imp_less_exp: 
30996  352 
"1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n" 
353 
by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] 

354 
power_le_imp_le_exp) 

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

355 

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

356 
lemma power_mono: 
30996  357 
"a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n" 
358 
by (induct n) 

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

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

360 

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

361 
lemma power_strict_mono [rule_format]: 
30996  362 
"a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n" 
363 
by (induct n) 

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

365 

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

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

367 
lemma power_Suc_less: 
30996  368 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n" 
369 
by (induct n) 

370 
(auto simp add: mult_strict_left_mono) 

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

371 

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

374 
proof (induct N) 

375 
case 0 then show ?case by simp 

376 
next 

377 
case (Suc N) then show ?case 

378 
apply (auto simp add: power_Suc_less less_Suc_eq) 

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

380 
apply simp 

381 
apply (rule mult_strict_mono) apply auto 

382 
done 

383 
qed 

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

384 

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

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

388 
proof (induct N) 

389 
case 0 then show ?case by simp 

390 
next 

391 
case (Suc N) then show ?case 

392 
apply (auto simp add: le_Suc_eq) 

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

394 
apply (rule mult_mono) apply auto 

395 
done 

396 
qed 

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

397 

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

398 
lemma power_Suc_less_one: 
30996  399 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1" 
400 
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

401 

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

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

405 
proof (induct N) 

406 
case 0 then show ?case by simp 

407 
next 

408 
case (Suc N) then show ?case 

409 
apply (auto simp add: le_Suc_eq) 

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

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

412 
done 

413 
qed 

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

414 

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

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

416 
lemma power_less_power_Suc: 
30996  417 
"1 < a \<Longrightarrow> a ^ n < a * a ^ n" 
418 
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

419 

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

422 
proof (induct N) 

423 
case 0 then show ?case by simp 

424 
next 

425 
case (Suc N) then show ?case 

426 
apply (auto simp add: power_less_power_Suc less_Suc_eq) 

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

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

429 
done 

430 
qed 

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

431 

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

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

15066  435 

436 
lemma power_strict_increasing_iff [simp]: 

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

438 
by (blast intro: power_less_imp_less_exp power_strict_increasing) 
15066  439 

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

440 
lemma power_le_imp_le_base: 
30996  441 
assumes le: "a ^ Suc n \<le> b ^ Suc n" 
442 
and ynonneg: "0 \<le> b" 

443 
shows "a \<le> b" 

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

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

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

446 
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

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

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

451 
qed 
14577  452 

22853  453 
lemma power_less_imp_less_base: 
454 
assumes less: "a ^ n < b ^ n" 

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

456 
shows "a < b" 

457 
proof (rule contrapos_pp [OF less]) 

458 
assume "~ a < b" 

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

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

30996  461 
thus "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less) 
22853  462 
qed 
463 

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

464 
lemma power_inject_base: 
30996  465 
"a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b" 
466 
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

467 

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

22955  471 

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

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

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

474 
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

475 

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

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

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

478 
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

479 

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

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

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

482 
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

483 

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

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

485 

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

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

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

488 

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

489 
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

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

491 
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

492 

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

493 
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

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

495 
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

496 

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

497 
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

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

499 
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

500 

30996  501 
end 
502 

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

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

505 

30996  506 
lemma power_abs: 
507 
"abs (a ^ n) = abs a ^ n" 

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

509 

510 
lemma abs_power_minus [simp]: 

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

35216  512 
by (simp add: power_abs) 
30996  513 

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

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

517 
case 0 show ?case by simp 

518 
next 

519 
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

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

521 

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

524 
by (rule zero_le_power [OF abs_ge_zero]) 

525 

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

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

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

528 
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

529 

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

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

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

532 
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

533 

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

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

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

536 
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

537 

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

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

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

540 
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

541 

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

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

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

544 
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

545 

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

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

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

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

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

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

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

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

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

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

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

556 
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

557 
qed 
30996  558 

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

559 
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

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

561 
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

562 
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

563 

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

564 
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

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

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

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

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

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

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

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

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

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

574 
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

575 
qed 
30996  576 

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

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

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

579 
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

580 

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

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

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

583 
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

584 

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

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

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

587 
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

588 

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

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

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

591 
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

592 

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

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

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

595 
unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) 
30996  596 

597 
end 

598 

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

599 

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

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

601 

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

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

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

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

605 
by (simp add: algebra_simps power2_eq_square mult_2_right) 
30996  606 

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

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

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

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

610 
by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute) 
30996  611 

612 
lemma power_0_Suc [simp]: 

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

614 
by simp 

30313  615 

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

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

619 
by (induct n) simp_all 

620 

621 
lemma power_eq_0_iff [simp]: 

622 
"a ^ n = 0 \<longleftrightarrow> 

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

624 
by (induct n) 

625 
(auto simp add: no_zero_divisors elim: contrapos_pp) 

626 

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

36409  630 
by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero) 
30313  631 

30996  632 
text{*Perhaps these should be simprules.*} 
633 
lemma power_inverse: 

36409  634 
fixes a :: "'a::division_ring_inverse_zero" 
635 
shows "inverse (a ^ n) = inverse a ^ n" 

30996  636 
apply (cases "a = 0") 
637 
apply (simp add: power_0_left) 

638 
apply (simp add: nonzero_power_inverse) 

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

640 

641 
lemma power_one_over: 

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

645 
lemma power_divide: 

36409  646 
"(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n" 
30996  647 
apply (cases "b = 0") 
648 
apply (simp add: power_0_left) 

649 
apply (rule nonzero_power_divide) 

650 
apply assumption 

30313  651 
done 
652 

653 

30960  654 
subsection {* Exponentiation for the Natural Numbers *} 
14577  655 

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

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

23305  659 

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

662 
by (induct n) auto 

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

663 

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

30056  667 

30996  668 
lemma power_Suc_0 [simp]: 
669 
"Suc 0 ^ n = Suc 0" 

670 
by simp 

30056  671 

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

672 
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

673 
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

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

30996  677 
assumes less: "i ^ m < i ^ n" 
21413  678 
shows "m < n" 
679 
proof (cases "i = 1") 

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

681 
next 

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

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

684 
qed 

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

685 

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

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

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

688 
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

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

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

691 

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

692 

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

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

694 

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

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

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

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

698 

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

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

700 

33364  701 
code_modulename SML 
702 
Power Arith 

703 

704 
code_modulename OCaml 

705 
Power Arith 

706 

707 
code_modulename Haskell 

708 
Power Arith 

709 

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

710 
end 