src/HOL/Word/Size.thy
changeset 24333 e77ea0ea7f2c
child 24406 d96eb21fc1bc
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Word/Size.thy	Mon Aug 20 04:34:31 2007 +0200
     1.3 @@ -0,0 +1,54 @@
     1.4 +(* 
     1.5 +    ID:         $Id$
     1.6 +    Author:     John Matthews, Galois Connections, Inc., copyright 2006
     1.7 +
     1.8 +    A typeclass for parameterizing types by size.
     1.9 +    Used primarily to parameterize machine word sizes. 
    1.10 +*)
    1.11 +theory Size
    1.12 +imports Numeral_Type
    1.13 +begin
    1.14 +
    1.15 +text {*
    1.16 +  The aim of this is to allow any type as index type, but to provide a
    1.17 +  default instantiation for numeral types. This independence requires
    1.18 +  some duplication with the definitions in Numeral\_Type.
    1.19 +*}
    1.20 +axclass len0 < type
    1.21 +
    1.22 +consts
    1.23 +  len_of :: "('a :: len0 itself) => nat"
    1.24 +
    1.25 +text {* 
    1.26 +  Some theorems are only true on words with length greater 0.
    1.27 +*}
    1.28 +axclass len < len0
    1.29 +  len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
    1.30 +
    1.31 +instance pls  :: len0 ..
    1.32 +instance num1 :: len0 ..
    1.33 +instance bit0 :: (len0) len0 ..
    1.34 +instance bit1 :: (len0) len0 ..
    1.35 +
    1.36 +defs (overloaded)
    1.37 +  len_pls:  "len_of (x::pls itself) == 0"
    1.38 +  len_num1: "len_of (x::num1 itself) == 1"
    1.39 +  len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
    1.40 +  len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
    1.41 +
    1.42 +lemmas len_of_numeral_defs [simp] = len_pls len_num1 len_bit0 len_bit1
    1.43 +
    1.44 +instance num1 :: len by (intro_classes) simp
    1.45 +instance bit0 :: (len) len by (intro_classes) simp
    1.46 +instance bit1 :: (len0) len by (intro_classes) simp
    1.47 +
    1.48 +-- "Examples:"
    1.49 +lemma "len_of TYPE(17) = 17" by simp
    1.50 +lemma "len_of TYPE(0) = 0" by simp
    1.51 +
    1.52 +-- "not simplified:"
    1.53 +lemma "len_of TYPE('a::len0) = x"
    1.54 +  oops
    1.55 +   
    1.56 +end
    1.57 +