equal
deleted
inserted
replaced
306 (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))" |
306 (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))" |
307 apply (induct m) |
307 apply (induct m) |
308 apply clarsimp |
308 apply clarsimp |
309 apply clarsimp |
309 apply clarsimp |
310 apply (case_tac w rule: bin_exhaust) |
310 apply (case_tac w rule: bin_exhaust) |
311 apply clarsimp |
311 apply simp |
312 apply (case_tac "n - m") |
|
313 apply arith |
|
314 apply simp |
|
315 apply (rule_tac f = "%n. bl ! n" in arg_cong) |
|
316 apply arith |
|
317 done |
312 done |
318 |
313 |
319 lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)" |
314 lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)" |
320 unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux) |
315 unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux) |
321 |
316 |