theory Lambda imports "../Nominal2" begin

atom_decl name

nominal_datatype lam =
  Var "name"
| App "lam" "lam"
| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)

nominal_primrec lookup where
  "lookup (n :: name) m [] \<longleftrightarrow> (n = m)"
| "lookup n m ((hn, hm) # t) \<longleftrightarrow>
     (n, m) = (hn, hm) \<or> (n \<noteq> hn \<and> m \<noteq> hm \<and> lookup n m t)"
  apply (simp add: eqvt_def lookup_graph_def)
  apply (rule, perm_simp, rule, rule)
  by pat_completeness auto

termination (eqvt) by lexicographic_order

nominal_primrec lam2_rec where
  "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs"
| "lam2_rec faa fll xs (Var n) (App l r) = False"
| "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False"
| "lam2_rec faa fll xs (App l r) (Var n) = False"
| "lam2_rec faa fll xs (App l1 r1) (App l2 r2) = faa l1 r1 l2 r2"
| "lam2_rec faa fll xs (App l r) (Lam [x]. t) = False"
| "lam2_rec faa fll xs (Lam [x]. t) (Var n) = False"
| "lam2_rec faa fll xs (Lam [x]. t) (App l1 r1) = False"
| "(atom x \<sharp> (xs, Lam [y]. s) \<and> atom y \<sharp> (x, xs, Lam [x]. t) \<and>
     (\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [x]. t = Lam [x']. t' \<longrightarrow> Lam [y]. s = Lam [y']. s'
        \<longrightarrow> fll x t y s = fll x' t' y' s')) \<Longrightarrow>
     lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = fll x t y s"
| "(atom x \<sharp> (xs, Lam [y]. s) \<and> atom y \<sharp> (x, xs, Lam [x]. t) \<and>
     \<not>(\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [x]. t = Lam [x']. t' \<longrightarrow> Lam [y]. s = Lam [y']. s'
        \<longrightarrow> fll x t y s = fll x' t' y' s')) \<Longrightarrow>
     lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = False"
  apply (simp add: eqvt_def lam2_rec_graph_def)
  apply (rule, perm_simp, rule, rule)
  defer
  apply (simp_all)[53]
  apply clarify
  apply metis
  apply simp
  apply (case_tac x)
  apply (rule_tac y="d" and c="(c, e)" in lam.strong_exhaust)
  apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust)
  apply simp_all[3]
  apply (metis, metis, metis)
  apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust)
  apply simp_all[3]
  apply (metis, metis, metis)
  apply (rule_tac y="e" and c="(name, c, d)" in lam.strong_exhaust)
  apply simp_all[2]
  apply (metis, metis)
  apply (thin_tac "\<And>faa fll xs n m. x = (faa, fll, xs, Var n, Var m) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs n l r. x = (faa, fll, xs, Var n, App l r) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs n xa t. x = (faa, fll, xs, Var n, Lam [xa]. t) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs l1 r1 l2 r2. x = (faa, fll, xs, App l1 r1, App l2 r2) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs l r n. x = (faa, fll, xs, App l r, Var n) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs l r xa t. x = (faa, fll, xs, App l r, Lam [xa]. t) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs xa t n. x = (faa, fll, xs, Lam [xa]. t, Var n) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs xa t l1 r1. x = (faa, fll, xs, Lam [xa]. t, App l1 r1) \<Longrightarrow> P")
  apply (drule_tac x="name" in meta_spec)+
  apply (drule_tac x="c" in meta_spec)+
  apply (drule_tac x="namea" in meta_spec)+
  apply (drule_tac x="lama" in meta_spec)
  apply (drule_tac x="lama" in meta_spec)
  apply (drule_tac x="lam" in meta_spec)+
  apply (drule_tac x="b" in meta_spec)+
  apply (drule_tac x="a" in meta_spec)+
  apply (case_tac "
(\<forall>x' y' t' s'.
             atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow>
             atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow>
             Lam [name]. lam = Lam [x']. t' \<longrightarrow>
             Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s')
  ")
  apply clarify
  apply (simp add: fresh_star_def)
  apply (thin_tac "\<lbrakk>atom name \<sharp> (c, Lam [namea]. lama) \<and>
         atom namea \<sharp> (name, c, Lam [name]. lam) \<and>
         (\<forall>x' y' t' s'.
             atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow>
             atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow>
             Lam [name]. lam = Lam [x']. t' \<longrightarrow>
             Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s');
         x = (a, b, c, Lam [name]. lam, Lam [namea]. lama)\<rbrakk>
        \<Longrightarrow> P")
  apply (simp add: fresh_star_def)
  done

termination (eqvt) by lexicographic_order

lemma lam_rec2_cong[fundef_cong]:
  "(\<And>s1 s2 s3 s4. l = App s1 s2 \<Longrightarrow> l2 = App s3 s4  \<Longrightarrow> faa s1 s2 s3 s4 = faa' s1 s2 s3 s4) \<Longrightarrow>
   (\<And>n t n' t'. l = Lam [n]. t \<Longrightarrow> l2 = Lam [n']. t' \<Longrightarrow> fll n t n' t' = fll' n t n' t') \<Longrightarrow>
  lam2_rec faa fll xs l l2 = lam2_rec faa' fll' xs l l2"
  apply (rule_tac y="l" and c="(xs, l2)" in lam.strong_exhaust)
  apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3]
  apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3]
  apply (rule_tac y="l2" and c="(name, xs, l)" in lam.strong_exhaust)
  apply auto[2]
  apply clarify
  apply (case_tac "(\<forall>x' y' t' s'.
              atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow>
              atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow>
              Lam [name]. lam = Lam [x']. t' \<longrightarrow>
              Lam [namea]. lama = Lam [y']. s' \<longrightarrow>
              fll name lam namea lama = fll x' t' y' s')")
  apply (subst lam2_rec.simps) apply (simp add: fresh_star_def)
  apply (subst lam2_rec.simps) apply (simp add: fresh_star_def)
  using Abs1_eq_iff lam.eq_iff apply metis
  apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def)
  apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def)
  apply rule
  done

nominal_primrec aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"
  where
[simp del]: "aux l r xs = lam2_rec
  (%t1 t2 t3 t4. (aux t1 t3 xs) \<and> (aux t2 t4 xs))
  (%x t y s. aux t s ((x, y) # xs)) xs l r"
  unfolding eqvt_def aux_graph_def
  apply (rule, perm_simp, rule, rule)
  by pat_completeness auto

termination (eqvt)
  by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all

lemma aux_simps[simp]:
  "aux (Var x) (Var y) xs = lookup x y xs"
  "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)"
  "aux (Var x) (App t1 t2) xs = False"
  "aux (Var x) (Lam [y].t) xs = False"
  "aux (App t1 t2) (Var x) xs = False"
  "aux (App t1 t2) (Lam [x].t) xs = False"
  "aux (Lam [x].t) (Var y) xs = False"
  "aux (Lam [x].t) (App t1 t2) xs = False"
  "\<lbrakk>atom x \<sharp> (s, xs); atom y \<sharp> (x, t, xs)\<rbrakk> \<Longrightarrow> aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)"
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps)
  apply (subst lam2_rec.simps)
  prefer 2 apply rule
  apply (rule, simp add: lam.fresh)
  apply (rule, simp add: lam.fresh)
  apply (intro allI impI)
  apply (rule_tac x="(x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh)
  apply (rule_tac x="(a, x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh)
  apply (rule_tac s="aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) s ((a, y) # xs)" in trans)
  apply (rule_tac s="(atom x \<rightleftharpoons> atom a) \<bullet> aux t s ((x, y) # xs)" in trans)
  apply (rule permute_pure[symmetric])
  apply (simp add: eqvts swap_fresh_fresh)
  apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim)
  apply (rename_tac b)
  apply (rule_tac s="aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) ((atom y \<rightleftharpoons> atom b) \<bullet> s) ((a, b) # xs)" in trans)
  apply (rule_tac s="(atom y \<rightleftharpoons> atom b) \<bullet> aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) s ((a, y) # xs)" in trans)
  apply (rule permute_pure[symmetric])
  apply (simp add: eqvts swap_fresh_fresh)
  apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim)
  apply (subst permute_eqvt)
  apply (simp add: eqvts swap_fresh_fresh)
  apply (rule sym)
  apply (rule_tac s="aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') s' ((a, y') # xs)" in trans)
  apply (rule_tac s="(atom x' \<rightleftharpoons> atom a) \<bullet> aux t' s' ((x', y') # xs)" in trans)
  apply (rule permute_pure[symmetric])
  apply (simp add: eqvts swap_fresh_fresh)
  apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim swap_fresh_fresh)
  apply (rule_tac s="aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') ((atom y' \<rightleftharpoons> atom b) \<bullet> s') ((a, b) # xs)" in trans)
  apply (rule_tac s="(atom y' \<rightleftharpoons> atom b) \<bullet> aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') s' ((a, y') # xs)" in trans)
  apply (rule permute_pure[symmetric])
  apply (simp add: eqvts swap_fresh_fresh)
  apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim swap_fresh_fresh)
  apply (subst permute_eqvt)
  apply (simp add: eqvts swap_fresh_fresh)
  apply (subgoal_tac "(atom x' \<rightleftharpoons> atom a) \<bullet> t' = (atom x \<rightleftharpoons> atom a) \<bullet> t")
  apply (subgoal_tac "(atom y' \<rightleftharpoons> atom b) \<bullet> s' = (atom y \<rightleftharpoons> atom b) \<bullet> s")
  apply simp
  apply (subgoal_tac "Lam [y]. s = Lam [b]. ((atom y \<rightleftharpoons> atom b) \<bullet> s)")
  apply (subgoal_tac "Lam [y']. s' = Lam [b]. ((atom y' \<rightleftharpoons> atom b) \<bullet> s')")
  apply (auto simp add: fresh_Pair_elim Abs1_eq_iff)[1]
  apply (rule sym)
  apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
  apply (rule sym)
  apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
  apply (subgoal_tac "Lam [x]. t = Lam [a]. ((atom x \<rightleftharpoons> atom a) \<bullet> t)")
  apply (subgoal_tac "Lam [x']. t' = Lam [a]. ((atom x' \<rightleftharpoons> atom a) \<bullet> t')")
  apply (auto simp add: fresh_Pair_elim Abs1_eq_iff)[1]
  apply (rule sym)
  apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
  apply (rule sym)
  apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
  done

lemma aux_induct:  "\<lbrakk>\<And>xs n m. P xs (Var n) (Var m); \<And>xs n l r. P xs (Var n) (App l r);
 \<And>xs n x t. P xs (Var n) (Lam [x]. t);
 \<And>xs l r n. P xs (App l r) (Var n);
 (\<And>xs l1 r1 l2 r2. P xs l1 l2 \<Longrightarrow> P xs r1 r2 \<Longrightarrow> P xs (App l1 r1) (App l2 r2));
 \<And>xs l r x t. P xs (App l r) (Lam [x]. t);
 \<And>xs x t n. P xs (Lam [x]. t) (Var n);
 \<And>xs x t l1 r1. P xs (Lam [x]. t) (App l1 r1);
 \<And>x xs y s t.
    atom x \<sharp> (xs, Lam [y]. s) \<and>
    atom y \<sharp> (x, xs, Lam [x]. t) \<Longrightarrow> P ((x, y) # xs) t s \<Longrightarrow> P xs (Lam [x]. t) (Lam [y]. s)\<rbrakk>
\<Longrightarrow> P (a :: (name \<times> name) list) b c"
  apply (induction_schema)
  apply (rule_tac y="b" and c="(a, c)" in lam.strong_exhaust)
  apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust)
  apply simp_all[3] apply (metis)
  apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust)
  apply simp_all[3] apply (metis, metis, metis)
  apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust)
  apply simp_all[3] apply (metis)
  apply (simp add: fresh_star_def)
  apply metis
  apply lexicographic_order
  done

lemma foldr_eqvt[eqvt]:
  "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)"
  apply (induct b)
  apply simp_all
  apply (perm_simp)
  apply simp
  done

nominal_primrec
  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
where
  "(Var x)[y ::= s] = (if x = y then s else (Var x))"
| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
| "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)
  apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
  apply(blast)+
  apply(simp_all add: fresh_star_def fresh_Pair_elim)
  apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
  apply(simp_all add: Abs_fresh_iff)
  apply(simp add: fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
done

termination (eqvt) by lexicographic_order

nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where
  "swapequal l r [] \<longleftrightarrow> l = r"
| "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow>
    swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t"
  unfolding eqvt_def swapequal_graph_def
  apply (rule, perm_simp, rule)
  apply(rule TrueI)
  apply (case_tac x)
  apply (case_tac c)
  apply metis
  apply (case_tac aa)
  apply (rename_tac l r lst h t hl hr)
  apply (rule_tac x="(l, r, hl, hr, t)" and ?'a="name" in obtain_fresh)
  apply simp
  apply simp
  apply simp
  sorry

termination (eqvt) by lexicographic_order

lemma lookup_swapequal: "lookup n m xs = swapequal (Var n) (Var m) xs"
  apply (induct xs arbitrary: m n)
  apply simp
  apply (case_tac a)
  apply simp
  apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh)
  apply (subst swapequal.simps)
  apply (simp add: fresh_Pair lam.fresh fresh_Nil)
  apply (case_tac "n = aa \<and> m = b")
  apply simp
  defer
  apply (case_tac "n = aa")
  apply (simp add: fresh_Pair_elim fresh_at_base)
  defer
  apply (simp add: fresh_Pair_elim fresh_at_base flip_def)
  apply (case_tac "m = b")
  apply simp
  defer
  apply simp
  sorry

(*
lemma lookup_property:
  assumes "distinct (map fst xs @ map snd xs)"
  shows "aux (Var n) (Var m) xs = swapequal (Var n) (Var m) xs"
  using assms
  apply (induct xs arbitrary: n m)
  apply simp
  apply simp
  apply (case_tac a)
  apply simp
  apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh)
  apply (subst swapequal.simps)
  apply (simp add: fresh_Pair lam.fresh fresh_Cons)
  apply auto[1]

  apply (case_tac "n = aa \<and> m = b")
  apply simp
proof -
  have "lookup n m xs = (fold (\<lambda>(x, y) t. if n = t then y else t) xs n = m)"
    using assms
    proof (induct xs, simp)
      fix a b xs
      assume d: "distinct (map fst xs @ map snd xs) \<Longrightarrow>
        lookup n m xs = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) xs n = m)"
      assume "distinct (map fst (a # xs) @ map snd (a # xs))"
      then have "lookup n m xs = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) xs n = m)"
        using d by simp
      then show "lookup n m (a # xs) =
          (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) (a # xs) n = m)"
        proof (cases a)
          case (Pair b c)
          assume "lookup n m xs = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) xs n = m)" "a = (b, c)"
          then show "lookup n m (a # xs) = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) (a # xs) n = m)"
            apply simp
            apply auto
            sledgehammer

        apply -
        apply (case_tac a)
        apply auto


    apply simp
    apply (case_tac a)
    apply simp
    apply metis
  also have "... = (Var (foldr (\<lambda>(x, y) t. if n = t then y else t) xs n) = Var m)" by simp
  also have "... = (foldr (\<lambda>(x, y) t. subst t x (Var y)) xs (Var n) = Var m)"
    apply (rule arg_cong) back
    apply (induct xs)
    apply simp
    apply (case_tac a)
    apply simp
    apply auto
    find_theorems "fold _ _ _ = fold _ _ _"
    apply (induct xs) apply simp
    apply simp
  apply (case_tac a)
  apply simp
  apply (simp only: lookup.simps)
  apply simp
  apply clarify
  apply (case_tac "n = aa")
  apply (case_tac "m = ba")
  apply simp
  apply (induct_tac xs)
  apply simp
  apply simp
  sorry*)

lemma reord: "
  a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow>
  swapequal t s ((x, y) # (a, b) # xs) = swapequal t s ((a, b) # (x, y) # xs)"
  sorry

lemma need:
  assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs"
  shows "swapequal (Lam [x]. t) (Lam [y]. s) xs = swapequal t s ((x, y) # xs)"
  using assms
  apply (induct xs arbitrary: t s x y)
  apply (rule_tac x="(x, y, t, s)" and ?'a="name" in obtain_fresh)
  apply (simp add: fresh_Pair_elim fresh_Nil)
  apply (subst swapequal.simps)
  apply (simp add: fresh_Pair fresh_Nil)
  apply auto[1]
  apply simp
  apply (subgoal_tac "[[atom x]]lst. t = [[atom a]]lst. ((x \<leftrightarrow> a) \<bullet> t)")
  apply (subgoal_tac "[[atom y]]lst. s = [[atom a]]lst. ((y \<leftrightarrow> a) \<bullet> s)")
  apply simp
  apply (simp add: Abs1_eq_iff)
  apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[1]
  apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt)
  apply (simp add: Abs1_eq_iff)
  apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[1]
  apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt)
  apply clarify
  apply (simp add: fresh_Cons fresh_Pair fresh_at_base)
  apply clarify
  apply (subst reord)
  apply auto[4]
  apply (rule_tac x="(x, y, t, s, a, b, xs)" and ?'a="name" in obtain_fresh)
  apply (rename_tac f)
  apply (subst (2) swapequal.simps)
  apply (simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)
  apply auto[1]
  apply (subst swapequal.simps)
  apply (simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)
  apply auto[1]
  apply simp
  apply (simp add: flip_def)
  apply (simp add: fresh_Pair_elim fresh_at_base)
  done

lemma aux_alphaish:
  assumes "distinct (map fst xs @ map snd xs)"
  shows "aux x y xs \<longleftrightarrow> swapequal x y xs"
  using assms
  apply (induct xs x y rule: aux_induct)
  apply (simp add: lookup_swapequal)
  prefer 8
  apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base)
  apply (elim conjE)
  apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base)
  apply (subgoal_tac "x \<notin> fst ` set xs \<and>
        x \<notin> snd ` set xs \<and> y \<notin> snd ` set xs \<and> y \<notin> fst ` set xs")
  apply (simp)
  apply (subst need)
  apply auto[1]
  sorry

lemma
  "aux x y [] \<longleftrightarrow> (x = y)"
  by (simp_all add: supp_Nil aux_alphaish)

end