equal
deleted
inserted
replaced
2606 consts |
2606 consts |
2607 fast_bv_to_nat_helper :: "[bit list, bin] => bin" |
2607 fast_bv_to_nat_helper :: "[bit list, bin] => bin" |
2608 |
2608 |
2609 primrec |
2609 primrec |
2610 fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] bin = bin" |
2610 fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] bin = bin" |
2611 fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) bin = fast_bv_to_nat_helper bs (bin BIT (bit_case False True b))" |
2611 fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) bin = fast_bv_to_nat_helper bs (bin BIT (bit_case bit.B0 bit.B1 b))" |
2612 |
2612 |
2613 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT False)" |
2613 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B0)" |
2614 by simp |
2614 by simp |
2615 |
2615 |
2616 lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT True)" |
2616 lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B1)" |
2617 by simp |
2617 by simp |
2618 |
2618 |
2619 lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)" |
2619 lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)" |
2620 proof (simp add: bv_to_nat_def) |
2620 proof (simp add: bv_to_nat_def) |
2621 have "\<forall> bin. \<not> (neg (number_of bin :: int)) \<longrightarrow> (foldl (%bn b. 2 * bn + bitval b) (number_of bin) bs) = number_of (fast_bv_to_nat_helper bs bin)" |
2621 have "\<forall> bin. \<not> (neg (number_of bin :: int)) \<longrightarrow> (foldl (%bn b. 2 * bn + bitval b) (number_of bin) bs) = number_of (fast_bv_to_nat_helper bs bin)" |