tuned theory name
authornipkow
Sat Jun 01 12:02:41 2013 +0200 (2013-06-01)
changeset 52282c79a3e15779e
parent 52281 780b3870319f
child 52283 1ce9feb47535
tuned theory name
src/HOL/IMP/HoareT.thy
src/HOL/IMP/Hoare_Total.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/IMP/HoareT.thy	Sat Jun 01 11:48:06 2013 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,214 +0,0 @@
     1.4 -(* Author: Tobias Nipkow *)
     1.5 -
     1.6 -theory HoareT imports Hoare_Sound_Complete Hoare_Examples begin
     1.7 -
     1.8 -subsection "Hoare Logic for Total Correctness"
     1.9 -
    1.10 -text{* Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only
    1.11 -works if execution is deterministic (which it is in our case). *}
    1.12 -
    1.13 -definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
    1.14 -  ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
    1.15 -"\<Turnstile>\<^sub>t {P}c{Q}  \<longleftrightarrow>  (\<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t))"
    1.16 -
    1.17 -text{* Provability of Hoare triples in the proof system for total
    1.18 -correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined
    1.19 -inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for
    1.20 -@{text"\<turnstile>"} only in the one place where nontermination can arise: the
    1.21 -@{term While}-rule. *}
    1.22 -
    1.23 -inductive
    1.24 -  hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
    1.25 -where
    1.26 -
    1.27 -Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}"  |
    1.28 -
    1.29 -Assign:  "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}"  |
    1.30 -
    1.31 -Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \<turnstile>\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1;;c\<^isub>2 {P\<^isub>3}"  |
    1.32 -
    1.33 -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>
    1.34 -  \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}"  |
    1.35 -
    1.36 -While:
    1.37 -  "(\<And>n::nat.
    1.38 -    \<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)})
    1.39 -   \<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}"  |
    1.40 -
    1.41 -conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
    1.42 -           \<turnstile>\<^sub>t {P'}c{Q'}"
    1.43 -
    1.44 -text{* The @{term While}-rule is like the one for partial correctness but it
    1.45 -requires additionally that with every execution of the loop body some measure
    1.46 -relation @{term[source]"T :: state \<Rightarrow> nat \<Rightarrow> bool"} decreases.
    1.47 -The following functional version is more intuitive: *}
    1.48 -
    1.49 -lemma While_fun:
    1.50 -  "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> n = f s} c {\<lambda>s. P s \<and> f s < n}\<rbrakk>
    1.51 -   \<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}"
    1.52 -  by (rule While [where T="\<lambda>s n. n = f s", simplified])
    1.53 -
    1.54 -text{* Building in the consequence rule: *}
    1.55 -
    1.56 -lemma strengthen_pre:
    1.57 -  "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
    1.58 -by (metis conseq)
    1.59 -
    1.60 -lemma weaken_post:
    1.61 -  "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
    1.62 -by (metis conseq)
    1.63 -
    1.64 -lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
    1.65 -by (simp add: strengthen_pre[OF _ Assign])
    1.66 -
    1.67 -lemma While_fun':
    1.68 -assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> n = f s} c {\<lambda>s. P s \<and> f s < n}"
    1.69 -    and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
    1.70 -shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}"
    1.71 -by(blast intro: assms(1) weaken_post[OF While_fun assms(2)])
    1.72 -
    1.73 -
    1.74 -text{* Our standard example: *}
    1.75 -
    1.76 -lemma "\<turnstile>\<^sub>t {\<lambda>s. s ''x'' = i} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum i}"
    1.77 -apply(rule Seq)
    1.78 - prefer 2
    1.79 - apply(rule While_fun' [where P = "\<lambda>s. (s ''y'' = sum i - sum(s ''x''))"
    1.80 -    and f = "\<lambda>s. nat(s ''x'')"])
    1.81 -   apply(rule Seq)
    1.82 -   prefer 2
    1.83 -   apply(rule Assign)
    1.84 -  apply(rule Assign')
    1.85 -  apply simp
    1.86 -  apply(simp add: minus_numeral_simps(1)[symmetric] del: minus_numeral_simps)
    1.87 - apply(simp)
    1.88 -apply(rule Assign')
    1.89 -apply simp
    1.90 -done
    1.91 -
    1.92 -
    1.93 -text{* The soundness theorem: *}
    1.94 -
    1.95 -theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
    1.96 -proof(unfold hoare_tvalid_def, induct rule: hoaret.induct)
    1.97 -  case (While P b T c)
    1.98 -  {
    1.99 -    fix s n
   1.100 -    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"
   1.101 -    proof(induction "n" arbitrary: s rule: less_induct)
   1.102 -      case (less n)
   1.103 -      thus ?case by (metis While(2) WhileFalse WhileTrue)
   1.104 -    qed
   1.105 -  }
   1.106 -  thus ?case by auto
   1.107 -next
   1.108 -  case If thus ?case by auto blast
   1.109 -qed fastforce+
   1.110 -
   1.111 -
   1.112 -text{*
   1.113 -The completeness proof proceeds along the same lines as the one for partial
   1.114 -correctness. First we have to strengthen our notion of weakest precondition
   1.115 -to take termination into account: *}
   1.116 -
   1.117 -definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where
   1.118 -"wp\<^sub>t c Q  \<equiv>  \<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t"
   1.119 -
   1.120 -lemma [simp]: "wp\<^sub>t SKIP Q = Q"
   1.121 -by(auto intro!: ext simp: wpt_def)
   1.122 -
   1.123 -lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
   1.124 -by(auto intro!: ext simp: wpt_def)
   1.125 -
   1.126 -lemma [simp]: "wp\<^sub>t (c\<^isub>1;;c\<^isub>2) Q = wp\<^sub>t c\<^isub>1 (wp\<^sub>t c\<^isub>2 Q)"
   1.127 -unfolding wpt_def
   1.128 -apply(rule ext)
   1.129 -apply auto
   1.130 -done
   1.131 -
   1.132 -lemma [simp]:
   1.133 - "wp\<^sub>t (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^isub>1 else c\<^isub>2) Q s)"
   1.134 -apply(unfold wpt_def)
   1.135 -apply(rule ext)
   1.136 -apply auto
   1.137 -done
   1.138 -
   1.139 -
   1.140 -text{* Now we define the number of iterations @{term "WHILE b DO c"} needs to
   1.141 -terminate when started in state @{text s}. Because this is a truly partial
   1.142 -function, we define it as an (inductive) relation first: *}
   1.143 -
   1.144 -inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where
   1.145 -Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0" |
   1.146 -Its_Suc: "\<lbrakk> bval b s;  (c,s) \<Rightarrow> s';  Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)"
   1.147 -
   1.148 -text{* The relation is in fact a function: *}
   1.149 -
   1.150 -lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
   1.151 -proof(induction arbitrary: n' rule:Its.induct)
   1.152 -  case Its_0 thus ?case by(metis Its.cases)
   1.153 -next
   1.154 -  case Its_Suc thus ?case by(metis Its.cases big_step_determ)
   1.155 -qed
   1.156 -
   1.157 -text{* For all terminating loops, @{const Its} yields a result: *}
   1.158 -
   1.159 -lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"
   1.160 -proof(induction "WHILE b DO c" s t rule: big_step_induct)
   1.161 -  case WhileFalse thus ?case by (metis Its_0)
   1.162 -next
   1.163 -  case WhileTrue thus ?case by (metis Its_Suc)
   1.164 -qed
   1.165 -
   1.166 -lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
   1.167 -proof (induction c arbitrary: Q)
   1.168 -  case SKIP show ?case by simp (blast intro:hoaret.Skip)
   1.169 -next
   1.170 -  case Assign show ?case by simp (blast intro:hoaret.Assign)
   1.171 -next
   1.172 -  case Seq thus ?case by simp (blast intro:hoaret.Seq)
   1.173 -next
   1.174 -  case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq)
   1.175 -next
   1.176 -  case (While b c)
   1.177 -  let ?w = "WHILE b DO c"
   1.178 -  let ?T = "Its b c"
   1.179 -  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)"
   1.180 -    unfolding wpt_def by (metis WHILE_Its)
   1.181 -  moreover
   1.182 -  { fix n
   1.183 -    { fix s t
   1.184 -      assume "bval b s" "?T s n" "(?w, s) \<Rightarrow> t" "Q t"
   1.185 -      from `bval b s` `(?w, s) \<Rightarrow> t` obtain s' where
   1.186 -        "(c,s) \<Rightarrow> s'" "(?w,s') \<Rightarrow> t" by auto      
   1.187 -      from `(?w, s') \<Rightarrow> t` obtain n'' where "?T s' n''" by (blast dest: WHILE_Its)
   1.188 -      with `bval b s` `(c, s) \<Rightarrow> s'`
   1.189 -      have "?T s (Suc n'')" by (rule Its_Suc)
   1.190 -      with `?T s n` have "n = Suc n''" by (rule Its_fun)
   1.191 -      with `(c,s) \<Rightarrow> s'` `(?w,s') \<Rightarrow> t` `Q t` `?T s' n''`
   1.192 -      have "wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T s' n' \<and> n' < n)) s"
   1.193 -        by (auto simp: wpt_def)
   1.194 -    } 
   1.195 -    hence "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow>
   1.196 -              wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T s' n' \<and> n' < n)) s"
   1.197 -      unfolding wpt_def by auto
   1.198 -      (* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *) 
   1.199 -    note strengthen_pre[OF this While]
   1.200 -  } note hoaret.While[OF this]
   1.201 -  moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by (auto simp add:wpt_def)
   1.202 -  ultimately show ?case by (rule conseq) 
   1.203 -qed
   1.204 -
   1.205 -
   1.206 -text{*\noindent In the @{term While}-case, @{const Its} provides the obvious
   1.207 -termination argument.
   1.208 -
   1.209 -The actual completeness theorem follows directly, in the same manner
   1.210 -as for partial correctness: *}
   1.211 -
   1.212 -theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
   1.213 -apply(rule strengthen_pre[OF _ wpt_is_pre])
   1.214 -apply(auto simp: hoare_tvalid_def hoare_valid_def wpt_def)
   1.215 -done
   1.216 -
   1.217 -end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/IMP/Hoare_Total.thy	Sat Jun 01 12:02:41 2013 +0200
     2.3 @@ -0,0 +1,214 @@
     2.4 +(* Author: Tobias Nipkow *)
     2.5 +
     2.6 +theory Hoare_Total imports Hoare_Sound_Complete Hoare_Examples begin
     2.7 +
     2.8 +subsection "Hoare Logic for Total Correctness"
     2.9 +
    2.10 +text{* Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only
    2.11 +works if execution is deterministic (which it is in our case). *}
    2.12 +
    2.13 +definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
    2.14 +  ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
    2.15 +"\<Turnstile>\<^sub>t {P}c{Q}  \<longleftrightarrow>  (\<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t))"
    2.16 +
    2.17 +text{* Provability of Hoare triples in the proof system for total
    2.18 +correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined
    2.19 +inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for
    2.20 +@{text"\<turnstile>"} only in the one place where nontermination can arise: the
    2.21 +@{term While}-rule. *}
    2.22 +
    2.23 +inductive
    2.24 +  hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
    2.25 +where
    2.26 +
    2.27 +Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}"  |
    2.28 +
    2.29 +Assign:  "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}"  |
    2.30 +
    2.31 +Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \<turnstile>\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1;;c\<^isub>2 {P\<^isub>3}"  |
    2.32 +
    2.33 +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>
    2.34 +  \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}"  |
    2.35 +
    2.36 +While:
    2.37 +  "(\<And>n::nat.
    2.38 +    \<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)})
    2.39 +   \<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}"  |
    2.40 +
    2.41 +conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
    2.42 +           \<turnstile>\<^sub>t {P'}c{Q'}"
    2.43 +
    2.44 +text{* The @{term While}-rule is like the one for partial correctness but it
    2.45 +requires additionally that with every execution of the loop body some measure
    2.46 +relation @{term[source]"T :: state \<Rightarrow> nat \<Rightarrow> bool"} decreases.
    2.47 +The following functional version is more intuitive: *}
    2.48 +
    2.49 +lemma While_fun:
    2.50 +  "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> n = f s} c {\<lambda>s. P s \<and> f s < n}\<rbrakk>
    2.51 +   \<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}"
    2.52 +  by (rule While [where T="\<lambda>s n. n = f s", simplified])
    2.53 +
    2.54 +text{* Building in the consequence rule: *}
    2.55 +
    2.56 +lemma strengthen_pre:
    2.57 +  "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
    2.58 +by (metis conseq)
    2.59 +
    2.60 +lemma weaken_post:
    2.61 +  "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
    2.62 +by (metis conseq)
    2.63 +
    2.64 +lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
    2.65 +by (simp add: strengthen_pre[OF _ Assign])
    2.66 +
    2.67 +lemma While_fun':
    2.68 +assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> n = f s} c {\<lambda>s. P s \<and> f s < n}"
    2.69 +    and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
    2.70 +shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}"
    2.71 +by(blast intro: assms(1) weaken_post[OF While_fun assms(2)])
    2.72 +
    2.73 +
    2.74 +text{* Our standard example: *}
    2.75 +
    2.76 +lemma "\<turnstile>\<^sub>t {\<lambda>s. s ''x'' = i} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum i}"
    2.77 +apply(rule Seq)
    2.78 + prefer 2
    2.79 + apply(rule While_fun' [where P = "\<lambda>s. (s ''y'' = sum i - sum(s ''x''))"
    2.80 +    and f = "\<lambda>s. nat(s ''x'')"])
    2.81 +   apply(rule Seq)
    2.82 +   prefer 2
    2.83 +   apply(rule Assign)
    2.84 +  apply(rule Assign')
    2.85 +  apply simp
    2.86 +  apply(simp add: minus_numeral_simps(1)[symmetric] del: minus_numeral_simps)
    2.87 + apply(simp)
    2.88 +apply(rule Assign')
    2.89 +apply simp
    2.90 +done
    2.91 +
    2.92 +
    2.93 +text{* The soundness theorem: *}
    2.94 +
    2.95 +theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
    2.96 +proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
    2.97 +  case (While P b T c)
    2.98 +  {
    2.99 +    fix s n
   2.100 +    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"
   2.101 +    proof(induction "n" arbitrary: s rule: less_induct)
   2.102 +      case (less n)
   2.103 +      thus ?case by (metis While.IH WhileFalse WhileTrue)
   2.104 +    qed
   2.105 +  }
   2.106 +  thus ?case by auto
   2.107 +next
   2.108 +  case If thus ?case by auto blast
   2.109 +qed fastforce+
   2.110 +
   2.111 +
   2.112 +text{*
   2.113 +The completeness proof proceeds along the same lines as the one for partial
   2.114 +correctness. First we have to strengthen our notion of weakest precondition
   2.115 +to take termination into account: *}
   2.116 +
   2.117 +definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where
   2.118 +"wp\<^sub>t c Q  \<equiv>  \<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t"
   2.119 +
   2.120 +lemma [simp]: "wp\<^sub>t SKIP Q = Q"
   2.121 +by(auto intro!: ext simp: wpt_def)
   2.122 +
   2.123 +lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
   2.124 +by(auto intro!: ext simp: wpt_def)
   2.125 +
   2.126 +lemma [simp]: "wp\<^sub>t (c\<^isub>1;;c\<^isub>2) Q = wp\<^sub>t c\<^isub>1 (wp\<^sub>t c\<^isub>2 Q)"
   2.127 +unfolding wpt_def
   2.128 +apply(rule ext)
   2.129 +apply auto
   2.130 +done
   2.131 +
   2.132 +lemma [simp]:
   2.133 + "wp\<^sub>t (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^isub>1 else c\<^isub>2) Q s)"
   2.134 +apply(unfold wpt_def)
   2.135 +apply(rule ext)
   2.136 +apply auto
   2.137 +done
   2.138 +
   2.139 +
   2.140 +text{* Now we define the number of iterations @{term "WHILE b DO c"} needs to
   2.141 +terminate when started in state @{text s}. Because this is a truly partial
   2.142 +function, we define it as an (inductive) relation first: *}
   2.143 +
   2.144 +inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where
   2.145 +Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0" |
   2.146 +Its_Suc: "\<lbrakk> bval b s;  (c,s) \<Rightarrow> s';  Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)"
   2.147 +
   2.148 +text{* The relation is in fact a function: *}
   2.149 +
   2.150 +lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
   2.151 +proof(induction arbitrary: n' rule:Its.induct)
   2.152 +  case Its_0 thus ?case by(metis Its.cases)
   2.153 +next
   2.154 +  case Its_Suc thus ?case by(metis Its.cases big_step_determ)
   2.155 +qed
   2.156 +
   2.157 +text{* For all terminating loops, @{const Its} yields a result: *}
   2.158 +
   2.159 +lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"
   2.160 +proof(induction "WHILE b DO c" s t rule: big_step_induct)
   2.161 +  case WhileFalse thus ?case by (metis Its_0)
   2.162 +next
   2.163 +  case WhileTrue thus ?case by (metis Its_Suc)
   2.164 +qed
   2.165 +
   2.166 +lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
   2.167 +proof (induction c arbitrary: Q)
   2.168 +  case SKIP show ?case by simp (blast intro:hoaret.Skip)
   2.169 +next
   2.170 +  case Assign show ?case by simp (blast intro:hoaret.Assign)
   2.171 +next
   2.172 +  case Seq thus ?case by simp (blast intro:hoaret.Seq)
   2.173 +next
   2.174 +  case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq)
   2.175 +next
   2.176 +  case (While b c)
   2.177 +  let ?w = "WHILE b DO c"
   2.178 +  let ?T = "Its b c"
   2.179 +  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)"
   2.180 +    unfolding wpt_def by (metis WHILE_Its)
   2.181 +  moreover
   2.182 +  { fix n
   2.183 +    { fix s t
   2.184 +      assume "bval b s" "?T s n" "(?w, s) \<Rightarrow> t" "Q t"
   2.185 +      from `bval b s` `(?w, s) \<Rightarrow> t` obtain s' where
   2.186 +        "(c,s) \<Rightarrow> s'" "(?w,s') \<Rightarrow> t" by auto      
   2.187 +      from `(?w, s') \<Rightarrow> t` obtain n'' where "?T s' n''" by (blast dest: WHILE_Its)
   2.188 +      with `bval b s` `(c, s) \<Rightarrow> s'`
   2.189 +      have "?T s (Suc n'')" by (rule Its_Suc)
   2.190 +      with `?T s n` have "n = Suc n''" by (rule Its_fun)
   2.191 +      with `(c,s) \<Rightarrow> s'` `(?w,s') \<Rightarrow> t` `Q t` `?T s' n''`
   2.192 +      have "wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T s' n' \<and> n' < n)) s"
   2.193 +        by (auto simp: wpt_def)
   2.194 +    } 
   2.195 +    hence "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow>
   2.196 +              wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T s' n' \<and> n' < n)) s"
   2.197 +      unfolding wpt_def by auto
   2.198 +      (* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *) 
   2.199 +    note strengthen_pre[OF this While]
   2.200 +  } note hoaret.While[OF this]
   2.201 +  moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by (auto simp add:wpt_def)
   2.202 +  ultimately show ?case by (rule conseq) 
   2.203 +qed
   2.204 +
   2.205 +
   2.206 +text{*\noindent In the @{term While}-case, @{const Its} provides the obvious
   2.207 +termination argument.
   2.208 +
   2.209 +The actual completeness theorem follows directly, in the same manner
   2.210 +as for partial correctness: *}
   2.211 +
   2.212 +theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
   2.213 +apply(rule strengthen_pre[OF _ wpt_is_pre])
   2.214 +apply(auto simp: hoare_tvalid_def hoare_valid_def wpt_def)
   2.215 +done
   2.216 +
   2.217 +end
     3.1 --- a/src/HOL/ROOT	Sat Jun 01 11:48:06 2013 +0200
     3.2 +++ b/src/HOL/ROOT	Sat Jun 01 12:02:41 2013 +0200
     3.3 @@ -130,7 +130,7 @@
     3.4      Live_True
     3.5      Hoare_Examples
     3.6      VCG
     3.7 -    HoareT
     3.8 +    Hoare_Total
     3.9      Collecting1
    3.10      Collecting_Examples
    3.11      Abs_Int_Tests