# HG changeset patch
# User nipkow
# Date 1634065063 -7200
# Node ID 403ce50e6a2a31175ae8e21f6b02478e71983c28
# Parent  40f03761f77fe265bd8c898022c73ec3dd9b9cb9
separated commands from annotations to be able to abstract about the latter only

diff -r 40f03761f77f -r 403ce50e6a2a src/HOL/Hoare/ExamplesTC.thy
--- a/src/HOL/Hoare/ExamplesTC.thy	Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/ExamplesTC.thy	Tue Oct 12 20:57:43 2021 +0200
@@ -27,7 +27,7 @@
 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;
@@ -84,7 +84,7 @@
   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
@@ -113,4 +113,21 @@
     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 -r 40f03761f77f -r 403ce50e6a2a src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Tue Oct 12 20:57:43 2021 +0200
@@ -20,13 +20,12 @@
 
 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"
 
@@ -38,15 +37,15 @@
 | "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'"
@@ -64,37 +63,37 @@
 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
@@ -104,25 +103,25 @@
 
 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)"
@@ -133,18 +132,18 @@
 
 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}"
@@ -153,13 +152,13 @@
           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
diff -r 40f03761f77f -r 403ce50e6a2a src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Tue Oct 12 20:57:43 2021 +0200
@@ -19,7 +19,7 @@
 | 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"
 
@@ -34,10 +34,10 @@
 | "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'"
@@ -54,45 +54,45 @@
     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
@@ -100,32 +100,32 @@
 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)"
@@ -136,18 +136,18 @@
 
 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}"
@@ -156,13 +156,13 @@
           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
diff -r 40f03761f77f -r 403ce50e6a2a src/HOL/Hoare/Hoare_Syntax.thy
--- a/src/HOL/Hoare/Hoare_Syntax.thy	Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/Hoare_Syntax.thy	Tue Oct 12 20:57:43 2021 +0200
@@ -15,10 +15,18 @@
   "_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)
@@ -27,6 +35,18 @@
  "_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 -r 40f03761f77f -r 403ce50e6a2a src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy	Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy	Tue Oct 12 20:57:43 2021 +0200
@@ -219,10 +219,11 @@
       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
@@ -252,8 +253,8 @@
       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+        
diff -r 40f03761f77f -r 403ce50e6a2a src/HOL/Hoare/hoare_syntax.ML
--- a/src/HOL/Hoare/hoare_syntax.ML	Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/hoare_syntax.ML	Tue Oct 12 20:57:43 2021 +0200
@@ -1,6 +1,7 @@
 (*  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.
 *)
@@ -84,14 +85,34 @@
 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
@@ -101,12 +122,14 @@
 
 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;
@@ -158,8 +181,9 @@
 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' *)
@@ -174,32 +198,40 @@
     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;
 
diff -r 40f03761f77f -r 403ce50e6a2a src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML	Tue Oct 12 20:57:43 2021 +0200
@@ -71,7 +71,7 @@
 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 =