52 apply(metis)+ |
87 apply(metis)+ |
53 --"compatibility" |
88 --"compatibility" |
54 apply(all_trivials) |
89 apply(all_trivials) |
55 apply(simp) |
90 apply(simp) |
56 apply(simp) |
91 apply(simp) |
|
92 defer |
57 apply(simp) |
93 apply(simp) |
58 apply(simp) |
94 apply(simp) |
59 apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff]) |
95 apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff]) |
60 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva x (evals enva t2a), t)") |
96 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenv x (evals enva t2a), t)") |
61 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (enva, t2a)") |
97 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (enva, t2a)") |
62 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa (evals enva t2a), ta)") |
98 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa (evals enva t2a), ta)") |
63 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva x (evals enva t2a), t))") |
99 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenv x (evals enva t2a), t))") |
64 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))") |
100 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))") |
65 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))") |
101 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))") |
66 apply(erule conjE)+ |
102 apply(erule conjE)+ |
67 defer |
103 defer |
68 apply (simp_all add: eqvt_at_def evals_def)[3] |
104 apply (simp_all add: eqvt_at_def evals_def)[3] |
69 apply(simp) |
105 apply(simp) |
70 defer |
|
71 apply(erule_tac c="(cenv, env)" in Abs_lst1_fcb2') |
|
72 apply(rule fresh_eqvt_at) |
|
73 back |
|
74 apply(simp add: eqvt_at_def) |
|
75 sorry |
106 sorry |
76 |
107 |
77 (* can probably not proved by a trivial size argument *) |
108 (* can probably not proved by a trivial size argument *) |
78 termination sorry |
109 termination sorry |
|
110 |
|
111 lemma [eqvt]: |
|
112 shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)" |
|
113 and "(p \<bullet> evals_aux v t env) = evals_aux (p \<bullet> v) (p \<bullet> t) (p \<bullet> env)" |
|
114 sorry |
|
115 |
|
116 (* fixme: should be a provided lemma *) |
|
117 lemma fv_bn_finite: |
|
118 shows "finite (fv_bn env)" |
|
119 apply(induct env rule: sem_neu_env.inducts(3)) |
|
120 apply(auto simp add: sem_neu_env.supp finite_supp) |
|
121 done |
|
122 |
|
123 lemma test: |
|
124 shows "supp (evals env t) \<subseteq> (supp t - set (bn env)) \<union> (fv_bn env)" |
|
125 and "supp (evals_aux s t env) \<subseteq> ((supp s) - set (bn cenv)) \<union> supp (fn cenv) \<union> supp (evals env t)" |
|
126 apply(induct rule: evals_evals_aux.induct) |
|
127 apply(simp add: sem_neu_env.supp lam.supp supp_Nil sem_neu_env.bn_defs) |
|
128 apply(simp add: sem_neu_env.supp lam.supp supp_Nil supp_Cons sem_neu_env.bn_defs) |
|
129 apply(rule conjI) |
|
130 apply(auto)[1] |
|
131 apply(rule impI) |
|
132 apply(simp) |
|
133 apply (metis (no_types) at_base_infinite finite_UNIV) |
|
134 apply(simp) |
|
135 apply(subst sem_neu_env.supp) |
|
136 apply(simp add: sem_neu_env.supp lam.supp) |
|
137 apply(auto)[1] |
|
138 apply(simp) |
|
139 apply(metis) |
|
140 sorry |
79 |
141 |
80 nominal_primrec |
142 nominal_primrec |
81 reify :: "sem \<Rightarrow> lam" and |
143 reify :: "sem \<Rightarrow> lam" and |
82 reifyn :: "neu \<Rightarrow> lam" |
144 reifyn :: "neu \<Rightarrow> lam" |
83 where |
145 where |
84 "reify (L env y t) = (fresh_fun (\<lambda>x::name. Lam [x]. (reify (evals (ECons env y (N (V x))) t))))" |
146 "atom x \<sharp> (env, y, t) \<Longrightarrow> reify (L env y t) = Lam [x]. (reify (evals (ECons env y (N (V x))) t))" |
85 | "reify (N n) = reifyn n" |
147 | "reify (N n) = reifyn n" |
86 | "reifyn (V x) = Var x" |
148 | "reifyn (V x) = Var x" |
87 | "reifyn (A n d) = App (reifyn n) (reify d)" |
149 | "reifyn (A n d) = App (reifyn n) (reify d)" |
88 defer |
150 apply(subgoal_tac "\<And>p x y. reify_reifyn_graph x y \<Longrightarrow> reify_reifyn_graph (p \<bullet> x) (p \<bullet> y)") |
89 defer |
151 apply(simp add: eqvt_def) |
|
152 apply(simp add: permute_fun_def) |
|
153 apply(rule allI) |
|
154 apply(rule ext) |
|
155 apply(rule ext) |
|
156 apply(rule iffI) |
|
157 apply(drule_tac x="p" in meta_spec) |
|
158 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
159 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
160 apply(simp add: permute_bool_def) |
|
161 apply(simp add: permute_bool_def) |
|
162 apply(erule reify_reifyn_graph.induct) |
|
163 apply(perm_simp) |
|
164 apply(rule reify_reifyn_graph.intros) |
|
165 apply(rule_tac p="-p" in permute_boolE) |
|
166 apply(perm_simp add: permute_minus_cancel) |
|
167 apply(simp) |
|
168 apply(simp) |
|
169 apply(perm_simp) |
|
170 apply(rule reify_reifyn_graph.intros) |
|
171 apply(simp) |
|
172 apply(perm_simp) |
|
173 apply(rule reify_reifyn_graph.intros) |
|
174 apply(perm_simp) |
|
175 apply(rule reify_reifyn_graph.intros) |
|
176 apply(simp) |
|
177 apply(simp) |
|
178 apply(rule TrueI) |
90 --"completeness" |
179 --"completeness" |
91 apply(case_tac x) |
180 apply(case_tac x) |
92 apply(simp) |
181 apply(simp) |
93 apply(case_tac a rule: sem_neu_env.exhaust(1)) |
182 apply(case_tac a rule: sem_neu_env.exhaust(1)) |
94 apply(metis)+ |
183 apply(subgoal_tac "\<exists>x::name. atom x \<sharp> (env, name, lam)") |
|
184 apply(metis) |
|
185 apply(rule obtain_fresh) |
|
186 apply(blast) |
|
187 apply(blast) |
95 apply(case_tac b rule: sem_neu_env.exhaust(2)) |
188 apply(case_tac b rule: sem_neu_env.exhaust(2)) |
96 apply(simp) |
189 apply(simp) |
97 apply(simp) |
190 apply(simp) |
98 apply(metis) |
191 apply(metis) |
99 --"compatibility" |
192 --"compatibility" |
100 apply(all_trivials) |
193 apply(all_trivials) |
101 defer |
194 defer |
102 apply(simp) |
195 apply(simp) |
103 apply(simp) |
196 apply(simp) |
|
197 apply(simp) |
|
198 apply(erule conjE) |
|
199 apply (simp add: meta_eq_to_obj_eq[OF reify_def, symmetric, unfolded fun_eq_iff]) |
|
200 apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva y (N (V x))) t)") |
|
201 apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva ya (N (V xa))) ta)") |
|
202 apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva y (N (V x))) t))") |
|
203 apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva ya (N (V xa))) ta))") |
|
204 defer |
|
205 apply (simp_all add: eqvt_at_def reify_def)[2] |
|
206 apply(subgoal_tac "\<exists>c::name. atom c \<sharp> (x, xa, enva, y, ya, t, ta)") |
|
207 prefer 2 |
|
208 apply(rule obtain_fresh) |
|
209 apply(blast) |
|
210 apply(erule exE) |
|
211 apply(rule trans) |
|
212 apply(rule sym) |
|
213 apply(rule_tac a="x" and b="c" in flip_fresh_fresh) |
|
214 apply(simp add: Abs_fresh_iff) |
|
215 apply(simp add: Abs_fresh_iff fresh_Pair) |
|
216 apply(auto)[1] |
|
217 apply(rule fresh_eqvt_at) |
|
218 back |
|
219 apply(assumption) |
|
220 apply(simp add: finite_supp) |
|
221 apply(rule_tac S="supp (enva, y, x, t)" in supports_fresh) |
|
222 apply(simp add: supports_def fresh_def[symmetric]) |
|
223 apply(perm_simp) |
|
224 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
225 apply(simp add: finite_supp) |
|
226 apply(simp add: fresh_def[symmetric]) |
|
227 apply(simp add: eqvt_at_def) |
|
228 apply(simp add: eqvt_at_def[symmetric]) |
|
229 apply(perm_simp) |
|
230 apply(simp add: flip_fresh_fresh) |
|
231 apply(rule sym) |
|
232 apply(rule trans) |
|
233 apply(rule sym) |
|
234 apply(rule_tac a="xa" and b="c" in flip_fresh_fresh) |
|
235 apply(simp add: Abs_fresh_iff) |
|
236 apply(simp add: Abs_fresh_iff fresh_Pair) |
|
237 apply(auto)[1] |
|
238 apply(rule fresh_eqvt_at) |
|
239 back |
|
240 apply(assumption) |
|
241 apply(simp add: finite_supp) |
|
242 apply(rule_tac S="supp (enva, ya, xa, ta)" in supports_fresh) |
|
243 apply(simp add: supports_def fresh_def[symmetric]) |
|
244 apply(perm_simp) |
|
245 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
246 apply(simp add: finite_supp) |
|
247 apply(simp add: fresh_def[symmetric]) |
|
248 apply(simp add: eqvt_at_def) |
|
249 apply(simp add: eqvt_at_def[symmetric]) |
|
250 apply(perm_simp) |
|
251 apply(simp add: flip_fresh_fresh) |
|
252 apply(simp (no_asm) add: Abs1_eq_iff) |
|
253 apply(rule sym) |
|
254 apply(erule_tac Abs_lst1_fcb2') |
|
255 apply(rule fresh_eqvt_at) |
|
256 back |
|
257 apply(drule_tac q="(c \<leftrightarrow> x)" in eqvt_at_perm) |
|
258 apply(perm_simp) |
|
259 apply(simp add: flip_fresh_fresh) |
|
260 apply(simp add: finite_supp) |
|
261 apply(rule supports_fresh) |
|
262 apply(rule_tac S="supp (enva, ya, xa, ta)" in supports_fresh) |
|
263 apply(simp add: supports_def fresh_def[symmetric]) |
|
264 apply(perm_simp) |
|
265 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
266 apply(simp add: finite_supp) |
|
267 apply(simp add: fresh_def[symmetric]) |
|
268 apply(simp add: eqvt_at_def) |
|
269 apply(simp add: eqvt_at_def[symmetric]) |
|
270 apply(perm_simp) |
|
271 apply(rule fresh_eqvt_at) |
|
272 back |
|
273 apply(drule_tac q="(c \<leftrightarrow> x)" in eqvt_at_perm) |
|
274 apply(perm_simp) |
|
275 apply(simp add: flip_fresh_fresh) |
|
276 apply(assumption) |
|
277 apply(simp add: finite_supp) |
104 sorry |
278 sorry |
105 |
279 |
106 termination sorry |
280 termination sorry |
107 |
281 |
108 definition |
282 definition |