theory Orphanage

lemma scheduleChooseNewThread_no_orphans:
  "\<lbrace> invs' and no_orphans
     and (\<lambda>s. ksSchedulerAction s = ChooseNewThread
              \<and> (st_tcb_at' runnable' (ksCurThread s) s
                 \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))) \<rbrace>
   scheduleChooseNewThread
   \<lbrace>\<lambda>_. no_orphans \<rbrace>" unfolding scheduleChooseNewThread_def apply (wp add: ssa_no_orphans hoare_vcg_all_lift) apply (wp hoare_disjI1 chooseThread_nosch)+ apply (wp nextDomain_invs_no_cicd' hoare_vcg_imp_lift
               hoare_lift_Pf2 [OF ksQ_all_queued_tcb_ptrs_lift[OF nextDomain_ksQ]
                                  nextDomain_ct']
               hoare_lift_Pf2 [OF st_tcb_at'_is_active_tcb_ptr_lift[OF nextDomain_st_tcb_at']
                                  nextDomain_ct']
               hoare_vcg_all_lift getDomainTime_wp)[2] apply (wpsimp simp: if_apply_def2 invs'_invs_no_cicd all_queued_tcb_ptrs_def
                       is_active_tcb_ptr_runnable')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and no_orphans and (\<lambda>s. ksSchedulerAction s = ChooseNewThread \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))))\<rbrace> scheduleChooseNewThread \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and no_orphans and (\<lambda>s. ksSchedulerAction s = ChooseNewThread \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))))\<rbrace> do domainTime <- getDomainTime;
when (domainTime = 0) $ nextDomain;
chooseThread;
setSchedulerAction ResumeCurrentThread
od \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>domainTime x t. \<lbrace>?P8 domainTime x t\<rbrace> chooseThread \<lbrace>\<lambda>rv s. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t\<rbrace>
 2. \<And>domainTime. \<lbrace>?B1 domainTime\<rbrace> when (domainTime = 0) $ nextDomain \<lbrace>\<lambda>x s. (no_orphans s \<and> all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>xa. ?P8 domainTime x xa s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> getDomainTime \<lbrace>?B1\<rbrace>
 4. \<And>s. (invs' and no_orphans and (\<lambda>s. ksSchedulerAction s = ChooseNewThread \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>domainTime. domainTime = 0 \<Longrightarrow> \<lbrace>?P'17 domainTime\<rbrace> nextDomain \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> getDomainTime \<lbrace>\<lambda>domainTime. if domainTime = 0 then \<lambda>s. no_orphans s \<and> ?P'17 domainTime s else (\<lambda>s. no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))\<rbrace>
 3. \<And>s. (invs' and no_orphans and (\<lambda>s. ksSchedulerAction s = ChooseNewThread \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getDomainTime \<lbrace>\<lambda>domainTime. if domainTime = 0 then \<lambda>s. no_orphans s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s) else (\<lambda>s. no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))\<rbrace>
 2. \<And>s. (invs' and no_orphans and (\<lambda>s. ksSchedulerAction s = ChooseNewThread \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))))) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!