nominal2: Nominal/Ex/LetPat.thy@ac7dff1194e8 (annotated)

2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	1	theory LetPat
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	2	imports "../Nominal2"
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
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	5	declare [[STEPS = 100]]
1596 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"
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	12	\| Lam x::"name" t::"trm" bind (set) x in t
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	13	\| Let p::"pat" "trm" t::"trm" bind (set) "f p" in t
2026 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}"
2300 9fb315392493 added FSet to the correct paper Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	24
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	25	thm trm_pat.distinct
2026 7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	26	thm trm_pat.induct
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	27	thm trm_pat.exhaust
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	28	thm trm_pat.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	29	thm trm_pat.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	30	thm trm_pat.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	31	thm trm_pat.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	32	thm trm_pat.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	33	thm trm_pat.size_eqvt
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2030 diff changeset	35
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36	end
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39

author	Christian Urban <urbanc@in.tum.de>
	Mon, 20 Sep 2010 21:52:45 +0800
changeset 2480	ac7dff1194e8
parent 2454	9ffee4eb1ae1
child 2648	5d9724ad543d
permissions	-rw-r--r--