equal
deleted
inserted
replaced
1 (* |
1 (* Title: HOL/Word/Examples/WordExamples.thy |
2 Authors: Gerwin Klein and Thomas Sewell, NICTA |
2 Authors: Gerwin Klein and Thomas Sewell, NICTA |
3 |
3 |
4 Examples demonstrating and testing various word operations. |
4 Examples demonstrating and testing various word operations. |
5 *) |
5 *) |
6 |
6 |
7 section "Examples of word operations" |
7 section "Examples of word operations" |
8 |
8 |
9 theory WordExamples |
9 theory WordExamples |
10 imports "../Word" "../WordBitwise" |
10 imports "../Word" "../WordBitwise" |
11 begin |
11 begin |
12 |
12 |
13 type_synonym word32 = "32 word" |
13 type_synonym word32 = "32 word" |
14 type_synonym word8 = "8 word" |
14 type_synonym word8 = "8 word" |
15 type_synonym byte = word8 |
15 type_synonym byte = word8 |
26 |
26 |
27 lemma "(127 :: 6 word) = -1" by simp |
27 lemma "(127 :: 6 word) = -1" by simp |
28 |
28 |
29 text "number ring simps" |
29 text "number ring simps" |
30 |
30 |
31 lemma |
31 lemma |
32 "27 + 11 = (38::'a::len word)" |
32 "27 + 11 = (38::'a::len word)" |
33 "27 + 11 = (6::5 word)" |
33 "27 + 11 = (6::5 word)" |
34 "7 * 3 = (21::'a::len word)" |
34 "7 * 3 = (21::'a::len word)" |
35 "11 - 27 = (-16::'a::len word)" |
35 "11 - 27 = (-16::'a::len word)" |
36 "- (- 11) = (11::'a::len word)" |
36 "- (- 11) = (11::'a::len word)" |
38 by simp_all |
38 by simp_all |
39 |
39 |
40 lemma "word_pred 2 = 1" by simp |
40 lemma "word_pred 2 = 1" by simp |
41 |
41 |
42 lemma "word_succ (- 3) = -2" by simp |
42 lemma "word_succ (- 3) = -2" by simp |
43 |
43 |
44 lemma "23 < (27::8 word)" by simp |
44 lemma "23 < (27::8 word)" by simp |
45 lemma "23 \<le> (27::8 word)" by simp |
45 lemma "23 \<le> (27::8 word)" by simp |
46 lemma "\<not> 23 < (27::2 word)" by simp |
46 lemma "\<not> 23 < (27::2 word)" by simp |
47 lemma "0 < (4::3 word)" by simp |
47 lemma "0 < (4::3 word)" by simp |
48 lemma "1 < (4::3 word)" by simp |
48 lemma "1 < (4::3 word)" by simp |
67 lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by simp |
67 lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by simp |
68 lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp |
68 lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp |
69 lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp |
69 lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp |
70 |
70 |
71 text "reducing goals to nat or int and arith:" |
71 text "reducing goals to nat or int and arith:" |
72 lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by unat_arith |
72 lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word" |
73 lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by uint_arith |
73 by unat_arith |
|
74 lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word" |
|
75 by unat_arith |
74 |
76 |
75 text "bool lists" |
77 text "bool lists" |
76 |
78 |
77 lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp |
79 lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp |
78 |
80 |
109 lemma "(0b0010 :: 4 word) !! 1" by simp |
111 lemma "(0b0010 :: 4 word) !! 1" by simp |
110 lemma "\<not> (0b0010 :: 4 word) !! 0" by simp |
112 lemma "\<not> (0b0010 :: 4 word) !! 0" by simp |
111 lemma "\<not> (0b1000 :: 3 word) !! 4" by simp |
113 lemma "\<not> (0b1000 :: 3 word) !! 4" by simp |
112 lemma "\<not> (1 :: 3 word) !! 2" by simp |
114 lemma "\<not> (1 :: 3 word) !! 2" by simp |
113 |
115 |
114 lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)" |
116 lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)" |
115 by (auto simp add: bin_nth_Bit0 bin_nth_Bit1) |
117 by (auto simp add: bin_nth_Bit0 bin_nth_Bit1) |
116 |
118 |
117 lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp |
119 lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp |
118 lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp |
120 lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp |
119 lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp |
121 lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp |
131 lemma "msb (0b1000::4 word)" by simp |
133 lemma "msb (0b1000::4 word)" by simp |
132 lemma "\<not> msb (1::4 word)" by simp |
134 lemma "\<not> msb (1::4 word)" by simp |
133 lemma "\<not> msb (0::4 word)" by simp |
135 lemma "\<not> msb (0::4 word)" by simp |
134 |
136 |
135 lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp |
137 lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp |
136 lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" |
138 lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" |
137 by simp |
139 by simp |
138 |
140 |
139 lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp |
141 lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp |
140 lemma "0b1011 >> 2 = (0b10::8 word)" by simp |
142 lemma "0b1011 >> 2 = (0b10::8 word)" by simp |
141 lemma "0b1011 >>> 2 = (0b10::8 word)" by simp |
143 lemma "0b1011 >>> 2 = (0b10::8 word)" by simp |
169 lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" |
171 lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" |
170 by word_bitwise |
172 by word_bitwise |
171 |
173 |
172 text "more proofs using bitwise expansion" |
174 text "more proofs using bitwise expansion" |
173 |
175 |
174 lemma "((x :: 10 word) AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)" |
176 lemma "(x AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)" |
|
177 for x :: "10 word" |
175 by word_bitwise |
178 by word_bitwise |
176 |
179 |
177 lemma "(((x :: 12 word) AND -8) >> 3) AND 7 = (x AND 56) >> 3" |
180 lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3" |
|
181 for x :: "12 word" |
178 by word_bitwise |
182 by word_bitwise |
179 |
183 |
180 text "some problems require further reasoning after bit expansion" |
184 text "some problems require further reasoning after bit expansion" |
181 |
185 |
182 lemma "x \<le> (42 :: 8 word) \<Longrightarrow> x \<le> 89" |
186 lemma "x \<le> 42 \<Longrightarrow> x \<le> 89" |
|
187 for x :: "8 word" |
183 apply word_bitwise |
188 apply word_bitwise |
184 apply blast |
189 apply blast |
185 done |
190 done |
186 |
191 |
187 lemma "((x :: word32) AND 1023) = 0 \<Longrightarrow> x \<le> -1024" |
192 lemma "(x AND 1023) = 0 \<Longrightarrow> x \<le> -1024" |
|
193 for x :: word32 |
188 apply word_bitwise |
194 apply word_bitwise |
189 apply clarsimp |
195 apply clarsimp |
190 done |
196 done |
191 |
197 |
192 text "operations like shifts by non-numerals will expose some internal list |
198 text "operations like shifts by non-numerals will expose some internal list |
193 representations but may still be easy to solve" |
199 representations but may still be easy to solve" |
194 |
200 |
195 lemma shiftr_overflow: |
201 lemma shiftr_overflow: "32 \<le> a \<Longrightarrow> b >> a = 0" |
196 "32 \<le> a \<Longrightarrow> (b::word32) >> a = 0" |
202 for b :: word32 |
197 apply (word_bitwise) |
203 apply word_bitwise |
198 apply simp |
204 apply simp |
199 done |
205 done |
200 |
206 |
201 |
|
202 end |
207 end |