nominal2: Nominal/Ex/SingleLet.thy@387fcbd33820 (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
2306 86c977b4a9bb equivariance done Christian Urban <urbanc@in.tum.de> parents: 2305 diff changeset	7	declare [[STEPS = 9]]
2288 3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 2146 diff changeset	8
2294 72ad4e766acf properly exported bn_descr Christian Urban <urbanc@in.tum.de> parents: 2293 diff changeset	9
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	10	nominal_datatype trm =
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	11	Var "name"
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	12	\| App "trm" "trm"
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	13	\| 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	14	\| Let a::"assg" t::"trm" bind_set "bn a" in t
2296 45a69c9cc4cc alpha works now Christian Urban <urbanc@in.tum.de> parents: 2295 diff changeset	15	\| Foo x::"name" y::"name" t::"trm" bind_set x in y t
45a69c9cc4cc alpha works now Christian Urban <urbanc@in.tum.de> parents: 2295 diff changeset	16	\| Bar x::"name" y::"name" t::"trm" bind y x in t x y
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	17	and assg =
2308 387fcbd33820 fixed problem with bn_info Christian Urban <urbanc@in.tum.de> parents: 2306 diff changeset	18	As "name" "name" "trm" "name"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	binder
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	20	bn::"assg \<Rightarrow> atom set"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	where
2308 387fcbd33820 fixed problem with bn_info Christian Urban <urbanc@in.tum.de> parents: 2306 diff changeset	22	"bn (As x y t z) = {atom x}"
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	23
2107 5686d83db1f9 ingnored parameters in equivariance; added a proper interface to be called from ML Christian Urban <urbanc@in.tum.de> parents: 2106 diff changeset	24	ML {* Inductive.the_inductive *}
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	25	thm trm_assg.fv
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	26	thm trm_assg.supp
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	27	thm trm_assg.eq_iff
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	28	thm trm_assg.bn
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	29	thm trm_assg.perm
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	30	thm trm_assg.induct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	31	thm trm_assg.inducts
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	32	thm trm_assg.distinct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	33	ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
2288 3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 2146 diff changeset	34
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 2146 diff changeset	35	(* TEMPORARY
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	36	thm trm_assg.fv[simplified trm_assg.supp(1-2)]
2288 3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 2146 diff changeset	37	*)
2064 2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 2028 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, 02 Jun 2010 11:37:51 +0200
changeset 2308	387fcbd33820
parent 2306	86c977b4a9bb
child 2311	4da5c5c29009
permissions	-rw-r--r--