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