diff --git a/src/HOL/Hoare/ExamplesTC.thy b/src/HOL/Hoare/ExamplesTC.thy
--- a/src/HOL/Hoare/ExamplesTC.thy
+++ b/src/HOL/Hoare/ExamplesTC.thy
@@ -1,116 +1,133 @@
 (* Title:      Examples using Hoare Logic for Total Correctness
    Author:     Walter Guttmann
 *)
 
 section \<open>Examples using Hoare Logic for Total Correctness\<close>
 
 theory ExamplesTC
   imports Hoare_Logic
 begin
 
 text \<open>
 This theory demonstrates a few simple partial- and total-correctness proofs.
 The first example is taken from HOL/Hoare/Examples.thy written by N. Galm.
 We have added the invariant \<open>m \<le> a\<close>.
 \<close>
 
 lemma multiply_by_add: "VARS m s a b
   {a=A \<and> b=B}
   m := 0; s := 0;
   WHILE m\<noteq>a
   INV {s=m*b \<and> a=A \<and> b=B \<and> m\<le>a}
   DO s := s+b; m := m+(1::nat) OD
   {s = A*B}"
   by vcg_simp
 
 text \<open>
 Here is the total-correctness proof for the same program.
 It needs the additional invariant \<open>m \<le> a\<close>.
 \<close>
-
+ML \<open>\<^const_syntax>\<open>HOL.eq\<close>\<close>
 lemma multiply_by_add_tc: "VARS m s a b
   [a=A \<and> b=B]
   m := 0; s := 0;
   WHILE m\<noteq>a
   INV {s=m*b \<and> a=A \<and> b=B \<and> m\<le>a}
   VAR {a-m}
   DO s := s+b; m := m+(1::nat) OD
   [s = A*B]"
   apply vcg_tc_simp
   by auto
 
 text \<open>
 Next, we prove partial correctness of a program that computes powers.
 \<close>
 
 lemma power: "VARS (p::int) i
   { True }
   p := 1;
   i := 0;
   WHILE i < n
     INV { p = x^i \<and> i \<le> n }
      DO p := p * x;
         i := i + 1
      OD
   { p = x^n }"
   apply vcg_simp
   by auto
 
 text \<open>
 Here is its total-correctness proof.
 \<close>
 
 lemma power_tc: "VARS (p::int) i
   [ True ]
   p := 1;
   i := 0;
   WHILE i < n
     INV { p = x^i \<and> i \<le> n }
     VAR { n - i }
      DO p := p * x;
         i := i + 1
      OD
   [ p = x^n ]"
   apply vcg_tc
   by auto
 
 text \<open>
 The last example is again taken from HOL/Hoare/Examples.thy.
 We have modified it to integers so it requires precondition \<open>0 \<le> x\<close>.
 \<close>
 
 lemma sqrt_tc: "VARS r
   [0 \<le> (x::int)]
   r := 0;
   WHILE (r+1)*(r+1) <= x
   INV {r*r \<le> x}
-  VAR {nat (x-r)}
+  VAR { nat (x-r)}
   DO r := r+1 OD
   [r*r \<le> x \<and> x < (r+1)*(r+1)]"
   apply vcg_tc_simp
   by (smt (verit) div_pos_pos_trivial mult_less_0_iff nonzero_mult_div_cancel_left)
 
 text \<open>
 A total-correctness proof allows us to extract a function for further use.
 For every input satisfying the precondition the function returns an output satisfying the postcondition.
 \<close>
 
 lemma sqrt_exists:
   "0 \<le> (x::int) \<Longrightarrow> \<exists>r' . r'*r' \<le> x \<and> x < (r'+1)*(r'+1)"
   using tc_extract_function sqrt_tc by blast
 
 definition "sqrt (x::int) \<equiv> (SOME r' . r'*r' \<le> x \<and> x < (r'+1)*(r'+1))"
 
 lemma sqrt_function:
   assumes "0 \<le> (x::int)"
     and "r' = sqrt x"
   shows "r'*r' \<le> x \<and> x < (r'+1)*(r'+1)"
 proof -
   let ?P = "\<lambda>r' . r'*r' \<le> x \<and> x < (r'+1)*(r'+1)"
   have "?P (SOME z . ?P z)"
     by (metis (mono_tags, lifting) assms(1) sqrt_exists some_eq_imp)
   thus ?thesis
     using assms(2) sqrt_def by auto
 qed
 
+text \<open>Nested loops!\<close>
+
+lemma "VARS (i::nat) j
+  [ True ]
+  WHILE 0 < i
+    INV { True }
+    VAR { z = i }
+     DO i := i - 1; j := i;
+        WHILE 0 < j
+        INV { z = i+1 }
+        VAR { j }
+        DO j := j - 1 OD
+     OD
+  [ i \<le> 0 ]"
+  apply vcg_tc
+  by auto
+
 end
diff --git a/src/HOL/Hoare/Hoare_Logic.thy b/src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy
+++ b/src/HOL/Hoare/Hoare_Logic.thy
@@ -1,218 +1,217 @@
 (*  Title:      HOL/Hoare/Hoare_Logic.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   1998 TUM
     Author:     Walter Guttmann (extension to total-correctness proofs)
 *)
 
 section \<open>Hoare logic\<close>
 
 theory Hoare_Logic
   imports Hoare_Syntax Hoare_Tac
 begin
 
 subsection \<open>Sugared semantic embedding of Hoare logic\<close>
 
 text \<open>
   Strictly speaking a shallow embedding (as implemented by Norbert Galm
   following Mike Gordon) would suffice. Maybe the datatype com comes in useful
   later.
 \<close>
 
 type_synonym 'a bexp = "'a set"
 type_synonym 'a assn = "'a set"
-type_synonym 'a var = "'a \<Rightarrow> nat"
 
 datatype 'a com =
   Basic "'a \<Rightarrow> 'a"
 | Seq "'a com" "'a com"
 | Cond "'a bexp" "'a com" "'a com"
-| While "'a bexp" "'a assn" "'a var" "'a com"
+| While "'a bexp" "'a com"
 
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 type_synonym 'a sem = "'a => 'a => bool"
 
 inductive Sem :: "'a com \<Rightarrow> 'a sem"
 where
   "Sem (Basic f) s (f s)"
 | "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (Seq c1 c2) s s'"
 | "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (Cond b c1 c2) s s'"
 | "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (Cond b c1 c2) s s'"
-| "s \<notin> b \<Longrightarrow> Sem (While b x y c) s s"
-| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow>
-   Sem (While b x y c) s s'"
+| "s \<notin> b \<Longrightarrow> Sem (While b c) s s"
+| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b c) s'' s' \<Longrightarrow>
+   Sem (While b c) s s'"
 
-definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
-  where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q"
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a anno \<Rightarrow> 'a bexp \<Rightarrow> bool"
+  where "Valid p c a q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q"
 
-definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
-  where "ValidTC p c q \<equiv> \<forall>s. s \<in> p \<longrightarrow> (\<exists>t. Sem c s t \<and> t \<in> q)"
+definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a anno \<Rightarrow> 'a bexp \<Rightarrow> bool"
+  where "ValidTC p c a q \<equiv> \<forall>s. s \<in> p \<longrightarrow> (\<exists>t. Sem c s t \<and> t \<in> q)"
 
 inductive_cases [elim!]:
   "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
   "Sem (Cond b c1 c2) s s'"
 
 lemma Sem_deterministic:
   assumes "Sem c s s1"
       and "Sem c s s2"
     shows "s1 = s2"
 proof -
   have "Sem c s s1 \<Longrightarrow> (\<forall>s2. Sem c s s2 \<longrightarrow> s1 = s2)"
     by (induct rule: Sem.induct) (subst Sem.simps, blast)+
   thus ?thesis
     using assms by simp
 qed
 
 lemma tc_implies_pc:
-  "ValidTC p c q \<Longrightarrow> Valid p c q"
+  "ValidTC p c a q \<Longrightarrow> Valid p c a q"
   by (metis Sem_deterministic Valid_def ValidTC_def)
 
 lemma tc_extract_function:
-  "ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
+  "ValidTC p c a q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
   by (metis ValidTC_def)
 
 
-lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
+lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) a q"
 by (auto simp:Valid_def)
 
-lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
+lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) a q"
 by (auto simp:Valid_def)
 
-lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (Seq c1 c2) R"
+lemma SeqRule: "Valid P c1 a1 Q \<Longrightarrow> Valid Q c2 a2 R \<Longrightarrow> Valid P (Seq c1 c2) (Aseq a1 a2) R"
 by (auto simp:Valid_def)
 
 lemma CondRule:
  "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
-  \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
+  \<Longrightarrow> Valid w c1 a1 q \<Longrightarrow> Valid w' c2 a2 q \<Longrightarrow> Valid p (Cond b c1 c2) (Acond a1 a2) q"
 by (auto simp:Valid_def)
 
 lemma While_aux:
-  assumes "Sem (While b i v c) s s'"
+  assumes "Sem (While b c) s s'"
   shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
     s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b"
   using assms
-  by (induct "While b i v c" s s') auto
+  by (induct "While b c" s s') auto
 
 lemma WhileRule:
- "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
+ "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c (A 0) i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b c) (Awhile i v A) q"
 apply (clarsimp simp:Valid_def)
 apply(drule While_aux)
   apply assumption
  apply blast
 apply blast
 done
 
 lemma SkipRuleTC:
   assumes "p \<subseteq> q"
-    shows "ValidTC p (Basic id) q"
+    shows "ValidTC p (Basic id) a q"
   by (metis assms Sem.intros(1) ValidTC_def id_apply subsetD)
 
 lemma BasicRuleTC:
   assumes "p \<subseteq> {s. f s \<in> q}"
-    shows "ValidTC p (Basic f) q"
+    shows "ValidTC p (Basic f) a q"
   by (metis assms Ball_Collect Sem.intros(1) ValidTC_def)
 
 lemma SeqRuleTC:
-  assumes "ValidTC p c1 q"
-      and "ValidTC q c2 r"
-    shows "ValidTC p (Seq c1 c2) r"
+  assumes "ValidTC p c1 a1 q"
+      and "ValidTC q c2 a2 r"
+    shows "ValidTC p (Seq c1 c2) (Aseq a1 a2) r"
   by (meson assms Sem.intros(2) ValidTC_def)
 
 lemma CondRuleTC:
  assumes "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}"
-     and "ValidTC w c1 q"
-     and "ValidTC w' c2 q"
-   shows "ValidTC p (Cond b c1 c2) q"
+     and "ValidTC w c1 a1 q"
+     and "ValidTC w' c2 a2 q"
+   shows "ValidTC p (Cond b c1 c2) (Acond a1 a2) q"
 proof (unfold ValidTC_def, rule allI)
   fix s
   show "s \<in> p \<longrightarrow> (\<exists>t . Sem (Cond b c1 c2) s t \<and> t \<in> q)"
     apply (cases "s \<in> b")
     apply (metis (mono_tags, lifting) assms(1,2) Ball_Collect Sem.intros(3) ValidTC_def)
     by (metis (mono_tags, lifting) assms(1,3) Ball_Collect Sem.intros(4) ValidTC_def)
 qed
 
 lemma WhileRuleTC:
   assumes "p \<subseteq> i"
-      and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (i \<inter> {s . v s < n})"
+      and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (A n) (i \<inter> {s . v s < n})"
       and "i \<inter> uminus b \<subseteq> q"
-    shows "ValidTC p (While b i v c) q"
+    shows "ValidTC p (While b c) (Awhile i v A) q"
 proof -
   {
     fix s n
-    have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) s t \<and> t \<in> q)"
+    have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
     proof (induction "n" arbitrary: s rule: less_induct)
       fix n :: nat
       fix s :: 'a
-      assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b i v c) s t \<and> t \<in> q)"
-      show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) s t \<and> t \<in> q)"
+      assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
+      show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
       proof (rule impI, cases "s \<in> b")
         assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
         hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
           using assms(1) by auto
         hence "\<exists>t . Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
           by (metis assms(2) ValidTC_def)
         from this obtain t where 3: "Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
           by auto
-        hence "\<exists>u . Sem (While b i v c) t u \<and> u \<in> q"
+        hence "\<exists>u . Sem (While b c) t u \<and> u \<in> q"
           using 1 by auto
-        thus "\<exists>t . Sem (While b i v c) s t \<and> t \<in> q"
+        thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q"
           using 2 3 Sem.intros(6) by force
       next
         assume "s \<notin> b" and "s \<in> i \<and> v s = n"
-        thus "\<exists>t . Sem (While b i v c) s t \<and> t \<in> q"
+        thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q"
           using Sem.intros(5) assms(3) by fastforce
       qed
     qed
   }
   thus ?thesis
     using assms(1) ValidTC_def by force
 qed
 
 
 subsubsection \<open>Concrete syntax\<close>
 
 setup \<open>
   Hoare_Syntax.setup
    {Basic = \<^const_syntax>\<open>Basic\<close>,
     Skip = \<^const_syntax>\<open>annskip\<close>,
     Seq = \<^const_syntax>\<open>Seq\<close>,
     Cond = \<^const_syntax>\<open>Cond\<close>,
     While = \<^const_syntax>\<open>While\<close>,
     Valid = \<^const_syntax>\<open>Valid\<close>,
     ValidTC = \<^const_syntax>\<open>ValidTC\<close>}
 \<close>
 
 
 subsubsection \<open>Proof methods: VCG\<close>
 
 declare BasicRule [Hoare_Tac.BasicRule]
   and SkipRule [Hoare_Tac.SkipRule]
   and SeqRule [Hoare_Tac.SeqRule]
   and CondRule [Hoare_Tac.CondRule]
   and WhileRule [Hoare_Tac.WhileRule]
 
 declare BasicRuleTC [Hoare_Tac.BasicRuleTC]
   and SkipRuleTC [Hoare_Tac.SkipRuleTC]
   and SeqRuleTC [Hoare_Tac.SeqRuleTC]
   and CondRuleTC [Hoare_Tac.CondRuleTC]
   and WhileRuleTC [Hoare_Tac.WhileRuleTC]
 
 method_setup vcg = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_simp = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 method_setup vcg_tc = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_tc_simp = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 end
diff --git a/src/HOL/Hoare/Hoare_Logic_Abort.thy b/src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy
@@ -1,236 +1,236 @@
 (*  Title:      HOL/Hoare/Hoare_Logic_Abort.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   2003 TUM
     Author:     Walter Guttmann (extension to total-correctness proofs)
 *)
 
 section \<open>Hoare Logic with an Abort statement for modelling run time errors\<close>
 
 theory Hoare_Logic_Abort
   imports Hoare_Syntax Hoare_Tac
 begin
 
 type_synonym 'a bexp = "'a set"
 type_synonym 'a assn = "'a set"
 type_synonym 'a var = "'a \<Rightarrow> nat"
 
 datatype 'a com =
   Basic "'a \<Rightarrow> 'a"
 | Abort
 | Seq "'a com" "'a com"
 | Cond "'a bexp" "'a com" "'a com"
-| While "'a bexp" "'a assn" "'a var" "'a com"
+| While "'a bexp" "'a com"
 
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 type_synonym 'a sem = "'a option => 'a option => bool"
 
 inductive Sem :: "'a com \<Rightarrow> 'a sem"
 where
   "Sem (Basic f) None None"
 | "Sem (Basic f) (Some s) (Some (f s))"
 | "Sem Abort s None"
 | "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (Seq c1 c2) s s'"
 | "Sem (Cond b c1 c2) None None"
 | "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (Cond b c1 c2) (Some s) s'"
 | "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (Cond b c1 c2) (Some s) s'"
-| "Sem (While b x y c) None None"
-| "s \<notin> b \<Longrightarrow> Sem (While b x y c) (Some s) (Some s)"
-| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow>
-   Sem (While b x y c) (Some s) s'"
+| "Sem (While b c) None None"
+| "s \<notin> b \<Longrightarrow> Sem (While b c) (Some s) (Some s)"
+| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b c) s'' s' \<Longrightarrow>
+   Sem (While b c) (Some s) s'"
 
 inductive_cases [elim!]:
   "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
   "Sem (Cond b c1 c2) s s'"
 
 lemma Sem_deterministic:
   assumes "Sem c s s1"
       and "Sem c s s2"
     shows "s1 = s2"
 proof -
   have "Sem c s s1 \<Longrightarrow> (\<forall>s2. Sem c s s2 \<longrightarrow> s1 = s2)"
     by (induct rule: Sem.induct) (subst Sem.simps, blast)+
   thus ?thesis
     using assms by simp
 qed
 
-definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
-  where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` p \<longrightarrow> s' \<in> Some ` q"
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a anno \<Rightarrow> 'a bexp \<Rightarrow> bool"
+  where "Valid p c a q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` p \<longrightarrow> s' \<in> Some ` q"
 
-definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
-  where "ValidTC p c q \<equiv> \<forall>s . s \<in> p \<longrightarrow> (\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> q)"
+definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a anno \<Rightarrow> 'a bexp \<Rightarrow> bool"
+  where "ValidTC p c a q \<equiv> \<forall>s . s \<in> p \<longrightarrow> (\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> q)"
 
 lemma tc_implies_pc:
-  "ValidTC p c q \<Longrightarrow> Valid p c q"
+  "ValidTC p c a q \<Longrightarrow> Valid p c a q"
   by (smt (verit) Sem_deterministic ValidTC_def Valid_def image_iff)
 
 lemma tc_extract_function:
-  "ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
+  "ValidTC p c a q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
   by (meson ValidTC_def)
 
 text \<open>The proof rules for partial correctness\<close>
 
-lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
+lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) a q"
 by (auto simp:Valid_def)
 
-lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
+lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) a q"
 by (auto simp:Valid_def)
 
-lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (Seq c1 c2) R"
+lemma SeqRule: "Valid P c1 a1 Q \<Longrightarrow> Valid Q c2 a2 R \<Longrightarrow> Valid P (Seq c1 c2) (Aseq a1 a2) R"
 by (auto simp:Valid_def)
 
 lemma CondRule:
  "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
-  \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
+  \<Longrightarrow> Valid w c1 a1 q \<Longrightarrow> Valid w' c2 a2 q \<Longrightarrow> Valid p (Cond b c1 c2) (Acond a1 a2) q"
 by (fastforce simp:Valid_def image_def)
 
 lemma While_aux:
-  assumes "Sem (While b i v c) s s'"
+  assumes "Sem (While b c) s s'"
   shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
     s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)"
   using assms
