equal
deleted
inserted
replaced
479 apply safe |
479 apply safe |
480 apply simp |
480 apply simp |
481 apply (case_tac v rule: bin_exhaust) |
481 apply (case_tac v rule: bin_exhaust) |
482 apply (case_tac w rule: bin_exhaust) |
482 apply (case_tac w rule: bin_exhaust) |
483 apply clarsimp |
483 apply clarsimp |
484 apply (case_tac b) |
|
485 apply (case_tac ba, safe, simp_all)+ |
|
486 done |
484 done |
487 |
485 |
488 lemma bl_not_aux_bin [rule_format] : |
486 lemma bl_not_aux_bin [rule_format] : |
489 "ALL w cs. map Not (bin_to_bl_aux n w cs) = |
487 "ALL w cs. map Not (bin_to_bl_aux n w cs) = |
490 bin_to_bl_aux n (NOT w) (map Not cs)" |
488 bin_to_bl_aux n (NOT w) (map Not cs)" |
491 apply (induct n) |
489 apply (induct n) |
492 apply clarsimp |
490 apply clarsimp |
493 apply clarsimp |
491 apply clarsimp |
494 apply (case_tac w rule: bin_exhaust) |
|
495 apply (case_tac b) |
|
496 apply auto |
|
497 done |
492 done |
498 |
493 |
499 lemmas bl_not_bin = bl_not_aux_bin |
494 lemmas bl_not_bin = bl_not_aux_bin |
500 [where cs = "[]", unfolded bin_to_bl_def [symmetric] map.simps] |
495 [where cs = "[]", unfolded bin_to_bl_def [symmetric] map.simps] |
501 |
496 |