--- 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