theory Orphanage

lemma tcbSchedDequeue_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> \<not> is_active_tcb_ptr tcb_ptr s \<rbrace>
   tcbSchedDequeue tcb_ptr
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding tcbSchedDequeue_def apply (wp setQueue_no_orphans_deq threadSet_no_orphans | clarsimp)+ apply (wp getObject_tcb_wp | clarsimp simp: threadGet_def)+ apply (drule obj_at_ko_at') apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> \<not> is_active_tcb_ptr tcb_ptr s\<rbrace> tcbSchedDequeue tcb_ptr \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> \<not> is_active_tcb_ptr tcb_ptr s\<rbrace> do queued <- threadGet tcbQueued tcb_ptr;
when queued $ do tdom <- threadGet tcbDomain tcb_ptr;
prio <- threadGet tcbPriority tcb_ptr;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> tcb_ptr) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) tcb_ptr
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?P'33 (ds_id True) tdom\<rbrace> threadGet tcbPriority tcb_ptr \<lbrace>\<lambda>rv s. \<exists>tcb_ptra. \<not> is_active_tcb_ptr tcb_ptra s \<and> filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (tdom, rv)) = filter (\<lambda>x. x \<noteq> tcb_ptra) (ksReadyQueues s (tdom, rv))\<rbrace>
 2. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain tcb_ptr \<lbrace>\<lambda>a b. no_orphans b \<and> ?P'33 queued a b\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet tcbQueued tcb_ptr \<lbrace>\<lambda>queued. if queued then ?Q3 queued else no_orphans\<rbrace>
 4. \<And>s. no_orphans s \<and> \<not> is_active_tcb_ptr tcb_ptr s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; \<not> is_active_tcb_ptr tcb_ptr s; tcb_at' tcb_ptr s\<rbrakk> \<Longrightarrow> \<exists>t. (tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s \<and> (\<exists>t. ko_at' t tcb_ptr s \<and> (\<exists>ta. ko_at' ta tcb_ptr s \<and> (\<exists>tcb_ptra. \<not> is_active_tcb_ptr tcb_ptra s \<and> filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (tcbDomain t, tcbPriority ta)) = filter (\<lambda>x. x \<noteq> tcb_ptra) (ksReadyQueues s (tcbDomain t, tcbPriority ta)))))) \<and> (\<not> tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; \<not> is_active_tcb_ptr tcb_ptr s; \<exists>ko. ko_at' ko tcb_ptr s \<and> True\<rbrakk> \<Longrightarrow> \<exists>t. (tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s \<and> (\<exists>t. ko_at' t tcb_ptr s \<and> (\<exists>ta. ko_at' ta tcb_ptr s \<and> (\<exists>tcb_ptra. \<not> is_active_tcb_ptr tcb_ptra s \<and> filter (\<lambda>x. x \<noteq> tcb_ptr) (ksReadyQueues s (tcbDomain t, tcbPriority ta)) = filter (\<lambda>x. x \<noteq> tcb_ptra) (ksReadyQueues s (tcbDomain t, tcbPriority ta)))))) \<and> (\<not> tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s) proof (prove)
goal:
No subgoals!