theory CSpace1_R

lemma cap_relation_masks:
  "cap_relation c c' \<Longrightarrow> cap_relation
      (cap_rights_update (cap_rights c \<inter> rmask) c)
      (RetypeDecls_H.maskCapRights (rights_mask_map rmask) c')" apply (case_tac c; simp add: isCap_defs maskCapRights_def Let_def
                                 rights_mask_map_def maskVMRights_def
                                 AllowSend_def AllowRecv_def
                                 cap_rights_update_def
                          split del: if_split split:bool.splits) apply (clarsimp simp add: isCap_defs) by (rule ArchAcc_R.arch_cap_rights_update
         [simplified, simplified rights_mask_map_def])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation c c' \<Longrightarrow> cap_relation (cap_rights_update (cap_rights c \<inter> rmask) c) (global.maskCapRights (rights_mask_map rmask) c') proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<exists>a'. acap_relation (acap_rights_update (acap_rights x12 \<inter> rmask) x12) a' \<and> (if c' = capability.NullCap then capability.NullCap else if c' = capability.DomainCap then capability.DomainCap else if case c' of capability.UntypedCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False then c' else if case c' of capability.EndpointCap v0 v1 v2 v3 v4 v5 \<Rightarrow> True | _ \<Rightarrow> False then capEPCanGrantReply_update (\<lambda>_. capEPCanGrantReply c' \<and> AllowGrantReply \<in> rmask) (capEPCanGrant_update (\<lambda>_. capEPCanGrant c' \<and> AllowGrant \<in> rmask) (capEPCanReceive_update (\<lambda>_. capEPCanReceive c' \<and> AllowRead \<in> rmask) (capEPCanSend_update (\<lambda>_. capEPCanSend c' \<and> AllowWrite \<in> rmask) c'))) else if case c' of capability.NotificationCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False then capNtfnCanReceive_update (\<lambda>_. capNtfnCanReceive c' \<and> AllowRead \<in> rmask) (capNtfnCanSend_update (\<lambda>_. capNtfnCanSend c' \<and> AllowWrite \<in> rmask) c') else if case c' of capability.ReplyCap v0 v1 v2 \<Rightarrow> True | _ \<Rightarrow> False then capReplyCanGrant_update (\<lambda>_. capReplyCanGrant c' \<and> AllowGrant \<in> rmask) c' else if case c' of capability.CNodeCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False then c' else if case c' of capability.ThreadCap v0 \<Rightarrow> True | _ \<Rightarrow> False then c' else if case c' of capability.IRQControlCap \<Rightarrow> True | _ \<Rightarrow> False then c' else if case c' of capability.IRQHandlerCap v0 \<Rightarrow> True | _ \<Rightarrow> False then c' else if case c' of capability.ArchObjectCap v0 \<Rightarrow> True | _ \<Rightarrow> False then Arch.maskCapRights (CapRights (AllowWrite \<in> rmask) (AllowRead \<in> rmask) (AllowGrant \<in> rmask) (AllowGrantReply \<in> rmask)) (capCap c') else if case c' of capability.Zombie v0 v1 v2 \<Rightarrow> True | _ \<Rightarrow> False then c' else undefined) = capability.ArchObjectCap a' proof (prove)
goal (1 subgoal):
 1. \<And>x12 a'. \<lbrakk>c = cap.ArchObjectCap x12; acap_relation x12 a'; c' = capability.ArchObjectCap a'\<rbrakk> \<Longrightarrow> \<exists>a'a. acap_relation (acap_rights_update (acap_rights x12 \<inter> rmask) x12) a'a \<and> Arch.maskCapRights (CapRights (AllowWrite \<in> rmask) (AllowRead \<in> rmask) (AllowGrant \<in> rmask) (AllowGrantReply \<in> rmask)) a' = capability.ArchObjectCap a'a