diff -r 47272fac86d8 -r b287510a4202 src/HOL/Data_Structures/Tree23_of_List.thy
--- a/src/HOL/Data_Structures/Tree23_of_List.thy	Sun Jan 14 20:55:58 2024 +0100
+++ b/src/HOL/Data_Structures/Tree23_of_List.thy	Mon Jan 15 22:50:13 2024 +0100
@@ -3,7 +3,9 @@
 section \<open>2-3 Tree from List\<close>
 
 theory Tree23_of_List
-imports Tree23
+imports
+  Tree23
+  Define_Time_Function
 begin
 
 text \<open>Linear-time bottom up conversion of a list of items into a complete 2-3 tree
@@ -116,21 +118,10 @@
 
 subsection "Linear running time"
 
-fun T_join_adj :: "'a tree23s \<Rightarrow> nat" where
-"T_join_adj (TTs t1 a (T t2)) = 1" |
-"T_join_adj (TTs t1 a (TTs t2 b (T t3))) = 1" |
-"T_join_adj (TTs t1 a (TTs t2 b ts)) = T_join_adj ts + 1"
-
-fun T_join_all :: "'a tree23s \<Rightarrow> nat" where
-"T_join_all (T t) = 1" |
-"T_join_all ts = T_join_adj ts + T_join_all (join_adj ts) + 1"
-
-fun T_leaves :: "'a list \<Rightarrow> nat" where
-"T_leaves [] = 1" |
-"T_leaves (a # as) = T_leaves as + 1"
-
-definition T_tree23_of_list :: "'a list \<Rightarrow> nat" where
-"T_tree23_of_list as = T_leaves as + T_join_all(leaves as)"
+define_time_fun join_adj
+define_time_fun join_all
+define_time_fun leaves
+define_time_fun tree23_of_list
 
 lemma T_join_adj: "not_T ts \<Longrightarrow> T_join_adj ts \<le> len ts div 2"
 by(induction ts rule: T_join_adj.induct) auto
@@ -163,6 +154,6 @@
 by(induction as) auto
 
 lemma T_tree23_of_list: "T_tree23_of_list as \<le> 3*(length as) + 3"
-using T_join_all[of "leaves as"] by(simp add: T_tree23_of_list_def T_leaves len_leaves)
+using T_join_all[of "leaves as"] by(simp add: T_leaves len_leaves)
 
 end