Nominal/Ex/TestMorePerm.thy
author Christian Urban <urbanc@in.tum.de>
Thu, 08 Apr 2010 11:50:30 +0200
changeset 1793 33f7201a0239
parent 1792 c29a139410d2
child 2082 0854af516f14
permissions -rw-r--r--
check whether the "weirdo" example from the binding bestiary works with shallow binders

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