theory TestMorePermimports "Parser"begin(* Since there are more permutations, we do not know how to prove equivalence (it is probably not true with the way alpha is defined now) so *)ML {* val _ = cheat_equivp := true *}atom_decl name(* example from my PHD *)atom_decl conamenominal_datatype phd = Ax "name" "coname"| Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2| AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2| AndL1 n::"name" t::"phd" "name" bind n in t| AndL2 n::"name" t::"phd" "name" bind n in t| ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2| ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in tthm phd.fvthm phd.eq_iffthm phd.bnthm phd.permthm phd.inductthm phd.distinctthm phd.fv[simplified phd.supp]text {* weirdo example from Peter Sewell's bestiary *}nominal_datatype weird = WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" bind x in p1, bind x in p2, bind y in p2, bind y in p3| WV "name"| WP "weird" "weird"thm permute_weird_raw.simps[no_vars]thm alpha_weird_raw.intros[no_vars]thm fv_weird_raw.simps[no_vars]end