theory Orphanage

lemma rescheduleRequired_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<rbrace>
   rescheduleRequired
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding rescheduleRequired_def apply (wp tcbSchedEnqueue_no_orphans hoare_vcg_all_lift ssa_no_orphans | wpc | clarsimp)+ apply (wps tcbSchedEnqueue_nosch, wp hoare_weak_lift_imp) apply (rename_tac word t p) apply (rule_tac P="word = t" in hoare_gen_asm) apply (wp hoare_disjI1 | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace> do action <- getSchedulerAction;
case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x3 t. \<lbrace>?P29 (SwitchToThread x3) x3 t\<rbrace> tcbSchedEnqueue x3 \<lbrace>\<lambda>rv s. ksSchedulerAction s = SwitchToThread t \<longrightarrow> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t\<rbrace>
 2. \<lbrace>?Q\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s \<and> (\<forall>t. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t)) \<and> (action = ChooseNewThread \<longrightarrow> no_orphans s \<and> (\<forall>t. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t)) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> no_orphans s \<and> (\<forall>xa. ?P29 action x xa s))\<rbrace>
 3. \<And>s. no_orphans s \<and> valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x3 t prev_s. \<lbrace>?P'41 x3 t prev_s\<rbrace> tcbSchedEnqueue x3 \<lbrace>\<lambda>rv s. t \<in> all_queued_tcb_ptrs s \<or> ksCurThread prev_s = t\<rbrace>
 2. \<lbrace>?Q\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s \<and> (\<forall>t. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t)) \<and> (action = ChooseNewThread \<longrightarrow> no_orphans s \<and> (\<forall>t. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t)) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> no_orphans s \<and> (\<forall>xa. ksSchedulerAction s = SwitchToThread xa \<longrightarrow> ?P'42 action x xa s))\<rbrace>
 3. \<And>s. no_orphans s \<and> valid_queues' s \<Longrightarrow> ?Q s
flex-flex pairs:
\<lambda>x3. ?P'42 (SwitchToThread x3) x3 \<equiv>\<^sup>? \<lambda>x3 t s. ?P'41 x3 t s s proof (prove)
goal (3 subgoals):
 1. \<And>word t p. \<lbrace>?P'41 word t p\<rbrace> tcbSchedEnqueue word \<lbrace>\<lambda>rv s. t \<in> all_queued_tcb_ptrs s \<or> ksCurThread p = t\<rbrace>
 2. \<lbrace>?Q\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s \<and> (\<forall>t. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t)) \<and> (action = ChooseNewThread \<longrightarrow> no_orphans s \<and> (\<forall>t. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t)) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> no_orphans s \<and> (\<forall>xa. ksSchedulerAction s = SwitchToThread xa \<longrightarrow> ?P'42 action x xa s))\<rbrace>
 3. \<And>s. no_orphans s \<and> valid_queues' s \<Longrightarrow> ?Q s
flex-flex pairs:
\<lambda>x3. ?P'42 (SwitchToThread x3) x3 \<equiv>\<^sup>? \<lambda>x3 t s. ?P'41 x3 t s s proof (prove)
goal (3 subgoals):
 1. \<And>word t p. word = t \<Longrightarrow> \<lbrace>?P'45 (SwitchToThread word) word t p\<rbrace> tcbSchedEnqueue word \<lbrace>\<lambda>rv s. t \<in> all_queued_tcb_ptrs s \<or> ksCurThread p = t\<rbrace>
 2. \<lbrace>?Q\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s \<and> (\<forall>t. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t)) \<and> (action = ChooseNewThread \<longrightarrow> no_orphans s \<and> (\<forall>t. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t)) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> no_orphans s \<and> (\<forall>xa. ksSchedulerAction s = SwitchToThread xa \<longrightarrow> (?P'45 action x xa s and K (x = xa)) s))\<rbrace>
 3. \<And>s. no_orphans s \<and> valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!