# HG changeset patch
# User nipkow
# Date 1633982121 -7200
# Node ID 40f03761f77fe265bd8c898022c73ec3dd9b9cb9
# Parent  059743bc8311847f798de917e2876e8b959e8475
more examples

diff -r 059743bc8311 -r 40f03761f77f src/HOL/IMP/Hoare_Total_EX.thy
--- 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
diff -r 059743bc8311 -r 40f03761f77f src/HOL/IMP/Hoare_Total_EX2.thy
--- 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
diff -r 059743bc8311 -r 40f03761f77f src/HOL/IMP/VCG_Total_EX2.thy
--- 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