theory Schedule_R

lemma tcbSchedDequeue_iflive'[wp]:
  "\<lbrace>if_live_then_nonz_cap'\<rbrace> tcbSchedDequeue tcb \<lbrace>\<lambda>_. if_live_then_nonz_cap'\<rbrace>" apply (simp add: tcbSchedDequeue_def) apply (wp threadSet_iflive' hoare_when_weak_wp | simp add: crunch_simps)+ apply ((wp | clarsimp simp: bitmap_fun_defs)+)[1]  (* deal with removeFromBitmap *)
       apply (wp threadSet_iflive' hoare_when_weak_wp | simp add: crunch_simps)+ apply (rule_tac Q="\<lambda>rv. \<top>" in hoare_post_imp, fastforce) apply (wp | simp add: crunch_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap'\<rbrace> tcbSchedDequeue tcb \<lbrace>\<lambda>_. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap'\<rbrace> do queued <- threadGet tcbQueued tcb;
when queued (do tdom <- threadGet tcbDomain tcb;
prio <- threadGet tcbPriority tcb;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> tcb) queue);
y <- when (null (filter (\<lambda>x. x \<noteq> tcb) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) tcb
od)
od \<lbrace>\<lambda>_. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>tdom prio. \<lbrace>\<lambda>s. ((\<exists>tcba. tcbBoundNotification tcba = None \<and> (\<exists>y. tcbBoundNotification tcba = Some y) \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s) \<and> ((\<exists>tcba. (tcbState tcba = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcba)) \<and> tcbState tcba \<noteq> Structures_H.thread_state.Inactive \<and> tcbState tcba \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s)\<rbrace> removeFromBitmap tdom prio \<lbrace>\<lambda>rv s. ((\<exists>tcba. tcbBoundNotification tcba = None \<and> (\<exists>y. tcbBoundNotification tcba = Some y) \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s) \<and> ((\<exists>tcba. (tcbState tcba = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcba)) \<and> tcbState tcba \<noteq> Structures_H.thread_state.Inactive \<and> tcbState tcba \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s)\<rbrace>
 2. \<And>queued tdom prio queue. \<lbrace>?B5 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> tcb) queue) \<lbrace>\<lambda>y s. if_live_then_nonz_cap' s \<and> ((\<exists>tcba. \<not> tcbBoundNotification tcba \<noteq> None \<and> tcbBoundNotification (tcbQueued_update (\<lambda>_. False) tcba) \<noteq> None \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s) \<and> ((\<exists>tcba. (tcbState tcba = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcba)) \<and> tcbState (tcbQueued_update (\<lambda>_. False) tcba) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (tcbQueued_update (\<lambda>_. False) tcba) \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s) \<and> ((\<exists>tcba. \<not> tcbQueued tcba \<and> tcbQueued (tcbQueued_update (\<lambda>_. False) tcba) \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s)\<rbrace>
 3. \<And>queued tdom prio. \<lbrace>?B4 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B5 queued tdom prio\<rbrace>
 4. \<And>queued tdom. \<lbrace>?B3 queued tdom\<rbrace> threadGet tcbPriority tcb \<lbrace>?B4 queued tdom\<rbrace>
 5. \<And>queued. \<lbrace>if_live_then_nonz_cap'\<rbrace> threadGet tcbDomain tcb \<lbrace>?B3 queued\<rbrace>
 6. \<lbrace>?Q\<rbrace> threadGet tcbQueued tcb \<lbrace>\<lambda>queued. if_live_then_nonz_cap'\<rbrace>
 7. \<And>s. if_live_then_nonz_cap' s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>queued tdom prio queue. \<lbrace>?B5 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> tcb) queue) \<lbrace>\<lambda>y s. if_live_then_nonz_cap' s \<and> ((\<exists>tcba. \<not> tcbBoundNotification tcba \<noteq> None \<and> tcbBoundNotification (tcbQueued_update (\<lambda>_. False) tcba) \<noteq> None \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s) \<and> ((\<exists>tcba. (tcbState tcba = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcba)) \<and> tcbState (tcbQueued_update (\<lambda>_. False) tcba) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (tcbQueued_update (\<lambda>_. False) tcba) \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s) \<and> ((\<exists>tcba. \<not> tcbQueued tcba \<and> tcbQueued (tcbQueued_update (\<lambda>_. False) tcba) \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s)\<rbrace>
 2. \<And>queued tdom prio. \<lbrace>?B4 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B5 queued tdom prio\<rbrace>
 3. \<And>queued tdom. \<lbrace>?B3 queued tdom\<rbrace> threadGet tcbPriority tcb \<lbrace>?B4 queued tdom\<rbrace>
 4. \<And>queued. \<lbrace>if_live_then_nonz_cap'\<rbrace> threadGet tcbDomain tcb \<lbrace>?B3 queued\<rbrace>
 5. \<lbrace>?Q\<rbrace> threadGet tcbQueued tcb \<lbrace>\<lambda>queued. if_live_then_nonz_cap'\<rbrace>
 6. \<And>s. if_live_then_nonz_cap' s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>queued tdom prio queue. \<lbrace>?B5 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> tcb) queue) \<lbrace>\<lambda>y s. if_live_then_nonz_cap' s \<and> ((\<exists>tcba. \<not> tcbBoundNotification tcba \<noteq> None \<and> tcbBoundNotification (tcbQueued_update (\<lambda>_. False) tcba) \<noteq> None \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s) \<and> ((\<exists>tcba. (tcbState tcba = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcba)) \<and> tcbState (tcbQueued_update (\<lambda>_. False) tcba) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (tcbQueued_update (\<lambda>_. False) tcba) \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s) \<and> ((\<exists>tcba. \<not> tcbQueued tcba \<and> tcbQueued (tcbQueued_update (\<lambda>_. False) tcba) \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s)\<rbrace>
 2. \<And>queued tdom prio. \<lbrace>?B4 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B5 queued tdom prio\<rbrace>
 3. \<And>queued tdom. \<lbrace>?B3 queued tdom\<rbrace> threadGet tcbPriority tcb \<lbrace>?B4 queued tdom\<rbrace>
 4. \<And>queued. \<lbrace>if_live_then_nonz_cap'\<rbrace> threadGet tcbDomain tcb \<lbrace>?B3 queued\<rbrace>
 5. \<lbrace>?Q\<rbrace> threadGet tcbQueued tcb \<lbrace>\<lambda>queued. if_live_then_nonz_cap'\<rbrace>
 6. \<And>s. if_live_then_nonz_cap' s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>queued tdom prio queue. \<lbrace>?P'32 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> tcb) queue) \<lbrace>\<lambda>rv s. ((\<exists>tcba. tcbBoundNotification tcba = None \<and> (\<exists>y. tcbBoundNotification tcba = Some y) \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s) \<and> ((\<exists>tcba. (tcbState tcba = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcba)) \<and> tcbState tcba \<noteq> Structures_H.thread_state.Inactive \<and> tcbState tcba \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcba tcb s) \<longrightarrow> ex_nonz_cap_to' tcb s)\<rbrace>
 2. \<And>queued tdom prio. \<lbrace>?B4 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>queue s. if_live_then_nonz_cap' s \<and> ?P'32 queued tdom prio queue s\<rbrace>
 3. \<And>queued tdom. \<lbrace>?B3 queued tdom\<rbrace> threadGet tcbPriority tcb \<lbrace>?B4 queued tdom\<rbrace>
 4. \<And>queued. \<lbrace>if_live_then_nonz_cap'\<rbrace> threadGet tcbDomain tcb \<lbrace>?B3 queued\<rbrace>
 5. \<lbrace>?Q\<rbrace> threadGet tcbQueued tcb \<lbrace>\<lambda>queued. if_live_then_nonz_cap'\<rbrace>
 6. \<And>s. if_live_then_nonz_cap' s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>queued tdom prio queue. \<lbrace>?P'32 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> tcb) queue) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>queued tdom prio. \<lbrace>?B4 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>queue s. if_live_then_nonz_cap' s \<and> ?P'32 queued tdom prio queue s\<rbrace>
 3. \<And>queued tdom. \<lbrace>?B3 queued tdom\<rbrace> threadGet tcbPriority tcb \<lbrace>?B4 queued tdom\<rbrace>
 4. \<And>queued. \<lbrace>if_live_then_nonz_cap'\<rbrace> threadGet tcbDomain tcb \<lbrace>?B3 queued\<rbrace>
 5. \<lbrace>?Q\<rbrace> threadGet tcbQueued tcb \<lbrace>\<lambda>queued. if_live_then_nonz_cap'\<rbrace>
 6. \<And>s. if_live_then_nonz_cap' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!