theory SyscallArgs_C

lemma replyOnRestart_twice':
  "((), s') \<in> fst (replyOnRestart t reply isCall s)
       \<Longrightarrow> replyOnRestart t reply' isCall' s'
             = return () s'" apply (clarsimp simp add: replyOnRestart_def in_monad) apply (drule use_valid [OF _ gts_sp', OF _ TrueI]) apply (case_tac "state = Restart") apply clarsimp apply (drule use_valid [OF _ setThreadState_st_tcb'], simp) apply (simp add: gts_eq when_def cong: bind_apply_cong) apply (simp add: gts_eq when_def cong: bind_apply_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), s') \<in> fst (replyOnRestart t reply isCall s) \<Longrightarrow> replyOnRestart t reply' isCall' s' = return () s' proof (prove)
goal (1 subgoal):
 1. \<And>s'' state. \<lbrakk>(state, s'') \<in> fst (getThreadState t s); state = Structures_H.thread_state.Restart \<longrightarrow> (\<exists>s''a. (isCall \<longrightarrow> ((), s''a) \<in> fst (replyFromKernel t (0, reply) s'')) \<and> (\<not> isCall \<longrightarrow> s''a = s'') \<and> ((), s') \<in> fst (setThreadState Structures_H.thread_state.Running t s''a)); state \<noteq> Structures_H.thread_state.Restart \<longrightarrow> s' = s''\<rbrakk> \<Longrightarrow> (do state <- getThreadState t;
when (state = Structures_H.thread_state.Restart) (do _ <- when isCall' (replyFromKernel t (0, reply'));
setThreadState Structures_H.thread_state.Running t
od)
od) s' = return () s' proof (prove)
goal (1 subgoal):
 1. \<And>s'' state. \<lbrakk>state = Structures_H.thread_state.Restart \<longrightarrow> (\<exists>s''a. (isCall \<longrightarrow> ((), s''a) \<in> fst (replyFromKernel t (0, reply) s'')) \<and> (\<not> isCall \<longrightarrow> s''a = s'') \<and> ((), s') \<in> fst (setThreadState Structures_H.thread_state.Running t s''a)); state \<noteq> Structures_H.thread_state.Restart \<longrightarrow> s' = s''; (st_tcb_at' (\<lambda>st. st = state) t and (\<lambda>a. True)) s''\<rbrakk> \<Longrightarrow> (do state <- getThreadState t;
when (state = Structures_H.thread_state.Restart) (do _ <- when isCall' (replyFromKernel t (0, reply'));
setThreadState Structures_H.thread_state.Running t
od)
od) s' = return () s' proof (prove)
goal (2 subgoals):
 1. \<And>s'' state. \<lbrakk>state = Structures_H.thread_state.Restart \<longrightarrow> (\<exists>s''a. (isCall \<longrightarrow> ((), s''a) \<in> fst (replyFromKernel t (0, reply) s'')) \<and> (\<not> isCall \<longrightarrow> s''a = s'') \<and> ((), s') \<in> fst (setThreadState Structures_H.thread_state.Running t s''a)); state \<noteq> Structures_H.thread_state.Restart \<longrightarrow> s' = s''; (st_tcb_at' (\<lambda>st. st = state) t and (\<lambda>a. True)) s''; state = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> (do state <- getThreadState t;
when (state = Structures_H.thread_state.Restart) (do _ <- when isCall' (replyFromKernel t (0, reply'));
setThreadState Structures_H.thread_state.Running t
od)
od) s' = return () s'
 2. \<And>s'' state. \<lbrakk>state = Structures_H.thread_state.Restart \<longrightarrow> (\<exists>s''a. (isCall \<longrightarrow> ((), s''a) \<in> fst (replyFromKernel t (0, reply) s'')) \<and> (\<not> isCall \<longrightarrow> s''a = s'') \<and> ((), s') \<in> fst (setThreadState Structures_H.thread_state.Running t s''a)); state \<noteq> Structures_H.thread_state.Restart \<longrightarrow> s' = s''; (st_tcb_at' (\<lambda>st. st = state) t and (\<lambda>a. True)) s''; state \<noteq> Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> (do state <- getThreadState t;
when (state = Structures_H.thread_state.Restart) (do _ <- when isCall' (replyFromKernel t (0, reply'));
setThreadState Structures_H.thread_state.Running t
od)
od) s' = return () s' proof (prove)
goal (2 subgoals):
 1. \<And>s'' s''a. \<lbrakk>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) t s''; isCall \<longrightarrow> ((), s''a) \<in> fst (replyFromKernel t (0, reply) s''); \<not> isCall \<longrightarrow> s''a = s''; ((), s') \<in> fst (setThreadState Structures_H.thread_state.Running t s''a)\<rbrakk> \<Longrightarrow> (do state <- getThreadState t;
when (state = Structures_H.thread_state.Restart) (do _ <- when isCall' (replyFromKernel t (0, reply'));
setThreadState Structures_H.thread_state.Running t
od)
od) s' = return () s'
 2. \<And>s'' state. \<lbrakk>state = Structures_H.thread_state.Restart \<longrightarrow> (\<exists>s''a. (isCall \<longrightarrow> ((), s''a) \<in> fst (replyFromKernel t (0, reply) s'')) \<and> (\<not> isCall \<longrightarrow> s''a = s'') \<and> ((), s') \<in> fst (setThreadState Structures_H.thread_state.Running t s''a)); state \<noteq> Structures_H.thread_state.Restart \<longrightarrow> s' = s''; (st_tcb_at' (\<lambda>st. st = state) t and (\<lambda>a. True)) s''; state \<noteq> Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> (do state <- getThreadState t;
when (state = Structures_H.thread_state.Restart) (do _ <- when isCall' (replyFromKernel t (0, reply'));
setThreadState Structures_H.thread_state.Running t
od)
od) s' = return () s' proof (prove)
goal (2 subgoals):
 1. \<And>s'' s''a. \<lbrakk>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) t s''; isCall \<longrightarrow> ((), s''a) \<in> fst (replyFromKernel t (0, reply) s''); \<not> isCall \<longrightarrow> s''a = s''; st_tcb_at' (\<lambda>s. s = Structures_H.thread_state.Running) t s'\<rbrakk> \<Longrightarrow> (do state <- getThreadState t;
when (state = Structures_H.thread_state.Restart) (do _ <- when isCall' (replyFromKernel t (0, reply'));
setThreadState Structures_H.thread_state.Running t
od)
od) s' = return () s'
 2. \<And>s'' state. \<lbrakk>state = Structures_H.thread_state.Restart \<longrightarrow> (\<exists>s''a. (isCall \<longrightarrow> ((), s''a) \<in> fst (replyFromKernel t (0, reply) s'')) \<and> (\<not> isCall \<longrightarrow> s''a = s'') \<and> ((), s') \<in> fst (setThreadState Structures_H.thread_state.Running t s''a)); state \<noteq> Structures_H.thread_state.Restart \<longrightarrow> s' = s''; (st_tcb_at' (\<lambda>st. st = state) t and (\<lambda>a. True)) s''; state \<noteq> Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> (do state <- getThreadState t;
when (state = Structures_H.thread_state.Restart) (do _ <- when isCall' (replyFromKernel t (0, reply'));
setThreadState Structures_H.thread_state.Running t
od)
od) s' = return () s' proof (prove)
goal (1 subgoal):
 1. \<And>s'' state. \<lbrakk>state = Structures_H.thread_state.Restart \<longrightarrow> (\<exists>s''a. (isCall \<longrightarrow> ((), s''a) \<in> fst (replyFromKernel t (0, reply) s'')) \<and> (\<not> isCall \<longrightarrow> s''a = s'') \<and> ((), s') \<in> fst (setThreadState Structures_H.thread_state.Running t s''a)); state \<noteq> Structures_H.thread_state.Restart \<longrightarrow> s' = s''; (st_tcb_at' (\<lambda>st. st = state) t and (\<lambda>a. True)) s''; state \<noteq> Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> (do state <- getThreadState t;
when (state = Structures_H.thread_state.Restart) (do _ <- when isCall' (replyFromKernel t (0, reply'));
setThreadState Structures_H.thread_state.Running t
od)
od) s' = return () s' proof (prove)
goal:
No subgoals!