theory CSpace1_R

lemma parentOf_preserve_oneway:
  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) \<Longrightarrow> (m'  \<turnstile> p parentOf x)" apply (clarsimp simp:parentOf_def) apply (frule iffD1[OF dom,OF domI]) apply (frule iffD1[OF dom[where x = p],OF domI]) apply clarsimp apply (frule_tac x1 = p in conjunct1[OF sameRegion]) apply assumption apply (frule_tac x1 = x in conjunct2[OF sameRegion]) apply assumption apply (drule_tac x = "cteCap y" in fun_cong) apply (drule_tac x = "cteCap cte'" in fun_cong) apply (drule_tac x = p in misc) apply assumption apply (drule_tac x = x in misc) apply assumption apply (clarsimp simp:isMDBParentOf_def split:cte.splits if_split_asm) by (clarsimp simp: sameRegionAs_def isCap_simps split:if_splits | rule conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p parentOf x \<Longrightarrow> m' \<turnstile> p parentOf x proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte. \<lbrakk>m x = Some cte; m p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m' x = Some cte \<and> m' p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte. \<lbrakk>m x = Some cte; m p = Some cte'; isMDBParentOf cte' cte; x \<in> dom m'\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m' x = Some cte \<and> m' p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte. \<lbrakk>m x = Some cte; m p = Some cte'; isMDBParentOf cte' cte; x \<in> dom m'; p \<in> dom m'\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m' x = Some cte \<and> m' p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte y ya. \<lbrakk>m x = Some cte; m p = Some cte'; isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya\<rbrakk> \<Longrightarrow> isMDBParentOf ya y proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte y ya. \<lbrakk>m x = Some cte; m p = Some cte'; isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya\<rbrakk> \<Longrightarrow> m' p = Some (?cte'15 cte' cte y ya)
 2. \<And>cte' cte y ya. \<lbrakk>m x = Some cte; m p = Some cte'; isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; global.sameRegionAs (cteCap cte') = global.sameRegionAs (cteCap (?cte'15 cte' cte y ya))\<rbrakk> \<Longrightarrow> isMDBParentOf ya y proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte y ya. \<lbrakk>m x = Some cte; m p = Some cte'; isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; global.sameRegionAs (cteCap cte') = global.sameRegionAs (cteCap ya)\<rbrakk> \<Longrightarrow> isMDBParentOf ya y proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte y ya. \<lbrakk>m x = Some cte; m p = Some cte'; isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; global.sameRegionAs (cteCap cte') = global.sameRegionAs (cteCap ya)\<rbrakk> \<Longrightarrow> m' x = Some (?cte'18 cte' cte y ya)
 2. \<And>cte' cte y ya. \<lbrakk>m x = Some cte; m p = Some cte'; isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; global.sameRegionAs (cteCap cte') = global.sameRegionAs (cteCap ya); (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap (?cte'18 cte' cte y ya)))\<rbrakk> \<Longrightarrow> isMDBParentOf ya y proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte y ya. \<lbrakk>m x = Some cte; m p = Some cte'; isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; global.sameRegionAs (cteCap cte') = global.sameRegionAs (cteCap ya); (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap y))\<rbrakk> \<Longrightarrow> isMDBParentOf ya y proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte y ya. \<lbrakk>m x = Some cte; m p = Some cte'; isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap y)); global.sameRegionAs (cteCap cte') (cteCap y) = global.sameRegionAs (cteCap ya) (cteCap y)\<rbrakk> \<Longrightarrow> isMDBParentOf ya y proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte y ya. \<lbrakk>m x = Some cte; m p = Some cte'; isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; global.sameRegionAs (cteCap cte') (cteCap y) = global.sameRegionAs (cteCap ya) (cteCap y); global.sameRegionAs (cteCap cte') (cteCap cte) = global.sameRegionAs (cteCap cte') (cteCap y)\<rbrakk> \<Longrightarrow> isMDBParentOf ya y proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte y ya. \<lbrakk>m x = Some cte; isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; global.sameRegionAs (cteCap cte') (cteCap y) = global.sameRegionAs (cteCap ya) (cteCap y); global.sameRegionAs (cteCap cte') (cteCap cte) = global.sameRegionAs (cteCap cte') (cteCap y)\<rbrakk> \<Longrightarrow> m' p = Some (?cte'24 cte' cte y ya)
 2. \<And>cte' cte y ya. \<lbrakk>m x = Some cte; isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; global.sameRegionAs (cteCap cte') (cteCap y) = global.sameRegionAs (cteCap ya) (cteCap y); global.sameRegionAs (cteCap cte') (cteCap cte) = global.sameRegionAs (cteCap cte') (cteCap y); isUntypedCap (cteCap cte') = isUntypedCap (cteCap (?cte'24 cte' cte y ya)) \<and> isNotificationCap (cteCap cte') = isNotificationCap (cteCap (?cte'24 cte' cte y ya)) \<and> (isNotificationCap (cteCap cte') \<longrightarrow> capNtfnBadge (cteCap cte') = capNtfnBadge (cteCap (?cte'24 cte' cte y ya))) \<and> isEndpointCap (cteCap cte') = isEndpointCap (cteCap (?cte'24 cte' cte y ya)) \<and> (isEndpointCap (cteCap cte') \<longrightarrow> capEPBadge (cteCap cte') = capEPBadge (cteCap (?cte'24 cte' cte y ya))) \<and> cteMDBNode cte' = cteMDBNode (?cte'24 cte' cte y ya)\<rbrakk> \<Longrightarrow> isMDBParentOf ya y proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte y ya. \<lbrakk>m x = Some cte; isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; global.sameRegionAs (cteCap cte') (cteCap y) = global.sameRegionAs (cteCap ya) (cteCap y); global.sameRegionAs (cteCap cte') (cteCap cte) = global.sameRegionAs (cteCap cte') (cteCap y); isUntypedCap (cteCap cte') = isUntypedCap (cteCap ya) \<and> isNotificationCap (cteCap cte') = isNotificationCap (cteCap ya) \<and> (isNotificationCap (cteCap cte') \<longrightarrow> capNtfnBadge (cteCap cte') = capNtfnBadge (cteCap ya)) \<and> isEndpointCap (cteCap cte') = isEndpointCap (cteCap ya) \<and> (isEndpointCap (cteCap cte') \<longrightarrow> capEPBadge (cteCap cte') = capEPBadge (cteCap ya)) \<and> cteMDBNode cte' = cteMDBNode ya\<rbrakk> \<Longrightarrow> isMDBParentOf ya y proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte y ya. \<lbrakk>isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; global.sameRegionAs (cteCap cte') (cteCap y) = global.sameRegionAs (cteCap ya) (cteCap y); global.sameRegionAs (cteCap cte') (cteCap cte) = global.sameRegionAs (cteCap cte') (cteCap y); isUntypedCap (cteCap cte') = isUntypedCap (cteCap ya) \<and> isNotificationCap (cteCap cte') = isNotificationCap (cteCap ya) \<and> (isNotificationCap (cteCap cte') \<longrightarrow> capNtfnBadge (cteCap cte') = capNtfnBadge (cteCap ya)) \<and> isEndpointCap (cteCap cte') = isEndpointCap (cteCap ya) \<and> (isEndpointCap (cteCap cte') \<longrightarrow> capEPBadge (cteCap cte') = capEPBadge (cteCap ya)) \<and> cteMDBNode cte' = cteMDBNode ya\<rbrakk> \<Longrightarrow> m' x = Some (?cte'26 cte' cte y ya)
 2. \<And>cte' cte y ya. \<lbrakk>isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; global.sameRegionAs (cteCap cte') (cteCap y) = global.sameRegionAs (cteCap ya) (cteCap y); global.sameRegionAs (cteCap cte') (cteCap cte) = global.sameRegionAs (cteCap cte') (cteCap y); isUntypedCap (cteCap cte') = isUntypedCap (cteCap ya) \<and> isNotificationCap (cteCap cte') = isNotificationCap (cteCap ya) \<and> (isNotificationCap (cteCap cte') \<longrightarrow> capNtfnBadge (cteCap cte') = capNtfnBadge (cteCap ya)) \<and> isEndpointCap (cteCap cte') = isEndpointCap (cteCap ya) \<and> (isEndpointCap (cteCap cte') \<longrightarrow> capEPBadge (cteCap cte') = capEPBadge (cteCap ya)) \<and> cteMDBNode cte' = cteMDBNode ya; isUntypedCap (cteCap cte) = isUntypedCap (cteCap (?cte'26 cte' cte y ya)) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap (?cte'26 cte' cte y ya)) \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap (?cte'26 cte' cte y ya))) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap (?cte'26 cte' cte y ya)) \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap (?cte'26 cte' cte y ya))) \<and> cteMDBNode cte = cteMDBNode (?cte'26 cte' cte y ya)\<rbrakk> \<Longrightarrow> isMDBParentOf ya y proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte y ya. \<lbrakk>isMDBParentOf cte' cte; m' x = Some y; m' p = Some ya; global.sameRegionAs (cteCap cte') (cteCap y) = global.sameRegionAs (cteCap ya) (cteCap y); global.sameRegionAs (cteCap cte') (cteCap cte) = global.sameRegionAs (cteCap cte') (cteCap y); isUntypedCap (cteCap cte') = isUntypedCap (cteCap ya) \<and> isNotificationCap (cteCap cte') = isNotificationCap (cteCap ya) \<and> (isNotificationCap (cteCap cte') \<longrightarrow> capNtfnBadge (cteCap cte') = capNtfnBadge (cteCap ya)) \<and> isEndpointCap (cteCap cte') = isEndpointCap (cteCap ya) \<and> (isEndpointCap (cteCap cte') \<longrightarrow> capEPBadge (cteCap cte') = capEPBadge (cteCap ya)) \<and> cteMDBNode cte' = cteMDBNode ya; isUntypedCap (cteCap cte) = isUntypedCap (cteCap y) \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap y) \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap y)) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap y) \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap y)) \<and> cteMDBNode cte = cteMDBNode y\<rbrakk> \<Longrightarrow> isMDBParentOf ya y proof (prove)
