| changeset 28562 | 4e74209f113e |
| parent 28524 | 644b62cf678f |
| child 28643 | caa1137d25dc |
| 28561:056255ade52a | 28562:4e74209f113e |
|---|---|
28 definition |
28 definition |
29 -- {* representation of words using unsigned or signed bins, |
29 -- {* representation of words using unsigned or signed bins, |
30 only difference in these is the type class *} |
30 only difference in these is the type class *} |
31 word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" |
31 word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" |
32 where |
32 where |
33 [code func del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" |
33 [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" |
34 |
34 |
35 code_datatype word_of_int |
35 code_datatype word_of_int |
36 |
36 |
37 |
37 |
38 subsection "Type conversions and casting" |
38 subsection "Type conversions and casting" |
94 "case x of of_int y => b" == "word_int_case (%y. b) x" |
94 "case x of of_int y => b" == "word_int_case (%y. b) x" |
95 |
95 |
96 |
96 |
97 subsection "Arithmetic operations" |
97 subsection "Arithmetic operations" |
98 |
98 |
99 declare uint_def [code func del] |
99 declare uint_def [code del] |
100 |
100 |
101 lemma [code func]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w" |
101 lemma [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w" |
102 by (auto simp add: uint_def word_of_int_def intro!: Abs_word_inverse) |
102 by (auto simp add: uint_def word_of_int_def intro!: Abs_word_inverse) |
103 (insert range_bintrunc, auto) |
103 (insert range_bintrunc, auto) |
104 |
104 |
105 instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}" |
105 instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}" |
106 begin |
106 begin |