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