| author | berghofe |
| Fri, 16 Jul 1999 12:02:06 +0200 | |
| changeset 7013 | 8a7fb425e04a |
| child 7373 | 776d888472aa |
| permissions | -rw-r--r-- |
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
1 |
(* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
3 |
*) |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
4 |
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
5 |
Brackin = Main + |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
6 |
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
7 |
(* ------------------------------------------------------------------------- *) |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
8 |
(* A couple from Steve Brackin's work. *) |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
9 |
(* ------------------------------------------------------------------------- *) |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
10 |
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
11 |
datatype T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 | |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
12 |
X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 | |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
13 |
X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 | |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
14 |
X32 | X33 | X34 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
15 |
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
16 |
datatype |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
17 |
('a, 'b, 'c) TY1 =
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
18 |
NoF__ |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
19 |
| Fk__ 'a (('a, 'b, 'c) TY2)
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
20 |
and |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
21 |
('a, 'b, 'c) TY2 =
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
22 |
Ta__ bool |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
23 |
| Td__ bool |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
24 |
| Tf__ (('a, 'b, 'c) TY1)
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
25 |
| Tk__ bool |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
26 |
| Tp__ bool |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
27 |
| App__ 'a (('a, 'b, 'c) TY1) (('a, 'b, 'c) TY2) (('a, 'b, 'c) TY3)
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
28 |
| Pair__ (('a, 'b, 'c) TY2) (('a, 'b, 'c) TY2)
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
29 |
and |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
30 |
('a, 'b, 'c) TY3 =
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
31 |
NoS__ |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
32 |
| Fresh__ (('a, 'b, 'c) TY2)
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
33 |
| Trustworthy__ 'a |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
34 |
| PrivateKey__ 'a 'b 'c |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
35 |
| PublicKey__ 'a 'b 'c |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
36 |
| Conveyed__ 'a (('a, 'b, 'c) TY2)
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
37 |
| Possesses__ 'a (('a, 'b, 'c) TY2)
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
38 |
| Received__ 'a (('a, 'b, 'c) TY2)
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
39 |
| Recognizes__ 'a (('a, 'b, 'c) TY2)
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
40 |
| NeverMalFromSelf__ 'a 'b (('a, 'b, 'c) TY2)
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
41 |
| Sends__ 'a (('a, 'b, 'c) TY2) 'b
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
42 |
| SharedSecret__ 'a (('a, 'b, 'c) TY2) 'b
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
43 |
| Believes__ 'a (('a, 'b, 'c) TY3)
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
44 |
| And__ (('a, 'b, 'c) TY3) (('a, 'b, 'c) TY3)
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
45 |
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
46 |
end |