# HG changeset patch
# User nipkow
# Date 1510062747 -3600
# Node ID 7a37240783630ced78d1fda1d043e11107ee08d3
# Parent  f6aa133f9b16e30260618af9b78490b02ecd8d6f
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.

diff -r f6aa133f9b16 -r 7a3724078363 src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy	Tue Nov 07 14:52:27 2017 +0100
@@ -187,21 +187,19 @@
 shows "P p \<and> f p \<le> p"
 proof-
   let ?Q = "%p. P p \<and> f p \<le> p \<and> p \<le> p0"
-  { fix p assume "?Q p"
-    note P = conjunct1[OF this] and 12 = conjunct2[OF this]
+  have "?Q (p \<triangle> f p)" if Q: "?Q p" for p
+  proof auto
+    note P = conjunct1[OF Q] and 12 = conjunct2[OF Q]
     note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
     let ?p' = "p \<triangle> f p"
-    have "?Q ?p'"
-    proof auto
-      show "P ?p'" by (blast intro: P Pinv)
-      have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2_acom[OF 1]])
-      also have "\<dots> \<le> ?p'" by(rule narrow1_acom[OF 1])
-      finally show "f ?p' \<le> ?p'" .
-      have "?p' \<le> p" by (rule narrow2_acom[OF 1])
-      also have "p \<le> p0" by(rule 2)
-      finally show "?p' \<le> p0" .
-    qed
-  }
+    show "P ?p'" by (blast intro: P Pinv)
+    have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2_acom[OF 1]])
+    also have "\<dots> \<le> ?p'" by(rule narrow1_acom[OF 1])
+    finally show "f ?p' \<le> ?p'" .
+    have "?p' \<le> p" by (rule narrow2_acom[OF 1])
+    also have "p \<le> p0" by(rule 2)
+    finally show "?p' \<le> p0" .
+  qed
   thus ?thesis
     using while_option_rule[where P = ?Q, OF _ assms(6)[simplified iter_narrow_def]]
     by (blast intro: assms(4,5) le_refl)
diff -r f6aa133f9b16 -r 7a3724078363 src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/HOL/IMP/Big_Step.thy	Tue Nov 07 14:52:27 2017 +0100
@@ -178,8 +178,9 @@
 proof -
   -- "to show the equivalence, we look at the derivation tree for"
   -- "each side and from that construct a derivation tree for the other side"
-  { fix s t assume "(?w, s) \<Rightarrow> t"
-    hence  "(?iw, s) \<Rightarrow> t"
+  have "(?iw, s) \<Rightarrow> t" if assm: "(?w, s) \<Rightarrow> t" for s t
+  proof -
+    from assm show ?thesis
     proof cases --"rule inversion on \<open>(?w, s) \<Rightarrow> t\<close>"
       case WhileFalse
       thus ?thesis by blast
@@ -193,11 +194,12 @@
       -- "then the whole @{text IF}"
       with `bval b s` show ?thesis by (rule IfTrue)
     qed
-  }
+  qed
   moreover
   -- "now the other direction:"
-  { fix s t assume "(?iw, s) \<Rightarrow> t"
-    hence "(?w, s) \<Rightarrow> t"
+  have "(?w, s) \<Rightarrow> t" if assm: "(?iw, s) \<Rightarrow> t" for s t
+  proof -
+    from assm show ?thesis
     proof cases --"rule inversion on \<open>(?iw, s) \<Rightarrow> t\<close>"
       case IfFalse
       hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast
@@ -212,7 +214,7 @@
       with `bval b s`
       show ?thesis by (rule WhileTrue)
     qed
-  }
+  qed
   ultimately
   show ?thesis by blast
 qed
diff -r f6aa133f9b16 -r 7a3724078363 src/HOL/IMP/Compiler2.thy
--- a/src/HOL/IMP/Compiler2.thy	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/HOL/IMP/Compiler2.thy	Tue Nov 07 14:52:27 2017 +0100
@@ -108,10 +108,11 @@
   "succs (x#xs) n = isuccs x n \<union> succs xs (1+n)" (is "_ = ?x \<union> ?xs")
 proof 
   let ?isuccs = "\<lambda>p P n i::int. 0 \<le> i \<and> i < size P \<and> p \<in> isuccs (P!!i) (n+i)"
