theory StateTranslation_D

lemma evalMonad_mapM_cong:
  assumes f: "\<And>x. evalMonad (f x) ms = evalMonad (f x) ms'"
  assumes P: "\<And>P x. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>"
  assumes det: "\<And>x. det_or_fail (f x)"
  shows "evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'" apply (induct xs) apply (simp add: mapM_Nil) apply (simp add: mapM_Cons) apply (subst evalMonad_bind [OF P det]) apply (subst evalMonad_bind [OF P det]) apply (clarsimp simp: f) apply (subst evalMonad_bind) apply (wp mapM_wp' P) apply (rule mapM_df, rule det) apply (subst evalMonad_bind) apply (wp mapM_wp' P) apply (rule mapM_df, rule det) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms' proof (prove)
goal (2 subgoals):
 1. evalMonad (mapM f []) ms = evalMonad (mapM f []) ms'
 2. \<And>a xs. evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms' \<Longrightarrow> evalMonad (mapM f (a # xs)) ms = evalMonad (mapM f (a # xs)) ms' proof (prove)
goal (1 subgoal):
 1. \<And>a xs. evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms' \<Longrightarrow> evalMonad (mapM f (a # xs)) ms = evalMonad (mapM f (a # xs)) ms' proof (prove)
goal (1 subgoal):
 1. \<And>a xs. evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms' \<Longrightarrow> evalMonad (do y <- f a;
ys <- mapM f xs;
return (y # ys)
od) ms = evalMonad (do y <- f a;
ys <- mapM f xs;
return (y # ys)
od) ms' proof (prove)
goal (1 subgoal):
 1. \<And>a xs. evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms' \<Longrightarrow> (if evalMonad (f a) ms = None then None else evalMonad (do ys <- mapM f xs;
return (the (evalMonad (f a) ms) # ys)
od) ms) = evalMonad (do y <- f a;
ys <- mapM f xs;
return (y # ys)
od) ms' proof (prove)
goal (1 subgoal):
 1. \<And>a xs. evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms' \<Longrightarrow> (if evalMonad (f a) ms = None then None else evalMonad (do ys <- mapM f xs;
return (the (evalMonad (f a) ms) # ys)
od) ms) = (if evalMonad (f a) ms' = None then None else evalMonad (do ys <- mapM f xs;
return (the (evalMonad (f a) ms') # ys)
od) ms') proof (prove)
goal (1 subgoal):
 1. \<And>a xs y. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> evalMonad (do ys <- mapM f xs;
return (y # ys)
od) ms = evalMonad (do ys <- mapM f xs;
return (y # ys)
od) ms' proof (prove)
goal (3 subgoals):
 1. \<And>a xs y P. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>a xs y. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> det_or_fail (mapM f xs)
 3. \<And>a xs y. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> (if evalMonad (mapM f xs) ms = None then None else evalMonad (return (y # the (evalMonad (mapM f xs) ms))) ms) = evalMonad (do ys <- mapM f xs;
return (y # ys)
od) ms' proof (prove)
goal (2 subgoals):
 1. \<And>a xs y. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> det_or_fail (mapM f xs)
 2. \<And>a xs y. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> (if evalMonad (mapM f xs) ms = None then None else evalMonad (return (y # the (evalMonad (mapM f xs) ms))) ms) = evalMonad (do ys <- mapM f xs;
return (y # ys)
od) ms' proof (prove)
goal (1 subgoal):
 1. \<And>a xs y. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> (if evalMonad (mapM f xs) ms = None then None else evalMonad (return (y # the (evalMonad (mapM f xs) ms))) ms) = evalMonad (do ys <- mapM f xs;
return (y # ys)
od) ms' proof (prove)
goal (3 subgoals):
 1. \<And>a xs y P. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>a xs y. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> det_or_fail (mapM f xs)
 3. \<And>a xs y. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> (if evalMonad (mapM f xs) ms = None then None else evalMonad (return (y # the (evalMonad (mapM f xs) ms))) ms) = (if evalMonad (mapM f xs) ms' = None then None else evalMonad (return (y # the (evalMonad (mapM f xs) ms'))) ms') proof (prove)
goal (2 subgoals):
 1. \<And>a xs y. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> det_or_fail (mapM f xs)
 2. \<And>a xs y. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> (if evalMonad (mapM f xs) ms = None then None else evalMonad (return (y # the (evalMonad (mapM f xs) ms))) ms) = (if evalMonad (mapM f xs) ms' = None then None else evalMonad (return (y # the (evalMonad (mapM f xs) ms'))) ms') proof (prove)
goal (1 subgoal):
 1. \<And>a xs y. \<lbrakk>evalMonad (mapM f xs) ms = evalMonad (mapM f xs) ms'; evalMonad (f a) ms' = Some y\<rbrakk> \<Longrightarrow> (if evalMonad (mapM f xs) ms = None then None else evalMonad (return (y # the (evalMonad (mapM f xs) ms))) ms) = (if evalMonad (mapM f xs) ms' = None then None else evalMonad (return (y # the (evalMonad (mapM f xs) ms'))) ms') proof (prove)
goal:
No subgoals!