src/HOL/Word/Type_Length.thy
author wenzelm
Mon Dec 07 10:38:04 2015 +0100 (2015-12-07)
changeset 61799 4cf66f21b764
parent 58874 7172c7ffb047
permissions -rw-r--r--
isabelle update_cartouches -c -t;
haftmann@37655
     1
(*  Title:      HOL/Word/Type_Length.thy
huffman@24465
     2
    Author:     John Matthews, Galois Connections, Inc., copyright 2006
huffman@24465
     3
*)
kleing@25262
     4
wenzelm@61799
     5
section \<open>Assigning lengths to types by typeclasses\<close>
kleing@25262
     6
haftmann@37655
     7
theory Type_Length
wenzelm@41413
     8
imports "~~/src/HOL/Library/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@61799
    14
  some duplication with the definitions in \<open>Numeral_Type\<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
wenzelm@61799
    20
text \<open>
huffman@24465
    21
  Some theorems are only true on words with length greater 0.
wenzelm@61799
    22
\<close>
haftmann@26514
    23
haftmann@26514
    24
class len = len0 +
haftmann@26514
    25
  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
haftmann@26514
    26
haftmann@26514
    27
instantiation num0 and num1 :: len0
haftmann@26514
    28
begin
haftmann@26514
    29
haftmann@26514
    30
definition
haftmann@26514
    31
  len_num0:  "len_of (x::num0 itself) = 0"
haftmann@26514
    32
haftmann@26514
    33
definition
haftmann@26514
    34
  len_num1: "len_of (x::num1 itself) = 1"
haftmann@26514
    35
haftmann@26514
    36
instance ..
huffman@24465
    37
haftmann@26514
    38
end
haftmann@26514
    39
haftmann@26514
    40
instantiation bit0 and bit1 :: (len0) len0
haftmann@26514
    41
begin
huffman@24465
    42
haftmann@26514
    43
definition
haftmann@26514
    44
  len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
haftmann@26514
    45
haftmann@26514
    46
definition
haftmann@26514
    47
  len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1"
haftmann@26514
    48
haftmann@26514
    49
instance ..
haftmann@26514
    50
haftmann@26514
    51
end
huffman@24465
    52
huffman@24465
    53
lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
huffman@24465
    54
haftmann@37655
    55
instance num1 :: len proof qed simp
haftmann@37655
    56
instance bit0 :: (len) len proof qed simp
haftmann@37655
    57
instance bit1 :: (len0) len proof qed simp
huffman@24465
    58
huffman@24465
    59
end
huffman@24465
    60