-  { fix p assume "p \<in> succs (x#xs) n"
-    then obtain i::int where isuccs: "?isuccs p (x#xs) n i"
+  have "p \<in> ?x \<union> ?xs" if assm: "p \<in> succs (x#xs) n" for p
+  proof -
+    from assm obtain i::int where isuccs: "?isuccs p (x#xs) n i"
       unfolding succs_def by auto     
-    have "p \<in> ?x \<union> ?xs" 
+    show ?thesis
     proof cases
       assume "i = 0" with isuccs show ?thesis by simp
     next
@@ -121,11 +122,12 @@
       hence "p \<in> ?xs" unfolding succs_def by blast
       thus ?thesis .. 
     qed
-  } 
+  qed
   thus "succs (x#xs) n \<subseteq> ?x \<union> ?xs" ..
-  
-  { fix p assume "p \<in> ?x \<or> p \<in> ?xs"
-    hence "p \<in> succs (x#xs) n"
+
+  have "p \<in> succs (x#xs) n" if assm: "p \<in> ?x \<or> p \<in> ?xs" for p
+  proof -
+    from assm show ?thesis
     proof
       assume "p \<in> ?x" thus ?thesis by (fastforce simp: succs_def)
     next
@@ -136,7 +138,7 @@
         by (simp add: algebra_simps)
       thus ?thesis unfolding succs_def by blast
     qed
-  }  
+  qed
   thus "?x \<union> ?xs \<subseteq> succs (x#xs) n" by blast
 qed
 
@@ -300,20 +302,19 @@
 
   note split_paired_Ex [simp del]
 
-  { assume "j0 \<in> {0 ..< size c}"
-    with j0 j rest c
-    have ?case
+  have ?case if assm: "j0 \<in> {0 ..< size c}"
+  proof -
+    from assm j0 j rest c show ?case
       by (fastforce dest!: Suc.IH intro!: exec_Suc)
-  } moreover {
-    assume "j0 \<notin> {0 ..< size c}"
-    moreover
+  qed
+  moreover
+  have ?case if assm: "j0 \<notin> {0 ..< size c}"
+  proof -
     from c j0 have "j0 \<in> succs c 0"
       by (auto dest: succs_iexec1 simp: exec1_def simp del: iexec.simps)
-    ultimately
-    have "j0 \<in> exits c" by (simp add: exits_def)
-    with c j0 rest
-    have ?case by fastforce
-  }
+    with assm have "j0 \<in> exits c" by (simp add: exits_def)
+    with c j0 rest show ?case by fastforce
+  qed
   ultimately
   show ?case by cases
 qed
@@ -560,14 +561,16 @@
   show ?case
   proof (induction n arbitrary: s rule: nat_less_induct)
     case (1 n)
-    
-    { assume "\<not> bval b s"
-      with "1.prems"
-      have ?case
-        by simp
-           (fastforce dest!: bcomp_exec_n bcomp_split simp: exec_n_simps)
-    } moreover {
-      assume b: "bval b s"
+
+    have ?case if assm: "\<not> bval b s"
+    proof -
+      from assm "1.prems"
+      show ?case
+        by simp (fastforce dest!: bcomp_split simp: exec_n_simps)
+    qed
+    moreover
+    have ?case if b: "bval b s"
+    proof -
       let ?c0 = "WHILE b DO c"
       let ?cs = "ccomp ?c0"
       let ?bs = "bcomp b False (size (ccomp c) + 1)"
@@ -579,7 +582,7 @@
         k:  "k \<le> n"
         by (fastforce dest!: bcomp_split)
       
-      have ?case
+      show ?case
       proof cases
         assume "ccomp c = []"
         with cs k
@@ -612,7 +615,7 @@
         ultimately
         show ?case using b by blast
       qed
-    }
+    qed
     ultimately show ?case by cases
   qed
 qed
