theory Tcb_R

lemma setP_vq'[wp]:
  "\<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> p \<le> maxPriority\<rbrace>
     setPriority t p
   \<lbrace>\<lambda>rv. valid_queues'\<rbrace>" apply (simp add: setPriority_def) apply (wpsimp wp: threadSet_valid_queues' hoare_drop_imps
                    threadSet_weak_sch_act_wf threadSet_sch_act) apply (rule_tac Q="\<lambda>_ s. valid_queues' s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> sch_act_wf (ksSchedulerAction s) s
              \<and> weak_sch_act_wf (ksSchedulerAction s) s" in hoare_strengthen_post,
          wp tcbSchedDequeue_valid_queues' tcbSchedDequeue_not_queued) apply (clarsimp simp: inQ_def) apply normalise_obj_at' apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> p \<le> maxPriority\<rbrace> setPriority t p \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> p \<le> maxPriority\<rbrace> do y <- tcbSchedDequeue t;
y <- threadSet (tcbPriority_update (\<lambda>_. p)) t;
runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv s. (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s\<rbrace>
 2. \<And>s. valid_queues' s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. valid_queues' s \<and> obj_at' (Not \<circ> tcbQueued) t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s
 2. \<And>s. valid_queues' s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> p \<le> maxPriority \<Longrightarrow> (valid_queues' and tcb_at' t) s \<and> True \<and> sch_act_wf (ksSchedulerAction s) s \<and> weak_sch_act_wf (ksSchedulerAction s) s proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>valid_queues' s; obj_at' (Not \<circ> tcbQueued) t s; sch_act_wf (ksSchedulerAction s) s; weak_sch_act_wf (ksSchedulerAction s) s; ko_at' ko t s; tcbQueued ko; tcbPriority ko \<noteq> p\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues s (tcbDomain ko, p))
 2. \<And>s. valid_queues' s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> p \<le> maxPriority \<Longrightarrow> (valid_queues' and tcb_at' t) s \<and> True \<and> sch_act_wf (ksSchedulerAction s) s \<and> weak_sch_act_wf (ksSchedulerAction s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues' s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> p \<le> maxPriority \<Longrightarrow> (valid_queues' and tcb_at' t) s \<and> True \<and> sch_act_wf (ksSchedulerAction s) s \<and> weak_sch_act_wf (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!