# HG changeset patch
# User nipkow
# Date 1369895271 -7200
# Node ID ee8e3eaad24c64bb0327e0ce546eb0d45786aa32
# Parent  f9e68ba3f004e9eecebb46d3cef7375207446146
tuned

diff -r f9e68ba3f004 -r ee8e3eaad24c src/HOL/IMP/HoareT.thy
--- a/src/HOL/IMP/HoareT.thy	Thu May 30 13:59:20 2013 +1000
+++ b/src/HOL/IMP/HoareT.thy	Thu May 30 08:27:51 2013 +0200
@@ -1,6 +1,6 @@
 (* Author: Tobias Nipkow *)
 
-theory HoareT imports Hoare_Sound_Complete begin
+theory HoareT imports Hoare_Sound_Complete Hoare_Examples begin
 
 subsection "Hoare Logic for Total Correctness"
 
@@ -26,8 +26,8 @@
 If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>
   \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" |
 While:
-  "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T n s} c {\<lambda>s. P s \<and> (\<exists>n'. T n' s \<and> n' < n)} \<rbrakk>
-   \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T n s)} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" |
+  "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T s n} c {\<lambda>s. P s \<and> (\<exists>n'. T s n' \<and> n' < n)} \<rbrakk>
+   \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T s n)} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" |
 conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
            \<turnstile>\<^sub>t {P'}c{Q'}"
 
@@ -47,37 +47,30 @@
 by (simp add: strengthen_pre[OF _ Assign])
 
 lemma While':
-assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T n s} c {\<lambda>s. P s \<and> (\<exists>n'. T n' s \<and> n' < n)}"
+assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T s n} c {\<lambda>s. P s \<and> (\<exists>n'. T s n' \<and> n' < n)}"
     and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
-shows "\<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T n s)} WHILE b DO c {Q}"
+shows "\<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T s n)} WHILE b DO c {Q}"
 by(blast intro: assms(1) weaken_post[OF While assms(2)])
 
 lemma While_fun:
   "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}\<rbrakk>
    \<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}"
-  by (rule While [where T="\<lambda>n s. f s = n", simplified])
+  by (rule While [where T="\<lambda>s n. f s = n", simplified])
 
 text{* Our standard example: *}
 
-abbreviation "w n ==
-  WHILE Less (V ''y'') (N n)
-  DO ( ''y'' ::= Plus (V ''y'') (N 1);; ''x'' ::= Plus (V ''x'') (V ''y'') )"
-
-lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 \<le> n} ''x'' ::= N 0;; ''y'' ::= N 0;; w n {\<lambda>s. s ''x'' = \<Sum>{1..n}}"
+lemma "\<turnstile>\<^sub>t {\<lambda>s. s ''x'' = i} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum i}"
 apply(rule Seq)
-prefer 2
-apply(rule While'
-  [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"
-   and T = "\<lambda>n' s. n' = nat (n - s ''y'')"])
-apply(rule Seq)
-prefer 2
-apply(rule Assign)
-apply(rule Assign')
-apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)
-apply clarsimp
-apply(rule Seq)
-prefer 2
-apply(rule Assign)
+ prefer 2
+ apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum i - sum(s ''x''))"
+    and T = "\<lambda>s n. n = nat(s ''x'')"])
+   apply(rule Seq)
+   prefer 2
+   apply(rule Assign)
+  apply(rule Assign')
+  apply simp
+  apply(simp add: minus_numeral_simps(1)[symmetric] del: minus_numeral_simps)
+ apply(simp)
 apply(rule Assign')
 apply simp
 done
@@ -90,7 +83,7 @@
   case (While P b T c)
   {
     fix s n
-    have "\<lbrakk> P s; T n s \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t"
+    have "\<lbrakk> P s; T s n \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t"
     proof(induction "n" arbitrary: s rule: less_induct)
       case (less n)
       thus ?case by (metis While(2) WhileFalse WhileTrue)
@@ -168,25 +161,25 @@
 next
   case (While b c)
   let ?w = "WHILE b DO c"
-  let ?T = "\<lambda>n s. Its b c s n"
+  let ?T = "Its b c"
   have "\<forall>s. wp\<^sub>t (WHILE b DO c) Q s \<longrightarrow> wp\<^sub>t (WHILE b DO c) Q s \<and> (\<exists>n. Its b c s n)"
     unfolding wpt_def by (metis WHILE_Its)
   moreover
   { fix n
     { fix s t
-      assume "bval b s" "?T n s" "(?w, s) \<Rightarrow> t" "Q t"
+      assume "bval b s" "?T s n" "(?w, s) \<Rightarrow> t" "Q t"
       from `bval b s` `(?w, s) \<Rightarrow> t` obtain s' where
         "(c,s) \<Rightarrow> s'" "(?w,s') \<Rightarrow> t" by auto      
-      from `(?w, s') \<Rightarrow> t` obtain n'' where "?T n'' s'" by (blast dest: WHILE_Its)
+      from `(?w, s') \<Rightarrow> t` obtain n'' where "?T s' n''" by (blast dest: WHILE_Its)
       with `bval b s` `(c, s) \<Rightarrow> s'`
-      have "?T (Suc n'') s" by (rule Its_Suc)
-      with `?T n s` have "n = Suc n''" by (rule Its_fun)
-      with `(c,s) \<Rightarrow> s'` `(?w,s') \<Rightarrow> t` `Q t` `?T n'' s'`
-      have "wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T n' s' \<and> n' < n)) s"
+      have "?T s (Suc n'')" by (rule Its_Suc)
+      with `?T s n` have "n = Suc n''" by (rule Its_fun)
+      with `(c,s) \<Rightarrow> s'` `(?w,s') \<Rightarrow> t` `Q t` `?T s' n''`
+      have "wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T s' n' \<and> n' < n)) s"
         by (auto simp: wpt_def)
     } 
-    hence "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T n s \<longrightarrow>
-              wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T n' s' \<and> n' < n)) s"
+    hence "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow>
+              wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T s' n' \<and> n' < n)) s"
       unfolding wpt_def by auto
       (* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *) 
     note strengthen_pre[OF this While]