equal
deleted
inserted
replaced
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 *) |
|
7 |
|
8 header "The len classes" |
|
9 |
|
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 |
|
17 some duplication with the definitions in @{text "Numeral_Type"}. |
|
18 *} |
|
19 |
|
20 class len0 = |
|
21 fixes len_of :: "'a itself \<Rightarrow> nat" |
|
22 |
|
23 text {* |
|
24 Some theorems are only true on words with length greater 0. |
|
25 *} |
|
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 .. |
|
40 |
|
41 end |
|
42 |
|
43 instantiation bit0 and bit1 :: (len0) len0 |
|
44 begin |
|
45 |
|
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 |
|
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 |
|