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