src/HOL/Word/Size.thy
author huffman
Tue Aug 28 20:13:47 2007 +0200 (2007-08-28)
changeset 24465 70f0214b3ecc
child 25262 d0928156e326
permissions -rw-r--r--
revert to Word library version from 2007/08/20
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
*)
huffman@24465
     8
theory Size
huffman@24465
     9
imports Numeral_Type
huffman@24465
    10
begin
huffman@24465
    11
huffman@24465
    12
text {*
huffman@24465
    13
  The aim of this is to allow any type as index type, but to provide a
huffman@24465
    14
  default instantiation for numeral types. This independence requires
huffman@24465
    15
  some duplication with the definitions in Numeral\_Type.
huffman@24465
    16
*}
huffman@24465
    17
axclass len0 < type
huffman@24465
    18
huffman@24465
    19
consts
huffman@24465
    20
  len_of :: "('a :: len0 itself) => nat"
huffman@24465
    21
huffman@24465
    22
text {* 
huffman@24465
    23
  Some theorems are only true on words with length greater 0.
huffman@24465
    24
*}
huffman@24465
    25
axclass len < len0
huffman@24465
    26
  len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
huffman@24465
    27
huffman@24465
    28
instance num0  :: len0 ..
huffman@24465
    29
instance num1 :: len0 ..
huffman@24465
    30
instance bit0 :: (len0) len0 ..
huffman@24465
    31
instance bit1 :: (len0) len0 ..
huffman@24465
    32
huffman@24465
    33
defs (overloaded)
huffman@24465
    34
  len_num0:  "len_of (x::num0 itself) == 0"
huffman@24465
    35
  len_num1: "len_of (x::num1 itself) == 1"
huffman@24465
    36
  len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
huffman@24465
    37
  len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
huffman@24465
    38
huffman@24465
    39
lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
huffman@24465
    40
huffman@24465
    41
instance num1 :: len by (intro_classes) simp
huffman@24465
    42
instance bit0 :: (len) len by (intro_classes) simp
huffman@24465
    43
instance bit1 :: (len0) len by (intro_classes) simp
huffman@24465
    44
huffman@24465
    45
-- "Examples:"
huffman@24465
    46
lemma "len_of TYPE(17) = 17" by simp
huffman@24465
    47
lemma "len_of TYPE(0) = 0" by simp
huffman@24465
    48
huffman@24465
    49
-- "not simplified:"
huffman@24465
    50
lemma "len_of TYPE('a::len0) = x"
huffman@24465
    51
  oops
huffman@24465
    52
   
huffman@24465
    53
end
huffman@24465
    54