theory CNodeInv_R

lemma (in mdb_swap) other_src_prev_src_dest:
  fixes cte
  defines "p \<equiv> mdbPrev (cteMDBNode cte)"
  assumes src_dest: "mdbNext src_node = dest"
  and     ps: "m (mdbPrev src_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 src_node" using p0 ps unfolding p_def by (cases cte, simp) (erule (1) prev_leadstoI [OF _ _ dlist]) also have "mdbPrev src_node \<noteq> 0" using ps no_0 by (rule no_0_neq) hence "m \<turnstile> mdbPrev src_node \<leadsto> src" .. finally have ps' [intro?]: "m \<turnstile> p \<leadsto>\<^sup>+ src" . from src_dest src have sd [intro?]: "m \<turnstile> src \<leadsto> dest" by (simp add: next_unfold') from ps' sd have pd [intro?]: "m \<turnstile> p \<leadsto>\<^sup>+ dest" .. show "p \<noteq> mdbPrev src_node" using pp by clarsimp show "p \<noteq> src" using ps' by clarsimp show "p \<noteq> mdbNext src_node" proof assume a: "p = mdbNext src_node" also have "m \<turnstile> src \<leadsto> mdbNext src_node" .. also have "m \<turnstile> p \<leadsto>\<^sup>+ src" .. finally show False by simp qed from src_dest have "mdbPrev dest_node = src" by simp hence "mdbPrev dest_node \<noteq> 0" using mdb_ptr_src.p_0 by (rule ssubst) thus "p \<noteq> mdbPrev dest_node" unfolding p_def using ps src_dest by (cases cte, auto simp add: p_prev_qe) show "p \<noteq> dest" proof assume "p = dest" hence "dest = p" .. also have "m \<turnstile> p \<leadsto>\<^sup>+ src" .. also have "m \<turnstile> src \<leadsto> dest" .. finally show False by simp qed show "p \<noteq> mdbNext dest_node" proof assume "p = mdbNext dest_node" also have "m \<turnstile> dest \<leadsto> mdbNext dest_node" .. also have "m \<turnstile> p \<leadsto>\<^sup>+ src" .. also have "m \<turnstile> src \<leadsto> dest" .. 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 src_node proof (prove)
using this:
p \<noteq> 0
m (mdbPrev src_node) = Some cte

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

goal (1 subgoal):
 1. m \<turnstile> mdbPrev (cteMDBNode cte) \<leadsto> mdbPrev src_node proof (state)
this:
m \<turnstile> p \<leadsto> mdbPrev src_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 src_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 src_node \<noteq> 0 proof (prove)
using this:
m (mdbPrev src_node) = Some cte
no_0 m

goal (1 subgoal):
 1. mdbPrev src_node \<noteq> 0 proof (state)
this:
mdbPrev src_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 src_node \<noteq> 0

goal (1 subgoal):
 1. m \<turnstile> mdbPrev src_node \<leadsto> src proof (state)
this:
m \<turnstile> mdbPrev src_node \<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>+ src proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ 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 (chain)
picking this:
mdbNext src_node = dest
m src = Some (CTE src_cap src_node) proof (prove)
using this:
mdbNext src_node = dest
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. m \<turnstile> src \<leadsto> dest proof (state)
this:
m \<turnstile> src \<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>+ src
m \<turnstile> src \<leadsto> dest proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ src
m \<turnstile> src \<leadsto> 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 (prove)
goal (1 subgoal):
 1. p \<noteq> mdbPrev src_node proof (prove)
using this:
m \<turnstile> p \<leadsto> mdbPrev src_node

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

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

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

goal (4 subgoals):
 1. p \<noteq> mdbNext src_node
 2. p \<noteq> mdbPrev dest_node
 3. p \<noteq> dest
 4. p \<noteq> mdbNext dest_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>+ src proof (state)
this:
m \<turnstile> p \<leadsto>\<^sup>+ 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 (3 subgoals):
 1. p \<noteq> mdbPrev dest_node
 2. p \<noteq> dest
 3. p \<noteq> mdbNext dest_node proof (chain)
picking this:
mdbNext src_node = dest proof (prove)
using this:
mdbNext src_node = dest

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

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

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

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

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

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

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<noteq> mdbPrev dest_node proof (prove)
using this:
mdbPrev dest_node \<noteq> 0
m (mdbPrev src_node) = Some cte
mdbNext src_node = dest

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. p = dest \<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> dest

goal (1 subgoal):
 1. 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>+ src proof (state)
this:
m \<turnstile> p \<leadsto>\<^sup>+ src

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

goal (1 subgoal):
 1. p = mdbNext dest_node \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> src \<leadsto> dest proof (state)
this:
m \<turnstile> src \<leadsto> 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:
No subgoals!