--- a/src/HOL/Library/Multiset.thy Fri Nov 01 12:15:53 2024 +0000
+++ b/src/HOL/Library/Multiset.thy Fri Nov 01 14:10:52 2024 +0000
@@ -954,6 +954,9 @@
lemma repeat_mset_empty[simp]: "repeat_mset n {#} = {#}"
by transfer simp
+lemma set_mset_sum: "finite A \<Longrightarrow> set_mset (\<Sum>x\<in>A. f x) = (\<Union>x\<in>A. set_mset (f x))"
+ by (induction A rule: finite_induct) auto
+
subsubsection \<open>Simprocs\<close>
@@ -1554,6 +1557,12 @@
shows "A = replicate_mset (size A) x"
using assms by (induction A) auto
+lemma count_conv_size_mset: "count A x = size (filter_mset (\<lambda>y. y = x) A)"
+ by (induction A) auto
+
+lemma size_conv_count_bool_mset: "size A = count A True + count A False"
+ by (induction A) auto
+
subsubsection \<open>Strong induction and subset induction for multisets\<close>
@@ -1730,6 +1739,10 @@
image_mset f (filter_mset P A) + image_mset g (filter_mset (\<lambda>x. \<not>P x) A)"
by (induction A) auto
+lemma filter_image_mset:
+ "filter_mset P (image_mset f A) = image_mset f (filter_mset (\<lambda>x. P (f x)) A)"
+ by (induction A) auto
+
lemma image_mset_Diff:
assumes "B \<subseteq># A"
shows "image_mset f (A - B) = image_mset f A - image_mset f B"
@@ -1983,7 +1996,10 @@
by (induct x) auto
lemma mset_zero_iff_right[simp]: "({#} = mset x) = (x = [])"
-by (induct x) auto
+ by (induct x) auto
+
+lemma mset_replicate [simp]: "mset (replicate n x) = replicate_mset n x"
+ by (induction n) auto
lemma count_mset_gt_0: "x \<in> set xs \<Longrightarrow> count (mset xs) x > 0"
by (induction xs) auto
@@ -2798,6 +2814,15 @@
shows "sum f A = {#} \<longleftrightarrow> (\<forall>a\<in>A. f a = {#})"
using assms by induct simp_all
+lemma mset_concat: "mset (concat xss) = (\<Sum>xs\<leftarrow>xss. mset xs)"
+ by (induction xss) auto
+
+lemma sum_mset_singleton_mset [simp]: "(\<Sum>x\<in>#A. {#f x#}) = image_mset f A"
+ by (induction A) auto
+
+lemma sum_list_singleton_mset [simp]: "(\<Sum>x\<leftarrow>xs. {#f x#}) = image_mset f (mset xs)"
+ by (induction xs) auto
+
lemma Union_mset_empty_conv[simp]: "\<Sum>\<^sub># M = {#} \<longleftrightarrow> (\<forall>i\<in>#M. i = {#})"
by (induction M) auto
@@ -3090,6 +3115,19 @@
@ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs")
using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp
+lemma sort_append:
+ assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set ys \<Longrightarrow> x \<le> y"
+ shows "sort (xs @ ys) = sort xs @ sort ys"
+ using assms by (intro properties_for_sort) (auto simp: sorted_append)
+
+lemma sort_append_replicate_left:
+ "(\<And>y. y \<in> set xs \<Longrightarrow> x \<le> y) \<Longrightarrow> sort (replicate n x @ xs) = replicate n x @ sort xs"
+ by (subst sort_append) auto
+
+lemma sort_append_replicate_right:
+ "(\<And>y. y \<in> set xs \<Longrightarrow> x \<ge> y) \<Longrightarrow> sort (xs @ replicate n x) = sort xs @ replicate n x"
+ by (subst sort_append) auto
+
text \<open>A stable parameterized quicksort\<close>
definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where
--- a/src/HOL/List.thy Fri Nov 01 12:15:53 2024 +0000
+++ b/src/HOL/List.thy Fri Nov 01 14:10:52 2024 +0000
@@ -1751,6 +1751,12 @@
using less_Suc_eq_0_disj by auto
qed simp
+lemma nth_append_left: "i < length xs \<Longrightarrow> (xs @ ys) ! i = xs ! i"
+ by (auto simp: nth_append)
+
+lemma nth_append_right: "i \<ge> length xs \<Longrightarrow> (xs @ ys) ! i = ys ! (i - length xs)"
+ by (auto simp: nth_append)
+
lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
by (induct xs) auto
@@ -5892,49 +5898,53 @@
lemma sort_conv_fold:
"sort xs = fold insort xs []"
-by (rule sort_key_conv_fold) simp
+ by (rule sort_key_conv_fold) simp
lemma length_sort[simp]: "length (sort_key f xs) = length xs"
-by (induct xs, auto)
+ by (induct xs, auto)
lemma set_sort[simp]: "set(sort_key f xs) = set xs"
-by (induct xs) (simp_all add: set_insort_key)
+ by (induct xs) (simp_all add: set_insort_key)
lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
-by(induct xs)(auto simp: set_insort_key)
+ by(induct xs)(auto simp: set_insort_key)
lemma distinct_insort_key:
"distinct (map f (insort_key f x xs)) = (f x \<notin> f ` set xs \<and> (distinct (map f xs)))"
-by (induct xs) (auto simp: set_insort_key)
+ by (induct xs) (auto simp: set_insort_key)
lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
-by (induct xs) (simp_all add: distinct_insort)
+ by (induct xs) (simp_all add: distinct_insort)
lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
-by (induct xs) (auto simp: set_insort_key)
+ by (induct xs) (auto simp: set_insort_key)
lemma sorted_insort: "sorted (insort x xs) = sorted xs"
-using sorted_insort_key [where f="\<lambda>x. x"] by simp
+ using sorted_insort_key [where f="\<lambda>x. x"] by simp
theorem sorted_sort_key [simp]: "sorted (map f (sort_key f xs))"
-by (induct xs) (auto simp:sorted_insort_key)
+ by (induct xs) (auto simp:sorted_insort_key)
theorem sorted_sort [simp]: "sorted (sort xs)"
-using sorted_sort_key [where f="\<lambda>x. x"] by simp
+ using sorted_sort_key [where f="\<lambda>x. x"] by simp
lemma insort_not_Nil [simp]:
"insort_key f a xs \<noteq> []"
-by (induction xs) simp_all
+ by (induction xs) simp_all
lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
-by (cases xs) auto
+ by (cases xs) auto
lemma sort_key_id_if_sorted: "sorted (map f xs) \<Longrightarrow> sort_key f xs = xs"
-by (induction xs) (auto simp add: insort_is_Cons)
+ by (induction xs) (auto simp add: insort_is_Cons)
text \<open>Subsumed by @{thm sort_key_id_if_sorted} but easier to find:\<close>
lemma sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
-by (simp add: sort_key_id_if_sorted)
+ by (simp add: sort_key_id_if_sorted)
+
+lemma sort_replicate [simp]: "sort (replicate n x) = replicate n x"
+ using sorted_replicate sorted_sort_id
+ by presburger
lemma insort_key_remove1:
assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"
@@ -6488,6 +6498,32 @@
by (simp add: greaterThanAtMost_def greaterThanLessThan_eq lessThan_Suc_atMost)
+lemma sorted_wrt_induct [consumes 1, case_names Nil Cons]:
+ assumes "sorted_wrt R xs"
+ assumes "P []"
+ "\<And>x xs. (\<And>y. y \<in> set xs \<Longrightarrow> R x y) \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"
+ shows "P xs"
+ using assms(1) by (induction xs) (auto intro: assms)
+
+lemma sorted_wrt_trans_induct [consumes 2, case_names Nil single Cons]:
+ assumes "sorted_wrt R xs" "transp R"
+ assumes "P []" "\<And>x. P [x]"
+ "\<And>x y xs. R x y \<Longrightarrow> P (y # xs) \<Longrightarrow> P (x # y # xs)"
+ shows "P xs"
+ using assms(1)
+ by (induction xs rule: induct_list012)
+ (auto intro: assms simp: sorted_wrt2[OF assms(2)])
+
+lemmas sorted_induct [consumes 1, case_names Nil single Cons] =
+ sorted_wrt_trans_induct[OF _ preorder_class.transp_on_le]
+
+lemma sorted_wrt_map_mono:
+ assumes "sorted_wrt R xs"
+ assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> R x y \<Longrightarrow> R' (f x) (f y)"
+ shows "sorted_wrt R' (map f xs)"
+ using assms by (induction rule: sorted_wrt_induct) auto
+
+
subsubsection \<open>\<open>lists\<close>: the list-forming operator over sets\<close>
inductive_set
--- a/src/HOL/Product_Type.thy Fri Nov 01 12:15:53 2024 +0000
+++ b/src/HOL/Product_Type.thy Fri Nov 01 14:10:52 2024 +0000
@@ -1185,6 +1185,12 @@
"(\<lambda>(x,y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
by auto
+lemma Times_insert_right: "A \<times> insert y B = (\<lambda>x. (x, y)) ` A \<union> A \<times> B"
+ by auto
+
+lemma Times_insert_left: "insert x A \<times> B = (\<lambda>y. (x, y)) ` B \<union> A \<times> B"
+ by auto
+
lemma product_swap: "prod.swap ` (A \<times> B) = B \<times> A"
by (auto simp add: set_eq_iff)