theory IpcCancel_R

lemma threadSet_valid_inQ_queues:
  "\<lbrace>valid_inQ_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb) \<and> \<not>(inQ d p (f tcb)))
                        \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb) \<and> \<not>(inQ d p (f tcb))) t s
                        \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))\<rbrace>
     threadSet f t
   \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>" apply (simp add: threadSet_def) apply wp apply (simp add: valid_inQ_queues_def pred_tcb_at'_def) apply (wp setObject_queues_unchanged_tcb
             hoare_Ball_helper
             hoare_vcg_all_lift
             setObject_tcb_strongest)[1] apply (wp getObject_tcb_wp) apply (clarsimp simp: valid_inQ_queues_def pred_tcb_at'_def) apply (clarsimp simp: obj_at'_def projectKOs) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))\<rbrace> threadSet f t \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))\<rbrace> do tcb <- getObject t;
setObject t (f tcb)
od \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>
 2. \<lbrace>?Q\<rbrace> getObject t \<lbrace>?B1\<rbrace>
 3. \<And>s. (valid_inQ_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>rv s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p))\<rbrace>
 2. \<lbrace>?Q\<rbrace> getObject t \<lbrace>?B1\<rbrace>
 3. \<And>s. (valid_inQ_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getObject t \<lbrace>\<lambda>tcb s. \<forall>x xa. (\<forall>xb\<in>set (ksReadyQueues s (x, xa)). if t = xb then inQ x xa (f tcb) else obj_at' (inQ x xa) xb s) \<and> distinct (ksReadyQueues s (x, xa))\<rbrace>
 2. \<And>s. (valid_inQ_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_inQ_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (\<forall>x xa. (\<forall>xb\<in>set (ksReadyQueues s (x, xa)). if t = xb then inQ x xa (f ta) else obj_at' (inQ x xa) xb s) \<and> distinct (ksReadyQueues s (x, xa)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)); \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)); tcb_at' t s\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> (\<forall>x xa. t \<in> set (ksReadyQueues s (x, xa)) \<longrightarrow> inQ x xa (f ta)) proof (prove)
goal (1 subgoal):
 1. \<And>s obj x xa. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). \<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (objBitsKO ko) \<and> (\<exists>obj. ko = KOTCB obj \<and> inQ d p obj \<and> ps_clear t (objBitsKO ko) s)) \<and> distinct (ksReadyQueues s (d, p)); \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (f tcb)) \<longrightarrow> inQ d p obj \<and> \<not> inQ d p (f obj) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)); ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s; t \<in> set (ksReadyQueues s (x, xa))\<rbrakk> \<Longrightarrow> inQ x xa (f obj) proof (prove)
goal:
No subgoals!