Some examples of using whileLoop in Monad_WP about l4v

[talsewell]

The whileLoop combinator mostly exists to be used by AutoCorres as a state-monad equivalent to a while loop in C. I don't think it is used in the seL4 proofs.

The key unroll rule is proven in NonDetMonadLemmas - whileLoop_unroll - the while loop is equivalent to checking whether the condition currently holds, and if it does, performing one iteration of the loop plus the while loop. Isabelle wouldn't accept this as a recursive definition by default, thus the complicated definition.

The AutoCorres quickstart manual gives some example proofs involving whileLoop, e.g. in Chapter 2

[lsf37]

The AutoCorres examples directory contains the examples in the quickstart tutorial, as well as a few other ones. An easy example of how to reason about whileLoop is in https://github.com/seL4/l4v/blob/master/tools/autocorres/tests/examples/ListRev.thy

While this is generated from a C file, the proof at the bottom is purely monadic.