Theory FSet_Extra

(* Title:        Formalizing an abstract calculus based on splitting in a modular way
 * Author:       Ghilain Bergeron <ghilain.bergeron at inria.fr>, 2023 *)

theory FSet_Extra
  imports Main "HOL-Library.FSet"
begin

text ‹
  This theory contains some additional lemmas regarding sets and finite sets, which were useful 
  in the process of proving some lemmas in 🗏‹Modular_Splitting_Calculus.thy› and
  🗏‹Lightweight_Avatar.thy›.
› 

(*<*)
(*! Where should we put this? *)
lemma Union_of_singleton_is_setcompr: ‹(⋃ x ∈ A. { y. y = f x ∧ P x }) = { f x | x. x ∈ A ∧ P x }›
  by auto
(*>*)

lemma finite_because_singleton: ‹(∀C1 ∈ S. ∀C2 ∈ S. C1 = C2) ⟶ finite S› for S
  by (metis finite.simps is_singletonI' is_singleton_the_elem)

lemma finite_union_of_finite_is_finite: ‹finite E ⟹ (∀D ∈ E. finite({f C |C. P C ∧ g C = D})) ⟹
                                  finite({f C |C. P C ∧ g C ∈ E})›
proof -
  assume finite_E: ‹finite E› and
         all_finite: ‹∀D ∈ E. finite({f C |C. P C ∧ g C = D})›
  have ‹finite (⋃{{f C |C. P C ∧ g C = D} |D. D∈E})›
    using finite_E all_finite finite_UN_I
    by (simp add: setcompr_eq_image)
  moreover have ‹{f C |C. P C ∧ g C ∈ E} ⊆ ⋃{{f C |C. P C ∧ g C = D} |D. D∈E}›
    by blast
  ultimately show ?thesis by (meson finite_subset)
qed

definition list_of_fset :: "'a fset ⇒ 'a list" where
  ‹list_of_fset A = (SOME l. fset_of_list l = A)›

lemma fin_set_fset: "finite A ⟹ ∃Af. fset Af = A" by (metis finite_list fset_of_list.rep_eq)

lemma fimage_snd_zip_is_snd [simp]:
  ‹length x = length y ⟹ (λ(x, y). y) |`| fset_of_list (zip x y) = fset_of_list y›
proof -
  assume length_x_eq_length_y: ‹length x = length y›
  have ‹(λ(x, y). y) |`| fset_of_list A = fset_of_list (map (λ(x, y). y) A)› for A
    by auto
  then show ?thesis
    using length_x_eq_length_y
    by (smt (verit, ccfv_SIG) cond_case_prod_eta map_snd_zip snd_conv)
qed

lemma if_in_ffUnion_then_in_subset: ‹x |∈| ffUnion A ⟹ ∃ a. a |∈| A ∧ x |∈| a›
  by (induct ‹A› rule: fset_induct, fastforce+)

lemma fset_ffUnion_subset_iff_all_fsets_subset: ‹fset (ffUnion A) ⊆ B ⟷ fBall A (λ x. fset x ⊆ B)›
proof (intro fBallI subsetI iffI)
  fix a x
  assume ffUnion_A_subset_B: ‹fset (ffUnion A) ⊆ B› and
         a_in_A: ‹a |∈| A› and
         x_in_fset_a: ‹x ∈ fset a›
  then have ‹x |∈| a›
    by simp
  then have ‹x |∈| ffUnion A›
    by (metis a_in_A ffunion_insert funion_iff set_finsert)
  then show ‹x ∈ B›
    using ffUnion_A_subset_B by blast
next
  fix x
  assume all_in_A_subset_B: ‹fBall A (λ x. fset x ⊆ B)› and
         ‹x ∈ fset (ffUnion A)›
  then have ‹x |∈| ffUnion A›
    by simp
  then obtain a where ‹a |∈| A› and
                      x_in_a: ‹x |∈| a›
    by (meson if_in_ffUnion_then_in_subset)
  then have ‹fset a ⊆ B›
    using all_in_A_subset_B
    by blast
  then show ‹x ∈ B›
    using x_in_a by blast
qed

lemma fBall_fset_of_list_iff_Ball_set: ‹fBall (fset_of_list A) P ⟷ Ball (set A) P›
  by (simp add: fset_of_list.rep_eq)

lemma wf_fsubset: ‹wfP (|⊂|)›
proof -
  have ‹wfP (λ A B. fcard A < fcard B)›
    by (simp add: wfp_if_convertible_to_nat)
  then show ‹wfP (|⊂|)›
    by (simp add: wfP_pfsubset)
qed
 
lemma non_zero_fcard_of_non_empty_set: ‹fcard A > 0 ⟷ A ≠ {||}›
  by (metis bot.not_eq_extremum fcard_fempty less_numeral_extra(3) pfsubset_fcard_mono)

lemma fimage_of_non_fempty_is_non_fempty: ‹A ≠ {||} ⟹ f |`| A ≠ {||}›
  unfolding fimage_is_fempty
  by blast

lemma Union_empty_if_set_empty_or_all_empty:
  ‹ffUnion A = {||} ⟹ A = {||} ∨ fBall A (λ x. x = {||})›
  by (metis (mono_tags, lifting) ffunion_insert finsert_absorb funion_fempty_right)

lemma fBall_fimage_is_fBall: ‹fBall (f |`| A) P ⟷ fBall A (λ x. P (f x))›
  by auto

lemma fset_map2: ‹v ∈ fset A ⟹ g (f v) ∈ set (map g (map f (list_of_fset A)))›
proof -
  assume ‹v ∈ fset A›
  then show ‹g (f v) ∈ set (map g (map f (list_of_fset A)))›
    unfolding list_of_fset_def
    by (smt (verit, ccfv_SIG) exists_fset_of_list fset_of_list.rep_eq imageI list.set_map someI_ex)
qed

end