(* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy
A couple 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