theory Schedule_R

lemma chooseThread_nosch:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
  chooseThread
  \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" unfolding chooseThread_def Let_def curDomain_def supply if_split[split del] apply (simp only: return_bind, simp) apply (wp findM_inv | simp)+ apply (case_tac queue) apply (wp stt_nosch | simp add: curDomain_def bitmap_fun_defs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> chooseThread \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do curdom <- if 1 < numDomains then gets ksCurDomain else return 0;
l1 <- getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0 then do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do curdom <- if 1 < numDomains then gets ksCurDomain else return 0;
l1 <- getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0 then do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do curdom <- if Suc 0 < numDomains then gets ksCurDomain else return 0;
l1 <- getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0 then do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od else global.switchToIdleThread
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>curdom l1 prio queue x. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?B9 curdom l1 prio queue x ()\<rbrace> global.switchToThread (hd queue) \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>
 2. \<And>curdom l1 prio queue x. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?B8 curdom l1 prio queue x\<rbrace> haskell_assert x [] \<lbrace>?B9 curdom l1 prio queue x\<rbrace>
 3. \<And>curdom l1 prio queue. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?B7 curdom l1 prio queue\<rbrace> isRunnable (head queue) \<lbrace>?B8 curdom l1 prio queue\<rbrace>
 4. \<And>curdom l1 prio. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?B6 curdom l1 prio\<rbrace> getQueue curdom prio \<lbrace>?B7 curdom l1 prio\<rbrace>
 5. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q5 curdom l1\<rbrace> getHighestPrio curdom \<lbrace>?B6 curdom l1\<rbrace>
 6. \<And>curdom l1. \<not> l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?R5 curdom l1\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>
 7. \<And>curdom. \<lbrace>?B3 curdom\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>l1 s. (l1 \<noteq> 0 \<longrightarrow> ?Q5 curdom l1 s) \<and> (\<not> l1 \<noteq> 0 \<longrightarrow> ?R5 curdom l1 s)\<rbrace>
 8. \<lbrace>?Q2\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>?B3\<rbrace>
 9. \<And>s. P (ksSchedulerAction s) \<Longrightarrow> ?Q2 s proof (prove)
goal (10 subgoals):
 1. \<And>curdom l1 prio queue x. \<lbrakk>l1 \<noteq> 0; queue = []\<rbrakk> \<Longrightarrow> \<lbrace>?B9 curdom l1 prio queue x ()\<rbrace> global.switchToThread (hd queue) \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>
 2. \<And>curdom l1 prio queue x a list. \<lbrakk>l1 \<noteq> 0; queue = a # list\<rbrakk> \<Longrightarrow> \<lbrace>?B9 curdom l1 prio queue x ()\<rbrace> global.switchToThread (hd queue) \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>
 3. \<And>curdom l1 prio queue x. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?B8 curdom l1 prio queue x\<rbrace> haskell_assert x [] \<lbrace>?B9 curdom l1 prio queue x\<rbrace>
 4. \<And>curdom l1 prio queue. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?B7 curdom l1 prio queue\<rbrace> isRunnable (head queue) \<lbrace>?B8 curdom l1 prio queue\<rbrace>
 5. \<And>curdom l1 prio. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?B6 curdom l1 prio\<rbrace> getQueue curdom prio \<lbrace>?B7 curdom l1 prio\<rbrace>
 6. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q5 curdom l1\<rbrace> getHighestPrio curdom \<lbrace>?B6 curdom l1\<rbrace>
 7. \<And>curdom l1. \<not> l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?R5 curdom l1\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>
 8. \<And>curdom. \<lbrace>?B3 curdom\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>l1 s. (l1 \<noteq> 0 \<longrightarrow> ?Q5 curdom l1 s) \<and> (\<not> l1 \<noteq> 0 \<longrightarrow> ?R5 curdom l1 s)\<rbrace>
 9. \<lbrace>?Q2\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>?B3\<rbrace>
 10. \<And>s. P (ksSchedulerAction s) \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!