nominal2: Nominal/Ex/SingleLetFoo.thy@5111dadd1162 (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
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	declare [[STEPS = 4]]
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	(* alpha does not work for this type *)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	8
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	atom_decl name
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	10
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	nominal_datatype trm =
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	Var "name"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	\| App "trm" "trm"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	\| 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	15	\| 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	16	\| 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	17	\| Foo2 x::name a::"assg" t::"trm" bind_set x "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	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
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	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	26	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	27
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	(* there is something wrong with the free variables *)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	text {*
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	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	32	*}
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	inductive
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	alpha_trm_raw and alpha_assg_raw and alpha_bn_raw
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	where
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	"name = namea \<Longrightarrow> alpha_trm_raw (Var_raw name) (Var_raw namea)"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	\| "\<lbrakk>alpha_trm_raw trm_raw1 trm_raw1a; alpha_trm_raw trm_raw2 trm_raw2a\<rbrakk>
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	\<Longrightarrow> alpha_trm_raw (App_raw trm_raw1 trm_raw2) (App_raw trm_raw1a trm_raw2a)"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	\| "\<exists>p. ({atom name}, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea}, trm_rawa) \<Longrightarrow>
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	alpha_trm_raw (Lam_raw name trm_raw) (Lam_raw namea trm_rawa)"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	\| "\<lbrakk>\<exists>p. (bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p (bn_raw assg_rawa, trm_rawa);
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	alpha_bn_raw assg_raw assg_rawa\<rbrakk>
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	\<Longrightarrow> alpha_trm_raw (Let_raw assg_raw trm_raw) (Let_raw assg_rawa trm_rawa)"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	45	\| "\<lbrakk>\<exists>p. (bn_raw assg_raw1 \<union> bn_raw ass_raw2, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	(bn_raw assg_raw1a \<union> bn_raw ass_raw2a, trm_rawa);
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	47	alpha_bn_raw assg_raw1 assg_raw1a; alpha_bn_raw assg_raw2 assg_raw2a\<rbrakk>
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	\<Longrightarrow> alpha_trm_raw (Foo1_raw assg_raw1 assg_raw2 trm_raw) (Foo1_raw assg_raw1a assg_raw2a trm_rawa)"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	49	\| "\<lbrakk>\<exists>p. ({atom name} \<union> bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	50	({atom namea} \<union> bn_raw assg_rawa, trm_rawa);
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	51	alpha_bn_raw assg_raw assg_rawa\<rbrakk>
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	52	\<Longrightarrow> alpha_trm_raw (Foo2_raw name assg_raw trm_raw) (Foo2_raw namea assg_rawa trm_rawa)"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	53
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	54	\| "\<lbrakk>name = namea; alpha_trm_raw trm_raw trm_rawa\<rbrakk>
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	55	\<Longrightarrow> alpha_assg_raw (As_raw name trm_raw) (As_raw namea trm_rawa)"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	\| "alpha_trm_raw trm_raw trm_rawa \<Longrightarrow> alpha_bn_raw (As_raw name trm_raw) (As_raw namea trm_rawa)"
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	57
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	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	59
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	60	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	61
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	62	lemma
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	63	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	64	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	65	(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	66	using assms
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	67	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	68	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	69	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	70	apply(rule conjI)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	apply(simp)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	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	73	apply(rule conjI)
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 fresh_star_def)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	75	apply(rule conjI)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	76	apply(simp)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	77	apply(rule all)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	apply(simp)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	79	unfolding flip_def
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	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	81	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	82	apply(simp)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	83	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	84	apply(auto)[2]
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	85	apply(simp)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	86	apply(rule all)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	87	apply(rule all)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	88	apply(simp)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	89	done
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	90
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	91	lemma
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	92	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	93	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	94	using assms
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	95	apply(simp add: supp_at_base)
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	96
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	97
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	98	end
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	99
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	100
5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: diff changeset	101

author	Christian Urban <urbanc@in.tum.de>
	Thu, 13 May 2010 19:06:54 +0100
changeset 2130	5111dadd1162
child 2132	d74e08799b63
permissions	-rw-r--r--