author | haftmann |
Sun, 17 Nov 2019 20:44:35 +0000 | |
changeset 71138 | 9de7f1067520 |
parent 71094 | a197532693a5 |
child 71157 | 8bdf3c36011c |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Parity.thy |
2 |
Author: Jeremy Avigad |
|
3 |
Author: Jacques D. Fleuriot |
|
21256 | 4 |
*) |
5 |
||
60758 | 6 |
section \<open>Parity in rings and semirings\<close> |
21256 | 7 |
|
8 |
theory Parity |
|
66815 | 9 |
imports Euclidean_Division |
21256 | 10 |
begin |
11 |
||
61799 | 12 |
subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close> |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
13 |
|
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
14 |
class semiring_parity = comm_semiring_1 + semiring_modulo + |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
15 |
assumes even_iff_mod_2_eq_zero: "2 dvd a \<longleftrightarrow> a mod 2 = 0" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
16 |
and odd_iff_mod_2_eq_one: "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
17 |
and odd_one [simp]: "\<not> 2 dvd 1" |
66839 | 18 |
begin |
19 |
||
58740 | 20 |
abbreviation even :: "'a \<Rightarrow> bool" |
63654 | 21 |
where "even a \<equiv> 2 dvd a" |
54228 | 22 |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
23 |
abbreviation odd :: "'a \<Rightarrow> bool" |
63654 | 24 |
where "odd a \<equiv> \<not> 2 dvd a" |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
25 |
|
66815 | 26 |
lemma parity_cases [case_names even odd]: |
27 |
assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P" |
|
28 |
assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P" |
|
29 |
shows P |
|
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
30 |
using assms by (cases "even a") |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
31 |
(simp_all add: even_iff_mod_2_eq_zero [symmetric] odd_iff_mod_2_eq_one [symmetric]) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
32 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
33 |
lemma not_mod_2_eq_0_eq_1 [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
34 |
"a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
35 |
by (cases a rule: parity_cases) simp_all |
66815 | 36 |
|
37 |
lemma not_mod_2_eq_1_eq_0 [simp]: |
|
38 |
"a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0" |
|
39 |
by (cases a rule: parity_cases) simp_all |
|
40 |
||
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
41 |
lemma mod2_eq_if: "a mod 2 = (if 2 dvd a then 0 else 1)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
42 |
by (simp add: even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one) |
58787 | 43 |
|
58690 | 44 |
lemma evenE [elim?]: |
45 |
assumes "even a" |
|
46 |
obtains b where "a = 2 * b" |
|
58740 | 47 |
using assms by (rule dvdE) |
58690 | 48 |
|
58681 | 49 |
lemma oddE [elim?]: |
58680 | 50 |
assumes "odd a" |
51 |
obtains b where "a = 2 * b + 1" |
|
58787 | 52 |
proof - |
66815 | 53 |
have "a = 2 * (a div 2) + a mod 2" |
54 |
by (simp add: mult_div_mod_eq) |
|
55 |
with assms have "a = 2 * (a div 2) + 1" |
|
56 |
by (simp add: odd_iff_mod_2_eq_one) |
|
57 |
then show ?thesis .. |
|
58 |
qed |
|
59 |
||
60 |
lemma mod_2_eq_odd: |
|
61 |
"a mod 2 = of_bool (odd a)" |
|
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
62 |
by (auto elim: oddE simp add: even_iff_mod_2_eq_zero) |
66815 | 63 |
|
67816 | 64 |
lemma of_bool_odd_eq_mod_2: |
65 |
"of_bool (odd a) = a mod 2" |
|
66 |
by (simp add: mod_2_eq_odd) |
|
67 |
||
66815 | 68 |
lemma even_zero [simp]: |
69 |
"even 0" |
|
70 |
by (fact dvd_0_right) |
|
71 |
||
72 |
lemma odd_even_add: |
|
73 |
"even (a + b)" if "odd a" and "odd b" |
|
74 |
proof - |
|
75 |
from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1" |
|
76 |
by (blast elim: oddE) |
|
77 |
then have "a + b = 2 * c + 2 * d + (1 + 1)" |
|
78 |
by (simp only: ac_simps) |
|
79 |
also have "\<dots> = 2 * (c + d + 1)" |
|
80 |
by (simp add: algebra_simps) |
|
81 |
finally show ?thesis .. |
|
82 |
qed |
|
83 |
||
84 |
lemma even_add [simp]: |
|
85 |
"even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)" |
|
86 |
by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add) |
|
87 |
||
88 |
lemma odd_add [simp]: |
|
89 |
"odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)" |
|
90 |
by simp |
|
91 |
||
92 |
lemma even_plus_one_iff [simp]: |
|
93 |
"even (a + 1) \<longleftrightarrow> odd a" |
|
94 |
by (auto simp add: dvd_add_right_iff intro: odd_even_add) |
|
95 |
||
96 |
lemma even_mult_iff [simp]: |
|
97 |
"even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q") |
|
98 |
proof |
|
99 |
assume ?Q |
|
100 |
then show ?P |
|
101 |
by auto |
|
102 |
next |
|
103 |
assume ?P |
|
104 |
show ?Q |
|
105 |
proof (rule ccontr) |
|
106 |
assume "\<not> (even a \<or> even b)" |
|
107 |
then have "odd a" and "odd b" |
|
108 |
by auto |
|
109 |
then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1" |
|
110 |
by (blast elim: oddE) |
|
111 |
then have "a * b = (2 * r + 1) * (2 * s + 1)" |
|
112 |
by simp |
|
113 |
also have "\<dots> = 2 * (2 * r * s + r + s) + 1" |
|
114 |
by (simp add: algebra_simps) |
|
115 |
finally have "odd (a * b)" |
|
116 |
by simp |
|
117 |
with \<open>?P\<close> show False |
|
118 |
by auto |
|
119 |
qed |
|
120 |
qed |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
121 |
|
63654 | 122 |
lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))" |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
123 |
proof - |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
124 |
have "even (2 * numeral n)" |
66815 | 125 |
unfolding even_mult_iff by simp |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
126 |
then have "even (numeral n + numeral n)" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
127 |
unfolding mult_2 . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
128 |
then show ?thesis |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
129 |
unfolding numeral.simps . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
130 |
qed |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
131 |
|
63654 | 132 |
lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))" |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
133 |
proof |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
134 |
assume "even (numeral (num.Bit1 n))" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
135 |
then have "even (numeral n + numeral n + 1)" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
136 |
unfolding numeral.simps . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
137 |
then have "even (2 * numeral n + 1)" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
138 |
unfolding mult_2 . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
139 |
then have "2 dvd numeral n * 2 + 1" |
58740 | 140 |
by (simp add: ac_simps) |
63654 | 141 |
then have "2 dvd 1" |
142 |
using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
143 |
then show False by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
144 |
qed |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
145 |
|
63654 | 146 |
lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0" |
58680 | 147 |
by (induct n) auto |
148 |
||
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
149 |
end |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
150 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
151 |
class ring_parity = ring + semiring_parity |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
152 |
begin |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
153 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
154 |
subclass comm_ring_1 .. |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
155 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
156 |
lemma even_minus: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
157 |
"even (- a) \<longleftrightarrow> even a" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
158 |
by (fact dvd_minus_iff) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
159 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
160 |
lemma even_diff [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
161 |
"even (a - b) \<longleftrightarrow> even (a + b)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
162 |
using even_add [of a "- b"] by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
163 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
164 |
end |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
165 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
166 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
167 |
subsection \<open>Special case: euclidean rings containing the natural numbers\<close> |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
168 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
169 |
class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring + |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
170 |
assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
171 |
and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
172 |
and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
173 |
begin |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
174 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
175 |
lemma division_segment_eq_iff: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
176 |
"a = b" if "division_segment a = division_segment b" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
177 |
and "euclidean_size a = euclidean_size b" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
178 |
using that division_segment_euclidean_size [of a] by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
179 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
180 |
lemma euclidean_size_of_nat [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
181 |
"euclidean_size (of_nat n) = n" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
182 |
proof - |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
183 |
have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
184 |
by (fact division_segment_euclidean_size) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
185 |
then show ?thesis by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
186 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
187 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
188 |
lemma of_nat_euclidean_size: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
189 |
"of_nat (euclidean_size a) = a div division_segment a" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
190 |
proof - |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
191 |
have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
192 |
by (subst nonzero_mult_div_cancel_left) simp_all |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
193 |
also have "\<dots> = a div division_segment a" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
194 |
by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
195 |
finally show ?thesis . |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
196 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
197 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
198 |
lemma division_segment_1 [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
199 |
"division_segment 1 = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
200 |
using division_segment_of_nat [of 1] by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
201 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
202 |
lemma division_segment_numeral [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
203 |
"division_segment (numeral k) = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
204 |
using division_segment_of_nat [of "numeral k"] by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
205 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
206 |
lemma euclidean_size_1 [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
207 |
"euclidean_size 1 = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
208 |
using euclidean_size_of_nat [of 1] by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
209 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
210 |
lemma euclidean_size_numeral [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
211 |
"euclidean_size (numeral k) = numeral k" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
212 |
using euclidean_size_of_nat [of "numeral k"] by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
213 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
214 |
lemma of_nat_dvd_iff: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
215 |
"of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q") |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
216 |
proof (cases "m = 0") |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
217 |
case True |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
218 |
then show ?thesis |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
219 |
by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
220 |
next |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
221 |
case False |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
222 |
show ?thesis |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
223 |
proof |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
224 |
assume ?Q |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
225 |
then show ?P |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
226 |
by auto |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
227 |
next |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
228 |
assume ?P |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
229 |
with False have "of_nat n = of_nat n div of_nat m * of_nat m" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
230 |
by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
231 |
then have "of_nat n = of_nat (n div m * m)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
232 |
by (simp add: of_nat_div) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
233 |
then have "n = n div m * m" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
234 |
by (simp only: of_nat_eq_iff) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
235 |
then have "n = m * (n div m)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
236 |
by (simp add: ac_simps) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
237 |
then show ?Q .. |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
238 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
239 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
240 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
241 |
lemma of_nat_mod: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
242 |
"of_nat (m mod n) = of_nat m mod of_nat n" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
243 |
proof - |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
244 |
have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
245 |
by (simp add: div_mult_mod_eq) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
246 |
also have "of_nat m = of_nat (m div n * n + m mod n)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
247 |
by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
248 |
finally show ?thesis |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
249 |
by (simp only: of_nat_div of_nat_mult of_nat_add) simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
250 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
251 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
252 |
lemma one_div_two_eq_zero [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
253 |
"1 div 2 = 0" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
254 |
proof - |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
255 |
from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
256 |
by (simp only:) simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
257 |
then show ?thesis |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
258 |
by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
259 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
260 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
261 |
lemma one_mod_two_eq_one [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
262 |
"1 mod 2 = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
263 |
proof - |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
264 |
from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
265 |
by (simp only:) simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
266 |
then show ?thesis |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
267 |
by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
268 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
269 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
270 |
subclass semiring_parity |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
271 |
proof |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
272 |
show "2 dvd a \<longleftrightarrow> a mod 2 = 0" for a |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
273 |
by (fact dvd_eq_mod_eq_0) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
274 |
show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" for a |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
275 |
proof |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
276 |
assume "a mod 2 = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
277 |
then show "\<not> 2 dvd a" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
278 |
by auto |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
279 |
next |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
280 |
assume "\<not> 2 dvd a" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
281 |
have eucl: "euclidean_size (a mod 2) = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
282 |
proof (rule order_antisym) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
283 |
show "euclidean_size (a mod 2) \<le> 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
284 |
using mod_size_less [of 2 a] by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
285 |
show "1 \<le> euclidean_size (a mod 2)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
286 |
using \<open>\<not> 2 dvd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
287 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
288 |
from \<open>\<not> 2 dvd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
289 |
by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
290 |
then have "\<not> of_nat 2 dvd of_nat (euclidean_size a)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
291 |
by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
292 |
then have "\<not> 2 dvd euclidean_size a" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
293 |
using of_nat_dvd_iff [of 2] by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
294 |
then have "euclidean_size a mod 2 = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
295 |
by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
296 |
then have "of_nat (euclidean_size a mod 2) = of_nat 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
297 |
by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
298 |
then have "of_nat (euclidean_size a) mod 2 = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
299 |
by (simp add: of_nat_mod) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
300 |
from \<open>\<not> 2 dvd a\<close> eucl |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
301 |
show "a mod 2 = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
302 |
by (auto intro: division_segment_eq_iff simp add: division_segment_mod) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
303 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
304 |
show "\<not> is_unit 2" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
305 |
proof (rule notI) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
306 |
assume "is_unit 2" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
307 |
then have "of_nat 2 dvd of_nat 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
308 |
by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
309 |
then have "is_unit (2::nat)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
310 |
by (simp only: of_nat_dvd_iff) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
311 |
then show False |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
312 |
by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
313 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
314 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
315 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
316 |
lemma even_of_nat [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
317 |
"even (of_nat a) \<longleftrightarrow> even a" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
318 |
proof - |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
319 |
have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
320 |
by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
321 |
also have "\<dots> \<longleftrightarrow> even a" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
322 |
by (simp only: of_nat_dvd_iff) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
323 |
finally show ?thesis . |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
324 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
325 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
326 |
lemma one_mod_2_pow_eq [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
327 |
"1 mod (2 ^ n) = of_bool (n > 0)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
328 |
proof - |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
329 |
have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
330 |
using of_nat_mod [of 1 "2 ^ n"] by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
331 |
also have "\<dots> = of_bool (n > 0)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
332 |
by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
333 |
finally show ?thesis . |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
334 |
qed |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
335 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
336 |
lemma one_div_2_pow_eq [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
337 |
"1 div (2 ^ n) = of_bool (n = 0)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
338 |
using div_mult_mod_eq [of 1 "2 ^ n"] by auto |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
339 |
|
66815 | 340 |
lemma even_succ_div_two [simp]: |
341 |
"even a \<Longrightarrow> (a + 1) div 2 = a div 2" |
|
342 |
by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero) |
|
343 |
||
344 |
lemma odd_succ_div_two [simp]: |
|
345 |
"odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1" |
|
346 |
by (auto elim!: oddE simp add: add.assoc) |
|
347 |
||
348 |
lemma even_two_times_div_two: |
|
349 |
"even a \<Longrightarrow> 2 * (a div 2) = a" |
|
350 |
by (fact dvd_mult_div_cancel) |
|
351 |
||
352 |
lemma odd_two_times_div_two_succ [simp]: |
|
353 |
"odd a \<Longrightarrow> 2 * (a div 2) + 1 = a" |
|
354 |
using mult_div_mod_eq [of 2 a] |
|
355 |
by (simp add: even_iff_mod_2_eq_zero) |
|
356 |
||
67051 | 357 |
lemma coprime_left_2_iff_odd [simp]: |
358 |
"coprime 2 a \<longleftrightarrow> odd a" |
|
359 |
proof |
|
360 |
assume "odd a" |
|
361 |
show "coprime 2 a" |
|
362 |
proof (rule coprimeI) |
|
363 |
fix b |
|
364 |
assume "b dvd 2" "b dvd a" |
|
365 |
then have "b dvd a mod 2" |
|
366 |
by (auto intro: dvd_mod) |
|
367 |
with \<open>odd a\<close> show "is_unit b" |
|
368 |
by (simp add: mod_2_eq_odd) |
|
369 |
qed |
|
370 |
next |
|
371 |
assume "coprime 2 a" |
|
372 |
show "odd a" |
|
373 |
proof (rule notI) |
|
374 |
assume "even a" |
|
375 |
then obtain b where "a = 2 * b" .. |
|
376 |
with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)" |
|
377 |
by simp |
|
378 |
moreover have "\<not> coprime 2 (2 * b)" |
|
379 |
by (rule not_coprimeI [of 2]) simp_all |
|
380 |
ultimately show False |
|
381 |
by blast |
|
382 |
qed |
|
383 |
qed |
|
384 |
||
385 |
lemma coprime_right_2_iff_odd [simp]: |
|
386 |
"coprime a 2 \<longleftrightarrow> odd a" |
|
387 |
using coprime_left_2_iff_odd [of a] by (simp add: ac_simps) |
|
388 |
||
67828 | 389 |
lemma div_mult2_eq': |
390 |
"a div (of_nat m * of_nat n) = a div of_nat m div of_nat n" |
|
391 |
proof (cases a "of_nat m * of_nat n" rule: divmod_cases) |
|
392 |
case (divides q) |
|
393 |
then show ?thesis |
|
394 |
using nonzero_mult_div_cancel_right [of "of_nat m" "q * of_nat n"] |
|
395 |
by (simp add: ac_simps) |
|
396 |
next |
|
397 |
case (remainder q r) |
|
398 |
then have "division_segment r = 1" |
|
399 |
using division_segment_of_nat [of "m * n"] by simp |
|
400 |
with division_segment_euclidean_size [of r] |
|
401 |
have "of_nat (euclidean_size r) = r" |
|
402 |
by simp |
|
67908 | 403 |
have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0" |
404 |
by simp |
|
405 |
with remainder(6) have "r div (of_nat m * of_nat n) = 0" |
|
67828 | 406 |
by simp |
67908 | 407 |
with \<open>of_nat (euclidean_size r) = r\<close> |
408 |
have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0" |
|
409 |
by simp |
|
410 |
then have "of_nat (euclidean_size r div (m * n)) = 0" |
|
67828 | 411 |
by (simp add: of_nat_div) |
67908 | 412 |
then have "of_nat (euclidean_size r div m div n) = 0" |
413 |
by (simp add: div_mult2_eq) |
|
414 |
with \<open>of_nat (euclidean_size r) = r\<close> have "r div of_nat m div of_nat n = 0" |
|
415 |
by (simp add: of_nat_div) |
|
67828 | 416 |
with remainder(1) |
417 |
have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n" |
|
418 |
by simp |
|
67908 | 419 |
with remainder(5) remainder(7) show ?thesis |
67828 | 420 |
using div_plus_div_distrib_dvd_right [of "of_nat m" "q * (of_nat m * of_nat n)" r] |
421 |
by (simp add: ac_simps) |
|
422 |
next |
|
423 |
case by0 |
|
424 |
then show ?thesis |
|
425 |
by auto |
|
426 |
qed |
|
427 |
||
428 |
lemma mod_mult2_eq': |
|
429 |
"a mod (of_nat m * of_nat n) = of_nat m * (a div of_nat m mod of_nat n) + a mod of_nat m" |
|
430 |
proof - |
|
431 |
have "a div (of_nat m * of_nat n) * (of_nat m * of_nat n) + a mod (of_nat m * of_nat n) = a div of_nat m div of_nat n * of_nat n * of_nat m + (a div of_nat m mod of_nat n * of_nat m + a mod of_nat m)" |
|
432 |
by (simp add: combine_common_factor div_mult_mod_eq) |
|
433 |
moreover have "a div of_nat m div of_nat n * of_nat n * of_nat m = of_nat n * of_nat m * (a div of_nat m div of_nat n)" |
|
434 |
by (simp add: ac_simps) |
|
435 |
ultimately show ?thesis |
|
436 |
by (simp add: div_mult2_eq' mult_commute) |
|
437 |
qed |
|
438 |
||
68028 | 439 |
lemma div_mult2_numeral_eq: |
440 |
"a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B") |
|
441 |
proof - |
|
442 |
have "?A = a div of_nat (numeral k) div of_nat (numeral l)" |
|
443 |
by simp |
|
444 |
also have "\<dots> = a div (of_nat (numeral k) * of_nat (numeral l))" |
|
445 |
by (fact div_mult2_eq' [symmetric]) |
|
446 |
also have "\<dots> = ?B" |
|
447 |
by simp |
|
448 |
finally show ?thesis . |
|
449 |
qed |
|
450 |
||
70911 | 451 |
lemma numeral_Bit0_div_2: |
452 |
"numeral (num.Bit0 n) div 2 = numeral n" |
|
453 |
proof - |
|
454 |
have "numeral (num.Bit0 n) = numeral n + numeral n" |
|
455 |
by (simp only: numeral.simps) |
|
456 |
also have "\<dots> = numeral n * 2" |
|
457 |
by (simp add: mult_2_right) |
|
458 |
finally have "numeral (num.Bit0 n) div 2 = numeral n * 2 div 2" |
|
459 |
by simp |
|
460 |
also have "\<dots> = numeral n" |
|
461 |
by (rule nonzero_mult_div_cancel_right) simp |
|
462 |
finally show ?thesis . |
|
463 |
qed |
|
464 |
||
465 |
lemma numeral_Bit1_div_2: |
|
466 |
"numeral (num.Bit1 n) div 2 = numeral n" |
|
467 |
proof - |
|
468 |
have "numeral (num.Bit1 n) = numeral n + numeral n + 1" |
|
469 |
by (simp only: numeral.simps) |
|
470 |
also have "\<dots> = numeral n * 2 + 1" |
|
471 |
by (simp add: mult_2_right) |
|
472 |
finally have "numeral (num.Bit1 n) div 2 = (numeral n * 2 + 1) div 2" |
|
473 |
by simp |
|
474 |
also have "\<dots> = numeral n * 2 div 2 + 1 div 2" |
|
475 |
using dvd_triv_right by (rule div_plus_div_distrib_dvd_left) |
|
476 |
also have "\<dots> = numeral n * 2 div 2" |
|
477 |
by simp |
|
478 |
also have "\<dots> = numeral n" |
|
479 |
by (rule nonzero_mult_div_cancel_right) simp |
|
480 |
finally show ?thesis . |
|
481 |
qed |
|
482 |
||
71138 | 483 |
lemma exp_mod_exp: |
484 |
\<open>2 ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close> |
|
485 |
proof - |
|
486 |
have \<open>(2::nat) ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close> (is \<open>?lhs = ?rhs\<close>) |
|
487 |
by (auto simp add: not_less monoid_mult_class.power_add dest!: le_Suc_ex) |
|
488 |
then have \<open>of_nat ?lhs = of_nat ?rhs\<close> |
|
489 |
by simp |
|
490 |
then show ?thesis |
|
491 |
by (simp add: of_nat_mod) |
|
492 |
qed |
|
493 |
||
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
494 |
end |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
495 |
|
70340 | 496 |
class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat |
58679 | 497 |
begin |
498 |
||
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
499 |
subclass ring_parity .. |
58680 | 500 |
|
67906 | 501 |
lemma minus_1_mod_2_eq [simp]: |
502 |
"- 1 mod 2 = 1" |
|
503 |
by (simp add: mod_2_eq_odd) |
|
504 |
||
505 |
lemma minus_1_div_2_eq [simp]: |
|
506 |
"- 1 div 2 = - 1" |
|
507 |
proof - |
|
508 |
from div_mult_mod_eq [of "- 1" 2] |
|
509 |
have "- 1 div 2 * 2 = - 1 * 2" |
|
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
510 |
using add_implies_diff by fastforce |
67906 | 511 |
then show ?thesis |
512 |
using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp |
|
513 |
qed |
|
514 |
||
58679 | 515 |
end |
516 |
||
66808
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66582
diff
changeset
|
517 |
|
69593 | 518 |
subsection \<open>Instance for \<^typ>\<open>nat\<close>\<close> |
66808
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66582
diff
changeset
|
519 |
|
70340 | 520 |
instance nat :: unique_euclidean_semiring_with_nat |
66815 | 521 |
by standard (simp_all add: dvd_eq_mod_eq_0) |
66808
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66582
diff
changeset
|
522 |
|
66815 | 523 |
lemma even_Suc_Suc_iff [simp]: |
524 |
"even (Suc (Suc n)) \<longleftrightarrow> even n" |
|
58787 | 525 |
using dvd_add_triv_right_iff [of 2 n] by simp |
58687 | 526 |
|
66815 | 527 |
lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n" |
528 |
using even_plus_one_iff [of n] by simp |
|
58787 | 529 |
|
66815 | 530 |
lemma even_diff_nat [simp]: |
531 |
"even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat |
|
58787 | 532 |
proof (cases "n \<le> m") |
533 |
case True |
|
534 |
then have "m - n + n * 2 = m + n" by (simp add: mult_2_right) |
|
66815 | 535 |
moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp |
536 |
ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:) |
|
58787 | 537 |
then show ?thesis by auto |
538 |
next |
|
539 |
case False |
|
540 |
then show ?thesis by simp |
|
63654 | 541 |
qed |
542 |
||
66815 | 543 |
lemma odd_pos: |
544 |
"odd n \<Longrightarrow> 0 < n" for n :: nat |
|
58690 | 545 |
by (auto elim: oddE) |
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
59816
diff
changeset
|
546 |
|
66815 | 547 |
lemma Suc_double_not_eq_double: |
548 |
"Suc (2 * m) \<noteq> 2 * n" |
|
62597 | 549 |
proof |
550 |
assume "Suc (2 * m) = 2 * n" |
|
551 |
moreover have "odd (Suc (2 * m))" and "even (2 * n)" |
|
552 |
by simp_all |
|
553 |
ultimately show False by simp |
|
554 |
qed |
|
555 |
||
66815 | 556 |
lemma double_not_eq_Suc_double: |
557 |
"2 * m \<noteq> Suc (2 * n)" |
|
62597 | 558 |
using Suc_double_not_eq_double [of n m] by simp |
559 |
||
66815 | 560 |
lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n" |
561 |
by (auto elim: oddE) |
|
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
59816
diff
changeset
|
562 |
|
66815 | 563 |
lemma even_Suc_div_two [simp]: |
564 |
"even n \<Longrightarrow> Suc n div 2 = n div 2" |
|
565 |
using even_succ_div_two [of n] by simp |
|
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
59816
diff
changeset
|
566 |
|
66815 | 567 |
lemma odd_Suc_div_two [simp]: |
568 |
"odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)" |
|
569 |
using odd_succ_div_two [of n] by simp |
|
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
59816
diff
changeset
|
570 |
|
66815 | 571 |
lemma odd_two_times_div_two_nat [simp]: |
572 |
assumes "odd n" |
|
573 |
shows "2 * (n div 2) = n - (1 :: nat)" |
|
574 |
proof - |
|
575 |
from assms have "2 * (n div 2) + 1 = n" |
|
576 |
by (rule odd_two_times_div_two_succ) |
|
577 |
then have "Suc (2 * (n div 2)) - 1 = n - 1" |
|
58787 | 578 |
by simp |
66815 | 579 |
then show ?thesis |
580 |
by simp |
|
58787 | 581 |
qed |
58680 | 582 |
|
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
583 |
lemma not_mod2_eq_Suc_0_eq_0 [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
584 |
"n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
585 |
using not_mod_2_eq_1_eq_0 [of n] by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
586 |
|
69502 | 587 |
lemma odd_card_imp_not_empty: |
588 |
\<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close> |
|
589 |
using that by auto |
|
590 |
||
70365
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
591 |
lemma nat_induct2 [case_names 0 1 step]: |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
592 |
assumes "P 0" "P 1" and step: "\<And>n::nat. P n \<Longrightarrow> P (n + 2)" |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
593 |
shows "P n" |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
594 |
proof (induct n rule: less_induct) |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
595 |
case (less n) |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
596 |
show ?case |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
597 |
proof (cases "n < Suc (Suc 0)") |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
598 |
case True |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
599 |
then show ?thesis |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
600 |
using assms by (auto simp: less_Suc_eq) |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
601 |
next |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
602 |
case False |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
603 |
then obtain k where k: "n = Suc (Suc k)" |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
604 |
by (force simp: not_less nat_le_iff_add) |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
605 |
then have "k<n" |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
606 |
by simp |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
607 |
with less assms have "P (k+2)" |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
608 |
by blast |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
609 |
then show ?thesis |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
610 |
by (simp add: k) |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
611 |
qed |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
612 |
qed |
58687 | 613 |
|
71138 | 614 |
|
60758 | 615 |
subsection \<open>Parity and powers\<close> |
58689 | 616 |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
617 |
context ring_1 |
58689 | 618 |
begin |
619 |
||
63654 | 620 |
lemma power_minus_even [simp]: "even n \<Longrightarrow> (- a) ^ n = a ^ n" |
58690 | 621 |
by (auto elim: evenE) |
58689 | 622 |
|
63654 | 623 |
lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)" |
58690 | 624 |
by (auto elim: oddE) |
625 |
||
66815 | 626 |
lemma uminus_power_if: |
627 |
"(- a) ^ n = (if even n then a ^ n else - (a ^ n))" |
|
628 |
by auto |
|
629 |
||
63654 | 630 |
lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1" |
58690 | 631 |
by simp |
58689 | 632 |
|
63654 | 633 |
lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1" |
58690 | 634 |
by simp |
58689 | 635 |
|
66582 | 636 |
lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)" |
637 |
by (cases "even (n + k)") auto |
|
638 |
||
67371
2d9cf74943e1
moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents:
67083
diff
changeset
|
639 |
lemma minus_one_power_iff: "(- 1) ^ n = (if even n then 1 else - 1)" |
2d9cf74943e1
moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents:
67083
diff
changeset
|
640 |
by (induct n) auto |
2d9cf74943e1
moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents:
67083
diff
changeset
|
641 |
|
63654 | 642 |
end |
58689 | 643 |
|
644 |
context linordered_idom |
|
645 |
begin |
|
646 |
||
63654 | 647 |
lemma zero_le_even_power: "even n \<Longrightarrow> 0 \<le> a ^ n" |
58690 | 648 |
by (auto elim: evenE) |
58689 | 649 |
|
63654 | 650 |
lemma zero_le_odd_power: "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a" |
58689 | 651 |
by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) |
652 |
||
63654 | 653 |
lemma zero_le_power_eq: "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a" |
58787 | 654 |
by (auto simp add: zero_le_even_power zero_le_odd_power) |
63654 | 655 |
|
656 |
lemma zero_less_power_eq: "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a" |
|
58689 | 657 |
proof - |
658 |
have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0" |
|
58787 | 659 |
unfolding power_eq_0_iff [of a n, symmetric] by blast |
58689 | 660 |
show ?thesis |
63654 | 661 |
unfolding less_le zero_le_power_eq by auto |
58689 | 662 |
qed |
663 |
||
63654 | 664 |
lemma power_less_zero_eq [simp]: "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0" |
58689 | 665 |
unfolding not_le [symmetric] zero_le_power_eq by auto |
666 |
||
63654 | 667 |
lemma power_le_zero_eq: "a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)" |
668 |
unfolding not_less [symmetric] zero_less_power_eq by auto |
|
669 |
||
670 |
lemma power_even_abs: "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n" |
|
58689 | 671 |
using power_abs [of a n] by (simp add: zero_le_even_power) |
672 |
||
673 |
lemma power_mono_even: |
|
674 |
assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>" |
|
675 |
shows "a ^ n \<le> b ^ n" |
|
676 |
proof - |
|
677 |
have "0 \<le> \<bar>a\<bar>" by auto |
|
63654 | 678 |
with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close> have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n" |
679 |
by (rule power_mono) |
|
680 |
with \<open>even n\<close> show ?thesis |
|
681 |
by (simp add: power_even_abs) |
|
58689 | 682 |
qed |
683 |
||
684 |
lemma power_mono_odd: |
|
685 |
assumes "odd n" and "a \<le> b" |
|
686 |
shows "a ^ n \<le> b ^ n" |
|
687 |
proof (cases "b < 0") |
|
63654 | 688 |
case True |
689 |
with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto |
|
690 |
then have "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono) |
|
60758 | 691 |
with \<open>odd n\<close> show ?thesis by simp |
58689 | 692 |
next |
63654 | 693 |
case False |
694 |
then have "0 \<le> b" by auto |
|
58689 | 695 |
show ?thesis |
696 |
proof (cases "a < 0") |
|
63654 | 697 |
case True |
698 |
then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto |
|
60758 | 699 |
then have "a ^ n \<le> 0" unfolding power_le_zero_eq using \<open>odd n\<close> by auto |
63654 | 700 |
moreover from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto |
58689 | 701 |
ultimately show ?thesis by auto |
702 |
next |
|
63654 | 703 |
case False |
704 |
then have "0 \<le> a" by auto |
|
705 |
with \<open>a \<le> b\<close> show ?thesis |
|
706 |
using power_mono by auto |
|
58689 | 707 |
qed |
708 |
qed |
|
62083 | 709 |
|
60758 | 710 |
text \<open>Simplify, when the exponent is a numeral\<close> |
58689 | 711 |
|
712 |
lemma zero_le_power_eq_numeral [simp]: |
|
713 |
"0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a" |
|
714 |
by (fact zero_le_power_eq) |
|
715 |
||
716 |
lemma zero_less_power_eq_numeral [simp]: |
|
63654 | 717 |
"0 < a ^ numeral w \<longleftrightarrow> |
718 |
numeral w = (0 :: nat) \<or> |
|
719 |
even (numeral w :: nat) \<and> a \<noteq> 0 \<or> |
|
720 |
odd (numeral w :: nat) \<and> 0 < a" |
|
58689 | 721 |
by (fact zero_less_power_eq) |
722 |
||
723 |
lemma power_le_zero_eq_numeral [simp]: |
|
63654 | 724 |
"a ^ numeral w \<le> 0 \<longleftrightarrow> |
725 |
(0 :: nat) < numeral w \<and> |
|
726 |
(odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)" |
|
58689 | 727 |
by (fact power_le_zero_eq) |
728 |
||
729 |
lemma power_less_zero_eq_numeral [simp]: |
|
730 |
"a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0" |
|
731 |
by (fact power_less_zero_eq) |
|
732 |
||
733 |
lemma power_even_abs_numeral [simp]: |
|
734 |
"even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w" |
|
735 |
by (fact power_even_abs) |
|
736 |
||
737 |
end |
|
738 |
||
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
739 |
|
69593 | 740 |
subsection \<open>Instance for \<^typ>\<open>int\<close>\<close> |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
741 |
|
70340 | 742 |
instance int :: unique_euclidean_ring_with_nat |
66839 | 743 |
by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def) |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
744 |
|
67816 | 745 |
lemma even_diff_iff: |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
746 |
"even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int |
67816 | 747 |
by (fact even_diff) |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
748 |
|
67816 | 749 |
lemma even_abs_add_iff: |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
750 |
"even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int |
67816 | 751 |
by simp |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
752 |
|
67816 | 753 |
lemma even_add_abs_iff: |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
754 |
"even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int |
67816 | 755 |
by simp |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
756 |
|
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
757 |
lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k" |
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
758 |
by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric]) |
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
759 |
|
71138 | 760 |
lemma zdiv_zmult2_eq: |
761 |
\<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int |
|
762 |
proof (cases \<open>b \<ge> 0\<close>) |
|
763 |
case True |
|
764 |
with that show ?thesis |
|
765 |
using div_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp |
|
766 |
next |
|
767 |
case False |
|
768 |
with that show ?thesis |
|
769 |
using div_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp |
|
770 |
qed |
|
771 |
||
772 |
lemma zmod_zmult2_eq: |
|
773 |
\<open>a mod (b * c) = b * (a div b mod c) + a mod b\<close> if \<open>c \<ge> 0\<close> for a b c :: int |
|
774 |
proof (cases \<open>b \<ge> 0\<close>) |
|
775 |
case True |
|
776 |
with that show ?thesis |
|
777 |
using mod_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp |
|
778 |
next |
|
779 |
case False |
|
780 |
with that show ?thesis |
|
781 |
using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp |
|
782 |
qed |
|
783 |
||
71094 | 784 |
|
785 |
subsection \<open>Abstract bit shifts\<close> |
|
786 |
||
787 |
class semiring_bits = semiring_parity + |
|
71138 | 788 |
assumes bit_eq_rec: \<open>a = b \<longleftrightarrow> (even a = even b) \<and> a div 2 = b div 2\<close> |
71094 | 789 |
and bit_induct [case_names stable rec]: |
790 |
\<open>(\<And>a. a div 2 = a \<Longrightarrow> P a) |
|
791 |
\<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)) |
|
792 |
\<Longrightarrow> P a\<close> |
|
71138 | 793 |
assumes bits_div_0 [simp]: \<open>0 div a = 0\<close> |
794 |
and bits_div_by_1 [simp]: \<open>a div 1 = a\<close> |
|
795 |
and bit_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close> |
|
796 |
and even_succ_div_2 [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close> |
|
797 |
and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close> |
|
798 |
and mod_exp_eq: \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close> |
|
799 |
and mult_exp_mod_exp_eq: \<open>m \<le> n \<Longrightarrow> (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\<close> |
|
800 |
and div_exp_mod_exp_eq: \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close> |
|
801 |
begin |
|
802 |
||
803 |
lemma bits_1_div_2 [simp]: |
|
804 |
\<open>1 div 2 = 0\<close> |
|
805 |
using even_succ_div_2 [of 0] by simp |
|
806 |
||
807 |
lemma bits_1_div_exp [simp]: |
|
808 |
\<open>1 div 2 ^ n = of_bool (n = 0)\<close> |
|
809 |
using div_exp_eq [of 1 1] by (cases n) simp_all |
|
810 |
||
811 |
lemma even_succ_div_exp [simp]: |
|
812 |
\<open>(1 + a) div 2 ^ n = a div 2 ^ n\<close> if \<open>even a\<close> and \<open>n > 0\<close> |
|
813 |
proof (cases n) |
|
814 |
case 0 |
|
815 |
with that show ?thesis |
|
816 |
by simp |
|
817 |
next |
|
818 |
case (Suc n) |
|
819 |
with \<open>even a\<close> have \<open>(1 + a) div 2 ^ Suc n = a div 2 ^ Suc n\<close> |
|
820 |
proof (induction n) |
|
821 |
case 0 |
|
822 |
then show ?case |
|
823 |
by simp |
|
824 |
next |
|
825 |
case (Suc n) |
|
826 |
then show ?case |
|
827 |
using div_exp_eq [of _ 1 \<open>Suc n\<close>, symmetric] |
|
828 |
by simp |
|
829 |
qed |
|
830 |
with Suc show ?thesis |
|
831 |
by simp |
|
832 |
qed |
|
833 |
||
834 |
lemma even_succ_mod_exp [simp]: |
|
835 |
\<open>(1 + a) mod 2 ^ n = 1 + (a mod 2 ^ n)\<close> if \<open>even a\<close> and \<open>n > 0\<close> |
|
836 |
using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] that |
|
837 |
apply simp |
|
838 |
by (metis local.add.left_commute local.add_left_cancel local.div_mult_mod_eq) |
|
839 |
||
840 |
lemma bits_mod_by_1 [simp]: |
|
841 |
\<open>a mod 1 = 0\<close> |
|
842 |
using div_mult_mod_eq [of a 1] by simp |
|
843 |
||
844 |
lemma bits_mod_0 [simp]: |
|
845 |
\<open>0 mod a = 0\<close> |
|
846 |
using div_mult_mod_eq [of 0 a] by simp |
|
847 |
||
848 |
lemma one_mod_two_eq_one [simp]: |
|
849 |
\<open>1 mod 2 = 1\<close> |
|
850 |
by (simp add: mod2_eq_if) |
|
851 |
||
852 |
end |
|
71094 | 853 |
|
854 |
lemma nat_bit_induct [case_names zero even odd]: |
|
855 |
"P n" if zero: "P 0" |
|
856 |
and even: "\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)" |
|
857 |
and odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))" |
|
858 |
proof (induction n rule: less_induct) |
|
859 |
case (less n) |
|
860 |
show "P n" |
|
861 |
proof (cases "n = 0") |
|
862 |
case True with zero show ?thesis by simp |
|
863 |
next |
|
864 |
case False |
|
865 |
with less have hyp: "P (n div 2)" by simp |
|
866 |
show ?thesis |
|
867 |
proof (cases "even n") |
|
868 |
case True |
|
869 |
then have "n \<noteq> 1" |
|
870 |
by auto |
|
871 |
with \<open>n \<noteq> 0\<close> have "n div 2 > 0" |
|
872 |
by simp |
|
873 |
with \<open>even n\<close> hyp even [of "n div 2"] show ?thesis |
|
874 |
by simp |
|
875 |
next |
|
876 |
case False |
|
877 |
with hyp odd [of "n div 2"] show ?thesis |
|
878 |
by simp |
|
879 |
qed |
|
880 |
qed |
|
881 |
qed |
|
882 |
||
883 |
instance nat :: semiring_bits |
|
884 |
proof |
|
885 |
show \<open>m = n \<longleftrightarrow> (even m \<longleftrightarrow> even n) \<and> m div 2 = n div 2\<close> |
|
886 |
for m n :: nat |
|
887 |
by (auto dest: odd_two_times_div_two_succ) |
|
888 |
show \<open>P n\<close> if stable: \<open>\<And>n. n div 2 = n \<Longrightarrow> P n\<close> |
|
889 |
and rec: \<open>\<And>n b. P n \<Longrightarrow> (of_bool b + 2 * n) div 2 = n \<Longrightarrow> P (of_bool b + 2 * n)\<close> |
|
890 |
for P and n :: nat |
|
891 |
proof (induction n rule: nat_bit_induct) |
|
892 |
case zero |
|
893 |
from stable [of 0] show ?case |
|
894 |
by simp |
|
895 |
next |
|
896 |
case (even n) |
|
897 |
with rec [of n False] show ?case |
|
898 |
by simp |
|
899 |
next |
|
900 |
case (odd n) |
|
901 |
with rec [of n True] show ?case |
|
902 |
by simp |
|
903 |
qed |
|
71138 | 904 |
show \<open>q mod 2 ^ m mod 2 ^ n = q mod 2 ^ min m n\<close> |
905 |
for q m n :: nat |
|
906 |
apply (auto simp add: less_iff_Suc_add power_add mod_mod_cancel split: split_min_lin) |
|
907 |
apply (metis div_mult2_eq mod_div_trivial mod_eq_self_iff_div_eq_0 mod_mult_self2_is_0 power_commutes) |
|
908 |
done |
|
909 |
show \<open>(q * 2 ^ m) mod (2 ^ n) = (q mod 2 ^ (n - m)) * 2 ^ m\<close> if \<open>m \<le> n\<close> |
|
910 |
for q m n :: nat |
|
911 |
using that |
|
912 |
apply (auto simp add: mod_mod_cancel div_mult2_eq power_add mod_mult2_eq le_iff_add split: split_min_lin) |
|
913 |
apply (simp add: mult.commute) |
|
914 |
done |
|
915 |
qed (auto simp add: div_mult2_eq mod_mult2_eq power_add) |
|
71094 | 916 |
|
70353 | 917 |
lemma int_bit_induct [case_names zero minus even odd]: |
70338 | 918 |
"P k" if zero_int: "P 0" |
919 |
and minus_int: "P (- 1)" |
|
920 |
and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)" |
|
921 |
and odd_int: "\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))" for k :: int |
|
922 |
proof (cases "k \<ge> 0") |
|
923 |
case True |
|
924 |
define n where "n = nat k" |
|
925 |
with True have "k = int n" |
|
926 |
by simp |
|
927 |
then show "P k" |
|
70353 | 928 |
proof (induction n arbitrary: k rule: nat_bit_induct) |
70338 | 929 |
case zero |
930 |
then show ?case |
|
931 |
by (simp add: zero_int) |
|
932 |
next |
|
933 |
case (even n) |
|
934 |
have "P (int n * 2)" |
|
935 |
by (rule even_int) (use even in simp_all) |
|
936 |
with even show ?case |
|
937 |
by (simp add: ac_simps) |
|
938 |
next |
|
939 |
case (odd n) |
|
940 |
have "P (1 + (int n * 2))" |
|
941 |
by (rule odd_int) (use odd in simp_all) |
|
942 |
with odd show ?case |
|
943 |
by (simp add: ac_simps) |
|
944 |
qed |
|
945 |
next |
|
946 |
case False |
|
947 |
define n where "n = nat (- k - 1)" |
|
948 |
with False have "k = - int n - 1" |
|
949 |
by simp |
|
950 |
then show "P k" |
|
70353 | 951 |
proof (induction n arbitrary: k rule: nat_bit_induct) |
70338 | 952 |
case zero |
953 |
then show ?case |
|
954 |
by (simp add: minus_int) |
|
955 |
next |
|
956 |
case (even n) |
|
957 |
have "P (1 + (- int (Suc n) * 2))" |
|
958 |
by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>) |
|
959 |
also have "\<dots> = - int (2 * n) - 1" |
|
960 |
by (simp add: algebra_simps) |
|
961 |
finally show ?case |
|
962 |
using even by simp |
|
963 |
next |
|
964 |
case (odd n) |
|
965 |
have "P (- int (Suc n) * 2)" |
|
966 |
by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>) |
|
967 |
also have "\<dots> = - int (Suc (2 * n)) - 1" |
|
968 |
by (simp add: algebra_simps) |
|
969 |
finally show ?case |
|
970 |
using odd by simp |
|
971 |
qed |
|
972 |
qed |
|
973 |
||
71094 | 974 |
instance int :: semiring_bits |
975 |
proof |
|
976 |
show \<open>k = l \<longleftrightarrow> (even k \<longleftrightarrow> even l) \<and> k div 2 = l div 2\<close> |
|
977 |
for k l :: int |
|
978 |
by (auto dest: odd_two_times_div_two_succ) |
|
979 |
show \<open>P k\<close> if stable: \<open>\<And>k. k div 2 = k \<Longrightarrow> P k\<close> |
|
980 |
and rec: \<open>\<And>k b. P k \<Longrightarrow> (of_bool b + 2 * k) div 2 = k \<Longrightarrow> P (of_bool b + 2 * k)\<close> |
|
981 |
for P and k :: int |
|
982 |
proof (induction k rule: int_bit_induct) |
|
983 |
case zero |
|
984 |
from stable [of 0] show ?case |
|
985 |
by simp |
|
986 |
next |
|
987 |
case minus |
|
988 |
from stable [of \<open>- 1\<close>] show ?case |
|
989 |
by simp |
|
990 |
next |
|
991 |
case (even k) |
|
992 |
with rec [of k False] show ?case |
|
993 |
by (simp add: ac_simps) |
|
994 |
next |
|
995 |
case (odd k) |
|
996 |
with rec [of k True] show ?case |
|
997 |
by (simp add: ac_simps) |
|
998 |
qed |
|
71138 | 999 |
show \<open>k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n\<close> |
1000 |
for m n :: nat and k :: int |
|
1001 |
using mod_exp_eq [of \<open>nat k\<close> m n] |
|
1002 |
apply (auto simp add: mod_mod_cancel zdiv_zmult2_eq power_add zmod_zmult2_eq le_iff_add split: split_min_lin) |
|
1003 |
apply (auto simp add: less_iff_Suc_add mod_mod_cancel power_add) |
|
1004 |
apply (simp only: flip: mult.left_commute [of \<open>2 ^ m\<close>]) |
|
1005 |
apply (subst zmod_zmult2_eq) apply simp_all |
|
1006 |
done |
|
1007 |
show \<open>(k * 2 ^ m) mod (2 ^ n) = (k mod 2 ^ (n - m)) * 2 ^ m\<close> |
|
1008 |
if \<open>m \<le> n\<close> for m n :: nat and k :: int |
|
1009 |
using that |
|
1010 |
apply (auto simp add: power_add zmod_zmult2_eq le_iff_add split: split_min_lin) |
|
1011 |
apply (simp add: ac_simps) |
|
1012 |
done |
|
1013 |
qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add) |
|
67816 | 1014 |
|
71094 | 1015 |
class semiring_bit_shifts = semiring_bits + |
1016 |
fixes push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> |
|
1017 |
assumes push_bit_eq_mult: \<open>push_bit n a = a * 2 ^ n\<close> |
|
1018 |
fixes drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> |
|
1019 |
assumes drop_bit_eq_div: \<open>drop_bit n a = a div 2 ^ n\<close> |
|
67816 | 1020 |
begin |
1021 |
||
71094 | 1022 |
definition take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> |
1023 |
where take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close> |
|
67816 | 1024 |
|
71094 | 1025 |
text \<open> |
1026 |
Logically, \<^const>\<open>push_bit\<close>, |
|
1027 |
\<^const>\<open>drop_bit\<close> and \<^const>\<open>take_bit\<close> are just aliases; having them |
|
1028 |
as separate operations makes proofs easier, otherwise proof automation |
|
1029 |
would fiddle with concrete expressions \<^term>\<open>2 ^ n\<close> in a way obfuscating the basic |
|
1030 |
algebraic relationships between those operations. |
|
1031 |
Having |
|
1032 |
\<^const>\<open>push_bit\<close> and \<^const>\<open>drop_bit\<close> as definitional class operations |
|
1033 |
takes into account that specific instances of these can be implemented |
|
1034 |
differently wrt. code generation. |
|
1035 |
\<close> |
|
67816 | 1036 |
|
71138 | 1037 |
lemma bit_ident: |
1038 |
"push_bit n (drop_bit n a) + take_bit n a = a" |
|
1039 |
using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div) |
|
1040 |
||
1041 |
lemma push_bit_push_bit [simp]: |
|
1042 |
"push_bit m (push_bit n a) = push_bit (m + n) a" |
|
1043 |
by (simp add: push_bit_eq_mult power_add ac_simps) |
|
1044 |
||
1045 |
lemma push_bit_0_id [simp]: |
|
1046 |
"push_bit 0 = id" |
|
1047 |
by (simp add: fun_eq_iff push_bit_eq_mult) |
|
1048 |
||
1049 |
lemma push_bit_of_0 [simp]: |
|
1050 |
"push_bit n 0 = 0" |
|
1051 |
by (simp add: push_bit_eq_mult) |
|
1052 |
||
1053 |
lemma push_bit_of_1: |
|
1054 |
"push_bit n 1 = 2 ^ n" |
|
1055 |
by (simp add: push_bit_eq_mult) |
|
1056 |
||
1057 |
lemma push_bit_Suc [simp]: |
|
1058 |
"push_bit (Suc n) a = push_bit n (a * 2)" |
|
1059 |
by (simp add: push_bit_eq_mult ac_simps) |
|
1060 |
||
1061 |
lemma push_bit_double: |
|
1062 |
"push_bit n (a * 2) = push_bit n a * 2" |
|
1063 |
by (simp add: push_bit_eq_mult ac_simps) |
|
1064 |
||
1065 |
lemma push_bit_add: |
|
1066 |
"push_bit n (a + b) = push_bit n a + push_bit n b" |
|
1067 |
by (simp add: push_bit_eq_mult algebra_simps) |
|
1068 |
||
1069 |
lemma take_bit_0 [simp]: |
|
1070 |
"take_bit 0 a = 0" |
|
1071 |
by (simp add: take_bit_eq_mod) |
|
1072 |
||
1073 |
lemma take_bit_Suc [simp]: |
|
1074 |
\<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)\<close> |
|
1075 |
proof - |
|
1076 |
have \<open>take_bit (Suc n) (a div 2 * 2 + of_bool (odd a)) = take_bit n (a div 2) * 2 + of_bool (odd a)\<close> |
|
1077 |
using even_succ_mod_exp [of \<open>2 * (a div 2)\<close> \<open>Suc n\<close>] |
|
1078 |
mult_exp_mod_exp_eq [of 1 \<open>Suc n\<close> \<open>a div 2\<close>] |
|
1079 |
by (auto simp add: take_bit_eq_mod ac_simps) |
|
1080 |
then show ?thesis |
|
1081 |
using div_mult_mod_eq [of a 2] by (simp add: mod_2_eq_odd) |
|
1082 |
qed |
|
1083 |
||
1084 |
lemma take_bit_of_0 [simp]: |
|
1085 |
"take_bit n 0 = 0" |
|
1086 |
by (simp add: take_bit_eq_mod) |
|
1087 |
||
1088 |
lemma take_bit_of_1 [simp]: |
|
1089 |
"take_bit n 1 = of_bool (n > 0)" |
|
1090 |
by (cases n) simp_all |
|
1091 |
||
1092 |
lemma drop_bit_of_0 [simp]: |
|
1093 |
"drop_bit n 0 = 0" |
|
1094 |
by (simp add: drop_bit_eq_div) |
|
1095 |
||
1096 |
lemma drop_bit_of_1 [simp]: |
|
1097 |
"drop_bit n 1 = of_bool (n = 0)" |
|
1098 |
by (simp add: drop_bit_eq_div) |
|
1099 |
||
1100 |
lemma drop_bit_0 [simp]: |
|
1101 |
"drop_bit 0 = id" |
|
1102 |
by (simp add: fun_eq_iff drop_bit_eq_div) |
|
1103 |
||
1104 |
lemma drop_bit_Suc [simp]: |
|
1105 |
"drop_bit (Suc n) a = drop_bit n (a div 2)" |
|
1106 |
using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div) |
|
1107 |
||
1108 |
lemma drop_bit_half: |
|
1109 |
"drop_bit n (a div 2) = drop_bit n a div 2" |
|
1110 |
by (induction n arbitrary: a) simp_all |
|
1111 |
||
1112 |
lemma drop_bit_of_bool [simp]: |
|
1113 |
"drop_bit n (of_bool d) = of_bool (n = 0 \<and> d)" |
|
1114 |
by (cases n) simp_all |
|
1115 |
||
1116 |
lemma take_bit_eq_0_imp_dvd: |
|
1117 |
"take_bit n a = 0 \<Longrightarrow> 2 ^ n dvd a" |
|
1118 |
by (simp add: take_bit_eq_mod mod_0_imp_dvd) |
|
1119 |
||
1120 |
lemma even_take_bit_eq [simp]: |
|
1121 |
\<open>even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a\<close> |
|
1122 |
by (cases n) simp_all |
|
1123 |
||
1124 |
lemma take_bit_take_bit [simp]: |
|
1125 |
"take_bit m (take_bit n a) = take_bit (min m n) a" |
|
1126 |
by (simp add: take_bit_eq_mod mod_exp_eq ac_simps) |
|
1127 |
||
1128 |
lemma drop_bit_drop_bit [simp]: |
|
1129 |
"drop_bit m (drop_bit n a) = drop_bit (m + n) a" |
|
1130 |
by (simp add: drop_bit_eq_div power_add div_exp_eq ac_simps) |
|
1131 |
||
1132 |
lemma push_bit_take_bit: |
|
1133 |
"push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)" |
|
1134 |
apply (simp add: push_bit_eq_mult take_bit_eq_mod power_add ac_simps) |
|
1135 |
using mult_exp_mod_exp_eq [of m \<open>m + n\<close> a] apply (simp add: ac_simps power_add) |
|
1136 |
done |
|
1137 |
||
1138 |
lemma take_bit_push_bit: |
|
1139 |
"take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)" |
|
1140 |
proof (cases "m \<le> n") |
|
1141 |
case True |
|
1142 |
then show ?thesis |
|
1143 |
apply (simp add:) |
|
1144 |
apply (simp_all add: push_bit_eq_mult take_bit_eq_mod) |
|
1145 |
apply (auto dest!: le_Suc_ex simp add: power_add ac_simps) |
|
1146 |
using mult_exp_mod_exp_eq [of m m \<open>a * 2 ^ n\<close> for n] |
|
1147 |
apply (simp add: ac_simps) |
|
1148 |
done |
|
1149 |
next |
|
1150 |
case False |
|
1151 |
then show ?thesis |
|
1152 |
using push_bit_take_bit [of n "m - n" a] |
|
1153 |
by simp |
|
1154 |
qed |
|
1155 |
||
1156 |
lemma take_bit_drop_bit: |
|
1157 |
"take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)" |
|
1158 |
by (simp add: drop_bit_eq_div take_bit_eq_mod ac_simps div_exp_mod_exp_eq) |
|
1159 |
||
1160 |
lemma drop_bit_take_bit: |
|
1161 |
"drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)" |
|
1162 |
proof (cases "m \<le> n") |
|
1163 |
case True |
|
1164 |
then show ?thesis |
|
1165 |
using take_bit_drop_bit [of "n - m" m a] by simp |
|
1166 |
next |
|
1167 |
case False |
|
1168 |
then obtain q where \<open>m = n + q\<close> |
|
1169 |
by (auto simp add: not_le dest: less_imp_Suc_add) |
|
1170 |
then have \<open>drop_bit m (take_bit n a) = 0\<close> |
|
1171 |
using div_exp_eq [of \<open>a mod 2 ^ n\<close> n q] |
|
1172 |
by (simp add: take_bit_eq_mod drop_bit_eq_div) |
|
1173 |
with False show ?thesis |
|
1174 |
by simp |
|
1175 |
qed |
|
1176 |
||
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
1177 |
end |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
1178 |
|
71094 | 1179 |
instantiation nat :: semiring_bit_shifts |
1180 |
begin |
|
1181 |
||
1182 |
definition push_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close> |
|
1183 |
where \<open>push_bit_nat n m = m * 2 ^ n\<close> |
|
1184 |
||
1185 |
definition drop_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close> |
|
1186 |
where \<open>drop_bit_nat n m = m div 2 ^ n\<close> |
|
1187 |
||
1188 |
instance proof |
|
1189 |
show \<open>push_bit n m = m * 2 ^ n\<close> for n m :: nat |
|
1190 |
by (simp add: push_bit_nat_def) |
|
1191 |
show \<open>drop_bit n m = m div 2 ^ n\<close> for n m :: nat |
|
1192 |
by (simp add: drop_bit_nat_def) |
|
1193 |
qed |
|
1194 |
||
1195 |
end |
|
1196 |
||
1197 |
instantiation int :: semiring_bit_shifts |
|
1198 |
begin |
|
1199 |
||
1200 |
definition push_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close> |
|
1201 |
where \<open>push_bit_int n k = k * 2 ^ n\<close> |
|
1202 |
||
1203 |
definition drop_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close> |
|
1204 |
where \<open>drop_bit_int n k = k div 2 ^ n\<close> |
|
1205 |
||
1206 |
instance proof |
|
1207 |
show \<open>push_bit n k = k * 2 ^ n\<close> for n :: nat and k :: int |
|
1208 |
by (simp add: push_bit_int_def) |
|
1209 |
show \<open>drop_bit n k = k div 2 ^ n\<close> for n :: nat and k :: int |
|
1210 |
by (simp add: drop_bit_int_def) |
|
1211 |
qed |
|
1212 |
||
1213 |
end |
|
1214 |
||
1215 |
class unique_euclidean_semiring_with_bit_shifts = |
|
1216 |
unique_euclidean_semiring_with_nat + semiring_bit_shifts |
|
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
1217 |
begin |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
1218 |
|
71138 | 1219 |
lemma take_bit_of_exp [simp]: |
1220 |
\<open>take_bit m (2 ^ n) = of_bool (n < m) * 2 ^ n\<close> |
|
1221 |
by (simp add: take_bit_eq_mod exp_mod_exp) |
|
67960 | 1222 |
|
71138 | 1223 |
lemma take_bit_of_2 [simp]: |
1224 |
\<open>take_bit n 2 = of_bool (2 \<le> n) * 2\<close> |
|
1225 |
using take_bit_of_exp [of n 1] by simp |
|
67988
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1226 |
|
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1227 |
lemma push_bit_eq_0_iff [simp]: |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1228 |
"push_bit n a = 0 \<longleftrightarrow> a = 0" |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1229 |
by (simp add: push_bit_eq_mult) |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1230 |
|
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1231 |
lemma push_bit_numeral [simp]: |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1232 |
"push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))" |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1233 |
by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric]) (simp add: ac_simps) |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1234 |
|
68010 | 1235 |
lemma push_bit_of_nat: |
1236 |
"push_bit n (of_nat m) = of_nat (push_bit n m)" |
|
1237 |
by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult) |
|
1238 |
||
67961 | 1239 |
lemma take_bit_add: |
67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67906
diff
changeset
|
1240 |
"take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)" |
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67906
diff
changeset
|
1241 |
by (simp add: take_bit_eq_mod mod_simps) |
67816 | 1242 |
|
67961 | 1243 |
lemma take_bit_eq_0_iff: |
1244 |
"take_bit n a = 0 \<longleftrightarrow> 2 ^ n dvd a" |
|
1245 |
by (simp add: take_bit_eq_mod mod_eq_0_iff_dvd) |
|
1246 |
||
67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67906
diff
changeset
|
1247 |
lemma take_bit_of_1_eq_0_iff [simp]: |
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67906
diff
changeset
|
1248 |
"take_bit n 1 = 0 \<longleftrightarrow> n = 0" |
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67906
diff
changeset
|
1249 |
by (simp add: take_bit_eq_mod) |
67816 | 1250 |
|
67988
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1251 |
lemma take_bit_numeral_bit0 [simp]: |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1252 |
"take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2" |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1253 |
by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] take_bit_Suc |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1254 |
ac_simps even_mult_iff nonzero_mult_div_cancel_right [OF numeral_neq_zero]) simp |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1255 |
|
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1256 |
lemma take_bit_numeral_bit1 [simp]: |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1257 |
"take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1" |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1258 |
by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] take_bit_Suc |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1259 |
ac_simps even_add even_mult_iff div_mult_self1 [OF numeral_neq_zero]) (simp add: ac_simps) |
67961 | 1260 |
|
68010 | 1261 |
lemma take_bit_of_nat: |
1262 |
"take_bit n (of_nat m) = of_nat (take_bit n m)" |
|
1263 |
by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"]) |
|
1264 |
||
67988
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1265 |
lemma drop_bit_numeral_bit0 [simp]: |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1266 |
"drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)" |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1267 |
by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] drop_bit_Suc |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1268 |
nonzero_mult_div_cancel_left [OF numeral_neq_zero]) |
67816 | 1269 |
|
67988
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1270 |
lemma drop_bit_numeral_bit1 [simp]: |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1271 |
"drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)" |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1272 |
by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] drop_bit_Suc |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1273 |
div_mult_self4 [OF numeral_neq_zero]) simp |
67816 | 1274 |
|
68010 | 1275 |
lemma drop_bit_of_nat: |
1276 |
"drop_bit n (of_nat m) = of_nat (drop_bit n m)" |
|
68389 | 1277 |
by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"]) |
68010 | 1278 |
|
58770 | 1279 |
end |
67816 | 1280 |
|
71094 | 1281 |
instance nat :: unique_euclidean_semiring_with_bit_shifts .. |
1282 |
||
1283 |
instance int :: unique_euclidean_semiring_with_bit_shifts .. |
|
1284 |
||
67988
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1285 |
lemma push_bit_of_Suc_0 [simp]: |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1286 |
"push_bit n (Suc 0) = 2 ^ n" |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1287 |
using push_bit_of_1 [where ?'a = nat] by simp |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1288 |
|
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1289 |
lemma take_bit_of_Suc_0 [simp]: |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1290 |
"take_bit n (Suc 0) = of_bool (0 < n)" |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1291 |
using take_bit_of_1 [where ?'a = nat] by simp |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1292 |
|
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1293 |
lemma drop_bit_of_Suc_0 [simp]: |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1294 |
"drop_bit n (Suc 0) = of_bool (n = 0)" |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1295 |
using drop_bit_of_1 [where ?'a = nat] by simp |
01c651412081
explicit simp rules for computing abstract bit operations
haftmann
parents:
67961
diff
changeset
|
1296 |
|
70973 | 1297 |
lemma take_bit_eq_self: |
1298 |
\<open>take_bit n m = m\<close> if \<open>m < 2 ^ n\<close> for n m :: nat |
|
1299 |
using that by (simp add: take_bit_eq_mod) |
|
1300 |
||
70911 | 1301 |
lemma push_bit_minus_one: |
1302 |
"push_bit n (- 1 :: int) = - (2 ^ n)" |
|
1303 |
by (simp add: push_bit_eq_mult) |
|
1304 |
||
67816 | 1305 |
end |