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