theory ArchCNodeInv_AI

lemma weak_derived_update_cap_data [CNodeInv_AI_assms]:
  "\<lbrakk>update_cap_data P x c \<noteq> NullCap; weak_derived c c'\<rbrakk>
  \<Longrightarrow> weak_derived (update_cap_data P x c) c'" apply (simp add: weak_derived_def copy_of_def
                   cap_master_update_cap_data cap_asid_update_cap_data
                   cap_asid_base_update_cap_data
                   cap_vptr_update_cap_data
              split del: if_split cong: if_cong) apply (erule disjE) apply (clarsimp split: if_split_asm) apply (clarsimp simp: is_cap_simps) apply (simp add: update_cap_data_def arch_update_cap_data_def is_cap_simps) apply (erule (1) same_object_as_update_cap_data) apply clarsimp apply (rule conjI, clarsimp simp: is_cap_simps update_cap_data_def split del: if_split)+ apply clarsimp 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; weak_derived c c'\<rbrakk> \<Longrightarrow> weak_derived (update_cap_data P x c) c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>update_cap_data P x c \<noteq> NullCap; (if is_untyped_cap c' then c' = c else same_object_as c' c \<and> is_reply_cap c' = is_reply_cap c \<and> is_master_reply_cap c' = is_master_reply_cap c) \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = c\<rbrakk> \<Longrightarrow> (if is_untyped_cap c' then c' = update_cap_data P x c else same_object_as c' (update_cap_data P x c) \<and> is_reply_cap c' = is_reply_cap c \<and> is_master_reply_cap c' = is_master_reply_cap c) \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = update_cap_data P x c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>update_cap_data P x c \<noteq> NullCap; (if is_untyped_cap c' then c' = c else same_object_as c' c \<and> is_reply_cap c' = is_reply_cap c \<and> is_master_reply_cap c' = is_master_reply_cap c) \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c'\<rbrakk> \<Longrightarrow> (if is_untyped_cap c' then c' = update_cap_data P x c else same_object_as c' (update_cap_data P x c) \<and> is_reply_cap c' = is_reply_cap c \<and> is_master_reply_cap c' = is_master_reply_cap c) \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = update_cap_data P x c
 2. \<lbrakk>update_cap_data P x c \<noteq> NullCap; c' = c\<rbrakk> \<Longrightarrow> (if is_untyped_cap c' then c' = update_cap_data P x c else same_object_as c' (update_cap_data P x c) \<and> is_reply_cap c' = is_reply_cap c \<and> is_master_reply_cap c' = is_master_reply_cap c) \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = update_cap_data P x c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>update_cap_data P x c \<noteq> NullCap; is_untyped_cap c; c' = c\<rbrakk> \<Longrightarrow> c = update_cap_data P x c
 2. \<lbrakk>update_cap_data P x c \<noteq> NullCap; \<not> is_untyped_cap c'; same_object_as c' c; is_reply_cap c' = is_reply_cap c; is_master_reply_cap c' = is_master_reply_cap c; cap_asid c = cap_asid c'; cap_asid_base c = cap_asid_base c'; cap_vptr c = cap_vptr c'; c' \<noteq> update_cap_data P x c\<rbrakk> \<Longrightarrow> same_object_as c' (update_cap_data P x c)
 3. \<lbrakk>update_cap_data P x c \<noteq> NullCap; c' = c\<rbrakk> \<Longrightarrow> (if is_untyped_cap c' then c' = update_cap_data P x c else same_object_as c' (update_cap_data P x c) \<and> is_reply_cap c' = is_reply_cap c \<and> is_master_reply_cap c' = is_master_reply_cap c) \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = update_cap_data P x c proof (prove)
goal (3 subgoals):
 1. \<And>dev r bits f. \<lbrakk>update_cap_data P x (UntypedCap dev r bits f) \<noteq> NullCap; c' = UntypedCap dev r bits f; c = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> UntypedCap dev r bits f = update_cap_data P x (UntypedCap dev r bits f)
 2. \<lbrakk>update_cap_data P x c \<noteq> NullCap; \<not> is_untyped_cap c'; same_object_as c' c; is_reply_cap c' = is_reply_cap c; is_master_reply_cap c' = is_master_reply_cap c; cap_asid c = cap_asid c'; cap_asid_base c = cap_asid_base c'; cap_vptr c = cap_vptr c'; c' \<noteq> update_cap_data P x c\<rbrakk> \<Longrightarrow> same_object_as c' (update_cap_data P x c)
 3. \<lbrakk>update_cap_data P x c \<noteq> NullCap; c' = c\<rbrakk> \<Longrightarrow> (if is_untyped_cap c' then c' = update_cap_data P x c else same_object_as c' (update_cap_data P x c) \<and> is_reply_cap c' = is_reply_cap c \<and> is_master_reply_cap c' = is_master_reply_cap c) \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = update_cap_data P x c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>update_cap_data P x c \<noteq> NullCap; \<not> is_untyped_cap c'; same_object_as c' c; is_reply_cap c' = is_reply_cap c; is_master_reply_cap c' = is_master_reply_cap c; cap_asid c = cap_asid c'; cap_asid_base c = cap_asid_base c'; cap_vptr c = cap_vptr c'; c' \<noteq> update_cap_data P x c\<rbrakk> \<Longrightarrow> same_object_as c' (update_cap_data P x c)
 2. \<lbrakk>update_cap_data P x c \<noteq> NullCap; c' = c\<rbrakk> \<Longrightarrow> (if is_untyped_cap c' then c' = update_cap_data P x c else same_object_as c' (update_cap_data P x c) \<and> is_reply_cap c' = is_reply_cap c \<and> is_master_reply_cap c' = is_master_reply_cap c) \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = update_cap_data P x c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>update_cap_data P x c \<noteq> NullCap; c' = c\<rbrakk> \<Longrightarrow> (if is_untyped_cap c' then c' = update_cap_data P x c else same_object_as c' (update_cap_data P x c) \<and> is_reply_cap c' = is_reply_cap c \<and> is_master_reply_cap c' = is_master_reply_cap c) \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = update_cap_data P x c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>update_cap_data P x c \<noteq> NullCap; c' = c\<rbrakk> \<Longrightarrow> (is_untyped_cap c \<longrightarrow> c = update_cap_data P x c) \<and> (\<not> is_untyped_cap c \<longrightarrow> same_object_as c (update_cap_data P x c) \<or> c = update_cap_data P x c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>update_cap_data P x c \<noteq> NullCap; c' = c\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap c \<longrightarrow> same_object_as c (update_cap_data P x c) \<or> c = update_cap_data P x c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>update_cap_data P x c \<noteq> NullCap; c' = c; \<not> is_untyped_cap c; c \<noteq> update_cap_data P x c\<rbrakk> \<Longrightarrow> same_object_as c (update_cap_data P x c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>update_cap_data P x c \<noteq> NullCap; c' = c; \<forall>dev r bits f. c \<noteq> UntypedCap dev r bits f; c \<noteq> update_cap_data P x c\<rbrakk> \<Longrightarrow> case c of UntypedCap dev r bits free \<Rightarrow> False | IRQControlCap \<Rightarrow> case update_cap_data P x c of IRQHandlerCap n \<Rightarrow> False | _ \<Rightarrow> same_region_as c (update_cap_data P x c) | ArchObjectCap ac \<Rightarrow> case update_cap_data P x c of ArchObjectCap x \<Rightarrow> same_aobject_as ac x | _ \<Rightarrow> same_region_as c (update_cap_data P x c) | _ \<Rightarrow> same_region_as c (update_cap_data P x c) proof (prove)
goal:
No subgoals!