theory Ipc_DR

lemma dcorres_symb_exec_r_evalMonad:
  assumes wp:"\<And>sa. \<lbrace>(=) sa\<rbrace> f \<lbrace>\<lambda>r. (=) sa\<rbrace>"
  assumes corres:"\<And>rv. evalMonad f s = Some rv \<Longrightarrow> dcorres r P ((=) s) h (g rv)"
  shows "\<lbrakk> empty_when_fail f; weak_det_spec ((=) s) f \<rbrakk> \<Longrightarrow> dcorres r P ((=) s) h (f>>=g)" apply (rule_tac Q'="\<lambda>r. (=) s and K_bind (evalMonad f s = Some r)" in corres_symb_exec_r) apply (rule dcorres_expand_pfx) using corres apply (clarsimp simp:corres_underlying_def) apply (wp wp, simp, rule evalMonad_wp) apply (simp add:wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f\<rbrakk> \<Longrightarrow> dcorres r P ((=) s) h (f >>= g) proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f\<rbrakk> \<Longrightarrow> dcorres r P ((=) s and K_bind (evalMonad f s = Some rv)) h (g rv)
 2. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r. (=) s and K_bind (evalMonad f s = Some r)\<rbrace>
 3. \<And>sa. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> f \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) f proof (prove)
goal (4 subgoals):
 1. \<And>rv sa s'. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; sa = transform s'; P sa; ((=) s and K_bind (evalMonad f s = Some rv)) s'\<rbrakk> \<Longrightarrow> dcorres r ((=) sa) ((=) s') h (g rv)
 2. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r. (=) s and K_bind (evalMonad f s = Some r)\<rbrace>
 3. \<And>sa. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> f \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) f proof (prove)
using this:
evalMonad f s = Some ?rv \<Longrightarrow> dcorres r P ((=) s) h (g ?rv)

goal (4 subgoals):
 1. \<And>rv sa s'. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; sa = transform s'; P sa; ((=) s and K_bind (evalMonad f s = Some rv)) s'\<rbrakk> \<Longrightarrow> dcorres r ((=) sa) ((=) s') h (g rv)
 2. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r. (=) s and K_bind (evalMonad f s = Some r)\<rbrace>
 3. \<And>sa. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> f \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) f proof (prove)
goal (3 subgoals):
 1. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r. (=) s and K_bind (evalMonad f s = Some r)\<rbrace>
 2. \<And>sa. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> f \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) f proof (prove)
goal (5 subgoals):
 1. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f\<rbrakk> \<Longrightarrow> empty_when_fail f
 2. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) f
 3. \<And>sa. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; s = sa\<rbrakk> \<Longrightarrow> s = sa \<and> s = sa
 4. \<And>sa. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> f \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>empty_when_fail f; weak_det_spec ((=) s) f; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) f proof (prove)
goal:
No subgoals!