We reexamine the While combinator of higher-order logic (HOL) and introduce the For combinator. We argue that both combinators should be part of the toolbox of any HOL practitioner, not only because they make efficient computations within HOL possible, but also because they facilitate elegant inductive reasoning about loops. We present two examples that support this argument.
Full Text: Looping around the Orbit [pdf] (accepted for TPHOLs 2007)
Supplementary Material:
Theory files for Isabelle developer version (March 1st 2007) [tar.gz]
Last update: March 1st 2007, 1:00 PM.