60 apply(simp (no_asm_use) only: eqvts) |
60 apply(simp (no_asm_use) only: eqvts) |
61 apply(subst (asm) permute_fun_app_eq) |
61 apply(subst (asm) permute_fun_app_eq) |
62 back |
62 back |
63 apply(simp) |
63 apply(simp) |
64 done |
64 done |
|
65 |
|
66 lemma helper: |
|
67 assumes "A - C = A - D" |
|
68 and "B - C = B - D" |
|
69 and "E \<subseteq> A \<union> B" |
|
70 shows "E - C = E - D" |
|
71 using assms |
|
72 by blast |
65 |
73 |
66 nominal_primrec |
74 nominal_primrec |
67 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
75 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
68 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
76 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
69 where |
77 where |
222 apply clarify |
230 apply clarify |
223 --"This is exactly the assumption for the properly defined function" |
231 --"This is exactly the assumption for the properly defined function" |
224 defer |
232 defer |
225 apply (simp add: ty_tys.eq_iff) |
233 apply (simp add: ty_tys.eq_iff) |
226 apply (simp only: Abs_eq_res_set) |
234 apply (simp only: Abs_eq_res_set) |
227 apply (subgoal_tac "(atom ` fset xsa \<inter> supp T - atom ` fset xs \<inter> supp Ta) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)") |
235 apply (subgoal_tac "(atom ` fset xsa \<inter> supp Ta - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)") |
228 apply (subst (asm) Abs_eq_iff2) |
236 apply (subst (asm) Abs_eq_iff2) |
229 apply (clarify) |
237 apply (clarify) |
230 apply (simp add: alphas) |
238 apply (simp add: alphas) |
231 apply (clarify) |
239 apply (clarify) |
232 apply (rule trans) |
240 apply (rule trans) |
258 apply (simp add: fresh_def) |
266 apply (simp add: fresh_def) |
259 apply(drule_tac a="atom x" in fresh_eqvt_at) |
267 apply(drule_tac a="atom x" in fresh_eqvt_at) |
260 apply (simp add: supp_Pair finite_supp) |
268 apply (simp add: supp_Pair finite_supp) |
261 apply (simp add: fresh_Pair) |
269 apply (simp add: fresh_Pair) |
262 apply(auto simp add: Abs_fresh_iff fresh_star_def)[1] |
270 apply(auto simp add: Abs_fresh_iff fresh_star_def)[1] |
263 prefer 2 |
|
264 apply auto[1] |
271 apply auto[1] |
265 apply (erule_tac x="atom x" in ballE) |
|
266 apply auto[1] |
|
267 apply (auto simp add: fresh_def)[1] |
|
268 |
272 |
269 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
273 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
270 prefer 2 |
274 prefer 2 |
271 apply (rule perm_supp_eq) |
275 apply (rule perm_supp_eq) |
272 apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* \<theta>'") |
276 apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* \<theta>'") |
273 apply (auto simp add: fresh_star_def)[1] |
277 apply (auto simp add: fresh_star_def)[1] |
274 apply (simp add: fresh_star_Un fresh_star_def) |
278 apply (simp add: fresh_star_Un fresh_star_def) |
275 apply blast |
279 apply blast |
276 apply(simp add: eqvt_at_def inter_eqvt supp_eqvt) |
280 apply(simp add: eqvt_at_def inter_eqvt supp_eqvt) |
277 apply (simp only: Abs_eq_res_set[symmetric]) |
281 apply (simp only: Abs_eq_res_set[symmetric]) |
278 |
282 apply (simp add: Abs_eq_iff alphas) |
279 apply (rule_tac s="[p \<bullet> atom ` fset xs \<inter> supp (\<theta>', p \<bullet> T)]res. subst \<theta>' (p \<bullet> T)" in trans) |
283 apply rule |
280 --"What if (p \<bullet> xs) is not fresh for \<theta>' ?" |
284 prefer 2 |
|
285 apply (rule_tac x="0 :: perm" in exI) |
|
286 apply (simp add: fresh_star_zero) |
|
287 apply (rule helper) |
|
288 prefer 3 |
|
289 apply (subgoal_tac "supp ((\<lambda>(l, r). subst l r) (\<theta>', (p \<bullet> T))) \<subseteq> supp \<theta>' \<union> supp (p \<bullet> T)") |
|
290 apply simp |
|
291 apply (subst supp_Pair[symmetric]) |
|
292 apply (rule supp_eqvt_at) |
|
293 apply (simp add: eqvt_at_def) |
|
294 defer --"because eqvt_at Ta" |
|
295 apply (simp add: supp_Pair finite_supp) |
|
296 prefer 2 apply blast |
|
297 prefer 2 apply (metis finite_UNIV finite_imageI obtain_at_base rangeI) |
|
298 --"p and xs and xsa are fresh for theta" |
281 oops |
299 oops |
282 |
|
283 |
300 |
284 section {* defined as two separate nominal datatypes *} |
301 section {* defined as two separate nominal datatypes *} |
285 |
302 |
286 nominal_datatype ty2 = |
303 nominal_datatype ty2 = |
287 Var2 "name" |
304 Var2 "name" |