equal
deleted
inserted
replaced
441 by (induct "length xs",simp_all) |
441 by (induct "length xs",simp_all) |
442 hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = |
442 hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = |
443 bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2" |
443 bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2" |
444 by simp |
444 by simp |
445 also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2" |
445 also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2" |
446 by (simp add: ring_distrib) |
446 by (simp add: ring_distribs) |
447 finally show ?thesis . |
447 finally show ?thesis . |
448 qed |
448 qed |
449 qed |
449 qed |
450 qed |
450 qed |
451 thus ?thesis .. |
451 thus ?thesis .. |