theory CSpace1_R

lemma mdb_chunked_preserve:
  assumes dom:"\<And>x. (x \<in> dom m) = (x \<in> dom m')"
  assumes sameRegion:"\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte'
  \<and> sameRegionAs (cteCap cte) = sameRegionAs (cteCap cte')
  \<and> (\<lambda>x. sameRegionAs x (cteCap cte)) = (\<lambda>x. sameRegionAs x (cteCap cte'))"
  assumes node:"\<And>p. mdb_next m p = mdb_next m' p"
  shows
  "mdb_chunked m = mdb_chunked m'" apply (rule iffI) apply (erule mdb_chunked_preserve_oneway[rotated -1]) apply (simp add:dom sameRegion node)+ apply (erule mdb_chunked_preserve_oneway[rotated -1]) apply (simp add:dom[symmetric]) apply (frule sameRegion) apply assumption apply simp apply (simp add:node) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chunked m = mdb_chunked m' proof (prove)
goal (2 subgoals):
 1. mdb_chunked m \<Longrightarrow> mdb_chunked m'
 2. mdb_chunked m' \<Longrightarrow> mdb_chunked m proof (prove)
goal (4 subgoals):
 1. \<And>x. (x \<in> dom m) = (x \<in> dom m')
 2. \<And>x cte cte'. \<lbrakk>m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte' \<and> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 3. \<And>p. mdb_next m p = mdb_next m' p
 4. mdb_chunked m' \<Longrightarrow> mdb_chunked m proof (prove)
goal (1 subgoal):
 1. mdb_chunked m' \<Longrightarrow> mdb_chunked m proof (prove)
goal (3 subgoals):
 1. \<And>x. (x \<in> dom m') = (x \<in> dom m)
 2. \<And>x cte cte'. \<lbrakk>m' x = Some cte; m x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte' \<and> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 3. \<And>p. mdb_next m' p = mdb_next m p proof (prove)
goal (2 subgoals):
 1. \<And>x cte cte'. \<lbrakk>m' x = Some cte; m x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte' \<and> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 2. \<And>p. mdb_next m' p = mdb_next m p proof (prove)
goal (3 subgoals):
 1. \<And>x cte cte'. \<lbrakk>m' x = Some cte; m x = Some cte'\<rbrakk> \<Longrightarrow> m' x = Some (?cte'13 x cte cte')
 2. \<And>x cte cte'. \<lbrakk>m' x = Some cte; m x = Some cte'; cteMDBNode cte' = cteMDBNode (?cte'13 x cte cte') \<and> global.sameRegionAs (cteCap cte') = global.sameRegionAs (cteCap (?cte'13 x cte cte')) \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte')) = (\<lambda>xa. global.sameRegionAs xa (cteCap (?cte'13 x cte cte')))\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte' \<and> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 3. \<And>p. mdb_next m' p = mdb_next m p proof (prove)
goal (2 subgoals):
 1. \<And>x cte cte'. \<lbrakk>m' x = Some cte; m x = Some cte'; cteMDBNode cte' = cteMDBNode cte \<and> global.sameRegionAs (cteCap cte') = global.sameRegionAs (cteCap cte) \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte')) = (\<lambda>x. global.sameRegionAs x (cteCap cte))\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte' \<and> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 2. \<And>p. mdb_next m' p = mdb_next m p proof (prove)
goal (1 subgoal):
 1. \<And>p. mdb_next m' p = mdb_next m p proof (prove)
goal:
No subgoals!