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