430 |
430 |
431 lemma supp_lookup_notin: |
431 lemma supp_lookup_notin: |
432 shows "x \<notin> set xs \<Longrightarrow> supp (lookup xs n x) = {atom x}" |
432 shows "x \<notin> set xs \<Longrightarrow> supp (lookup xs n x) = {atom x}" |
433 by (induct arbitrary: n rule: lookup.induct) (auto simp add: ln.supp pure_supp supp_at_base) |
433 by (induct arbitrary: n rule: lookup.induct) (auto simp add: ln.supp pure_supp supp_at_base) |
434 |
434 |
435 lemma [eqvt]: |
435 lemma supp_lookup_fresh: |
|
436 shows "atom ` set xs \<sharp>* lookup xs n x" |
|
437 by (case_tac "x \<in> set xs") (auto simp add: fresh_star_def fresh_def supp_lookup_in supp_lookup_notin) |
|
438 |
|
439 lemma lookup_eqvt[eqvt]: |
436 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
440 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
437 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
441 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
438 |
442 |
439 nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y") |
443 nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y") |
440 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
444 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
441 where |
445 where |
442 "trans (Var x) xs = lookup xs 0 x" |
446 "trans (Var x) xs = lookup xs 0 x" |
443 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
447 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
444 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
448 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
445 apply(simp add: eqvt_def trans_graph_def) |
449 apply (simp add: eqvt_def trans_graph_def) |
446 apply (rule, perm_simp, rule) |
450 apply (rule, perm_simp, rule) |
447 apply (erule trans_graph.induct) |
451 apply (erule trans_graph.induct) |
448 apply(simp) |
452 apply (auto simp add: ln.fresh) |
449 apply (case_tac "xa \<in> set xs") |
453 apply (simp add: supp_lookup_fresh) |
450 apply (simp add: fresh_star_def fresh_def supp_lookup_in) |
|
451 apply (simp add: fresh_star_def fresh_def supp_lookup_notin) |
|
452 apply blast |
|
453 apply (simp add: fresh_star_def ln.fresh) |
454 apply (simp add: fresh_star_def ln.fresh) |
454 apply(simp) |
|
455 apply (simp add: ln.fresh fresh_star_def) |
455 apply (simp add: ln.fresh fresh_star_def) |
456 apply(case_tac x) |
456 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
457 apply(simp) |
457 apply (auto simp add: fresh_star_def)[3] |
458 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
458 apply (erule Abs1_eq_fdest) |
459 apply(simp_all add: fresh_star_def)[3] |
459 apply (simp_all add: fresh_star_def) |
460 apply(blast) |
460 apply (drule supp_eqvt_at) |
461 apply(blast) |
461 apply (rule finite_supp) |
462 apply(simp_all) |
462 apply (auto simp add: supp_Pair fresh_def supp_Cons supp_at_base)[1] |
463 apply(elim conjE) |
463 apply (simp add: eqvt_at_def swap_fresh_fresh) |
464 apply clarify |
464 done |
465 apply (erule Abs1_eq_fdest) |
|
466 apply (simp_all add: ln.fresh) |
|
467 prefer 2 |
|
468 apply(drule supp_eqvt_at) |
|
469 apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2] |
|
470 prefer 2 |
|
471 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
|
472 apply (simp add: eqvt_at_def) |
|
473 apply (metis atom_name_def swap_fresh_fresh) |
|
474 apply(simp add: fresh_star_def) |
|
475 done |
|
476 |
465 |
477 |
466 |
478 termination |
467 termination |
479 by (relation "measure (size o fst)") (simp_all add: lam.size) |
468 by (relation "measure (size o fst)") (simp_all add: lam.size) |
480 |
469 |