src/HOL/Word/Size.thy
author huffman
Wed Aug 22 18:53:54 2007 +0200 (2007-08-22)
changeset 24406 d96eb21fc1bc
parent 24333 e77ea0ea7f2c
permissions -rw-r--r--
rename type pls to num0
kleing@24333
     1
(* 
kleing@24333
     2
    ID:         $Id$
kleing@24333
     3
    Author:     John Matthews, Galois Connections, Inc., copyright 2006
kleing@24333
     4
kleing@24333
     5
    A typeclass for parameterizing types by size.
kleing@24333
     6
    Used primarily to parameterize machine word sizes. 
kleing@24333
     7
*)
kleing@24333
     8
theory Size
kleing@24333
     9
imports Numeral_Type
kleing@24333
    10
begin
kleing@24333
    11
kleing@24333
    12
text {*
kleing@24333
    13
  The aim of this is to allow any type as index type, but to provide a
kleing@24333
    14
  default instantiation for numeral types. This independence requires
kleing@24333
    15
  some duplication with the definitions in Numeral\_Type.
kleing@24333
    16
*}
kleing@24333
    17
axclass len0 < type
kleing@24333
    18
kleing@24333
    19
consts
kleing@24333
    20
  len_of :: "('a :: len0 itself) => nat"
kleing@24333
    21
kleing@24333
    22
text {* 
kleing@24333
    23
  Some theorems are only true on words with length greater 0.
kleing@24333
    24
*}
kleing@24333
    25
axclass len < len0
kleing@24333
    26
  len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
kleing@24333
    27
huffman@24406
    28
instance num0  :: len0 ..
kleing@24333
    29
instance num1 :: len0 ..
kleing@24333
    30
instance bit0 :: (len0) len0 ..
kleing@24333
    31
instance bit1 :: (len0) len0 ..
kleing@24333
    32
kleing@24333
    33
defs (overloaded)
huffman@24406
    34
  len_num0: "len_of (x::num0 itself) == 0"
kleing@24333
    35
  len_num1: "len_of (x::num1 itself) == 1"
kleing@24333
    36
  len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
kleing@24333
    37
  len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
kleing@24333
    38
huffman@24406
    39
lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
kleing@24333
    40
kleing@24333
    41
instance num1 :: len by (intro_classes) simp
kleing@24333
    42
instance bit0 :: (len) len by (intro_classes) simp
kleing@24333
    43
instance bit1 :: (len0) len by (intro_classes) simp
kleing@24333
    44
kleing@24333
    45
-- "Examples:"
kleing@24333
    46
lemma "len_of TYPE(17) = 17" by simp
kleing@24333
    47
lemma "len_of TYPE(0) = 0" by simp
kleing@24333
    48
kleing@24333
    49
-- "not simplified:"
kleing@24333
    50
lemma "len_of TYPE('a::len0) = x"
kleing@24333
    51
  oops
kleing@24333
    52
   
kleing@24333
    53
end
kleing@24333
    54