src/HOL/Word/Type_Length.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 37655 f4d616d41a59
child 58874 7172c7ffb047
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
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
haftmann@37655
     5
header {* Assigning lengths to types by typeclasses *}
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
huffman@24465
    11
text {*
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
haftmann@26560
    14
  some duplication with the definitions in @{text "Numeral_Type"}.
huffman@24465
    15
*}
huffman@24465
    16
haftmann@29608
    17
class len0 =
haftmann@26514
    18
  fixes len_of :: "'a itself \<Rightarrow> nat"
huffman@24465
    19
huffman@24465
    20
text {* 
huffman@24465
    21
  Some theorems are only true on words with length greater 0.
huffman@24465
    22
*}
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