src/HOL/Word/Size.thy
author huffman
Tue Aug 28 20:13:47 2007 +0200 (2007-08-28)
changeset 24465 70f0214b3ecc
child 25262 d0928156e326
permissions -rw-r--r--
revert to Word library version from 2007/08/20
     1 (* 
     2     ID:         $Id$
     3     Author:     John Matthews, Galois Connections, Inc., copyright 2006
     4 
     5     A typeclass for parameterizing types by size.
     6     Used primarily to parameterize machine word sizes. 
     7 *)
     8 theory Size
     9 imports Numeral_Type
    10 begin
    11 
    12 text {*
    13   The aim of this is to allow any type as index type, but to provide a
    14   default instantiation for numeral types. This independence requires
    15   some duplication with the definitions in Numeral\_Type.
    16 *}
    17 axclass len0 < type
    18 
    19 consts
    20   len_of :: "('a :: len0 itself) => nat"
    21 
    22 text {* 
    23   Some theorems are only true on words with length greater 0.
    24 *}
    25 axclass len < len0
    26   len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
    27 
    28 instance num0  :: len0 ..
    29 instance num1 :: len0 ..
    30 instance bit0 :: (len0) len0 ..
    31 instance bit1 :: (len0) len0 ..
    32 
    33 defs (overloaded)
    34   len_num0:  "len_of (x::num0 itself) == 0"
    35   len_num1: "len_of (x::num1 itself) == 1"
    36   len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
    37   len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
    38 
    39 lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
    40 
    41 instance num1 :: len by (intro_classes) simp
    42 instance bit0 :: (len) len by (intro_classes) simp
    43 instance bit1 :: (len0) len by (intro_classes) simp
    44 
    45 -- "Examples:"
    46 lemma "len_of TYPE(17) = 17" by simp
    47 lemma "len_of TYPE(0) = 0" by simp
    48 
    49 -- "not simplified:"
    50 lemma "len_of TYPE('a::len0) = x"
    51   oops
    52    
    53 end
    54