theory CNodeInv_R

lemma (in mdb_swap) other_dest_prev_dest_src:
  fixes cte
  defines "p \<equiv> mdbPrev (cteMDBNode cte)"
  assumes dest_src: "mdbNext dest_node = src"
  and     ps: "m (mdbPrev dest_node) = Some cte"
  and     p0: "p \<noteq> 0"
  shows  "p \<noteq> mdbPrev src_node" "p \<noteq> src" "p \<noteq> mdbNext src_node"
  "p \<noteq> mdbPrev dest_node" "p \<noteq> dest" "p \<noteq> mdbNext dest_node" proof - note really_annoying_simps [simp del] = word_neq_0_conv have pp: "m \<turnstile> p \<leadsto> mdbPrev dest_node" using p0 ps unfolding p_def by (cases cte, simp) (erule (1) prev_leadstoI [OF _ _ dlist]) also have "mdbPrev dest_node \<noteq> 0" using ps no_0 by (rule no_0_neq) hence "m \<turnstile> mdbPrev dest_node \<leadsto> dest" .. finally have ps' [intro?]: "m \<turnstile> p \<leadsto>\<^sup>+ dest" . from dest_src dest have sd [intro?]: "m \<turnstile> dest \<leadsto> src" by (simp add: next_unfold') from ps' sd have pd [intro?]: "m \<turnstile> p \<leadsto>\<^sup>+ src" .. show "p \<noteq> mdbPrev dest_node" using pp by clarsimp show "p \<noteq> dest" using ps' by clarsimp show "p \<noteq> mdbNext dest_node" proof assume a: "p = mdbNext dest_node" also have "m \<turnstile> dest \<leadsto> mdbNext dest_node" .. also have "m \<turnstile> p \<leadsto>\<^sup>+ dest" .. finally show False by simp qed from dest_src have "mdbPrev src_node = dest" by simp hence s0: "mdbPrev src_node \<noteq> 0" using p_0 by (rule ssubst) have sn: "mdbNext src_node \<noteq> dest" using dest_src by (clarsimp simp: s0) show "p \<noteq> mdbPrev src_node" unfolding p_def using ps dest_src by (cases cte) (clarsimp simp: mdb_ptr_src.p_prev_qe sn s0) show "p \<noteq> src" proof assume "p = src" hence "src = p" .. also have "m \<turnstile> p \<leadsto>\<^sup>+ dest" .. also have "m \<turnstile> dest \<leadsto> src" .. finally show False by simp qed show "p \<noteq> mdbNext src_node" proof assume "p = mdbNext src_node" also have "m \<turnstile> src \<leadsto> mdbNext src_node" .. also have "m \<turnstile> p \<leadsto>\<^sup>+ dest" .. also have "m \<turnstile> dest \<leadsto> src" .. finally show False by simp qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p \<noteq> mdbPrev src_node &&& p \<noteq> src &&& p \<noteq> mdbNext src_node) &&& p \<noteq> mdbPrev dest_node &&& p \<noteq> dest &&& p \<noteq> mdbNext dest_node proof (state)
