theory CNodeInv_R

lemma (in mdb_swap) other_dest_next_src_dest:
  fixes cte
  defines "p \<equiv> mdbNext (cteMDBNode cte)"
  assumes src_dest: "mdbNext src_node = dest"
  and     ps: "m (mdbNext 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 - have sn: "m \<turnstile> dest \<leadsto> mdbNext dest_node" .. also have pn: "m \<turnstile> mdbNext dest_node \<leadsto> p" using ps by (simp add: next_unfold' p_def) finally have sp [intro?]: "m \<turnstile> dest \<leadsto>\<^sup>+ p" . have "m \<turnstile> src \<leadsto> mdbNext src_node" .. also have "mdbNext src_node = dest" by fact+ finally have ds [intro?]: "m \<turnstile> src \<leadsto> dest" . show "p \<noteq> mdbPrev dest_node" proof assume a: "p = mdbPrev dest_node" hence "mdbPrev dest_node \<noteq> 0" using p0 by simp hence "m \<turnstile> mdbPrev dest_node \<leadsto> dest" .. hence "m \<turnstile> p \<leadsto> dest" using a by simp thus False using sp by - (drule (1) trancl_into_trancl2, simp) qed show "p \<noteq> dest" proof assume "p = dest" also have "m \<turnstile> dest \<leadsto> mdbNext dest_node" .. also have "m \<turnstile> mdbNext dest_node \<leadsto> p" by (rule pn) finally show False by simp qed show "p \<noteq> mdbNext dest_node" using pn by clarsimp show "p \<noteq> mdbPrev src_node" proof assume a: "p = mdbPrev src_node" hence "mdbPrev src_node \<noteq> 0" using p0 by simp hence "m \<turnstile> mdbPrev src_node \<leadsto> src" .. also have "m \<turnstile> src \<leadsto> dest" .. also have "m \<turnstile> dest \<leadsto>\<^sup>+ p" .. finally show False using a by simp qed show "p \<noteq> src" proof assume "p = src" also have "m \<turnstile> src \<leadsto> dest" .. also have "m \<turnstile> dest \<leadsto>\<^sup>+ p" .. finally show False by simp qed show "p \<noteq> mdbNext src_node" proof assume "p = mdbNext src_node" also have "mdbNext src_node = dest" by fact+ also have "m \<turnstile> dest \<leadsto>\<^sup>+ p" .. 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 (prove)
goal (1 subgoal):
 1. m \<turnstile> dest \<leadsto> mdbNext dest_node proof (state)
this:
m \<turnstile> dest \<leadsto> mdbNext 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> dest \<leadsto> mdbNext 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. m \<turnstile> mdbNext dest_node \<leadsto> p proof (prove)
using this:
m (mdbNext dest_node) = Some cte

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

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> dest \<leadsto>\<^sup>+ p proof (prove)
using this:
m \<turnstile> dest \<leadsto>\<^sup>+ p

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

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> src \<leadsto> mdbNext src_node proof (state)
this:
m \<turnstile> src \<leadsto> mdbNext 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> src \<leadsto> mdbNext 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. mdbNext src_node = dest proof (state)
this:
mdbNext src_node = 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> src \<leadsto> dest proof (prove)
using this:
m \<turnstile> src \<leadsto> dest

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 (prove)
goal (1 subgoal):
 1. p \<noteq> mdbPrev dest_node proof (state)
goal (1 subgoal):
 1. p = mdbPrev dest_node \<Longrightarrow> False proof (state)
this:
p = mdbPrev dest_node

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

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

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

goal (1 subgoal):
 1. p = mdbPrev dest_node \<Longrightarrow> False 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 (1 subgoal):
 1. p = mdbPrev dest_node \<Longrightarrow> False proof (prove)
using this:
m \<turnstile> mdbPrev dest_node \<leadsto> dest

goal (1 subgoal):
 1. m \<turnstile> p \<leadsto> dest proof (prove)
using this:
m \<turnstile> mdbPrev dest_node \<leadsto> dest
p = mdbPrev dest_node

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

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

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

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

goal:
No subgoals! 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 (state)
goal (1 subgoal):
 1. p = dest \<Longrightarrow> False proof (state)
this:
p = dest

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

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

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

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

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

goal:
No subgoals! 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 (prove)
using this:
m \<turnstile> mdbNext dest_node \<leadsto> p

goal (1 subgoal):
 1. p \<noteq> mdbNext dest_node 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 (prove)
goal (1 subgoal):
 1. p \<noteq> mdbPrev src_node proof (state)
goal (1 subgoal):
 1. p = mdbPrev src_node \<Longrightarrow> False proof (state)
this:
p = mdbPrev src_node

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

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

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

goal (1 subgoal):
 1. p = mdbPrev src_node \<Longrightarrow> False 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 (1 subgoal):
 1. p = mdbPrev src_node \<Longrightarrow> False proof (state)
this:
m \<turnstile> mdbPrev src_node \<leadsto> src

goal (1 subgoal):
 1. p = mdbPrev src_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 = mdbPrev src_node \<Longrightarrow> False proof (state)
this:
m \<turnstile> src \<leadsto> dest

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

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

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

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

goal:
No subgoals! 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 (state)
this:
p = src

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

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

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

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. mdbNext src_node = dest proof (state)
this:
mdbNext src_node = dest

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

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

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

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

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

goal:
No subgoals!