# HG changeset patch
# User nipkow
# Date 1028737970 -7200
# Node ID 194e8d2cbe0f5741c7880b21e26a0e259325053a
# Parent  2529a53514e654e90e55156bc6d01c9acbb2b635
Added time example at the end.

diff -r 2529a53514e6 -r 194e8d2cbe0f src/HOL/Isar_examples/HoareEx.thy
--- a/src/HOL/Isar_examples/HoareEx.thy	Wed Aug 07 17:36:05 2002 +0200
+++ b/src/HOL/Isar_examples/HoareEx.thy	Wed Aug 07 18:32:50 2002 +0200
@@ -284,4 +284,55 @@
       .{\<acute>S = (SUM j<n. j)}."
   by hoare auto
 
-end
\ No newline at end of file
+subsection{*Time*}
+
+text{*
+A simple embedding of time in Hoare logic: function @{text timeit}
+inserts an extra variable to keep track of the elapsed time.
+*}
+
+record tstate = time :: nat
+
+types 'a time = "\<lparr>time::nat, \<dots>::'a\<rparr>"
+
+consts timeit :: "'a time com \<Rightarrow> 'a time com"
+primrec
+"timeit(Basic f) = (Basic f; Basic(%s. s\<lparr>time := Suc(time s)\<rparr>))"
+"timeit(c1;c2) = (timeit c1; timeit c2)"
+"timeit(Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
+"timeit(While b iv c) = While b iv (timeit c)"
+
+
+record tvars = tstate +
+  I :: nat
+  J :: nat
+
+lemma lem: "(0::nat) < n \<Longrightarrow> n+n \<le> Suc(n*n)"
+by(induct n, simp_all)
+
+lemma "|- .{i = \<acute>I & \<acute>time = 0}.
+ timeit(
+ WHILE \<acute>I \<noteq> 0
+ INV .{2*\<acute>time + \<acute>I*\<acute>I + 5*\<acute>I = i*i + 5*i}.
+ DO
+   \<acute>J := \<acute>I;
+   WHILE \<acute>J \<noteq> 0
+   INV .{0 < \<acute>I & 2*\<acute>time + \<acute>I*\<acute>I + 3*\<acute>I + 2*\<acute>J - 2 = i*i + 5*i}.
+   DO \<acute>J := \<acute>J - 1 OD;
+   \<acute>I := \<acute>I - 1
+ OD
+ ) .{2*\<acute>time = i*i + 5*i}."
+apply simp
+apply hoare
+    apply simp
+   apply clarsimp
+  apply clarsimp
+  apply arith
+ prefer 2
+ apply clarsimp
+apply (clarsimp simp:nat_distrib)
+apply(frule lem)
+apply arith
+done
+
+end