author | nipkow |
Tue, 05 Nov 2019 14:57:41 +0100 | |
changeset 71033 | c1b63124245c |
parent 70192 | b4bf82ed0ad5 |
child 71149 | a7d1fb0c9e16 |
permissions | -rw-r--r-- |
55210 | 1 |
(* Title: HOL/Word/Bits.thy |
70192 | 2 |
Author: Brian Huffman, PSU and Gerwin Klein, NICTA |
24334 | 3 |
*) |
4 |
||
70191 | 5 |
section \<open>Syntactic type classes for bit operations\<close> |
24333 | 6 |
|
54854
3324a0078636
prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.
haftmann
parents:
54847
diff
changeset
|
7 |
theory Bits |
65363 | 8 |
imports Main |
24333 | 9 |
begin |
10 |
||
70191 | 11 |
class bit_operations = |
65363 | 12 |
fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT _" [70] 71) |
13 |
and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64) |
|
14 |
and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59) |
|
15 |
and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59) |
|
70191 | 16 |
and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55) |
17 |
and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55) |
|
18 |
fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100) |
|
19 |
and lsb :: "'a \<Rightarrow> bool" |
|
20 |
and msb :: "'a \<Rightarrow> bool" |
|
21 |
and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a" |
|
24333 | 22 |
|
61799 | 23 |
text \<open> |
24333 | 24 |
We want the bitwise operations to bind slightly weaker |
65363 | 25 |
than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to |
61799 | 26 |
bind slightly stronger than \<open>*\<close>. |
27 |
\<close> |
|
24352 | 28 |
|
25762 | 29 |
end |