theory Ipc_DR

lemma evalMonad_mapM:
  assumes as:"evalMonad (mapM f ls) s = Some v"
  assumes "\<And>l. empty_when_fail (f l)"
  assumes "\<And>P l. weak_det_spec P (f l)"
  assumes wp: "\<And>s l. \<lbrace>(=) s\<rbrace> f l \<lbrace>\<lambda>r. (=) s\<rbrace>"
  shows "v = (map (\<lambda>p. the (evalMonad (f p) s)) ls)" using as proof (induct ls arbitrary: v) case Nil thus ?case by (clarsimp simp:evalMonad_def mapM_def sequence_def return_def) next case (Cons l ls) show ?case using Cons.prems apply clarsimp apply (clarsimp simp:mapM_Cons) apply (subst (asm) evalMonad_compose) apply (simp add: Cons assms)+ apply (clarsimp split:option.splits) apply (subst (asm) evalMonad_compose) apply (rule empty_when_fail_mapM) apply (simp add: Cons assms)+ apply (rule weak_det_spec_mapM) apply (simp add: Cons assms)+ apply (wp mapM_wp) apply (simp add: Cons assms)+ apply fastforce apply simp apply (clarsimp split:option.splits) apply (simp add: Cons) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. v = map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
using this:
evalMonad (mapM f ls) s = Some v

goal (1 subgoal):
 1. v = map (\<lambda>p. the (evalMonad (f p) s)) ls proof (state)
