theory Untyped_R

lemma chain_n:
  "mdb_chain_0 n" proof - from chain have "m \<turnstile> mdbNext parent_node \<leadsto>\<^sup>* 0" using dlist parent apply (cases "mdbNext parent_node = 0") apply simp apply (erule dlistEn, simp) apply (auto simp: mdb_chain_0_def) done moreover have "\<not>m \<turnstile> mdbNext parent_node \<leadsto>\<^sup>* parent" using parent_next apply clarsimp apply (drule (1) rtrancl_into_trancl2) apply simp done moreover have "\<not> m \<turnstile> 0 \<leadsto>\<^sup>* site" using no_0 site by (auto elim!: next_rtrancl_tranclE dest!: no_0_lhs_trancl) moreover have "\<not> m \<turnstile> 0 \<leadsto>\<^sup>* parent" using no_0 parent by (auto elim!: next_rtrancl_tranclE dest!: no_0_lhs_trancl) moreover note chain ultimately show "mdb_chain_0 n" using no_0 parent site apply (simp add: n new_parent_def new_site_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 parent_node \<leadsto>\<^sup>* 0 proof (prove)
using this:
mdb_chain_0 m
valid_dlist m
m parent = Some (CTE parent_cap parent_node)

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. mdb_chain_0 n proof (state)
this:
(0, parent) \<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 parent_node \<leadsto>\<^sup>* 0
(mdbNext parent_node, parent) \<notin> (mdb_next_rel m)\<^sup>*
(0, site) \<notin> (mdb_next_rel m)\<^sup>*
(0, parent) \<notin> (mdb_next_rel m)\<^sup>*
mdb_chain_0 m proof (prove)
using this:
m \<turnstile> mdbNext parent_node \<leadsto>\<^sup>* 0
(mdbNext parent_node, parent) \<notin> (mdb_next_rel m)\<^sup>*
(0, site) \<notin> (mdb_next_rel m)\<^sup>*
(0, parent) \<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 parent_node \<leadsto>\<^sup>* 0
(mdbNext parent_node, parent) \<notin> (mdb_next_rel m)\<^sup>*
(0, site) \<notin> (mdb_next_rel m)\<^sup>*
(0, parent) \<notin> (mdb_next_rel m)\<^sup>*
mdb_chain_0 m
no_0 m
m parent = Some (CTE parent_cap parent_node)
m site = Some (CTE site_cap site_node)

goal (1 subgoal):
 1. mdb_chain_0 n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> mdbNext parent_node \<leadsto>\<^sup>* 0; (mdbNext parent_node, parent) \<notin> (mdb_next_rel m)\<^sup>*; mdb_chain_0 m; no_0 m; m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node)\<rbrakk> \<Longrightarrow> mdb_chain_0 (m(site \<mapsto> CTE c' (MDB (mdbNext parent_node) parent True True), parent \<mapsto> CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node))) proof (prove)
goal:
No subgoals! proof (state)
this:
mdb_chain_0 n

goal:
No subgoals!