# HG changeset patch
# User nipkow
# Date 1326454282 -3600
# Node ID d43ddad41d81435b84d31a00a883734639f90f11
# Parent  78175db15b9180bec4723b022f23dca53feea348
tuned

diff -r 78175db15b91 -r d43ddad41d81 src/HOL/IMP/HoareT.thy
--- a/src/HOL/IMP/HoareT.thy	Fri Jan 13 11:55:06 2012 +0100
+++ b/src/HOL/IMP/HoareT.thy	Fri Jan 13 12:31:22 2012 +0100
@@ -2,9 +2,8 @@
 
 theory HoareT imports Hoare_Sound_Complete begin
 
-text{*
-Now that we have termination, we can define
-total validity, @{text"\<Turnstile>\<^sub>t"}, as partial validity and guaranteed termination:*}
+text{* Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only
+works if execution is deterministic (which it is in our case). *}
 
 definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
   ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
@@ -61,15 +60,14 @@
 apply(rule Semi)
 prefer 2
 apply(rule While'
-  [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 <= n \<and> 0 <= s ''y'' \<and> s ''y'' \<le> n"
-   and f = "\<lambda>s. nat n - nat (s ''y'')"])
+  [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"
+   and f = "\<lambda>s. nat (n - s ''y'')"])
 apply(rule Semi)
 prefer 2
 apply(rule Assign)
 apply(rule Assign')
 apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)
 apply clarsimp
-apply arith
 apply fastforce
 apply(rule Semi)
 prefer 2