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