diff -r 9786f64d8285 -r d6daa049c1db src/HOL/Data_Structures/Selection.thy
--- a/src/HOL/Data_Structures/Selection.thy	Thu Oct 31 15:46:53 2024 +0100
+++ b/src/HOL/Data_Structures/Selection.thy	Thu Oct 31 18:43:32 2024 +0100
@@ -525,15 +525,17 @@
 \<close>
 function mom_select where
   "mom_select k xs = (
-     if length xs \<le> 20 then
+     let n = length xs
+     in if n \<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
+       let M = mom_select (((n + 4) div 5 - 1) div 2) (map slow_median (chop 5 xs));
+           (ls, es, gs) = partition3 M xs;
+           nl = length ls
        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
+         if k < nl then mom_select k ls 
+         else let ne = length es in if k < nl + ne then M
+         else mom_select (k - nl - ne) gs
       )"
   by auto
 
@@ -564,7 +566,8 @@
     have length_eq: "length xs = nl + ne + length gs"
       unfolding nl_def ne_def ls_def es_def gs_def
       using [[simp_depth_limit = 1]] by (induction xs) auto
-    note IH = "1.IH"(2,3)[OF False x_def tw refl refl]
+    note IH = "1.IH"(2)[OF refl False x_def tw refl refl refl]
+              "1.IH"(3)[OF refl False x_def tw refl refl 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
@@ -572,6 +575,7 @@
     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)
+      try0
     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" .
@@ -697,17 +701,13 @@
 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)
 
+time_fun mom_select
 
-text \<open>
-  The option \<open>domintros\<close> 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 = T_length xs + (
-     if length xs \<le> 20 then
-       T_slow_select k xs
-     else
+lemmas [simp del] = T_mom_select.simps
+
+lemma T_mom_select_simps:
+  "length xs \<le> 20 \<Longrightarrow> T_mom_select k xs = T_slow_select k xs + T_length xs + 1"
+  "length xs > 20 \<Longrightarrow> T_mom_select k xs = (
        let xss = chop 5 xs;
            ms = map slow_median xss;
            idx = (((length xs + 4) div 5 - 1) div 2);
@@ -719,27 +719,14 @@
          (if k < nl then T_mom_select k ls 
           else T_length es + (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 + 1
+         T_partition3 x xs + T_length ls + T_length xs + 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
-
+   by (subst T_mom_select.simps; simp add: Let_def case_prod_unfold)+
 
 function T'_mom_select :: "nat \<Rightarrow> nat" where
   "T'_mom_select n =
      (if n \<le> 20 then
-        482
+        483
       else
         T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n+3\<rceil>) + 19 * n + 54)"
   by force+
@@ -748,7 +735,7 @@
 lemmas [simp del] = T'_mom_select.simps
 
 
-lemma T'_mom_select_ge: "T'_mom_select n \<ge> 482"
+lemma T'_mom_select_ge: "T'_mom_select n \<ge> 483"
   by (induction n rule: T'_mom_select.induct; subst T'_mom_select.simps) auto
 
 lemma T'_mom_select_mono:
@@ -758,7 +745,7 @@
   show ?case
   proof (cases "m \<le> 20")
     case True
-    hence "T'_mom_select m = 482"
+    hence "T'_mom_select m = 483"
       by (subst T'_mom_select.simps) auto
     also have "\<dots> \<le> T'_mom_select n"
       by (rule T'_mom_select_ge)
@@ -784,24 +771,26 @@
   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))"
+    "x = mom_select (((n + 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]
+  note IH = "1.IH"(1)[OF n_def]
+            "1.IH"(2)[OF n_def _ x_def tw refl refl nl_def]
+            "1.IH"(3)[OF n_def _ x_def tw refl refl nl_def _ ne_def]
 
   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 + 2"
+    hence "T_mom_select k xs \<le> (length xs)\<^sup>2 + 4 * length xs + 3"
       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"
+      by (subst T_mom_select_simps(1)) (auto simp: T_length_eq)
+    also have "\<dots> \<le> 20\<^sup>2 + 4 * 20 + 3"
       using True by (intro add_mono power_mono) auto
-    also have "\<dots> = 482"
+    also have "\<dots> = 483"
       by simp
     also have "\<dots> = T'_mom_select (length xs)"
       using True by (simp add: T'_mom_select.simps)
@@ -845,11 +834,11 @@
 
     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))"
+      "T_rec1 = T_mom_select (((n + 4) div 5 - 1) div 2) (map slow_median (chop 5 xs))"
     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)
+      using False unfolding T_rec1_def by (intro IH(1)) (auto simp: length_chop)
     hence "T_rec1 \<le> T'_mom_select (nat \<lceil>0.2 * n\<rceil>)"
       by (simp add: length_chop)
 
@@ -865,7 +854,7 @@
       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>)
+        by (rule IH(2)) (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)
@@ -883,15 +872,14 @@
       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 
-      proof (rule IH(2))
-        show "\<not> length xs \<le> 20"
+      proof (rule IH(3))
+        show "\<not>n \<le> 20"
           using False by auto
-        show "\<not> k < length ls" "\<not>k < length ls + length es"
+        show "\<not> k < nl" "\<not>k < nl + ne"
           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"
+        thus "k - nl - ne < 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>"
@@ -903,10 +891,19 @@
     qed
 
     text \<open>Now for the final inequality chain:\<close>
-    have "T_mom_select k xs \<le> T_rec2 + T_rec1 + T_ms + 2 * n + nl + ne + T_chop 5 xs + 5" 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)
+    have "T_mom_select k xs =
+            (if k < nl then T_mom_select k ls
+             else T_length es +
+               (if k < nl + ne then 0 else T_mom_select (k - nl - ne) gs)) +
+             T_mom_select (((n + 4) div 5 - 1) div 2) (map slow_median (chop 5 xs)) +
+             T_chop 5 xs + T_map T_slow_median (chop 5 xs) + T_partition3 x xs +
+             T_length ls + T_length xs + 1" using False
+      by (subst T_mom_select_simps;
+          unfold Let_def n_def [symmetric] x_def [symmetric] nl_def [symmetric] 
+          ne_def [symmetric] prod.case tw [symmetric]) simp_all
+    also have "\<dots> \<le> T_rec2 + T_rec1 + T_ms + 2 * n + nl + ne + T_chop 5 xs + 5" using False
+      by (auto simp add: T_rec1_def T_rec2_def T_partition3_eq
+                         T_length_eq T_ms_def nl_def ne_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 + 48\<close>