--- a/Nominal/Abs.thy	Fri Mar 19 12:31:17 2010 +0100
+++ b/Nominal/Abs.thy	Fri Mar 19 12:31:55 2010 +0100
@@ -1,5 +1,5 @@
 theory Abs
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" "Nominal2_FSet"
 begin
 
 lemma permute_boolI:
@@ -749,17 +749,6 @@
 
 (* support of concrete atom sets *)
 
-lemma atom_eqvt_raw:
-  fixes p::"perm"
-  shows "(p \<bullet> atom) = atom"
-by (simp add: expand_fun_eq permute_fun_def atom_eqvt)
-
-lemma atom_image_cong:
-  shows "(atom ` X = atom ` Y) = (X = Y)"
-apply(rule inj_image_eq_iff)
-apply(simp add: inj_on_def)
-done
-
 lemma supp_atom_image:
   fixes as::"'a::at_base set"
   shows "supp (atom ` as) = supp as"
@@ -793,5 +782,10 @@
   \<and> pi \<bullet> bs = cs)"
 by (simp add: alpha_gen)
 
+(* maybe should be added to Infinite.thy *)
+lemma infinite_Un:
+  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+  by simp
+
 end
 

--- a/Nominal/LamEx.thy	Fri Mar 19 12:31:17 2010 +0100
+++ b/Nominal/LamEx.thy	Fri Mar 19 12:31:55 2010 +0100
@@ -41,10 +41,6 @@
   "\<not>(P \<and> Q) \<longleftrightarrow> (\<not>P) \<or> (\<not>Q)"
   by simp
 
-lemma infinite_Un:
-  "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
-
 instance
 apply default
 apply(induct_tac x)

--- a/Nominal/LamEx2.thy	Fri Mar 19 12:31:17 2010 +0100
+++ b/Nominal/LamEx2.thy	Fri Mar 19 12:31:55 2010 +0100
@@ -41,10 +41,6 @@
   "\<not>(P \<and> Q) \<longleftrightarrow> (\<not>P) \<or> (\<not>Q)"
   by simp
 
-lemma infinite_Un:
-  "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
-
 instance
 apply default
 apply(induct_tac x)

--- a/Nominal/Nominal2_FSet.thy	Fri Mar 19 12:31:17 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Fri Mar 19 12:31:55 2010 +0100
@@ -61,6 +61,10 @@
 lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)"
   by (lifting set_eqvt)
 
+lemma fin_fset_to_set:
+  "finite (fset_to_set x)"
+  by (induct x) (simp_all)
+
 lemma supp_fset_to_set:
   "supp (fset_to_set x) = supp x"
   apply (simp add: supp_def)
@@ -80,28 +84,75 @@
   apply (simp add: eqvts eqvts_raw atom_fmap_cong)
   done
 
-(*lemma "\<not> (memb x S) \<Longrightarrow> \<not> (memb y T) \<Longrightarrow> ((x # S) \<approx> (y # T)) = (x = y \<and> S \<approx> T)"*)
+lemma supp_atom_insert:
+  "finite (xs :: atom set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs"
+  apply (simp add: supp_finite_atom_set)
+  apply (simp add: supp_atom)
+  done
 
-lemma infinite_Un:
-  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
+lemma atom_image_cong:
+  shows "(atom ` X = atom ` Y) = (X = Y)"
+  apply(rule inj_image_eq_iff)
+  apply(simp add: inj_on_def)
+  done
 
-lemma supp_insert: "supp (insert (x :: 'a :: fs) xs) = supp x \<union> supp xs"
-  oops
+lemma atom_eqvt_raw:
+  fixes p::"perm"
+  shows "(p \<bullet> atom) = atom"
+  by (simp add: expand_fun_eq permute_fun_def atom_eqvt)
 
-lemma supp_finsert:
-  "supp (finsert (x :: 'a :: fs) S) = supp x \<union> supp S"
+lemma supp_finite_at_set:
+  fixes S::"('a :: at) set"
+  assumes a: "finite S"
+  shows "supp S = atom ` S"
+  apply(rule finite_supp_unique)
+  apply(simp add: supports_def)
+  apply (rule finite_induct[OF a])
+  apply (simp add: eqvts)
+  apply (simp)
+  apply clarify
+  apply (subst atom_image_cong[symmetric])
+  apply (subst atom_eqvt_raw[symmetric])
+  apply (subst eqvts[symmetric])
+  apply (rule swap_set_not_in)
+  apply simp_all
+  apply(rule finite_imageI)
+  apply(rule a)
+  apply (subst atom_image_cong[symmetric])
+  apply (subst atom_eqvt_raw[symmetric])
+  apply (subst eqvts[symmetric])
+  apply (rule swap_set_in)
+  apply simp_all
+  done
+
+lemma supp_at_insert:
+  "finite (xs :: ('a :: at) set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs"
+  apply (simp add: supp_finite_at_set)
+  apply (simp add: supp_at_base)
+  done
+
+lemma supp_atom_finsert:
+  "supp (finsert (x :: atom) S) = supp x \<union> supp S"
   apply (subst supp_fset_to_set[symmetric])
-  apply simp
-  (* apply (simp add: supp_insert supp_fset_to_set) *)
-  oops
+  apply (simp add: supp_finite_atom_set)
+  apply (simp add: supp_atom_insert[OF fin_fset_to_set])
+  apply (simp add: supp_fset_to_set)
+  done
 
-instance fset :: (fs) fs
+lemma supp_at_finsert:
+  "supp (finsert (x :: 'a :: at) S) = supp x \<union> supp S"
+  apply (subst supp_fset_to_set[symmetric])
+  apply (simp add: supp_finite_atom_set)
+  apply (simp add: supp_at_insert[OF fin_fset_to_set])
+  apply (simp add: supp_fset_to_set)
+  done
+
+instance fset :: (at) fs
   apply (default)
   apply (induct_tac x rule: fset_induct)
   apply (simp add: supp_def eqvts)
-  (* apply (simp add: supp_finsert) *)
-  (* apply default ? *)
-  oops
+  apply (simp add: supp_at_finsert)
+  apply (simp add: supp_at_base)
+  done
 
 end

--- a/Nominal/Term1.thy	Fri Mar 19 12:31:17 2010 +0100
+++ b/Nominal/Term1.thy	Fri Mar 19 12:31:55 2010 +0100
@@ -195,9 +195,6 @@
 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
 
-lemma inf_or: "(infinite x \<or> infinite y) = infinite (x \<union> y)"
-by (simp add: finite_Un)
-
 lemma supp_fv_let:
   assumes sa : "fv_bp bp = supp bp"
   shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\<rbrakk>
@@ -212,7 +209,7 @@
 apply(simp only: permute_ABS)
 apply(simp only: Abs_eq_iff)
 apply(simp only: alpha_gen supp_Pair split_conv eqvts)
-apply(simp only: inf_or[symmetric])
+apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
 apply (simp only: eqvts[symmetric] fv_trm1_eqvt[symmetric])