theory CNodeInv_R

lemma no_next_prev_rtrancl:
  assumes  c0: "valid_mdb_ctes m"
  and src: "m src = Some (CTE cap src_node)"
  and "mdbPrev src_node \<noteq> 0"
  shows   "\<not> m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* mdbPrev src_node" proof assume asm: "m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* mdbPrev src_node" from c0 have n0: "no_0 m" .. from c0 have chain: "mdb_chain_0 m" .. have  "m \<turnstile> src \<leadsto>\<^sup>+ mdbPrev src_node" using src by - (rule rtrancl_into_trancl2 [OF _ asm], clarsimp simp: next_unfold') moreover from c0 have vd: "valid_dlist m" .. have "m \<turnstile> mdbPrev src_node \<leadsto> src" by (rule prev_leadstoI [OF _ _ vd]) fact+ ultimately have "m \<turnstile> src \<leadsto>\<^sup>+ src" .. thus False using mdb_chain_0_no_loops [OF chain n0] by (simp add: no_loops_trancl_simp) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbNext src_node, mdbPrev src_node) \<notin> (mdb_next_rel m)\<^sup>* proof (state)
goal (1 subgoal):
 1. m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* mdbPrev src_node \<Longrightarrow> False proof (state)
this:
m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* mdbPrev src_node

goal (1 subgoal):
 1. m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* mdbPrev src_node \<Longrightarrow> False proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. no_0 m proof (state)
this:
no_0 m

goal (1 subgoal):
 1. m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* mdbPrev src_node \<Longrightarrow> False proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. mdb_chain_0 m proof (state)
this:
mdb_chain_0 m

goal (1 subgoal):
 1. m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* mdbPrev src_node \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> src \<leadsto>\<^sup>+ mdbPrev src_node proof (prove)
using this:
m src = Some (CTE cap src_node)

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

goal (1 subgoal):
 1. m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* mdbPrev src_node \<Longrightarrow> False proof (state)
this:
m \<turnstile> src \<leadsto>\<^sup>+ mdbPrev src_node

goal (1 subgoal):
 1. m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* mdbPrev src_node \<Longrightarrow> False proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. valid_dlist m proof (state)
this:
valid_dlist m

goal (1 subgoal):
 1. m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* mdbPrev src_node \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> mdbPrev src_node \<leadsto> src proof (state)
this:
m \<turnstile> mdbPrev src_node \<leadsto> src

goal (1 subgoal):
 1. m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* mdbPrev src_node \<Longrightarrow> False proof (chain)
picking this:
m \<turnstile> src \<leadsto>\<^sup>+ mdbPrev src_node
m \<turnstile> mdbPrev src_node \<leadsto> src proof (prove)
using this:
m \<turnstile> src \<leadsto>\<^sup>+ mdbPrev src_node
m \<turnstile> mdbPrev src_node \<leadsto> src

goal (1 subgoal):
 1. m \<turnstile> src \<leadsto>\<^sup>+ src proof (state)
this:
m \<turnstile> src \<leadsto>\<^sup>+ src

goal (1 subgoal):
 1. m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* mdbPrev src_node \<Longrightarrow> False proof (prove)
using this:
m \<turnstile> src \<leadsto>\<^sup>+ src

goal (1 subgoal):
 1. False proof (prove)
using this:
m \<turnstile> src \<leadsto>\<^sup>+ src
no_loops m

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals!