theory CNodeInv_R

lemma mdb_chain_0_cases [consumes 3, case_names srcdest destsrc indep]:
  assumes chain: "mdb_chain_0 m"
  and   no: "no_0 m"
  and   ds: "dest \<noteq> src"
  and  srcdest: "\<lbrakk> m \<turnstile> src \<leadsto>\<^sup>+ dest; \<not> m \<turnstile> dest \<leadsto>\<^sup>* src; m \<turnstile> dest \<leadsto>\<^sup>* 0 \<rbrakk> \<Longrightarrow> R"
  and  destsrc: "\<lbrakk> m \<turnstile> dest \<leadsto>\<^sup>+ src; \<not> m \<turnstile> src \<leadsto>\<^sup>* dest; m \<turnstile> src \<leadsto>\<^sup>* 0 \<rbrakk> \<Longrightarrow> R"
  and  neither: "\<lbrakk>  \<not> m \<turnstile> src \<leadsto>\<^sup>+ dest; \<not> m \<turnstile> dest \<leadsto>\<^sup>+ src \<rbrakk> \<Longrightarrow> R"
  shows "R" proof (cases "m \<turnstile> src \<leadsto>\<^sup>+ dest") case True thus ?thesis proof (rule srcdest) show "\<not> m \<turnstile> dest \<leadsto>\<^sup>* src" by (rule no_loops_tranclE [OF mdb_chain_0_no_loops]) fact+ show "m \<turnstile> dest \<leadsto>\<^sup>* 0" by (rule mdb_chain_0_trancl) fact+ qed next case False note F = False show ?thesis proof (cases "m \<turnstile> dest \<leadsto>\<^sup>+ src") case True thus ?thesis proof (rule destsrc) show "\<not> m \<turnstile> src \<leadsto>\<^sup>* dest" using False ds by (clarsimp elim!: next_rtrancl_tranclE) show "m \<turnstile> src \<leadsto>\<^sup>* 0" by (rule mdb_chain_0_trancl) fact+ qed next case False with F show ?thesis by (rule neither) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R proof (state)
goal (2 subgoals):
 1. m \<turnstile> src \<leadsto>\<^sup>+ dest \<Longrightarrow> R
 2. (src, dest) \<notin> (mdb_next_rel m)\<^sup>+ \<Longrightarrow> R proof (state)
this:
m \<turnstile> src \<leadsto>\<^sup>+ dest

goal (2 subgoals):
 1. m \<turnstile> src \<leadsto>\<^sup>+ dest \<Longrightarrow> R
 2. (src, dest) \<notin> (mdb_next_rel m)\<^sup>+ \<Longrightarrow> R proof (prove)
using this:
m \<turnstile> src \<leadsto>\<^sup>+ dest

goal (1 subgoal):
 1. R proof (state)
goal (2 subgoals):
 1. (dest, src) \<notin> (mdb_next_rel m)\<^sup>*
 2. m \<turnstile> dest \<leadsto>\<^sup>* 0 proof (prove)
goal (1 subgoal):
 1. (dest, src) \<notin> (mdb_next_rel m)\<^sup>* proof (state)
this:
(dest, src) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m \<turnstile> dest \<leadsto>\<^sup>* 0 proof (prove)
goal (1 subgoal):
 1. m \<turnstile> dest \<leadsto>\<^sup>* 0 proof (state)
this:
m \<turnstile> dest \<leadsto>\<^sup>* 0

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

goal (1 subgoal):
 1. (src, dest) \<notin> (mdb_next_rel m)\<^sup>+ \<Longrightarrow> R proof (state)
goal (1 subgoal):
 1. (src, dest) \<notin> (mdb_next_rel m)\<^sup>+ \<Longrightarrow> R proof (state)
this:
(src, dest) \<notin> (mdb_next_rel m)\<^sup>+

goal (1 subgoal):
 1. (src, dest) \<notin> (mdb_next_rel m)\<^sup>+ \<Longrightarrow> R proof (state)
this:
(src, dest) \<notin> (mdb_next_rel m)\<^sup>+

goal (1 subgoal):
 1. (src, dest) \<notin> (mdb_next_rel m)\<^sup>+ \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. R proof (state)
goal (2 subgoals):
 1. m \<turnstile> dest \<leadsto>\<^sup>+ src \<Longrightarrow> R
 2. (dest, src) \<notin> (mdb_next_rel m)\<^sup>+ \<Longrightarrow> R proof (state)
this:
m \<turnstile> dest \<leadsto>\<^sup>+ src

goal (2 subgoals):
 1. m \<turnstile> dest \<leadsto>\<^sup>+ src \<Longrightarrow> R
 2. (dest, src) \<notin> (mdb_next_rel m)\<^sup>+ \<Longrightarrow> R proof (prove)
using this:
m \<turnstile> dest \<leadsto>\<^sup>+ src

goal (1 subgoal):
 1. R proof (state)
goal (2 subgoals):
 1. (src, dest) \<notin> (mdb_next_rel m)\<^sup>*
 2. m \<turnstile> src \<leadsto>\<^sup>* 0 proof (prove)
goal (1 subgoal):
 1. (src, dest) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
using this:
(src, dest) \<notin> (mdb_next_rel m)\<^sup>+
dest \<noteq> src

goal (1 subgoal):
 1. (src, dest) \<notin> (mdb_next_rel m)\<^sup>* proof (state)
this:
(src, dest) \<notin> (mdb_next_rel m)\<^sup>*

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

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

goal (1 subgoal):
 1. (dest, src) \<notin> (mdb_next_rel m)\<^sup>+ \<Longrightarrow> R proof (state)
goal (1 subgoal):
 1. (dest, src) \<notin> (mdb_next_rel m)\<^sup>+ \<Longrightarrow> R proof (state)
this:
(dest, src) \<notin> (mdb_next_rel m)\<^sup>+

goal (1 subgoal):
 1. (dest, src) \<notin> (mdb_next_rel m)\<^sup>+ \<Longrightarrow> R proof (chain)
picking this:
(src, dest) \<notin> (mdb_next_rel m)\<^sup>+
(dest, src) \<notin> (mdb_next_rel m)\<^sup>+ proof (prove)
using this:
(src, dest) \<notin> (mdb_next_rel m)\<^sup>+
(dest, src) \<notin> (mdb_next_rel m)\<^sup>+

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

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

goal:
No subgoals!