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)
  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)+
  unfolding fresh_star_def
  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)
  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)
  apply (simp_all)[53]
  apply clarify
  apply metis
  apply simp
  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)
  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

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
  apply clarify
  apply (rule_tac s="(x \<leftrightarrow> xa) \<bullet> swapequal_sumC ((hla \<leftrightarrow> x) \<bullet> la, (hra \<leftrightarrow> x) \<bullet> ra, ta)" in trans)
  apply (simp only: permute_pure)
  apply (simp add: eqvt_at_def fresh_Pair_elim)
  apply (simp add: flip_fresh_fresh)
  apply (subgoal_tac "(x \<leftrightarrow> xa) \<bullet> (hla \<leftrightarrow> x) \<bullet> la = (hla \<leftrightarrow> xa) \<bullet> la")
  apply (subgoal_tac "(x \<leftrightarrow> xa) \<bullet> (hra \<leftrightarrow> x) \<bullet> ra = (hra \<leftrightarrow> xa) \<bullet> ra")
  apply simp
  apply (subst permute_eqvt)
  apply (simp add: flip_fresh_fresh flip_eqvt)
  apply (subst permute_eqvt)
  apply (simp add: flip_fresh_fresh flip_eqvt)
  done

termination (eqvt) by lexicographic_order

lemma var_eq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> swapequal (Var ab) (Var ab) xs"
  apply (induct xs)
  apply simp
  apply (case_tac a)
  apply (simp add: fresh_Cons)
  apply (rule_tac x="(ab, aa, b, xs)" and ?'a="name" in obtain_fresh)
  apply (subst swapequal.simps)
  apply (simp add: fresh_Pair lam.fresh)
  apply (simp add: fresh_Pair_elim)
  by (metis flip_at_base_simps(3) fresh_Pair fresh_at_base(2))

lemma var_neq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var ab) (Var m) xs"
  apply (induct xs arbitrary: m)
  apply simp
  apply (case_tac a)
  apply (simp add: fresh_Cons)
  apply (rule_tac x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh)
  apply (subst swapequal.simps)
  apply (simp add: fresh_Pair lam.fresh)
  apply auto[1]
  apply (elim conjE)
  apply (simp add: fresh_Pair_elim)
  apply (simp add: flip_at_base_simps(3) fresh_Pair fresh_at_base(2))
  apply (subgoal_tac "ab \<noteq> (b \<leftrightarrow> aba) \<bullet> m")
  apply simp
  by (metis (lifting) permute_flip_at)

lemma var_neq_swapequal2: "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var m) (Var ab) xs"
  apply (induct xs arbitrary: m)
  apply simp
  apply (case_tac a)
  apply (simp add: fresh_Cons)
  apply (rule_tac x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh)
  apply (subst swapequal.simps)
  apply (simp add: fresh_Pair lam.fresh)
  apply auto[1]
  apply (elim conjE)
  apply (simp add: fresh_Pair_elim)
  apply (simp add: flip_at_base_simps(3) fresh_Pair fresh_at_base(2))
  apply (subgoal_tac "ab \<noteq> (aa \<leftrightarrow> aba) \<bullet> m")
  apply simp
  by (metis (lifting) permute_flip_at)

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
  apply (simp add: var_eq_swapequal fresh_Pair_elim)
  apply (case_tac "n = aa")
  apply (simp add: fresh_Pair_elim fresh_at_base)
  apply (simp add: var_neq_swapequal fresh_Pair_elim)
  apply (simp add: fresh_Pair_elim fresh_at_base flip_def)
  apply (case_tac "m = b")
  apply simp
  apply (simp add: var_neq_swapequal2 fresh_at_base)
  apply simp
  done

