theory KHeap_DP

lemma is_exclusive_cap_update_cap_data:
  "safe_for_derive (update_cap_data_det badge cap) = safe_for_derive cap" apply (rule iffI) apply (simp_all add: safe_for_derive_def update_cap_data_def update_cap_data_det_def) apply (case_tac cap, simp_all add: safe_for_derive_def badge_update_def
                               split: if_split_asm) apply (case_tac cap, simp_all add: badge_update_def guard_update_def
                                     update_cap_badge_def
                              split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. safe_for_derive (update_cap_data_det badge cap) = safe_for_derive cap proof (prove)
goal (2 subgoals):
 1. safe_for_derive (update_cap_data_det badge cap) \<Longrightarrow> safe_for_derive cap
 2. safe_for_derive cap \<Longrightarrow> safe_for_derive (update_cap_data_det badge cap) proof (prove)
goal (2 subgoals):
 1. case case cap of EndpointCap x b xa \<Rightarrow> badge_update badge cap | NotificationCap x b xa \<Rightarrow> badge_update badge cap | CNodeCap object g gs x \<Rightarrow> guard_update cap badge | _ \<Rightarrow> cap of NullCap \<Rightarrow> False | UntypedCap x xa xb \<Rightarrow> False | ReplyCap x xa \<Rightarrow> False | MasterReplyCap x \<Rightarrow> False | IrqControlCap \<Rightarrow> False | PageTableCap x xa xb \<Rightarrow> False | PageDirectoryCap x xa xb \<Rightarrow> False | ZombieCap x \<Rightarrow> False | _ \<Rightarrow> True \<Longrightarrow> case cap of NullCap \<Rightarrow> False | UntypedCap x xa xb \<Rightarrow> False | ReplyCap x xa \<Rightarrow> False | MasterReplyCap x \<Rightarrow> False | IrqControlCap \<Rightarrow> False | PageTableCap x xa xb \<Rightarrow> False | PageDirectoryCap x xa xb \<Rightarrow> False | ZombieCap x \<Rightarrow> False | _ \<Rightarrow> True
 2. case cap of NullCap \<Rightarrow> False | UntypedCap x xa xb \<Rightarrow> False | ReplyCap x xa \<Rightarrow> False | MasterReplyCap x \<Rightarrow> False | IrqControlCap \<Rightarrow> False | PageTableCap x xa xb \<Rightarrow> False | PageDirectoryCap x xa xb \<Rightarrow> False | ZombieCap x \<Rightarrow> False | _ \<Rightarrow> True \<Longrightarrow> case case cap of EndpointCap x b xa \<Rightarrow> badge_update badge cap | NotificationCap x b xa \<Rightarrow> badge_update badge cap | CNodeCap object g gs x \<Rightarrow> guard_update cap badge | _ \<Rightarrow> cap of NullCap \<Rightarrow> False | UntypedCap x xa xb \<Rightarrow> False | ReplyCap x xa \<Rightarrow> False | MasterReplyCap x \<Rightarrow> False | IrqControlCap \<Rightarrow> False | PageTableCap x xa xb \<Rightarrow> False | PageDirectoryCap x xa xb \<Rightarrow> False | ZombieCap x \<Rightarrow> False | _ \<Rightarrow> True proof (prove)
goal (1 subgoal):
 1. case cap of NullCap \<Rightarrow> False | UntypedCap x xa xb \<Rightarrow> False | ReplyCap x xa \<Rightarrow> False | MasterReplyCap x \<Rightarrow> False | IrqControlCap \<Rightarrow> False | PageTableCap x xa xb \<Rightarrow> False | PageDirectoryCap x xa xb \<Rightarrow> False | ZombieCap x \<Rightarrow> False | _ \<Rightarrow> True \<Longrightarrow> case case cap of EndpointCap x b xa \<Rightarrow> badge_update badge cap | NotificationCap x b xa \<Rightarrow> badge_update badge cap | CNodeCap object g gs x \<Rightarrow> guard_update cap badge | _ \<Rightarrow> cap of NullCap \<Rightarrow> False | UntypedCap x xa xb \<Rightarrow> False | ReplyCap x xa \<Rightarrow> False | MasterReplyCap x \<Rightarrow> False | IrqControlCap \<Rightarrow> False | PageTableCap x xa xb \<Rightarrow> False | PageDirectoryCap x xa xb \<Rightarrow> False | ZombieCap x \<Rightarrow> False | _ \<Rightarrow> True proof (prove)
goal:
No subgoals!