Theory multisets_continued

theory multisets_continued

(* N. Peltier - http://membres-lig.imag.fr/peltier/ *)

imports Main "HOL-Library.Multiset"

begin

subsection ‹Multisets›

text ‹We use the Multiset theory provided in Isabelle. We prove some additional 
(mostly trivial) lemmata.›

lemma mset_set_inclusion:
  assumes "finite E2"
  assumes "E1 ⊂ E2"  
  shows "mset_set E1 ⊂# (mset_set E2)"
proof (rule ccontr) 
  let ?s1 = "mset_set E1" 
  let ?s2 = "mset_set E2"
  assume "¬ ?s1 ⊂# ?s2"
  from assms(1) and assms(2) have "finite E1" using finite_subset less_imp_le by auto 
  from ‹¬ ?s1 ⊂# ?s2› obtain x where "(count ?s1 x > count ?s2 x)" using subseteq_mset_def [of ?s1 ?s2]
    by (metis assms(1) assms(2) finite_set_mset_mset_set finite_subset less_imp_le 
      less_le not_le_imp_less subset_mset.le_less) 
  from this have "count ?s1 x > 0" by linarith
  from this and ‹finite E1› have "count ?s1 x = 1" and "x ∈ E1" using subseteq_mset_def by auto
  from this and assms(2) have "x ∈ E2" by auto
  from this and ‹finite E2› have "count ?s2 x = 1" by auto
  from this and ‹count ?s1 x = 1› and ‹(count ?s1 x > count ?s2 x)› show False by auto
qed

lemma mset_ordering_addition:
  assumes "A = B + C"
  shows "B ⊆# A"
  using assms by simp

lemma equal_image_mset:
  assumes "∀x ∈ E. (f x) = (g x)"
  shows "{# (f x). x ∈# (mset_set E) #} = {# (g x). x ∈# (mset_set E)  #}"
by (meson assms count_eq_zero_iff count_mset_set(3) image_mset_cong)

lemma multiset_order_inclusion:
  assumes "E ⊂# F"
  assumes "trans r"
  shows "(E,F) ∈ (mult r)"
proof -
  let ?G = "F-E"
  from assms(1) have "F = E +?G"
    by (simp add: subset_mset.add_diff_inverse subset_mset_def) 
  from this assms(1) have "?G ≠ {#}"
    by fastforce
  have "E = E + {#}" by auto
  from this ‹F = E +?G›  ‹?G ≠ {#}› assms(2) show ?thesis  using one_step_implies_mult [of ?G "{#}" r E] by auto
qed

lemma multiset_order_inclusion_eq:
  assumes "E ⊆# F"
  assumes "trans r"
  shows "E = F ∨ (E,F) ∈ (mult r)"
proof (cases)
  assume "E = F"
  then show ?thesis by auto
next
  assume "E ≠ F"
  from this and assms(1) have "E ⊂# F" by auto
  from this assms(2) and multiset_order_inclusion show ?thesis by auto
qed

lemma image_mset_ordering:
  assumes "M1 = {# (f1 u). u ∈# L #}"
  assumes "M2 = {# (f2 u). u ∈# L #}"
  assumes "∀u. (u ∈# L ⟶ (((f1 u), (f2 u)) ∈ r ∨ (f1 u) = (f2 u)))"
  assumes "∃u. (u ∈# L ∧ ((f1 u), (f2 u)) ∈ r)"
  assumes "irrefl r"
  shows "( (M1,M2) ∈ (mult r) )"
proof -
  let ?L' = "{# u ∈# L.  (f1 u) = (f2 u) #}"
  let ?L'' = "{# u ∈# L.  (f1 u) ≠ (f2 u) #}"
  have "L = ?L' + ?L''" by (simp) 
  from assms(3) have "∀u. (u ∈# ?L'' ⟶ ((f1 u),(f2 u)) ∈ r)" by auto
  let ?M1' = "{# (f1 u). u ∈# ?L' #}"
  let ?M2' = "{# (f2 u). u ∈# ?L' #}"
  have "?M1' = ?M2'"
    by (metis (mono_tags, lifting) mem_Collect_eq multiset.map_cong0 set_mset_filter) 
  let ?M1'' = "{# (f1 u). u ∈# ?L'' #}"
  let ?M2'' = "{# (f2 u). u ∈# ?L'' #}"
  from ‹L = ?L' + ?L''› have "M1 = ?M1' + ?M1''" by (metis assms(1) image_mset_union) 
  from ‹L = ?L' + ?L''› have "M2 = ?M2' + ?M2''" by (metis assms(2) image_mset_union) 
  have dom: "(∀k ∈ set_mset ?M1''. ∃j ∈ set_mset ?M2''. (k, j) ∈ r)"  
  proof 
    fix k assume "k ∈ set_mset ?M1''"
    from this obtain u where "k = (f1 u)" and "u ∈# ?L''" by auto
    from ‹u ∈# ?L''› have "(f2 u) ∈# ?M2''" by simp
    from ‹∀u. (u ∈# ?L'' ⟶ ((f1 u),(f2 u)) ∈ r)› and ‹u ∈# ?L''› 
      have "((f1 u),(f2 u)) ∈ r" by auto
    from this and ‹k = (f1 u)› and ‹(f2 u) ∈ set_mset ?M2''›
      show "∃j ∈ set_mset ?M2''. (k, j) ∈ r" by auto
  qed
  have "?L'' ≠ {#}" 
  proof -
    from assms(4) obtain u where "u ∈# L" and "( (f1 u),(f2 u) ) ∈ r" by auto
    from assms(5) ‹( (f1 u),(f2 u) ) ∈ r› have "( (f1 u) ≠ (f2 u) )"  
      unfolding irrefl_def by fastforce 
    from ‹u ∈# L› ‹( (f1 u) ≠ (f2 u) )› have "u ∈# ?L''" by auto
    from this show ?thesis by force 
  qed
  from this have  "?M2'' ≠ {#}" by auto
  from this and dom and ‹M1 = ?M1' + ?M1''› ‹M2 = ?M2' + ?M2''› ‹?M1'=?M2'› 
  show "(M1,M2) ∈ (mult r)" by (simp add: one_step_implies_mult)
qed

lemma image_mset_ordering_eq:
  assumes "M1 = {# (f1 u). u ∈# L #}"
  assumes "M2 = {# (f2 u). u ∈# L #}"
  assumes "∀u. (u ∈# L ⟶ (((f1 u), (f2 u)) ∈ r ∨ (f1 u) = (f2 u)))"
  shows "(M1 = M2) ∨ ( (M1,M2) ∈ (mult r) )"
proof (cases)
  assume "M1 = M2" then show ?thesis by auto
  next assume "M1 ≠ M2"
  let ?L' = "{# u ∈# L.  (f1 u) = (f2 u) #}"
  let ?L'' = "{# u ∈# L.  (f1 u) ≠ (f2 u) #}"
  have "L = ?L' + ?L''" by (simp) 
  from assms(3) have "∀u. (u ∈# ?L'' ⟶ ((f1 u),(f2 u)) ∈ r)" by auto
  let ?M1' = "{# (f1 u). u ∈# ?L' #}"
  let ?M2' = "{# (f2 u). u ∈# ?L' #}"
  have "?M1' = ?M2'"
    by (metis (mono_tags, lifting) mem_Collect_eq multiset.map_cong0 set_mset_filter)
  let ?M1'' = "{# (f1 u). u ∈# ?L'' #}"
  let ?M2'' = "{# (f2 u). u ∈# ?L'' #}"
  from ‹L = ?L' + ?L''› have "M1 = ?M1' + ?M1''" by (metis assms(1) image_mset_union) 
  from ‹L = ?L' + ?L''› have "M2 = ?M2' + ?M2''" by (metis assms(2) image_mset_union) 
  have dom: "(∀k ∈ set_mset ?M1''. ∃j ∈ set_mset ?M2''. (k, j) ∈ r)"  
  proof 
    fix k assume "k ∈ set_mset ?M1''"
    from this obtain u where "k = (f1 u)" and "u ∈# ?L''" by auto
    from ‹u ∈# ?L''› have "(f2 u) ∈# ?M2''" by simp
    from ‹∀u. (u ∈# ?L'' ⟶ ((f1 u),(f2 u)) ∈ r)› and ‹u ∈# ?L''› 
      have "((f1 u),(f2 u)) ∈ r" by auto
    from this and ‹k = (f1 u)› and ‹(f2 u) ∈ set_mset ?M2''›
      show "∃j ∈ set_mset ?M2''. (k, j) ∈ r" by auto
  qed
  from ‹M1 ≠ M2› have  "?M2'' ≠ {#}"
    using ‹M1 = image_mset f1 {# u ∈# L. f1 u = f2 u#} + image_mset f1 {# u ∈# L. f1 u ≠ f2 u#}› ‹M2 = image_mset f2 {# u ∈# L. f1 u = f2 u#} + image_mset f2 {# u ∈# L. f1 u ≠ f2 u#}› ‹image_mset f1 {# u ∈# L. f1 u = f2 u#} = image_mset f2 {# u ∈# L. f1 u = f2 u#}› by auto 
  from this and dom and ‹M1 = ?M1' + ?M1''› ‹M2 = ?M2' + ?M2''› ‹?M1'=?M2'› 
  have "(M1,M2) ∈ (mult r)" by (simp add: one_step_implies_mult)
  from this show ?thesis by auto
qed

lemma mult1_def_lemma :
  assumes "M = M0 + {#a#} ∧ N = M0 + K ∧ (∀b. b ∈# K ⟶ (b, a) ∈ r)"
  shows "(N,M) ∈ (mult1 r)"
proof -
  from assms(1) show ?thesis using mult1_def [of r] by auto
qed

lemma mset_ordering_add1:
  assumes "(E1,E2) ∈ (mult r)"
  shows "(E1,E2 + {# a #}) ∈ (mult r)"
proof -
  have i: "(E2,E2 + {# a #}) ∈ (mult1 r)" using mult1_def_lemma [of "E2 + {# a #}" E2 a E2 "{#}" r] 
    by auto
  have i: "(E2,E2 + {# a #}) ∈ (mult1 r)" using mult1_def_lemma [of "E2 + {# a #}" E2 a E2 "{#}" r] 
    by auto
  from assms(1) have "(E1,E2) ∈ (mult1 r)⇧+" using mult_def by auto 
  from this and i have "(E1,E2 + {# a #}) ∈ (mult1 r)⇧+" by auto
  then show ?thesis using mult_def by auto
qed

lemma mset_ordering_singleton:
  assumes "∀x. (x ∈# E1 ⟶ (x,a) ∈ r)"
  shows "(E1, {# a #}) ∈ (mult r)"
proof -
  let ?K = "E1"
  let ?M0 = "{#}"
  have i: "E1 = ?M0 + ?K" by auto
  have ii: "{# a #} = ?M0 + {# a #}" by auto
  from assms(1) have iii: "∀x. (x ∈# ?K ⟶ (x,a) ∈ r)" by auto
  from i and ii and iii show ?thesis using mult1_def_lemma [of "{# a #}"  ?M0 a E1 ?K r] mult_def by auto 
qed


lemma monotonic_fun_mult1:
  assumes "⋀ t s. ((t,s) ∈ r ⟹ ((f t), (f s)) ∈ r)"
  assumes "(E1,E2) ∈ (mult1 r)"
  shows "({# (f x). x ∈# E1 #},{# (f x). x ∈# E2 #}) ∈  (mult1 r)"
proof -
  let ?E1 = "{# (f x). x ∈# E1 #}"
  let ?E2 = "{# (f x). x ∈# E2 #}"
  from assms(2) obtain M0 a K where "E2 = M0 + {#a#}" and "E1 = M0 + K" and "(∀b. b ∈# K ⟶ (b, a) ∈ r)" 
    unfolding mult1_def [of r]  by auto
  let ?K = "{# (f x). x ∈# K #}"
  let ?M0 = "{# (f x). x ∈# M0 #}"
  from ‹E2 = M0 + {#a#}› have "?E2 = ?M0 + {# (f a) #}" by simp 
  from ‹E1 = M0 + K› have "?E1 = ?M0 + ?K" by simp 
  have "(∀b. b ∈# ?K ⟶ (b, (f a)) ∈ r)"
  proof ((rule allI),(rule impI))
    fix b assume "b  ∈# ?K"
    from ‹b  ∈# ?K› obtain b' where "b = (f b')" and "b' ∈# K"
      by (auto simp: insert_DiffM2 msed_map_invR union_single_eq_member)
    from ‹b' ∈# K› and ‹(∀b. b ∈# K ⟶ (b, a) ∈ r)› have "(b',a) ∈ r" by auto
    from assms(1) and this and ‹b = (f b')› show "(b, (f a)) ∈ r" by auto
  qed
  from ‹?E1 = ?M0 + ?K› and ‹?E2 = ?M0 + {# (f a) #}› and ‹(∀b. b ∈# ?K ⟶ (b, (f a)) ∈ r)› 
    show "(?E1,?E2) ∈  (mult1 r)" by (metis mult1_def_lemma)
qed

lemma monotonic_fun_mult:
  assumes "⋀ t s. ((t,s) ∈ r ⟹ ((f t), (f s)) ∈ r)"
  assumes "(E1,E2) ∈ (mult r)"
  shows "({# (f x). x ∈# E1 #},{# (f x). x ∈# E2 #}) ∈  (mult r)"
proof -
  let ?E1 = "{# (f x). x ∈# E1 #}"
  let ?E2 = "{# (f x). x ∈# E2 #}"
  let ?P = "λx. (?E1,{# (f y). y ∈# x #}) ∈ (mult r)"
  show ?thesis
  proof (rule trancl_induct [of E1 E2 "(mult1 r)" ?P])
    from assms(1) show "(E1, E2) ∈ (mult1 r)⇧+" using assms(2) mult_def by blast
  next
    fix x assume "(E1, x) ∈ mult1 r" 
    have "(image_mset f E1, image_mset f x) ∈ mult1 r" 
      by (simp add: ‹(E1, x) ∈ mult1 r› assms(1) monotonic_fun_mult1) 
    from this show "(image_mset f E1, image_mset f x) ∈ mult r" by (simp add: mult_def) 
  next
    fix x z assume "(E1, x) ∈ (mult1 r)⇧+"
      "(x, z) ∈ mult1 r" and "(image_mset f E1, image_mset f x) ∈ mult r"
    from ‹(x, z) ∈ mult1 r› have "(image_mset f x, image_mset f z) ∈ mult1 r"
      by (simp add: assms(1) monotonic_fun_mult1) 
    from this and ‹(image_mset f E1, image_mset f x) ∈ mult r› 
      show "(image_mset f E1, image_mset f z) ∈ mult r" 
      using mult_def trancl.trancl_into_trancl by fastforce  
  qed
qed

lemma mset_set_insert_eq:
  assumes "finite E"
  shows "mset_set (E ∪ { x }) ⊆# mset_set E + {# x #}"
proof (rule ccontr)
  assume "¬ ?thesis"
  from this obtain y where "(count (mset_set (E ∪ { x })) y) 
    > (count (mset_set E + {# x #}) y)"
    by (meson leI subseteq_mset_def)
  from assms(1) have "finite (E ∪ { x })" by auto
  have "(count (mset_set E + {# x #}) y) = (count (mset_set E) y) + (count {# x #} y)" by auto
  have "x ≠ y"
  proof
    assume "x = y"
    then have "y ∈ E ∪ { x }" by auto
    from ‹finite (E ∪ { x })› this have "(count (mset_set (E ∪ { x })) y) = 1" 
      using count_mset_set(1) by auto
    from this and ‹(count (mset_set (E ∪ { x })) y) > (count (mset_set E + {# x #}) y)› have 
      "(count (mset_set E + {# x #}) y) = 0" by auto
    from ‹(count (mset_set E + {# x #}) y) = 0› have "count {# x #} y = 0" by auto
    from ‹x = y› have "count {# x #} y = 1" using count_mset_set by auto
    from this and ‹count {# x #} y = 0› show False by auto
  qed
  have "y ∉ E"
  proof 
    assume "y ∈ E"
    then have "y ∈ E ∪ { x }" by auto
    from ‹finite (E ∪ { x })› this have "(count (mset_set (E ∪ { x })) y) = 1" 
      using count_mset_set(1) by auto
    from this and ‹(count (mset_set (E ∪ { x })) y) > (count (mset_set E + {# x #}) y)› have 
      "(count (mset_set E + {# x #}) y) = 0" by auto
    from ‹(count (mset_set E + {# x #}) y) = 0› have "count (mset_set E) y = 0" by (simp split: if_splits)
    from ‹y ∈ E› ‹finite E› have "count (mset_set E) y = 1" using count_mset_set(1) by auto
    from this and ‹count (mset_set E) y = 0› show False by auto
  qed
  from this and ‹x ≠ y› have "y ∉ E ∪ { x }" by auto
  from this have "(count (mset_set (E ∪ { x })) y) = 0" by auto
  from this and ‹(count (mset_set (E ∪ { x })) y) 
    > (count (mset_set E + {# x #}) y)› show False by auto
qed
  
lemma mset_set_insert:
  assumes "x ∉ E"
  assumes "finite E"
  shows "mset_set (E ∪ { x }) = mset_set E + {# x #}"
proof (rule ccontr)
  assume "¬ ?thesis"
  from this obtain y where "(count (mset_set (E ∪ { x })) y) 
    ≠ (count (mset_set E + {# x #}) y)" by (meson multiset_eqI) 
  have "(count (mset_set E + {# x #}) y) = (count (mset_set E) y) + (count {# x #} y)" by auto
  from assms(2) have "finite (E ∪ { x })" by auto
  have "x ≠ y"
  proof
    assume "x = y"
    then have "y ∈ E ∪ { x }" by auto
    from ‹finite (E ∪ { x })› this have "(count (mset_set (E ∪ { x })) y) = 1" 
      using count_mset_set(1) by auto
    from ‹x = y› have "count {# x #} y = 1" using count_mset_set by auto
    from ‹x = y› ‹x ∉ E› have "(count (mset_set E) y) = 0"  using count_mset_set by auto
    from ‹count {# x #} y = 1› ‹(count (mset_set E) y) = 0› 
      ‹(count (mset_set E + {# x #}) y) = (count (mset_set E) y) + (count {# x #} y)› 
      have "(count (mset_set E + {# x #}) y) = 1" by auto
    from this and ‹(count (mset_set (E ∪ { x })) y) = 1› and ‹(count (mset_set (E ∪ { x })) y) 
    ≠ (count (mset_set E + {# x #}) y)› show False by auto
  qed
  from ‹x ≠ y› have "count {# x #} y = 0" using count_mset_set by auto
  have "y ∉ E"
  proof
    assume "y ∈ E"
    then have "y ∈ E ∪ { x }" by auto
    from ‹finite (E ∪ { x })› this have "(count (mset_set (E ∪ { x })) y) = 1" 
      using count_mset_set(1) by auto
    from assms(2) ‹y ∈ E› have "(count (mset_set E) y) = 1"  using count_mset_set by auto
    from ‹count {# x #} y = 0› ‹(count (mset_set E) y) = 1› 
      ‹(count (mset_set E + {# x #}) y) = (count (mset_set E) y) + (count {# x #} y)› 
      have "(count (mset_set E + {# x #}) y) = 1" by auto
    from this and ‹(count (mset_set (E ∪ { x })) y) = 1› and ‹(count (mset_set (E ∪ { x })) y) 
    ≠ (count (mset_set E + {# x #}) y)› show False by auto
  qed
  from this and ‹x ≠ y› have "y ∉ E ∪ { x }" by auto
  from this have "(count (mset_set (E ∪ { x })) y) = 0" by auto
  from ‹y ∉ E› have "(count (mset_set E) y) = 0" using count_mset_set by auto
  from ‹count {# x #} y = 0› ‹(count (mset_set E) y) = 0› 
      ‹(count (mset_set E + {# x #}) y) = (count (mset_set E) y) + (count {# x #} y)› 
      have "(count (mset_set E + {# x #}) y) = 0" by auto
   from this and ‹(count (mset_set (E ∪ { x })) y) = 0› and ‹(count (mset_set (E ∪ { x })) y) 
    ≠ (count (mset_set E + {# x #}) y)› show False by auto
qed

lemma mset_image_comp:
  shows "{# (f x). x ∈# {# (g x). x ∈# E #} #} = {# (f (g x)). x ∈# E #}"
   by (simp add: image_mset.compositionality comp_def)

lemma mset_set_mset_image:
  shows "⋀ E. card E = N ⟹ finite E ⟹ mset_set (g ` E) ⊆#  {# (g x). x ∈# mset_set (E) #}"
proof (induction N)
  case 0
    assume "card E = 0"
    assume "finite E"
    from this and ‹card E = 0› have "E = {}" by auto
    then show "mset_set (g ` E) ⊆#  {# (g x). x ∈# mset_set (E) #}" by auto
next
  case (Suc N)
    assume "card E = (Suc N)"
    assume "finite E"
    from this and ‹card E = (Suc N)› have "E ≠ {}" by auto
    from this obtain x where "x ∈ E" by auto
    let ?E = "E - { x }"
    from ‹finite E› ‹card E = (Suc N)› and ‹x ∈ E› have "card ?E = N" by auto
    from ‹finite E› have "finite ?E" by auto
    from this and "Suc.IH" [of ?E] and ‹card ?E = N› 
      have ind: "mset_set (g ` ?E) ⊆#  {# (g x). x ∈# mset_set (?E) #}" by force
    from ‹x ∈ E› have "E = ?E ∪ { x }" by auto
    have "x ∉ ?E" by auto
    from ‹finite ?E› ‹E = ?E ∪ { x }› and ‹x ∉ ?E› have "mset_set (?E ∪ { x }) = mset_set ?E + {# x #}" 
      using mset_set_insert [of x ?E] by auto
    from this have 
    "{# (g x). x ∈# mset_set (?E ∪ { x }) #} = {# (g x). x ∈# mset_set ?E #} + {# (g x) #}"
      by auto
    have "(g ` (?E ∪ { x }) = (g ` ?E) ∪ { g x })" by auto
    from this have i: "mset_set (g ` (?E ∪ { x })) = mset_set ( (g ` ?E) ∪ { g x } )" by auto 
    from ‹finite ?E› have "finite (g ` ?E)" by auto
    from this have "mset_set ( (g ` ?E) ∪ { g x } ) ⊆# mset_set (g ` ?E) + {# (g x) #}" 
        using  mset_set_insert_eq [of "(g ` ?E)" "(g x)" ] by meson
    from this i have ii: "mset_set (g ` (?E ∪ { x })) ⊆# mset_set (g ` ?E) + {# (g x) #}" by auto
    from ind have "mset_set (g ` ?E) + {# (g x) #} ⊆#  {# (g x). x ∈# mset_set (?E) #} + {# (g x) #}" 
      using Multiset.subset_mset.add_right_mono by metis
    from this and ii have "mset_set (g ` (?E ∪ { x })) ⊆# {# (g x). x ∈# mset_set (?E) #} + {# (g x) #}"
      using subset_mset.trans [of "mset_set (g ` (?E ∪ { x }))" ] by metis
    from this and ‹E = ?E ∪ { x }› ‹{# (g x). x ∈# mset_set (?E ∪ { x }) #} = {# (g x). x ∈# mset_set ?E #} + {# (g x) #}› 
     show "mset_set (g ` E) ⊆# {# (g x). x ∈# mset_set E #}" 
      by metis
qed

lemma split_mset_set: 
  assumes "C = C1 ∪ C2"
  assumes "C1 ∩ C2 = {}"
  assumes "finite C1"
  assumes "finite C2"
  shows "(mset_set C) = (mset_set C1) + (mset_set C2)"
proof (rule ccontr)
  assume "(mset_set C) ≠ (mset_set C1) + (mset_set C2)"
  then obtain x where "count (mset_set C) x ≠ count ((mset_set C1) + (mset_set C2)) x"
    by (meson multiset_eqI)
  from assms(3) assms(4) assms(1) have "finite C" by auto

  have "count ((mset_set C1) + (mset_set C2)) x = (count (mset_set C1) x) + (count (mset_set C2) x)"
    by auto
  from this and ‹count (mset_set C) x ≠ count ((mset_set C1) + (mset_set C2)) x› have 
    "count (mset_set C) x ≠ (count (mset_set C1) x) + (count (mset_set C2) x)" by auto
  have "x ∈ C1 ∨ x ∈ C2"
  proof (rule ccontr)
    assume "¬ (x ∈ C1 ∨ x ∈ C2)"
    then have "x ∉ C1" and "x∉ C2" by auto
    from assms(1) ‹x ∉ C1› and ‹x∉ C2› have "x ∉ C" by auto
    from ‹x ∉ C1› have "(count (mset_set C1) x) = 0" by auto
    from ‹x ∉ C2› have "(count (mset_set C2) x) = 0" by auto
    from ‹x ∉ C› have "(count (mset_set C) x) = 0" by auto
    from ‹(count (mset_set C1) x) = 0› ‹(count (mset_set C2) x) = 0› 
      ‹(count (mset_set C) x) = 0› 
      ‹count (mset_set C) x ≠ (count (mset_set C1) x) + (count (mset_set C2) x)›
      show False by auto
  qed

  have "(x ∉ C1 ∨ x ∈ C2)"
  proof (rule ccontr)
    assume "¬ (x ∉ C1 ∨ x ∈ C2)"  
    then have "x ∈ C1" and " x∉ C2" by auto
    from assms(1) ‹x ∈ C1› have "x ∈ C" by auto
    from assms(3) ‹x ∈ C1› have "(count (mset_set C1) x) = 1" by auto
    from ‹x ∉ C2› have "(count (mset_set C2) x) = 0" by auto
    from assms(3) assms(4) assms(1) have "finite C" by auto
    from ‹finite C› ‹x ∈ C› have "(count (mset_set C) x) = 1" by auto
    from ‹(count (mset_set C1) x) = 1› ‹(count (mset_set C2) x) = 0› 
      ‹(count (mset_set C) x) = 1› 
      ‹count (mset_set C) x ≠ (count (mset_set C1) x) + (count (mset_set C2) x)›
      show False by auto
  qed
  have "(x ∉ C2 ∨ x ∈ C1)"
  proof (rule ccontr)
    assume "¬ (x ∉ C2 ∨ x ∈ C1)"  
    then have "x ∈ C2" and " x∉ C1" by auto
    from assms(1) ‹x ∈ C2› have "x ∈ C" by auto
    from assms(4) ‹x ∈ C2› have "(count (mset_set C2) x) = 1" by auto
    from ‹x ∉ C1› have "(count (mset_set C1) x) = 0" by auto
    from ‹finite C› ‹x ∈ C› have "(count (mset_set C) x) = 1" by auto
    from ‹(count (mset_set C2) x) = 1› ‹(count (mset_set C1) x) = 0› 
      ‹(count (mset_set C) x) = 1› 
      ‹count (mset_set C) x ≠ (count (mset_set C1) x) + (count (mset_set C2) x)›
      show False by auto
  qed
  from ‹x ∈ C1 ∨ x ∈ C2› ‹(x ∉ C1 ∨ x ∈ C2)› ‹(x ∉ C2 ∨ x ∈ C1)›
    have "x ∈ C1 ∧ x ∈ C2" by blast
  from this and assms(2) show False by auto
qed

lemma image_mset_thm:
  assumes "E = {# (f x). x ∈# E' #}"
  assumes "x ∈# E"
  shows "∃ y. ((y ∈# E') ∧ x = (f y))"
using assms by auto

lemma split_image_mset:
  assumes "M = M1 + M2"
  shows "{# (f x). x ∈# M #} = {# (f x). x ∈# M1 #} + {# (f x). x ∈# M2 #}"
by (simp add: assms)

end