theory TcbAcc_R

lemma threadSet_iflive'T:
  assumes x: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases. getF (F tcb) = getF tcb"
  shows
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s
      \<and> ((\<exists>tcb. \<not> bound (tcbBoundNotification tcb) \<and> bound (tcbBoundNotification (F tcb))
              \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s)
      \<and> ((\<exists>tcb. (tcbState tcb = Inactive \<or> tcbState tcb = IdleThreadState)
              \<and> tcbState (F tcb) \<noteq> Inactive
              \<and> tcbState (F tcb) \<noteq> IdleThreadState
              \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s)
      \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (F tcb)
              \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s)\<rbrace>
     threadSet F t
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: threadSet_def) apply (wp setObject_tcb_iflive' getObject_tcb_wp) apply (clarsimp simp: obj_at'_def projectKOs) apply (subst conj_assoc[symmetric], subst imp_disjL[symmetric]) apply (subst conj_assoc[symmetric], subst imp_disjL[symmetric]) apply (rule conjI) apply (rule impI, clarsimp) apply (erule if_live_then_nonz_capE') apply (clarsimp simp: ko_wp_at'_def) apply (clarsimp simp: bspec_split [OF spec [OF x]]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> ((\<exists>tcb. \<not> tcbBoundNotification tcb \<noteq> None \<and> tcbBoundNotification (F tcb) \<noteq> None \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. (tcbState tcb = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcb)) \<and> tcbState (F tcb) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F tcb) \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (F tcb) \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s)\<rbrace> threadSet F t \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> ((\<exists>tcb. tcbBoundNotification tcb = None \<and> (\<exists>y. tcbBoundNotification (F tcb) = Some y) \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. (tcbState tcb = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcb)) \<and> tcbState (F tcb) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F tcb) \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (F tcb) \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s)\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if_live_then_nonz_cap' s \<and> ((\<exists>tcb. tcbBoundNotification tcb = None \<and> (\<exists>y. tcbBoundNotification (F tcb) = Some y) \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. (tcbState tcb = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcb)) \<and> tcbState (F tcb) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F tcb) \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (F tcb) \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> if_live_then_nonz_cap' s \<and> (live' (injectKO (F ta)) \<longrightarrow> ex_nonz_cap_to' t s) \<and> obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF (F ta)) t s) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>if_live_then_nonz_cap' s; tcbBoundNotification obj = None \<and> (\<exists>y. tcbBoundNotification (F obj) = Some y) \<longrightarrow> ex_nonz_cap_to' t s; (tcbState obj = Structures_H.thread_state.Inactive \<or> idle' (tcbState obj)) \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s; \<not> tcbQueued obj \<and> tcbQueued (F obj) \<longrightarrow> ex_nonz_cap_to' t s; ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> ((\<exists>y. tcbBoundNotification (F obj) = Some y) \<longrightarrow> ex_nonz_cap_to' t s) \<and> (tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s) \<and> (tcbQueued (F obj) \<longrightarrow> ex_nonz_cap_to' t s) \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF obj = getF (F obj)) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>if_live_then_nonz_cap' s; tcbBoundNotification obj = None \<and> (\<exists>y. tcbBoundNotification (F obj) = Some y) \<longrightarrow> ex_nonz_cap_to' t s; (tcbState obj = Structures_H.thread_state.Inactive \<or> idle' (tcbState obj)) \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s; \<not> tcbQueued obj \<and> tcbQueued (F obj) \<longrightarrow> ex_nonz_cap_to' t s; ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> ((\<exists>y. tcbBoundNotification (F obj) = Some y) \<or> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s) \<and> (tcbQueued (F obj) \<longrightarrow> ex_nonz_cap_to' t s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF obj = getF (F obj)) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>if_live_then_nonz_cap' s; tcbBoundNotification obj = None \<and> (\<exists>y. tcbBoundNotification (F obj) = Some y) \<longrightarrow> ex_nonz_cap_to' t s; (tcbState obj = Structures_H.thread_state.Inactive \<or> idle' (tcbState obj)) \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s; \<not> tcbQueued obj \<and> tcbQueued (F obj) \<longrightarrow> ex_nonz_cap_to' t s; ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> (((\<exists>y. tcbBoundNotification (F obj) = Some y) \<or> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState) \<or> tcbQueued (F obj) \<longrightarrow> ex_nonz_cap_to' t s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF obj = getF (F obj)) proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>if_live_then_nonz_cap' s; tcbBoundNotification obj = None \<and> (\<exists>y. tcbBoundNotification (F obj) = Some y) \<longrightarrow> ex_nonz_cap_to' t s; (tcbState obj = Structures_H.thread_state.Inactive \<or> idle' (tcbState obj)) \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s; \<not> tcbQueued obj \<and> tcbQueued (F obj) \<longrightarrow> ex_nonz_cap_to' t s; ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> ((\<exists>y. tcbBoundNotification (F obj) = Some y) \<or> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState) \<or> tcbQueued (F obj) \<longrightarrow> ex_nonz_cap_to' t s
 2. \<And>s obj. \<lbrakk>if_live_then_nonz_cap' s; tcbBoundNotification obj = None \<and> (\<exists>y. tcbBoundNotification (F obj) = Some y) \<longrightarrow> ex_nonz_cap_to' t s; (tcbState obj = Structures_H.thread_state.Inactive \<or> idle' (tcbState obj)) \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s; \<not> tcbQueued obj \<and> tcbQueued (F obj) \<longrightarrow> ex_nonz_cap_to' t s; ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF obj = getF (F obj) proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>if_live_then_nonz_cap' s; ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s; (\<exists>y. tcbBoundNotification (F obj) = Some y) \<or> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState \<or> tcbQueued (F obj); (\<exists>y. tcbBoundNotification obj = Some y) \<or> tcbBoundNotification (F obj) = None; tcbState obj \<noteq> Structures_H.thread_state.Inactive \<and> tcbState obj \<noteq> Structures_H.thread_state.IdleThreadState \<or> tcbState (F obj) = Structures_H.thread_state.Inactive \<or> idle' (tcbState (F obj)); tcbQueued obj \<or> \<not> tcbQueued (F obj)\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' t s
 2. \<And>s obj. \<lbrakk>if_live_then_nonz_cap' s; tcbBoundNotification obj = None \<and> (\<exists>y. tcbBoundNotification (F obj) = Some y) \<longrightarrow> ex_nonz_cap_to' t s; (tcbState obj = Structures_H.thread_state.Inactive \<or> idle' (tcbState obj)) \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s; \<not> tcbQueued obj \<and> tcbQueued (F obj) \<longrightarrow> ex_nonz_cap_to' t s; ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF obj = getF (F obj) proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s; (\<exists>y. tcbBoundNotification (F obj) = Some y) \<or> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState \<or> tcbQueued (F obj); (\<exists>y. tcbBoundNotification obj = Some y) \<or> tcbBoundNotification (F obj) = None; tcbState obj \<noteq> Structures_H.thread_state.Inactive \<and> tcbState obj \<noteq> Structures_H.thread_state.IdleThreadState \<or> tcbState (F obj) = Structures_H.thread_state.Inactive \<or> idle' (tcbState (F obj)); tcbQueued obj \<or> \<not> tcbQueued (F obj)\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s
 2. \<And>s obj. \<lbrakk>if_live_then_nonz_cap' s; tcbBoundNotification obj = None \<and> (\<exists>y. tcbBoundNotification (F obj) = Some y) \<longrightarrow> ex_nonz_cap_to' t s; (tcbState obj = Structures_H.thread_state.Inactive \<or> idle' (tcbState obj)) \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s; \<not> tcbQueued obj \<and> tcbQueued (F obj) \<longrightarrow> ex_nonz_cap_to' t s; ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF obj = getF (F obj) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>if_live_then_nonz_cap' s; tcbBoundNotification obj = None \<and> (\<exists>y. tcbBoundNotification (F obj) = Some y) \<longrightarrow> ex_nonz_cap_to' t s; (tcbState obj = Structures_H.thread_state.Inactive \<or> idle' (tcbState obj)) \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (F obj) \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s; \<not> tcbQueued obj \<and> tcbQueued (F obj) \<longrightarrow> ex_nonz_cap_to' t s; ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF obj = getF (F obj) proof (prove)
goal:
No subgoals!