theory TcbAcc_R

lemma threadSet_not_inQ:
  "\<lbrace>ct_not_inQ and (\<lambda>s. (\<exists>tcb. tcbQueued (F tcb) \<and> \<not> tcbQueued tcb)
                          \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread
                          \<longrightarrow> t \<noteq> ksCurThread s)\<rbrace>
   threadSet F t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (simp add: threadSet_def ct_not_inQ_def) apply (wp) apply (rule hoare_convert_imp [OF setObject_nosch]) apply (rule updateObject_tcb_inv) apply (wps setObject_ct_inv) apply (wp setObject_tcb_strongest getObject_tcb_wp)+ apply (case_tac "t = ksCurThread s") apply (clarsimp simp: obj_at'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ and (\<lambda>s. (\<exists>tcb. tcbQueued (F tcb) \<and> \<not> tcbQueued tcb) \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> t \<noteq> ksCurThread s)\<rbrace> threadSet F t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>s. (\<exists>tcb. tcbQueued (F tcb) \<and> \<not> tcbQueued tcb) \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> t \<noteq> ksCurThread s)\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> setObject t (F tcb) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getObject t \<lbrace>?B1\<rbrace>
 3. \<And>s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>s. (\<exists>tcb. tcbQueued (F tcb) \<and> \<not> tcbQueued tcb) \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> t \<noteq> ksCurThread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>tcb p q n ko. \<lbrace>\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace> updateObject (F tcb) p q n ko \<lbrace>\<lambda>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>tcb. \<lbrace>?R2 tcb\<rbrace> setObject t (F tcb) \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getObject t \<lbrace>\<lambda>tcb s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ?R2 tcb s\<rbrace>
 4. \<And>s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>s. (\<exists>tcb. tcbQueued (F tcb) \<and> \<not> tcbQueued tcb) \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> t \<noteq> ksCurThread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?R2 tcb\<rbrace> setObject t (F tcb) \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getObject t \<lbrace>\<lambda>tcb s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ?R2 tcb s\<rbrace>
 3. \<And>s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>s. (\<exists>tcb. tcbQueued (F tcb) \<and> \<not> tcbQueued tcb) \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> t \<noteq> ksCurThread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb prev_s. \<lbrace>?P8 tcb prev_s\<rbrace> setObject t (F tcb) \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) (ksCurThread prev_s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> getObject t \<lbrace>\<lambda>tcb s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ?P8 tcb s s\<rbrace>
 3. \<And>s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>s. (\<exists>tcb. tcbQueued (F tcb) \<and> \<not> tcbQueued tcb) \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> t \<noteq> ksCurThread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>s. (\<exists>tcb. tcbQueued (F tcb) \<and> \<not> tcbQueued tcb) \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> t \<noteq> ksCurThread s)) s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> (if t = ksCurThread s then (Not \<circ> tcbQueued) (F ta) else obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>s. (\<exists>tcb. tcbQueued (F tcb) \<and> \<not> tcbQueued tcb) \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> t \<noteq> ksCurThread s)) s; t = ksCurThread s\<rbrakk> \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> (if t = ksCurThread s then (Not \<circ> tcbQueued) (F ta) else obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s)))
 2. \<And>s. \<lbrakk>((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>s. (\<exists>tcb. tcbQueued (F tcb) \<and> \<not> tcbQueued tcb) \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> t \<noteq> ksCurThread s)) s; t \<noteq> ksCurThread s\<rbrakk> \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> (if t = ksCurThread s then (Not \<circ> tcbQueued) (F ta) else obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s))) proof (prove)
goal:
No subgoals!