--- a/Nominal/Ex/Foo2.thy	Fri Nov 26 19:03:23 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Fri Nov 26 22:43:26 2010 +0000
@@ -298,6 +298,36 @@
 *}
 
 
+thm at_set_avoiding2 supp_perm_eq at_set_avoiding
+
+lemma abs_rename_set:
+  fixes x::"'a::fs"
+  assumes "b' \<sharp> x" "sort_of b = sort_of b'"
+  shows "\<exists>y. [{b}]set. x = [{b'}]set. y"
+apply(rule_tac x="(b \<rightleftharpoons> b') \<bullet> x" in exI)
+apply(subst Abs_swap1[where a="b" and b="b'"])
+apply(simp)
+using assms
+apply(simp add: fresh_def)
+apply(perm_simp)
+using assms
+apply(simp)
+done
+
+lemma abs_rename_list:
+  fixes x::"'a::fs"
+  assumes "b' \<sharp> x" "sort_of b = sort_of b'"
+  shows "\<exists>y. [[b]]lst. x = [[b']]lst. y"
+apply(rule_tac x="(b \<rightleftharpoons> b') \<bullet> x" in exI)
+apply(subst Abs_swap2[where a="b" and b="b'"])
+apply(simp)
+using assms
+apply(simp add: fresh_def)
+apply(perm_simp)
+using assms
+apply(simp)
+done
+
 lemma test3:
   fixes c::"'a::fs"
   assumes a: "y = Let2 x1 x2 trm1 trm2"
@@ -307,24 +337,19 @@
 apply -
 apply(subgoal_tac "\<exists>q::perm. (q \<bullet> {atom x1, atom x2}) \<sharp>* (c, x1, x2, trm1, trm2)")
 apply(erule exE)
-apply(drule_tac p="- q" in permute_boolI)
 apply(perm_simp)
+apply(drule_tac x="q \<bullet> x1" in spec)
+apply(drule_tac x="q \<bullet> x2" in spec)
 apply(simp only: foo.eq_iff)
-apply(drule_tac x="x1" in spec)
-apply(drule_tac x="x2" in spec)
 apply(simp)
-apply(drule mp)
+apply(erule mp)
 apply(rule conjI)
-defer
-apply(rule_tac p="q" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel)
+apply(simp add: fresh_star_prod)
 apply(rule conjI)
 prefer 2
-apply(rule_tac x="(atom x2 \<rightleftharpoons> atom (q \<bullet> x2)) \<bullet> trm2" in exI)
-apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"])
-apply(simp)
+apply(rule abs_rename_list)
+apply(simp add: fresh_star_prod)
 apply(simp add: fresh_star_def)
-apply(simp add: fresh_def supp_Pair)
 apply(simp)
 apply(case_tac "x1=x2")
 apply(simp)
@@ -363,11 +388,6 @@
 apply(simp add: fresh_star_def)
 apply(simp add: fresh_def supp_Pair)
 apply(simp add: supp_at_base)
-apply(simp)
-defer
-apply(rule_tac p="q" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel fresh_star_prod)
-apply(simp)
 apply(rule at_set_avoiding3[where x="()", simplified])
 apply(simp)
 apply(simp add: finite_supp)
@@ -386,6 +406,25 @@
 apply(auto)
 done
 
+lemma test5:
+  fixes c::"'a::fs"
+  assumes "\<And>name. y = Var name \<Longrightarrow> P" 
+  and     "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
+  and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
+  and     "\<And>assn1 trm1 assn2 trm2. 
+    \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+apply(rule_tac y="y" in foo.exhaust(1))
+apply (erule assms)
+apply (erule assms)
+prefer 3
+apply(erule test4[where c="c"])
+apply (rule assms(5)) 
+apply assumption
+apply(simp)
+oops
+
 
 end