nominal2: Nominal/Ex/SingleLet.thy@d974059827ad (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
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	7	ML {* val _ = cheat_alpha_eqvt := true *}
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	8
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	9	nominal_datatype trm =
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	10	Var "name"
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	11	\| App "trm" "trm"
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	12	\| 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	13	\| 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	14	and assg =
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	15	As "name" "trm"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	binder
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	17	bn::"assg \<Rightarrow> atom set"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	where
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	19	"bn (As x t) = {atom x}"
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	20
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	21	thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	22	thm trm_assg.fv
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	23	thm trm_assg.supp
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	24	thm trm_assg.eq_iff
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	25	thm trm_assg.bn
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	26	thm trm_assg.perm
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	27	thm trm_assg.induct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	28	thm trm_assg.inducts
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	29	thm trm_assg.distinct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	30	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	31	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	32
d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	33	setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	34	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	35	declare alpha_gen_eqvt[eqvt]
d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	36	equivariance alpha_trm_raw
d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	37
1596 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	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	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Mon, 03 May 2010 14:03:30 +0200
changeset 2024	d974059827ad
parent 1911	60b5c61d3de2
child 2028	15c5a2926622
permissions	-rw-r--r--