Theory Misc.MultisetAdditional

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory MultisetAdditional
  imports Main "HOL-Library.Multiset" ListAdditional WordAdditional
begin
(*>*)

section ‹Some facts on multiset arithmetic›

subsection‹Some notation for multiset mapping›

syntax
  "_mset_from_mapped_list" :: ‹logic ⇒ pttrn ⇒ logic ⇒ logic› ("{# _ ∷ _ ← _ #}")
  "_mset_from_mapped_mset" :: ‹logic ⇒ pttrn ⇒ logic ⇒ logic› ("{# _ . _ ← _ #}")
  "_mset_from_anon_mapped_list" :: ‹logic ⇒ logic ⇒ logic› ("{# _ ∷ _ #}")
  "_mset_from_anon_mapped_mset" :: ‹logic ⇒ logic ⇒ logic› ("{# _ . _ #}")
translations
  "_mset_from_mapped_list entry var lst"      ⇌
    "(CONST Multiset.image_mset) (λvar. entry) ((CONST Multiset.mset) lst)"
  "_mset_from_mapped_mset entry var mset"      ⇌
    "(CONST Multiset.image_mset) (λvar. entry) mset"
  "_mset_from_anon_mapped_list entryfunc lst" ⇌
    "(CONST Multiset.image_mset) entryfunc     ((CONST Multiset.mset) lst)"
  "_mset_from_anon_mapped_mset entryfunc ms " ⇌
    "(CONST Multiset.image_mset) entryfunc ms"

notation image_mset (infixr ‹`#› 90)

(*<*)
notepad
begin
  fix t :: ‹nat ⇒ 'a set›
  have ‹{# t a ∷ (a, b) ← [(0,0),(1,1)] #} = {# λ(a, b). t a ∷ [(0,0), (1,1)] #}›
    by auto
end
(*>*)

subsection‹Alternative characterization of injectivity via multisets›

text‹Injectivity can be expressed as the equality of multiset-images and set-images:›
lemma inj_on_via_mset:
  assumes ‹finite A›
      and ‹image_mset f (mset_set A) = mset_set (f ` A)›
    shows ‹inj_on f A›
