src/HOL/Datatype_Benchmark/Brackin.thy

prefer ac_simps collections over separate name bindings for add and mult

(*  Title:      HOL/Datatype_Benchmark/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