theory CSpace1_R

lemma parentOf_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>
    sameRegionAs (cteCap cte) = sameRegionAs (cteCap cte')
  \<and> (\<lambda>x. sameRegionAs x (cteCap cte)) = (\<lambda>x. sameRegionAs x (cteCap cte'))"
  assumes misc:"\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte'\<rbrakk> \<Longrightarrow>
  isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte')
  \<and> isNotificationCap (cteCap cte)  = isNotificationCap (cteCap cte')
  \<and> (isNotificationCap (cteCap cte) \<longrightarrow> (capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')))
  \<and> (isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte'))
  \<and> (isEndpointCap (cteCap cte) \<longrightarrow> (capEPBadge (cteCap cte) = capEPBadge (cteCap cte')))
  \<and> cteMDBNode cte = cteMDBNode cte'"
  assumes node:"\<And>p. mdb_next m p = mdb_next m' p"
  shows "(m  \<turnstile> p parentOf x) = (m'  \<turnstile> p parentOf x)" apply (rule iffI) apply (rule parentOf_preserve_oneway[OF dom sameRegion misc node]) apply (assumption)+ apply (rule parentOf_preserve_oneway) apply (auto simp:dom sameRegion misc node) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p parentOf x = m' \<turnstile> p parentOf x proof (prove)
goal (2 subgoals):
 1. m \<turnstile> p parentOf x \<Longrightarrow> m' \<turnstile> p parentOf x
 2. m' \<turnstile> p parentOf x \<Longrightarrow> m \<turnstile> p parentOf x proof (prove)
goal (6 subgoals):
 1. \<And>xa cte cte'. \<lbrakk>m \<turnstile> p parentOf x; m xa = Some cte; m' xa = Some cte'\<rbrakk> \<Longrightarrow> m (?x6 xa cte cte') = Some cte
 2. \<And>xa cte cte'. \<lbrakk>m \<turnstile> p parentOf x; m xa = Some cte; m' xa = Some cte'\<rbrakk> \<Longrightarrow> m' (?x6 xa cte cte') = Some cte'
 3. \<And>xa cte cte'. \<lbrakk>m \<turnstile> p parentOf x; m xa = Some cte; m' xa = Some cte'\<rbrakk> \<Longrightarrow> m (?x5 xa cte cte') = Some cte
 4. \<And>xa cte cte'. \<lbrakk>m \<turnstile> p parentOf x; m xa = Some cte; m' xa = Some cte'\<rbrakk> \<Longrightarrow> m' (?x5 xa cte cte') = Some cte'
 5. m \<turnstile> p parentOf x \<Longrightarrow> m \<turnstile> p parentOf x
 6. m' \<turnstile> p parentOf x \<Longrightarrow> m \<turnstile> p parentOf x proof (prove)
goal (1 subgoal):
 1. m' \<turnstile> p parentOf x \<Longrightarrow> m \<turnstile> p parentOf x proof (prove)
goal (5 subgoals):
 1. \<And>xa. m' \<turnstile> p parentOf x \<Longrightarrow> (xa \<in> dom ?m13) = (xa \<in> dom m)
 2. \<And>xa cte cte'. \<lbrakk>m' \<turnstile> p parentOf x; ?m13 xa = Some cte; m xa = Some cte'\<rbrakk> \<Longrightarrow> 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>xa cte cte'. \<lbrakk>m' \<turnstile> p parentOf x; ?m13 xa = Some cte; m xa = Some cte'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> cteMDBNode cte = cteMDBNode cte'
 4. \<And>pa. m' \<turnstile> p parentOf x \<Longrightarrow> mdb_next ?m13 pa = mdb_next m pa
 5. m' \<turnstile> p parentOf x \<Longrightarrow> ?m13 \<turnstile> p parentOf x proof (prove)
goal:
No subgoals!