goal (2 subgoals):
 1. \<And>v. evalMonad (mapM f []) s = Some v \<Longrightarrow> v = map (\<lambda>p. the (evalMonad (f p) s)) []
 2. \<And>a ls v. \<lbrakk>\<And>v. evalMonad (mapM f ls) s = Some v \<Longrightarrow> v = map (\<lambda>p. the (evalMonad (f p) s)) ls; evalMonad (mapM f (a # ls)) s = Some v\<rbrakk> \<Longrightarrow> v = map (\<lambda>p. the (evalMonad (f p) s)) (a # ls) proof (state)
this:
evalMonad (mapM f []) s = Some v

goal (2 subgoals):
 1. \<And>v. evalMonad (mapM f []) s = Some v \<Longrightarrow> v = map (\<lambda>p. the (evalMonad (f p) s)) []
 2. \<And>a ls v. \<lbrakk>\<And>v. evalMonad (mapM f ls) s = Some v \<Longrightarrow> v = map (\<lambda>p. the (evalMonad (f p) s)) ls; evalMonad (mapM f (a # ls)) s = Some v\<rbrakk> \<Longrightarrow> v = map (\<lambda>p. the (evalMonad (f p) s)) (a # ls) proof (prove)
using this:
evalMonad (mapM f []) s = Some v

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

goal (1 subgoal):
 1. \<And>a ls v. \<lbrakk>\<And>v. evalMonad (mapM f ls) s = Some v \<Longrightarrow> v = map (\<lambda>p. the (evalMonad (f p) s)) ls; evalMonad (mapM f (a # ls)) s = Some v\<rbrakk> \<Longrightarrow> v = map (\<lambda>p. the (evalMonad (f p) s)) (a # ls) proof (state)
goal (1 subgoal):
 1. \<And>a ls v. \<lbrakk>\<And>v. evalMonad (mapM f ls) s = Some v \<Longrightarrow> v = map (\<lambda>p. the (evalMonad (f p) s)) ls; evalMonad (mapM f (a # ls)) s = Some v\<rbrakk> \<Longrightarrow> v = map (\<lambda>p. the (evalMonad (f p) s)) (a # ls) proof (state)
this:
evalMonad (mapM f ls) s = Some ?v \<Longrightarrow> ?v = map (\<lambda>p. the (evalMonad (f p) s)) ls
evalMonad (mapM f (l # ls)) s = Some v

goal (1 subgoal):
 1. \<And>a ls v. \<lbrakk>\<And>v. evalMonad (mapM f ls) s = Some v \<Longrightarrow> v = map (\<lambda>p. the (evalMonad (f p) s)) ls; evalMonad (mapM f (a # ls)) s = Some v\<rbrakk> \<Longrightarrow> v = map (\<lambda>p. the (evalMonad (f p) s)) (a # ls) proof (prove)
goal (1 subgoal):
 1. v = map (\<lambda>p. the (evalMonad (f p) s)) (l # ls) proof (prove)
using this:
evalMonad (mapM f (l # ls)) s = Some v

goal (1 subgoal):
 1. v = map (\<lambda>p. the (evalMonad (f p) s)) (l # ls) proof (prove)
goal (1 subgoal):
 1. evalMonad (mapM f (l # ls)) s = Some v \<Longrightarrow> v = the (evalMonad (f l) s) # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (1 subgoal):
 1. evalMonad (do y <- f l;
ys <- mapM f ls;
return (y # ys)
od) s = Some v \<Longrightarrow> v = the (evalMonad (f l) s) # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (4 subgoals):
 1. empty_when_fail (f l)
 2. weak_det_spec ((=) s) (f l)
 3. \<And>s. \<lbrace>(=) s\<rbrace> f l \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. (case evalMonad (f l) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (do ys <- mapM f ls;
return (r # ys)
od) s) = Some v \<Longrightarrow> v = the (evalMonad (f l) s) # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (1 subgoal):
 1. (case evalMonad (f l) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (do ys <- mapM f ls;
return (r # ys)
od) s) = Some v \<Longrightarrow> v = the (evalMonad (f l) s) # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evalMonad (f l) s = Some x2; evalMonad (do ys <- mapM f ls;
return (x2 # ys)
od) s = Some v\<rbrakk> \<Longrightarrow> v = x2 # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (4 subgoals):
 1. \<And>x2. evalMonad (f l) s = Some x2 \<Longrightarrow> empty_when_fail (mapM f ls)
 2. \<And>x2. evalMonad (f l) s = Some x2 \<Longrightarrow> weak_det_spec ((=) s) (mapM f ls)
 3. \<And>x2 sa. evalMonad (f l) s = Some x2 \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM f ls \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>x2. \<lbrakk>evalMonad (f l) s = Some x2; (case evalMonad (mapM f ls) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (x2 # r)) s) = Some v\<rbrakk> \<Longrightarrow> v = x2 # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (4 subgoals):
 1. \<And>x2 P la. evalMonad (f l) s = Some x2 \<Longrightarrow> weak_det_spec P (f la) \<and> empty_when_fail (f la)
 2. \<And>x2. evalMonad (f l) s = Some x2 \<Longrightarrow> weak_det_spec ((=) s) (mapM f ls)
 3. \<And>x2 sa. evalMonad (f l) s = Some x2 \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM f ls \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>x2. \<lbrakk>evalMonad (f l) s = Some x2; (case evalMonad (mapM f ls) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (x2 # r)) s) = Some v\<rbrakk> \<Longrightarrow> v = x2 # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (3 subgoals):
 1. \<And>x2. evalMonad (f l) s = Some x2 \<Longrightarrow> weak_det_spec ((=) s) (mapM f ls)
 2. \<And>x2 sa. evalMonad (f l) s = Some x2 \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM f ls \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>x2. \<lbrakk>evalMonad (f l) s = Some x2; (case evalMonad (mapM f ls) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (x2 # r)) s) = Some v\<rbrakk> \<Longrightarrow> v = x2 # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (3 subgoals):
 1. \<And>x2 r P. evalMonad (f l) s = Some x2 \<Longrightarrow> weak_det_spec P (f r)
 2. \<And>x2 sa. evalMonad (f l) s = Some x2 \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM f ls \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>x2. \<lbrakk>evalMonad (f l) s = Some x2; (case evalMonad (mapM f ls) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (x2 # r)) s) = Some v\<rbrakk> \<Longrightarrow> v = x2 # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (2 subgoals):
 1. \<And>x2 sa. evalMonad (f l) s = Some x2 \<Longrightarrow> \<lbrace>(=) sa\<rbrace> mapM f ls \<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<And>x2. \<lbrakk>evalMonad (f l) s = Some x2; (case evalMonad (mapM f ls) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (x2 # r)) s) = Some v\<rbrakk> \<Longrightarrow> v = x2 # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (4 subgoals):
 1. \<And>x2 sa x. \<lbrakk>evalMonad (f l) s = Some x2; x \<in> ?S21 x2 sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> f x \<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<And>x2 sa. evalMonad (f l) s = Some x2 \<Longrightarrow> set ls \<subseteq> ?S21 x2 sa
 3. \<And>x2 sa saa. \<lbrakk>evalMonad (f l) s = Some x2; sa = saa\<rbrakk> \<Longrightarrow> sa = saa
 4. \<And>x2. \<lbrakk>evalMonad (f l) s = Some x2; (case evalMonad (mapM f ls) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (x2 # r)) s) = Some v\<rbrakk> \<Longrightarrow> v = x2 # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (3 subgoals):
 1. \<And>x2 sa. evalMonad (f l) s = Some x2 \<Longrightarrow> set ls \<subseteq> ?S21 x2 sa
 2. \<And>x2 sa saa. \<lbrakk>evalMonad (f l) s = Some x2; sa = saa\<rbrakk> \<Longrightarrow> sa = saa
 3. \<And>x2. \<lbrakk>evalMonad (f l) s = Some x2; (case evalMonad (mapM f ls) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (x2 # r)) s) = Some v\<rbrakk> \<Longrightarrow> v = x2 # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (2 subgoals):
 1. \<And>x2 sa saa. \<lbrakk>evalMonad (f l) s = Some x2; sa = saa\<rbrakk> \<Longrightarrow> sa = saa
 2. \<And>x2. \<lbrakk>evalMonad (f l) s = Some x2; (case evalMonad (mapM f ls) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (x2 # r)) s) = Some v\<rbrakk> \<Longrightarrow> v = x2 # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evalMonad (f l) s = Some x2; (case evalMonad (mapM f ls) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (x2 # r)) s) = Some v\<rbrakk> \<Longrightarrow> v = x2 # map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a. \<lbrakk>evalMonad (f l) s = Some x2; evalMonad (mapM f ls) s = Some x2a; v = x2 # x2a\<rbrakk> \<Longrightarrow> x2a = map (\<lambda>p. the (evalMonad (f p) s)) ls proof (prove)
goal:
No subgoals! proof (state)
this:
v = map (\<lambda>p. the (evalMonad (f p) s)) (l # ls)

goal:
No subgoals!