author nipkow Tue, 28 Sep 2021 20:58:04 +0200 changeset 74372 90c99974f648 parent 74370 d8dc8fdc46fc (current diff) parent 74371 4b9876198603 (diff) child 74384 bd9a5e128c31
merged
```--- a/src/HOL/IMP/Hoare_Total.thy	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/HOL/IMP/Hoare_Total.thy	Tue Sep 28 20:58:04 2021 +0200
@@ -89,6 +89,32 @@
apply simp
done

+text \<open>Nested loops. This poses a problem for VCGs because the proof of the inner loop needs to
+refer to outer loops. This works here because the invariant is not written down statically but
+created in the context of a proof that has already introduced/fixed outer \<open>n\<close>s that can be
+referred to.\<close>
+
+lemma
+ "\<turnstile>\<^sub>t {\<lambda>_. True}
+  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>_. True}"
+apply(rule While_fun'[where f = "\<lambda>s. nat(s ''x'')"])
+ prefer 2 apply simp
+apply(rule_tac P\<^sub>2 = "\<lambda>s. nat(s ''x'') < n" in Seq)
+ apply(rule_tac P\<^sub>2 = "\<lambda>s. nat(s ''x'') < n" in Seq)
+  apply(rule Assign')
+  apply simp
+ apply(rule Assign')
+ apply simp
+(* note that the invariant refers to the outer \<open>n\<close>: *)
+apply(rule While_fun'[where f = "\<lambda>s. nat(s ''y'')"])
+ prefer 2 apply simp
+apply(rule Assign')
+apply simp
+done

text\<open>The soundness theorem:\<close>
```