--- a/CONTRIBUTORS Fri Jan 08 20:40:56 2021 +0100
+++ b/CONTRIBUTORS Fri Jan 08 19:53:44 2021 +0100
@@ -6,6 +6,12 @@
Contributions to Isabelle2021
-----------------------------
+* January 2021: Manuel Eberl
+ Characteristic of a semiring
+
+* January 2021: Manuel Eberl
+ Algebraic integers in HOL-Computational_Algebra
+
* December 2020: Stepan Holub
Contributed lemmas for theory HOL.List.
--- a/NEWS Fri Jan 08 20:40:56 2021 +0100
+++ b/NEWS Fri Jan 08 19:53:44 2021 +0100
@@ -165,6 +165,13 @@
* For the natural numbers, "Sup {} = 0".
+* New constant semiring_char gives the characteristic of any type of
+class semiring_1, with the convenient notation CHAR('a). For example,
+CHAR(nat) = CHAR(int) = CHAR(real) = 0, CHAR(17) = 17.
+
+* HOL-Computational_Algebra.Polynomial: Definition and basic properties
+of algebraic integers.
+
* Library theory "Bit_Operations" with generic bit operations.
* Library theory "Signed_Division" provides operations for signed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Selection.thy Fri Jan 08 19:53:44 2021 +0100
@@ -0,0 +1,1038 @@
+(*
+ File: Data_Structures/Selection.thy
+ Author: Manuel Eberl, TU München
+*)
+section \<open>The Median-of-Medians Selection Algorithm\<close>
+theory Selection
+ imports Complex_Main Sorting Time_Funs
+begin
+
+text \<open>
+ Note that there is significant overlap between this theory (which is intended mostly for the
+ Functional Data Structures book) and the Median-of-Medians AFP entry.
+\<close>
+
+subsection \<open>Auxiliary material\<close>
+
+lemma replicate_numeral: "replicate (numeral n) x = x # replicate (pred_numeral n) x"
+ by (simp add: numeral_eq_Suc)
+
+lemma isort_correct: "isort xs = sort xs"
+ using sorted_isort mset_isort by (metis properties_for_sort)
+
+lemma sum_list_replicate [simp]: "sum_list (replicate n x) = n * x"
+ by (induction n) auto
+
+lemma mset_concat: "mset (concat xss) = sum_list (map mset xss)"
+ by (induction xss) simp_all
+
+lemma set_mset_sum_list [simp]: "set_mset (sum_list xs) = (\<Union>x\<in>set xs. set_mset x)"
+ by (induction xs) auto
+
+lemma filter_mset_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 filter_mset_sum_list: "filter_mset P (sum_list xs) = sum_list (map (filter_mset P) xs)"
+ by (induction xs) simp_all
+
+lemma sum_mset_mset_mono:
+ assumes "(\<And>x. x \<in># A \<Longrightarrow> f x \<subseteq># g x)"
+ shows "(\<Sum>x\<in>#A. f x) \<subseteq># (\<Sum>x\<in>#A. g x)"
+ using assms by (induction A) (auto intro!: subset_mset.add_mono)
+
+lemma mset_filter_mono:
+ assumes "A \<subseteq># B" "\<And>x. x \<in># A \<Longrightarrow> P x \<Longrightarrow> Q x"
+ shows "filter_mset P A \<subseteq># filter_mset Q B"
+ by (rule mset_subset_eqI) (insert assms, auto simp: mset_subset_eq_count count_eq_zero_iff)
+
+lemma size_mset_sum_mset_distrib: "size (sum_mset A :: 'a multiset) = sum_mset (image_mset size A)"
+ by (induction A) auto
+
+lemma sum_mset_mono:
+ assumes "\<And>x. x \<in># A \<Longrightarrow> f x \<le> (g x :: 'a :: {ordered_ab_semigroup_add,comm_monoid_add})"
+ shows "(\<Sum>x\<in>#A. f x) \<le> (\<Sum>x\<in>#A. g x)"
+ using assms by (induction A) (auto intro!: add_mono)
+
+lemma filter_mset_is_empty_iff: "filter_mset P A = {#} \<longleftrightarrow> (\<forall>x. x \<in># A \<longrightarrow> \<not>P x)"
+ by (auto simp: multiset_eq_iff count_eq_zero_iff)
+
+lemma sort_eq_Nil_iff [simp]: "sort xs = [] \<longleftrightarrow> xs = []"
+ by (metis set_empty set_sort)
+
+lemma sort_mset_cong: "mset xs = mset ys \<Longrightarrow> sort xs = sort ys"
+ by (metis sorted_list_of_multiset_mset)
+
+lemma Min_set_sorted: "sorted xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> Min (set xs) = hd xs"
+ by (cases xs; force intro: Min_insert2)
+
+lemma hd_sort:
+ fixes xs :: "'a :: linorder list"
+ shows "xs \<noteq> [] \<Longrightarrow> hd (sort xs) = Min (set xs)"
+ by (subst Min_set_sorted [symmetric]) auto
+
+lemma length_filter_conv_size_filter_mset: "length (filter P xs) = size (filter_mset P (mset xs))"
+ by (induction xs) auto
+
+lemma sorted_filter_less_subset_take:
+ assumes "sorted xs" and "i < length xs"
+ shows "{#x \<in># mset xs. x < xs ! i#} \<subseteq># mset (take i xs)"
+ using assms
+proof (induction xs arbitrary: i rule: list.induct)
+ case (Cons x xs i)
+ show ?case
+ proof (cases i)
+ case 0
+ thus ?thesis using Cons.prems by (auto simp: filter_mset_is_empty_iff)
+ next
+ case (Suc i')
+ have "{#y \<in># mset (x # xs). y < (x # xs) ! i#} \<subseteq># add_mset x {#y \<in># mset xs. y < xs ! i'#}"
+ using Suc Cons.prems by (auto)
+ also have "\<dots> \<subseteq># add_mset x (mset (take i' xs))"
+ unfolding mset_subset_eq_add_mset_cancel using Cons.prems Suc
+ by (intro Cons.IH) (auto)
+ also have "\<dots> = mset (take i (x # xs))" by (simp add: Suc)
+ finally show ?thesis .
+ qed
+qed auto
+
+lemma sorted_filter_greater_subset_drop:
+ assumes "sorted xs" and "i < length xs"
+ shows "{#x \<in># mset xs. x > xs ! i#} \<subseteq># mset (drop (Suc i) xs)"
+ using assms
+proof (induction xs arbitrary: i rule: list.induct)
+ case (Cons x xs i)
+ show ?case
+ proof (cases i)
+ case 0
+ thus ?thesis by (auto simp: sorted_append filter_mset_is_empty_iff)
+ next
+ case (Suc i')
+ have "{#y \<in># mset (x # xs). y > (x # xs) ! i#} \<subseteq># {#y \<in># mset xs. y > xs ! i'#}"
+ using Suc Cons.prems by (auto simp: set_conv_nth)
+ also have "\<dots> \<subseteq># mset (drop (Suc i') xs)"
+ using Cons.prems Suc by (intro Cons.IH) (auto)
+ also have "\<dots> = mset (drop (Suc i) (x # xs))" by (simp add: Suc)
+ finally show ?thesis .
+ qed
+qed auto
+
+
+subsection \<open>Chopping a list into equally-sized bits\<close>
+
+fun chop :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
+ "chop 0 _ = []"
+| "chop _ [] = []"
+| "chop n xs = take n xs # chop n (drop n xs)"
+
+lemmas [simp del] = chop.simps
+
+text \<open>
+ This is an alternative induction rule for \<^const>\<open>chop\<close>, which is often nicer to use.
+\<close>
+lemma chop_induct' [case_names trivial reduce]:
+ assumes "\<And>n xs. n = 0 \<or> xs = [] \<Longrightarrow> P n xs"
+ assumes "\<And>n xs. n > 0 \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> P n (drop n xs) \<Longrightarrow> P n xs"
+ shows "P n xs"
+ using assms
+proof induction_schema
+ show "wf (measure (length \<circ> snd))"
+ by auto
+qed (blast | simp)+
+
+lemma chop_eq_Nil_iff [simp]: "chop n xs = [] \<longleftrightarrow> n = 0 \<or> xs = []"
+ by (induction n xs rule: chop.induct; subst chop.simps) auto
+
+lemma chop_0 [simp]: "chop 0 xs = []"
+ by (simp add: chop.simps)
+
+lemma chop_Nil [simp]: "chop n [] = []"
+ by (cases n) (auto simp: chop.simps)
+
+lemma chop_reduce: "n > 0 \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> chop n xs = take n xs # chop n (drop n xs)"
+ by (cases n; cases xs) (auto simp: chop.simps)
+
+lemma concat_chop [simp]: "n > 0 \<Longrightarrow> concat (chop n xs) = xs"
+ by (induction n xs rule: chop.induct; subst chop.simps) auto
+
+lemma chop_elem_not_Nil [dest]: "ys \<in> set (chop n xs) \<Longrightarrow> ys \<noteq> []"
+ by (induction n xs rule: chop.induct; subst (asm) chop.simps)
+ (auto simp: eq_commute[of "[]"] split: if_splits)
+
+lemma length_chop_part_le: "ys \<in> set (chop n xs) \<Longrightarrow> length ys \<le> n"
+ by (induction n xs rule: chop.induct; subst (asm) chop.simps) (auto split: if_splits)
+
+lemma length_chop:
+ assumes "n > 0"
+ shows "length (chop n xs) = nat \<lceil>length xs / n\<rceil>"
+proof -
+ from \<open>n > 0\<close> have "real n * length (chop n xs) \<ge> length xs"
+ by (induction n xs rule: chop.induct; subst chop.simps) (auto simp: field_simps)
+ moreover from \<open>n > 0\<close> have "real n * length (chop n xs) < length xs + n"
+ by (induction n xs rule: chop.induct; subst chop.simps)
+ (auto simp: field_simps split: nat_diff_split_asm)+
+ ultimately have "length (chop n xs) \<ge> length xs / n" and "length (chop n xs) < length xs / n + 1"
+ using assms by (auto simp: field_simps)
+ thus ?thesis by linarith
+qed
+
+lemma sum_msets_chop: "n > 0 \<Longrightarrow> (\<Sum>ys\<leftarrow>chop n xs. mset ys) = mset xs"
+ by (subst mset_concat [symmetric]) simp_all
+
+lemma UN_sets_chop: "n > 0 \<Longrightarrow> (\<Union>ys\<in>set (chop n xs). set ys) = set xs"
+ by (simp only: set_concat [symmetric] concat_chop)
+
+lemma chop_append: "d dvd length xs \<Longrightarrow> chop d (xs @ ys) = chop d xs @ chop d ys"
+ by (induction d xs rule: chop_induct') (auto simp: chop_reduce dvd_imp_le)
+
+lemma chop_replicate [simp]: "d > 0 \<Longrightarrow> chop d (replicate d xs) = [replicate d xs]"
+ by (subst chop_reduce) auto
+
+lemma chop_replicate_dvd [simp]:
+ assumes "d dvd n"
+ shows "chop d (replicate n x) = replicate (n div d) (replicate d x)"
+proof (cases "d = 0")
+ case False
+ from assms obtain k where k: "n = d * k"
+ by blast
+ have "chop d (replicate (d * k) x) = replicate k (replicate d x)"
+ using False by (induction k) (auto simp: replicate_add chop_append)
+ thus ?thesis using False by (simp add: k)
+qed auto
+
+lemma chop_concat:
+ assumes "\<forall>xs\<in>set xss. length xs = d" and "d > 0"
+ shows "chop d (concat xss) = xss"
+ using assms
+proof (induction xss)
+ case (Cons xs xss)
+ have "chop d (concat (xs # xss)) = chop d (xs @ concat xss)"
+ by simp
+ also have "\<dots> = chop d xs @ chop d (concat xss)"
+ using Cons.prems by (intro chop_append) auto
+ also have "chop d xs = [xs]"
+ using Cons.prems by (subst chop_reduce) auto
+ also have "chop d (concat xss) = xss"
+ using Cons.prems by (intro Cons.IH) auto
+ finally show ?case by simp
+qed auto
+
+
+subsection \<open>Selection\<close>
+
+definition select :: "nat \<Rightarrow> ('a :: linorder) list \<Rightarrow> 'a" where
+ "select k xs = sort xs ! k"
+
+lemma select_0: "xs \<noteq> [] \<Longrightarrow> select 0 xs = Min (set xs)"
+ by (simp add: hd_sort select_def flip: hd_conv_nth)
+
+lemma select_mset_cong: "mset xs = mset ys \<Longrightarrow> select k xs = select k ys"
+ using sort_mset_cong[of xs ys] unfolding select_def by auto
+
+lemma select_in_set [intro,simp]:
+ assumes "k < length xs"
+ shows "select k xs \<in> set xs"
+proof -
+ from assms have "sort xs ! k \<in> set (sort xs)" by (intro nth_mem) auto
+ also have "set (sort xs) = set xs" by simp
+ finally show ?thesis by (simp add: select_def)
+qed
+
+lemma
+ assumes "n < length xs"
+ shows size_less_than_select: "size {#y \<in># mset xs. y < select n xs#} \<le> n"
+ and size_greater_than_select: "size {#y \<in># mset xs. y > select n xs#} < length xs - n"
+proof -
+ have "size {#y \<in># mset (sort xs). y < select n xs#} \<le> size (mset (take n (sort xs)))"
+ unfolding select_def using assms
+ by (intro size_mset_mono sorted_filter_less_subset_take) auto
+ thus "size {#y \<in># mset xs. y < select n xs#} \<le> n"
+ by simp
+ have "size {#y \<in># mset (sort xs). y > select n xs#} \<le> size (mset (drop (Suc n) (sort xs)))"
+ unfolding select_def using assms
+ by (intro size_mset_mono sorted_filter_greater_subset_drop) auto
+ thus "size {#y \<in># mset xs. y > select n xs#} < length xs - n"
+ using assms by simp
+qed
+
+
+subsection \<open>The designated median of a list\<close>
+
+definition median where "median xs = select ((length xs - 1) div 2) xs"
+
+lemma median_in_set [intro, simp]:
+ assumes "xs \<noteq> []"
+ shows "median xs \<in> set xs"
+proof -
+ from assms have "length xs > 0" by auto
+ hence "(length xs - 1) div 2 < length xs" by linarith
+ thus ?thesis by (simp add: median_def)
+qed
+
+lemma size_less_than_median: "size {#y \<in># mset xs. y < median xs#} \<le> (length xs - 1) div 2"
+proof (cases "xs = []")
+ case False
+ hence "length xs > 0"
+ by auto
+ hence less: "(length xs - 1) div 2 < length xs"
+ by linarith
+ show "size {#y \<in># mset xs. y < median xs#} \<le> (length xs - 1) div 2"
+ using size_less_than_select[OF less] by (simp add: median_def)
+qed auto
+
+lemma size_greater_than_median: "size {#y \<in># mset xs. y > median xs#} \<le> length xs div 2"
+proof (cases "xs = []")
+ case False
+ hence "length xs > 0"
+ by auto
+ hence less: "(length xs - 1) div 2 < length xs"
+ by linarith
+ have "size {#y \<in># mset xs. y > median xs#} < length xs - (length xs - 1) div 2"
+ using size_greater_than_select[OF less] by (simp add: median_def)
+ also have "\<dots> = length xs div 2 + 1"
+ using \<open>length xs > 0\<close> by linarith
+ finally show "size {#y \<in># mset xs. y > median xs#} \<le> length xs div 2"
+ by simp
+qed auto
+
+lemmas median_props = size_less_than_median size_greater_than_median
+
+
+subsection \<open>A recurrence for selection\<close>
+
+definition partition3 :: "'a \<Rightarrow> 'a :: linorder list \<Rightarrow> 'a list \<times> 'a list \<times> 'a list" where
+ "partition3 x xs = (filter (\<lambda>y. y < x) xs, filter (\<lambda>y. y = x) xs, filter (\<lambda>y. y > x) xs)"
+
+lemma partition3_code [code]:
+ "partition3 x [] = ([], [], [])"
+ "partition3 x (y # ys) =
+ (case partition3 x ys of (ls, es, gs) \<Rightarrow>
+ if y < x then (y # ls, es, gs) else if x = y then (ls, y # es, gs) else (ls, es, y # gs))"
+ by (auto simp: partition3_def)
+
+lemma sort_append:
+ assumes "\<forall>x\<in>set xs. \<forall>y\<in>set ys. x \<le> y"
+ shows "sort (xs @ ys) = sort xs @ sort ys"
+ using assms by (intro properties_for_sort) (auto simp: sorted_append)
+
+lemma select_append:
+ assumes "\<forall>y\<in>set ys. \<forall>z\<in>set zs. y \<le> z"
+ shows "k < length ys \<Longrightarrow> select k (ys @ zs) = select k ys"
+ and "k \<in> {length ys..<length ys + length zs} \<Longrightarrow>
+ select k (ys @ zs) = select (k - length ys) zs"
+ using assms by (simp_all add: select_def sort_append nth_append)
+
+lemma select_append':
+ assumes "\<forall>y\<in>set ys. \<forall>z\<in>set zs. y \<le> z" and "k < length ys + length zs"
+ shows "select k (ys @ zs) = (if k < length ys then select k ys else select (k - length ys) zs)"
+ using assms by (auto intro!: select_append)
+
+theorem select_rec_partition:
+ assumes "k < length xs"
+ shows "select k xs = (
+ let (ls, es, gs) = partition3 x xs
+ in
+ if k < length ls then select k ls
+ else if k < length ls + length es then x
+ else select (k - length ls - length es) gs
+ )" (is "_ = ?rhs")
+proof -
+ define ls es gs where "ls = filter (\<lambda>y. y < x) xs" and "es = filter (\<lambda>y. y = x) xs"
+ and "gs = filter (\<lambda>y. y > x) xs"
+ define nl ne where [simp]: "nl = length ls" "ne = length es"
+ have mset_eq: "mset xs = mset ls + mset es + mset gs"
+ unfolding ls_def es_def gs_def by (induction xs) auto
+ have length_eq: "length xs = length ls + length es + length gs"
+ unfolding ls_def es_def gs_def by (induction xs) auto
+ have [simp]: "select i es = x" if "i < length es" for i
+ proof -
+ have "select i es \<in> set (sort es)" unfolding select_def
+ using that by (intro nth_mem) auto
+ thus ?thesis
+ by (auto simp: es_def)
+ qed
+
+ have "select k xs = select k (ls @ (es @ gs))"
+ by (intro select_mset_cong) (simp_all add: mset_eq)
+ also have "\<dots> = (if k < nl then select k ls else select (k - nl) (es @ gs))"
+ unfolding nl_ne_def using assms
+ by (intro select_append') (auto simp: ls_def es_def gs_def length_eq)
+ also have "\<dots> = (if k < nl then select k ls else if k < nl + ne then x
+ else select (k - nl - ne) gs)"
+ proof (rule if_cong)
+ assume "\<not>k < nl"
+ have "select (k - nl) (es @ gs) =
+ (if k - nl < ne then select (k - nl) es else select (k - nl - ne) gs)"
+ unfolding nl_ne_def using assms \<open>\<not>k < nl\<close>
+ by (intro select_append') (auto simp: ls_def es_def gs_def length_eq)
+ also have "\<dots> = (if k < nl + ne then x else select (k - nl - ne) gs)"
+ using \<open>\<not>k < nl\<close> by auto
+ finally show "select (k - nl) (es @ gs) = \<dots>" .
+ qed simp_all
+ also have "\<dots> = ?rhs"
+ by (simp add: partition3_def ls_def es_def gs_def)
+ finally show ?thesis .
+qed
+
+
+subsection \<open>The size of the lists in the recursive calls\<close>
+
+text \<open>
+ We now derive an upper bound for the number of elements of a list that are smaller
+ (resp. bigger) than the median of medians with chopping size 5. To avoid having to do the
+ same proof twice, we do it generically for an operation \<open>\<prec>\<close> that we will later instantiate
+ with either \<open><\<close> or \<open>>\<close>.
+\<close>
+
+context
+ fixes xs :: "'a :: linorder list"
+ fixes M defines "M \<equiv> median (map median (chop 5 xs))"
+begin
+
+lemma size_median_of_medians_aux:
+ fixes R :: "'a :: linorder \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
+ assumes R: "R \<in> {(<), (>)}"
+ shows "size {#y \<in># mset xs. y \<prec> M#} \<le> nat \<lceil>0.7 * length xs + 3\<rceil>"
+proof -
+ define n and m where [simp]: "n = length xs" and "m = length (chop 5 xs)"
+ text \<open>We define an abbreviation for the multiset of all the chopped-up groups:\<close>
+
+ text \<open>We then split that multiset into those groups whose medians is less than @{term M}
+ and the rest.\<close>
+ define Y_small ("Y\<^sub>\<prec>") where "Y\<^sub>\<prec> = filter_mset (\<lambda>ys. median ys \<prec> M) (mset (chop 5 xs))"
+ define Y_big ("Y\<^sub>\<succeq>") where "Y\<^sub>\<succeq> = filter_mset (\<lambda>ys. \<not>(median ys \<prec> M)) (mset (chop 5 xs))"
+ have "m = size (mset (chop 5 xs))" by (simp add: m_def)
+ also have "mset (chop 5 xs) = Y\<^sub>\<prec> + Y\<^sub>\<succeq>" unfolding Y_small_def Y_big_def
+ by (rule multiset_partition)
+ finally have m_eq: "m = size Y\<^sub>\<prec> + size Y\<^sub>\<succeq>" by simp
+
+ text \<open>At most half of the lists have a median that is smaller than the median of medians:\<close>
+ have "size Y\<^sub>\<prec> = size (image_mset median Y\<^sub>\<prec>)" by simp
+ also have "image_mset median Y\<^sub>\<prec> = {#y \<in># mset (map median (chop 5 xs)). y \<prec> M#}"
+ unfolding Y_small_def by (subst filter_mset_image_mset [symmetric]) simp_all
+ also have "size \<dots> \<le> (length (map median (chop 5 xs))) div 2"
+ unfolding M_def using median_props[of "map median (chop 5 xs)"] R by auto
+ also have "\<dots> = m div 2" by (simp add: m_def)
+ finally have size_Y\<^sub>_small: "size Y\<^sub>\<prec> \<le> m div 2" .
+
+ text \<open>We estimate the number of elements less than @{term M} by grouping them into elements
+ coming from @{term "Y\<^sub>\<prec>"} and elements coming from @{term "Y\<^sub>\<succeq>"}:\<close>
+ have "{#y \<in># mset xs. y \<prec> M#} = {#y \<in># (\<Sum>ys\<leftarrow>chop 5 xs. mset ys). y \<prec> M#}"
+ by (subst sum_msets_chop) simp_all
+ also have "\<dots> = (\<Sum>ys\<leftarrow>chop 5 xs. {#y \<in># mset ys. y \<prec> M#})"
+ by (subst filter_mset_sum_list) (simp add: o_def)
+ also have "\<dots> = (\<Sum>ys\<in>#mset (chop 5 xs). {#y \<in># mset ys. y \<prec> M#})"
+ by (subst sum_mset_sum_list [symmetric]) simp_all
+ also have "mset (chop 5 xs) = Y\<^sub>\<prec> + Y\<^sub>\<succeq>"
+ by (simp add: Y_small_def Y_big_def not_le)
+ also have "(\<Sum>ys\<in>#\<dots>. {#y \<in># mset ys. y \<prec> M#}) =
+ (\<Sum>ys\<in>#Y\<^sub>\<prec>. {#y \<in># mset ys. y \<prec> M#}) + (\<Sum>ys\<in>#Y\<^sub>\<succeq>. {#y \<in># mset ys. y \<prec> M#})"
+ by simp
+
+ text \<open>Next, we overapproximate the elements contributed by @{term "Y\<^sub>\<prec>"}: instead of those elements
+ that are smaller than the median, we take \<^emph>\<open>all\<close> the elements of each group.
+ For the elements contributed by @{term "Y\<^sub>\<succeq>"}, we overapproximate by taking all those that
+ are less than their median instead of only those that are less than @{term M}.\<close>
+ also have "\<dots> \<subseteq># (\<Sum>ys\<in>#Y\<^sub>\<prec>. mset ys) + (\<Sum>ys\<in>#Y\<^sub>\<succeq>. {#y \<in># mset ys. y \<prec> median ys#})"
+ using R
+ by (intro subset_mset.add_mono sum_mset_mset_mono mset_filter_mono) (auto simp: Y_big_def)
+ finally have "size {# y \<in># mset xs. y \<prec> M#} \<le> size \<dots>"
+ by (rule size_mset_mono)
+ hence "size {# y \<in># mset xs. y \<prec> M#} \<le>
+ (\<Sum>ys\<in>#Y\<^sub>\<prec>. length ys) + (\<Sum>ys\<in>#Y\<^sub>\<succeq>. size {#y \<in># mset ys. y \<prec> median ys#})"
+ by (simp add: size_mset_sum_mset_distrib multiset.map_comp o_def)
+
+ text \<open>Next, we further overapproximate the first sum by noting that each group has
+ at most size 5.\<close>
+ also have "(\<Sum>ys\<in>#Y\<^sub>\<prec>. length ys) \<le> (\<Sum>ys\<in>#Y\<^sub>\<prec>. 5)"
+ by (intro sum_mset_mono) (auto simp: Y_small_def length_chop_part_le)
+ also have "\<dots> = 5 * size Y\<^sub>\<prec>" by simp
+
+ text \<open>Next, we note that each group in @{term "Y\<^sub>\<succeq>"} can have at most 2 elements that are
+ smaller than its median.\<close>
+ also have "(\<Sum>ys\<in>#Y\<^sub>\<succeq>. size {#y \<in># mset ys. y \<prec> median ys#}) \<le>
+ (\<Sum>ys\<in>#Y\<^sub>\<succeq>. length ys div 2)"
+ proof (intro sum_mset_mono, goal_cases)
+ fix ys assume "ys \<in># Y\<^sub>\<succeq>"
+ hence "ys \<noteq> []"
+ by (auto simp: Y_big_def)
+ thus "size {#y \<in># mset ys. y \<prec> median ys#} \<le> length ys div 2"
+ using R median_props[of ys] by auto
+ qed
+ also have "\<dots> \<le> (\<Sum>ys\<in>#Y\<^sub>\<succeq>. 2)"
+ by (intro sum_mset_mono div_le_mono diff_le_mono)
+ (auto simp: Y_big_def dest: length_chop_part_le)
+ also have "\<dots> = 2 * size Y\<^sub>\<succeq>" by simp
+
+ text \<open>Simplifying gives us the main result.\<close>
+ also have "5 * size Y\<^sub>\<prec> + 2 * size Y\<^sub>\<succeq> = 2 * m + 3 * size Y\<^sub>\<prec>"
+ by (simp add: m_eq)
+ also have "\<dots> \<le> 3.5 * m"
+ using \<open>size Y\<^sub>\<prec> \<le> m div 2\<close> by linarith
+ also have "\<dots> = 3.5 * \<lceil>n / 5\<rceil>"
+ by (simp add: m_def length_chop)
+ also have "\<dots> \<le> 0.7 * n + 3.5"
+ by linarith
+ finally have "size {#y \<in># mset xs. y \<prec> M#} \<le> 0.7 * n + 3.5"
+ by simp
+ thus "size {#y \<in># mset xs. y \<prec> M#} \<le> nat \<lceil>0.7 * n + 3\<rceil>"
+ by linarith
+qed
+
+lemma size_less_than_median_of_medians:
+ "size {#y \<in># mset xs. y < M#} \<le> nat \<lceil>0.7 * length xs + 3\<rceil>"
+ using size_median_of_medians_aux[of "(<)"] by simp
+
+lemma size_greater_than_median_of_medians:
+ "size {#y \<in># mset xs. y > M#} \<le> nat \<lceil>0.7 * length xs + 3\<rceil>"
+ using size_median_of_medians_aux[of "(>)"] by simp
+
+end
+
+
+subsection \<open>Efficient algorithm\<close>
+
+text \<open>
+ We handle the base cases and computing the median for the chopped-up sublists of size 5
+ using the naive selection algorithm where we sort the list using insertion sort.
+\<close>
+definition slow_select where
+ "slow_select k xs = isort xs ! k"
+
+definition slow_median where
+ "slow_median xs = slow_select ((length xs - 1) div 2) xs"
+
+lemma slow_select_correct: "slow_select k xs = select k xs"
+ by (simp add: slow_select_def select_def isort_correct)
+
+lemma slow_median_correct: "slow_median xs = median xs"
+ by (simp add: median_def slow_median_def slow_select_correct)
+
+text \<open>
+ The definition of the selection algorithm is complicated somewhat by the fact that its
+ termination is contingent on its correctness: if the first recursive call were to return an
+ element for \<open>x\<close> that is e.g. smaller than all list elements, the algorithm would not terminate.
+
+ Therefore, we first prove partial correctness, then termination, and then combine the two
+ to obtain total correctness.
+\<close>
+function mom_select where
+ "mom_select k xs = (
+ if length xs \<le> 20 then
+ slow_select k xs
+ else
+ let M = mom_select (((length xs + 4) div 5 - 1) div 2) (map slow_median (chop 5 xs));
+ (ls, es, gs) = partition3 M xs
+ in
+ if k < length ls then mom_select k ls
+ else if k < length ls + length es then M
+ else mom_select (k - length ls - length es) gs
+ )"
+ by auto
+
+text \<open>
+ If @{const "mom_select"} terminates, it agrees with @{const select}:
+\<close>
+lemma mom_select_correct_aux:
+ assumes "mom_select_dom (k, xs)" and "k < length xs"
+ shows "mom_select k xs = select k xs"
+ using assms
+proof (induction rule: mom_select.pinduct)
+ case (1 k xs)
+ show "mom_select k xs = select k xs"
+ proof (cases "length xs \<le> 20")
+ case True
+ thus "mom_select k xs = select k xs" using "1.prems" "1.hyps"
+ by (subst mom_select.psimps) (auto simp: select_def slow_select_correct)
+ next
+ case False
+ define x where
+ "x = mom_select (((length xs + 4) div 5 - 1) div 2) (map slow_median (chop 5 xs))"
+ define ls es gs where "ls = filter (\<lambda>y. y < x) xs" and "es = filter (\<lambda>y. y = x) xs"
+ and "gs = filter (\<lambda>y. y > x) xs"
+ define nl ne where "nl = length ls" and "ne = length es"
+ note defs = nl_def ne_def x_def ls_def es_def gs_def
+ have tw: "(ls, es, gs) = partition3 x xs"
+ unfolding partition3_def defs One_nat_def ..
+ have length_eq: "length xs = nl + ne + length gs"
+ unfolding nl_def ne_def ls_def es_def gs_def by (induction xs) auto
+ note IH = "1.IH"(2,3)[OF False x_def tw refl refl]
+
+ have "mom_select k xs = (if k < nl then mom_select k ls else if k < nl + ne then x
+ else mom_select (k - nl - ne) gs)" using "1.hyps" False
+ by (subst mom_select.psimps) (simp_all add: partition3_def flip: defs One_nat_def)
+ also have "\<dots> = (if k < nl then select k ls else if k < nl + ne then x
+ else select (k - nl - ne) gs)"
+ using IH length_eq "1.prems" by (simp add: ls_def es_def gs_def nl_def ne_def)
+ also have "\<dots> = select k xs" using \<open>k < length xs\<close>
+ by (subst (3) select_rec_partition[of _ _ x]) (simp_all add: nl_def ne_def flip: tw)
+ finally show "mom_select k xs = select k xs" .
+ qed
+qed
+
+text \<open>
+ @{const mom_select} indeed terminates for all inputs:
+\<close>
+lemma mom_select_termination: "All mom_select_dom"
+proof (relation "measure (length \<circ> snd)"; (safe)?)
+ fix k :: nat and xs :: "'a list"
+ assume "\<not> length xs \<le> 20"
+ thus "((((length xs + 4) div 5 - 1) div 2, map slow_median (chop 5 xs)), k, xs)
+ \<in> measure (length \<circ> snd)"
+ by (auto simp: length_chop nat_less_iff ceiling_less_iff)
+next
+ fix k :: nat and xs ls es gs :: "'a list"
+ define x where "x = mom_select (((length xs + 4) div 5 - 1) div 2) (map slow_median (chop 5 xs))"
+ assume A: "\<not> length xs \<le> 20"
+ "(ls, es, gs) = partition3 x xs"
+ "mom_select_dom (((length xs + 4) div 5 - 1) div 2,
+ map slow_median (chop 5 xs))"
+ have less: "((length xs + 4) div 5 - 1) div 2 < nat \<lceil>length xs / 5\<rceil>"
+ using A(1) by linarith
+
+ text \<open>For termination, it suffices to prove that @{term x} is in the list.\<close>
+ have "x = select (((length xs + 4) div 5 - 1) div 2) (map slow_median (chop 5 xs))"
+ using less unfolding x_def by (intro mom_select_correct_aux A) (auto simp: length_chop)
+ also have "\<dots> \<in> set (map slow_median (chop 5 xs))"
+ using less by (intro select_in_set) (simp_all add: length_chop)
+ also have "\<dots> \<subseteq> set xs"
+ unfolding set_map
+ proof safe
+ fix ys assume ys: "ys \<in> set (chop 5 xs)"
+ hence "median ys \<in> set ys"
+ by auto
+ also have "set ys \<subseteq> \<Union>(set ` set (chop 5 xs))"
+ using ys by blast
+ also have "\<dots> = set xs"
+ by (rule UN_sets_chop) simp_all
+ finally show "slow_median ys \<in> set xs"
+ by (simp add: slow_median_correct)
+ qed
+ finally have "x \<in> set xs" .
+ thus "((k, ls), k, xs) \<in> measure (length \<circ> snd)"
+ and "((k - length ls - length es, gs), k, xs) \<in> measure (length \<circ> snd)"
+ using A(1,2) by (auto simp: partition3_def intro!: length_filter_less[of x])
+qed
+
+termination mom_select by (rule mom_select_termination)
+
+lemmas [simp del] = mom_select.simps
+
+lemma mom_select_correct: "k < length xs \<Longrightarrow> mom_select k xs = select k xs"
+ using mom_select_correct_aux and mom_select_termination by blast
+
+
+
+subsection \<open>Running time analysis\<close>
+
+fun T_partition3 :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
+ "T_partition3 x [] = 1"
+| "T_partition3 x (y # ys) = T_partition3 x ys + 1"
+
+lemma T_partition3_eq: "T_partition3 x xs = length xs + 1"
+ by (induction x xs rule: T_partition3.induct) auto
+
+definition T_slow_select :: "nat \<Rightarrow> 'a :: linorder list \<Rightarrow> nat" where
+ "T_slow_select k xs = T_isort xs + T_nth (isort xs) k + 1"
+
+definition T_slow_median :: "'a :: linorder list \<Rightarrow> nat" where
+ "T_slow_median xs = T_slow_select ((length xs - 1) div 2) xs + 1"
+
+lemma T_slow_select_le: "T_slow_select k xs \<le> length xs ^ 2 + 3 * length xs + 3"
+proof -
+ have "T_slow_select k xs \<le> (length xs + 1)\<^sup>2 + (length (isort xs) + 1) + 1"
+ unfolding T_slow_select_def
+ by (intro add_mono T_isort_length) (auto simp: T_nth_eq)
+ also have "\<dots> = length xs ^ 2 + 3 * length xs + 3"
+ by (simp add: isort_correct algebra_simps power2_eq_square)
+ finally show ?thesis .
+qed
+
+lemma T_slow_median_le: "T_slow_median xs \<le> length xs ^ 2 + 3 * length xs + 4"
+ unfolding T_slow_median_def using T_slow_select_le[of "(length xs - 1) div 2" xs] by simp
+
+
+fun T_chop :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
+ "T_chop 0 _ = 1"
+| "T_chop _ [] = 1"
+| "T_chop n xs = T_take n xs + T_drop n xs + T_chop n (drop n xs)"
+
+lemmas [simp del] = T_chop.simps
+
+lemma T_chop_Nil [simp]: "T_chop d [] = 1"
+ by (cases d) (auto simp: T_chop.simps)
+
+lemma T_chop_0 [simp]: "T_chop 0 xs = 1"
+ by (auto simp: T_chop.simps)
+
+lemma T_chop_reduce:
+ "n > 0 \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> T_chop n xs = T_take n xs + T_drop n xs + T_chop n (drop n xs)"
+ by (cases n; cases xs) (auto simp: T_chop.simps)
+
+lemma T_chop_le: "T_chop d xs \<le> 5 * length xs + 1"
+ by (induction d xs rule: T_chop.induct) (auto simp: T_chop_reduce T_take_eq T_drop_eq)
+
+text \<open>
+ The option ‘domintros’ here allows us to explicitly reason about where the function does and
+ does not terminate. With this, we can skip the termination proof this time because we can
+ reuse the one for \<^const>\<open>mom_select\<close>.
+\<close>
+function (domintros) T_mom_select :: "nat \<Rightarrow> 'a :: linorder list \<Rightarrow> nat" where
+ "T_mom_select k xs = (
+ if length xs \<le> 20 then
+ T_slow_select k xs
+ else
+ let xss = chop 5 xs;
+ ms = map slow_median xss;
+ idx = (((length xs + 4) div 5 - 1) div 2);
+ x = mom_select idx ms;
+ (ls, es, gs) = partition3 x xs;
+ nl = length ls;
+ ne = length es
+ in
+ (if k < nl then T_mom_select k ls
+ else if k < nl + ne then 0
+ else T_mom_select (k - nl - ne) gs) +
+ T_mom_select idx ms + T_chop 5 xs + T_map T_slow_median xss +
+ T_partition3 x xs + T_length ls + T_length es + 1
+ )"
+ by auto
+
+termination T_mom_select
+proof (rule allI, safe)
+ fix k :: nat and xs :: "'a :: linorder list"
+ have "mom_select_dom (k, xs)"
+ using mom_select_termination by blast
+ thus "T_mom_select_dom (k, xs)"
+ by (induction k xs rule: mom_select.pinduct)
+ (rule T_mom_select.domintros, simp_all)
+qed
+
+lemmas [simp del] = T_mom_select.simps
+
+
+function T'_mom_select :: "nat \<Rightarrow> nat" where
+ "T'_mom_select n =
+ (if n \<le> 20 then
+ 463
+ else
+ T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n+3\<rceil>) + 17 * n + 50)"
+ by force+
+termination by (relation "measure id"; simp; linarith)
+
+lemmas [simp del] = T'_mom_select.simps
+
+
+lemma T'_mom_select_ge: "T'_mom_select n \<ge> 463"
+ by (induction n rule: T'_mom_select.induct; subst T'_mom_select.simps) auto
+
+lemma T'_mom_select_mono:
+ "m \<le> n \<Longrightarrow> T'_mom_select m \<le> T'_mom_select n"
+proof (induction n arbitrary: m rule: less_induct)
+ case (less n m)
+ show ?case
+ proof (cases "m \<le> 20")
+ case True
+ hence "T'_mom_select m = 463"
+ by (subst T'_mom_select.simps) auto
+ also have "\<dots> \<le> T'_mom_select n"
+ by (rule T'_mom_select_ge)
+ finally show ?thesis .
+ next
+ case False
+ hence "T'_mom_select m =
+ T'_mom_select (nat \<lceil>0.2*m\<rceil>) + T'_mom_select (nat \<lceil>0.7*m + 3\<rceil>) + 17 * m + 50"
+ by (subst T'_mom_select.simps) auto
+ also have "\<dots> \<le> T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>) + 17 * n + 50"
+ using \<open>m \<le> n\<close> and False by (intro add_mono less.IH; linarith)
+ also have "\<dots> = T'_mom_select n"
+ using \<open>m \<le> n\<close> and False by (subst T'_mom_select.simps) auto
+ finally show ?thesis .
+ qed
+qed
+
+lemma T_mom_select_le_aux: "T_mom_select k xs \<le> T'_mom_select (length xs)"
+proof (induction k xs rule: T_mom_select.induct)
+ case (1 k xs)
+ define n where [simp]: "n = length xs"
+ define x where
+ "x = mom_select (((length xs + 4) div 5 - 1) div 2) (map slow_median (chop 5 xs))"
+ define ls es gs where "ls = filter (\<lambda>y. y < x) xs" and "es = filter (\<lambda>y. y = x) xs"
+ and "gs = filter (\<lambda>y. y > x) xs"
+ define nl ne where "nl = length ls" and "ne = length es"
+ note defs = nl_def ne_def x_def ls_def es_def gs_def
+ have tw: "(ls, es, gs) = partition3 x xs"
+ unfolding partition3_def defs One_nat_def ..
+ note IH = "1.IH"(1,2,3)[OF _ refl refl refl x_def tw refl refl refl refl]
+
+ show ?case
+ proof (cases "length xs \<le> 20")
+ case True \<comment> \<open>base case\<close>
+ hence "T_mom_select k xs \<le> (length xs)\<^sup>2 + 3 * length xs + 3"
+ using T_slow_select_le[of k xs] by (subst T_mom_select.simps) auto
+ also have "\<dots> \<le> 20\<^sup>2 + 3 * 20 + 3"
+ using True by (intro add_mono power_mono) auto
+ also have "\<dots> \<le> 463"
+ by simp
+ also have "\<dots> = T'_mom_select (length xs)"
+ using True by (simp add: T'_mom_select.simps)
+ finally show ?thesis by simp
+ next
+ case False \<comment> \<open>recursive case\<close>
+ have "((n + 4) div 5 - 1) div 2 < nat \<lceil>n / 5\<rceil>"
+ using False unfolding n_def by linarith
+ hence "x = select (((n + 4) div 5 - 1) div 2) (map slow_median (chop 5 xs))"
+ unfolding x_def n_def by (intro mom_select_correct) (auto simp: length_chop)
+ also have "((n + 4) div 5 - 1) div 2 = (nat \<lceil>n / 5\<rceil> - 1) div 2"
+ by linarith
+ also have "select \<dots> (map slow_median (chop 5 xs)) = median (map slow_median (chop 5 xs))"
+ by (auto simp: median_def length_chop)
+ finally have x_eq: "x = median (map slow_median (chop 5 xs))" .
+
+ text \<open>The cost of computing the medians of all the subgroups:\<close>
+ define T_ms where "T_ms = T_map T_slow_median (chop 5 xs)"
+ have "T_ms \<le> 9 * n + 45"
+ proof -
+ have "T_ms = (\<Sum>ys\<leftarrow>chop 5 xs. T_slow_median ys) + length (chop 5 xs) + 1"
+ by (simp add: T_ms_def T_map_eq)
+ also have "(\<Sum>ys\<leftarrow>chop 5 xs. T_slow_median ys) \<le> (\<Sum>ys\<leftarrow>chop 5 xs. 44)"
+ proof (intro sum_list_mono)
+ fix ys assume "ys \<in> set (chop 5 xs)"
+ hence "length ys \<le> 5"
+ using length_chop_part_le by blast
+ have "T_slow_median ys \<le> (length ys) ^ 2 + 3 * length ys + 4"
+ by (rule T_slow_median_le)
+ also have "\<dots> \<le> 5 ^ 2 + 3 * 5 + 4"
+ using \<open>length ys \<le> 5\<close> by (intro add_mono power_mono) auto
+ finally show "T_slow_median ys \<le> 44" by simp
+ qed
+ also have "(\<Sum>ys\<leftarrow>chop 5 xs. 44) + length (chop 5 xs) + 1 =
+ 45 * nat \<lceil>real n / 5\<rceil> + 1"
+ by (simp add: map_replicate_const length_chop)
+ also have "\<dots> \<le> 9 * n + 45"
+ by linarith
+ finally show "T_ms \<le> 9 * n + 45" by simp
+ qed
+
+ text \<open>The cost of the first recursive call (to compute the median of medians):\<close>
+ define T_rec1 where
+ "T_rec1 = T_mom_select (((length xs + 4) div 5 - 1) div 2) (map slow_median (chop 5 xs))"
+ have "T_rec1 \<le> T'_mom_select (length (map slow_median (chop 5 xs)))"
+ using False unfolding T_rec1_def by (intro IH(3)) auto
+ hence "T_rec1 \<le> T'_mom_select (nat \<lceil>0.2 * n\<rceil>)"
+ by (simp add: length_chop)
+
+ text \<open>The cost of the second recursive call (to compute the final result):\<close>
+ define T_rec2 where "T_rec2 = (if k < nl then T_mom_select k ls
+ else if k < nl + ne then 0
+ else T_mom_select (k - nl - ne) gs)"
+ consider "k < nl" | "k \<in> {nl..<nl+ne}" | "k \<ge> nl+ne"
+ by force
+ hence "T_rec2 \<le> T'_mom_select (nat \<lceil>0.7 * n + 3\<rceil>)"
+ proof cases
+ assume "k < nl"
+ hence "T_rec2 = T_mom_select k ls"
+ by (simp add: T_rec2_def)
+ also have "\<dots> \<le> T'_mom_select (length ls)"
+ by (rule IH(1)) (use \<open>k < nl\<close> False in \<open>auto simp: defs\<close>)
+ also have "length ls \<le> nat \<lceil>0.7 * n + 3\<rceil>"
+ unfolding ls_def using size_less_than_median_of_medians[of xs]
+ by (auto simp: length_filter_conv_size_filter_mset slow_median_correct[abs_def] x_eq)
+ hence "T'_mom_select (length ls) \<le> T'_mom_select (nat \<lceil>0.7 * n + 3\<rceil>)"
+ by (rule T'_mom_select_mono)
+ finally show ?thesis .
+ next
+ assume "k \<in> {nl..<nl + ne}"
+ hence "T_rec2 = 0"
+ by (simp add: T_rec2_def)
+ thus ?thesis
+ using T'_mom_select_ge[of "nat \<lceil>0.7 * n + 3\<rceil>"] by simp
+ next
+ assume "k \<ge> nl + ne"
+ hence "T_rec2 = T_mom_select (k - nl - ne) gs"
+ by (simp add: T_rec2_def)
+ also have "\<dots> \<le> T'_mom_select (length gs)"
+ unfolding nl_def ne_def by (rule IH(2)) (use \<open>k \<ge> nl + ne\<close> False in \<open>auto simp: defs\<close>)
+ also have "length gs \<le> nat \<lceil>0.7 * n + 3\<rceil>"
+ unfolding gs_def using size_greater_than_median_of_medians[of xs]
+ by (auto simp: length_filter_conv_size_filter_mset slow_median_correct[abs_def] x_eq)
+ hence "T'_mom_select (length gs) \<le> T'_mom_select (nat \<lceil>0.7 * n + 3\<rceil>)"
+ by (rule T'_mom_select_mono)
+ finally show ?thesis .
+ qed
+
+ text \<open>Now for the final inequality chain:\<close>
+ have "T_mom_select k xs = T_rec2 + T_rec1 + T_ms + n + nl + ne + T_chop 5 xs + 4" using False
+ by (subst T_mom_select.simps, unfold Let_def tw [symmetric] defs [symmetric])
+ (simp_all add: nl_def ne_def T_rec1_def T_rec2_def T_partition3_eq
+ T_length_eq T_ms_def)
+ also have "nl \<le> n" by (simp add: nl_def ls_def)
+ also have "ne \<le> n" by (simp add: ne_def es_def)
+ also note \<open>T_ms \<le> 9 * n + 45\<close>
+ also have "T_chop 5 xs \<le> 5 * n + 1"
+ using T_chop_le[of 5 xs] by simp
+ also note \<open>T_rec1 \<le> T'_mom_select (nat \<lceil>0.2*n\<rceil>)\<close>
+ also note \<open>T_rec2 \<le> T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>)\<close>
+ finally have "T_mom_select k xs \<le>
+ T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>) + T'_mom_select (nat \<lceil>0.2*n\<rceil>) + 17 * n + 50"
+ by simp
+ also have "\<dots> = T'_mom_select n"
+ using False by (subst T'_mom_select.simps) auto
+ finally show ?thesis by simp
+ qed
+qed
+
+subsection \<open>Akra--Bazzi Light\<close>
+
+lemma akra_bazzi_light_aux1:
+ fixes a b :: real and n n0 :: nat
+ assumes ab: "a > 0" "a < 1" "n > n0"
+ assumes "n0 \<ge> (max 0 b + 1) / (1 - a)"
+ shows "nat \<lceil>a*n+b\<rceil> < n"
+proof -
+ have "a * real n + max 0 b \<ge> 0"
+ using ab by simp
+ hence "real (nat \<lceil>a*n+b\<rceil>) \<le> a * n + max 0 b + 1"
+ by linarith
+ also {
+ have "n0 \<ge> (max 0 b + 1) / (1 - a)"
+ by fact
+ also have "\<dots> < real n"
+ using assms by simp
+ finally have "a * real n + max 0 b + 1 < real n"
+ using ab by (simp add: field_simps)
+ }
+ finally show "nat \<lceil>a*n+b\<rceil> < n"
+ using \<open>n > n0\<close> by linarith
+qed
+
+lemma akra_bazzi_light_aux2:
+ fixes f :: "nat \<Rightarrow> real"
+ fixes n\<^sub>0 :: nat and a b c d :: real and C1 C2 C\<^sub>1 C\<^sub>2 :: real
+ assumes bounds: "a > 0" "c > 0" "a + c < 1" "C\<^sub>1 \<ge> 0"
+ assumes rec: "\<forall>n>n\<^sub>0. f n = f (nat \<lceil>a*n+b\<rceil>) + f (nat \<lceil>c*n+d\<rceil>) + C\<^sub>1 * n + C\<^sub>2"
+ assumes ineqs: "n\<^sub>0 > (max 0 b + max 0 d + 2) / (1 - a - c)"
+ "C\<^sub>3 \<ge> C\<^sub>1 / (1 - a - c)"
+ "C\<^sub>3 \<ge> (C\<^sub>1 * n\<^sub>0 + C\<^sub>2 + C\<^sub>4) / ((1 - a - c) * n\<^sub>0 - max 0 b - max 0 d - 2)"
+ "\<forall>n\<le>n\<^sub>0. f n \<le> C\<^sub>4"
+ shows "f n \<le> C\<^sub>3 * n + C\<^sub>4"
+proof (induction n rule: less_induct)
+ case (less n)
+ have "0 \<le> C\<^sub>1 / (1 - a - c)"
+ using bounds by auto
+ also have "\<dots> \<le> C\<^sub>3"
+ by fact
+ finally have "C\<^sub>3 \<ge> 0" .
+
+ show ?case
+ proof (cases "n > n\<^sub>0")
+ case False
+ hence "f n \<le> C\<^sub>4"
+ using ineqs(4) by auto
+ also have "\<dots> \<le> C\<^sub>3 * real n + C\<^sub>4"
+ using bounds \<open>C\<^sub>3 \<ge> 0\<close> by auto
+ finally show ?thesis .
+ next
+ case True
+ have nonneg: "a * n \<ge> 0" "c * n \<ge> 0"
+ using bounds by simp_all
+
+ have "(max 0 b + 1) / (1 - a) \<le> (max 0 b + max 0 d + 2) / (1 - a - c)"
+ using bounds by (intro frac_le) auto
+ hence "n\<^sub>0 \<ge> (max 0 b + 1) / (1 - a)"
+ using ineqs(1) by linarith
+ hence rec_less1: "nat \<lceil>a*n+b\<rceil> < n"
+ using bounds \<open>n > n\<^sub>0\<close> by (intro akra_bazzi_light_aux1[of _ n\<^sub>0]) auto
+
+ have "(max 0 d + 1) / (1 - c) \<le> (max 0 b + max 0 d + 2) / (1 - a - c)"
+ using bounds by (intro frac_le) auto
+ hence "n\<^sub>0 \<ge> (max 0 d + 1) / (1 - c)"
+ using ineqs(1) by linarith
+ hence rec_less2: "nat \<lceil>c*n+d\<rceil> < n"
+ using bounds \<open>n > n\<^sub>0\<close> by (intro akra_bazzi_light_aux1[of _ n\<^sub>0]) auto
+
+ have "f n = f (nat \<lceil>a*n+b\<rceil>) + f (nat \<lceil>c*n+d\<rceil>) + C\<^sub>1 * n + C\<^sub>2"
+ using \<open>n > n\<^sub>0\<close> by (subst rec) auto
+ also have "\<dots> \<le> (C\<^sub>3 * nat \<lceil>a*n+b\<rceil> + C\<^sub>4) + (C\<^sub>3 * nat \<lceil>c*n+d\<rceil> + C\<^sub>4) + C\<^sub>1 * n + C\<^sub>2"
+ using rec_less1 rec_less2 by (intro add_mono less.IH) auto
+ also have "\<dots> \<le> (C\<^sub>3 * (a*n+max 0 b+1) + C\<^sub>4) + (C\<^sub>3 * (c*n+max 0 d+1) + C\<^sub>4) + C\<^sub>1 * n + C\<^sub>2"
+ using bounds \<open>C\<^sub>3 \<ge> 0\<close> nonneg by (intro add_mono mult_left_mono order.refl; linarith)
+ also have "\<dots> = C\<^sub>3 * n + ((C\<^sub>3 * (max 0 b + max 0 d + 2) + 2 * C\<^sub>4 + C\<^sub>2) -
+ (C\<^sub>3 * (1 - a - c) - C\<^sub>1) * n)"
+ by (simp add: algebra_simps)
+ also have "\<dots> \<le> C\<^sub>3 * n + ((C\<^sub>3 * (max 0 b + max 0 d + 2) + 2 * C\<^sub>4 + C\<^sub>2) -
+ (C\<^sub>3 * (1 - a - c) - C\<^sub>1) * n\<^sub>0)"
+ using \<open>n > n\<^sub>0\<close> ineqs(2) bounds
+ by (intro add_mono diff_mono order.refl mult_left_mono) (auto simp: field_simps)
+ also have "(C\<^sub>3 * (max 0 b + max 0 d + 2) + 2 * C\<^sub>4 + C\<^sub>2) - (C\<^sub>3 * (1 - a - c) - C\<^sub>1) * n\<^sub>0 \<le> C\<^sub>4"
+ using ineqs bounds by (simp add: field_simps)
+ finally show "f n \<le> C\<^sub>3 * real n + C\<^sub>4"
+ by (simp add: mult_right_mono)
+ qed
+qed
+
+lemma akra_bazzi_light:
+ fixes f :: "nat \<Rightarrow> real"
+ fixes n\<^sub>0 :: nat and a b c d C\<^sub>1 C\<^sub>2 :: real
+ assumes bounds: "a > 0" "c > 0" "a + c < 1" "C\<^sub>1 \<ge> 0"
+ assumes rec: "\<forall>n>n\<^sub>0. f n = f (nat \<lceil>a*n+b\<rceil>) + f (nat \<lceil>c*n+d\<rceil>) + C\<^sub>1 * n + C\<^sub>2"
+ shows "\<exists>C\<^sub>3 C\<^sub>4. \<forall>n. f n \<le> C\<^sub>3 * real n + C\<^sub>4"
+proof -
+ define n\<^sub>0' where "n\<^sub>0' = max n\<^sub>0 (nat \<lceil>(max 0 b + max 0 d + 2) / (1 - a - c) + 1\<rceil>)"
+ define C\<^sub>4 where "C\<^sub>4 = Max (f ` {..n\<^sub>0'})"
+ define C\<^sub>3 where "C\<^sub>3 = max (C\<^sub>1 / (1 - a - c))
+ ((C\<^sub>1 * n\<^sub>0' + C\<^sub>2 + C\<^sub>4) / ((1 - a - c) * n\<^sub>0' - max 0 b - max 0 d - 2))"
+
+ have "f n \<le> C\<^sub>3 * n + C\<^sub>4" for n
+ proof (rule akra_bazzi_light_aux2[OF bounds _])
+ show "\<forall>n>n\<^sub>0'. f n = f (nat \<lceil>a*n+b\<rceil>) + f (nat \<lceil>c*n+d\<rceil>) + C\<^sub>1 * n + C\<^sub>2"
+ using rec by (auto simp: n\<^sub>0'_def)
+ next
+ show "C\<^sub>3 \<ge> C\<^sub>1 / (1 - a - c)"
+ and "C\<^sub>3 \<ge> (C\<^sub>1 * n\<^sub>0' + C\<^sub>2 + C\<^sub>4) / ((1 - a - c) * n\<^sub>0' - max 0 b - max 0 d - 2)"
+ by (simp_all add: C\<^sub>3_def)
+ next
+ have "(max 0 b + max 0 d + 2) / (1 - a - c) < nat \<lceil>(max 0 b + max 0 d + 2) / (1 - a - c) + 1\<rceil>"
+ by linarith
+ also have "\<dots> \<le> n\<^sub>0'"
+ by (simp add: n\<^sub>0'_def)
+ finally show "(max 0 b + max 0 d + 2) / (1 - a - c) < real n\<^sub>0'" .
+ next
+ show "\<forall>n\<le>n\<^sub>0'. f n \<le> C\<^sub>4"
+ by (auto simp: C\<^sub>4_def)
+ qed
+ thus ?thesis by blast
+qed
+
+lemma akra_bazzi_light_nat:
+ fixes f :: "nat \<Rightarrow> nat"
+ fixes n\<^sub>0 :: nat and a b c d :: real and C\<^sub>1 C\<^sub>2 :: nat
+ assumes bounds: "a > 0" "c > 0" "a + c < 1" "C\<^sub>1 \<ge> 0"
+ assumes rec: "\<forall>n>n\<^sub>0. f n = f (nat \<lceil>a*n+b\<rceil>) + f (nat \<lceil>c*n+d\<rceil>) + C\<^sub>1 * n + C\<^sub>2"
+ shows "\<exists>C\<^sub>3 C\<^sub>4. \<forall>n. f n \<le> C\<^sub>3 * n + C\<^sub>4"
+proof -
+ have "\<exists>C\<^sub>3 C\<^sub>4. \<forall>n. real (f n) \<le> C\<^sub>3 * real n + C\<^sub>4"
+ using assms by (intro akra_bazzi_light[of a c C\<^sub>1 n\<^sub>0 f b d C\<^sub>2]) auto
+ then obtain C\<^sub>3 C\<^sub>4 where le: "\<forall>n. real (f n) \<le> C\<^sub>3 * real n + C\<^sub>4"
+ by blast
+ have "f n \<le> nat \<lceil>C\<^sub>3\<rceil> * n + nat \<lceil>C\<^sub>4\<rceil>" for n
+ proof -
+ have "real (f n) \<le> C\<^sub>3 * real n + C\<^sub>4"
+ using le by blast
+ also have "\<dots> \<le> real (nat \<lceil>C\<^sub>3\<rceil>) * real n + real (nat \<lceil>C\<^sub>4\<rceil>)"
+ by (intro add_mono mult_right_mono; linarith)
+ also have "\<dots> = real (nat \<lceil>C\<^sub>3\<rceil> * n + nat \<lceil>C\<^sub>4\<rceil>)"
+ by simp
+ finally show ?thesis by linarith
+ qed
+ thus ?thesis by blast
+qed
+
+lemma T'_mom_select_le': "\<exists>C\<^sub>1 C\<^sub>2. \<forall>n. T'_mom_select n \<le> C\<^sub>1 * n + C\<^sub>2"
+proof (rule akra_bazzi_light_nat)
+ show "\<forall>n>20. T'_mom_select n = T'_mom_select (nat \<lceil>0.2 * n + 0\<rceil>) +
+ T'_mom_select (nat \<lceil>0.7 * n + 3\<rceil>) + 17 * n + 50"
+ using T'_mom_select.simps by auto
+qed auto
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Time_Funs.thy Fri Jan 08 19:53:44 2021 +0100
@@ -0,0 +1,65 @@
+(*
+ File: Data_Structures/Time_Functions.thy
+ Author: Manuel Eberl, TU München
+*)
+section \<open>Time functions for various standard library operations\<close>
+theory Time_Funs
+ imports Main
+begin
+
+fun T_length :: "'a list \<Rightarrow> nat" where
+ "T_length [] = 1"
+| "T_length (x # xs) = T_length xs + 1"
+
+lemma T_length_eq: "T_length xs = length xs + 1"
+ by (induction xs) auto
+
+lemmas [simp del] = T_length.simps
+
+
+fun T_map :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where
+ "T_map T_f [] = 1"
+| "T_map T_f (x # xs) = T_f x + T_map T_f xs + 1"
+
+lemma T_map_eq: "T_map T_f xs = (\<Sum>x\<leftarrow>xs. T_f x) + length xs + 1"
+ by (induction xs) auto
+
+lemmas [simp del] = T_map.simps
+
+
+fun T_filter :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where
+ "T_filter T_p [] = 1"
+| "T_filter T_p (x # xs) = T_p x + T_filter T_p xs + 1"
+
+lemma T_filter_eq: "T_filter T_p xs = (\<Sum>x\<leftarrow>xs. T_p x) + length xs + 1"
+ by (induction xs) auto
+
+lemmas [simp del] = T_filter.simps
+
+
+fun T_nth :: "'a list \<Rightarrow> nat \<Rightarrow> nat" where
+ "T_nth [] n = 1"
+| "T_nth (x # xs) n = (case n of 0 \<Rightarrow> 1 | Suc n' \<Rightarrow> T_nth xs n' + 1)"
+
+lemma T_nth_eq: "T_nth xs n = min n (length xs) + 1"
+ by (induction xs n rule: T_nth.induct) (auto split: nat.splits)
+
+lemmas [simp del] = T_nth.simps
+
+
+fun T_take :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
+ "T_take n [] = 1"
+| "T_take n (x # xs) = (case n of 0 \<Rightarrow> 1 | Suc n' \<Rightarrow> T_take n' xs + 1)"
+
+lemma T_take_eq: "T_take n xs = min n (length xs) + 1"
+ by (induction xs arbitrary: n) (auto split: nat.splits)
+
+fun T_drop :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
+ "T_drop n [] = 1"
+| "T_drop n (x # xs) = (case n of 0 \<Rightarrow> 1 | Suc n' \<Rightarrow> T_drop n' xs + 1)"
+
+lemma T_drop_eq: "T_drop n xs = min n (length xs) + 1"
+ by (induction xs arbitrary: n) (auto split: nat.splits)
+
+
+end
--- a/src/HOL/ROOT Fri Jan 08 20:40:56 2021 +0100
+++ b/src/HOL/ROOT Fri Jan 08 19:53:44 2021 +0100
@@ -288,6 +288,7 @@
Heaps
Leftist_Heap
Binomial_Heap
+ Selection
document_files "root.tex" "root.bib"
session "HOL-Import" in Import = HOL +