theory KHeap_DR

lemma fast_finalise_no_effect:
  "\<lbrakk>opt_cap (y, tcb_pending_op_slot) (transform s) = Some cap;
   not_idle_thread y s;tcb_at y s; valid_etcbs s \<rbrakk>
  \<Longrightarrow> PageTableUnmap_D.fast_finalise cap (PageTableUnmap_D.is_final_cap' cap x) = return ()" apply (clarsimp simp:opt_cap_def transform_def tcb_at_def dest!:get_tcb_SomeD) apply (clarsimp simp:slots_of_def transform_objects_def
    not_idle_thread_def restrict_map_def
    split:option.splits if_splits) apply (drule(1) valid_etcbs_tcb_etcb, clarsimp) apply (clarsimp simp:object_slots_def transform_tcb_def) apply (clarsimp simp:infer_tcb_pending_op_def tcb_slots
    split:Structures_A.thread_state.splits | drule(1) valid_etcbs_tcb_etcb)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>opt_cap (y, tcb_pending_op_slot) (transform s) = Some cap; not_idle_thread y s; tcb_at y s; valid_etcbs s\<rbrakk> \<Longrightarrow> PageTableUnmap_D.fast_finalise cap (PageTableUnmap_D.is_final_cap' cap x) = return () proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>slots_of y \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s, cdl_cdt = transform_cdt s, cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr> tcb_pending_op_slot = Some cap; not_idle_thread y s; valid_etcbs s; kheap s y = Some (TCB tcb)\<rbrakk> \<Longrightarrow> PageTableUnmap_D.fast_finalise cap (PageTableUnmap_D.is_final_cap' cap x) = return () proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>y \<noteq> idle_thread s; valid_etcbs s; kheap s y = Some (TCB tcb); ekheap s y = None; object_slots undefined tcb_pending_op_slot = Some cap\<rbrakk> \<Longrightarrow> PageTableUnmap_D.fast_finalise cap (PageTableUnmap_D.is_final_cap' cap x) = return ()
 2. \<And>tcb x2. \<lbrakk>y \<noteq> idle_thread s; valid_etcbs s; kheap s y = Some (TCB tcb); ekheap s y = Some x2; object_slots (transform_tcb (machine_state s) y tcb x2) tcb_pending_op_slot = Some cap\<rbrakk> \<Longrightarrow> PageTableUnmap_D.fast_finalise cap (PageTableUnmap_D.is_final_cap' cap x) = return () proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2. \<lbrakk>y \<noteq> idle_thread s; valid_etcbs s; kheap s y = Some (TCB tcb); ekheap s y = Some x2; object_slots (transform_tcb (machine_state s) y tcb x2) tcb_pending_op_slot = Some cap\<rbrakk> \<Longrightarrow> PageTableUnmap_D.fast_finalise cap (PageTableUnmap_D.is_final_cap' cap x) = return () proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2. \<lbrakk>y \<noteq> idle_thread s; valid_etcbs s; kheap s y = Some (TCB tcb); ekheap s y = Some x2; (if tcb_pending_op_slot = tcb_boundntfn_slot then Some (infer_tcb_bound_notification (tcb_bound_notification tcb)) else [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb)] tcb_pending_op_slot) = Some cap\<rbrakk> \<Longrightarrow> PageTableUnmap_D.fast_finalise cap (PageTableUnmap_D.is_final_cap' cap x) = return () proof (prove)
goal:
No subgoals!