equal
deleted
inserted
replaced
11 subsection \<open>Fragments of algebraic bit representations\<close> |
11 subsection \<open>Fragments of algebraic bit representations\<close> |
12 |
12 |
13 context comm_semiring_1 |
13 context comm_semiring_1 |
14 begin |
14 begin |
15 |
15 |
16 primrec radix_value :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'a" |
|
17 where "radix_value f b [] = 0" |
|
18 | "radix_value f b (a # as) = f a + radix_value f b as * b" |
|
19 |
|
20 abbreviation (input) unsigned_of_bits :: "bool list \<Rightarrow> 'a" |
16 abbreviation (input) unsigned_of_bits :: "bool list \<Rightarrow> 'a" |
21 where "unsigned_of_bits \<equiv> radix_value of_bool 2" |
17 where "unsigned_of_bits \<equiv> horner_sum of_bool 2" |
22 |
18 |
23 lemma unsigned_of_bits_replicate_False [simp]: |
19 lemma unsigned_of_bits_replicate_False [simp]: |
24 "unsigned_of_bits (replicate n False) = 0" |
20 "unsigned_of_bits (replicate n False) = 0" |
25 by (induction n) simp_all |
21 by (induction n) simp_all |
26 |
22 |