diff -r 5be8e34c2c0e -r 6bf332360510 Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Sun Nov 14 10:02:30 2010 +0000
+++ b/Nominal-General/Nominal2_Base.thy	Sun Nov 14 11:05:22 2010 +0000
@@ -6,6 +6,7 @@
 *)
 theory Nominal2_Base
 imports Main Infinite_Set
+        "~~/src/HOL/Quotient_Examples/FSet"
 uses ("nominal_library.ML")
      ("nominal_atoms.ML")
 begin
@@ -504,6 +505,11 @@
   unfolding mem_def
   by (simp add: permute_fun_app_eq)
 
+lemma empty_eqvt:
+  shows "p \<bullet> {} = {}"
+  unfolding empty_def Collect_def
+  by (simp add: permute_fun_def permute_bool_def)
+
 lemma insert_eqvt:
   shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
   unfolding permute_set_eq_image image_insert ..
@@ -569,6 +575,10 @@
 
 end
 
+lemma set_eqvt:
+  shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
+  by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
+
 subsection {* Permutations for options *}
 
 instantiation option :: (pt) pt
@@ -585,6 +595,39 @@
 
 end
 
+
+subsection {* Permutations for fsets *}
+
+lemma permute_fset_rsp[quot_respect]:
+  shows "(op = ===> list_eq ===> list_eq) permute permute"
+  unfolding fun_rel_def
+  by (simp add: set_eqvt[symmetric])
+
+instantiation fset :: (pt) pt
+begin
+
+quotient_definition
+  "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is
+  "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
+instance 
+proof
+  fix x :: "'a fset" and p q :: "perm"
+  show "0 \<bullet> x = x" by (descending) (simp)
+  show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp)
+qed
+
+end
+
+lemma permute_fset [simp]:
+  fixes S::"('a::pt) fset"
+  shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
+  and   "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
+  by (lifting permute_list.simps)
+
+
+
 subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *}
 
 instantiation char :: pt
@@ -1019,6 +1062,7 @@
 
 section {* Finite Support instances for other types *}
 
+
 subsection {* Type @{typ "'a \<times> 'b"} is finitely-supported. *}
 
 lemma supp_Pair: 
@@ -1037,14 +1081,13 @@
   shows "a \<sharp> ()"
   by (simp add: fresh_def supp_Unit)
 
-
-
 instance prod :: (fs, fs) fs
 apply default
 apply (induct_tac x)
 apply (simp add: supp_Pair finite_supp)
 done
 
+
 subsection {* Type @{typ "'a + 'b"} is finitely supported *}
 
 lemma supp_Inl: 
@@ -1069,6 +1112,7 @@
 apply (simp_all add: supp_Inl supp_Inr finite_supp)
 done
 
+
 subsection {* Type @{typ "'a option"} is finitely supported *}
 
 lemma supp_None: 
@@ -1093,6 +1137,7 @@
 apply (simp_all add: supp_None supp_Some finite_supp)
 done
 
+
 subsubsection {* Type @{typ "'a list"} is finitely supported *}
 
 lemma supp_Nil: 
@@ -1190,7 +1235,7 @@
     by (simp add: fresh_def[symmetric] swap_fresh_fresh)
 qed
 
-lemma Union_of_fin_supp_sets:
+lemma Union_of_finite_supp_sets:
   fixes S::"('a::fs set)"
   assumes fin: "finite S"   
   shows "finite (\<Union>x\<in>S. supp x)"
@@ -1203,38 +1248,81 @@
 proof -
   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
     by (rule supp_finite_atom_set[symmetric])
-       (rule Union_of_fin_supp_sets[OF fin])
+       (rule Union_of_finite_supp_sets[OF fin])
   also have "\<dots> \<subseteq> supp S"
     by (rule supp_subset_fresh)
        (simp add: Union_fresh)
   finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
 qed
 
-lemma supp_of_fin_sets:
+lemma supp_of_finite_sets:
   fixes S::"('a::fs set)"
   assumes fin: "finite S"
   shows "(supp S) = (\<Union>x\<in>S. supp x)"
 apply(rule subset_antisym)
 apply(rule supp_is_subset)
 apply(rule Union_supports_set)
-apply(rule Union_of_fin_supp_sets[OF fin])
+apply(rule Union_of_finite_supp_sets[OF fin])
 apply(rule Union_included_in_supp[OF fin])
 done
 
-lemma supp_of_fin_union:
+lemma finite_sets_supp:
+  fixes S::"('a::fs set)"
+  assumes "finite S"
+  shows "finite (supp S)"
+using assms
+by (simp only: supp_of_finite_sets Union_of_finite_supp_sets)
+
+lemma supp_of_finite_union:
   fixes S T::"('a::fs) set"
   assumes fin1: "finite S"
   and     fin2: "finite T"
   shows "supp (S \<union> T) = supp S \<union> supp T"
   using fin1 fin2
-  by (simp add: supp_of_fin_sets)
+  by (simp add: supp_of_finite_sets)
 
-lemma supp_of_fin_insert:
+lemma supp_of_finite_insert:
   fixes S::"('a::fs) set"
   assumes fin:  "finite S"
   shows "supp (insert x S) = supp x \<union> supp S"
   using fin
-  by (simp add: supp_of_fin_sets)
+  by (simp add: supp_of_finite_sets)
+
+
+subsection {* Type @{typ "'a fset"} is finitely supported *}
+
+lemma fset_eqvt: 
+  shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
+  by (lifting set_eqvt)
+
+lemma supp_fset [simp]:
+  shows "supp (fset S) = supp S"
+  unfolding supp_def
+  by (simp add: fset_eqvt fset_cong)
+
+lemma supp_empty_fset [simp]:
+  shows "supp {||} = {}"
+  unfolding supp_def
+  by simp
+
+lemma supp_insert_fset [simp]:
+  fixes x::"'a::fs"
+  and   S::"'a fset"
+  shows "supp (insert_fset x S) = supp x \<union> supp S"
+  apply(subst supp_fset[symmetric])
+  apply(simp add: supp_fset supp_of_finite_insert)
+  done
+
+lemma fset_finite_supp:
+  fixes S::"('a::fs) fset"
+  shows "finite (supp S)"
+  by (induct S) (simp_all add: finite_supp)
+
+
+instance fset :: (fs) fs
+  apply (default)
+  apply (rule fset_finite_supp)
+  done
 
 
 section {* Fresh-Star *}
@@ -1577,7 +1665,7 @@
 lemma supp_finite_set_at_base:
   assumes a: "finite S"
   shows "supp S = atom ` S"
-apply(simp add: supp_of_fin_sets[OF a])
+apply(simp add: supp_of_finite_sets[OF a])
 apply(simp add: supp_at_base)
 apply(auto)
 done