# HG changeset patch
# User Peter Lammich
# Date 1607102469 0
# Node ID 64d8a7e6d8fa596c6272222523fa0cbdfe91a9b5
# Parent  ba65dc3e35af7693f5711428a3e30a891c9e8cf4# Parent  ea189da0ff604ca602b4a2b24bec59ef8e77b8e8
merged

diff -r ba65dc3e35af -r 64d8a7e6d8fa CONTRIBUTORS
--- a/CONTRIBUTORS	Fri Dec 04 17:20:41 2020 +0000
+++ b/CONTRIBUTORS	Fri Dec 04 17:21:09 2020 +0000
@@ -5,6 +5,9 @@
 
 Contributions to this Isabelle version
 --------------------------------------
+* December 2020 Walter Guttmann
+  Extension of session HOL/Hoare with total correctness proof system
+
 * November 2020: Stepan Holub
   Removed preconditions from lemma comm_append_are_replicate
 
diff -r ba65dc3e35af -r 64d8a7e6d8fa src/HOL/Data_Structures/Tree23_Map.thy
--- a/src/HOL/Data_Structures/Tree23_Map.thy	Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Data_Structures/Tree23_Map.thy	Fri Dec 04 17:21:09 2020 +0000
@@ -98,14 +98,14 @@
 
 subsection \<open>Balancedness\<close>
 
-lemma complete_upd: "complete t \<Longrightarrow> complete (treeI(upd x y t)) \<and> height(upd x y t) = height t"
+lemma complete_upd: "complete t \<Longrightarrow> complete (treeI(upd x y t)) \<and> hI(upd x y t) = height t"
 by (induct t) (auto split!: if_split upI.split)(* 16 secs in 2015 *)
 
 corollary complete_update: "complete t \<Longrightarrow> complete (update x y t)"
 by (simp add: update_def complete_upd)
 
 
-lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t"
+lemma height_del: "complete t \<Longrightarrow> hD(del x t) = height t"
 by(induction x t rule: del.induct)
   (auto simp add: heights max_def height_split_min split: prod.split)
 
diff -r ba65dc3e35af -r 64d8a7e6d8fa src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Fri Dec 04 17:21:09 2020 +0000
@@ -45,7 +45,7 @@
         (case ins x l of
            TI l' => TI (Node2 l' a r) |
            OF l1 b l2 => TI (Node3 l1 b l2 a r)) |
-      EQ \<Rightarrow> TI (Node2 l x r) |
+      EQ \<Rightarrow> TI (Node2 l a r) |
       GT \<Rightarrow>
         (case ins x r of
            TI r' => TI (Node2 l a r') |
@@ -210,18 +210,11 @@
 
 text\<open>First a standard proof that \<^const>\<open>ins\<close> preserves \<^const>\<open>complete\<close>.\<close>
 
-instantiation upI :: (type)height
-begin
+fun hI :: "'a upI \<Rightarrow> nat" where
+"hI (TI t) = height t" |
+"hI (OF l a r) = height l"
 
-fun height_upI :: "'a upI \<Rightarrow> nat" where
-"height (TI t) = height t" |
-"height (OF l a r) = height l"
-
-instance ..
-
-end
-
-lemma complete_ins: "complete t \<Longrightarrow> complete (treeI(ins a t)) \<and> height(ins a t) = height t"
+lemma complete_ins: "complete t \<Longrightarrow> complete (treeI(ins a t)) \<and> hI(ins a t) = height t"
 by (induct t) (auto split!: if_split upI.split) (* 15 secs in 2015 *)
 
 text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
@@ -290,37 +283,30 @@
 
 subsection "Proofs for delete"
 
-instantiation upD :: (type)height
-begin
-
-fun height_upD :: "'a upD \<Rightarrow> nat" where
-"height (TD t) = height t" |
-"height (UF t) = height t + 1"
-
-instance ..
-
-end
+fun hD :: "'a upD \<Rightarrow> nat" where
+"hD (TD t) = height t" |
+"hD (UF t) = height t + 1"
 
 lemma complete_treeD_node21:
