1(* Title: Benchmarks/Datatype_Benchmark/Brackin.thy 2 3A couple of datatypes from Steve Brackin's work. 4*) 5 6theory Brackin imports Main begin 7 8datatype 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 14datatype ('a, 'b, 'c) TY1 = 15 NoF 16 | Fk 'a "('a, 'b, 'c) TY2" 17and ('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" 25and ('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 41end 42