Pattern matching in do notation

[formrre]

HOL currently doesn't support the following inside do-od notation:

(SOME x) <- action;
f x

Monad syntax includes a field for fail, which could be used to implement this in the style of Haskell's MonadFail.

In particular the above should desugar to:

action `mbind` (\y. case y of
                        | SOME x -> f x
                        | _ -> fail)

[mn200]

Sounds great!