theory KHeap_DR

lemma ntfn_bound_set_lift:
  "\<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow>
  get_bound_notification_threads ntfnptr (transform s) =
  ntfn_bound_set ntfnptr s" apply (rule set_eqI) apply (clarsimp simp: get_bound_notification_threads_def ntfn_bound_set_def) apply (rule iffI) apply (clarsimp simp: transform_def transform_objects_def) apply (clarsimp simp: restrict_map_Some_iff) apply (clarsimp simp: infer_tcb_bound_notification_def transform_object_def
                         transform_tcb_def restrict_map_Some_iff tcb_slots
                  split: Structures_A.kernel_object.splits option.splits
                         Structures_A.thread_state.splits
                         ARM_A.arch_kernel_obj.splits| drule(1) valid_etcbs_tcb_etcb)+ apply (clarsimp simp: transform_def transform_object_def
                        transform_tcb_def transform_objects_def tcb_slots valid_idle_def obj_at_def
                        infer_tcb_bound_notification_def map_add_def restrict_map_Some_iff pred_tcb_at_def
                 split: nat.splits option.splits | drule(1) valid_etcbs_tcb_etcb)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow> get_bound_notification_threads ntfnptr (transform s) = ntfn_bound_set ntfnptr s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow> (x \<in> get_bound_notification_threads ntfnptr (transform s)) = (x \<in> ntfn_bound_set ntfnptr s) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow> (\<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr)) = (\<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr)\<rbrakk> \<Longrightarrow> \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr
 2. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x a. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); (\<exists>z. (kheap s |` (- {idle_thread s})) x = Some z \<and> transform_object (machine_state s) x ((ekheap s |` (- {idle_thread s})) x) z = Tcb a) \<or> (kheap s |` (- {idle_thread s})) x = None \<and> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s})) x = Some (Tcb a)\<rbrakk> \<Longrightarrow> \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr
 2. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x a z. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); kheap s x = Some z; x \<noteq> idle_thread s; transform_object (machine_state s) x (ekheap s x) z = Tcb a\<rbrakk> \<Longrightarrow> \<exists>t. z = TCB t \<and> tcb_bound_notification t = Some ntfnptr
 2. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (3 subgoals):
 1. \<And>x a x11 x12. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a 6 = Some (BoundNotificationCap ntfnptr); kheap s x = Some (kernel_object.CNode x11 x12); x \<noteq> idle_thread s; (case x11 of 0 \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 x12\<rparr> | Suc nat \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) x12, cdl_cnode_size_bits = Suc nat\<rparr>) = Tcb a\<rbrakk> \<Longrightarrow> False
 2. \<And>x a x2. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a 6 = Some (BoundNotificationCap ntfnptr); kheap s x = Some (TCB x2); x \<noteq> idle_thread s; ekheap s x = None; undefined = Tcb a\<rbrakk> \<Longrightarrow> tcb_bound_notification x2 = Some ntfnptr
 3. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal:
No subgoals!