author | wenzelm |
Thu, 01 Sep 2016 20:59:51 +0200 | |
changeset 63762 | 6920b1885eff |
parent 61799 | src/HOL/Word/Type_Length.thy@4cf66f21b764 |
child 64113 | 86efd3d4dc98 |
permissions | -rw-r--r-- |
63762 | 1 |
(* Title: HOL/Library/Type_Length.thy |
2 |
Author: John Matthews, Galois Connections, Inc., Copyright 2006 |
|
24465 | 3 |
*) |
25262
d0928156e326
Added reference to Jeremy Dawson's paper on the word library.
kleing
parents:
24465
diff
changeset
|
4 |
|
63762 | 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 | 7 |
theory Type_Length |
63762 | 8 |
imports Numeral_Type |
24465 | 9 |
begin |
10 |
||
61799 | 11 |
text \<open> |
24465 | 12 |
The aim of this is to allow any type as index type, but to provide a |
13 |
default instantiation for numeral types. This independence requires |
|
63762 | 14 |
some duplication with the definitions in \<^file>\<open>Numeral_Type.thy\<close>. |
61799 | 15 |
\<close> |
24465 | 16 |
|
29608 | 17 |
class len0 = |
26514 | 18 |
fixes len_of :: "'a itself \<Rightarrow> nat" |
24465 | 19 |
|
63762 | 20 |
text \<open>Some theorems are only true on words with length greater 0.\<close> |
26514 | 21 |
|
22 |
class len = len0 + |
|
23 |
assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)" |
|
24 |
||
25 |
instantiation num0 and num1 :: len0 |
|
26 |
begin |
|
27 |
||
63762 | 28 |
definition len_num0: "len_of (_ :: num0 itself) = 0" |
29 |
definition len_num1: "len_of (_ :: num1 itself) = 1" |
|
26514 | 30 |
|
31 |
instance .. |
|
24465 | 32 |
|
26514 | 33 |
end |
34 |
||
35 |
instantiation bit0 and bit1 :: (len0) len0 |
|
36 |
begin |
|
24465 | 37 |
|
63762 | 38 |
definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * len_of TYPE('a)" |
39 |
definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * len_of TYPE('a) + 1" |
|
26514 | 40 |
|
41 |
instance .. |
|
42 |
||
43 |
end |
|
24465 | 44 |
|
45 |
lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1 |
|
46 |
||
63762 | 47 |
instance num1 :: len |
48 |
by standard simp |
|
49 |
instance bit0 :: (len) len |
|
50 |
by standard simp |
|
51 |
instance bit1 :: (len0) len |
|
52 |
by standard simp |
|
24465 | 53 |
|
54 |
end |