isabelle: src/HOL/Word/Bits.thy@ae643fb4ca30 (annotated)

55210 d1e3b708d74b tuned headers; wenzelm parents: 54854 diff changeset	1	(* Title: HOL/Word/Bits.thy
70192 b4bf82ed0ad5 separate type class for bit comprehension haftmann parents: 70191 diff changeset	2	Author: Brian Huffman, PSU and Gerwin Klein, NICTA
24334 22863f364531 added header kleing parents: 24333 diff changeset	3	*)
22863f364531 added header kleing parents: 24333 diff changeset	4
70191 bdc835d934b7 no need to maintain two separate type classes haftmann parents: 70190 diff changeset	5	section \<open>Syntactic type classes for bit operations\<close>
24333 e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	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 5eb619751b14 misc tuning and modernization; wenzelm parents: 61799 diff changeset	8	imports Main
24333 e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	9	begin
e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	10
70191 bdc835d934b7 no need to maintain two separate type classes haftmann parents: 70190 diff changeset	11	class bit_operations =
71149 a7d1fb0c9e16 proper prefix syntax haftmann parents: 70192 diff changeset	12	fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT")
65363 5eb619751b14 misc tuning and modernization; wenzelm parents: 61799 diff changeset	13	and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
5eb619751b14 misc tuning and modernization; wenzelm parents: 61799 diff changeset	14	and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59)
5eb619751b14 misc tuning and modernization; wenzelm parents: 61799 diff changeset	15	and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)
70191 bdc835d934b7 no need to maintain two separate type classes haftmann parents: 70190 diff changeset	16	and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55)
bdc835d934b7 no need to maintain two separate type classes haftmann parents: 70190 diff changeset	17	and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
bdc835d934b7 no need to maintain two separate type classes haftmann parents: 70190 diff changeset	18	fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100)
bdc835d934b7 no need to maintain two separate type classes haftmann parents: 70190 diff changeset	19	and lsb :: "'a \<Rightarrow> bool"
bdc835d934b7 no need to maintain two separate type classes haftmann parents: 70190 diff changeset	20	and msb :: "'a \<Rightarrow> bool"
bdc835d934b7 no need to maintain two separate type classes haftmann parents: 70190 diff changeset	21	and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
24333 e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	22
61799 4cf66f21b764 isabelle update_cartouches -c -t; wenzelm parents: 58874 diff changeset	23	text \<open>
24333 e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	24	We want the bitwise operations to bind slightly weaker
65363 5eb619751b14 misc tuning and modernization; wenzelm parents: 61799 diff changeset	25	than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to
61799 4cf66f21b764 isabelle update_cartouches -c -t; wenzelm parents: 58874 diff changeset	26	bind slightly stronger than \<open>*\<close>.
4cf66f21b764 isabelle update_cartouches -c -t; wenzelm parents: 58874 diff changeset	27	\<close>
24352 eda777a2785b use class instead of axclass huffman parents: 24334 diff changeset	28
25762 c03e9d04b3e4 splitted class uminus from class minus haftmann parents: 25382 diff changeset	29	end

author	wenzelm
	Mon, 08 Jun 2020 22:31:36 +0200
changeset 71928	ae643fb4ca30
parent 71149	a7d1fb0c9e16
child 71957	3e162c63371a
permissions	-rw-r--r--