1 (* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy |
|
2 |
|
3 A couple from Steve Brackin's work. |
|
4 *) |
|
5 |
|
6 theory Brackin imports Main begin |
|
7 |
|
8 datatype T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 | |
|
9 X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 | |
|
10 X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 | |
|
11 X32 | X33 | X34 |
|
12 |
|
13 datatype |
|
14 ('a, 'b, 'c) TY1 = |
|
15 NoF__ |
|
16 | Fk__ 'a "('a, 'b, 'c) TY2" |
|
17 and |
|
18 ('a, 'b, 'c) TY2 = |
|
19 Ta__ bool |
|
20 | Td__ bool |
|
21 | Tf__ "('a, 'b, 'c) TY1" |
|
22 | Tk__ bool |
|
23 | Tp__ bool |
|
24 | App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3" |
|
25 | Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2" |
|
26 and |
|
27 ('a, 'b, 'c) TY3 = |
|
28 NoS__ |
|
29 | Fresh__ "('a, 'b, 'c) TY2" |
|
30 | Trustworthy__ 'a |
|
31 | PrivateKey__ 'a 'b 'c |
|
32 | PublicKey__ 'a 'b 'c |
|
33 | Conveyed__ 'a "('a, 'b, 'c) TY2" |
|
34 | Possesses__ 'a "('a, 'b, 'c) TY2" |
|
35 | Received__ 'a "('a, 'b, 'c) TY2" |
|
36 | Recognizes__ 'a "('a, 'b, 'c) TY2" |
|
37 | NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2" |
|
38 | Sends__ 'a "('a, 'b, 'c) TY2" 'b |
|
39 | SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b |
|
40 | Believes__ 'a "('a, 'b, 'c) TY3" |
|
41 | And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3" |
|
42 |
|
43 end |
|