--- a/src/HOL/IMP/HoareT.thy Fri Dec 07 15:53:28 2012 +0100
+++ b/src/HOL/IMP/HoareT.thy Fri Dec 07 16:38:25 2012 +0100
@@ -1,7 +1,9 @@
-header{* Hoare Logic for Total Correctness *}
+(* Author: Tobias Nipkow *)
theory HoareT imports Hoare_Sound_Complete begin
+subsection "Hoare Logic for Total Correctness"
+
text{* Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only
works if execution is deterministic (which it is in our case). *}
--- a/src/HOL/IMP/VC.thy Fri Dec 07 15:53:28 2012 +0100
+++ b/src/HOL/IMP/VC.thy Fri Dec 07 16:38:25 2012 +0100
@@ -1,8 +1,8 @@
-header "Verification Conditions"
+(* Author: Tobias Nipkow *)
theory VC imports Hoare begin
-subsection "VCG via Weakest Preconditions"
+subsection "Verification Conditions"
text{* Annotated commands: commands where loops are annotated with
invariants. *}
@@ -46,7 +46,7 @@
"strip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)" |
"strip (Awhile I b c) = (WHILE b DO strip c)"
-subsection "Soundness"
+text {* Soundness: *}
lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} strip c {Q}"
proof(induction c arbitrary: Q)
@@ -68,7 +68,7 @@
by (metis strengthen_pre vc_sound)
-subsection "Completeness"
+text{* Completeness: *}
lemma pre_mono:
"\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
@@ -122,7 +122,7 @@
qed
-subsection "An Optimization"
+text{* An Optimization: *}
fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
"vcpre ASKIP Q = (\<lambda>s. True, Q)" |