-  by (induct "While b i v c" s s') auto
+  by (induct "While b c" s s') auto
 
 lemma WhileRule:
- "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
+ "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c (A 0) i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b c) (Awhile i v A) q"
 apply (clarsimp simp:Valid_def)
 apply(drule While_aux)
   apply assumption
  apply blast
 apply blast
 done
 
-lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort q"
+lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort a q"
 by(auto simp:Valid_def)
 
 text \<open>The proof rules for total correctness\<close>
 
 lemma SkipRuleTC:
   assumes "p \<subseteq> q"
-    shows "ValidTC p (Basic id) q"
+    shows "ValidTC p (Basic id) a q"
   by (metis Sem.intros(2) ValidTC_def assms id_def subsetD)
 
 lemma BasicRuleTC:
   assumes "p \<subseteq> {s. f s \<in> q}"
-    shows "ValidTC p (Basic f) q"
+    shows "ValidTC p (Basic f) a q"
   by (metis Ball_Collect Sem.intros(2) ValidTC_def assms)
 
 lemma SeqRuleTC:
-  assumes "ValidTC p c1 q"
-      and "ValidTC q c2 r"
-    shows "ValidTC p (Seq c1 c2) r"
+  assumes "ValidTC p c1 a1 q"
+      and "ValidTC q c2 a2 r"
+    shows "ValidTC p (Seq c1 c2) (Aseq a1 a2) r"
   by (meson assms Sem.intros(4) ValidTC_def)
 
 lemma CondRuleTC:
  assumes "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}"
-     and "ValidTC w c1 q"
-     and "ValidTC w' c2 q"
-   shows "ValidTC p (Cond b c1 c2) q"
+     and "ValidTC w c1 a1 q"
+     and "ValidTC w' c2 a2 q"
+   shows "ValidTC p (Cond b c1 c2) (Acons a1 a2)  q"
 proof (unfold ValidTC_def, rule allI)
   fix s
   show "s \<in> p \<longrightarrow> (\<exists>t . Sem (Cond b c1 c2) (Some s) (Some t) \<and> t \<in> q)"
     apply (cases "s \<in> b")
     apply (metis (mono_tags, lifting) Ball_Collect Sem.intros(6) ValidTC_def assms(1,2))
     by (metis (mono_tags, lifting) Ball_Collect Sem.intros(7) ValidTC_def assms(1,3))
 qed
 
 lemma WhileRuleTC:
   assumes "p \<subseteq> i"
-      and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (i \<inter> {s . v s < n})"
+      and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (A n) (i \<inter> {s . v s < n})"
       and "i \<inter> uminus b \<subseteq> q"
-    shows "ValidTC p (While b i v c) q"
+    shows "ValidTC p (While b c) (Awhile i v A) q"
 proof -
   {
     fix s n
-    have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)"
+    have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q)"
     proof (induction "n" arbitrary: s rule: less_induct)
       fix n :: nat
       fix s :: 'a
-      assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)"
-      show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)"
+      assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q)"
+      show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q)"
       proof (rule impI, cases "s \<in> b")
         assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
         hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
           using assms(1) by auto
         hence "\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}"
           by (metis assms(2) ValidTC_def)
         from this obtain t where 3: "Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}"
           by auto
-        hence "\<exists>u . Sem (While b i v c) (Some t) (Some u) \<and> u \<in> q"
+        hence "\<exists>u . Sem (While b c) (Some t) (Some u) \<and> u \<in> q"
           using 1 by auto
-        thus "\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q"
+        thus "\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q"
           using 2 3 Sem.intros(10) by force
       next
         assume "s \<notin> b" and "s \<in> i \<and> v s = n"
-        thus "\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q"
+        thus "\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q"
           using Sem.intros(9) assms(3) by fastforce
       qed
     qed
   }
   thus ?thesis
     using assms(1) ValidTC_def by force
 qed
 
 
 subsection \<open>Concrete syntax\<close>
 
 setup \<open>
   Hoare_Syntax.setup
    {Basic = \<^const_syntax>\<open>Basic\<close>,
     Skip = \<^const_syntax>\<open>annskip\<close>,
     Seq = \<^const_syntax>\<open>Seq\<close>,
     Cond = \<^const_syntax>\<open>Cond\<close>,
     While = \<^const_syntax>\<open>While\<close>,
     Valid = \<^const_syntax>\<open>Valid\<close>,
     ValidTC = \<^const_syntax>\<open>ValidTC\<close>}
 \<close>
 
 \<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close>
 syntax
   "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
   "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
 translations
   "P \<rightarrow> c" \<rightleftharpoons> "IF P THEN c ELSE CONST Abort FI"
   "a[i] := v" \<rightharpoonup> "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
   \<comment> \<open>reverse translation not possible because of duplicate \<open>a\<close>\<close>
 
 text \<open>
   Note: there is no special syntax for guarded array access. Thus
   you must write \<open>j < length a \<rightarrow> a[i] := a!j\<close>.
 \<close>
 
 
 subsection \<open>Proof methods: VCG\<close>
 
 declare BasicRule [Hoare_Tac.BasicRule]
   and SkipRule [Hoare_Tac.SkipRule]
   and AbortRule [Hoare_Tac.AbortRule]
   and SeqRule [Hoare_Tac.SeqRule]
   and CondRule [Hoare_Tac.CondRule]
   and WhileRule [Hoare_Tac.WhileRule]
 
 declare BasicRuleTC [Hoare_Tac.BasicRuleTC]
   and SkipRuleTC [Hoare_Tac.SkipRuleTC]
   and SeqRuleTC [Hoare_Tac.SeqRuleTC]
   and CondRuleTC [Hoare_Tac.CondRuleTC]
   and WhileRuleTC [Hoare_Tac.WhileRuleTC]
 
 method_setup vcg = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_simp = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 method_setup vcg_tc = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_tc_simp = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 end
diff --git a/src/HOL/Hoare/Hoare_Syntax.thy b/src/HOL/Hoare/Hoare_Syntax.thy
--- a/src/HOL/Hoare/Hoare_Syntax.thy
+++ b/src/HOL/Hoare/Hoare_Syntax.thy
@@ -1,32 +1,52 @@
 (*  Title:      HOL/Hoare/Hoare_Syntax.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Author:     Walter Guttmann (extension to total-correctness proofs)
 *)
 
 section \<open>Concrete syntax for Hoare logic, with translations for variables\<close>
 
 theory Hoare_Syntax
   imports Main
 begin
 
 syntax
   "_assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'com"  ("(2_ :=/ _)" [70, 65] 61)
   "_Seq" :: "'com \<Rightarrow> 'com \<Rightarrow> 'com"  ("(_;/ _)" [61,60] 60)
   "_Cond" :: "'bexp \<Rightarrow> 'com \<Rightarrow> 'com \<Rightarrow> 'com"  ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
   "_While" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'var \<Rightarrow> 'com \<Rightarrow> 'com"  ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
 
+text \<open>The \<open>VAR {_}\<close> syntax supports two variants:
+\<^item> \<open>VAR {x = t}\<close> where \<open>t::nat\<close> is the decreasing expression,
+  the variant, and \<open>x\<close> a variable that can be referred to from inner annotations.
+  The \<open>x\<close> can be necessary for nested loops, e.g. to prove that the inner loops do not mess with \<open>t\<close>.
+\<^item> \<open>VAR {t}\<close> where the variable is omitted because it is not needed.
+\<close>
+
 syntax
   "_While0" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'com \<Rightarrow> 'com"  ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
-translations
-  "WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD"
+
+text \<open>The \<open>_While0\<close> syntax is translated into the \<open>_While\<close> syntax with the trivial variant 0.
+This is ok because partial correctness proofs do not make use of the variant.\<close>
 
 syntax
  "_hoare_vars" :: "[idts, 'assn,'com, 'assn] \<Rightarrow> bool"  ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
  "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \<Rightarrow> bool"  ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
 syntax (output)
  "_hoare" :: "['assn, 'com, 'assn] \<Rightarrow> bool"  ("{_} // _ // {_}" [0,55,0] 50)
  "_hoare_tc" :: "['assn, 'com, 'assn] \<Rightarrow> bool"  ("[_] // _ // [_]" [0,55,0] 50)
 
+text \<open>Completeness requires(?) the ability to refer to an outer variant in an inner invariant.
+Thus we need to abstract over a variable equated with the variant, the \<open>x\<close> in \<open>VAR {x = t}\<close>.
+But the \<open>x\<close> should only occur in invariants. To enforce this, syntax translations in \<open>hoare_syntax.ML\<close>
+separate the program from its annotations and only the latter are abstracted over over \<open>x\<close>.
+(Thus \<open>x\<close> can also occur in inner variants, but that neither helps nor hurts.)\<close>
+
+datatype 'a anno =
+  Abasic |
+  Aseq "'a anno"  "'a anno" |
+  Acond "'a anno" "'a anno" |
+  Awhile "'a set" "'a \<Rightarrow> nat" "nat \<Rightarrow> 'a anno"
+
 ML_file \<open>hoare_syntax.ML\<close>
 
 end
