src/HOL/Library/Type_Length.thy
changeset 64113 86efd3d4dc98
parent 63762 6920b1885eff
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/Type_Length.thy	Sat Oct 08 17:30:19 2016 +0200
     1.2 +++ b/src/HOL/Library/Type_Length.thy	Sat Oct 08 14:09:53 2016 +0200
     1.3 @@ -17,10 +17,22 @@
     1.4  class len0 =
     1.5    fixes len_of :: "'a itself \<Rightarrow> nat"
     1.6  
     1.7 +syntax "_type_length" :: "type \<Rightarrow> nat" ("(1LENGTH/(1'(_')))")
     1.8 +
     1.9 +translations "LENGTH('a)" \<rightharpoonup>
    1.10 +  "CONST len_of (CONST Pure.type :: 'a itself)"
    1.11 +
    1.12 +print_translation \<open>
    1.13 +  let
    1.14 +    fun len_of_itself_tr' ctxt [Const (@{const_syntax Pure.type}, Type (_, [T]))] =
    1.15 +      Syntax.const @{syntax_const "_type_length"} $ Syntax_Phases.term_of_typ ctxt T
    1.16 +  in [(@{const_syntax len_of}, len_of_itself_tr')] end
    1.17 +\<close>
    1.18 +
    1.19  text \<open>Some theorems are only true on words with length greater 0.\<close>
    1.20  
    1.21  class len = len0 +
    1.22 -  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
    1.23 +  assumes len_gt_0 [iff]: "0 < LENGTH('a)"
    1.24  
    1.25  instantiation num0 and num1 :: len0
    1.26  begin
    1.27 @@ -35,8 +47,8 @@
    1.28  instantiation bit0 and bit1 :: (len0) len0
    1.29  begin
    1.30  
    1.31 -definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * len_of TYPE('a)"
    1.32 -definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * len_of TYPE('a) + 1"
    1.33 +definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * LENGTH('a)"
    1.34 +definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * LENGTH('a) + 1"
    1.35  
    1.36  instance ..
    1.37