author | wenzelm |
Mon, 16 Mar 2009 18:24:30 +0100 | |
changeset 30549 | d2d7874648bd |
parent 29631 | 3aa049e5f156 |
permissions | -rw-r--r-- |
24465 | 1 |
(* |
2 |
Author: John Matthews, Galois Connections, Inc., copyright 2006 |
|
3 |
||
4 |
A typeclass for parameterizing types by size. |
|
5 |
Used primarily to parameterize machine word sizes. |
|
6 |
*) |
|
25262
d0928156e326
Added reference to Jeremy Dawson's paper on the word library.
kleing
parents:
24465
diff
changeset
|
7 |
|
26560 | 8 |
header "The len classes" |
25262
d0928156e326
Added reference to Jeremy Dawson's paper on the word library.
kleing
parents:
24465
diff
changeset
|
9 |
|
24465 | 10 |
theory Size |
11 |
imports Numeral_Type |
|
12 |
begin |
|
13 |
||
14 |
text {* |
|
15 |
The aim of this is to allow any type as index type, but to provide a |
|
16 |
default instantiation for numeral types. This independence requires |
|
26560 | 17 |
some duplication with the definitions in @{text "Numeral_Type"}. |
24465 | 18 |
*} |
19 |
||
29608 | 20 |
class len0 = |
26514 | 21 |
fixes len_of :: "'a itself \<Rightarrow> nat" |
24465 | 22 |
|
23 |
text {* |
|
24 |
Some theorems are only true on words with length greater 0. |
|
25 |
*} |
|
26514 | 26 |
|
27 |
class len = len0 + |
|
28 |
assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)" |
|
29 |
||
30 |
instantiation num0 and num1 :: len0 |
|
31 |
begin |
|
32 |
||
33 |
definition |
|
34 |
len_num0: "len_of (x::num0 itself) = 0" |
|
35 |
||
36 |
definition |
|
37 |
len_num1: "len_of (x::num1 itself) = 1" |
|
38 |
||
39 |
instance .. |
|
24465 | 40 |
|
26514 | 41 |
end |
42 |
||
43 |
instantiation bit0 and bit1 :: (len0) len0 |
|
44 |
begin |
|
24465 | 45 |
|
26514 | 46 |
definition |
47 |
len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)" |
|
48 |
||
49 |
definition |
|
50 |
len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1" |
|
51 |
||
52 |
instance .. |
|
53 |
||
54 |
end |
|
24465 | 55 |
|
56 |
lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1 |
|
57 |
||
58 |
instance num1 :: len by (intro_classes) simp |
|
59 |
instance bit0 :: (len) len by (intro_classes) simp |
|
60 |
instance bit1 :: (len0) len by (intro_classes) simp |
|
61 |
||
62 |
-- "Examples:" |
|
63 |
lemma "len_of TYPE(17) = 17" by simp |
|
64 |
lemma "len_of TYPE(0) = 0" by simp |
|
65 |
||
66 |
-- "not simplified:" |
|
67 |
lemma "len_of TYPE('a::len0) = x" |
|
68 |
oops |
|
69 |
||
70 |
end |
|
71 |