Pattern matching in do notation

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)
```