theory TcbAcc_R

lemma tcbSchedEnqueue_not_st:
  "(\<And>tcb st qd. P (tcb\<lparr>tcbState := st, tcbQueued := qd\<rparr>) \<longleftrightarrow> P tcb)
     \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. obj_at' P t'\<rbrace>" apply (simp add: tcbSchedEnqueue_def unless_def) apply (wp threadGet_wp | simp)+ apply (clarsimp simp: obj_at'_def) apply (case_tac obja) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb st qd. P (tcbQueued_update (\<lambda>_. qd) (tcbState_update (\<lambda>_. st) tcb)) = P tcb) \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb st qd. P (tcbQueued_update (\<lambda>_. qd) (tcbState_update (\<lambda>_. st) tcb)) = P tcb) \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> do queued <- threadGet tcbQueued t;
when (\<not> queued) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
od \<lbrace>\<lambda>_. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>tcb st qd. P (tcbQueued_update (\<lambda>_. qd) (tcbState_update (\<lambda>_. st) tcb)) = P tcb; obj_at' P t' s\<rbrakk> \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>tcb. (\<not> tcbQueued tcb \<longrightarrow> ko_at' tcb t s \<and> (\<exists>tcb. ko_at' tcb t s) \<and> obj_at' (\<lambda>a. (t = t' \<longrightarrow> P (tcbQueued_update (\<lambda>_. True) a)) \<and> (t \<noteq> t' \<longrightarrow> P a)) t' s) \<and> (tcbQueued tcb \<longrightarrow> ko_at' tcb t s)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko obj koa obja. \<lbrakk>\<And>tcb st qd. P (tcbQueued_update (\<lambda>_. qd) (tcbState_update (\<lambda>_. st) tcb)) = P tcb; ksPSpace s t' = Some ko; is_aligned t' (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; P obj; ps_clear t' (objBitsKO ko) s; ksPSpace s t = Some koa; is_aligned t (objBitsKO koa); ps_clear t (objBitsKO koa) s; fst (projectKO koa s) = {(obja, s)}\<rbrakk> \<Longrightarrow> \<exists>tcb. (\<not> tcbQueued tcb \<longrightarrow> obja = tcb \<and> (t = t' \<longrightarrow> P (tcbQueued_update (\<lambda>_. True) obj))) \<and> (tcbQueued tcb \<longrightarrow> obja = tcb) proof (prove)
goal (1 subgoal):
 1. \<And>s ko obj koa obja x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>\<And>tcb st qd. P (tcbQueued_update (\<lambda>_. qd) (tcbState_update (\<lambda>_. st) tcb)) = P tcb; ksPSpace s t' = Some ko; is_aligned t' (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; P obj; ps_clear t' (objBitsKO ko) s; ksPSpace s t = Some koa; is_aligned t (objBitsKO koa); ps_clear t (objBitsKO koa) s; fst (projectKO koa s) = {(obja, s)}; obja = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<exists>tcb. (\<not> tcbQueued tcb \<longrightarrow> obja = tcb \<and> (t = t' \<longrightarrow> P (tcbQueued_update (\<lambda>_. True) obj))) \<and> (tcbQueued tcb \<longrightarrow> obja = tcb) proof (prove)
goal:
No subgoals!