diff --git a/src/HOL/IMP/Hoare_Total_EX.thy b/src/HOL/IMP/Hoare_Total_EX.thy
--- a/src/HOL/IMP/Hoare_Total_EX.thy
+++ b/src/HOL/IMP/Hoare_Total_EX.thy
@@ -1,142 +1,178 @@
 (* Author: Tobias Nipkow *)
 
 subsubsection "\<open>nat\<close>-Indexed Invariant"
 
 theory Hoare_Total_EX
 imports Hoare
 begin
 
 text\<open>This is the standard set of rules that you find in many publications.
 The While-rule is different from the one in Concrete Semantics in that the
 invariant is indexed by natural numbers and goes down by 1 with
 every iteration. The completeness proof is easier but the rule is harder
 to apply in program proofs.\<close>
 
 definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
   ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
 "\<Turnstile>\<^sub>t {P}c{Q}  \<longleftrightarrow>  (\<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t))"
 
 inductive
   hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
 where
 
 Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}"  |
 
 Assign:  "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}"  |
 
 Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \<turnstile>\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}"  |
 
 If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
   \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"  |
 
 While:
   "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {P (Suc n)} c {P n};
      \<forall>n s. P (Suc n) s \<longrightarrow> bval b s;  \<forall>s. P 0 s \<longrightarrow> \<not> bval b s \<rbrakk>
    \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. \<exists>n. P n s} WHILE b DO c {P 0}"  |
 
 conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
            \<turnstile>\<^sub>t {P'}c{Q'}"
 
 text\<open>Building in the consequence rule:\<close>
 
 lemma strengthen_pre:
   "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
 by (metis conseq)
 
 lemma weaken_post:
   "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
 by (metis conseq)
 
 lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
 by (simp add: strengthen_pre[OF _ Assign])
 
 text\<open>The soundness theorem:\<close>
 
 theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
 proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
   case (While P c b)
   have "P n s \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P 0 t" for n s
   proof(induction "n" arbitrary: s)
     case 0 thus ?case using While.hyps(3) WhileFalse by blast
   next
     case Suc
     thus ?case by (meson While.IH While.hyps(2) WhileTrue)
   qed
   thus ?case by auto
 next
   case If thus ?case by auto blast
 qed fastforce+
 
 
 definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where
 "wp\<^sub>t c Q  =  (\<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"
 
 lemma [simp]: "wp\<^sub>t SKIP Q = Q"
 by(auto intro!: ext simp: wpt_def)
 
 lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
 by(auto intro!: ext simp: wpt_def)
 
 lemma [simp]: "wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)"
 unfolding wpt_def
 apply(rule ext)
 apply auto
 done
 
 lemma [simp]:
  "wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q s)"
 apply(unfold wpt_def)
 apply(rule ext)
 apply auto
 done
 
 
 text\<open>Function \<open>wpw\<close> computes the weakest precondition of a While-loop
 that is unfolded a fixed number of times.\<close>
 
 fun wpw :: "bexp \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> assn \<Rightarrow> assn" where
 "wpw b c 0 Q s = (\<not> bval b s \<and> Q s)" |
 "wpw b c (Suc n) Q s = (bval b s \<and> (\<exists>s'. (c,s) \<Rightarrow> s' \<and>  wpw b c n Q s'))"
 
 lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> Q t \<Longrightarrow> \<exists>n. wpw b c n Q s"
 proof(induction "WHILE b DO c" s t rule: big_step_induct)
   case WhileFalse thus ?case using wpw.simps(1) by blast 
 next
   case WhileTrue thus ?case using wpw.simps(2) by blast
 qed
 
 lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
 proof (induction c arbitrary: Q)
   case SKIP show ?case by (auto intro:hoaret.Skip)
 next
   case Assign show ?case by (auto intro:hoaret.Assign)
 next
   case Seq thus ?case by (auto intro:hoaret.Seq)
 next
   case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
 next
   case (While b c)
   let ?w = "WHILE b DO c"
   have c1: "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> (\<exists>n. wpw b c n Q s)"
     unfolding wpt_def by (metis WHILE_Its)
   have c3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> Q s" by simp
   have w2: "\<forall>n s. wpw b c (Suc n) Q s \<longrightarrow> bval b s" by simp
   have w3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> \<not> bval b s" by simp
   have "\<turnstile>\<^sub>t {wpw b c (Suc n) Q} c {wpw b c n Q}" for n
   proof -
     have *: "\<forall>s. wpw b c (Suc n) Q s \<longrightarrow> (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c n Q t)" by simp
     show ?thesis by(rule strengthen_pre[OF * While.IH[of "wpw b c n Q", unfolded wpt_def]])
   qed
   from conseq[OF c1 hoaret.While[OF this w2 w3] c3]
   show ?case .
 qed
 
 theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
 apply(rule strengthen_pre[OF _ wpt_is_pre])
 apply(auto simp: hoare_tvalid_def wpt_def)
 done
 
 corollary hoaret_sound_complete: "\<turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> \<Turnstile>\<^sub>t {P}c{Q}"
 by (metis hoaret_sound hoaret_complete)
 