diff -r f6aa133f9b16 -r 7a3724078363 src/HOL/IMP/Denotational.thy
--- a/src/HOL/IMP/Denotational.thy	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/HOL/IMP/Denotational.thy	Tue Nov 07 14:52:27 2017 +0100
@@ -90,9 +90,13 @@
 lemma chain_iterates: fixes f :: "'a set \<Rightarrow> 'a set"
   assumes "mono f" shows "chain(\<lambda>n. (f^^n) {})"
 proof-
-  { fix n have "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" using assms
-    by(induction n) (auto simp: mono_def) }
-  thus ?thesis by(auto simp: chain_def)
+  have "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" for n
+  proof (induction n)
+    case 0 show ?case by simp
+  next
+    case (Suc n) thus ?case using assms by (auto simp: mono_def)
+  qed
+  thus ?thesis by(auto simp: chain_def assms)
 qed
 
 theorem lfp_if_cont:
@@ -112,8 +116,9 @@
     finally show "f ?U \<subseteq> ?U" by simp
   qed
 next
-  { fix n p assume "f p \<subseteq> p"
-    have "(f^^n){} \<subseteq> p"
+  have "(f^^n){} \<subseteq> p" if "f p \<subseteq> p" for n p
+  proof -
+    show ?thesis
     proof(induction n)
       case 0 show ?case by simp
     next
@@ -121,7 +126,7 @@
       from monoD[OF mono_if_cont[OF assms] Suc] `f p \<subseteq> p`
       show ?case by simp
     qed
-  }
+  qed
   thus "?U \<subseteq> lfp f" by(auto simp: lfp_def)
 qed
 
diff -r f6aa133f9b16 -r 7a3724078363 src/HOL/IMP/Hoare_Sound_Complete.thy
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue Nov 07 14:52:27 2017 +0100
@@ -11,15 +11,13 @@
 lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
 proof(induction rule: hoare.induct)
   case (While P b c)
-  { fix s t
-    have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s  \<Longrightarrow>  P t \<and> \<not> bval b t"
-    proof(induction "WHILE b DO c" s t rule: big_step_induct)
-      case WhileFalse thus ?case by blast
-    next
-      case WhileTrue thus ?case
-        using While.IH unfolding hoare_valid_def by blast
-    qed
-  }
+  have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s  \<Longrightarrow>  P t \<and> \<not> bval b t" for s t
+  proof(induction "WHILE b DO c" s t rule: big_step_induct)
+    case WhileFalse thus ?case by blast
+  next
+    case WhileTrue thus ?case
+      using While.IH unfolding hoare_valid_def by blast
+  qed
   thus ?case unfolding hoare_valid_def by blast
 qed (auto simp: hoare_valid_def)
 
diff -r f6aa133f9b16 -r 7a3724078363 src/HOL/IMP/Hoare_Total.thy
--- a/src/HOL/IMP/Hoare_Total.thy	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/HOL/IMP/Hoare_Total.thy	Tue Nov 07 14:52:27 2017 +0100
@@ -95,14 +95,10 @@
 theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
 proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
   case (While P b T c)
-  {
-    fix s n
-    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.IH WhileFalse WhileTrue)
-    qed
-  }
+  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" for s n
+  proof(induction "n" arbitrary: s rule: less_induct)
+    case (less n) thus ?case by (metis While.IH WhileFalse WhileTrue)
+  qed
   thus ?case by auto
 next
   case If thus ?case by auto blast
@@ -176,12 +172,13 @@
   case (While b c)
   let ?w = "WHILE b DO c"
   let ?T = "Its b c"
-  have "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> wp\<^sub>t ?w Q s \<and> (\<exists>n. Its b c s n)"
+  have 1: "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> wp\<^sub>t ?w Q s \<and> (\<exists>n. Its b c s n)"
     unfolding wpt_def by (metis WHILE_Its)
