434 |
434 |
435 lemma [eqvt]: |
435 lemma [eqvt]: |
436 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
436 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) |
437 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
438 |
438 |
439 nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y") |
439 nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y") |
440 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
440 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
441 where |
441 where |
442 "trans (Var x) xs = lookup xs 0 x" |
442 "trans (Var x) xs = lookup xs 0 x" |
443 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
443 | "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))" |
444 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
445 apply(simp add: eqvt_def trans_graph_def) |
445 apply(simp add: eqvt_def trans_graph_def) |
446 apply (rule, perm_simp, rule) |
446 apply (rule, perm_simp, rule) |
447 apply (erule trans_graph.induct) |
447 apply (erule trans_graph.induct) |
|
448 apply(simp) |
448 apply (case_tac "xa \<in> set xs") |
449 apply (case_tac "xa \<in> set xs") |
449 apply (simp add: fresh_star_def fresh_def supp_lookup_in) |
450 apply (simp add: fresh_star_def fresh_def supp_lookup_in) |
450 apply (simp add: fresh_star_def fresh_def supp_lookup_notin) |
451 apply (simp add: fresh_star_def fresh_def supp_lookup_notin) |
451 apply blast |
452 apply blast |
452 apply (simp add: fresh_star_def ln.fresh) |
453 apply (simp add: fresh_star_def ln.fresh) |
|
454 apply(simp) |
453 apply (simp add: ln.fresh fresh_star_def) |
455 apply (simp add: ln.fresh fresh_star_def) |
454 apply(case_tac x) |
456 apply(case_tac x) |
455 apply(simp) |
457 apply(simp) |
456 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
458 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
457 apply(simp_all add: fresh_star_def)[3] |
459 apply(simp_all add: fresh_star_def)[3] |