author | nipkow |
Wed, 20 Dec 2017 14:53:34 +0100 | |
changeset 67229 | 4ecf0ef70efb |
parent 67122 | 85b40f300fab |
permissions | -rw-r--r-- |
67122
85b40f300fab
simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
wenzelm
parents:
66453
diff
changeset
|
1 |
(* Title: HOL/Word/WordExamples.thy |
65363 | 2 |
Authors: Gerwin Klein and Thomas Sewell, NICTA |
24441 | 3 |
|
65363 | 4 |
Examples demonstrating and testing various word operations. |
24441 | 5 |
*) |
6 |
||
58874 | 7 |
section "Examples of word operations" |
25262
d0928156e326
Added reference to Jeremy Dawson's paper on the word library.
kleing
parents:
24465
diff
changeset
|
8 |
|
29629 | 9 |
theory WordExamples |
67122
85b40f300fab
simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
wenzelm
parents:
66453
diff
changeset
|
10 |
imports WordBitwise |
24441 | 11 |
begin |
12 |
||
42463 | 13 |
type_synonym word32 = "32 word" |
14 |
type_synonym word8 = "8 word" |
|
15 |
type_synonym byte = word8 |
|
29640 | 16 |
|
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
17 |
text "modulus" |
24441 | 18 |
|
19 |
lemma "(27 :: 4 word) = -5" by simp |
|
20 |
||
21 |
lemma "(27 :: 4 word) = 11" by simp |
|
22 |
||
23 |
lemma "27 \<noteq> (11 :: 6 word)" by simp |
|
24 |
||
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
25 |
text "signed" |
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
26 |
|
24441 | 27 |
lemma "(127 :: 6 word) = -1" by simp |
28 |
||
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
29 |
text "number ring simps" |
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
30 |
|
65363 | 31 |
lemma |
24465 | 32 |
"27 + 11 = (38::'a::len word)" |
24441 | 33 |
"27 + 11 = (6::5 word)" |
24465 | 34 |
"7 * 3 = (21::'a::len word)" |
35 |
"11 - 27 = (-16::'a::len word)" |
|
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
47567
diff
changeset
|
36 |
"- (- 11) = (11::'a::len word)" |
24465 | 37 |
"-40 + 1 = (-39::'a::len word)" |
24441 | 38 |
by simp_all |
39 |
||
40 |
lemma "word_pred 2 = 1" by simp |
|
41 |
||
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
47567
diff
changeset
|
42 |
lemma "word_succ (- 3) = -2" by simp |
65363 | 43 |
|
24441 | 44 |
lemma "23 < (27::8 word)" by simp |
45 |
lemma "23 \<le> (27::8 word)" by simp |
|
46 |
lemma "\<not> 23 < (27::2 word)" by simp |
|
47 |
lemma "0 < (4::3 word)" by simp |
|
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
48 |
lemma "1 < (4::3 word)" by simp |
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
49 |
lemma "0 < (1::3 word)" by simp |
24441 | 50 |
|
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
51 |
text "ring operations" |
24441 | 52 |
|
53 |
lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by simp |
|
54 |
||
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
55 |
text "casting" |
24441 | 56 |
|
57 |
lemma "uint (234567 :: 10 word) = 71" by simp |
|
58 |
lemma "uint (-234567 :: 10 word) = 953" by simp |
|
59 |
lemma "sint (234567 :: 10 word) = 71" by simp |
|
60 |
lemma "sint (-234567 :: 10 word) = -71" by simp |
|
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
61 |
lemma "uint (1 :: 10 word) = 1" by simp |
24441 | 62 |
|
63 |
lemma "unat (-234567 :: 10 word) = 953" by simp |
|
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
64 |
lemma "unat (1 :: 10 word) = 1" by simp |
24441 | 65 |
|
66 |
lemma "ucast (0b1010 :: 4 word) = (0b10 :: 2 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 |
|
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
69 |
lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp |
24441 | 70 |
|
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
71 |
text "reducing goals to nat or int and arith:" |
65363 | 72 |
lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word" |
73 |
by unat_arith |
|
74 |
lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word" |
|
75 |
by unat_arith |
|
24441 | 76 |
|
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
77 |
text "bool lists" |
24441 | 78 |
|
24465 | 79 |
lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp |
24441 | 80 |
|
81 |
lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp |
|
82 |
||
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
83 |
text "this is not exactly fast, but bearable" |
24441 | 84 |
lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp |
85 |
||
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
86 |
text "this works only for replicate n True" |
24441 | 87 |
lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" |
88 |
by (unfold mask_bl [symmetric]) (simp add: mask_def) |
|
89 |
||
90 |
||
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
91 |
text "bit operations" |
24441 | 92 |
|
93 |
lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by simp |
|
94 |
lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by simp |
|
95 |
lemma "0xF0 XOR 0xFF = (0x0F :: byte)" by simp |
|
96 |
lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp |
|
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
97 |
lemma "0 AND 5 = (0 :: byte)" by simp |
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
98 |
lemma "1 AND 1 = (1 :: byte)" by simp |
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
99 |
lemma "1 AND 0 = (0 :: byte)" by simp |
46064
88ef116e0522
add simp rules for bitwise word operations with 1
huffman
parents:
46015
diff
changeset
|
100 |
lemma "1 AND 5 = (1 :: byte)" by simp |
88ef116e0522
add simp rules for bitwise word operations with 1
huffman
parents:
46015
diff
changeset
|
101 |
lemma "1 OR 6 = (7 :: byte)" by simp |
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
102 |
lemma "1 OR 1 = (1 :: byte)" by simp |
46064
88ef116e0522
add simp rules for bitwise word operations with 1
huffman
parents:
46015
diff
changeset
|
103 |
lemma "1 XOR 7 = (6 :: byte)" by simp |
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
104 |
lemma "1 XOR 1 = (0 :: byte)" by simp |
46064
88ef116e0522
add simp rules for bitwise word operations with 1
huffman
parents:
46015
diff
changeset
|
105 |
lemma "NOT 1 = (254 :: byte)" by simp |
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
106 |
lemma "NOT 0 = (255 :: byte)" apply simp oops |
46064
88ef116e0522
add simp rules for bitwise word operations with 1
huffman
parents:
46015
diff
changeset
|
107 |
(* FIXME: "NOT 0" rewrites to "max_word" instead of "-1" *) |
24441 | 108 |
|
109 |
lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp |
|
110 |
||
111 |
lemma "(0b0010 :: 4 word) !! 1" by simp |
|
112 |
lemma "\<not> (0b0010 :: 4 word) !! 0" by simp |
|
113 |
lemma "\<not> (0b1000 :: 3 word) !! 4" by simp |
|
46172 | 114 |
lemma "\<not> (1 :: 3 word) !! 2" by simp |
24441 | 115 |
|
65363 | 116 |
lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)" |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25262
diff
changeset
|
117 |
by (auto simp add: bin_nth_Bit0 bin_nth_Bit1) |
24441 | 118 |
|
24465 | 119 |
lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp |
120 |
lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp |
|
121 |
lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp |
|
46173
5cc700033194
add simp rules for set_bit and msb applied to 0 and 1
huffman
parents:
46172
diff
changeset
|
122 |
lemma "set_bit 1 3 True = (0b1001::'a::len0 word)" by simp |
5cc700033194
add simp rules for set_bit and msb applied to 0 and 1
huffman
parents:
46172
diff
changeset
|
123 |
lemma "set_bit 1 0 False = (0::'a::len0 word)" by simp |
5cc700033194
add simp rules for set_bit and msb applied to 0 and 1
huffman
parents:
46172
diff
changeset
|
124 |
lemma "set_bit 0 3 True = (0b1000::'a::len0 word)" by simp |
5cc700033194
add simp rules for set_bit and msb applied to 0 and 1
huffman
parents:
46172
diff
changeset
|
125 |
lemma "set_bit 0 3 False = (0::'a::len0 word)" by simp |
24441 | 126 |
|
24465 | 127 |
lemma "lsb (0b0101::'a::len word)" by simp |
128 |
lemma "\<not> lsb (0b1000::'a::len word)" by simp |
|
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
129 |
lemma "lsb (1::'a::len word)" by simp |
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
130 |
lemma "\<not> lsb (0::'a::len word)" by simp |
24441 | 131 |
|
132 |
lemma "\<not> msb (0b0101::4 word)" by simp |
|
133 |
lemma "msb (0b1000::4 word)" by simp |
|
46173
5cc700033194
add simp rules for set_bit and msb applied to 0 and 1
huffman
parents:
46172
diff
changeset
|
134 |
lemma "\<not> msb (1::4 word)" by simp |
5cc700033194
add simp rules for set_bit and msb applied to 0 and 1
huffman
parents:
46172
diff
changeset
|
135 |
lemma "\<not> msb (0::4 word)" by simp |
24441 | 136 |
|
24465 | 137 |
lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp |
65363 | 138 |
lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" |
24441 | 139 |
by simp |
140 |
||
24465 | 141 |
lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp |
24441 | 142 |
lemma "0b1011 >> 2 = (0b10::8 word)" by simp |
143 |
lemma "0b1011 >>> 2 = (0b10::8 word)" by simp |
|
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
144 |
lemma "1 << 2 = (0b100::'a::len0 word)" apply simp? oops |
24441 | 145 |
|
146 |
lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp |
|
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
147 |
lemma "slice 3 (1::6 word) = (0::3 word)" apply simp? oops |
24441 | 148 |
|
149 |
lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp |
|
150 |
lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp |
|
151 |
lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp |
|
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
47567
diff
changeset
|
152 |
lemma "word_roti (- 2) 0b0110 = (0b1001::4 word)" by simp |
46015
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
153 |
lemma "word_rotr 2 0 = (0::4 word)" by simp |
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
154 |
lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops |
713c1f396e33
add several new tests, most of which don't work yet
huffman
parents:
44762
diff
changeset
|
155 |
lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops |
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
47567
diff
changeset
|
156 |
lemma "word_roti (- 2) 1 = (0b0100::4 word)" apply simp? oops |
24441 | 157 |
|
158 |
lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" |
|
159 |
proof - |
|
160 |
have "(x AND 0xff00) OR (x AND 0x00ff) = x AND (0xff00 OR 0x00ff)" |
|
161 |
by (simp only: word_ao_dist2) |
|
162 |
also have "0xff00 OR 0x00ff = (-1::16 word)" |
|
163 |
by simp |
|
164 |
also have "x AND -1 = x" |
|
165 |
by simp |
|
166 |
finally show ?thesis . |
|
167 |
qed |
|
168 |
||
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
169 |
text "alternative proof using bitwise expansion" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
170 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
171 |
lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
172 |
by word_bitwise |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
173 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
174 |
text "more proofs using bitwise expansion" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
175 |
|
65363 | 176 |
lemma "(x AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)" |
177 |
for x :: "10 word" |
|
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
178 |
by word_bitwise |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
179 |
|
65363 | 180 |
lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3" |
181 |
for x :: "12 word" |
|
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
182 |
by word_bitwise |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
183 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
184 |
text "some problems require further reasoning after bit expansion" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
185 |
|
65363 | 186 |
lemma "x \<le> 42 \<Longrightarrow> x \<le> 89" |
187 |
for x :: "8 word" |
|
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
188 |
apply word_bitwise |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
189 |
apply blast |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
190 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
191 |
|
65363 | 192 |
lemma "(x AND 1023) = 0 \<Longrightarrow> x \<le> -1024" |
193 |
for x :: word32 |
|
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
194 |
apply word_bitwise |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
195 |
apply clarsimp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
196 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
197 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
198 |
text "operations like shifts by non-numerals will expose some internal list |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
199 |
representations but may still be easy to solve" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
200 |
|
65363 | 201 |
lemma shiftr_overflow: "32 \<le> a \<Longrightarrow> b >> a = 0" |
202 |
for b :: word32 |
|
203 |
apply word_bitwise |
|
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
204 |
apply simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
205 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
46173
diff
changeset
|
206 |
|
24441 | 207 |
end |