diff --git a/src/HOL/Hoare/SchorrWaite.thy b/src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy
+++ b/src/HOL/Hoare/SchorrWaite.thy
@@ -1,575 +1,576 @@
 (*  Title:      HOL/Hoare/SchorrWaite.thy
     Author:     Farhad Mehta
     Copyright   2003 TUM
 *)
 
 section \<open>Proof of the Schorr-Waite graph marking algorithm\<close>
 
 theory SchorrWaite
   imports HeapSyntax
 begin
 
 subsection \<open>Machinery for the Schorr-Waite proof\<close>
 
 definition
   \<comment> \<open>Relations induced by a mapping\<close>
   rel :: "('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<times> 'a) set"
   where "rel m = {(x,y). m x = Ref y}"
 
 definition
   relS :: "('a \<Rightarrow> 'a ref) set \<Rightarrow> ('a \<times> 'a) set"
   where "relS M = (\<Union>m \<in> M. rel m)"
 
 definition
   addrs :: "'a ref set \<Rightarrow> 'a set"
   where "addrs P = {a. Ref a \<in> P}"
 
 definition
   reachable :: "('a \<times> 'a) set \<Rightarrow> 'a ref set \<Rightarrow> 'a set"
   where "reachable r P = (r\<^sup>* `` addrs P)"
 
 lemmas rel_defs = relS_def rel_def
 
 text \<open>Rewrite rules for relations induced by a mapping\<close>
 
 lemma self_reachable: "b \<in> B \<Longrightarrow> b \<in> R\<^sup>* `` B"
 apply blast
 done
 
 lemma oneStep_reachable: "b \<in> R``B \<Longrightarrow> b \<in> R\<^sup>* `` B"
 apply blast
 done
 
 lemma still_reachable: "\<lbrakk>B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Rb\<^sup>* `` B \<subseteq> Ra\<^sup>* `` A "
 apply (clarsimp simp only:Image_iff)
 apply (erule rtrancl_induct)
  apply blast
 apply (subgoal_tac "(y, z) \<in> Ra\<union>(Rb-Ra)")
  apply (erule UnE)
  apply (auto intro:rtrancl_into_rtrancl)
 apply blast
 done
 
 lemma still_reachable_eq: "\<lbrakk> A\<subseteq>Rb\<^sup>*``B; B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Ra-Rb. y \<in>(Rb\<^sup>*``B); \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Ra\<^sup>*``A =  Rb\<^sup>*``B "
 apply (rule equalityI)
  apply (erule still_reachable ,assumption)+
 done
 
 lemma reachable_null: "reachable mS {Null} = {}"
 apply (simp add: reachable_def addrs_def)
 done
 
 lemma reachable_empty: "reachable mS {} = {}"
 apply (simp add: reachable_def addrs_def)
 done
 
 lemma reachable_union: "(reachable mS aS \<union> reachable mS bS) = reachable mS (aS \<union> bS)"
 apply (simp add: reachable_def rel_defs addrs_def)
 apply blast
 done
 
 lemma reachable_union_sym: "reachable r (insert a aS) = (r\<^sup>* `` addrs {a}) \<union> reachable r aS"
 apply (simp add: reachable_def rel_defs addrs_def)
 apply blast
 done
 
 lemma rel_upd1: "(a,b) \<notin> rel (r(q:=t)) \<Longrightarrow> (a,b) \<in> rel r \<Longrightarrow> a=q"
 apply (rule classical)
 apply (simp add:rel_defs fun_upd_apply)
 done
 
 lemma rel_upd2: "(a,b)  \<notin> rel r \<Longrightarrow> (a,b) \<in> rel (r(q:=t)) \<Longrightarrow> a=q"
 apply (rule classical)
 apply (simp add:rel_defs fun_upd_apply)
 done
 
 definition
   \<comment> \<open>Restriction of a relation\<close>
   restr ::"('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set"       ("(_/ | _)" [50, 51] 50)
   where "restr r m = {(x,y). (x,y) \<in> r \<and> \<not> m x}"
 
 text \<open>Rewrite rules for the restriction of a relation\<close>
 
 lemma restr_identity[simp]:
  " (\<forall>x. \<not> m x) \<Longrightarrow> (R |m) = R"
 by (auto simp add:restr_def)
 
 lemma restr_rtrancl[simp]: " \<lbrakk>m l\<rbrakk> \<Longrightarrow> (R | m)\<^sup>* `` {l} = {l}"
 by (auto simp add:restr_def elim:converse_rtranclE)
 
 lemma [simp]: " \<lbrakk>m l\<rbrakk> \<Longrightarrow> (l,x) \<in> (R | m)\<^sup>* = (l=x)"
 by (auto simp add:restr_def elim:converse_rtranclE)
 
 lemma restr_upd: "((rel (r (q := t)))|(m(q := True))) = ((rel (r))|(m(q := True))) "
 apply (auto simp:restr_def rel_def fun_upd_apply)
 apply (rename_tac a b)
 apply (case_tac "a=q")
  apply auto
 done
 
 lemma restr_un: "((r \<union> s)|m) = (r|m) \<union> (s|m)"
   by (auto simp add:restr_def)
 
 lemma rel_upd3: "(a, b) \<notin> (r|(m(q := t))) \<Longrightarrow> (a,b) \<in> (r|m) \<Longrightarrow> a = q "
 apply (rule classical)
 apply (simp add:restr_def fun_upd_apply)
 done
 
 definition
   \<comment> \<open>A short form for the stack mapping function for List\<close>
   S :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref)"
   where "S c l r = (\<lambda>x. if c x then r x else l x)"
 
 text \<open>Rewrite rules for Lists using S as their mapping\<close>
 
 lemma [rule_format,simp]:
  "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c l r) p stack = List (S (c(a:=x)) (l(a:=y)) (r(a:=z))) p stack"
 apply(induct_tac stack)
  apply(simp add:fun_upd_apply S_def)+
 done
 
 lemma [rule_format,simp]:
  "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c l (r(a:=z))) p stack = List (S c l r) p stack"
 apply(induct_tac stack)
  apply(simp add:fun_upd_apply S_def)+
 done
 
 lemma [rule_format,simp]:
  "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c (l(a:=z)) r) p stack = List (S c l r) p stack"
 apply(induct_tac stack)
  apply(simp add:fun_upd_apply S_def)+
 done
 
 lemma [rule_format,simp]:
  "\<forall>p. a \<notin> set stack \<longrightarrow> List (S (c(a:=z)) l r) p stack = List (S c l r) p stack"
 apply(induct_tac stack)
  apply(simp add:fun_upd_apply S_def)+
 done
 
 primrec
   \<comment> \<open>Recursive definition of what is means for a the graph/stack structure to be reconstructible\<close>
   stkOk :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow>'a list \<Rightarrow>  bool"
 where
   stkOk_nil:  "stkOk c l r iL iR t [] = True"
 | stkOk_cons:
     "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and> 
       iL p = (if c p then l p else t) \<and>
       iR p = (if c p then t else r p))"
 
 text \<open>Rewrite rules for stkOk\<close>
 
 lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
   stkOk (c(x := f)) l r iL iR t xs = stkOk c l r iL iR t xs"
 apply (induct xs)
  apply (auto simp:eq_sym_conv)
 done
 
 lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
  stkOk c (l(x := g)) r iL iR t xs = stkOk c l r iL iR t xs"
 apply (induct xs)
  apply (auto simp:eq_sym_conv)
 done
 
 lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
  stkOk c l (r(x := g)) iL iR t xs = stkOk c l r iL iR t xs"
 apply (induct xs)
  apply (auto simp:eq_sym_conv)
 done
 
 lemma stkOk_r_rewrite [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
   stkOk c l (r(x := g)) iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
 apply (induct xs)
  apply (auto simp:eq_sym_conv)
 done
 
 lemma [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
  stkOk c (l(x := g)) r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
 apply (induct xs)
  apply (auto simp:eq_sym_conv)
 done
 
 lemma [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
  stkOk (c(x := g)) l r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
 apply (induct xs)
  apply (auto simp:eq_sym_conv)
 done
 
 
 subsection \<open>The Schorr-Waite algorithm\<close>
 
 theorem SchorrWaiteAlgorithm: 
 "VARS c m l r t p q root
  {R = reachable (relS {l, r}) {root} \<and> (\<forall>x. \<not> m x) \<and> iR = r \<and> iL = l} 
  t := root; p := Null;
  WHILE p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m
  INV {\<exists>stack.
           List (S c l r) p stack \<and>                                      \<comment> \<open>\<open>i1\<close>\<close>
           (\<forall>x \<in> set stack. m x) \<and>                                       \<comment> \<open>\<open>i2\<close>\<close>
           R = reachable (relS{l, r}) {t,p} \<and>                            \<comment> \<open>\<open>i3\<close>\<close>
           (\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow>                                         \<comment> \<open>\<open>i4\<close>\<close>
                  x \<in> reachable (relS{l,r}|m) ({t}\<union>set(map r stack))) \<and>
           (\<forall>x. m x \<longrightarrow> x \<in> R) \<and>                                         \<comment> \<open>\<open>i5\<close>\<close>
           (\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and>             \<comment> \<open>\<open>i6\<close>\<close>
           (stkOk c l r iL iR t stack)                                   \<comment> \<open>\<open>i7\<close>\<close>}
  DO IF t = Null \<or> t^.m
       THEN IF p^.c
                THEN q := t; t := p; p := p^.r; t^.r := q                \<comment> \<open>\<open>pop\<close>\<close>
                ELSE q := t; t := p^.r; p^.r := p^.l;                    \<comment> \<open>\<open>swing\<close>\<close>
                         p^.l := q; p^.c := True          FI    
       ELSE q := p; p := t; t := t^.l; p^.l := q;                        \<comment> \<open>\<open>push\<close>\<close>
                p^.m := True; p^.c := False            FI       OD
  {(\<forall>x. (x \<in> R) = m x) \<and> (r = iR \<and> l = iL) }"
-  (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}")
+  (is "Valid
+         {(c, m, l, r, t, p, q, root). ?Pre c m l r root}
+         (Seq _ (Seq _ (While {(c, m, l, r, t, p, q, root). ?whileB m t p} _)))
+         (Aseq _ (Aseq _ (Awhile {(c, m, l, r, t, p, q, root). ?inv c m l r t p} _ _))) _")
 proof (vcg)
-  let "While {(c, m, l, r, t, p, q, root). ?whileB m t p}
-    {(c, m, l, r, t, p, q, root). ?inv c m l r t p} _ ?body" = ?c3
   {
 
     fix c m l r t p q root
     assume "?Pre c m l r root"
     thus "?inv c m l r root Null"  by (auto simp add: reachable_def addrs_def)
   next
 
     fix c m l r t p q
     let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
     assume a: "?inv c m l r t p \<and> \<not>(p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)"  
     then obtain stack where inv: "?Inv stack" by blast
     from a have pNull: "p = Null" and tDisj: "t=Null \<or> (t\<noteq>Null \<and> t^.m )" by auto
     let "?I1 \<and> _ \<and> _ \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> _"  =  "?Inv stack"
     from inv have i1: "?I1" and i4: "?I4" and i5: "?I5" and i6: "?I6" by simp+
     from pNull i1 have stackEmpty: "stack = []" by simp
     from tDisj i4 have RisMarked[rule_format]: "\<forall>x.  x \<in> R \<longrightarrow> m x"  by(auto simp: reachable_def addrs_def stackEmpty)
     from i5 i6 show "(\<forall>x.(x \<in> R) = m x) \<and> r = iR \<and> l = iL"  by(auto simp: stackEmpty fun_eq_iff intro:RisMarked)
 
   next   
       fix c m l r t p q root
       let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
       let "\<exists>stack. ?popInv stack"  =  "?inv c m l (r(p \<rightarrow> t)) p (p^.r)"
       let "\<exists>stack. ?swInv stack"  =
         "?inv (c(p \<rightarrow> True)) m (l(p \<rightarrow> t)) (r(p \<rightarrow> p^.l)) (p^.r) p"
       let "\<exists>stack. ?puInv stack"  =
         "?inv (c(t \<rightarrow> False)) (m(t \<rightarrow> True)) (l(t \<rightarrow> p)) r (t^.l) t"
       let "?ifB1"  =  "(t = Null \<or> t^.m)"
       let "?ifB2"  =  "p^.c" 
 
-      assume "(\<exists>stack.?Inv stack) \<and> (p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)" (is "_ \<and> ?whileB")
-      then obtain stack where inv: "?Inv stack" and whileB: "?whileB" by blast
+      assume "(\<exists>stack.?Inv stack) \<and> ?whileB m t p"
+      then obtain stack where inv: "?Inv stack" and whileB: "?whileB m t p" by blast
       let "?I1 \<and> ?I2 \<and> ?I3 \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> ?I7" = "?Inv stack"
       from inv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4"
                   and i5: "?I5" and i6: "?I6" and i7: "?I7" by simp+        
       have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
 
       show "(?ifB1 \<longrightarrow> (?ifB2 \<longrightarrow> (\<exists>stack.?popInv stack)) \<and> 
                             (\<not>?ifB2 \<longrightarrow> (\<exists>stack.?swInv stack)) ) \<and>
               (\<not>?ifB1 \<longrightarrow> (\<exists>stack.?puInv stack))"
       proof - 
         {
           assume ifB1: "t = Null \<or> t^.m" and ifB2: "p^.c"
           from ifB1 whileB have pNotNull: "p \<noteq> Null" by auto
           then obtain addr_p where addr_p_eq: "p = Ref addr_p" by auto
           with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl"
             by auto
           with i2 have m_addr_p: "p^.m" by auto
           have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
           from stack_eq stackDist have p_notin_stack_tl: "addr p \<notin> set stack_tl" by simp
           let "?poI1\<and> ?poI2\<and> ?poI3\<and> ?poI4\<and> ?poI5\<and> ?poI6\<and> ?poI7" = "?popInv stack_tl"
           have "?popInv stack_tl"
           proof -
 
             \<comment> \<open>List property is maintained:\<close>
             from i1 p_notin_stack_tl ifB2
             have poI1: "List (S c l (r(p \<rightarrow> t))) (p^.r) stack_tl" 
               by(simp add: addr_p_eq stack_eq, simp add: S_def)
 
             moreover
             \<comment> \<open>Everything on the stack is marked:\<close>
             from i2 have poI2: "\<forall> x \<in> set stack_tl. m x" by (simp add:stack_eq)
             moreover
 
             \<comment> \<open>Everything is still reachable:\<close>
             let "(R = reachable ?Ra ?A)" = "?I3"
             let "?Rb" = "(relS {l, r(p \<rightarrow> t)})"
             let "?B" = "{p, p^.r}"
             \<comment> \<open>Our goal is \<open>R = reachable ?Rb ?B\<close>.\<close>
             have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" (is "?L = ?R")
             proof
               show "?L \<subseteq> ?R"
               proof (rule still_reachable)
                 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" by(fastforce simp:addrs_def relS_def rel_def addr_p_eq 
                      intro:oneStep_reachable Image_iff[THEN iffD2])
                 show "\<forall>(x,y) \<in> ?Ra-?Rb. y \<in> (?Rb\<^sup>* `` addrs ?B)" by (clarsimp simp:relS_def) 
                      (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
               qed
               show "?R \<subseteq> ?L"
               proof (rule still_reachable)
                 show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
                   by(fastforce simp:addrs_def rel_defs addr_p_eq 
                       intro:oneStep_reachable Image_iff[THEN iffD2])
               next
                 show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
                   by (clarsimp simp:relS_def) 
                      (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd2)
               qed
             qed
             with i3 have poI3: "R = reachable ?Rb ?B"  by (simp add:reachable_def) 
             moreover
 
             \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
             let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A"  =  ?I4        
             let "?Rb" = "relS {l, r(p \<rightarrow> t)} | m"
             let "?B" = "{p} \<union> set (map (r(p \<rightarrow> t)) stack_tl)"
             \<comment> \<open>Our goal is \<open>\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B\<close>.\<close>
             let ?T = "{t, p^.r}"
 
             have "?Ra\<^sup>* `` addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
             proof (rule still_reachable)
               have rewrite: "\<forall>s\<in>set stack_tl. (r(p \<rightarrow> t)) s = r s"
                 by (auto simp add:p_notin_stack_tl intro:fun_upd_other) 
               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
                 by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
                 by (clarsimp simp:restr_def relS_def) 
                   (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
             qed
             \<comment> \<open>We now bring a term from the right to the left of the subset relation.\<close>
             hence subset: "?Ra\<^sup>* `` addrs ?A - ?Rb\<^sup>* `` addrs ?T \<subseteq> ?Rb\<^sup>* `` addrs ?B"
               by blast
             have poI4: "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B"
             proof (rule allI, rule impI)
               fix x
               assume a: "x \<in> R \<and> \<not> m x"
               \<comment> \<open>First, a disjunction on \<^term>\<open>p^.r\<close> used later in the proof\<close>
               have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2 
                 by auto
               \<comment> \<open>\<^term>\<open>x\<close> belongs to the left hand side of @{thm[source] subset}:\<close>
               have incl: "x \<in> ?Ra\<^sup>*``addrs ?A" using  a i4 by (simp only:reachable_def, clarsimp)
               have excl: "x \<notin> ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def)
               \<comment> \<open>And therefore also belongs to the right hand side of @{thm[source]subset},\<close>
               \<comment> \<open>which corresponds to our goal.\<close>
               from incl excl subset  show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def)
             qed
             moreover
 
             \<comment> \<open>If it is marked, then it is reachable\<close>
             from i5 have poI5: "\<forall>x. m x \<longrightarrow> x \<in> R" .
             moreover
 
             \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
             from i7 i6 ifB2 
             have poI6: "\<forall>x. x \<notin> set stack_tl \<longrightarrow> (r(p \<rightarrow> t)) x = iR x \<and> l x = iL x" 
               by(auto simp: addr_p_eq stack_eq fun_upd_apply)
 
             moreover
 
             \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
             from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \<rightarrow> t)) iL iR p stack_tl"
               by (clarsimp simp:stack_eq addr_p_eq)
 
             ultimately show "?popInv stack_tl" by simp
           qed
           hence "\<exists>stack. ?popInv stack" ..
         }
         moreover
 
         \<comment> \<open>Proofs of the Swing and Push arm follow.\<close>
         \<comment> \<open>Since they are in principle simmilar to the Pop arm proof,\<close>
         \<comment> \<open>we show fewer comments and use frequent pattern matching.\<close>
         {
           \<comment> \<open>Swing arm\<close>
           assume ifB1: "?ifB1" and nifB2: "\<not>?ifB2"
           from ifB1 whileB have pNotNull: "p \<noteq> Null" by clarsimp
           then obtain addr_p where addr_p_eq: "p = Ref addr_p" by clarsimp
           with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" by clarsimp
           with i2 have m_addr_p: "p^.m" by clarsimp
           from stack_eq stackDist have p_notin_stack_tl: "(addr p) \<notin> set stack_tl"
             by simp
           let "?swI1\<and>?swI2\<and>?swI3\<and>?swI4\<and>?swI5\<and>?swI6\<and>?swI7" = "?swInv stack"
           have "?swInv stack"
           proof -
             
             \<comment> \<open>List property is maintained:\<close>
             from i1 p_notin_stack_tl nifB2
             have swI1: "?swI1"
               by (simp add:addr_p_eq stack_eq, simp add:S_def)
             moreover
             
             \<comment> \<open>Everything on the stack is marked:\<close>
             from i2
             have swI2: "?swI2" .
             moreover
             
             \<comment> \<open>Everything is still reachable:\<close>
             let "R = reachable ?Ra ?A" = "?I3"
             let "R = reachable ?Rb ?B" = "?swI3"
             have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
             proof (rule still_reachable_eq)
               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
                 by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
             next
               show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
                 by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
             next
               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
                 by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
             next
               show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
                 by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
             qed
             with i3
             have swI3: "?swI3" by (simp add:reachable_def) 
             moreover
 
             \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
             let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
             let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?swI4
             let ?T = "{t}"
             have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
             proof (rule still_reachable)
               have rewrite: "(\<forall>s\<in>set stack_tl. (r(addr p := l(addr p))) s = r s)"
                 by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
                 by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
             next
               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
                 by (clarsimp simp:relS_def restr_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
             qed
             then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
               by blast
             have ?swI4
             proof (rule allI, rule impI)
               fix x
               assume a: "x \<in> R \<and>\<not> m x"
               with i4 addr_p_eq stack_eq  have inc: "x \<in> ?Ra\<^sup>*``addrs ?A" 
                 by (simp only:reachable_def, clarsimp)
               with ifB1 a 
               have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T" 
                 by (auto simp add:addrs_def)
               from inc exc subset  show "x \<in> reachable ?Rb ?B" 
                 by (auto simp add:reachable_def)
             qed
             moreover
             
             \<comment> \<open>If it is marked, then it is reachable\<close>
             from i5
             have "?swI5" .
             moreover
 
             \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
             from i6 stack_eq
             have "?swI6"
               by clarsimp           
             moreover
 
             \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
             from stackDist i7 nifB2 
             have "?swI7"
               by (clarsimp simp:addr_p_eq stack_eq)
 
             ultimately show ?thesis by auto
           qed
           then have "\<exists>stack. ?swInv stack" by blast
         }
         moreover
 
         {
           \<comment> \<open>Push arm\<close>
           assume nifB1: "\<not>?ifB1"
           from nifB1 whileB have tNotNull: "t \<noteq> Null" by clarsimp
           then obtain addr_t where addr_t_eq: "t = Ref addr_t" by clarsimp
           with i1 obtain new_stack where new_stack_eq: "new_stack = (addr t) # stack" by clarsimp
           from tNotNull nifB1 have n_m_addr_t: "\<not> (t^.m)" by clarsimp
           with i2 have t_notin_stack: "(addr t) \<notin> set stack" by blast
           let "?puI1\<and>?puI2\<and>?puI3\<and>?puI4\<and>?puI5\<and>?puI6\<and>?puI7" = "?puInv new_stack"
           have "?puInv new_stack"
           proof -
             
             \<comment> \<open>List property is maintained:\<close>
             from i1 t_notin_stack
             have puI1: "?puI1"
               by (simp add:addr_t_eq new_stack_eq, simp add:S_def)
             moreover
             
             \<comment> \<open>Everything on the stack is marked:\<close>
             from i2
             have puI2: "?puI2" 
               by (simp add:new_stack_eq fun_upd_apply)
             moreover
             
             \<comment> \<open>Everything is still reachable:\<close>
             let "R = reachable ?Ra ?A" = "?I3"
             let "R = reachable ?Rb ?B" = "?puI3"
             have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
             proof (rule still_reachable_eq)
               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
                 by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
             next
               show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
                 by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
             next
               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
                 by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
             next
               show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
                 by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
             qed
             with i3
             have puI3: "?puI3" by (simp add:reachable_def) 
             moreover
             
             \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
             let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
             let "\<forall>x. x \<in> R \<and> \<not> ?new_m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?puI4
             let ?T = "{t}"
             have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
             proof (rule still_reachable)
               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
                 by (fastforce simp:new_stack_eq addrs_def intro:self_reachable)
             next
               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
                 by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd) 
                    (fastforce simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3)
             qed
             then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
               by blast
             have ?puI4
             proof (rule allI, rule impI)
               fix x
               assume a: "x \<in> R \<and> \<not> ?new_m x"
               have xDisj: "x=(addr t) \<or> x\<noteq>(addr t)" by simp
               with i4 a have inc: "x \<in> ?Ra\<^sup>*``addrs ?A"
                 by (fastforce simp:addr_t_eq addrs_def reachable_def intro:self_reachable)
               have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T"
                 using xDisj a n_m_addr_t
                 by (clarsimp simp add:addrs_def addr_t_eq) 
               from inc exc subset  show "x \<in> reachable ?Rb ?B" 
                 by (auto simp add:reachable_def)
             qed  
             moreover
             
             \<comment> \<open>If it is marked, then it is reachable\<close>
             from i5
             have "?puI5"
               by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable)
             moreover
             
             \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
             from i6 
             have "?puI6"
               by (simp add:new_stack_eq)
             moreover
 
             \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
             from stackDist i6 t_notin_stack i7
             have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq)
 
             ultimately show ?thesis by auto
           qed
           then have "\<exists>stack. ?puInv stack" by blast
 
         }
         ultimately show ?thesis by blast
       qed
     }
   qed
 
 end
