author | haftmann |
Thu, 17 Sep 2020 09:57:31 +0000 | |
changeset 72262 | a282abb07642 |
parent 72198 | 7ffa26f05c72 |
child 72515 | c7038c397ae3 |
permissions | -rw-r--r-- |
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset
|
1 |
(* Author: Florian Haftmann, TUM |
67909 | 2 |
*) |
3 |
||
70912 | 4 |
section \<open>Proof(s) of concept for algebraically founded lists of bits\<close> |
67909 | 5 |
|
6 |
theory Bit_Lists |
|
70926 | 7 |
imports |
72262 | 8 |
"HOL-Word.Word" "HOL-Library.More_List" |
67909 | 9 |
begin |
10 |
||
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
11 |
subsection \<open>Fragments of algebraic bit representations\<close> |
70912 | 12 |
|
67909 | 13 |
context comm_semiring_1 |
14 |
begin |
|
70912 | 15 |
|
16 |
abbreviation (input) unsigned_of_bits :: "bool list \<Rightarrow> 'a" |
|
72024 | 17 |
where "unsigned_of_bits \<equiv> horner_sum of_bool 2" |
70912 | 18 |
|
19 |
lemma unsigned_of_bits_replicate_False [simp]: |
|
20 |
"unsigned_of_bits (replicate n False) = 0" |
|
21 |
by (induction n) simp_all |
|
22 |
||
23 |
end |
|
24 |
||
71094 | 25 |
context unique_euclidean_semiring_with_bit_shifts |
70912 | 26 |
begin |
67909 | 27 |
|
70912 | 28 |
lemma unsigned_of_bits_append [simp]: |
29 |
"unsigned_of_bits (bs @ cs) = unsigned_of_bits bs |
|
30 |
+ push_bit (length bs) (unsigned_of_bits cs)" |
|
31 |
by (induction bs) (simp_all add: push_bit_double, |
|
32 |
simp_all add: algebra_simps) |
|
33 |
||
34 |
lemma unsigned_of_bits_take [simp]: |
|
71420 | 35 |
"unsigned_of_bits (take n bs) = take_bit n (unsigned_of_bits bs)" |
70912 | 36 |
proof (induction bs arbitrary: n) |
37 |
case Nil |
|
38 |
then show ?case |
|
39 |
by simp |
|
40 |
next |
|
41 |
case (Cons b bs) |
|
42 |
then show ?case |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset
|
43 |
by (cases n) (simp_all add: ac_simps take_bit_Suc) |
70912 | 44 |
qed |
45 |
||
46 |
lemma unsigned_of_bits_drop [simp]: |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset
|
47 |
"unsigned_of_bits (drop n bs) = drop_bit n (unsigned_of_bits bs)" |
70912 | 48 |
proof (induction bs arbitrary: n) |
49 |
case Nil |
|
50 |
then show ?case |
|
51 |
by simp |
|
52 |
next |
|
53 |
case (Cons b bs) |
|
54 |
then show ?case |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset
|
55 |
by (cases n) (simp_all add: drop_bit_Suc) |
70912 | 56 |
qed |
57 |
||
71420 | 58 |
lemma bit_unsigned_of_bits_iff: |
59 |
\<open>bit (unsigned_of_bits bs) n \<longleftrightarrow> nth_default False bs n\<close> |
|
60 |
proof (induction bs arbitrary: n) |
|
61 |
case Nil |
|
62 |
then show ?case |
|
63 |
by simp |
|
64 |
next |
|
65 |
case (Cons b bs) |
|
66 |
then show ?case |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset
|
67 |
by (cases n) (simp_all add: bit_Suc) |
71420 | 68 |
qed |
69 |
||
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
70 |
primrec n_bits_of :: "nat \<Rightarrow> 'a \<Rightarrow> bool list" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
71 |
where |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
72 |
"n_bits_of 0 a = []" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
73 |
| "n_bits_of (Suc n) a = odd a # n_bits_of n (a div 2)" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
74 |
|
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
75 |
lemma n_bits_of_eq_iff: |
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset
|
76 |
"n_bits_of n a = n_bits_of n b \<longleftrightarrow> take_bit n a = take_bit n b" |
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
77 |
apply (induction n arbitrary: a b) |
71823 | 78 |
apply (auto elim!: evenE oddE simp add: take_bit_Suc mod_2_eq_odd) |
79 |
apply (metis dvd_triv_right even_plus_one_iff odd_iff_mod_2_eq_one) |
|
80 |
apply (metis dvd_triv_right even_plus_one_iff odd_iff_mod_2_eq_one) |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
81 |
done |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
82 |
|
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
83 |
lemma take_n_bits_of [simp]: |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
84 |
"take m (n_bits_of n a) = n_bits_of (min m n) a" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
85 |
proof - |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
86 |
define q and v and w where "q = min m n" and "v = m - q" and "w = n - q" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
87 |
then have "v = 0 \<or> w = 0" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
88 |
by auto |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
89 |
then have "take (q + v) (n_bits_of (q + w) a) = n_bits_of q a" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
90 |
by (induction q arbitrary: a) auto |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
91 |
with q_def v_def w_def show ?thesis |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
92 |
by simp |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
93 |
qed |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
94 |
|
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
95 |
lemma unsigned_of_bits_n_bits_of [simp]: |
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset
|
96 |
"unsigned_of_bits (n_bits_of n a) = take_bit n a" |
71823 | 97 |
by (induction n arbitrary: a) (simp_all add: ac_simps take_bit_Suc mod_2_eq_odd) |
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
98 |
|
70912 | 99 |
end |
100 |
||
101 |
||
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
102 |
subsection \<open>Syntactic bit representation\<close> |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
103 |
|
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
104 |
class bit_representation = |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
105 |
fixes bits_of :: "'a \<Rightarrow> bool list" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
106 |
and of_bits :: "bool list \<Rightarrow> 'a" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
107 |
assumes of_bits_of [simp]: "of_bits (bits_of a) = a" |
70912 | 108 |
|
109 |
text \<open>Unclear whether a \<^typ>\<open>bool\<close> instantiation is needed or not\<close> |
|
110 |
||
111 |
instantiation nat :: bit_representation |
|
112 |
begin |
|
113 |
||
114 |
fun bits_of_nat :: "nat \<Rightarrow> bool list" |
|
115 |
where "bits_of (n::nat) = |
|
116 |
(if n = 0 then [] else odd n # bits_of (n div 2))" |
|
117 |
||
118 |
lemma bits_of_nat_simps [simp]: |
|
119 |
"bits_of (0::nat) = []" |
|
120 |
"n > 0 \<Longrightarrow> bits_of n = odd n # bits_of (n div 2)" for n :: nat |
|
121 |
by simp_all |
|
122 |
||
123 |
declare bits_of_nat.simps [simp del] |
|
124 |
||
125 |
definition of_bits_nat :: "bool list \<Rightarrow> nat" |
|
126 |
where [simp]: "of_bits_nat = unsigned_of_bits" |
|
127 |
\<comment> \<open>remove simp\<close> |
|
128 |
||
129 |
instance proof |
|
130 |
show "of_bits (bits_of n) = n" for n :: nat |
|
131 |
by (induction n rule: nat_bit_induct) simp_all |
|
132 |
qed |
|
67909 | 133 |
|
134 |
end |
|
135 |
||
71420 | 136 |
lemma bit_of_bits_nat_iff: |
137 |
\<open>bit (of_bits bs :: nat) n \<longleftrightarrow> nth_default False bs n\<close> |
|
138 |
by (simp add: bit_unsigned_of_bits_iff) |
|
139 |
||
70912 | 140 |
lemma bits_of_Suc_0 [simp]: |
141 |
"bits_of (Suc 0) = [True]" |
|
142 |
by simp |
|
143 |
||
144 |
lemma bits_of_1_nat [simp]: |
|
145 |
"bits_of (1 :: nat) = [True]" |
|
146 |
by simp |
|
147 |
||
148 |
lemma bits_of_nat_numeral_simps [simp]: |
|
149 |
"bits_of (numeral Num.One :: nat) = [True]" (is ?One) |
|
150 |
"bits_of (numeral (Num.Bit0 n) :: nat) = False # bits_of (numeral n :: nat)" (is ?Bit0) |
|
151 |
"bits_of (numeral (Num.Bit1 n) :: nat) = True # bits_of (numeral n :: nat)" (is ?Bit1) |
|
152 |
proof - |
|
153 |
show ?One |
|
154 |
by simp |
|
155 |
define m :: nat where "m = numeral n" |
|
156 |
then have "m > 0" and *: "numeral n = m" "numeral (Num.Bit0 n) = 2 * m" "numeral (Num.Bit1 n) = Suc (2 * m)" |
|
157 |
by simp_all |
|
158 |
from \<open>m > 0\<close> show ?Bit0 ?Bit1 |
|
159 |
by (simp_all add: *) |
|
160 |
qed |
|
161 |
||
162 |
lemma unsigned_of_bits_of_nat [simp]: |
|
163 |
"unsigned_of_bits (bits_of n) = n" for n :: nat |
|
164 |
using of_bits_of [of n] by simp |
|
165 |
||
166 |
instantiation int :: bit_representation |
|
67909 | 167 |
begin |
168 |
||
70912 | 169 |
fun bits_of_int :: "int \<Rightarrow> bool list" |
170 |
where "bits_of_int k = odd k # |
|
171 |
(if k = 0 \<or> k = - 1 then [] else bits_of_int (k div 2))" |
|
172 |
||
173 |
lemma bits_of_int_simps [simp]: |
|
174 |
"bits_of (0 :: int) = [False]" |
|
175 |
"bits_of (- 1 :: int) = [True]" |
|
176 |
"k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> bits_of k = odd k # bits_of (k div 2)" for k :: int |
|
177 |
by simp_all |
|
178 |
||
179 |
lemma bits_of_not_Nil [simp]: |
|
180 |
"bits_of k \<noteq> []" for k :: int |
|
181 |
by simp |
|
182 |
||
183 |
declare bits_of_int.simps [simp del] |
|
184 |
||
185 |
definition of_bits_int :: "bool list \<Rightarrow> int" |
|
186 |
where "of_bits_int bs = (if bs = [] \<or> \<not> last bs then unsigned_of_bits bs |
|
187 |
else unsigned_of_bits bs - 2 ^ length bs)" |
|
188 |
||
189 |
lemma of_bits_int_simps [simp]: |
|
190 |
"of_bits [] = (0 :: int)" |
|
191 |
"of_bits [False] = (0 :: int)" |
|
192 |
"of_bits [True] = (- 1 :: int)" |
|
193 |
"of_bits (bs @ [b]) = (unsigned_of_bits bs :: int) - (2 ^ length bs) * of_bool b" |
|
194 |
"of_bits (False # bs) = 2 * (of_bits bs :: int)" |
|
195 |
"bs \<noteq> [] \<Longrightarrow> of_bits (True # bs) = 1 + 2 * (of_bits bs :: int)" |
|
196 |
by (simp_all add: of_bits_int_def push_bit_of_1) |
|
197 |
||
198 |
instance proof |
|
199 |
show "of_bits (bits_of k) = k" for k :: int |
|
200 |
by (induction k rule: int_bit_induct) simp_all |
|
201 |
qed |
|
202 |
||
203 |
lemma bits_of_1_int [simp]: |
|
204 |
"bits_of (1 :: int) = [True, False]" |
|
205 |
by simp |
|
206 |
||
207 |
lemma bits_of_int_numeral_simps [simp]: |
|
208 |
"bits_of (numeral Num.One :: int) = [True, False]" (is ?One) |
|
209 |
"bits_of (numeral (Num.Bit0 n) :: int) = False # bits_of (numeral n :: int)" (is ?Bit0) |
|
210 |
"bits_of (numeral (Num.Bit1 n) :: int) = True # bits_of (numeral n :: int)" (is ?Bit1) |
|
211 |
"bits_of (- numeral (Num.Bit0 n) :: int) = False # bits_of (- numeral n :: int)" (is ?nBit0) |
|
212 |
"bits_of (- numeral (Num.Bit1 n) :: int) = True # bits_of (- numeral (Num.inc n) :: int)" (is ?nBit1) |
|
213 |
proof - |
|
214 |
show ?One |
|
215 |
by simp |
|
216 |
define k :: int where "k = numeral n" |
|
217 |
then have "k > 0" and *: "numeral n = k" "numeral (Num.Bit0 n) = 2 * k" "numeral (Num.Bit1 n) = 2 * k + 1" |
|
218 |
"numeral (Num.inc n) = k + 1" |
|
219 |
by (simp_all add: add_One) |
|
220 |
have "- (2 * k) div 2 = - k" "(- (2 * k) - 1) div 2 = - k - 1" |
|
221 |
by simp_all |
|
222 |
with \<open>k > 0\<close> show ?Bit0 ?Bit1 ?nBit0 ?nBit1 |
|
223 |
by (simp_all add: *) |
|
224 |
qed |
|
225 |
||
71420 | 226 |
lemma bit_of_bits_int_iff: |
227 |
\<open>bit (of_bits bs :: int) n \<longleftrightarrow> nth_default (bs \<noteq> [] \<and> last bs) bs n\<close> |
|
228 |
proof (induction bs arbitrary: n) |
|
229 |
case Nil |
|
230 |
then show ?case |
|
231 |
by simp |
|
232 |
next |
|
233 |
case (Cons b bs) |
|
234 |
then show ?case |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset
|
235 |
by (cases n; cases b; cases bs) (simp_all add: bit_Suc) |
71420 | 236 |
qed |
237 |
||
70912 | 238 |
lemma of_bits_append [simp]: |
239 |
"of_bits (bs @ cs) = of_bits bs + push_bit (length bs) (of_bits cs :: int)" |
|
240 |
if "bs \<noteq> []" "\<not> last bs" |
|
241 |
using that proof (induction bs rule: list_nonempty_induct) |
|
242 |
case (single b) |
|
243 |
then show ?case |
|
244 |
by simp |
|
245 |
next |
|
246 |
case (cons b bs) |
|
247 |
then show ?case |
|
248 |
by (cases b) (simp_all add: push_bit_double) |
|
249 |
qed |
|
250 |
||
251 |
lemma of_bits_replicate_False [simp]: |
|
252 |
"of_bits (replicate n False) = (0 :: int)" |
|
253 |
by (auto simp add: of_bits_int_def) |
|
254 |
||
255 |
lemma of_bits_drop [simp]: |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset
|
256 |
"of_bits (drop n bs) = drop_bit n (of_bits bs :: int)" |
70912 | 257 |
if "n < length bs" |
258 |
using that proof (induction bs arbitrary: n) |
|
259 |
case Nil |
|
260 |
then show ?case |
|
261 |
by simp |
|
262 |
next |
|
263 |
case (Cons b bs) |
|
264 |
show ?case |
|
265 |
proof (cases n) |
|
266 |
case 0 |
|
267 |
then show ?thesis |
|
268 |
by simp |
|
269 |
next |
|
270 |
case (Suc n) |
|
271 |
with Cons.prems have "bs \<noteq> []" |
|
272 |
by auto |
|
273 |
with Suc Cons.IH [of n] Cons.prems show ?thesis |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset
|
274 |
by (cases b) (simp_all add: drop_bit_Suc) |
70912 | 275 |
qed |
276 |
qed |
|
67909 | 277 |
|
278 |
end |
|
279 |
||
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
280 |
lemma unsigned_of_bits_eq_of_bits: |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
281 |
"unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
282 |
by (simp add: of_bits_int_def) |
70912 | 283 |
|
71443 | 284 |
unbundle word.lifting |
285 |
||
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
286 |
instantiation word :: (len) bit_representation |
67909 | 287 |
begin |
288 |
||
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
289 |
lift_definition bits_of_word :: "'a word \<Rightarrow> bool list" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
290 |
is "n_bits_of LENGTH('a)" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
291 |
by (simp add: n_bits_of_eq_iff) |
70912 | 292 |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
293 |
lift_definition of_bits_word :: "bool list \<Rightarrow> 'a word" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
294 |
is unsigned_of_bits . |
70912 | 295 |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
296 |
instance proof |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
297 |
fix a :: "'a word" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
298 |
show "of_bits (bits_of a) = a" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
299 |
by transfer simp |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
300 |
qed |
70912 | 301 |
|
302 |
end |
|
303 |
||
71443 | 304 |
lifting_update word.lifting |
305 |
lifting_forget word.lifting |
|
306 |
||
70912 | 307 |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
308 |
subsection \<open>Bit representations with bit operations\<close> |
67909 | 309 |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
310 |
class semiring_bit_representation = semiring_bit_operations + bit_representation + |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
311 |
assumes and_eq: "length bs = length cs \<Longrightarrow> |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
312 |
of_bits bs AND of_bits cs = of_bits (map2 (\<and>) bs cs)" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
313 |
and or_eq: "length bs = length cs \<Longrightarrow> |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
314 |
of_bits bs OR of_bits cs = of_bits (map2 (\<or>) bs cs)" |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
315 |
and xor_eq: "length bs = length cs \<Longrightarrow> |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
316 |
of_bits bs XOR of_bits cs = of_bits (map2 (\<noteq>) bs cs)" |
71094 | 317 |
and push_bit_eq: "push_bit n a = of_bits (replicate n False @ bits_of a)" |
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
318 |
and drop_bit_eq: "n < length (bits_of a) \<Longrightarrow> drop_bit n a = of_bits (drop n (bits_of a))" |
67909 | 319 |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
320 |
class ring_bit_representation = ring_bit_operations + semiring_bit_representation + |
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
321 |
assumes not_eq: "not = of_bits \<circ> map Not \<circ> bits_of" |
67909 | 322 |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
323 |
instance nat :: semiring_bit_representation |
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
324 |
by standard (simp_all add: bit_eq_iff bit_unsigned_of_bits_iff nth_default_map2 [of _ _ _ False False] |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
325 |
bit_and_iff bit_or_iff bit_xor_iff) |
70912 | 326 |
|
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
327 |
instance int :: ring_bit_representation |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
328 |
proof |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
329 |
{ |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
330 |
fix bs cs :: \<open>bool list\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
331 |
assume \<open>length bs = length cs\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
332 |
then have \<open>cs = [] \<longleftrightarrow> bs = []\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
333 |
by auto |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
334 |
with \<open>length bs = length cs\<close> have \<open>zip bs cs \<noteq> [] \<and> last (map2 (\<and>) bs cs) \<longleftrightarrow> (bs \<noteq> [] \<and> last bs) \<and> (cs \<noteq> [] \<and> last cs)\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
335 |
and \<open>zip bs cs \<noteq> [] \<and> last (map2 (\<or>) bs cs) \<longleftrightarrow> (bs \<noteq> [] \<and> last bs) \<or> (cs \<noteq> [] \<and> last cs)\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
336 |
and \<open>zip bs cs \<noteq> [] \<and> last (map2 (\<noteq>) bs cs) \<longleftrightarrow> ((bs \<noteq> [] \<and> last bs) \<noteq> (cs \<noteq> [] \<and> last cs))\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
337 |
by (auto simp add: last_map last_zip zip_eq_Nil_iff prod_eq_iff) |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
338 |
then show \<open>of_bits bs AND of_bits cs = (of_bits (map2 (\<and>) bs cs) :: int)\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
339 |
and \<open>of_bits bs OR of_bits cs = (of_bits (map2 (\<or>) bs cs) :: int)\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
340 |
and \<open>of_bits bs XOR of_bits cs = (of_bits (map2 (\<noteq>) bs cs) :: int)\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
341 |
by (simp_all add: fun_eq_iff bit_eq_iff bit_and_iff bit_or_iff bit_xor_iff bit_not_iff bit_of_bits_int_iff \<open>length bs = length cs\<close> nth_default_map2 [of bs cs _ \<open>bs \<noteq> [] \<and> last bs\<close> \<open>cs \<noteq> [] \<and> last cs\<close>]) |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
342 |
} |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
343 |
show \<open>push_bit n k = of_bits (replicate n False @ bits_of k)\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
344 |
for k :: int and n :: nat |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
345 |
by (cases "n = 0") simp_all |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
346 |
show \<open>drop_bit n k = of_bits (drop n (bits_of k))\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
347 |
if \<open>n < length (bits_of k)\<close> for k :: int and n :: nat |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
348 |
using that by simp |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
349 |
show \<open>(not :: int \<Rightarrow> _) = of_bits \<circ> map Not \<circ> bits_of\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
350 |
proof (rule sym, rule ext) |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
351 |
fix k :: int |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
352 |
show \<open>(of_bits \<circ> map Not \<circ> bits_of) k = NOT k\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
353 |
by (induction k rule: int_bit_induct) (simp_all add: not_int_def) |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
354 |
qed |
70912 | 355 |
qed |
67909 | 356 |
|
357 |
end |