author  paulson <lp15@cam.ac.uk> 
Mon, 24 Feb 2014 15:45:55 +0000  
changeset 55718  34618f031ba9 
parent 55096  916b2ac758f4 
child 55811  aa1acc25126b 
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 
55096  9 
imports Num Equiv_Relations 
15131  10 
begin 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset

11 

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

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

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

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

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

20 

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

23 

24 
notation (HTML output) 

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

26 

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

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

28 

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

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

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

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

32 

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

33 
notation (latex output) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

35 

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

36 
notation (HTML output) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

38 

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

40 

30996  41 
context monoid_mult 
42 
begin 

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

43 

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

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

45 

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

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

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

49 

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

53 

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 

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

70 
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

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: 
53076  77 
"a ^ (2 * n) = (a ^ n)\<^sup>2" 
47192
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: 
53076  81 
"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

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

83 

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

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

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

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

87 

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

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

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

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

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

92 

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

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

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

97 
next 

98 
case (Suc n) 

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

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

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

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

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

104 
qed 

105 

30996  106 
end 
107 

108 
context comm_monoid_mult 

109 
begin 

110 

111 
lemma power_mult_distrib: 

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

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

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

114 

30996  115 
end 
116 

47191  117 
context semiring_numeral 
118 
begin 

119 

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

121 
by (simp only: sqr_conv_mult numeral_mult) 

122 

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

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

125 
numeral_sqr numeral_mult power_add power_one_right) 

126 

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

128 
by (rule numeral_pow [symmetric]) 

129 

130 
end 

131 

30996  132 
context semiring_1 
133 
begin 

134 

135 
lemma of_nat_power: 

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

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

138 

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

140 
by (simp add: numeral_eq_Suc) 
47191  141 

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

142 
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

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

144 

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

145 
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

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

147 

30996  148 
end 
149 

150 
context comm_semiring_1 

151 
begin 

152 

153 
text {* The divides relation *} 

154 

155 
lemma le_imp_power_dvd: 

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

157 
proof 

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

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

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

161 
by (rule power_add) 

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

163 
qed 

164 

165 
lemma power_le_dvd: 

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

167 
by (rule dvd_trans [OF le_imp_power_dvd]) 

168 

169 
lemma dvd_power_same: 

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

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

172 

173 
lemma dvd_power_le: 

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

175 
by (rule power_le_dvd [OF dvd_power_same]) 

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

176 

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

179 
shows "x dvd (x ^ n)" 

180 
using assms proof 

181 
assume "0 < n" 

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

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

184 
next 

185 
assume "x = 1" 

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

187 
qed 

188 

189 
end 

190 

191 
context ring_1 

192 
begin 

193 

194 
lemma power_minus: 

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

196 
proof (induct n) 

197 
case 0 show ?case by simp 

198 
next 

199 
case (Suc n) then show ?case 

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

201 
qed 

202 

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

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

206 
power_one_right mult_minus_left mult_minus_right minus_minus) 

207 

208 
lemma power_minus_Bit1: 

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

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

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

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

212 
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

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

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

215 

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

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

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

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

219 
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

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

221 
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

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

223 

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

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

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

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

227 

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

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

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

230 
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

231 

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

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

233 

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

234 
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

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

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

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

240 

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

241 
lemma 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

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

243 
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

244 

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

245 
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

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

247 
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

248 

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

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

250 

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

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

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

253 

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

254 
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

255 
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

256 

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

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

258 

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

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

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

261 

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

262 
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

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

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

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

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

267 

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

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

269 

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

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

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

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

275 
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

276 

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

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

278 

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

279 

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

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

281 

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

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

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

284 

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

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

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

287 
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

288 

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

289 
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

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

291 
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

292 

30996  293 
end 
294 

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

295 
context linordered_semidom 
30996  296 
begin 
297 

298 
lemma zero_less_power [simp]: 

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

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

301 

302 
lemma zero_le_power [simp]: 

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

304 
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

305 

47241  306 
lemma power_mono: 
307 
"a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n" 

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

309 

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

311 
using power_mono [of 1 a n] by simp 

312 

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

314 
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

315 

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

316 
lemma power_gt1_lemma: 
30996  317 
assumes gt1: "1 < a" 
318 
shows "1 < a * a ^ n" 

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

319 
proof  
30996  320 
from gt1 have "0 \<le> a" 
321 
by (fact order_trans [OF zero_le_one less_imp_le]) 

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

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

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

14577  325 
zero_le_one order_refl) 
326 
finally show ?thesis by simp 

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

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

328 

30996  329 
lemma power_gt1: 
330 
"1 < a \<Longrightarrow> 1 < a ^ Suc n" 

