Theory Countably_Infinite_Multiset

section ‹Countably Infinite Multisets›

theory Countably_Infinite_Multiset
imports Countable_Multiset
begin

typedef 'a cinfmset = ‹{M :: 'a cmset. cminfinite M}›
  by (auto intro!: exI[of _ ‹cmconst _›])

setup_lifting type_definition_cinfmset

lift_bnf (no_warn_wits) 'a cinfmset
  for map: cinfmimage rel: cinfmrel
  by (auto simp: cminfinite_cmimage)

lift_definition cinfmcount :: ‹'a cinfmset ⇒ 'a ⇒ enat› is cmcount .

context begin
interpretation cmset_as_typedef .
lift_definition cinfmreplace :: ‹'a cinfmset ⇒ 'a ⇒ 'a ⇒ 'a cinfmset› is cmreplace
  by (rule cminfinite_cmreplace)

lemma set_infmset_alt: ‹set_cinfmset xs = {a. cinfmcount xs a ≠ 0}›
  unfolding set_cinfmset_def cinfmcount_def cmset_alt
  by auto

lemma set_cinfset_cinfmreplace: 
  ‹set_cinfmset (cinfmreplace M x y) ⊆ set_cinfmset M ∪ {y}›
  including cmset.lifting
proof transfer
  fix M :: ‹'a cmset› and x y
  assume ‹cminfinite M›
  show ‹cmset (cmreplace M x y) ⊆ cmset M ∪ {y}›
    by transfer auto
qed
end

lemma inj_cinfmcount: ‹inj cinfmcount›
  unfolding inj_on_def cinfmcount_def map_fun_def o_apply id_apply
  by (simp add: Rep_cinfmset_inject inj_cmcount inj_eq)

lemma in_range_cinfmcount:
  ‹countable {x. f x ≠ 0} ⟹ (∃x. f x = ∞) ∨ infinite {x. f x ≠ 0} ⟹ f ∈ range cinfmcount›
  by (drule in_range_cmcount) (smt (verit, best) Collect_cong Rep_cinfmset_cases UNIV_I cinfmcount.rep_eq cminfinite_alt image_iff mem_Collect_eq)

lemma cinfmcount_cinfmimage[simp]: 
  ‹cinfmcount (cinfmimage f M) b = isum (cinfmcount M) {a. f a = b}›
  by transfer (rule cmcount_cmimage)

lemma countable_nonzero_cinfmcount: ‹countable {x. cinfmcount M x ≠ 0}›
  by transfer (rule countable_nonzero_cmcount)

lemma infinite_nonzero_cinfmcount: ‹(∃x. cinfmcount M x = ∞) ∨ infinite {x. cinfmcount M x ≠ 0}›
  by transfer (simp add: cminfinite_alt)

lemma type_definition_cinfmset: ‹type_definition cinfmcount (inv cinfmcount) {f. countable {x. f x ≠ 0} ∧ ((∃x. f x = ∞) ∨ infinite {x. f x ≠ 0})}›
  by standard (auto simp: inj_cinfmcount in_range_cinfmcount inv_f_f f_inv_into_f countable_nonzero_cinfmcount infinite_nonzero_cinfmcount)

lifting_update cinfmset.lifting
lifting_forget cinfmset.lifting

definition get_cinfmset :: ‹'a cinfmset ⇒ nat ⇒ 'a› where
  ‹get_cinfmset M i = lnth (rep_cmset (Rep_cinfmset M)) i›

context includes cinfmset.lifting begin
interpretation cmset_as_Quotient .
lemma get_cinfmset_inject:
  ‹∀i. get_cinfmset M i = get_cinfmset N i ⟹ M = N›
  unfolding get_cinfmset_def
proof transfer
  fix M N :: ‹'a cmset›
  assume ‹cminfinite M› ‹cminfinite N›
    ‹∀i. lnth (rep_cmset M) i = lnth (rep_cmset N) i›
  then have ‹rep_cmset M = rep_cmset N›
    by (simp add: cminfinite.rep_eq linfinite_eq_llength lnth_equalityI)
  then show ‹M = N›
    by (metis UNIV_I cmcount.rep_eq inj_cmcount inj_on_def)
qed

end

end