13 |
13 |
14 typedef (open word) 'a word |
14 typedef (open word) 'a word |
15 = "{(0::int) ..< 2^CARD('a)}" by auto |
15 = "{(0::int) ..< 2^CARD('a)}" by auto |
16 |
16 |
17 instance word :: (type) number .. |
17 instance word :: (type) number .. |
18 instance word :: (type) minus .. |
|
19 instance word :: (type) plus .. |
|
20 instance word :: (type) one .. |
|
21 instance word :: (type) zero .. |
|
22 instance word :: (type) times .. |
|
23 instance word :: (type) power .. |
|
24 instance word :: (type) size .. |
18 instance word :: (type) size .. |
25 instance word :: (type) inverse .. |
19 instance word :: (type) inverse .. |
26 instance word :: (type) bit .. |
20 instance word :: (type) bit .. |
27 |
21 |
|
22 subsection {* Basic arithmetic *} |
|
23 |
|
24 definition |
|
25 Abs_word' :: "int \<Rightarrow> 'a word" |
|
26 where "Abs_word' x = Abs_word (x mod 2^CARD('a))" |
|
27 |
|
28 lemma Rep_word_mod: "Rep_word (x::'a word) mod 2^CARD('a) = Rep_word x" |
|
29 by (simp only: mod_pos_pos_trivial Rep_word [simplified]) |
|
30 |
|
31 lemma Rep_word_inverse': "Abs_word' (Rep_word x) = x" |
|
32 unfolding Abs_word'_def Rep_word_mod |
|
33 by (rule Rep_word_inverse) |
|
34 |
|
35 lemma Abs_word'_inverse: "Rep_word (Abs_word' z::'a word) = z mod 2^CARD('a)" |
|
36 unfolding Abs_word'_def |
|
37 by (simp add: Abs_word_inverse) |
|
38 |
|
39 lemmas Rep_word_simps = |
|
40 Rep_word_inject [symmetric] |
|
41 Rep_word_mod |
|
42 Rep_word_inverse' |
|
43 Abs_word'_inverse |
|
44 |
|
45 instance word :: (type) "{zero,one,plus,minus,times,power}" |
|
46 word_zero_def: "0 \<equiv> Abs_word' 0" |
|
47 word_one_def: "1 \<equiv> Abs_word' 1" |
|
48 word_add_def: "x + y \<equiv> Abs_word' (Rep_word x + Rep_word y)" |
|
49 word_mult_def: "x * y \<equiv> Abs_word' (Rep_word x * Rep_word y)" |
|
50 word_diff_def: "x - y \<equiv> Abs_word' (Rep_word x - Rep_word y)" |
|
51 word_minus_def: "- x \<equiv> Abs_word' (- Rep_word x)" |
|
52 word_power_def: "x ^ n \<equiv> Abs_word' (Rep_word x ^ n)" |
|
53 .. |
|
54 |
|
55 lemmas word_arith_defs = |
|
56 word_zero_def |
|
57 word_one_def |
|
58 word_add_def |
|
59 word_mult_def |
|
60 word_diff_def |
|
61 word_minus_def |
|
62 word_power_def |
|
63 |
|
64 instance word :: (type) "{comm_ring,comm_monoid_mult,recpower}" |
|
65 apply (intro_classes, unfold word_arith_defs) |
|
66 apply (simp_all add: Rep_word_simps zmod_simps ring_simps |
|
67 mod_pos_pos_trivial) |
|
68 done |
|
69 |
|
70 instance word :: (finite) comm_ring_1 |
|
71 apply (intro_classes, unfold word_arith_defs) |
|
72 apply (simp_all add: Rep_word_simps zmod_simps ring_simps |
|
73 mod_pos_pos_trivial one_less_power) |
|
74 done |
|
75 |
|
76 lemma word_of_nat: "of_nat n = Abs_word' (int n)" |
|
77 apply (induct n) |
|
78 apply (simp add: word_zero_def) |
|
79 apply (simp add: Rep_word_simps word_arith_defs zmod_simps) |
|
80 done |
|
81 |
|
82 lemma word_of_int: "of_int z = Abs_word' z" |
|
83 apply (cases z rule: int_diff_cases) |
|
84 apply (simp add: Rep_word_simps word_diff_def word_of_nat zmod_simps) |
|
85 done |
28 |
86 |
29 subsection "Type conversions and casting" |
87 subsection "Type conversions and casting" |
30 |
88 |
31 constdefs |
89 constdefs |
32 -- {* representation of words using unsigned or signed bins, |
90 -- {* representation of words using unsigned or signed bins, |
68 "case x of of_int y => b" == "word_int_case (%y. b) x" |
126 "case x of of_int y => b" == "word_int_case (%y. b) x" |
69 |
127 |
70 |
128 |
71 subsection "Arithmetic operations" |
129 subsection "Arithmetic operations" |
72 |
130 |
73 defs (overloaded) |
131 lemma Abs_word'_eq: "Abs_word' = word_of_int" |
74 word_1_wi: "(1 :: ('a) word) == word_of_int 1" |
132 unfolding expand_fun_eq Abs_word'_def word_of_int_def |
75 word_0_wi: "(0 :: ('a) word) == word_of_int 0" |
133 by (simp add: bintrunc_mod2p) |
|
134 |
|
135 lemma word_1_wi: "(1 :: ('a) word) == word_of_int 1" |
|
136 by (simp only: word_arith_defs Abs_word'_eq) |
|
137 |
|
138 lemma word_0_wi: "(0 :: ('a) word) == word_of_int 0" |
|
139 by (simp only: word_arith_defs Abs_word'_eq) |
76 |
140 |
77 constdefs |
141 constdefs |
78 word_succ :: "'a word => 'a word" |
142 word_succ :: "'a word => 'a word" |
79 "word_succ a == word_of_int (Numeral.succ (uint a))" |
143 "word_succ a == word_of_int (Numeral.succ (uint a))" |
80 |
144 |
85 word_power :: "'a word => nat => 'a word" |
149 word_power :: "'a word => nat => 'a word" |
86 primrec |
150 primrec |
87 "word_power a 0 = 1" |
151 "word_power a 0 = 1" |
88 "word_power a (Suc n) = a * word_power a n" |
152 "word_power a (Suc n) = a * word_power a n" |
89 |
153 |
90 defs (overloaded) |
154 lemma |
91 word_pow: "power == word_power" |
155 word_pow: "power == word_power" |
|
156 apply (rule eq_reflection, rule ext, rule ext) |
|
157 apply (rename_tac n, induct_tac n, simp_all add: power_Suc) |
|
158 done |
|
159 |
|
160 lemma |
92 word_add_def: "a + b == word_of_int (uint a + uint b)" |
161 word_add_def: "a + b == word_of_int (uint a + uint b)" |
|
162 and |
93 word_sub_wi: "a - b == word_of_int (uint a - uint b)" |
163 word_sub_wi: "a - b == word_of_int (uint a - uint b)" |
|
164 and |
94 word_minus_def: "- a == word_of_int (- uint a)" |
165 word_minus_def: "- a == word_of_int (- uint a)" |
|
166 and |
95 word_mult_def: "a * b == word_of_int (uint a * uint b)" |
167 word_mult_def: "a * b == word_of_int (uint a * uint b)" |
96 |
168 by (simp_all only: word_arith_defs Abs_word'_eq uint_def) |
97 |
169 |
98 subsection "Bit-wise operations" |
170 subsection "Bit-wise operations" |
99 |
171 |
100 defs (overloaded) |
172 defs (overloaded) |
101 word_and_def: |
173 word_and_def: |