theory Finalise_R

lemma mdb_chunked2D:
  "\<lbrakk> mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p'';
     m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd'');
     sameRegionAs cap cap''; p \<noteq> p'' \<rbrakk>
     \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') \<and> sameRegionAs cap cap'" apply (subgoal_tac "\<exists>cap' nd'. m p' = Some (CTE cap' nd')") apply (clarsimp simp add: mdb_chunked_def) apply (drule spec[where x=p]) apply (drule spec[where x=p'']) apply clarsimp apply (drule mp, erule trancl_into_trancl2) apply (erule trancl.intros(1)) apply (simp add: is_chunk_def) apply (drule spec, drule mp, erule trancl.intros(1)) apply (drule mp, rule trancl_into_rtrancl) apply (erule trancl.intros(1)) apply clarsimp apply (clarsimp simp: mdb_next_unfold) apply (case_tac z, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') \<and> global.sameRegionAs cap cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; \<exists>cap' nd'. m p' = Some (CTE cap' nd')\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') \<and> global.sameRegionAs cap cap'
 2. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') proof (prove)
goal (2 subgoals):
 1. \<And>cap' nd'. \<lbrakk>\<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)); m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; m p' = Some (CTE cap' nd')\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap'
 2. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') proof (prove)
goal (2 subgoals):
 1. \<And>cap' nd'. \<lbrakk>m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; m p' = Some (CTE cap' nd'); \<forall>p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p))\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap'
 2. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') proof (prove)
goal (2 subgoals):
 1. \<And>cap' nd'. \<lbrakk>m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; m p' = Some (CTE cap' nd'); \<forall>cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p'' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p'' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p'' \<or> m \<turnstile> p'' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> is_chunk m cap p p'') \<and> (m \<turnstile> p'' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p'' p))\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap'
 2. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') proof (prove)
goal (2 subgoals):
 1. \<And>cap' nd'. \<lbrakk>m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; m p' = Some (CTE cap' nd'); m \<turnstile> p \<leadsto>\<^sup>+ p'' \<or> m \<turnstile> p'' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> is_chunk m cap p p''; m \<turnstile> p'' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap'' p'' p\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap'
 2. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') proof (prove)
goal (3 subgoals):
 1. \<And>cap' nd'. \<lbrakk>m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; m p' = Some (CTE cap' nd'); m \<turnstile> p \<leadsto>\<^sup>+ p'' \<or> m \<turnstile> p'' \<leadsto>\<^sup>+ p; m \<turnstile> p'' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap'' p'' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p''
 2. \<And>cap' nd'. \<lbrakk>m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; m p' = Some (CTE cap' nd'); m \<turnstile> p \<leadsto>\<^sup>+ p'' \<or> m \<turnstile> p'' \<leadsto>\<^sup>+ p; m \<turnstile> p'' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap'' p'' p; is_chunk m cap p p''\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap'
 3. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') proof (prove)
goal (2 subgoals):
 1. \<And>cap' nd'. \<lbrakk>m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; m p' = Some (CTE cap' nd'); m \<turnstile> p \<leadsto>\<^sup>+ p'' \<or> m \<turnstile> p'' \<leadsto>\<^sup>+ p; m \<turnstile> p'' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap'' p'' p; is_chunk m cap p p''\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap'
 2. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') proof (prove)
goal (2 subgoals):
 1. \<And>cap' nd'. \<lbrakk>m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; m p' = Some (CTE cap' nd'); m \<turnstile> p \<leadsto>\<^sup>+ p'' \<or> m \<turnstile> p'' \<leadsto>\<^sup>+ p; m \<turnstile> p'' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''a. m \<turnstile> p'' \<leadsto>\<^sup>+ p''a \<longrightarrow> m \<turnstile> p''a \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''a. (\<exists>n''. m p''a = Some (CTE cap''a n'')) \<and> global.sameRegionAs cap'' cap''a)); \<forall>p''a. m \<turnstile> p \<leadsto>\<^sup>+ p''a \<longrightarrow> m \<turnstile> p''a \<leadsto>\<^sup>* p'' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p''a = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap'
 2. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') proof (prove)
goal (2 subgoals):
 1. \<And>cap' nd'. \<lbrakk>m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; m p' = Some (CTE cap' nd'); m \<turnstile> p \<leadsto>\<^sup>+ p'' \<or> m \<turnstile> p'' \<leadsto>\<^sup>+ p; m \<turnstile> p'' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''a. m \<turnstile> p'' \<leadsto>\<^sup>+ p''a \<longrightarrow> m \<turnstile> p''a \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''a. (\<exists>n''. m p''a = Some (CTE cap''a n'')) \<and> global.sameRegionAs cap'' cap''a)); m \<turnstile> p' \<leadsto>\<^sup>* p'' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap'
 2. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') proof (prove)
goal (3 subgoals):
 1. \<And>cap' nd'. \<lbrakk>m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; m p' = Some (CTE cap' nd'); m \<turnstile> p \<leadsto>\<^sup>+ p'' \<or> m \<turnstile> p'' \<leadsto>\<^sup>+ p; m \<turnstile> p'' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''a. m \<turnstile> p'' \<leadsto>\<^sup>+ p''a \<longrightarrow> m \<turnstile> p''a \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''a. (\<exists>n''. m p''a = Some (CTE cap''a n'')) \<and> global.sameRegionAs cap'' cap''a))\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p''
 2. \<And>cap' nd'. \<lbrakk>m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; m p' = Some (CTE cap' nd'); m \<turnstile> p \<leadsto>\<^sup>+ p'' \<or> m \<turnstile> p'' \<leadsto>\<^sup>+ p; m \<turnstile> p'' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''a. m \<turnstile> p'' \<leadsto>\<^sup>+ p''a \<longrightarrow> m \<turnstile> p''a \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''a. (\<exists>n''. m p''a = Some (CTE cap''a n'')) \<and> global.sameRegionAs cap'' cap''a)); \<exists>cap''. (\<exists>n''. m p' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap'
 3. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') proof (prove)
goal (2 subgoals):
 1. \<And>cap' nd'. \<lbrakk>m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''; m p' = Some (CTE cap' nd'); m \<turnstile> p \<leadsto>\<^sup>+ p'' \<or> m \<turnstile> p'' \<leadsto>\<^sup>+ p; m \<turnstile> p'' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''a. m \<turnstile> p'' \<leadsto>\<^sup>+ p''a \<longrightarrow> m \<turnstile> p''a \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''a. (\<exists>n''. m p''a = Some (CTE cap''a n'')) \<and> global.sameRegionAs cap'' cap''a)); \<exists>cap''. (\<exists>n''. m p' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap'
 2. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> p''\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>mdb_chunked m; p' = mdbNext nd; m p = Some (CTE cap nd); m (mdbNext (cteMDBNode z)) = Some (CTE cap'' nd''); global.sameRegionAs cap cap''; p \<noteq> mdbNext (cteMDBNode z); m (mdbNext nd) = Some z; p'' = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> \<exists>cap' nd'. z = CTE cap' nd' proof (prove)
goal:
No subgoals!