nominal2: Nominal/Ex/NBE.thy@0f1b44c9c5a0 (annotated)

2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Lambda
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	"../Nominal2"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	begin
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	5
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	atom_decl name
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	8
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	nominal_datatype lam =
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	Var "name"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	\| App "lam" "lam"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	\| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	13
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	nominal_datatype sem =
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	15	L e::"env" x::"name" l::"lam" binds x "bn e" in l
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	\| N "neu"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	and neu =
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	V "name"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	\| A "neu" "sem"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	and env =
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	ENil
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	\| ECons "env" "name" "sem"
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	23	binder
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	24	bn
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	25	where
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	26	"bn ENil = []"
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	27	\| "bn (ECons env x v) = (atom x) # (bn env)"
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	28
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	29	thm sem_neu_env.supp
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	30
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	31	lemma [simp]:
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	32	shows "finite (fv_bn env)"
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	33	apply(induct env rule: sem_neu_env.inducts(3))
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	34	apply(rule TrueI)+
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	35	apply(auto simp add: sem_neu_env.supp finite_supp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	36	done
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	37
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	38	lemma test1:
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	39	shows "supp p \<sharp>* (fv_bn env) \<Longrightarrow> (p \<bullet> env) = permute_bn p env"
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	40	apply(induct env rule: sem_neu_env.inducts(3))
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	41	apply(rule TrueI)+
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	42	apply(auto simp add: sem_neu_env.perm_bn_simps sem_neu_env.supp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	43	apply(drule meta_mp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	44	apply(drule fresh_star_supp_conv)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	45	apply(subst (asm) supp_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	46	apply(simp add: finite_supp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	47	apply(simp add: fresh_star_Un)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	48	apply(rule fresh_star_supp_conv)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	49	apply(subst supp_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	50	apply(simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	51	apply(simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	52	apply(simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	53	apply(rule perm_supp_eq)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	54	apply(drule fresh_star_supp_conv)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	55	apply(subst (asm) supp_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	56	apply(simp add: finite_supp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	57	apply(simp add: fresh_star_Un)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	58	apply(rule fresh_star_supp_conv)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	59	apply(simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	60	done
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	61
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	62	thm alpha_sem_raw_alpha_neu_raw_alpha_env_raw_alpha_bn_raw.inducts(4)[no_vars]
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	63
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	64	lemma alpha_bn_inducts_raw[consumes 1]:
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	65	"\<lbrakk>alpha_bn_raw x7 x8;
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	66	P4 ENil_raw ENil_raw;
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	67	\<And>env_raw env_rawa sem_raw sem_rawa name namea.
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	68	\<lbrakk>alpha_bn_raw env_raw env_rawa; P4 env_raw env_rawa; alpha_sem_raw sem_raw sem_rawa\<rbrakk>
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	69	\<Longrightarrow> P4 (ECons_raw env_raw name sem_raw) (ECons_raw env_rawa namea sem_rawa)\<rbrakk>
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	70	\<Longrightarrow> P4 x7 x8"
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	71	apply(induct rule: alpha_sem_raw_alpha_neu_raw_alpha_env_raw_alpha_bn_raw.inducts(4))
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	72	apply(rule TrueI)+
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	73	apply(auto)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	74	done
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	75
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	76	lemmas alpha_bn_inducts[consumes 1] = alpha_bn_inducts_raw[quot_lifted]
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	77
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	78	lemma test2:
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	79	shows "alpha_bn env1 env2 \<Longrightarrow> p \<bullet> (bn env1) = q \<bullet> (bn env2) \<Longrightarrow> permute_bn p env1 = permute_bn q env2"
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	80	apply(induct rule: alpha_bn_inducts)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	81	apply(auto simp add: sem_neu_env.perm_bn_simps sem_neu_env.bn_defs)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	82	apply(simp add: atom_eqvt)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	83	done
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	84
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	85	lemma fresh_star_Union:
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	86	assumes "as \<subseteq> bs" "bs \<sharp>* x"
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	87	shows "as \<sharp>* x"
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	88	using assms by (auto simp add: fresh_star_def)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	89
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	90
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	91	nominal_primrec (invariant "\<lambda>x y. case x of Inl (x1, y1) \<Rightarrow>
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	92	supp y \<subseteq> (supp y1 - set (bn x1)) \<union> (fv_bn x1) \| Inr (x2, y2) \<Rightarrow> supp y \<subseteq> supp x2 \<union> supp y2")
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	93	evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	94	evals_aux :: "sem \<Rightarrow> sem \<Rightarrow> sem"
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	95	where
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	96	"evals ENil (Var x) = N (V x)"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	97	\| "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))"
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	98	\| "atom x \<sharp> env \<Longrightarrow> evals env (Lam [x]. t) = L env x t"
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	99	\| "evals env (App t1 t2) = evals_aux (evals env t1) (evals env t2)"
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	100	\| "set (atom x # bn env) \<sharp>* (fv_bn env, t') \<Longrightarrow> evals_aux (L env x t) t' = evals (ECons env x t') t"
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	101	\| "evals_aux (N n) t' = N (A n t')"
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	102	apply(simp add: eqvt_def evals_evals_aux_graph_def)
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	103	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	104	apply(simp)
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	105	apply(erule evals_evals_aux_graph.induct)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	106	apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	107	apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	108	apply(rule conjI)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	109	apply(rule impI)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	110	apply(blast)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	111	apply(rule impI)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	112	apply(simp add: supp_at_base)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	113	apply(blast)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	114	apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	115	apply(blast)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	116	apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	117	apply(blast)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	118	apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	119	apply(blast)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	120	apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	121	--"completeness"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	122	apply(case_tac x)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	123	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	124	apply(case_tac a)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	125	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	126	apply(case_tac aa rule: sem_neu_env.exhaust(3))
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	127	apply(simp add: sem_neu_env.fresh)
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	128	apply(case_tac b rule: lam.exhaust)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	apply(metis)+
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	130	apply(case_tac aa rule: sem_neu_env.exhaust(3))
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	131	apply(rule_tac y="b" and c="env" in lam.strong_exhaust)
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	132	apply(metis)+
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	133	apply(simp add: fresh_star_def)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	134	apply(simp)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	135	apply(rule_tac y="b" and c="ECons env name sem" in lam.strong_exhaust)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	136	apply(metis)+
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	137	apply(simp add: fresh_star_def)
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	138	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	139	apply(case_tac b)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	140	apply(simp)
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	141	apply(rule_tac y="a" and c="(a, ba)" in sem_neu_env.strong_exhaust(1))
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	142	apply(simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	143	apply(rotate_tac 4)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	144	apply(drule_tac x="name" in meta_spec)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	145	apply(drule_tac x="env" in meta_spec)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	146	apply(drule_tac x="ba" in meta_spec)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	147	apply(drule_tac x="lam" in meta_spec)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	148	apply(simp add: sem_neu_env.alpha_refl)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	149	apply(rotate_tac 9)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	150	apply(drule_tac meta_mp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	151	apply(simp (no_asm_use) add: fresh_star_def sem_neu_env.fresh fresh_Pair)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	152	apply(simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	153	apply(subst fresh_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	154	defer
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	155	apply(simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	156	apply(subst fresh_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	157	defer
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	158	apply(simp)
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	159	apply(metis)+
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	160	--"compatibility"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	161	apply(all_trivials)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	162	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	163	apply(simp)
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	164	defer
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	165	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	166	apply(simp)
2953 80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	167	apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff])
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	168	apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons env x t'a, t)")
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	169	apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons enva xa t'a, ta)")
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	170	apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons env x t'a, t))")
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	171	apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons enva xa t'a, ta))")
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	172	apply(erule conjE)+
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	173	defer
2953 80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	174	apply (simp_all add: eqvt_at_def evals_def)[3]
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	175	defer
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	176	defer
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	177	apply(simp add: sem_neu_env.alpha_refl)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	178	apply(erule conjE)+
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	179	apply(erule_tac c="(env, enva)" in Abs_lst1_fcb2)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	180	apply(simp add: Abs_fresh_iff)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	181	apply(simp add: fresh_star_def)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	182	apply(perm_simp)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	183	apply(simp add: fresh_star_Pair perm_supp_eq)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	184	apply(perm_simp)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	185	apply(simp add: fresh_star_Pair perm_supp_eq)
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	186	apply(simp add: sem_neu_env.bn_defs sem_neu_env.supp)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	187	using at_set_avoiding3
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	188	apply -
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	189	apply(drule_tac x="set (atom x # bn env)" in meta_spec)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	190	apply(drule_tac x="(fv_bn env, fv_bn enva, env, enva, x, xa, t, ta, t'a)" in meta_spec)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	191	apply(drule_tac x="[atom x # bn env]lst. t" in meta_spec)
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	192	apply(simp (no_asm_use) add: finite_supp Abs_fresh_star_iff)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	193	apply(drule meta_mp)
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	194	apply(simp add: supp_Pair finite_supp supp_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	195	apply(drule meta_mp)
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	196	apply(simp add: fresh_star_def)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	197	apply(erule exE)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	198	apply(erule conjE)+
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	199	apply(rule trans)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	200	apply(rule sym)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	201	apply(rule_tac p="p" in perm_supp_eq)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	202	apply(simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	203	apply(perm_simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	204	apply(simp add: fresh_star_Un fresh_star_insert)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	205	apply(rule conjI)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	206	apply(simp (no_asm_use) add: fresh_star_def fresh_Pair)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	207	apply(simp add: fresh_def)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	208	apply(simp add: supp_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	209	apply(blast)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	210	apply(rule conjI)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	211	apply(simp (no_asm_use) add: fresh_star_def fresh_Pair)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	212	apply(simp add: fresh_def)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	213	apply(simp add: supp_finite_atom_set)
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	214	apply(blast)
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	215	apply(rule conjI)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	216	apply(simp (no_asm_use) add: fresh_star_def fresh_Pair)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	217	apply(simp add: fresh_def)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	218	apply(simp add: supp_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	219	apply(blast)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	220	apply(simp (no_asm_use) add: fresh_star_def fresh_Pair)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	221	apply(simp add: fresh_def)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	222	apply(simp add: supp_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	223	apply(blast)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	224	apply(simp add: eqvt_at_def perm_supp_eq)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	225	apply(subst (3) perm_supp_eq)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	226	apply(simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	227	apply(simp add: fresh_star_def fresh_Pair)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	228	apply(auto)[1]
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	229	apply(rotate_tac 6)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	230	apply(drule sym)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	231	apply(simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	232	apply(rotate_tac 11)
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	233	apply(drule trans)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	234	apply(rule sym)
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	235	apply(rule_tac p="p" in supp_perm_eq)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	236	apply(assumption)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	237	apply(rotate_tac 11)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	238	apply(rule sym)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	239	apply(simp add: atom_eqvt)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	240	apply(simp (no_asm_use) add: Abs_eq_iff2 alphas)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	241	apply(erule conjE \| erule exE)+
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	242	apply(rule trans)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	243	apply(rule sym)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	244	apply(rule_tac p="pa" in perm_supp_eq)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	245	apply(erule fresh_star_Union)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	246	apply(simp (no_asm_use) add: fresh_star_insert fresh_star_Un)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	247	apply(rule conjI)
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	248	apply(perm_simp)
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	249	apply(simp add: fresh_star_insert fresh_star_Un)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	250	apply(simp add: fresh_Pair)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	251	apply(simp add: fresh_def)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	252	apply(simp add: supp_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	253	apply(blast)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	254	apply(rule conjI)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	255	apply(perm_simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	256	apply(simp add: fresh_star_insert fresh_star_Un)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	257	apply(simp add: fresh_Pair)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	258	apply(simp add: fresh_def)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	259	apply(simp add: supp_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	260	apply(blast)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	261	apply(rule conjI)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	262	apply(perm_simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	263	defer
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	264	apply(perm_simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	265	apply(simp add: fresh_star_insert fresh_star_Un)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	266	apply(simp add: fresh_star_Pair)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	267	apply(simp add: fresh_star_def fresh_def)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	268	apply(simp add: supp_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	269	apply(blast)
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	270	apply(simp)
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	271	apply(perm_simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	272	apply(subst (3) perm_supp_eq)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	273	apply(erule fresh_star_Union)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	274	apply(simp add: fresh_star_insert fresh_star_Un)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	275	apply(simp add: fresh_star_def fresh_Pair)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	276	apply(subgoal_tac "pa \<bullet> enva = p \<bullet> env")
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	277	apply(simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	278	defer
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	279	apply(simp (no_asm_use) add: fresh_star_insert fresh_star_Un)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	280	apply(simp (no_asm_use) add: fresh_star_def)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	281	apply(rule ballI)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	282	apply(subgoal_tac "a \<notin> supp ta - insert (atom xa) (set (bn enva)) \<union> (fv_bn enva \<union> supp t'a)")
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	283	apply(simp only: fresh_def)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	284	apply(blast)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	285	apply(simp (no_asm_use))
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	286	apply(rule conjI)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	287	apply(blast)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	288	apply(simp add: fresh_Pair)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	289	apply(simp add: fresh_star_def fresh_def)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	290	apply(simp add: supp_finite_atom_set)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	291	apply(subst test1)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	292	apply(erule fresh_star_Union)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	293	apply(simp add: fresh_star_insert fresh_star_Un)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	294	apply(simp add: fresh_star_def fresh_Pair)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	295	apply(subst test1)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	296	apply(simp)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	297	apply(simp add: fresh_star_insert fresh_star_Un)
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	298	apply(simp add: fresh_star_def fresh_Pair)
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	299	apply(rule sym)
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	300	apply(erule test2)
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	301	apply(perm_simp)
ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	302	apply(simp)
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	303	done
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	304
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	305
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	306
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	307
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	308	text {* can probably not proved by a trivial size argument *}
0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	309	termination (* apply(lexicographic_order) *)
2968 ddb69d9f45d0 more one the NBE example Christian Urban <urbanc@in.tum.de> parents: 2967 diff changeset	310	sorry
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	311
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	312	lemma [eqvt]:
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	313	shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)"
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	314	and "(p \<bullet> evals_aux v s) = evals_aux (p \<bullet> v) (p \<bullet> s)"
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	315	sorry
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	316
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	317	(* fixme: should be a provided lemma *)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	318	lemma fv_bn_finite:
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	319	shows "finite (fv_bn env)"
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	320	apply(induct env rule: sem_neu_env.inducts(3))
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	321	apply(auto simp add: sem_neu_env.supp finite_supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	322	done
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	323
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	324	lemma test:
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	325	fixes env::"env"
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	326	shows "supp (evals env t) \<subseteq> (supp t - set (bn env)) \<union> (fv_bn env)"
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	327	and "supp (evals_aux s v) \<subseteq> (supp s) \<union> (supp v)"
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	328	apply(induct env t and s v rule: evals_evals_aux.induct)
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	329	apply(simp add: sem_neu_env.supp lam.supp supp_Nil sem_neu_env.bn_defs)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	330	apply(simp add: sem_neu_env.supp lam.supp supp_Nil supp_Cons sem_neu_env.bn_defs)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	331	apply(rule conjI)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	332	apply(auto)[1]
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	333	apply(rule impI)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	334	apply(simp)
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	335	apply(simp add: supp_at_base)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	336	apply(blast)
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	337	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	338	apply(subst sem_neu_env.supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	339	apply(simp add: sem_neu_env.supp lam.supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	340	apply(auto)[1]
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	341	apply(simp add: lam.supp sem_neu_env.supp)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	342	apply(blast)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	343	apply(simp add: sem_neu_env.supp sem_neu_env.bn_defs)
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	344	apply(blast)
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	345	apply(simp add: sem_neu_env.supp)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	346	done
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	347
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	348
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	349	nominal_primrec
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	350	reify :: "sem \<Rightarrow> lam" and
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	351	reifyn :: "neu \<Rightarrow> lam"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	352	where
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	353	"atom x \<sharp> (env, y, t) \<Longrightarrow> reify (L env y t) = Lam [x]. (reify (evals (ECons env y (N (V x))) t))"
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	354	\| "reify (N n) = reifyn n"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	355	\| "reifyn (V x) = Var x"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	356	\| "reifyn (A n d) = App (reifyn n) (reify d)"
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	357	apply(subgoal_tac "\<And>p x y. reify_reifyn_graph x y \<Longrightarrow> reify_reifyn_graph (p \<bullet> x) (p \<bullet> y)")
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	358	apply(simp add: eqvt_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	359	apply(simp add: permute_fun_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	360	apply(rule allI)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	361	apply(rule ext)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	362	apply(rule ext)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	363	apply(rule iffI)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	364	apply(drule_tac x="p" in meta_spec)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	365	apply(drule_tac x="- p \<bullet> x" in meta_spec)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	366	apply(drule_tac x="- p \<bullet> xa" in meta_spec)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	367	apply(simp add: permute_bool_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	368	apply(simp add: permute_bool_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	369	apply(erule reify_reifyn_graph.induct)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	370	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	371	apply(rule reify_reifyn_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	372	apply(rule_tac p="-p" in permute_boolE)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	373	apply(perm_simp add: permute_minus_cancel)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	374	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	375	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	376	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	377	apply(rule reify_reifyn_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	378	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	379	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	380	apply(rule reify_reifyn_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	381	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	382	apply(rule reify_reifyn_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	383	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	384	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	385	apply(rule TrueI)
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	386	--"completeness"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	387	apply(case_tac x)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	388	apply(simp)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	389	apply(case_tac a rule: sem_neu_env.exhaust(1))
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	390	apply(subgoal_tac "\<exists>x::name. atom x \<sharp> (env, name, lam)")
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	391	apply(metis)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	392	apply(rule obtain_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	393	apply(blast)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	394	apply(blast)
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	395	apply(case_tac b rule: sem_neu_env.exhaust(2))
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	396	apply(simp)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	397	apply(simp)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	398	apply(metis)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	399	--"compatibility"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	400	apply(all_trivials)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	401	defer
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	402	apply(simp)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	403	apply(simp)
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	404	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	405	apply(erule conjE)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	406	apply (simp add: meta_eq_to_obj_eq[OF reify_def, symmetric, unfolded fun_eq_iff])
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	407	apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons env y (N (V x))) t)")
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	408	apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva ya (N (V xa))) ta)")
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	409	apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons env y (N (V x))) t))")
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	410	apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva ya (N (V xa))) ta))")
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	411	defer
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	412	apply (simp_all add: eqvt_at_def reify_def)[2]
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	413	apply(subgoal_tac "\<exists>c::name. atom c \<sharp> (x, xa, env, enva, y, ya, t, ta)")
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	414	prefer 2
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	415	apply(rule obtain_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	416	apply(blast)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	417	apply(erule exE)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	418	apply(rule trans)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	419	apply(rule sym)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	420	apply(rule_tac a="x" and b="c" in flip_fresh_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	421	apply(simp add: Abs_fresh_iff)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	422	apply(simp add: Abs_fresh_iff fresh_Pair)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	423	apply(auto)[1]
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	424	apply(rule fresh_eqvt_at)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	425	back
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	426	apply(assumption)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	427	apply(simp add: finite_supp)
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	428	apply(rule_tac S="supp (env, y, x, t)" in supports_fresh)
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	429	apply(simp add: supports_def fresh_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	430	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	431	apply(simp add: swap_fresh_fresh fresh_Pair)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	432	apply(simp add: finite_supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	433	apply(simp add: fresh_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	434	apply(simp add: eqvt_at_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	435	apply(simp add: eqvt_at_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	436	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	437	apply(simp add: flip_fresh_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	438	apply(rule sym)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	439	apply(rule trans)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	440	apply(rule sym)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	441	apply(rule_tac a="xa" and b="c" in flip_fresh_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	442	apply(simp add: Abs_fresh_iff)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	443	apply(simp add: Abs_fresh_iff fresh_Pair)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	444	apply(auto)[1]
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	445	apply(rule fresh_eqvt_at)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	446	back
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	447	apply(assumption)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	448	apply(simp add: finite_supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	449	apply(rule_tac S="supp (enva, ya, xa, ta)" in supports_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	450	apply(simp add: supports_def fresh_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	451	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	452	apply(simp add: swap_fresh_fresh fresh_Pair)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	453	apply(simp add: finite_supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	454	apply(simp add: fresh_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	455	apply(simp add: eqvt_at_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	456	apply(simp add: eqvt_at_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	457	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	458	apply(simp add: flip_fresh_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	459	apply(simp (no_asm) add: Abs1_eq_iff)
2969 0f1b44c9c5a0 defined a function directly over a nominal datatype with bn Christian Urban <urbanc@in.tum.de> parents: 2968 diff changeset	460	(* HERE *)
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	461	thm at_set_avoiding3
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	462	using at_set_avoiding3
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	463	apply -
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	464	apply(drule_tac x="set (atom y # bn env)" in meta_spec)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	465	apply(drule_tac x="(env, enva)" in meta_spec)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	466	apply(drule_tac x="[atom y # bn env]lst. t" in meta_spec)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	467	apply(simp (no_asm_use) add: finite_supp)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	468	apply(drule meta_mp)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	469	apply(rule Abs_fresh_star)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	470	apply(auto)[1]
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	471	apply(erule exE)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	472	apply(erule conjE)+
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	473	apply(drule_tac q="(x \<leftrightarrow> c)" in eqvt_at_perm)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	474	apply(perm_simp)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	475	apply(simp add: flip_fresh_fresh fresh_Pair)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	476	apply(drule_tac q="(xa \<leftrightarrow> c)" in eqvt_at_perm)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	477	apply(perm_simp)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	478	apply(simp add: flip_fresh_fresh fresh_Pair)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	479	apply(drule sym)
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	480	(* HERE *)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	481	apply(rotate_tac 9)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	482	apply(drule sym)
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	483	apply(rotate_tac 9)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	484	apply(drule trans)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	485	apply(rule sym)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	486	apply(rule_tac p="p" in supp_perm_eq)
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	487	apply(assumption)
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	488	apply(simp)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	489	apply(perm_simp)
2967 d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	490	apply(simp (no_asm_use) add: Abs_eq_iff2 alphas)
d7e8b9b78e28 some improvements to the NBE example Christian Urban <urbanc@in.tum.de> parents: 2956 diff changeset	491	apply(erule conjE \| erule exE)+
2956 7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	492	apply(clarify)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	493	apply(rule trans)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	494	apply(rule sym)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	495	apply(rule_tac p="pa" in perm_supp_eq)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	496	defer
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	497	apply(rule sym)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	498	apply(rule trans)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	499	apply(rule sym)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	500	apply(rule_tac p="p" in perm_supp_eq)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	501	defer
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	502	apply(simp add: atom_eqvt)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	503	apply(drule_tac q="(x \<leftrightarrow> c)" in eqvt_at_perm)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	504	apply(perm_simp)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	505	apply(simp add: flip_fresh_fresh fresh_Pair)
7e1c309bf820 more on NBE Christian Urban <urbanc@in.tum.de> parents: 2955 diff changeset	506
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	507	apply(rule sym)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	508	apply(erule_tac Abs_lst1_fcb2')
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	509	apply(rule fresh_eqvt_at)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	510	back
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	511	apply(drule_tac q="(c \<leftrightarrow> x)" in eqvt_at_perm)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	512	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	513	apply(simp add: flip_fresh_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	514	apply(simp add: finite_supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	515	apply(rule supports_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	516	apply(rule_tac S="supp (enva, ya, xa, ta)" in supports_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	517	apply(simp add: supports_def fresh_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	518	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	519	apply(simp add: swap_fresh_fresh fresh_Pair)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	520	apply(simp add: finite_supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	521	apply(simp add: fresh_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	522	apply(simp add: eqvt_at_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	523	apply(simp add: eqvt_at_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	524	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	525	apply(rule fresh_eqvt_at)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	526	back
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	527	apply(drule_tac q="(c \<leftrightarrow> x)" in eqvt_at_perm)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	528	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	529	apply(simp add: flip_fresh_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	530	apply(assumption)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	531	apply(simp add: finite_supp)
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	532	sorry
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	533
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	534	termination sorry
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	535
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	536	definition
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	537	eval :: "lam \<Rightarrow> sem"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	538	where
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	539	"eval t = evals ENil t"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	540
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	541	definition
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	542	normalize :: "lam \<Rightarrow> lam"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	543	where
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	544	"normalize t = reify (eval t)"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	545
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	546	end

author	Christian Urban <urbanc@in.tum.de>
	Sun, 17 Jul 2011 04:04:17 +0100
changeset 2969	0f1b44c9c5a0
parent 2968	ddb69d9f45d0
child 3235	5ebd327ffb96
permissions	-rw-r--r--