# HG changeset patch
# User nipkow
# Date 1711372105 -3600
# Node ID 7bbb0d65ce72d7bba6f170c8d25524afb2fcaba8
# Parent  217f8173d3585b1f10b74d6901f3cf7cc95caf4c
documented running time function framework by Jonas Stahl

diff -r 217f8173d358 -r 7bbb0d65ce72 CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Mar 25 10:16:14 2024 +0100
+++ b/CONTRIBUTORS	Mon Mar 25 14:08:25 2024 +0100
@@ -12,6 +12,10 @@
 * March 2024: Anthony Bordg, Manuel Eberl, Wenda Li, Larry Paulson
   New and more general definition of meromorphicity in HOL-Complex_Analysis
 
+* Feb/March 2024: Jonas Stahl
+  Automatic translation of HOL functions into corresponding
+  step-counting running-time functions
+
 * 2023/2024: Makarius Wenzel and Fabian Huch
   More robust and scalable support for distributed build clusters.
 
diff -r 217f8173d358 -r 7bbb0d65ce72 NEWS
--- a/NEWS	Mon Mar 25 10:16:14 2024 +0100
+++ b/NEWS	Mon Mar 25 14:08:25 2024 +0100
@@ -52,6 +52,9 @@
     "preplay_timeout". INCOMPATIBILITY.
   - Added the action "order" testing the proof method of the same name.
 
+* Session Data_Structures provides automatic translation from
+HOL functions into corresponding step-counting running-time functions.See theory Define_Time_Function.
+
 * Explicit type class for discrete_linear_ordered_semidom for integral
 semidomains with a discrete linear order.
 
diff -r 217f8173d358 -r 7bbb0d65ce72 src/HOL/Data_Structures/Define_Time_Function.thy
--- a/src/HOL/Data_Structures/Define_Time_Function.thy	Mon Mar 25 10:16:14 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.thy	Mon Mar 25 14:08:25 2024 +0100
@@ -1,9 +1,10 @@
 (*
 Author: Jonas Stahl
 
-Automatic definition of running time functions from HOL functions
+Automatic definition of step-counting running-time functions from HOL functions
 following the translation described in Section 1.5, Running Time, of the book
 Functional Data Structures and Algorithms. A Proof Assistant Approach.
+See https://functional-algorithms-verified.org
 *)
 
 theory Define_Time_Function
@@ -20,17 +21,33 @@
 
 declare [[time_prefix = "T_"]]
 
-text \<open>The pre-defined functions below are assumed to have constant running time.
+text \<open>
+This theory provides commands for the automatic definition of step-counting running-time functions
+from HOL functions following the translation described in Section 1.5, Running Time, of the book
+"Functional Data Structures and Algorithms. A Proof Assistant Approach."
+See @{url "https://functional-algorithms-verified.org"}
+
+Command \<open>time_fun f\<close> retrieves the definition of \<open>f\<close> and defines a corresponding step-counting
+running-time function \<open>T_f\<close>. For all auxiliary functions used by \<open>f\<close> (excluding constructors),
+running time functions must already have been defined.
+If the definition of the function requires a manual termination proof,
+use \<open>time_function\<close> accompanied by a \<open>termination\<close> command.
+Limitation: The commands do not work properly in locales yet.
+
+The pre-defined functions below are assumed to have constant running time.
 In fact, we make that constant 0.
 This does not change the asymptotic running time of user-defined functions using the
 pre-defined functions because 1 is added for every user-defined function call.
 
-Note: Many of the functions below are polymorphic and reside in type classes.
+Many of the functions below are polymorphic and reside in type classes.
 The constant-time assumption is justified only for those types where the hardware offers
 suitable support, e.g. numeric types. The argument size is implicitly bounded, too.
 
 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>
+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>.
+
+Users of this running time framework need to ensure that 0-time functions are used only
+within the above restrictions.\<close>
 
 time_fun_0 "(+)"
 time_fun_0 "(-)"