equal
deleted
inserted
replaced
33 lemma "x = (5 :: 4 word) \<Longrightarrow> 4 * x = 4" by smt |
33 lemma "x = (5 :: 4 word) \<Longrightarrow> 4 * x = 4" by smt |
34 |
34 |
35 |
35 |
36 section \<open>Bit-level logic\<close> |
36 section \<open>Bit-level logic\<close> |
37 |
37 |
|
38 context |
|
39 includes bit_operations_syntax |
|
40 begin |
|
41 |
38 lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by smt |
42 lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by smt |
39 lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by smt |
43 lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by smt |
40 lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by smt |
44 lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by smt |
41 lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by smt |
45 lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by smt |
42 lemma "word_cat (27::4 word) (27::8 word) = (2843::12 word)" by smt |
46 lemma "word_cat (27::4 word) (27::8 word) = (2843::12 word)" by smt |
50 lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by smt |
54 lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by smt |
51 lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by smt |
55 lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by smt |
52 lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by smt |
56 lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by smt |
53 lemma "w < 256 \<Longrightarrow> (w :: 16 word) AND 0x00FF = w" by smt |
57 lemma "w < 256 \<Longrightarrow> (w :: 16 word) AND 0x00FF = w" by smt |
54 |
58 |
|
59 end |
|
60 |
55 |
61 |
56 section \<open>Combined integer-bitvector properties\<close> |
62 section \<open>Combined integer-bitvector properties\<close> |
57 |
63 |
58 lemma |
64 lemma |
59 assumes "bv2int 0 = 0" |
65 assumes "bv2int 0 = 0" |