nominal2: Nominal/Ex/SingleLet.thy@c6db12ddb60c (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
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	7	ML {* print_depth 50 *}
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 2296 diff changeset	8	declare [[STEPS = 8]]
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	9
2294 72ad4e766acf properly exported bn_descr Christian Urban <urbanc@in.tum.de> parents: 2293 diff changeset	10
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	11	nominal_datatype trm =
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	12	Var "name"
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	13	\| App "trm" "trm"
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	14	\| 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	15	\| 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	16	\| 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	17	\| 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	18	and assg =
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	19	As "name" "trm"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	binder
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	21	bn::"assg \<Rightarrow> atom set"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	where
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	23	"bn (As x t) = {atom x}"
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	24
2296 45a69c9cc4cc alpha works now Christian Urban <urbanc@in.tum.de> parents: 2295 diff changeset	25
2302 c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	26	thm permute_trm_raw_permute_assg_raw.simps[no_vars]
2293 aecebd5ed424 hving a working fv-definition without the export Christian Urban <urbanc@in.tum.de> parents: 2292 diff changeset	27	thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars]
2295 8aff3f3ce47f started to work on alpha Christian Urban <urbanc@in.tum.de> parents: 2294 diff changeset	28	thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
8aff3f3ce47f started to work on alpha Christian Urban <urbanc@in.tum.de> parents: 2294 diff changeset	29
2302 c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	30	ML {* val {inducts, ... } = Function.get_info @{context} @{term "fv_trm_raw"}*}
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	31	ML {* Rule_Cases.strict_mutual_rule @{context} (the inducts) *}
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	32
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	33	(*
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	34	lemma empty_eqvt[eqvt]:
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	35	shows "p \<bullet> {} = {}"
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	36	unfolding empty_def
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	37	by (perm_simp) (rule refl)
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	38	*)
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	39	lemma
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	40	"(p \<bullet> {}) = {}"
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	41	thm eqvts_raw
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	42	thm eqvts
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	43	apply(perm_strict_simp)
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	44
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	45
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	46	lemma
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	47	shows "p1 \<bullet> fv_trm_raw trm_raw = fv_trm_raw (p1 \<bullet> trm_raw)"
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	48	and "p1 \<bullet> fv_assg_raw assg_raw = fv_assg_raw (p1 \<bullet> assg_raw)"
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	49	and "p1 \<bullet> fv_bn_raw assg_raw = fv_bn_raw (p1 \<bullet> assg_raw)"
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	50	apply(induct trm_raw and assg_raw and assg_raw rule: fv_trm_raw_fv_assg_raw_fv_bn_raw.induct)
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	51	apply(simp_all)
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	52	apply(perm_simp)
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	53	apply(rule refl)
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	54	apply(perm_simp)
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	55	apply(rule refl)
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	56	apply(perm_simp)
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	57	apply(rule refl)
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	58	apply(simp add: fv_trm_raw.simps)
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	59
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	60
2296 45a69c9cc4cc alpha works now Christian Urban <urbanc@in.tum.de> parents: 2295 diff changeset	61
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	62	ML {* Inductive.the_inductive *}
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	63	thm trm_assg.fv
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	64	thm trm_assg.supp
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	65	thm trm_assg.eq_iff
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	66	thm trm_assg.bn
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	67	thm trm_assg.perm
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	68	thm trm_assg.induct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	69	thm trm_assg.inducts
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	70	thm trm_assg.distinct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	71	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	72
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	73	(* TEMPORARY
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	74	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	75	*)
2064 2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	76
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	77
2146 a2f70c09e77d minor tuning Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	78
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	79	end
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	80
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	81
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	82

author	Christian Urban <urbanc@in.tum.de>
	Thu, 27 May 2010 18:37:52 +0200
changeset 2302	c6db12ddb60c
parent 2299	09bbed4f21d6
child 2303	c785fff02a8f
permissions	-rw-r--r--