theory CNodeInv_R

lemma modify_map_lhs_rtrancl:
  "\<lbrakk> m p = Some cte; \<not> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* p \<rbrakk> \<Longrightarrow>
  modify_map m p f \<turnstile> p \<leadsto>\<^sup>* x = (x = p \<or> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x)" apply rule apply (erule next_rtrancl_tranclE) apply simp apply (drule (2) iffD1 [OF modify_map_lhs_trancl]) apply simp apply (erule disjE) apply simp apply (drule (2) iffD2 [OF modify_map_lhs_trancl]) apply (erule trancl_into_rtrancl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> p \<leadsto>\<^sup>* x = (x = p \<or> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; modify_map m p f \<turnstile> p \<leadsto>\<^sup>* x\<rbrakk> \<Longrightarrow> x = p \<or> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x
 2. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; x = p \<or> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> p \<leadsto>\<^sup>* x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; p = x\<rbrakk> \<Longrightarrow> x = p \<or> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x
 2. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; p \<noteq> x; modify_map m p f \<turnstile> p \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> x = p \<or> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x
 3. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; x = p \<or> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> p \<leadsto>\<^sup>* x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; p \<noteq> x; modify_map m p f \<turnstile> p \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> x = p \<or> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x
 2. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; x = p \<or> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> p \<leadsto>\<^sup>* x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; p \<noteq> x; modify_map m p f \<turnstile> p \<leadsto>\<^sup>+ x; m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x\<rbrakk> \<Longrightarrow> x = p \<or> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x
 2. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; x = p \<or> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> p \<leadsto>\<^sup>* x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; x = p \<or> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> p \<leadsto>\<^sup>* x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; x = p\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> p \<leadsto>\<^sup>* x
 2. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> p \<leadsto>\<^sup>* x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> p \<leadsto>\<^sup>* x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*; m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x; modify_map m p f \<turnstile> p \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> p \<leadsto>\<^sup>* x proof (prove)
goal:
No subgoals!