src/HOL/Word/BitSyntax.thy

* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.

* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution

header {* Syntactic class for bitwise operations *}

theory BitSyntax
imports Main
begin

axclass bit < type

text {*
  We want the bitwise operations to bind slightly weaker
  than @{text "+"} and @{text "-"}, but @{text "~~"} to 
  bind slightly stronger than @{text "*"}.
*}
consts
  bitNOT  :: "'a::bit \<Rightarrow> 'a"       ("NOT _" [70] 71)
  bitAND  :: "'a::bit \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
  bitOR   :: "'a::bit \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR"  59)
  bitXOR  :: "'a::bit \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)

text {*
  Testing and shifting operations.
*}
consts
  test_bit :: "'a::bit \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100)
  lsb      :: "'a::bit \<Rightarrow> bool"
  msb      :: "'a::bit \<Rightarrow> bool"
  set_bit  :: "'a::bit \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
  set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a::bit" (binder "BITS " 10)
  shiftl   :: "'a::bit \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55)
  shiftr   :: "'a::bit \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)


subsection {* Bitwise operations on type @{typ bit} *}

instance bit :: bit ..

defs (overloaded)
  NOT_bit_def: "NOT x \<equiv> case x of bit.B0 \<Rightarrow> bit.B1 | bit.B1 \<Rightarrow> bit.B0"
  AND_bit_def: "x AND y \<equiv> case x of bit.B0 \<Rightarrow> bit.B0 | bit.B1 \<Rightarrow> y"
  OR_bit_def: "x OR y :: bit \<equiv> NOT (NOT x AND NOT y)"
  XOR_bit_def: "x XOR y :: bit \<equiv> (x AND NOT y) OR (NOT x AND y)"

lemma bit_simps [simp]:
  "NOT bit.B0 = bit.B1"
  "NOT bit.B1 = bit.B0"
  "bit.B0 AND y = bit.B0"
  "bit.B1 AND y = y"
  "bit.B0 OR y = y"
  "bit.B1 OR y = bit.B1"
  "bit.B0 XOR y = y"
  "bit.B1 XOR y = NOT y"
by (simp_all add: NOT_bit_def AND_bit_def OR_bit_def
                  XOR_bit_def split: bit.split)

lemma bit_NOT_NOT: "NOT (NOT (b::bit)) = b"
by (induct b) simp_all

end