# HG changeset patch # User nipkow # Date 1749894356 -7200 # Node ID e0fb460181876c6ec97afcff7a3312d277d53d64 # Parent e2be3370ae0365a4baee0ac508aee0f0fec036cd more minus_list lemmas (incl code via fold instead of foldr) diff -r e2be3370ae03 -r e0fb46018187 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Sat Jun 14 00:22:10 2025 +0200 +++ b/src/HOL/Library/Multiset.thy Sat Jun 14 11:45:56 2025 +0200 @@ -4332,8 +4332,8 @@ lemma [code]: "filter_mset f (mset xs) = mset (filter f xs)" by simp -lemma [code]: "mset xs - mset ys = mset (fold remove1 ys xs)" - by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute diff_diff_add) +lemma [code]: "mset xs - mset ys = mset (minus_list_mset xs ys)" + by simp lemma [code]: "mset xs \# mset ys = diff -r e2be3370ae03 -r e0fb46018187 src/HOL/List.thy --- a/src/HOL/List.thy Sat Jun 14 00:22:10 2025 +0200 +++ b/src/HOL/List.thy Sat Jun 14 11:45:56 2025 +0200 @@ -4618,6 +4618,9 @@ "a \ set xs \ remove1 a xs = ys \ (\ls rs. xs = ls @ a # rs \ a \ set ls \ ys = ls @ rs)" by (metis remove1.simps(2) remove1_append split_list_first) +lemma foldr_fold_remove1[code_unfold]: "foldr remove1 = fold remove1" +using foldr_fold[of _ remove1] remove1_commute by fastforce + subsubsection \\<^const>\removeAll\\ @@ -4689,6 +4692,9 @@ by (auto simp: Cons) qed +lemma foldr_fold_removeAll[code_unfold]: "foldr removeAll = fold removeAll" +using foldr_fold[of _ removeAll] removeAll_commute by fastforce + subsubsection \\<^const>\minus_list_mset\\ @@ -4696,19 +4702,15 @@ i.e. up to the multiset of elements. Thus this function comes into its own in connection with multisets where \mset(minus_list_mset xs ys) = mset xs - mset ys\ is proved.\ -(* In Multiset: -lemma "mset(minus_list_mset xs ys) = mset xs - mset ys" -apply(induction ys) -apply (auto simp: minus_list_mset_def) -done -*) - lemma minus_list_mset_Nil2 [simp]: "minus_list_mset xs [] = xs" by (simp add: minus_list_mset_def) lemma minus_list_mset_Cons2 [simp]: "minus_list_mset xs (y#ys) = remove1 y (minus_list_mset xs ys)" by (simp add: minus_list_mset_def) +lemma minus_list_set_subset_minus_list_mset: "set xs - set ys \ set(minus_list_mset xs ys)" +by(induction ys arbitrary: xs)(simp, fastforce) + lemma minus_list_mset_remove1_commute: "minus_list_mset (remove1 x xs) ys = remove1 x (minus_list_mset xs ys)" by (induction ys) (auto simp: remove1_commute) @@ -4735,6 +4737,19 @@ lemma length_minus_list_mset: "length(minus_list_mset xs ys) \ length xs" by (induction ys) (auto simp: le_diff_conv length_remove1) +lemma minus_list_mset_subset: + "set (minus_list_mset xs ys) \ set xs" +by (induction ys) (simp, force) + +lemma distinct_minus_list_mset: + assumes "distinct xs" + shows "distinct (minus_list_mset xs ys)" +by (induction ys) (use assms in auto) + +lemma set_minus_list_mset_distinct: + assumes "distinct xs" shows "set (minus_list_mset xs ys) = set xs - set ys" +by (induction ys) (use assms distinct_minus_list_mset[of xs] in auto) + subsubsection \\<^const>\minus_list_set\\ @@ -4770,6 +4785,9 @@ lemma length_minus_list_set: "length(minus_list_set xs ys) \ length xs" by (simp add: minus_list_set_eq_filter) +lemma distinct_minus_list_set: "distinct xs \ distinct (minus_list_set xs ys)" +by (simp add: minus_list_set_eq_filter) + subsubsection \\<^const>\replicate\\