proof -
  {
       fix x y
    assume ‹x ∈ A›
       and ‹y ∈ A›
       and ‹x ≠ y›
       and ‹f x = f y›
    moreover from this have ‹{# x, y #} ⊆# mset_set A›
      by (simp add: assms(1) mset_set.remove)
    moreover from this have ‹{# f x, f y #} ⊆# (image_mset f (mset_set A))›
      using image_mset_subseteq_mono by fastforce
    ultimately have ‹count (image_mset f (mset_set A)) (f x) ≥ 2›
      by (metis (no_types, lifting) One_nat_def add.right_neutral add_Suc_right
        cancel_comm_monoid_add_class.diff_cancel count_add_mset count_diff nat_1_add_1
        subseteq_mset_def)
    from this have False
      by (simp add: ‹x ∈ A› assms)
  }
  from this show ?thesis
    by (auto simp add: inj_on_def)
qed

subsection‹Multiset decompositions›

lemma mset_sub_drop:
  shows ‹mset (drop n ls) ⊆# mset ls›
by (induction ls arbitrary: n; clarsimp) (metis append_take_drop_id mset.simps(2) mset_append
    mset_subset_eq_add_right)

lemma mset_nth_decomposition:
  assumes ‹n < length ls›
    shows ‹mset ls = mset (take n ls) + {# ls ! n #} + mset (drop (n+1) ls)›
using assms by (subst id_take_nth_drop [where i=n]) auto

lemma mset_drop_nth:
  assumes ‹n < length ls›
    shows ‹mset (drop_nth n ls) = mset (take n ls) + mset (drop (n+1) ls)›
using assms drop_nth_def by (metis mset_append)

lemma mset_drop_nth':
  assumes ‹n < length ls›
    shows ‹mset (drop_nth n ls) = mset ls - {# ls ! n #}›
using assms mset_nth_decomposition mset_drop_nth by fastforce

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma mset_drop_nth'':
  assumes ‹n < length ls›
    shows ‹mset ls = {# ls ! n #} + mset (drop_nth n ls)›
using mset_drop_nth' assms by fastforce

lemma mset_sub_drop_nth [intro]:
  assumes ‹n < length ls›
    shows ‹mset (drop_nth n ls) ⊆# mset ls›
using assms mset_drop_nth' by fastforce

named_theorems mset_simps

lemma mapped_multiset_eq [mset_simps]:
    fixes ms :: ‹'a multiset›
      and ξ τ :: ‹'a ⇒ 'b›
  assumes ‹∀x. (x∈#ms ⟶ ξ x = τ x)›
    shows ‹{# ξ . ms #} = {# τ . ms #}›
using assms by (metis multiset.map_cong)

lemma mset_set_minus_singletonE [elim]:
  assumes ‹i ∈# mset_set s - {#i#}›
    shows ‹R›
proof -
  have ‹⋀s j. count (mset_set s) j ≤ 1›
    by (metis count_mset_set order_refl zero_le)
  from this have ‹⋀s j. count (mset_set s - {#j#}) j = 0›
    by auto
  from this have False
    using assms by (metis count_eq_zero_iff)
  from this show ?thesis
    by auto
qed

lemma mset_range_minus_singletonE [elim]:
  assumes ‹i ∈# mset [0..<N] - {#i#}›
    shows ‹R›
using assms Multiset.mset_upt mset_set_minus_singletonE by auto

lemma mset_minus_drop_nth [mset_simps]:
  assumes ‹n < length ls›
    shows ‹mset ls - mset (drop_nth n ls) = {# ls ! n #}›
using assms mset_drop_nth' mset_nth_decomposition by fastforce

lemma mset_set_tagged:
  assumes ‹finite s›
    shows ‹mset_set s = (f `# ms') ⟷ (∃s'. (ms' = mset_set s') ∧ s = f ` s' ∧ inj_on f s')›
proof
  {
    assume ‹mset_set s = (f `# ms')›
    moreover from this [symmetric] and assms have ‹∀x. count (f `# ms') x ≤ 1›
      by (clarsimp simp add: count_mset_set')
    moreover have ‹∀x. count ms' x ≤ count (f `# ms') (f x)›
      by (metis count_le_replicate_mset_subset_eq image_mset_subseteq_mono
        image_replicate_mset le_refl)
    moreover from calculation have ‹∀x. count ms' x ≤ 1›
      using le_trans by blast
    ultimately have ‹ms' = mset_set (set_mset ms')›
      by (metis count_eq_zero_iff count_greater_eq_one_iff count_mset_set'
       finite_set_mset multi_count_eq nle_le)
  }
  moreover {
       fix r :: ‹'a ⇒ 'b›
       and t
    assume F: ‹finite t›
       and E: ‹r `# (mset_set t) = mset_set (r ` t)›
    {
         fix x y
      assume ‹x ∈ t›
         and ‹y ∈ t›
         and ‹x ≠ y›
         and ‹r x = r y›
      moreover from this and F have ‹ {# x, y #} ⊆#  mset_set t›
        by (simp add: mset_set.remove)
      moreover from this have ‹{# r x, r y #} ⊆# (r `# mset_set t)›
        using image_mset_subseteq_mono by fastforce
      moreover from calculation have ‹count (r `# mset_set t) (r x) ≥ 2›
        by (simp add: count_le_replicate_mset_subset_eq numeral_2_eq_2)
      ultimately have False
        using E by (metis count_mset_set(1) count_mset_set(2) count_mset_set(3) not_numeral_le_zero
          numeral_le_one_iff semiring_norm(69))
    }
    from this have ‹inj_on r t›
      by (metis inj_on_def)
  }
  ultimately show ‹mset_set s = (f `# ms') ⟹ (∃s'. (ms' = mset_set s') ∧ s = f ` s' ∧ inj_on f s')›
    using assms by (metis finite_set_mset finite_set_mset_mset_set inj_on_via_mset set_image_mset)
  show ‹(∃s'. (ms' = mset_set s') ∧ s = f ` s' ∧ inj_on f s') ⟹ mset_set s = (f `# ms')›
    by (metis image_mset_mset_set)
qed

definition map_from_graph :: ‹('a × 'b) set ⇒ 'a ⇒ 'b› where
  ‹map_from_graph g a ≡
    if a ∉ fst ` g then
      undefined
    else
      snd (SOME t. t ∈ g ∧ fst t = a)›

lemma map_from_graph_eval:
  assumes ‹(a, b) ∈ g›
      and ‹inj_on fst g›
    shows ‹map_from_graph g a = b›
proof -
  from assms have ‹{t. t ∈ g ∧ fst t = a} = {(a, b)}›
    by (intro equalityI subsetI; clarsimp simp add: inj_on_def)
  moreover from this have ‹(SOME t. t ∈ g ∧ fst t = a) = (a,b)›
    by blast
  moreover from calculation have ‹a ∈ fst ` g›
    by auto
  ultimately show ?thesis
    by (clarsimp simp add: map_from_graph_def)
qed

lemma map_from_graph_eval':
  assumes ‹t ∈ g›
      and ‹inj_on fst g›
    shows ‹map_from_graph g (fst t) = snd t›
using assms map_from_graph_eval by (metis prod.collapse)

lemma mset_map_sum_lift_single:
  shows ‹add_mset x ms0 = (f `# ms') ⟷ (∃x' ms0'. ms' = add_mset x' ms0' ∧ x = f x' ∧ ms0 = (f `# ms0'))›
by (metis (full_types) msed_map_invL msed_map_invR)

lemma mset_sum_count:
  shows ‹count (∑x ∈# ms. ξ x) t = (∑x ∈# ms. count (ξ x) t)›
by (induction ms; auto)

lemma set_product_sum:
  assumes ‹finite A›
      and ‹finite B›
    shows ‹(∑x∈#mset_set A. {# Pair x . mset_set B #}) = mset_set (A × B)›
proof -
  let ?P = ‹∑x∈#mset_set A. {# Pair x. mset_set B #}›
  have EQ: ‹⋀a b. count ?P (a,b) = (∑x∈#mset_set A. (count {# Pair x . mset_set B #} (a,b)))›
    by (simp add: mset_sum_count)
  moreover {
       fix a b x
    assume ‹x ∈# mset_set A›
       and ‹x ≠ a›
    then have ‹count {# Pair x . mset_set B #} (a,b) = 0›
      by (clarsimp simp add: count_image_mset)
  } moreover {
       fix a b x
    assume ‹x ∈# mset_set A›
       and ‹a ∉ A›
    then have ‹count {# Pair x . mset_set B #} (a,b) = 0›
      using assms calculation by fastforce
  } moreover {
       fix a b x
    assume ‹x ∈# mset_set A›
       and ‹b ∉ B›
    then have ‹count {# Pair x . mset_set B #} (a,b) = 0›
      using assms calculation by fastforce
  } moreover {
       fix a b
    assume ‹a ∈ A›
       and B: ‹b ∈ B›
    {
         fix x
      assume M: ‹x ∈# mset_set A›
      {
        assume ‹x = a›
        moreover have ‹Pair a -` {(a, b)} ∩ B = {b}›
          using ‹b ∈ B› by blast
        ultimately have ‹count {# Pair x . mset_set B #} (a,b) = 1›
          using assms B by (clarsimp simp add: count_image_mset)
      }
      from this and calculation have ‹count {# Pair x . mset_set B #} (a,b) = (if x = a then 1 else 0)›
        using M by meson
    }
    moreover from calculation have ‹count ?P (a,b) = (∑x∈#mset_set A. (if x = a then 1 else 0))›
      using image_mset_cong EQ by force
    moreover have ‹⋀ms t. (∑ x∈#ms. (if x = t then 1 else 0)) = count ms t›
      by (simp add: sum_mset_delta)
    moreover from this have ‹(∑x∈#mset_set A. (if x = a then 1 else 0)) = count (mset_set A) a›
      by force
    ultimately have ‹count ?P (a,b) = 1›
      by (simp add: ‹a ∈ A› assms(1))
  } moreover {
       fix a b
    assume ‹a ∉ A›
    then have ‹count ?P (a,b) = 0›
      using EQ calculation by force
  } moreover {
       fix a b
    assume ‹b ∉ B›
    then have ‹count ?P (a,b) = 0›
      using EQ calculation by auto
  }
  moreover from calculation have ‹⋀a b. count ?P (a,b) = (if (a,b) ∈ A × B then 1 else 0)›
    by (meson mem_Sigma_iff)
  moreover from calculation have ‹⋀ t. count ?P t = count (mset_set (A × B)) t›
    using assms by (clarsimp, simp add: count_mset_set')
  ultimately show ?thesis
    by (meson multi_count_eq)
qed

lemma multiset_map_comp':
  shows ‹{# ξ x . x ← {# f . ms #} #} = {# ξ (f y) . y ← ms #}›
using Multiset.Multiset.multiset.map_comp by (auto simp add: comp_def)

lemma multiset_map_comp_retract:
  assumes ‹⋀x. x ∈# ms ⟹ f (g x) = x›
    shows ‹{# ξ x . x ← ms #} = {# ξ (f y) . y ← {# g . ms #} #}›
using assms by (simp add: mapped_multiset_eq multiset_map_comp')

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma multiset_map_comp_word_cast_general:
    fixes ms :: ‹'a::{len} word multiset›
  assumes ‹⋀x. x ∈# ms ⟹ unat x < 2^LENGTH('b::{len})›
    shows ‹{# ξ x . x ← ms #} = {# ξ (ucast x) . x ← {# ucast::_ ⇒ 'b word . ms #} #}›
proof -
  let ?g = ‹ucast :: 'a word ⇒ 'b word›
  let ?f = ‹ucast :: 'b word ⇒ 'a word›
  have ‹⋀x. x ∈# ms ⟹ ?f (?g x) = x›
    using WordAdditional.ucast_ucast_eq assms by blast
  from this show ?thesis
    using multiset_map_comp_retract[where f=‹?f› and g=‹?g›] by blast
qed

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma multiset_map_comp_word_up_down:
    fixes ms :: ‹'a::{len} word multiset›
  assumes ‹LENGTH('a) ≤ LENGTH('b::{len})›
    shows ‹{# ξ x . x ← ms #} = {# ξ ((ucast x) :: 'a word) . x ← {# ucast::'a word ⇒ 'b word . ms #} #}›
by (simp add: assms eq_ucast_ucast_eq multiset_map_comp')

lemma multiset_map_comp_word_nat_cast:
    fixes ms :: ‹nat multiset›
  assumes ‹⋀x. x ∈# ms ⟹ x < 2^LENGTH('a::{len})›
    shows ‹{# ξ x . x ← ms #} = {# ξ (unat x) . x ← {# word_of_nat::nat ⇒ 'a word . ms #} #}›
proof -
  let ?g = ‹word_of_nat :: nat ⇒ 'a word›
  let ?f = ‹unat :: 'a word ⇒ nat›
  have ‹⋀x. x ∈# ms ⟹ ?f (?g x) = x›
    using assms unat_of_nat_len by blast
  from this show ?thesis
    using multiset_map_comp_retract[where f=‹?f› and g=‹?g›] by blast
qed

lemma multiset_map_comp_nat_word_cast:
  shows ‹{# ξ x . x ← ms #} = {# ξ (word_of_nat x) . x ← {# unat . ms #} #}›
by (simp add: multiset_map_comp')

lemma mset_reindex_core:
  shows ‹mset xs = {# xs ! i . i ← mset_set {0..<(length xs)} #}›
proof (induction xs)
  show ‹mset [] = {# (!) [] . mset_set {0..<length []} #}›
    by clarsimp
next
     fix x
     and xs :: ‹'a list›
  assume ‹mset xs = {# (!) xs . mset_set {0..<length xs} #}›
  from this show ‹mset (x # xs) = {# (!) (x # xs) . mset_set {0..<length (x # xs)} #}›
    by (metis map_nth mset_map mset_upt)
qed

lemma mset_reindex:
  assumes ‹length xs = hi›
    shows ‹mset xs = {# xs ! i . i ← mset_set {0..<hi} #}›
using mset_reindex_core assms by blast

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma set_upt_image_word_of_nat:
  assumes ‹b < 2^LENGTH('l::{len})›
    shows ‹{0..<(word_of_nat b::'l word)} = word_of_nat ` {0..<b}›
proof (intro set_eqI iffI)
     fix x :: ‹'l word›
  assume ‹x ∈ {0..<word_of_nat b}›
  from this show ‹x ∈ word_of_nat ` {0..<b}›
    by (metis atLeastLessThan_iff imageI le0 unat_less_helper word_unat.Rep_inverse)
next
     fix x :: ‹'l word›
  assume ‹x ∈ word_of_nat ` {0..<b}›
  moreover from this obtain y where ‹x = word_of_nat y›
    by blast
  ultimately show ‹x ∈ {0..<word_of_nat b}›
    using assms of_nat_mono_maybe by fastforce
qed

lemma set_upt_image_unat:
  shows ‹unat ` {0..<b} = {0..<unat b}›
by (auto simp add: unat_mono intro: set_eqI) (metis atLeastLessThan_iff image_eqI le_unat_uoi'
  word_coorder.extremum word_of_nat_less)

lemma mset_upt_nat_word_cast:
  fixes b :: ‹'l::{len} word›
  shows ‹{# unat . mset_set {0..<b} #} = mset_set {0..<(unat b)}›
proof -
  have ‹inj_on unat {0..<b}›
    by (simp add: set_upt_image_unat linorder_inj_onI')
  from image_mset_mset_set[OF this] show ?thesis
    by (simp add: set_upt_image_unat)
qed

lemma mset_upt_word_nat_cast:
  fixes b :: ‹'l::{len} word›
  shows ‹{# word_of_nat . mset_set {0..<(unat b)} #} = mset_set {0..<b}›
proof -
  have ‹mset_set {0..<b} = {# x . x ← mset_set {0..<b} #}›
    by auto
  also have ‹… = {# word_of_nat x . x ← {# unat . mset_set {0..<b} #} #}›
    using multiset_map_comp_nat_word_cast by blast
  also have ‹… = {# word_of_nat x . x ← mset_set {0..<(unat b)} #}›
    using mset_upt_nat_word_cast by metis
  finally show ?thesis
    by simp
qed

lemma mset_reindex_word:
    fixes hi :: ‹'l::{len} word›
  assumes ‹length xs = unat hi›
    shows ‹mset xs = {# xs ! unat i . i ← mset_set {0..<hi} #}›
proof -
  have bound: ‹⋀x. x ∈# mset_set {0..<(unat hi)} ⟹ x < 2^LENGTH('l)›
    by (meson atLeastLessThan_iff elem_mset_set finite_atLeastLessThan less_Suc_eq less_Suc_unat_less_bound)
  from mset_reindex_core have ‹mset xs = {# xs ! i . i ← mset_set {0..<(unat hi)} #}›
    using assms by metis
  also have ‹… = {# xs ! (unat i) . i ← {# (word_of_nat :: nat ⇒ 'l word) . mset_set {0..<(unat hi)} #} #}›
    using bound multiset_map_comp_word_nat_cast by blast
  also have ‹… = {# xs ! (unat i) . i ← mset_set {0..<hi} #}›
    by (simp add: mset_upt_word_nat_cast)
  finally show ?thesis by simp
qed

(*<*)
end
(*>*)