-  "\<lbrakk>complete r; complete (treeD l'); height r = height l' \<rbrakk> \<Longrightarrow> complete (treeD (node21 l' a r))"
+  "\<lbrakk>complete r; complete (treeD l'); height r = hD l' \<rbrakk> \<Longrightarrow> complete (treeD (node21 l' a r))"
 by(induct l' a r rule: node21.induct) auto
 
 lemma complete_treeD_node22:
-  "\<lbrakk>complete(treeD r'); complete l; height r' = height l \<rbrakk> \<Longrightarrow> complete (treeD (node22 l a r'))"
+  "\<lbrakk>complete(treeD r'); complete l; hD r' = height l \<rbrakk> \<Longrightarrow> complete (treeD (node22 l a r'))"
 by(induct l a r' rule: node22.induct) auto
 
 lemma complete_treeD_node31:
-  "\<lbrakk> complete (treeD l'); complete m; complete r; height l' = height r; height m = height r \<rbrakk>
+  "\<lbrakk> complete (treeD l'); complete m; complete r; hD l' = height r; height m = height r \<rbrakk>
   \<Longrightarrow> complete (treeD (node31 l' a m b r))"
 by(induct l' a m b r rule: node31.induct) auto
 
 lemma complete_treeD_node32:
-  "\<lbrakk> complete l; complete (treeD m'); complete r; height l = height r; height m' = height r \<rbrakk>
+  "\<lbrakk> complete l; complete (treeD m'); complete r; height l = height r; hD m' = height r \<rbrakk>
   \<Longrightarrow> complete (treeD (node32 l a m' b r))"
 by(induct l a m' b r rule: node32.induct) auto
 
 lemma complete_treeD_node33:
-  "\<lbrakk> complete l; complete m; complete(treeD r'); height l = height r'; height m = height r' \<rbrakk>
+  "\<lbrakk> complete l; complete m; complete(treeD r'); height l = hD r'; height m = hD r' \<rbrakk>
   \<Longrightarrow> complete (treeD (node33 l a m b r'))"
 by(induct l a m b r' rule: node33.induct) auto
 
@@ -328,37 +314,37 @@
   complete_treeD_node31 complete_treeD_node32 complete_treeD_node33
 
 lemma height'_node21:
-   "height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1"
+   "height r > 0 \<Longrightarrow> hD(node21 l' a r) = max (hD l') (height r) + 1"
 by(induct l' a r rule: node21.induct)(simp_all)
 
 lemma height'_node22:
-   "height l > 0 \<Longrightarrow> height(node22 l a r') = max (height l) (height r') + 1"
+   "height l > 0 \<Longrightarrow> hD(node22 l a r') = max (height l) (hD r') + 1"
 by(induct l a r' rule: node22.induct)(simp_all)
 
 lemma height'_node31:
-  "height m > 0 \<Longrightarrow> height(node31 l a m b r) =
-   max (height l) (max (height m) (height r)) + 1"
+  "height m > 0 \<Longrightarrow> hD(node31 l a m b r) =
+   max (hD l) (max (height m) (height r)) + 1"
 by(induct l a m b r rule: node31.induct)(simp_all add: max_def)
 
 lemma height'_node32:
-  "height r > 0 \<Longrightarrow> height(node32 l a m b r) =
-   max (height l) (max (height m) (height r)) + 1"
+  "height r > 0 \<Longrightarrow> hD(node32 l a m b r) =
+   max (height l) (max (hD m) (height r)) + 1"
 by(induct l a m b r rule: node32.induct)(simp_all add: max_def)
 
 lemma height'_node33:
-  "height m > 0 \<Longrightarrow> height(node33 l a m b r) =
-   max (height l) (max (height m) (height r)) + 1"
+  "height m > 0 \<Longrightarrow> hD(node33 l a m b r) =
+   max (height l) (max (height m) (hD r)) + 1"
 by(induct l a m b r rule: node33.induct)(simp_all add: max_def)
 
 lemmas heights = height'_node21 height'_node22
   height'_node31 height'_node32 height'_node33
 
 lemma height_split_min:
-  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> complete t \<Longrightarrow> height t' = height t"
+  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> complete t \<Longrightarrow> hD t' = height t"
 by(induct t arbitrary: x t' rule: split_min.induct)
   (auto simp: heights split: prod.splits)
 
-lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t"
+lemma height_del: "complete t \<Longrightarrow> hD(del x t) = height t"
 by(induction x t rule: del.induct)
   (auto simp: heights max_def height_split_min split: prod.splits)
 
diff -r ba65dc3e35af -r 64d8a7e6d8fa src/HOL/Hoare/ExamplesTC.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/ExamplesTC.thy	Fri Dec 04 17:21:09 2020 +0000
@@ -0,0 +1,118 @@
+(* 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>
+
+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)}
+  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
+
+end
diff -r ba65dc3e35af -r 64d8a7e6d8fa src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/Hoare.thy	Fri Dec 04 17:21:09 2020 +0000
@@ -3,7 +3,7 @@
 *)
 
 theory Hoare
-imports Examples ExamplesAbort Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation
+imports Examples ExamplesAbort ExamplesTC Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation
 begin
 
 end
diff -r ba65dc3e35af -r 64d8a7e6d8fa src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Fri Dec 04 17:21:09 2020 +0000
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Hoare/Hoare_Logic.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   1998 TUM
+    Author:     Walter Guttmann (extension to total-correctness proofs)
 
 Sugared semantic embedding of Hoare logic.
 Strictly speaking a shallow embedding (as implemented by Norbert Galm
@@ -14,12 +15,19 @@
 
 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"               ("(_;/ _)"      [61,60] 60)
 | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
-| While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
+| While "'a bexp" "'a assn" "'a var" "'a com"  ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)"  [0,0,0,0] 61)
+
+syntax (xsymbols)
+  "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
+
+translations
+  "WHILE b INV {x} DO c OD" => "WHILE b INV {x} VAR {0} DO c OD"
 
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
@@ -31,17 +39,38 @@
 | "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
 | "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
 | "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
-| "s \<notin> b \<Longrightarrow> Sem (While b x c) s s"
-| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
-   Sem (While b x c) 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'"
 
 inductive_cases [elim!]:
   "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
   "Sem (IF b THEN c1 ELSE c2 FI) 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 \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q)"
+  where "Valid p c 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)"
 
+lemma tc_implies_pc:
+  "ValidTC p c q \<Longrightarrow> Valid p c 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"
+  by (metis ValidTC_def)
 
 syntax
   "_assign" :: "idt => 'b => 'a com"  ("(2_ :=/ _)" [70, 65] 61)
@@ -57,6 +86,16 @@
 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
 print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare\<close>))]\<close>
 
+syntax
+ "_hoare_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
+                    ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
+syntax ("" output)
+ "_hoare_tc"      :: "['a assn,'a com,'a assn] => bool"
+                    ("[_] // _ // [_]" [0,55,0] 50)
+
+parse_translation \<open>[(\<^syntax_const>\<open>_hoare_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close>
+print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>))]\<close>
+
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
 by (auto simp:Valid_def)
@@ -73,14 +112,14 @@
 by (auto simp:Valid_def)
 
 lemma While_aux:
-  assumes "Sem (WHILE b INV {i} DO c OD) s s'"
+  assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) 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 INV {i} DO c OD" s s') auto
+  by (induct "WHILE b INV {i} VAR {v} DO c OD" 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 c) q"
+ "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"
 apply (clarsimp simp:Valid_def)
 apply(drule While_aux)
   apply assumption
@@ -88,8 +127,73 @@
 apply blast
 done
 
+lemma SkipRuleTC:
+  assumes "p \<subseteq> q"
+    shows "ValidTC p (Basic id) q"
+  by (metis assms Sem.intros(1) ValidTC_def id_apply subsetD)
 
-lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}"
+lemma BasicRuleTC:
+  assumes "p \<subseteq> {s. f s \<in> q}"
+    shows "ValidTC p (Basic f) 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 (c1;c2) 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"
+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 "i \<inter> uminus b \<subseteq> q"
+    shows "ValidTC p (While b i v c) 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)"
+    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)"
+      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"
+          using 1 by auto
+        thus "\<exists>t . Sem (While b i v 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"
+          using Sem.intros(5) assms(3) by fastforce
+      qed
+    qed
+  }
+  thus ?thesis
+    using assms(1) ValidTC_def by force
+qed
+
+lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
   by blast
 
 lemmas AbortRule = SkipRule  \<comment> \<open>dummy version\<close>
@@ -104,4 +208,13 @@
     SIMPLE_METHOD' (Hoare.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.hoare_tc_tac ctxt (K all_tac)))\<close>
+  "verification condition generator"
+
+method_setup vcg_tc_simp = \<open>
+  Scan.succeed (fn ctxt =>
+    SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+  "verification condition generator plus simplification"
+
 end
diff -r ba65dc3e35af -r 64d8a7e6d8fa src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Fri Dec 04 17:21:09 2020 +0000
@@ -1,8 +1,9 @@
 (*  Title:      HOL/Hoare/Hoare_Logic_Abort.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   2003 TUM
+    Author:     Walter Guttmann (extension to total-correctness proofs)
 
-Like Hoare.thy, but with an Abort statement for modelling run time errors.
+Like Hoare_Logic.thy, but with an Abort statement for modelling run time errors.
 *)
 
 theory Hoare_Logic_Abort
@@ -11,13 +12,20 @@
 
 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"               ("(_;/ _)"      [61,60] 60)
 | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
-| While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
+| While "'a bexp" "'a assn" "'a var" "'a com"  ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)"  [0,0,0,0] 61)
+
+syntax (xsymbols)
+  "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
+
+translations
+  "WHILE b INV {x} DO c OD" => "WHILE b INV {x} VAR {0} DO c OD"
 
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
@@ -32,18 +40,39 @@
 | "Sem (IF b THEN c1 ELSE c2 FI) None None"
 | "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
 | "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
-| "Sem (While b x c) None None"
-| "s \<notin> b \<Longrightarrow> Sem (While b x c) (Some s) (Some s)"
-| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
-   Sem (While b x c) (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'"
 
 inductive_cases [elim!]:
   "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
   "Sem (IF b THEN c1 ELSE c2 FI) 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> Some ` p \<longrightarrow> s' \<in> Some ` q"
+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 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)"
+
+lemma tc_implies_pc:
+  "ValidTC p c q \<Longrightarrow> Valid p c q"
+  by (smt 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"
+  by (meson ValidTC_def)
 
 syntax
   "_assign" :: "idt => 'b => 'a com"  ("(2_ :=/ _)" [70, 65] 61)
@@ -57,11 +86,19 @@
 
 ML_file \<open>hoare_syntax.ML\<close>
 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
-print_translation
-  \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort\<close>))]\<close>
+print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort\<close>))]\<close>
 
