src/HOL/Library/While_Combinator.thy

   apply (erule_tac x = "\<lambda>i. f (Suc i)" in allE)
   apply blast
   done
 
 hide const while_aux
+
+lemma def_while_unfold: assumes fdef: "f == while test do"
+      shows "f x = (if test x then f(do x) else x)"
+proof -
+  have "f x = while test do x" using fdef by simp
+  also have "\<dots> = (if test x then while test do (do x) else x)"
+    by(rule while_unfold)
+  also have "\<dots> = (if test x then f(do x) else x)" by(simp add:fdef[symmetric])
+  finally show ?thesis .
+qed
+
 
 text {*
  The proof rule for @{term while}, where @{term P} is the invariant.
 *}