src/HOL/Library/Type_Length.thy
changeset 63762 6920b1885eff
parent 61799 4cf66f21b764
child 64113 86efd3d4dc98
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Type_Length.thy	Thu Sep 01 20:59:51 2016 +0200
     1.3 @@ -0,0 +1,54 @@
     1.4 +(*  Title:      HOL/Library/Type_Length.thy
     1.5 +    Author:     John Matthews, Galois Connections, Inc., Copyright 2006
     1.6 +*)
     1.7 +
     1.8 +section \<open>Assigning lengths to types by type classes\<close>
     1.9 +
    1.10 +theory Type_Length
    1.11 +imports Numeral_Type
    1.12 +begin
    1.13 +
    1.14 +text \<open>
    1.15 +  The aim of this is to allow any type as index type, but to provide a
    1.16 +  default instantiation for numeral types. This independence requires
    1.17 +  some duplication with the definitions in \<^file>\<open>Numeral_Type.thy\<close>.
    1.18 +\<close>
    1.19 +
    1.20 +class len0 =
    1.21 +  fixes len_of :: "'a itself \<Rightarrow> nat"
    1.22 +
    1.23 +text \<open>Some theorems are only true on words with length greater 0.\<close>
    1.24 +
    1.25 +class len = len0 +
    1.26 +  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
    1.27 +
    1.28 +instantiation num0 and num1 :: len0
    1.29 +begin
    1.30 +
    1.31 +definition len_num0: "len_of (_ :: num0 itself) = 0"
    1.32 +definition len_num1: "len_of (_ :: num1 itself) = 1"
    1.33 +
    1.34 +instance ..
    1.35 +
    1.36 +end
    1.37 +
    1.38 +instantiation bit0 and bit1 :: (len0) len0
    1.39 +begin
    1.40 +
    1.41 +definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * len_of TYPE('a)"
    1.42 +definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * len_of TYPE('a) + 1"
    1.43 +
    1.44 +instance ..
    1.45 +
    1.46 +end
    1.47 +
    1.48 +lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
    1.49 +
    1.50 +instance num1 :: len
    1.51 +  by standard simp
    1.52 +instance bit0 :: (len) len
    1.53 +  by standard simp
    1.54 +instance bit1 :: (len0) len
    1.55 +  by standard simp
    1.56 +
    1.57 +end