theory CNodeInv_R

lemma (in mdb_swap) swap_cases [case_names src_dest dest_src other]:
  assumes src_dest:
  "\<lbrakk>mdbNext src_node = dest; mdbPrev dest_node = src; mdbNext dest_node \<noteq> src; mdbPrev src_node \<noteq> dest\<rbrakk> \<Longrightarrow> P"
  and dest_src:
  "\<lbrakk>mdbNext dest_node = src; mdbPrev src_node = dest; mdbNext src_node \<noteq> dest; mdbPrev dest_node \<noteq> src\<rbrakk> \<Longrightarrow> P"
  and other:
  "\<lbrakk>mdbNext src_node \<noteq> dest; mdbPrev dest_node \<noteq> src; mdbNext dest_node \<noteq> src; mdbPrev src_node \<noteq> dest \<rbrakk> \<Longrightarrow> P"
  shows "P" proof (cases "mdbNext src_node = dest") case True thus ?thesis proof (rule src_dest) from True show "mdbPrev dest_node = src" by simp show "mdbNext dest_node \<noteq> src" proof assume "mdbNext dest_node = src" hence "m \<turnstile> dest \<leadsto> src" using dest by - (rule next_fold, simp+) moreover have "m \<turnstile> src \<leadsto> dest" using src True by - (rule next_fold, simp+) finally show False by simp qed show "mdbPrev src_node \<noteq> dest" proof assume "mdbPrev src_node = dest" hence "mdbNext dest_node = src" using src by (clarsimp elim: dlistEp) hence "m \<turnstile> dest \<leadsto> src" using dest by - (rule next_fold, simp+) moreover have "m \<turnstile> src \<leadsto> dest" using src True by - (rule next_fold, simp+) finally show False by simp qed qed next case False note firstFalse = False show ?thesis proof (cases "mdbNext dest_node = src") case True thus ?thesis proof (rule dest_src) from True show "mdbPrev src_node = dest" by simp show "mdbPrev dest_node \<noteq> src" proof assume "mdbPrev dest_node = src" hence "mdbNext src_node = dest" using dest by (clarsimp elim: dlistEp) hence "m \<turnstile> src \<leadsto> dest" using src by - (rule next_fold, simp+) moreover have "m \<turnstile> dest \<leadsto> src" using dest True by - (rule next_fold, simp+) finally show False by simp qed qed fact+ next case False from firstFalse show ?thesis proof (rule other) show "mdbPrev dest_node \<noteq> src" and "mdbPrev src_node \<noteq> dest" using False firstFalse by simp+ qed fact+ qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (state)
goal (2 subgoals):
 1. mdbNext src_node = dest \<Longrightarrow> P
 2. mdbNext src_node \<noteq> dest \<Longrightarrow> P proof (state)
this:
mdbNext src_node = dest

goal (2 subgoals):
 1. mdbNext src_node = dest \<Longrightarrow> P
 2. mdbNext src_node \<noteq> dest \<Longrightarrow> P proof (prove)
using this:
mdbNext src_node = dest

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

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

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

goal (1 subgoal):
 1. mdbNext dest_node = src \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> src \<leadsto> dest proof (prove)
using this:
m src = Some (CTE src_cap src_node)
mdbNext src_node = dest

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

goal (1 subgoal):
 1. mdbNext dest_node = src \<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:
mdbNext dest_node \<noteq> src

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

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

goal (1 subgoal):
 1. mdbNext dest_node = src proof (prove)
using this:
mdbPrev src_node = dest
m src = Some (CTE src_cap src_node)

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

goal (1 subgoal):
 1. mdbPrev src_node = dest \<Longrightarrow> False proof (prove)
using this:
mdbNext dest_node = src

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

goal (1 subgoal):
 1. mdbPrev src_node = dest \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> src \<leadsto> dest proof (prove)
using this:
m src = Some (CTE src_cap src_node)
mdbNext src_node = dest

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

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

goal:
No subgoals! proof (state)
this:
P

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

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

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

goal (2 subgoals):
 1. mdbNext dest_node = src \<Longrightarrow> P
 2. mdbNext dest_node \<noteq> src \<Longrightarrow> P proof (prove)
using this:
mdbNext dest_node = src

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

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

goal (1 subgoal):
 1. mdbNext src_node = dest proof (prove)
using this:
mdbPrev dest_node = src
m dest = Some (CTE dest_cap dest_node)

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

goal (1 subgoal):
 1. mdbPrev dest_node = src \<Longrightarrow> False proof (prove)
using this:
mdbNext src_node = dest

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

goal (1 subgoal):
 1. mdbPrev dest_node = src \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> dest \<leadsto> src proof (prove)
using this:
m dest = Some (CTE dest_cap dest_node)
mdbNext dest_node = src

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

goal (1 subgoal):
 1. mdbPrev dest_node = 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:
mdbPrev dest_node \<noteq> src

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

goal (1 subgoal):
 1. mdbNext dest_node \<noteq> src \<Longrightarrow> P proof (state)
goal (1 subgoal):
 1. mdbNext dest_node \<noteq> src \<Longrightarrow> P proof (state)
this:
mdbNext dest_node \<noteq> src

goal (1 subgoal):
 1. mdbNext dest_node \<noteq> src \<Longrightarrow> P proof (chain)
picking this:
mdbNext src_node \<noteq> dest proof (prove)
using this:
mdbNext src_node \<noteq> dest

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

goal (1 subgoal):
 1. mdbPrev dest_node \<noteq> src &&& mdbPrev src_node \<noteq> dest proof (state)
this:
mdbPrev dest_node \<noteq> src
mdbPrev src_node \<noteq> dest

goal (1 subgoal):
 1. mdbNext dest_node \<noteq> src proof (state)
this:
P

goal:
No subgoals! proof (state)
this:
P

goal:
No subgoals!