Theory Countable_Set_Extra

(******************************************************************************)
(* Project: Isabelle/UTP Toolkit                                              *)
(* File: Countable_Set_Extra.thy                                              *)
(* Authors: Simon Foster and Frank Zeyda                                      *)
(* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk                 *)
(******************************************************************************)

section ‹ Countable Sets: Extra functions and properties ›

theory Countable_Set_Extra
imports
  "HOL-Library.Countable_Set_Type"
  Sequence
  FSet_Extra
begin

subsection ‹ Extra syntax ›

notation cempty (‹{}⇩c›)
notation cin (infix ‹∈⇩c› 50)
notation cUn (infixl ‹∪⇩c› 65)
notation cInt (infixl ‹∩⇩c› 70)
notation cDiff (infixl ‹-⇩c› 65)
notation cUnion (‹⋃⇩c_› [900] 900)
notation cimage (infixr ‹`⇩c› 90)

abbreviation csubseteq :: "'a cset ⇒ 'a cset ⇒ bool" (‹(_/ ⊆⇩c _)› [51, 51] 50)
where "A ⊆⇩c B ≡ A ≤ B"

abbreviation csubset :: "'a cset ⇒ 'a cset ⇒ bool" (‹(_/ ⊂⇩c _)› [51, 51] 50)
where "A ⊂⇩c B ≡ A < B"

subsection ‹ Countable set functions ›

setup_lifting type_definition_cset

lift_definition cnin :: "'a ⇒ 'a cset ⇒ bool" (infix ‹∉⇩c› 50) is "(∉)" .

definition cBall :: "'a cset ⇒ ('a ⇒ bool) ⇒ bool" where
"cBall A P = (∀x. x ∈⇩c A ⟶ P x)"

definition cBex :: "'a cset ⇒ ('a ⇒ bool) ⇒ bool" where
"cBex A P = (∃x. x ∈⇩c A ⟶ P x)"

declare cBall_def [mono,simp]
declare cBex_def [mono,simp]

syntax
  "_cBall" :: "pttrn => 'a cset => bool => bool" (‹(3∀ _∈⇩c_./ _)› [0, 0, 10] 10)
  "_cBex"  :: "pttrn => 'a cset => bool => bool" (‹(3∃ _∈⇩c_./ _)› [0, 0, 10] 10)

syntax_consts
  "_cBall" == cBall and
  "_cBex" == cBex

translations
  "∀ x∈⇩cA. P" == "CONST cBall A (%x. P)"
  "∃ x∈⇩cA. P" == "CONST cBex  A (%x. P)"

definition cset_Collect :: "('a ⇒ bool) ⇒ 'a cset" where
"cset_Collect = (acset o Collect)"

lift_definition cset_Coll :: "'a cset ⇒ ('a ⇒ bool) ⇒ 'a cset" is "λ A P. {x ∈ A. P x}"
  by (auto)

lemma cset_Coll_equiv: "cset_Coll A P = cset_Collect (λ x. x ∈⇩c A ∧ P x)"
  by (simp add:cset_Collect_def cset_Coll_def cin_def)

declare cset_Collect_def [simp]

syntax
  "_cColl" :: "pttrn => bool => 'a cset" (‹(1{_./ _}⇩c)›)
syntax_consts
  "_cColl" ⇌ cset_Collect
translations
  "{x . P}⇩c" ⇌ "(CONST cset_Collect) (λ x . P)"

syntax
  "_cCollect" :: "pttrn => 'a cset => bool => 'a cset"    (‹(1{_ ∈⇩c/ _./ _}⇩c)›)
syntax_consts
  "_cCollect" ⇌ cset_Coll
translations
  "{x ∈⇩c A. P}⇩c" => "CONST cset_Coll A (λ x. P)"

lemma cset_CollectI: "P (a :: 'a::countable) ⟹ a ∈⇩c {x. P x}⇩c"
  by (simp add: cin_def)

lemma cset_CollI: "⟦ a ∈⇩c A; P a ⟧ ⟹ a ∈⇩c {x ∈⇩c A. P x}⇩c"
  by (simp add: cin.rep_eq cset_Coll.rep_eq)

lemma cset_CollectD: "(a :: 'a::countable) ∈⇩c {x. P x}⇩c ⟹ P a"
  by (simp add: cin_def)

lemma cset_Collect_cong: "(⋀x. P x = Q x) ==> {x. P x}⇩c = {x. Q x}⇩c"
  by simp

text ‹ Avoid eta-contraction for robust pretty-printing. ›

typed_print_translation ‹
  [(\<^const_syntax>‹cset_Collect›, Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>‹_cColl›)]
›

lift_definition cset_set :: "'a list ⇒ 'a cset" is set
  using countable_finite by blast

lemma countable_finite_power:
  "countable(A) ⟹ countable {B. B ⊆ A ∧ finite(B)}"
  by (metis Collect_conj_eq Int_commute countable_Collect_finite_subset)

lift_definition cInter :: "'a cset cset ⇒ 'a cset"  (‹⋂⇩c_› [900] 900)
  is "λA. if A = {} then {} else ⋂ A"
  using countable_INT [of _ _ id] by auto

abbreviation (input) cINTER :: "'a cset ⇒ ('a ⇒ 'b cset) ⇒ 'b cset"
  where "cINTER A f ≡ cInter (cimage f A)"

lift_definition cfinite :: "'a cset ⇒ bool" is finite .
lift_definition cInfinite :: "'a cset ⇒ bool" is infinite .
lift_definition clist :: "'a::linorder cset ⇒ 'a list" is sorted_list_of_set .
lift_definition ccard :: "'a cset ⇒ nat" is card .
lift_definition cPow :: "'a cset ⇒ 'a cset cset" is "λ A. {B. B ⊆⇩c A ∧ cfinite(B)}"
proof -
  fix A
  have "{B :: 'a cset. B ⊆⇩c A ∧ cfinite B} = acset ` {B :: 'a set. B ⊆ rcset A ∧ finite B}"
    apply (auto simp add: cfinite.rep_eq cin_def less_eq_cset_def countable_finite)
    using image_iff apply fastforce
    done

  moreover have "countable {B :: 'a set. B ⊆ rcset A ∧ finite B}"
    by (auto intro: countable_finite_power)

  ultimately show "countable {B. B ⊆⇩c A ∧ cfinite B}"
    by simp
qed

definition CCollect :: "('a ⇒ bool option) ⇒ 'a cset option" where
"CCollect p = (if (None ∉ range p) then Some (cset_Collect (the ∘ p)) else None)"

definition cset_mapM :: "'a option cset ⇒ 'a cset option" where
"cset_mapM A = (if (None ∈⇩c A) then None else Some (the `⇩c A))"

lemma cset_mapM_Some_image [simp]:
  "cset_mapM (cimage Some A) = Some A"
  apply (auto simp add: cset_mapM_def)
  apply (metis cimage_cinsert cinsertI1 option.sel set_cinsert)
  done

definition CCollect_ext :: "('a ⇒ 'b option) ⇒ ('a ⇒ bool option) ⇒ 'b cset option" where
"CCollect_ext f p = do { xs ← CCollect p; cset_mapM (f `⇩c xs) }"

lemma the_Some_image [simp]:
  "the ` Some ` xs = xs"
  by (auto simp add:image_iff)

lemma CCollect_ext_Some [simp]:
  "CCollect_ext Some xs = CCollect xs"
  apply (case_tac "CCollect xs")
   apply (auto simp add:CCollect_ext_def)
  done

lift_definition list_of_cset :: "'a :: linorder cset ⇒ 'a list" is sorted_list_of_set .

lift_definition fset_cset :: "'a fset ⇒ 'a cset" is id
  using uncountable_infinite by auto

definition cset_count :: "'a cset ⇒ 'a ⇒ nat" where
"cset_count A =
  (if (finite (rcset A))
   then (SOME f::'a⇒nat. inj_on f (rcset A))
   else (SOME f::'a⇒nat. bij_betw f (rcset A) UNIV))"

lemma cset_count_inj_seq:
  "inj_on (cset_count A) (rcset A)"
proof (cases "finite (rcset A)")
  case True note fin = this
  obtain count :: "'a ⇒ nat" where count_inj: "inj_on count (rcset A)"
    by (metis countable_def mem_Collect_eq rcset)
  with fin show ?thesis
    by (metis (poly_guards_query) cset_count_def someI_ex)
next
  case False note inf = this
  obtain count :: "'a ⇒ nat" where count_bij: "bij_betw count (rcset A) UNIV"
    by (metis countableE_infinite inf mem_Collect_eq rcset)
  with inf have "bij_betw (cset_count A) (rcset A) UNIV"
    by (metis (poly_guards_query) cset_count_def someI_ex)
  thus ?thesis
    by (metis bij_betw_imp_inj_on)
qed

lemma cset_count_infinite_bij:
  assumes "infinite (rcset A)"
  shows "bij_betw (cset_count A) (rcset A) UNIV"
proof -
  from assms obtain count :: "'a ⇒ nat" where count_bij: "bij_betw count (rcset A) UNIV"
    by (metis countableE_infinite mem_Collect_eq rcset)
  with assms show ?thesis
    by (metis (poly_guards_query) cset_count_def someI_ex)
qed

definition cset_seq :: "'a cset ⇒ (nat ⇀ 'a)" where
"cset_seq A i = (if (i ∈ range (cset_count A) ∧ inv_into (rcset A) (cset_count A) i ∈⇩c A)
                 then Some (inv_into (rcset A) (cset_count A) i)
                 else None)"

lemma cset_seq_ran: "ran (cset_seq A) = rcset(A)"
  apply (auto simp add: ran_def cset_seq_def cin.rep_eq)
  apply (metis cset_count_inj_seq inv_into_f_f rangeI)
  done

lemma cset_seq_inj: "inj cset_seq"
proof (rule injI)
  fix A B :: "'a cset"
  assume "cset_seq A = cset_seq B"
  thus "A = B"
    by (metis cset_seq_ran rcset_inverse)
qed

lift_definition cset2seq :: "'a cset ⇒ 'a seq"
is "(λ A i. if (i ∈ cset_count A ` rcset A) then inv_into (rcset A) (cset_count A) i else (SOME x. x ∈⇩c A))" .

lemma range_cset2seq:
  "A ≠ {}⇩c ⟹ range (Rep_seq (cset2seq A)) = rcset A"
  by (force intro: someI2 simp add: cset2seq.rep_eq cset_count_inj_seq bot_cset.rep_eq cin.rep_eq)

lemma infinite_cset_count_surj: "infinite (rcset A) ⟹ surj (cset_count A)"
  using bij_betw_imp_surj cset_count_infinite_bij by auto

lemma cset2seq_inj:
  "inj_on cset2seq {A. A ≠ {}⇩c}"
  apply (rule inj_onI)
  apply (simp)
  apply (metis range_cset2seq rcset_inject)
  done

lift_definition nat_seq2set :: "nat seq ⇒ nat set" is
"λ f. prod_encode ` {(x, f x) | x. True}" .

lemma inj_nat_seq2set: "inj nat_seq2set"
proof (rule injI, transfer)
  fix f g
  assume "prod_encode ` {(x, f x) |x. True} = prod_encode ` {(x, g x) |x. True}"
  hence "{(x, f x) |x. True} = {(x, g x) |x. True}"
    by (simp add: inj_image_eq_iff[OF inj_prod_encode])
  thus "f = g"
    by (auto simp add: set_eq_iff)
qed

lift_definition bit_seq_of_nat_set :: "nat set ⇒ bool seq"
is "λ A i. i ∈ A" .

lemma bit_seq_of_nat_set_inj: "inj bit_seq_of_nat_set"
  apply (rule injI)
  apply transfer
  apply (auto simp add: fun_eq_iff)
  done

lemma bit_seq_of_nat_cset_bij: "bij bit_seq_of_nat_set"
  apply (rule bijI)
   apply (fact bit_seq_of_nat_set_inj)
  apply transfer
  apply (rule surjI)
  apply auto
  done

text ‹ This function is a partial injection from countable sets of natural sets to natural sets.
        When used with the Schroeder-Bernstein theorem, it can be used to conjure a total
        bijection between these two types. ›

definition nat_set_cset_collapse :: "nat set cset ⇒ nat set" where
"nat_set_cset_collapse = inv bit_seq_of_nat_set ∘ seq_inj ∘ cset2seq ∘ (λ A. (bit_seq_of_nat_set `⇩c A))"

lemma nat_set_cset_collapse_inj: "inj_on nat_set_cset_collapse {A. A ≠ {}⇩c}"
proof -
  have "(`⇩c) bit_seq_of_nat_set ` {A. A ≠ {}⇩c} ⊆ {A. A ≠ {}⇩c}"
    by (auto simp add:cimage.rep_eq)
  thus ?thesis
    apply (simp add: nat_set_cset_collapse_def)
    apply (rule comp_inj_on)
     apply (meson bit_seq_of_nat_set_inj cset.inj_map injD inj_onI)
    apply (rule comp_inj_on)
     apply (metis cset2seq_inj subset_inj_on)
    apply (rule comp_inj_on)
     apply (rule subset_inj_on)
      apply (rule seq_inj)
     apply (simp)
    apply (meson UNIV_I bij_imp_bij_inv bij_is_inj bit_seq_of_nat_cset_bij subsetI subset_inj_on)
    done
qed

lemma inj_csingle:
  "inj csingle"
  by (auto intro: injI simp add: cinsert_def bot_cset.rep_eq)

lemma range_csingle:
  "range csingle ⊆ {A. A ≠ {}⇩c}"
  by (auto)

lift_definition csets :: "'a set ⇒ 'a cset set" is
"λ A. {B. B ⊆ A ∧ countable B}" by auto

lemma csets_finite: "finite A ⟹ finite (csets A)"
  by (auto simp add: csets_def)

lemma csets_infinite: "infinite A ⟹ infinite (csets A)"
  by (auto simp add: csets_def, metis csets.abs_eq csets.rep_eq finite_countable_subset finite_imageI)

lemma csets_UNIV:
  "csets (UNIV :: 'a set) = (UNIV :: 'a cset set)"
  by (auto simp add: csets_def, metis image_iff rcset rcset_inverse)

lemma infinite_nempty_cset:
  assumes "infinite (UNIV :: 'a set)"
  shows "infinite ({A. A ≠ {}⇩c} :: 'a cset set)"
proof -
  have "infinite (UNIV :: 'a cset set)"
    by (metis assms csets_UNIV csets_infinite)
  hence "infinite ((UNIV :: 'a cset set) - {{}⇩c})"
    by (rule infinite_remove)
  thus ?thesis
    by (auto)
qed

lemma nat_set_cset_partial_bij:
  obtains f :: "nat set cset ⇒ nat set" where "bij_betw f {A. A ≠ {}⇩c} UNIV"
  using Schroeder_Bernstein[OF nat_set_cset_collapse_inj, of UNIV csingle, simplified, OF inj_csingle range_csingle]
  by (auto)

lemma nat_set_cset_bij:
  obtains f :: "nat set cset ⇒ nat set" where "bij f"
proof -
  obtain g :: "nat set cset ⇒ nat set" where "bij_betw g {A. A ≠ {}⇩c} UNIV"
    using nat_set_cset_partial_bij by blast
  moreover obtain h :: "nat set cset ⇒ nat set cset" where "bij_betw h UNIV {A. A ≠ {}⇩c}"
  proof -
    have "infinite (UNIV :: nat set cset set)"
      by (metis Finite_Set.finite_set csets_UNIV csets_infinite infinite_UNIV_char_0)
    then obtain h' :: "nat set cset ⇒ nat set cset" where "bij_betw h' UNIV (UNIV - {{}⇩c})"
      using infinite_imp_bij_betw[of "UNIV :: nat set cset set" "{}⇩c"] by auto
    moreover have "(UNIV :: nat set cset set) - {{}⇩c} = {A. A ≠ {}⇩c}"
      by (auto)
    ultimately show ?thesis
      using that by (auto)
  qed
  ultimately have "bij (g ∘ h)"
    using bij_betw_trans by blast
  with that show ?thesis
    by (auto)
qed

definition "nat_set_cset_bij = (SOME f :: nat set cset ⇒ nat set. bij f)"

lemma bij_nat_set_cset_bij:
  "bij nat_set_cset_bij"
  by (metis nat_set_cset_bij nat_set_cset_bij_def someI_ex)

lemma inj_on_image_csets:
  "inj_on f A ⟹ inj_on ((`⇩c) f) (csets A)"
  by (fastforce simp add: inj_on_def cimage_def cin_def csets_def)

lemma image_csets_surj:
  "⟦ inj_on f A; f ` A = B ⟧ ⟹ (`⇩c) f ` csets A = csets B"
  apply (auto simp add: cimage_def csets_def image_mono map_fun_def)
  apply (simp add: image_comp)
  apply (auto simp add: image_Collect)
  apply (erule subset_imageE)
  using countable_image_inj_on subset_inj_on by blast

lemma bij_betw_image_csets:
  "bij_betw f A B ⟹ bij_betw ((`⇩c) f) (csets A) (csets B)"
  by (simp add: bij_betw_def inj_on_image_csets image_csets_surj)
end