nominal2: Nominal/Ex/TestMorePerm.thy@118a0ca16381 (annotated)

1595 aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory TestMorePerm
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1793 diff changeset	2	imports "../NewParser"
1595 aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
1793 33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	5	text {*
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	6	"Weirdo" example from Peter Sewell's bestiary.
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	7
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1793 diff changeset	8	This example is not covered by our binding
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1793 diff changeset	9	specification.
1595 aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10
1793 33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	11	*}
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	12	ML {* val _ = cheat_equivp := true *}
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	13
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	14	atom_decl name
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	15
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1793 diff changeset	16	nominal_datatype weird =
1793 33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	17	Foo_var "name"
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1793 diff changeset	18	\| Foo_pair "weird" "weird"
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1793 diff changeset	19	\| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1793 diff changeset	20	bind x in p1 p2,
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1793 diff changeset	21	bind y in p2 p3
1793 33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	22
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1793 diff changeset	23	thm alpha_weird_raw.intros[no_vars]
1595 aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25	thm permute_weird_raw.simps[no_vars]
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26	thm alpha_weird_raw.intros[no_vars]
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	thm fv_weird_raw.simps[no_vars]
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1793 diff changeset	29	equivariance alpha_weird_raw
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1793 diff changeset	30
1595 aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32	end
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35

author	Christian Urban <urbanc@in.tum.de>
	Tue, 01 Jun 2010 15:46:07 +0200 (2010-06-01)
changeset 2307	118a0ca16381
parent 2105	e25b0fff0dd2
permissions	-rw-r--r--