theory Ipc_DR

lemma evalMonad_mapM_functional:
  assumes fn: "\<And>n. functional (f n)"
  and    det: "\<And>n. n \<in> set ns \<Longrightarrow> det (f n)"
  shows   "the (evalMonad (mapM f ns) s) = map (\<lambda>n. the (evalMonad (f n) s)) ns" using det proof (induct ns) case Nil thus ?case by (simp add: mapM_Nil) next case (Cons n ns') have det': "det (f n)" using Cons.prems by clarsimp show ?case apply (simp add: mapM_Cons evalMonad_bind_functional [OF fn det']) apply (subst evalMonad_bind_functional) apply (rule mapM_functional [OF fn]) apply (rule det_mapM [OF Cons.prems]) apply assumption apply clarsimp apply simp apply (subst Cons.hyps) apply (rule Cons.prems) apply simp apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. the (evalMonad (mapM f ns) s) = map (\<lambda>n. the (evalMonad (f n) s)) ns proof (prove)
using this:
?n \<in> set ns \<Longrightarrow> det (f ?n)

goal (1 subgoal):
 1. the (evalMonad (mapM f ns) s) = map (\<lambda>n. the (evalMonad (f n) s)) ns proof (state)
goal (2 subgoals):
 1. (\<And>n. n \<in> set [] \<Longrightarrow> det (f n)) \<Longrightarrow> the (evalMonad (mapM f []) s) = map (\<lambda>n. the (evalMonad (f n) s)) []
 2. \<And>a ns. \<lbrakk>(\<And>n. n \<in> set ns \<Longrightarrow> det (f n)) \<Longrightarrow> the (evalMonad (mapM f ns) s) = map (\<lambda>n. the (evalMonad (f n) s)) ns; \<And>n. n \<in> set (a # ns) \<Longrightarrow> det (f n)\<rbrakk> \<Longrightarrow> the (evalMonad (mapM f (a # ns)) s) = map (\<lambda>n. the (evalMonad (f n) s)) (a # ns) proof (state)
this:
?n \<in> set [] \<Longrightarrow> det (f ?n)

goal (2 subgoals):
 1. (\<And>n. n \<in> set [] \<Longrightarrow> det (f n)) \<Longrightarrow> the (evalMonad (mapM f []) s) = map (\<lambda>n. the (evalMonad (f n) s)) []
 2. \<And>a ns. \<lbrakk>(\<And>n. n \<in> set ns \<Longrightarrow> det (f n)) \<Longrightarrow> the (evalMonad (mapM f ns) s) = map (\<lambda>n. the (evalMonad (f n) s)) ns; \<And>n. n \<in> set (a # ns) \<Longrightarrow> det (f n)\<rbrakk> \<Longrightarrow> the (evalMonad (mapM f (a # ns)) s) = map (\<lambda>n. the (evalMonad (f n) s)) (a # ns) proof (prove)
using this:
?n \<in> set [] \<Longrightarrow> det (f ?n)

goal (1 subgoal):
 1. the (evalMonad (mapM f []) s) = map (\<lambda>n. the (evalMonad (f n) s)) [] proof (state)
this:
the (evalMonad (mapM f []) s) = map (\<lambda>n. the (evalMonad (f n) s)) []

goal (1 subgoal):
 1. \<And>a ns. \<lbrakk>(\<And>n. n \<in> set ns \<Longrightarrow> det (f n)) \<Longrightarrow> the (evalMonad (mapM f ns) s) = map (\<lambda>n. the (evalMonad (f n) s)) ns; \<And>n. n \<in> set (a # ns) \<Longrightarrow> det (f n)\<rbrakk> \<Longrightarrow> the (evalMonad (mapM f (a # ns)) s) = map (\<lambda>n. the (evalMonad (f n) s)) (a # ns) proof (state)
goal (1 subgoal):
 1. \<And>a ns. \<lbrakk>(\<And>n. n \<in> set ns \<Longrightarrow> det (f n)) \<Longrightarrow> the (evalMonad (mapM f ns) s) = map (\<lambda>n. the (evalMonad (f n) s)) ns; \<And>n. n \<in> set (a # ns) \<Longrightarrow> det (f n)\<rbrakk> \<Longrightarrow> the (evalMonad (mapM f (a # ns)) s) = map (\<lambda>n. the (evalMonad (f n) s)) (a # ns) proof (state)
this:
(\<And>n. n \<in> set ns' \<Longrightarrow> det (f n)) \<Longrightarrow> the (evalMonad (mapM f ns') s) = map (\<lambda>n. the (evalMonad (f n) s)) ns'
?n \<in> set (n # ns') \<Longrightarrow> det (f ?n)

goal (1 subgoal):
 1. \<And>a ns. \<lbrakk>(\<And>n. n \<in> set ns \<Longrightarrow> det (f n)) \<Longrightarrow> the (evalMonad (mapM f ns) s) = map (\<lambda>n. the (evalMonad (f n) s)) ns; \<And>n. n \<in> set (a # ns) \<Longrightarrow> det (f n)\<rbrakk> \<Longrightarrow> the (evalMonad (mapM f (a # ns)) s) = map (\<lambda>n. the (evalMonad (f n) s)) (a # ns) proof (prove)
goal (1 subgoal):
 1. det (f n) proof (prove)
using this:
?n \<in> set (n # ns') \<Longrightarrow> det (f ?n)

goal (1 subgoal):
 1. det (f n) proof (state)
this:
det (f n)

goal (1 subgoal):
 1. \<And>a ns. \<lbrakk>(\<And>n. n \<in> set ns \<Longrightarrow> det (f n)) \<Longrightarrow> the (evalMonad (mapM f ns) s) = map (\<lambda>n. the (evalMonad (f n) s)) ns; \<And>n. n \<in> set (a # ns) \<Longrightarrow> det (f n)\<rbrakk> \<Longrightarrow> the (evalMonad (mapM f (a # ns)) s) = map (\<lambda>n. the (evalMonad (f n) s)) (a # ns) proof (prove)
goal (1 subgoal):
 1. the (evalMonad (mapM f (n # ns')) s) = map (\<lambda>n. the (evalMonad (f n) s)) (n # ns') proof (prove)
goal (1 subgoal):
 1. the (evalMonad (do ys <- mapM f ns';
return (the (evalMonad (f n) s) # ys)
od) s) = the (evalMonad (f n) s) # map (\<lambda>n. the (evalMonad (f n) s)) ns' proof (prove)
goal (3 subgoals):
 1. functional (mapM f ns')
 2. det (mapM f ns')
 3. the (evalMonad (return (the (evalMonad (f n) s) # the (evalMonad (mapM f ns') s))) s) = the (evalMonad (f n) s) # map (\<lambda>n. the (evalMonad (f n) s)) ns' proof (prove)
goal (2 subgoals):
 1. det (mapM f ns')
 2. the (evalMonad (return (the (evalMonad (f n) s) # the (evalMonad (mapM f ns') s))) s) = the (evalMonad (f n) s) # map (\<lambda>n. the (evalMonad (f n) s)) ns' proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> ?S2 \<Longrightarrow> x \<in> set (n # ns')
 2. set ns' \<subseteq> ?S2
 3. the (evalMonad (return (the (evalMonad (f n) s) # the (evalMonad (mapM f ns') s))) s) = the (evalMonad (f n) s) # map (\<lambda>n. the (evalMonad (f n) s)) ns' proof (prove)
goal (2 subgoals):
 1. set ns' \<subseteq> set (n # ns')
 2. the (evalMonad (return (the (evalMonad (f n) s) # the (evalMonad (mapM f ns') s))) s) = the (evalMonad (f n) s) # map (\<lambda>n. the (evalMonad (f n) s)) ns' proof (prove)
goal (1 subgoal):
 1. the (evalMonad (return (the (evalMonad (f n) s) # the (evalMonad (mapM f ns') s))) s) = the (evalMonad (f n) s) # map (\<lambda>n. the (evalMonad (f n) s)) ns' proof (prove)
goal (1 subgoal):
 1. the (evalMonad (mapM f ns') s) = map (\<lambda>n. the (evalMonad (f n) s)) ns' proof (prove)
goal (2 subgoals):
 1. \<And>n. n \<in> set ns' \<Longrightarrow> det (f n)
 2. map (\<lambda>n. the (evalMonad (f n) s)) ns' = map (\<lambda>n. the (evalMonad (f n) s)) ns' proof (prove)
goal (2 subgoals):
 1. \<And>na. na \<in> set ns' \<Longrightarrow> na \<in> set (n # ns')
 2. map (\<lambda>n. the (evalMonad (f n) s)) ns' = map (\<lambda>n. the (evalMonad (f n) s)) ns' proof (prove)
goal (1 subgoal):
 1. map (\<lambda>n. the (evalMonad (f n) s)) ns' = map (\<lambda>n. the (evalMonad (f n) s)) ns' proof (prove)
goal:
No subgoals! proof (state)
this:
the (evalMonad (mapM f (n # ns')) s) = map (\<lambda>n. the (evalMonad (f n) s)) (n # ns')

goal:
No subgoals!