--- a/Nominal/Ex/Lambda.thy	Tue Jun 07 17:45:38 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Jun 07 20:58:00 2011 +0100
@@ -474,6 +474,46 @@
 apply(simp add: fresh_star_def)
 done
 
+
+termination
+  by (relation "measure (size o fst)") (simp_all add: lam.size)
+
+nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
+  cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
+where
+  "cbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
+| "cbvs (App t1 t2) xs = (cbvs t1 xs) + (cbvs t2 xs)"
+| "atom x \<sharp> xs \<Longrightarrow> cbvs (Lam [x]. t) xs = (cbvs t (x # xs))"
+apply(simp add: eqvt_def cbvs_graph_def)
+apply (rule, perm_simp, rule)
+  apply (erule cbvs_graph.induct)
+  apply(simp add: fresh_star_def pure_fresh)
+  apply(simp add: fresh_star_def pure_fresh)
+  apply(simp add: fresh_star_def pure_fresh)
+apply(case_tac x)
+apply(simp)
+apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
+apply(simp_all add: fresh_star_def)[3]
+apply(blast)
+apply(blast)
+apply(simp_all)
+apply(elim conjE)
+apply clarify
+apply (erule Abs1_eq_fdest)
+apply (simp_all add: ln.fresh)
+apply(simp add: fresh_star_def)
+apply(drule supp_eqvt_at)
+apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2]
+apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")
+apply (simp add: eqvt_at_def)
+apply (metis atom_name_def swap_fresh_fresh)
+done
+
+
+termination
+  by (relation "measure (size o fst)") (simp_all add: lam.size)
+
+
 nominal_datatype db = 
   DBVar nat
 | DBApp db db