73 done |
76 done |
74 |
77 |
75 lemma even_neg: "even (-(x::int)) = even x" |
78 lemma even_neg: "even (-(x::int)) = even x" |
76 by (auto simp add: even_def zmod_zminus1_eq_if) |
79 by (auto simp add: even_def zmod_zminus1_eq_if) |
77 |
80 |
78 lemma even_difference: |
81 lemma even_difference: |
79 "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))" |
82 "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))" |
80 by (simp only: diff_minus even_sum even_neg) |
83 by (simp only: diff_minus even_sum even_neg) |
81 |
84 |
82 lemma even_pow_gt_zero [rule_format]: |
85 lemma even_pow_gt_zero: |
83 "even (x::int) ==> 0 < n --> even (x^n)" |
86 "even (x::int) ==> 0 < n ==> even (x^n)" |
84 apply (induct n) |
87 by (induct n) (auto simp add: even_product) |
85 apply (auto simp add: even_product) |
|
86 done |
|
87 |
88 |
88 lemma odd_pow: "odd x ==> odd((x::int)^n)" |
89 lemma odd_pow: "odd x ==> odd((x::int)^n)" |
89 apply (induct n) |
90 apply (induct n) |
90 apply (simp add: even_def) |
91 apply (simp add: even_def) |
91 apply (simp add: even_product) |
92 apply (simp add: even_product) |
92 done |
93 done |
93 |
94 |
94 lemma even_power: "even ((x::int)^n) = (even x & 0 < n)" |
95 lemma even_power: "even ((x::int)^n) = (even x & 0 < n)" |
95 apply (auto simp add: even_pow_gt_zero) |
96 apply (auto simp add: even_pow_gt_zero) |
96 apply (erule contrapos_pp, erule odd_pow) |
97 apply (erule contrapos_pp, erule odd_pow) |
97 apply (erule contrapos_pp, simp add: even_def) |
98 apply (erule contrapos_pp, simp add: even_def) |
98 done |
99 done |
99 |
100 |
100 lemma even_zero: "even (0::int)" |
101 lemma even_zero: "even (0::int)" |
101 by (simp add: even_def) |
102 by (simp add: even_def) |
102 |
103 |
103 lemma odd_one: "odd (1::int)" |
104 lemma odd_one: "odd (1::int)" |
104 by (simp add: even_def) |
105 by (simp add: even_def) |
105 |
106 |
106 lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero |
107 lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero |
107 odd_one even_product even_sum even_neg even_difference even_power |
108 odd_one even_product even_sum even_neg even_difference even_power |
108 |
109 |
109 |
110 |
110 subsection {* Equivalent definitions *} |
111 subsection {* Equivalent definitions *} |
111 |
112 |
112 lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x" |
113 lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x" |
113 by (auto simp add: even_def) |
114 by (auto simp add: even_def) |
114 |
115 |
115 lemma two_times_odd_div_two_plus_one: "odd (x::int) ==> |
116 lemma two_times_odd_div_two_plus_one: "odd (x::int) ==> |
116 2 * (x div 2) + 1 = x" |
117 2 * (x div 2) + 1 = x" |
117 apply (insert zmod_zdiv_equality [of x 2, THEN sym]) |
118 apply (insert zmod_zdiv_equality [of x 2, symmetric]) |
118 by (simp add: even_def) |
119 apply (simp add: even_def) |
|
120 done |
119 |
121 |
120 lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)" |
122 lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)" |
121 apply auto |
123 apply auto |
122 apply (rule exI) |
124 apply (rule exI) |
123 by (erule two_times_even_div_two [THEN sym]) |
125 apply (erule two_times_even_div_two [symmetric]) |
|
126 done |
124 |
127 |
125 lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)" |
128 lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)" |
126 apply auto |
129 apply auto |
127 apply (rule exI) |
130 apply (rule exI) |
128 by (erule two_times_odd_div_two_plus_one [THEN sym]) |
131 apply (erule two_times_odd_div_two_plus_one [symmetric]) |
|
132 done |
129 |
133 |
130 |
134 |
131 subsection {* even and odd for nats *} |
135 subsection {* even and odd for nats *} |
132 |
136 |
133 lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)" |
137 lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)" |
134 by (simp add: even_nat_def) |
138 by (simp add: even_nat_def) |
135 |
139 |
136 lemma even_nat_product: "even((x::nat) * y) = (even x | even y)" |
140 lemma even_nat_product: "even((x::nat) * y) = (even x | even y)" |
137 by (simp add: even_nat_def int_mult) |
141 by (simp add: even_nat_def int_mult) |
138 |
142 |
139 lemma even_nat_sum: "even ((x::nat) + y) = |
143 lemma even_nat_sum: "even ((x::nat) + y) = |
140 ((even x & even y) | (odd x & odd y))" |
144 ((even x & even y) | (odd x & odd y))" |
141 by (unfold even_nat_def, simp) |
145 by (unfold even_nat_def, simp) |
142 |
146 |
143 lemma even_nat_difference: |
147 lemma even_nat_difference: |
144 "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))" |
148 "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))" |
145 apply (auto simp add: even_nat_def zdiff_int [THEN sym]) |
149 apply (auto simp add: even_nat_def zdiff_int [symmetric]) |
146 apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym]) |
150 apply (case_tac "x < y", auto simp add: zdiff_int [symmetric]) |
147 apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym]) |
151 apply (case_tac "x < y", auto simp add: zdiff_int [symmetric]) |
148 done |
152 done |
149 |
153 |
150 lemma even_nat_Suc: "even (Suc x) = odd x" |
154 lemma even_nat_Suc: "even (Suc x) = odd x" |
151 by (simp add: even_nat_def) |
155 by (simp add: even_nat_def) |
152 |
156 |
154 by (simp add: even_nat_def int_power) |
158 by (simp add: even_nat_def int_power) |
155 |
159 |
156 lemma even_nat_zero: "even (0::nat)" |
160 lemma even_nat_zero: "even (0::nat)" |
157 by (simp add: even_nat_def) |
161 by (simp add: even_nat_def) |
158 |
162 |
159 lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] |
163 lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] |
160 even_nat_zero even_nat_Suc even_nat_product even_nat_sum even_nat_power |
164 even_nat_zero even_nat_Suc even_nat_product even_nat_sum even_nat_power |
161 |
165 |
162 |
166 |
163 subsection {* Equivalent definitions *} |
167 subsection {* Equivalent definitions *} |
164 |
168 |
165 lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==> |
169 lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==> |
166 x = 0 | x = Suc 0" |
170 x = 0 | x = Suc 0" |
167 by auto |
171 by auto |
168 |
172 |
169 lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0" |
173 lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0" |
170 apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) |
174 apply (insert mod_div_equality [of x "Suc (Suc 0)", symmetric]) |
171 apply (drule subst, assumption) |
175 apply (drule subst, assumption) |
172 apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0") |
176 apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0") |
173 apply force |
177 apply force |
174 apply (subgoal_tac "0 < Suc (Suc 0)") |
178 apply (subgoal_tac "0 < Suc (Suc 0)") |
175 apply (frule mod_less_divisor [of "Suc (Suc 0)" x]) |
179 apply (frule mod_less_divisor [of "Suc (Suc 0)" x]) |
176 apply (erule nat_lt_two_imp_zero_or_one, auto) |
180 apply (erule nat_lt_two_imp_zero_or_one, auto) |
177 done |
181 done |
178 |
182 |
179 lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0" |
183 lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0" |
180 apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) |
184 apply (insert mod_div_equality [of x "Suc (Suc 0)", symmetric]) |
181 apply (drule subst, assumption) |
185 apply (drule subst, assumption) |
182 apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0") |
186 apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0") |
183 apply force |
187 apply force |
184 apply (subgoal_tac "0 < Suc (Suc 0)") |
188 apply (subgoal_tac "0 < Suc (Suc 0)") |
185 apply (frule mod_less_divisor [of "Suc (Suc 0)" x]) |
189 apply (frule mod_less_divisor [of "Suc (Suc 0)" x]) |
186 apply (erule nat_lt_two_imp_zero_or_one, auto) |
190 apply (erule nat_lt_two_imp_zero_or_one, auto) |
187 done |
191 done |
188 |
192 |
189 lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" |
193 lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" |
190 apply (rule iffI) |
194 apply (rule iffI) |
191 apply (erule even_nat_mod_two_eq_zero) |
195 apply (erule even_nat_mod_two_eq_zero) |
192 apply (insert odd_nat_mod_two_eq_one [of x], auto) |
196 apply (insert odd_nat_mod_two_eq_one [of x], auto) |
193 done |
197 done |
194 |
198 |
196 apply (auto simp add: even_nat_equiv_def) |
200 apply (auto simp add: even_nat_equiv_def) |
197 apply (subgoal_tac "x mod (Suc (Suc 0)) < Suc (Suc 0)") |
201 apply (subgoal_tac "x mod (Suc (Suc 0)) < Suc (Suc 0)") |
198 apply (frule nat_lt_two_imp_zero_or_one, auto) |
202 apply (frule nat_lt_two_imp_zero_or_one, auto) |
199 done |
203 done |
200 |
204 |
201 lemma even_nat_div_two_times_two: "even (x::nat) ==> |
205 lemma even_nat_div_two_times_two: "even (x::nat) ==> |
202 Suc (Suc 0) * (x div Suc (Suc 0)) = x" |
206 Suc (Suc 0) * (x div Suc (Suc 0)) = x" |
203 apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) |
207 apply (insert mod_div_equality [of x "Suc (Suc 0)", symmetric]) |
204 apply (drule even_nat_mod_two_eq_zero, simp) |
208 apply (drule even_nat_mod_two_eq_zero, simp) |
205 done |
209 done |
206 |
210 |
207 lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> |
211 lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> |
208 Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" |
212 Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" |
209 apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) |
213 apply (insert mod_div_equality [of x "Suc (Suc 0)", symmetric]) |
210 apply (drule odd_nat_mod_two_eq_one, simp) |
214 apply (drule odd_nat_mod_two_eq_one, simp) |
211 done |
215 done |
212 |
216 |
213 lemma even_nat_equiv_def2: "even (x::nat) = (EX y. x = Suc (Suc 0) * y)" |
217 lemma even_nat_equiv_def2: "even (x::nat) = (EX y. x = Suc (Suc 0) * y)" |
214 apply (rule iffI, rule exI) |
218 apply (rule iffI, rule exI) |
215 apply (erule even_nat_div_two_times_two [THEN sym], auto) |
219 apply (erule even_nat_div_two_times_two [symmetric], auto) |
216 done |
220 done |
217 |
221 |
218 lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))" |
222 lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))" |
219 apply (rule iffI, rule exI) |
223 apply (rule iffI, rule exI) |
220 apply (erule odd_nat_div_two_times_two_plus_one [THEN sym], auto) |
224 apply (erule odd_nat_div_two_times_two_plus_one [symmetric], auto) |
221 done |
225 done |
222 |
226 |
223 subsection {* Parity and powers *} |
227 subsection {* Parity and powers *} |
224 |
228 |
225 lemma minus_one_even_odd_power: |
229 lemma minus_one_even_odd_power: |
226 "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) & |
230 "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) & |
227 (odd x --> (- 1::'a)^x = - 1)" |
231 (odd x --> (- 1::'a)^x = - 1)" |
228 apply (induct x) |
232 apply (induct x) |
229 apply (rule conjI) |
233 apply (rule conjI) |
230 apply simp |
234 apply simp |
231 apply (insert even_nat_zero, blast) |
235 apply (insert even_nat_zero, blast) |
232 apply (simp add: power_Suc) |
236 apply (simp add: power_Suc) |
233 done |
237 done |
234 |
238 |
235 lemma minus_one_even_power [simp]: |
239 lemma minus_one_even_power [simp]: |
236 "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1" |
240 "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1" |
237 by (rule minus_one_even_odd_power [THEN conjunct1, THEN mp], assumption) |
241 using minus_one_even_odd_power by blast |
238 |
242 |
239 lemma minus_one_odd_power [simp]: |
243 lemma minus_one_odd_power [simp]: |
240 "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1" |
244 "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1" |
241 by (rule minus_one_even_odd_power [THEN conjunct2, THEN mp], assumption) |
245 using minus_one_even_odd_power by blast |
242 |
246 |
243 lemma neg_one_even_odd_power: |
247 lemma neg_one_even_odd_power: |
244 "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & |
248 "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & |
245 (odd x --> (-1::'a)^x = -1)" |
249 (odd x --> (-1::'a)^x = -1)" |
246 apply (induct x) |
250 apply (induct x) |
247 apply (simp, simp add: power_Suc) |
251 apply (simp, simp add: power_Suc) |
248 done |
252 done |
249 |
253 |
250 lemma neg_one_even_power [simp]: |
254 lemma neg_one_even_power [simp]: |
251 "even x ==> (-1::'a::{number_ring,recpower})^x = 1" |
255 "even x ==> (-1::'a::{number_ring,recpower})^x = 1" |
252 by (rule neg_one_even_odd_power [THEN conjunct1, THEN mp], assumption) |
256 using neg_one_even_odd_power by blast |
253 |
257 |
254 lemma neg_one_odd_power [simp]: |
258 lemma neg_one_odd_power [simp]: |
255 "odd x ==> (-1::'a::{number_ring,recpower})^x = -1" |
259 "odd x ==> (-1::'a::{number_ring,recpower})^x = -1" |
256 by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption) |
260 using neg_one_even_odd_power by blast |
257 |
261 |
258 lemma neg_power_if: |
262 lemma neg_power_if: |
259 "(-x::'a::{comm_ring_1,recpower}) ^ n = |
263 "(-x::'a::{comm_ring_1,recpower}) ^ n = |
260 (if even n then (x ^ n) else -(x ^ n))" |
264 (if even n then (x ^ n) else -(x ^ n))" |
261 by (induct n, simp_all split: split_if_asm add: power_Suc) |
265 apply (induct n) |
262 |
266 apply (simp_all split: split_if_asm add: power_Suc) |
263 lemma zero_le_even_power: "even n ==> |
267 done |
|
268 |
|
269 lemma zero_le_even_power: "even n ==> |
264 0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n" |
270 0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n" |
265 apply (simp add: even_nat_equiv_def2) |
271 apply (simp add: even_nat_equiv_def2) |
266 apply (erule exE) |
272 apply (erule exE) |
267 apply (erule ssubst) |
273 apply (erule ssubst) |
268 apply (subst power_add) |
274 apply (subst power_add) |
269 apply (rule zero_le_square) |
275 apply (rule zero_le_square) |
270 done |
276 done |
271 |
277 |
272 lemma zero_le_odd_power: "odd n ==> |
278 lemma zero_le_odd_power: "odd n ==> |
273 (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)" |
279 (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)" |
274 apply (simp add: odd_nat_equiv_def2) |
280 apply (simp add: odd_nat_equiv_def2) |
275 apply (erule exE) |
281 apply (erule exE) |
276 apply (erule ssubst) |
282 apply (erule ssubst) |
277 apply (subst power_Suc) |
283 apply (subst power_Suc) |
278 apply (subst power_add) |
284 apply (subst power_add) |
279 apply (subst zero_le_mult_iff) |
285 apply (subst zero_le_mult_iff) |
280 apply auto |
286 apply auto |
281 apply (subgoal_tac "x = 0 & 0 < y") |
287 apply (subgoal_tac "x = 0 & 0 < y") |
282 apply (erule conjE, assumption) |
288 apply (erule conjE, assumption) |
283 apply (subst power_eq_0_iff [THEN sym]) |
289 apply (subst power_eq_0_iff [symmetric]) |
284 apply (subgoal_tac "0 <= x^y * x^y") |
290 apply (subgoal_tac "0 <= x^y * x^y") |
285 apply simp |
291 apply simp |
286 apply (rule zero_le_square)+ |
292 apply (rule zero_le_square)+ |
287 done |
293 done |
288 |
294 |
289 lemma zero_le_power_eq: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = |
295 lemma zero_le_power_eq: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = |
290 (even n | (odd n & 0 <= x))" |
296 (even n | (odd n & 0 <= x))" |
291 apply auto |
297 apply auto |
292 apply (subst zero_le_odd_power [THEN sym]) |
298 apply (subst zero_le_odd_power [symmetric]) |
293 apply assumption+ |
299 apply assumption+ |
294 apply (erule zero_le_even_power) |
300 apply (erule zero_le_even_power) |
295 apply (subst zero_le_odd_power) |
301 apply (subst zero_le_odd_power) |
296 apply assumption+ |
302 apply assumption+ |
297 done |
303 done |
298 |
304 |
299 lemma zero_less_power_eq: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = |
305 lemma zero_less_power_eq: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = |
300 (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))" |
306 (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))" |
301 apply (rule iffI) |
307 apply (rule iffI) |
302 apply clarsimp |
308 apply clarsimp |
303 apply (rule conjI) |
309 apply (rule conjI) |
304 apply clarsimp |
310 apply clarsimp |
305 apply (rule ccontr) |
311 apply (rule ccontr) |
306 apply (subgoal_tac "~ (0 <= x^n)") |
312 apply (subgoal_tac "~ (0 <= x^n)") |
307 apply simp |
313 apply simp |
308 apply (subst zero_le_odd_power) |
314 apply (subst zero_le_odd_power) |
309 apply assumption |
315 apply assumption |
310 apply simp |
316 apply simp |
311 apply (rule notI) |
317 apply (rule notI) |
312 apply (simp add: power_0_left) |
318 apply (simp add: power_0_left) |
313 apply (rule notI) |
319 apply (rule notI) |
314 apply (simp add: power_0_left) |
320 apply (simp add: power_0_left) |
321 apply (frule order_le_imp_less_or_eq) |
327 apply (frule order_le_imp_less_or_eq) |
322 apply auto |
328 apply auto |
323 apply (subst zero_le_odd_power) |
329 apply (subst zero_le_odd_power) |
324 apply assumption |
330 apply assumption |
325 apply (erule order_less_imp_le) |
331 apply (erule order_less_imp_le) |
326 done |
332 done |
327 |
333 |
328 lemma power_less_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n < 0) = |
334 lemma power_less_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n < 0) = |
329 (odd n & x < 0)" |
335 (odd n & x < 0)" |
330 apply (subst linorder_not_le [THEN sym])+ |
336 apply (subst linorder_not_le [symmetric])+ |
331 apply (subst zero_le_power_eq) |
337 apply (subst zero_le_power_eq) |
332 apply auto |
338 apply auto |
333 done |
339 done |
334 |
340 |
335 lemma power_le_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) = |
341 lemma power_le_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) = |
336 (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))" |
342 (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))" |
337 apply (subst linorder_not_less [THEN sym])+ |
343 apply (subst linorder_not_less [symmetric])+ |
338 apply (subst zero_less_power_eq) |
344 apply (subst zero_less_power_eq) |
339 apply auto |
345 apply auto |
340 done |
346 done |
341 |
347 |
342 lemma power_even_abs: "even n ==> |
348 lemma power_even_abs: "even n ==> |
343 (abs (x::'a::{recpower,ordered_idom}))^n = x^n" |
349 (abs (x::'a::{recpower,ordered_idom}))^n = x^n" |
344 apply (subst power_abs [THEN sym]) |
350 apply (subst power_abs [symmetric]) |
345 apply (simp add: zero_le_even_power) |
351 apply (simp add: zero_le_even_power) |
346 done |
352 done |
347 |
353 |
348 lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)" |
354 lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)" |
349 by (induct n, auto) |
355 by (induct n) auto |
350 |
356 |
351 lemma power_minus_even [simp]: "even n ==> |
357 lemma power_minus_even [simp]: "even n ==> |
352 (- x)^n = (x^n::'a::{recpower,comm_ring_1})" |
358 (- x)^n = (x^n::'a::{recpower,comm_ring_1})" |
353 apply (subst power_minus) |
359 apply (subst power_minus) |
354 apply simp |
360 apply simp |
355 done |
361 done |
356 |
362 |
357 lemma power_minus_odd [simp]: "odd n ==> |
363 lemma power_minus_odd [simp]: "odd n ==> |
358 (- x)^n = - (x^n::'a::{recpower,comm_ring_1})" |
364 (- x)^n = - (x^n::'a::{recpower,comm_ring_1})" |
359 apply (subst power_minus) |
365 apply (subst power_minus) |
360 apply simp |
366 apply simp |
361 done |
367 done |
362 |
368 |
363 (* Simplify, when the exponent is a numeral *) |
369 |
|
370 text {* Simplify, when the exponent is a numeral *} |
364 |
371 |
365 lemmas power_0_left_number_of = power_0_left [of "number_of w", standard] |
372 lemmas power_0_left_number_of = power_0_left [of "number_of w", standard] |
366 declare power_0_left_number_of [simp] |
373 declare power_0_left_number_of [simp] |
367 |
374 |
368 lemmas zero_le_power_eq_number_of = |
375 lemmas zero_le_power_eq_number_of [simp] = |
369 zero_le_power_eq [of _ "number_of w", standard] |
376 zero_le_power_eq [of _ "number_of w", standard] |
370 declare zero_le_power_eq_number_of [simp] |
377 |
371 |
378 lemmas zero_less_power_eq_number_of [simp] = |
372 lemmas zero_less_power_eq_number_of = |
|
373 zero_less_power_eq [of _ "number_of w", standard] |
379 zero_less_power_eq [of _ "number_of w", standard] |
374 declare zero_less_power_eq_number_of [simp] |
380 |
375 |
381 lemmas power_le_zero_eq_number_of [simp] = |
376 lemmas power_le_zero_eq_number_of = |
|
377 power_le_zero_eq [of _ "number_of w", standard] |
382 power_le_zero_eq [of _ "number_of w", standard] |
378 declare power_le_zero_eq_number_of [simp] |
383 |
379 |
384 lemmas power_less_zero_eq_number_of [simp] = |
380 lemmas power_less_zero_eq_number_of = |
|
381 power_less_zero_eq [of _ "number_of w", standard] |
385 power_less_zero_eq [of _ "number_of w", standard] |
382 declare power_less_zero_eq_number_of [simp] |
386 |
383 |
387 lemmas zero_less_power_nat_eq_number_of [simp] = |
384 lemmas zero_less_power_nat_eq_number_of = |
|
385 zero_less_power_nat_eq [of _ "number_of w", standard] |
388 zero_less_power_nat_eq [of _ "number_of w", standard] |
386 declare zero_less_power_nat_eq_number_of [simp] |
389 |
387 |
390 lemmas power_eq_0_iff_number_of [simp] = power_eq_0_iff [of _ "number_of w", standard] |
388 lemmas power_eq_0_iff_number_of = power_eq_0_iff [of _ "number_of w", standard] |
391 |
389 declare power_eq_0_iff_number_of [simp] |
392 lemmas power_even_abs_number_of [simp] = power_even_abs [of "number_of w" _, standard] |
390 |
|
391 lemmas power_even_abs_number_of = power_even_abs [of "number_of w" _, standard] |
|
392 declare power_even_abs_number_of [simp] |
|
393 |
393 |
394 |
394 |
395 subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *} |
395 subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *} |
396 |
396 |
397 lemma even_power_le_0_imp_0: |
397 lemma even_power_le_0_imp_0: |
398 "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0" |
398 "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0" |
399 apply (induct k) |
399 by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) |
400 apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) |
|
401 done |
|
402 |
400 |
403 lemma zero_le_power_iff: |
401 lemma zero_le_power_iff: |
404 "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,recpower}) | even n)" |
402 "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,recpower}) | even n)" |
405 (is "?P n") |
|
406 proof cases |
403 proof cases |
407 assume even: "even n" |
404 assume even: "even n" |
408 then obtain k where "n = 2*k" |
405 then obtain k where "n = 2*k" |
409 by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2) |
406 by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2) |
410 thus ?thesis by (simp add: zero_le_even_power even) |
407 thus ?thesis by (simp add: zero_le_even_power even) |
411 next |
408 next |
412 assume odd: "odd n" |
409 assume odd: "odd n" |
413 then obtain k where "n = Suc(2*k)" |
410 then obtain k where "n = Suc(2*k)" |
414 by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2) |
411 by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2) |
415 thus ?thesis |
412 thus ?thesis |
416 by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power |
413 by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power |
417 dest!: even_power_le_0_imp_0) |
414 dest!: even_power_le_0_imp_0) |
418 qed |
415 qed |
|
416 |
419 |
417 |
420 subsection {* Miscellaneous *} |
418 subsection {* Miscellaneous *} |
421 |
419 |
422 lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2" |
420 lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2" |
423 apply (subst zdiv_zadd1_eq) |
421 apply (subst zdiv_zadd1_eq) |