kings-crown/FVELER_Isabelle huggingface dataset:
theory Schedule_R

lemma arch_switchToIdleThread_corres:
  "corres dc (valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and
      valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_idle)
     (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_idle')
        arch_switch_to_idle_thread
        Arch.switchToIdleThread" apply (simp add: arch_switch_to_idle_thread_def
                ARM_H.switchToIdleThread_def) apply (corresKsimp corres: getIdleThread_corres setVMRoot_corres[@lift_corres_args]) apply (clarsimp simp: valid_idle_def valid_idle'_def pred_tcb_at_def obj_at_def is_tcb obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_idle) (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_idle') arch_switch_to_idle_thread Arch.switchToIdleThread proof (prove)
goal (1 subgoal):
 1. corres dc (valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_idle) (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_idle') (gets idle_thread >>= set_vm_root) (getIdleThread >>= setVMRoot) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; valid_arch_state s; valid_arch_state' s'; valid_objs s; pspace_aligned' s'; valid_asid_map s; pspace_distinct' s'; unique_table_refs (caps_of_state s); no_0_obj' s'; valid_idle' s'; valid_vs_lookup s; valid_global_objs s; pspace_aligned s; pspace_distinct s; valid_vspace_objs s; valid_idle s\<rbrakk> \<Longrightarrow> tcb_at (idle_thread s) s \<and> tcb_at' (ksIdleThread s') s' proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma sch_act_wf:
  "sch_act_wf sa s = ((\<forall>t. sa = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and>
                                                    tcb_in_cur_domain' t s) \<and>
                      (sa = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s))" by (case_tac sa,  simp_all add: )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_wf sa s = ((\<forall>t. sa = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s) \<and> (sa = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s))
theory Schedule_R

lemma threadSet_timeslice_invs:
  "\<lbrace>invs' and tcb_at' t\<rbrace> threadSet (tcbTimeSlice_update b) t \<lbrace>\<lambda>rv. invs'\<rbrace>" by (wp threadSet_invs_trivial, simp_all add: inQ_def cong: conj_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t\<rbrace> threadSet (tcbTimeSlice_update b) t \<lbrace>\<lambda>rv. invs'\<rbrace>
theory Schedule_R

lemma setCurThread_invs:
  "\<lbrace>invs' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and
    tcb_in_cur_domain' t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace>" by (rule hoare_pre, rule setCurThread_invs_no_cicd')
     (simp add: invs'_to_invs_no_cicd'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and tcb_in_cur_domain' t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace>
theory Schedule_R

lemma idle'_not_tcbQueued':
 assumes vq:   "Invariants_H.valid_queues s"
     and vq':  "valid_queues' s"
     and idle: "valid_idle' s"
 shows "obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s" proof - from idle have stidle: "st_tcb_at' (Not \<circ> runnable') (ksIdleThread s) s" by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs idle_tcb'_def) with vq vq' show ?thesis by (rule valid_queues_not_runnable_not_queued) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s proof (state)
goal (1 subgoal):
 1. obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s proof (chain)
picking this:
valid_idle' s proof (prove)
using this:
valid_idle' s

goal (1 subgoal):
 1. st_tcb_at' (Not \<circ> runnable') (ksIdleThread s) s proof (state)
this:
st_tcb_at' (Not \<circ> runnable') (ksIdleThread s) s

goal (1 subgoal):
 1. obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s proof (chain)
picking this:
Invariants_H.valid_queues s
valid_queues' s
st_tcb_at' (Not \<circ> runnable') (ksIdleThread s) s proof (prove)
using this:
Invariants_H.valid_queues s
valid_queues' s
st_tcb_at' (Not \<circ> runnable') (ksIdleThread s) s

goal (1 subgoal):
 1. obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s proof (state)
this:
obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s

goal:
No subgoals!
theory Schedule_R

