# Theory Expander_Graphs_Multiset_Extras

subsection ‹Multisets›

text ‹Some preliminary results about multisets.›

theory Expander_Graphs_Multiset_Extras
imports

Extra_Congruence_Method
begin

unbundle intro_cong_syntax

text ‹This is an induction scheme over the distinct elements of a multisets:
We can represent each multiset as a sum like:
@{text "replicate_mset n1 x1 + replicate_mset n2 x2 + ... + replicate_mset nk xk"} where the
@{term "xi"} are distinct.›

lemma disj_induct_mset:
assumes "P {#}"
assumes "n M x. P M  ¬(x ∈# M)  n > 0  P (M + replicate_mset n x)"
shows "P M"
proof (induction "size M" arbitrary: M rule:nat_less_induct)
case 1
show ?case
proof (cases "M = {#}")
case True
then show ?thesis using assms by simp
next
case False
then obtain x where x_def: "x ∈# M" using multiset_nonemptyE by auto
define M1 where "M1 = M - replicate_mset (count M x) x"
then have M_def: "M = M1 + replicate_mset (count M x) x"
have "size M1 < size M"
by (metis M_def x_def count_greater_zero_iff less_add_same_cancel1 size_replicate_mset size_union)
hence "P M1" using 1 by blast
then show "P M"
apply (subst M_def, rule assms(2), simp)
qed
qed

lemma sum_mset_conv:
fixes f :: "'a  'b::{semiring_1}"
shows "sum_mset (image_mset f A) = sum (λx. of_nat (count A x) * f x) (set_mset A)"
proof (induction A rule: disj_induct_mset)
case 1
then show ?case by simp
next
case (2 n M x)
moreover have "count M x = 0" using 2 by (simp add: count_eq_zero_iff)
moreover have "y. y  set_mset M  y  x" using 2 by blast
ultimately show ?case by (simp add:algebra_simps)
qed

lemma sum_mset_conv_2:
fixes f :: "'a  'b::{semiring_1}"
assumes "set_mset A  B" "finite B"
shows "sum_mset (image_mset f A) = sum (λx. of_nat (count A x) * f x) B" (is "?L = ?R")
proof -
have "?L = sum (λx. of_nat (count A x) * f x) (set_mset A)"
unfolding sum_mset_conv by simp
also have "... = ?R"
by (intro sum.mono_neutral_left assms) (simp_all add: iffD2[OF count_eq_zero_iff])
finally show ?thesis by simp
qed

lemma count_mset_exp: "count A x = size (filter_mset (λy. y = x) A)"
by (induction A, simp, simp)

lemma mset_repl: "mset (replicate k x) = replicate_mset k x"
by (induction k, auto)

lemma count_image_mset_inj:
assumes "inj f"
shows "count (image_mset f A) (f x) = count A x"
proof (cases "x  set_mset A")
case True
hence "f -` {f x}  set_mset A = {x}"
using assms by (auto simp add:vimage_def inj_def)
then show ?thesis by (simp add:count_image_mset)
next
case False
hence "f -` {f x}  set_mset A = {}"
using assms by (auto simp add:vimage_def inj_def)
thus ?thesis  using False by (simp add:count_image_mset count_eq_zero_iff)
qed

lemma count_image_mset_0_triv:
assumes "x  range f"
shows "count (image_mset f A) x = 0"
proof -
have "x  set_mset (image_mset f A)"
using assms by auto
thus ?thesis
by (meson count_inI)
qed

lemma filter_mset_ex_predicates:
assumes "x. ¬ P x  ¬ Q x"
shows "filter_mset P M + filter_mset Q M = filter_mset (λx. P x  Q x) M"
using assms by (induction M, auto)

lemma sum_count_2:
assumes "finite F"
shows "sum (count M) F = size (filter_mset (λx. x  F) M)"
using assms
proof (induction F rule:finite_induct)
case empty
then show ?case by simp
next
case (insert x F)
have "sum (count M) (insert x F) = size ({#y ∈# M. y = x#} + {#x ∈# M. x  F#})"
also have "... = size ({#y ∈# M. y = x  y  F#})"
using insert(2)
by (intro arg_cong[where f="size"] filter_mset_ex_predicates) simp
also have "... = size (filter_mset (λy. y  insert x F) M)"
by simp
finally show ?case by simp
qed

