diff -r c55aa6cb1518 -r 6e518b436740 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Jun 01 13:35:37 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 01 13:41:30 2011 +0900
@@ -407,70 +407,49 @@
   apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base)
   done
 
-nominal_primrec
-  trans :: "lam \<Rightarrow> name list \<Rightarrow> nat \<Rightarrow> db option"
+fun
+  vindex :: "name list \<Rightarrow> name \<Rightarrow> nat \<Rightarrow> db option" 
 where
-  "trans (Var x) [] n = None"
-| "trans (Var x) (h # t) n =
-     (if h = x then Some (DBVar n) else trans (Var x) t (n + 1))"
-| "trans (App t1 t2) xs n = dbapp_in (trans t1 xs n) (trans t2 xs n)"
-| "x \<notin> set xs \<Longrightarrow> trans (Lam [x].t) xs n = dblam_in (trans t (x # xs) n)"
+  "vindex [] v n = None"
+| "vindex (h # t) v n = (if v = h then (Some (DBVar n)) else (vindex t v (Suc n)))"
+
+lemma vindex_eqvt[eqvt]:
+  "(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)"
+  by (induct l arbitrary: n) (simp_all add: permute_pure)
+
+nominal_primrec
+  trans :: "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
   apply (rule, perm_simp, rule)
   apply (case_tac x)
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
-  apply (case_tac b)
   apply (auto simp add: fresh_star_def fresh_at_list)
   apply (rule_tac f="dblam_in" in arg_cong)
   apply (erule Abs1_eq_fdest)
   apply (simp_all add: pure_fresh)
   apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")
-  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> na = na")
   apply (simp add: eqvt_at_def)
-  apply (simp add: permute_pure)
   apply (metis atom_name_def swap_fresh_fresh fresh_at_list)
   done
 
 termination
-  apply (relation "measure (\<lambda>(t,l,_). size t + size t + length l)")
-  apply (simp_all add: lam.size)
-  done
+  by (relation "measure (\<lambda>(t,_). size t)") (simp_all add: lam.size)
 
 lemma trans_eqvt[eqvt]:
-  "p \<bullet> trans t l n = trans (p \<bullet>t) (p \<bullet>l) (p \<bullet>n)"
-proof (nominal_induct t avoiding: l p arbitrary: n rule: lam.strong_induct)
-  fix name l n p
-  show "p \<bullet> trans (Var name) l n =
-       trans (p \<bullet> Var name) (p \<bullet> l) (p \<bullet> n)"
-    apply (induct l arbitrary: n)
-    apply simp
-    apply auto
-    apply (simp add: permute_pure)
-    done
-next
-  fix lam1 lam2 l n p
-  assume 
-    "\<And>b ba n. ba \<bullet> trans lam1 b n = trans (ba \<bullet> lam1) (ba \<bullet> b) (ba \<bullet> n)"
-  "  \<And>b ba n. ba \<bullet> trans lam2 b n = trans (ba \<bullet> lam2) (ba \<bullet> b) (ba \<bullet> n)"
-  then show "p \<bullet> trans (App lam1 lam2) l n =
-          trans (p \<bullet> App lam1 lam2) (p \<bullet> l) (p \<bullet> n)"
-    by (simp add: db_in_eqvt)
-next
-  fix name :: name and l :: "name list" and p :: perm
-  fix lam n
-  assume
-    "atom name \<sharp> l"
-    "atom name \<sharp> p"
-    "\<And>b ba n. ba \<bullet> trans lam b n = trans (ba \<bullet> lam) (ba \<bullet> b) (ba \<bullet> n)"
-  then show
-    "p \<bullet> trans (Lam [name]. lam) l n =
-          trans (p \<bullet> Lam [name]. lam) (p \<bullet> l) (p \<bullet> n)"
+  "p \<bullet> trans t l = trans (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 (simp add: fresh_at_list[symmetric])
-  apply (simp add: db_in_eqvt)
+  apply (drule_tac x="name # l" in meta_spec)
+  apply auto
   done
-qed
 
 lemma db_trans_test:
   assumes a: "y \<noteq> x"