lemma clearExMonitor_invs'[wp]:
  "\<lbrace>invs'\<rbrace> doMachineOp ARM.clearExMonitor \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (wp dmo_invs' no_irq) apply (simp add: no_irq_clearExMonitor) apply (clarsimp simp: ARM.clearExMonitor_def machine_op_lift_def
                        in_monad select_f_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp ARM.clearExMonitor \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. no_irq ARM.clearExMonitor
 2. \<And>s. invs' s \<Longrightarrow> ((\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (ARM.clearExMonitor m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (ARM.clearExMonitor m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs') s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma Arch_switchToThread_invs[wp]:
  "\<lbrace>invs' and tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: ARM_H.switchToThread_def) apply (wp; auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t\<rbrace> do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma Arch_swichToThread_tcbDomain_triv[wp]:
  "\<lbrace> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace> Arch.switchToThread t \<lbrace> \<lambda>_. obj_at'  (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>" apply (clarsimp simp: ARM_H.switchToThread_def storeWordUser_def) apply (wp hoare_drop_imp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma Arch_swichToThread_tcbPriority_triv[wp]:
  "\<lbrace> obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace> Arch.switchToThread t \<lbrace> \<lambda>_. obj_at'  (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>" apply (clarsimp simp: ARM_H.switchToThread_def storeWordUser_def) apply (wp hoare_drop_imp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma Arch_switchToThread_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_. tcb_in_cur_domain' t' \<rbrace>" apply (rule tcb_in_cur_domain'_lift) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 2. \<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma tcbSchedDequeue_not_tcbQueued:
  "\<lbrace> tcb_at' t \<rbrace> tcbSchedDequeue t \<lbrace> \<lambda>_. obj_at' (\<lambda>x. \<not> tcbQueued x) t \<rbrace>" apply (simp add: tcbSchedDequeue_def) apply (wp|clarsimp)+ apply (rule_tac Q="\<lambda>queued. obj_at' (\<lambda>x. tcbQueued x = queued) t" in hoare_post_imp) apply (clarsimp simp: obj_at'_def) apply (wp threadGet_obj_at') apply (simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. obj_at' (\<lambda>x. \<not> tcbQueued x) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> do queued <- threadGet tcbQueued t;
when queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
od \<lbrace>\<lambda>_. obj_at' (\<lambda>x. \<not> tcbQueued x) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then tcb_at' t else obj_at' (\<lambda>x. \<not> tcbQueued x) t\<rbrace>
 2. \<And>s. tcb_at' t s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. obj_at' (\<lambda>x. tcbQueued x = rv) t s \<Longrightarrow> (if rv then tcb_at' t else obj_at' (\<lambda>x. \<not> tcbQueued x) t) s
 2. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. obj_at' (\<lambda>x. tcbQueued x = queued) t\<rbrace>
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. obj_at' (\<lambda>x. tcbQueued x = queued) t\<rbrace>
 2. \<And>s. tcb_at' t s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<Longrightarrow> obj_at' (\<lambda>t. tcbQueued t = tcbQueued t) t s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma Arch_switchToThread_obj_at[wp]:
  "\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace>
   Arch.switchToThread t
   \<lbrace>\<lambda>rv. obj_at' (P \<circ> tcbState) t\<rbrace>" apply (simp add: ARM_H.switchToThread_def ) apply (rule hoare_seq_ext)+ apply (rule doMachineOp_obj_at) apply (rule setVMRoot_obj_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. obj_at' (P \<circ> tcbState) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od \<lbrace>\<lambda>rv. obj_at' (P \<circ> tcbState) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrace>?B y\<rbrace> doMachineOp ARM.clearExMonitor \<lbrace>\<lambda>rv. obj_at' (P \<circ> tcbState) t\<rbrace>
 2. \<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> setVMRoot t \<lbrace>?B\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> setVMRoot t \<lbrace>\<lambda>y. obj_at' (P \<circ> tcbState) t\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma clearExMonitor_invs_no_cicd'[wp]:
  "\<lbrace>invs_no_cicd'\<rbrace> doMachineOp ARM.clearExMonitor \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>" apply (wp dmo_invs_no_cicd' no_irq) apply (simp add: no_irq_clearExMonitor) apply (clarsimp simp: ARM.clearExMonitor_def machine_op_lift_def
                        in_monad select_f_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> doMachineOp ARM.clearExMonitor \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. no_irq ARM.clearExMonitor
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (ARM.clearExMonitor m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and all_invs_but_ct_idle_or_in_cur_domain') s proof (prove)
goal (1 subgoal):
 1. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (ARM.clearExMonitor m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and all_invs_but_ct_idle_or_in_cur_domain') s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma Arch_switchToThread_invs_no_cicd':
  "\<lbrace>invs_no_cicd'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>" apply (simp add: ARM_H.switchToThread_def) by (wp|rule setVMRoot_invs_no_cicd')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace>
theory Schedule_R

lemma switchToThread_invs_no_cicd':
  "\<lbrace>invs_no_cicd' and st_tcb_at' runnable' t and tcb_in_cur_domain' t \<rbrace> ThreadDecls_H.switchToThread t \<lbrace>\<lambda>rv. invs' \<rbrace>" apply (simp add: Thread_H.switchToThread_def) apply (wp setCurThread_invs_no_cicd' tcbSchedDequeue_not_tcbQueued
            Arch_switchToThread_invs_no_cicd' Arch_switchToThread_pred_tcb') apply (auto elim!: pred_tcb'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and st_tcb_at' runnable' t and tcb_in_cur_domain' t\<rbrace> global.switchToThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and st_tcb_at' runnable' t and tcb_in_cur_domain' t\<rbrace> do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (all_invs_but_ct_idle_or_in_cur_domain' and st_tcb_at' runnable' t and tcb_in_cur_domain' t) s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s \<and> tcb_at' t s \<and> st_tcb_at' activatable' t s \<and> tcb_at' t s \<and> tcb_in_cur_domain' t s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma setCurThread_ct_in_state:
  "\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>" proof - show ?thesis apply (simp add: setCurThread_def) apply wp apply (simp add: ct_in_state'_def pred_tcb_at'_def o_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> modify (ksCurThread_update (\<lambda>_. t)) \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (P \<circ> tcbState) t s \<Longrightarrow> ct_in_state' P (s\<lparr>ksCurThread := t\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>

goal:
No subgoals!
theory Schedule_R

lemma switchToThread_ct_in_state[wp]:
  "\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> switchToThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>" proof - show ?thesis apply (simp add: Thread_H.switchToThread_def tcbSchedEnqueue_def unless_def) apply (wp setCurThread_ct_in_state Arch_switchToThread_obj_at
         | simp add: o_def cong: if_cong)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> global.switchToThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> global.switchToThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> global.switchToThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> global.switchToThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>

goal:
No subgoals!
theory Schedule_R

lemma setCurThread_obj_at[wp]:
  "\<lbrace>obj_at' P addr\<rbrace> setCurThread t \<lbrace>\<lambda>rv. obj_at' P addr\<rbrace>" apply (simp add: setCurThread_def) apply wp apply (fastforce intro: obj_at'_pspaceI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P addr\<rbrace> setCurThread t \<lbrace>\<lambda>rv. obj_at' P addr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P addr\<rbrace> modify (ksCurThread_update (\<lambda>_. t)) \<lbrace>\<lambda>rv. obj_at' P addr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' P addr s \<Longrightarrow> obj_at' P addr (s\<lparr>ksCurThread := t\<rparr>) proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma dmo_cap_to'[wp]:
  "\<lbrace>ex_nonz_cap_to' p\<rbrace>
     doMachineOp m
   \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" by (wp ex_nonz_cap_to_pres')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>
theory Schedule_R

lemma sct_cap_to'[wp]:
  "\<lbrace>ex_nonz_cap_to' p\<rbrace> setCurThread t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" apply (simp add: setCurThread_def) apply (wp ex_nonz_cap_to_pres') apply (clarsimp elim!: cte_wp_at'_pspaceI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> setCurThread t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> modify (ksCurThread_update (\<lambda>_. t)) \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P p s. cte_wp_at' P p s \<Longrightarrow> cte_wp_at' P p (s\<lparr>ksCurThread := t\<rparr>)
 2. \<And>s. ex_nonz_cap_to' p s \<Longrightarrow> ex_nonz_cap_to' p s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma iflive_inQ_nonz_cap_strg:
  "if_live_then_nonz_cap' s \<and> obj_at' (inQ d prio) t s
          \<longrightarrow> ex_nonz_cap_to' t s" by (clarsimp simp: obj_at'_real_def projectKOs inQ_def
              elim!: if_live_then_nonz_capE' ko_wp_at'_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if_live_then_nonz_cap' s \<and> obj_at' (inQ d prio) t s \<longrightarrow> ex_nonz_cap_to' t s
theory Schedule_R

lemma obj_tcb_at':
  "obj_at' (\<lambda>tcb::tcb. P tcb) t s \<Longrightarrow> tcb_at' t s" by (clarsimp simp: obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P t s \<Longrightarrow> tcb_at' t s
theory Schedule_R

lemma invs'_not_runnable_not_queued:
  fixes s
  assumes inv: "invs' s"
      and st: "st_tcb_at' (Not \<circ> runnable') t s"
  shows "obj_at' (Not \<circ> tcbQueued) t s" apply (insert assms) apply (rule valid_queues_not_runnable_not_queued) apply (clarsimp simp add: invs'_def valid_state'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' (Not \<circ> tcbQueued) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; st_tcb_at' (Not \<circ> runnable') t s\<rbrakk> \<Longrightarrow> obj_at' (Not \<circ> tcbQueued) t s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invs' s; st_tcb_at' (Not \<circ> runnable') t s\<rbrakk> \<Longrightarrow> Invariants_H.valid_queues s
 2. \<lbrakk>invs' s; st_tcb_at' (Not \<circ> runnable') t s\<rbrakk> \<Longrightarrow> valid_queues' s
 3. \<lbrakk>invs' s; st_tcb_at' (Not \<circ> runnable') t s\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> runnable') t s proof (prove)
goal:
No subgoals!