author | haftmann |
Thu, 02 Jul 2020 08:49:04 +0000 | |
changeset 71988 | ace45a11a45e |
parent 71965 | d45f5d4c41bd |
child 72082 | 41393ecb57ac |
permissions | -rw-r--r-- |
70342
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset
|
1 |
(* Title: HOL/Library/Z2.thy |
41959 | 2 |
Author: Brian Huffman |
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
3 |
*) |
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
4 |
|
60500 | 5 |
section \<open>The Field of Integers mod 2\<close> |
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
6 |
|
70342
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset
|
7 |
theory Z2 |
71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset
|
8 |
imports Main "HOL-Library.Bit_Operations" |
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
9 |
begin |
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
10 |
|
70342
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset
|
11 |
text \<open> |
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset
|
12 |
Note that in most cases \<^typ>\<open>bool\<close> is appropriate hen a binary type is needed; the |
70351 | 13 |
type provided here, for historical reasons named \<^text>\<open>bit\<close>, is only needed if proper |
70342
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset
|
14 |
field operations are required. |
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset
|
15 |
\<close> |
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset
|
16 |
|
71988 | 17 |
typedef bit = \<open>UNIV :: bool set\<close> .. |
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
18 |
|
71988 | 19 |
instantiation bit :: zero_neq_one |
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
20 |
begin |
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
21 |
|
71988 | 22 |
definition zero_bit :: bit |
23 |
where \<open>0 = Abs_bit False\<close> |
|
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
24 |
|
71988 | 25 |
definition one_bit :: bit |
26 |
where \<open>1 = Abs_bit True\<close> |
|
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
27 |
|
71988 | 28 |
instance |
29 |
by standard (simp add: zero_bit_def one_bit_def Abs_bit_inject) |
|
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
30 |
|
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
31 |
end |
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
32 |
|
71988 | 33 |
free_constructors case_bit for \<open>0::bit\<close> | \<open>1::bit\<close> |
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
34 |
proof - |
71988 | 35 |
fix P :: bool |
36 |
fix a :: bit |
|
37 |
assume \<open>a = 0 \<Longrightarrow> P\<close> and \<open>a = 1 \<Longrightarrow> P\<close> |
|
38 |
then show P |
|
39 |
by (cases a) (auto simp add: zero_bit_def one_bit_def Abs_bit_inject) |
|
40 |
qed simp |
|
41 |
||
42 |
lemma bit_not_zero_iff [simp]: |
|
43 |
\<open>a \<noteq> 0 \<longleftrightarrow> a = 1\<close> for a :: bit |
|
44 |
by (cases a) simp_all |
|
45 |
||
46 |
lemma bit_not_one_imp [simp]: |
|
47 |
\<open>a \<noteq> 1 \<longleftrightarrow> a = 0\<close> for a :: bit |
|
48 |
by (cases a) simp_all |
|
49 |
||
50 |
instantiation bit :: semidom_modulo |
|
51 |
begin |
|
52 |
||
53 |
definition plus_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> |
|
54 |
where \<open>a + b = Abs_bit (Rep_bit a \<noteq> Rep_bit b)\<close> |
|
55 |
||
56 |
definition minus_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> |
|
57 |
where [simp]: \<open>minus_bit = plus\<close> |
|
58 |
||
59 |
definition times_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> |
|
60 |
where \<open>a * b = Abs_bit (Rep_bit a \<and> Rep_bit b)\<close> |
|
61 |
||
62 |
definition divide_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> |
|
63 |
where [simp]: \<open>divide_bit = times\<close> |
|
64 |
||
65 |
definition modulo_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> |
|
66 |
where \<open>a mod b = Abs_bit (Rep_bit a \<and> \<not> Rep_bit b)\<close> |
|
67 |
||
68 |
instance |
|
69 |
by standard |
|
70 |
(auto simp flip: Rep_bit_inject |
|
71 |
simp add: zero_bit_def one_bit_def plus_bit_def times_bit_def modulo_bit_def Abs_bit_inverse Rep_bit_inverse) |
|
72 |
||
73 |
end |
|
74 |
||
75 |
lemma bit_2_eq_0 [simp]: |
|
76 |
\<open>2 = (0::bit)\<close> |
|
77 |
by (simp flip: one_add_one add: zero_bit_def plus_bit_def) |
|
78 |
||
79 |
instance bit :: semiring_parity |
|
80 |
apply standard |
|
81 |
apply (auto simp flip: Rep_bit_inject simp add: modulo_bit_def Abs_bit_inverse Rep_bit_inverse) |
|
82 |
apply (auto simp add: zero_bit_def one_bit_def Abs_bit_inverse Rep_bit_inverse) |
|
83 |
done |
|
84 |
||
85 |
lemma Abs_bit_eq_of_bool [code_abbrev]: |
|
86 |
\<open>Abs_bit = of_bool\<close> |
|
87 |
by (simp add: fun_eq_iff zero_bit_def one_bit_def) |
|
88 |
||
89 |
lemma Rep_bit_eq_odd: |
|
90 |
\<open>Rep_bit = odd\<close> |
|
91 |
proof - |
|
92 |
have \<open>\<not> Rep_bit 0\<close> |
|
93 |
by (simp only: zero_bit_def) (subst Abs_bit_inverse, auto) |
|
94 |
then show ?thesis |
|
95 |
by (auto simp flip: Rep_bit_inject simp add: fun_eq_iff) |
|
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
96 |
qed |
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
97 |
|
71988 | 98 |
lemma Rep_bit_iff_odd [code_abbrev]: |
99 |
\<open>Rep_bit b \<longleftrightarrow> odd b\<close> |
|
100 |
by (simp add: Rep_bit_eq_odd) |
|
101 |
||
102 |
lemma Not_Rep_bit_iff_even [code_abbrev]: |
|
103 |
\<open>\<not> Rep_bit b \<longleftrightarrow> even b\<close> |
|
104 |
by (simp add: Rep_bit_eq_odd) |
|
105 |
||
106 |
lemma Not_Not_Rep_bit [code_unfold]: |
|
107 |
\<open>\<not> \<not> Rep_bit b \<longleftrightarrow> Rep_bit b\<close> |
|
108 |
by simp |
|
109 |
||
110 |
code_datatype \<open>0::bit\<close> \<open>1::bit\<close> |
|
63462 | 111 |
|
71988 | 112 |
lemma Abs_bit_code [code]: |
113 |
\<open>Abs_bit False = 0\<close> |
|
114 |
\<open>Abs_bit True = 1\<close> |
|
115 |
by (simp_all add: Abs_bit_eq_of_bool) |
|
116 |
||
117 |
lemma Rep_bit_code [code]: |
|
118 |
\<open>Rep_bit 0 \<longleftrightarrow> False\<close> |
|
119 |
\<open>Rep_bit 1 \<longleftrightarrow> True\<close> |
|
120 |
by (simp_all add: Rep_bit_eq_odd) |
|
121 |
||
122 |
context zero_neq_one |
|
123 |
begin |
|
124 |
||
125 |
abbreviation of_bit :: \<open>bit \<Rightarrow> 'a\<close> |
|
126 |
where \<open>of_bit b \<equiv> of_bool (odd b)\<close> |
|
127 |
||
128 |
end |
|
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset
|
129 |
|
71953 | 130 |
context |
131 |
begin |
|
132 |
||
71988 | 133 |
qualified lemma bit_eq_iff: |
134 |
\<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b)\<close> for a b :: bit |
|
135 |
by (cases a; cases b) simp_all |
|
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
136 |
|
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
137 |
end |
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset
|
138 |
|
71988 | 139 |
lemma modulo_bit_unfold [simp, code]: |
140 |
\<open>a mod b = of_bool (odd a \<and> even b)\<close> for a b :: bit |
|
141 |
by (simp add: modulo_bit_def Abs_bit_eq_of_bool Rep_bit_eq_odd) |
|
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset
|
142 |
|
71988 | 143 |
lemma power_bit_unfold [simp, code]: |
144 |
\<open>a ^ n = of_bool (odd a \<or> n = 0)\<close> for a :: bit |
|
145 |
by (cases a) simp_all |
|
71953 | 146 |
|
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset
|
147 |
instantiation bit :: semiring_bits |
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset
|
148 |
begin |
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset
|
149 |
|
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset
|
150 |
definition bit_bit :: \<open>bit \<Rightarrow> nat \<Rightarrow> bool\<close> |
71988 | 151 |
where [simp]: \<open>bit_bit b n \<longleftrightarrow> odd b \<and> n = 0\<close> |
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset
|
152 |
|
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset
|
153 |
instance |
71953 | 154 |
apply standard |
71988 | 155 |
apply auto |
156 |
apply (metis bit.exhaust of_bool_eq(2)) |
|
71953 | 157 |
done |
158 |
||
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset
|
159 |
end |
71953 | 160 |
|
161 |
instantiation bit :: semiring_bit_shifts |
|
162 |
begin |
|
163 |
||
164 |
definition push_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close> |
|
71988 | 165 |
where [simp]: \<open>push_bit n b = of_bool (odd b \<and> n = 0)\<close> for b :: bit |
71953 | 166 |
|
167 |
definition drop_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close> |
|
71988 | 168 |
where [simp]: \<open>drop_bit_bit = push_bit\<close> |
71953 | 169 |
|
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset
|
170 |
definition take_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close> |
71988 | 171 |
where [simp]: \<open>take_bit n b = of_bool (odd b \<and> n > 0)\<close> for b :: bit |
172 |
||
173 |
instance |
|
174 |
by standard simp_all |
|
175 |
||
176 |
end |
|
177 |
||
178 |
instantiation bit :: semiring_bit_operations |
|
179 |
begin |
|
180 |
||
181 |
definition and_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> |
|
182 |
where [simp]: \<open>b AND c = of_bool (odd b \<and> odd c)\<close> for b c :: bit |
|
183 |
||
184 |
definition or_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> |
|
185 |
where [simp]: \<open>b OR c = of_bool (odd b \<or> odd c)\<close> for b c :: bit |
|
186 |
||
187 |
definition xor_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> |
|
188 |
where [simp]: \<open>b XOR c = of_bool (odd b \<noteq> odd c)\<close> for b c :: bit |
|
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset
|
189 |
|
71953 | 190 |
instance |
71988 | 191 |
by standard auto |
192 |
||
193 |
end |
|
194 |
||
195 |
lemma add_bit_eq_xor [simp, code]: |
|
196 |
\<open>(+) = ((XOR) :: bit \<Rightarrow> _)\<close> |
|
197 |
by (auto simp add: fun_eq_iff) |
|
198 |
||
199 |
lemma mult_bit_eq_and [simp, code]: |
|
200 |
\<open>(*) = ((AND) :: bit \<Rightarrow> _)\<close> |
|
201 |
by (simp add: fun_eq_iff) |
|
202 |
||
203 |
instantiation bit :: field |
|
204 |
begin |
|
205 |
||
206 |
definition uminus_bit :: \<open>bit \<Rightarrow> bit\<close> |
|
207 |
where [simp]: \<open>uminus_bit = id\<close> |
|
208 |
||
209 |
definition inverse_bit :: \<open>bit \<Rightarrow> bit\<close> |
|
210 |
where [simp]: \<open>inverse_bit = id\<close> |
|
211 |
||
212 |
instance |
|
213 |
by standard simp_all |
|
71953 | 214 |
|
215 |
end |
|
216 |
||
71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset
|
217 |
instantiation bit :: ring_bit_operations |
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset
|
218 |
begin |
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset
|
219 |
|
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset
|
220 |
definition not_bit :: \<open>bit \<Rightarrow> bit\<close> |
71988 | 221 |
where [simp]: \<open>NOT b = of_bool (even b)\<close> for b :: bit |
71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset
|
222 |
|
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset
|
223 |
instance |
71988 | 224 |
by standard simp_all |
71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset
|
225 |
|
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset
|
226 |
end |
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset
|
227 |
|
71988 | 228 |
lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)" |
229 |
by (simp only: Z2.bit_eq_iff even_numeral) simp |
|
71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset
|
230 |
|
71988 | 231 |
lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)" |
232 |
by (simp only: Z2.bit_eq_iff odd_numeral) simp |
|
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset
|
233 |
|
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset
|
234 |
end |