author | nipkow |
Wed, 06 Aug 2008 13:57:25 +0200 | |
changeset 27760 | 3aa86edac080 |
parent 26559 | 799983936aad |
child 29608 | 564ea783ace8 |
permissions | -rw-r--r-- |
24334 | 1 |
(* |
2 |
ID: $Id$ |
|
3 |
Author: Brian Huffman, PSU and Gerwin Klein, NICTA |
|
4 |
||
5 |
Syntactic class for bitwise operations. |
|
6 |
*) |
|
7 |
||
8 |
||
26559 | 9 |
header {* Syntactic classes for bitwise operations *} |
24333 | 10 |
|
11 |
theory BitSyntax |
|
26559 | 12 |
imports BinGeneral |
24333 | 13 |
begin |
14 |
||
24352 | 15 |
class bit = type + |
26559 | 16 |
fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT _" [70] 71) |
17 |
and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64) |
|
18 |
and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59) |
|
19 |
and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59) |
|
24333 | 20 |
|
21 |
text {* |
|
22 |
We want the bitwise operations to bind slightly weaker |
|
23 |
than @{text "+"} and @{text "-"}, but @{text "~~"} to |
|
24 |
bind slightly stronger than @{text "*"}. |
|
25 |
*} |
|
24352 | 26 |
|
24333 | 27 |
text {* |
28 |
Testing and shifting operations. |
|
29 |
*} |
|
26559 | 30 |
|
31 |
class bits = bit + |
|
32 |
fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100) |
|
33 |
and lsb :: "'a \<Rightarrow> bool" |
|
34 |
and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a" |
|
35 |
and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a" (binder "BITS " 10) |
|
36 |
and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55) |
|
37 |
and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55) |
|
38 |
||
39 |
class bitss = bits + |
|
40 |
fixes msb :: "'a \<Rightarrow> bool" |
|
24333 | 41 |
|
42 |
||
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25762
diff
changeset
|
43 |
subsection {* Bitwise operations on @{typ bit} *} |
24333 | 44 |
|
25762 | 45 |
instantiation bit :: bit |
46 |
begin |
|
47 |
||
26559 | 48 |
primrec bitNOT_bit where |
49 |
"NOT bit.B0 = bit.B1" |
|
50 |
| "NOT bit.B1 = bit.B0" |
|
25762 | 51 |
|
26559 | 52 |
primrec bitAND_bit where |
53 |
"bit.B0 AND y = bit.B0" |
|
54 |
| "bit.B1 AND y = y" |
|
25762 | 55 |
|
26559 | 56 |
primrec bitOR_bit where |
57 |
"bit.B0 OR y = y" |
|
58 |
| "bit.B1 OR y = bit.B1" |
|
25762 | 59 |
|
26559 | 60 |
primrec bitXOR_bit where |
61 |
"bit.B0 XOR y = y" |
|
62 |
| "bit.B1 XOR y = NOT y" |
|
25762 | 63 |
|
64 |
instance .. |
|
65 |
||
66 |
end |
|
24333 | 67 |
|
26559 | 68 |
lemmas bit_simps = |
69 |
bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps |
|
24333 | 70 |
|
24366 | 71 |
lemma bit_extra_simps [simp]: |
72 |
"x AND bit.B0 = bit.B0" |
|
73 |
"x AND bit.B1 = x" |
|
74 |
"x OR bit.B1 = bit.B1" |
|
75 |
"x OR bit.B0 = x" |
|
76 |
"x XOR bit.B1 = NOT x" |
|
77 |
"x XOR bit.B0 = x" |
|
78 |
by (cases x, auto)+ |
|
79 |
||
80 |
lemma bit_ops_comm: |
|
81 |
"(x::bit) AND y = y AND x" |
|
82 |
"(x::bit) OR y = y OR x" |
|
83 |
"(x::bit) XOR y = y XOR x" |
|
84 |
by (cases y, auto)+ |
|
85 |
||
86 |
lemma bit_ops_same [simp]: |
|
87 |
"(x::bit) AND x = x" |
|
88 |
"(x::bit) OR x = x" |
|
89 |
"(x::bit) XOR x = bit.B0" |
|
90 |
by (cases x, auto)+ |
|
91 |
||
92 |
lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x" |
|
93 |
by (cases x) auto |
|
24333 | 94 |
|
95 |
end |