[STATEMENT]
lemma eval_reverse:
  "eval E (Var x) = E x"
  "eval E (Const i) = return i"
  "eval E (Plus e1 e2) = bind (eval E e2) (\<lambda>j. bind (eval E e1) (\<lambda>i. return (i + j)))"
  "eval E (Div e1 e2) = bind (eval E e2) (\<lambda>j. bind (eval E e1) (\<lambda>i. if j = 0 then fail else return (i div j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (eval E (Var x) = E x &&& eval E (Const i) = return i) &&& eval E (Plus e1 e2) = bind (eval E e2) (\<lambda>j. bind (eval E e1) (\<lambda>i. return (i + j))) &&& eval E (Div e1 e2) = bind (eval E e2) (\<lambda>j. bind (eval E e1) (\<lambda>i. if j = 0 then fail else return (i div j)))
[PROOF STEP]
by(simp; rule bind_commute)+