+syntax
+ "_hoare_abort_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
+                          ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
+syntax ("" output)
+ "_hoare_abort_tc"      :: "['a assn,'a com,'a assn] => bool"
+                          ("[_] // _ // [_]" [0,55,0] 50)
 
-section \<open>The proof rules\<close>
+parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close>
+print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort_tc\<close>))]\<close>
+
+text \<open>The proof rules for partial correctness\<close>
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
 by (auto simp:Valid_def)
@@ -78,17 +115,15 @@
 by (fastforce simp:Valid_def image_def)
 
 lemma While_aux:
-  assumes "Sem (WHILE b INV {i} DO c OD) s s'"
+  assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) 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 INV {i} DO c OD" s s') auto
+  by (induct "WHILE b INV {i} VAR {v} DO c OD" 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 c) q"
-apply(simp add:Valid_def)
-apply(simp (no_asm) add:image_def)
-apply clarify
+ "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"
+apply (clarsimp simp:Valid_def)
 apply(drule While_aux)
   apply assumption
  apply blast
@@ -98,6 +133,74 @@
 lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort 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"
+  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"
+  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 (c1;c2) 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"
+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 "i \<inter> uminus b \<subseteq> q"
+    shows "ValidTC p (While b i v c) 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)"
+    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)"
+      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"
+          using 1 by auto
+        thus "\<exists>t . Sem (While b i v 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"
+          using Sem.intros(9) assms(3) by fastforce
+      qed
+    qed
+  }
+  thus ?thesis
+    using assms(1) ValidTC_def by force
+qed
+
 
 subsection \<open>Derivation of the proof rules and, most importantly, the VCG tactic\<close>
 
