theory TestMorePerm+ −
imports "../NewParser"+ −
begin+ −
+ −
text {* + −
"Weirdo" example from Peter Sewell's bestiary. + −
+ −
This example is not covered by our binding + −
specification.+ −
+ −
*}+ −
ML {* val _ = cheat_equivp := true *}+ −
+ −
atom_decl name+ −
+ −
nominal_datatype weird =+ −
Foo_var "name"+ −
| Foo_pair "weird" "weird" + −
| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"+ −
bind x in p1 p2, + −
bind y in p2 p3+ −
+ −
thm alpha_weird_raw.intros[no_vars]+ −
+ −
thm permute_weird_raw.simps[no_vars]+ −
thm alpha_weird_raw.intros[no_vars]+ −
thm fv_weird_raw.simps[no_vars]+ −
+ −
declare permute_weird_raw.simps[eqvt]+ −
declare alpha_gen_eqvt[eqvt]+ −
equivariance alpha_weird_raw+ −
+ −
+ −
end+ −
+ −
+ −
+ −