src/HOL/Word/Size.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 26560 d2fc9a18ee8a
child 29608 564ea783ace8
permissions -rw-r--r--
moved global ML bindings to global place;
     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 len classes"
    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 @{text "Numeral_Type"}.
    19 *}
    20 
    21 class len0 = type +
    22   fixes len_of :: "'a itself \<Rightarrow> nat"
    23 
    24 text {* 
    25   Some theorems are only true on words with length greater 0.
    26 *}
    27 
    28 class len = len0 +
    29   assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
    30 
    31 instantiation num0 and num1 :: len0
    32 begin
    33 
    34 definition
    35   len_num0:  "len_of (x::num0 itself) = 0"
    36 
    37 definition
    38   len_num1: "len_of (x::num1 itself) = 1"
    39 
    40 instance ..
    41 
    42 end
    43 
    44 instantiation bit0 and bit1 :: (len0) len0
    45 begin
    46 
    47 definition
    48   len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
    49 
    50 definition
    51   len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1"
    52 
    53 instance ..
    54 
    55 end
    56 
    57 lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
    58 
    59 instance num1 :: len by (intro_classes) simp
    60 instance bit0 :: (len) len by (intro_classes) simp
    61 instance bit1 :: (len0) len by (intro_classes) simp
    62 
    63 -- "Examples:"
    64 lemma "len_of TYPE(17) = 17" by simp
    65 lemma "len_of TYPE(0) = 0" by simp
    66 
    67 -- "not simplified:"
    68 lemma "len_of TYPE('a::len0) = x"
    69   oops
    70    
    71 end
    72