author | wenzelm |
Mon, 07 Dec 2015 10:38:04 +0100 | |
changeset 61799 | 4cf66f21b764 |
parent 58874 | 7172c7ffb047 |
permissions | -rw-r--r-- |
37655 | 1 |
(* Title: HOL/Word/Type_Length.thy |
24465 | 2 |
Author: John Matthews, Galois Connections, Inc., copyright 2006 |
3 |
*) |
|
25262
d0928156e326
Added reference to Jeremy Dawson's paper on the word library.
kleing
parents:
24465
diff
changeset
|
4 |
|
61799 | 5 |
section \<open>Assigning lengths to types by typeclasses\<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 |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
37655
diff
changeset
|
8 |
imports "~~/src/HOL/Library/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 |
|
61799 | 14 |
some duplication with the definitions in \<open>Numeral_Type\<close>. |
15 |
\<close> |
|
24465 | 16 |
|
29608 | 17 |
class len0 = |
26514 | 18 |
fixes len_of :: "'a itself \<Rightarrow> nat" |
24465 | 19 |
|
61799 | 20 |
text \<open> |
24465 | 21 |
Some theorems are only true on words with length greater 0. |
61799 | 22 |
\<close> |
26514 | 23 |
|
24 |
class len = len0 + |
|
25 |
assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)" |
|
26 |
||
27 |
instantiation num0 and num1 :: len0 |
|
28 |
begin |
|
29 |
||
30 |
definition |
|
31 |
len_num0: "len_of (x::num0 itself) = 0" |
|
32 |
||
33 |
definition |
|
34 |
len_num1: "len_of (x::num1 itself) = 1" |
|
35 |
||
36 |
instance .. |
|
24465 | 37 |
|
26514 | 38 |
end |
39 |
||
40 |
instantiation bit0 and bit1 :: (len0) len0 |
|
41 |
begin |
|
24465 | 42 |
|
26514 | 43 |
definition |
44 |
len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)" |
|
45 |
||
46 |
definition |
|
47 |
len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1" |
|
48 |
||
49 |
instance .. |
|
50 |
||
51 |
end |
|
24465 | 52 |
|
53 |
lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1 |
|
54 |
||
37655 | 55 |
instance num1 :: len proof qed simp |
56 |
instance bit0 :: (len) len proof qed simp |
|
57 |
instance bit1 :: (len0) len proof qed simp |
|
24465 | 58 |
|
59 |
end |
|
60 |