--- a/Quot/Nominal/Abs.thy	Wed Feb 17 17:51:35 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Thu Feb 18 23:07:28 2010 +0100
@@ -427,6 +427,35 @@
   shows "P p"
 sorry
 
+lemma tt1:
+  assumes a: "finite (supp p)"
+  shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
+using a
+unfolding fresh_star_def fresh_def
+apply(induct F\<equiv>"supp p" arbitrary: p rule: finite.induct)
+apply(simp add: supp_perm)
+defer
+apply(case_tac "a \<in> A")
+apply(simp add: insert_absorb)
+apply(subgoal_tac "A = supp p - {a}")
+prefer 2
+apply(blast)
+apply(case_tac "p \<bullet> a = a")
+apply(simp add: supp_perm)
+apply(drule_tac x="p + (((- p) \<bullet> a) \<rightleftharpoons> a)" in meta_spec)
+apply(simp)
+apply(drule meta_mp)
+apply(rule subset_antisym)
+apply(rule subsetI)
+apply(simp)
+apply(simp add: supp_perm)
+apply(case_tac "xa = p \<bullet> a")
+apply(simp)
+apply(case_tac "p \<bullet> a = (- p) \<bullet> a")
+apply(simp)
+defer
+apply(simp)
+oops
 
 lemma tt:
   "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"