--- a/src/HOL/Data_Structures/Time_Funs.thy Tue Aug 20 17:28:51 2024 +0200
+++ b/src/HOL/Data_Structures/Time_Funs.thy Wed Aug 21 20:40:59 2024 +0200
@@ -12,16 +12,25 @@
lemma T_append: "T_append xs ys = length xs + 1"
by(induction xs) auto
-text \<open>Automatic definition of \<open>T_length\<close> is cumbersome because of the type class for \<open>size\<close>.\<close>
+class T_size =
+ fixes T_size :: "'a \<Rightarrow> nat"
+
+instantiation list :: (_) T_size
+begin
-fun T_length :: "'a list \<Rightarrow> nat" where
- "T_length [] = 1"
-| "T_length (x # xs) = T_length xs + 1"
+time_fun length
+
+instance ..
+
+end
+
+abbreviation T_length :: "'a list \<Rightarrow> nat" where
+"T_length \<equiv> T_size"
lemma T_length_eq: "T_length xs = length xs + 1"
by (induction xs) auto
-lemmas [simp del] = T_length.simps
+lemmas [simp del] = T_size_list.simps
time_fun map