src/Benchmarks/Datatype_Benchmark/Brackin.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (22 months ago)
changeset 66924 b4d4027f743b
parent 62286 705d4c4003ea
permissions -rw-r--r--
more permissive;
wenzelm@62286
     1
(*  Title:      Benchmarks/Datatype_Benchmark/Brackin.thy
wenzelm@33695
     2
blanchet@58307
     3
A couple of datatypes from Steve Brackin's work.
berghofe@7013
     4
*)
berghofe@7013
     5
haftmann@16417
     6
theory Brackin imports Main begin
berghofe@7013
     7
blanchet@58307
     8
datatype T =
wenzelm@51699
     9
    X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
wenzelm@51699
    10
    X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
wenzelm@51699
    11
    X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
wenzelm@51699
    12
    X32 | X33 | X34
berghofe@7013
    13
blanchet@58307
    14
datatype ('a, 'b, 'c) TY1 =
wenzelm@51699
    15
      NoF
wenzelm@51699
    16
    | Fk 'a "('a, 'b, 'c) TY2"
wenzelm@51699
    17
and ('a, 'b, 'c) TY2 =
wenzelm@51699
    18
      Ta bool
wenzelm@51699
    19
    | Td bool
wenzelm@51699
    20
    | Tf "('a, 'b, 'c) TY1"
wenzelm@51699
    21
    | Tk bool
wenzelm@51699
    22
    | Tp bool
wenzelm@51699
    23
    | App 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
wenzelm@51699
    24
    | Pair "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
wenzelm@51699
    25
and ('a, 'b, 'c) TY3 =
wenzelm@51699
    26
      NoS
wenzelm@51699
    27
    | Fresh "('a, 'b, 'c) TY2"
wenzelm@51699
    28
    | Trustworthy 'a
wenzelm@51699
    29
    | PrivateKey 'a 'b 'c
wenzelm@51699
    30
    | PublicKey 'a 'b 'c
wenzelm@51699
    31
    | Conveyed 'a "('a, 'b, 'c) TY2"
wenzelm@51699
    32
    | Possesses 'a "('a, 'b, 'c) TY2"
wenzelm@51699
    33
    | Received 'a "('a, 'b, 'c) TY2"
wenzelm@51699
    34
    | Recognizes 'a "('a, 'b, 'c) TY2"
wenzelm@51699
    35
    | NeverMalFromSelf 'a 'b "('a, 'b, 'c) TY2"
wenzelm@51699
    36
    | Sends 'a "('a, 'b, 'c) TY2" 'b
wenzelm@51699
    37
    | SharedSecret 'a "('a, 'b, 'c) TY2" 'b
wenzelm@51699
    38
    | Believes 'a "('a, 'b, 'c) TY3"
wenzelm@51699
    39
    | And "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
berghofe@7013
    40
berghofe@7013
    41
end