src/HOL/Word/BitSyntax.thy
author haftmann
Wed Jan 02 15:14:02 2008 +0100 (2008-01-02)
changeset 25762 c03e9d04b3e4
parent 25382 72cfe89f7b21
child 26086 3c243098b64a
permissions -rw-r--r--
splitted class uminus from class minus
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
kleing@24333
     9
header {* Syntactic class for bitwise operations *}
kleing@24333
    10
kleing@24333
    11
theory BitSyntax
kleing@24333
    12
imports Main
kleing@24333
    13
begin
kleing@24333
    14
huffman@24352
    15
class bit = type +
huffman@24352
    16
  fixes bitNOT :: "'a \<Rightarrow> 'a"
huffman@24352
    17
    and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
huffman@24352
    18
    and bitOR  :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
huffman@24352
    19
    and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
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
huffman@24352
    27
notation
wenzelm@25382
    28
  bitNOT  ("NOT _" [70] 71) and
wenzelm@25382
    29
  bitAND  (infixr "AND" 64) and
wenzelm@25382
    30
  bitOR   (infixr "OR"  59) and
huffman@24352
    31
  bitXOR  (infixr "XOR" 59)
kleing@24333
    32
kleing@24333
    33
text {*
kleing@24333
    34
  Testing and shifting operations.
kleing@24333
    35
*}
kleing@24333
    36
consts
kleing@24333
    37
  test_bit :: "'a::bit \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100)
kleing@24333
    38
  lsb      :: "'a::bit \<Rightarrow> bool"
kleing@24333
    39
  msb      :: "'a::bit \<Rightarrow> bool"
kleing@24333
    40
  set_bit  :: "'a::bit \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
kleing@24333
    41
  set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a::bit" (binder "BITS " 10)
kleing@24333
    42
  shiftl   :: "'a::bit \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55)
kleing@24333
    43
  shiftr   :: "'a::bit \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
kleing@24333
    44
kleing@24333
    45
kleing@24333
    46
subsection {* Bitwise operations on type @{typ bit} *}
kleing@24333
    47
haftmann@25762
    48
instantiation bit :: bit
haftmann@25762
    49
begin
haftmann@25762
    50
haftmann@25762
    51
definition
haftmann@25762
    52
  NOT_bit_def: "NOT x = (case x of bit.B0 \<Rightarrow> bit.B1 | bit.B1 \<Rightarrow> bit.B0)"
haftmann@25762
    53
haftmann@25762
    54
definition
haftmann@25762
    55
  AND_bit_def: "x AND y = (case x of bit.B0 \<Rightarrow> bit.B0 | bit.B1 \<Rightarrow> y)"
haftmann@25762
    56
haftmann@25762
    57
definition
haftmann@25762
    58
  OR_bit_def: "(x OR y \<Colon> bit) = NOT (NOT x AND NOT y)"
haftmann@25762
    59
haftmann@25762
    60
definition
haftmann@25762
    61
  XOR_bit_def: "(x XOR y \<Colon> bit) = (x AND NOT y) OR (NOT x AND y)"
haftmann@25762
    62
haftmann@25762
    63
instance  ..
haftmann@25762
    64
haftmann@25762
    65
end
kleing@24333
    66
kleing@24333
    67
lemma bit_simps [simp]:
kleing@24333
    68
  "NOT bit.B0 = bit.B1"
kleing@24333
    69
  "NOT bit.B1 = bit.B0"
kleing@24333
    70
  "bit.B0 AND y = bit.B0"
kleing@24333
    71
  "bit.B1 AND y = y"
kleing@24333
    72
  "bit.B0 OR y = y"
kleing@24333
    73
  "bit.B1 OR y = bit.B1"
kleing@24333
    74
  "bit.B0 XOR y = y"
kleing@24333
    75
  "bit.B1 XOR y = NOT y"
kleing@24334
    76
  by (simp_all add: NOT_bit_def AND_bit_def OR_bit_def
kleing@24334
    77
                    XOR_bit_def split: bit.split)
kleing@24333
    78
huffman@24366
    79
lemma bit_extra_simps [simp]: 
huffman@24366
    80
  "x AND bit.B0 = bit.B0"
huffman@24366
    81
  "x AND bit.B1 = x"
huffman@24366
    82
  "x OR bit.B1 = bit.B1"
huffman@24366
    83
  "x OR bit.B0 = x"
huffman@24366
    84
  "x XOR bit.B1 = NOT x"
huffman@24366
    85
  "x XOR bit.B0 = x"
huffman@24366
    86
  by (cases x, auto)+
huffman@24366
    87
huffman@24366
    88
lemma bit_ops_comm: 
huffman@24366
    89
  "(x::bit) AND y = y AND x"
huffman@24366
    90
  "(x::bit) OR y = y OR x"
huffman@24366
    91
  "(x::bit) XOR y = y XOR x"
huffman@24366
    92
  by (cases y, auto)+
huffman@24366
    93
huffman@24366
    94
lemma bit_ops_same [simp]: 
huffman@24366
    95
  "(x::bit) AND x = x"
huffman@24366
    96
  "(x::bit) OR x = x"
huffman@24366
    97
  "(x::bit) XOR x = bit.B0"
huffman@24366
    98
  by (cases x, auto)+
huffman@24366
    99
huffman@24366
   100
lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
huffman@24366
   101
  by (cases x) auto
kleing@24333
   102
kleing@24333
   103
end