theory Orphanage

lemma setThreadState_isRestart_no_orphans:
  "\<lbrace> \<lambda>s. no_orphans s \<and> st_tcb_at' isRestart tcb_ptr s \<and> valid_queues' s\<rbrace>
   setThreadState state tcb_ptr
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding setThreadState_def apply (wp | clarsimp)+ apply (rule_tac Q="\<lambda>rv s. valid_queues' s \<and> no_orphans s" in hoare_post_imp) apply clarsimp apply (wp threadSet_valid_queues') apply (unfold no_orphans_disj all_queued_tcb_ptrs_def is_active_thread_state_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift threadSet_pred_tcb_at_state) apply (auto simp: st_tcb_at_double_neg' st_tcb_at_neg' inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> st_tcb_at' isRestart tcb_ptr s \<and> valid_queues' s\<rbrace> setThreadState state tcb_ptr \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> st_tcb_at' isRestart tcb_ptr s \<and> valid_queues' s\<rbrace> do threadSet (tcbState_update (\<lambda>_. state)) tcb_ptr;
runnable <- isRunnable tcb_ptr;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = tcb_ptr \<and> action = ResumeCurrentThread) $ rescheduleRequired
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. state)) tcb_ptr \<lbrace>\<lambda>x s. (\<not> st_tcb_at' runnable' tcb_ptr s \<and> ksCurThread s = tcb_ptr \<and> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> ((ksCurThread s = tcb_ptr \<longrightarrow> st_tcb_at' runnable' tcb_ptr s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> no_orphans s)\<rbrace>
 2. \<And>s. no_orphans s \<and> st_tcb_at' isRestart tcb_ptr s \<and> valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. valid_queues' s \<and> no_orphans s \<Longrightarrow> (\<not> st_tcb_at' runnable' tcb_ptr s \<and> ksCurThread s = tcb_ptr \<and> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> ((ksCurThread s = tcb_ptr \<longrightarrow> st_tcb_at' runnable' tcb_ptr s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> no_orphans s)
 2. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. state)) tcb_ptr \<lbrace>\<lambda>rv s. valid_queues' s \<and> no_orphans s\<rbrace>
 3. \<And>s. no_orphans s \<and> st_tcb_at' isRestart tcb_ptr s \<and> valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. state)) tcb_ptr \<lbrace>\<lambda>rv s. valid_queues' s \<and> no_orphans s\<rbrace>
 2. \<And>s. no_orphans s \<and> st_tcb_at' isRestart tcb_ptr s \<and> valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'26\<rbrace> threadSet (tcbState_update (\<lambda>_. state)) tcb_ptr \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> st_tcb_at' isRestart tcb_ptr s \<and> valid_queues' s \<Longrightarrow> ((\<forall>ko qdom prio. ko_at' ko tcb_ptr s \<and> inQ qdom prio (tcbState_update (\<lambda>_. state) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> tcb_ptr \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> ?P'26 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'26\<rbrace> threadSet (tcbState_update (\<lambda>_. state)) tcb_ptr \<lbrace>\<lambda>rv s. \<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT tcb_ptr s \<or> st_tcb_at' (\<lambda>state. \<not> (isRunning state \<or> isRestart state)) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace>
 2. \<And>s. (\<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT tcb_ptr s \<or> st_tcb_at' (\<lambda>state. \<not> (isRunning state \<or> isRestart state)) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) \<and> st_tcb_at' isRestart tcb_ptr s \<and> valid_queues' s \<Longrightarrow> ((\<forall>ko qdom prio. ko_at' ko tcb_ptr s \<and> inQ qdom prio (tcbState_update (\<lambda>_. state) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> tcb_ptr \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> ?P'26 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT tcb_ptr s \<or> st_tcb_at' (\<lambda>state. \<not> (isRunning state \<or> isRestart state)) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) \<and> st_tcb_at' isRestart tcb_ptr s \<and> valid_queues' s \<Longrightarrow> ((\<forall>ko qdom prio. ko_at' ko tcb_ptr s \<and> inQ qdom prio (tcbState_update (\<lambda>_. state) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> tcb_ptr \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (\<forall>x. x = ksCurThread s \<or> x \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT x s \<or> (tcb_at' tcb_ptr s \<longrightarrow> (if x = tcb_ptr then obj_at' (\<lambda>tcb. \<not> (isRunning (itcbState (tcb_to_itcb' (tcbState_update (\<lambda>_. state) tcb))) \<or> isRestart (itcbState (tcb_to_itcb' (tcbState_update (\<lambda>_. state) tcb))))) tcb_ptr s else st_tcb_at' (\<lambda>state. \<not> (isRunning state \<or> isRestart state)) x s)) \<or> ksSchedulerAction s = SwitchToThread x) proof (prove)
goal:
No subgoals!