Theory Nominal_Bounded_Set

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

section ‹Bounded Sets Equipped With a Permutation Action›

text ‹Additional lemmas about bounded sets.›

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)"
by (simp add: map_bset_permute)

end