1 (* Title: HOL/Datatype_Benchmark/Brackin.thy |
|
2 |
|
3 A couple of datatypes from Steve Brackin's work. |
|
4 *) |
|
5 |
|
6 theory Brackin imports Main begin |
|
7 |
|
8 datatype T = |
|
9 X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 | |
|
10 X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 | |
|
11 X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 | |
|
12 X32 | X33 | X34 |
|
13 |
|
14 datatype ('a, 'b, 'c) TY1 = |
|
15 NoF |
|
16 | Fk 'a "('a, 'b, 'c) TY2" |
|
17 and ('a, 'b, 'c) TY2 = |
|
18 Ta bool |
|
19 | Td bool |
|
20 | Tf "('a, 'b, 'c) TY1" |
|
21 | Tk bool |
|
22 | Tp bool |
|
23 | App 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3" |
|
24 | Pair "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2" |
|
25 and ('a, 'b, 'c) TY3 = |
|
26 NoS |
|
27 | Fresh "('a, 'b, 'c) TY2" |
|
28 | Trustworthy 'a |
|
29 | PrivateKey 'a 'b 'c |
|
30 | PublicKey 'a 'b 'c |
|
31 | Conveyed 'a "('a, 'b, 'c) TY2" |
|
32 | Possesses 'a "('a, 'b, 'c) TY2" |
|
33 | Received 'a "('a, 'b, 'c) TY2" |
|
34 | Recognizes 'a "('a, 'b, 'c) TY2" |
|
35 | NeverMalFromSelf 'a 'b "('a, 'b, 'c) TY2" |
|
36 | Sends 'a "('a, 'b, 'c) TY2" 'b |
|
37 | SharedSecret 'a "('a, 'b, 'c) TY2" 'b |
|
38 | Believes 'a "('a, 'b, 'c) TY3" |
|
39 | And "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3" |
|
40 |
|
41 end |
|