theory Untyped_R

lemma valid_nullcaps_n' [simp]:
  "valid_nullcaps n'" using nullcaps is_untyped c'_not_Null apply (clarsimp simp: valid_nullcaps_def n'_def n modify_map_if new_site_def
                        new_parent_def isCap_simps) apply (erule allE)+ apply (erule (1) impE) apply (simp add: nullMDBNode_def) apply (insert parent) apply (rule dlistEn, rule parent) apply clarsimp apply (clarsimp simp: nullPointer_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_nullcaps n' proof (prove)
using this:
valid_nullcaps m
isUntypedCap parent_cap
c' \<noteq> capability.NullCap

goal (1 subgoal):
 1. valid_nullcaps n' proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f node. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; c' \<noteq> capability.NullCap; parent_cap = capability.UntypedCap d v0 v1 f; m (mdbNext parent_node) = Some (CTE capability.NullCap node)\<rbrakk> \<Longrightarrow> mdbPrev_update (\<lambda>a. site) node = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f node. \<lbrakk>c' \<noteq> capability.NullCap; parent_cap = capability.UntypedCap d v0 v1 f; m (mdbNext parent_node) = Some (CTE capability.NullCap node); m (?p45 d v0 v1 f node) = Some (CTE capability.NullCap (?n47 d v0 v1 f node)) \<longrightarrow> ?n47 d v0 v1 f node = nullMDBNode\<rbrakk> \<Longrightarrow> mdbPrev_update (\<lambda>a. site) node = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f node. \<lbrakk>c' \<noteq> capability.NullCap; parent_cap = capability.UntypedCap d v0 v1 f; m (mdbNext parent_node) = Some (CTE capability.NullCap node); node = nullMDBNode\<rbrakk> \<Longrightarrow> mdbPrev_update (\<lambda>a. site) node = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f node. \<lbrakk>c' \<noteq> capability.NullCap; parent_cap = capability.UntypedCap d v0 v1 f; m (mdbNext parent_node) = Some (CTE capability.NullCap (MDB nullPointer nullPointer False False)); node = MDB nullPointer nullPointer False False\<rbrakk> \<Longrightarrow> site = nullPointer proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f node. \<lbrakk>c' \<noteq> capability.NullCap; parent_cap = capability.UntypedCap d v0 v1 f; m (mdbNext parent_node) = Some (CTE capability.NullCap (MDB nullPointer nullPointer False False)); node = MDB nullPointer nullPointer False False; m parent = Some (CTE parent_cap parent_node)\<rbrakk> \<Longrightarrow> site = nullPointer proof (prove)
goal (2 subgoals):
 1. \<And>d v0 v1 f node. \<lbrakk>c' \<noteq> capability.NullCap; parent_cap = capability.UntypedCap d v0 v1 f; m (mdbNext parent_node) = Some (CTE capability.NullCap (MDB nullPointer nullPointer False False)); node = MDB nullPointer nullPointer False False; m parent = Some (CTE parent_cap parent_node)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode (CTE parent_cap parent_node)) \<noteq> 0
 2. \<And>d v0 v1 f node cte'. \<lbrakk>c' \<noteq> capability.NullCap; parent_cap = capability.UntypedCap d v0 v1 f; m (mdbNext parent_node) = Some (CTE capability.NullCap (MDB nullPointer nullPointer False False)); node = MDB nullPointer nullPointer False False; m parent = Some (CTE parent_cap parent_node); m (mdbNext (cteMDBNode (CTE parent_cap parent_node))) = Some cte'; mdbPrev (cteMDBNode cte') = parent\<rbrakk> \<Longrightarrow> site = nullPointer proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f node cte'. \<lbrakk>c' \<noteq> capability.NullCap; parent_cap = capability.UntypedCap d v0 v1 f; m (mdbNext parent_node) = Some (CTE capability.NullCap (MDB nullPointer nullPointer False False)); node = MDB nullPointer nullPointer False False; m parent = Some (CTE parent_cap parent_node); m (mdbNext (cteMDBNode (CTE parent_cap parent_node))) = Some cte'; mdbPrev (cteMDBNode cte') = parent\<rbrakk> \<Longrightarrow> site = nullPointer proof (prove)
goal:
No subgoals!