# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1236793097 0
# Node ID 3e30ea95c7aa395246e8f9f5fdaa1698e82701aa
# Parent  00d153e32a5391b415e92a6aebdd17455219c5ab
added temporarily some timing test about conversions and simprocs

diff -r 00d153e32a53 -r 3e30ea95c7aa CookBook/Intro.thy
--- a/CookBook/Intro.thy	Wed Mar 11 13:42:03 2009 +0000
+++ b/CookBook/Intro.thy	Wed Mar 11 17:38:17 2009 +0000
@@ -130,7 +130,7 @@
 
   \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 
   \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}.
-  He also wrote section \ref{sec:conversion}.
+  He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}.
 
   \item {\bf Jeremy Dawson} wrote the first version of the chapter
   about parsing.
diff -r 00d153e32a53 -r 3e30ea95c7aa CookBook/Recipes/Timing.thy
--- a/CookBook/Recipes/Timing.thy	Wed Mar 11 13:42:03 2009 +0000
+++ b/CookBook/Recipes/Timing.thy	Wed Mar 11 17:38:17 2009 +0000
@@ -2,7 +2,7 @@
 imports "../Base"
 begin
 
-section {* Measuring Time\label{rec:timing} (TBD) *} 
+section {* Measuring Time\label{rec:timing} *} 
 
 text {*
  {\bf Problem:}
@@ -11,8 +11,8 @@
   {\bf Solution:} Time can be measured using the function 
   @{ML start_timing} and @{ML end_timing}.\smallskip
 
+  Assume the following function defined in Isabelle. 
 *}
-ML {* timeap *}
 
 fun 
  ackermann:: "(nat * nat) \<Rightarrow> nat"
@@ -21,18 +21,43 @@
   | "ackermann (m, 0) = ackermann (m - 1, 1)"
   | "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))"
 
-text {* Does not work yet! *}
+text {* 
+  We can now measure how long the simplifier takes to verify a datapoint
+  of this function. The timing can be done using the following wrapper function:
+*}
+
+ML{*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 also takes a state @{text "st"} as an argument and
+  applies this state to the tactic. This is because tactics are lazy functions
+  and we need to force them to run, otherwise the timing will be meaningless.
+  The used time will be calculated as the end time minus the start time.
+  The wrapper can now be used in the proof
+*}
 
 lemma "ackermann (3, 4) = 125"
-apply(tactic {* timeap  (asm_full_simp_tac (@{simpset} addsimps @{thms "nat_number"})) 1 *})
-(*
 apply(tactic {* 
-  let 
-    val start = start_timing ();
-    val res = asm_full_simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1;
-  in
-    (warning (#message  (end_timing start)); res)
-  end *})*)
+  timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *})
 done
 
+text {*
+  where it returns something on the cale of 3 seconds.
+
+  \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
diff -r 00d153e32a53 -r 3e30ea95c7aa CookBook/Solutions.thy
--- a/CookBook/Solutions.thy	Wed Mar 11 13:42:03 2009 +0000
+++ b/CookBook/Solutions.thy	Wed Mar 11 17:38:17 2009 +0000
@@ -1,5 +1,5 @@
 theory Solutions
-imports Base
+imports Base 
 begin
 
 chapter {* Solutions to Most Exercises\label{ch:solutions} *}
@@ -84,7 +84,7 @@
 text {* and a test case is the lemma *}
 
 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
-  apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc add_sp}]) 1 *})
+  apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *})
 txt {* 
   where the simproc produces the goal state
   
@@ -132,5 +132,63 @@
   \end{minipage}\bigskip
 *}(*<*)oops(*>*)
 
+subsection {* Tests start here *}
+
+lemma cheat: "P" sorry
+
+ML{*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*}
+
+ML{* 
+fun create_term1 0 = @{term "0::nat"}
+  | create_term1 n = 
+       Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 
+         $ (HOLogic.mk_number @{typ "nat"} n) $ (create_term1 (n-1))
+*}
+
+ML{* 
+fun create_term2 0 = @{term "0::nat"}
+  | create_term2 n = 
+       Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 
+         $ (create_term2 (n-1)) $ (HOLogic.mk_number @{typ nat} n)
+*}
+
+ML{*
+fun create_term n = 
+  HOLogic.mk_Trueprop
+  (@{term "P::nat\<Rightarrow> bool"} $ 
+   (Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 
+    $ (create_term1 n) $ (create_term2 n)))
+*}
+
+ML {*
+warning (Syntax.string_of_term @{context} (create_term 4))
+*}
+
+ML {* 
+val _ = Goal.prove @{context} [] [] (create_term 100) 
+   (fn _ => timing_wrapper (EVERY1 [add_tac, rtac @{thm cheat}]))
+*}
+
+ML {* 
+val _ = Goal.prove @{context} [] [] (create_term 100) 
+   (fn _ => timing_wrapper (EVERY1 [simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]), rtac @{thm cheat}]))
+*}
+
+ML {* 
+val _ = Goal.prove @{context} [] [] (create_term 400) 
+  (fn _ => timing_wrapper (EVERY1 [add_tac, rtac @{thm cheat}]))
+*}
+
+ML {* 
+val _ = Goal.prove @{context} [] [] (create_term 400) 
+   (fn _ => timing_wrapper (EVERY1 [simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]), rtac @{thm cheat}]))
+*}
 
 end
\ No newline at end of file
diff -r 00d153e32a53 -r 3e30ea95c7aa cookbook.pdf
Binary file cookbook.pdf has changed