--- a/src/HOL/IMP/Hoare_Total_EX.thy Mon Oct 11 17:04:35 2021 +0200
+++ b/src/HOL/IMP/Hoare_Total_EX.thy Mon Oct 11 21:55:21 2021 +0200
@@ -139,4 +139,40 @@
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
--- a/src/HOL/IMP/Hoare_Total_EX2.thy Mon Oct 11 17:04:35 2021 +0200
+++ b/src/HOL/IMP/Hoare_Total_EX2.thy Mon Oct 11 21:55:21 2021 +0200
@@ -190,4 +190,43 @@
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
--- a/src/HOL/IMP/VCG_Total_EX2.thy Mon Oct 11 17:04:35 2021 +0200
+++ b/src/HOL/IMP/VCG_Total_EX2.thy Mon Oct 11 21:55:21 2021 +0200
@@ -131,4 +131,25 @@
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