src/HOL/Word/Size.thy
author kleing
Fri Nov 02 12:35:27 2007 +0100 (2007-11-02)
changeset 25262 d0928156e326
parent 24465 70f0214b3ecc
child 26514 eff55c0a6d34
permissions -rw-r--r--
Added reference to Jeremy Dawson's paper on the word library.
Added header to remaining word/*.thy files so they show up in toc.
     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 
     9 header "The size class"
    10 
    11 theory Size
    12 imports Numeral_Type
    13 begin
    14 
    15 text {*
    16   The aim of this is to allow any type as index type, but to provide a
    17   default instantiation for numeral types. This independence requires
    18   some duplication with the definitions in Numeral\_Type.
    19 *}
    20 axclass len0 < type
    21 
    22 consts
    23   len_of :: "('a :: len0 itself) => nat"
    24 
    25 text {* 
    26   Some theorems are only true on words with length greater 0.
    27 *}
    28 axclass len < len0
    29   len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
    30 
    31 instance num0  :: len0 ..
    32 instance num1 :: len0 ..
    33 instance bit0 :: (len0) len0 ..
    34 instance bit1 :: (len0) len0 ..
    35 
    36 defs (overloaded)
    37   len_num0:  "len_of (x::num0 itself) == 0"
    38   len_num1: "len_of (x::num1 itself) == 1"
    39   len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
    40   len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
    41 
    42 lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
    43 
    44 instance num1 :: len by (intro_classes) simp
    45 instance bit0 :: (len) len by (intro_classes) simp
    46 instance bit1 :: (len0) len by (intro_classes) simp
    47 
    48 -- "Examples:"
    49 lemma "len_of TYPE(17) = 17" by simp
    50 lemma "len_of TYPE(0) = 0" by simp
    51 
    52 -- "not simplified:"
    53 lemma "len_of TYPE('a::len0) = x"
    54   oops
    55    
    56 end
    57