nominal2: Nominal/Ex/Ex2.thy@f659ce282610 (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 *}
2309 13f20fe02ff3 fixed problem with eqvt proofs Christian Urban <urbanc@in.tum.de> parents: 2301 diff changeset	6	declare [[STEPS = 9]]
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8	atom_decl name
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9
2026 7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	10	nominal_datatype trm =
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11	Var "name"
2026 7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	12	\| App "trm" "trm"
7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	13	\| 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	14	\| 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	15	and pat =
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	PN
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	\| PS "name"
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	\| PD "name" "name"
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	binder
2026 7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	20	f::"pat \<Rightarrow> atom set"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	where
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	"f PN = {}"
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	\| "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	24	\| "f (PS x) = {atom x}"
2300 9fb315392493 added FSet to the correct paper Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	25
9fb315392493 added FSet to the correct paper Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	26	thm fv_trm_raw.simps[no_vars] fv_pat_raw.simps[no_vars] fv_f_raw.simps[no_vars] f_raw.simps[no_vars]
9fb315392493 added FSet to the correct paper Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	27	thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]
9fb315392493 added FSet to the correct paper Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	28
9fb315392493 added FSet to the correct paper Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	29
9fb315392493 added FSet to the correct paper Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	30
2177 9b566c5dc1f5 overlapping deep binders proof Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	31
2026 7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	32	thm trm_pat.bn
7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	33	thm trm_pat.perm
7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	34	thm trm_pat.induct
7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	35	thm trm_pat.distinct
7f504136149b Another example where only alpha_eqvt fails. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	36	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	37
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2030 diff changeset	38
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39	end
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42

author	Christian Urban <urbanc@in.tum.de>
	Wed, 30 Jun 2010 16:56:37 +0100 (2010-06-30)
changeset 2341	f659ce282610
parent 2311	4da5c5c29009
permissions	-rw-r--r--