src/HOL/Library/Type_Length.thy
author wenzelm
Sat, 04 Nov 2017 15:24:40 +0100
changeset 67003 49850a679c2c
parent 64113 86efd3d4dc98
child 69593 3dda49e08b9d
permissions -rw-r--r--
more robust sorted_entries;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63762
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
     1
(*  Title:      HOL/Library/Type_Length.thy
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
     2
    Author:     John Matthews, Galois Connections, Inc., Copyright 2006
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
     3
*)
25262
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24465
diff changeset
     4
63762
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
     5
section \<open>Assigning lengths to types by type classes\<close>
25262
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24465
diff changeset
     6
37655
f4d616d41a59 more speaking theory names
haftmann
parents: 29631
diff changeset
     7
theory Type_Length
63762
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
     8
imports Numeral_Type
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
     9
begin
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
    10
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 58874
diff changeset
    11
text \<open>
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
    12
  The aim of this is to allow any type as index type, but to provide a
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
    13
  default instantiation for numeral types. This independence requires
63762
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
    14
  some duplication with the definitions in \<^file>\<open>Numeral_Type.thy\<close>.
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 58874
diff changeset
    15
\<close>
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
    16
29608
564ea783ace8 no base sort in class import
haftmann
parents: 26560
diff changeset
    17
class len0 =
26514
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    18
  fixes len_of :: "'a itself \<Rightarrow> nat"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
    19
64113
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    20
syntax "_type_length" :: "type \<Rightarrow> nat" ("(1LENGTH/(1'(_')))")
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    21
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    22
translations "LENGTH('a)" \<rightharpoonup>
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    23
  "CONST len_of (CONST Pure.type :: 'a itself)"
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    24
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    25
print_translation \<open>
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    26
  let
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    27
    fun len_of_itself_tr' ctxt [Const (@{const_syntax Pure.type}, Type (_, [T]))] =
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    28
      Syntax.const @{syntax_const "_type_length"} $ Syntax_Phases.term_of_typ ctxt T
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    29
  in [(@{const_syntax len_of}, len_of_itself_tr')] end
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    30
\<close>
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    31
63762
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
    32
text \<open>Some theorems are only true on words with length greater 0.\<close>
26514
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    33
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    34
class len = len0 +
64113
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    35
  assumes len_gt_0 [iff]: "0 < LENGTH('a)"
26514
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    36
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    37
instantiation num0 and num1 :: len0
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    38
begin
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    39
63762
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
    40
definition len_num0: "len_of (_ :: num0 itself) = 0"
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
    41
definition len_num1: "len_of (_ :: num1 itself) = 1"
26514
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    42
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    43
instance ..
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
    44
26514
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    45
end
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    46
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    47
instantiation bit0 and bit1 :: (len0) len0
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    48
begin
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
    49
64113
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    50
definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * LENGTH('a)"
86efd3d4dc98 dedicated syntax for types with a length
haftmann
parents: 63762
diff changeset
    51
definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * LENGTH('a) + 1"
26514
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    52
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    53
instance ..
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    54
eff55c0a6d34 tuned towards code generation
haftmann
parents: 25262
diff changeset
    55
end
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
    56
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
    57
lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
    58
63762
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
    59
instance num1 :: len
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
    60
  by standard simp
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
    61
instance bit0 :: (len) len
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
    62
  by standard simp
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
    63
instance bit1 :: (len0) len
6920b1885eff clarified session;
wenzelm
parents: 61799
diff changeset
    64
  by standard simp
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
    65
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents:
diff changeset
    66
end