--- a/NEWS Sat Oct 08 17:30:19 2016 +0200
+++ b/NEWS Sat Oct 08 14:09:53 2016 +0200
@@ -249,6 +249,8 @@
*** HOL ***
+* Dedicated syntax LENGTH('a) for length of types.
+
* New proof method "argo" using the built-in Argo solver based on SMT
technology. The method can be used to prove goals of quantifier-free
propositional logic, goals based on a combination of quantifier-free
--- a/src/HOL/Library/Type_Length.thy Sat Oct 08 17:30:19 2016 +0200
+++ b/src/HOL/Library/Type_Length.thy Sat Oct 08 14:09:53 2016 +0200
@@ -17,10 +17,22 @@
class len0 =
fixes len_of :: "'a itself \<Rightarrow> nat"
+syntax "_type_length" :: "type \<Rightarrow> nat" ("(1LENGTH/(1'(_')))")
+
+translations "LENGTH('a)" \<rightharpoonup>
+ "CONST len_of (CONST Pure.type :: 'a itself)"
+
+print_translation \<open>
+ let
+ fun len_of_itself_tr' ctxt [Const (@{const_syntax Pure.type}, Type (_, [T]))] =
+ Syntax.const @{syntax_const "_type_length"} $ Syntax_Phases.term_of_typ ctxt T
+ in [(@{const_syntax len_of}, len_of_itself_tr')] end
+\<close>
+
text \<open>Some theorems are only true on words with length greater 0.\<close>
class len = len0 +
- assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
+ assumes len_gt_0 [iff]: "0 < LENGTH('a)"
instantiation num0 and num1 :: len0
begin
@@ -35,8 +47,8 @@
instantiation bit0 and bit1 :: (len0) len0
begin
-definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * len_of TYPE('a)"
-definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * len_of TYPE('a) + 1"
+definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * LENGTH('a)"
+definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * LENGTH('a) + 1"
instance ..
--- a/src/HOL/ex/Word_Type.thy Sat Oct 08 17:30:19 2016 +0200
+++ b/src/HOL/ex/Word_Type.thy Sat Oct 08 14:09:53 2016 +0200
@@ -9,21 +9,6 @@
"~~/src/HOL/Library/Type_Length"
begin
-subsection \<open>Compact syntax for types with a length\<close>
-
-syntax "_type_length" :: "type \<Rightarrow> nat" ("(1LENGTH/(1'(_')))")
-
-translations "LENGTH('a)" \<rightharpoonup>
- "CONST len_of (CONST Pure.type :: 'a itself)"
-
-print_translation \<open>
- let
- fun len_of_itself_tr' ctxt [Const (@{const_syntax Pure.type}, Type (_, [T]))] =
- Syntax.const @{syntax_const "_type_length"} $ Syntax_Phases.term_of_typ ctxt T
- in [(@{const_syntax len_of}, len_of_itself_tr')] end
-\<close>
-
-
subsection \<open>Truncating bit representations of numeric types\<close>
class semiring_bits = semiring_div_parity +