theory KHeap_DR

lemma cancel_all_ipc_def_alt1: "PageTableUnmap_D.cancel_all_ipc ep =
  (  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> Some (Tcb (remove_pending_operation tcb RestartCap))))
  od)" apply (simp add:PageTableUnmap_D.cancel_all_ipc_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) apply (case_tac x2) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. PageTableUnmap_D.cancel_all_ipc ep = 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> Some (Tcb (remove_pending_operation tcb RestartCap)))
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 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> Some (Tcb (remove_pending_operation tcb RestartCap)) 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 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> Some (Tcb (remove_pending_operation tcb RestartCap)) 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 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> Some (Tcb (remove_pending_operation tcb RestartCap)) 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 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> Some (Tcb (remove_pending_operation tcb RestartCap)) 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 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> Some (Tcb (remove_pending_operation tcb RestartCap)) 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 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> 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) 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 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> 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) proof (prove)
goal (1 subgoal):
 1. \<And>cdl_objects x x2. cdl_objects x = Some x2 \<Longrightarrow> ((\<exists>tcb. x2 = Tcb tcb \<and> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> Some (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) \<and> ((\<forall>tcb. x2 = Tcb tcb \<longrightarrow> \<not> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = x2) proof (prove)
goal (10 subgoals):
 1. \<And>cdl_objects x x2. \<lbrakk>cdl_objects x = Some x2; x2 = cdl_object.Endpoint\<rbrakk> \<Longrightarrow> ((\<exists>tcb. x2 = Tcb tcb \<and> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> Some (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) \<and> ((\<forall>tcb. x2 = Tcb tcb \<longrightarrow> \<not> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = x2)
 2. \<And>cdl_objects x x2. \<lbrakk>cdl_objects x = Some x2; x2 = cdl_object.Notification\<rbrakk> \<Longrightarrow> ((\<exists>tcb. x2 = Tcb tcb \<and> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> Some (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) \<and> ((\<forall>tcb. x2 = Tcb tcb \<longrightarrow> \<not> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = x2)
 3. \<And>cdl_objects x x2 x3. \<lbrakk>cdl_objects x = Some x2; x2 = Tcb x3\<rbrakk> \<Longrightarrow> ((\<exists>tcb. x2 = Tcb tcb \<and> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> Some (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) \<and> ((\<forall>tcb. x2 = Tcb tcb \<longrightarrow> \<not> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = x2)
 4. \<And>cdl_objects x x2 x4. \<lbrakk>cdl_objects x = Some x2; x2 = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> ((\<exists>tcb. x2 = Tcb tcb \<and> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> Some (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) \<and> ((\<forall>tcb. x2 = Tcb tcb \<longrightarrow> \<not> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = x2)
 5. \<And>cdl_objects x x2 x5. \<lbrakk>cdl_objects x = Some x2; x2 = AsidPool x5\<rbrakk> \<Longrightarrow> ((\<exists>tcb. x2 = Tcb tcb \<and> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> Some (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) \<and> ((\<forall>tcb. x2 = Tcb tcb \<longrightarrow> \<not> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = x2)
 6. \<And>cdl_objects x x2 x6. \<lbrakk>cdl_objects x = Some x2; x2 = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> ((\<exists>tcb. x2 = Tcb tcb \<and> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> Some (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) \<and> ((\<forall>tcb. x2 = Tcb tcb \<longrightarrow> \<not> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = x2)
 7. \<And>cdl_objects x x2 x7. \<lbrakk>cdl_objects x = Some x2; x2 = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> ((\<exists>tcb. x2 = Tcb tcb \<and> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> Some (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) \<and> ((\<forall>tcb. x2 = Tcb tcb \<longrightarrow> \<not> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = x2)
 8. \<And>cdl_objects x x2 x8. \<lbrakk>cdl_objects x = Some x2; x2 = Frame x8\<rbrakk> \<Longrightarrow> ((\<exists>tcb. x2 = Tcb tcb \<and> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> Some (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) \<and> ((\<forall>tcb. x2 = Tcb tcb \<longrightarrow> \<not> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = x2)
 9. \<And>cdl_objects x x2. \<lbrakk>cdl_objects x = Some x2; x2 = cdl_object.Untyped\<rbrakk> \<Longrightarrow> ((\<exists>tcb. x2 = Tcb tcb \<and> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> Some (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) \<and> ((\<forall>tcb. x2 = Tcb tcb \<longrightarrow> \<not> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = x2)
 10. \<And>cdl_objects x x2 x10. \<lbrakk>cdl_objects x = Some x2; x2 = IRQNode x10\<rbrakk> \<Longrightarrow> ((\<exists>tcb. x2 = Tcb tcb \<and> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> Some (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) \<and> ((\<forall>tcb. x2 = Tcb tcb \<longrightarrow> \<not> is_thread_blocked_on_endpoint tcb ep) \<longrightarrow> (case x2 of Tcb t \<Rightarrow> if is_thread_blocked_on_endpoint t ep then Tcb (remove_pending_operation t RestartCap) else Tcb t | _ \<Rightarrow> x2) = x2) proof (prove)
goal:
No subgoals!