theory Intent_DR

lemma evalMonad_mapM:
  "\<lbrakk>\<forall>r\<in>(set ls). evalMonad (f r) sa = evalMonad (g r) sb;
    \<And>s r. \<lbrace>(=) s\<rbrace> f r\<lbrace>\<lambda>r. (=) s\<rbrace>;
    \<And>s r. \<lbrace>(=) s\<rbrace> g r\<lbrace>\<lambda>r. (=) s\<rbrace>;
    \<And>r. empty_when_fail (f r);
    \<And>r. empty_when_fail (g r);
    \<And>r P. weak_det_spec P (f r);
    \<And>r P. weak_det_spec P (g r)\<rbrakk>
   \<Longrightarrow> evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb" proof(induct ls) case Nil show ?case by (clarsimp simp:mapM_def sequence_def) next case (Cons x ls) show ?case apply (clarsimp simp:mapM_Cons) apply (subst evalMonad_compose) apply (simp add:Cons)+ apply (subst evalMonad_compose) apply (simp add:Cons) apply (rule empty_when_fail_mapM) apply (simp add:Cons) apply (rule weak_det_spec_mapM) apply (simp add:Cons) apply (rule mapM_wp_inv) apply (simp add:Cons) apply (subst evalMonad_compose) apply (simp add:Cons)+ apply (subst evalMonad_compose) apply (rule empty_when_fail_mapM) apply (simp add:Cons) apply (rule weak_det_spec_mapM) apply (simp add:Cons) apply (rule mapM_wp_inv) apply (simp add:Cons) apply (subgoal_tac "evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb") apply (clarsimp split:option.splits) apply (rule Cons.hyps) apply (simp add:Cons)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>r\<in>set ls. evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>r\<in>set []. evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f []) sa = evalMonad (mapM g []) sb
 2. \<And>a ls. \<lbrakk>\<lbrakk>\<forall>r\<in>set ls. evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb; \<forall>r\<in>set (a # ls). evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f (a # ls)) sa = evalMonad (mapM g (a # ls)) sb proof (state)
this:
\<forall>r\<in>set []. evalMonad (f r) sa = evalMonad (g r) sb
\<lbrace>(=) ?s\<rbrace> f ?r \<lbrace>\<lambda>r. (=) ?s\<rbrace>
\<lbrace>(=) ?s\<rbrace> g ?r \<lbrace>\<lambda>r. (=) ?s\<rbrace>
empty_when_fail (f ?r)
empty_when_fail (g ?r)
weak_det_spec ?P (f ?r)
weak_det_spec ?P (g ?r)

goal (2 subgoals):
 1. \<lbrakk>\<forall>r\<in>set []. evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f []) sa = evalMonad (mapM g []) sb
 2. \<And>a ls. \<lbrakk>\<lbrakk>\<forall>r\<in>set ls. evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb; \<forall>r\<in>set (a # ls). evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f (a # ls)) sa = evalMonad (mapM g (a # ls)) sb proof (prove)
goal (1 subgoal):
 1. evalMonad (mapM f []) sa = evalMonad (mapM g []) sb proof (state)
this:
evalMonad (mapM f []) sa = evalMonad (mapM g []) sb

goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>\<lbrakk>\<forall>r\<in>set ls. evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb; \<forall>r\<in>set (a # ls). evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f (a # ls)) sa = evalMonad (mapM g (a # ls)) sb proof (state)
goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>\<lbrakk>\<forall>r\<in>set ls. evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb; \<forall>r\<in>set (a # ls). evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f (a # ls)) sa = evalMonad (mapM g (a # ls)) sb proof (state)
this:
\<lbrakk>\<forall>r\<in>set ls. evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb
\<forall>r\<in>set (x # ls). evalMonad (f r) sa = evalMonad (g r) sb
\<lbrace>(=) ?s\<rbrace> f ?r \<lbrace>\<lambda>r. (=) ?s\<rbrace>
\<lbrace>(=) ?s\<rbrace> g ?r \<lbrace>\<lambda>r. (=) ?s\<rbrace>
empty_when_fail (f ?r)
empty_when_fail (g ?r)
weak_det_spec ?P (f ?r)
weak_det_spec ?P (g ?r)

goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>\<lbrakk>\<forall>r\<in>set ls. evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb; \<forall>r\<in>set (a # ls). evalMonad (f r) sa = evalMonad (g r) sb; \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>; \<And>r. empty_when_fail (f r); \<And>r. empty_when_fail (g r); \<And>r P. weak_det_spec P (f r); \<And>r P. weak_det_spec P (g r)\<rbrakk> \<Longrightarrow> evalMonad (mapM f (a # ls)) sa = evalMonad (mapM g (a # ls)) sb proof (prove)
goal (1 subgoal):
 1. evalMonad (mapM f (x # ls)) sa = evalMonad (mapM g (x # ls)) sb proof (prove)
goal (1 subgoal):
 1. evalMonad (do y <- f x;
ys <- mapM f ls;
return (y # ys)
od) sa = evalMonad (do y <- g x;
ys <- mapM g ls;
return (y # ys)
od) sb proof (prove)
goal (4 subgoals):
 1. empty_when_fail (f x)
 2. weak_det_spec ((=) sa) (f x)
 3. \<And>s. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. (case evalMonad (f x) sa of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (do ys <- mapM f ls;
return (r # ys)
od) sa) = evalMonad (do y <- g x;
ys <- mapM g ls;
return (y # ys)
od) sb proof (prove)
goal (1 subgoal):
 1. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (do ys <- mapM f ls;
return (r # ys)
od) sa) = evalMonad (do y <- g x;
ys <- mapM g ls;
return (y # ys)
od) sb proof (prove)
goal (4 subgoals):
 1. \<And>r. empty_when_fail (mapM f ls)
 2. \<And>r. weak_det_spec ((=) sa) (mapM f ls)
 3. \<And>r s. \<lbrace>(=) s\<rbrace> mapM f ls \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = evalMonad (do y <- g x;
ys <- mapM g ls;
return (y # ys)
od) sb proof (prove)
goal (4 subgoals):
 1. empty_when_fail (mapM f ls)
 2. \<And>r. weak_det_spec ((=) sa) (mapM f ls)
 3. \<And>r s. \<lbrace>(=) s\<rbrace> mapM f ls \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = evalMonad (do y <- g x;
ys <- mapM g ls;
return (y # ys)
od) sb proof (prove)
goal (4 subgoals):
 1. \<And>P l. weak_det_spec P (f l) \<and> empty_when_fail (f l)
 2. \<And>r. weak_det_spec ((=) sa) (mapM f ls)
 3. \<And>r s. \<lbrace>(=) s\<rbrace> mapM f ls \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = evalMonad (do y <- g x;
ys <- mapM g ls;
return (y # ys)
od) sb proof (prove)
goal (3 subgoals):
 1. \<And>r. weak_det_spec ((=) sa) (mapM f ls)
 2. \<And>r s. \<lbrace>(=) s\<rbrace> mapM f ls \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = evalMonad (do y <- g x;
ys <- mapM g ls;
return (y # ys)
od) sb proof (prove)
goal (3 subgoals):
 1. \<And>r ra P. weak_det_spec P (f ra)
 2. \<And>r s. \<lbrace>(=) s\<rbrace> mapM f ls \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = evalMonad (do y <- g x;
ys <- mapM g ls;
return (y # ys)
od) sb proof (prove)
goal (2 subgoals):
 1. \<And>r s. \<lbrace>(=) s\<rbrace> mapM f ls \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = evalMonad (do y <- g x;
ys <- mapM g ls;
return (y # ys)
od) sb proof (prove)
goal (2 subgoals):
 1. \<And>r s x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = evalMonad (do y <- g x;
ys <- mapM g ls;
return (y # ys)
od) sb proof (prove)
goal (1 subgoal):
 1. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = evalMonad (do y <- g x;
ys <- mapM g ls;
return (y # ys)
od) sb proof (prove)
goal (4 subgoals):
 1. empty_when_fail (g x)
 2. weak_det_spec ((=) sb) (g x)
 3. \<And>s. \<lbrace>(=) s\<rbrace> g x \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (do ys <- mapM g ls;
return (r # ys)
od) sb) proof (prove)
goal (1 subgoal):
 1. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (do ys <- mapM g ls;
return (r # ys)
od) sb) proof (prove)
goal (4 subgoals):
 1. \<And>r. empty_when_fail (mapM g ls)
 2. \<And>r. weak_det_spec ((=) sb) (mapM g ls)
 3. \<And>r s. \<lbrace>(=) s\<rbrace> mapM g ls \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM g ls) sb of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sb) proof (prove)
goal (4 subgoals):
 1. \<And>r P l. weak_det_spec P (g l) \<and> empty_when_fail (g l)
 2. \<And>r. weak_det_spec ((=) sb) (mapM g ls)
 3. \<And>r s. \<lbrace>(=) s\<rbrace> mapM g ls \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM g ls) sb of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sb) proof (prove)
goal (3 subgoals):
 1. \<And>r. weak_det_spec ((=) sb) (mapM g ls)
 2. \<And>r s. \<lbrace>(=) s\<rbrace> mapM g ls \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM g ls) sb of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sb) proof (prove)
goal (3 subgoals):
 1. \<And>r ra P. weak_det_spec P (g ra)
 2. \<And>r s. \<lbrace>(=) s\<rbrace> mapM g ls \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM g ls) sb of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sb) proof (prove)
goal (2 subgoals):
 1. \<And>r s. \<lbrace>(=) s\<rbrace> mapM g ls \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM g ls) sb of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sb) proof (prove)
goal (2 subgoals):
 1. \<And>r s x. \<lbrace>(=) s\<rbrace> g x \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM g ls) sb of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sb) proof (prove)
goal (1 subgoal):
 1. (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM g ls) sb of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sb) proof (prove)
goal (2 subgoals):
 1. evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb \<Longrightarrow> (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM f ls) sa of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sa) = (case evalMonad (g x) sb of None \<Rightarrow> None | Some r \<Rightarrow> case evalMonad (mapM g ls) sb of None \<Rightarrow> None | Some ra \<Rightarrow> evalMonad (return (r # ra)) sb)
 2. evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb proof (prove)
goal (1 subgoal):
 1. evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb proof (prove)
goal (7 subgoals):
 1. \<forall>r\<in>set ls. evalMonad (f r) sa = evalMonad (g r) sb
 2. \<And>s r. \<lbrace>(=) s\<rbrace> f r \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s r. \<lbrace>(=) s\<rbrace> g r \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>r. empty_when_fail (f r)
 5. \<And>r. empty_when_fail (g r)
 6. \<And>r P. weak_det_spec P (f r)
 7. \<And>r P. weak_det_spec P (g r) proof (prove)
goal:
No subgoals! proof (state)
this:
evalMonad (mapM f (x # ls)) sa = evalMonad (mapM g (x # ls)) sb

goal:
No subgoals!