src/Benchmarks/Datatype_Benchmark/Brackin.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (23 months ago)
changeset 66924 b4d4027f743b
parent 62286 705d4c4003ea
permissions -rw-r--r--
more permissive;
     1 (*  Title:      Benchmarks/Datatype_Benchmark/Brackin.thy
     2 
     3 A couple of datatypes from Steve Brackin's work.
     4 *)
     5 
     6 theory Brackin imports Main begin
     7 
     8 datatype 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 
    14 datatype ('a, 'b, 'c) TY1 =
    15       NoF
    16     | Fk 'a "('a, 'b, 'c) TY2"
    17 and ('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"
    25 and ('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 
    41 end