src/HOL/Library/While_Combinator.thy
changeset 14300 bf8b8c9425c3
parent 12791 ccc0f45ad2c4
child 14589 feae7b5fd425
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Wed Dec 17 16:23:52 2003 +0100
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Thu Dec 18 08:20:36 2003 +0100
     1.3 @@ -68,6 +68,17 @@
     1.4  
     1.5  hide const while_aux
     1.6  
     1.7 +lemma def_while_unfold: assumes fdef: "f == while test do"
     1.8 +      shows "f x = (if test x then f(do x) else x)"
     1.9 +proof -
    1.10 +  have "f x = while test do x" using fdef by simp
    1.11 +  also have "\<dots> = (if test x then while test do (do x) else x)"
    1.12 +    by(rule while_unfold)
    1.13 +  also have "\<dots> = (if test x then f(do x) else x)" by(simp add:fdef[symmetric])
    1.14 +  finally show ?thesis .
    1.15 +qed
    1.16 +
    1.17 +
    1.18  text {*
    1.19   The proof rule for @{term while}, where @{term P} is the invariant.
    1.20  *}