theory ArchCNodeInv_AI

lemma same_object_as_update_cap_data [CNodeInv_AI_assms]:
  "\<lbrakk> update_cap_data P x c \<noteq> NullCap; same_object_as c' c \<rbrakk> \<Longrightarrow>
  same_object_as c' (update_cap_data P x c)" apply (clarsimp simp: same_object_as_def is_cap_simps
                  split: cap.split_asm arch_cap.splits if_split_asm) apply (simp add: update_cap_data_def badge_update_def cap_rights_update_def is_cap_simps arch_update_cap_data_def
                   Let_def split_def the_cnode_cap_def bits_of_def split: if_split_asm cap.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>update_cap_data P x c \<noteq> NullCap; same_object_as c' c\<rbrakk> \<Longrightarrow> same_object_as c' (update_cap_data P x c) proof (prove)
goal (13 subgoals):
 1. \<And>x32 x33 r b R. \<lbrakk>update_cap_data P x (EndpointCap r b R) \<noteq> NullCap; c' = EndpointCap r x32 x33; c = EndpointCap r b R\<rbrakk> \<Longrightarrow> (\<exists>ra ba Ra. update_cap_data P x (EndpointCap r b R) = EndpointCap ra ba Ra) \<and> obj_ref_of (update_cap_data P x (EndpointCap r b R)) = r
 2. \<And>x42 x43 r b R. \<lbrakk>update_cap_data P x (NotificationCap r b R) \<noteq> NullCap; c' = NotificationCap r x42 x43; c = NotificationCap r b R\<rbrakk> \<Longrightarrow> (\<exists>ra ba Ra. update_cap_data P x (NotificationCap r b R) = NotificationCap ra ba Ra) \<and> obj_ref_of (update_cap_data P x (NotificationCap r b R)) = r
 3. \<And>x51 x52 x53 m' cr. \<lbrakk>update_cap_data P x (ReplyCap x51 m' cr) \<noteq> NullCap; c' = ReplyCap x51 x52 x53; c = ReplyCap x51 m' cr\<rbrakk> \<Longrightarrow> \<exists>m'a cra. update_cap_data P x (ReplyCap x51 m' cr) = ReplyCap x51 m'a cra
 4. \<And>x63 r bits g. \<lbrakk>update_cap_data P x (CNodeCap r bits g) \<noteq> NullCap; c' = CNodeCap r (bits_of (CNodeCap r bits g)) x63; c = CNodeCap r bits g\<rbrakk> \<Longrightarrow> (\<exists>ra bitsa ga. update_cap_data P x (CNodeCap r bits g) = CNodeCap ra bitsa ga) \<and> obj_ref_of (update_cap_data P x (CNodeCap r bits g)) = r \<and> bits_of (update_cap_data P x (CNodeCap r bits g)) = bits_of (CNodeCap r bits g)
 5. \<And>r. \<lbrakk>update_cap_data P x (ThreadCap r) \<noteq> NullCap; c' = ThreadCap r; c = ThreadCap r\<rbrakk> \<Longrightarrow> (\<exists>ra. update_cap_data P x (ThreadCap r) = ThreadCap ra) \<and> obj_ref_of (update_cap_data P x (ThreadCap r)) = r
 6. \<lbrakk>update_cap_data P x DomainCap \<noteq> NullCap; c' = DomainCap; c = DomainCap\<rbrakk> \<Longrightarrow> update_cap_data P x DomainCap = DomainCap
 7. \<lbrakk>update_cap_data P x IRQControlCap \<noteq> NullCap; c = IRQControlCap; c' = IRQControlCap\<rbrakk> \<Longrightarrow> case update_cap_data P x IRQControlCap of IRQHandlerCap n \<Rightarrow> False | _ \<Rightarrow> same_region_as IRQControlCap (update_cap_data P x IRQControlCap)
 8. \<And>x10. \<lbrakk>update_cap_data P x (IRQHandlerCap x10) \<noteq> NullCap; c' = IRQHandlerCap x10; c = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> update_cap_data P x (IRQHandlerCap x10) = IRQHandlerCap x10
 9. \<And>x12a x11 x12b. \<lbrakk>update_cap_data P x (ArchObjectCap x12a) \<noteq> NullCap; c = ArchObjectCap x12a; arch_same_region_as (ASIDPoolCap x11 x12b) x12a; c' = ArchObjectCap (ASIDPoolCap x11 x12b)\<rbrakk> \<Longrightarrow> case update_cap_data P x (ArchObjectCap x12a) of ArchObjectCap x \<Rightarrow> same_aobject_as (ASIDPoolCap x11 x12b) x | _ \<Rightarrow> same_region_as (ArchObjectCap (ASIDPoolCap x11 x12b)) (update_cap_data P x (ArchObjectCap x12a))
 10. \<And>x12a. \<lbrakk>update_cap_data P x (ArchObjectCap x12a) \<noteq> NullCap; c = ArchObjectCap x12a; arch_same_region_as ASIDControlCap x12a; c' = ArchObjectCap ASIDControlCap\<rbrakk> \<Longrightarrow> case update_cap_data P x (ArchObjectCap x12a) of ArchObjectCap x \<Rightarrow> same_aobject_as ASIDControlCap x | _ \<Rightarrow> same_region_as (ArchObjectCap ASIDControlCap) (update_cap_data P x (ArchObjectCap x12a))
A total of 13 subgoals... proof (prove)
goal:
No subgoals!