# Theory Nominal_Bounded_Set

```theory Nominal_Bounded_Set
imports
Nominal2.Nominal2
"HOL-Cardinals.Bounded_Set"
begin

section ‹Bounded Sets Equipped With a Permutation Action›

interpretation bset_lifting: bset_lifting .

lemma Abs_bset_inverse' [simp]:
assumes "|A| <o natLeq +c |UNIV :: 'k set|"
shows "set_bset (Abs_bset A :: 'a set['k]) = A"
by (metis Abs_bset_inverse assms mem_Collect_eq)

text ‹Bounded sets are equipped with a permutation action, provided their elements are.›

instantiation bset :: (pt,type) pt
begin

lift_definition permute_bset :: "perm ⇒ 'a set['b] ⇒ 'a set['b]" is
permute
proof -
fix p and A :: "'a set"
have "|p ∙ A| ≤o |A|" by (simp add: permute_set_eq_image)
also assume "|A| <o natLeq +c |UNIV :: 'b set|"
finally show "|p ∙ A| <o natLeq +c |UNIV :: 'b set|" .
qed

instance
by standard (transfer, simp)+

end

lemma Abs_bset_eqvt [simp]:
assumes "|A| <o natLeq +c |UNIV :: 'k set|"
shows "p ∙ (Abs_bset A :: 'a::pt set['k]) = Abs_bset (p ∙ A)"
by (simp add: permute_bset_def map_bset_def image_def permute_set_def) (metis (no_types, lifting) Abs_bset_inverse' assms)

lemma supp_Abs_bset [simp]:
assumes "|A| <o natLeq +c |UNIV :: 'k set|"
shows "supp (Abs_bset A :: 'a::pt set['k]) = supp A"
proof -
from assms have "⋀p. p ∙ (Abs_bset A :: 'a::pt set['k]) ≠ Abs_bset A ⟷ p ∙ A ≠ A"
by simp (metis map_bset.rep_eq permute_set_eq_image set_bset_inverse set_bset_to_set_bset)
then show ?thesis
unfolding supp_def by simp
qed

lemma map_bset_permute: "p ∙ B = map_bset (permute p) B"
by transfer (auto simp add: image_def permute_set_def)

lemma set_bset_eqvt [eqvt]:
"p ∙ set_bset B = set_bset (p ∙ B)"
by transfer simp

lemma map_bset_eqvt [eqvt]:
"p ∙ map_bset f B = map_bset (p ∙ f) (p ∙ B)"
by transfer simp

lemma bempty_eqvt [eqvt]: "p ∙ bempty = bempty"
by transfer simp

lemma binsert_eqvt [eqvt]: "p ∙ (binsert x B) = binsert (p ∙ x) (p ∙ B)"
by transfer simp

lemma bsingleton_eqvt [eqvt]: "p ∙ bsingleton x = bsingleton (p ∙ x)"