--- a/Nominal/Nominal2_Base.thy	Mon Nov 29 05:17:41 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Nov 29 08:01:09 2010 +0000
@@ -952,7 +952,6 @@
 
 section {* Support for finite sets of atoms *}
 
-
 lemma supp_finite_atom_set:
   fixes S::"atom set"
   assumes "finite S"
@@ -1159,6 +1158,10 @@
   shows "supp (x # xs) = supp x \<union> supp xs"
 by (simp add: supp_def Collect_imp_eq Collect_neg_eq)
 
+lemma supp_append:
+  shows "supp (xs @ ys) = supp xs \<union> supp ys"
+  by (induct xs) (auto simp add: supp_Nil supp_Cons)
+
 lemma fresh_Nil: 
   shows "a \<sharp> []"
   by (simp add: fresh_def supp_Nil)
@@ -1167,6 +1170,11 @@
   shows "a \<sharp> (x # xs) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> xs"
   by (simp add: fresh_def supp_Cons)
 
+lemma fresh_append:
+  shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
+  by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
+
+
 instance list :: (fs) fs
 apply default
 apply (induct_tac x)
@@ -1312,6 +1320,29 @@
   using fin unfolding fresh_def
   by (simp add: supp_of_finite_insert)
 
+lemma supp_set_empty:
+  shows "supp {} = {}"
+  unfolding supp_def
+  by (simp add: empty_eqvt)
+
+lemma fresh_set_empty:
+  shows "a \<sharp> {}"
+  by (simp add: fresh_def supp_set_empty)
+
+lemma supp_set:
+  fixes xs :: "('a::fs) list"
+  shows "supp (set xs) = supp xs"
+apply(induct xs)
+apply(simp add: supp_set_empty supp_Nil)
+apply(simp add: supp_Cons supp_of_finite_insert)
+done
+
+lemma fresh_set:
+  fixes xs :: "('a::fs) list"
+  shows "a \<sharp> (set xs) \<longleftrightarrow> a \<sharp> xs"
+unfolding fresh_def
+by (simp add: supp_set)
+
 
 subsection {* Type @{typ "'a fset"} is finitely supported *}
 
@@ -1364,12 +1395,23 @@
   shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x"
 by (auto simp add: fresh_star_def fresh_def)
 
-lemma fresh_star_prod:
-  fixes as::"atom set"
+lemma fresh_star_Pair:
   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
   by (auto simp add: fresh_star_def fresh_Pair)
 
-lemma fresh_star_union:
+lemma fresh_star_list:
+  shows "as \<sharp>* (xs @ ys) \<longleftrightarrow> as \<sharp>* xs \<and> as \<sharp>* ys"
+  and   "as \<sharp>* (x # xs) \<longleftrightarrow> as \<sharp>* x \<and> as \<sharp>* xs"
+  and   "as \<sharp>* []"
+by (auto simp add: fresh_star_def fresh_Nil fresh_Cons fresh_append)
+
+lemma fresh_star_set:
+  fixes xs::"('a::fs) list"
+  shows "as \<sharp>* set xs \<longleftrightarrow> as \<sharp>* xs"
+unfolding fresh_star_def
+by (simp add: fresh_set)
+
+lemma fresh_star_Un:
   shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
   by (auto simp add: fresh_star_def)
 
@@ -1398,9 +1440,9 @@
   shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"
   by (simp add: fresh_star_def fresh_Unit) 
 
-lemma fresh_star_prod_elim: 
+lemma fresh_star_Pair_elim: 
   shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"
-  by (rule, simp_all add: fresh_star_prod)
+  by (rule, simp_all add: fresh_star_Pair)
 
 lemma fresh_star_zero:
   shows "as \<sharp>* (0::perm)"
@@ -1427,6 +1469,15 @@
 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
 done
 
+lemma at_fresh_star_inter:
+  assumes a: "(p \<bullet> bs) \<sharp>* bs" 
+  and     b: "finite bs"
+  shows "p \<bullet> bs \<inter> bs = {}"
+using a b
+unfolding fresh_star_def
+unfolding fresh_def
+by (auto simp add: supp_finite_atom_set)
+
 
 section {* Induction principle for permutations *}
 
@@ -1525,6 +1576,12 @@
   qed
 qed
 
+lemma perm_supp_eq:
+  assumes a: "(supp p) \<sharp>* x"
+  shows "p \<bullet> x = x"
+by (rule supp_perm_eq)
+   (simp add: fresh_star_supp_conv a)
+
 
 section {* Avoiding of atom sets *}
 
@@ -1607,7 +1664,7 @@
 apply(erule_tac c="(c, x)" in at_set_avoiding)
 apply(simp add: supp_Pair)
 apply(rule_tac x="p" in exI)
-apply(simp add: fresh_star_prod)
+apply(simp add: fresh_star_Pair)
 apply(rule fresh_star_supp_conv)
 apply(auto simp add: fresh_star_def)
 done
@@ -1621,7 +1678,7 @@
 apply(erule_tac c="(c, x)" in at_set_avoiding)
 apply(simp add: supp_Pair)
 apply(rule_tac x="p" in exI)
-apply(simp add: fresh_star_prod)
+apply(simp add: fresh_star_Pair)
 apply(rule fresh_star_supp_conv)
 apply(auto simp add: fresh_star_def)
 done