--- a/Nominal/Ex/Lambda.thy	Tue Jan 18 06:55:18 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Jan 18 11:02:57 2011 +0100
@@ -102,6 +102,58 @@
 apply(simp_all add: lam.supp supp_at_base)
 done
 
+nominal_datatype ln = 
+  LNBnd nat
+| LNVar name
+| LNApp ln ln
+| LNLam ln
+
+fun
+  lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" 
+where
+  "lookup [] n x = LNVar x"
+| "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
+
+lemma [eqvt]:
+  shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
+apply(induct xs arbitrary: n)
+apply(simp_all add: permute_pure)
+done
+
+nominal_primrec
+  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))"
+apply(case_tac x)
+apply(simp)
+apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
+apply(simp_all)[3]
+apply(blast)
+apply(blast)
+apply(simp add: fresh_star_def)
+apply(simp_all add: lam.distinct)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: Abs_eq_iff)
+apply(erule conjE)
+apply(erule exE)
+apply(simp add: alphas)
+apply(simp add: atom_eqvt)
+apply(clarify)
+apply(rule trans)
+apply(rule_tac p="p" in supp_perm_eq[symmetric])
+apply(simp (no_asm) add: ln.supp)
+apply(drule supp_eqvt_at)
+apply(simp add: finite_supp)
+oops
+
+
+
+
+
 nominal_datatype db = 
   DBVar nat
 | DBApp db db
@@ -112,7 +164,6 @@
 where  
   "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v"
 
-
 lemma mbind_eqvt:
   fixes c::"'a::pt option"
   shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))"