| author | wenzelm |
| Sun, 13 Dec 2020 23:11:41 +0100 | |
| changeset 72907 | 3883f536d84d |
| parent 62286 | 705d4c4003ea |
| permissions | -rw-r--r-- |
|
62286
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
wenzelm
parents:
58330
diff
changeset
|
1 |
(* Title: Benchmarks/Datatype_Benchmark/Brackin.thy |
| 33695 | 2 |
|
| 58307 | 3 |
A couple of datatypes from Steve Brackin's work. |
|
7013
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 |
|
| 16417 | 6 |
theory Brackin imports Main begin |
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
7 |
|
| 58307 | 8 |
datatype T = |
|
51699
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
9 |
X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 | |
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
10 |
X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 | |
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
11 |
X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 | |
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
12 |
X32 | X33 | X34 |
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
13 |
|
| 58307 | 14 |
datatype ('a, 'b, 'c) TY1 =
|
|
51699
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
15 |
NoF |
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
16 |
| Fk 'a "('a, 'b, 'c) TY2"
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
17 |
and ('a, 'b, 'c) TY2 =
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
18 |
Ta bool |
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
19 |
| Td bool |
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
20 |
| Tf "('a, 'b, 'c) TY1"
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
21 |
| Tk bool |
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
22 |
| Tp bool |
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
23 |
| App 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
24 |
| Pair "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
25 |
and ('a, 'b, 'c) TY3 =
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
26 |
NoS |
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
27 |
| Fresh "('a, 'b, 'c) TY2"
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
28 |
| Trustworthy 'a |
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
29 |
| PrivateKey 'a 'b 'c |
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
30 |
| PublicKey 'a 'b 'c |
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
31 |
| Conveyed 'a "('a, 'b, 'c) TY2"
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
32 |
| Possesses 'a "('a, 'b, 'c) TY2"
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
33 |
| Received 'a "('a, 'b, 'c) TY2"
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
34 |
| Recognizes 'a "('a, 'b, 'c) TY2"
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
35 |
| NeverMalFromSelf 'a 'b "('a, 'b, 'c) TY2"
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
36 |
| Sends 'a "('a, 'b, 'c) TY2" 'b
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
37 |
| SharedSecret 'a "('a, 'b, 'c) TY2" 'b
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
38 |
| Believes 'a "('a, 'b, 'c) TY3"
|
|
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
39 |
| And "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
|
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
40 |
|
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
41 |
end |