theory RWHelper_DP

lemma all_scheduable_tcbs_rewrite:
  "all_scheduable_tcbs (cdl_objects s) =
  sep_all_scheduable_tcbs (sep_heap (sep_state_projection s))" apply (intro set_eqI iffI) apply (clarsimp simp:all_scheduable_tcbs_def sep_state_projection_def
    sep_all_scheduable_tcbs_def object_at_heap_def object_project_def
    is_tcb_obj_type) apply (clarsimp simp:object_type_def object_slots_object_clean
    tcb_scheduable_def object_slots_def scheduable_cap_def) apply (fastforce simp:object_clean_def asid_reset_def update_slots_def
    reset_cap_asid_def intent_reset_def object_slots_def
    split:if_splits) apply (clarsimp simp:all_scheduable_tcbs_def sep_state_projection_def
    sep_all_scheduable_tcbs_def object_at_heap_def object_project_def
    is_tcb_obj_type split:option.splits) apply (clarsimp simp:object_type_def tcb_scheduable_def
   scheduable_cap_def object_slots_def object_clean_def asid_reset_def
   update_slots_def intent_reset_def reset_cap_asid_def
   split:cdl_object.splits cdl_cap.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_scheduable_tcbs (cdl_objects s) = sep_all_scheduable_tcbs (cdl.lift sep_heap s) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> all_scheduable_tcbs (cdl_objects s) \<Longrightarrow> x \<in> sep_all_scheduable_tcbs (cdl.lift sep_heap s)
 2. \<And>x. x \<in> sep_all_scheduable_tcbs (cdl.lift sep_heap s) \<Longrightarrow> x \<in> all_scheduable_tcbs (cdl_objects s) proof (prove)
goal (2 subgoals):
 1. \<And>x tcb. \<lbrakk>cdl_objects s x = Some (Tcb tcb); tcb_scheduable tcb\<rbrakk> \<Longrightarrow> object_type (Tcb tcb) = TcbType \<and> (\<exists>cap. object_slots (object_clean (Tcb tcb)) tcb_pending_op_slot = Some cap \<and> scheduable_cap cap)
 2. \<And>x. x \<in> sep_all_scheduable_tcbs (cdl.lift sep_heap s) \<Longrightarrow> x \<in> all_scheduable_tcbs (cdl_objects s) proof (prove)
goal (2 subgoals):
 1. \<And>x tcb. \<lbrakk>cdl_objects s x = Some (Tcb tcb); cdl_tcb_caps tcb tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps tcb tcb_pending_op_slot = Some RestartCap\<rbrakk> \<Longrightarrow> \<exists>cap. (case object_clean (Tcb tcb) of Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | PageTable x \<Rightarrow> cdl_page_table_caps x | PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) tcb_pending_op_slot = Some cap \<and> (case cap of RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False)
 2. \<And>x. x \<in> sep_all_scheduable_tcbs (cdl.lift sep_heap s) \<Longrightarrow> x \<in> all_scheduable_tcbs (cdl_objects s) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> sep_all_scheduable_tcbs (cdl.lift sep_heap s) \<Longrightarrow> x \<in> all_scheduable_tcbs (cdl_objects s) proof (prove)
goal (1 subgoal):
 1. \<And>x z cap. \<lbrakk>object_type z = TcbType; scheduable_cap cap; cdl_objects s x = Some z; object_slots (object_clean z) tcb_pending_op_slot = Some cap\<rbrakk> \<Longrightarrow> \<exists>tcb. z = Tcb tcb \<and> tcb_scheduable tcb proof (prove)
goal:
No subgoals!