477 

   478 termination

   479   by (relation "measure (size o fst)") (simp_all add: lam.size)

   480 

   481 nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")

   482   cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"

   483 where

   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)"

   486 | "atom x \<sharp> xs \<Longrightarrow> cbvs (Lam [x]. t) xs = (cbvs t (x # xs))"

   487 apply(simp add: eqvt_def cbvs_graph_def)

   488 apply (rule, perm_simp, rule)

   489   apply (erule cbvs_graph.induct)

   490   apply(simp add: fresh_star_def pure_fresh)

   491   apply(simp add: fresh_star_def pure_fresh)

   492   apply(simp add: fresh_star_def pure_fresh)

   493 apply(case_tac x)

   494 apply(simp)

   495 apply(rule_tac y="a" and c="b" in lam.strong_exhaust)

   496 apply(simp_all add: fresh_star_def)[3]

   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 

   513 termination

   514   by (relation "measure (size o fst)") (simp_all add: lam.size)

   515 

   516