# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1730470252 0
# Node ID 6f0cd46be030bd80b69399a92ff6b8a18cdf5445
# Parent  137b0b107c4b1d5d4fd443cc0e3140fde763a267
Library material from Eberl's Parallel_Shear_Sort

diff -r 137b0b107c4b -r 6f0cd46be030 src/HOL/Library/Multiset.thy
--- 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
diff -r 137b0b107c4b -r 6f0cd46be030 src/HOL/List.thy
--- 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
diff -r 137b0b107c4b -r 6f0cd46be030 src/HOL/Product_Type.thy
--- 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)