@@ -115,6 +218,15 @@
     SIMPLE_METHOD' (Hoare.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.hoare_tc_tac ctxt (K all_tac)))\<close>
+  "verification condition generator"
+
+method_setup vcg_tc_simp = \<open>
+  Scan.succeed (fn ctxt =>
+    SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+  "verification condition generator plus simplification"
+
 \<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)
diff -r ba65dc3e35af -r 64d8a7e6d8fa src/HOL/Hoare/README.html
--- a/src/HOL/Hoare/README.html	Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/README.html	Fri Dec 04 17:21:09 2020 +0000
@@ -62,6 +62,32 @@
 This is a logic of partial correctness. You can only prove that your program
 does the right thing <i>if</i> it terminates, but not <i>that</i> it
 terminates.
+A logic of total correctness is also provided and described below.
+
+<H3>Total correctness</H3>
+
+To prove termination, each WHILE-loop must be annotated with a variant:
+<UL>
+<LI> <kbd>WHILE _ INV {_} VAR {_} DO _ OD</kbd>
+</UL>
+A variant is an expression with type <kbd>nat</kbd>, which may use program
+variables and normal variables.
+<P>
+
+A total-correctness goal has the form
+<PRE>
+VARS x y ... [P] prog [Q]
+</PRE>
+enclosing the pre- and postcondition in square brackets.
+<P>
+
+Methods <kbd>vcg_tc</kbd> and <kbd>vcg_tc_simp</kbd> can be used to derive
+verification conditions.
+<P>
+
+From a total-correctness proof, a function can be extracted which
+for every input satisfying the precondition returns an output
+satisfying the postcondition.
 
 <H3>Notes on the implementation</H3>
 
