theory IpcCancel_R

lemma sts_valid_queues_partial:
  "\<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace>
    setThreadState st t
   \<lbrace>\<lambda>_ s. \<forall>t' d p.
            (t' \<in> set(ksReadyQueues s (d, p)) \<longrightarrow>
             (obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s
              \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)))
            \<and> distinct (ksReadyQueues s (d, p))\<rbrace>"
  (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_ s. \<forall>t' d p. ?OA t' d p s \<and> ?DISTINCT d p s \<rbrace>") apply (rule_tac Q="\<lambda>_ s. (\<forall>t' d p. ?OA t' d p s) \<and> (\<forall>d p. ?DISTINCT d p s)"
           in hoare_post_imp) apply (clarsimp) apply (rule hoare_conjI) apply (rule_tac Q="\<lambda>s. \<forall>t' d p.
             ((t'\<in>set(ksReadyQueues s (d, p))
               \<or> \<not> (sch_act_simple s))
                  \<longrightarrow> (obj_at'(\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s
                       \<and> st_tcb_at' runnable' t' s))" in hoare_pre_imp) apply (fastforce simp: Invariants_H.valid_queues_def valid_queues_no_bitmap_def
                           pred_tcb_at'_def obj_at'_def inQ_def) apply (rule hoare_vcg_all_lift)+ apply (rule hoare_convert_imp) including no_pre apply (wp sts_ksQ setThreadState_oa_queued hoare_impI sts_pred_tcb_neq'
            | clarsimp)+ apply (rule_tac Q="\<lambda>s. \<forall>d p. ?DISTINCT d p s \<and> sch_act_simple s" in hoare_pre_imp) apply (clarsimp simp: Invariants_H.valid_queues_def valid_queues_no_bitmap_def) apply (wp hoare_vcg_all_lift sts_ksQ) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. \<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (\<forall>t' d p. t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> (\<forall>d p. distinct (ksReadyQueues s (d, p))) \<Longrightarrow> \<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> distinct (ksReadyQueues s (d, p))
 2. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. (\<forall>t' d p. t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> (\<forall>d p. distinct (ksReadyQueues s (d, p)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. (\<forall>t' d p. t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> (\<forall>d p. distinct (ksReadyQueues s (d, p)))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>r s. \<forall>t' d p. t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)\<rbrace>
 2. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>r s. \<forall>d p. distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. (Invariants_H.valid_queues and sch_act_simple) s \<Longrightarrow> \<forall>t' d p. t' \<in> set (ksReadyQueues s (d, p)) \<or> \<not> sch_act_simple s \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> st_tcb_at' runnable' t' s
 2. \<lbrace>\<lambda>s. \<forall>t' d p. t' \<in> set (ksReadyQueues s (d, p)) \<or> \<not> sch_act_simple s \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> st_tcb_at' runnable' t' s\<rbrace> setThreadState st t \<lbrace>\<lambda>r s. \<forall>t' d p. t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)\<rbrace>
 3. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>r s. \<forall>d p. distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<forall>t' d p. t' \<in> set (ksReadyQueues s (d, p)) \<or> \<not> sch_act_simple s \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> st_tcb_at' runnable' t' s\<rbrace> setThreadState st t \<lbrace>\<lambda>r s. \<forall>t' d p. t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)\<rbrace>
 2. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>r s. \<forall>d p. distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t' d p. \<lbrace>\<lambda>s. t' \<in> set (ksReadyQueues s (d, p)) \<or> \<not> sch_act_simple s \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> st_tcb_at' runnable' t' s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)\<rbrace>
 2. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>r s. \<forall>d p. distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>t' d p. \<lbrace>\<lambda>s. \<not> (t' \<in> set (ksReadyQueues s (d, p)) \<or> \<not> sch_act_simple s)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. t' \<notin> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>t' d p. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> st_tcb_at' runnable' t' s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)\<rbrace>
 3. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>r s. \<forall>d p. distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>t' d p. \<lbrace>\<lambda>s. \<not> (t' \<in> set (ksReadyQueues s (d, p)) \<or> \<not> sch_act_simple s)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. t' \<notin> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>t' d p. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> st_tcb_at' runnable' t' s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)\<rbrace>
 3. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>r s. \<forall>d p. distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>r s. \<forall>d p. distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (Invariants_H.valid_queues and sch_act_simple) s \<Longrightarrow> \<forall>d p. distinct (ksReadyQueues s (d, p)) \<and> sch_act_simple s
 2. \<lbrace>\<lambda>s. \<forall>d p. distinct (ksReadyQueues s (d, p)) \<and> sch_act_simple s\<rbrace> setThreadState st t \<lbrace>\<lambda>r s. \<forall>d p. distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d p. distinct (ksReadyQueues s (d, p)) \<and> sch_act_simple s\<rbrace> setThreadState st t \<lbrace>\<lambda>r s. \<forall>d p. distinct (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p s. distinct (ksReadyQueues s (d, p)) \<and> sch_act_simple s \<Longrightarrow> sch_act_simple s \<and> distinct (ksReadyQueues s (d, p)) proof (prove)
goal:
No subgoals!