theory SyscallArgs_C

lemma ccorres_invocationCatch_Inr:
  "ccorres (f \<currency> r) xf P P' hs
   (invocationCatch thread isBlocking isCall injector (Inr v)) c
   =
   ccorres ((f \<circ> Inr) \<currency> r) xf P P' hs
   (do _ \<leftarrow> setThreadState Restart thread;
       doE reply \<leftarrow> performInvocation isBlocking isCall (injector v);
           if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk ()
                         else liftE (replyOnRestart thread reply isCall)
       odE od) c" apply (simp add: invocationCatch_def liftE_bindE o_xo_injector cong: ccorres_all_cong) apply (subst ccorres_liftM_simp[symmetric]) apply (simp add: liftM_def bind_assoc bindE_def) apply (rule_tac f="\<lambda>f. ccorres rvr xs P P' hs f c" for rvr xs in arg_cong) apply (rule ext) apply (rule bind_apply_cong [OF refl])+ apply (simp add: throwError_bind returnOk_bind lift_def liftE_def
                   alternative_bind
            split: sum.split if_split) apply (simp add: throwError_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (f \<currency> r) xf P P' hs (invocationCatch thread isBlocking isCall injector (Inr v)) c = ccorres ((f \<circ> Inr) \<currency> r) xf P P' hs (do _ <- setThreadState Structures_H.thread_state.Restart thread;
doE reply <- global.performInvocation isBlocking isCall (injector v);
if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)
odE
od) c proof (prove)
goal (1 subgoal):
 1. ccorres (f \<currency> r) xf P P' hs (do y <- setThreadState Structures_H.thread_state.Restart thread;
doE reply <- global.performInvocation isBlocking isCall (injector v) >>= case_sum (throwError \<circ> Inr) returnOk;
liftE (if reply = [] then replyOnRestart thread [] isCall \<sqinter> return () else replyOnRestart thread reply isCall)
odE
od) c = ccorres (f \<currency> r \<circ> case_sum (Inl \<circ> Inr) Inr) xf P P' hs (do _ <- setThreadState Structures_H.thread_state.Restart thread;
doE reply <- global.performInvocation isBlocking isCall (injector v);
if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)
odE
od) c proof (prove)
goal (1 subgoal):
 1. ccorres (f \<currency> r) xf P P' hs (do y <- setThreadState Structures_H.thread_state.Restart thread;
doE reply <- global.performInvocation isBlocking isCall (injector v) >>= case_sum (throwError \<circ> Inr) returnOk;
liftE (if reply = [] then replyOnRestart thread [] isCall \<sqinter> return () else replyOnRestart thread reply isCall)
odE
od) c = ccorres (f \<currency> r) xf P P' hs (liftM (case_sum (Inl \<circ> Inr) Inr) (do _ <- setThreadState Structures_H.thread_state.Restart thread;
doE reply <- global.performInvocation isBlocking isCall (injector v);
if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)
odE
od)) c proof (prove)
goal (1 subgoal):
 1. ccorres (f \<currency> r) xf P P' hs (do y <- setThreadState Structures_H.thread_state.Restart thread;
x <- global.performInvocation isBlocking isCall (injector v);
(case x of Inl x \<Rightarrow> (throwError \<circ> Inr) x | Inr x \<Rightarrow> returnOk x) >>= Nondet_Monad.lift (\<lambda>reply. liftE (if reply = [] then replyOnRestart thread [] isCall \<sqinter> return () else replyOnRestart thread reply isCall))
od) c = ccorres (f \<currency> r) xf P P' hs (do x <- setThreadState Structures_H.thread_state.Restart thread;
x <- global.performInvocation isBlocking isCall (injector v);
x <- Nondet_Monad.lift (\<lambda>reply. if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)) x;
return (case x of Inl x \<Rightarrow> (Inl \<circ> Inr) x | Inr x \<Rightarrow> Inr x)
od) c proof (prove)
goal (1 subgoal):
 1. do y <- setThreadState Structures_H.thread_state.Restart thread;
x <- global.performInvocation isBlocking isCall (injector v);
(case x of Inl x \<Rightarrow> (throwError \<circ> Inr) x | Inr x \<Rightarrow> returnOk x) >>= Nondet_Monad.lift (\<lambda>reply. liftE (if reply = [] then replyOnRestart thread [] isCall \<sqinter> return () else replyOnRestart thread reply isCall))
od = do x <- setThreadState Structures_H.thread_state.Restart thread;
x <- global.performInvocation isBlocking isCall (injector v);
x <- Nondet_Monad.lift (\<lambda>reply. if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)) x;
return (case x of Inl x \<Rightarrow> (Inl \<circ> Inr) x | Inr x \<Rightarrow> Inr x)
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do y <- setThreadState Structures_H.thread_state.Restart thread;
x <- global.performInvocation isBlocking isCall (injector v);
(case x of Inl x \<Rightarrow> (throwError \<circ> Inr) x | Inr x \<Rightarrow> returnOk x) >>= Nondet_Monad.lift (\<lambda>reply. liftE (if reply = [] then replyOnRestart thread [] isCall \<sqinter> return () else replyOnRestart thread reply isCall))
od) x = (do x <- setThreadState Structures_H.thread_state.Restart thread;
x <- global.performInvocation isBlocking isCall (injector v);
x <- Nondet_Monad.lift (\<lambda>reply. if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)) x;
return (case x of Inl x \<Rightarrow> (Inl \<circ> Inr) x | Inr x \<Rightarrow> Inr x)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta. \<lbrakk>(rv, st) \<in> fst (setThreadState Structures_H.thread_state.Restart thread x); (rva, sta) \<in> fst (global.performInvocation isBlocking isCall (injector v) st)\<rbrakk> \<Longrightarrow> ((case rva of Inl x \<Rightarrow> (throwError \<circ> Inr) x | Inr x \<Rightarrow> returnOk x) >>= Nondet_Monad.lift (\<lambda>reply. liftE (if reply = [] then replyOnRestart thread [] isCall \<sqinter> return () else replyOnRestart thread reply isCall))) sta = (do x <- Nondet_Monad.lift (\<lambda>reply. if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)) rva;
return (case x of Inl x \<Rightarrow> (Inl \<circ> Inr) x | Inr x \<Rightarrow> Inr x)
od) sta proof (prove)
goal (1 subgoal):
 1. \<And>x st rva sta. \<lbrakk>((), st) \<in> fst (setThreadState Structures_H.thread_state.Restart thread x); (rva, sta) \<in> fst (global.performInvocation isBlocking isCall (injector v) st)\<rbrakk> \<Longrightarrow> \<forall>x1. rva = Inl x1 \<longrightarrow> throwError (Inr x1) sta = return (Inl (Inr x1)) sta proof (prove)
goal:
No subgoals!