theory CNode_DR

lemma cancel_badged_sends_def':
  "CSpace_D.cancel_badged_sends ep badge =
  (  do s\<leftarrow>get;
     tcb_filter_modify {x. \<exists>tcb. (cdl_objects s) x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep}
       (\<lambda>x. (case x of Some (Tcb tcb ) \<Rightarrow>
          if get_tcb_ep_badge tcb = Some badge then Some (Tcb (remove_pending_operation tcb cdl_cap.RestartCap))
          else x))
  od)" apply (simp add:CSpace_D.cancel_badged_sends_def get_def simpler_modify_def tcb_filter_modify_def) apply (clarsimp simp:bind_def) apply (rule ext) apply clarsimp apply (case_tac s) apply clarsimp apply (rule ext) apply (clarsimp simp:option_map_def split:option.splits cdl_object.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. CSpace_D.cancel_badged_sends ep badge = do s <- get;
tcb_filter_modify {x. \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep} (\<lambda>x. case x of Some (Tcb tcb) \<Rightarrow> if get_tcb_ep_badge tcb = Some badge then Some (Tcb (remove_pending_operation tcb RestartCap)) else x)
od proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. ({((), s\<lparr>cdl_objects := map_option (\<lambda>obj. case obj of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep \<and> get_tcb_ep_badge t = Some badge then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> obj) \<circ> cdl_objects s\<rparr>)}, False)) = do s <- \<lambda>s. ({(s, s)}, False);
\<lambda>sa. ({((), sa\<lparr>cdl_objects := \<lambda>x. if \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep then case cdl_objects sa x of Some (Tcb tcb) \<Rightarrow> if get_tcb_ep_badge tcb = Some badge then Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects sa x else cdl_objects sa x\<rparr>)}, False)
od proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. ({((), s\<lparr>cdl_objects := map_option (\<lambda>obj. case obj of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep \<and> get_tcb_ep_badge t = Some badge then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> obj) \<circ> cdl_objects s\<rparr>)}, False)) = (\<lambda>s. ({((), s\<lparr>cdl_objects := \<lambda>x. if \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep then case cdl_objects s x of Some (Tcb tcb) \<Rightarrow> if get_tcb_ep_badge tcb = Some badge then Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects s x else cdl_objects s x\<rparr>)}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>s. ({((), s\<lparr>cdl_objects := map_option (\<lambda>obj. case obj of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep \<and> get_tcb_ep_badge t = Some badge then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> obj) \<circ> cdl_objects s\<rparr>)}, False) = ({((), s\<lparr>cdl_objects := \<lambda>x. if \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep then case cdl_objects s x of Some (Tcb tcb) \<Rightarrow> if get_tcb_ep_badge tcb = Some badge then Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects s x else cdl_objects s x\<rparr>)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>s. s\<lparr>cdl_objects := map_option (\<lambda>obj. case obj of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep \<and> get_tcb_ep_badge t = Some badge then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> obj) \<circ> cdl_objects s\<rparr> = s\<lparr>cdl_objects := \<lambda>x. if \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep then case cdl_objects s x of Some (Tcb tcb) \<Rightarrow> if get_tcb_ep_badge tcb = Some badge then Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects s x else cdl_objects s x\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s cdl_arch cdl_objectsa cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain. s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> \<Longrightarrow> s\<lparr>cdl_objects := map_option (\<lambda>obj. case obj of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep \<and> get_tcb_ep_badge t = Some badge then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> obj) \<circ> cdl_objects s\<rparr> = s\<lparr>cdl_objects := \<lambda>x. if \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep then case cdl_objects s x of Some (Tcb tcb) \<Rightarrow> if get_tcb_ep_badge tcb = Some badge then Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects s x else cdl_objects s x\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objectsa cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain. map_option (\<lambda>obj. case obj of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep \<and> get_tcb_ep_badge t = Some badge then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> obj) \<circ> cdl_objectsa = (\<lambda>x. if \<exists>tcb. cdl_objectsa x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep then case cdl_objects \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> x of Some (Tcb tcb) \<Rightarrow> if get_tcb_ep_badge tcb = Some badge then Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> x else cdl_objects \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> x) proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objectsa cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x. (map_option (\<lambda>obj. case obj of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep \<and> get_tcb_ep_badge t = Some badge then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> obj) \<circ> cdl_objectsa) x = (if \<exists>tcb. cdl_objectsa x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep then case cdl_objects \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> x of Some (Tcb tcb) \<Rightarrow> if get_tcb_ep_badge tcb = Some badge then Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> x else cdl_objects \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> x) proof (prove)
goal:
No subgoals!