--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/QuotientSet.thy	Sat Nov 26 09:53:52 2011 +0000
@@ -0,0 +1,91 @@
+theory QuotientSet
+imports 
+  "../Nominal2"
+begin
+
+lemma supp_quot:
+  "(supp (R, x)) supports (R `` {x})"
+unfolding supports_def
+unfolding fresh_def[symmetric]
+apply(perm_simp)
+apply(simp add: swap_fresh_fresh)
+done
+
+lemma
+  assumes "equiv UNIV R"
+  and "(x, y) \<in> R"
+  shows "R `` {x} = R `` {y}"
+using assms
+by (rule equiv_class_eq)
+
+lemma s1:
+  assumes "equiv UNIV R"
+  and "(x, y) \<in> R"
+  shows "a \<sharp> (R `` {x}) \<longleftrightarrow> a \<sharp> (R `` {y})"
+using assms
+apply(subst equiv_class_eq)
+apply(auto)
+done
+
+lemma s2:
+  fixes x::"'a::fs"
+  assumes "equiv UNIV R"
+  and     "supp R = {}"
+  shows "\<Inter>{supp y | y. (x, y) \<in> R} supports (R `` {x})"
+unfolding supports_def
+apply(rule allI)+
+apply(rule impI)
+apply(rule swap_fresh_fresh)
+apply(drule conjunct1)
+apply(auto)[1]
+apply(subst s1)
+apply(rule assms)
+apply(assumption)
+apply(rule supports_fresh)
+apply(rule supp_quot)
+apply(simp add: supp_Pair finite_supp assms)
+apply(simp add: supp_Pair assms)
+apply(drule conjunct2)
+apply(auto)[1]
+apply(subst s1)
+apply(rule assms)
+apply(assumption)
+apply(rule supports_fresh)
+apply(rule supp_quot)
+apply(simp add: supp_Pair finite_supp assms)
+apply(simp add: supp_Pair assms)
+done
+
+lemma s3:
+  fixes S::"'a::fs set"
+  assumes "finite S"
+  and "S \<noteq> {}"
+  and "a \<sharp> S"
+  shows "\<exists>x \<in> S. a \<sharp> x"
+using assms
+apply(auto simp add: fresh_def)
+apply(subst (asm) supp_of_finite_sets)
+apply(auto)
+done
+
+(*
+lemma supp_inter:
+  fixes x::"'a::fs"
+  assumes "equiv UNIV R"
+  and     "supp R = {}"
+  shows "supp (R `` {x}) = \<Inter>{supp y | y. (x, y) \<in> R}"
+apply(rule finite_supp_unique)
+apply(rule s2)
+apply(rule assms)
+apply(rule assms)
+apply(metis (lam_lifting, no_types) at_base_infinite finite_UNIV)
+*)
+
+  
+
+
+
+end
+
+
+