src/HOL/Library/Type_Length.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 69597 ff784d5a5bfb
child 70348 bde161c740ca
permissions -rw-r--r--
improved code equations taken over from AFP
     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 syntax "_type_length" :: "type \<Rightarrow> nat" (\<open>(1LENGTH/(1'(_')))\<close>)
    21 
    22 translations "LENGTH('a)" \<rightharpoonup>
    23   "CONST len_of (CONST Pure.type :: 'a itself)"
    24 
    25 print_translation \<open>
    26   let
    27     fun len_of_itself_tr' ctxt [Const (\<^const_syntax>\<open>Pure.type\<close>, Type (_, [T]))] =
    28       Syntax.const \<^syntax_const>\<open>_type_length\<close> $ Syntax_Phases.term_of_typ ctxt T
    29   in [(\<^const_syntax>\<open>len_of\<close>, len_of_itself_tr')] end
    30 \<close>
    31 
    32 text \<open>Some theorems are only true on words with length greater 0.\<close>
    33 
    34 class len = len0 +
    35   assumes len_gt_0 [iff]: "0 < LENGTH('a)"
    36 
    37 instantiation num0 and num1 :: len0
    38 begin
    39 
    40 definition len_num0: "len_of (_ :: num0 itself) = 0"
    41 definition len_num1: "len_of (_ :: num1 itself) = 1"
    42 
    43 instance ..
    44 
    45 end
    46 
    47 instantiation bit0 and bit1 :: (len0) len0
    48 begin
    49 
    50 definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * LENGTH('a)"
    51 definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * LENGTH('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
    60   by standard simp
    61 instance bit0 :: (len) len
    62   by standard simp
    63 instance bit1 :: (len0) len
    64   by standard simp
    65 
    66 end