Nominal/Ex/TestMorePerm.thy
author Christian Urban <urbanc@in.tum.de>
Wed, 12 May 2010 16:33:25 +0100
changeset 2118 0e52851acac4
parent 2105 e25b0fff0dd2
permissions -rw-r--r--
moved the data-transformation into the parser

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]

equivariance alpha_weird_raw


end