nominal2: Nominal/Ex/NBE.thy@4049a2651dd9 (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
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	nominal_datatype sem =
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	16	L e::"env" x::"name" l::"lam" binds "bn e" x in l
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	\| N "neu"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	and neu =
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	V "name"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	\| A "neu" "sem"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	and env =
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	ENil
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	\| ECons "env" "name" "sem"
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	24	binder
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	25	bn
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	26	where
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	27	"bn ENil = []"
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	28	\| "bn (ECons env x v) = atom x # bn env"
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
2953 80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	30	nominal_primrec
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	where
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	"evals ENil (Var x) = N (V x)"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	\| "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	\| "evals env (Lam [x]. t) = L env x t"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	\| "evals env (App t1 t2) = evals_aux (evals env t1) t2 env"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	\| "evals_aux (L cenv x t) t2 env = evals (ECons cenv x (evals env t2)) t"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	\| "evals_aux (N n) t2 env = N (A n (evals env t2))"
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	40	apply(subgoal_tac "\<And>p x y. evals_evals_aux_graph x y \<Longrightarrow> evals_evals_aux_graph (p \<bullet> x) (p \<bullet> y)")
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	41	apply(simp add: eqvt_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	42	apply(simp add: permute_fun_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	43	apply(rule allI)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	44	apply(rule ext)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	45	apply(rule ext)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	46	apply(rule iffI)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	47	apply(drule_tac x="p" in meta_spec)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	48	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	49	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	50	apply(simp add: permute_bool_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	51	apply(simp add: permute_bool_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	52	apply(erule evals_evals_aux_graph.induct)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	53	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	54	apply(rule evals_evals_aux_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	55	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	56	apply(rule evals_evals_aux_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	57	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	58	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	59	apply(rule evals_evals_aux_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	60	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	61	apply(rule evals_evals_aux_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	62	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	63	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	64	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	65	apply(rule evals_evals_aux_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	66	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	67	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	68	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	69	apply(rule evals_evals_aux_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	70	apply(simp)
2953 80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	71	apply (rule TrueI)
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	--"completeness"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	73	apply(case_tac x)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	75	apply(case_tac a)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	76	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	77	apply(case_tac aa rule: sem_neu_env.exhaust(3))
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	79	apply(case_tac b rule: lam.exhaust)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	apply(metis)+
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	81	apply(case_tac b rule: lam.exhaust)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	82	apply(metis)+
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	83	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	84	apply(case_tac b)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	85	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	86	apply(case_tac a rule: sem_neu_env.exhaust(1))
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	87	apply(metis)+
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	88	--"compatibility"
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	89	apply(all_trivials)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	90	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	91	apply(simp)
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	92	defer
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	93	apply(simp)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	94	apply(simp)
2953 80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	95	apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff])
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	96	apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenv x (evals enva t2a), t)")
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	97	apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (enva, t2a)")
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	98	apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa (evals enva t2a), ta)")
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	99	apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenv x (evals enva t2a), t))")
2953 80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	100	apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))")
80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	101	apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))")
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	102	apply(erule conjE)+
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	103	defer
2953 80f01215d1a6 Setup eqvt_at for first goal Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2952 diff changeset	104	apply (simp_all add: eqvt_at_def evals_def)[3]
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	105	apply(simp)
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	106	sorry
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	107
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	108	(* can probably not proved by a trivial size argument *)
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	109	termination sorry
e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	110
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	111	lemma [eqvt]:
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	112	shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)"
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	113	and "(p \<bullet> evals_aux v t env) = evals_aux (p \<bullet> v) (p \<bullet> t) (p \<bullet> env)"
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	114	sorry
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	115
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	116	(* fixme: should be a provided lemma *)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	117	lemma fv_bn_finite:
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	118	shows "finite (fv_bn env)"
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	119	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	120	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	121	done
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	122
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	123	lemma test:
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	124	shows "supp (evals env t) \<subseteq> (supp t - set (bn env)) \<union> (fv_bn env)"
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	125	and "supp (evals_aux s t env) \<subseteq> ((supp s) - set (bn cenv)) \<union> supp (fn cenv) \<union> supp (evals env t)"
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	126	apply(induct rule: evals_evals_aux.induct)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	127	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	128	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	129	apply(rule conjI)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	130	apply(auto)[1]
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	131	apply(rule impI)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	132	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	133	apply (metis (no_types) at_base_infinite finite_UNIV)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	134	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	135	apply(subst sem_neu_env.supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	136	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	137	apply(auto)[1]
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	138	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	139	apply(metis)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	140	sorry
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	141
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	142	nominal_primrec
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	143	reify :: "sem \<Rightarrow> lam" and
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	144	reifyn :: "neu \<Rightarrow> lam"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	145	where
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	146	"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	147	\| "reify (N n) = reifyn n"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	148	\| "reifyn (V x) = Var x"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	149	\| "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	150	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	151	apply(simp add: eqvt_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	152	apply(simp add: permute_fun_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	153	apply(rule allI)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	154	apply(rule ext)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	155	apply(rule ext)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	156	apply(rule iffI)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	157	apply(drule_tac x="p" in meta_spec)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	158	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	159	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	160	apply(simp add: permute_bool_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	161	apply(simp add: permute_bool_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	162	apply(erule reify_reifyn_graph.induct)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	163	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	164	apply(rule reify_reifyn_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	165	apply(rule_tac p="-p" in permute_boolE)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	166	apply(perm_simp add: permute_minus_cancel)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	167	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	168	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	169	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	170	apply(rule reify_reifyn_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	171	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	172	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	173	apply(rule reify_reifyn_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	174	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	175	apply(rule reify_reifyn_graph.intros)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	176	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	177	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	178	apply(rule TrueI)
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	179	--"completeness"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	180	apply(case_tac x)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	181	apply(simp)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	182	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	183	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	184	apply(metis)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	185	apply(rule obtain_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	186	apply(blast)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	187	apply(blast)
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	188	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	189	apply(simp)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	190	apply(simp)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	191	apply(metis)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	192	--"compatibility"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	193	apply(all_trivials)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	194	defer
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	195	apply(simp)
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	196	apply(simp)
2955 4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	197	apply(simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	198	apply(erule conjE)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	199	apply (simp add: meta_eq_to_obj_eq[OF reify_def, symmetric, unfolded fun_eq_iff])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	200	apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva y (N (V x))) t)")
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	201	apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva ya (N (V xa))) ta)")
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	202	apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva y (N (V x))) t))")
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	203	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	204	defer
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	205	apply (simp_all add: eqvt_at_def reify_def)[2]
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	206	apply(subgoal_tac "\<exists>c::name. atom c \<sharp> (x, xa, enva, y, ya, t, ta)")
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	207	prefer 2
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	208	apply(rule obtain_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	209	apply(blast)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	210	apply(erule exE)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	211	apply(rule trans)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	212	apply(rule sym)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	213	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	214	apply(simp add: Abs_fresh_iff)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	215	apply(simp add: Abs_fresh_iff fresh_Pair)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	216	apply(auto)[1]
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	217	apply(rule fresh_eqvt_at)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	218	back
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	219	apply(assumption)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	220	apply(simp add: finite_supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	221	apply(rule_tac S="supp (enva, y, x, t)" in supports_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	222	apply(simp add: supports_def fresh_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	223	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	224	apply(simp add: swap_fresh_fresh fresh_Pair)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	225	apply(simp add: finite_supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	226	apply(simp add: fresh_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	227	apply(simp add: eqvt_at_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	228	apply(simp add: eqvt_at_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	229	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	230	apply(simp add: flip_fresh_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	231	apply(rule sym)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	232	apply(rule trans)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	233	apply(rule sym)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	234	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	235	apply(simp add: Abs_fresh_iff)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	236	apply(simp add: Abs_fresh_iff fresh_Pair)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	237	apply(auto)[1]
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	238	apply(rule fresh_eqvt_at)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	239	back
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	240	apply(assumption)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	241	apply(simp add: finite_supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	242	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	243	apply(simp add: supports_def fresh_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	244	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	245	apply(simp add: swap_fresh_fresh fresh_Pair)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	246	apply(simp add: finite_supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	247	apply(simp add: fresh_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	248	apply(simp add: eqvt_at_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	249	apply(simp add: eqvt_at_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	250	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	251	apply(simp add: flip_fresh_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	252	apply(simp (no_asm) add: Abs1_eq_iff)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	253	apply(rule sym)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	254	apply(erule_tac Abs_lst1_fcb2')
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	255	apply(rule fresh_eqvt_at)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	256	back
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	257	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	258	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	259	apply(simp add: flip_fresh_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	260	apply(simp add: finite_supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	261	apply(rule supports_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	262	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	263	apply(simp add: supports_def fresh_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	264	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	265	apply(simp add: swap_fresh_fresh fresh_Pair)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	266	apply(simp add: finite_supp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	267	apply(simp add: fresh_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	268	apply(simp add: eqvt_at_def)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	269	apply(simp add: eqvt_at_def[symmetric])
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	270	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	271	apply(rule fresh_eqvt_at)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	272	back
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	273	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	274	apply(perm_simp)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	275	apply(simp add: flip_fresh_fresh)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	276	apply(assumption)
4049a2651dd9 more on the NBE function Christian Urban <urbanc@in.tum.de> parents: 2954 diff changeset	277	apply(simp add: finite_supp)
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	278	sorry
2952 e4c2854833ad attempt for NBE Christian Urban <urbanc@in.tum.de> parents: diff changeset	279
2954 dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	280	termination sorry
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	281
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	282	definition
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	283	eval :: "lam \<Rightarrow> sem"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	284	where
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	285	"eval t = evals ENil t"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	286
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	287	definition
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	288	normalize :: "lam \<Rightarrow> lam"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	289	where
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	290	"normalize t = reify (eval t)"
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	291
dc6007dd9c30 a little further with NBE Christian Urban <urbanc@in.tum.de> parents: 2953 diff changeset	292	end

author	Christian Urban <urbanc@in.tum.de>
	Wed, 06 Jul 2011 15:59:11 +0200
changeset 2955	4049a2651dd9
parent 2954	dc6007dd9c30
child 2956	7e1c309bf820
permissions	-rw-r--r--