--- a/Nominal/Ex/Lambda.thy	Mon Jun 06 13:11:04 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Jun 07 08:52:59 2011 +0100
@@ -47,6 +47,51 @@
 apply(simp add: swap_commute)
 done
 
+nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
+  frees_set :: "lam \<Rightarrow> atom set"
+where
+  "frees_set (Var x) = {atom x}"
+| "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2"
+| "frees_set (Lam [x]. t) = (frees_set t) - {atom x}"
+apply(simp add: eqvt_def frees_set_graph_def)
+apply (rule, perm_simp, rule)
+apply(erule frees_set_graph.induct)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(rule_tac y="x" in lam.exhaust)
+apply(auto)[6]
+apply(simp)
+apply(simp)
+apply(simp)
+apply (erule Abs1_eq_fdest)
+apply(simp add: fresh_def)
+apply(subst supp_of_finite_sets)
+apply(simp)
+apply(simp add: supp_atom)
+apply(simp add: fresh_def)
+apply(subst supp_of_finite_sets)
+apply(simp)
+apply(simp add: supp_atom)
+apply(subst  supp_finite_atom_set[symmetric])
+apply(simp)
+apply(simp add: fresh_def[symmetric])
+apply(rule fresh_eqvt_at)
+apply(assumption)
+apply(simp add: finite_supp)
+apply(simp)
+apply(simp add: eqvt_at_def eqvts)
+apply(simp)
+done
+
+print_theorems
+
+termination 
+  by (relation "measure size") (auto simp add: lam.size)
+
+
+thm frees_set.simps
+
 lemma fresh_fun_eqvt_app3:
   assumes a: "eqvt f"
   and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z"
@@ -72,6 +117,7 @@
   apply (simp add: eqvt_def f_graph_def)
   apply (perm_simp)
   apply(simp add: eq[simplified eqvt_def])
+  apply(rule TrueI)
   apply(rule_tac y="x" in lam.exhaust)
   apply(auto simp add: fresh_star_def)
   apply(erule Abs1_eq_fdest)
@@ -91,6 +137,8 @@
 termination
   by (relation "measure size") (auto simp add: lam.size)
 
+thm f.simps
+
 end