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