diff -r ba65dc3e35af -r 64d8a7e6d8fa src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy	Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/SchorrWaite.thy	Fri Dec 04 17:21:09 2020 +0000
@@ -222,7 +222,7 @@
   (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}")
 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
+    {(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
diff -r ba65dc3e35af -r 64d8a7e6d8fa src/HOL/Hoare/hoare_syntax.ML
--- a/src/HOL/Hoare/hoare_syntax.ML	Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/hoare_syntax.ML	Fri Dec 04 17:21:09 2020 +0000
@@ -1,5 +1,6 @@
 (*  Title:      HOL/Hoare/hoare_syntax.ML
     Author:     Leonor Prensa Nieto & Tobias Nipkow
+    Author:     Walter Guttmann (extension to total-correctness proofs)
 
 Syntax translations for Hoare logic.
 *)
@@ -7,6 +8,7 @@
 signature HOARE_SYNTAX =
 sig
   val hoare_vars_tr: term list -> term
+  val hoare_tc_vars_tr: term list -> term
   val spec_tr': string -> term list -> term
 end;
 
@@ -47,6 +49,8 @@
 
 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 *)
 
@@ -57,8 +61,8 @@
       Syntax.const \<^const_syntax>\<open>Seq\<close> $ com_tr c1 xs $ com_tr c2 xs
   | com_tr (Const (\<^const_syntax>\<open>Cond\<close>,_) $ b $ c1 $ c2) xs =
       Syntax.const \<^const_syntax>\<open>Cond\<close> $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
-  | com_tr (Const (\<^const_syntax>\<open>While\<close>,_) $ b $ I $ c) xs =
-      Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
+  | com_tr (Const (\<^const_syntax>\<open>While\<close>,_) $ b $ I $ V $ c) xs =
+      Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr b xs $ assn_tr I xs $ var_tr V xs $ com_tr c xs
   | com_tr t _ = t;
 
 fun vars_tr (Const (\<^syntax_const>\<open>_idts\<close>, _) $ idt $ vars) = idt :: vars_tr vars
@@ -73,6 +77,13 @@
       end
   | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
 
+fun hoare_tc_vars_tr [vars, pre, prg, post] =
+      let val xs = vars_tr vars
+      in Syntax.const \<^const_syntax>\<open>ValidTC\<close> $
+         assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
+      end
+  | hoare_tc_vars_tr ts = raise TERM ("hoare_tc_vars_tr", ts);
+
 end;
 
 
@@ -122,6 +133,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;
+
 
 (* com_tr' *)
 
@@ -142,8 +156,8 @@
       Syntax.const \<^const_syntax>\<open>Seq\<close> $ com_tr' c1 $ com_tr' c2
   | com_tr' (Const (\<^const_syntax>\<open>Cond\<close>, _) $ b $ c1 $ c2) =
       Syntax.const \<^const_syntax>\<open>Cond\<close> $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
-  | com_tr' (Const (\<^const_syntax>\<open>While\<close>, _) $ b $ I $ c) =
-      Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr' b $ assn_tr' I $ com_tr' c
+  | com_tr' (Const (\<^const_syntax>\<open>While\<close>, _) $ b $ I $ V $ c) =
+      Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr' b $ assn_tr' I $ var_tr' V $ com_tr' c
   | com_tr' t = t;
 
 in
diff -r ba65dc3e35af -r 64d8a7e6d8fa src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/hoare_tac.ML	Fri Dec 04 17:21:09 2020 +0000
@@ -1,5 +1,6 @@
 (*  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.
 *)
@@ -9,6 +10,7 @@
   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: HOARE =
@@ -195,5 +197,39 @@
 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 var_names = map (fst o dest_Free) vars;
+    fun wlp_tac i =
+      resolve_tac ctxt @{thms SeqRuleTC} 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 @{thms SkipRuleTC} i,
+          EVERY [
+            resolve_tac ctxt @{thms BasicRuleTC} i,
+            resolve_tac ctxt [Mlem] i,
+            split_simp_tac ctxt i],
+          EVERY [
+            resolve_tac ctxt @{thms CondRuleTC} i,
+            rule_tac false (i + 2),
+            rule_tac false (i + 1)],
+          EVERY [
+            resolve_tac ctxt @{thms WhileRuleTC} 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;
 
diff -r ba65dc3e35af -r 64d8a7e6d8fa src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Isar_Examples/Hoare.thy	Fri Dec 04 17:21:09 2020 +0000
@@ -21,12 +21,13 @@
 
 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"    ("(_;/ _)" [60, 61] 60)
   | Cond "'a bexp" "'a com" "'a com"
-  | While "'a bexp" "'a assn" "'a com"
+  | While "'a bexp" "'a assn" "'a var" "'a com"
 
 abbreviation Skip  ("SKIP")
   where "SKIP \<equiv> Basic id"
@@ -43,7 +44,7 @@
     "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
   | "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
   | "Sem (Cond b c1 c2) s s' \<longleftrightarrow> (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
-  | "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
+  | "Sem (While b x y c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"  ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
   where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)"
@@ -147,10 +148,10 @@
 
 theorem while:
   assumes body: "\<turnstile> (P \<inter> b) c P"
-  shows "\<turnstile> P (While b X c) (P \<inter> -b)"
+  shows "\<turnstile> P (While b X Y c) (P \<inter> -b)"
 proof
   fix s s' assume s: "s \<in> P"
-  assume "Sem (While b X c) s s'"
+  assume "Sem (While b X Y c) s s'"
   then obtain n where "iter n b (Sem c) s s'" by auto
   from this and s show "s' \<in> P \<inter> -b"
   proof (induct n arbitrary: s)
@@ -207,7 +208,7 @@
   "B [a/\<acute>x]" \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
   "\<acute>x := a" \<rightharpoonup> "CONST Basic (_quote (\<acute>(_update_name x (\<lambda>_. a))))"
   "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
-  "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
+  "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i (\<lambda>_. 0) c"
   "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
 
 parse_translation \<open>
@@ -335,10 +336,10 @@
 
 text \<open>While statements --- with optional invariant.\<close>
 
-lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
+lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P V c) (P \<inter> -b)"
   by (rule while)
 
-lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)"
+lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined V c) (P \<inter> -b)"
   by (rule while)
 
 
