nominal2: Nominal/Ex/SingleLet.thy@2725853f43b9 (annotated)

1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	1	theory SingleLet
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 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	atom_decl name
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	7	nominal_datatype trm =
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	8	Var "name"
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	9	\| App "trm" "trm"
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	10	\| Lam x::"name" t::"trm" bind_set x in t
d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	11	\| Let a::"assg" t::"trm" bind_set "bn a" in t
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	12	and assg =
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	13	As "name" "trm"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14	binder
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	15	bn::"assg \<Rightarrow> atom set"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	where
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	17	"bn (As x t) = {atom x}"
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	18
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	19	thm trm_assg.fv
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	20	thm trm_assg.supp
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	21	thm trm_assg.eq_iff
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	22	thm trm_assg.bn
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	23	thm trm_assg.perm
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	24	thm trm_assg.induct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	25	thm trm_assg.inducts
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	26	thm trm_assg.distinct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	27	ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	28	thm trm_assg.fv[simplified trm_assg.supp(1-2)]
d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	29
d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	30	declare permute_trm_raw_permute_assg_raw.simps[eqvt]
d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	31	declare alpha_gen_eqvt[eqvt]
2064 2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	32
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	33	equivariance alpha_trm_raw
2064 2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	34
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35
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>
	Wed, 05 May 2010 10:24:54 +0100 (2010-05-05)
changeset 2064	2725853f43b9
parent 2028	15c5a2926622
child 2104	2205b572bc9b
permissions	-rw-r--r--