theory Monad_Lists

lemma mapM_upd:
  assumes "\<And>x rv s s'. (rv,s') \<in> fst (f x s) \<Longrightarrow> x \<in> set xs \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))"
  shows "(rv,s') \<in> fst (mapM f xs s) \<Longrightarrow> (rv, g s') \<in> fst (mapM f xs (g s))" using assms proof (induct xs arbitrary: rv s s') case Nil thus ?case by (simp add: mapM_Nil return_def) next case (Cons z zs) from Cons.prems show ?case apply (clarsimp simp: mapM_Cons in_monad) apply (drule Cons.prems, simp) apply (rule exI, erule conjI) apply (erule Cons.hyps) apply (erule Cons.prems) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv, s') \<in> fst (mapM f xs s) \<Longrightarrow> (rv, g s') \<in> fst (mapM f xs (g s)) proof (prove)
using this:
\<lbrakk>(?rv, ?s') \<in> fst (f ?x ?s); ?x \<in> set xs\<rbrakk> \<Longrightarrow> (?rv, g ?s') \<in> fst (f ?x (g ?s))

goal (1 subgoal):
 1. (rv, s') \<in> fst (mapM f xs s) \<Longrightarrow> (rv, g s') \<in> fst (mapM f xs (g s)) proof (state)
goal (2 subgoals):
 1. \<And>rv s s'. \<lbrakk>(rv, s') \<in> fst (mapM f [] s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set []\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (mapM f [] (g s))
 2. \<And>a xs rv s s'. \<lbrakk>\<And>rv s s'. \<lbrakk>(rv, s') \<in> fst (mapM f xs s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set xs\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (mapM f xs (g s)); (rv, s') \<in> fst (mapM f (a # xs) s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set (a # xs)\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (mapM f (a # xs) (g s)) proof (state)
this:
(rv, s') \<in> fst (mapM f [] s)
\<lbrakk>(?rv, ?s') \<in> fst (f ?x ?s); ?x \<in> set []\<rbrakk> \<Longrightarrow> (?rv, g ?s') \<in> fst (f ?x (g ?s))

goal (2 subgoals):
 1. \<And>rv s s'. \<lbrakk>(rv, s') \<in> fst (mapM f [] s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set []\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (mapM f [] (g s))
 2. \<And>a xs rv s s'. \<lbrakk>\<And>rv s s'. \<lbrakk>(rv, s') \<in> fst (mapM f xs s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set xs\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (mapM f xs (g s)); (rv, s') \<in> fst (mapM f (a # xs) s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set (a # xs)\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (mapM f (a # xs) (g s)) proof (prove)
using this:
(rv, s') \<in> fst (mapM f [] s)
\<lbrakk>(?rv, ?s') \<in> fst (f ?x ?s); ?x \<in> set []\<rbrakk> \<Longrightarrow> (?rv, g ?s') \<in> fst (f ?x (g ?s))

goal (1 subgoal):
 1. (rv, g s') \<in> fst (mapM f [] (g s)) proof (state)
this:
(rv, g s') \<in> fst (mapM f [] (g s))

goal (1 subgoal):
 1. \<And>a xs rv s s'. \<lbrakk>\<And>rv s s'. \<lbrakk>(rv, s') \<in> fst (mapM f xs s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set xs\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (mapM f xs (g s)); (rv, s') \<in> fst (mapM f (a # xs) s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set (a # xs)\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (mapM f (a # xs) (g s)) proof (state)
goal (1 subgoal):
 1. \<And>a xs rv s s'. \<lbrakk>\<And>rv s s'. \<lbrakk>(rv, s') \<in> fst (mapM f xs s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set xs\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (mapM f xs (g s)); (rv, s') \<in> fst (mapM f (a # xs) s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set (a # xs)\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (mapM f (a # xs) (g s)) proof (state)
this:
\<lbrakk>(?rv, ?s') \<in> fst (mapM f zs ?s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (?rv, g ?s') \<in> fst (mapM f zs (g ?s))
(rv, s') \<in> fst (mapM f (z # zs) s)
\<lbrakk>(?rv, ?s') \<in> fst (f ?x ?s); ?x \<in> set (z # zs)\<rbrakk> \<Longrightarrow> (?rv, g ?s') \<in> fst (f ?x (g ?s))

goal (1 subgoal):
 1. \<And>a xs rv s s'. \<lbrakk>\<And>rv s s'. \<lbrakk>(rv, s') \<in> fst (mapM f xs s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set xs\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (mapM f xs (g s)); (rv, s') \<in> fst (mapM f (a # xs) s); \<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x \<in> set (a # xs)\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (mapM f (a # xs) (g s)) proof (chain)
picking this:
(rv, s') \<in> fst (mapM f (z # zs) s)
\<lbrakk>(?rv, ?s') \<in> fst (f ?x ?s); ?x \<in> set (z # zs)\<rbrakk> \<Longrightarrow> (?rv, g ?s') \<in> fst (f ?x (g ?s)) proof (prove)
using this:
(rv, s') \<in> fst (mapM f (z # zs) s)
\<lbrakk>(?rv, ?s') \<in> fst (f ?x ?s); ?x \<in> set (z # zs)\<rbrakk> \<Longrightarrow> (?rv, g ?s') \<in> fst (f ?x (g ?s))

goal (1 subgoal):
 1. (rv, g s') \<in> fst (mapM f (z # zs) (g s)) proof (prove)
goal (1 subgoal):
 1. \<And>s'' y ys. \<lbrakk>\<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s)); (y, s'') \<in> fst (f z s); (ys, s') \<in> fst (mapM f zs s''); rv = y # ys\<rbrakk> \<Longrightarrow> \<exists>s''. (y, s'') \<in> fst (f z (g s)) \<and> (ys, g s') \<in> fst (mapM f zs s'') proof (prove)
goal (1 subgoal):
 1. \<And>s'' y ys. \<lbrakk>\<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s)); (ys, s') \<in> fst (mapM f zs s''); rv = y # ys; (y, g s'') \<in> fst (f z (g s))\<rbrakk> \<Longrightarrow> \<exists>s''. (y, s'') \<in> fst (f z (g s)) \<and> (ys, g s') \<in> fst (mapM f zs s'') proof (prove)
goal (1 subgoal):
 1. \<And>s'' y ys. \<lbrakk>\<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s)); (ys, s') \<in> fst (mapM f zs s''); rv = y # ys\<rbrakk> \<Longrightarrow> (ys, g s') \<in> fst (mapM f zs (g s'')) proof (prove)
goal (1 subgoal):
 1. \<And>s'' y ys rv s' x s. \<lbrakk>\<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s)); rv = y # ys; (rv, s') \<in> fst (f x s); x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s)) proof (prove)
goal (1 subgoal):
 1. \<And>s'' y ys rv s' x s. \<lbrakk>\<And>rv s' x s. \<lbrakk>(rv, s') \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s') \<in> fst (f x (g s)); rv = y # ys; x \<in> set zs\<rbrakk> \<Longrightarrow> x \<in> set (z # zs) proof (prove)
goal:
No subgoals! proof (state)
this:
(rv, g s') \<in> fst (mapM f (z # zs) (g s))

goal:
No subgoals!