theory Orphanage

lemma tcbSchedAppend_almost_no_orphans:
  "\<lbrace> \<lambda>s. almost_no_orphans thread s \<and> valid_queues' s \<rbrace>
   tcbSchedAppend thread
   \<lbrace> \<lambda>_ s. no_orphans s \<rbrace>" unfolding tcbSchedAppend_def apply (wp setQueue_almost_no_orphans_enq[where tcb_ptr=thread] threadSet_no_orphans
            | clarsimp simp: unless_def | simp only: subset_insertI)+ apply (unfold threadGet_def) apply (wp getObject_tcb_wp | clarsimp)+ apply (drule obj_at_ko_at', clarsimp) apply (rule_tac x=ko in exI) apply (clarsimp simp: almost_no_orphans_def no_orphans_def) apply (drule queued_in_queue | simp)+ apply (auto simp: all_queued_tcb_ptrs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans thread s \<and> valid_queues' s\<rbrace> tcbSchedAppend thread \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans thread s \<and> valid_queues' s\<rbrace> do queued <- threadGet tcbQueued thread;
unless queued $ do tdom <- threadGet tcbDomain thread;
prio <- threadGet tcbPriority thread;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [thread];
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) thread
od
od \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadGet tcbQueued thread \<lbrace>\<lambda>queued. if queued then no_orphans else almost_no_orphans thread\<rbrace>
 2. \<And>s. almost_no_orphans thread s \<and> valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> liftM tcbQueued $ getObject thread \<lbrace>\<lambda>queued. if queued then no_orphans else almost_no_orphans thread\<rbrace>
 2. \<And>s. almost_no_orphans thread s \<and> valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>almost_no_orphans thread s; valid_queues' s; tcb_at' thread s\<rbrakk> \<Longrightarrow> \<exists>t. (tcbQueued t \<longrightarrow> ko_at' t thread s \<and> no_orphans s) \<and> (\<not> tcbQueued t \<longrightarrow> ko_at' t thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>almost_no_orphans thread s; valid_queues' s; ko_at' ko thread s\<rbrakk> \<Longrightarrow> \<exists>t. (tcbQueued t \<longrightarrow> ko_at' t thread s \<and> no_orphans s) \<and> (\<not> tcbQueued t \<longrightarrow> ko_at' t thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>almost_no_orphans thread s; valid_queues' s; ko_at' ko thread s\<rbrakk> \<Longrightarrow> (tcbQueued ko \<longrightarrow> ko_at' ko thread s \<and> no_orphans s) \<and> (\<not> tcbQueued ko \<longrightarrow> ko_at' ko thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko tcb_ptr. \<lbrakk>\<forall>ptr. ptr \<in> all_active_tcb_ptrs s \<longrightarrow> ptr = thread \<or> ptr = ksCurThread s \<or> ptr \<in> all_queued_tcb_ptrs s \<or> ksSchedulerAction s = SwitchToThread ptr; valid_queues' s; ko_at' ko thread s; tcbQueued ko; tcb_ptr \<in> all_active_tcb_ptrs s; tcb_ptr \<noteq> ksCurThread s; sch_act_not tcb_ptr s\<rbrakk> \<Longrightarrow> tcb_ptr \<in> all_queued_tcb_ptrs s proof (prove)
goal (1 subgoal):
 1. \<And>s ko tcb_ptr. \<lbrakk>\<forall>ptr. ptr \<in> all_active_tcb_ptrs s \<longrightarrow> ptr = thread \<or> ptr = ksCurThread s \<or> ptr \<in> all_queued_tcb_ptrs s \<or> ksSchedulerAction s = SwitchToThread ptr; ko_at' ko thread s; tcbQueued ko; tcb_ptr \<in> all_active_tcb_ptrs s; tcb_ptr \<noteq> ksCurThread s; sch_act_not tcb_ptr s; \<exists>a b. thread \<in> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> tcb_ptr \<in> all_queued_tcb_ptrs s proof (prove)
goal:
No subgoals!