src/HOL/Word/Size.thy
author haftmann
Wed Jan 21 23:40:23 2009 +0100 (2009-01-21)
changeset 29608 564ea783ace8
parent 26560 d2fc9a18ee8a
child 29631 3aa049e5f156
permissions -rw-r--r--
no base sort in class import
huffman@24465
     1
(* 
huffman@24465
     2
    ID:         $Id$
huffman@24465
     3
    Author:     John Matthews, Galois Connections, Inc., copyright 2006
huffman@24465
     4
huffman@24465
     5
    A typeclass for parameterizing types by size.
huffman@24465
     6
    Used primarily to parameterize machine word sizes. 
huffman@24465
     7
*)
kleing@25262
     8
haftmann@26560
     9
header "The len classes"
kleing@25262
    10
huffman@24465
    11
theory Size
huffman@24465
    12
imports Numeral_Type
huffman@24465
    13
begin
huffman@24465
    14
huffman@24465
    15
text {*
huffman@24465
    16
  The aim of this is to allow any type as index type, but to provide a
huffman@24465
    17
  default instantiation for numeral types. This independence requires
haftmann@26560
    18
  some duplication with the definitions in @{text "Numeral_Type"}.
huffman@24465
    19
*}
huffman@24465
    20
haftmann@29608
    21
class len0 =
haftmann@26514
    22
  fixes len_of :: "'a itself \<Rightarrow> nat"
huffman@24465
    23
huffman@24465
    24
text {* 
huffman@24465
    25
  Some theorems are only true on words with length greater 0.
huffman@24465
    26
*}
haftmann@26514
    27
haftmann@26514
    28
class len = len0 +
haftmann@26514
    29
  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
haftmann@26514
    30
haftmann@26514
    31
instantiation num0 and num1 :: len0
haftmann@26514
    32
begin
haftmann@26514
    33
haftmann@26514
    34
definition
haftmann@26514
    35
  len_num0:  "len_of (x::num0 itself) = 0"
haftmann@26514
    36
haftmann@26514
    37
definition
haftmann@26514
    38
  len_num1: "len_of (x::num1 itself) = 1"
haftmann@26514
    39
haftmann@26514
    40
instance ..
huffman@24465
    41
haftmann@26514
    42
end
haftmann@26514
    43
haftmann@26514
    44
instantiation bit0 and bit1 :: (len0) len0
haftmann@26514
    45
begin
huffman@24465
    46
haftmann@26514
    47
definition
haftmann@26514
    48
  len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
haftmann@26514
    49
haftmann@26514
    50
definition
haftmann@26514
    51
  len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('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
huffman@24465
    59
instance num1 :: len by (intro_classes) simp
huffman@24465
    60
instance bit0 :: (len) len by (intro_classes) simp
huffman@24465
    61
instance bit1 :: (len0) len by (intro_classes) simp
huffman@24465
    62
huffman@24465
    63
-- "Examples:"
huffman@24465
    64
lemma "len_of TYPE(17) = 17" by simp
huffman@24465
    65
lemma "len_of TYPE(0) = 0" by simp
huffman@24465
    66
huffman@24465
    67
-- "not simplified:"
huffman@24465
    68
lemma "len_of TYPE('a::len0) = x"
huffman@24465
    69
  oops
huffman@24465
    70
   
huffman@24465
    71
end
huffman@24465
    72