nominal2: Nominal/Ex/Ex4.thy@b151399bd2c3 (annotated)

2126 79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Ex4
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports "../NewParser"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
2145 f89773ab0685 Ex4 does work, and I don't see the difference between the alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2130 diff changeset	5	declare [[STEPS = 5]]
2126 79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	atom_decl name
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	8
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	nominal_datatype trm =
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	Var "name"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	\| App "trm" "trm"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	\| Lam x::"name" t::"trm" bind_set x in t
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	\| Let p::"pat" "trm" t::"trm" bind_set "f p" in t
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	\| Foo1 p::"pat" q::"pat" t::"trm" bind_set "f p" "f q" in t
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	\| Foo2 x::"name" p::"pat" t::"trm" bind_set x "f p" in t
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	and pat =
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	PN
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	\| PS "name"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	\| PD "pat" "pat"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	binder
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	f::"pat \<Rightarrow> atom set"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	where
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	"f PN = {}"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	\| "f (PS x) = {atom x}"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	\| "f (PD p1 p2) = (f p1) \<union> (f p2)"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	26
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	thm permute_trm_raw_permute_pat_raw.simps
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	thm fv_trm_raw.simps fv_pat_raw.simps fv_f_raw.simps
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
2145 f89773ab0685 Ex4 does work, and I don't see the difference between the alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2130 diff changeset	30	thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]
2126 79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	31
2145 f89773ab0685 Ex4 does work, and I don't see the difference between the alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2130 diff changeset	32	(*
2126 79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	inductive
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	alpha_trm_raw and alpha_pat_raw and alpha_f_raw
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	where
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	(* alpha_trm_raw *)
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	"name = namea \<Longrightarrow> alpha_trm_raw (Var_raw name) (Var_raw namea)"
79d2fc006098 added an example which goes outside our current speciifcation 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>
79d2fc006098 added an example which goes outside our current speciifcation 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)"
79d2fc006098 added an example which goes outside our current speciifcation 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>
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	alpha_trm_raw (Lam_raw name trm_raw) (Lam_raw namea trm_rawa)"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	\| "\<lbrakk>\<exists>p. (f_raw pat_raw, trm_raw2) \<approx>gen alpha_trm_raw fv_trm_raw p (f_raw pat_rawa, trm_raw2a);
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	alpha_f_raw pat_raw pat_rawa; alpha_trm_raw trm_raw1 trm_raw1a\<rbrakk>
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	\<Longrightarrow> alpha_trm_raw (Let_raw pat_raw trm_raw1 trm_raw2) (Let_raw pat_rawa trm_raw1a trm_raw2a)"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	45	\| "\<lbrakk>\<exists>p. (f_raw pat_raw1 \<union> f_raw pat_raw2, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p (f_raw pat_raw1a \<union> f_raw pat_raw2a, trm_rawa);
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk>
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	47	\<Longrightarrow> alpha_trm_raw (Foo1_raw pat_raw1 pat_raw2 trm_raw) (Foo1_raw pat_raw1a pat_raw2a trm_rawa)"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	\| "\<lbrakk>\<exists>p. ({atom name} \<union> f_raw pat_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea} \<union> f_raw pat_rawa, trm_rawa);
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	49	alpha_f_raw pat_raw pat_rawa\<rbrakk>
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	50	\<Longrightarrow> alpha_trm_raw (Foo2_raw name pat_raw trm_raw) (Foo2_raw namea pat_rawa trm_rawa)"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	51
2130 5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: 2126 diff changeset	52	(* alpha_pat_raw *)
2126 79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	53	\| "alpha_pat_raw PN_raw PN_raw"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	54	\| "name = namea \<Longrightarrow> alpha_pat_raw (PS_raw name) (PS_raw namea)"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	55	\| "\<lbrakk>alpha_pat_raw pat_raw1 pat_raw1a; alpha_pat_raw pat_raw2 pat_raw2a\<rbrakk>
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	\<Longrightarrow> alpha_pat_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	57
2130 5111dadd1162 added a more instructive example - has some problems with fv though Christian Urban <urbanc@in.tum.de> parents: 2126 diff changeset	58	(* alpha_f_raw *)
2126 79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	59	\| "alpha_f_raw PN_raw PN_raw"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	60	\| "alpha_f_raw (PS_raw name) (PS_raw namea)"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	61	\| "\<lbrakk>alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk>
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	62	\<Longrightarrow> alpha_f_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)"
2145 f89773ab0685 Ex4 does work, and I don't see the difference between the alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2130 diff changeset	63	*)
2126 79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	64
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	65	lemmas all = alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	66
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	67	lemma
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	68	shows "alpha_trm_raw (Foo2_raw x (PS_raw x) (Var_raw x))
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	69	(Foo2_raw y (PS_raw y) (Var_raw y))"
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	70	apply(rule all)
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	apply(rule_tac x="(atom x \<rightleftharpoons> atom y)" in exI)
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	apply(simp add: alphas)
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	73	apply(simp add: supp_at_base fresh_star_def)
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	apply(rule conjI)
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	75	apply(rule all)
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	76	apply(simp)
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	77	apply(perm_simp)
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	apply(simp)
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	79	apply(rule all)
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	done
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	81
2145 f89773ab0685 Ex4 does work, and I don't see the difference between the alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2130 diff changeset	82
2126 79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	83
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	84	end
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	85
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	86
79d2fc006098 added an example which goes outside our current speciifcation Christian Urban <urbanc@in.tum.de> parents: diff changeset	87

author	Christian Urban <urbanc@in.tum.de>
	Sun, 27 Jun 2010 21:41:21 +0100
changeset 2337	b151399bd2c3
parent 2145	f89773ab0685
permissions	-rw-r--r--