diff -r ad426ba60606 -r de5c9a0040ec Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Mon Jun 27 19:13:55 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Mon Jun 27 19:15:18 2011 +0100
@@ -145,7 +145,6 @@
   finally show ?thesis by simp
 qed
 
-(*
 lemma Abs_lst_fcb2:
   fixes as bs :: "atom list"
     and x y :: "'b :: fs"
@@ -158,7 +157,91 @@
   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
   shows "f as x c = f bs y c"
-*)
+proof -
+  have fin1: "finite (supp (f as x c))"
+    apply(rule_tac S="supp (as, x, c)" in supports_finite)
+    apply(simp add: supports_def)
+    apply(simp add: fresh_def[symmetric])
+    apply(clarify)
+    apply(subst perm1)
+    apply(simp add: supp_swap fresh_star_def)
+    apply(simp add: swap_fresh_fresh fresh_Pair)
+    apply(simp add: finite_supp)
+    done
+  have fin2: "finite (supp (f bs y c))"
+    apply(rule_tac S="supp (bs, y, c)" in supports_finite)
+    apply(simp add: supports_def)
+    apply(simp add: fresh_def[symmetric])
+    apply(clarify)
+    apply(subst perm2)
+    apply(simp add: supp_swap fresh_star_def)
+    apply(simp add: swap_fresh_fresh fresh_Pair)
+    apply(simp add: finite_supp)
+    done
+  obtain q::"perm" where 
+    fr1: "(q \<bullet> (set as)) \<sharp>* (as, bs, x, y, c, f as x c, f bs y c)" and 
+    fr2: "supp q \<sharp>* Abs_lst as x" and 
+    inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)"
+    using at_set_avoiding3[where xs="set as" and c="(as, bs, x, y, c, f as x c, f bs y c)" 
+      and x="Abs_lst as x"]
+    apply(simp add: supp_Pair finite_supp fin1 fin2 Abs_fresh_star)
+    apply(erule exE)
+    apply(erule conjE)+
+    apply(drule fresh_star_supp_conv)
+    apply(blast)
+    done
+  have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp
+  also have "\<dots> = Abs_lst as x"
+    apply(rule perm_supp_eq)
+    apply(simp add: fr2)
+    done
+  finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using e by simp
+  then obtain r::perm where 
+    qq1: "q \<bullet> x = r \<bullet> y" and 
+    qq2: "q \<bullet> as = r \<bullet> bs" and 
+    qq3: "supp r \<subseteq> (set (q \<bullet> as) \<union> set bs)"
+    apply -
+    apply(drule_tac sym)
+    apply(simp only: Abs_eq_iff2 alphas)
+    apply(erule exE)
+    apply(erule conjE)+
+    apply(drule_tac x="p" in meta_spec)
+    apply(simp)
+    apply(blast)
+    done
+  have "f as x c = q \<bullet> (f as x c)"
+    apply(rule sym)
+    apply(rule perm_supp_eq)
+    using inc fcb1 fr1
+    apply(simp add: set_eqvt)
+    apply(simp add: fresh_star_Pair)
+    apply(auto simp add: fresh_star_def)
+    done
+  also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" 
+    apply(subst perm1)
+    using inc fresh1 fr1
+    apply(simp add: set_eqvt)
+    apply(simp add: fresh_star_Pair)
+    apply(auto simp add: fresh_star_def)
+    done
+  also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp
+  also have "\<dots> = r \<bullet> (f bs y c)"
+    apply(rule sym)
+    apply(subst perm2)
+    using qq3 fresh2 fr1
+    apply(simp add: set_eqvt)
+    apply(simp add: fresh_star_Pair)
+    apply(auto simp add: fresh_star_def)
+    done
+  also have "... = f bs y c"   
+    apply(rule perm_supp_eq)
+    using qq3 fr1 fcb2
+    apply(simp add: set_eqvt)
+    apply(simp add: fresh_star_Pair)
+    apply(auto simp add: fresh_star_def)
+    done
+  finally show ?thesis by simp
+qed
 
 lemma supp_zero_perm_zero:
   shows "supp (p :: perm) = {} \<longleftrightarrow> p = 0"