@@ -387,7 +388,7 @@
   by (induct n) 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 c) q"
+    "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"
   apply (clarsimp simp: Valid_def)
   apply (drule iter_aux)
     prefer 2
@@ -400,6 +401,11 @@
   by blast
 
 lemmas AbortRule = SkipRule  \<comment> \<open>dummy version\<close>
+lemmas SeqRuleTC = SkipRule  \<comment> \<open>dummy version\<close>
+lemmas SkipRuleTC = SkipRule  \<comment> \<open>dummy version\<close>
+lemmas BasicRuleTC = SkipRule  \<comment> \<open>dummy version\<close>
+lemmas CondRuleTC = SkipRule  \<comment> \<open>dummy version\<close>
+lemmas WhileRuleTC = SkipRule  \<comment> \<open>dummy version\<close>
 
 ML_file \<open>~~/src/HOL/Hoare/hoare_tac.ML\<close>
 
diff -r ba65dc3e35af -r 64d8a7e6d8fa src/HOL/Isar_Examples/Hoare_Ex.thy
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Fri Dec 04 17:21:09 2020 +0000
@@ -280,7 +280,7 @@
     "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
   | "timeit (c1; c2) = (timeit c1; timeit c2)"
   | "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
-  | "timeit (While b iv c) = While b iv (timeit c)"
+  | "timeit (While b iv v c) = While b iv v (timeit c)"
 
 record tvars = tstate +
   I :: nat