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