author | wenzelm |
Wed, 29 Dec 2010 17:34:41 +0100 | |
changeset 41413 | 64cd30d6b0b8 |
parent 37655 | f4d616d41a59 |
child 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 |
|
37655 | 5 |
header {* Assigning lengths to types by typeclasses *} |
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 |
||
11 |
text {* |
|
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 |
|
26560 | 14 |
some duplication with the definitions in @{text "Numeral_Type"}. |
24465 | 15 |
*} |
16 |
||
29608 | 17 |
class len0 = |
26514 | 18 |
fixes len_of :: "'a itself \<Rightarrow> nat" |
24465 | 19 |
|
20 |
text {* |
|
21 |
Some theorems are only true on words with length greater 0. |
|
22 |
*} |
|
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 |