39 lemma neq_one_mod_two [simp, presburger]: |
39 lemma neq_one_mod_two [simp, presburger]: |
40 "((x::int) mod 2 ~= 0) = (x mod 2 = 1)" by presburger |
40 "((x::int) mod 2 ~= 0) = (x mod 2 = 1)" by presburger |
41 |
41 |
42 |
42 |
43 subsection {* Behavior under integer arithmetic operations *} |
43 subsection {* Behavior under integer arithmetic operations *} |
|
44 declare dvd_def[algebra] |
|
45 lemma nat_even_iff_2_dvd[algebra]: "even (x::nat) \<longleftrightarrow> 2 dvd x" |
|
46 by (presburger add: even_nat_def even_def) |
|
47 lemma int_even_iff_2_dvd[algebra]: "even (x::int) \<longleftrightarrow> 2 dvd x" |
|
48 by presburger |
44 |
49 |
45 lemma even_times_anything: "even (x::int) ==> even (x * y)" |
50 lemma even_times_anything: "even (x::int) ==> even (x * y)" |
46 by (simp add: even_def zmod_zmult1_eq') |
51 by algebra |
47 |
52 |
48 lemma anything_times_even: "even (y::int) ==> even (x * y)" |
53 lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra |
49 by (simp add: even_def zmod_zmult1_eq) |
54 |
50 |
55 lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" |
51 lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" |
|
52 by (simp add: even_def zmod_zmult1_eq) |
56 by (simp add: even_def zmod_zmult1_eq) |
53 |
57 |
54 lemma even_product[presburger]: "even((x::int) * y) = (even x | even y)" |
58 lemma even_product[presburger]: "even((x::int) * y) = (even x | even y)" |
55 apply (auto simp add: even_times_anything anything_times_even) |
59 apply (auto simp add: even_times_anything anything_times_even) |
56 apply (rule ccontr) |
60 apply (rule ccontr) |
69 lemma odd_plus_odd: "odd (x::int) ==> odd y ==> even (x + y)" by presburger |
73 lemma odd_plus_odd: "odd (x::int) ==> odd y ==> even (x + y)" by presburger |
70 |
74 |
71 lemma even_sum[presburger]: "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))" |
75 lemma even_sum[presburger]: "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))" |
72 by presburger |
76 by presburger |
73 |
77 |
74 lemma even_neg[presburger]: "even (-(x::int)) = even x" by presburger |
78 lemma even_neg[presburger, algebra]: "even (-(x::int)) = even x" by presburger |
75 |
79 |
76 lemma even_difference: |
80 lemma even_difference: |
77 "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))" by presburger |
81 "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))" by presburger |
78 |
82 |
79 lemma even_pow_gt_zero: |
83 lemma even_pow_gt_zero: |
80 "even (x::int) ==> 0 < n ==> even (x^n)" |
84 "even (x::int) ==> 0 < n ==> even (x^n)" |
81 by (induct n) (auto simp add: even_product) |
85 by (induct n) (auto simp add: even_product) |
82 |
86 |
83 lemma odd_pow_iff[presburger]: "odd ((x::int) ^ n) \<longleftrightarrow> (n = 0 \<or> odd x)" |
87 lemma odd_pow_iff[presburger, algebra]: |
|
88 "odd ((x::int) ^ n) \<longleftrightarrow> (n = 0 \<or> odd x)" |
84 apply (induct n, simp_all) |
89 apply (induct n, simp_all) |
85 apply presburger |
90 apply presburger |
86 apply (case_tac n, auto) |
91 apply (case_tac n, auto) |
87 apply (simp_all add: even_product) |
92 apply (simp_all add: even_product) |
88 done |
93 done |
118 subsection {* even and odd for nats *} |
123 subsection {* even and odd for nats *} |
119 |
124 |
120 lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)" |
125 lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)" |
121 by (simp add: even_nat_def) |
126 by (simp add: even_nat_def) |
122 |
127 |
123 lemma even_nat_product[presburger]: "even((x::nat) * y) = (even x | even y)" |
128 lemma even_nat_product[presburger, algebra]: "even((x::nat) * y) = (even x | even y)" |
124 by (simp add: even_nat_def int_mult) |
129 by (simp add: even_nat_def int_mult) |
125 |
130 |
126 lemma even_nat_sum[presburger]: "even ((x::nat) + y) = |
131 lemma even_nat_sum[presburger, algebra]: "even ((x::nat) + y) = |
127 ((even x & even y) | (odd x & odd y))" by presburger |
132 ((even x & even y) | (odd x & odd y))" by presburger |
128 |
133 |
129 lemma even_nat_difference[presburger]: |
134 lemma even_nat_difference[presburger, algebra]: |
130 "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))" |
135 "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))" |
131 by presburger |
136 by presburger |
132 |
137 |
133 lemma even_nat_Suc[presburger]: "even (Suc x) = odd x" by presburger |
138 lemma even_nat_Suc[presburger, algebra]: "even (Suc x) = odd x" by presburger |
134 |
139 |
135 lemma even_nat_power[presburger]: "even ((x::nat)^y) = (even x & 0 < y)" |
140 lemma even_nat_power[presburger, algebra]: "even ((x::nat)^y) = (even x & 0 < y)" |
136 by (simp add: even_nat_def int_power) |
141 by (simp add: even_nat_def int_power) |
137 |
142 |
138 lemma even_nat_zero[presburger]: "even (0::nat)" by presburger |
143 lemma even_nat_zero[presburger]: "even (0::nat)" by presburger |
139 |
144 |
140 lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] |
145 lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] |
247 apply (erule zero_le_even_power) |
252 apply (erule zero_le_even_power) |
248 done |
253 done |
249 |
254 |
250 lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = |
255 lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = |
251 (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))" |
256 (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))" |
252 apply (rule iffI) |
257 |
253 apply clarsimp |
258 unfolding order_less_le zero_le_power_eq by auto |
254 apply (rule conjI) |
|
255 apply clarsimp |
|
256 apply (rule ccontr) |
|
257 apply (subgoal_tac "~ (0 <= x^n)") |
|
258 apply simp |
|
259 apply (subst zero_le_odd_power) |
|
260 apply assumption |
|
261 apply simp |
|
262 apply (rule notI) |
|
263 apply (simp add: power_0_left) |
|
264 apply (rule notI) |
|
265 apply (simp add: power_0_left) |
|
266 apply auto |
|
267 apply (subgoal_tac "0 <= x^n") |
|
268 apply (frule order_le_imp_less_or_eq) |
|
269 apply simp |
|
270 apply (erule zero_le_even_power) |
|
271 done |
|
272 |
259 |
273 lemma power_less_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n < 0) = |
260 lemma power_less_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n < 0) = |
274 (odd n & x < 0)" |
261 (odd n & x < 0)" |
275 apply (subst linorder_not_le [symmetric])+ |
262 apply (subst linorder_not_le [symmetric])+ |
276 apply (subst zero_le_power_eq) |
263 apply (subst zero_le_power_eq) |
277 apply auto |
264 apply auto |
278 done |
265 done |
279 |
266 |
340 done |
328 done |
341 |
329 |
342 |
330 |
343 subsection {* More Even/Odd Results *} |
331 subsection {* More Even/Odd Results *} |
344 |
332 |
345 lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)" |
333 lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)" by presburger |
346 by (simp add: even_nat_equiv_def2 numeral_2_eq_2) |
334 lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))" by presburger |
347 |
335 lemma even_add [simp]: "even(m + n::nat) = (even m = even n)" by presburger |
348 lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))" |
336 |
349 by (simp add: odd_nat_equiv_def2 numeral_2_eq_2) |
337 lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)" by presburger |
350 |
|
351 lemma even_add [simp]: "even(m + n::nat) = (even m = even n)" |
|
352 by auto |
|
353 |
|
354 lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)" |
|
355 by auto |
|
356 |
338 |
357 lemma div_Suc: "Suc a div c = a div c + Suc 0 div c + |
339 lemma div_Suc: "Suc a div c = a div c + Suc 0 div c + |
358 (a mod c + Suc 0 mod c) div c" |
340 (a mod c + Suc 0 mod c) div c" |
359 apply (subgoal_tac "Suc a = a + Suc 0") |
341 apply (subgoal_tac "Suc a = a + Suc 0") |
360 apply (erule ssubst) |
342 apply (erule ssubst) |
361 apply (rule div_add1_eq, simp) |
343 apply (rule div_add1_eq, simp) |
362 done |
344 done |
363 |
345 |
364 lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" |
346 lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger |
365 apply (simp add: numeral_2_eq_2) |
|
366 apply (subst div_Suc) |
|
367 apply (simp add: even_nat_mod_two_eq_zero) |
|
368 done |
|
369 |
347 |
370 lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)" |
348 lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)" |
371 apply (simp add: numeral_2_eq_2) |
349 by presburger |
372 apply (subst div_Suc) |
350 |
373 apply (simp add: odd_nat_mod_two_eq_one) |
351 lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))" by presburger |
374 done |
352 lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" by presburger |
375 |
353 |
376 lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))" |
354 lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)" by presburger |
377 by (case_tac "n", auto) |
|
378 |
|
379 lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" |
|
380 apply (induct n, simp) |
|
381 apply (subst mod_Suc, simp) |
|
382 done |
|
383 |
|
384 lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)" |
|
385 apply (rule mod_div_equality [of n 4, THEN subst]) |
|
386 apply (simp add: even_num_iff) |
|
387 done |
|
388 |
355 |
389 lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)" |
356 lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)" |
390 apply (rule mod_div_equality [of n 4, THEN subst]) |
357 by presburger |
391 apply simp |
|
392 done |
|
393 |
358 |
394 text {* Simplify, when the exponent is a numeral *} |
359 text {* Simplify, when the exponent is a numeral *} |
395 |
360 |
396 lemmas power_0_left_number_of = power_0_left [of "number_of w", standard] |
361 lemmas power_0_left_number_of = power_0_left [of "number_of w", standard] |
397 declare power_0_left_number_of [simp] |
362 declare power_0_left_number_of [simp] |
439 qed |
404 qed |
440 |
405 |
441 |
406 |
442 subsection {* Miscellaneous *} |
407 subsection {* Miscellaneous *} |
443 |
408 |
444 lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" |
409 lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger |
445 by (cases n, simp_all) |
|
446 |
410 |
447 lemma [presburger]:"(x + 1) div 2 = x div 2 \<longleftrightarrow> even (x::int)" by presburger |
411 lemma [presburger]:"(x + 1) div 2 = x div 2 \<longleftrightarrow> even (x::int)" by presburger |
448 lemma [presburger]: "(x + 1) div 2 = x div 2 + 1 \<longleftrightarrow> odd (x::int)" by presburger |
412 lemma [presburger]: "(x + 1) div 2 = x div 2 + 1 \<longleftrightarrow> odd (x::int)" by presburger |
449 lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2" by presburger |
413 lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2" by presburger |
450 lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" by presburger |
414 lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" by presburger |