src/HOL/Word/Type_Length.thy
author haftmann
Wed Jun 30 16:28:14 2010 +0200 (2010-06-30)
changeset 37655 f4d616d41a59
parent 29631 src/HOL/Word/Size.thy@3aa049e5f156
child 41413 64cd30d6b0b8
permissions -rw-r--r--
more speaking theory names
     1 (*  Title:      HOL/Word/Type_Length.thy
     2     Author:     John Matthews, Galois Connections, Inc., copyright 2006
     3 *)
     4 
     5 header {* Assigning lengths to types by typeclasses *}
     6 
     7 theory Type_Length
     8 imports Numeral_Type
     9 begin
    10 
    11 text {*
    12   The aim of this is to allow any type as index type, but to provide a
    13   default instantiation for numeral types. This independence requires
    14   some duplication with the definitions in @{text "Numeral_Type"}.
    15 *}
    16 
    17 class len0 =
    18   fixes len_of :: "'a itself \<Rightarrow> nat"
    19 
    20 text {* 
    21   Some theorems are only true on words with length greater 0.
    22 *}
    23 
    24 class len = len0 +
    25   assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
    26 
    27 instantiation num0 and num1 :: len0
    28 begin
    29 
    30 definition
    31   len_num0:  "len_of (x::num0 itself) = 0"
    32 
    33 definition
    34   len_num1: "len_of (x::num1 itself) = 1"
    35 
    36 instance ..
    37 
    38 end
    39 
    40 instantiation bit0 and bit1 :: (len0) len0
    41 begin
    42 
    43 definition
    44   len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
    45 
    46 definition
    47   len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1"
    48 
    49 instance ..
    50 
    51 end
    52 
    53 lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
    54 
    55 instance num1 :: len proof qed simp
    56 instance bit0 :: (len) len proof qed simp
    57 instance bit1 :: (len0) len proof qed simp
    58 
    59 end
    60