theory CNodeInv_R

lemma cap_revoke_mdb_stuff1:
  "\<lbrakk> (s, s') \<in> state_relation; cte_wp_at ((=) cap) p s;
     cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s';
     cap \<noteq> cap.NullCap; cteCap cte \<noteq> NullCap \<rbrakk>
     \<Longrightarrow> (descendants_of p (cdt s) = {})
          = (\<not> (mdbNext (cteMDBNode cte) \<noteq> nullPointer
             \<and> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'))" apply (subst descendants_of_empty_state_relation) apply assumption apply (clarsimp elim!: cte_wp_at_weakenE) apply (simp add: descendants_of'_def) apply safe apply (drule spec[where x="mdbNext (cteMDBNode cte)"]) apply (erule notE, rule subtree.direct_parent) apply (clarsimp simp: mdb_next_unfold cte_wp_at_ctes_of) apply (simp add: nullPointer_def) apply (clarsimp simp: parentOf_def cte_wp_at_ctes_of) apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule(1) subtree_first_step) apply clarsimp apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule(1) subtree_first_step) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (descendants_of p (cdt s) = {}) = (\<not> (mdbNext (cteMDBNode cte) \<noteq> nullPointer \<and> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s')) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (s, ?s') \<in> state_relation
 2. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 3. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (descendants_of' (cte_map p) (ctes_of ?s') = {}) = (\<not> (mdbNext (cteMDBNode cte) \<noteq> nullPointer \<and> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (descendants_of' (cte_map p) (ctes_of s') = {}) = (\<not> (mdbNext (cteMDBNode cte) \<noteq> nullPointer \<and> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (descendants_of' (cte_map p) (ctes_of s') = {}) = (\<not> (mdbNext (cteMDBNode cte) \<noteq> nullPointer \<and> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (\<forall>x. \<not> ctes_of s' \<turnstile> cte_map p \<rightarrow> x) = (mdbNext (cteMDBNode cte) = nullPointer \<or> \<not> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; \<forall>x. \<not> ctes_of s' \<turnstile> cte_map p \<rightarrow> x; mdbNext (cteMDBNode cte) \<noteq> nullPointer; cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; \<not> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; mdbNext (cteMDBNode cte) \<noteq> nullPointer; cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'; \<not> ctes_of s' \<turnstile> cte_map p \<rightarrow> mdbNext (cteMDBNode cte)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; \<not> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; mdbNext (cteMDBNode cte) \<noteq> nullPointer; cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map p \<leadsto> mdbNext (cteMDBNode cte)
 2. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; mdbNext (cteMDBNode cte) \<noteq> nullPointer; cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0
 3. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; mdbNext (cteMDBNode cte) \<noteq> nullPointer; cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map p parentOf mdbNext (cteMDBNode cte)
 4. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> False
 5. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; \<not> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; mdbNext (cteMDBNode cte) \<noteq> nullPointer; cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0
 2. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; mdbNext (cteMDBNode cte) \<noteq> nullPointer; cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map p parentOf mdbNext (cteMDBNode cte)
 3. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> False
 4. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; \<not> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; mdbNext (cteMDBNode cte) \<noteq> nullPointer; cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map p parentOf mdbNext (cteMDBNode cte)
 2. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; \<not> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; \<not> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some cte; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; \<not> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; mdbNext (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) \<noteq> nullPointer \<and> (\<exists>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte' \<and> isMDBParentOf cte cte')\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; \<not> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; \<not> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some cte; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; \<forall>ctea. ctes_of s' (mdbNext (cteMDBNode cte)) = Some ctea \<longrightarrow> \<not> isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; invs s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; ctes_of s' \<turnstile> cte_map p \<rightarrow> x; \<forall>ctea. ctes_of s' (mdbNext (cteMDBNode cte)) = Some ctea \<longrightarrow> \<not> isMDBParentOf cte ctea; mdbNext (cteMDBNode cte) \<noteq> nullPointer \<and> (\<exists>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte' \<and> isMDBParentOf cte cte')\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!