dedicated syntax for types with a length
authorhaftmann
Sat Oct 08 14:09:53 2016 +0200 (2016-10-08)
changeset 6411386efd3d4dc98
parent 64112 84c1ae86b9af
child 64114 45e065eea984
dedicated syntax for types with a length
NEWS
src/HOL/Library/Type_Length.thy
src/HOL/ex/Word_Type.thy
     1.1 --- a/NEWS	Sat Oct 08 17:30:19 2016 +0200
     1.2 +++ b/NEWS	Sat Oct 08 14:09:53 2016 +0200
     1.3 @@ -249,6 +249,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Dedicated syntax LENGTH('a) for length of types.
     1.8 +
     1.9  * New proof method "argo" using the built-in Argo solver based on SMT
    1.10  technology. The method can be used to prove goals of quantifier-free
    1.11  propositional logic, goals based on a combination of quantifier-free
     2.1 --- a/src/HOL/Library/Type_Length.thy	Sat Oct 08 17:30:19 2016 +0200
     2.2 +++ b/src/HOL/Library/Type_Length.thy	Sat Oct 08 14:09:53 2016 +0200
     2.3 @@ -17,10 +17,22 @@
     2.4  class len0 =
     2.5    fixes len_of :: "'a itself \<Rightarrow> nat"
     2.6  
     2.7 +syntax "_type_length" :: "type \<Rightarrow> nat" ("(1LENGTH/(1'(_')))")
     2.8 +
     2.9 +translations "LENGTH('a)" \<rightharpoonup>
    2.10 +  "CONST len_of (CONST Pure.type :: 'a itself)"
    2.11 +
    2.12 +print_translation \<open>
    2.13 +  let
    2.14 +    fun len_of_itself_tr' ctxt [Const (@{const_syntax Pure.type}, Type (_, [T]))] =
    2.15 +      Syntax.const @{syntax_const "_type_length"} $ Syntax_Phases.term_of_typ ctxt T
    2.16 +  in [(@{const_syntax len_of}, len_of_itself_tr')] end
    2.17 +\<close>
    2.18 +
    2.19  text \<open>Some theorems are only true on words with length greater 0.\<close>
    2.20  
    2.21  class len = len0 +
    2.22 -  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
    2.23 +  assumes len_gt_0 [iff]: "0 < LENGTH('a)"
    2.24  
    2.25  instantiation num0 and num1 :: len0
    2.26  begin
    2.27 @@ -35,8 +47,8 @@
    2.28  instantiation bit0 and bit1 :: (len0) len0
    2.29  begin
    2.30  
    2.31 -definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * len_of TYPE('a)"
    2.32 -definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * len_of TYPE('a) + 1"
    2.33 +definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * LENGTH('a)"
    2.34 +definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * LENGTH('a) + 1"
    2.35  
    2.36  instance ..
    2.37  
     3.1 --- a/src/HOL/ex/Word_Type.thy	Sat Oct 08 17:30:19 2016 +0200
     3.2 +++ b/src/HOL/ex/Word_Type.thy	Sat Oct 08 14:09:53 2016 +0200
     3.3 @@ -9,21 +9,6 @@
     3.4      "~~/src/HOL/Library/Type_Length"
     3.5  begin
     3.6  
     3.7 -subsection \<open>Compact syntax for types with a length\<close>
     3.8 -
     3.9 -syntax "_type_length" :: "type \<Rightarrow> nat" ("(1LENGTH/(1'(_')))")
    3.10 -
    3.11 -translations "LENGTH('a)" \<rightharpoonup>
    3.12 -  "CONST len_of (CONST Pure.type :: 'a itself)"
    3.13 -
    3.14 -print_translation \<open>
    3.15 -  let
    3.16 -    fun len_of_itself_tr' ctxt [Const (@{const_syntax Pure.type}, Type (_, [T]))] =
    3.17 -      Syntax.const @{syntax_const "_type_length"} $ Syntax_Phases.term_of_typ ctxt T
    3.18 -  in [(@{const_syntax len_of}, len_of_itself_tr')] end
    3.19 -\<close>
    3.20 -
    3.21 -
    3.22  subsection \<open>Truncating bit representations of numeric types\<close>
    3.23  
    3.24  class semiring_bits = semiring_div_parity +