# HG changeset patch
# User nipkow
# Date 1641819933 -3600
# Node ID 7733c794cfea98fc8c171c47dc1177f3ef9292f3
# Parent  a565a2889b49f2a15487398bdc96d28a85e6e442
added lemma

diff -r a565a2889b49 -r 7733c794cfea src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Sun Jan 09 18:50:06 2022 +0000
+++ b/src/HOL/Library/While_Combinator.thy	Mon Jan 10 14:05:33 2022 +0100
@@ -239,6 +239,15 @@
   apply blast
   done
 
+text \<open>Combine invariant preservation and variant decrease in one goal:\<close>
+theorem while_rule2:
+  "[| P s;
+      !!s. [| P s; b s  |] ==> P (c s) \<and> (c s, s) \<in> r;
+      !!s. [| P s; \<not> b s  |] ==> Q s;
+      wf r |] ==>
+   Q (while b c s)"
+using while_rule[of P] by metis
+
 text\<open>Proving termination:\<close>
 
 theorem wf_while_option_Some: