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

1595 aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory TestMorePerm
1773 c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1595 diff changeset	2	imports "../Parser"
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
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	8	In case of deep binders, it is not coverd by our
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	9	approach of defining alpha-equivalence with a
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	10	single permutation.
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	Check whether it works with shallow binders as
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	defined below.
1595 aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14
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	15	*}
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	16	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	17
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	18	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	19
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	20	nominal_datatype foo =
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	21	Foo_var "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	22	\| Foo_pair "foo" "foo"
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	23	\| Foo x::"name" y::"name" p1::"foo" p2::"foo" p3::"foo"
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	24	bind x in p1, bind x in p2,
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	25	bind y in p2, bind y in p3
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	26
33f7201a0239 check whether the "weirdo" example from the binding bestiary works with shallow binders Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	27	thm alpha_foo_raw.intros[no_vars]
1595 aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29	thm permute_weird_raw.simps[no_vars]
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	thm alpha_weird_raw.intros[no_vars]
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	thm fv_weird_raw.simps[no_vars]
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32
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	end
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36
aeed597d2043 Move examples which create more permutations out Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Tue, 27 Apr 2010 14:29:59 +0200
changeset 1958	e2e19188576e
parent 1793	33f7201a0239
child 2082	0854af516f14
permissions	-rw-r--r--