author | haftmann |
Mon, 10 Aug 2020 15:34:55 +0000 | |
changeset 72130 | 9e5862223442 |
parent 72088 | a36db1c8238e |
child 72292 | 4a58c38b85ff |
permissions | -rw-r--r-- |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1 |
(* Title: HOL/Word/Reversed_Bit_Lists.thy |
71997 | 2 |
Author: Jeremy Dawson, NICTA |
3 |
*) |
|
4 |
||
5 |
section \<open>Bit values as reversed lists of bools\<close> |
|
6 |
||
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
7 |
theory Reversed_Bit_Lists |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
8 |
imports Word |
71997 | 9 |
begin |
10 |
||
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
11 |
context comm_semiring_1 |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
12 |
begin |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
13 |
|
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
14 |
lemma horner_sum_append: |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
15 |
\<open>horner_sum f a (xs @ ys) = horner_sum f a xs + a ^ length xs * horner_sum f a ys\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
16 |
using sum.atLeastLessThan_shift_bounds [of _ 0 \<open>length xs\<close> \<open>length ys\<close>] |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
17 |
atLeastLessThan_add_Un [of 0 \<open>length xs\<close> \<open>length ys\<close>] |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
18 |
by (simp add: horner_sum_eq_sum sum_distrib_left sum.union_disjoint ac_simps nth_append power_add) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
19 |
|
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
20 |
end |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
21 |
|
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
22 |
lemma horner_sum_of_bool_2_concat: |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
23 |
\<open>horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
24 |
for ws :: \<open>'a::len word list\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
25 |
proof (induction ws) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
26 |
case Nil |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
27 |
then show ?case |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
28 |
by simp |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
29 |
next |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
30 |
case (Cons w ws) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
31 |
moreover have \<open>horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
32 |
proof transfer |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
33 |
fix k :: int |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
34 |
have \<open>map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)] |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
35 |
= map (bit k) [0..<LENGTH('a)]\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
36 |
by simp |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
37 |
then show \<open>horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)]) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
38 |
= take_bit LENGTH('a) k\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
39 |
by (simp only: horner_sum_bit_eq_take_bit) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
40 |
qed |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
41 |
ultimately show ?case |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
42 |
by (simp add: horner_sum_append) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
43 |
qed |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
44 |
|
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
45 |
|
71997 | 46 |
subsection \<open>Implicit augmentation of list prefixes\<close> |
47 |
||
48 |
primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
49 |
where |
|
50 |
Z: "takefill fill 0 xs = []" |
|
51 |
| Suc: "takefill fill (Suc n) xs = |
|
52 |
(case xs of |
|
53 |
[] \<Rightarrow> fill # takefill fill n xs |
|
54 |
| y # ys \<Rightarrow> y # takefill fill n ys)" |
|
55 |
||
56 |
lemma nth_takefill: "m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)" |
|
57 |
apply (induct n arbitrary: m l) |
|
58 |
apply clarsimp |
|
59 |
apply clarsimp |
|
60 |
apply (case_tac m) |
|
61 |
apply (simp split: list.split) |
|
62 |
apply (simp split: list.split) |
|
63 |
done |
|
64 |
||
65 |
lemma takefill_alt: "takefill fill n l = take n l @ replicate (n - length l) fill" |
|
66 |
by (induct n arbitrary: l) (auto split: list.split) |
|
67 |
||
68 |
lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill" |
|
69 |
by (simp add: takefill_alt replicate_add [symmetric]) |
|
70 |
||
71 |
lemma takefill_le': "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l" |
|
72 |
by (induct m arbitrary: l n) (auto split: list.split) |
|
73 |
||
74 |
lemma length_takefill [simp]: "length (takefill fill n l) = n" |
|
75 |
by (simp add: takefill_alt) |
|
76 |
||
77 |
lemma take_takefill': "n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w" |
|
78 |
by (induct k arbitrary: w n) (auto split: list.split) |
|
79 |
||
80 |
lemma drop_takefill: "drop k (takefill fill (m + k) w) = takefill fill m (drop k w)" |
|
81 |
by (induct k arbitrary: w) (auto split: list.split) |
|
82 |
||
83 |
lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l" |
|
84 |
by (auto simp: le_iff_add takefill_le') |
|
85 |
||
86 |
lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w" |
|
87 |
by (auto simp: le_iff_add take_takefill') |
|
88 |
||
89 |
lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)" |
|
90 |
by (induct xs) auto |
|
91 |
||
92 |
lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs" |
|
93 |
by (induct xs arbitrary: l) auto |
|
94 |
||
95 |
lemmas takefill_same [simp] = takefill_same' [OF refl] |
|
96 |
||
97 |
lemma tf_rev: |
|
98 |
"n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) = |
|
99 |
rev (takefill y m (rev (takefill x k (rev bl))))" |
|
100 |
apply (rule nth_equalityI) |
|
101 |
apply (auto simp add: nth_takefill rev_nth) |
|
102 |
apply (rule_tac f = "\<lambda>n. bl ! n" in arg_cong) |
|
103 |
apply arith |
|
104 |
done |
|
105 |
||
106 |
lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w" |
|
107 |
by auto |
|
108 |
||
109 |
lemmas takefill_Suc_cases = |
|
110 |
list.cases [THEN takefill.Suc [THEN trans]] |
|
111 |
||
112 |
lemmas takefill_Suc_Nil = takefill_Suc_cases (1) |
|
113 |
lemmas takefill_Suc_Cons = takefill_Suc_cases (2) |
|
114 |
||
115 |
lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2] |
|
116 |
takefill_minus [symmetric, THEN trans]] |
|
117 |
||
118 |
lemma takefill_numeral_Nil [simp]: |
|
119 |
"takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []" |
|
120 |
by (simp add: numeral_eq_Suc) |
|
121 |
||
122 |
lemma takefill_numeral_Cons [simp]: |
|
123 |
"takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs" |
|
124 |
by (simp add: numeral_eq_Suc) |
|
125 |
||
126 |
||
127 |
subsection \<open>Range projection\<close> |
|
128 |
||
129 |
definition bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a list" |
|
130 |
where "bl_of_nth n f = map f (rev [0..<n])" |
|
131 |
||
132 |
lemma bl_of_nth_simps [simp, code]: |
|
133 |
"bl_of_nth 0 f = []" |
|
134 |
"bl_of_nth (Suc n) f = f n # bl_of_nth n f" |
|
135 |
by (simp_all add: bl_of_nth_def) |
|
136 |
||
137 |
lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n" |
|
138 |
by (simp add: bl_of_nth_def) |
|
139 |
||
140 |
lemma nth_bl_of_nth [simp]: "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m" |
|
141 |
by (simp add: bl_of_nth_def rev_map) |
|
142 |
||
143 |
lemma bl_of_nth_inj: "(\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g" |
|
144 |
by (simp add: bl_of_nth_def) |
|
145 |
||
146 |
lemma bl_of_nth_nth_le: "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs" |
|
147 |
apply (induct n arbitrary: xs) |
|
148 |
apply clarsimp |
|
149 |
apply clarsimp |
|
150 |
apply (rule trans [OF _ hd_Cons_tl]) |
|
151 |
apply (frule Suc_le_lessD) |
|
152 |
apply (simp add: rev_nth trans [OF drop_Suc drop_tl, symmetric]) |
|
153 |
apply (subst hd_drop_conv_nth) |
|
154 |
apply force |
|
155 |
apply simp_all |
|
156 |
apply (rule_tac f = "\<lambda>n. drop n xs" in arg_cong) |
|
157 |
apply simp |
|
158 |
done |
|
159 |
||
160 |
lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) ((!) (rev xs)) = xs" |
|
161 |
by (simp add: bl_of_nth_nth_le) |
|
162 |
||
72079 | 163 |
|
164 |
subsection \<open>More\<close> |
|
165 |
||
166 |
definition rotater1 :: "'a list \<Rightarrow> 'a list" |
|
167 |
where "rotater1 ys = |
|
168 |
(case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)" |
|
169 |
||
170 |
definition rotater :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
171 |
where "rotater n = rotater1 ^^ n" |
|
172 |
||
173 |
lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified] |
|
174 |
||
175 |
lemma rotate1_rl': "rotater1 (l @ [a]) = a # l" |
|
176 |
by (cases l) (auto simp: rotater1_def) |
|
177 |
||
178 |
lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l" |
|
179 |
apply (unfold rotater1_def) |
|
180 |
apply (cases "l") |
|
181 |
apply (case_tac [2] "list") |
|
182 |
apply auto |
|
183 |
done |
|
184 |
||
185 |
lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l" |
|
186 |
by (cases l) (auto simp: rotater1_def) |
|
187 |
||
188 |
lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)" |
|
189 |
by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl') |
|
190 |
||
191 |
lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)" |
|
192 |
by (induct n) (auto simp: rotater_def intro: rotater1_rev') |
|
193 |
||
194 |
lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))" |
|
195 |
using rotater_rev' [where xs = "rev ys"] by simp |
|
196 |
||
197 |
lemma rotater_drop_take: |
|
198 |
"rotater n xs = |
|
199 |
drop (length xs - n mod length xs) xs @ |
|
200 |
take (length xs - n mod length xs) xs" |
|
201 |
by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop) |
|
202 |
||
203 |
lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)" |
|
204 |
unfolding rotater_def by auto |
|
205 |
||
206 |
lemma nth_rotater: |
|
207 |
\<open>rotater m xs ! n = xs ! ((n + (length xs - m mod length xs)) mod length xs)\<close> if \<open>n < length xs\<close> |
|
208 |
using that by (simp add: rotater_drop_take nth_append not_less less_diff_conv ac_simps le_mod_geq) |
|
209 |
||
210 |
lemma nth_rotater1: |
|
211 |
\<open>rotater1 xs ! n = xs ! ((n + (length xs - 1)) mod length xs)\<close> if \<open>n < length xs\<close> |
|
212 |
using that nth_rotater [of n xs 1] by simp |
|
213 |
||
214 |
lemma rotate_inv_plus [rule_format]: |
|
215 |
"\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and> |
|
216 |
rotate k (rotater n xs) = rotate m xs \<and> |
|
217 |
rotater n (rotate k xs) = rotate m xs \<and> |
|
218 |
rotate n (rotater k xs) = rotater m xs" |
|
219 |
by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans]) |
|
220 |
||
221 |
lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus] |
|
222 |
||
223 |
lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified] |
|
224 |
||
225 |
lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1] |
|
226 |
lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1] |
|
227 |
||
228 |
lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs" |
|
229 |
by auto |
|
230 |
||
231 |
lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys" |
|
232 |
by auto |
|
233 |
||
234 |
lemma length_rotater [simp]: "length (rotater n xs) = length xs" |
|
235 |
by (simp add : rotater_rev) |
|
236 |
||
237 |
lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs" |
|
238 |
apply (rule box_equals) |
|
239 |
defer |
|
240 |
apply (rule rotate_conv_mod [symmetric])+ |
|
241 |
apply simp |
|
242 |
done |
|
243 |
||
244 |
lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z" |
|
245 |
by simp |
|
246 |
||
247 |
lemmas rotate_eqs = |
|
248 |
trans [OF rotate0 [THEN fun_cong] id_apply] |
|
249 |
rotate_rotate [symmetric] |
|
250 |
rotate_id |
|
251 |
rotate_conv_mod |
|
252 |
rotate_eq_mod |
|
253 |
||
254 |
lemmas rrs0 = rotate_eqs [THEN restrict_to_left, |
|
255 |
simplified rotate_gal [symmetric] rotate_gal' [symmetric]] |
|
256 |
lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]] |
|
257 |
lemmas rotater_eqs = rrs1 [simplified length_rotater] |
|
258 |
lemmas rotater_0 = rotater_eqs (1) |
|
259 |
lemmas rotater_add = rotater_eqs (2) |
|
260 |
||
261 |
lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)" |
|
262 |
by (induct xs) auto |
|
263 |
||
264 |
lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)" |
|
265 |
by (cases xs) (auto simp: rotater1_def last_map butlast_map) |
|
266 |
||
267 |
lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)" |
|
268 |
by (induct n) (auto simp: rotater_def rotater1_map) |
|
269 |
||
270 |
lemma but_last_zip [rule_format] : |
|
271 |
"\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow> |
|
272 |
last (zip xs ys) = (last xs, last ys) \<and> |
|
273 |
butlast (zip xs ys) = zip (butlast xs) (butlast ys)" |
|
274 |
apply (induct xs) |
|
275 |
apply auto |
|
276 |
apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+ |
|
277 |
done |
|
278 |
||
279 |
lemma but_last_map2 [rule_format] : |
|
280 |
"\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow> |
|
281 |
last (map2 f xs ys) = f (last xs) (last ys) \<and> |
|
282 |
butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)" |
|
283 |
apply (induct xs) |
|
284 |
apply auto |
|
285 |
apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+ |
|
286 |
done |
|
287 |
||
288 |
lemma rotater1_zip: |
|
289 |
"length xs = length ys \<Longrightarrow> |
|
290 |
rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)" |
|
291 |
apply (unfold rotater1_def) |
|
292 |
apply (cases xs) |
|
293 |
apply auto |
|
294 |
apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+ |
|
295 |
done |
|
296 |
||
297 |
lemma rotater1_map2: |
|
298 |
"length xs = length ys \<Longrightarrow> |
|
299 |
rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)" |
|
300 |
by (simp add: rotater1_map rotater1_zip) |
|
301 |
||
302 |
lemmas lrth = |
|
303 |
box_equals [OF asm_rl length_rotater [symmetric] |
|
304 |
length_rotater [symmetric], |
|
305 |
THEN rotater1_map2] |
|
306 |
||
307 |
lemma rotater_map2: |
|
308 |
"length xs = length ys \<Longrightarrow> |
|
309 |
rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)" |
|
310 |
by (induct n) (auto intro!: lrth) |
|
311 |
||
312 |
lemma rotate1_map2: |
|
313 |
"length xs = length ys \<Longrightarrow> |
|
314 |
rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" |
|
315 |
by (cases xs; cases ys) auto |
|
316 |
||
317 |
lemmas lth = box_equals [OF asm_rl length_rotate [symmetric] |
|
318 |
length_rotate [symmetric], THEN rotate1_map2] |
|
319 |
||
320 |
lemma rotate_map2: |
|
321 |
"length xs = length ys \<Longrightarrow> |
|
322 |
rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)" |
|
323 |
by (induct n) (auto intro!: lth) |
|
324 |
||
72081
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
325 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
326 |
subsection \<open>Explicit bit representation of \<^typ>\<open>int\<close>\<close> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
327 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
328 |
primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
329 |
where |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
330 |
Nil: "bl_to_bin_aux [] w = w" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
331 |
| Cons: "bl_to_bin_aux (b # bs) w = bl_to_bin_aux bs (of_bool b + 2 * w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
332 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
333 |
definition bl_to_bin :: "bool list \<Rightarrow> int" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
334 |
where "bl_to_bin bs = bl_to_bin_aux bs 0" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
335 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
336 |
primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
337 |
where |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
338 |
Z: "bin_to_bl_aux 0 w bl = bl" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
339 |
| Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
340 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
341 |
definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
342 |
where "bin_to_bl n w = bin_to_bl_aux n w []" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
343 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
344 |
lemma bin_to_bl_aux_zero_minus_simp [simp]: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
345 |
"0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
346 |
by (cases n) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
347 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
348 |
lemma bin_to_bl_aux_minus1_minus_simp [simp]: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
349 |
"0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
350 |
by (cases n) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
351 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
352 |
lemma bin_to_bl_aux_one_minus_simp [simp]: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
353 |
"0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
354 |
by (cases n) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
355 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
356 |
lemma bin_to_bl_aux_Bit0_minus_simp [simp]: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
357 |
"0 < n \<Longrightarrow> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
358 |
bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
359 |
by (cases n) simp_all |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
360 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
361 |
lemma bin_to_bl_aux_Bit1_minus_simp [simp]: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
362 |
"0 < n \<Longrightarrow> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
363 |
bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
364 |
by (cases n) simp_all |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
365 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
366 |
lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
367 |
by (induct bs arbitrary: w) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
368 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
369 |
lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
370 |
by (induct n arbitrary: w bs) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
371 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
372 |
lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
373 |
unfolding bl_to_bin_def by (rule bl_to_bin_aux_append) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
374 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
375 |
lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
376 |
by (simp add: bin_to_bl_def bin_to_bl_aux_append) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
377 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
378 |
lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
379 |
by (auto simp: bin_to_bl_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
380 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
381 |
lemma size_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
382 |
by (induct n arbitrary: w bs) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
383 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
384 |
lemma size_bin_to_bl [simp]: "length (bin_to_bl n w) = n" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
385 |
by (simp add: bin_to_bl_def size_bin_to_bl_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
386 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
387 |
lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
388 |
apply (induct bs arbitrary: w n) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
389 |
apply auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
390 |
apply (simp_all only: add_Suc [symmetric]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
391 |
apply (auto simp add: bin_to_bl_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
392 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
393 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
394 |
lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
395 |
unfolding bl_to_bin_def |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
396 |
apply (rule box_equals) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
397 |
apply (rule bl_bin_bl') |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
398 |
prefer 2 |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
399 |
apply (rule bin_to_bl_aux.Z) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
400 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
401 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
402 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
403 |
lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
404 |
apply (rule_tac box_equals) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
405 |
defer |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
406 |
apply (rule bl_bin_bl) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
407 |
apply (rule bl_bin_bl) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
408 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
409 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
410 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
411 |
lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
412 |
by (auto simp: bl_to_bin_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
413 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
414 |
lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
415 |
by (auto simp: bl_to_bin_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
416 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
417 |
lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
418 |
by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
419 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
420 |
lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
421 |
by (simp add: bin_to_bl_def bin_to_bl_zero_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
422 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
423 |
lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
424 |
by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
425 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
426 |
lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
427 |
by (simp add: bin_to_bl_def bin_to_bl_minus1_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
428 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
429 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
430 |
subsection \<open>Semantic interpretation of \<^typ>\<open>bool list\<close> as \<^typ>\<open>int\<close>\<close> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
431 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
432 |
lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
433 |
by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def take_bit_Suc ac_simps mod_2_eq_odd) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
434 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
435 |
lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
436 |
by (auto simp: bin_to_bl_def bin_bl_bin') |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
437 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
438 |
lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
439 |
by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
440 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
441 |
lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (bintrunc m w) = bin_to_bl n w" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
442 |
by (auto intro: bl_to_bin_inj) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
443 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
444 |
lemma bin_to_bl_aux_bintr: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
445 |
"bin_to_bl_aux n (bintrunc m bin) bl = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
446 |
replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
447 |
apply (induct n arbitrary: m bin bl) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
448 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
449 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
450 |
apply (case_tac "m") |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
451 |
apply (clarsimp simp: bin_to_bl_zero_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
452 |
apply (erule thin_rl) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
453 |
apply (induct_tac n) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
454 |
apply (auto simp add: take_bit_Suc) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
455 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
456 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
457 |
lemma bin_to_bl_bintr: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
458 |
"bin_to_bl n (bintrunc m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
459 |
unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
460 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
461 |
lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
462 |
by (induct n) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
463 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
464 |
lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
465 |
by (fact size_bin_to_bl_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
466 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
467 |
lemma len_bin_to_bl: "length (bin_to_bl n w) = n" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
468 |
by (fact size_bin_to_bl) (* FIXME: duplicate *) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
469 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
470 |
lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
471 |
by (induction bs arbitrary: w) (simp_all add: bin_sign_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
472 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
473 |
lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
474 |
by (simp add: bl_to_bin_def sign_bl_bin') |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
475 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
476 |
lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
477 |
by (induction n arbitrary: w bs) (auto simp add: bin_sign_def even_iff_mod_2_eq_zero bit_Suc) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
478 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
479 |
lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
480 |
unfolding bin_to_bl_def by (rule bl_sbin_sign_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
481 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
482 |
lemma bin_nth_of_bl_aux: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
483 |
"bin_nth (bl_to_bin_aux bl w) n = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
484 |
(n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bin_nth w (n - size bl))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
485 |
apply (induction bl arbitrary: w) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
486 |
apply simp_all |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
487 |
apply safe |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
488 |
apply (simp_all add: not_le nth_append bit_double_iff even_bit_succ_iff split: if_splits) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
489 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
490 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
491 |
lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
492 |
by (simp add: bl_to_bin_def bin_nth_of_bl_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
493 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
494 |
lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
495 |
apply (induct n arbitrary: m w) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
496 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
497 |
apply (case_tac m, clarsimp) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
498 |
apply (clarsimp simp: bin_to_bl_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
499 |
apply (simp add: bin_to_bl_aux_alt) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
500 |
apply (case_tac m, clarsimp) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
501 |
apply (clarsimp simp: bin_to_bl_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
502 |
apply (simp add: bin_to_bl_aux_alt bit_Suc) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
503 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
504 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
505 |
lemma nth_bin_to_bl_aux: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
506 |
"n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
507 |
(if n < m then bit w (m - 1 - n) else bl ! (n - m))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
508 |
apply (induction bl arbitrary: w) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
509 |
apply simp_all |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
510 |
apply (simp add: bin_nth_bl [of \<open>m - Suc n\<close> m] rev_nth flip: bin_to_bl_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
511 |
apply (metis One_nat_def Suc_pred add_diff_cancel_left' |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
512 |
add_diff_cancel_right' bin_to_bl_aux_alt bin_to_bl_def |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
513 |
diff_Suc_Suc diff_is_0_eq diff_zero less_Suc_eq_0_disj |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
514 |
less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append size_bin_to_bl_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
515 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
516 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
517 |
lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
518 |
by (simp add: bin_to_bl_def nth_bin_to_bl_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
519 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
520 |
lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
521 |
apply (rule nth_equalityI) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
522 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
523 |
apply (clarsimp simp: nth_takefill rev_nth nth_bin_to_bl bin_nth_of_bl) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
524 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
525 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
526 |
lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
527 |
by (simp add: takefill_bintrunc) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
528 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
529 |
lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
530 |
proof (induction bs arbitrary: w) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
531 |
case Nil |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
532 |
then show ?case |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
533 |
by simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
534 |
next |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
535 |
case (Cons b bs) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
536 |
from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>] |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
537 |
show ?case |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
538 |
apply (auto simp add: algebra_simps) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
539 |
apply (subst mult_2 [of \<open>2 ^ length bs\<close>]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
540 |
apply (simp only: add.assoc) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
541 |
apply (rule pos_add_strict) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
542 |
apply simp_all |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
543 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
544 |
qed |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
545 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
546 |
lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
547 |
proof (induct bs) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
548 |
case Nil |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
549 |
then show ?case by simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
550 |
next |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
551 |
case (Cons b bs) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
552 |
with bl_to_bin_lt2p_aux[where w=1] show ?case |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
553 |
by (simp add: bl_to_bin_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
554 |
qed |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
555 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
556 |
lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
557 |
by (metis bin_bl_bin bintr_lt2p bl_bin_bl) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
558 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
559 |
lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
560 |
proof (induction bs arbitrary: w) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
561 |
case Nil |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
562 |
then show ?case |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
563 |
by simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
564 |
next |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
565 |
case (Cons b bs) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
566 |
from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>] |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
567 |
show ?case |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
568 |
apply (auto simp add: algebra_simps) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
569 |
apply (rule add_le_imp_le_left [of \<open>2 ^ length bs\<close>]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
570 |
apply (rule add_increasing) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
571 |
apply simp_all |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
572 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
573 |
qed |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
574 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
575 |
lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
576 |
apply (unfold bl_to_bin_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
577 |
apply (rule xtrans(4)) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
578 |
apply (rule bl_to_bin_ge2p_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
579 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
580 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
581 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
582 |
lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
583 |
apply (unfold bin_to_bl_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
584 |
apply (cases n, clarsimp) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
585 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
586 |
apply (auto simp add: bin_to_bl_aux_alt) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
587 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
588 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
589 |
lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
590 |
using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
591 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
592 |
lemma butlast_rest_bl2bin_aux: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
593 |
"bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
594 |
by (induct bl arbitrary: w) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
595 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
596 |
lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
597 |
by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
598 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
599 |
lemma trunc_bl2bin_aux: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
600 |
"bintrunc m (bl_to_bin_aux bl w) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
601 |
bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
602 |
proof (induct bl arbitrary: w) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
603 |
case Nil |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
604 |
show ?case by simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
605 |
next |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
606 |
case (Cons b bl) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
607 |
show ?case |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
608 |
proof (cases "m - length bl") |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
609 |
case 0 |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
610 |
then have "Suc (length bl) - m = Suc (length bl - m)" by simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
611 |
with Cons show ?thesis by simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
612 |
next |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
613 |
case (Suc n) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
614 |
then have "m - Suc (length bl) = n" by simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
615 |
with Cons Suc show ?thesis by (simp add: take_bit_Suc ac_simps) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
616 |
qed |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
617 |
qed |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
618 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
619 |
lemma trunc_bl2bin: "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
620 |
by (simp add: bl_to_bin_def trunc_bl2bin_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
621 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
622 |
lemma trunc_bl2bin_len [simp]: "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
623 |
by (simp add: trunc_bl2bin) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
624 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
625 |
lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
626 |
apply (rule trans) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
627 |
prefer 2 |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
628 |
apply (rule trunc_bl2bin [symmetric]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
629 |
apply (cases "k \<le> length bl") |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
630 |
apply auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
631 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
632 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
633 |
lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
634 |
apply (rule nth_equalityI) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
635 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
636 |
apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
637 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
638 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
639 |
lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
640 |
by (induct xs arbitrary: w) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
641 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
642 |
lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
643 |
unfolding bl_to_bin_def by (erule last_bin_last') |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
644 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
645 |
lemma bin_last_last: "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
646 |
by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
647 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
648 |
lemma drop_bin2bl_aux: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
649 |
"drop m (bin_to_bl_aux n bin bs) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
650 |
bin_to_bl_aux (n - m) bin (drop (m - n) bs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
651 |
apply (induction n arbitrary: m bin bs) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
652 |
apply auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
653 |
apply (case_tac "m \<le> n") |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
654 |
apply (auto simp add: not_le Suc_diff_le) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
655 |
apply (case_tac "m - n") |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
656 |
apply auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
657 |
apply (use Suc_diff_Suc in fastforce) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
658 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
659 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
660 |
lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
661 |
by (simp add: bin_to_bl_def drop_bin2bl_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
662 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
663 |
lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
664 |
apply (induct m arbitrary: w bs) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
665 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
666 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
667 |
apply (simp add: bin_to_bl_aux_alt) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
668 |
apply (simp add: bin_to_bl_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
669 |
apply (simp add: bin_to_bl_aux_alt) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
670 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
671 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
672 |
lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
673 |
by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
674 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
675 |
lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
676 |
apply (induct n arbitrary: b c) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
677 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
678 |
apply (clarsimp simp: Let_def split: prod.split_asm) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
679 |
apply (simp add: bin_to_bl_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
680 |
apply (simp add: take_bin2bl_lem drop_bit_Suc) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
681 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
682 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
683 |
lemma bin_to_bl_drop_bit: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
684 |
"k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
685 |
using bin_split_take by simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
686 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
687 |
lemma bin_split_take1: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
688 |
"k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
689 |
using bin_split_take by simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
690 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
691 |
lemma bl_bin_bl_rep_drop: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
692 |
"bin_to_bl n (bl_to_bin bl) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
693 |
replicate (n - length bl) False @ drop (length bl - n) bl" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
694 |
by (simp add: bl_to_bin_inj bl_to_bin_rep_F trunc_bl2bin) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
695 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
696 |
lemma bl_to_bin_aux_cat: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
697 |
"bl_to_bin_aux bs (bin_cat w nv v) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
698 |
bin_cat w (nv + length bs) (bl_to_bin_aux bs v)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
699 |
by (rule bit_eqI) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
700 |
(auto simp add: bin_nth_of_bl_aux bin_nth_cat algebra_simps) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
701 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
702 |
lemma bin_to_bl_aux_cat: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
703 |
"bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
704 |
bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
705 |
by (induction nw arbitrary: w bs) (simp_all add: concat_bit_Suc) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
706 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
707 |
lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
708 |
using bl_to_bin_aux_cat [where nv = "0" and v = "0"] |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
709 |
by (simp add: bl_to_bin_def [symmetric]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
710 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
711 |
lemma bin_to_bl_cat: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
712 |
"bin_to_bl (nv + nw) (bin_cat v nw w) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
713 |
bin_to_bl_aux nv v (bin_to_bl nw w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
714 |
by (simp add: bin_to_bl_def bin_to_bl_aux_cat) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
715 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
716 |
lemmas bl_to_bin_aux_app_cat = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
717 |
trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt] |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
718 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
719 |
lemmas bin_to_bl_aux_cat_app = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
720 |
trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt] |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
721 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
722 |
lemma bl_to_bin_app_cat: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
723 |
"bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
724 |
by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
725 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
726 |
lemma bin_to_bl_cat_app: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
727 |
"bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
728 |
by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
729 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
730 |
text \<open>\<open>bl_to_bin_app_cat_alt\<close> and \<open>bl_to_bin_app_cat\<close> are easily interderivable.\<close> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
731 |
lemma bl_to_bin_app_cat_alt: "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
732 |
by (simp add: bl_to_bin_app_cat) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
733 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
734 |
lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
735 |
apply (unfold bl_to_bin_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
736 |
apply (induct n) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
737 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
738 |
apply (simp only: Suc_eq_plus1 replicate_add append_Cons [symmetric] bl_to_bin_aux_append) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
739 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
740 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
741 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
742 |
lemma bin_exhaust: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
743 |
"(\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q) \<Longrightarrow> Q" for bin :: int |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
744 |
apply (cases \<open>even bin\<close>) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
745 |
apply (auto elim!: evenE oddE) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
746 |
apply fastforce |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
747 |
apply fastforce |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
748 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
749 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
750 |
primrec rbl_succ :: "bool list \<Rightarrow> bool list" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
751 |
where |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
752 |
Nil: "rbl_succ Nil = Nil" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
753 |
| Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
754 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
755 |
primrec rbl_pred :: "bool list \<Rightarrow> bool list" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
756 |
where |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
757 |
Nil: "rbl_pred Nil = Nil" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
758 |
| Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
759 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
760 |
primrec rbl_add :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
761 |
where \<comment> \<open>result is length of first arg, second arg may be longer\<close> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
762 |
Nil: "rbl_add Nil x = Nil" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
763 |
| Cons: "rbl_add (y # ys) x = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
764 |
(let ws = rbl_add ys (tl x) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
765 |
in (y \<noteq> hd x) # (if hd x \<and> y then rbl_succ ws else ws))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
766 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
767 |
primrec rbl_mult :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
768 |
where \<comment> \<open>result is length of first arg, second arg may be longer\<close> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
769 |
Nil: "rbl_mult Nil x = Nil" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
770 |
| Cons: "rbl_mult (y # ys) x = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
771 |
(let ws = False # rbl_mult ys x |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
772 |
in if y then rbl_add ws x else ws)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
773 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
774 |
lemma size_rbl_pred: "length (rbl_pred bl) = length bl" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
775 |
by (induct bl) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
776 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
777 |
lemma size_rbl_succ: "length (rbl_succ bl) = length bl" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
778 |
by (induct bl) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
779 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
780 |
lemma size_rbl_add: "length (rbl_add bl cl) = length bl" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
781 |
by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
782 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
783 |
lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
784 |
by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
785 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
786 |
lemmas rbl_sizes [simp] = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
787 |
size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
788 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
789 |
lemmas rbl_Nils = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
790 |
rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
791 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
792 |
lemma rbl_add_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
793 |
apply (induct bla arbitrary: blb) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
794 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
795 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
796 |
apply (case_tac blb, clarsimp) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
797 |
apply (clarsimp simp: Let_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
798 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
799 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
800 |
lemma rbl_add_take2: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
801 |
"length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
802 |
apply (induct bla arbitrary: blb) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
803 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
804 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
805 |
apply (case_tac blb, clarsimp) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
806 |
apply (clarsimp simp: Let_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
807 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
808 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
809 |
lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
810 |
apply (induct bla arbitrary: blb) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
811 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
812 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
813 |
apply (case_tac blb, clarsimp) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
814 |
apply (clarsimp simp: Let_def rbl_add_app2) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
815 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
816 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
817 |
lemma rbl_mult_take2: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
818 |
"length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
819 |
apply (rule trans) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
820 |
apply (rule rbl_mult_app2 [symmetric]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
821 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
822 |
apply (rule_tac f = "rbl_mult bla" in arg_cong) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
823 |
apply (rule append_take_drop_id) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
824 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
825 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
826 |
lemma rbl_add_split: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
827 |
"P (rbl_add (y # ys) (x # xs)) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
828 |
(\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
829 |
(y \<longrightarrow> ((x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws)))) \<and> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
830 |
(\<not> y \<longrightarrow> P (x # ws)))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
831 |
by (cases y) (auto simp: Let_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
832 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
833 |
lemma rbl_mult_split: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
834 |
"P (rbl_mult (y # ys) xs) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
835 |
(\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
836 |
(y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
837 |
by (auto simp: Let_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
838 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
839 |
lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
840 |
proof (unfold bin_to_bl_def, induction n arbitrary: bin) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
841 |
case 0 |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
842 |
then show ?case |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
843 |
by simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
844 |
next |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
845 |
case (Suc n) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
846 |
obtain b k where \<open>bin = of_bool b + 2 * k\<close> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
847 |
using bin_exhaust by blast |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
848 |
moreover have \<open>(2 * k - 1) div 2 = k - 1\<close> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
849 |
using even_succ_div_2 [of \<open>2 * (k - 1)\<close>] |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
850 |
by simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
851 |
ultimately show ?case |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
852 |
using Suc [of \<open>bin div 2\<close>] |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
853 |
by simp (simp add: bin_to_bl_aux_alt) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
854 |
qed |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
855 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
856 |
lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
857 |
apply (unfold bin_to_bl_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
858 |
apply (induction n arbitrary: bin) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
859 |
apply simp_all |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
860 |
apply (case_tac bin rule: bin_exhaust) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
861 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
862 |
apply (simp add: bin_to_bl_aux_alt ac_simps) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
863 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
864 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
865 |
lemma rbl_add: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
866 |
"\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
867 |
rev (bin_to_bl n (bina + binb))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
868 |
apply (unfold bin_to_bl_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
869 |
apply (induct n) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
870 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
871 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
872 |
apply (case_tac bina rule: bin_exhaust) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
873 |
apply (case_tac binb rule: bin_exhaust) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
874 |
apply (case_tac b) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
875 |
apply (case_tac [!] "ba") |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
876 |
apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
877 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
878 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
879 |
lemma rbl_add_long: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
880 |
"m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
881 |
rev (bin_to_bl n (bina + binb))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
882 |
apply (rule box_equals [OF _ rbl_add_take2 rbl_add]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
883 |
apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
884 |
apply (rule rev_swap [THEN iffD1]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
885 |
apply (simp add: rev_take drop_bin2bl) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
886 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
887 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
888 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
889 |
lemma rbl_mult_gt1: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
890 |
"m \<ge> length bl \<Longrightarrow> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
891 |
rbl_mult bl (rev (bin_to_bl m binb)) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
892 |
rbl_mult bl (rev (bin_to_bl (length bl) binb))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
893 |
apply (rule trans) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
894 |
apply (rule rbl_mult_take2 [symmetric]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
895 |
apply simp_all |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
896 |
apply (rule_tac f = "rbl_mult bl" in arg_cong) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
897 |
apply (rule rev_swap [THEN iffD1]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
898 |
apply (simp add: rev_take drop_bin2bl) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
899 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
900 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
901 |
lemma rbl_mult_gt: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
902 |
"m > n \<Longrightarrow> |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
903 |
rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
904 |
rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
905 |
by (auto intro: trans [OF rbl_mult_gt1]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
906 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
907 |
lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt] |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
908 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
909 |
lemma rbbl_Cons: "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (of_bool b + 2 * x))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
910 |
by (simp add: bin_to_bl_def) (simp add: bin_to_bl_aux_alt) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
911 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
912 |
lemma rbl_mult: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
913 |
"rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
914 |
rev (bin_to_bl n (bina * binb))" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
915 |
apply (induct n arbitrary: bina binb) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
916 |
apply simp_all |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
917 |
apply (unfold bin_to_bl_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
918 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
919 |
apply (case_tac bina rule: bin_exhaust) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
920 |
apply (case_tac binb rule: bin_exhaust) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
921 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
922 |
apply (simp add: bin_to_bl_aux_alt) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
923 |
apply (simp add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
924 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
925 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
926 |
lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
927 |
by (induct xs) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
928 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
929 |
lemma bin_cat_foldl_lem: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
930 |
"foldl (\<lambda>u. bin_cat u n) x xs = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
931 |
bin_cat x (size xs * n) (foldl (\<lambda>u. bin_cat u n) y xs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
932 |
apply (induct xs arbitrary: x) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
933 |
apply simp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
934 |
apply (simp (no_asm)) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
935 |
apply (frule asm_rl) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
936 |
apply (drule meta_spec) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
937 |
apply (erule trans) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
938 |
apply (drule_tac x = "bin_cat y n a" in meta_spec) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
939 |
apply (simp add: bin_cat_assoc_sym min.absorb2) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
940 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
941 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
942 |
lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))" |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
943 |
apply (unfold bin_rcat_eq_foldl) |
72081
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
944 |
apply (rule sym) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
945 |
apply (induct wl) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
946 |
apply (auto simp add: bl_to_bin_append) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
947 |
apply (simp add: bl_to_bin_aux_alt sclem) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
948 |
apply (simp add: bin_cat_foldl_lem [symmetric]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
949 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
950 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
951 |
lemma bin_last_bl_to_bin: "bin_last (bl_to_bin bs) \<longleftrightarrow> bs \<noteq> [] \<and> last bs" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
952 |
by(cases "bs = []")(auto simp add: bl_to_bin_def last_bin_last'[where w=0]) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
953 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
954 |
lemma bin_rest_bl_to_bin: "bin_rest (bl_to_bin bs) = bl_to_bin (butlast bs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
955 |
by(cases "bs = []")(simp_all add: bl_to_bin_def butlast_rest_bl2bin_aux) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
956 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
957 |
lemma bl_xor_aux_bin: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
958 |
"map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
959 |
bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
960 |
apply (induction n arbitrary: v w bs cs) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
961 |
apply auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
962 |
apply (case_tac v rule: bin_exhaust) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
963 |
apply (case_tac w rule: bin_exhaust) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
964 |
apply clarsimp |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
965 |
done |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
966 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
967 |
lemma bl_or_aux_bin: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
968 |
"map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
969 |
bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
970 |
by (induct n arbitrary: v w bs cs) simp_all |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
971 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
972 |
lemma bl_and_aux_bin: |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
973 |
"map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
974 |
bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
975 |
by (induction n arbitrary: v w bs cs) simp_all |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
976 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
977 |
lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
978 |
by (induct n arbitrary: w cs) auto |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
979 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
980 |
lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
981 |
by (simp add: bin_to_bl_def bl_not_aux_bin) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
982 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
983 |
lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
984 |
by (simp add: bin_to_bl_def bl_and_aux_bin) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
985 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
986 |
lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
987 |
by (simp add: bin_to_bl_def bl_or_aux_bin) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
988 |
|
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
989 |
lemma bl_xor_bin: "map2 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)" |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
990 |
using bl_xor_aux_bin by (simp add: bin_to_bl_def) |
e4d42f5766dc
clearer separation of pre-word bit list material
haftmann
parents:
72079
diff
changeset
|
991 |
|
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
992 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
993 |
subsection \<open>Type \<^typ>\<open>'a word\<close>\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
994 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
995 |
lift_definition of_bl :: \<open>bool list \<Rightarrow> 'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
996 |
is bl_to_bin . |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
997 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
998 |
lift_definition to_bl :: \<open>'a::len word \<Rightarrow> bool list\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
999 |
is \<open>bin_to_bl LENGTH('a)\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1000 |
by (simp add: bl_to_bin_inj) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1001 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1002 |
lemma to_bl_eq: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1003 |
\<open>to_bl w = bin_to_bl (LENGTH('a)) (uint w)\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1004 |
for w :: \<open>'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1005 |
by transfer simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1006 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1007 |
lemma bit_of_bl_iff: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1008 |
\<open>bit (of_bl bs :: 'a word) n \<longleftrightarrow> rev bs ! n \<and> n < LENGTH('a::len) \<and> n < length bs\<close> |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1009 |
by transfer (simp add: bin_nth_of_bl ac_simps) |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1010 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1011 |
lemma rev_to_bl_eq: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1012 |
\<open>rev (to_bl w) = map (bit w) [0..<LENGTH('a)]\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1013 |
for w :: \<open>'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1014 |
apply (rule nth_equalityI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1015 |
apply (simp add: to_bl.rep_eq) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1016 |
apply (simp add: bin_nth_bl bit_word.rep_eq to_bl.rep_eq) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1017 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1018 |
|
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1019 |
lemma to_bl_eq_rev: |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1020 |
\<open>to_bl w = map (bit w) (rev [0..<LENGTH('a)])\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1021 |
for w :: \<open>'a::len word\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1022 |
using rev_to_bl_eq [of w] |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1023 |
apply (subst rev_is_rev_conv [symmetric]) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1024 |
apply (simp add: rev_map) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1025 |
done |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1026 |
|
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1027 |
lemma of_bl_rev_eq: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1028 |
\<open>of_bl (rev bs) = horner_sum of_bool 2 bs\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1029 |
apply (rule bit_word_eqI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1030 |
apply (simp add: bit_of_bl_iff) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1031 |
apply transfer |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1032 |
apply (simp add: bit_horner_sum_bit_iff ac_simps) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1033 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1034 |
|
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1035 |
lemma of_bl_eq: |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1036 |
\<open>of_bl bs = horner_sum of_bool 2 (rev bs)\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1037 |
using of_bl_rev_eq [of \<open>rev bs\<close>] by simp |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1038 |
|
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1039 |
lemma bshiftr1_eq: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1040 |
\<open>bshiftr1 b w = of_bl (b # butlast (to_bl w))\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1041 |
apply transfer |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1042 |
apply auto |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1043 |
apply (subst bl_to_bin_app_cat [of \<open>[True]\<close>, simplified]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1044 |
apply simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1045 |
apply (metis One_nat_def add.commute bin_bl_bin bin_last_bl_to_bin bin_rest_bl_to_bin butlast_bin_rest concat_bit_eq last.simps list.distinct(1) list.size(3) list.size(4) odd_iff_mod_2_eq_one plus_1_eq_Suc power_Suc0_right push_bit_of_1 size_bin_to_bl take_bit_eq_mod trunc_bl2bin_len) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1046 |
apply (simp add: butlast_rest_bl2bin) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1047 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1048 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1049 |
lemma length_to_bl_eq: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1050 |
\<open>length (to_bl w) = LENGTH('a)\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1051 |
for w :: \<open>'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1052 |
by transfer simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1053 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1054 |
lemma word_rotr_eq: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1055 |
\<open>word_rotr n w = of_bl (rotater n (to_bl w))\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1056 |
apply (rule bit_word_eqI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1057 |
subgoal for n |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1058 |
apply (cases \<open>n < LENGTH('a)\<close>) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1059 |
apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff rotater_rev length_to_bl_eq nth_rotate rev_to_bl_eq ac_simps) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1060 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1061 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1062 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1063 |
lemma word_rotl_eq: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1064 |
\<open>word_rotl n w = of_bl (rotate n (to_bl w))\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1065 |
proof - |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1066 |
have \<open>rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1067 |
by (simp add: rotater_rev') |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1068 |
then show ?thesis |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1069 |
apply (simp add: word_rotl_eq_word_rotr bit_of_bl_iff length_to_bl_eq rev_to_bl_eq) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1070 |
apply (rule bit_word_eqI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1071 |
subgoal for n |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1072 |
apply (cases \<open>n < LENGTH('a)\<close>) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1073 |
apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff nth_rotater) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1074 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1075 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1076 |
qed |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1077 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1078 |
lemma to_bl_def': "(to_bl :: 'a::len word \<Rightarrow> bool list) = bin_to_bl (LENGTH('a)) \<circ> uint" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1079 |
by transfer (simp add: fun_eq_iff) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1080 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1081 |
\<comment> \<open>type definitions theorem for in terms of equivalent bool list\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1082 |
lemma td_bl: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1083 |
"type_definition |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1084 |
(to_bl :: 'a::len word \<Rightarrow> bool list) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1085 |
of_bl |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1086 |
{bl. length bl = LENGTH('a)}" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1087 |
apply (standard; transfer) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1088 |
apply (auto dest: sym) |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1089 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1090 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1091 |
interpretation word_bl: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1092 |
type_definition |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1093 |
"to_bl :: 'a::len word \<Rightarrow> bool list" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1094 |
of_bl |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1095 |
"{bl. length bl = LENGTH('a::len)}" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1096 |
by (fact td_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1097 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1098 |
lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1099 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1100 |
lemma word_size_bl: "size w = size (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1101 |
by (auto simp: word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1102 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1103 |
lemma to_bl_use_of_bl: "to_bl w = bl \<longleftrightarrow> w = of_bl bl \<and> length bl = length (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1104 |
by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1105 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1106 |
lemma length_bl_gt_0 [iff]: "0 < length (to_bl x)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1107 |
for x :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1108 |
unfolding word_bl_Rep' by (rule len_gt_0) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1109 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1110 |
lemma bl_not_Nil [iff]: "to_bl x \<noteq> []" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1111 |
for x :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1112 |
by (fact length_bl_gt_0 [unfolded length_greater_0_conv]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1113 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1114 |
lemma length_bl_neq_0 [iff]: "length (to_bl x) \<noteq> 0" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1115 |
for x :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1116 |
by (fact length_bl_gt_0 [THEN gr_implies_not0]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1117 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1118 |
lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1119 |
apply transfer |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1120 |
apply (auto simp add: bin_sign_def) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1121 |
using bin_sign_lem bl_sbin_sign apply fastforce |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1122 |
using bin_sign_lem bl_sbin_sign apply force |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1123 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1124 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1125 |
lemma of_bl_drop': |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1126 |
"lend = length bl - LENGTH('a::len) \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1127 |
of_bl (drop lend bl) = (of_bl bl :: 'a word)" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1128 |
by transfer (simp flip: trunc_bl2bin) |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1129 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1130 |
lemma test_bit_of_bl: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1131 |
"(of_bl bl::'a::len word) !! n = (rev bl ! n \<and> n < LENGTH('a) \<and> n < length bl)" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1132 |
by transfer (simp add: bin_nth_of_bl ac_simps) |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1133 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1134 |
lemma no_of_bl: "(numeral bin ::'a::len word) = of_bl (bin_to_bl (LENGTH('a)) (numeral bin))" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1135 |
by transfer simp |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1136 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1137 |
lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1138 |
by transfer simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1139 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1140 |
lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1141 |
by (simp add: uint_bl word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1142 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1143 |
lemma to_bl_of_bin: "to_bl (word_of_int bin::'a::len word) = bin_to_bl (LENGTH('a)) bin" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1144 |
by (auto simp: uint_bl word_ubin.eq_norm word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1145 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1146 |
lemma to_bl_numeral [simp]: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1147 |
"to_bl (numeral bin::'a::len word) = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1148 |
bin_to_bl (LENGTH('a)) (numeral bin)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1149 |
unfolding word_numeral_alt by (rule to_bl_of_bin) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1150 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1151 |
lemma to_bl_neg_numeral [simp]: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1152 |
"to_bl (- numeral bin::'a::len word) = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1153 |
bin_to_bl (LENGTH('a)) (- numeral bin)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1154 |
unfolding word_neg_numeral_alt by (rule to_bl_of_bin) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1155 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1156 |
lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1157 |
by (simp add: uint_bl word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1158 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1159 |
lemma uint_bl_bin: "bl_to_bin (bin_to_bl (LENGTH('a)) (uint x)) = uint x" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1160 |
for x :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1161 |
by (rule trans [OF bin_bl_bin word_ubin.norm_Rep]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1162 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1163 |
lemma ucast_bl: "ucast w = of_bl (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1164 |
by transfer simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1165 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1166 |
lemma ucast_down_bl: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1167 |
\<open>(ucast :: 'a::len word \<Rightarrow> 'b::len word) (of_bl bl) = of_bl bl\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1168 |
if \<open>is_down (ucast :: 'a::len word \<Rightarrow> 'b::len word)\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1169 |
using that by transfer simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1170 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1171 |
lemma of_bl_append_same: "of_bl (X @ to_bl w) = w" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1172 |
by transfer (simp add: bl_to_bin_app_cat) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1173 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1174 |
lemma ucast_of_bl_up: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1175 |
\<open>ucast (of_bl bl :: 'a::len word) = of_bl bl\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1176 |
if \<open>size bl \<le> size (of_bl bl :: 'a::len word)\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1177 |
using that |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1178 |
apply transfer |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1179 |
apply (rule bit_eqI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1180 |
apply (auto simp add: bit_take_bit_iff) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1181 |
apply (subst (asm) trunc_bl2bin_len [symmetric]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1182 |
apply (auto simp only: bit_take_bit_iff) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1183 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1184 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1185 |
lemma word_rev_tf: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1186 |
"to_bl (of_bl bl::'a::len word) = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1187 |
rev (takefill False (LENGTH('a)) (rev bl))" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1188 |
by transfer (simp add: bl_bin_bl_rtf) |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1189 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1190 |
lemma word_rep_drop: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1191 |
"to_bl (of_bl bl::'a::len word) = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1192 |
replicate (LENGTH('a) - length bl) False @ |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1193 |
drop (length bl - LENGTH('a)) bl" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1194 |
by (simp add: word_rev_tf takefill_alt rev_take) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1195 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1196 |
lemma to_bl_ucast: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1197 |
"to_bl (ucast (w::'b::len word) ::'a::len word) = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1198 |
replicate (LENGTH('a) - LENGTH('b)) False @ |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1199 |
drop (LENGTH('b) - LENGTH('a)) (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1200 |
apply (unfold ucast_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1201 |
apply (rule trans) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1202 |
apply (rule word_rep_drop) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1203 |
apply simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1204 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1205 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1206 |
lemma ucast_up_app: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1207 |
\<open>to_bl (ucast w :: 'b::len word) = replicate n False @ (to_bl w)\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1208 |
if \<open>source_size (ucast :: 'a word \<Rightarrow> 'b word) + n = target_size (ucast :: 'a word \<Rightarrow> 'b word)\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1209 |
for w :: \<open>'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1210 |
using that |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1211 |
by (auto simp add : source_size target_size to_bl_ucast) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1212 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1213 |
lemma ucast_down_drop [OF refl]: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1214 |
"uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1215 |
to_bl (uc w) = drop n (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1216 |
by (auto simp add : source_size target_size to_bl_ucast) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1217 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1218 |
lemma scast_down_drop [OF refl]: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1219 |
"sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1220 |
to_bl (sc w) = drop n (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1221 |
apply (subgoal_tac "sc = ucast") |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1222 |
apply safe |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1223 |
apply simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1224 |
apply (erule ucast_down_drop) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1225 |
apply (rule down_cast_same [symmetric]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1226 |
apply (simp add : source_size target_size is_down) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1227 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1228 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1229 |
lemma word_0_bl [simp]: "of_bl [] = 0" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1230 |
by transfer simp |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1231 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1232 |
lemma word_1_bl: "of_bl [True] = 1" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1233 |
by transfer (simp add: bl_to_bin_def) |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1234 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1235 |
lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1236 |
by transfer (simp add: bl_to_bin_rep_False) |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1237 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1238 |
lemma to_bl_0 [simp]: "to_bl (0::'a::len word) = replicate (LENGTH('a)) False" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1239 |
by (simp add: uint_bl word_size bin_to_bl_zero) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1240 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1241 |
\<comment> \<open>links with \<open>rbl\<close> operations\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1242 |
lemma word_succ_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1243 |
by transfer (simp add: rbl_succ) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1244 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1245 |
lemma word_pred_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = rev (rbl_pred (rev bl))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1246 |
by transfer (simp add: rbl_pred) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1247 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1248 |
lemma word_add_rbl: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1249 |
"to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1250 |
to_bl (v + w) = rev (rbl_add (rev vbl) (rev wbl))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1251 |
apply transfer |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1252 |
apply (drule sym) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1253 |
apply (drule sym) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1254 |
apply (simp add: rbl_add) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1255 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1256 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1257 |
lemma word_mult_rbl: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1258 |
"to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1259 |
to_bl (v * w) = rev (rbl_mult (rev vbl) (rev wbl))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1260 |
apply transfer |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1261 |
apply (drule sym) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1262 |
apply (drule sym) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1263 |
apply (simp add: rbl_mult) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1264 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1265 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1266 |
lemma rtb_rbl_ariths: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1267 |
"rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1268 |
"rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1269 |
"rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1270 |
"rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1271 |
by (auto simp: rev_swap [symmetric] word_succ_rbl word_pred_rbl word_mult_rbl word_add_rbl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1272 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1273 |
lemma of_bl_length_less: |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1274 |
\<open>(of_bl x :: 'a::len word) < 2 ^ k\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1275 |
if \<open>length x = k\<close> \<open>k < LENGTH('a)\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1276 |
proof - |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1277 |
from that have \<open>length x < LENGTH('a)\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1278 |
by simp |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1279 |
then have \<open>(of_bl x :: 'a::len word) < 2 ^ length x\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1280 |
apply (simp add: of_bl_eq) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1281 |
apply transfer |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1282 |
apply (simp add: take_bit_horner_sum_bit_eq) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1283 |
apply (subst length_rev [symmetric]) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1284 |
apply (simp only: horner_sum_of_bool_2_less) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1285 |
done |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1286 |
with that show ?thesis |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1287 |
by simp |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1288 |
qed |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1289 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1290 |
lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1291 |
by simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1292 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1293 |
lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1294 |
by transfer (simp add: bl_not_bin) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1295 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1296 |
lemma bl_word_xor: "to_bl (v XOR w) = map2 (\<noteq>) (to_bl v) (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1297 |
by transfer (simp flip: bl_xor_bin) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1298 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1299 |
lemma bl_word_or: "to_bl (v OR w) = map2 (\<or>) (to_bl v) (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1300 |
by transfer (simp flip: bl_or_bin) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1301 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1302 |
lemma bl_word_and: "to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1303 |
by transfer (simp flip: bl_and_bin) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1304 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1305 |
lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1306 |
apply (unfold word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1307 |
apply (safe elim!: bin_nth_uint_imp) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1308 |
apply (frule bin_nth_uint_imp) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1309 |
apply (fast dest!: bin_nth_bl)+ |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1310 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1311 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1312 |
lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1313 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1314 |
lemma test_bit_bl: "w !! n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1315 |
by transfer (auto simp add: bin_nth_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1316 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1317 |
lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1318 |
by (simp add: word_size rev_nth test_bit_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1319 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1320 |
lemma map_bit_interval_eq: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1321 |
\<open>map (bit w) [0..<n] = takefill False n (rev (to_bl w))\<close> for w :: \<open>'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1322 |
proof (rule nth_equalityI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1323 |
show \<open>length (map (bit w) [0..<n]) = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1324 |
length (takefill False n (rev (to_bl w)))\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1325 |
by simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1326 |
fix m |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1327 |
assume \<open>m < length (map (bit w) [0..<n])\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1328 |
then have \<open>m < n\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1329 |
by simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1330 |
then have \<open>bit w m \<longleftrightarrow> takefill False n (rev (to_bl w)) ! m\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1331 |
by (auto simp add: nth_takefill not_less rev_nth to_bl_nth word_size test_bit_word_eq dest: bit_imp_le_length) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1332 |
with \<open>m < n \<close>show \<open>map (bit w) [0..<n] ! m \<longleftrightarrow> takefill False n (rev (to_bl w)) ! m\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1333 |
by simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1334 |
qed |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1335 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1336 |
lemma to_bl_unfold: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1337 |
\<open>to_bl w = rev (map (bit w) [0..<LENGTH('a)])\<close> for w :: \<open>'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1338 |
by (simp add: map_bit_interval_eq takefill_bintrunc to_bl_def flip: bin_to_bl_def) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1339 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1340 |
lemma nth_rev_to_bl: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1341 |
\<open>rev (to_bl w) ! n \<longleftrightarrow> bit w n\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1342 |
if \<open>n < LENGTH('a)\<close> for w :: \<open>'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1343 |
using that by (simp add: to_bl_unfold) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1344 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1345 |
lemma nth_to_bl: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1346 |
\<open>to_bl w ! n \<longleftrightarrow> bit w (LENGTH('a) - Suc n)\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1347 |
if \<open>n < LENGTH('a)\<close> for w :: \<open>'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1348 |
using that by (simp add: to_bl_unfold rev_nth) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1349 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1350 |
lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1351 |
by (auto simp: of_bl_def bl_to_bin_rep_F) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1352 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1353 |
lemma [code abstract]: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1354 |
\<open>uint (of_bl bs :: 'a word) = horner_sum of_bool 2 (take LENGTH('a::len) (rev bs))\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1355 |
apply (simp add: of_bl_eq flip: take_bit_horner_sum_bit_eq) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1356 |
apply transfer |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1357 |
apply simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1358 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1359 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1360 |
lemma [code]: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1361 |
\<open>to_bl w = map (bit w) (rev [0..<LENGTH('a::len)])\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1362 |
for w :: \<open>'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1363 |
by (simp add: to_bl_unfold rev_map) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1364 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1365 |
lemma word_reverse_eq_of_bl_rev_to_bl: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1366 |
\<open>word_reverse w = of_bl (rev (to_bl w))\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1367 |
by (rule bit_word_eqI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1368 |
(auto simp add: bit_word_reverse_iff bit_of_bl_iff nth_to_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1369 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1370 |
lemmas word_reverse_no_def [simp] = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1371 |
word_reverse_eq_of_bl_rev_to_bl [of "numeral w"] for w |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1372 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1373 |
lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1374 |
by (rule nth_equalityI) (simp_all add: nth_rev_to_bl word_reverse_def word_rep_drop flip: of_bl_eq) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1375 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1376 |
lemma to_bl_n1 [simp]: "to_bl (-1::'a::len word) = replicate (LENGTH('a)) True" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1377 |
apply (rule word_bl.Abs_inverse') |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1378 |
apply simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1379 |
apply (rule word_eqI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1380 |
apply (clarsimp simp add: word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1381 |
apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1382 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1383 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1384 |
lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1385 |
by (simp add: zip_rev bl_word_or rev_map) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1386 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1387 |
lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1388 |
by (simp add: zip_rev bl_word_and rev_map) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1389 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1390 |
lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 (\<noteq>) (rev (to_bl x)) (rev (to_bl y))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1391 |
by (simp add: zip_rev bl_word_xor rev_map) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1392 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1393 |
lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1394 |
by (simp add: bl_word_not rev_map) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1395 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1396 |
lemma bshiftr1_numeral [simp]: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1397 |
\<open>bshiftr1 b (numeral w :: 'a word) = of_bl (b # butlast (bin_to_bl LENGTH('a::len) (numeral w)))\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1398 |
by (simp add: bshiftr1_eq) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1399 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1400 |
lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1401 |
unfolding bshiftr1_eq by (rule word_bl.Abs_inverse) simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1402 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1403 |
lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1404 |
by transfer (simp add: bl_to_bin_append) |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1405 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1406 |
lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1407 |
for w :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1408 |
proof - |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1409 |
have "shiftl1 w = shiftl1 (of_bl (to_bl w))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1410 |
by simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1411 |
also have "\<dots> = of_bl (to_bl w @ [False])" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1412 |
by (rule shiftl1_of_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1413 |
finally show ?thesis . |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1414 |
qed |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1415 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1416 |
lemma bl_shiftl1: "to_bl (shiftl1 w) = tl (to_bl w) @ [False]" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1417 |
for w :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1418 |
by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1419 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1420 |
\<comment> \<open>Generalized version of \<open>bl_shiftl1\<close>. Maybe this one should replace it?\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1421 |
lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1422 |
by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1423 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1424 |
lemma shiftr1_bl: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1425 |
\<open>shiftr1 w = of_bl (butlast (to_bl w))\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1426 |
proof (rule bit_word_eqI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1427 |
fix n |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1428 |
assume \<open>n < LENGTH('a)\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1429 |
show \<open>bit (shiftr1 w) n \<longleftrightarrow> bit (of_bl (butlast (to_bl w)) :: 'a word) n\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1430 |
proof (cases \<open>n = LENGTH('a) - 1\<close>) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1431 |
case True |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1432 |
then show ?thesis |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1433 |
by (simp add: bit_shiftr1_iff bit_of_bl_iff) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1434 |
next |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1435 |
case False |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1436 |
with \<open>n < LENGTH('a)\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1437 |
have \<open>n < LENGTH('a) - 1\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1438 |
by simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1439 |
with \<open>n < LENGTH('a)\<close> show ?thesis |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1440 |
by (simp add: bit_shiftr1_iff bit_of_bl_iff rev_nth nth_butlast |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1441 |
word_size test_bit_word_eq to_bl_nth) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1442 |
qed |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1443 |
qed |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1444 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1445 |
lemma bl_shiftr1: "to_bl (shiftr1 w) = False # butlast (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1446 |
for w :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1447 |
by (simp add: shiftr1_bl word_rep_drop len_gt_0 [THEN Suc_leI]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1448 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1449 |
\<comment> \<open>Generalized version of \<open>bl_shiftr1\<close>. Maybe this one should replace it?\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1450 |
lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1451 |
apply (rule word_bl.Abs_inverse') |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1452 |
apply (simp del: butlast.simps) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1453 |
apply (simp add: shiftr1_bl of_bl_def) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1454 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1455 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1456 |
lemma bl_sshiftr1: "to_bl (sshiftr1 w) = hd (to_bl w) # butlast (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1457 |
for w :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1458 |
proof (rule nth_equalityI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1459 |
fix n |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1460 |
assume \<open>n < length (to_bl (sshiftr1 w))\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1461 |
then have \<open>n < LENGTH('a)\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1462 |
by simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1463 |
then show \<open>to_bl (sshiftr1 w) ! n \<longleftrightarrow> (hd (to_bl w) # butlast (to_bl w)) ! n\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1464 |
apply (cases n) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1465 |
apply (simp_all add: to_bl_nth word_size hd_conv_nth test_bit_eq_bit bit_sshiftr1_iff nth_butlast Suc_diff_Suc nth_to_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1466 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1467 |
qed simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1468 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1469 |
lemma drop_shiftr: "drop n (to_bl (w >> n)) = take (size w - n) (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1470 |
for w :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1471 |
apply (unfold shiftr_def) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1472 |
apply (induct n) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1473 |
prefer 2 |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1474 |
apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1475 |
apply (rule butlast_take [THEN trans]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1476 |
apply (auto simp: word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1477 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1478 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1479 |
lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1480 |
for w :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1481 |
apply (unfold sshiftr_eq) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1482 |
apply (induct n) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1483 |
prefer 2 |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1484 |
apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1485 |
apply (rule butlast_take [THEN trans]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1486 |
apply (auto simp: word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1487 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1488 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1489 |
lemma take_shiftr: "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1490 |
apply (unfold shiftr_def) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1491 |
apply (induct n) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1492 |
prefer 2 |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1493 |
apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1494 |
apply (rule take_butlast [THEN trans]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1495 |
apply (auto simp: word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1496 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1497 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1498 |
lemma take_sshiftr' [rule_format] : |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1499 |
"n \<le> size w \<longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1500 |
take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1501 |
for w :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1502 |
apply (unfold sshiftr_eq) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1503 |
apply (induct n) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1504 |
prefer 2 |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1505 |
apply (simp add: bl_sshiftr1) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1506 |
apply (rule impI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1507 |
apply (rule take_butlast [THEN trans]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1508 |
apply (auto simp: word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1509 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1510 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1511 |
lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1512 |
lemmas take_sshiftr = take_sshiftr' [THEN conjunct2] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1513 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1514 |
lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1515 |
by (auto intro: append_take_drop_id [symmetric]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1516 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1517 |
lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1518 |
lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1519 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1520 |
lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1521 |
by (induct n) (auto simp: shiftl_def shiftl1_of_bl replicate_app_Cons_same) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1522 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1523 |
lemma shiftl_bl: "w << n = of_bl (to_bl w @ replicate n False)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1524 |
for w :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1525 |
proof - |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1526 |
have "w << n = of_bl (to_bl w) << n" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1527 |
by simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1528 |
also have "\<dots> = of_bl (to_bl w @ replicate n False)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1529 |
by (rule shiftl_of_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1530 |
finally show ?thesis . |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1531 |
qed |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1532 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1533 |
lemma bl_shiftl: "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1534 |
by (simp add: shiftl_bl word_rep_drop word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1535 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1536 |
lemma shiftr1_bl_of: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1537 |
"length bl \<le> LENGTH('a) \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1538 |
shiftr1 (of_bl bl::'a::len word) = of_bl (butlast bl)" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1539 |
by transfer (simp add: butlast_rest_bl2bin trunc_bl2bin) |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1540 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1541 |
lemma shiftr_bl_of: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1542 |
"length bl \<le> LENGTH('a) \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1543 |
(of_bl bl::'a::len word) >> n = of_bl (take (length bl - n) bl)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1544 |
apply (unfold shiftr_def) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1545 |
apply (induct n) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1546 |
apply clarsimp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1547 |
apply clarsimp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1548 |
apply (subst shiftr1_bl_of) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1549 |
apply simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1550 |
apply (simp add: butlast_take) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1551 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1552 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1553 |
lemma shiftr_bl: "x >> n \<equiv> of_bl (take (LENGTH('a) - n) (to_bl x))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1554 |
for x :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1555 |
using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1556 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1557 |
lemma aligned_bl_add_size [OF refl]: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1558 |
"size x - n = m \<Longrightarrow> n \<le> size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1559 |
take m (to_bl y) = replicate m False \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1560 |
to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)" for x :: \<open>'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1561 |
apply (subgoal_tac "x AND y = 0") |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1562 |
prefer 2 |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1563 |
apply (rule word_bl.Rep_eqD) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1564 |
apply (simp add: bl_word_and) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1565 |
apply (rule align_lem_and [THEN trans]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1566 |
apply (simp_all add: word_size)[5] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1567 |
apply simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1568 |
apply (subst word_plus_and_or [symmetric]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1569 |
apply (simp add : bl_word_or) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1570 |
apply (rule align_lem_or) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1571 |
apply (simp_all add: word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1572 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1573 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1574 |
lemma mask_bl: "mask n = of_bl (replicate n True)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1575 |
by (auto simp add : test_bit_of_bl word_size intro: word_eqI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1576 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1577 |
lemma bl_and_mask': |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1578 |
"to_bl (w AND mask n :: 'a::len word) = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1579 |
replicate (LENGTH('a) - n) False @ |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1580 |
drop (LENGTH('a) - n) (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1581 |
apply (rule nth_equalityI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1582 |
apply simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1583 |
apply (clarsimp simp add: to_bl_nth word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1584 |
apply (simp add: word_size word_ops_nth_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1585 |
apply (auto simp add: word_size test_bit_bl nth_append rev_nth) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1586 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1587 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1588 |
lemma slice1_eq_of_bl: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1589 |
\<open>(slice1 n w :: 'b::len word) = of_bl (takefill False n (to_bl w))\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1590 |
for w :: \<open>'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1591 |
proof (rule bit_word_eqI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1592 |
fix m |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1593 |
assume \<open>m < LENGTH('b)\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1594 |
show \<open>bit (slice1 n w :: 'b::len word) m \<longleftrightarrow> bit (of_bl (takefill False n (to_bl w)) :: 'b word) m\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1595 |
by (cases \<open>m \<ge> n\<close>; cases \<open>LENGTH('a) \<ge> n\<close>) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1596 |
(auto simp add: bit_slice1_iff bit_of_bl_iff not_less rev_nth not_le nth_takefill nth_to_bl algebra_simps) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1597 |
qed |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1598 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1599 |
lemma slice1_no_bin [simp]: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1600 |
"slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (LENGTH('b::len)) (numeral w)))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1601 |
by (simp add: slice1_eq_of_bl) (* TODO: neg_numeral *) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1602 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1603 |
lemma slice_no_bin [simp]: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1604 |
"slice n (numeral w :: 'b word) = of_bl (takefill False (LENGTH('b::len) - n) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1605 |
(bin_to_bl (LENGTH('b::len)) (numeral w)))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1606 |
by (simp add: slice_def) (* TODO: neg_numeral *) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1607 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1608 |
lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1609 |
by (simp add: slice_def word_size slice1_eq_of_bl takefill_alt) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1610 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1611 |
lemmas slice_take = slice_take' [unfolded word_size] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1612 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1613 |
\<comment> \<open>shiftr to a word of the same size is just slice, |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1614 |
slice is just shiftr then ucast\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1615 |
lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1616 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1617 |
lemma slice1_down_alt': |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1618 |
"sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1619 |
to_bl sl = takefill False fs (drop k (to_bl w))" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1620 |
apply (simp add: slice1_eq_of_bl) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1621 |
apply transfer |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1622 |
apply (simp add: bl_bin_bl_rep_drop) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1623 |
using drop_takefill |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1624 |
apply force |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1625 |
done |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1626 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1627 |
lemma slice1_up_alt': |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1628 |
"sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1629 |
to_bl sl = takefill False fs (replicate k False @ (to_bl w))" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1630 |
apply (simp add: slice1_eq_of_bl) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1631 |
apply transfer |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1632 |
apply (simp add: bl_bin_bl_rep_drop flip: takefill_append) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1633 |
apply (metis diff_add_inverse) |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1634 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1635 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1636 |
lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1637 |
lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1638 |
lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1639 |
lemmas slice1_up_alts = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1640 |
le_add_diff_inverse [symmetric, THEN su1] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1641 |
le_add_diff_inverse2 [symmetric, THEN su1] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1642 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1643 |
lemma slice1_tf_tf': |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1644 |
"to_bl (slice1 n w :: 'a::len word) = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1645 |
rev (takefill False (LENGTH('a)) (rev (takefill False n (to_bl w))))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1646 |
unfolding slice1_eq_of_bl by (rule word_rev_tf) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1647 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1648 |
lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1649 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1650 |
lemma revcast_eq_of_bl: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1651 |
\<open>(revcast w :: 'b::len word) = of_bl (takefill False (LENGTH('b)) (to_bl w))\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1652 |
for w :: \<open>'a::len word\<close> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1653 |
by (simp add: revcast_def slice1_eq_of_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1654 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1655 |
lemmas revcast_no_def [simp] = revcast_eq_of_bl [where w="numeral w", unfolded word_size] for w |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1656 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1657 |
lemma to_bl_revcast: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1658 |
"to_bl (revcast w :: 'a::len word) = takefill False (LENGTH('a)) (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1659 |
apply (rule nth_equalityI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1660 |
apply simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1661 |
apply (cases \<open>LENGTH('a) \<le> LENGTH('b)\<close>) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1662 |
apply (auto simp add: nth_to_bl nth_takefill bit_revcast_iff) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1663 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1664 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1665 |
lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1666 |
apply (rule bit_word_eqI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1667 |
apply (simp add: bit_word_cat_iff bit_of_bl_iff nth_append not_less nth_rev_to_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1668 |
apply (meson bit_word.rep_eq less_diff_conv2 nth_rev_to_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1669 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1670 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1671 |
lemma of_bl_append: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1672 |
"(of_bl (xs @ ys) :: 'a::len word) = of_bl xs * 2^(length ys) + of_bl ys" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1673 |
apply transfer |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1674 |
apply (simp add: bl_to_bin_app_cat bin_cat_num) |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1675 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1676 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1677 |
lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1678 |
by (rule word_eqI) (auto simp: test_bit_of_bl nth_append) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1679 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1680 |
lemma of_bl_True [simp]: "(of_bl (True # xs) :: 'a::len word) = 2^length xs + of_bl xs" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1681 |
by (subst of_bl_append [where xs="[True]", simplified]) (simp add: word_1_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1682 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1683 |
lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1684 |
by (cases x) simp_all |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1685 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1686 |
lemma word_split_bl': |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1687 |
"std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1688 |
(a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)))" |
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1689 |
apply (simp add: word_split_def) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1690 |
apply transfer |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1691 |
apply (cases \<open>LENGTH('b) \<le> LENGTH('a)\<close>) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1692 |
apply (auto simp add: drop_bit_take_bit drop_bin2bl bin_to_bl_drop_bit [symmetric, of \<open>LENGTH('a)\<close> \<open>LENGTH('a) - LENGTH('b)\<close> \<open>LENGTH('b)\<close>]) |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1693 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1694 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1695 |
lemma word_split_bl: "std = size c - size b \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1696 |
(a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1697 |
word_split c = (a, b)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1698 |
apply (rule iffI) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1699 |
defer |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1700 |
apply (erule (1) word_split_bl') |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1701 |
apply (case_tac "word_split c") |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1702 |
apply (auto simp add: word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1703 |
apply (frule word_split_bl' [rotated]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1704 |
apply (auto simp add: word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1705 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1706 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1707 |
lemma word_split_bl_eq: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1708 |
"(word_split c :: ('c::len word \<times> 'd::len word)) = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1709 |
(of_bl (take (LENGTH('a::len) - LENGTH('d::len)) (to_bl c)), |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1710 |
of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1711 |
for c :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1712 |
apply (rule word_split_bl [THEN iffD1]) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1713 |
apply (unfold word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1714 |
apply (rule refl conjI)+ |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1715 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1716 |
|
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1717 |
lemma word_rcat_bl: |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1718 |
\<open>word_rcat wl = of_bl (concat (map to_bl wl))\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1719 |
proof - |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1720 |
define ws where \<open>ws = rev wl\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1721 |
moreover have \<open>word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws)))\<close> |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1722 |
apply (simp add: word_rcat_def of_bl_eq rev_concat rev_map comp_def rev_to_bl_eq flip: horner_sum_of_bool_2_concat) |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1723 |
apply transfer |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1724 |
apply simp |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1725 |
done |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1726 |
ultimately show ?thesis |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1727 |
by simp |
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72088
diff
changeset
|
1728 |
qed |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1729 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1730 |
lemma size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1731 |
by (induct wl) (auto simp: word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1732 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1733 |
lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1734 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1735 |
lemma nth_rcat_lem: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1736 |
"n < length (wl::'a word list) * LENGTH('a::len) \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1737 |
rev (concat (map to_bl wl)) ! n = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1738 |
rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1739 |
apply (induct wl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1740 |
apply clarsimp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1741 |
apply (clarsimp simp add : nth_append size_rcat_lem) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1742 |
apply (simp flip: mult_Suc minus_div_mult_eq_mod add: less_Suc_eq_le not_less) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1743 |
apply (metis (no_types, lifting) diff_is_0_eq div_le_mono len_not_eq_0 less_Suc_eq less_mult_imp_div_less nonzero_mult_div_cancel_right not_le nth_Cons_0) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1744 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1745 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1746 |
lemma foldl_eq_foldr: "foldl (+) x xs = foldr (+) (x # xs) 0" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1747 |
for x :: "'a::comm_monoid_add" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1748 |
by (induct xs arbitrary: x) (auto simp: add.assoc) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1749 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1750 |
lemmas word_cat_bl_no_bin [simp] = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1751 |
word_cat_bl [where a="numeral a" and b="numeral b", unfolded to_bl_numeral] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1752 |
for a b (* FIXME: negative numerals, 0 and 1 *) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1753 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1754 |
lemmas word_split_bl_no_bin [simp] = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1755 |
word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1756 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1757 |
lemmas word_rot_defs = word_roti_eq_word_rotr_word_rotl word_rotr_eq word_rotl_eq |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1758 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1759 |
lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1760 |
by (simp add: word_rotl_eq to_bl_use_of_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1761 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1762 |
lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1763 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1764 |
lemmas word_rotl_eqs = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1765 |
blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1766 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1767 |
lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1768 |
by (simp add: word_rotr_eq to_bl_use_of_bl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1769 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1770 |
lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1771 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1772 |
lemmas word_rotr_eqs = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1773 |
brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1774 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1775 |
declare word_rotr_eqs (1) [simp] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1776 |
declare word_rotl_eqs (1) [simp] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1777 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1778 |
lemmas abl_cong = arg_cong [where f = "of_bl"] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1779 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1780 |
locale word_rotate |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1781 |
begin |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1782 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1783 |
lemmas word_rot_defs' = to_bl_rotl to_bl_rotr |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1784 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1785 |
lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1786 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1787 |
lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1788 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1789 |
lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2 |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1790 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1791 |
lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map for v |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1792 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1793 |
lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1794 |
|
71997 | 1795 |
end |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1796 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1797 |
lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take, |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1798 |
simplified word_bl_Rep'] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1799 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1800 |
lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take, |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1801 |
simplified word_bl_Rep'] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1802 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1803 |
lemma bl_word_roti_dt': |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1804 |
"n = nat ((- i) mod int (size (w :: 'a::len word))) \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1805 |
to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1806 |
apply (unfold word_roti_eq_word_rotr_word_rotl) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1807 |
apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1808 |
apply safe |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1809 |
apply (simp add: zmod_zminus1_eq_if) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1810 |
apply safe |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1811 |
apply (simp add: nat_mult_distrib) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1812 |
apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1813 |
[THEN conjunct2, THEN order_less_imp_le]] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1814 |
nat_mod_distrib) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1815 |
apply (simp add: nat_mod_distrib) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1816 |
done |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1817 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1818 |
lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1819 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1820 |
lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1821 |
lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1822 |
lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1823 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1824 |
lemmas word_rotr_dt_no_bin' [simp] = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1825 |
word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1826 |
(* FIXME: negative numerals, 0 and 1 *) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1827 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1828 |
lemmas word_rotl_dt_no_bin' [simp] = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1829 |
word_rotl_dt [where w="numeral w", unfolded to_bl_numeral] for w |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1830 |
(* FIXME: negative numerals, 0 and 1 *) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1831 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1832 |
lemma max_word_bl: "to_bl (max_word::'a::len word) = replicate LENGTH('a) True" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1833 |
by (fact to_bl_n1) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1834 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1835 |
lemma to_bl_mask: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1836 |
"to_bl (mask n :: 'a::len word) = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1837 |
replicate (LENGTH('a) - n) False @ |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1838 |
replicate (min (LENGTH('a)) n) True" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1839 |
by (simp add: mask_bl word_rep_drop min_def) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1840 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1841 |
lemma map_replicate_True: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1842 |
"n = length xs \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1843 |
map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1844 |
by (induct xs arbitrary: n) auto |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1845 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1846 |
lemma map_replicate_False: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1847 |
"n = length xs \<Longrightarrow> map (\<lambda>(x,y). x \<and> y) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1848 |
(zip xs (replicate n False)) = replicate n False" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1849 |
by (induct xs arbitrary: n) auto |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1850 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1851 |
lemma bl_and_mask: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1852 |
fixes w :: "'a::len word" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1853 |
and n :: nat |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1854 |
defines "n' \<equiv> LENGTH('a) - n" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1855 |
shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1856 |
proof - |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1857 |
note [simp] = map_replicate_True map_replicate_False |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1858 |
have "to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n::'a::len word))" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1859 |
by (simp add: bl_word_and) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1860 |
also have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1861 |
by simp |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1862 |
also have "map2 (\<and>) \<dots> (to_bl (mask n::'a::len word)) = |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1863 |
replicate n' False @ drop n' (to_bl w)" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1864 |
unfolding to_bl_mask n'_def by (subst zip_append) auto |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1865 |
finally show ?thesis . |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1866 |
qed |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1867 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1868 |
lemma drop_rev_takefill: |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1869 |
"length xs \<le> n \<Longrightarrow> |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1870 |
drop (n - length xs) (rev (takefill False n (rev xs))) = xs" |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1871 |
by (simp add: takefill_alt rev_take) |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1872 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1873 |
declare bin_to_bl_def [simp] |
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1874 |
|
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72081
diff
changeset
|
1875 |
end |