goal (6 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node
 4. p \<noteq> mdbPrev dest_node
 5. p \<noteq> dest
 6. p \<noteq> mdbNext dest_node proof (state)
this:
(?w \<noteq> 0) = (0 < ?w)

goal (6 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node
 4. p \<noteq> mdbPrev dest_node
 5. p \<noteq> dest
 6. p \<noteq> mdbNext dest_node proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leadsto> mdbPrev dest_node proof (prove)
using this:
p \<noteq> 0
m (mdbPrev dest_node) = Some cte

goal (1 subgoal):
 1. m \<turnstile> p \<leadsto> mdbPrev dest_node proof (prove)
using this:
mdbPrev (cteMDBNode cte) \<noteq> 0
m (mdbPrev dest_node) = Some cte

goal (1 subgoal):
 1. m \<turnstile> mdbPrev (cteMDBNode cte) \<leadsto> mdbPrev dest_node proof (state)
this:
m \<turnstile> p \<leadsto> mdbPrev dest_node

goal (6 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node
 4. p \<noteq> mdbPrev dest_node
 5. p \<noteq> dest
 6. p \<noteq> mdbNext dest_node proof (state)
this:
m \<turnstile> p \<leadsto> mdbPrev dest_node

goal (6 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node
 4. p \<noteq> mdbPrev dest_node
 5. p \<noteq> dest
 6. p \<noteq> mdbNext dest_node proof (prove)
goal (1 subgoal):
 1. mdbPrev dest_node \<noteq> 0 proof (prove)
using this:
m (mdbPrev dest_node) = Some cte
no_0 m

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

goal (6 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node
 4. p \<noteq> mdbPrev dest_node
 5. p \<noteq> dest
 6. p \<noteq> mdbNext dest_node proof (prove)
using this:
mdbPrev dest_node \<noteq> 0

goal (1 subgoal):
 1. m \<turnstile> mdbPrev dest_node \<leadsto> dest proof (state)
this:
m \<turnstile> mdbPrev dest_node \<leadsto> dest

goal (6 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node
 4. p \<noteq> mdbPrev dest_node
 5. p \<noteq> dest
 6. p \<noteq> mdbNext dest_node proof (chain)
picking this:
m \<turnstile> p \<leadsto>\<^sup>+ dest proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ dest

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

goal (6 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node
 4. p \<noteq> mdbPrev dest_node
 5. p \<noteq> dest
 6. p \<noteq> mdbNext dest_node proof (chain)
picking this:
mdbNext dest_node = src
m dest = Some (CTE dest_cap dest_node) proof (prove)
using this:
mdbNext dest_node = src
m dest = Some (CTE dest_cap dest_node)

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

goal (6 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node
 4. p \<noteq> mdbPrev dest_node
 5. p \<noteq> dest
 6. p \<noteq> mdbNext dest_node proof (chain)
picking this:
m \<turnstile> p \<leadsto>\<^sup>+ dest
m \<turnstile> dest \<leadsto> src proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ dest
m \<turnstile> dest \<leadsto> src

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

goal (6 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node
 4. p \<noteq> mdbPrev dest_node
 5. p \<noteq> dest
 6. p \<noteq> mdbNext dest_node proof (prove)
goal (1 subgoal):
 1. p \<noteq> mdbPrev dest_node proof (prove)
using this:
m \<turnstile> p \<leadsto> mdbPrev dest_node

goal (1 subgoal):
 1. p \<noteq> mdbPrev dest_node proof (state)
this:
p \<noteq> mdbPrev dest_node

goal (5 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node
 4. p \<noteq> dest
 5. p \<noteq> mdbNext dest_node proof (prove)
goal (1 subgoal):
 1. p \<noteq> dest proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ dest

goal (1 subgoal):
 1. p \<noteq> dest proof (state)
this:
p \<noteq> dest

goal (4 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node
 4. p \<noteq> mdbNext dest_node proof (prove)
goal (1 subgoal):
 1. p \<noteq> mdbNext dest_node proof (state)
goal (1 subgoal):
 1. p = mdbNext dest_node \<Longrightarrow> False proof (state)
this:
p = mdbNext dest_node

goal (1 subgoal):
 1. p = mdbNext dest_node \<Longrightarrow> False proof (state)
this:
p = mdbNext dest_node

goal (1 subgoal):
 1. p = mdbNext dest_node \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> dest \<leadsto> mdbNext dest_node proof (state)
this:
m \<turnstile> dest \<leadsto> mdbNext dest_node

goal (1 subgoal):
 1. p = mdbNext dest_node \<Longrightarrow> False proof (state)
this:
m \<turnstile> dest \<leadsto> mdbNext dest_node

goal (1 subgoal):
 1. p = mdbNext dest_node \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leadsto>\<^sup>+ dest proof (state)
this:
m \<turnstile> p \<leadsto>\<^sup>+ dest

goal (1 subgoal):
 1. p = mdbNext dest_node \<Longrightarrow> False proof (chain)
picking this:
m \<turnstile> dest \<leadsto>\<^sup>+ dest proof (prove)
using this:
m \<turnstile> dest \<leadsto>\<^sup>+ dest

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

goal:
No subgoals! proof (state)
this:
p \<noteq> mdbNext dest_node

goal (3 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node proof (chain)
picking this:
mdbNext dest_node = src proof (prove)
using this:
mdbNext dest_node = src

goal (1 subgoal):
 1. mdbPrev src_node = dest proof (state)
this:
mdbPrev src_node = dest

goal (3 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node proof (prove)
using this:
mdbPrev src_node = dest

goal (1 subgoal):
 1. mdbPrev src_node \<noteq> 0 proof (prove)
using this:
mdbPrev src_node = dest
dest \<noteq> 0

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

goal (3 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node proof (prove)
goal (1 subgoal):
 1. mdbNext src_node \<noteq> dest proof (prove)
using this:
mdbNext dest_node = src

goal (1 subgoal):
 1. mdbNext src_node \<noteq> dest proof (state)
this:
mdbNext src_node \<noteq> dest

goal (3 subgoals):
 1. p \<noteq> mdbPrev src_node
 2. p \<noteq> src
 3. p \<noteq> mdbNext src_node proof (prove)
goal (1 subgoal):
 1. p \<noteq> mdbPrev src_node proof (prove)
goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<noteq> mdbPrev src_node proof (prove)
using this:
m (mdbPrev dest_node) = Some cte
mdbNext dest_node = src

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<noteq> mdbPrev src_node proof (state)
this:
p \<noteq> mdbPrev src_node

goal (2 subgoals):
 1. p \<noteq> src
 2. p \<noteq> mdbNext src_node proof (prove)
goal (1 subgoal):
 1. p \<noteq> src proof (state)
goal (1 subgoal):
 1. p = src \<Longrightarrow> False proof (state)
this:
p = src

goal (1 subgoal):
 1. p = src \<Longrightarrow> False proof (prove)
using this:
p = src

goal (1 subgoal):
 1. src = p proof (state)
this:
src = p

goal (1 subgoal):
 1. p = src \<Longrightarrow> False proof (state)
this:
src = p

goal (1 subgoal):
 1. p = src \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leadsto>\<^sup>+ dest proof (state)
this:
m \<turnstile> p \<leadsto>\<^sup>+ dest

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

goal (1 subgoal):
 1. p = src \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> dest \<leadsto> src proof (state)
this:
m \<turnstile> dest \<leadsto> src

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

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

goal:
No subgoals! proof (state)
this:
p \<noteq> src

goal (1 subgoal):
 1. p \<noteq> mdbNext src_node proof (prove)
goal (1 subgoal):
 1. p \<noteq> mdbNext src_node proof (state)
goal (1 subgoal):
 1. p = mdbNext src_node \<Longrightarrow> False proof (state)
this:
p = mdbNext src_node

goal (1 subgoal):
 1. p = mdbNext src_node \<Longrightarrow> False proof (state)
this:
p = mdbNext src_node

goal (1 subgoal):
 1. p = mdbNext src_node \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> src \<leadsto> mdbNext src_node proof (state)
this:
m \<turnstile> src \<leadsto> mdbNext src_node

goal (1 subgoal):
 1. p = mdbNext src_node \<Longrightarrow> False proof (state)
this:
m \<turnstile> src \<leadsto> mdbNext src_node

goal (1 subgoal):
 1. p = mdbNext src_node \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leadsto>\<^sup>+ dest proof (state)
this:
m \<turnstile> p \<leadsto>\<^sup>+ dest

goal (1 subgoal):
 1. p = mdbNext src_node \<Longrightarrow> False proof (state)
this:
m \<turnstile> p \<leadsto>\<^sup>+ dest

goal (1 subgoal):
 1. p = mdbNext src_node \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> dest \<leadsto> src proof (state)
this:
m \<turnstile> dest \<leadsto> src

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

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

goal:
No subgoals! proof (state)
this:
p \<noteq> mdbNext src_node

goal:
No subgoals!