476 |
476 |
477 |
477 |
478 termination |
478 termination |
479 by (relation "measure (size o fst)") (simp_all add: lam.size) |
479 by (relation "measure (size o fst)") (simp_all add: lam.size) |
480 |
480 |
481 nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y") |
481 nominal_primrec |
482 cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat" |
482 cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat" |
483 where |
483 where |
484 "cbvs (Var x) xs = (if x \<in> set xs then 1 else 0)" |
484 "cbvs (Var x) xs = (if x \<in> set xs then 1 else 0)" |
485 | "cbvs (App t1 t2) xs = (cbvs t1 xs) + (cbvs t2 xs)" |
485 | "cbvs (App t1 t2) xs = (cbvs t1 xs) + (cbvs t2 xs)" |
486 | "atom x \<sharp> xs \<Longrightarrow> cbvs (Lam [x]. t) xs = (cbvs t (x # xs))" |
486 | "atom x \<sharp> xs \<Longrightarrow> cbvs (Lam [x]. t) xs = (cbvs t (x # xs))" |
487 apply(simp add: eqvt_def cbvs_graph_def) |
487 apply(simp add: eqvt_def cbvs_graph_def) |
488 apply (rule, perm_simp, rule) |
488 apply(rule, perm_simp, rule) |
489 apply (erule cbvs_graph.induct) |
489 apply(simp_all) |
490 apply(simp add: fresh_star_def pure_fresh) |
490 apply(case_tac x) |
491 apply(simp add: fresh_star_def pure_fresh) |
491 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
492 apply(simp add: fresh_star_def pure_fresh) |
492 apply(auto simp add: fresh_star_def) |
493 apply(case_tac x) |
493 apply(erule Abs1_eq_fdest) |
494 apply(simp) |
494 apply(simp_all add: pure_fresh) |
495 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
495 apply (simp add: eqvt_at_def swap_fresh_fresh) |
496 apply(simp_all add: fresh_star_def)[3] |
496 done |
497 apply(blast) |
|
498 apply(blast) |
|
499 apply(simp_all) |
|
500 apply(elim conjE) |
|
501 apply clarify |
|
502 apply (erule Abs1_eq_fdest) |
|
503 apply (simp_all add: ln.fresh) |
|
504 apply(simp add: fresh_star_def) |
|
505 apply(drule supp_eqvt_at) |
|
506 apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2] |
|
507 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
|
508 apply (simp add: eqvt_at_def) |
|
509 apply (metis atom_name_def swap_fresh_fresh) |
|
510 done |
|
511 |
|
512 |
497 |
513 termination |
498 termination |
514 by (relation "measure (size o fst)") (simp_all add: lam.size) |
499 by (relation "measure (size o fst)") (simp_all add: lam.size) |
515 |
500 |
516 |
501 |