# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1333091490 -7200
# Node ID 31bc3e2e80bfbf224162066cd2fc1413f6b8f0b6
# Parent  57dcb5c0d5db73fe080ac67f4b27835980d1db29
More on Aux

diff -r 57dcb5c0d5db -r 31bc3e2e80bf Nominal/Ex/AuxNoFCB.thy
--- a/Nominal/Ex/AuxNoFCB.thy	Fri Mar 30 07:36:43 2012 +0200
+++ b/Nominal/Ex/AuxNoFCB.thy	Fri Mar 30 09:11:30 2012 +0200
@@ -381,13 +381,56 @@
   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)
-  prefer 8
+  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)
@@ -395,8 +438,9 @@
         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[1]
-  sorry
+  apply auto[2]
+  apply simp
+  done
 
 lemma
   "aux x y [] \<longleftrightarrow> (x = y)"