src/Benchmarks/Datatype_Benchmark/Brackin.thy
author wenzelm
Sat, 10 Nov 2018 19:01:20 +0100
changeset 69281 599b6d0d199b
parent 62286 705d4c4003ea
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
bec342db1bf4 eliminated obsolete CVS Ids;
wenzelm
parents: 16417
diff changeset
     2
58307
8172bbb37b06 use new datatypes for benchmarks
blanchet
parents: 58305
diff changeset
     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
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 7373
diff changeset
     6
theory Brackin imports Main begin
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     7
58307
8172bbb37b06 use new datatypes for benchmarks
blanchet
parents: 58305
diff changeset
     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
8172bbb37b06 use new datatypes for benchmarks
blanchet
parents: 58305
diff changeset
    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