src/HOL/Library/Type_Length.thy
changeset 63762 6920b1885eff
parent 61799 4cf66f21b764
child 64113 86efd3d4dc98
equal deleted inserted replaced
63761:2ca536d0163e 63762:6920b1885eff
       
     1 (*  Title:      HOL/Library/Type_Length.thy
       
     2     Author:     John Matthews, Galois Connections, Inc., Copyright 2006
       
     3 *)
       
     4 
       
     5 section \<open>Assigning lengths to types by type classes\<close>
       
     6 
       
     7 theory Type_Length
       
     8 imports Numeral_Type
       
     9 begin
       
    10 
       
    11 text \<open>
       
    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 \<^file>\<open>Numeral_Type.thy\<close>.
       
    15 \<close>
       
    16 
       
    17 class len0 =
       
    18   fixes len_of :: "'a itself \<Rightarrow> nat"
       
    19 
       
    20 text \<open>Some theorems are only true on words with length greater 0.\<close>
       
    21 
       
    22 class len = len0 +
       
    23   assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
       
    24 
       
    25 instantiation num0 and num1 :: len0
       
    26 begin
       
    27 
       
    28 definition len_num0: "len_of (_ :: num0 itself) = 0"
       
    29 definition len_num1: "len_of (_ :: num1 itself) = 1"
       
    30 
       
    31 instance ..
       
    32 
       
    33 end
       
    34 
       
    35 instantiation bit0 and bit1 :: (len0) len0
       
    36 begin
       
    37 
       
    38 definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * len_of TYPE('a)"
       
    39 definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * len_of TYPE('a) + 1"
       
    40 
       
    41 instance ..
       
    42 
       
    43 end
       
    44 
       
    45 lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
       
    46 
       
    47 instance num1 :: len
       
    48   by standard simp
       
    49 instance bit0 :: (len) len
       
    50   by standard simp
       
    51 instance bit1 :: (len0) len
       
    52   by standard simp
       
    53 
       
    54 end