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 "\nat\-Indexed Invariant" theory Hoare_Total_EX imports Hoare begin text\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.\ definition hoare_tvalid :: "assn \ com \ assn \ bool" ("\\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where "\\<^sub>t {P}c{Q} \ (\s. P s \ (\t. (c,s) \ t \ Q t))" inductive hoaret :: "assn \ com \ assn \ bool" ("\\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50) where Skip: "\\<^sub>t {P} SKIP {P}" | Assign: "\\<^sub>t {\s. P(s[a/x])} x::=a {P}" | Seq: "\ \\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \ \ \\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}" | If: "\ \\<^sub>t {\s. P s \ bval b s} c\<^sub>1 {Q}; \\<^sub>t {\s. P s \ \ bval b s} c\<^sub>2 {Q} \ \ \\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" | While: "\ \n::nat. \\<^sub>t {P (Suc n)} c {P n}; \n s. P (Suc n) s \ bval b s; \s. P 0 s \ \ bval b s \ \ \\<^sub>t {\s. \n. P n s} WHILE b DO c {P 0}" | conseq: "\ \s. P' s \ P s; \\<^sub>t {P}c{Q}; \s. Q s \ Q' s \ \ \\<^sub>t {P'}c{Q'}" text\Building in the consequence rule:\ lemma strengthen_pre: "\ \s. P' s \ P s; \\<^sub>t {P} c {Q} \ \ \\<^sub>t {P'} c {Q}" by (metis conseq) lemma weaken_post: "\ \\<^sub>t {P} c {Q}; \s. Q s \ Q' s \ \ \\<^sub>t {P} c {Q'}" by (metis conseq) lemma Assign': "\s. P s \ Q(s[a/x]) \ \\<^sub>t {P} x ::= a {Q}" by (simp add: strengthen_pre[OF _ Assign]) text\The soundness theorem:\ theorem hoaret_sound: "\\<^sub>t {P}c{Q} \ \\<^sub>t {P}c{Q}" proof(unfold hoare_tvalid_def, induction rule: hoaret.induct) case (While P c b) have "P n s \ \t. (WHILE b DO c, s) \ t \ 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 \ assn \ assn" ("wp\<^sub>t") where "wp\<^sub>t c Q = (\s. \t. (c,s) \ t \ 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 = (\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 = (\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\Function \wpw\ computes the weakest precondition of a While-loop that is unfolded a fixed number of times.\ fun wpw :: "bexp \ com \ nat \ assn \ assn" where "wpw b c 0 Q s = (\ bval b s \ Q s)" | "wpw b c (Suc n) Q s = (bval b s \ (\s'. (c,s) \ s' \ wpw b c n Q s'))" lemma WHILE_Its: "(WHILE b DO c,s) \ t \ Q t \ \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: "\\<^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: "\s. wp\<^sub>t ?w Q s \ (\n. wpw b c n Q s)" unfolding wpt_def by (metis WHILE_Its) have c3: "\s. wpw b c 0 Q s \ Q s" by simp have w2: "\n s. wpw b c (Suc n) Q s \ bval b s" by simp have w3: "\s. wpw b c 0 Q s \ \ bval b s" by simp have "\\<^sub>t {wpw b c (Suc n) Q} c {wpw b c n Q}" for n proof - have *: "\s. wpw b c (Suc n) Q s \ (\t. (c, s) \ t \ 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: "\\<^sub>t {P}c{Q} \ \\<^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: "\\<^sub>t {P}c{Q} \ \\<^sub>t {P}c{Q}" by (metis hoaret_sound hoaret_complete) +text \Two examples:\ + +lemma "\\<^sub>t +{\s. \n. n = nat(s ''x'')} + WHILE Less (N 0) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N (-1)) +{\s. s ''x'' \ 0}" +apply(rule weaken_post) + apply(rule While) + apply(rule Assign') + apply auto +done + +lemma "\\<^sub>t +{\s. \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)))) +{\s. s ''x'' \ 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 = "\m s. n = nat(s ''x'') \ 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\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 \Hoare_Total_EX\: pre and post-condition are connected via a universally quantified HOL variable.\ type_synonym lvname = string type_synonym assn2 = "(lvname \ nat) \ state \ bool" definition hoare_tvalid :: "assn2 \ com \ assn2 \ bool" ("\\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where "\\<^sub>t {P}c{Q} \ (\l s. P l s \ (\t. (c,s) \ t \ Q l t))" inductive hoaret :: "assn2 \ com \ assn2 \ bool" ("\\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50) where Skip: "\\<^sub>t {P} SKIP {P}" | Assign: "\\<^sub>t {\l s. P l (s[a/x])} x::=a {P}" | Seq: "\ \\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \ \ \\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}" | If: "\ \\<^sub>t {\l s. P l s \ bval b s} c\<^sub>1 {Q}; \\<^sub>t {\l s. P l s \ \ bval b s} c\<^sub>2 {Q} \ \ \\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" | While: "\ \\<^sub>t {\l. P (l(x := Suc(l(x))))} c {P}; \l s. l x > 0 \ P l s \ bval b s; \l s. l x = 0 \ P l s \ \ bval b s \ \ \\<^sub>t {\l s. \n. P (l(x:=n)) s} WHILE b DO c {\l s. P (l(x := 0)) s}" | conseq: "\ \l s. P' l s \ P l s; \\<^sub>t {P}c{Q}; \l s. Q l s \ Q' l s \ \ \\<^sub>t {P'}c{Q'}" text\Building in the consequence rule:\ lemma strengthen_pre: "\ \l s. P' l s \ P l s; \\<^sub>t {P} c {Q} \ \ \\<^sub>t {P'} c {Q}" by (metis conseq) lemma weaken_post: "\ \\<^sub>t {P} c {Q}; \l s. Q l s \ Q' l s \ \ \\<^sub>t {P} c {Q'}" by (metis conseq) lemma Assign': "\l s. P l s \ Q l (s[a/x]) \ \\<^sub>t {P} x ::= a {Q}" by (simp add: strengthen_pre[OF _ Assign]) text\The soundness theorem:\ theorem hoaret_sound: "\\<^sub>t {P}c{Q} \ \\<^sub>t {P}c{Q}" proof(unfold hoare_tvalid_def, induction rule: hoaret.induct) case (While P x c b) have "\ l x = n; P l s \ \ \t. (WHILE b DO c, s) \ t \ 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 \ assn2 \ assn2" ("wp\<^sub>t") where "wp\<^sub>t c Q = (\l s. \t. (c,s) \ t \ 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 = (\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 = (\l s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q l s)" by (auto simp: wpt_def fun_eq_iff) text\Function \wpw\ computes the weakest precondition of a While-loop that is unfolded a fixed number of times.\ fun wpw :: "bexp \ com \ nat \ assn2 \ assn2" where "wpw b c 0 Q l s = (\ bval b s \ Q l s)" | "wpw b c (Suc n) Q l s = (bval b s \ (\s'. (c,s) \ s' \ wpw b c n Q l s'))" lemma WHILE_Its: "(WHILE b DO c,s) \ t \ Q l t \ \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 \ string set" where "support P = {x. \l1 l2 s. (\y. y \ x \ l1 y = l2 y) \ P l1 s \ P l2 s}" lemma support_wpt: "support (wp\<^sub>t c Q) \ support Q" by(simp add: support_def wpt_def) blast lemma support_wpw0: "support (wpw b c n Q) \ support Q" proof(induction n) case 0 show ?case by (simp add: support_def) blast next case Suc have 1: "support (\l s. A s \ B l s) \ support B" for A B by(auto simp: support_def) have 2: "support (\l s. \s'. A s s' \ B l s') \ 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) \ 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) \ insert x (support Q)" using support_wpw0[of b c _ Q] support_wpw_Un[of b c _ Q] by blast lemma assn2_lupd: "x \ support Q \ 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 \ SOME x. x \ support Q" lemma wpw_lupd: "x \ support Q \ 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) \ \\<^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 "\x. x \ support Q" using While.prems infinite_UNIV_listI using ex_new_if_finite by blast hence [simp]: "?x \ support Q" by (rule someI_ex) let ?w = "WHILE b DO c" have fsup: "finite (support (\l. wpw b c (l x) Q l))" for x using finite_subset[OF support_wpw] While.prems by simp have c1: "\l s. wp\<^sub>t ?w Q l s \ (\n. wpw b c n Q l s)" unfolding wpt_def by (metis WHILE_Its) have c2: "\l s. l ?x = 0 \ wpw b c (l ?x) Q l s \ \ bval b s" by (simp cong: conj_cong) have w2: "\l s. 0 < l ?x \ wpw b c (l ?x) Q l s \ bval b s" by (auto simp: gr0_conv_Suc cong: conj_cong) have 1: "\l s. wpw b c (Suc(l ?x)) Q l s \ (\t. (c, s) \ t \ wpw b c (l ?x) Q l t)" by simp have *: "\\<^sub>t {\l. wpw b c (Suc (l ?x)) Q l} c {\l. wpw b c (l ?x) Q l}" by(rule strengthen_pre[OF 1 While.IH[of "\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) \ \\<^sub>t {P}c{Q} \ \\<^sub>t {P}c{Q}" apply(rule strengthen_pre[OF _ wpt_is_pre]) apply(auto simp: hoare_tvalid_def wpt_def) done + +text \Two examples:\ + +lemma "\\<^sub>t +{\l s. l ''x'' = nat(s ''x'')} + WHILE Less (N 0) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N (-1)) +{\l s. s ''x'' \ 0}" +apply(rule conseq) +prefer 2 + apply(rule While[where P = "\l s. l ''x'' = nat(s ''x'')" and x = "''x''"]) + apply(rule Assign') + apply auto +done + +lemma "\\<^sub>t +{\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)))) +{\l s. s ''x'' \ 0}" +apply(rule conseq) +prefer 2 + apply(rule While[where P = "\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 = "\l s. l ''x'' = nat(s ''x'') \ 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 \ Theory \VCG_Total_EX\ 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. \ text\Annotated commands: commands where loops are annotated with invariants.\ datatype acom = Askip ("SKIP") | Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) | Aseq acom acom ("_;;/ _" [60, 61] 60) | Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | Awhile assn2 lvname bexp acom ("({_'/_}/ WHILE _/ DO _)" [0, 0, 0, 61] 61) notation com.SKIP ("SKIP") text\Strip annotations:\ fun strip :: "acom \ com" where "strip SKIP = SKIP" | "strip (x ::= a) = (x ::= a)" | "strip (C\<^sub>1;; C\<^sub>2) = (strip C\<^sub>1;; strip C\<^sub>2)" | "strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" | "strip ({_/_} WHILE b DO C) = (WHILE b DO strip C)" text\Weakest precondition from annotated commands:\ fun pre :: "acom \ assn2 \ assn2" where "pre SKIP Q = Q" | "pre (x ::= a) Q = (\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 = (\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 = (\l s. \n. I (l(x:=n)) s)" text\Verification condition:\ fun vc :: "acom \ assn2 \ 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) \ vc C\<^sub>2 Q)" | "vc (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = (vc C\<^sub>1 Q \ vc C\<^sub>2 Q)" | "vc ({I/x} WHILE b DO C) Q = (\l s. (I (l(x:=Suc(l x))) s \ pre C I l s) \ (l x > 0 \ I l s \ bval b s) \ (I (l(x := 0)) s \ \ bval b s \ Q l s) \ vc C I)" lemma vc_sound: "vc C Q \ \\<^sub>t {pre C Q} strip C {Q}" proof(induction C arbitrary: Q) case (Awhile I x b C) show ?case proof(simp, rule weaken_post[OF While[of I x]], goal_cases) case 1 show ?case using Awhile.IH[of "I"] Awhile.prems by (auto intro: strengthen_pre) next case 3 show ?case using Awhile.prems by (simp) (metis fun_upd_triv) qed (insert Awhile.prems, auto) qed (auto intro: conseq Seq If simp: Skip Assign) text\Completeness:\ lemma pre_mono: "\l s. P l s \ P' l s \ pre C P l s \ 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: "\l s. P l s \ P' l s \ vc C P \ vc C P'" proof(induction C arbitrary: P P') case Aseq thus ?case by simp (metis pre_mono) qed simp_all lemma vc_complete: "\\<^sub>t {P}c{Q} \ \C. strip C = c \ vc C Q \ (\l s. P l s \ pre C Q l s)" (is "_ \ \C. ?G P c Q C") proof (induction rule: hoaret.induct) case Skip show ?case (is "\C. ?C C") proof show "?C Askip" by simp qed next case (Assign P a x) show ?case (is "\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 "\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 (\l s. P l s \ bval b s) c1 Q C1" by blast from If.IH obtain C2 where ih2: "?G (\l s. P l s \ \bval b s) c2 Q C2" by blast show ?case (is "\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 (\l s. P (l(x:=Suc(l x))) s \ bval b s) c P C" by blast show ?case (is "\C. ?C C") proof have "vc ({P/x} WHILE b DO C) (\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 \Two examples:\ + +lemma vc1: "vc + ({\l s. l ''x'' = nat(s ''x'') / ''x''} WHILE Less (N 0) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N (-1))) + (\l s. s ''x'' \ 0)" +by auto + +thm vc_sound[OF vc1, simplified] + +lemma vc2: "vc + ({\l s. l ''x'' = nat(s ''x'') / ''x''} WHILE Less (N 0) (V ''x'') + DO (''x'' ::= Plus (V ''x'') (N (-1));; + (''y'' ::= V ''x'';; + {\l s. l ''x'' = nat(s ''x'') \ l ''y'' = nat(s ''y'') / ''y''} + WHILE Less (N 0) (V ''y'') DO ''y'' ::= Plus (V ''y'') (N (-1))))) +(\l s. s ''x'' \ 0)" +by auto + +thm vc_sound[OF vc2, simplified] + end