theory TestMorePerm
imports "../Parser"
begin

text {* 
  "Weirdo" example from Peter Sewell's bestiary. 

  In case of deep binders, it is not coverd by our 
  approach of defining alpha-equivalence with a 
  single permutation.

  Check whether it works with shallow binders as
  defined below.

*}
ML {* val _ = cheat_equivp := true *}

atom_decl name

nominal_datatype foo =
  Foo_var "name"
| Foo_pair "foo" "foo" 
| Foo x::"name" y::"name" p1::"foo" p2::"foo" p3::"foo"
    bind x in p1, bind x in p2, 
    bind y in p2, bind y in p3

thm alpha_foo_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]


end