author | haftmann |
Thu, 18 Jun 2020 09:07:30 +0000 | |
changeset 71957 | 3e162c63371a |
parent 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 |
71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71149
diff
changeset
|
8 |
imports Main "HOL-Library.Bit_Operations" |
24333 | 9 |
begin |
10 |
||
70191 | 11 |
class bit_operations = |
71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71149
diff
changeset
|
12 |
fixes shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55) |
70191 | 13 |
and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55) |
14 |
fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100) |
|
15 |
and lsb :: "'a \<Rightarrow> bool" |
|
16 |
and msb :: "'a \<Rightarrow> bool" |
|
17 |
and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a" |
|
24333 | 18 |
|
61799 | 19 |
text \<open> |
24333 | 20 |
We want the bitwise operations to bind slightly weaker |
65363 | 21 |
than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to |
61799 | 22 |
bind slightly stronger than \<open>*\<close>. |
23 |
\<close> |
|
24352 | 24 |
|
25762 | 25 |
end |