331 
by (simp add: power_gt1_lemma) 

24376  332 

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

335 
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

336 

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

337 
lemma power_le_imp_le_exp: 
30996  338 
assumes gt1: "1 < a" 
339 
shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n" 

340 
proof (induct m arbitrary: n) 

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

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

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

344 
case (Suc m) 
14577  345 
show ?case 
346 
proof (cases n) 

347 
case 0 

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

30996  351 
not_less [symmetric]) 
14577  352 
next 
353 
case (Suc n) 

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

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

359 

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

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

364 

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

365 
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

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

367 
lemma power_less_imp_less_exp: 
30996  368 
"1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n" 
369 
by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] 

370 
power_le_imp_le_exp) 

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

371 

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

372 
lemma power_strict_mono [rule_format]: 
30996  373 
"a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n" 
374 
by (induct n) 

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

376 

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

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

378 
lemma power_Suc_less: 
30996  379 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n" 
380 
by (induct n) 

381 
(auto simp add: mult_strict_left_mono) 

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

382 

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

385 
proof (induct N) 

386 
case 0 then show ?case by simp 

387 
next 

388 
case (Suc N) then show ?case 

389 
apply (auto simp add: power_Suc_less less_Suc_eq) 

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

391 
apply simp 

392 
apply (rule mult_strict_mono) apply auto 

393 
done 

394 
qed 

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

395 

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

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

399 
proof (induct N) 

400 
case 0 then show ?case by simp 

401 
next 

402 
case (Suc N) then show ?case 

403 
apply (auto simp add: le_Suc_eq) 

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

405 
apply (rule mult_mono) apply auto 

406 
done 

407 
qed 

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

408 

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

409 
lemma power_Suc_less_one: 
30996  410 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1" 
411 
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

412 

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

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

416 
proof (induct N) 

417 
case 0 then show ?case by simp 

418 
next 

419 
case (Suc N) then show ?case 

420 
apply (auto simp add: le_Suc_eq) 

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

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

423 
done 

424 
qed 

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

425 

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

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

427 
lemma power_less_power_Suc: 
30996  428 
"1 < a \<Longrightarrow> a ^ n < a * a ^ n" 
429 
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

430 

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

433 
proof (induct N) 

434 
case 0 then show ?case by simp 

435 
next 

436 
case (Suc N) then show ?case 

437 
apply (auto simp add: power_less_power_Suc less_Suc_eq) 

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

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

440 
done 

441 
qed 

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

442 

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

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

15066  446 

447 
lemma power_strict_increasing_iff [simp]: 

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

449 
by (blast intro: power_less_imp_less_exp power_strict_increasing) 
15066  450 

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

451 
lemma power_le_imp_le_base: 
30996  452 
assumes le: "a ^ Suc n \<le> b ^ Suc n" 
453 
and ynonneg: "0 \<le> b" 

454 
shows "a \<le> b" 

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

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

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

457 
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

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

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

462 
qed 
14577  463 

22853  464 
lemma power_less_imp_less_base: 
465 
assumes less: "a ^ n < b ^ n" 

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

467 
shows "a < b" 

468 
proof (rule contrapos_pp [OF less]) 

469 
assume "~ a < b" 

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

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

30996  472 
thus "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less) 
22853  473 
qed 
474 

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

475 
lemma power_inject_base: 
30996  476 
"a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b" 
477 
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

478 

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

22955  482 

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

483 
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

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

485 
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

486 

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

487 
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

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

489 
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

490 

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

491 
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

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

493 
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

494 

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

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

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

499 

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

500 
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

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

502 
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

503 

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

504 
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

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

506 
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

507 

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

508 
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

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

510 
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

511 

30996  512 
end 
513 

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

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

516 

30996  517 
lemma power_abs: 
518 
"abs (a ^ n) = abs a ^ n" 

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

520 

521 
lemma abs_power_minus [simp]: 

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

35216  523 
by (simp add: power_abs) 
30996  524 

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

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

528 
case 0 show ?case by simp 

529 
next 

530 
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

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

532 

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

535 
by (rule zero_le_power [OF abs_ge_zero]) 

536 

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

537 
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

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

539 
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

540 

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

541 
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

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

543 
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

544 

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

545 
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

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

547 
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

548 

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

549 
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

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

551 
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

552 

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

553 
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

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

555 
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

556 

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

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

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

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

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

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

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

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

564 
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

565 
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

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

567 
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

568 
qed 
30996  569 

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

570 
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

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

572 
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

573 
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

574 

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

575 
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

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

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

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

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

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

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

582 
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

583 
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

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

585 
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

586 
qed 
30996  587 

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

588 
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

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

590 
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

591 

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

