# HG changeset patch
# User nipkow
# Date 1711288263 -3600
# Node ID 773b99044329042e0b3000e5132c7da3784d2ebd
# Parent  1fd5f96e1da338cf04e8c622d91dbafa59e4763c# Parent  4aeb25ba90f3871ce70f5b823ca30f89a619999a
merged

diff -r 1fd5f96e1da3 -r 773b99044329 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Sun Mar 24 14:04:30 2024 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Sun Mar 24 14:51:03 2024 +0100
@@ -472,19 +472,19 @@
 
 subsubsection \<open>Timing Functions\<close>
 
-define_time_fun link
+time_fun link
 
 lemma T_link[simp]: "T_link t\<^sub>1 t\<^sub>2 = 0"
 by(cases t\<^sub>1; cases t\<^sub>2, auto)
 
-define_time_fun rank
+time_fun rank
 
 lemma T_rank[simp]: "T_rank t = 0"
 by(cases t, auto)
 
-define_time_fun ins_tree
+time_fun ins_tree
 
-define_time_fun insert
+time_fun insert
 
 lemma T_ins_tree_simple_bound: "T_ins_tree t ts \<le> length ts + 1"
 by (induction t ts rule: T_ins_tree.induct) auto
@@ -504,7 +504,7 @@
 
 subsubsection \<open>\<open>T_merge\<close>\<close>
 
