theory Schedule_R

lemma threadSet_valid_queues_dequeue_wp:
 "\<lbrace> valid_queues_no_bitmap_except t and
        valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and
        (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d,p))) \<rbrace>
          threadSet (tcbQueued_update (\<lambda>_. False)) t
       \<lbrace>\<lambda>rv. valid_queues \<rbrace>" unfolding threadSet_def apply (rule hoare_seq_ext[OF _ getObject_tcb_sp]) apply (rule hoare_pre) apply (simp add: valid_queues_def valid_queues_no_bitmap_except_def valid_queues_no_bitmap_def) apply (wp setObject_queues_unchanged_tcb hoare_Ball_helper hoare_vcg_all_lift
             setObject_tcb_strongest) apply (clarsimp simp: valid_queues_no_bitmap_except_def obj_at'_def valid_queues_no_bitmap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues_no_bitmap_except t and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d, p)))\<rbrace> threadSet (tcbQueued_update (\<lambda>_. False)) t \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues_no_bitmap_except t and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d, p)))\<rbrace> do tcb <- getObject t;
setObject t $ tcbQueued_update (\<lambda>_. False) tcb
od \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrace>valid_queues_no_bitmap_except t and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d, p))) and ko_at' tcb t\<rbrace> setObject t $ tcbQueued_update (\<lambda>_. False) tcb \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrace>?Q4 tcb\<rbrace> setObject t $ tcbQueued_update (\<lambda>_. False) tcb \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>
 2. \<And>tcb s. (valid_queues_no_bitmap_except t and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d, p))) and ko_at' tcb t) s \<Longrightarrow> ?Q4 tcb s proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrace>?Q4 tcb\<rbrace> setObject t (tcbQueued_update (\<lambda>_. False) tcb) \<lbrace>\<lambda>rv s. (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace>
 2. \<And>tcb s. (valid_queues_no_bitmap_except t and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d, p))) and ko_at' tcb t) s \<Longrightarrow> ?Q4 tcb s proof (prove)
goal (1 subgoal):
 1. \<And>tcb s. (valid_queues_no_bitmap_except t and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d, p))) and ko_at' tcb t) s \<Longrightarrow> (\<forall>x xa. (\<forall>xb\<in>set (ksReadyQueues s (x, xa)). if t = xb then (inQ x xa and runnable' \<circ> tcbState) (tcbQueued_update (\<lambda>_. False) tcb) else obj_at' (inQ x xa and runnable' \<circ> tcbState) xb s) \<and> distinct (ksReadyQueues s (x, xa)) \<and> (maxDomain < x \<longrightarrow> ksReadyQueues s (x, xa) = []) \<and> (maxPriority < xa \<longrightarrow> ksReadyQueues s (x, xa) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s proof (prove)
goal:
No subgoals!