(* Author: René Thiemann Akihisa Yamada License: BSD *) section ‹Preliminaries› subsection ‹Missing Multiset› text ‹This theory provides some definitions and lemmas on multisets which we did not find in the Isabelle distribution.› theory Missing_Multiset imports "HOL-Library.Multiset" Missing_List begin lemma remove_nth_soundness: assumes "n < length as" shows "mset (remove_nth n as) = mset as - {#(as!n)#}" using assms proof (induct as arbitrary: n) case (Cons a as) note [simp] = remove_nth_def show ?case proof (cases n) case (Suc n) with Cons have n_bd: "n < length as" by auto with Cons have "mset (remove_nth n as) = mset as - {#as ! n#}" by auto hence G: "mset (remove_nth (Suc n) (a # as)) = mset as - {#as ! n#} + {#a#}" by simp thus ?thesis proof (cases "a = as!n") case True with G and Suc and insert_DiffM2[symmetric] and insert_DiffM2[of _ "{#as ! n#}"] and nth_mem_mset[of n as] and n_bd show ?thesis by auto next case False from G and Suc and diff_union_swap[OF this[symmetric], symmetric] show ?thesis by simp qed qed auto qed auto lemma multiset_subset_insert: "{ps. ps ⊆# add_mset x xs} = {ps. ps ⊆# xs} ∪ add_mset x ` {ps. ps ⊆# xs}" (is "?l = ?r") proof - { fix ps have "(ps ∈ ?l) = (ps ⊆# xs + {# x #})" by auto also have "… = (ps ∈ ?r)" proof (cases "x ∈# ps") case True then obtain qs where ps: "ps = qs + {#x#}" by (metis insert_DiffM2) show ?thesis unfolding ps mset_subset_eq_mono_add_right_cancel by (auto dest: mset_subset_eq_insertD) next case False hence id: "(ps ⊆# xs + {#x#}) = (ps ⊆# xs)" by (simp add: subset_mset.inf.absorb_iff2 inter_add_left1) show ?thesis unfolding id using False by auto qed finally have "(ps ∈ ?l) = (ps ∈ ?r)" . } thus ?thesis by auto qed lemma multiset_of_subseqs: "mset ` set (subseqs xs) = { ps. ps ⊆# mset xs}" proof (induct xs) case (Cons x xs) show ?case (is "?l = ?r") proof - have id: "?r = {ps. ps ⊆# mset xs} ∪ (add_mset x) ` {ps. ps ⊆# mset xs}" by (simp add: multiset_subset_insert) show ?thesis unfolding id Cons[symmetric] by (auto simp add: Let_def) (metis UnCI image_iff mset.simps(2)) qed qed simp lemma remove1_mset: "w ∈ set vs ⟹ mset (remove1 w vs) + {#w#} = mset vs" by (induct vs) auto lemma fold_remove1_mset: "mset ws ⊆# mset vs ⟹ mset (fold remove1 ws vs) + mset ws = mset vs" proof (induct ws arbitrary: vs) case (Cons w ws vs) from Cons(2) have "w ∈ set vs" using set_mset_mono by force from remove1_mset[OF this] have vs: "mset vs = mset (remove1 w vs) + {#w#}" by simp from Cons(2)[unfolded vs] have "mset ws ⊆# mset (remove1 w vs)" by auto from Cons(1)[OF this,symmetric] show ?case unfolding vs by (simp add: ac_simps) qed simp lemma subseqs_sub_mset: "ws ∈ set (subseqs vs) ⟹ mset ws ⊆# mset vs" proof (induct vs arbitrary: ws) case (Cons v vs Ws) note mem = Cons(2) note IH = Cons(1) show ?case proof (cases Ws) case (Cons w ws) show ?thesis proof (cases "v = w") case True from mem Cons have "ws ∈ set (subseqs vs)" by (auto simp: Let_def Cons_in_subseqsD[of _ ws vs]) from IH[OF this] show ?thesis unfolding Cons True by simp next case False with mem Cons have "Ws ∈ set (subseqs vs)" by (auto simp: Let_def Cons_in_subseqsD[of _ ws vs]) note IH = mset_subset_eq_count[OF IH[OF this]] with IH[of v] show ?thesis by (intro mset_subset_eqI, auto, linarith) qed qed simp qed simp lemma filter_mset_inequality: "filter_mset f xs ≠ xs ⟹ ∃ x ∈# xs. ¬ f x" by (induct xs, auto) end