theory Finalise_R

lemma cancelAll_ct_not_ksQ_helper:
  "\<lbrace>(\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and (\<lambda>s. ksCurThread s \<notin> set q) \<rbrace>
   mapM_x (\<lambda>t. do
                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
                 tcbSchedEnqueue t
               od) q
   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" apply (rule mapM_x_inv_wp2, simp) apply (wp) apply (wps tcbSchedEnqueue_ct') apply (wp tcbSchedEnqueue_ksQ) apply (wps setThreadState_ct') apply (wp sts_ksQ') apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and (\<lambda>s. ksCurThread s \<notin> set q)\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) q \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a as. suffix (a # as) q \<Longrightarrow> \<lbrace>\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set (a # as)\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart a;
tcbSchedEnqueue a
od \<lbrace>\<lambda>r s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set as\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a as x. suffix (a # as) q \<Longrightarrow> \<lbrace>?B4 a as x\<rbrace> tcbSchedEnqueue a \<lbrace>\<lambda>r s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set as\<rbrace>
 2. \<And>a as. suffix (a # as) q \<Longrightarrow> \<lbrace>?Q3 a as\<rbrace> setThreadState Structures_H.thread_state.Restart a \<lbrace>?B4 a as\<rbrace>
 3. \<And>a as s. \<lbrakk>suffix (a # as) q; ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set (a # as)\<rbrakk> \<Longrightarrow> ?Q3 a as s proof (prove)
goal (3 subgoals):
 1. \<And>a as x prev_s. suffix (a # as) q \<Longrightarrow> \<lbrace>?P5 a as x prev_s\<rbrace> tcbSchedEnqueue a \<lbrace>\<lambda>rv s'. ksCurThread prev_s \<notin> set (ksReadyQueues s' p) \<and> ksCurThread prev_s \<notin> set as\<rbrace>
 2. \<And>a as. suffix (a # as) q \<Longrightarrow> \<lbrace>?Q3 a as\<rbrace> setThreadState Structures_H.thread_state.Restart a \<lbrace>\<lambda>x s. ?P5 a as x s s\<rbrace>
 3. \<And>a as s. \<lbrakk>suffix (a # as) q; ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set (a # as)\<rbrakk> \<Longrightarrow> ?Q3 a as s proof (prove)
goal (2 subgoals):
 1. \<And>a as. suffix (a # as) q \<Longrightarrow> \<lbrace>?Q3 a as\<rbrace> setThreadState Structures_H.thread_state.Restart a \<lbrace>\<lambda>x s. (ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<noteq> a) \<and> ksCurThread s \<notin> set as\<rbrace>
 2. \<And>a as s. \<lbrakk>suffix (a # as) q; ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set (a # as)\<rbrakk> \<Longrightarrow> ?Q3 a as s proof (prove)
goal (2 subgoals):
 1. \<And>a as prev_s. suffix (a # as) q \<Longrightarrow> \<lbrace>?P16 a as prev_s\<rbrace> setThreadState Structures_H.thread_state.Restart a \<lbrace>\<lambda>rv s'. ksCurThread prev_s \<notin> set (ksReadyQueues s' p) \<and> ksCurThread prev_s \<noteq> a \<and> ksCurThread prev_s \<notin> set as\<rbrace>
 2. \<And>a as s. \<lbrakk>suffix (a # as) q; ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set (a # as)\<rbrakk> \<Longrightarrow> ?P16 a as s s proof (prove)
goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>suffix (a # as) q; ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set (a # as)\<rbrakk> \<Longrightarrow> (runnable' Structures_H.thread_state.Restart \<or> ksCurThread s \<noteq> a) \<and> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<noteq> a \<and> ksCurThread s \<notin> set as proof (prove)
goal:
No subgoals!