--- a/Nominal/Nominal2_FSet.thy	Fri Mar 19 10:24:49 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Fri Mar 19 12:22:10 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