diff -r fb201e383f1b -r da575186d492 Nominal/Ex/AuxNoFCB.thy
--- a/Nominal/Ex/AuxNoFCB.thy	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,402 +0,0 @@
-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)
-  unfolding fresh_star_def
-  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)
-  apply (simp only: fresh_Pair_elim)
-  apply blast
-  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')")
-  unfolding fresh_star_def
-  apply (subst lam2_rec.simps) apply simp
-  apply (subst lam2_rec.simps) apply simp
-  apply metis
-  apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def)
-  apply (subst lam2_rec.simps(10)) apply (simp_all add: fresh_star_def)
-  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)
-  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)
-  apply (rule refl)
-  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, 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"
-  "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var m) (Var ab) xs"
-  apply (induct xs arbitrary: m)
-  apply simp_all[2]
-  apply (case_tac [!] a)
-  apply (simp_all add: fresh_Cons)
-  apply (rule_tac [!] x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh)
-  apply (subst swapequal.simps)
-  apply (auto simp add: fresh_Pair lam.fresh)[1]
-  apply (elim conjE)
-  apply (simp add: fresh_Pair_elim fresh_at_base permute_flip_at)
-  apply (subst swapequal.simps)
-  apply (auto simp add: fresh_Pair lam.fresh)[1]
-  apply (elim conjE)
-  apply (simp add: fresh_Pair_elim fresh_at_base permute_flip_at)
-  done
-
-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 (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh)
-  apply simp
-  apply (subst swapequal.simps)
-  apply (simp add: fresh_Pair lam.fresh fresh_Nil)
-  by (metis (hide_lams, mono_tags) flip_at_base_simps(3) flip_at_simps(1) fresh_Pair fresh_at_base(2) lam.perm_simps(1) var_eq_swapequal var_neq_swapequal(1) var_neq_swapequal(2))
-
-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 (subst permute_eqvt) apply (simp add: flip_eqvt)
-  apply (subst permute_eqvt) apply (simp add: flip_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)[2]
-  apply (simp add: fresh_permute_left)
-  apply (simp add: fresh_permute_left)
-  apply clarify
-  apply (simp add: fresh_Cons fresh_Pair fresh_at_base)
-  apply clarify
-  apply (simp add: swapequal_reorder)
-  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 (auto simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)[1]
-  apply (subst swapequal.simps)
-  apply (auto simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)[1]
-  apply (simp add: flip_def 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 auto[1]
-  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 (auto simp add: fresh_Pair)[1]
-  apply (subst swapequal.simps) apply (auto simp add: fresh_Pair lam.fresh)
-  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 add: swapequal_app)
-  apply (simp, rule distinct_swapequal, simp)+
-  apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base conjE)
-  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 (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
-
-
-