--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Recipes/Timing.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,69 @@
+theory Timing
+imports "../Base"
+begin
+
+section {* Measuring Time\label{rec:timing} *} 
+
+text {*
+ {\bf Problem:}
+  You want to measure the running time of a tactic or function.\smallskip
+
+  {\bf Solution:} Time can be measured using the function 
+  @{ML start_timing} and @{ML end_timing}.\smallskip
+
+  Suppose you defined the Ackermann function inside Isabelle. 
+*}
+
+fun 
+ ackermann:: "(nat \<times> nat) \<Rightarrow> nat"
+where
+    "ackermann (0, n) = n + 1"
+  | "ackermann (m, 0) = ackermann (m - 1, 1)"
+  | "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))"
+
+text {* 
+  You can measure how long the simplifier takes to verify a datapoint
+  of this function. The timing of a tactic can be done using the following 
+  wrapper function:
+*}
+
+ML %linenosgray{*fun timing_wrapper tac st =
+let 
+  val t_start = start_timing ();
+  val res = tac st;
+  val t_end = end_timing t_start;
+in
+  (warning (#message t_end); res)
+end*}
+
+text {*
+  Note that this function, in addition to a tactic, also takes a state @{text
+  "st"} as argument and applies this state to the tactic (Line 4). The reason is that
+  tactics are lazy functions and you need to force them to run, otherwise the
+  timing will be meaningless.  The time between start and finish of the tactic
+  will be calculated as the end time minus the start time.  An example of the
+  wrapper is the proof
+
+
+*}
+
+lemma "ackermann (3, 4) = 125"
+apply(tactic {* 
+  timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *})
+done
+
+text {*
+  where it returns something on the scale of 3 seconds. We chose to return
+  this information as a string, but the timing information is also accessible
+  in number format.
+
+  \begin{readmore}
+  Basic functions regarding timing are defined in @{ML_file 
+  "Pure/ML-Systems/polyml_common.ML"} (for the PolyML compiler). Some more
+  advanced functions are defined in @{ML_file "Pure/General/output.ML"}.
+  \end{readmore}
+*}
+
+
+
+end
\ No newline at end of file