--- a/Nominal/Ex/LamTest.thy	Mon Jan 10 08:51:51 2011 +0000
+++ b/Nominal/Ex/LamTest.thy	Mon Jan 10 11:36:55 2011 +0000
@@ -25,6 +25,14 @@
 apply(rule fin)
 done
 
+lemma finite_supp_eqvt_at:
+  assumes asm: "eqvt_at f x"
+  and     fin: "finite (supp x)"
+  shows "finite (supp (f x))"
+apply(rule finite_subset)
+apply(rule supp_eqvt_at[OF asm fin])
+apply(rule fin)
+done
 
 definition
  "eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
@@ -1702,6 +1710,16 @@
 thm depth.psimps
 thm depth.simps
 
+
+lemma swap_set_not_in_at:
+  fixes a b::"'a::at"
+  and   S::"'a::at set"
+  assumes a: "a \<notin> S" "b \<notin> S"
+  shows "(a \<leftrightarrow> b) \<bullet> S = S"
+  unfolding permute_set_eq
+  using a by (auto simp add: permute_flip_at)
+
+
 nominal_primrec 
   frees :: "lam \<Rightarrow> name set"
 where
@@ -1724,6 +1742,7 @@
 apply(simp add: Abs_fresh_iff)
 apply(simp)
 apply(drule test)
+apply(rule_tac t="frees_sumC t - {x}" and s="(x \<leftrightarrow> a) \<bullet> (frees_sumC t - {x})" in subst)
 oops
 
 nominal_primrec

--- a/Nominal/Nominal2_Base.thy	Mon Jan 10 08:51:51 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Jan 10 11:36:55 2011 +0000
@@ -952,18 +952,6 @@
 instance atom :: fs
 by default (simp add: supp_atom)
 
-section {* Support for finite sets of atoms *}
-
-lemma supp_finite_atom_set:
-  fixes S::"atom set"
-  assumes "finite S"
-  shows "supp S = S"
-  apply(rule finite_supp_unique)
-  apply(simp add: supports_def)
-  apply(simp add: swap_set_not_in)
-  apply(rule assms)
-  apply(simp add: swap_set_in)
-done
 
 section {* Type @{typ perm} is finitely-supported. *}
 
@@ -1266,6 +1254,27 @@
 
 section {* Support of Finite Sets of Finitely Supported Elements *}
 
+text {* support and freshness for atom sets *}
+
+lemma supp_finite_atom_set:
+  fixes S::"atom set"
+  assumes "finite S"
+  shows "supp S = S"
+  apply(rule finite_supp_unique)
+  apply(simp add: supports_def)
+  apply(simp add: swap_set_not_in)
+  apply(rule assms)
+  apply(simp add: swap_set_in)
+done
+
+lemma fresh_finite_atom_set:
+  fixes S::"atom set"
+  assumes "finite S"
+  shows "a \<sharp> S \<longleftrightarrow> a \<notin> S"
+  unfolding fresh_def
+  by (simp add: supp_finite_atom_set[OF assms])
+
+
 lemma Union_fresh:
   shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
   unfolding Union_image_eq[symmetric]
@@ -1977,6 +1986,18 @@
 apply(auto)
 done
 
+lemma fresh_finite_set_at_base:
+  fixes a::"'a::at_base"
+  assumes a: "finite S"
+  shows "atom a \<sharp> S \<longleftrightarrow> a \<notin> S"
+  unfolding fresh_def
+  apply(simp add: supp_finite_set_at_base[OF a])
+  apply(subst inj_image_mem_iff)
+  apply(simp add: inj_on_def)
+  apply(simp)
+  done
+
+
 section {* Infrastructure for concrete atom types *}
 
 section {* A swapping operation for concrete atoms *}