kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma threadSet_state_refs_of'_helper'[simp]:
  "{r. (r \<in> tcb_st_refs_of' ts \<or>
        r \<in> tcb_bound_refs' ntfnptr) \<and>
       snd r \<noteq> TCBBound} =
   tcb_st_refs_of' ts" by (auto simp: tcb_st_refs_of'_def tcb_bound_refs'_def
          split: thread_state.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {r. (r \<in> tcb_st_refs_of' ts \<or> r \<in> tcb_bound_refs' ntfnptr) \<and> snd r \<noteq> TCBBound} = tcb_st_refs_of' ts
theory TcbAcc_R

lemma threadSet_ctes_ofT:
  assumes x: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases.
                 getF (F tcb) = getF tcb"
  shows "\<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" apply (simp add: threadSet_def) apply (wp getObject_tcb_wp) apply (clarsimp simp: obj_at'_def projectKOs) apply (case_tac obj) apply (simp add: bspec_split [OF spec [OF x]]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ctes_of s) \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> P (ctes_of s) \<and> obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF (F ta)) t s) proof (prove)
goal (1 subgoal):
 1. \<And>s obj a b. \<lbrakk>P (ctes_of s); ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s; (a, b) \<in> ran tcb_cte_cases\<rbrakk> \<Longrightarrow> a obj = a (F obj) proof (prove)
goal (1 subgoal):
 1. \<And>s obj a b x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>P (ctes_of s); ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s; (a, b) \<in> ran tcb_cte_cases; obj = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> a obj = a (F obj) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_idle'T:
  assumes x: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases. getF (F tcb) = getF tcb"
  shows
  "\<lbrace>\<lambda>s. valid_idle' s
      \<and> (t = ksIdleThread s \<longrightarrow>
          (\<forall>tcb. ko_at' tcb t s \<and> idle_tcb' tcb \<longrightarrow> idle_tcb' (F tcb)))\<rbrace>
     threadSet F t
   \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" apply (simp add: threadSet_def) apply (wp setObject_tcb_idle' getObject_tcb_wp) apply (clarsimp simp: obj_at'_def projectKOs) apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs idle_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> (\<forall>tcb. ko_at' tcb t s \<and> idle_tcb' tcb \<longrightarrow> idle_tcb' (F tcb)))\<rbrace> threadSet F t \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> (\<forall>tcb. ko_at' tcb (ksIdleThread s) s \<and> idle_tcb' tcb \<longrightarrow> idle_tcb' (F tcb)))\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> (\<forall>tcb. ko_at' tcb (ksIdleThread s) s \<and> idle_tcb' tcb \<longrightarrow> idle_tcb' (F tcb))) \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> idle' (tcbState (F ta)) \<and> tcbBoundNotification (F ta) = None)) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>valid_idle' s; idle_tcb' obj \<longrightarrow> idle_tcb' (F obj); ksPSpace s (ksIdleThread s) = Some (KOTCB obj); is_aligned (ksIdleThread s) (objBitsKO (KOTCB obj)); ps_clear (ksIdleThread s) (objBitsKO (KOTCB obj)) s; t = ksIdleThread s\<rbrakk> \<Longrightarrow> idle' (tcbState (F obj)) \<and> tcbBoundNotification (F obj) = None proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma set_tcb_valid_bitmapQ[wp]:
  "\<lbrace> valid_bitmapQ \<rbrace> setObject t (f tcb :: tcb) \<lbrace>\<lambda>_. valid_bitmapQ \<rbrace>" apply (rule setObject_tcb_pre) apply (simp add: bitmapQ_defs setObject_def split_def) apply (wp hoare_Ball_helper hoare_vcg_all_lift updateObject_default_inv | simp add: bitmapQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ and tcb_at' t\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> [])) and tcb_at' t\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- updateObject_default (f tcb) (snd p) t (fst p) (snd (lookupAround2 t ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> [])\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma set_tcb_bitmapQ_no_L1_orphans[wp]:
  "\<lbrace> bitmapQ_no_L1_orphans \<rbrace> setObject t (f tcb :: tcb) \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans \<rbrace>" apply (rule setObject_tcb_pre) apply (simp add: bitmapQ_defs setObject_def split_def) apply (wp hoare_Ball_helper hoare_vcg_all_lift updateObject_default_inv | simp add: bitmapQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans and tcb_at' t\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize) and tcb_at' t\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- updateObject_default (f tcb) (snd p) t (fst p) (snd (lookupAround2 t ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma set_tcb_bitmapQ_no_L2_orphans[wp]:
  "\<lbrace> bitmapQ_no_L2_orphans \<rbrace> setObject t (f tcb :: tcb) \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans \<rbrace>" apply (rule setObject_tcb_pre) apply (simp add: bitmapQ_defs setObject_def split_def) apply (wp hoare_Ball_helper hoare_vcg_all_lift updateObject_default_inv | simp add: bitmapQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans and tcb_at' t\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>d i. (\<exists>j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i) and tcb_at' t\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- updateObject_default (f tcb) (snd p) t (fst p) (snd (lookupAround2 t ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. \<forall>d i. (\<exists>j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_valid_bitmapQ[wp]:
  "\<lbrace> valid_bitmapQ \<rbrace> threadSet f t \<lbrace> \<lambda>rv. valid_bitmapQ \<rbrace>" unfolding bitmapQ_defs threadSet_def by (clarsimp simp: setObject_def split_def)
     (wp | simp add: updateObject_default_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ\<rbrace> threadSet f t \<lbrace>\<lambda>rv. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> [])\<rbrace> do tcb <- getObject t;
setObject t $ f tcb
od \<lbrace>\<lambda>rv s. \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> [])\<rbrace>
theory TcbAcc_R

lemma threadSet_valid_bitmapQ_no_L1_orphans[wp]:
  "\<lbrace> bitmapQ_no_L1_orphans \<rbrace> threadSet f t \<lbrace> \<lambda>rv. bitmapQ_no_L1_orphans \<rbrace>" unfolding bitmapQ_defs threadSet_def by (clarsimp simp: setObject_def split_def)
     (wp | simp add: updateObject_default_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans\<rbrace> threadSet f t \<lbrace>\<lambda>rv. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace> do tcb <- getObject t;
setObject t $ f tcb
od \<lbrace>\<lambda>rv s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace>
theory TcbAcc_R

lemma threadSet_valid_bitmapQ_no_L2_orphans[wp]:
  "\<lbrace> bitmapQ_no_L2_orphans \<rbrace> threadSet f t \<lbrace> \<lambda>rv. bitmapQ_no_L2_orphans \<rbrace>" unfolding bitmapQ_defs threadSet_def by (clarsimp simp: setObject_def split_def)
     (wp | simp add: updateObject_default_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans\<rbrace> threadSet f t \<lbrace>\<lambda>rv. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace> do tcb <- getObject t;
setObject t $ f tcb
od \<lbrace>\<lambda>rv s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace>
theory TcbAcc_R

lemma threadSet_valid_queues:
  "\<lbrace>Invariants_H.valid_queues and
    (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and>
                     \<not>(inQ d p (f tcb) \<and> runnable' (tcbState (f tcb))))
                \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and>
                                 \<not>(inQ d p (f tcb) \<and> runnable' (tcbState (f tcb)))) t s
                \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))
    )\<rbrace>
     threadSet f t
   \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" unfolding valid_queues_def by (wp threadSet_valid_queues_no_bitmap;simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (f tcb) \<and> runnable' (tcbState (f tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (f tcb) \<and> runnable' (tcbState (f tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))\<rbrace> threadSet f t \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (f tcb) \<and> runnable' (tcbState (f tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (f tcb) \<and> runnable' (tcbState (f tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace>
theory TcbAcc_R

lemma addToQs_set_def:
  "(t' \<in> set (addToQs F t qs (qdom, prio))) = (t' \<in> set (qs (qdom, prio))
      \<or> (t' = t \<and> (\<forall>ko. \<not> inQ qdom prio (F ko))))" by (auto simp add: addToQs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (t' \<in> set (addToQs F t qs (qdom, prio))) = (t' \<in> set (qs (qdom, prio)) \<or> t' = t \<and> (\<forall>ko. \<not> inQ qdom prio (F ko)))
theory TcbAcc_R

lemma addToQs_subset:
  "set (qs p) \<subseteq> set (addToQs F t qs p)" by (clarsimp simp: addToQs_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (qs p) \<subseteq> set (addToQs F t qs p)
theory TcbAcc_R

lemma threadSet_cur:
  "\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. cur_tcb' s\<rbrace>" apply (simp add: threadSet_def cur_tcb'_def) apply (wp hoare_lift_Pf [OF setObject_tcb_at'] setObject_ct_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> threadSet f t \<lbrace>\<lambda>rv. cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> do tcb <- getObject t;
setObject t (f tcb)
od \<lbrace>\<lambda>rv s. tcb_at' (ksCurThread s) s\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma modifyReadyQueuesL1Bitmap_obj_at[wp]:
  "\<lbrace>obj_at' P t\<rbrace> modifyReadyQueuesL1Bitmap a b \<lbrace>\<lambda>rv. obj_at' P t\<rbrace>" apply (simp add: modifyReadyQueuesL1Bitmap_def getReadyQueuesL1Bitmap_def) apply wp apply (fastforce intro: obj_at'_pspaceI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> modifyReadyQueuesL1Bitmap a b \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks a);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap ks)(a := b l1)\<rparr>)
od \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' P t s \<Longrightarrow> obj_at' P t (s\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap s)(a := b (ksReadyQueuesL1Bitmap s a))\<rparr>) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_typ_at'[wp]:
  "\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> threadSet t F \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>" by (simp add: threadSet_def, wp setObject_typ_at')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> threadSet t F \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>
theory TcbAcc_R

lemma setObject_tcb_pde_mappings'[wp]:
  "\<lbrace>valid_pde_mappings'\<rbrace> setObject p (tcb :: tcb) \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>" apply (wp valid_pde_mappings_lift' setObject_typ_at') apply (rule obj_at_setObject2) apply (auto dest: updateObject_default_result) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde_mappings'\<rbrace> setObject p tcb \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> setObject p tcb \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace>
 2. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (2 subgoals):
 1. \<And>x ko s' v oko xa y n s. (ko, s') \<in> fst (updateObject v oko xa y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(ARM_H.pde)
 2. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma not_obj_at_elim':
  assumes typat: "typ_at' TCBT t s"
      and nobj: "\<not>obj_at' (\<lambda>tcb::tcb. P tcb) t s"
    shows "obj_at' (Not \<circ> P) t s" using assms apply - apply (drule not_obj_at' [THEN iffD1]) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' (Not \<circ> P) t s proof (prove)
using this:
typ_at' TCBT t s
\<not> obj_at' P t s

goal (1 subgoal):
 1. obj_at' (Not \<circ> P) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at' TCBT t s; \<not> obj_at' P t s\<rbrakk> \<Longrightarrow> obj_at' (Not \<circ> P) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at' TCBT t s; \<not> typ_at' TCBT t s \<or> obj_at' (Not \<circ> P) t s\<rbrakk> \<Longrightarrow> obj_at' (Not \<circ> P) t s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_obj_at'_strongish[wp]:
  "\<lbrace>obj_at' (\<lambda>obj. if t = t' then P (f obj) else P obj) t'\<rbrace>
     threadSet f t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>" by (simp add: hoare_weaken_pre [OF threadSet_obj_at'_really_strongest])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>obj. if t = t' then P (f obj) else P obj) t'\<rbrace> threadSet f t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>
theory TcbAcc_R

lemma threadSet_ct[wp]:
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace>" apply (simp add: threadSet_def) apply (wp setObject_ct_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do tcb <- getObject t;
setObject t (f tcb)
od \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_cd[wp]:
  "\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace>" apply (simp add: threadSet_def) apply (wp setObject_cd_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> do tcb <- getObject t;
setObject t (f tcb)
od \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_ksDomSchedule[wp]:
  "\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace>" apply (simp add: threadSet_def) apply (wp setObject_ksDomSchedule_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> do tcb <- getObject t;
setObject t (f tcb)
od \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_it[wp]:
  "\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>" apply (simp add: threadSet_def) apply (wp setObject_it_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do tcb <- getObject t;
setObject t (f tcb)
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_sch_act:
  "(\<And>tcb. tcbState (F tcb) = tcbState tcb \<and> tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow>
  \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
  threadSet F t
  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (wp sch_act_wf_lift threadSet_pred_tcb_no_state | simp add: tcb_in_cur_domain'_def)+ apply (rule_tac f="ksCurDomain" in hoare_lift_Pf) apply (wp threadSet_obj_at'_strongish | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcbState (F tcb) = tcbState tcb \<and> tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ta. (\<And>tcb. tcbState (F tcb) = tcbState tcb \<and> tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) ta s\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) ta s\<rbrace>
 2. \<And>P. (\<And>tcb. tcbState (F tcb) = tcbState tcb \<and> tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 3. \<And>P. (\<And>tcb. tcbState (F tcb) = tcbState tcb \<and> tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 4. \<And>s. \<lbrakk>\<And>tcb. tcbState (F tcb) = tcbState tcb \<and> tcbDomain (F tcb) = tcbDomain tcb; sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) s proof (prove)
goal (5 subgoals):
 1. \<And>ta x. (\<And>tcb. tcbState (F tcb) = tcbState tcb \<and> tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) ta\<rbrace> threadSet F t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) ta\<rbrace>
 2. \<And>ta P. (\<And>tcb. tcbState (F tcb) = tcbState tcb \<and> tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 3. \<And>P. (\<And>tcb. tcbState (F tcb) = tcbState tcb \<and> tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 4. \<And>P. (\<And>tcb. tcbState (F tcb) = tcbState tcb \<and> tcbDomain (F tcb) = tcbDomain tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 5. \<And>s. \<lbrakk>\<And>tcb. tcbState (F tcb) = tcbState tcb \<and> tcbDomain (F tcb) = tcbDomain tcb; sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_invs_trivial_helper[simp]:
  "{r \<in> state_refs_of' s t. snd r \<noteq> TCBBound}
   \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} = state_refs_of' s t" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {r \<in> state_refs_of' s t. snd r \<noteq> TCBBound} \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} = state_refs_of' s t