| author | haftmann |
| Fri, 01 Nov 2013 18:51:14 +0100 | |
| changeset 54230 | b1d955791529 |
| parent 51699 | 0539e75b4170 |
| child 58305 | 57752a91eec4 |
| permissions | -rw-r--r-- |
| 45860 | 1 |
(* Title: HOL/Datatype_Benchmark/Brackin.thy |
| 33695 | 2 |
|
3 |
A couple 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 |
|
|
51699
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
8 |
datatype T = |
|
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 |
|
|
51699
0539e75b4170
proper identifiers -- avoid crash of case translations;
wenzelm
parents:
45860
diff
changeset
|
14 |
datatype ('a, 'b, 'c) TY1 =
|
|
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 |