theory CSpace1_R

lemma untyped_mdb'_preserve:
  assumes dom:"\<And>x. (x \<in> dom m) = (x \<in> dom m')"
  assumes misc:"\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte'\<rbrakk> \<Longrightarrow>
  isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte')
  \<and> untypedRange (cteCap cte) = untypedRange (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> capRange (cteCap cte) = capRange (cteCap cte')
  \<and> cteMDBNode cte = cteMDBNode cte'"
  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 mdb_next:"\<And>p. mdb_next m p = mdb_next m' p"
  shows
  "untyped_mdb' m = untyped_mdb' m'" apply (rule iffI) apply (erule mdb_untyped'_preserve_oneway[rotated -1]) apply (simp add:dom misc sameRegion range mdb_next)+ apply (erule mdb_untyped'_preserve_oneway[rotated -1]) apply (simp add:dom[symmetric]) apply (frule(1) misc,simp) apply (frule(1) sameRegion,simp) apply (simp add:mdb_next[symmetric])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_mdb' m = untyped_mdb' m' proof (prove)
goal (2 subgoals):
 1. untyped_mdb' m \<Longrightarrow> untyped_mdb' m'
 2. untyped_mdb' m' \<Longrightarrow> untyped_mdb' m proof (prove)
goal (5 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> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> untypedRange (cteCap cte) = untypedRange (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> capRange (cteCap cte) = capRange (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'
 3. \<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'))
 4. \<And>p. mdb_next m p = mdb_next m' p
 5. untyped_mdb' m' \<Longrightarrow> untyped_mdb' m proof (prove)
goal (1 subgoal):
 1. untyped_mdb' m' \<Longrightarrow> untyped_mdb' 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> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> untypedRange (cteCap cte) = untypedRange (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> capRange (cteCap cte) = capRange (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'
 3. \<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'))
 4. \<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> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> untypedRange (cteCap cte) = untypedRange (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> capRange (cteCap cte) = capRange (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'
 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 (1 subgoal):
 1. \<And>p. mdb_next m' p = mdb_next m p proof (prove)
goal:
No subgoals!