+text \<open>Two examples:\<close>
+
+lemma "\<turnstile>\<^sub>t 
+{\<lambda>s. \<exists>n. n = nat(s ''x'')}
+ WHILE Less (N 0) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N (-1))
+{\<lambda>s. s ''x'' \<le> 0}"
+apply(rule weaken_post)
+ apply(rule While)
+   apply(rule Assign')
+   apply auto
+done
+
+lemma "\<turnstile>\<^sub>t 
+{\<lambda>s. \<exists>n. n = nat(s ''x'')}
+ WHILE Less (N 0) (V ''x'')
+ DO (''x'' ::= Plus (V ''x'') (N (-1));;
+    (''y'' ::= V ''x'';;
+     WHILE Less (N 0) (V ''y'') DO ''y'' ::= Plus (V ''y'') (N (-1))))
+{\<lambda>s. s ''x'' \<le> 0}"
+apply(rule weaken_post)
+ apply(rule While)
+   defer
+   apply auto[3]
+apply(rule Seq)
+ prefer 2
+ apply(rule Seq)
+  prefer 2
+  apply(rule weaken_post)
+   apply(rule_tac P = "\<lambda>m s. n = nat(s ''x'') \<and> m = nat(s ''y'')" in While)
+     apply(rule Assign')
+     apply auto[4]
+ apply(rule Assign)
+apply(rule Assign')
+apply auto
+done
+
 end
diff --git a/src/HOL/IMP/Hoare_Total_EX2.thy b/src/HOL/IMP/Hoare_Total_EX2.thy
--- a/src/HOL/IMP/Hoare_Total_EX2.thy
+++ b/src/HOL/IMP/Hoare_Total_EX2.thy
@@ -1,193 +1,232 @@
 (* Author: Tobias Nipkow *)
 
 subsubsection "Hoare Logic for Total Correctness With Logical Variables"
 
 theory Hoare_Total_EX2
 imports Hoare
 begin
 
 text\<open>This is the standard set of rules that you find in many publications.
 In the while-rule, a logical variable is needed to remember the pre-value
 of the variant (an expression that decreases by one with each iteration).
 In this theory, logical variables are modeled explicitly.
 A simpler (but not quite as flexible) approach is found in theory \<open>Hoare_Total_EX\<close>:
 pre and post-condition are connected via a universally quantified HOL variable.\<close>
 
 type_synonym lvname = string
 type_synonym assn2 = "(lvname \<Rightarrow> nat) \<Rightarrow> state \<Rightarrow> bool"
 
 definition hoare_tvalid :: "assn2 \<Rightarrow> com \<Rightarrow> assn2 \<Rightarrow> bool"
   ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
 "\<Turnstile>\<^sub>t {P}c{Q}  \<longleftrightarrow>  (\<forall>l s. P l s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q l t))"
 
 inductive
   hoaret :: "assn2 \<Rightarrow> com \<Rightarrow> assn2 \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
 where
 
 Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}"  |
 
 Assign:  "\<turnstile>\<^sub>t {\<lambda>l s. P l (s[a/x])} x::=a {P}"  |
 
 Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \<turnstile>\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}" |
 
 If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>l s. P l s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>l s. P l s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
   \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" |
 
 While:
   "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>l. P (l(x := Suc(l(x))))} c {P};
      \<forall>l s. l x > 0 \<and> P l s \<longrightarrow> bval b s;
      \<forall>l s. l x = 0 \<and> P l s \<longrightarrow> \<not> bval b s \<rbrakk>
    \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>l s. \<exists>n. P (l(x:=n)) s} WHILE b DO c {\<lambda>l s. P (l(x := 0)) s}" |
 
 conseq: "\<lbrakk> \<forall>l s. P' l s \<longrightarrow> P l s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>l s. Q l s \<longrightarrow> Q' l s  \<rbrakk> \<Longrightarrow>
            \<turnstile>\<^sub>t {P'}c{Q'}"
 
 text\<open>Building in the consequence rule:\<close>
 
 lemma strengthen_pre:
   "\<lbrakk> \<forall>l s. P' l s \<longrightarrow> P l s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
 by (metis conseq)
 
 lemma weaken_post:
   "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>l s. Q l s \<longrightarrow> Q' l s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
 by (metis conseq)
 
 lemma Assign': "\<forall>l s. P l s \<longrightarrow> Q l (s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
 by (simp add: strengthen_pre[OF _ Assign])
 
 text\<open>The soundness theorem:\<close>
 
 theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
 proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
   case (While P x c b)
   have "\<lbrakk> l x = n; P l s \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P (l(x := 0)) t" for n l s
   proof(induction "n" arbitrary: l s)
     case 0 thus ?case using While.hyps(3) WhileFalse
       by (metis fun_upd_triv)
   next
     case Suc
     thus ?case using While.IH While.hyps(2) WhileTrue
       by (metis fun_upd_same fun_upd_triv fun_upd_upd zero_less_Suc)
   qed
   thus ?case by fastforce
 next
   case If thus ?case by auto blast
 qed fastforce+
 
 
 definition wpt :: "com \<Rightarrow> assn2 \<Rightarrow> assn2" ("wp\<^sub>t") where
 "wp\<^sub>t c Q  =  (\<lambda>l s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q l t)"
 
 lemma [simp]: "wp\<^sub>t SKIP Q = Q"
 by(auto intro!: ext simp: wpt_def)
 
 lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>l s. Q l (s(x := aval e s)))"
 by(auto intro!: ext simp: wpt_def)
 
 lemma wpt_Seq[simp]: "wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)"
 by (auto simp: wpt_def fun_eq_iff)
 
 lemma [simp]:
  "wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\<lambda>l s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q l s)"
 by (auto simp: wpt_def fun_eq_iff)
 
 
 text\<open>Function \<open>wpw\<close> computes the weakest precondition of a While-loop
 that is unfolded a fixed number of times.\<close>
 
 fun wpw :: "bexp \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> assn2 \<Rightarrow> assn2" where
 "wpw b c 0 Q l s = (\<not> bval b s \<and> Q l s)" |
 "wpw b c (Suc n) Q l s = (bval b s \<and> (\<exists>s'. (c,s) \<Rightarrow> s' \<and>  wpw b c n Q l s'))"
 
 lemma WHILE_Its:
   "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> Q l t \<Longrightarrow> \<exists>n. wpw b c n Q l s"
 proof(induction "WHILE b DO c" s t arbitrary: l rule: big_step_induct)
   case WhileFalse thus ?case using wpw.simps(1) by blast
 next
   case WhileTrue show ?case
     using wpw.simps(2) WhileTrue(1,2) WhileTrue(5)[OF WhileTrue(6)] by blast
 qed
 
 definition support :: "assn2 \<Rightarrow> string set" where
 "support P = {x. \<exists>l1 l2 s. (\<forall>y. y \<noteq> x \<longrightarrow> l1 y = l2 y) \<and> P l1 s \<noteq> P l2 s}"
 
 lemma support_wpt: "support (wp\<^sub>t c Q) \<subseteq> support Q"
 by(simp add: support_def wpt_def) blast
 
 
 lemma support_wpw0: "support (wpw b c n Q) \<subseteq> support Q"
 proof(induction n)
   case 0 show ?case by (simp add: support_def) blast
 next
   case Suc
   have 1: "support (\<lambda>l s. A s \<and> B l s) \<subseteq> support B" for A B
     by(auto simp: support_def)
   have 2: "support (\<lambda>l s. \<exists>s'. A s s' \<and> B l s') \<subseteq> support B" for A B
     by(auto simp: support_def) blast+
   from Suc 1 2 show ?case by simp (meson order_trans)
 qed
 
 lemma support_wpw_Un:
   "support (%l. wpw b c (l x) Q l) \<subseteq> insert x (UN n. support(wpw b c n Q))"
 using support_wpw0[of b c _ Q]
 apply(auto simp add: support_def subset_iff)
 apply metis
 apply metis
 done
 
 lemma support_wpw: "support (%l. wpw b c (l x) Q l) \<subseteq> insert x (support Q)"
 using support_wpw0[of b c _ Q] support_wpw_Un[of b c _ Q]
 by blast
 
 lemma assn2_lupd: "x \<notin> support Q \<Longrightarrow> Q (l(x:=n)) = Q l"
 by(simp add: support_def fun_upd_other fun_eq_iff)
   (metis (no_types, lifting) fun_upd_def)
 
 abbreviation "new Q \<equiv> SOME x. x \<notin> support Q"
 
 lemma wpw_lupd: "x \<notin> support Q \<Longrightarrow> wpw b c n Q (l(x := u)) = wpw b c n Q l"
 by(induction n) (auto simp: assn2_lupd fun_eq_iff)
 
 lemma wpt_is_pre: "finite(support Q) \<Longrightarrow> \<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
 proof (induction c arbitrary: Q)
   case SKIP show ?case by (auto intro:hoaret.Skip)
 next
   case Assign show ?case by (auto intro:hoaret.Assign)
 next
   case (Seq c1 c2) show ?case
     by (auto intro:hoaret.Seq Seq finite_subset[OF support_wpt])
 next
   case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
 next
   case (While b c)
   let ?x = "new Q"
   have "\<exists>x. x \<notin> support Q" using While.prems infinite_UNIV_listI
     using ex_new_if_finite by blast
   hence [simp]: "?x \<notin> support Q" by (rule someI_ex)
   let ?w = "WHILE b DO c"
   have fsup: "finite (support (\<lambda>l. wpw b c (l x) Q l))" for x
     using finite_subset[OF support_wpw] While.prems by simp
   have c1: "\<forall>l s. wp\<^sub>t ?w Q l s \<longrightarrow> (\<exists>n. wpw b c n Q l s)"
     unfolding wpt_def by (metis WHILE_Its)
   have c2: "\<forall>l s. l ?x = 0 \<and> wpw b c (l ?x) Q l s \<longrightarrow> \<not> bval b s"
     by (simp cong: conj_cong)
   have w2: "\<forall>l s. 0 < l ?x \<and> wpw b c (l ?x) Q l s \<longrightarrow> bval b s"
     by (auto simp: gr0_conv_Suc cong: conj_cong)
   have 1: "\<forall>l s. wpw b c (Suc(l ?x)) Q l s \<longrightarrow>
                   (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c (l ?x) Q l t)"
     by simp
   have *: "\<turnstile>\<^sub>t {\<lambda>l. wpw b c (Suc (l ?x)) Q l} c {\<lambda>l. wpw b c (l ?x) Q l}"
     by(rule strengthen_pre[OF 1
           While.IH[of "\<lambda>l. wpw b c (l ?x) Q l", unfolded wpt_def, OF fsup]])
   show ?case
   apply(rule conseq[OF _ hoaret.While[OF _ w2 c2]])
     apply (simp_all add: c1 * assn2_lupd wpw_lupd del: wpw.simps(2))
   done
 qed
 
 theorem hoaret_complete: "finite(support Q) \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
 apply(rule strengthen_pre[OF _ wpt_is_pre])
 apply(auto simp: hoare_tvalid_def wpt_def)
 done
 
