theory ArchCSpaceInv_AI

lemma is_derived_cap_arch_asid:
  "is_derived_arch cap cap' \<Longrightarrow> cap_master_cap cap = cap_master_cap cap' \<Longrightarrow>
      is_pt_cap cap' \<or> is_pd_cap cap' \<Longrightarrow> cap_asid cap = cap_asid cap'" unfolding is_derived_arch_def apply (cases cap; cases cap'; simp) by (auto simp: is_cap_simps cap_master_cap_def split: arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_derived_arch cap cap'; cap_master_cap cap = cap_master_cap cap'; is_pt_cap cap' \<or> is_pd_cap cap'\<rbrakk> \<Longrightarrow> cap_asid cap = cap_asid cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = cap_asid cap' \<and> cap_asid cap \<noteq> None) \<and> (vs_cap_ref cap = vs_cap_ref cap' \<or> is_pg_cap cap'); cap_master_cap cap = cap_master_cap cap'; is_pt_cap cap' \<or> is_pd_cap cap'\<rbrakk> \<Longrightarrow> cap_asid cap = cap_asid cap' proof (prove)
goal (23 subgoals):
 1. \<And>x12. \<lbrakk>\<not> is_pt_cap NullCap \<and> \<not> is_pd_cap NullCap \<and> (vs_cap_ref NullCap = vs_cap_ref (ArchObjectCap x12) \<or> is_pg_cap (ArchObjectCap x12)); cap_master_cap NullCap = cap_master_cap (ArchObjectCap x12); is_pt_cap (ArchObjectCap x12) \<or> is_pd_cap (ArchObjectCap x12); cap = NullCap; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> None = cap_asid (ArchObjectCap x12)
 2. \<And>x21 x22 x23 x24 x12. \<lbrakk>\<not> is_pt_cap (UntypedCap x21 x22 x23 x24) \<and> \<not> is_pd_cap (UntypedCap x21 x22 x23 x24) \<and> (vs_cap_ref (UntypedCap x21 x22 x23 x24) = vs_cap_ref (ArchObjectCap x12) \<or> is_pg_cap (ArchObjectCap x12)); cap_master_cap (UntypedCap x21 x22 x23 x24) = cap_master_cap (ArchObjectCap x12); is_pt_cap (ArchObjectCap x12) \<or> is_pd_cap (ArchObjectCap x12); cap = UntypedCap x21 x22 x23 x24; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> None = cap_asid (ArchObjectCap x12)
 3. \<And>x31 x32 x33 x12. \<lbrakk>\<not> is_pt_cap (EndpointCap x31 x32 x33) \<and> \<not> is_pd_cap (EndpointCap x31 x32 x33) \<and> (vs_cap_ref (EndpointCap x31 x32 x33) = vs_cap_ref (ArchObjectCap x12) \<or> is_pg_cap (ArchObjectCap x12)); cap_master_cap (EndpointCap x31 x32 x33) = cap_master_cap (ArchObjectCap x12); is_pt_cap (ArchObjectCap x12) \<or> is_pd_cap (ArchObjectCap x12); cap = EndpointCap x31 x32 x33; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> None = cap_asid (ArchObjectCap x12)
 4. \<And>x41 x42 x43 x12. \<lbrakk>\<not> is_pt_cap (NotificationCap x41 x42 x43) \<and> \<not> is_pd_cap (NotificationCap x41 x42 x43) \<and> (vs_cap_ref (NotificationCap x41 x42 x43) = vs_cap_ref (ArchObjectCap x12) \<or> is_pg_cap (ArchObjectCap x12)); cap_master_cap (NotificationCap x41 x42 x43) = cap_master_cap (ArchObjectCap x12); is_pt_cap (ArchObjectCap x12) \<or> is_pd_cap (ArchObjectCap x12); cap = NotificationCap x41 x42 x43; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> None = cap_asid (ArchObjectCap x12)
 5. \<And>x51 x52 x53 x12. \<lbrakk>\<not> is_pt_cap (ReplyCap x51 x52 x53) \<and> \<not> is_pd_cap (ReplyCap x51 x52 x53) \<and> (vs_cap_ref (ReplyCap x51 x52 x53) = vs_cap_ref (ArchObjectCap x12) \<or> is_pg_cap (ArchObjectCap x12)); cap_master_cap (ReplyCap x51 x52 x53) = cap_master_cap (ArchObjectCap x12); is_pt_cap (ArchObjectCap x12) \<or> is_pd_cap (ArchObjectCap x12); cap = ReplyCap x51 x52 x53; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> None = cap_asid (ArchObjectCap x12)
 6. \<And>x61 x62 x63 x12. \<lbrakk>\<not> is_pt_cap (CNodeCap x61 x62 x63) \<and> \<not> is_pd_cap (CNodeCap x61 x62 x63) \<and> (vs_cap_ref (CNodeCap x61 x62 x63) = vs_cap_ref (ArchObjectCap x12) \<or> is_pg_cap (ArchObjectCap x12)); cap_master_cap (CNodeCap x61 x62 x63) = cap_master_cap (ArchObjectCap x12); is_pt_cap (ArchObjectCap x12) \<or> is_pd_cap (ArchObjectCap x12); cap = CNodeCap x61 x62 x63; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> None = cap_asid (ArchObjectCap x12)
 7. \<And>x7 x12. \<lbrakk>\<not> is_pt_cap (ThreadCap x7) \<and> \<not> is_pd_cap (ThreadCap x7) \<and> (vs_cap_ref (ThreadCap x7) = vs_cap_ref (ArchObjectCap x12) \<or> is_pg_cap (ArchObjectCap x12)); cap_master_cap (ThreadCap x7) = cap_master_cap (ArchObjectCap x12); is_pt_cap (ArchObjectCap x12) \<or> is_pd_cap (ArchObjectCap x12); cap = ThreadCap x7; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> None = cap_asid (ArchObjectCap x12)
 8. \<And>x12. \<lbrakk>\<not> is_pt_cap DomainCap \<and> \<not> is_pd_cap DomainCap \<and> (vs_cap_ref DomainCap = vs_cap_ref (ArchObjectCap x12) \<or> is_pg_cap (ArchObjectCap x12)); cap_master_cap DomainCap = cap_master_cap (ArchObjectCap x12); is_pt_cap (ArchObjectCap x12) \<or> is_pd_cap (ArchObjectCap x12); cap = DomainCap; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> None = cap_asid (ArchObjectCap x12)
 9. \<And>x12. \<lbrakk>\<not> is_pt_cap IRQControlCap \<and> \<not> is_pd_cap IRQControlCap \<and> (vs_cap_ref IRQControlCap = vs_cap_ref (ArchObjectCap x12) \<or> is_pg_cap (ArchObjectCap x12)); cap_master_cap IRQControlCap = cap_master_cap (ArchObjectCap x12); is_pt_cap (ArchObjectCap x12) \<or> is_pd_cap (ArchObjectCap x12); cap = IRQControlCap; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> None = cap_asid (ArchObjectCap x12)
 10. \<And>x10 x12. \<lbrakk>\<not> is_pt_cap (IRQHandlerCap x10) \<and> \<not> is_pd_cap (IRQHandlerCap x10) \<and> (vs_cap_ref (IRQHandlerCap x10) = vs_cap_ref (ArchObjectCap x12) \<or> is_pg_cap (ArchObjectCap x12)); cap_master_cap (IRQHandlerCap x10) = cap_master_cap (ArchObjectCap x12); is_pt_cap (ArchObjectCap x12) \<or> is_pd_cap (ArchObjectCap x12); cap = IRQHandlerCap x10; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> None = cap_asid (ArchObjectCap x12)
A total of 23 subgoals...