theory ADT_H

lemma absIsOriginalCap_correct:
assumes valid_ioc: "valid_ioc s"
assumes valid_objs: "valid_objs s"
assumes rel: "(s,s') \<in> state_relation"
assumes pspace_aligned: "pspace_aligned s"
assumes pspace_distinct: "pspace_distinct s"
assumes pspace_aligned': "pspace_aligned' s'"
assumes pspace_distinct': "pspace_distinct' s'"
shows
  "absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s" proof - from valid_ioc have no_cap_not_orig:
    "\<forall>p. caps_of_state s p = None \<longrightarrow> is_original_cap s p = False"
  and null_cap_not_orig:
    "\<forall>p. caps_of_state s p = Some cap.NullCap \<longrightarrow> is_original_cap s p = False" by (fastforce simp: valid_ioc_def2 null_filter_def)+ have cnp:
  "\<forall>a b. caps_of_state s (a, b) \<noteq> None \<longrightarrow>
         (cteMap (gsCNodes s')) (cte_map (a, b)) = (a, b)" using cteMap_correct[OF rel valid_objs pspace_aligned pspace_distinct
                            pspace_aligned' pspace_distinct'] by (clarsimp simp: dom_def) show ?thesis apply (subgoal_tac "revokable_relation (is_original_cap s)
                          (null_filter (caps_of_state s)) (ctes_of s') \<and>
                        pspace_relation (kheap s) (ksPSpace s')") prefer 2 using rel apply (clarsimp simp add: state_relation_def) apply (rule ext) apply (clarsimp simp add: revokable_relation_def
                              null_filter_def absIsOriginalCap_def
                       split: if_split_asm) apply (erule_tac x=a in allE) apply (erule_tac x=b in allE) apply (case_tac "caps_of_state s (a, b)") apply (clarsimp simp: no_cap_not_orig) apply (frule (1) pspace_relation_cte_wp_atI[OF _ _ valid_objs]) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (subgoal_tac "(a,b) = (aa,ba)", simp) apply (cut_tac a=aa and b=ba in cnp[rule_format], simp) apply (simp add: cte_map_def) apply simp apply (case_tac "aa = cap.NullCap") apply (clarsimp simp add: null_cap_not_orig) apply (frule (1) pspace_relation_ctes_ofI
              [OF _ caps_of_state_cteD pspace_aligned' pspace_distinct']) apply clarsimp apply (frule (1) pspace_relation_ctes_ofI
             [OF _ caps_of_state_cteD pspace_aligned' pspace_distinct']) apply (clarsimp simp add: dom_def) apply (cut_tac a=a and b=b in cnp[rule_format], simp+) apply (case_tac cte, clarsimp) apply (case_tac aa, simp_all) apply (rename_tac arch_cap) apply (case_tac arch_cap, simp_all) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s proof (state)
goal (1 subgoal):
 1. absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s proof (chain)
picking this:
valid_ioc s proof (prove)
using this:
valid_ioc s

goal (1 subgoal):
 1. \<forall>p. caps_of_state s p = None \<longrightarrow> is_original_cap s p = False &&& \<forall>p. caps_of_state s p = Some cap.NullCap \<longrightarrow> is_original_cap s p = False proof (state)
this:
\<forall>p. caps_of_state s p = None \<longrightarrow> is_original_cap s p = False
\<forall>p. caps_of_state s p = Some cap.NullCap \<longrightarrow> is_original_cap s p = False

goal (1 subgoal):
 1. absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s proof (prove)
goal (1 subgoal):
 1. \<forall>a b. caps_of_state s (a, b) \<noteq> None \<longrightarrow> cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) proof (prove)
using this:
?p \<in> dom (caps_of_state s) \<longrightarrow> cteMap (gsCNodes s') (cte_map ?p) = ?p

goal (1 subgoal):
 1. \<forall>a b. caps_of_state s (a, b) \<noteq> None \<longrightarrow> cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) proof (state)
this:
\<forall>a b. caps_of_state s (a, b) \<noteq> None \<longrightarrow> cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)

goal (1 subgoal):
 1. absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s proof (prove)
goal (1 subgoal):
 1. absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s proof (prove)
goal (2 subgoals):
 1. revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> pspace_relation (kheap s) (ksPSpace s') \<Longrightarrow> absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s
 2. revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> pspace_relation (kheap s) (ksPSpace s') proof (prove)
goal (2 subgoals):
 1. revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> pspace_relation (kheap s) (ksPSpace s')
 2. revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> pspace_relation (kheap s) (ksPSpace s') \<Longrightarrow> absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s proof (prove)
using this:
(s, s') \<in> state_relation

goal (2 subgoals):
 1. revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> pspace_relation (kheap s) (ksPSpace s')
 2. revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> pspace_relation (kheap s) (ksPSpace s') \<Longrightarrow> absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s proof (prove)
goal (1 subgoal):
 1. revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> pspace_relation (kheap s) (ksPSpace s') \<Longrightarrow> absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s proof (prove)
goal (1 subgoal):
 1. \<And>x. revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> pspace_relation (kheap s) (ksPSpace s') \<Longrightarrow> absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') x = is_original_cap s x proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. caps_of_state s (a, b) = Some cap.NullCap \<or> caps_of_state s (a, b) = None \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); \<forall>b. caps_of_state s (a, b) = Some cap.NullCap \<or> caps_of_state s (a, b) = None \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node)\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap.NullCap \<or> caps_of_state s (a, b) = None \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node)\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap.NullCap \<or> caps_of_state s (a, b) = None \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = None\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b)
 2. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap.NullCap \<or> caps_of_state s (a, b) = None \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = None; cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); ctes_of s' (cte_map (a, b)) = Some y; cteCap y \<noteq> capability.NullCap; mdbRevocable (cteMDBNode y)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap.NullCap \<or> caps_of_state s (a, b) = None \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = None; cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); ctes_of s' (cte_map (a, b)) = Some y; cteCap y \<noteq> capability.NullCap; mdbRevocable (cteMDBNode y); \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap y) \<and> cte_map (a, b) = cte_map slot\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap.NullCap \<or> caps_of_state s (a, b) = None \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b y c aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = None; cteMap (gsCNodes s') (cte_map (aa, ba)) = (a, b); ctes_of s' (cte_map (aa, ba)) = Some y; cteCap y \<noteq> capability.NullCap; mdbRevocable (cteMDBNode y); caps_of_state s (aa, ba) = Some c; cap_relation c (cteCap y); cte_map (a, b) = cte_map (aa, ba)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap.NullCap \<or> caps_of_state s (a, b) = None \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b y c aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = None; cteMap (gsCNodes s') (cte_map (aa, ba)) = (a, b); ctes_of s' (cte_map (aa, ba)) = Some y; cteCap y \<noteq> capability.NullCap; mdbRevocable (cteMDBNode y); caps_of_state s (aa, ba) = Some c; cap_relation c (cteCap y); cte_map (a, b) = cte_map (aa, ba)\<rbrakk> \<Longrightarrow> (a, b) = (aa, ba)
 2. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap.NullCap \<or> caps_of_state s (a, b) = None \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b y c aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = None; cteMap (gsCNodes s') (cte_map (aa, ba)) = (a, b); ctes_of s' (cte_map (aa, ba)) = Some y; cteCap y \<noteq> capability.NullCap; mdbRevocable (cteMDBNode y); caps_of_state s (aa, ba) = Some c; cap_relation c (cteCap y); cte_map (a, b) = cte_map (aa, ba); cteMap (gsCNodes s') (cte_map (aa, ba)) = (aa, ba)\<rbrakk> \<Longrightarrow> (a, b) = (aa, ba)
 2. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap.NullCap \<or> caps_of_state s (a, b) = None \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap.NullCap \<or> caps_of_state s (a, b) = None \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); aa = cap.NullCap \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); aa = cap.NullCap \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa; aa = cap.NullCap\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b)
 2. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); aa = cap.NullCap \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa; aa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap.NullCap; cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); ctes_of s' (cte_map (a, b)) = Some y; cteCap y \<noteq> capability.NullCap; mdbRevocable (cteMDBNode y)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); aa = cap.NullCap \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa; aa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap.NullCap; cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); ctes_of s' (cte_map (a, b)) = Some y; cteCap y \<noteq> capability.NullCap; mdbRevocable (cteMDBNode y); \<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cap_relation cap.NullCap (cteCap cte)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); aa = cap.NullCap \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa; aa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); aa = cap.NullCap \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa; aa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); aa = cap.NullCap \<or> (\<forall>cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node); caps_of_state s (a, b) = Some aa; aa \<noteq> cap.NullCap; \<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cap_relation aa (cteCap cte)\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cte_map (a, b) \<in> dom (ctes_of s') \<and> (\<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte))) = is_original_cap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa cte. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); \<forall>cap node. cte = CTE cap node \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node; caps_of_state s (a, b) = Some aa; aa \<noteq> cap.NullCap; ctes_of s' (cte_map (a, b)) = Some cte; cap_relation aa (cteCap cte)\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) \<and> cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte)) = is_original_cap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa cte. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); \<forall>cap node. cte = CTE cap node \<longrightarrow> is_original_cap s (a, b) = mdbRevocable node; caps_of_state s (a, b) = Some aa; aa \<noteq> cap.NullCap; ctes_of s' (cte_map (a, b)) = Some cte; cap_relation aa (cteCap cte); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (cteCap cte \<noteq> capability.NullCap \<and> mdbRevocable (cteMDBNode cte)) = is_original_cap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa x1 x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); is_original_cap s (a, b) = mdbRevocable x2; caps_of_state s (a, b) = Some aa; aa \<noteq> cap.NullCap; ctes_of s' (cte_map (a, b)) = Some (CTE x1 x2); cap_relation aa x1; cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (x1 \<noteq> capability.NullCap \<and> mdbRevocable x2) = mdbRevocable x2 proof (prove)
goal (1 subgoal):
 1. \<And>a b aa x1 x2 x12. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); is_original_cap s (a, b) = mdbRevocable x2; caps_of_state s (a, b) = Some (cap.ArchObjectCap x12); ctes_of s' (cte_map (a, b)) = Some (CTE x1 x2); \<exists>a'. acap_relation x12 a' \<and> x1 = capability.ArchObjectCap a'; cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); aa = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> (x1 \<noteq> capability.NullCap \<and> mdbRevocable x2) = mdbRevocable x2 proof (prove)
goal (1 subgoal):
 1. \<And>a b aa x1 x2 arch_cap. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); is_original_cap s (a, b) = mdbRevocable x2; caps_of_state s (a, b) = Some (cap.ArchObjectCap arch_cap); ctes_of s' (cte_map (a, b)) = Some (CTE x1 x2); \<exists>a'. acap_relation arch_cap a' \<and> x1 = capability.ArchObjectCap a'; cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); aa = cap.ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (x1 \<noteq> capability.NullCap \<and> mdbRevocable x2) = mdbRevocable x2 proof (prove)
goal:
No subgoals! proof (state)
this:
absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s

goal:
No subgoals!