author | haftmann |
Sun, 01 Aug 2021 10:20:34 +0000 | |
changeset 74097 | 6d7be1227d02 |
parent 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 |
72515
c7038c397ae3
moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents:
72262
diff
changeset
|
8 |
"HOL-Library.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 |
instantiation nat :: bit_representation |
|
110 |
begin |
|
111 |
||
112 |
fun bits_of_nat :: "nat \<Rightarrow> bool list" |
|
113 |
where "bits_of (n::nat) = |
|
114 |
(if n = 0 then [] else odd n # bits_of (n div 2))" |
|
115 |
||
116 |
lemma bits_of_nat_simps [simp]: |
|
117 |
"bits_of (0::nat) = []" |
|
118 |
"n > 0 \<Longrightarrow> bits_of n = odd n # bits_of (n div 2)" for n :: nat |
|
119 |
by simp_all |
|
120 |
||
121 |
declare bits_of_nat.simps [simp del] |
|
122 |
||
123 |
definition of_bits_nat :: "bool list \<Rightarrow> nat" |
|
124 |
where [simp]: "of_bits_nat = unsigned_of_bits" |
|
125 |
\<comment> \<open>remove simp\<close> |
|
126 |
||
127 |
instance proof |
|
128 |
show "of_bits (bits_of n) = n" for n :: nat |
|
129 |
by (induction n rule: nat_bit_induct) simp_all |
|
130 |
qed |
|
67909 | 131 |
|
132 |
end |
|
133 |
||
71420 | 134 |
lemma bit_of_bits_nat_iff: |
135 |
\<open>bit (of_bits bs :: nat) n \<longleftrightarrow> nth_default False bs n\<close> |
|
136 |
by (simp add: bit_unsigned_of_bits_iff) |
|
137 |
||
70912 | 138 |
lemma bits_of_Suc_0 [simp]: |
139 |
"bits_of (Suc 0) = [True]" |
|
140 |
by simp |
|
141 |
||
142 |
lemma bits_of_1_nat [simp]: |
|
143 |
"bits_of (1 :: nat) = [True]" |
|
144 |
by simp |
|
145 |
||
146 |
lemma bits_of_nat_numeral_simps [simp]: |
|
147 |
"bits_of (numeral Num.One :: nat) = [True]" (is ?One) |
|
148 |
"bits_of (numeral (Num.Bit0 n) :: nat) = False # bits_of (numeral n :: nat)" (is ?Bit0) |
|
149 |
"bits_of (numeral (Num.Bit1 n) :: nat) = True # bits_of (numeral n :: nat)" (is ?Bit1) |
|
150 |
proof - |
|
151 |
show ?One |
|
152 |
by simp |
|
153 |
define m :: nat where "m = numeral n" |
|
154 |
then have "m > 0" and *: "numeral n = m" "numeral (Num.Bit0 n) = 2 * m" "numeral (Num.Bit1 n) = Suc (2 * m)" |
|
155 |
by simp_all |
|
156 |
from \<open>m > 0\<close> show ?Bit0 ?Bit1 |
|
157 |
by (simp_all add: *) |
|
158 |
qed |
|
159 |
||
160 |
lemma unsigned_of_bits_of_nat [simp]: |
|
161 |
"unsigned_of_bits (bits_of n) = n" for n :: nat |
|
162 |
using of_bits_of [of n] by simp |
|
163 |
||
164 |
instantiation int :: bit_representation |
|
67909 | 165 |
begin |
166 |
||
70912 | 167 |
fun bits_of_int :: "int \<Rightarrow> bool list" |
168 |
where "bits_of_int k = odd k # |
|
169 |
(if k = 0 \<or> k = - 1 then [] else bits_of_int (k div 2))" |
|
170 |
||
171 |
lemma bits_of_int_simps [simp]: |
|
172 |
"bits_of (0 :: int) = [False]" |
|
173 |
"bits_of (- 1 :: int) = [True]" |
|
174 |
"k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> bits_of k = odd k # bits_of (k div 2)" for k :: int |
|
175 |
by simp_all |
|
176 |
||
177 |
lemma bits_of_not_Nil [simp]: |
|
178 |
"bits_of k \<noteq> []" for k :: int |
|
179 |
by simp |
|
180 |
||
181 |
declare bits_of_int.simps [simp del] |
|
182 |
||
183 |
definition of_bits_int :: "bool list \<Rightarrow> int" |
|
184 |
where "of_bits_int bs = (if bs = [] \<or> \<not> last bs then unsigned_of_bits bs |
|
185 |
else unsigned_of_bits bs - 2 ^ length bs)" |
|
186 |
||
187 |
lemma of_bits_int_simps [simp]: |
|
188 |
"of_bits [] = (0 :: int)" |
|
189 |
"of_bits [False] = (0 :: int)" |
|
190 |
"of_bits [True] = (- 1 :: int)" |
|
191 |
"of_bits (bs @ [b]) = (unsigned_of_bits bs :: int) - (2 ^ length bs) * of_bool b" |
|
192 |
"of_bits (False # bs) = 2 * (of_bits bs :: int)" |
|
193 |
"bs \<noteq> [] \<Longrightarrow> of_bits (True # bs) = 1 + 2 * (of_bits bs :: int)" |
|
194 |
by (simp_all add: of_bits_int_def push_bit_of_1) |
|
195 |
||
196 |
instance proof |
|
197 |
show "of_bits (bits_of k) = k" for k :: int |
|
198 |
by (induction k rule: int_bit_induct) simp_all |
|
199 |
qed |
|
200 |
||
201 |
lemma bits_of_1_int [simp]: |
|
202 |
"bits_of (1 :: int) = [True, False]" |
|
203 |
by simp |
|
204 |
||
205 |
lemma bits_of_int_numeral_simps [simp]: |
|
206 |
"bits_of (numeral Num.One :: int) = [True, False]" (is ?One) |
|
207 |
"bits_of (numeral (Num.Bit0 n) :: int) = False # bits_of (numeral n :: int)" (is ?Bit0) |
|
208 |
"bits_of (numeral (Num.Bit1 n) :: int) = True # bits_of (numeral n :: int)" (is ?Bit1) |
|
209 |
"bits_of (- numeral (Num.Bit0 n) :: int) = False # bits_of (- numeral n :: int)" (is ?nBit0) |
|
210 |
"bits_of (- numeral (Num.Bit1 n) :: int) = True # bits_of (- numeral (Num.inc n) :: int)" (is ?nBit1) |
|
211 |
proof - |
|
212 |
show ?One |
|
213 |
by simp |
|
214 |
define k :: int where "k = numeral n" |
|
215 |
then have "k > 0" and *: "numeral n = k" "numeral (Num.Bit0 n) = 2 * k" "numeral (Num.Bit1 n) = 2 * k + 1" |
|
216 |
"numeral (Num.inc n) = k + 1" |
|
217 |
by (simp_all add: add_One) |
|
218 |
have "- (2 * k) div 2 = - k" "(- (2 * k) - 1) div 2 = - k - 1" |
|
219 |
by simp_all |
|
220 |
with \<open>k > 0\<close> show ?Bit0 ?Bit1 ?nBit0 ?nBit1 |
|
221 |
by (simp_all add: *) |
|
222 |
qed |
|
223 |
||
71420 | 224 |
lemma bit_of_bits_int_iff: |
225 |
\<open>bit (of_bits bs :: int) n \<longleftrightarrow> nth_default (bs \<noteq> [] \<and> last bs) bs n\<close> |
|
226 |
proof (induction bs arbitrary: n) |
|
227 |
case Nil |
|
228 |
then show ?case |
|
229 |
by simp |
|
230 |
next |
|
231 |
case (Cons b bs) |
|
232 |
then show ?case |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset
|
233 |
by (cases n; cases b; cases bs) (simp_all add: bit_Suc) |
71420 | 234 |
qed |
235 |
||
70912 | 236 |
lemma of_bits_append [simp]: |
237 |
"of_bits (bs @ cs) = of_bits bs + push_bit (length bs) (of_bits cs :: int)" |
|
238 |
if "bs \<noteq> []" "\<not> last bs" |
|
239 |
using that proof (induction bs rule: list_nonempty_induct) |
|
240 |
case (single b) |
|
241 |
then show ?case |
|
242 |
by simp |
|
243 |
next |
|
244 |
case (cons b bs) |
|
245 |
then show ?case |
|
246 |
by (cases b) (simp_all add: push_bit_double) |
|
247 |
qed |
|
248 |
||
249 |
lemma of_bits_replicate_False [simp]: |
|
250 |
"of_bits (replicate n False) = (0 :: int)" |
|
251 |
by (auto simp add: of_bits_int_def) |
|
252 |
||
253 |
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
|
254 |
"of_bits (drop n bs) = drop_bit n (of_bits bs :: int)" |
70912 | 255 |
if "n < length bs" |
256 |
using that proof (induction bs arbitrary: n) |
|
257 |
case Nil |
|
258 |
then show ?case |
|
259 |
by simp |
|
260 |
next |
|
261 |
case (Cons b bs) |
|
262 |
show ?case |
|
263 |
proof (cases n) |
|
264 |
case 0 |
|
265 |
then show ?thesis |
|
266 |
by simp |
|
267 |
next |
|
268 |
case (Suc n) |
|
269 |
with Cons.prems have "bs \<noteq> []" |
|
270 |
by auto |
|
271 |
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
|
272 |
by (cases b) (simp_all add: drop_bit_Suc) |
70912 | 273 |
qed |
274 |
qed |
|
67909 | 275 |
|
276 |
end |
|
277 |
||
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
278 |
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
|
279 |
"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
|
280 |
by (simp add: of_bits_int_def) |
70912 | 281 |
|
71443 | 282 |
unbundle word.lifting |
283 |
||
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
284 |
instantiation word :: (len) bit_representation |
67909 | 285 |
begin |
286 |
||
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
287 |
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
|
288 |
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
|
289 |
by (simp add: n_bits_of_eq_iff) |
70912 | 290 |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
291 |
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
|
292 |
is unsigned_of_bits . |
70912 | 293 |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
294 |
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
|
295 |
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
|
296 |
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
|
297 |
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
|
298 |
qed |
70912 | 299 |
|
300 |
end |
|
301 |
||
71443 | 302 |
lifting_update word.lifting |
303 |
lifting_forget word.lifting |
|
304 |
||
70912 | 305 |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
306 |
subsection \<open>Bit representations with bit operations\<close> |
67909 | 307 |
|
74097 | 308 |
class semiring_bit_representation = semiring_bit_operations + bit_representation |
309 |
opening bit_operations_syntax + |
|
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 |
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
|
311 |
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
|
312 |
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
|
313 |
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
|
314 |
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
|
315 |
of_bits bs XOR of_bits cs = of_bits (map2 (\<noteq>) bs cs)" |
71094 | 316 |
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
|
317 |
and drop_bit_eq: "n < length (bits_of a) \<Longrightarrow> drop_bit n a = of_bits (drop n (bits_of a))" |
67909 | 318 |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
319 |
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
|
320 |
assumes not_eq: "not = of_bits \<circ> map Not \<circ> bits_of" |
67909 | 321 |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70926
diff
changeset
|
322 |
instance nat :: semiring_bit_representation |
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
323 |
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
|
324 |
bit_and_iff bit_or_iff bit_xor_iff) |
70912 | 325 |
|
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
326 |
instance int :: ring_bit_representation |
74097 | 327 |
including bit_operations_syntax proof |
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
328 |
{ |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
329 |
fix bs cs :: \<open>bool list\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
330 |
assume \<open>length bs = length cs\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
331 |
then have \<open>cs = [] \<longleftrightarrow> bs = []\<close> |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
332 |
by auto |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
333 |
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
|
334 |
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
|
335 |
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
|
336 |
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
|
337 |
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
|
338 |
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
|
339 |
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
|
340 |
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
|
341 |
} |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
342 |
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
|
343 |
for k :: int and n :: nat |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
344 |
by (cases "n = 0") simp_all |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
345 |
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
|
346 |
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
|
347 |
using that by simp |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
348 |
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
|
349 |
proof (rule sym, rule ext) |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
350 |
fix k :: int |
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71535
diff
changeset
|
351 |
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
|
352 |
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
|
353 |
qed |
70912 | 354 |
qed |
67909 | 355 |
|
356 |
end |