theory Schedule_R

lemma setCurThread_invs_no_cicd':
  "\<lbrace>invs_no_cicd' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and tcb_in_cur_domain' t\<rbrace>
     setCurThread t
   \<lbrace>\<lambda>rv. invs'\<rbrace>" proof - have ct_not_inQ_ct: "\<And>s t . \<lbrakk> ct_not_inQ s; obj_at' (\<lambda>x. \<not> tcbQueued x) t s\<rbrakk> \<Longrightarrow> ct_not_inQ (s\<lparr> ksCurThread := t \<rparr>)" apply (simp add: ct_not_inQ_def o_def) done show ?thesis apply (simp add: setCurThread_def) apply wp apply (clarsimp simp add: all_invs_but_ct_idle_or_in_cur_domain'_def invs'_def cur_tcb'_def
                              valid_state'_def Invariants_H.valid_queues_def
                              sch_act_wf ct_in_state'_def state_refs_of'_def
                              ps_clear_def valid_irq_node'_def valid_queues'_def ct_not_inQ_ct
                              ct_idle_or_in_cur_domain'_def
                              bitmapQ_defs valid_queues_no_bitmap_def
                        cong: option.case_cong) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and tcb_in_cur_domain' t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and tcb_in_cur_domain' t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>ct_not_inQ s; obj_at' (\<lambda>x. \<not> tcbQueued x) t s\<rbrakk> \<Longrightarrow> ct_not_inQ (s\<lparr>ksCurThread := t\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>ct_not_inQ ?s; obj_at' (\<lambda>x. \<not> tcbQueued x) ?t ?s\<rbrakk> \<Longrightarrow> ct_not_inQ (?s\<lparr>ksCurThread := ?t\<rparr>)

goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and tcb_in_cur_domain' t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and tcb_in_cur_domain' t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and tcb_in_cur_domain' t\<rbrace> modify (ksCurThread_update (\<lambda>_. t)) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (all_invs_but_ct_idle_or_in_cur_domain' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and tcb_in_cur_domain' t) s \<Longrightarrow> invs' (s\<lparr>ksCurThread := t\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and tcb_in_cur_domain' t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace>

goal:
No subgoals!