goal (3 subgoals):
 1. \<And>x1 x1a x1b x2b x1c x2c. \<lbrakk>m' x = Some (CTE x1c x2c); m' p = Some (CTE x1b x2b); global.sameRegionAs x1 x1c; global.sameRegionAs x1 x1a; isUntypedCap x1 = isUntypedCap x1b; isUntypedCap x1a = isUntypedCap x1c; isNotificationCap x1 = isNotificationCap x1b; isNotificationCap x1a = isNotificationCap x1c; isNotificationCap x1b \<longrightarrow> capNtfnBadge x1 = capNtfnBadge x1b; isNotificationCap x1c \<longrightarrow> capNtfnBadge x1a = capNtfnBadge x1c; isEndpointCap x1; capEPBadge x1 = capEPBadge x1a; mdbRevocable x2b; global.sameRegionAs x1b x1c; isEndpointCap x1b; capEPBadge x1a \<noteq> 0; capEPBadge x1b = capEPBadge x1a; \<not> mdbFirstBadged x2c; \<not> isEndpointCap x1a; \<not> isEndpointCap x1c\<rbrakk> \<Longrightarrow> capEPBadge x1a = capEPBadge x1c
 2. \<And>x1 x1a x1b x2b x1c x2c. \<lbrakk>m' x = Some (CTE x1c x2c); m' p = Some (CTE x1b x2b); global.sameRegionAs x1 x1c; global.sameRegionAs x1 x1a; isUntypedCap x1 = isUntypedCap x1b; isUntypedCap x1a = isUntypedCap x1c; isNotificationCap x1; isNotificationCap x1a = isNotificationCap x1c; capNtfnBadge x1 = capNtfnBadge x1a; isNotificationCap x1c \<longrightarrow> capNtfnBadge x1a = capNtfnBadge x1c; isEndpointCap x1 = isEndpointCap x1b; isEndpointCap x1a = isEndpointCap x1c; isEndpointCap x1b \<longrightarrow> capEPBadge x1 = 0; isEndpointCap x1c \<longrightarrow> capEPBadge x1a = capEPBadge x1c; mdbRevocable x2b; global.sameRegionAs x1b x1c; isEndpointCap x1b \<longrightarrow> capEPBadge x1b = 0; isNotificationCap x1b; capNtfnBadge x1a \<noteq> 0; capNtfnBadge x1b = capNtfnBadge x1a; \<not> mdbFirstBadged x2c\<rbrakk> \<Longrightarrow> if isEndpointCap x1b \<and> capEPBadge x1b \<noteq> 0 then capEPBadge x1c = 0 else capNtfnBadge x1a = capNtfnBadge x1c
 3. \<And>x1 x1a x1b x2b x1c x2c. \<lbrakk>m' x = Some (CTE x1c x2c); m' p = Some (CTE x1b x2b); global.sameRegionAs x1 x1c; global.sameRegionAs x1 x1a; isUntypedCap x1 = isUntypedCap x1b; isUntypedCap x1a = isUntypedCap x1c; isNotificationCap x1 = isNotificationCap x1b; isNotificationCap x1a = isNotificationCap x1c; isNotificationCap x1b \<longrightarrow> capNtfnBadge x1 = 0; isNotificationCap x1c \<longrightarrow> capNtfnBadge x1a = capNtfnBadge x1c; isEndpointCap x1 = isEndpointCap x1b; isEndpointCap x1a = isEndpointCap x1c; isEndpointCap x1b \<longrightarrow> capEPBadge x1 = 0; isEndpointCap x1c \<longrightarrow> capEPBadge x1a = capEPBadge x1c; mdbRevocable x2b; global.sameRegionAs x1b x1c; isEndpointCap x1b \<longrightarrow> capEPBadge x1b = 0; isNotificationCap x1b \<longrightarrow> capNtfnBadge x1b = 0\<rbrakk> \<Longrightarrow> if isEndpointCap x1b \<and> capEPBadge x1b \<noteq> 0 then capEPBadge x1c = 0 \<and> \<not> mdbFirstBadged x2c else if isNotificationCap x1b \<and> capNtfnBadge x1b \<noteq> 0 then capNtfnBadge x1c = 0 \<and> \<not> mdbFirstBadged x2c else True