293 lemma lookup2_eqvt[eqvt]: |
293 lemma lookup2_eqvt[eqvt]: |
294 shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)" |
294 shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)" |
295 by (induct Ts T rule: lookup2.induct) simp_all |
295 by (induct Ts T rule: lookup2.induct) simp_all |
296 |
296 |
297 nominal_primrec |
297 nominal_primrec |
298 subst :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2" |
298 subst2 :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2" |
299 where |
299 where |
300 "subst \<theta> (Var2 X) = lookup2 \<theta> X" |
300 "subst2 \<theta> (Var2 X) = lookup2 \<theta> X" |
301 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)" |
301 | "subst2 \<theta> (Fun2 T1 T2) = Fun2 (subst2 \<theta> T1) (subst2 \<theta> T2)" |
302 unfolding eqvt_def subst_graph_def |
302 unfolding eqvt_def subst2_graph_def |
303 apply (rule, perm_simp, rule) |
303 apply (rule, perm_simp, rule) |
304 apply(rule TrueI) |
304 apply(rule TrueI) |
305 apply(case_tac x) |
305 apply(case_tac x) |
306 apply(rule_tac y="b" in ty2.exhaust) |
306 apply(rule_tac y="b" in ty2.exhaust) |
307 apply(blast) |
307 apply(blast) |
308 apply(blast) |
308 apply(blast) |
309 apply(simp_all add: ty2.distinct) |
309 apply(simp_all add: ty2.distinct) |
310 done |
310 done |
311 |
311 |
312 termination |
312 termination |
313 by (relation "measure (size o snd)") (simp_all add: ty2.size) |
313 by lexicographic_order |
314 |
314 |
315 lemma subst_eqvt[eqvt]: |
315 lemma subst_eqvt[eqvt]: |
316 shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)" |
316 shows "(p \<bullet> subst2 \<theta> T) = subst2 (p \<bullet> \<theta>) (p \<bullet> T)" |
317 by (induct \<theta> T rule: subst.induct) (simp_all add: lookup2_eqvt) |
317 by (induct \<theta> T rule: subst2.induct) (simp_all add: lookup2_eqvt) |
318 |
318 |
319 lemma supp_fun_app2_eqvt: |
319 lemma supp_fun_app2_eqvt: |
320 assumes e: "eqvt f" |
320 assumes e: "eqvt f" |
321 shows "supp (f a b) \<subseteq> supp a \<union> supp b" |
321 shows "supp (f a b) \<subseteq> supp a \<union> supp b" |
322 using supp_fun_app_eqvt[OF e] supp_fun_app |
322 using supp_fun_app_eqvt[OF e] supp_fun_app |
323 by blast |
323 by blast |
324 |
324 |
325 lemma supp_subst: |
325 lemma supp_subst: |
326 "supp (subst \<theta> t) \<subseteq> supp \<theta> \<union> supp t" |
326 "supp (subst2 \<theta> t) \<subseteq> supp \<theta> \<union> supp t" |
327 apply (rule supp_fun_app2_eqvt) |
327 apply (rule supp_fun_app2_eqvt) |
328 unfolding eqvt_def by (simp add: eqvts_raw) |
328 unfolding eqvt_def by (simp add: eqvts_raw) |
329 |
329 |
330 lemma fresh_star_inter1: |
330 lemma fresh_star_inter1: |
331 "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z" |
331 "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z" |
332 unfolding fresh_star_def by blast |
332 unfolding fresh_star_def by blast |
333 |
333 |
334 nominal_primrec |
334 nominal_primrec |
335 substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2" |
335 substs2 :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2" |
336 where |
336 where |
337 "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)" |
337 "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs2 \<theta> (All2 xs t) = All2 xs (subst2 \<theta> t)" |
338 unfolding eqvt_def substs_graph_def |
338 unfolding eqvt_def substs2_graph_def |
339 apply (rule, perm_simp, rule) |
339 apply (rule, perm_simp, rule) |
340 apply auto[2] |
340 apply auto[2] |
341 apply (rule_tac y="b" and c="a" in tys2.strong_exhaust) |
341 apply (rule_tac y="b" and c="a" in tys2.strong_exhaust) |
342 apply auto |
342 apply auto |
343 apply (erule Abs_res_fcb) |
343 apply (erule Abs_res_fcb) |
352 apply (simp add: subst_eqvt) |
352 apply (simp add: subst_eqvt) |
353 apply (subst Abs_eq_iff) |
353 apply (subst Abs_eq_iff) |
354 apply (rule_tac x="0::perm" in exI) |
354 apply (rule_tac x="0::perm" in exI) |
355 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
355 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
356 apply (simp add: alphas fresh_star_zero) |
356 apply (simp add: alphas fresh_star_zero) |
357 apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa") |
357 apply (subgoal_tac "\<And>x. x \<in> supp (subst2 \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa") |
358 apply blast |
358 apply blast |
359 apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)") |
359 apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)") |
360 apply (simp add: supp_Pair eqvts eqvts_raw) |
360 apply (simp add: supp_Pair eqvts eqvts_raw) |
361 apply auto[1] |
361 apply auto[1] |
362 apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'") |
362 apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'") |