--- a/Nominal/Ex/Lambda.thy	Tue Jun 07 08:52:59 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Jun 07 10:40:06 2011 +0100
@@ -84,13 +84,16 @@
 apply(simp)
 done
 
-print_theorems
-
 termination 
   by (relation "measure size") (auto simp add: lam.size)
 
+thm frees_set.simps
+thm frees_set.induct
 
-thm frees_set.simps
+lemma "frees_set t = supp t"
+apply(induct rule: frees_set.induct)
+apply(simp_all add: lam.supp supp_at_base)
+done
 
 lemma fresh_fun_eqvt_app3:
   assumes a: "eqvt f"
@@ -159,8 +162,6 @@
 
 thm hei.f.simps
 
-
-
 inductive 
   triv :: "lam \<Rightarrow> nat \<Rightarrow> bool"
 where
@@ -207,6 +208,7 @@
 | "height (Lam [x].t) = height t + 1"
   unfolding eqvt_def height_graph_def
   apply (rule, perm_simp, rule)
+apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply (erule Abs1_eq_fdest)
@@ -229,6 +231,7 @@
 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
   unfolding eqvt_def frees_lst_graph_def
   apply (rule, perm_simp, rule)
+apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)
 apply (erule Abs1_eq_fdest)
@@ -258,6 +261,7 @@
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
   unfolding eqvt_def subst_graph_def
   apply (rule, perm_simp, rule)
+apply(rule TrueI)
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 apply(blast)+
@@ -413,25 +417,34 @@
   "lookup [] n x = LNVar x"
 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
 
+lemma supp_lookup:
+  shows "supp (lookup xs n x) \<subseteq> supp x"
+  apply(induct arbitrary: n rule: lookup.induct)
+  apply(simp add: ln.supp)
+  apply(simp add: ln.supp pure_supp)
+  done
+  
+
 lemma [eqvt]:
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
-nominal_primrec
+nominal_primrec (invariant "\<lambda>x y. supp y \<subseteq> supp x")
   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
 where
   "trans (Var x) xs = lookup xs 0 x"
 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
-  unfolding eqvt_def trans_graph_def
-  apply (rule, perm_simp, rule)
+apply(simp add: eqvt_def trans_graph_def)
+apply (rule, perm_simp, rule)
+defer
 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 add: lam.distinct lam.eq_iff)
+apply(simp_all)
 apply(elim conjE)
 apply clarify
 apply (erule Abs1_eq_fdest)
@@ -443,6 +456,13 @@
 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)
+apply(simp add: fresh_def)
+defer
+apply(erule trans_graph.induct)
+defer
+apply(simp add: lam.supp ln.supp)
+apply(blast)
+apply(simp add: lam.supp ln.supp)
 oops
 
 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)"
@@ -549,13 +569,14 @@
   by (induct l arbitrary: n) (simp_all add: permute_pure)
 
 nominal_primrec
-  trans :: "lam \<Rightarrow> name list \<Rightarrow> db option"
+  transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option"
 where
-  "trans (Var x) l = vindex l x 0"
-| "trans (App t1 t2) xs = dbapp_in (trans t1 xs) (trans t2 xs)"
-| "x \<notin> set xs \<Longrightarrow> trans (Lam [x].t) xs = dblam_in (trans t (x # xs))"
-  unfolding eqvt_def trans_graph_def
+  "transdb (Var x) l = vindex l x 0"
+| "transdb (App t1 t2) xs = dbapp_in (transdb t1 xs) (transdb t2 xs)"
+| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = dblam_in (transdb t (x # xs))"
+  unfolding eqvt_def transdb_graph_def
   apply (rule, perm_simp, rule)
+  apply(rule TrueI)
   apply (case_tac x)
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply (auto simp add: fresh_star_def fresh_at_list)
@@ -570,13 +591,13 @@
 termination
   by (relation "measure (\<lambda>(t,_). size t)") (simp_all add: lam.size)
 
-lemma trans_eqvt[eqvt]:
-  "p \<bullet> trans t l = trans (p \<bullet>t) (p \<bullet>l)"
+lemma transdb_eqvt[eqvt]:
+  "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)"
   apply (nominal_induct t avoiding: l p rule: lam.strong_induct)
   apply (simp add: vindex_eqvt)
   apply (simp_all add: permute_pure)
   apply (simp add: fresh_at_list)
-  apply (subst trans.simps)
+  apply (subst transdb.simps)
   apply (simp add: fresh_at_list[symmetric])
   apply (drule_tac x="name # l" in meta_spec)
   apply auto
@@ -659,6 +680,7 @@
 | "\<not>eqvt f \<Longrightarrow> map_term f t = t"
   apply (simp add: eqvt_def map_term_graph_def)
   apply (rule, perm_simp, rule)
+  apply(rule TrueI)
   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
   apply auto
   apply (erule Abs1_eq_fdest)