theory Orphanage

lemma no_orphans_lift:
   assumes typ_at'_is_lifted:
     "\<And> tcb_ptr. \<lbrace> \<lambda>s. \<not> typ_at' TCBT tcb_ptr s\<rbrace> f \<lbrace> \<lambda>_ s. \<not> typ_at' TCBT tcb_ptr s \<rbrace>"
   assumes ksCurThread_is_lifted:
     "\<And> tcb_ptr. \<lbrace> \<lambda>s. tcb_ptr = ksCurThread s \<rbrace> f \<lbrace> \<lambda>_ s. tcb_ptr = ksCurThread s \<rbrace>"
   assumes st_tcb_at'_is_lifted:
     "\<And>P p. \<lbrace> \<lambda>s. st_tcb_at' P p s\<rbrace> f \<lbrace> \<lambda>_ s. st_tcb_at' P p s \<rbrace>"
   assumes ksReadyQueues_is_lifted:
     "\<And>P. \<lbrace> \<lambda>s. P (ksReadyQueues s)\<rbrace> f \<lbrace> \<lambda>_ s. P (ksReadyQueues s) \<rbrace>"
   assumes ksSchedulerAction_is_lifted:
     "\<And>P. \<lbrace> \<lambda>s. P (ksSchedulerAction s)\<rbrace> f \<lbrace> \<lambda>_ s. P (ksSchedulerAction s) \<rbrace>"
   shows
     "\<lbrace> \<lambda>s. no_orphans s \<rbrace> f \<lbrace> \<lambda>_ s. no_orphans s \<rbrace>" apply (unfold no_orphans_disj
                all_active_tcb_ptrs_def
                all_queued_tcb_ptrs_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) apply (rule ksCurThread_is_lifted) apply (wp hoare_vcg_disj_lift) apply (rule ksReadyQueues_is_lifted) apply (wp hoare_vcg_disj_lift) apply (rule typ_at'_is_lifted) apply (wp hoare_vcg_disj_lift) apply (rule st_tcb_at'_is_lifted) apply (rule ksSchedulerAction_is_lifted) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> f \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>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> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace> f \<lbrace>\<lambda>_ 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> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb_ptr. \<lbrace>?P2 tcb_ptr\<rbrace> f \<lbrace>\<lambda>rv s. tcb_ptr = ksCurThread s\<rbrace>
 2. \<And>tcb_ptr. \<lbrace>?P'2 tcb_ptr\<rbrace> f \<lbrace>\<lambda>rv s. 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> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace>
 3. \<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> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr \<Longrightarrow> \<forall>x. ?P2 x s \<or> ?P'2 x s proof (prove)
goal (2 subgoals):
 1. \<And>tcb_ptr. \<lbrace>?P'2 tcb_ptr\<rbrace> f \<lbrace>\<lambda>rv s. 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> is_active_thread_state 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> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr \<Longrightarrow> \<forall>x. x = ksCurThread s \<or> ?P'2 x s proof (prove)
goal (3 subgoals):
 1. \<And>tcb_ptr. \<lbrace>?P5 tcb_ptr\<rbrace> f \<lbrace>\<lambda>rv s. tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)}\<rbrace>
 2. \<And>tcb_ptr. \<lbrace>?P'5 tcb_ptr\<rbrace> f \<lbrace>\<lambda>rv s. \<not> typ_at' TCBT tcb_ptr s \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace>
 3. \<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> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr \<Longrightarrow> \<forall>x. x = ksCurThread s \<or> ?P5 x s \<or> ?P'5 x s proof (prove)
goal (2 subgoals):
 1. \<And>tcb_ptr. \<lbrace>?P'5 tcb_ptr\<rbrace> f \<lbrace>\<lambda>rv s. \<not> typ_at' TCBT tcb_ptr s \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state 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> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr \<Longrightarrow> \<forall>x. x = ksCurThread s \<or> x \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> ?P'5 x s proof (prove)
goal (3 subgoals):
 1. \<And>tcb_ptr. \<lbrace>?P10 tcb_ptr\<rbrace> f \<lbrace>\<lambda>rv s. \<not> typ_at' TCBT tcb_ptr s\<rbrace>
 2. \<And>tcb_ptr. \<lbrace>?P'10 tcb_ptr\<rbrace> f \<lbrace>\<lambda>rv s. st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace>
 3. \<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> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr \<Longrightarrow> \<forall>x. x = ksCurThread s \<or> x \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> ?P10 x s \<or> ?P'10 x s proof (prove)
goal (2 subgoals):
 1. \<And>tcb_ptr. \<lbrace>?P'10 tcb_ptr\<rbrace> f \<lbrace>\<lambda>rv s. st_tcb_at' (\<lambda>state. \<not> is_active_thread_state 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> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr \<Longrightarrow> \<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> ?P'10 x s proof (prove)
goal (3 subgoals):
 1. \<And>tcb_ptr. \<lbrace>?P14 tcb_ptr\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr\<rbrace>
 2. \<And>tcb_ptr. \<lbrace>?P'14 tcb_ptr\<rbrace> f \<lbrace>\<lambda>rv s. ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace>
 3. \<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> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr \<Longrightarrow> \<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> ?P14 x s \<or> ?P'14 x s proof (prove)
goal (2 subgoals):
 1. \<And>tcb_ptr. \<lbrace>?P'14 tcb_ptr\<rbrace> f \<lbrace>\<lambda>rv s. 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> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr \<Longrightarrow> \<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> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) x s \<or> ?P'14 x 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> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr \<Longrightarrow> \<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> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) x s \<or> ksSchedulerAction s = SwitchToThread x proof (prove)
goal:
No subgoals!