--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/TestMorePerm.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,49 @@
+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
+
+
+