# HG changeset patch
# User nipkow
# Date 1469273144 -7200
# Node ID d7b5e2a222c2ebd8e7e3f0e93a6e18c9e2fb0cda
# Parent  831816778409a26b256aaab2abdd947efda85049
added new vcg based on existentially quantified while-rule

diff -r 831816778409 -r d7b5e2a222c2 src/HOL/IMP/Hoare_Sound_Complete.thy
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Fri Jul 22 17:35:54 2016 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Sat Jul 23 13:25:44 2016 +0200
@@ -1,8 +1,12 @@
 (* Author: Tobias Nipkow *)
 
-theory Hoare_Sound_Complete imports Hoare begin
+subsection \<open>Soundness and Completeness\<close>
 
-subsection "Soundness"
+theory Hoare_Sound_Complete
+imports Hoare
+begin
+
+subsubsection "Soundness"
 
 lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
 proof(induction rule: hoare.induct)
@@ -20,7 +24,7 @@
 qed (auto simp: hoare_valid_def)
 
 
-subsection "Weakest Precondition"
+subsubsection "Weakest Precondition"
 
 definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where
 "wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t  \<longrightarrow>  Q t)"
@@ -52,7 +56,7 @@
 by(simp add: wp_While_If)
 
 
-subsection "Completeness"
+subsubsection "Completeness"
 
 lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
 proof(induction c arbitrary: Q)
diff -r 831816778409 -r d7b5e2a222c2 src/HOL/IMP/Hoare_Total.thy
--- a/src/HOL/IMP/Hoare_Total.thy	Fri Jul 22 17:35:54 2016 +0200
+++ b/src/HOL/IMP/Hoare_Total.thy	Sat Jul 23 13:25:44 2016 +0200
@@ -1,8 +1,12 @@
 (* Author: Tobias Nipkow *)
 
-theory Hoare_Total imports Hoare_Sound_Complete Hoare_Examples begin
+subsection "Hoare Logic for Total Correctness"
 
-subsection "Hoare Logic for Total Correctness"
+theory Hoare_Total
+imports Hoare_Examples
+begin
+
+subsubsection "Hoare Logic for Total Correctness --- Separate Termination Relation"
 
 text{* Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only
 works if execution is deterministic (which it is in our case). *}
diff -r 831816778409 -r d7b5e2a222c2 src/HOL/IMP/Hoare_Total_EX.thy
--- a/src/HOL/IMP/Hoare_Total_EX.thy	Fri Jul 22 17:35:54 2016 +0200
+++ b/src/HOL/IMP/Hoare_Total_EX.thy	Sat Jul 23 13:25:44 2016 +0200
@@ -1,8 +1,10 @@
 (* Author: Tobias Nipkow *)
 
-theory Hoare_Total_EX imports Hoare_Sound_Complete Hoare_Examples begin
+theory Hoare_Total_EX
+imports Hoare
+begin
 
-subsection "Hoare Logic for Total Correctness"
+subsubsection "Hoare Logic for Total Correctness --- \<open>nat\<close>-Indexed Invariant"
 
 text{* This is the standard set of rules that you find in many publications.
 The While-rule is different from the one in Concrete Semantics in that the
diff -r 831816778409 -r d7b5e2a222c2 src/HOL/IMP/VCG_Total_EX.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/VCG_Total_EX.thy	Sat Jul 23 13:25:44 2016 +0200
@@ -0,0 +1,71 @@
+(* Author: Tobias Nipkow *)
+
+theory VCG_Total_EX
+imports "~~/src/HOL/IMP/Hoare_Total_EX"
+begin
+
+subsection "Verification Conditions for Total Correctness"
+
+text{* Annotated commands: commands where loops are annotated with
+invariants. *}
+
+datatype acom =
+  Askip                  ("SKIP") |
+  Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
+  Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |
+  Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
+  Awhile "nat \<Rightarrow> assn" bexp acom
+    ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)
+
+notation com.SKIP ("SKIP")
+
+text{* Strip annotations: *}
+
+fun strip :: "acom \<Rightarrow> com" where
+"strip SKIP = SKIP" |
+"strip (x ::= a) = (x ::= a)" |
+"strip (C\<^sub>1;; C\<^sub>2) = (strip C\<^sub>1;; strip C\<^sub>2)" |
+"strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" |
+"strip ({_} WHILE b DO C) = (WHILE b DO strip C)"
+
+text{* Weakest precondition from annotated commands: *}
+
+fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
+"pre SKIP Q = Q" |
+"pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
+"pre (C\<^sub>1;; C\<^sub>2) Q = pre C\<^sub>1 (pre C\<^sub>2 Q)" |
+"pre (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q =
+  (\<lambda>s. if bval b s then pre C\<^sub>1 Q s else pre C\<^sub>2 Q s)" |
+"pre ({I} WHILE b DO C) Q = (\<lambda>s. EX n. I n s)"
+
+text{* Verification condition: *}
+
+fun vc :: "acom \<Rightarrow> assn \<Rightarrow> bool" where
+"vc SKIP Q = True" |
+"vc (x ::= a) Q = True" |
+"vc (C\<^sub>1;; C\<^sub>2) Q = (vc C\<^sub>1 (pre C\<^sub>2 Q) \<and> vc C\<^sub>2 Q)" |
+"vc (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = (vc C\<^sub>1 Q \<and> vc C\<^sub>2 Q)" |
+"vc ({I} WHILE b DO C) Q =
+  (\<forall>s n. (I (Suc n) s \<longrightarrow> pre C (I n) s) \<and>
+       (I (Suc n) s \<longrightarrow> bval b s) \<and>
+       (I 0 s \<longrightarrow> \<not> bval b s \<and> Q s) \<and>
+       vc C (I n))"
+
+lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C Q} strip C {Q}"
+proof(induction C arbitrary: Q)
+  case (Awhile I b C)
+  show ?case
+  proof(simp, rule conseq[OF _ While[of I]], goal_cases)
+    case (2 n) show ?case
+      using Awhile.IH[of "I n"] Awhile.prems
+      by (auto intro: strengthen_pre)
+  qed (insert Awhile.prems, auto)
+qed (auto intro: conseq Seq If simp: Skip Assign)
+
+text\<open>When trying to extend the completeness proof of the VCG for partial correctness
+to total correctness one runs into the following problem.
+In the case of the while-rule, the universally quantified \<open>n\<close> in the first premise
+means that for that premise the induction hypothesis does not yield a single
+annotated command \<open>C\<close> but merely that for every \<open>n\<close> such a \<open>C\<close> exists.\<close>
+
+end
diff -r 831816778409 -r d7b5e2a222c2 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Jul 22 17:35:54 2016 +0200
+++ b/src/HOL/ROOT	Sat Jul 23 13:25:44 2016 +0200
@@ -137,9 +137,10 @@
     Live
     Live_True
     Hoare_Examples
+    Hoare_Sound_Complete
     VCG
     Hoare_Total
-    Hoare_Total_EX
+    VCG_Total_EX
     Collecting1
     Collecting_Examples
     Abs_Int_Tests