nominal2: Nominal/Ex/Ex2.thy@20be95dce643 (annotated)

1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory Ex2
2026 7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	2	imports "../NewParser"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	text {* example 2 *}
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	atom_decl name
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8
2026 7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	9	nominal_datatype trm =
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	Var "name"
2026 7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	11	\| App "trm" "trm"
7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	12	\| Lam x::"name" t::"trm" bind_set x in t
7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	13	\| Let p::"pat" "trm" t::"trm" bind_set "f p" in t
7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	14	and pat =
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	PN
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	\| PS "name"
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	\| PD "name" "name"
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	binder
2026 7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	19	f::"pat \<Rightarrow> atom set"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	where
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	"f PN = {}"
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	\| "f (PD x y) = {atom x, atom y}"
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	\| "f (PS x) = {atom x}"
2026 7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	24	thm trm_pat.bn
7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	25	thm trm_pat.perm
7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	26	thm trm_pat.induct
7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	27	thm trm_pat.distinct
7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	28	thm trm_pat.fv[simplified trm_pat.supp(1-2)]
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	end
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33

author	Christian Urban <urbanc@in.tum.de>
	Tue, 04 May 2010 14:38:07 +0100 (2010-05-04)
changeset 2048	20be95dce643
parent 2030	43d7612f1429
child 2082	0854af516f14
permissions	-rw-r--r--