src/Benchmarks/Datatype_Benchmark/Brackin.thy
 author wenzelm Mon, 22 May 2017 00:23:25 +0200 changeset 65897 94b0da1b242e parent 62286 705d4c4003ea permissions -rw-r--r--
back to scala-2.11.8 due to apparent non-termination of HOL-Codegenerator_Test;
```
(*  Title:      Benchmarks/Datatype_Benchmark/Brackin.thy

A couple of datatypes from Steve Brackin's work.
*)

theory Brackin imports Main begin

datatype T =
X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
X32 | X33 | X34

datatype ('a, 'b, 'c) TY1 =
NoF
| Fk 'a "('a, 'b, 'c) TY2"
and ('a, 'b, 'c) TY2 =
Ta bool
| Td bool
| Tf "('a, 'b, 'c) TY1"
| Tk bool
| Tp bool
| App 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
| Pair "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
and ('a, 'b, 'c) TY3 =
NoS
| Fresh "('a, 'b, 'c) TY2"
| Trustworthy 'a
| PrivateKey 'a 'b 'c
| PublicKey 'a 'b 'c
| Conveyed 'a "('a, 'b, 'c) TY2"
| Possesses 'a "('a, 'b, 'c) TY2"
| Received 'a "('a, 'b, 'c) TY2"
| Recognizes 'a "('a, 'b, 'c) TY2"
| NeverMalFromSelf 'a 'b "('a, 'b, 'c) TY2"
| Sends 'a "('a, 'b, 'c) TY2" 'b
| SharedSecret 'a "('a, 'b, 'c) TY2" 'b
| Believes 'a "('a, 'b, 'c) TY3"
| And "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"

end
```