theory Untyped_R

lemma parent_next_prev:
  "(m \<turnstile> p \<leftarrow> mdbNext parent_node) = (p = parent \<and> mdbNext parent_node \<noteq> 0)" using parent apply - apply (rule iffI) apply (clarsimp simp add: mdb_prev_def) apply (rule conjI) apply (erule dlistEn) apply clarsimp apply simp apply clarsimp apply clarsimp apply (rule dlist_nextD0) apply (rule parent_next) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leftarrow> mdbNext parent_node = (p = parent \<and> mdbNext parent_node \<noteq> 0) proof (prove)
using this:
m parent = Some (CTE parent_cap parent_node)

goal (1 subgoal):
 1. m \<turnstile> p \<leftarrow> mdbNext parent_node = (p = parent \<and> mdbNext parent_node \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. m parent = Some (CTE parent_cap parent_node) \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext parent_node = (p = parent \<and> mdbNext parent_node \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m \<turnstile> p \<leftarrow> mdbNext parent_node\<rbrakk> \<Longrightarrow> p = parent \<and> mdbNext parent_node \<noteq> 0
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); p = parent \<and> mdbNext parent_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext parent_node proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m (mdbNext parent_node) = Some z; p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode z) = parent \<and> mdbNext parent_node \<noteq> 0
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); p = parent \<and> mdbNext parent_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext parent_node proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m (mdbNext parent_node) = Some z; p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode z) = parent
 2. \<And>z. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m (mdbNext parent_node) = Some z; p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> mdbNext parent_node \<noteq> 0
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); p = parent \<and> mdbNext parent_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext parent_node proof (prove)
goal (4 subgoals):
 1. \<And>z. \<lbrakk>m (mdbNext parent_node) = Some z; p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode (CTE parent_cap parent_node)) \<noteq> 0
 2. \<And>z cte'. \<lbrakk>m (mdbNext parent_node) = Some z; p = mdbPrev (cteMDBNode z); m (mdbNext (cteMDBNode (CTE parent_cap parent_node))) = Some cte'; mdbPrev (cteMDBNode cte') = parent\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode z) = parent
 3. \<And>z. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m (mdbNext parent_node) = Some z; p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> mdbNext parent_node \<noteq> 0
 4. \<lbrakk>m parent = Some (CTE parent_cap parent_node); p = parent \<and> mdbNext parent_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext parent_node proof (prove)
goal (3 subgoals):
 1. \<And>z cte'. \<lbrakk>m (mdbNext parent_node) = Some z; p = mdbPrev (cteMDBNode z); m (mdbNext (cteMDBNode (CTE parent_cap parent_node))) = Some cte'; mdbPrev (cteMDBNode cte') = parent\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode z) = parent
 2. \<And>z. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m (mdbNext parent_node) = Some z; p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> mdbNext parent_node \<noteq> 0
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); p = parent \<and> mdbNext parent_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext parent_node proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m (mdbNext parent_node) = Some z; p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> mdbNext parent_node \<noteq> 0
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); p = parent \<and> mdbNext parent_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext parent_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); p = parent \<and> mdbNext parent_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext parent_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); p = parent; mdbNext parent_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leftarrow> mdbNext parent_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); p = parent; mdbNext parent_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto> mdbNext parent_node
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); p = parent; mdbNext parent_node \<noteq> 0\<rbrakk> \<Longrightarrow> mdbNext parent_node \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); p = parent; mdbNext parent_node \<noteq> 0\<rbrakk> \<Longrightarrow> mdbNext parent_node \<noteq> 0 proof (prove)
goal:
No subgoals!