src/HOL/Library/Type_Length.thy
author wenzelm
Tue May 15 13:57:39 2018 +0200 (16 months ago)
changeset 68189 6163c90694ef
parent 64113 86efd3d4dc98
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned headers;
wenzelm@63762
     1
(*  Title:      HOL/Library/Type_Length.thy
wenzelm@63762
     2
    Author:     John Matthews, Galois Connections, Inc., Copyright 2006
huffman@24465
     3
*)
kleing@25262
     4
wenzelm@63762
     5
section \<open>Assigning lengths to types by type classes\<close>
kleing@25262
     6
haftmann@37655
     7
theory Type_Length
wenzelm@63762
     8
imports Numeral_Type
huffman@24465
     9
begin
huffman@24465
    10
wenzelm@61799
    11
text \<open>
huffman@24465
    12
  The aim of this is to allow any type as index type, but to provide a
huffman@24465
    13
  default instantiation for numeral types. This independence requires
wenzelm@63762
    14
  some duplication with the definitions in \<^file>\<open>Numeral_Type.thy\<close>.
wenzelm@61799
    15
\<close>
huffman@24465
    16
haftmann@29608
    17
class len0 =
haftmann@26514
    18
  fixes len_of :: "'a itself \<Rightarrow> nat"
huffman@24465
    19
haftmann@64113
    20
syntax "_type_length" :: "type \<Rightarrow> nat" ("(1LENGTH/(1'(_')))")
haftmann@64113
    21
haftmann@64113
    22
translations "LENGTH('a)" \<rightharpoonup>
haftmann@64113
    23
  "CONST len_of (CONST Pure.type :: 'a itself)"
haftmann@64113
    24
haftmann@64113
    25
print_translation \<open>
haftmann@64113
    26
  let
haftmann@64113
    27
    fun len_of_itself_tr' ctxt [Const (@{const_syntax Pure.type}, Type (_, [T]))] =
haftmann@64113
    28
      Syntax.const @{syntax_const "_type_length"} $ Syntax_Phases.term_of_typ ctxt T
haftmann@64113
    29
  in [(@{const_syntax len_of}, len_of_itself_tr')] end
haftmann@64113
    30
\<close>
haftmann@64113
    31
wenzelm@63762
    32
text \<open>Some theorems are only true on words with length greater 0.\<close>
haftmann@26514
    33
haftmann@26514
    34
class len = len0 +
haftmann@64113
    35
  assumes len_gt_0 [iff]: "0 < LENGTH('a)"
haftmann@26514
    36
haftmann@26514
    37
instantiation num0 and num1 :: len0
haftmann@26514
    38
begin
haftmann@26514
    39
wenzelm@63762
    40
definition len_num0: "len_of (_ :: num0 itself) = 0"
wenzelm@63762
    41
definition len_num1: "len_of (_ :: num1 itself) = 1"
haftmann@26514
    42
haftmann@26514
    43
instance ..
huffman@24465
    44
haftmann@26514
    45
end
haftmann@26514
    46
haftmann@26514
    47
instantiation bit0 and bit1 :: (len0) len0
haftmann@26514
    48
begin
huffman@24465
    49
haftmann@64113
    50
definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * LENGTH('a)"
haftmann@64113
    51
definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * LENGTH('a) + 1"
haftmann@26514
    52
haftmann@26514
    53
instance ..
haftmann@26514
    54
haftmann@26514
    55
end
huffman@24465
    56
huffman@24465
    57
lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
huffman@24465
    58
wenzelm@63762
    59
instance num1 :: len
wenzelm@63762
    60
  by standard simp
wenzelm@63762
    61
instance bit0 :: (len) len
wenzelm@63762
    62
  by standard simp
wenzelm@63762
    63
instance bit1 :: (len0) len
wenzelm@63762
    64
  by standard simp
huffman@24465
    65
huffman@24465
    66
end