equal
deleted
inserted
replaced
243 lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0" |
243 lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0" |
244 by (induct n) auto |
244 by (induct n) auto |
245 |
245 |
246 lemma len_bin_to_bl_aux: |
246 lemma len_bin_to_bl_aux: |
247 "length (bin_to_bl_aux n w bs) = n + length bs" |
247 "length (bin_to_bl_aux n w bs) = n + length bs" |
248 by (induct n arbitrary: w bs) auto |
248 by (fact size_bin_to_bl_aux) |
249 |
249 |
250 lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n" |
250 lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n" |
251 by (fact size_bin_to_bl) (* FIXME: duplicate *) |
251 by (fact size_bin_to_bl) (* FIXME: duplicate *) |
252 |
252 |
253 lemma sign_bl_bin': |
253 lemma sign_bl_bin': |