src/HOL/Library/While_Combinator.thy

    apply blast
   apply (erule wf_subset)
   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:
   assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}"
   and "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"