# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1713266967 -7200
# Node ID 247751d2510292c2f1152362c468488bf91a5fc0
# Parent  693d4e6cc5b8d09852474a1251418360a7b51ccb
canonical time function for List.nth

diff -r 693d4e6cc5b8 -r 247751d25102 src/HOL/Data_Structures/Selection.thy
--- 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
 
diff -r 693d4e6cc5b8 -r 247751d25102 src/HOL/Data_Structures/Time_Funs.thy
--- 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