isabelle-cookbook: CookBook/Recipes/Timing.thy@b6fca043a796 (annotated)

154 e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Timing
e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports "../Base"
e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
155 b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	5	section {* Measuring the Time of an Operation\label{rec:timing} (TBD) *}
154 e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	text {*
e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	{\bf Problem:}
e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	You want to measure the running time of a tactic or function.\smallskip
e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	10
e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	{\bf Solution:} Time can be measured using the function
e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	@{ML start_timing} and @{ML end_timing}.\smallskip
e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	13
e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	*}
155 b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	15	ML {* timeap *}
154 e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	16
155 b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	17	fun
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	18	ackermann:: "(nat * nat) \<Rightarrow> nat"
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	19	where
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	20	"ackermann (0, n) = n + 1"
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	21	\| "ackermann (m, 0) = ackermann (m - 1, 1)"
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	22	\| "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))"
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	23
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	24	text {* Does not work yet! *}
154 e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	25
155 b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	26	lemma "ackermann (3, 4) = 125"
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	27	apply(tactic {* timeap (asm_full_simp_tac (@{simpset} addsimps @{thms "nat_number"})) 1 *})
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	28	(*
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	29	apply(tactic {*
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	30	let
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	31	val start = start_timing ();
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	32	val res = asm_full_simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1;
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	33	in
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	34	(warning (#message (end_timing start)); res)
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	35	end }))
b6fca043a796 tuned Christian Urban <urbanc@in.tum.de> parents: 154 diff changeset	36	done
154 e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	37
e81ebb37aa83 updated to repository version; added a section about timing Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	end

author	Christian Urban <urbanc@in.tum.de>
	Mon, 02 Mar 2009 10:06:06 +0000 (2009-03-02)
changeset 155	b6fca043a796
parent 154	e81ebb37aa83
child 157	76cdc8f562fc
permissions	-rw-r--r--