diff --git a/src/HOL/Hoare/hoare_syntax.ML b/src/HOL/Hoare/hoare_syntax.ML
--- a/src/HOL/Hoare/hoare_syntax.ML
+++ b/src/HOL/Hoare/hoare_syntax.ML
@@ -1,221 +1,253 @@
 (*  Title:      HOL/Hoare/hoare_syntax.ML
     Author:     Leonor Prensa Nieto & Tobias Nipkow
-    Author:     Walter Guttmann (extension to total-correctness proofs)
+    Author:     Walter Guttmann (initial extension to total-correctness proofs)
+    Author:     Tobias Nipkow (complete version of total correctness with separate anno type)
 
 Syntax translations for Hoare logic.
 *)
 
 signature HOARE_SYNTAX =
 sig
   val hoare_vars_tr: Proof.context -> term list -> term
   val hoare_tc_vars_tr: Proof.context -> term list -> term
   val spec_tr': string -> Proof.context -> term list -> term
   val setup:
     {Basic: string, Skip: string, Seq: string, Cond: string, While: string,
       Valid: string, ValidTC: string} -> theory -> theory
 end;
 
 structure Hoare_Syntax: HOARE_SYNTAX =
 struct
 
 (** theory data **)
 
 structure Data = Theory_Data
 (
   type T =
     {Basic: string, Skip: string, Seq: string, Cond: string, While: string,
       Valid: string, ValidTC: string} option;
   val empty: T = NONE;
   val extend = I;
   fun merge (data1, data2) =
     if is_some data1 andalso is_some data2 andalso data1 <> data2 then
       error "Cannot merge syntax from different Hoare Logics"
     else merge_options (data1, data2);
 );
 
 fun const_syntax ctxt which =
   (case Data.get (Proof_Context.theory_of ctxt) of
     SOME consts => which consts
   | NONE => error "Undefined Hoare syntax consts");
 
 val syntax_const = Syntax.const oo const_syntax;
 
 
 
 (** parse translation **)
 
 local
 
 fun idt_name (Free (x, _)) = SOME x
   | idt_name (Const (\<^syntax_const>\<open>_constrain\<close>, _) $ t $ _) = idt_name t
   | idt_name _ = NONE;
 
 fun eq_idt tu =
   (case apply2 idt_name tu of
     (SOME x, SOME y) => x = y
   | _ => false);
 
 fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
   | mk_abstuple (x :: xs) body =
       Syntax.const \<^const_syntax>\<open>case_prod\<close> $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
 
 fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
   | mk_fbody x e (y :: xs) =
       Syntax.const \<^const_syntax>\<open>Pair\<close> $
         (if eq_idt (x, y) then e else y) $ mk_fbody x e xs;
 
 fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
 
 
 (* bexp_tr & assn_tr *)
 (*all meta-variables for bexp except for TRUE are translated as if they
   were boolean expressions*)
 
 fun bexp_tr (Const ("TRUE", _)) _ = Syntax.const "TRUE"   (* FIXME !? *)
   | bexp_tr b xs = Syntax.const \<^const_syntax>\<open>Collect\<close> $ mk_abstuple xs b;
 
 fun assn_tr r xs = Syntax.const \<^const_syntax>\<open>Collect\<close> $ mk_abstuple xs r;
 
 fun var_tr v xs = mk_abstuple xs v;
 
 
 (* com_tr *)
 
 fun com_tr ctxt =
   let
     fun tr (Const (\<^syntax_const>\<open>_assign\<close>, _) $ x $ e) xs =
