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+ −
+ −
+ −
+ −