|
24465
|
1 |
(*
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: John Matthews, Galois Connections, Inc., copyright 2006
|
|
|
4 |
|
|
|
5 |
A typeclass for parameterizing types by size.
|
|
|
6 |
Used primarily to parameterize machine word sizes.
|
|
|
7 |
*)
|
|
|
8 |
theory Size
|
|
|
9 |
imports Numeral_Type
|
|
|
10 |
begin
|
|
|
11 |
|
|
|
12 |
text {*
|
|
|
13 |
The aim of this is to allow any type as index type, but to provide a
|
|
|
14 |
default instantiation for numeral types. This independence requires
|
|
|
15 |
some duplication with the definitions in Numeral\_Type.
|
|
|
16 |
*}
|
|
|
17 |
axclass len0 < type
|
|
|
18 |
|
|
|
19 |
consts
|
|
|
20 |
len_of :: "('a :: len0 itself) => nat"
|
|
|
21 |
|
|
|
22 |
text {*
|
|
|
23 |
Some theorems are only true on words with length greater 0.
|
|
|
24 |
*}
|
|
|
25 |
axclass len < len0
|
|
|
26 |
len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
|
|
|
27 |
|
|
|
28 |
instance num0 :: len0 ..
|
|
|
29 |
instance num1 :: len0 ..
|
|
|
30 |
instance bit0 :: (len0) len0 ..
|
|
|
31 |
instance bit1 :: (len0) len0 ..
|
|
|
32 |
|
|
|
33 |
defs (overloaded)
|
|
|
34 |
len_num0: "len_of (x::num0 itself) == 0"
|
|
|
35 |
len_num1: "len_of (x::num1 itself) == 1"
|
|
|
36 |
len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
|
|
|
37 |
len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
|
|
|
38 |
|
|
|
39 |
lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
|
|
|
40 |
|
|
|
41 |
instance num1 :: len by (intro_classes) simp
|
|
|
42 |
instance bit0 :: (len) len by (intro_classes) simp
|
|
|
43 |
instance bit1 :: (len0) len by (intro_classes) simp
|
|
|
44 |
|
|
|
45 |
-- "Examples:"
|
|
|
46 |
lemma "len_of TYPE(17) = 17" by simp
|
|
|
47 |
lemma "len_of TYPE(0) = 0" by simp
|
|
|
48 |
|
|
|
49 |
-- "not simplified:"
|
|
|
50 |
lemma "len_of TYPE('a::len0) = x"
|
|
|
51 |
oops
|
|
|
52 |
|
|
|
53 |
end
|
|
|
54 |
|