18 Nil: "bl_to_bin_aux [] w = w" |
18 Nil: "bl_to_bin_aux [] w = w" |
19 | Cons: "bl_to_bin_aux (b # bs) w = |
19 | Cons: "bl_to_bin_aux (b # bs) w = |
20 bl_to_bin_aux bs (w BIT (if b then 1 else 0))" |
20 bl_to_bin_aux bs (w BIT (if b then 1 else 0))" |
21 |
21 |
22 definition bl_to_bin :: "bool list \<Rightarrow> int" where |
22 definition bl_to_bin :: "bool list \<Rightarrow> int" where |
23 bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls" |
23 bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0" |
24 |
|
25 lemma [code]: |
|
26 "bl_to_bin bs = bl_to_bin_aux bs 0" |
|
27 by (simp add: bl_to_bin_def Pls_def) |
|
28 |
24 |
29 primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where |
25 primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where |
30 Z: "bin_to_bl_aux 0 w bl = bl" |
26 Z: "bin_to_bl_aux 0 w bl = bl" |
31 | Suc: "bin_to_bl_aux (Suc n) w bl = |
27 | Suc: "bin_to_bl_aux (Suc n) w bl = |
32 bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)" |
28 bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)" |
86 if y then rbl_add ws x else ws)" |
82 if y then rbl_add ws x else ws)" |
87 |
83 |
88 lemma butlast_power: |
84 lemma butlast_power: |
89 "(butlast ^^ n) bl = take (length bl - n) bl" |
85 "(butlast ^^ n) bl = take (length bl - n) bl" |
90 by (induct n) (auto simp: butlast_take) |
86 by (induct n) (auto simp: butlast_take) |
|
87 |
|
88 lemma bin_to_bl_aux_zero_minus_simp [simp]: |
|
89 "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = |
|
90 bin_to_bl_aux (n - 1) 0 (False # bl)" |
|
91 by (cases n) auto |
91 |
92 |
92 lemma bin_to_bl_aux_Pls_minus_simp [simp]: |
93 lemma bin_to_bl_aux_Pls_minus_simp [simp]: |
93 "0 < n ==> bin_to_bl_aux n Int.Pls bl = |
94 "0 < n ==> bin_to_bl_aux n Int.Pls bl = |
94 bin_to_bl_aux (n - 1) Int.Pls (False # bl)" |
95 bin_to_bl_aux (n - 1) Int.Pls (False # bl)" |
95 by (cases n) auto |
96 by (cases n) auto |
176 apply (rule bl_bin_bl) |
177 apply (rule bl_bin_bl) |
177 apply simp |
178 apply simp |
178 done |
179 done |
179 |
180 |
180 lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl" |
181 lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl" |
181 unfolding bl_to_bin_def by (auto simp: BIT_simps) |
|
182 |
|
183 lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = Int.Pls" |
|
184 unfolding bl_to_bin_def by auto |
182 unfolding bl_to_bin_def by auto |
|
183 |
|
184 lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0" |
|
185 unfolding bl_to_bin_def by auto |
|
186 |
|
187 lemma bin_to_bl_zero_aux: |
|
188 "bin_to_bl_aux n 0 bl = replicate n False @ bl" |
|
189 by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) |
185 |
190 |
186 lemma bin_to_bl_Pls_aux: |
191 lemma bin_to_bl_Pls_aux: |
187 "bin_to_bl_aux n Int.Pls bl = replicate n False @ bl" |
192 "bin_to_bl_aux n Int.Pls bl = replicate n False @ bl" |
188 by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) |
193 by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) |
189 |
194 |
197 lemma bin_to_bl_Min: "bin_to_bl n Int.Min = replicate n True" |
202 lemma bin_to_bl_Min: "bin_to_bl n Int.Min = replicate n True" |
198 unfolding bin_to_bl_def by (simp add : bin_to_bl_Min_aux) |
203 unfolding bin_to_bl_def by (simp add : bin_to_bl_Min_aux) |
199 |
204 |
200 lemma bl_to_bin_rep_F: |
205 lemma bl_to_bin_rep_F: |
201 "bl_to_bin (replicate n False @ bl) = bl_to_bin bl" |
206 "bl_to_bin (replicate n False @ bl) = bl_to_bin bl" |
202 apply (simp add: bin_to_bl_Pls_aux [symmetric] bin_bl_bin') |
207 apply (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') |
203 apply (simp add: bl_to_bin_def) |
208 apply (simp add: bl_to_bin_def) |
204 done |
209 done |
205 |
210 |
206 lemma bin_to_bl_trunc [simp]: |
211 lemma bin_to_bl_trunc [simp]: |
207 "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w" |
212 "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w" |
212 replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl" |
217 replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl" |
213 apply (induct n arbitrary: m bin bl) |
218 apply (induct n arbitrary: m bin bl) |
214 apply clarsimp |
219 apply clarsimp |
215 apply clarsimp |
220 apply clarsimp |
216 apply (case_tac "m") |
221 apply (case_tac "m") |
217 apply (clarsimp simp: bin_to_bl_Pls_aux) |
222 apply (clarsimp simp: bin_to_bl_zero_aux) |
218 apply (erule thin_rl) |
223 apply (erule thin_rl) |
219 apply (induct_tac n) |
224 apply (induct_tac n) |
220 apply auto |
225 apply auto |
221 done |
226 done |
222 |
227 |
223 lemma bin_to_bl_bintr: |
228 lemma bin_to_bl_bintr: |
224 "bin_to_bl n (bintrunc m bin) = |
229 "bin_to_bl n (bintrunc m bin) = |
225 replicate (n - m) False @ bin_to_bl (min n m) bin" |
230 replicate (n - m) False @ bin_to_bl (min n m) bin" |
226 unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr) |
231 unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr) |
227 |
232 |
228 lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.Pls" |
233 lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0" |
229 by (induct n) auto |
234 by (induct n) auto |
230 |
235 |
231 lemma len_bin_to_bl_aux: |
236 lemma len_bin_to_bl_aux: |
232 "length (bin_to_bl_aux n w bs) = n + length bs" |
237 "length (bin_to_bl_aux n w bs) = n + length bs" |
233 by (induct n arbitrary: w bs) auto |
238 by (induct n arbitrary: w bs) auto |
237 |
242 |
238 lemma sign_bl_bin': |
243 lemma sign_bl_bin': |
239 "bin_sign (bl_to_bin_aux bs w) = bin_sign w" |
244 "bin_sign (bl_to_bin_aux bs w) = bin_sign w" |
240 by (induct bs arbitrary: w) auto |
245 by (induct bs arbitrary: w) auto |
241 |
246 |
242 lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = Int.Pls" |
247 lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0" |
243 unfolding bl_to_bin_def by (simp add : sign_bl_bin') |
248 unfolding bl_to_bin_def by (simp add : sign_bl_bin') |
244 |
249 |
245 lemma bl_sbin_sign_aux: |
250 lemma bl_sbin_sign_aux: |
246 "hd (bin_to_bl_aux (Suc n) w bs) = |
251 "hd (bin_to_bl_aux (Suc n) w bs) = |
247 (bin_sign (sbintrunc n w) = Int.Min)" |
252 (bin_sign (sbintrunc n w) = -1)" |
248 apply (induct n arbitrary: w bs) |
253 apply (induct n arbitrary: w bs) |
249 apply clarsimp |
254 apply clarsimp |
250 apply (cases w rule: bin_exhaust) |
255 apply (cases w rule: bin_exhaust) |
251 apply (simp split add : bit.split) |
256 apply (simp split add : bit.split) |
252 apply clarsimp |
257 apply clarsimp |
253 done |
258 done |
254 |
259 |
255 lemma bl_sbin_sign: |
260 lemma bl_sbin_sign: |
256 "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Int.Min)" |
261 "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)" |
257 unfolding bin_to_bl_def by (rule bl_sbin_sign_aux) |
262 unfolding bin_to_bl_def by (rule bl_sbin_sign_aux) |
258 |
263 |
259 lemma bin_nth_of_bl_aux: |
264 lemma bin_nth_of_bl_aux: |
260 "bin_nth (bl_to_bin_aux bl w) n = |
265 "bin_nth (bl_to_bin_aux bl w) n = |
261 (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))" |
266 (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))" |
652 bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)" |
657 bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)" |
653 by (induct nw) auto |
658 by (induct nw) auto |
654 |
659 |
655 lemma bl_to_bin_aux_alt: |
660 lemma bl_to_bin_aux_alt: |
656 "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)" |
661 "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)" |
657 using bl_to_bin_aux_cat [where nv = "0" and v = "Int.Pls"] |
662 using bl_to_bin_aux_cat [where nv = "0" and v = "0"] |
658 unfolding bl_to_bin_def [symmetric] by simp |
663 unfolding bl_to_bin_def [symmetric] by simp |
659 |
664 |
660 lemma bin_to_bl_cat: |
665 lemma bin_to_bl_cat: |
661 "bin_to_bl (nv + nw) (bin_cat v nw w) = |
666 "bin_to_bl (nv + nw) (bin_cat v nw w) = |
662 bin_to_bl_aux nv v (bin_to_bl nw w)" |
667 bin_to_bl_aux nv v (bin_to_bl nw w)" |
683 |
688 |
684 lemma mask_lem: "(bl_to_bin (True # replicate n False)) = |
689 lemma mask_lem: "(bl_to_bin (True # replicate n False)) = |
685 Int.succ (bl_to_bin (replicate n True))" |
690 Int.succ (bl_to_bin (replicate n True))" |
686 apply (unfold bl_to_bin_def) |
691 apply (unfold bl_to_bin_def) |
687 apply (induct n) |
692 apply (induct n) |
688 apply (simp add: BIT_simps) |
693 apply (simp add: Int.succ_def) |
689 apply (simp only: Suc_eq_plus1 replicate_add |
694 apply (simp only: Suc_eq_plus1 replicate_add |
690 append_Cons [symmetric] bl_to_bin_aux_append) |
695 append_Cons [symmetric] bl_to_bin_aux_append) |
691 apply (simp add: BIT_simps) |
696 apply (simp add: BIT_simps) |
692 done |
697 done |
693 |
698 |