summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Manuel Eberl <eberlm@in.tum.de> |

Fri, 08 Jan 2021 19:53:44 +0100 | |

changeset 73108 | 981a383610df |

parent 73107 | f062d19c4b44 |

child 73109 | 783406dd051e |

HOL-Data_Structures: added Selection and time functions for list functions

--- 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