--- a/src/HOL/Data_Structures/Selection.thy Mon Apr 15 22:24:31 2024 +0100
+++ b/src/HOL/Data_Structures/Selection.thy Tue Apr 16 13:29:27 2024 +0200
@@ -310,6 +310,12 @@
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 length_partition3:
+ assumes "partition3 x xs = (ls, es, gs)"
+ shows "length xs = length ls + length es + length gs"
+ using assms by (induction xs arbitrary: ls es gs)
+ (auto simp: partition3_code split: if_splits prod.splits)
+
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"
@@ -643,19 +649,39 @@
definition T_slow_median :: "'a :: linorder list \<Rightarrow> nat" where
"T_slow_median xs = T_length xs + T_slow_select ((length xs - 1) div 2) xs"
-lemma T_slow_select_le: "T_slow_select k xs \<le> length xs ^ 2 + 3 * length xs + 2"
+lemma T_slow_select_le:
+ assumes "k < length xs"
+ shows "T_slow_select k xs \<le> length xs ^ 2 + 3 * length xs + 1"
proof -
- have "T_slow_select k xs \<le> (length xs + 1)\<^sup>2 + (length (insort xs) + 1)"
- unfolding T_slow_select_def
- by (intro add_mono T_insort_length) (auto simp: T_nth_eq)
- also have "\<dots> = length xs ^ 2 + 3 * length xs + 2"
- by (simp add: insort_correct algebra_simps power2_eq_square)
- finally show ?thesis .
+ have "T_slow_select k xs = T_insort xs + T_nth (Sorting.insort xs) k"
+ unfolding T_slow_select_def ..
+ also have "T_insort xs \<le> (length xs + 1) ^ 2"
+ by (rule T_insort_length)
+ also have "T_nth (Sorting.insort xs) k = k + 1"
+ using assms by (subst T_nth_eq) (auto simp: length_insort)
+ also have "k + 1 \<le> length xs"
+ using assms by linarith
+ also have "(length xs + 1) ^ 2 + length xs = length xs ^ 2 + 3 * length xs + 1"
+ by (simp add: algebra_simps power2_eq_square)
+ finally show ?thesis by - simp_all
qed
-lemma T_slow_median_le: "T_slow_median xs \<le> length xs ^ 2 + 4 * length xs + 3"
- unfolding T_slow_median_def using T_slow_select_le[of "(length xs - 1) div 2" xs]
- by (simp add: algebra_simps T_length_eq)
+lemma T_slow_median_le:
+ assumes "xs \<noteq> []"
+ shows "T_slow_median xs \<le> length xs ^ 2 + 4 * length xs + 2"
+proof -
+ have "T_slow_median xs = length xs + T_slow_select ((length xs - 1) div 2) xs + 1"
+ by (simp add: T_slow_median_def T_length_eq)
+ also from assms have "length xs > 0"
+ by simp
+ hence "(length xs - 1) div 2 < length xs"
+ by linarith
+ hence "T_slow_select ((length xs - 1) div 2) xs \<le> length xs ^ 2 + 3 * length xs + 1"
+ by (intro T_slow_select_le) auto
+ also have "length xs + \<dots> + 1 = length xs ^ 2 + 4 * length xs + 2"
+ by (simp add: algebra_simps)
+ finally show ?thesis by - simp_all
+qed
time_fun chop
@@ -717,16 +743,16 @@
function T'_mom_select :: "nat \<Rightarrow> nat" where
"T'_mom_select n =
(if n \<le> 20 then
- 483
+ 482
else
- T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n+3\<rceil>) + 19 * n + 55)"
+ T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n+3\<rceil>) + 19 * n + 54)"
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> 483"
+lemma T'_mom_select_ge: "T'_mom_select n \<ge> 482"
by (induction n rule: T'_mom_select.induct; subst T'_mom_select.simps) auto
lemma T'_mom_select_mono:
@@ -736,7 +762,7 @@
show ?case
proof (cases "m \<le> 20")
case True
- hence "T'_mom_select m = 483"
+ hence "T'_mom_select m = 482"
by (subst T'_mom_select.simps) auto
also have "\<dots> \<le> T'_mom_select n"
by (rule T'_mom_select_ge)
@@ -744,9 +770,9 @@
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>) + 19 * m + 55"
+ T'_mom_select (nat \<lceil>0.2*m\<rceil>) + T'_mom_select (nat \<lceil>0.7*m + 3\<rceil>) + 19 * m + 54"
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>) + 19 * n + 55"
+ also have "\<dots> \<le> T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>) + 19 * n + 54"
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
@@ -754,7 +780,10 @@
qed
qed
-lemma T_mom_select_le_aux: "T_mom_select k xs \<le> T'_mom_select (length xs)"
+lemma T_mom_select_le_aux:
+ assumes "k < length xs"
+ shows "T_mom_select k xs \<le> T'_mom_select (length xs)"
+ using assms
proof (induction k xs rule: T_mom_select.induct)
case (1 k xs)
define n where [simp]: "n = length xs"
@@ -771,11 +800,12 @@
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 + 4 * length xs + 3"
- using T_slow_select_le[of k xs] by (subst T_mom_select.simps) (auto simp: T_length_eq)
- also have "\<dots> \<le> 20\<^sup>2 + 4 * 20 + 3"
+ hence "T_mom_select k xs \<le> (length xs)\<^sup>2 + 4 * length xs + 2"
+ using T_slow_select_le[of k xs] \<open>k < length xs\<close>
+ by (subst T_mom_select.simps) (auto simp: T_length_eq)
+ also have "\<dots> \<le> 20\<^sup>2 + 4 * 20 + 2"
using True by (intro add_mono power_mono) auto
- also have "\<dots> = 483"
+ also have "\<dots> = 482"
by simp
also have "\<dots> = T'_mom_select (length xs)"
using True by (simp add: T'_mom_select.simps)
@@ -794,34 +824,36 @@
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> 10 * n + 49"
+ have "T_ms \<le> 10 * n + 48"
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. 48)"
+ also have "(\<Sum>ys\<leftarrow>chop 5 xs. T_slow_median ys) \<le> (\<Sum>ys\<leftarrow>chop 5 xs. 47)"
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 + 4 * length ys + 3"
+ hence "length ys \<le> 5" "ys \<noteq> []"
+ using length_chop_part_le[of ys 5 xs] by auto
+ from \<open>ys \<noteq> []\<close> have "T_slow_median ys \<le> (length ys) ^ 2 + 4 * length ys + 2"
by (rule T_slow_median_le)
- also have "\<dots> \<le> 5 ^ 2 + 4 * 5 + 3"
+ also have "\<dots> \<le> 5 ^ 2 + 4 * 5 + 2"
using \<open>length ys \<le> 5\<close> by (intro add_mono power_mono) auto
- finally show "T_slow_median ys \<le> 48" by simp
+ finally show "T_slow_median ys \<le> 47" by simp
qed
- also have "(\<Sum>ys\<leftarrow>chop 5 xs. 48) + length (chop 5 xs) + 1 =
- 49 * nat \<lceil>real n / 5\<rceil> + 1"
+ also have "(\<Sum>ys\<leftarrow>chop 5 xs. 47) + length (chop 5 xs) + 1 =
+ 48 * nat \<lceil>real n / 5\<rceil> + 1"
by (simp add: map_replicate_const length_chop)
- also have "\<dots> \<le> 10 * n + 49"
+ also have "\<dots> \<le> 10 * n + 48"
by linarith
- finally show "T_ms \<le> 10 * n + 49" by simp
+ finally show "T_ms \<le> 10 * n + 48" 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
+ from False have "((length xs + 4) div 5 - Suc 0) div 2 < nat \<lceil>real (length xs) / 5\<rceil>"
+ by linarith
+ hence "T_rec1 \<le> T'_mom_select (length (map slow_median (chop 5 xs)))"
+ using False unfolding T_rec1_def by (intro IH(3)) (auto simp: length_chop)
hence "T_rec1 \<le> T'_mom_select (nat \<lceil>0.2 * n\<rceil>)"
by (simp add: length_chop)
@@ -855,7 +887,17 @@
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>)
+ unfolding nl_def ne_def
+ proof (rule IH(2))
+ show "\<not> length xs \<le> 20"
+ using False by auto
+ show "\<not> k < length ls" "\<not>k < length ls + length es"
+ using \<open>k \<ge> nl + ne\<close> by (auto simp: nl_def ne_def)
+ have "length xs = nl + ne + length gs"
+ unfolding defs by (rule length_partition3) (simp_all add: partition3_def)
+ thus "k - length ls - length es < length gs"
+ using \<open>k \<ge> nl + ne\<close> \<open>k < length xs\<close> by (auto simp: nl_def ne_def)
+ qed
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)
@@ -871,13 +913,13 @@
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> 10 * n + 49\<close>
+ also note \<open>T_ms \<le> 10 * n + 48\<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>) + 19 * n + 55"
+ T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>) + T'_mom_select (nat \<lceil>0.2*n\<rceil>) + 19 * n + 54"
by simp
also have "\<dots> = T'_mom_select n"
using False by (subst T'_mom_select.simps) auto
@@ -1034,7 +1076,7 @@
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>) + 19 * n + 55"
+ T'_mom_select (nat \<lceil>0.7 * n + 3\<rceil>) + 19 * n + 54"
using T'_mom_select.simps by auto
qed auto
--- a/src/HOL/Data_Structures/Time_Funs.thy Mon Apr 15 22:24:31 2024 +0100
+++ b/src/HOL/Data_Structures/Time_Funs.thy Tue Apr 16 13:29:27 2024 +0200
@@ -43,12 +43,9 @@
lemmas [simp del] = T_filter.simps
+time_fun nth
-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"
+lemma T_nth_eq: "n < length xs \<Longrightarrow> T_nth xs n = n + 1"
by (induction xs n rule: T_nth.induct) (auto split: nat.splits)
lemmas [simp del] = T_nth.simps