592 
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

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

594 
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

595 

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

596 
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

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

598 
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

599 

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

600 
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

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

602 
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

603 

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

604 
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

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

606 
unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) 
30996  607 

608 
end 

609 

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

610 

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

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

612 

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

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

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

615 
shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n" 
34618f031ba9
A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents:
55096
diff
changeset

616 
by (metis gr_implies_not0 le_eq_less_or_eq less_one nat_le_linear power_increasing power_one_right) 
34618f031ba9
A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents:
55096
diff
changeset

617 

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

618 
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

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

620 

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

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

622 
fixes x y :: "'a::comm_semiring_1" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

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

624 
by (simp add: algebra_simps power2_eq_square mult_2_right) 
30996  625 

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

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

627 
fixes x y :: "'a::comm_ring_1" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset

628 
shows "(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

629 
by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute) 
30996  630 

631 
lemma power_0_Suc [simp]: 

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

633 
by simp 

30313  634 

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

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

638 
by (induct n) simp_all 

639 

640 
lemma power_eq_0_iff [simp]: 

641 
"a ^ n = 0 \<longleftrightarrow> 

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

643 
by (induct n) 

644 
(auto simp add: no_zero_divisors elim: contrapos_pp) 

645 

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

36409  649 
by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero) 
30313  650 

30996  651 
text{*Perhaps these should be simprules.*} 
652 
lemma power_inverse: 

36409  653 
fixes a :: "'a::division_ring_inverse_zero" 
654 
shows "inverse (a ^ n) = inverse a ^ n" 

30996  655 
apply (cases "a = 0") 
656 
apply (simp add: power_0_left) 

657 
apply (simp add: nonzero_power_inverse) 

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

659 

660 
lemma power_one_over: 

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

664 
lemma power_divide: 

36409  665 
"(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n" 
30996  666 
apply (cases "b = 0") 
667 
apply (simp add: power_0_left) 

668 
apply (rule nonzero_power_divide) 

669 
apply assumption 

30313  670 
done 
671 

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

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

673 

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

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

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

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

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

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

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

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

681 

30313  682 

30960  683 
subsection {* Exponentiation for the Natural Numbers *} 
14577  684 

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

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

23305  688 

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

691 
by (induct n) auto 

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

692 

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

30056  696 

30996  697 
lemma power_Suc_0 [simp]: 
698 
"Suc 0 ^ n = Suc 0" 

699 
by simp 

30056  700 

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

701 
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

702 
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

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

30996  706 
assumes less: "i ^ m < i ^ n" 
21413  707 
shows "m < n" 
708 
proof (cases "i = 1") 

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

710 
next 

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

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

713 
qed 

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

714 

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

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

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

717 
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

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

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

720 

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

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

722 
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

723 
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

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

725 

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

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

727 
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

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

729 
shows "m \<le> n" 
54249  730 
proof (cases m) 
731 
case 0 then show ?thesis by simp 

732 
next 

733 
case (Suc k) 

734 
show ?thesis 

735 
proof (rule ccontr) 

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

737 
then have "n < m" by simp 

738 
with assms Suc show False 

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

740 
qed 

741 
qed 

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

742 

55096  743 
subsubsection {* Cardinality of the Powerset *} 
744 

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

746 
unfolding UNIV_bool by simp 

747 

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

749 
proof (induct rule: finite_induct) 

750 
case empty 

751 
show ?case by auto 

752 
next 

753 
case (insert x A) 

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

755 
unfolding inj_on_def by (blast elim!: equalityE) 

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

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

758 
then show ?case using insert 

759 
apply (simp add: Pow_insert) 

760 
apply (subst card_Un_disjoint, auto) 

761 
done 

762 
qed 

763 

764 
subsubsection {* Generalized product over a set *} 

765 

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

767 
apply (erule finite_induct) 

768 
apply auto 

769 
done 

770 

771 
lemma setprod_gen_delta: 

772 
assumes fS: "finite S" 

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

774 
proof 

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

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

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

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

779 
moreover 

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

781 
let ?A = "S  {a}" 

782 
let ?B = "{a}" 

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

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

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

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

787 
apply (rule setprod_cong) by auto 

788 
have cA: "card ?A = card S  1" using fS a by auto 

789 
have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto 

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

791 
using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] 

792 
by simp 

793 
then have ?thesis using a cA 

794 
by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)} 

795 
ultimately show ?thesis by blast 

796 
qed 

797 

798 
lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)" 

799 
by auto 

800 

801 
lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)" 

802 
by auto 

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

803 

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

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

805 

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

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

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

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

809 

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

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

811 

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

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

813 
code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 
33364  814 

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

815 
end 
49824  816 