lemma swapequal_reorder: "
  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)"
  apply (rule_tac x="(a, b, x, y, t, s, xs)" and ?'a="name" in obtain_fresh)
  apply (rule_tac x="(a, b, x, y, t, s, xs, aa)" and ?'a="name" in obtain_fresh)
  apply (rename_tac f g)
  apply (simp add: fresh_Pair_elim fresh_at_base)
  apply (subst swapequal.simps)
  apply (auto simp add: fresh_Pair fresh_Cons fresh_at_base)[1]
  apply (subgoal_tac "(x \<leftrightarrow> f) \<bullet> atom g \<sharp> t")
  apply (subst swapequal.simps)
  apply (simp add: fresh_Pair fresh_Cons fresh_permute_left)
  apply rule apply assumption
  apply (simp add: flip_at_base_simps fresh_at_base flip_def)
  apply (subst swapequal.simps)
  apply (simp add: fresh_Pair fresh_Cons fresh_at_base)
  apply rule apply (rotate_tac 12)
  apply assumption
  apply (simp add: fresh_Pair fresh_Cons fresh_at_base)
  apply (subst swapequal.simps)
  apply (simp add: fresh_Pair fresh_Cons fresh_at_base fresh_permute_left)
  apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> atom f \<sharp> t")
  apply rule apply assumption
  apply (simp add: flip_at_base_simps fresh_at_base flip_def)
  apply (simp add: flip_at_base_simps fresh_at_base flip_def)
  apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> (x \<leftrightarrow> f) \<bullet> t = (x \<leftrightarrow> f) \<bullet> (a \<leftrightarrow> g) \<bullet> t")
  apply (subgoal_tac "(b \<leftrightarrow> g) \<bullet> (y \<leftrightarrow> f) \<bullet> s = (y \<leftrightarrow> f) \<bullet> (b \<leftrightarrow> g) \<bullet> s")
  apply simp
  apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt)
  apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt)
  apply (simp add: flip_at_base_simps fresh_at_base flip_def)
  done

lemma swapequal_lambda:
  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 swapequal_reorder)
  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 distinct_swapequal: "\<forall>p q. p \<bullet> l \<noteq> q \<bullet> r \<Longrightarrow> \<not>swapequal l r xs"
  apply (induct xs rule:swapequal.induct)
  apply simp
  apply metis
  apply (simp add: fresh_Pair_elim)
  apply (subgoal_tac "\<forall>(p\<Colon>perm) q\<Colon>perm. p \<bullet> (hl \<leftrightarrow> x) \<bullet> l \<noteq> q \<bullet> (hr \<leftrightarrow> x) \<bullet> r")
  apply simp
  apply (intro allI)
  apply (drule_tac x="p + (hl \<leftrightarrow> x)" in spec)
  apply (drule_tac x="q + (hr \<leftrightarrow> x)" in spec)
  apply simp
  done

lemma swapequal_app: "(swapequal l1 l2 xs \<and> swapequal r1 r2 xs) = swapequal (App l1 r1) (App l2 r2) xs"
  apply (induct xs arbitrary: l1 l2 r1 r2)
  apply simp
  apply (case_tac a)
  apply simp
  apply (rule_tac x="(l1, l2, r1, r2, aa, b, xs)" and ?'a="name" in obtain_fresh)
  apply (simp add: fresh_Pair_elim)
  apply (subst swapequal.simps) apply (simp add: fresh_Pair) apply auto[1]
  apply (subst swapequal.simps) apply (simp add: fresh_Pair lam.fresh) apply auto[1]
  apply simp
  done

lemma [simp]: "distinct (map fst xs) \<Longrightarrow> distinct xs"
  by (induct xs) auto

lemma [simp]:
  "atom x \<sharp> xs \<Longrightarrow> x \<notin> fst ` set xs"
  "atom x \<sharp> xs \<Longrightarrow> x \<notin> snd ` set xs"
  apply (induct xs)
  apply simp_all
  apply (case_tac [!] a)
  apply (simp_all add: fresh_Cons fresh_Pair 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)
  apply (simp, rule distinct_swapequal, simp)
  apply (simp, rule distinct_swapequal, simp)
  apply (simp, rule distinct_swapequal, simp)
  apply (simp add: swapequal_app)
  apply (simp, rule distinct_swapequal, simp)
  apply (simp, rule distinct_swapequal, simp)
  apply (simp, rule distinct_swapequal, simp)
  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 swapequal_lambda)
  apply auto[2]
  apply simp
  done

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

end