definition concat_mset :: "('a multiset) multiset  'a multiset"
where "concat_mset xss = fold_mset (λxs ys. xs + ys) {#} xss"

lemma image_concat_mset:
"image_mset f (concat_mset xss) = concat_mset (image_mset (image_mset f) xss)"
unfolding concat_mset_def by (induction xss, auto)

"concat_mset (image_mset (λx. f x + g x) xs) = concat_mset (image_mset f xs) + concat_mset (image_mset g xs)"
unfolding concat_mset_def by (induction xs) auto

"concat_mset (xs + ys) = concat_mset xs + concat_mset ys"
unfolding concat_mset_def by (induction xs, auto)

lemma size_concat_mset:
"size (concat_mset xss) = sum_mset (image_mset size xss)"
unfolding concat_mset_def by (induction xss, auto)

lemma filter_concat_mset:
"filter_mset P (concat_mset xss) = concat_mset (image_mset (filter_mset P) xss)"
unfolding concat_mset_def by (induction xss, auto)

lemma count_concat_mset:
"count (concat_mset xss) xs = sum_mset (image_mset (λx. count x xs) xss)"
unfolding concat_mset_def by (induction xss, auto)

lemma set_mset_concat_mset:
"set_mset (concat_mset xss) =  (set_mset ` (set_mset xss))"
unfolding concat_mset_def by (induction xss, auto)

lemma concat_mset_empty:
unfolding concat_mset_def by simp

lemma concat_mset_single: "concat_mset {#x#} = x"
unfolding concat_mset_def by simp

lemma concat_disjoint_union_mset:
assumes "finite I"
assumes "i. i  I  finite (A i)"
assumes "i j. i  I  j  I  i  j  A i  A j = {}"
shows  "mset_set ( (A ` I)) = concat_mset (image_mset (mset_set  A) (mset_set I))"
using assms
proof (induction I rule:finite_induct)
case empty
then show ?case by (simp add:concat_mset_empty)
next
case (insert x F)
have "mset_set ( (A ` insert x F)) = mset_set (A x  ( (A ` F)))"
by simp
also have "... = mset_set (A x) + mset_set ( (A ` F))"
using insert by (intro mset_set_Union) auto
also have "... = mset_set (A x) + concat_mset (image_mset (mset_set  A) (mset_set F))"
using insert by (intro arg_cong2[where f="(+)"] insert(3)) auto
also have "... = concat_mset (image_mset (mset_set  A) ({#x#} + mset_set F))"
also have "... = concat_mset (image_mset (mset_set  A) (mset_set (insert x F)))"
using insert by (intro_cong ) auto
finally show ?case by blast
qed

lemma size_filter_mset_conv:
"size (filter_mset f A) = sum_mset (image_mset (λx. of_bool (f x) :: nat) A)"
by (induction A, auto)

lemma filter_mset_const: "filter_mset (λ_. c) xs = (if c then xs else {#})"
by simp

lemma repeat_image_concat_mset:
"repeat_mset n (image_mset f A) = concat_mset (image_mset (λx. replicate_mset n (f x)) A)"
unfolding concat_mset_def by (induction A, auto)

lemma mset_prod_eq:
assumes "finite A" "finite B"
shows
"mset_set (A × B) = concat_mset {# {# (x,y). y ∈# mset_set B #} .x ∈# mset_set A #}"
using assms(1)
proof (induction rule:finite_induct)
case empty
then show ?case unfolding concat_mset_def by simp
next
case (insert x F)
have "mset_set (insert x F × B) = mset_set (F × B  (λy. (x,y)) ` B)"
by (intro arg_cong[where f="mset_set"]) auto
also have "... = mset_set (F × B) + mset_set ((λy. (x,y)) ` B)"
using insert(1,2) assms(2) by (intro mset_set_Union finite_cartesian_product) auto
also have "... = mset_set (F × B) + {# (x,y). y ∈# mset_set B #}"
by (intro arg_cong2[where f="(+)"] image_mset_mset_set[symmetric] inj_onI) auto
also have "... = concat_mset {#image_mset (Pair x) (mset_set B). x ∈# {#x#} + (mset_set F)#}"