author | haftmann |
Sun, 18 Aug 2013 15:29:50 +0200 | |
changeset 53062 | 3af1a6020014 |
parent 41413 | 64cd30d6b0b8 |
child 53438 | 6301ed01e34d |
permissions | -rw-r--r-- |
37655 | 1 |
(* Title: HOL/Word/Bit_Operations.thy |
2 |
Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA |
|
24334 | 3 |
*) |
4 |
||
26559 | 5 |
header {* Syntactic classes for bitwise operations *} |
24333 | 6 |
|
37655 | 7 |
theory Bit_Operations |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
37655
diff
changeset
|
8 |
imports "~~/src/HOL/Library/Bit" |
24333 | 9 |
begin |
10 |
||
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
41413
diff
changeset
|
11 |
subsection {* Abstract syntactic bit operations *} |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
41413
diff
changeset
|
12 |
|
29608 | 13 |
class bit = |
26559 | 14 |
fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT _" [70] 71) |
15 |
and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64) |
|
16 |
and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59) |
|
17 |
and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59) |
|
24333 | 18 |
|
19 |
text {* |
|
20 |
We want the bitwise operations to bind slightly weaker |
|
21 |
than @{text "+"} and @{text "-"}, but @{text "~~"} to |
|
22 |
bind slightly stronger than @{text "*"}. |
|
23 |
*} |
|
24352 | 24 |
|
24333 | 25 |
text {* |
26 |
Testing and shifting operations. |
|
27 |
*} |
|
26559 | 28 |
|
29 |
class bits = bit + |
|
30 |
fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100) |
|
31 |
and lsb :: "'a \<Rightarrow> bool" |
|
32 |
and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a" |
|
33 |
and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a" (binder "BITS " 10) |
|
34 |
and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55) |
|
35 |
and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55) |
|
36 |
||
37 |
class bitss = bits + |
|
38 |
fixes msb :: "'a \<Rightarrow> bool" |
|
24333 | 39 |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
41413
diff
changeset
|
40 |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25762
diff
changeset
|
41 |
subsection {* Bitwise operations on @{typ bit} *} |
24333 | 42 |
|
25762 | 43 |
instantiation bit :: bit |
44 |
begin |
|
45 |
||
26559 | 46 |
primrec bitNOT_bit where |
37655 | 47 |
"NOT 0 = (1::bit)" |
48 |
| "NOT 1 = (0::bit)" |
|
25762 | 49 |
|
26559 | 50 |
primrec bitAND_bit where |
37655 | 51 |
"0 AND y = (0::bit)" |
52 |
| "1 AND y = (y::bit)" |
|
25762 | 53 |
|
26559 | 54 |
primrec bitOR_bit where |
37655 | 55 |
"0 OR y = (y::bit)" |
56 |
| "1 OR y = (1::bit)" |
|
25762 | 57 |
|
26559 | 58 |
primrec bitXOR_bit where |
37655 | 59 |
"0 XOR y = (y::bit)" |
60 |
| "1 XOR y = (NOT y :: bit)" |
|
25762 | 61 |
|
62 |
instance .. |
|
63 |
||
64 |
end |
|
24333 | 65 |
|
26559 | 66 |
lemmas bit_simps = |
67 |
bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps |
|
24333 | 68 |
|
24366 | 69 |
lemma bit_extra_simps [simp]: |
37655 | 70 |
"x AND 0 = (0::bit)" |
71 |
"x AND 1 = (x::bit)" |
|
72 |
"x OR 1 = (1::bit)" |
|
73 |
"x OR 0 = (x::bit)" |
|
74 |
"x XOR 1 = NOT (x::bit)" |
|
75 |
"x XOR 0 = (x::bit)" |
|
24366 | 76 |
by (cases x, auto)+ |
77 |
||
78 |
lemma bit_ops_comm: |
|
79 |
"(x::bit) AND y = y AND x" |
|
80 |
"(x::bit) OR y = y OR x" |
|
81 |
"(x::bit) XOR y = y XOR x" |
|
82 |
by (cases y, auto)+ |
|
83 |
||
84 |
lemma bit_ops_same [simp]: |
|
85 |
"(x::bit) AND x = x" |
|
86 |
"(x::bit) OR x = x" |
|
37655 | 87 |
"(x::bit) XOR x = 0" |
24366 | 88 |
by (cases x, auto)+ |
89 |
||
90 |
lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x" |
|
91 |
by (cases x) auto |
|
24333 | 92 |
|
93 |
end |