theory Classical
imports "../Nominal2"
begin

(* example from Urban's PhD *)

atom_decl name
atom_decl coname

nominal_datatype trm =
   Ax "name" "coname"
|  Cut n::"coname" t1::"trm" c::"coname" t2::"trm"             bind n in t1, bind c in t2
|  AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2
|  AndL1 n::"name" t::"trm" "name"                             bind n in t
|  AndL2 n::"name" t::"trm" "name"                             bind n in t
|  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"       bind c in t1, bind n in t2
|  ImpR c::"coname" n::"name" t::"trm" "coname"                bind n c in t

thm trm.distinct
thm trm.induct
thm trm.exhaust
thm trm.strong_exhaust
thm trm.strong_exhaust[simplified]
thm trm.fv_defs
thm trm.bn_defs
thm trm.perm_simps
thm trm.eq_iff
thm trm.fv_bn_eqvt
thm trm.size_eqvt
thm trm.supp
thm trm.supp[simplified]




end