--- a/Nominal/Ex/QuotientSet.thy	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-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
-
-
-