416 where |
416 where |
417 "lookup [] n x = LNVar x" |
417 "lookup [] n x = LNVar x" |
418 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
418 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
419 |
419 |
420 lemma supp_lookup: |
420 lemma supp_lookup: |
421 shows "supp (lookup xs n x) \<subseteq> supp x" |
421 shows "supp (lookup xs n x) \<subseteq> {atom x}" |
422 apply(induct arbitrary: n rule: lookup.induct) |
422 apply(induct arbitrary: n rule: lookup.induct) |
423 apply(simp add: ln.supp) |
423 apply(simp add: ln.supp supp_at_base) |
424 apply(simp add: ln.supp pure_supp) |
424 apply(simp add: ln.supp pure_supp) |
425 done |
425 done |
426 |
426 |
|
427 lemma supp_lookup_in: |
|
428 shows "x \<in> set xs \<Longrightarrow> supp (lookup xs n x) = {}" |
|
429 by (induct arbitrary: n rule: lookup.induct)(auto simp add: ln.supp pure_supp) |
|
430 |
|
431 lemma supp_lookup_notin: |
|
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) |
427 |
434 |
428 lemma [eqvt]: |
435 lemma [eqvt]: |
429 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)" |
430 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
437 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
431 |
438 |
432 nominal_primrec (invariant "\<lambda>x y. supp y \<subseteq> supp x") |
439 nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y") |
433 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
440 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
434 where |
441 where |
435 "trans (Var x) xs = lookup xs 0 x" |
442 "trans (Var x) xs = lookup xs 0 x" |
436 | "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)" |
437 | "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))" |
438 apply(simp add: eqvt_def trans_graph_def) |
445 apply(simp add: eqvt_def trans_graph_def) |
439 apply (rule, perm_simp, rule) |
446 apply (rule, perm_simp, rule) |
440 defer |
447 apply (erule trans_graph.induct) |
|
448 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_notin) |
|
451 apply blast |
|
452 apply (simp add: fresh_star_def ln.fresh) |
|
453 apply (simp add: ln.fresh fresh_star_def) |
441 apply(case_tac x) |
454 apply(case_tac x) |
442 apply(simp) |
455 apply(simp) |
443 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
456 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
444 apply(simp_all add: fresh_star_def)[3] |
457 apply(simp_all add: fresh_star_def)[3] |
445 apply(blast) |
458 apply(blast) |
454 apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2] |
467 apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2] |
455 prefer 2 |
468 prefer 2 |
456 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
469 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
457 apply (simp add: eqvt_at_def) |
470 apply (simp add: eqvt_at_def) |
458 apply (metis atom_name_def swap_fresh_fresh) |
471 apply (metis atom_name_def swap_fresh_fresh) |
459 apply(simp add: fresh_def) |
472 apply(simp add: fresh_star_def) |
460 defer |
473 done |
461 apply(erule trans_graph.induct) |
|
462 defer |
|
463 apply(simp add: lam.supp ln.supp) |
|
464 apply(blast) |
|
465 apply(simp add: lam.supp ln.supp) |
|
466 oops |
|
467 |
474 |
468 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)" |
475 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)" |
469 apply (case_tac "x = xa") |
476 apply (case_tac "x = xa") |
470 apply simp |
477 apply simp |
471 apply (simp add: lam.eq_iff Abs1_eq_iff flip_def[symmetric]) |
478 apply (simp add: lam.eq_iff Abs1_eq_iff flip_def[symmetric]) |