792 lemma abs_same_binder:

   793   fixes t ta s sa :: "_ :: fs"

   794   assumes "sort_of (atom x) = sort_of (atom y)"

   795   shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa

   796      \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)"

   797   by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair)

   798 

   799 nominal_primrec

   800   aux2 :: "lam \<Rightarrow> lam \<Rightarrow> bool"

   801 where

   802   "aux2 (Var x) (Var y) = (x = y)"

   803 | "aux2 (App t1 t2) (App s1 s2) = (aux2 t1 s1 \<and> aux2 t2 s2)"

   804 | "aux2 (Var x) (App t1 t2) = False"

   805 | "aux2 (Var x) (Lam [y].t) = False"

   806 | "aux2 (App t1 t2) (Var x) = False"

   807 | "aux2 (App t1 t2) (Lam [x].t) = False"

   808 | "aux2 (Lam [x].t) (Var y) = False"

   809 | "aux2 (Lam [x].t) (App t1 t2) = False"

   810 | "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s"

   811   apply(simp add: eqvt_def aux2_graph_def)

   812   apply(rule, perm_simp, rule, rule)

   813   apply(case_tac x)

   814   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)

   815   apply(rule_tac y="b" in lam.exhaust)

   816   apply(auto)[3]

   817   apply(rule_tac y="b" in lam.exhaust)

   818   apply(auto)[3]

   819   apply(rule_tac y="b" and c="(name, lam)" in lam.strong_exhaust)

   820   apply(auto)[3]

   821   apply(drule_tac x="name" in meta_spec)

   822   apply(drule_tac x="name" in meta_spec)

   823   apply(drule_tac x="lam" in meta_spec)

   824   apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec)

   825   apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base lam.fresh flip_def)

   826   apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2))

   827   apply simp_all

   828   apply (simp add: abs_same_binder)

   829   apply (erule_tac c="()" in Abs_lst1_fcb2)

   830   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)

   831   done

   832