src/HOL/Word/Size.thy
changeset 26514 eff55c0a6d34
parent 25262 d0928156e326
child 26560 d2fc9a18ee8a
     1.1 --- a/src/HOL/Word/Size.thy	Wed Apr 02 15:58:32 2008 +0200
     1.2 +++ b/src/HOL/Word/Size.thy	Wed Apr 02 15:58:36 2008 +0200
     1.3 @@ -17,27 +17,42 @@
     1.4    default instantiation for numeral types. This independence requires
     1.5    some duplication with the definitions in Numeral\_Type.
     1.6  *}
     1.7 -axclass len0 < type
     1.8  
     1.9 -consts
    1.10 -  len_of :: "('a :: len0 itself) => nat"
    1.11 +class len0 = type +
    1.12 +  fixes len_of :: "'a itself \<Rightarrow> nat"
    1.13  
    1.14  text {* 
    1.15    Some theorems are only true on words with length greater 0.
    1.16  *}
    1.17 -axclass len < len0
    1.18 -  len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
    1.19 +
    1.20 +class len = len0 +
    1.21 +  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
    1.22 +
    1.23 +instantiation num0 and num1 :: len0
    1.24 +begin
    1.25 +
    1.26 +definition
    1.27 +  len_num0:  "len_of (x::num0 itself) = 0"
    1.28 +
    1.29 +definition
    1.30 +  len_num1: "len_of (x::num1 itself) = 1"
    1.31 +
    1.32 +instance ..
    1.33  
    1.34 -instance num0  :: len0 ..
    1.35 -instance num1 :: len0 ..
    1.36 -instance bit0 :: (len0) len0 ..
    1.37 -instance bit1 :: (len0) len0 ..
    1.38 +end
    1.39 +
    1.40 +instantiation bit0 and bit1 :: (len0) len0
    1.41 +begin
    1.42  
    1.43 -defs (overloaded)
    1.44 -  len_num0:  "len_of (x::num0 itself) == 0"
    1.45 -  len_num1: "len_of (x::num1 itself) == 1"
    1.46 -  len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
    1.47 -  len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
    1.48 +definition
    1.49 +  len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
    1.50 +
    1.51 +definition
    1.52 +  len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1"
    1.53 +
    1.54 +instance ..
    1.55 +
    1.56 +end
    1.57  
    1.58  lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
    1.59