theory IpcCancel_R

lemma asUser_valid_inQ_queues[wp]:
  "\<lbrace> valid_inQ_queues \<rbrace> asUser t f \<lbrace>\<lambda>rv. valid_inQ_queues \<rbrace>" unfolding valid_inQ_queues_def Ball_def apply (wpsimp wp: hoare_vcg_all_lift) defer apply (wp asUser_ksQ) apply assumption apply (simp add: inQ_def[abs_def] obj_at'_conj) apply (rule hoare_convert_imp) apply (wp asUser_ksQ) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> asUser t f \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d p. (\<forall>x. x \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (inQ d p) x s) \<and> distinct (ksReadyQueues s (d, p))\<rbrace> asUser t f \<lbrace>\<lambda>rv s. \<forall>d p. (\<forall>x. x \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (inQ d p) x s) \<and> distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>d p x. \<lbrace>?P5 d p x\<rbrace> asUser t f \<lbrace>\<lambda>rv s. x \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (inQ d p) x s\<rbrace>
 2. \<And>d p. \<lbrace>?P'4 d p\<rbrace> asUser t f \<lbrace>\<lambda>rv s. distinct (ksReadyQueues s (d, p))\<rbrace>
 3. \<And>s. \<forall>d p. (\<forall>x. x \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (inQ d p) x s) \<and> distinct (ksReadyQueues s (d, p)) \<Longrightarrow> \<forall>x xa. (\<forall>xb. ?P5 x xa xb s) \<and> ?P'4 x xa s proof (prove)
goal (3 subgoals):
 1. \<And>d p. \<lbrace>?P'4 d p\<rbrace> asUser t f \<lbrace>\<lambda>rv s. distinct (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>s. \<forall>d p. (\<forall>x. x \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (inQ d p) x s) \<and> distinct (ksReadyQueues s (d, p)) \<Longrightarrow> \<forall>x xa. (\<forall>xb. ?P5 x xa xb s) \<and> ?P'4 x xa s
 3. \<And>d p x. \<lbrace>?P5 d p x\<rbrace> asUser t f \<lbrace>\<lambda>rv s. x \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (inQ d p) x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<forall>d p. (\<forall>x. x \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (inQ d p) x s) \<and> distinct (ksReadyQueues s (d, p)) \<Longrightarrow> \<forall>x xa. (\<forall>xb. ?P5 x xa xb s) \<and> distinct (ksReadyQueues s (x, xa))
 2. \<And>d p x. \<lbrace>?P5 d p x\<rbrace> asUser t f \<lbrace>\<lambda>rv s. x \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (inQ d p) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p x. \<lbrace>\<lambda>s. x \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (inQ d p) x s\<rbrace> asUser t f \<lbrace>\<lambda>rv s. x \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (inQ d p) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p x. \<lbrace>\<lambda>s. x \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' tcbQueued x s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) x s\<rbrace> asUser t f \<lbrace>\<lambda>rv s. x \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' tcbQueued x s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>d p x. \<lbrace>\<lambda>s. x \<notin> set (ksReadyQueues s (d, p))\<rbrace> asUser t f \<lbrace>\<lambda>rv s. x \<notin> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>d p x. \<lbrace>\<lambda>s. obj_at' tcbQueued x s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) x s\<rbrace> asUser t f \<lbrace>\<lambda>rv s. obj_at' tcbQueued x s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p x. \<lbrace>\<lambda>s. obj_at' tcbQueued x s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) x s\<rbrace> asUser t f \<lbrace>\<lambda>rv s. obj_at' tcbQueued x s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) x s\<rbrace> proof (prove)
goal:
No subgoals!