theory Orphanage

lemma suspend_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' t s \<rbrace>
   suspend t
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding suspend_def apply (wp | clarsimp simp: unless_def | rule conjI)+ apply (clarsimp simp: is_active_tcb_ptr_def is_active_thread_state_def st_tcb_at_neg2) apply (wp setThreadState_not_active_no_orphans hoare_disjI1 setThreadState_st_tcb
             | clarsimp simp: is_active_thread_state_def isRunning_def isRestart_def)+ apply (wp hoare_drop_imp)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' t s\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' t s\<rbrace> do cancelIPC t;
state <- getThreadState t;
if state = Structures_H.thread_state.Running then updateRestartPC t else return ();
setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>state. \<lbrace>?B4 () state ()\<rbrace> setThreadState Structures_H.thread_state.Inactive t \<lbrace>\<lambda>xb s. no_orphans s \<and> \<not> is_active_tcb_ptr t s\<rbrace>
 2. \<And>x state. \<lbrace>?B3 x state\<rbrace> if state = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>?B4 x state\<rbrace>
 3. \<And>x. \<lbrace>?B1 x\<rbrace> getThreadState t \<lbrace>?B3 x\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 5. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' t s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>state. \<lbrace>?B4 () state ()\<rbrace> setThreadState Structures_H.thread_state.Inactive t \<lbrace>\<lambda>xb s. no_orphans s \<and> (st_tcb_at' (\<lambda>ts. \<not> isRunning ts \<and> \<not> isRestart ts) t s \<or> \<not> tcb_at' t s)\<rbrace>
 2. \<And>x state. \<lbrace>?B3 x state\<rbrace> if state = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>?B4 x state\<rbrace>
 3. \<And>x. \<lbrace>?B1 x\<rbrace> getThreadState t \<lbrace>?B3 x\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 5. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' t s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B1 ()\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> no_orphans s \<and> invs' s \<and> valid_queues' s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> no_orphans s \<and> valid_queues' s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 3. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' t s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' t s \<Longrightarrow> (no_orphans s \<and> valid_queues' s \<and> valid_objs' s) \<and> (tcb_at' t and invs') s \<and> (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)) s \<and> (no_orphans s \<and> valid_queues' s \<and> valid_objs' s) \<and> (valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)) s proof (prove)
goal:
No subgoals!