nominal2: Nominal/Ex/SingleLetFoo.thy@231a20534950 (annotated)

2130 5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory SingleLetFoo
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports "../NewParser"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	5
2132 d74e08799b63 SingleLetFoo with everything. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2130 diff changeset	6	declare [[STEPS = 5]]
2130 5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	7
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	atom_decl name
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	nominal_datatype trm =
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	Var "name"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	\| App "trm" "trm"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	\| Lam x::"name" t::"trm" bind_set x in t
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	\| Let a::"assg" t::"trm" bind_set "bn a" in t
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	\| Foo1 a1::"assg" a2::"assg" t::"trm" bind_set "bn a1" "bn a2" in t
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	\| Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t
2133 16834a4ca1bb Proper fv/alpha for multiple compound binders Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2132 diff changeset	17
2130 5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	and assg =
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	As "name" "trm"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	binder
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	bn::"assg \<Rightarrow> atom set"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	where
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	"bn (As x t) = {atom x}"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	24
2132 d74e08799b63 SingleLetFoo with everything. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2130 diff changeset	25	thm trm_assg.distinct
d74e08799b63 SingleLetFoo with everything. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2130 diff changeset	26	thm trm_assg.eq_iff
d74e08799b63 SingleLetFoo with everything. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2130 diff changeset	27	thm trm_assg.supp
d74e08799b63 SingleLetFoo with everything. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2130 diff changeset	28	thm trm_assg.perm
2133 16834a4ca1bb Proper fv/alpha for multiple compound binders Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2132 diff changeset	29	thm trm_assg.fv[simplified trm_assg.supp(1-2),no_vars]
2132 d74e08799b63 SingleLetFoo with everything. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2130 diff changeset	30
2130 5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	thm permute_trm_raw_permute_assg_raw.simps
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars]
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	33
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	35
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	36
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	lemmas all = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	38
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	lemma test: "p \<bullet> bn_raw \<equiv> bn_raw" sorry
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	40
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	lemma
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	assumes "distinct [x,y, z, u]"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	shows "alpha_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z))
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	(Foo2_raw u (As_raw y (Var_raw z)) (Var_raw u))"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	45	using assms
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	apply(rule_tac all)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	47	apply(rule_tac x="(z \<leftrightarrow> u) + (x \<leftrightarrow> y)" in exI)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	apply(simp only: alphas)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	49	apply(rule conjI)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	50	apply(simp)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	51	apply(simp add: supp_at_base fresh_star_def)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	52	apply(rule conjI)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	53	apply(simp add: supp_at_base fresh_star_def)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	54	apply(rule conjI)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	55	apply(simp)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	apply(rule all)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	57	apply(simp)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	unfolding flip_def
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	59	apply(perm_simp add: test)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	60	unfolding flip_def[symmetric]
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	61	apply(simp)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	62	apply(subst flip_at_base_simps(3))
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	63	apply(auto)[2]
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	64	apply(simp)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	65	apply(rule all)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	66	apply(rule all)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	67	apply(simp)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	68	done
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	69
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	70	lemma
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	assumes "distinct [x,y,z,u]"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	shows "fv_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z)) = {atom z}"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	73	using assms
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	apply(simp add: supp_at_base)
2136 2fc55508a6d0 polished example Christian Urban <urbanc@in.tum.de> parents: 2133 diff changeset	75	done
2130 5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	76
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	77
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	end
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	79
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	80
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	81

author	Christian Urban <urbanc@in.tum.de>
	Mon, 07 Jun 2010 11:33:00 +0200
changeset 2213	231a20534950
parent 2136	2fc55508a6d0
permissions	-rw-r--r--