28 | "bn (ECons env x v) = (atom x) # (bn env)" |
28 | "bn (ECons env x v) = (atom x) # (bn env)" |
29 |
29 |
30 |
30 |
31 nominal_primrec |
31 nominal_primrec |
32 evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and |
32 evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and |
33 evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem" |
33 evals_aux :: "sem \<Rightarrow> sem \<Rightarrow> sem" |
34 where |
34 where |
35 "evals ENil (Var x) = N (V x)" |
35 "evals ENil (Var x) = N (V x)" |
36 | "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))" |
36 | "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))" |
37 | "evals env (Lam [x]. t) = L env x t" |
37 | "atom x \<sharp> env \<Longrightarrow> evals env (Lam [x]. t) = L env x t" |
38 | "evals env (App t1 t2) = evals_aux (evals env t1) t2 env" |
38 | "evals env (App t1 t2) = evals_aux (evals env t1) (evals env t2)" |
39 | "evals_aux (L cenv x t) t2 env = evals (ECons cenv x (evals env t2)) t" |
39 | "evals_aux (L cenv x t) t' = evals (ECons cenv x t') t" |
40 | "evals_aux (N n) t2 env = N (A n (evals env t2))" |
40 | "evals_aux (N n) t' = N (A n t')" |
41 apply(subgoal_tac "\<And>p x y. evals_evals_aux_graph x y \<Longrightarrow> evals_evals_aux_graph (p \<bullet> x) (p \<bullet> y)") |
41 apply(simp add: eqvt_def evals_evals_aux_graph_def) |
42 apply(simp add: eqvt_def) |
42 apply(perm_simp) |
43 apply(simp add: permute_fun_def) |
|
44 apply(rule allI) |
|
45 apply(rule ext) |
|
46 apply(rule ext) |
|
47 apply(rule iffI) |
|
48 apply(drule_tac x="p" in meta_spec) |
|
49 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
50 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
51 apply(simp add: permute_bool_def) |
|
52 apply(simp add: permute_bool_def) |
|
53 apply(erule evals_evals_aux_graph.induct) |
|
54 apply(perm_simp) |
|
55 apply(rule evals_evals_aux_graph.intros) |
|
56 apply(perm_simp) |
|
57 apply(rule evals_evals_aux_graph.intros) |
|
58 apply(simp) |
|
59 apply(perm_simp) |
|
60 apply(rule evals_evals_aux_graph.intros) |
|
61 apply(perm_simp) |
|
62 apply(rule evals_evals_aux_graph.intros) |
|
63 apply(simp) |
|
64 apply(simp) |
|
65 apply(perm_simp) |
|
66 apply(rule evals_evals_aux_graph.intros) |
|
67 apply(simp) |
|
68 apply(simp) |
|
69 apply(perm_simp) |
|
70 apply(rule evals_evals_aux_graph.intros) |
|
71 apply(simp) |
43 apply(simp) |
72 apply (rule TrueI) |
44 apply (rule TrueI) |
73 --"completeness" |
45 --"completeness" |
74 apply(case_tac x) |
46 apply(case_tac x) |
75 apply(simp) |
47 apply(simp) |
76 apply(case_tac a) |
48 apply(case_tac a) |
77 apply(simp) |
49 apply(simp) |
78 apply(case_tac aa rule: sem_neu_env.exhaust(3)) |
50 apply(case_tac aa rule: sem_neu_env.exhaust(3)) |
79 apply(simp) |
51 apply(simp add: sem_neu_env.fresh) |
80 apply(case_tac b rule: lam.exhaust) |
52 apply(case_tac b rule: lam.exhaust) |
81 apply(metis)+ |
53 apply(metis)+ |
82 apply(case_tac b rule: lam.exhaust) |
54 apply(case_tac aa rule: sem_neu_env.exhaust(3)) |
|
55 apply(rule_tac y="b" and c="env" in lam.strong_exhaust) |
83 apply(metis)+ |
56 apply(metis)+ |
|
57 apply(simp add: fresh_star_def) |
|
58 apply(simp) |
|
59 apply(rule_tac y="b" and c="ECons env name sem" in lam.strong_exhaust) |
|
60 apply(metis)+ |
|
61 apply(simp add: fresh_star_def) |
84 apply(simp) |
62 apply(simp) |
85 apply(case_tac b) |
63 apply(case_tac b) |
86 apply(simp) |
64 apply(simp) |
87 apply(case_tac a rule: sem_neu_env.exhaust(1)) |
65 apply(case_tac a rule: sem_neu_env.exhaust(1)) |
88 apply(metis)+ |
66 apply(metis)+ |
92 apply(simp) |
70 apply(simp) |
93 defer |
71 defer |
94 apply(simp) |
72 apply(simp) |
95 apply(simp) |
73 apply(simp) |
96 apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff]) |
74 apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff]) |
97 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenv x (evals enva t2a), t)") |
75 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenv x t'a, t)") |
98 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (enva, t2a)") |
76 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa t'a, ta)") |
99 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa (evals enva t2a), ta)") |
77 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenv x t'a, t))") |
100 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenv x (evals enva t2a), t))") |
78 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa t'a, ta))") |
101 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))") |
|
102 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))") |
|
103 apply(erule conjE)+ |
79 apply(erule conjE)+ |
104 defer |
80 defer |
105 apply (simp_all add: eqvt_at_def evals_def)[3] |
81 apply (simp_all add: eqvt_at_def evals_def)[3] |
106 apply(simp) |
82 apply(simp add: sem_neu_env.alpha_refl) |
|
83 apply(erule conjE)+ |
|
84 apply(erule_tac c="(env, enva)" in Abs_lst1_fcb2) |
|
85 apply(simp add: Abs_fresh_iff) |
|
86 apply(simp add: fresh_star_def) |
|
87 apply(perm_simp) |
|
88 apply(simp add: fresh_star_Pair perm_supp_eq) |
|
89 apply(perm_simp) |
|
90 apply(simp add: fresh_star_Pair perm_supp_eq) |
|
91 thm Abs_lst1_fcb2' |
107 sorry |
92 sorry |
108 |
93 |
109 (* can probably not proved by a trivial size argument *) |
94 (* can probably not proved by a trivial size argument *) |
110 termination sorry |
95 termination sorry |
111 |
96 |
112 lemma [eqvt]: |
97 lemma [eqvt]: |
113 shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)" |
98 shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)" |
114 and "(p \<bullet> evals_aux v t env) = evals_aux (p \<bullet> v) (p \<bullet> t) (p \<bullet> env)" |
99 and "(p \<bullet> evals_aux v s) = evals_aux (p \<bullet> v) (p \<bullet> s)" |
115 sorry |
100 sorry |
116 |
101 |
117 (* fixme: should be a provided lemma *) |
102 (* fixme: should be a provided lemma *) |
118 lemma fv_bn_finite: |
103 lemma fv_bn_finite: |
119 shows "finite (fv_bn env)" |
104 shows "finite (fv_bn env)" |
122 done |
107 done |
123 |
108 |
124 lemma test: |
109 lemma test: |
125 fixes env::"env" |
110 fixes env::"env" |
126 shows "supp (evals env t) \<subseteq> (supp t - set (bn env)) \<union> (fv_bn env)" |
111 shows "supp (evals env t) \<subseteq> (supp t - set (bn env)) \<union> (fv_bn env)" |
127 and "supp (evals_aux s t env) \<subseteq> (supp s) \<union> (fv_bn env) \<union> (supp (t) - set (bn env))" |
112 and "supp (evals_aux s v) \<subseteq> (supp s) \<union> (supp v)" |
128 apply(induct env t and s t env rule: evals_evals_aux.induct) |
113 apply(induct env t and s v rule: evals_evals_aux.induct) |
129 apply(simp add: sem_neu_env.supp lam.supp supp_Nil sem_neu_env.bn_defs) |
114 apply(simp add: sem_neu_env.supp lam.supp supp_Nil sem_neu_env.bn_defs) |
130 apply(simp add: sem_neu_env.supp lam.supp supp_Nil supp_Cons sem_neu_env.bn_defs) |
115 apply(simp add: sem_neu_env.supp lam.supp supp_Nil supp_Cons sem_neu_env.bn_defs) |
131 apply(rule conjI) |
116 apply(rule conjI) |
132 apply(auto)[1] |
117 apply(auto)[1] |
133 apply(rule impI) |
118 apply(rule impI) |
278 apply(simp add: flip_fresh_fresh fresh_Pair) |
259 apply(simp add: flip_fresh_fresh fresh_Pair) |
279 apply(drule_tac q="(xa \<leftrightarrow> c)" in eqvt_at_perm) |
260 apply(drule_tac q="(xa \<leftrightarrow> c)" in eqvt_at_perm) |
280 apply(perm_simp) |
261 apply(perm_simp) |
281 apply(simp add: flip_fresh_fresh fresh_Pair) |
262 apply(simp add: flip_fresh_fresh fresh_Pair) |
282 apply(drule sym) |
263 apply(drule sym) |
|
264 (* HERE *) |
|
265 apply(rotate_tac 9) |
|
266 apply(drule sym) |
283 apply(rotate_tac 9) |
267 apply(rotate_tac 9) |
284 apply(drule trans) |
268 apply(drule trans) |
285 apply(rule sym) |
269 apply(rule sym) |
286 (* HERE *) |
|
287 |
|
288 apply(rule_tac p="p" in supp_perm_eq) |
270 apply(rule_tac p="p" in supp_perm_eq) |
289 apply(simp) |
271 apply(assumption) |
290 apply(perm_simp) |
272 apply(simp) |
291 apply(simp add: Abs_eq_iff2 alphas) |
273 apply(perm_simp) |
|
274 apply(simp (no_asm_use) add: Abs_eq_iff2 alphas) |
|
275 apply(erule conjE | erule exE)+ |
292 apply(clarify) |
276 apply(clarify) |
293 apply(rule trans) |
277 apply(rule trans) |
294 apply(rule sym) |
278 apply(rule sym) |
295 apply(rule_tac p="pa" in perm_supp_eq) |
279 apply(rule_tac p="pa" in perm_supp_eq) |
296 defer |
280 defer |