-define_time_fun merge
+time_fun merge
 
 (* Warning: \<open>T_merge.induct\<close> is less convenient than the equivalent \<open>merge.induct\<close>,
 apparently because of the \<open>let\<close> clauses introduced by pattern_aliases; should be investigated.
@@ -547,14 +547,14 @@
 
 subsubsection \<open>\<open>T_get_min\<close>\<close>
 
-define_time_fun root
+time_fun root
 
 lemma T_root[simp]: "T_root t = 0"
 by(cases t)(simp_all)
 
-define_time_fun min
+time_fun min
 
-define_time_fun get_min
+time_fun get_min
 
 lemma T_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min ts = length ts"
 by (induction ts rule: T_get_min.induct) auto
@@ -571,7 +571,7 @@
 
 subsubsection \<open>\<open>T_del_min\<close>\<close>
 
-define_time_fun get_min_rest
+time_fun get_min_rest
 (*fun T_get_min_rest :: "'a::linorder trees \<Rightarrow> nat" where
   "T_get_min_rest [t] = 1"
 | "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts"*)
@@ -595,7 +595,7 @@
 
 definition "T_rev xs = length xs + 1"
 
-define_time_fun del_min
+time_fun del_min
 
 lemma T_del_min_bound:
   fixes ts
diff -r 1fd5f96e1da3 -r 773b99044329 src/HOL/Data_Structures/Define_Time_0.ML
--- a/src/HOL/Data_Structures/Define_Time_0.ML	Sun Mar 24 14:04:30 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_0.ML	Sun Mar 24 14:51:03 2024 +0100
@@ -37,7 +37,7 @@
 end
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>define_time_0\<close> "ML setup for global theory"
+  Outer_Syntax.command \<^command_keyword>\<open>time_fun_0\<close> "ML setup for global theory"
     (Parse.prop >> (Toplevel.theory o save));
 
 end
\ No newline at end of file
diff -r 1fd5f96e1da3 -r 773b99044329 src/HOL/Data_Structures/Define_Time_Function.ML
--- a/src/HOL/Data_Structures/Define_Time_Function.ML	Sun Mar 24 14:04:30 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML	Sun Mar 24 14:51:03 2024 +0100
@@ -16,11 +16,10 @@
 val print_timing':  Proof.context -> pfunc -> pfunc -> unit
 val print_timing:  Proof.context -> Function.info -> Function.info -> unit
 
-val reg_and_proove_time_func: theory -> term list -> term list -> term option converter
-      -> (bool -> local_theory -> term list -> term option -> term)
+val reg_and_proove_time_func: theory -> term list -> term list
       -> bool -> Function.info * theory
-val reg_time_func: theory -> term list -> term list -> term option converter
-      -> (bool -> local_theory -> term list -> term option -> term) -> bool -> theory
+val reg_time_func: theory -> term list -> term list
+      -> bool -> theory
 
 val time_dom_tac: Proof.context -> thm -> thm list -> int -> tactic
 
@@ -316,10 +315,10 @@
   if not (casecIsCase T) then error "Internal error: invalid case type" else
     let val (nconst, args') = casecArgs f args in
       plus
+        (f (List.last args))
         (if nconst then
           SOME (build_func (Const (t,casecTyp T), args'))
          else NONE)
-        (f (List.last args))
     end
   | casec _ _ _ _ _ = error "Internal error: invalid case term"
 
@@ -332,8 +331,8 @@
     val tt = f tt
     val ft = f ft
   in
-    plus (case (tt,ft) of (NONE, NONE) => NONE | _ =>
-       (SOME ((Const (If_name, @{typ "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"})) $ rcond $ (opt_term tt) $ (opt_term ft)))) (f cond)
+    plus (f cond) (case (tt,ft) of (NONE, NONE) => NONE | _ =>
+       (SOME ((Const (If_name, @{typ "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"})) $ rcond $ (opt_term tt) $ (opt_term ft))))
   end
 
 fun letc_change_typ (Type ("fun", [T1, Type ("fun", [T2, _])])) = (Type ("fun", [T1, Type ("fun", [change_typ T2, HOLogic.natT])]))
@@ -363,16 +362,16 @@
 fun top_converter is_rec _ _ = opt_term o (fn exp => plus exp (if is_rec then SOME one else NONE))
 
 (* Use converter to convert right side of a term *)
-fun to_time ctxt origin converter top_converter term =
-  top_converter ctxt origin (walk ctxt origin converter term)
+fun to_time ctxt origin is_rec term =
+  top_converter is_rec ctxt origin (walk ctxt origin converter term)
 
 (* Converts a term to its running time version *)
-fun convert_term ctxt (origin: term list) conv topConv (pT $ (Const (eqN, _) $ l $ r)) =
+fun convert_term ctxt (origin: term list) is_rec (pT $ (Const (eqN, _) $ l $ r)) =
       pT
       $ (Const (eqN, @{typ "nat \<Rightarrow> nat \<Rightarrow> bool"})
         $ (build_func ((walk_func l []) |>> (fun_to_time ctxt origin) |>> Option.valOf ||> conv_args ctxt origin))
-        $ (to_time ctxt origin conv topConv r))
-  | convert_term _ _ _ _ _ = error "Internal error: invalid term to convert"
+        $ (to_time ctxt origin is_rec r))
+  | convert_term _ _ _ _ = error "Internal error: invalid term to convert"
 
 (* 4. Tactic to prove "f_dom n" *)
 fun time_dom_tac ctxt induct_rule domintros =
@@ -389,10 +388,10 @@
    handle Empty => error "Function or terms of function not found"
 
 (* Register timing function of a given function *)
-fun reg_and_proove_time_func (theory: theory) (term: term list) (terms: term list) conv topConv print =
-  reg_time_func theory term terms conv topConv false
+fun reg_and_proove_time_func (theory: theory) (term: term list) (terms: term list) print =
+  reg_time_func theory term terms false
   |> proove_termination term terms print
-and reg_time_func (theory: theory) (term: term list) (terms: term list) conv topConv print =
+and reg_time_func (theory: theory) (term: term list) (terms: term list) print =
   let
     val lthy = Named_Target.theory_init theory
     val _ =
@@ -403,7 +402,7 @@
 
     (* 1. Fix all terms *)
     (* Exchange Var in types and terms to Free and check constraints *)
-    val terms = map 
+    val terms = map
       (map_aterms fixTerms
         #> map_types (map_atyps fixTypes)
         #> fixPartTerms lthy term)
@@ -417,7 +416,7 @@
       - On left side change name of function to timing function
       - Convert right side of equation with conversion schema
     *)
-    val timing_terms = map (convert_term lthy term conv (topConv is_rec)) terms
+    val timing_terms = map (convert_term lthy term is_rec) terms
 
     (* 4. Register function and prove termination *)
     val names = map Term.term_name term
@@ -522,38 +521,60 @@
     (time_info, Local_Theory.exit_global lthy')
   end
 
+fun fix_definition (Const ("Pure.eq", _) $ l $ r) = Const ("HOL.Trueprop", @{typ "bool \<Rightarrow> prop"})
+      $ (Const ("HOL.eq", @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"}) $ l $ r)
+  | fix_definition t = t
+fun check_definition [t] = [t]
+  | check_definition _ = error "Only a single defnition is allowed"
+
 (* Convert function into its timing function (called by command) *)
-fun reg_time_fun_cmd (funcs, thms) conv topConv (theory: theory) =
+fun reg_time_fun_cmd (funcs, thms) (theory: theory) =
 let
   val ctxt = Proof_Context.init_global theory
   val fterms = map (Syntax.read_term ctxt) funcs
   val (_, lthy') = reg_and_proove_time_func theory fterms
     (case thms of NONE => get_terms theory (hd fterms)
                 | SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
-    conv topConv true
+    true
 in lthy'
 end
 
 (* Convert function into its timing function (called by command) with termination proof provided by user*)
-fun reg_time_function_cmd (funcs, thms) conv topConv (theory: theory) =
+fun reg_time_function_cmd (funcs, thms) (theory: theory) =
 let
   val ctxt = Proof_Context.init_global theory
   val fterms = map (Syntax.read_term ctxt) funcs
   val theory = reg_time_func theory fterms
     (case thms of NONE => get_terms theory (hd fterms)
                 | SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
-    conv topConv true
+    true
 in theory
 end
 
+(* Convert function into its timing function (called by command) *)
+fun reg_time_definition_cmd (funcs, thms) (theory: theory) =
+let
+  val ctxt = Proof_Context.init_global theory
+  val fterms = map (Syntax.read_term ctxt) funcs
+  val (_, lthy') = reg_and_proove_time_func theory fterms
+    (case thms of NONE => get_terms theory (hd fterms) |> check_definition |> map fix_definition
+                | SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
+    true
+in lthy'
+end
+
 val parser = (Scan.repeat1 Parse.prop) -- (Scan.option (Parse.keyword_improper "equations" -- Parse.thms1 >> snd))
 
-val _ = Outer_Syntax.command @{command_keyword "define_time_fun"}
+val _ = Outer_Syntax.command @{command_keyword "time_fun"}
   "Defines runtime function of a function"
-  (parser >> (fn p => Toplevel.theory (reg_time_fun_cmd p converter top_converter)))
+  (parser >> (fn p => Toplevel.theory (reg_time_fun_cmd p)))
 
-val _ = Outer_Syntax.command @{command_keyword "define_time_function"}
+val _ = Outer_Syntax.command @{command_keyword "time_function"}
   "Defines runtime function of a function"
-  (parser >> (fn p => Toplevel.theory (reg_time_function_cmd p converter top_converter)))
+  (parser >> (fn p => Toplevel.theory (reg_time_function_cmd p)))
+
+val _ = Outer_Syntax.command @{command_keyword "time_definition"}
+  "Defines runtime function of a definition"
+  (parser >> (fn p => Toplevel.theory (reg_time_definition_cmd p)))
 
 end
diff -r 1fd5f96e1da3 -r 773b99044329 src/HOL/Data_Structures/Define_Time_Function.thy
--- a/src/HOL/Data_Structures/Define_Time_Function.thy	Sun Mar 24 14:04:30 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.thy	Sun Mar 24 14:51:03 2024 +0100
@@ -8,10 +8,11 @@
 
 theory Define_Time_Function
   imports Main
-  keywords "define_time_fun" :: thy_decl
-    and    "define_time_function" :: thy_goal
+  keywords "time_fun" :: thy_decl
+    and    "time_function" :: thy_goal
+    and    "time_definition" :: thy_goal
     and    "equations"
-    and    "define_time_0" :: thy_decl
+    and    "time_fun_0" :: thy_decl
 begin
 
 ML_file Define_Time_0.ML
@@ -31,17 +32,17 @@
 The constant-time assumption for \<open>(=)\<close> is justified for recursive data types such as lists and trees
 as long as the comparison is of the form \<open>t = c\<close> where \<open>c\<close> is a constant term, for example \<open>xs = []\<close>.\<close>
 
-define_time_0 "(+)"
-define_time_0 "(-)"
-define_time_0 "(*)"
-define_time_0 "(/)"
-define_time_0 "(div)"
-define_time_0 "(<)"
-define_time_0 "(\<le>)"
-define_time_0 "Not"
-define_time_0 "(\<and>)"
-define_time_0 "(\<or>)"
-define_time_0 "Num.numeral_class.numeral"
-define_time_0 "(=)"
+time_fun_0 "(+)"
+time_fun_0 "(-)"
+time_fun_0 "(*)"
+time_fun_0 "(/)"
+time_fun_0 "(div)"
+time_fun_0 "(<)"
+time_fun_0 "(\<le>)"
+time_fun_0 "Not"
+time_fun_0 "(\<and>)"
+time_fun_0 "(\<or>)"
+time_fun_0 "Num.numeral_class.numeral"
+time_fun_0 "(=)"
 
 end
\ No newline at end of file
diff -r 1fd5f96e1da3 -r 773b99044329 src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Sun Mar 24 14:04:30 2024 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Sun Mar 24 14:51:03 2024 +0100
@@ -160,16 +160,16 @@
 subsection "Complexity"
 
 text \<open>Auxiliary time functions (which are both 0):\<close>
-define_time_fun mht
-define_time_fun node
+time_fun mht
+time_fun node
 
 lemma T_mht_0[simp]: "T_mht t = 0"
 by(cases t)auto
 
 text \<open>Define timing function\<close>
-define_time_fun merge
-define_time_fun insert
-define_time_fun del_min
+time_fun merge
+time_fun insert
+time_fun del_min
 
 lemma T_merge_min_height: "ltree l \<Longrightarrow> ltree r \<Longrightarrow> T_merge l r \<le> min_height l + min_height r + 1"
 proof(induction l r rule: merge.induct)
diff -r 1fd5f96e1da3 -r 773b99044329 src/HOL/Data_Structures/Queue_2Lists.thy
--- a/src/HOL/Data_Structures/Queue_2Lists.thy	Sun Mar 24 14:04:30 2024 +0100
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy	Sun Mar 24 14:51:03 2024 +0100
@@ -59,10 +59,10 @@
 
 text \<open>Running times:\<close>
 
-define_time_fun norm
-define_time_fun enq
-define_time_fun tl
-define_time_fun deq
+time_fun norm
+time_fun enq
+time_fun tl
+time_fun deq
 
 lemma T_tl_0: "T_tl xs = 0"
 by(cases xs)auto
diff -r 1fd5f96e1da3 -r 773b99044329 src/HOL/Data_Structures/Reverse.thy
--- a/src/HOL/Data_Structures/Reverse.thy	Sun Mar 24 14:04:30 2024 +0100
+++ b/src/HOL/Data_Structures/Reverse.thy	Sun Mar 24 14:51:03 2024 +0100
@@ -2,8 +2,8 @@
 imports Define_Time_Function
 begin
 
-define_time_fun append
-define_time_fun rev
+time_fun append
+time_fun rev
 
 lemma T_append: "T_append xs ys = length xs + 1"
 by(induction xs) auto
@@ -21,7 +21,7 @@
 lemma itrev_Nil: "itrev xs [] = rev xs"
 by(simp add: itrev)
 
-define_time_fun itrev
+time_fun itrev
 
 lemma T_itrev: "T_itrev xs ys = length xs + 1"
 by(induction xs arbitrary: ys) auto
diff -r 1fd5f96e1da3 -r 773b99044329 src/HOL/Data_Structures/Set2_Join.thy
--- a/src/HOL/Data_Structures/Set2_Join.thy	Sun Mar 24 14:04:30 2024 +0100
+++ b/src/HOL/Data_Structures/Set2_Join.thy	Sun Mar 24 14:51:03 2024 +0100
@@ -81,36 +81,36 @@
 
 subsection "\<open>split\<close>"
 
-fun split :: "('a*'b)tree \<Rightarrow> 'a \<Rightarrow> ('a*'b)tree \<times> bool \<times> ('a*'b)tree" where
-"split Leaf k = (Leaf, False, Leaf)" |
-"split (Node l (a, _) r) x =
+fun split :: "'a \<Rightarrow> ('a*'b)tree \<Rightarrow> ('a*'b)tree \<times> bool \<times> ('a*'b)tree" where
+"split x Leaf = (Leaf, False, Leaf)" |
+"split x (Node l (a, _) r) =
   (case cmp x a of
-     LT \<Rightarrow> let (l1,b,l2) = split l x in (l1, b, join l2 a r) |
-     GT \<Rightarrow> let (r1,b,r2) = split r x in (join l a r1, b, r2) |
+     LT \<Rightarrow> let (l1,b,l2) = split x l in (l1, b, join l2 a r) |
+     GT \<Rightarrow> let (r1,b,r2) = split x r in (join l a r1, b, r2) |
      EQ \<Rightarrow> (l, True, r))"
 
-lemma split: "split t x = (l,b,r) \<Longrightarrow> bst t \<Longrightarrow>
+lemma split: "split x t = (l,b,r) \<Longrightarrow> bst t \<Longrightarrow>
   set_tree l = {a \<in> set_tree t. a < x} \<and> set_tree r = {a \<in> set_tree t. x < a}
   \<and> (b = (x \<in> set_tree t)) \<and> bst l \<and> bst r"
 proof(induction t arbitrary: l b r rule: tree2_induct)
   case Leaf thus ?case by simp
 next
   case (Node y a b z l c r)
-  consider (LT) l1 xin l2 where "(l1,xin,l2) = split y x" 
-    and "split \<langle>y, (a, b), z\<rangle> x = (l1, xin, join l2 a z)" and "cmp x a = LT"
-  | (GT) r1 xin r2 where "(r1,xin,r2) = split z x" 
-    and "split \<langle>y, (a, b), z\<rangle> x = (join y a r1, xin, r2)" and "cmp x a = GT"
-  | (EQ) "split \<langle>y, (a, b), z\<rangle> x = (y, True, z)" and "cmp x a = EQ"
+  consider (LT) l1 xin l2 where "(l1,xin,l2) = split x y" 
+    and "split x \<langle>y, (a, b), z\<rangle> = (l1, xin, join l2 a z)" and "cmp x a = LT"
+  | (GT) r1 xin r2 where "(r1,xin,r2) = split x z" 
+    and "split x \<langle>y, (a, b), z\<rangle> = (join y a r1, xin, r2)" and "cmp x a = GT"
+  | (EQ) "split x \<langle>y, (a, b), z\<rangle> = (y, True, z)" and "cmp x a = EQ"
     by (force split: cmp_val.splits prod.splits if_splits)
 
   thus ?case 
   proof cases
     case (LT l1 xin l2)
-    with Node.IH(1)[OF \<open>(l1,xin,l2) = split y x\<close>[symmetric]] Node.prems
+    with Node.IH(1)[OF \<open>(l1,xin,l2) = split x y\<close>[symmetric]] Node.prems
     show ?thesis by (force intro!: bst_join)
   next
     case (GT r1 xin r2)
-    with Node.IH(2)[OF \<open>(r1,xin,r2) = split z x\<close>[symmetric]] Node.prems
+    with Node.IH(2)[OF \<open>(r1,xin,r2) = split x z\<close>[symmetric]] Node.prems
     show ?thesis by (force intro!: bst_join)
   next
     case EQ
@@ -118,7 +118,7 @@
   qed
 qed
 
-lemma split_inv: "split t x = (l,b,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
+lemma split_inv: "split x t = (l,b,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
 proof(induction t arbitrary: l b r rule: tree2_induct)
   case Leaf thus ?case by simp
 next
@@ -132,7 +132,7 @@
 subsection "\<open>insert\<close>"
 
 definition insert :: "'a \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"insert x t = (let (l,_,r) = split t x in join l x r)"
+"insert x t = (let (l,_,r) = split x t in join l x r)"
 
 lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = {x} \<union> set_tree t"
 by(auto simp add: insert_def split split: prod.split)
@@ -147,7 +147,7 @@
 subsection "\<open>delete\<close>"
 
 definition delete :: "'a \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"delete x t = (let (l,_,r) = split t x in join2 l r)"
+"delete x t = (let (l,_,r) = split x t in join2 l r)"
 
 lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete x t) = set_tree t - {x}"
 by(auto simp: delete_def split split: prod.split)
@@ -166,7 +166,7 @@
   (if t1 = Leaf then t2 else
    if t2 = Leaf then t1 else
    case t1 of Node l1 (a, _) r1 \<Rightarrow>
-   let (l2,_ ,r2) = split t2 a;
+   let (l2,_ ,r2) = split a t2;
        l' = union l1 l2; r' = union r1 r2
    in join l' a r')"
 
@@ -202,7 +202,7 @@
   (if t1 = Leaf then Leaf else
    if t2 = Leaf then Leaf else
    case t1 of Node l1 (a, _) r1 \<Rightarrow>
-   let (l2,b,r2) = split t2 a;
+   let (l2,b,r2) = split a t2;
        l' = inter l1 l2; r' = inter r1 r2
    in if b then join l' a r' else join2 l' r')"
 
@@ -224,7 +224,7 @@
       case False
       let ?L1 = "set_tree l1" let ?R1 = "set_tree r1"
       have *: "a \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
-      obtain l2 b r2 where sp: "split t2 a = (l2,b,r2)" using prod_cases3 by blast
+      obtain l2 b r2 where sp: "split a t2 = (l2,b,r2)" using prod_cases3 by blast
       let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?A = "if b then {a} else {}"
       have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?A" and
            **: "?L2 \<inter> ?R2 = {}" "a \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
@@ -267,7 +267,7 @@
   (if t1 = Leaf then Leaf else
    if t2 = Leaf then t1 else
    case t2 of Node l2 (a, _) r2 \<Rightarrow>
-   let (l1,_,r1) = split t1 a;
+   let (l1,_,r1) = split a t1;
        l' = diff l1 l2; r' = diff r1 r2
    in join2 l' r')"
 
@@ -288,7 +288,7 @@
     next
       case False
       let ?L2 = "set_tree l2" let ?R2 = "set_tree r2"
-      obtain l1 b r1 where sp: "split t1 a = (l1,b,r1)" using prod_cases3 by blast
+      obtain l1 b r1 where sp: "split a t1 = (l1,b,r1)" using prod_cases3 by blast
       let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?A = "if b then {a} else {}"
       have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?A" and
            **: "a \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
diff -r 1fd5f96e1da3 -r 773b99044329 src/HOL/Data_Structures/Time_Funs.thy
--- a/src/HOL/Data_Structures/Time_Funs.thy	Sun Mar 24 14:04:30 2024 +0100
+++ b/src/HOL/Data_Structures/Time_Funs.thy	Sun Mar 24 14:51:03 2024 +0100
@@ -48,8 +48,8 @@
 
 lemmas [simp del] = T_nth.simps
 
-define_time_fun take
-define_time_fun drop
+time_fun take
+time_fun drop
 
 lemma T_take_eq: "T_take n xs = min n (length xs) + 1"
   by (induction xs arbitrary: n) (auto split: nat.splits)
diff -r 1fd5f96e1da3 -r 773b99044329 src/HOL/Data_Structures/Tree23_of_List.thy
--- a/src/HOL/Data_Structures/Tree23_of_List.thy	Sun Mar 24 14:04:30 2024 +0100
+++ b/src/HOL/Data_Structures/Tree23_of_List.thy	Sun Mar 24 14:51:03 2024 +0100
@@ -118,10 +118,10 @@
 
 subsection "Linear running time"
 
-define_time_fun join_adj
-define_time_fun join_all
-define_time_fun leaves
-define_time_fun tree23_of_list
+time_fun join_adj
+time_fun join_all
+time_fun leaves
+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