+
+text \<open>Two examples:\<close>
+
+lemma "\<turnstile>\<^sub>t 
+{\<lambda>l s. l ''x'' = nat(s ''x'')}
+ WHILE Less (N 0) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N (-1))
+{\<lambda>l s. s ''x'' \<le> 0}"
+apply(rule conseq)
+prefer 2
+ apply(rule While[where P = "\<lambda>l s. l ''x'' = nat(s ''x'')" and x = "''x''"])
+   apply(rule Assign')
+   apply auto
+done
+
+lemma "\<turnstile>\<^sub>t 
+{\<lambda>l s. l ''x'' = nat(s ''x'')}
+ WHILE Less (N 0) (V ''x'')
+ DO (''x'' ::= Plus (V ''x'') (N (-1));;
+    (''y'' ::= V ''x'';;
+     WHILE Less (N 0) (V ''y'') DO ''y'' ::= Plus (V ''y'') (N (-1))))
+{\<lambda>l s. s ''x'' \<le> 0}"
+apply(rule conseq)
+prefer 2
+ apply(rule While[where P = "\<lambda>l s. l ''x'' = nat(s ''x'')" and x = "''x''"])
+   defer
+   apply auto
+apply(rule Seq)
+ prefer 2
+ apply(rule Seq)
+  prefer 2
+  apply(rule weaken_post)
+   apply(rule_tac P = "\<lambda>l s. l ''x'' = nat(s ''x'') \<and> l ''y'' = nat(s ''y'')" and x = "''y''" in While)
+     apply(rule Assign')
+     apply auto[4]
+ apply(rule Assign)
+apply(rule Assign')
+apply auto
+done
+
 end
diff --git a/src/HOL/IMP/VCG_Total_EX2.thy b/src/HOL/IMP/VCG_Total_EX2.thy
--- a/src/HOL/IMP/VCG_Total_EX2.thy
+++ b/src/HOL/IMP/VCG_Total_EX2.thy
@@ -1,134 +1,155 @@
 (* Author: Tobias Nipkow *)
 
 subsubsection "VCG for Total Correctness With Logical Variables"
 
 theory VCG_Total_EX2
 imports Hoare_Total_EX2
 begin
 
 text \<open>
 Theory \<open>VCG_Total_EX\<close> conatins a VCG built on top of a Hoare logic without logical variables.
 As a result the completeness proof runs into a problem. This theory uses a Hoare logic
 with logical variables and proves soundness and completeness.
 \<close>
 
 text\<open>Annotated commands: commands where loops are annotated with
 invariants.\<close>
 
 datatype acom =
   Askip                  ("SKIP") |
   Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
   Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |
   Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
   Awhile assn2 lvname bexp acom
     ("({_'/_}/ WHILE _/ DO _)"  [0, 0, 0, 61] 61)
 
 notation com.SKIP ("SKIP")
 
 text\<open>Strip annotations:\<close>
 
 fun strip :: "acom \<Rightarrow> com" where
 "strip SKIP = SKIP" |
 "strip (x ::= a) = (x ::= a)" |
 "strip (C\<^sub>1;; C\<^sub>2) = (strip C\<^sub>1;; strip C\<^sub>2)" |
 "strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" |
 "strip ({_/_} WHILE b DO C) = (WHILE b DO strip C)"
 
 text\<open>Weakest precondition from annotated commands:\<close>
 
 fun pre :: "acom \<Rightarrow> assn2 \<Rightarrow> assn2" where
 "pre SKIP Q = Q" |
 "pre (x ::= a) Q = (\<lambda>l s. Q l (s(x := aval a s)))" |
 "pre (C\<^sub>1;; C\<^sub>2) Q = pre C\<^sub>1 (pre C\<^sub>2 Q)" |
 "pre (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q =
   (\<lambda>l s. if bval b s then pre C\<^sub>1 Q l s else pre C\<^sub>2 Q l s)" |
 "pre ({I/x} WHILE b DO C) Q = (\<lambda>l s. \<exists>n. I (l(x:=n)) s)"
 
 text\<open>Verification condition:\<close>
 
 fun vc :: "acom \<Rightarrow> assn2 \<Rightarrow> bool" where
 "vc SKIP Q = True" |
 "vc (x ::= a) Q = True" |
 "vc (C\<^sub>1;; C\<^sub>2) Q = (vc C\<^sub>1 (pre C\<^sub>2 Q) \<and> vc C\<^sub>2 Q)" |
 "vc (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = (vc C\<^sub>1 Q \<and> vc C\<^sub>2 Q)" |
 "vc ({I/x} WHILE b DO C) Q =
   (\<forall>l s. (I (l(x:=Suc(l x))) s \<longrightarrow> pre C I l s) \<and>
        (l x > 0 \<and> I l s \<longrightarrow> bval b s) \<and>
        (I (l(x := 0)) s \<longrightarrow> \<not> bval b s \<and> Q l s) \<and>
        vc C I)"
 
 lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C Q} strip C {Q}"
 proof(induction C arbitrary: Q)
   case (Awhile I x b C)
   show ?case
   proof(simp, rule weaken_post[OF While[of I x]], goal_cases)
     case 1 show ?case
       using Awhile.IH[of "I"] Awhile.prems by (auto intro: strengthen_pre)
   next
     case 3 show ?case
       using Awhile.prems by (simp) (metis fun_upd_triv)
   qed (insert Awhile.prems, auto)
 qed (auto intro: conseq Seq If simp: Skip Assign)
 
 
 text\<open>Completeness:\<close>
 
 lemma pre_mono:
   "\<forall>l s. P l s \<longrightarrow> P' l s \<Longrightarrow> pre C P l s \<Longrightarrow> pre C P' l s"
 proof (induction C arbitrary: P P' l s)
   case Aseq thus ?case by simp metis
 qed simp_all
 
 lemma vc_mono:
   "\<forall>l s. P l s \<longrightarrow> P' l s \<Longrightarrow> vc C P \<Longrightarrow> vc C P'"
 proof(induction C arbitrary: P P')
   case Aseq thus ?case by simp (metis pre_mono)
 qed simp_all
 
 lemma vc_complete:
  "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<exists>C. strip C = c \<and> vc C Q \<and> (\<forall>l s. P l s \<longrightarrow> pre C Q l s)"
   (is "_ \<Longrightarrow> \<exists>C. ?G P c Q C")
 proof (induction rule: hoaret.induct)
   case Skip
   show ?case (is "\<exists>C. ?C C")
   proof show "?C Askip" by simp qed
 next
   case (Assign P a x)
   show ?case (is "\<exists>C. ?C C")
   proof show "?C(Aassign x a)" by simp qed
 next
   case (Seq P c1 Q c2 R)
   from Seq.IH obtain C1 where ih1: "?G P c1 Q C1" by blast
   from Seq.IH obtain C2 where ih2: "?G Q c2 R C2" by blast
   show ?case (is "\<exists>C. ?C C")
   proof
     show "?C(Aseq C1 C2)"
       using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)
   qed
 next
   case (If P b c1 Q c2)
   from If.IH obtain C1 where ih1: "?G (\<lambda>l s. P l s \<and> bval b s) c1 Q C1"
     by blast
   from If.IH obtain C2 where ih2: "?G (\<lambda>l s. P l s \<and> \<not>bval b s) c2 Q C2"
     by blast
   show ?case (is "\<exists>C. ?C C")
   proof
     show "?C(Aif b C1 C2)" using ih1 ih2 by simp
   qed
 next
   case (While P x c b)
   from While.IH obtain C where
     ih: "?G (\<lambda>l s. P (l(x:=Suc(l x))) s \<and> bval b s) c P C"
     by blast
   show ?case (is "\<exists>C. ?C C")
   proof
     have "vc ({P/x} WHILE b DO C) (\<lambda>l. P (l(x := 0)))"
       using ih While.hyps(2,3)
       by simp (metis fun_upd_same zero_less_Suc)
     thus "?C(Awhile P x b C)" using ih by simp
  qed
 next
   case conseq thus ?case by(fast elim!: pre_mono vc_mono)
 qed
 
+
+text \<open>Two examples:\<close>
+
+lemma vc1: "vc
+ ({\<lambda>l s. l ''x'' = nat(s ''x'') / ''x''} WHILE Less (N 0) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N (-1)))
+ (\<lambda>l s. s ''x'' \<le> 0)"
+by auto
+
+thm vc_sound[OF vc1, simplified]
+
+lemma vc2: "vc 
+ ({\<lambda>l s. l ''x'' = nat(s ''x'') / ''x''} WHILE Less (N 0) (V ''x'')
+ DO (''x'' ::= Plus (V ''x'') (N (-1));;
+    (''y'' ::= V ''x'';;
+     {\<lambda>l s. l ''x'' = nat(s ''x'') \<and> l ''y'' = nat(s ''y'') / ''y''}
+     WHILE Less (N 0) (V ''y'') DO ''y'' ::= Plus (V ''y'') (N (-1)))))
+(\<lambda>l s. s ''x'' \<le> 0)"
+by auto
+
+thm vc_sound[OF vc2, simplified]
+
 end