theory Orphanage

lemma ThreadDecls_H_switchToThread_no_orphans:
  "\<lbrace> \<lambda>s. no_orphans s \<and>
         st_tcb_at' runnable' tcb_ptr s \<and>
         (ksCurThread s \<in> all_active_tcb_ptrs s
            \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)\<rbrace>
   ThreadDecls_H.switchToThread tcb_ptr
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding Thread_H.switchToThread_def apply (wp setCurThread_almost_no_orphans
            tcbSchedDequeue_almost_no_orphans) apply (wps tcbSchedDequeue_ct') apply (wp tcbSchedDequeue_all_queued_tcb_ptrs hoare_convert_imp)+ apply (wps) apply (wp)+ apply (wps) apply (wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> st_tcb_at' runnable' tcb_ptr s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)\<rbrace> global.switchToThread tcb_ptr \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> st_tcb_at' runnable' tcb_ptr s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)\<rbrace> do Arch.switchToThread tcb_ptr;
tcbSchedDequeue tcb_ptr;
setCurThread tcb_ptr
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?P'6 x\<rbrace> tcbSchedDequeue tcb_ptr \<lbrace>\<lambda>rv s. ksCurThread s \<noteq> tcb_ptr \<longrightarrow> ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s\<rbrace>
 2. \<lbrace>?Q\<rbrace> Arch.switchToThread tcb_ptr \<lbrace>\<lambda>x s. no_orphans s \<and> ?P'6 x s\<rbrace>
 3. \<And>s. no_orphans s \<and> st_tcb_at' runnable' tcb_ptr s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x prev_s. \<lbrace>?P8 x prev_s\<rbrace> tcbSchedDequeue tcb_ptr \<lbrace>\<lambda>rv s'. ksCurThread prev_s \<noteq> tcb_ptr \<longrightarrow> ksCurThread prev_s \<in> all_active_tcb_ptrs prev_s \<longrightarrow> ksCurThread prev_s \<in> all_queued_tcb_ptrs s'\<rbrace>
 2. \<lbrace>?Q\<rbrace> Arch.switchToThread tcb_ptr \<lbrace>\<lambda>x s. no_orphans s \<and> ?P8 x s s\<rbrace>
 3. \<And>s. no_orphans s \<and> st_tcb_at' runnable' tcb_ptr s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. \<not> ?P26 s\<rbrace> Arch.switchToThread tcb_ptr \<lbrace>\<lambda>rv s. ksCurThread s \<notin> all_active_tcb_ptrs s\<rbrace>
 2. \<lbrace>?R26\<rbrace> Arch.switchToThread tcb_ptr \<lbrace>\<lambda>rv s. ksCurThread s \<in> all_queued_tcb_ptrs s \<and> ksCurThread s \<noteq> tcb_ptr\<rbrace>
 3. \<And>s. no_orphans s \<and> st_tcb_at' runnable' tcb_ptr s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s) \<Longrightarrow> no_orphans s \<and> (ksCurThread s \<noteq> tcb_ptr \<longrightarrow> ?P26 s \<longrightarrow> ?R26 s) proof (prove)
goal (3 subgoals):
 1. \<And>prev_s. \<lbrace>\<lambda>a. \<not> ?P29 prev_s a\<rbrace> Arch.switchToThread tcb_ptr \<lbrace>\<lambda>rv s'. ksCurThread prev_s \<notin> all_active_tcb_ptrs prev_s\<rbrace>
 2. \<lbrace>?R26\<rbrace> Arch.switchToThread tcb_ptr \<lbrace>\<lambda>rv s. ksCurThread s \<in> all_queued_tcb_ptrs s \<and> ksCurThread s \<noteq> tcb_ptr\<rbrace>
 3. \<And>s. no_orphans s \<and> st_tcb_at' runnable' tcb_ptr s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s) \<Longrightarrow> no_orphans s \<and> (ksCurThread s \<noteq> tcb_ptr \<longrightarrow> ?P29 s s \<longrightarrow> ?R26 s) proof (prove)
goal (2 subgoals):
 1. \<lbrace>?R26\<rbrace> Arch.switchToThread tcb_ptr \<lbrace>\<lambda>rv s. ksCurThread s \<in> all_queued_tcb_ptrs s \<and> ksCurThread s \<noteq> tcb_ptr\<rbrace>
 2. \<And>s. no_orphans s \<and> st_tcb_at' runnable' tcb_ptr s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s) \<Longrightarrow> no_orphans s \<and> (ksCurThread s \<noteq> tcb_ptr \<longrightarrow> ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ?R26 s) proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P39 prev_s\<rbrace> Arch.switchToThread tcb_ptr \<lbrace>\<lambda>rv s'. ksCurThread prev_s \<in> all_queued_tcb_ptrs prev_s \<and> ksCurThread prev_s \<noteq> tcb_ptr\<rbrace>
 2. \<And>s. no_orphans s \<and> st_tcb_at' runnable' tcb_ptr s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s) \<Longrightarrow> no_orphans s \<and> (ksCurThread s \<noteq> tcb_ptr \<longrightarrow> ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ?P39 s s) proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s \<and> st_tcb_at' runnable' tcb_ptr s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s) \<Longrightarrow> no_orphans s \<and> (ksCurThread s \<noteq> tcb_ptr \<longrightarrow> ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s \<and> ksCurThread s \<noteq> tcb_ptr) proof (prove)
goal:
No subgoals!