theory ArchCSpace_AI

lemma is_derived_is_cap:
  "is_derived m p cap cap' \<Longrightarrow>
    (is_pg_cap cap = is_pg_cap cap')
  \<and> (is_pt_cap cap = is_pt_cap cap')
  \<and> (is_pd_cap cap = is_pd_cap cap')
  \<and> (is_ep_cap cap = is_ep_cap cap')
  \<and> (is_ntfn_cap cap = is_ntfn_cap cap')
  \<and> (is_cnode_cap cap = is_cnode_cap cap')
  \<and> (is_thread_cap cap = is_thread_cap cap')
  \<and> (is_zombie cap = is_zombie cap')
  \<and> (is_arch_cap cap = is_arch_cap cap')
  \<and> (cap_is_device cap = cap_is_device cap')" apply (clarsimp simp: is_derived_def is_derived_arch_def split: if_split_asm) by (clarsimp simp: cap_master_cap_def is_cap_simps
              split: cap.splits arch_cap.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m p cap cap' \<Longrightarrow> is_pg_cap cap = is_pg_cap cap' \<and> is_pt_cap cap = is_pt_cap cap' \<and> is_pd_cap cap = is_pd_cap cap' \<and> is_ep_cap cap = is_ep_cap cap' \<and> is_ntfn_cap cap = is_ntfn_cap cap' \<and> is_cnode_cap cap = is_cnode_cap cap' \<and> is_thread_cap cap = is_thread_cap cap' \<and> is_zombie cap = is_zombie cap' \<and> is_arch_cap cap = is_arch_cap cap' \<and> cap_is_device cap = cap_is_device cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_untyped_cap cap'; cap \<noteq> NullCap; \<not> is_zombie cap'; cap \<noteq> IRQControlCap; cap_master_cap cap' = cap_master_cap cap; descendants_of p m = {}; is_master_reply_cap cap' = is_reply_cap cap; is_pt_cap cap \<longrightarrow> cap_asid cap = cap_asid cap' \<and> (\<exists>y. cap_asid cap = Some y); is_pd_cap cap \<longrightarrow> cap_asid cap = cap_asid cap' \<and> (\<exists>y. cap_asid cap = Some y); vs_cap_ref cap = vs_cap_ref cap' \<or> is_pg_cap cap'; \<not> is_reply_cap cap'; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> is_pg_cap cap = is_pg_cap cap' \<and> is_pt_cap cap = is_pt_cap cap' \<and> is_pd_cap cap = is_pd_cap cap' \<and> is_ep_cap cap = is_ep_cap cap' \<and> is_ntfn_cap cap = is_ntfn_cap cap' \<and> is_cnode_cap cap = is_cnode_cap cap' \<and> is_thread_cap cap = is_thread_cap cap' \<and> \<not> is_zombie cap \<and> is_arch_cap cap = is_arch_cap cap' \<and> cap_is_device cap = cap_is_device cap'
 2. \<lbrakk>\<not> is_untyped_cap cap'; cap \<noteq> NullCap; \<not> is_zombie cap'; cap \<noteq> IRQControlCap; cap_master_cap cap' = cap_master_cap cap; (cap_badge cap', cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap cap' = is_reply_cap cap; is_pt_cap cap \<longrightarrow> cap_asid cap = cap_asid cap' \<and> (\<exists>y. cap_asid cap = Some y); is_pd_cap cap \<longrightarrow> cap_asid cap = cap_asid cap' \<and> (\<exists>y. cap_asid cap = Some y); vs_cap_ref cap = vs_cap_ref cap' \<or> is_pg_cap cap'; \<not> is_reply_cap cap'; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> is_pg_cap cap = is_pg_cap cap' \<and> is_pt_cap cap = is_pt_cap cap' \<and> is_pd_cap cap = is_pd_cap cap' \<and> is_ep_cap cap = is_ep_cap cap' \<and> is_ntfn_cap cap = is_ntfn_cap cap' \<and> is_cnode_cap cap = is_cnode_cap cap' \<and> is_thread_cap cap = is_thread_cap cap' \<and> \<not> is_zombie cap \<and> is_arch_cap cap = is_arch_cap cap' \<and> cap_is_device cap = cap_is_device cap'