equal
deleted
inserted
replaced
828 done |
828 done |
829 |
829 |
830 lemma ucast_up_app': |
830 lemma ucast_up_app': |
831 "uc = ucast ==> source_size uc + n = target_size uc ==> |
831 "uc = ucast ==> source_size uc + n = target_size uc ==> |
832 to_bl (uc w) = replicate n False @ (to_bl w)" |
832 to_bl (uc w) = replicate n False @ (to_bl w)" |
833 apply (auto simp add : source_size target_size to_bl_ucast) |
833 by (auto simp add : source_size target_size to_bl_ucast) |
834 apply (rule_tac f = "%n. replicate n False" in arg_cong) |
|
835 apply simp |
|
836 done |
|
837 |
834 |
838 lemma ucast_down_drop': |
835 lemma ucast_down_drop': |
839 "uc = ucast ==> source_size uc = target_size uc + n ==> |
836 "uc = ucast ==> source_size uc = target_size uc + n ==> |
840 to_bl (uc w) = drop n (to_bl w)" |
837 to_bl (uc w) = drop n (to_bl w)" |
841 by (auto simp add : source_size target_size to_bl_ucast) |
838 by (auto simp add : source_size target_size to_bl_ucast) |