Eval function with new do-notation

eval.thy

fun eval :: "exp ⇒ state ⇒ (val × state) option"
and eval_l :: "lexp ⇒ state ⇒ (val × state) option" where
  "eval (Const c) s = Some (c, s)"
| "eval Null s = Some (NullVal, s)"
| "eval (V x) (σ, μ) = Some (σ x, (σ, μ))"
| "eval (Plus i⇩1 i⇩2) s = do {
  (v⇩1, s) ← eval i⇩1 s;
  (v⇩2, s) ← eval i⇩2 s;
  v ← plus_val v⇩1 v⇩2;
  Some (v, s)
}"
| "eval (Less i⇩1 i⇩2) s = do {
  (v⇩1, s) ← eval i⇩1 s;
  (v⇩2, s) ← eval i⇩2 s;
  v ← less_val v⇩1 v⇩2;
  Some (v, s)
}"
| "eval (Not b) s = do {
  (v, s) ← eval b s;
  v ← not_val v;
  Some (v, s)
}"
| "eval (And b⇩1 b⇩2) s = do {
  (v⇩1, s) ← eval b⇩1 s;
  (v⇩2, s) ← eval b⇩2 s;
  v ← and_val v⇩1 v⇩2;
  Some (v, s)
}"
| "eval (New e) s = do {
  (v, (σ, μ)) ← eval e s;
  (v, μ) ← new_block v μ;
  Some (v, (σ, μ))
}"
| "eval (Deref e) s = do {
  (v, (σ, μ)) ← eval e s;
  v ← get_mem v μ;
  Some (v, (σ, μ))
}"
| "eval (Ref e) s = (case (eval_l e s) of
                       None ⇒ None |
                       Some (v, s') ⇒ (case v of
                                          (I _) ⇒ None |
                                          (A _) ⇒ Some (v,s')))"
| "eval (Index e⇩1 e⇩2) s = do {
  (v⇩1, s) ← eval e⇩1 s;
  (v⇩2, (σ, μ)) ← eval e⇩2 s;
  v ← index_mem v⇩1 v⇩2 μ;
  Some (v, (σ, μ))
}"
| "eval_l (Derefl e) s = (case (eval e s) of
                            None ⇒ None |
                            Some (v, s') ⇒ (case v of
                                               (I _) ⇒ None |
                                               (A _) ⇒ Some (v, s')))"
| "eval_l (Indexl e⇩1 e⇩2) s = do {
  (v⇩1, s) ← eval e⇩1 s;
  (v⇩2, s) ← eval e⇩2 s;
  v ← plus_val v⇩1 v⇩2;
  Some (v, s)
}"