--- a/Nominal/Ex/Lambda.thy	Tue Jul 05 09:26:20 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue Jul 05 09:28:16 2011 +0900
@@ -789,6 +789,47 @@
 
 termination by lexicographic_order
 
+lemma abs_same_binder:
+  fixes t ta s sa :: "_ :: fs"
+  assumes "sort_of (atom x) = sort_of (atom y)"
+  shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa
+     \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)"
+  by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair)
+
+nominal_primrec
+  aux2 :: "lam \<Rightarrow> lam \<Rightarrow> bool"
+where
+  "aux2 (Var x) (Var y) = (x = y)"
+| "aux2 (App t1 t2) (App s1 s2) = (aux2 t1 s1 \<and> aux2 t2 s2)"
+| "aux2 (Var x) (App t1 t2) = False"
+| "aux2 (Var x) (Lam [y].t) = False"
+| "aux2 (App t1 t2) (Var x) = False"
+| "aux2 (App t1 t2) (Lam [x].t) = False"
+| "aux2 (Lam [x].t) (Var y) = False"
+| "aux2 (Lam [x].t) (App t1 t2) = False"
+| "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s"
+  apply(simp add: eqvt_def aux2_graph_def)
+  apply(rule, perm_simp, rule, rule)
+  apply(case_tac x)
+  apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
+  apply(rule_tac y="b" in lam.exhaust)
+  apply(auto)[3]
+  apply(rule_tac y="b" in lam.exhaust)
+  apply(auto)[3]
+  apply(rule_tac y="b" and c="(name, lam)" in lam.strong_exhaust)
+  apply(auto)[3]
+  apply(drule_tac x="name" in meta_spec)
+  apply(drule_tac x="name" in meta_spec)
+  apply(drule_tac x="lam" in meta_spec)
+  apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec)
+  apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base lam.fresh flip_def)
+  apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2))
+  apply simp_all
+  apply (simp add: abs_same_binder)
+  apply (erule_tac c="()" in Abs_lst1_fcb2)
+  apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)
+  done
+
 text {* tests of functions containing if and case *}
 
 consts P :: "lam \<Rightarrow> bool"