theory ArchCSpace_AI

lemma is_derived_cap_asid_issues:
  "is_derived m p cap cap'
      \<Longrightarrow> ((is_pt_cap cap \<or> is_pd_cap cap) \<longrightarrow> cap_asid cap \<noteq> None)
             \<and> (is_pg_cap cap \<or> (vs_cap_ref cap = vs_cap_ref cap'))" unfolding is_derived_def apply (cases "is_derived_arch cap cap'") apply (erule is_derived_cap_arch_asid_issues) apply (clarsimp split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m p cap cap' \<Longrightarrow> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None) \<and> (is_pg_cap cap \<or> vs_cap_ref cap = vs_cap_ref cap') proof (prove)
goal (1 subgoal):
 1. cap \<noteq> NullCap \<and> \<not> is_zombie cap' \<and> cap \<noteq> IRQControlCap \<and> (if is_untyped_cap cap' then cap_master_cap cap' = cap_master_cap cap \<and> descendants_of p m = {} else cap_master_cap cap' = cap_master_cap cap \<and> (cap_badge cap', cap_badge cap) \<in> capBadge_ordering False) \<and> is_master_reply_cap cap' = is_reply_cap cap \<and> is_derived_arch cap cap' \<and> \<not> is_reply_cap cap' \<and> \<not> is_master_reply_cap cap \<Longrightarrow> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None) \<and> (is_pg_cap cap \<or> vs_cap_ref cap = vs_cap_ref cap') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap \<noteq> NullCap \<and> \<not> is_zombie cap' \<and> cap \<noteq> IRQControlCap \<and> (if is_untyped_cap cap' then cap_master_cap cap' = cap_master_cap cap \<and> descendants_of p m = {} else cap_master_cap cap' = cap_master_cap cap \<and> (cap_badge cap', cap_badge cap) \<in> capBadge_ordering False) \<and> is_master_reply_cap cap' = is_reply_cap cap \<and> is_derived_arch cap cap' \<and> \<not> is_reply_cap cap' \<and> \<not> is_master_reply_cap cap; is_derived_arch cap cap'\<rbrakk> \<Longrightarrow> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None) \<and> (is_pg_cap cap \<or> vs_cap_ref cap = vs_cap_ref cap')
 2. \<lbrakk>cap \<noteq> NullCap \<and> \<not> is_zombie cap' \<and> cap \<noteq> IRQControlCap \<and> (if is_untyped_cap cap' then cap_master_cap cap' = cap_master_cap cap \<and> descendants_of p m = {} else cap_master_cap cap' = cap_master_cap cap \<and> (cap_badge cap', cap_badge cap) \<in> capBadge_ordering False) \<and> is_master_reply_cap cap' = is_reply_cap cap \<and> is_derived_arch cap cap' \<and> \<not> is_reply_cap cap' \<and> \<not> is_master_reply_cap cap; \<not> is_derived_arch cap cap'\<rbrakk> \<Longrightarrow> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None) \<and> (is_pg_cap cap \<or> vs_cap_ref cap = vs_cap_ref cap') proof (prove)
goal (2 subgoals):
 1. cap \<noteq> NullCap \<and> \<not> is_zombie cap' \<and> cap \<noteq> IRQControlCap \<and> (if is_untyped_cap cap' then cap_master_cap cap' = cap_master_cap cap \<and> descendants_of p m = {} else cap_master_cap cap' = cap_master_cap cap \<and> (cap_badge cap', cap_badge cap) \<in> capBadge_ordering False) \<and> is_master_reply_cap cap' = is_reply_cap cap \<and> is_derived_arch cap cap' \<and> \<not> is_reply_cap cap' \<and> \<not> is_master_reply_cap cap \<Longrightarrow> cap_master_cap cap = cap_master_cap cap'
 2. \<lbrakk>cap \<noteq> NullCap \<and> \<not> is_zombie cap' \<and> cap \<noteq> IRQControlCap \<and> (if is_untyped_cap cap' then cap_master_cap cap' = cap_master_cap cap \<and> descendants_of p m = {} else cap_master_cap cap' = cap_master_cap cap \<and> (cap_badge cap', cap_badge cap) \<in> capBadge_ordering False) \<and> is_master_reply_cap cap' = is_reply_cap cap \<and> is_derived_arch cap cap' \<and> \<not> is_reply_cap cap' \<and> \<not> is_master_reply_cap cap; \<not> is_derived_arch cap cap'\<rbrakk> \<Longrightarrow> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None) \<and> (is_pg_cap cap \<or> vs_cap_ref cap = vs_cap_ref cap') proof (prove)
goal:
No subgoals!