theory TestMorePerm
imports "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 coname

nominal_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 t

thm phd.fv
thm phd.eq_iff
thm phd.bn
thm phd.perm
thm phd.induct
thm phd.distinct
thm 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