-          syntax_const ctxt #Basic $ mk_fexp x e xs
+          (syntax_const ctxt #Basic $ mk_fexp x e xs, Syntax.const \<^const_syntax>\<open>Abasic\<close>)
       | tr (Const (\<^syntax_const>\<open>_Seq\<close>,_) $ c1 $ c2) xs =
-          syntax_const ctxt #Seq $ tr c1 xs $ tr c2 xs
+          let val (c1',a1) = tr c1 xs;
+              val (c2',a2) = tr c2 xs
+          in (syntax_const ctxt #Seq $ c1' $ c2', Syntax.const \<^const_syntax>\<open>Aseq\<close> $ a1 $ a2) end
       | tr (Const (\<^syntax_const>\<open>_Cond\<close>,_) $ b $ c1 $ c2) xs =
-          syntax_const ctxt #Cond $ bexp_tr b xs $ tr c1 xs $ tr c2 xs
-      | tr (Const (\<^syntax_const>\<open>_While\<close>,_) $ b $ I $ V $ c) xs =
-          syntax_const ctxt #While $ bexp_tr b xs $ assn_tr I xs $ var_tr V xs $ tr c xs
-      | tr t _ = t;
+          let val (c1',a1) = tr c1 xs;
+              val (c2',a2) = tr c2 xs
+          in (syntax_const ctxt #Cond $ bexp_tr b xs $ c1' $ c2',
+              Syntax.const \<^const_syntax>\<open>Acond\<close> $ a1 $ a2)
+          end
+      | tr (Const (\<^syntax_const>\<open>_While\<close>,_) $ b $ i $ v $ c) xs =
+          let val (c',a) = tr c xs
+              val (v',A) = case v of
+                Const (\<^const_syntax>\<open>HOL.eq\<close>, _) $ z $ t => (t, Syntax_Trans.abs_tr [z, a]) |
+                t => (t, absdummy dummyT a)
+          in (syntax_const ctxt #While $ bexp_tr b xs $ c',
+              Syntax.const \<^const_syntax>\<open>Awhile\<close>
+                $ assn_tr i xs $ var_tr v' xs $ A)
+          end
+      | tr (Const (\<^syntax_const>\<open>_While0\<close>,_) $ b $ I $ c) xs =
+          let val (c',a) = tr c xs
+          in (syntax_const ctxt #While $ bexp_tr b xs $ c',
+              Syntax.const \<^const_syntax>\<open>Awhile\<close>
+                $ assn_tr I xs $ var_tr (Syntax.const \<^const_syntax>\<open>zero_class.zero\<close>) xs
+                $ absdummy dummyT a)
+          end
+      | tr t _ = (t, Syntax.const \<^const_syntax>\<open>Abasic\<close>)
   in tr end;
 
 fun vars_tr (Const (\<^syntax_const>\<open>_idts\<close>, _) $ idt $ vars) = idt :: vars_tr vars
   | vars_tr t = [t];
 
 in
 
 fun hoare_vars_tr ctxt [vars, pre, prg, post] =
       let val xs = vars_tr vars
-      in syntax_const ctxt #Valid $ assn_tr pre xs $ com_tr ctxt prg xs $ assn_tr post xs end
+          val (c',a) = com_tr ctxt prg xs
+      in syntax_const ctxt #Valid $ assn_tr pre xs $ c' $ a $ assn_tr post xs end
   | hoare_vars_tr _ ts = raise TERM ("hoare_vars_tr", ts);
 
 fun hoare_tc_vars_tr ctxt [vars, pre, prg, post] =
       let val xs = vars_tr vars
-      in syntax_const ctxt #ValidTC $ assn_tr pre xs $ com_tr ctxt prg xs $ assn_tr post xs end
+          val (c',a) = com_tr ctxt prg xs
+      in syntax_const ctxt #ValidTC $ assn_tr pre xs $ c' $ a $ assn_tr post xs end
   | hoare_tc_vars_tr _ ts = raise TERM ("hoare_tc_vars_tr", ts);
 
 end;
 
 
 
 (** print translation **)
 
 local
 
 fun dest_abstuple
       (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (v, _, body)) =
         subst_bound (Syntax.free v, dest_abstuple body)
   | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
   | dest_abstuple tm = tm;
 
 fun abs2list (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
   | abs2list (Abs (x, T, _)) = [Free (x, T)]
   | abs2list _ = [];
 
 fun mk_ts (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (_, _, t)) = mk_ts t
   | mk_ts (Abs (_, _, t)) = mk_ts t
   | mk_ts (Const (\<^const_syntax>\<open>Pair\<close>, _) $ a $ b) = a :: mk_ts b
   | mk_ts t = [t];
 
 fun mk_vts (Const (\<^const_syntax>\<open>case_prod\<close>,_) $ Abs (x, _, t)) =
       (Syntax.free x :: abs2list t, mk_ts t)
   | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
   | mk_vts _ = raise Match;
 
 fun find_ch [] _ _ = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))  (* FIXME no_ch!? *)
   | find_ch ((v, t) :: vts) i xs =
       if t = Bound i then find_ch vts (i - 1) xs
       else (true, (v, subst_bounds (xs, t)));
 
 fun is_f (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs _) = true
   | is_f (Abs _) = true
   | is_f _ = false;
 
 
 (* assn_tr' & bexp_tr'*)
 
 fun assn_tr' (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T) = dest_abstuple T
   | assn_tr' (Const (\<^const_syntax>\<open>inter\<close>, _) $
         (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T1) $ (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T2)) =
       Syntax.const \<^const_syntax>\<open>inter\<close> $ dest_abstuple T1 $ dest_abstuple T2
   | assn_tr' t = t;
 
 fun bexp_tr' (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T) = dest_abstuple T
   | bexp_tr' t = t;
 
-fun var_tr' (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T) = dest_abstuple T
-  | var_tr' t = t;
+fun var_tr' xo T =
+  let val n = dest_abstuple T
+  in case xo of NONE => n | SOME x => Syntax.const \<^const_syntax>\<open>HOL.eq\<close> $ Syntax.free x $ n end
 
 
 (* com_tr' *)
 
 fun mk_assign ctxt f =
   let
     val (vs, ts) = mk_vts f;
     val (ch, (a, b)) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
   in
     if ch
     then Syntax.const \<^syntax_const>\<open>_assign\<close> $ a $ b
     else syntax_const ctxt #Skip
   end;
 
-fun com_tr' ctxt t =
+fun com_tr' ctxt (t,a) =
   let
     val (head, args) = apfst (try (#1 o Term.dest_Const)) (Term.strip_comb t);
     fun arg k = nth args (k - 1);
     val n = length args;
+    val (_, args_a) = apfst (try (#1 o Term.dest_Const)) (Term.strip_comb a);
+    fun arg_a k = nth args_a (k - 1)
   in
-    (case head of
+    case head of
       NONE => t
     | SOME c =>
         if c = const_syntax ctxt #Basic andalso n = 1 andalso is_f (arg 1) then
           mk_assign ctxt (arg 1)
         else if c = const_syntax ctxt #Seq andalso n = 2 then
-          Syntax.const \<^syntax_const>\<open>_Seq\<close> $ com_tr' ctxt (arg 1) $ com_tr' ctxt (arg 2)
+          Syntax.const \<^syntax_const>\<open>_Seq\<close>
+            $ com_tr' ctxt (arg 1, arg_a 1) $ com_tr' ctxt (arg 2, arg_a 2)
         else if c = const_syntax ctxt #Cond andalso n = 3 then
           Syntax.const \<^syntax_const>\<open>_Cond\<close> $
-            bexp_tr' (arg 1) $ com_tr' ctxt (arg 2) $ com_tr' ctxt (arg 3)
-        else if c = const_syntax ctxt #While andalso n = 4 then
-          Syntax.const \<^syntax_const>\<open>_While\<close> $
-            bexp_tr' (arg 1) $ assn_tr' (arg 2) $ var_tr' (arg 3) $ com_tr' ctxt (arg 4)
-        else t)
+            bexp_tr' (arg 1) $ com_tr' ctxt (arg 2, arg_a 1) $ com_tr' ctxt (arg 3, arg_a 2)
+        else if c = const_syntax ctxt #While andalso n = 2 then
+               let val (xo,a') = case arg_a 3 of
+                     Abs(x,_,a) => (if loose_bvar1(a,0) then SOME x else NONE,
+                                    subst_bound (Syntax.free x, a)) |
+                     t => (NONE,t)
+               in Syntax.const \<^syntax_const>\<open>_While\<close>
+                 $ bexp_tr' (arg 1) $ assn_tr' (arg_a 1) $ var_tr' xo (arg_a 2) $ com_tr' ctxt (arg 2, a')
+               end
+        else t
   end;
 
 in
 
-fun spec_tr' syn ctxt [p, c, q] =
-  Syntax.const syn $ assn_tr' p $ com_tr' ctxt c $ assn_tr' q;
+fun spec_tr' syn ctxt [p, c, a, q] =
+  Syntax.const syn $ assn_tr' p $ com_tr' ctxt (c,a) $ assn_tr' q;
 
 end;
 
 
 (** setup **)
 
 val _ =
   Theory.setup
    (Sign.parse_translation
     [(\<^syntax_const>\<open>_hoare_vars\<close>, hoare_vars_tr),
      (\<^syntax_const>\<open>_hoare_vars_tc\<close>, hoare_tc_vars_tr)]);
 
 fun setup consts =
   Data.put (SOME consts) #>
   Sign.print_translation
    [(#Valid consts, spec_tr' \<^syntax_const>\<open>_hoare\<close>),
     (#ValidTC consts, spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>)];
 
 end;
diff --git a/src/HOL/Hoare/hoare_tac.ML b/src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML
+++ b/src/HOL/Hoare/hoare_tac.ML
@@ -1,234 +1,234 @@
 (*  Title:      HOL/Hoare/hoare_tac.ML
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Author:     Walter Guttmann (extension to total-correctness proofs)
 
 Derivation of the proof rules and, most importantly, the VCG tactic.
 *)
 
 signature HOARE_TAC =
 sig
   val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool ->
     int -> tactic
   val hoare_tac: Proof.context -> (int -> tactic) -> int -> tactic
   val hoare_tc_tac: Proof.context -> (int -> tactic) -> int -> tactic
 end;
 
 structure Hoare_Tac: HOARE_TAC =
 struct
 
 (*** The tactics ***)
 
 (*****************************************************************************)
 (** The function Mset makes the theorem                                     **)
 (** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}",        **)
 (** where (x1,...,xn) are the variables of the particular program we are    **)
 (** working on at the moment of the call                                    **)
 (*****************************************************************************)
 
 local
 
 (** maps (%x1 ... xn. t) to [x1,...,xn] **)
 fun abs2list \<^Const_>\<open>case_prod _ _ _ for \<open>Abs (x, T, t)\<close>\<close> = Free (x, T) :: abs2list t
   | abs2list (Abs (x, T, _)) = [Free (x, T)]
   | abs2list _ = [];
 
 (** maps {(x1,...,xn). t} to [x1,...,xn] **)
 fun mk_vars \<^Const_>\<open>Collect _ for T\<close> = abs2list T
   | mk_vars _ = [];
 
 (** abstraction of body over a tuple formed from a list of free variables.
 Types are also built **)
 fun mk_abstupleC [] body = absfree ("x", \<^Type>\<open>unit\<close>) body
   | mk_abstupleC [v] body = absfree (dest_Free v) body
   | mk_abstupleC (v :: w) body =
       let
         val (x, T) = dest_Free v;
         val z = mk_abstupleC w body;
         val T2 =
           (case z of
             Abs (_, T, _) => T
           | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
       in
         \<^Const>\<open>case_prod T T2 \<^Type>\<open>bool\<close> for \<open>absfree (x, T) z\<close>\<close>
       end;
 
 (** maps [x1,...,xn] to (x1,...,xn) and types**)
 fun mk_bodyC [] = \<^Const>\<open>Unity\<close>
   | mk_bodyC [x] = x
   | mk_bodyC (x :: xs) =
       let
         val (_, T) = dest_Free x;
         val z = mk_bodyC xs;
         val T2 =
           (case z of
             Free (_, T) => T
           | \<^Const_>\<open>Pair A B for _ _\<close> => \<^Type>\<open>prod A B\<close>);
      in \<^Const>\<open>Pair T T2 for x z\<close> end;
 
 (** maps a subgoal of the form:
     VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]
 **)
 fun get_vars c =
   let
     val d = Logic.strip_assums_concl c;
-    val Const _ $ pre $ _ $ _ = HOLogic.dest_Trueprop d;
+    val Const _ $ pre $ _ $ _ $ _ = HOLogic.dest_Trueprop d;
   in mk_vars pre end;
 
 fun mk_CollectC tm =
   let val \<^Type>\<open>fun t _\<close> = fastype_of tm;
   in \<^Const>\<open>Collect t for tm\<close> end;
 
 fun inclt ty = \<^Const>\<open>less_eq ty\<close>;
 
 in
 
 fun Mset ctxt prop =
   let
     val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())];
 
     val vars = get_vars prop;
     val varsT = fastype_of (mk_bodyC vars);
     val big_Collect =
       mk_CollectC (mk_abstupleC vars (Free (P, varsT --> \<^Type>\<open>bool\<close>) $ mk_bodyC vars));
     val small_Collect =
       mk_CollectC (Abs ("x", varsT, Free (P, varsT --> \<^Type>\<open>bool\<close>) $ Bound 0));
 
     val MsetT = fastype_of big_Collect;
     fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
     val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
     val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac ctxt 1);
  in (vars, th) end;
 
 end;
 
 
 (*****************************************************************************)
 (** Simplifying:                                                            **)
 (** Some useful lemmata, lists and simplification tactics to control which  **)
 (** theorems are used to simplify at each moment, so that the original      **)
 (** input does not suffer any unexpected transformation                     **)
 (*****************************************************************************)
 
 (**Simp_tacs**)
 
 fun before_set2pred_simp_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]);
 
 fun split_simp_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]);
 
 (*****************************************************************************)
 (** set_to_pred_tac transforms sets inclusion into predicates implication,  **)
 (** maintaining the original variable names.                                **)
 (** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1"              **)
 (** Subgoals containing intersections (A Int B) or complement sets (-A)     **)
 (** are first simplified by "before_set2pred_simp_tac", that returns only   **)
 (** subgoals of the form "{x. P x} <= {x. Q x}", which are easily           **)
 (** transformed.                                                            **)
 (** This transformation may solve very easy subgoals due to a ligth         **)
 (** simplification done by (split_all_tac)                                  **)
 (*****************************************************************************)
 
 fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
   before_set2pred_simp_tac ctxt i THEN_MAYBE
   EVERY [
     resolve_tac ctxt [subsetI] i,
     resolve_tac ctxt [CollectI] i,
     dresolve_tac ctxt [CollectD] i,
     TRY (split_all_tac ctxt i) THEN_MAYBE
      (rename_tac var_names i THEN
       full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]);
 
 (*******************************************************************************)
 (** basic_simp_tac is called to simplify all verification conditions. It does **)
 (** a light simplification by applying "mem_Collect_eq", then it calls        **)
 (** max_simp_tac, which solves subgoals of the form "A <= A",                 **)
 (** and transforms any other into predicates, applying then                   **)
 (** the tactic chosen by the user, which may solve the subgoal completely.    **)
 (*******************************************************************************)
 
 fun max_simp_tac ctxt var_names tac =
   FIRST' [resolve_tac ctxt [subset_refl],
     set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
 
 fun basic_simp_tac ctxt var_names tac =
   simp_tac
     (put_simpset HOL_basic_ss ctxt
       addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc])
   THEN_MAYBE' max_simp_tac ctxt var_names tac;
 
 
 (** hoare_rule_tac **)
 
 fun hoare_rule_tac ctxt (vars, Mlem) tac =
   let
     val get_thms = Proof_Context.get_thms ctxt;
     val var_names = map (fst o dest_Free) vars;
     fun wlp_tac i =
       resolve_tac ctxt (get_thms \<^named_theorems>\<open>SeqRule\<close>) i THEN rule_tac false (i + 1)
     and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*)
       ((wlp_tac i THEN rule_tac pre_cond i)
         ORELSE
         (FIRST [
           resolve_tac ctxt (get_thms \<^named_theorems>\<open>SkipRule\<close>) i,
           resolve_tac ctxt (get_thms \<^named_theorems>\<open>AbortRule\<close>) i,
           EVERY [
             resolve_tac ctxt (get_thms \<^named_theorems>\<open>BasicRule\<close>) i,
             resolve_tac ctxt [Mlem] i,
             split_simp_tac ctxt i],
           EVERY [
             resolve_tac ctxt (get_thms \<^named_theorems>\<open>CondRule\<close>) i,
             rule_tac false (i + 2),
             rule_tac false (i + 1)],
           EVERY [
             resolve_tac ctxt (get_thms \<^named_theorems>\<open>WhileRule\<close>) i,
             basic_simp_tac ctxt var_names tac (i + 2),
             rule_tac true (i + 1)]]
          THEN (
            if pre_cond then basic_simp_tac ctxt var_names tac i
            else resolve_tac ctxt [subset_refl] i)));
   in rule_tac end;
 
 
 (** tac is the tactic the user chooses to solve or simplify **)
 (** the final verification conditions                       **)
 
 fun hoare_tac ctxt tac = SUBGOAL (fn (goal, i) =>
   SELECT_GOAL (hoare_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
 
 
 (* total correctness rules *)
 
 fun hoare_tc_rule_tac ctxt (vars, Mlem) tac =
   let
     val get_thms = Proof_Context.get_thms ctxt;
     val var_names = map (fst o dest_Free) vars;
     fun wlp_tac i =
       resolve_tac ctxt (get_thms \<^named_theorems>\<open>SeqRuleTC\<close>) i THEN rule_tac false (i + 1)
     and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*)
       ((wlp_tac i THEN rule_tac pre_cond i)
         ORELSE
         (FIRST [
           resolve_tac ctxt (get_thms \<^named_theorems>\<open>SkipRuleTC\<close>) i,
           EVERY [
             resolve_tac ctxt (get_thms \<^named_theorems>\<open>BasicRuleTC\<close>) i,
             resolve_tac ctxt [Mlem] i,
             split_simp_tac ctxt i],
           EVERY [
             resolve_tac ctxt (get_thms \<^named_theorems>\<open>CondRuleTC\<close>) i,
             rule_tac false (i + 2),
             rule_tac false (i + 1)],
           EVERY [
             resolve_tac ctxt (get_thms \<^named_theorems>\<open>WhileRuleTC\<close>) i,
             basic_simp_tac ctxt var_names tac (i + 2),
             rule_tac true (i + 1)]]
          THEN (
            if pre_cond then basic_simp_tac ctxt var_names tac i
            else resolve_tac ctxt [subset_refl] i)));
   in rule_tac end;
 
 
 fun hoare_tc_tac ctxt tac = SUBGOAL (fn (goal, i) =>
   SELECT_GOAL (hoare_tc_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
 
 end;