src/HOL/While.thy

While functional for defining tail-recursive functions

(*  Title:      HOL/While
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   2000 TU Muenchen

Defines a while-combinator "while" and proves
a) an unrestricted unfolding law (even if while diverges!)
   (I got this idea from Wolfgang Goerigk)
b) the invariant rule for reasoning about while
*)

While = Recdef +

consts while_aux :: "('a => bool) * ('a => 'a) * 'a => 'a"
recdef while_aux
 "same_fst (%b. True) (%b. same_fst (%c. True) (%c.
  {(t,s).  b s & c s = t &
           ~(? f. f 0 = s & (!i. b(f i) & c(f i) = f(i+1)))}))"
"while_aux(b,c,s) =
  (if (? f. f 0 = s & (!i. b(f i) & c(f i) = f(i+1)))
   then arbitrary
   else if b s then while_aux(b,c,c s) else s)"

constdefs
 while :: "('a => bool) => ('a => 'a) => 'a => 'a"
"while b c s == while_aux(b,c,s)"

end