theory CSpace1_R

lemma preserve_stuff:
  "valid_dlist m = valid_dlist m'
 \<and> ut_revocable' m = ut_revocable' m'
 \<and> class_links m = class_links m'
 \<and> distinct_zombies m = distinct_zombies m'
 \<and> caps_contained' m = caps_contained' m'
 \<and> mdb_chunked m = mdb_chunked m'
 \<and> valid_badges m = valid_badges m'
 \<and> untyped_mdb' m = untyped_mdb' m'
 \<and> irq_control m = irq_control m'" apply (intro conjI) apply (rule valid_dlist_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ apply (rule ut_revocable_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ apply (rule class_links_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ apply (rule distinct_zombies_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ apply (rule caps_contained'_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ apply (rule mdb_chunked_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ apply (rule valid_badges_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ apply (rule untyped_mdb'_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ apply (rule irq_control_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_dlist m = valid_dlist m' \<and> ut_revocable' m = ut_revocable' m' \<and> class_links m = class_links m' \<and> distinct_zombies m = distinct_zombies m' \<and> caps_contained' m = caps_contained' m' \<and> mdb_chunked m = mdb_chunked m' \<and> valid_badges m = valid_badges m' \<and> untyped_mdb' m = untyped_mdb' m' \<and> irq_control m = irq_control m' proof (prove)
goal (9 subgoals):
 1. valid_dlist m = valid_dlist m'
 2. ut_revocable' m = ut_revocable' m'
 3. class_links m = class_links m'
 4. distinct_zombies m = distinct_zombies m'
 5. caps_contained' m = caps_contained' m'
 6. mdb_chunked m = mdb_chunked m'
 7. valid_badges m = valid_badges m'
 8. untyped_mdb' m = untyped_mdb' m'
 9. irq_control m = irq_control m' proof (prove)
goal (10 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'
 3. ut_revocable' m = ut_revocable' m'
 4. class_links m = class_links m'
 5. distinct_zombies m = distinct_zombies m'
 6. caps_contained' m = caps_contained' m'
 7. mdb_chunked m = mdb_chunked m'
 8. valid_badges m = valid_badges m'
 9. untyped_mdb' m = untyped_mdb' m'
 10. irq_control m = irq_control m' proof (prove)
goal (8 subgoals):
 1. ut_revocable' m = ut_revocable' m'
 2. class_links m = class_links m'
 3. distinct_zombies m = distinct_zombies m'
 4. caps_contained' m = caps_contained' m'
 5. mdb_chunked m = mdb_chunked m'
 6. valid_badges m = valid_badges m'
 7. untyped_mdb' m = untyped_mdb' m'
 8. irq_control m = irq_control m' proof (prove)
goal (9 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> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte')
 3. class_links m = class_links m'
 4. distinct_zombies m = distinct_zombies m'
 5. caps_contained' m = caps_contained' m'
 6. mdb_chunked m = mdb_chunked m'
 7. valid_badges m = valid_badges m'
 8. untyped_mdb' m = untyped_mdb' m'
 9. irq_control m = irq_control m' proof (prove)
goal (7 subgoals):
 1. class_links m = class_links m'
 2. distinct_zombies m = distinct_zombies m'
 3. caps_contained' m = caps_contained' m'
 4. mdb_chunked m = mdb_chunked m'
 5. valid_badges m = valid_badges m'
 6. untyped_mdb' m = untyped_mdb' m'
 7. irq_control m = irq_control m' proof (prove)
goal (9 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> capClass (cteCap cte) = capClass (cteCap cte')
 3. \<And>p. mdb_next m p = mdb_next m' p
 4. distinct_zombies m = distinct_zombies m'
 5. caps_contained' m = caps_contained' m'
 6. mdb_chunked m = mdb_chunked m'
 7. valid_badges m = valid_badges m'
 8. untyped_mdb' m = untyped_mdb' m'
 9. irq_control m = irq_control m' proof (prove)
goal (6 subgoals):
 1. distinct_zombies m = distinct_zombies m'
 2. caps_contained' m = caps_contained' m'
 3. mdb_chunked m = mdb_chunked m'
 4. valid_badges m = valid_badges m'
 5. untyped_mdb' m = untyped_mdb' m'
 6. irq_control m = irq_control m' proof (prove)
goal (8 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> isZombie (cteCap cte) = isZombie (cteCap cte') \<and> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> isArchPageCap (cteCap cte) = isArchPageCap (cteCap cte') \<and> capBits (cteCap cte) = capBits (cteCap cte') \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte') \<and> capClass (cteCap cte) = capClass (cteCap cte')
 3. \<And>p. mdb_next m p = mdb_next m' p
 4. caps_contained' m = caps_contained' m'
 5. mdb_chunked m = mdb_chunked m'
 6. valid_badges m = valid_badges m'
 7. untyped_mdb' m = untyped_mdb' m'
 8. irq_control m = irq_control m' proof (prove)
goal (5 subgoals):
 1. caps_contained' m = caps_contained' m'
 2. mdb_chunked m = mdb_chunked m'
 3. valid_badges m = valid_badges m'
 4. untyped_mdb' m = untyped_mdb' m'
 5. irq_control m = irq_control m' proof (prove)
goal (6 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> capRange (cteCap cte) = capRange (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'
 3. mdb_chunked m = mdb_chunked m'
 4. valid_badges m = valid_badges m'
 5. untyped_mdb' m = untyped_mdb' m'
 6. irq_control m = irq_control m' proof (prove)
goal (4 subgoals):
 1. mdb_chunked m = mdb_chunked m'
 2. valid_badges m = valid_badges m'
 3. untyped_mdb' m = untyped_mdb' m'
 4. irq_control m = irq_control m' proof (prove)
goal (6 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. valid_badges m = valid_badges m'
 5. untyped_mdb' m = untyped_mdb' m'
 6. irq_control m = irq_control m' proof (prove)
goal (3 subgoals):
 1. valid_badges m = valid_badges m'
 2. untyped_mdb' m = untyped_mdb' m'
 3. irq_control m = irq_control m' proof (prove)
goal (6 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> 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'
 3. \<And>x cte cte'. \<lbrakk>m x = Some cte; m' x = 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'))
 4. \<And>p. mdb_next m p = mdb_next m' p
 5. untyped_mdb' m = untyped_mdb' m'
 6. irq_control m = irq_control m' proof (prove)
goal (2 subgoals):
 1. untyped_mdb' m = untyped_mdb' m'
 2. irq_control m = irq_control 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. irq_control m = irq_control m' proof (prove)
goal (1 subgoal):
 1. irq_control m = irq_control m' proof (prove)
goal (2 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> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte' proof (prove)
goal:
No subgoals!