theory CSpace1_R

lemma chain_n:
  "mdb_chain_0 n" proof - from chain have "m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0" using dlist src apply (cases "mdbNext src_node = 0") apply simp apply (erule dlistEn, simp) apply (auto simp: mdb_chain_0_def) done moreover have "\<not>m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* src" using src_next apply clarsimp apply (drule (1) rtrancl_into_trancl2) apply simp done moreover have "\<not> m \<turnstile> 0 \<leadsto>\<^sup>* dest" using no_0 dest by (auto elim!: next_rtrancl_tranclE dest!: no_0_lhs_trancl) moreover have "\<not> m \<turnstile> 0 \<leadsto>\<^sup>* src" using no_0 src by (auto elim!: next_rtrancl_tranclE dest!: no_0_lhs_trancl) moreover note chain ultimately show "mdb_chain_0 n" using no_0 src dest apply (simp add: n new_src_def new_dest_def) apply (auto intro!: mdb_chain_0_update no_0_update simp: next_update_lhs_rtrancl) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chain_0 n proof (state)
goal (1 subgoal):
 1. mdb_chain_0 n proof (chain)
picking this:
mdb_chain_0 m proof (prove)
using this:
mdb_chain_0 m

goal (1 subgoal):
 1. m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0 proof (prove)
using this:
mdb_chain_0 m
valid_dlist m
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdb_chain_0 m; valid_dlist m; m src = Some (CTE src_cap src_node); mdbNext src_node = 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0
 2. \<lbrakk>mdb_chain_0 m; valid_dlist m; m src = Some (CTE src_cap src_node); mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_chain_0 m; valid_dlist m; m src = Some (CTE src_cap src_node); mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0 proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdb_chain_0 m; valid_dlist m; mdbNext src_node \<noteq> 0; m (mdbNext (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbPrev (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0 proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0

goal (1 subgoal):
 1. mdb_chain_0 n proof (state)
this:
m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0

goal (1 subgoal):
 1. mdb_chain_0 n proof (prove)
goal (1 subgoal):
 1. (mdbNext src_node, src) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
using this:
m \<turnstile> src \<leadsto> mdbNext src_node

goal (1 subgoal):
 1. (mdbNext src_node, src) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> src \<leadsto> mdbNext src_node; m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* src\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* src; m \<turnstile> src \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
(mdbNext src_node, src) \<notin> (mdb_next_rel m)\<^sup>*

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

goal (1 subgoal):
 1. mdb_chain_0 n proof (prove)
goal (1 subgoal):
 1. (0, dest) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
using this:
no_0 m
m dest = Some (CTE dest_cap dest_node)

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

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

goal (1 subgoal):
 1. mdb_chain_0 n proof (prove)
goal (1 subgoal):
 1. (0, src) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
using this:
no_0 m
m src = Some (CTE src_cap src_node)

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

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

goal (1 subgoal):
 1. mdb_chain_0 n proof (state)
this:
mdb_chain_0 m

goal (1 subgoal):
 1. mdb_chain_0 n proof (chain)
picking this:
m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0
(mdbNext src_node, src) \<notin> (mdb_next_rel m)\<^sup>*
(0, dest) \<notin> (mdb_next_rel m)\<^sup>*
(0, src) \<notin> (mdb_next_rel m)\<^sup>*
mdb_chain_0 m proof (prove)
using this:
m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0
(mdbNext src_node, src) \<notin> (mdb_next_rel m)\<^sup>*
(0, dest) \<notin> (mdb_next_rel m)\<^sup>*
(0, src) \<notin> (mdb_next_rel m)\<^sup>*
mdb_chain_0 m

goal (1 subgoal):
 1. mdb_chain_0 n proof (prove)
using this:
m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0
(mdbNext src_node, src) \<notin> (mdb_next_rel m)\<^sup>*
(0, dest) \<notin> (mdb_next_rel m)\<^sup>*
(0, src) \<notin> (mdb_next_rel m)\<^sup>*
mdb_chain_0 m
no_0 m
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdb_chain_0 n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* 0; (mdbNext src_node, src) \<notin> (mdb_next_rel m)\<^sup>*; mdb_chain_0 m; no_0 m; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> mdb_chain_0 (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))), src \<mapsto> CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) proof (prove)
goal:
No subgoals! proof (state)
this:
mdb_chain_0 n

goal:
No subgoals!