--- a/Nominal/Nominal2_Supp.thy	Sat Mar 20 04:51:26 2010 +0100
+++ b/Nominal/Nominal2_Supp.thy	Sat Mar 20 13:50:00 2010 +0100
@@ -372,23 +372,100 @@
 done
 
 
-(*
-lemma supp_infinite:
-  fixes S::"atom set"
-  assumes asm: "finite (UNIV - S)"
-  shows "(supp S) = (UNIV - S)"
-apply(rule finite_supp_unique)
-apply(auto simp add: supports_def permute_set_eq swap_atom)[1]
-apply(rule asm)
-apply(auto simp add: permute_set_eq swap_atom)[1]
+section {* transpositions of permutations *}
+
+fun
+  add_perm 
+where
+  "add_perm [] = 0"
+| "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"
+
+lemma add_perm_append:
+  shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"
+by (induct xs arbitrary: ys)
+   (auto simp add: add_assoc)
+
+lemma perm_list_exists:
+  fixes p::perm
+  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 = {}")
+apply(simp)
+apply(simp add: supp_perm)
+apply(rule_tac x="[]" in exI)
+apply(simp add: supp_Nil)
+apply(simp add: expand_perm_eq)
+apply(subgoal_tac "\<exists>x. x \<in> supp p")
+defer
+apply(auto)[1]
+apply(erule exE)
+apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec)
+apply(drule mp)
+defer
+apply(erule exE)
+apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)
+apply(simp add: add_perm_append)
+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)
+defer
+apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")
+apply(blast)
+apply(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")
+apply(simp)
+apply(case_tac "sort_of xa = sort_of x")
+apply(simp)
+apply(auto)[1]
+apply(simp)
+apply(simp)
 done
 
-lemma supp_infinite_coinfinite:
-  fixes S::"atom set"
-  assumes asm1: "infinite S"
-  and     asm2: "infinite (UNIV-S)"
-  shows "(supp S) = (UNIV::atom set)"
-*)
+section {* Lemma about support and permutations *}
+
+lemma supp_perm_eq:
+  assumes a: "(supp x) \<sharp>* p"
+  shows "p \<bullet> x = x"
+proof -
+  obtain xs where eq: "p = add_perm xs" and sub: "supp xs \<subseteq> supp p"
+    using perm_list_exists by blast
+  from a have "\<forall>a \<in> supp p. a \<sharp> x"
+    by (auto simp add: fresh_star_def fresh_def supp_perm)
+  with eq sub have "\<forall>a \<in> supp xs. a \<sharp> x" by auto
+  then have "add_perm xs \<bullet> x = x" 
+    by (induct xs rule: add_perm.induct)
+       (simp_all add: supp_Cons supp_Pair supp_atom swap_fresh_fresh)
+  then show "p \<bullet> x = x" using eq by simp
+qed
+
 
 
 end
\ No newline at end of file