Add a ‘while’ constant to state_transformer theory

[mn200]

There is a natural notion of while loop for state monads. With our do notation, you'd like to have it satisfy the following theorem:

while guard body = 
  do 
     gval <- guard;
     if gval then 
        do 
          body;
          while guard body
        od
     else return ()
  od

I think it should be possible to define this in terms of our existing WHILE combinator. Something like

mwhile g b = SND (g (WHILE (FST o g) (SND o b o SND o g)))

[mn200]

To make this type-check, you actually need:

Define`
  mwhile g b = SND o g o WHILE (FST o g) (SND o b o SND o g)
`;

This is a version of the notion that allows for a side-effecting guard g.

The issue is that this can’t be made to satisfy the desired “monadic” characterisation because of problems when it’s undefined. In particular, this definition calls WHILE on the initial state, but the characterisation calls the guard first, and then calls itself recursively on the resulting state.