theory Schedule_R

lemma threadSet_valid_queues'_dequeue: (* threadSet_valid_queues' is too weak for dequeue *)
  "\<lbrace>\<lambda>s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and>
        obj_at' (inQ d p) t s \<rbrace>
   threadSet (tcbQueued_update (\<lambda>_. False)) t
   \<lbrace>\<lambda>rv. valid_queues' \<rbrace>" unfolding valid_queues'_def apply (rule hoare_pre) apply (wp hoare_vcg_all_lift) apply (simp only: imp_conv_disj not_obj_at') apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) apply (simp add: not_obj_at') apply (clarsimp simp: typ_at_tcb') apply normalise_obj_at' apply (fastforce elim: obj_at'_weaken simp: inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> obj_at' (inQ d p) t s\<rbrace> threadSet (tcbQueued_update (\<lambda>_. False)) t \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> obj_at' (inQ d p) t s\<rbrace> threadSet (tcbQueued_update (\<lambda>_. False)) t \<lbrace>\<lambda>rv s. \<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbQueued_update (\<lambda>_. False)) t \<lbrace>\<lambda>rv s. \<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> obj_at' (inQ d p) t s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>d p ta. \<lbrace>?P6 d p ta\<rbrace> threadSet (tcbQueued_update (\<lambda>_. False)) t \<lbrace>\<lambda>rv s. obj_at' (inQ d p) ta s \<longrightarrow> ta \<in> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> obj_at' (inQ d p) t s \<Longrightarrow> \<forall>x xa xb. ?P6 x xa xb s proof (prove)
goal (2 subgoals):
 1. \<And>d p ta. \<lbrace>?P6 d p ta\<rbrace> threadSet (tcbQueued_update (\<lambda>_. False)) t \<lbrace>\<lambda>rv s. (\<not> typ_at' TCBT ta s \<or> obj_at' (Not \<circ> inQ d p) ta s) \<or> ta \<in> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> obj_at' (inQ d p) t s \<Longrightarrow> \<forall>x xa xb. ?P6 x xa xb s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> obj_at' (inQ d p) t s \<Longrightarrow> \<forall>x xa xb. (\<not> typ_at' TCBT xb s \<or> obj_at' (\<lambda>obj. if t = xb then (Not \<circ> inQ x xa) (tcbQueued_update (\<lambda>_. False) obj) else (Not \<circ> inQ x xa) obj) xb s) \<or> xb \<in> set (ksReadyQueues s (x, xa)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> obj_at' (inQ d p) t s \<Longrightarrow> \<forall>x xa xb. typ_at' TCBT xb s \<longrightarrow> obj_at' (\<lambda>obj. (t = xb \<longrightarrow> \<not> inQ x xa (tcbQueued_update (\<lambda>_. False) obj)) \<and> (t \<noteq> xb \<longrightarrow> \<not> inQ x xa obj)) xb s \<or> xb \<in> set (ksReadyQueues s (x, xa)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p)); obj_at' (inQ d p) t s; tcb_at' xb s; xb \<notin> set (ksReadyQueues s (x, xa))\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>obj. (t = xb \<longrightarrow> \<not> inQ x xa (tcbQueued_update (\<lambda>_. False) obj)) \<and> (t \<noteq> xb \<longrightarrow> \<not> inQ x xa obj)) xb s proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb ko koa. \<lbrakk>\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p)); xb \<notin> set (ksReadyQueues s (x, xa)); ko_at' koa xb s; ko_at' ko t s; inQ d p ko\<rbrakk> \<Longrightarrow> (t = xb \<longrightarrow> \<not> inQ x xa (tcbQueued_update (\<lambda>_. False) koa)) \<and> (t \<noteq> xb \<longrightarrow> \<not> inQ x xa koa) proof (prove)
goal:
No subgoals!