-  moreover
-  { fix n
-    let ?R = "\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'<n. ?T s' n')"
-    { fix s t assume "bval b s" and "?T s n" and "(?w, s) \<Rightarrow> t" and "Q t"
+  let ?R = "\<lambda>n s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'<n. ?T s' n')"
+  have "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow> wp\<^sub>t c (?R n) s" for n
+  proof -
+    have "wp\<^sub>t c (?R n) s" if "bval b s" and "?T s n" and "(?w, s) \<Rightarrow> t" and "Q t" for s t
+    proof -
       from `bval b s` and `(?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 s' n'"
@@ -189,16 +186,16 @@
       with `bval b s` and `(c, s) \<Rightarrow> 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'` and `(?w,s') \<Rightarrow> t` and `Q t` and `?T s' n'`
-      have "wp\<^sub>t c ?R s" by (auto simp: wpt_def)
-    }
-    hence "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow> wp\<^sub>t c ?R s"
+      show ?thesis by (auto simp: wpt_def)
+    qed
+    thus ?thesis
       unfolding wpt_def by auto
       (* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *) 
-    note strengthen_pre[OF this While.IH]
-  } note hoaret.While[OF this]
-  moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s"
+  qed
+  note 2 = hoaret.While[OF strengthen_pre[OF this While.IH]]
+  have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s"
     by (auto simp add:wpt_def)
-  ultimately show ?case by (rule conseq)
+  with 1 2 show ?case by (rule conseq)
 qed
 
 
diff -r f6aa133f9b16 -r 7a3724078363 src/HOL/IMP/Hoare_Total_EX.thy
--- a/src/HOL/IMP/Hoare_Total_EX.thy	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/HOL/IMP/Hoare_Total_EX.thy	Tue Nov 07 14:52:27 2017 +0100
@@ -55,16 +55,13 @@
 theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
 proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
   case (While P c b)
-  {
-    fix n s
-    have "\<lbrakk> P n s \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P 0 t"
-    proof(induction "n" arbitrary: s)
-      case 0 thus ?case using While.hyps(3) WhileFalse by blast
-    next
-      case (Suc n)
-      thus ?case by (meson While.IH While.hyps(2) WhileTrue)
-    qed
-  }
+  have "P n s \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P 0 t" for n s
+  proof(induction "n" arbitrary: s)
+    case 0 thus ?case using While.hyps(3) WhileFalse by blast
+  next
+    case Suc
+    thus ?case by (meson While.IH While.hyps(2) WhileTrue)
+  qed
   thus ?case by auto
 next
   case If thus ?case by auto blast
@@ -125,11 +122,11 @@
   have c3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> Q s" by simp
   have w2: "\<forall>n s. wpw b c (Suc n) Q s \<longrightarrow> bval b s" by simp
   have w3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> \<not> bval b s" by simp
-  { fix n
-    have 1: "\<forall>s. wpw b c (Suc n) Q s \<longrightarrow> (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c n Q t)"
-      by simp
-    note strengthen_pre[OF 1 While.IH[of "wpw b c n Q", unfolded wpt_def]]
-  }
+  have "\<turnstile>\<^sub>t {wpw b c (Suc n) Q} c {wpw b c n Q}" for n
+  proof -
+    have *: "\<forall>s. wpw b c (Suc n) Q s \<longrightarrow> (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c n Q t)" by simp
+    show ?thesis by(rule strengthen_pre[OF * While.IH[of "wpw b c n Q", unfolded wpt_def]])
+  qed
   from conseq[OF c1 hoaret.While[OF this w2 w3] c3]
   show ?case .
 qed
diff -r f6aa133f9b16 -r 7a3724078363 src/HOL/IMP/Hoare_Total_EX2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Hoare_Total_EX2.thy	Tue Nov 07 14:52:27 2017 +0100
@@ -0,0 +1,193 @@
+(* Author: Tobias Nipkow *)
+
+theory Hoare_Total_EX2
+imports Hoare
+begin
+
+subsubsection "Hoare Logic for Total Correctness --- With Logical Variables"
+
+text{* This is the standard set of rules that you find in many publications.
+In the while-rule, a logical variable is needed to remember the pre-value
+of the variant (an expression that decreases by one with each iteration).
+In this theory, logical variables are modeled explicitly.
+A simpler (but not quite as flexible) approach is found in theory \<open>Hoare_Total_EX\<close>:
+pre and post-condition are connected via a universally quantified HOL variable. *}
+
+type_synonym lvname = string
+type_synonym assn2 = "(lvname \<Rightarrow> nat) \<Rightarrow> state \<Rightarrow> bool"
+
+definition hoare_tvalid :: "assn2 \<Rightarrow> com \<Rightarrow> assn2 \<Rightarrow> bool"
+  ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
+"\<Turnstile>\<^sub>t {P}c{Q}  \<longleftrightarrow>  (\<forall>l s. P l s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q l t))"
+
+inductive
+  hoaret :: "assn2 \<Rightarrow> com \<Rightarrow> assn2 \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
+where
+
+Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}"  |
+
+Assign:  "\<turnstile>\<^sub>t {\<lambda>l s. P l (s[a/x])} x::=a {P}"  |
+
+Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \<turnstile>\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}" |
+
+If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>l s. P l s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>l s. P l s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
+  \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" |
+
+While:
+  "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>l. P (l(x := Suc(l(x))))} c {P};
+     \<forall>l s. l x > 0 \<and> P l s \<longrightarrow> bval b s;
+     \<forall>l s. l x = 0 \<and> P l s \<longrightarrow> \<not> bval b s \<rbrakk>
+   \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>l s. \<exists>n. P (l(x:=n)) s} WHILE b DO c {\<lambda>l s. P (l(x := 0)) s}" |
+
+conseq: "\<lbrakk> \<forall>l s. P' l s \<longrightarrow> P l s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>l s. Q l s \<longrightarrow> Q' l s  \<rbrakk> \<Longrightarrow>
+           \<turnstile>\<^sub>t {P'}c{Q'}"
+
+text{* Building in the consequence rule: *}
+
+lemma strengthen_pre:
+  "\<lbrakk> \<forall>l s. P' l s \<longrightarrow> P l s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
+by (metis conseq)
+
+lemma weaken_post:
+  "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>l s. Q l s \<longrightarrow> Q' l s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
+by (metis conseq)
+
+lemma Assign': "\<forall>l s. P l s \<longrightarrow> Q l (s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
+by (simp add: strengthen_pre[OF _ Assign])
+
+text{* The soundness theorem: *}
+
+theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
+proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
+  case (While P x c b)
+  have "\<lbrakk> l x = n; P l s \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P (l(x := 0)) t" for n l s
+  proof(induction "n" arbitrary: l s)
+    case 0 thus ?case using While.hyps(3) WhileFalse
+      by (metis fun_upd_triv)
+  next
+    case Suc
+    thus ?case using While.IH While.hyps(2) WhileTrue
+      by (metis fun_upd_same fun_upd_triv fun_upd_upd zero_less_Suc)
+  qed
+  thus ?case by fastforce
+next
+  case If thus ?case by auto blast
+qed fastforce+
+
+
+definition wpt :: "com \<Rightarrow> assn2 \<Rightarrow> assn2" ("wp\<^sub>t") where
+"wp\<^sub>t c Q  =  (\<lambda>l s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q l t)"
+
+lemma [simp]: "wp\<^sub>t SKIP Q = Q"
+by(auto intro!: ext simp: wpt_def)
+
+lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>l s. Q l (s(x := aval e s)))"
+by(auto intro!: ext simp: wpt_def)
+
+lemma wpt_Seq[simp]: "wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)"
+by (auto simp: wpt_def fun_eq_iff)
+
+lemma [simp]:
+ "wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\<lambda>l s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q l s)"
+by (auto simp: wpt_def fun_eq_iff)
+
+
+text{* Function @{text wpw} computes the weakest precondition of a While-loop
+that is unfolded a fixed number of times. *}
+
+fun wpw :: "bexp \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> assn2 \<Rightarrow> assn2" where
+"wpw b c 0 Q l s = (\<not> bval b s \<and> Q l s)" |
+"wpw b c (Suc n) Q l s = (bval b s \<and> (\<exists>s'. (c,s) \<Rightarrow> s' \<and>  wpw b c n Q l s'))"
+
+lemma WHILE_Its:
+  "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> Q l t \<Longrightarrow> \<exists>n. wpw b c n Q l s"
+proof(induction "WHILE b DO c" s t arbitrary: l rule: big_step_induct)
+  case WhileFalse thus ?case using wpw.simps(1) by blast
+next
+  case WhileTrue show ?case
+    using wpw.simps(2) WhileTrue(1,2) WhileTrue(5)[OF WhileTrue(6)] by blast
+qed
+
+definition support :: "assn2 \<Rightarrow> string set" where
+"support P = {x. \<exists>l1 l2 s. (\<forall>y. y \<noteq> x \<longrightarrow> l1 y = l2 y) \<and> P l1 s \<noteq> P l2 s}"
+
+lemma support_wpt: "support (wp\<^sub>t c Q) \<subseteq> support Q"
+by(simp add: support_def wpt_def) blast
+
+
+lemma support_wpw0: "support (wpw b c n Q) \<subseteq> support Q"
+proof(induction n)
+  case 0 show ?case by (simp add: support_def) blast
+next
+  case Suc
+  have 1: "support (\<lambda>l s. A s \<and> B l s) \<subseteq> support B" for A B
+    by(auto simp: support_def)
+  have 2: "support (\<lambda>l s. \<exists>s'. A s s' \<and> B l s') \<subseteq> support B" for A B
+    by(auto simp: support_def) blast+
+  from Suc 1 2 show ?case by simp (meson order_trans)
+qed
+
+lemma support_wpw_Un:
+  "support (%l. wpw b c (l x) Q l) \<subseteq> insert x (UN n. support(wpw b c n Q))"
+using support_wpw0[of b c _ Q]
+apply(auto simp add: support_def subset_iff)
+apply metis
+apply metis
+done
+
+lemma support_wpw: "support (%l. wpw b c (l x) Q l) \<subseteq> insert x (support Q)"
+using support_wpw0[of b c _ Q] support_wpw_Un[of b c _ Q]
+by blast
+
+lemma assn2_lupd: "x \<notin> support Q \<Longrightarrow> Q (l(x:=n)) = Q l"
+by(simp add: support_def fun_upd_other fun_eq_iff)
+  (metis (no_types, lifting) fun_upd_def)
+
+abbreviation "new Q \<equiv> SOME x. x \<notin> support Q"
+
+lemma wpw_lupd: "x \<notin> support Q \<Longrightarrow> wpw b c n Q (l(x := u)) = wpw b c n Q l"
+by(induction n) (auto simp: assn2_lupd fun_eq_iff)
+
+lemma wpt_is_pre: "finite(support Q) \<Longrightarrow> \<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
+proof (induction c arbitrary: Q)
+  case SKIP show ?case by (auto intro:hoaret.Skip)
+next
+  case Assign show ?case by (auto intro:hoaret.Assign)
+next
+  case (Seq c1 c2) show ?case
+    by (auto intro:hoaret.Seq Seq finite_subset[OF support_wpt])
+next
+  case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
+next
+  case (While b c)
+  let ?x = "new Q"
+  have "\<exists>x. x \<notin> support Q" using While.prems infinite_UNIV_listI
+    using ex_new_if_finite by blast
+  hence [simp]: "?x \<notin> support Q" by (rule someI_ex)
+  let ?w = "WHILE b DO c"
+  have fsup: "finite (support (\<lambda>l. wpw b c (l x) Q l))" for x
+    using finite_subset[OF support_wpw] While.prems by simp
+  have c1: "\<forall>l s. wp\<^sub>t ?w Q l s \<longrightarrow> (\<exists>n. wpw b c n Q l s)"
+    unfolding wpt_def by (metis WHILE_Its)
+  have c2: "\<forall>l s. l ?x = 0 \<and> wpw b c (l ?x) Q l s \<longrightarrow> \<not> bval b s"
+    by (simp cong: conj_cong)
+  have w2: "\<forall>l s. 0 < l ?x \<and> wpw b c (l ?x) Q l s \<longrightarrow> bval b s"
+    by (auto simp: gr0_conv_Suc cong: conj_cong)
+  have 1: "\<forall>l s. wpw b c (Suc(l ?x)) Q l s \<longrightarrow>
+                  (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c (l ?x) Q l t)"
+    by simp
+  have *: "\<turnstile>\<^sub>t {\<lambda>l. wpw b c (Suc (l ?x)) Q l} c {\<lambda>l. wpw b c (l ?x) Q l}"
+    by(rule strengthen_pre[OF 1
+          While.IH[of "\<lambda>l. wpw b c (l ?x) Q l", unfolded wpt_def, OF fsup]])
+  show ?case
+  apply(rule conseq[OF _ hoaret.While[OF _ w2 c2]])
+    apply (simp_all add: c1 * assn2_lupd wpw_lupd del: wpw.simps(2))
+  done
+qed
+
+theorem hoaret_complete: "finite(support Q) \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
+apply(rule strengthen_pre[OF _ wpt_is_pre])
+apply(auto simp: hoare_tvalid_def wpt_def)
+done
+
+end
diff -r f6aa133f9b16 -r 7a3724078363 src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/HOL/IMP/Live_True.thy	Tue Nov 07 14:52:27 2017 +0100
@@ -15,18 +15,18 @@
 
 lemma L_mono: "mono (L c)"
 proof-
-  { fix X Y have "X \<subseteq> Y \<Longrightarrow> L c X \<subseteq> L c Y"
-    proof(induction c arbitrary: X Y)
-      case (While b c)
-      show ?case
-      proof(simp, rule lfp_mono)
-        fix Z show "vars b \<union> X \<union> L c Z \<subseteq> vars b \<union> Y \<union> L c Z"
-          using While by auto
-      qed
-    next
-      case If thus ?case by(auto simp: subset_iff)
-    qed auto
-  } thus ?thesis by(rule monoI)
+  have "X \<subseteq> Y \<Longrightarrow> L c X \<subseteq> L c Y" for X Y
+  proof(induction c arbitrary: X Y)
+    case (While b c)
+    show ?case
+    proof(simp, rule lfp_mono)
+      fix Z show "vars b \<union> X \<union> L c Z \<subseteq> vars b \<union> Y \<union> L c Z"
+        using While by auto
+    qed
+  next
+    case If thus ?case by(auto simp: subset_iff)
+  qed auto
+  thus ?thesis by(rule monoI)
 qed
 
 lemma mono_union_L:
diff -r f6aa133f9b16 -r 7a3724078363 src/HOL/IMP/VCG_Total_EX.thy
--- a/src/HOL/IMP/VCG_Total_EX.thy	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/HOL/IMP/VCG_Total_EX.thy	Tue Nov 07 14:52:27 2017 +0100
@@ -1,7 +1,7 @@
 (* Author: Tobias Nipkow *)
 
 theory VCG_Total_EX
-imports "~~/src/HOL/IMP/Hoare_Total_EX"
+imports Hoare_Total_EX
 begin
 
 subsection "Verification Conditions for Total Correctness"
diff -r f6aa133f9b16 -r 7a3724078363 src/HOL/IMP/VCG_Total_EX2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/VCG_Total_EX2.thy	Tue Nov 07 14:52:27 2017 +0100
@@ -0,0 +1,134 @@
+(* Author: Tobias Nipkow *)
+
+theory VCG_Total_EX2
+imports Hoare_Total_EX2
+begin
+
+subsection "Verification Conditions for Total Correctness"
+
+text \<open>
+Theory \<open>VCG_Total_EX\<close> conatins a VCG built on top of a Hoare logic without logical variables.
+As a result the completeness proof runs into a problem. This theory uses a Hoare logic
+with logical variables and proves soundness and completeness.
+\<close>
+
+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 assn2 lvname bexp acom
+    ("({_'/_}/ WHILE _/ DO _)"  [0, 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> assn2 \<Rightarrow> assn2" where
+"pre SKIP Q = Q" |
+"pre (x ::= a) Q = (\<lambda>l s. Q l (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>l s. if bval b s then pre C\<^sub>1 Q l s else pre C\<^sub>2 Q l s)" |
+"pre ({I/x} WHILE b DO C) Q = (\<lambda>l s. EX n. I (l(x:=n)) s)"
+
+text{* Verification condition: *}
+
+fun vc :: "acom \<Rightarrow> assn2 \<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/x} WHILE b DO C) Q =
+  (\<forall>l s. (I (l(x:=Suc(l x))) s \<longrightarrow> pre C I l s) \<and>
+       (l x > 0 \<and> I l s \<longrightarrow> bval b s) \<and>
+       (I (l(x := 0)) s \<longrightarrow> \<not> bval b s \<and> Q l s) \<and>
+       vc C I)"
+
+lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C Q} strip C {Q}"
+proof(induction C arbitrary: Q)
+  case (Awhile I x b C)
+  show ?case
+  proof(simp, rule weaken_post[OF While[of I x]], goal_cases)
+    case 1 show ?case
+      using Awhile.IH[of "I"] Awhile.prems by (auto intro: strengthen_pre)
+  next
+    case 3 show ?case
+      using Awhile.prems by (simp) (metis fun_upd_triv)
+  qed (insert Awhile.prems, auto)
+qed (auto intro: conseq Seq If simp: Skip Assign)
+
+
+text{* Completeness: *}
+
+lemma pre_mono:
+  "\<forall>l s. P l s \<longrightarrow> P' l s \<Longrightarrow> pre C P l s \<Longrightarrow> pre C P' l s"
+proof (induction C arbitrary: P P' l s)
+  case Aseq thus ?case by simp metis
+qed simp_all
+
+lemma vc_mono:
+  "\<forall>l s. P l s \<longrightarrow> P' l s \<Longrightarrow> vc C P \<Longrightarrow> vc C P'"
+proof(induction C arbitrary: P P')
+  case Aseq thus ?case by simp (metis pre_mono)
+qed simp_all
+
+lemma vc_complete:
+ "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<exists>C. strip C = c \<and> vc C Q \<and> (\<forall>l s. P l s \<longrightarrow> pre C Q l s)"
+  (is "_ \<Longrightarrow> \<exists>C. ?G P c Q C")
+proof (induction rule: hoaret.induct)
+  case Skip
+  show ?case (is "\<exists>C. ?C C")
+  proof show "?C Askip" by simp qed
+next
+  case (Assign P a x)
+  show ?case (is "\<exists>C. ?C C")
+  proof show "?C(Aassign x a)" by simp qed
+next
+  case (Seq P c1 Q c2 R)
+  from Seq.IH obtain C1 where ih1: "?G P c1 Q C1" by blast
+  from Seq.IH obtain C2 where ih2: "?G Q c2 R C2" by blast
+  show ?case (is "\<exists>C. ?C C")
+  proof
+    show "?C(Aseq C1 C2)"
+      using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)
+  qed
+next
+  case (If P b c1 Q c2)
+  from If.IH obtain C1 where ih1: "?G (\<lambda>l s. P l s \<and> bval b s) c1 Q C1"
+    by blast
+  from If.IH obtain C2 where ih2: "?G (\<lambda>l s. P l s \<and> \<not>bval b s) c2 Q C2"
+    by blast
+  show ?case (is "\<exists>C. ?C C")
+  proof
+    show "?C(Aif b C1 C2)" using ih1 ih2 by simp
+  qed
+next
+  case (While P x c b)
+  from While.IH obtain C where
+    ih: "?G (\<lambda>l s. P (l(x:=Suc(l x))) s \<and> bval b s) c P C"
+    by blast
+  show ?case (is "\<exists>C. ?C C")
+  proof
+    have "vc ({P/x} WHILE b DO C) (\<lambda>l. P (l(x := 0)))"
+      using ih While.hyps(2,3)
+      by simp (metis fun_upd_same zero_less_Suc)
+    thus "?C(Awhile P x b C)" using ih by simp
+ qed
+next
+  case conseq thus ?case by(fast elim!: pre_mono vc_mono)
+qed
+
+end
diff -r f6aa133f9b16 -r 7a3724078363 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/HOL/ROOT	Tue Nov 07 14:52:27 2017 +0100
@@ -153,6 +153,7 @@
     VCG
     Hoare_Total
     VCG_Total_EX
+    VCG_Total_EX2
     Collecting1
     Collecting_Examples
     Abs_Int_Tests