--- a/Nominal/Abs.thy	Wed Mar 03 19:10:40 2010 +0100
+++ b/Nominal/Abs.thy	Thu Mar 04 15:31:21 2010 +0100
@@ -425,7 +425,14 @@
   add_perm 
 where
   "add_perm [] = 0"
-| "add_perm ((a,b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"
+| "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"
+
+fun
+  elem_perm
+where
+  "elem_perm [] = {}"
+| "elem_perm ((a, b) # xs) = {a, b} \<union> elem_perm xs"
+
 
 lemma add_perm_apend:
   shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"
@@ -433,9 +440,9 @@
 apply(auto simp add: add_assoc)
 done
 
-lemma
+lemma perm_list_exists:
   fixes p::perm
-  shows "\<exists>xs. p = add_perm xs"
+  shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"
 apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct)
 apply(rename_tac p)
 apply(case_tac "supp p = {}")
@@ -444,7 +451,7 @@
 apply(drule perm_zero)
 apply(simp)
 apply(rule_tac x="[]" in exI)
-apply(simp)
+apply(simp add: supp_Nil)
 apply(subgoal_tac "\<exists>x. x \<in> supp p")
 defer
 apply(auto)[1]
@@ -455,9 +462,17 @@
 apply(erule exE)
 apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)
 apply(simp add: add_perm_apend)
+apply(erule conjE)
 apply(drule sym)
 apply(simp)
 apply(simp add: expand_perm_eq)
+apply(simp add: supp_append)
+apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom)
+apply(rule conjI)
+prefer 2
+apply(auto)[1]
+apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2))
+defer
 apply(rule psubset_card_mono)
 apply(simp add: finite_supp)
 apply(rule psubsetI)
@@ -465,7 +480,20 @@
 apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")
 apply(blast)
 apply(simp add: supp_perm)
-apply(auto simp add: supp_perm)
+defer
+apply(auto simp add: supp_perm)[1]
+apply(case_tac "x = xa")
+apply(simp)
+apply(case_tac "((- p) \<bullet> x) = xa")
+apply(simp)
+apply(case_tac "sort_of xa = sort_of x")
+apply(simp)
+apply(auto)[1]
+apply(simp)
+apply(simp)
+apply(subgoal_tac "{a. p \<bullet> (- p \<bullet> x \<rightleftharpoons> x) \<bullet> a \<noteq> a} \<subseteq> {a. p \<bullet> a \<noteq> a}")
+apply(blast)
+apply(auto simp add: supp_perm)[1]
 apply(case_tac "x = xa")
 apply(simp)
 apply(case_tac "((- p) \<bullet> x) = xa")
@@ -477,23 +505,37 @@
 apply(simp)
 done
 
-lemma tt1:
-  shows "(supp x) \<sharp>* add_perm xs \<Longrightarrow> (add_perm xs) \<bullet> x = x"
+lemma tt0:
+  fixes p::perm
+  shows "(supp x) \<sharp>* p \<Longrightarrow> \<forall>a \<in> supp p. a \<sharp> x"
+apply(auto simp add: fresh_star_def supp_perm fresh_def)
+done
+
+lemma uu0:
+  shows "(\<forall>a \<in> elem_perm xs. a \<sharp> x) \<Longrightarrow> (add_perm xs \<bullet> x) = x"
 apply(induct xs rule: add_perm.induct)
 apply(simp)
-apply(simp)
-apply(case_tac "a = b")
-apply(simp)
-apply(drule meta_mp)
-defer
-apply(simp)
-apply(rule swap_fresh_fresh)
-apply(simp add: fresh_def)
-apply(auto)[1]
-apply(simp add: fresh_star_def fresh_def supp_perm)
-apply(drule_tac x="a" in bspec)
-apply(simp)
-oops
+apply(simp add: swap_fresh_fresh)
+done
+
+lemma yy0:
+  fixes xs::"(atom \<times> atom) list"
+  shows "supp xs = elem_perm xs"
+apply(induct xs rule: elem_perm.induct)
+apply(auto simp add: supp_Nil supp_Cons supp_Pair supp_atom)
+done
+
+lemma tt1:
+  shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
+apply(drule tt0)
+apply(subgoal_tac "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p")
+prefer 2
+apply(rule perm_list_exists)
+apply(erule exE)
+apply(simp only: yy0)
+apply(rule uu0)
+apply(auto)
+done
 
 
 lemma perm_induct_test:
@@ -512,7 +554,7 @@
 sorry
 
 
-
+(*
 lemma tt:
   "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
 apply(induct p rule: perm_induct_test)
@@ -539,7 +581,7 @@
 apply(simp add: fresh_star_def fresh_def)
 apply(simp)
 done
-
+*)
 lemma yy:
   assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
   shows "S1 = S2"
@@ -556,7 +598,6 @@
 apply(simp)
 oops
 
-*)
 
 fun
   distinct_perms