1(*  Title:      Benchmarks/Datatype_Benchmark/Brackin.thy
2
3A couple of datatypes from Steve Brackin's work.
4*)
5
6theory Brackin imports Main begin
7
8datatype 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
14datatype ('a, 'b, 'c) TY1 =
15      NoF
16    | Fk 'a "('a, 'b, 'c) TY2"
17and ('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"
25and ('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
41end
42