src/HOL/Word/Size.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:     John Matthews, Galois Connections, Inc., copyright 2006
     3 
     4     A typeclass for parameterizing types by size.
     5     Used primarily to parameterize machine word sizes. 
     6 *)
     7 
     8 header "The len classes"
     9 
    10 theory Size
    11 imports Numeral_Type
    12 begin
    13 
    14 text {*
    15   The aim of this is to allow any type as index type, but to provide a
    16   default instantiation for numeral types. This independence requires
    17   some duplication with the definitions in @{text "Numeral_Type"}.
    18 *}
    19 
    20 class len0 =
    21   fixes len_of :: "'a itself \<Rightarrow> nat"
    22 
    23 text {* 
    24   Some theorems are only true on words with length greater 0.
    25 *}
    26 
    27 class len = len0 +
    28   assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
    29 
    30 instantiation num0 and num1 :: len0
    31 begin
    32 
    33 definition
    34   len_num0:  "len_of (x::num0 itself) = 0"
    35 
    36 definition
    37   len_num1: "len_of (x::num1 itself) = 1"
    38 
    39 instance ..
    40 
    41 end
    42 
    43 instantiation bit0 and bit1 :: (len0) len0
    44 begin
    45 
    46 definition
    47   len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
    48 
    49 definition
    50   len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1"
    51 
    52 instance ..
    53 
    54 end
    55 
    56 lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
    57 
    58 instance num1 :: len by (intro_classes) simp
    59 instance bit0 :: (len) len by (intro_classes) simp
    60 instance bit1 :: (len0) len by (intro_classes) simp
    61 
    62 -- "Examples:"
    63 lemma "len_of TYPE(17) = 17" by simp
    64 lemma "len_of TYPE(0) = 0" by simp
    65 
    66 -- "not simplified:"
    67 lemma "len_of TYPE('a::len0) = x"
    68   oops
    69    
    70 end
    71