theory CNodeInv_R

lemma neg_next_trancl_xp:
  assumes node: "m ptr' = Some (CTE cap node)"
  and      dom: "mdbPrev node \<in> dom m"
  and      no0: "no_0 m"
  and       vd: "valid_dlist m"
  and       nl: "\<not> m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'"
  shows "\<not> m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node" using nl proof (rule contrapos_nn) assume "m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node" show "m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'" proof (rule trancl_into_trancl) have "mdbPrev node \<noteq> 0" using assms by auto thus "m \<turnstile> mdbPrev node \<leadsto> ptr'" using vd node apply - apply (erule (1) valid_dlistEp) apply simp apply (rule next_fold) apply simp apply simp done qed fact+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ptr, mdbPrev node) \<notin> (mdb_next_rel m)\<^sup>+ proof (prove)
using this:
(ptr, ptr') \<notin> (mdb_next_rel m)\<^sup>+

goal (1 subgoal):
 1. (ptr, mdbPrev node) \<notin> (mdb_next_rel m)\<^sup>+ proof (state)
goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>+ ptr' proof (state)
this:
m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node

goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>+ ptr' proof (prove)
goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto>\<^sup>+ ptr' proof (state)
goal (2 subgoals):
 1. m \<turnstile> ptr \<leadsto>\<^sup>+ ?b
 2. m \<turnstile> ?b \<leadsto> ptr' proof (prove)
goal (1 subgoal):
 1. mdbPrev node \<noteq> 0 proof (prove)
using this:
m ptr' = Some (CTE cap node)
mdbPrev node \<in> dom m
no_0 m
valid_dlist m
(ptr, ptr') \<notin> (mdb_next_rel m)\<^sup>+

goal (1 subgoal):
 1. mdbPrev node \<noteq> 0 proof (state)
this:
mdbPrev node \<noteq> 0

goal (2 subgoals):
 1. m \<turnstile> ptr \<leadsto>\<^sup>+ ?b
 2. m \<turnstile> ?b \<leadsto> ptr' proof (prove)
using this:
mdbPrev node \<noteq> 0

goal (1 subgoal):
 1. m \<turnstile> mdbPrev node \<leadsto> ptr' proof (prove)
using this:
mdbPrev node \<noteq> 0
valid_dlist m
m ptr' = Some (CTE cap node)

goal (1 subgoal):
 1. m \<turnstile> mdbPrev node \<leadsto> ptr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev node \<noteq> 0; valid_dlist m; m ptr' = Some (CTE cap node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev node \<leadsto> ptr' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbPrev node \<noteq> 0; m ptr' = Some (CTE cap node)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (CTE cap node)) \<noteq> 0
 2. \<And>cte'. \<lbrakk>mdbPrev node \<noteq> 0; m ptr' = Some (CTE cap node); m (mdbPrev (cteMDBNode (CTE cap node))) = Some cte'; mdbNext (cteMDBNode cte') = ptr'\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev node \<leadsto> ptr' proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdbPrev node \<noteq> 0; m ptr' = Some (CTE cap node); m (mdbPrev (cteMDBNode (CTE cap node))) = Some cte'; mdbNext (cteMDBNode cte') = ptr'\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev node \<leadsto> ptr' proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>mdbPrev node \<noteq> 0; m ptr' = Some (CTE cap node); m (mdbPrev (cteMDBNode (CTE cap node))) = Some cte'; mdbNext (cteMDBNode cte') = ptr'\<rbrakk> \<Longrightarrow> m (mdbPrev node) = Some (?cte7 cte')
 2. \<And>cte'. \<lbrakk>mdbPrev node \<noteq> 0; m ptr' = Some (CTE cap node); m (mdbPrev (cteMDBNode (CTE cap node))) = Some cte'; mdbNext (cteMDBNode cte') = ptr'\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode (?cte7 cte')) = ptr' proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdbPrev node \<noteq> 0; m ptr' = Some (CTE cap node); m (mdbPrev (cteMDBNode (CTE cap node))) = Some cte'; mdbNext (cteMDBNode cte') = ptr'\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte') = ptr' proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> mdbPrev node \<leadsto> ptr'

goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node proof (state)
this:
m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'

goal:
No subgoals!