diff -r e81ebb37aa83 -r b6fca043a796 CookBook/Recipes/Timing.thy --- a/CookBook/Recipes/Timing.thy Sun Mar 01 21:48:59 2009 +0000 +++ b/CookBook/Recipes/Timing.thy Mon Mar 02 10:06:06 2009 +0000 @@ -2,7 +2,7 @@ imports "../Base" begin -section {* Measuring the Time of an Operation\label{rec:timing} *} +section {* Measuring the Time of an Operation\label{rec:timing} (TBD) *} text {* {\bf Problem:} @@ -12,23 +12,27 @@ @{ML start_timing} and @{ML end_timing}.\smallskip *} +ML {* timeap *} -ML{*fun ackermann (0, n) = n + 1 - | ackermann (m, 0) = ackermann (m - 1, 1) - | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *} +fun + ackermann:: "(nat * nat) \ 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 {* Does not work yet! *} -ML {* -let - val start = start_timing () - val res = ackermann (3,12) - val time = (end_timing start) -in - (res,time) -end -*} - -text {* - check what @{text "#all"} does? -*} +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 *})*) +done end \ No newline at end of file