author | haftmann |
Thu, 23 Oct 2014 14:04:05 +0200 | |
changeset 58769 | 70fff47875cd |
parent 58740 | cb9d84d3e7f2 |
child 58770 | ae5e9b4f8daf |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Parity.thy |
2 |
Author: Jeremy Avigad |
|
3 |
Author: Jacques D. Fleuriot |
|
21256 | 4 |
*) |
5 |
||
6 |
header {* Even and Odd for int and nat *} |
|
7 |
||
8 |
theory Parity |
|
30738 | 9 |
imports Main |
21256 | 10 |
begin |
11 |
||
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
12 |
subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *} |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
13 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
14 |
lemma two_dvd_Suc_Suc_iff [simp]: |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
15 |
"2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
16 |
using dvd_add_triv_right_iff [of 2 n] by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
17 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
18 |
lemma two_dvd_Suc_iff: |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
19 |
"2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
20 |
by (induct n) auto |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
21 |
|
58687 | 22 |
lemma two_dvd_diff_nat_iff: |
23 |
fixes m n :: nat |
|
24 |
shows "2 dvd m - n \<longleftrightarrow> m < n \<or> 2 dvd m + n" |
|
25 |
proof (cases "n \<le> m") |
|
26 |
case True |
|
27 |
then have "m - n + n * 2 = m + n" by simp |
|
28 |
moreover have "2 dvd m - n \<longleftrightarrow> 2 dvd m - n + n * 2" by simp |
|
29 |
ultimately have "2 dvd m - n \<longleftrightarrow> 2 dvd m + n" by (simp only:) |
|
30 |
then show ?thesis by auto |
|
31 |
next |
|
32 |
case False |
|
33 |
then show ?thesis by simp |
|
34 |
qed |
|
35 |
||
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
36 |
lemma two_dvd_diff_iff: |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
37 |
fixes k l :: int |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
38 |
shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
39 |
using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: ac_simps) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
40 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
41 |
lemma two_dvd_abs_add_iff: |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
42 |
fixes k l :: int |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
43 |
shows "2 dvd \<bar>k\<bar> + l \<longleftrightarrow> 2 dvd k + l" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
44 |
by (cases "k \<ge> 0") (simp_all add: two_dvd_diff_iff ac_simps) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
45 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
46 |
lemma two_dvd_add_abs_iff: |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
47 |
fixes k l :: int |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
48 |
shows "2 dvd k + \<bar>l\<bar> \<longleftrightarrow> 2 dvd k + l" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
49 |
using two_dvd_abs_add_iff [of l k] by (simp add: ac_simps) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
50 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
51 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
52 |
subsection {* Ring structures with parity *} |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
53 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
54 |
class semiring_parity = semiring_dvd + semiring_numeral + |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
55 |
assumes two_not_dvd_one [simp]: "\<not> 2 dvd 1" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
56 |
assumes not_dvd_not_dvd_dvd_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
57 |
assumes two_is_prime: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b" |
58680 | 58 |
assumes not_dvd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1" |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
59 |
begin |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
60 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
61 |
lemma two_dvd_plus_one_iff [simp]: |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
62 |
"2 dvd a + 1 \<longleftrightarrow> \<not> 2 dvd a" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
63 |
by (auto simp add: dvd_add_right_iff intro: not_dvd_not_dvd_dvd_add) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
64 |
|
58680 | 65 |
lemma not_two_dvdE [elim?]: |
66 |
assumes "\<not> 2 dvd a" |
|
67 |
obtains b where "a = 2 * b + 1" |
|
68 |
proof - |
|
69 |
from assms obtain b where *: "a = b + 1" |
|
70 |
by (blast dest: not_dvd_ex_decrement) |
|
71 |
with assms have "2 dvd b + 2" by simp |
|
72 |
then have "2 dvd b" by simp |
|
73 |
then obtain c where "b = 2 * c" .. |
|
74 |
with * have "a = 2 * c + 1" by simp |
|
75 |
with that show thesis . |
|
76 |
qed |
|
77 |
||
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
78 |
end |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
79 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
80 |
instance nat :: semiring_parity |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
81 |
proof |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
82 |
show "\<not> (2 :: nat) dvd 1" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
83 |
by (rule notI, erule dvdE) simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
84 |
next |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
85 |
fix m n :: nat |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
86 |
assume "\<not> 2 dvd m" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
87 |
moreover assume "\<not> 2 dvd n" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
88 |
ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
89 |
by (simp add: two_dvd_Suc_iff) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
90 |
then have "2 dvd Suc m + Suc n" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
91 |
by (blast intro: dvd_add) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
92 |
also have "Suc m + Suc n = m + n + 2" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
93 |
by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
94 |
finally show "2 dvd m + n" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
95 |
using dvd_add_triv_right_iff [of 2 "m + n"] by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
96 |
next |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
97 |
fix m n :: nat |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
98 |
assume *: "2 dvd m * n" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
99 |
show "2 dvd m \<or> 2 dvd n" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
100 |
proof (rule disjCI) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
101 |
assume "\<not> 2 dvd n" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
102 |
then have "2 dvd Suc n" by (simp add: two_dvd_Suc_iff) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
103 |
then obtain r where "Suc n = 2 * r" .. |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
104 |
moreover from * obtain s where "m * n = 2 * s" .. |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
105 |
then have "2 * s + m = m * Suc n" by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
106 |
ultimately have " 2 * s + m = 2 * (m * r)" by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
107 |
then have "m = 2 * (m * r - s)" by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
108 |
then show "2 dvd m" .. |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
109 |
qed |
58680 | 110 |
next |
111 |
fix n :: nat |
|
112 |
assume "\<not> 2 dvd n" |
|
113 |
then show "\<exists>m. n = m + 1" |
|
114 |
by (cases n) simp_all |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
115 |
qed |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
116 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
117 |
class ring_parity = comm_ring_1 + semiring_parity |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
118 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
119 |
instance int :: ring_parity |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
120 |
proof |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
121 |
show "\<not> (2 :: int) dvd 1" by (simp add: dvd_int_unfold_dvd_nat) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
122 |
fix k l :: int |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
123 |
assume "\<not> 2 dvd k" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
124 |
moreover assume "\<not> 2 dvd l" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
125 |
ultimately have "2 dvd nat \<bar>k\<bar> + nat \<bar>l\<bar>" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
126 |
by (auto simp add: dvd_int_unfold_dvd_nat intro: not_dvd_not_dvd_dvd_add) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
127 |
then have "2 dvd \<bar>k\<bar> + \<bar>l\<bar>" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
128 |
by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
129 |
then show "2 dvd k + l" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
130 |
by (simp add: two_dvd_abs_add_iff two_dvd_add_abs_iff) |
58680 | 131 |
next |
132 |
fix k l :: int |
|
133 |
assume "2 dvd k * l" |
|
134 |
then show "2 dvd k \<or> 2 dvd l" |
|
135 |
by (simp add: dvd_int_unfold_dvd_nat two_is_prime nat_abs_mult_distrib) |
|
136 |
next |
|
137 |
fix k :: int |
|
138 |
have "k = (k - 1) + 1" by simp |
|
139 |
then show "\<exists>l. k = l + 1" .. |
|
140 |
qed |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
141 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
142 |
context semiring_div_parity |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
143 |
begin |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
144 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
145 |
subclass semiring_parity |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
146 |
proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
147 |
fix a b c |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
148 |
show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
149 |
by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
150 |
next |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
151 |
fix a b c |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
152 |
assume "(b + c) mod a = 0" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
153 |
with mod_add_eq [of b c a] |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
154 |
have "(b mod a + c mod a) mod a = 0" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
155 |
by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
156 |
moreover assume "b mod a = 0" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
157 |
ultimately show "c mod a = 0" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
158 |
by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
159 |
next |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
160 |
show "1 mod 2 = 1" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
161 |
by (fact one_mod_two_eq_one) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
162 |
next |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
163 |
fix a b |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
164 |
assume "a mod 2 = 1" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
165 |
moreover assume "b mod 2 = 1" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
166 |
ultimately show "(a + b) mod 2 = 0" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
167 |
using mod_add_eq [of a b 2] by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
168 |
next |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
169 |
fix a b |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
170 |
assume "(a * b) mod 2 = 0" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
171 |
then have "(a mod 2) * (b mod 2) = 0" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
172 |
by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2]) |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
173 |
then show "a mod 2 = 0 \<or> b mod 2 = 0" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
174 |
by (rule divisors_zero) |
58680 | 175 |
next |
176 |
fix a |
|
177 |
assume "a mod 2 = 1" |
|
178 |
then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp |
|
179 |
then show "\<exists>b. a = b + 1" .. |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
180 |
qed |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
181 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
182 |
end |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
183 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
184 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
185 |
subsection {* Dedicated @{text even}/@{text odd} predicate *} |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
186 |
|
58680 | 187 |
subsubsection {* Properties *} |
188 |
||
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
189 |
context semiring_parity |
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset
|
190 |
begin |
21256 | 191 |
|
58740 | 192 |
abbreviation even :: "'a \<Rightarrow> bool" |
54228 | 193 |
where |
58740 | 194 |
"even a \<equiv> 2 dvd a" |
54228 | 195 |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
196 |
abbreviation odd :: "'a \<Rightarrow> bool" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
197 |
where |
58740 | 198 |
"odd a \<equiv> \<not> 2 dvd a" |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
199 |
|
58690 | 200 |
lemma evenE [elim?]: |
201 |
assumes "even a" |
|
202 |
obtains b where "a = 2 * b" |
|
58740 | 203 |
using assms by (rule dvdE) |
58690 | 204 |
|
58681 | 205 |
lemma oddE [elim?]: |
58680 | 206 |
assumes "odd a" |
207 |
obtains b where "a = 2 * b + 1" |
|
58740 | 208 |
using assms by (rule not_two_dvdE) |
58680 | 209 |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
210 |
lemma even_times_iff [simp, presburger, algebra]: |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
211 |
"even (a * b) \<longleftrightarrow> even a \<or> even b" |
58740 | 212 |
by (auto simp add: dest: two_is_prime) |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
213 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
214 |
lemma even_zero [simp]: |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
215 |
"even 0" |
58740 | 216 |
by simp |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
217 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
218 |
lemma odd_one [simp]: |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
219 |
"odd 1" |
58740 | 220 |
by simp |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
221 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
222 |
lemma even_numeral [simp]: |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
223 |
"even (numeral (Num.Bit0 n))" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
224 |
proof - |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
225 |
have "even (2 * numeral n)" |
58740 | 226 |
unfolding even_times_iff by simp |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
227 |
then have "even (numeral n + numeral n)" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
228 |
unfolding mult_2 . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
229 |
then show ?thesis |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
230 |
unfolding numeral.simps . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
231 |
qed |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
232 |
|
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
233 |
lemma odd_numeral [simp]: |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
234 |
"odd (numeral (Num.Bit1 n))" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
235 |
proof |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
236 |
assume "even (numeral (num.Bit1 n))" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
237 |
then have "even (numeral n + numeral n + 1)" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
238 |
unfolding numeral.simps . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
239 |
then have "even (2 * numeral n + 1)" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
240 |
unfolding mult_2 . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
241 |
then have "2 dvd numeral n * 2 + 1" |
58740 | 242 |
by (simp add: ac_simps) |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
243 |
with dvd_add_times_triv_left_iff [of 2 "numeral n" 1] |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
244 |
have "2 dvd 1" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
245 |
by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
246 |
then show False by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
247 |
qed |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
248 |
|
58680 | 249 |
lemma even_add [simp]: |
250 |
"even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)" |
|
58740 | 251 |
by (auto simp add: dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add) |
58680 | 252 |
|
253 |
lemma odd_add [simp]: |
|
254 |
"odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))" |
|
255 |
by simp |
|
256 |
||
257 |
lemma even_power [simp, presburger]: |
|
258 |
"even (a ^ n) \<longleftrightarrow> even a \<and> n \<noteq> 0" |
|
259 |
by (induct n) auto |
|
260 |
||
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
261 |
end |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
262 |
|
58679 | 263 |
context ring_parity |
264 |
begin |
|
265 |
||
266 |
lemma even_minus [simp, presburger, algebra]: |
|
267 |
"even (- a) \<longleftrightarrow> even a" |
|
58740 | 268 |
by (fact dvd_minus_iff) |
58679 | 269 |
|
58680 | 270 |
lemma even_diff [simp]: |
271 |
"even (a - b) \<longleftrightarrow> even (a + b)" |
|
272 |
using even_add [of a "- b"] by simp |
|
273 |
||
58679 | 274 |
end |
275 |
||
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
276 |
|
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
277 |
subsubsection {* Parity and division *} |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
278 |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
279 |
context semiring_div_parity |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
280 |
begin |
58645 | 281 |
|
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
282 |
lemma one_div_two_eq_zero [simp]: -- \<open>FIXME move\<close> |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
283 |
"1 div 2 = 0" |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
284 |
proof (cases "2 = 0") |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
285 |
case True then show ?thesis by simp |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
286 |
next |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
287 |
case False |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
288 |
from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" . |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
289 |
with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
290 |
then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq) |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
291 |
then have "1 div 2 = 0 \<or> 2 = 0" by (rule divisors_zero) |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
292 |
with False show ?thesis by auto |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
293 |
qed |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
294 |
|
58711 | 295 |
lemma even_iff_mod_2_eq_zero: |
58645 | 296 |
"even a \<longleftrightarrow> a mod 2 = 0" |
58740 | 297 |
by (fact dvd_eq_mod_eq_0) |
54228 | 298 |
|
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
299 |
lemma even_succ_div_two [simp]: |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
300 |
"even a \<Longrightarrow> (a + 1) div 2 = a div 2" |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
301 |
by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero) |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
302 |
|
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
303 |
lemma odd_succ_div_two [simp]: |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
304 |
"odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1" |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
305 |
by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc) |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
306 |
|
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
307 |
lemma even_two_times_div_two: |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
308 |
"even a \<Longrightarrow> 2 * (a div 2) = a" |
58740 | 309 |
by (fact dvd_mult_div_cancel) |
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
310 |
|
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
311 |
lemma odd_two_times_div_two_succ: |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
312 |
"odd a \<Longrightarrow> 2 * (a div 2) + 1 = a" |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
313 |
using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero) |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
314 |
|
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset
|
315 |
end |
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset
|
316 |
|
58680 | 317 |
|
58687 | 318 |
subsubsection {* Particularities for @{typ nat} and @{typ int} *} |
319 |
||
320 |
lemma even_Suc [simp, presburger, algebra]: |
|
321 |
"even (Suc n) = odd n" |
|
58740 | 322 |
by (fact two_dvd_Suc_iff) |
58687 | 323 |
|
58689 | 324 |
lemma odd_pos: |
325 |
"odd (n :: nat) \<Longrightarrow> 0 < n" |
|
58690 | 326 |
by (auto elim: oddE) |
58689 | 327 |
|
58687 | 328 |
lemma even_diff_nat [simp]: |
329 |
fixes m n :: nat |
|
330 |
shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" |
|
58740 | 331 |
by (fact two_dvd_diff_nat_iff) |
58680 | 332 |
|
58679 | 333 |
lemma even_int_iff: |
334 |
"even (int n) \<longleftrightarrow> even n" |
|
58740 | 335 |
by (simp add: dvd_int_iff) |
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
31718
diff
changeset
|
336 |
|
58687 | 337 |
lemma even_nat_iff: |
338 |
"0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k" |
|
339 |
by (simp add: even_int_iff [symmetric]) |
|
340 |
||
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
341 |
lemma even_num_iff: |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
342 |
"0 < n \<Longrightarrow> even n = odd (n - 1 :: nat)" |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
343 |
by simp |
58687 | 344 |
|
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
345 |
lemma even_Suc_div_two [simp]: |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
346 |
"even n \<Longrightarrow> Suc n div 2 = n div 2" |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
347 |
using even_succ_div_two [of n] by simp |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
348 |
|
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
349 |
lemma odd_Suc_div_two [simp]: |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
350 |
"odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)" |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
351 |
using odd_succ_div_two [of n] by simp |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
352 |
|
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
353 |
lemma odd_two_times_div_two_Suc: |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
354 |
"odd n \<Longrightarrow> Suc (2 * (n div 2)) = n" |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
355 |
using odd_two_times_div_two_succ [of n] by simp |
58769 | 356 |
|
357 |
lemma parity_induct [case_names zero even odd]: |
|
358 |
assumes zero: "P 0" |
|
359 |
assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)" |
|
360 |
assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))" |
|
361 |
shows "P n" |
|
362 |
proof (induct n rule: less_induct) |
|
363 |
case (less n) |
|
364 |
show "P n" |
|
365 |
proof (cases "n = 0") |
|
366 |
case True with zero show ?thesis by simp |
|
367 |
next |
|
368 |
case False |
|
369 |
with less have hyp: "P (n div 2)" by simp |
|
370 |
show ?thesis |
|
371 |
proof (cases "even n") |
|
372 |
case True |
|
373 |
with hyp even [of "n div 2"] show ?thesis |
|
374 |
by (simp add: dvd_mult_div_cancel) |
|
375 |
next |
|
376 |
case False |
|
377 |
with hyp odd [of "n div 2"] show ?thesis |
|
378 |
by (simp add: odd_two_times_div_two_Suc) |
|
379 |
qed |
|
380 |
qed |
|
381 |
qed |
|
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
382 |
|
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
383 |
text {* Nice facts about division by @{term 4} *} |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
384 |
|
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
385 |
lemma even_even_mod_4_iff: |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
386 |
"even (n::nat) \<longleftrightarrow> even (n mod 4)" |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
387 |
by presburger |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
388 |
|
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
389 |
lemma odd_mod_4_div_2: |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
390 |
"n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)" |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
391 |
by presburger |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
392 |
|
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
393 |
lemma even_mod_4_div_2: |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
394 |
"n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)" |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
395 |
by presburger |
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
396 |
|
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
397 |
text {* Parity and powers *} |
58689 | 398 |
|
399 |
context comm_ring_1 |
|
400 |
begin |
|
401 |
||
402 |
lemma power_minus_even [simp]: |
|
403 |
"even n \<Longrightarrow> (- a) ^ n = a ^ n" |
|
58690 | 404 |
by (auto elim: evenE) |
58689 | 405 |
|
406 |
lemma power_minus_odd [simp]: |
|
407 |
"odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)" |
|
58690 | 408 |
by (auto elim: oddE) |
409 |
||
410 |
lemma neg_power_if: |
|
411 |
"(- a) ^ n = (if even n then a ^ n else - (a ^ n))" |
|
412 |
by simp |
|
58689 | 413 |
|
414 |
lemma neg_one_even_power [simp]: |
|
415 |
"even n \<Longrightarrow> (- 1) ^ n = 1" |
|
58690 | 416 |
by simp |
58689 | 417 |
|
418 |
lemma neg_one_odd_power [simp]: |
|
419 |
"odd n \<Longrightarrow> (- 1) ^ n = - 1" |
|
58690 | 420 |
by simp |
58689 | 421 |
|
422 |
end |
|
423 |
||
424 |
lemma zero_less_power_nat_eq_numeral [simp]: -- \<open>FIXME move\<close> |
|
425 |
"0 < (n :: nat) ^ numeral w \<longleftrightarrow> 0 < n \<or> numeral w = (0 :: nat)" |
|
426 |
by (fact nat_zero_less_power_iff) |
|
427 |
||
428 |
context linordered_idom |
|
429 |
begin |
|
430 |
||
431 |
lemma power_eq_0_iff' [simp]: -- \<open>FIXME move\<close> |
|
432 |
"a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0" |
|
433 |
by (induct n) auto |
|
434 |
||
435 |
lemma power2_less_eq_zero_iff [simp]: -- \<open>FIXME move\<close> |
|
436 |
"a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0" |
|
437 |
proof (cases "a = 0") |
|
438 |
case True then show ?thesis by simp |
|
439 |
next |
|
440 |
case False then have "a < 0 \<or> a > 0" by auto |
|
441 |
then have "a\<^sup>2 > 0" by auto |
|
442 |
then have "\<not> a\<^sup>2 \<le> 0" by (simp add: not_le) |
|
443 |
with False show ?thesis by simp |
|
444 |
qed |
|
445 |
||
446 |
lemma zero_le_even_power: |
|
447 |
"even n \<Longrightarrow> 0 \<le> a ^ n" |
|
58690 | 448 |
by (auto elim: evenE) |
58689 | 449 |
|
450 |
lemma zero_le_odd_power: |
|
451 |
"odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a" |
|
452 |
by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) |
|
453 |
||
58718 | 454 |
lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close> |
58689 | 455 |
"0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n" |
456 |
proof (cases "even n") |
|
457 |
case True |
|
458 |
then obtain k where "n = 2 * k" .. |
|
58690 | 459 |
then show ?thesis by simp |
58689 | 460 |
next |
461 |
case False |
|
462 |
then obtain k where "n = 2 * k + 1" .. |
|
463 |
moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0" |
|
464 |
by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff) |
|
465 |
ultimately show ?thesis |
|
466 |
by (auto simp add: zero_le_mult_iff zero_le_even_power) |
|
467 |
qed |
|
468 |
||
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
469 |
lemma zero_le_power_eq [presburger]: |
58689 | 470 |
"0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a" |
471 |
using zero_le_power_iff [of a n] by auto |
|
472 |
||
473 |
lemma zero_less_power_eq [presburger]: |
|
474 |
"0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a" |
|
475 |
proof - |
|
476 |
have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0" |
|
477 |
unfolding power_eq_0_iff' [of a n, symmetric] by blast |
|
478 |
show ?thesis |
|
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset
|
479 |
unfolding less_le zero_le_power_eq by auto |
58689 | 480 |
qed |
481 |
||
482 |
lemma power_less_zero_eq [presburger]: |
|
483 |
"a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0" |
|
484 |
unfolding not_le [symmetric] zero_le_power_eq by auto |
|
485 |
||
486 |
lemma power_le_zero_eq [presburger]: |
|
487 |
"a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)" |
|
488 |
unfolding not_less [symmetric] zero_less_power_eq by auto |
|
489 |
||
490 |
lemma power_even_abs: |
|
491 |
"even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n" |
|
492 |
using power_abs [of a n] by (simp add: zero_le_even_power) |
|
493 |
||
494 |
lemma power_mono_even: |
|
495 |
assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>" |
|
496 |
shows "a ^ n \<le> b ^ n" |
|
497 |
proof - |
|
498 |
have "0 \<le> \<bar>a\<bar>" by auto |
|
499 |
with `\<bar>a\<bar> \<le> \<bar>b\<bar>` |
|
500 |
have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n" by (rule power_mono) |
|
501 |
with `even n` show ?thesis by (simp add: power_even_abs) |
|
502 |
qed |
|
503 |
||
504 |
lemma power_mono_odd: |
|
505 |
assumes "odd n" and "a \<le> b" |
|
506 |
shows "a ^ n \<le> b ^ n" |
|
507 |
proof (cases "b < 0") |
|
508 |
case True with `a \<le> b` have "- b \<le> - a" and "0 \<le> - b" by auto |
|
509 |
hence "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono) |
|
510 |
with `odd n` show ?thesis by simp |
|
511 |
next |
|
512 |
case False then have "0 \<le> b" by auto |
|
513 |
show ?thesis |
|
514 |
proof (cases "a < 0") |
|
515 |
case True then have "n \<noteq> 0" and "a \<le> 0" using `odd n` [THEN odd_pos] by auto |
|
516 |
then have "a ^ n \<le> 0" unfolding power_le_zero_eq using `odd n` by auto |
|
517 |
moreover |
|
518 |
from `0 \<le> b` have "0 \<le> b ^ n" by auto |
|
519 |
ultimately show ?thesis by auto |
|
520 |
next |
|
521 |
case False then have "0 \<le> a" by auto |
|
522 |
with `a \<le> b` show ?thesis using power_mono by auto |
|
523 |
qed |
|
524 |
qed |
|
525 |
||
526 |
text {* Simplify, when the exponent is a numeral *} |
|
527 |
||
528 |
lemma zero_le_power_eq_numeral [simp]: |
|
529 |
"0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a" |
|
530 |
by (fact zero_le_power_eq) |
|
531 |
||
532 |
lemma zero_less_power_eq_numeral [simp]: |
|
533 |
"0 < a ^ numeral w \<longleftrightarrow> numeral w = (0 :: nat) |
|
534 |
\<or> even (numeral w :: nat) \<and> a \<noteq> 0 \<or> odd (numeral w :: nat) \<and> 0 < a" |
|
535 |
by (fact zero_less_power_eq) |
|
536 |
||
537 |
lemma power_le_zero_eq_numeral [simp]: |
|
538 |
"a ^ numeral w \<le> 0 \<longleftrightarrow> (0 :: nat) < numeral w |
|
539 |
\<and> (odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)" |
|
540 |
by (fact power_le_zero_eq) |
|
541 |
||
542 |
lemma power_less_zero_eq_numeral [simp]: |
|
543 |
"a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0" |
|
544 |
by (fact power_less_zero_eq) |
|
545 |
||
546 |
lemma power_eq_0_iff_numeral [simp]: |
|
547 |
"a ^ numeral w = (0 :: nat) \<longleftrightarrow> a = 0 \<and> numeral w \<noteq> (0 :: nat)" |
|
548 |
by (fact power_eq_0_iff) |
|
549 |
||
550 |
lemma power_even_abs_numeral [simp]: |
|
551 |
"even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w" |
|
552 |
by (fact power_even_abs) |
|
553 |
||
554 |
end |
|
555 |
||
556 |
||
58687 | 557 |
subsubsection {* Tools setup *} |
558 |
||
58679 | 559 |
declare transfer_morphism_int_nat [transfer add return: |
560 |
even_int_iff |
|
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
31718
diff
changeset
|
561 |
] |
21256 | 562 |
|
58679 | 563 |
lemma [presburger]: |
564 |
"even n \<longleftrightarrow> even (int n)" |
|
565 |
using even_int_iff [of n] by simp |
|
25600 | 566 |
|
58687 | 567 |
lemma (in semiring_parity) [presburger]: |
58680 | 568 |
"even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b" |
569 |
by auto |
|
21256 | 570 |
|
58687 | 571 |
lemma [presburger, algebra]: |
572 |
fixes m n :: nat |
|
573 |
shows "even (m - n) \<longleftrightarrow> m < n \<or> even m \<and> even n \<or> odd m \<and> odd n" |
|
574 |
by auto |
|
575 |
||
576 |
lemma [presburger, algebra]: |
|
577 |
fixes m n :: nat |
|
578 |
shows "even (m ^ n) \<longleftrightarrow> even m \<and> 0 < n" |
|
579 |
by simp |
|
580 |
||
581 |
lemma [presburger]: |
|
582 |
fixes k :: int |
|
583 |
shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k" |
|
584 |
by presburger |
|
585 |
||
586 |
lemma [presburger]: |
|
587 |
fixes k :: int |
|
588 |
shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k" |
|
589 |
by presburger |
|
590 |
||
591 |
lemma [presburger]: |
|
592 |
"Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n" |
|
593 |
by presburger |
|
594 |
||
21256 | 595 |
end |
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
47225
diff
changeset
|
596 |