theory ArchFinalise_AI

lemma final_cap_pd_slot_eq:
  "\<lbrakk>is_final_cap' (ArchObjectCap (PageDirectoryCap p asid)) s;
    cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s;
    cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s\<rbrakk>
  \<Longrightarrow> slot' = slot" apply (clarsimp simp:is_final_cap'_def2) apply (case_tac "(a,b) = slot'") apply (case_tac "(a,b) = slot") apply simp apply (erule_tac x="fst slot" in allE) apply (erule_tac x="snd slot" in allE) apply (clarsimp simp: gen_obj_refs_def cap_irqs_def cte_wp_at_def) apply (erule_tac x="fst slot'" in allE) apply (erule_tac x="snd slot'" in allE) apply (clarsimp simp: gen_obj_refs_def cap_irqs_def cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_final_cap' (ArchObjectCap (PageDirectoryCap p asid)) s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s\<rbrakk> \<Longrightarrow> slot' = slot proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<and> ba = b)\<rbrakk> \<Longrightarrow> slot' = slot proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<and> ba = b); (a, b) = slot'\<rbrakk> \<Longrightarrow> slot' = slot
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<and> ba = b); (a, b) \<noteq> slot'\<rbrakk> \<Longrightarrow> slot' = slot proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<and> ba = b); (a, b) = slot'; (a, b) = slot\<rbrakk> \<Longrightarrow> slot' = slot
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<and> ba = b); (a, b) = slot'; (a, b) \<noteq> slot\<rbrakk> \<Longrightarrow> slot' = slot
 3. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<and> ba = b); (a, b) \<noteq> slot'\<rbrakk> \<Longrightarrow> slot' = slot proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<and> ba = b); (a, b) = slot'; (a, b) \<noteq> slot\<rbrakk> \<Longrightarrow> slot' = slot
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<and> ba = b); (a, b) \<noteq> slot'\<rbrakk> \<Longrightarrow> slot' = slot proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; (a, b) = slot'; (a, b) \<noteq> slot; \<forall>ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (fst slot, ba) s = (fst slot = a \<and> ba = b)\<rbrakk> \<Longrightarrow> slot' = slot
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<and> ba = b); (a, b) \<noteq> slot'\<rbrakk> \<Longrightarrow> slot' = slot proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; (a, b) = slot'; (a, b) \<noteq> slot; cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (fst slot, snd slot) s = (fst slot = a \<and> snd slot = b)\<rbrakk> \<Longrightarrow> slot' = slot
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<and> ba = b); (a, b) \<noteq> slot'\<rbrakk> \<Longrightarrow> slot' = slot proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<and> ba = b); (a, b) \<noteq> slot'\<rbrakk> \<Longrightarrow> slot' = slot proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; (a, b) \<noteq> slot'; \<forall>ba. cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (fst slot', ba) s = (fst slot' = a \<and> ba = b)\<rbrakk> \<Longrightarrow> slot' = slot proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid'))) slot s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap p asid''))) slot' s; (a, b) \<noteq> slot'; cte_wp_at (\<lambda>c. gen_obj_refs (ArchObjectCap (PageDirectoryCap p asid)) \<inter> gen_obj_refs c \<noteq> {}) (fst slot', snd slot') s = (fst slot' = a \<and> snd slot' = b)\<rbrakk> \<Longrightarrow> slot' = slot proof (prove)
goal:
No subgoals!