17 morphisms uint Abs_word by auto |
17 morphisms uint Abs_word by auto |
18 |
18 |
19 definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where |
19 definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where |
20 -- {* representation of words using unsigned or signed bins, |
20 -- {* representation of words using unsigned or signed bins, |
21 only difference in these is the type class *} |
21 only difference in these is the type class *} |
22 [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" |
22 "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" |
23 |
23 |
24 lemma uint_word_of_int [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = w mod 2 ^ len_of TYPE('a)" |
24 lemma uint_word_of_int [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = w mod 2 ^ len_of TYPE('a)" |
25 by (auto simp add: word_of_int_def bintrunc_mod2p intro: Abs_word_inverse) |
25 by (auto simp add: word_of_int_def bintrunc_mod2p intro: Abs_word_inverse) |
26 |
26 |
27 code_datatype word_of_int |
27 code_datatype word_of_int |
|
28 |
|
29 notation fcomp (infixl "o>" 60) |
|
30 notation scomp (infixl "o\<rightarrow>" 60) |
|
31 |
|
32 instantiation word :: ("{len0, typerep}") random |
|
33 begin |
|
34 |
|
35 definition |
|
36 "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) o\<rightarrow> (\<lambda>k. Pair ( |
|
37 let j = word_of_int (Code_Numeral.int_of k) :: 'a word |
|
38 in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))" |
|
39 |
|
40 instance .. |
|
41 |
|
42 end |
|
43 |
|
44 no_notation fcomp (infixl "o>" 60) |
|
45 no_notation scomp (infixl "o\<rightarrow>" 60) |
28 |
46 |
29 |
47 |
30 subsection {* Type conversions and casting *} |
48 subsection {* Type conversions and casting *} |
31 |
49 |
32 definition sint :: "'a :: len word => int" where |
50 definition sint :: "'a :: len word => int" where |