kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace1_R

lemma ut_revocable_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> cteMDBNode cte = cteMDBNode cte'
  \<and> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte')"
  shows  "ut_revocable' m = ut_revocable' m'" apply (rule iffI) apply (rule ut_revocable_preserve_oneway[OF dom misc]) apply (assumption)+ apply (rule ut_revocable_preserve_oneway[OF dom[symmetric]]) apply (simp add:misc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ut_revocable' m = ut_revocable' m' proof (prove)
goal (2 subgoals):
 1. ut_revocable' m \<Longrightarrow> ut_revocable' m'
 2. ut_revocable' m' \<Longrightarrow> ut_revocable' m proof (prove)
goal (4 subgoals):
 1. \<And>x cte cte'. \<lbrakk>ut_revocable' m; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m (?x4 x cte cte') = Some cte
 2. \<And>x cte cte'. \<lbrakk>ut_revocable' m; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m' (?x4 x cte cte') = Some cte'
 3. ut_revocable' m \<Longrightarrow> ut_revocable' m
 4. ut_revocable' m' \<Longrightarrow> ut_revocable' m proof (prove)
goal (1 subgoal):
 1. ut_revocable' m' \<Longrightarrow> ut_revocable' m proof (prove)
goal (2 subgoals):
 1. \<And>x cte cte'. \<lbrakk>ut_revocable' m'; m' x = Some cte; m x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte' \<and> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte')
 2. ut_revocable' m' \<Longrightarrow> ut_revocable' m' proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma class_links_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> capClass (cteCap cte) = capClass (cteCap cte')"
  assumes node:"\<And>p. mdb_next m p = mdb_next m' p"
  shows  "class_links m = class_links m'" apply (rule iffI) apply (rule class_links_preserve_oneway[OF dom misc]) apply (simp add:node)+ apply (rule class_links_preserve_oneway) apply (simp add:dom misc node)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. class_links m = class_links m' proof (prove)
goal (2 subgoals):
 1. class_links m \<Longrightarrow> class_links m'
 2. class_links m' \<Longrightarrow> class_links m proof (prove)
goal (5 subgoals):
 1. \<And>x cte cte'. \<lbrakk>class_links m; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m (?x4 x cte cte') = Some cte
 2. \<And>x cte cte'. \<lbrakk>class_links m; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m' (?x4 x cte cte') = Some cte'
 3. \<And>p. class_links m \<Longrightarrow> mdb_next m p = mdb_next m' p
 4. class_links m \<Longrightarrow> class_links m
 5. class_links m' \<Longrightarrow> class_links m proof (prove)
goal (1 subgoal):
 1. class_links m' \<Longrightarrow> class_links m proof (prove)
goal (4 subgoals):
 1. \<And>x. class_links m' \<Longrightarrow> (x \<in> dom ?m10) = (x \<in> dom m)
 2. \<And>x cte cte'. \<lbrakk>class_links m'; ?m10 x = Some cte; m x = Some cte'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')
 3. \<And>p. class_links m' \<Longrightarrow> mdb_next ?m10 p = mdb_next m p
 4. class_links m' \<Longrightarrow> class_links ?m10 proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma distinct_zombies_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>
      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>
      capUntypedPtr (cteCap cte) = capUntypedPtr (cteCap cte') \<and>
      capClass (cteCap cte) = capClass (cteCap cte')"
  assumes node: "\<And>p. mdb_next m p = mdb_next m' p"
  shows  "distinct_zombies m = distinct_zombies m'" apply (rule iffI) apply (rule distinct_zombies_preserve_oneway[OF dom misc node]) apply (assumption)+ apply (rule distinct_zombies_preserve_oneway) apply (simp add:dom misc node)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_zombies m = distinct_zombies m' proof (prove)
goal (2 subgoals):
 1. distinct_zombies m \<Longrightarrow> distinct_zombies m'
 2. distinct_zombies m' \<Longrightarrow> distinct_zombies m proof (prove)
goal (4 subgoals):
 1. \<And>x cte cte'. \<lbrakk>distinct_zombies m; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m (?x5 x cte cte') = Some cte
 2. \<And>x cte cte'. \<lbrakk>distinct_zombies m; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m' (?x5 x cte cte') = Some cte'
 3. distinct_zombies m \<Longrightarrow> distinct_zombies m
 4. distinct_zombies m' \<Longrightarrow> distinct_zombies m proof (prove)
goal (1 subgoal):
 1. distinct_zombies m' \<Longrightarrow> distinct_zombies m proof (prove)
goal (4 subgoals):
 1. \<And>x. distinct_zombies m' \<Longrightarrow> (x \<in> dom ?m10) = (x \<in> dom m)
 2. \<And>x cte cte'. \<lbrakk>distinct_zombies m'; ?m10 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. distinct_zombies m' \<Longrightarrow> mdb_next ?m10 p = mdb_next m p
 4. distinct_zombies m' \<Longrightarrow> distinct_zombies ?m10 proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma caps_contained'_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> capRange (cteCap cte) = capRange (cteCap cte')
  \<and> cteMDBNode cte = cteMDBNode cte'"
  shows "caps_contained' m = caps_contained' m'" apply (rule iffI) apply (rule caps_contained'_preserve_oneway[OF dom misc]) apply (assumption)+ apply (rule caps_contained'_preserve_oneway) apply (auto simp:dom misc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_contained' m = caps_contained' m' proof (prove)
goal (2 subgoals):
 1. caps_contained' m \<Longrightarrow> caps_contained' m'
 2. caps_contained' m' \<Longrightarrow> caps_contained' m proof (prove)
goal (4 subgoals):
 1. \<And>x cte cte'. \<lbrakk>caps_contained' m; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m (?x4 x cte cte') = Some cte
 2. \<And>x cte cte'. \<lbrakk>caps_contained' m; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m' (?x4 x cte cte') = Some cte'
 3. caps_contained' m \<Longrightarrow> caps_contained' m
 4. caps_contained' m' \<Longrightarrow> caps_contained' m proof (prove)
goal (1 subgoal):
 1. caps_contained' m' \<Longrightarrow> caps_contained' m proof (prove)
goal (3 subgoals):
 1. \<And>x. caps_contained' m' \<Longrightarrow> (x \<in> dom ?m9) = (x \<in> dom m)
 2. \<And>x cte cte'. \<lbrakk>caps_contained' m'; ?m9 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. caps_contained' m' \<Longrightarrow> caps_contained' ?m9 proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma is_chunk_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 " \<lbrakk>m x =Some (CTE a b);m' x = Some (CTE c d)\<rbrakk> \<Longrightarrow> is_chunk m a p p' = is_chunk m' c p p'" apply (rule iffI) apply (rule is_chunk_preserve_oneway[OF dom sameRegion node],assumption+) apply (rule is_chunk_preserve_oneway) apply (auto simp:dom sameRegion node) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d)\<rbrakk> \<Longrightarrow> is_chunk m a p p' = is_chunk m' c p p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); is_chunk m a p p'\<rbrakk> \<Longrightarrow> is_chunk m' c p p'
 2. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); is_chunk m' c p p'\<rbrakk> \<Longrightarrow> is_chunk m a p p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); is_chunk m' c p p'\<rbrakk> \<Longrightarrow> is_chunk m a p p' proof (prove)
goal (6 subgoals):
 1. \<And>xa. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); is_chunk m' c p p'\<rbrakk> \<Longrightarrow> (xa \<in> dom ?m12) = (xa \<in> dom m)
 2. \<And>xa cte cte'. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); is_chunk m' c p p'; ?m12 xa = Some cte; m xa = 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>pa. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); is_chunk m' c p p'\<rbrakk> \<Longrightarrow> mdb_next ?m12 pa = mdb_next m pa
 4. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); is_chunk m' c p p'\<rbrakk> \<Longrightarrow> ?m12 ?x12 = Some (CTE ?a12 ?b12)
 5. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); is_chunk m' c p p'\<rbrakk> \<Longrightarrow> m ?x12 = Some (CTE a ?d12)
 6. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); is_chunk m' c p p'\<rbrakk> \<Longrightarrow> is_chunk ?m12 ?a12 p p' proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma irq_control_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>
      isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and>
      cteMDBNode cte = cteMDBNode cte'"
  shows "irq_control m = irq_control m'" apply (rule iffI[OF irq_control_preserve_oneway[OF dom misc]]) apply (assumption)+ apply (rule irq_control_preserve_oneway) apply (simp add:dom misc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_control m = irq_control m' proof (prove)
goal (4 subgoals):
 1. \<And>x cte cte'. \<lbrakk>irq_control m; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m (?x2 x cte cte') = Some cte
 2. \<And>x cte cte'. \<lbrakk>irq_control m; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m' (?x2 x cte cte') = Some cte'
 3. irq_control m \<Longrightarrow> irq_control m
 4. irq_control m' \<Longrightarrow> irq_control m proof (prove)
goal (1 subgoal):
 1. irq_control m' \<Longrightarrow> irq_control m proof (prove)
goal (3 subgoals):
 1. \<And>x. irq_control m' \<Longrightarrow> (x \<in> dom ?m8) = (x \<in> dom m)
 2. \<And>x cte cte'. \<lbrakk>irq_control m'; ?m8 x = Some cte; m x = Some cte'\<rbrakk> \<Longrightarrow> isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and> cteMDBNode cte = cteMDBNode cte'
 3. irq_control m' \<Longrightarrow> irq_control ?m8 proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma mdb_inv_preserve_fun_upd:
  "mdb_inv_preserve m m' \<Longrightarrow> mdb_inv_preserve (m(a \<mapsto> b)) (m'(a \<mapsto> b))" by (clarsimp simp:mdb_inv_preserve_def mdb_next_def split:if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_inv_preserve m m' \<Longrightarrow> mdb_inv_preserve (m(a \<mapsto> b)) (m'(a \<mapsto> b))
theory CSpace1_R

lemma updateCap_ctes_of_wp:
  "\<lbrace>\<lambda>s.  P (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. cap)))\<rbrace>
  updateCap ptr cap
  \<lbrace>\<lambda>r s.  P (ctes_of s)\<rbrace>" by (rule validI, simp add: updateCap_stuff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. cap)))\<rbrace> updateCap ptr cap \<lbrace>\<lambda>r s. P (ctes_of s)\<rbrace>
theory CSpace1_R

lemma updateCap_cte_wp_at':
  "\<lbrace>\<lambda>s. cte_at' ptr s \<longrightarrow> Q (cte_wp_at' (\<lambda>cte. if p = ptr then P' (CTE cap (cteMDBNode cte)) else P' cte) p s)\<rbrace>
        updateCap ptr cap \<lbrace>\<lambda>rv s. Q (cte_wp_at' P' p s)\<rbrace>" apply (simp add:updateCap_def cte_wp_at_ctes_of) apply (wp setCTE_ctes_of_wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of split del: if_split) apply (case_tac cte, auto split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>_. True) ptr s \<longrightarrow> Q (cte_wp_at' (\<lambda>cte. if p = ptr then P' (CTE cap (cteMDBNode cte)) else P' cte) p s)\<rbrace> updateCap ptr cap \<lbrace>\<lambda>rv s. Q (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>cte. ctes_of s ptr = Some cte) \<longrightarrow> Q (\<exists>cte. ctes_of s p = Some cte \<and> (if p = ptr then P' (CTE cap (cteMDBNode cte)) else P' cte))\<rbrace> do cte <- getCTE ptr;
setCTE ptr (cteCap_update (\<lambda>_. cap) cte)
od \<lbrace>\<lambda>rv s. Q (\<exists>cte. ctes_of s p = Some cte \<and> P' cte)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>cte. ctes_of s ptr = Some cte) \<longrightarrow> Q (\<exists>cte. ctes_of s p = Some cte \<and> (if p = ptr then P' (CTE cap (cteMDBNode cte)) else P' cte)) \<Longrightarrow> cte_wp_at' (\<lambda>_. True) ptr s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) ptr s \<and> Q (\<exists>ctea. ((ctes_of s)(ptr \<mapsto> cteCap_update (\<lambda>_. cap) cte)) p = Some ctea \<and> P' ctea)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>Q (\<exists>cte. ctes_of s p = Some cte \<and> (if p = ptr then P' (CTE cap (cteMDBNode cte)) else P' cte)); ctes_of s ptr = Some cte\<rbrakk> \<Longrightarrow> Q (\<exists>ctea. (if p = ptr then Some (cteCap_update (\<lambda>_. cap) cte) else ctes_of s p) = Some ctea \<and> P' ctea) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma modify_map_eq[simp]:
  "\<lbrakk>m slot = Some srcCTE; cap = cteCap srcCTE\<rbrakk>
   \<Longrightarrow>(modify_map m slot (cteCap_update (\<lambda>_. cap))) = m" apply (rule ext) apply (case_tac srcCTE) apply (auto simp:modify_map_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = Some srcCTE; cap = cteCap srcCTE\<rbrakk> \<Longrightarrow> modify_map m slot (cteCap_update (\<lambda>_. cap)) = m proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>m slot = Some srcCTE; cap = cteCap srcCTE\<rbrakk> \<Longrightarrow> modify_map m slot (cteCap_update (\<lambda>_. cap)) x = m x proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2. \<lbrakk>m slot = Some srcCTE; cap = cteCap srcCTE; srcCTE = CTE x1 x2\<rbrakk> \<Longrightarrow> modify_map m slot (cteCap_update (\<lambda>_. cap)) x = m x proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma setUntypedCapAsFull_valid_cap:
  "\<lbrace>valid_cap' cap and cte_wp_at' ((=) srcCTE) slot\<rbrace>
   setUntypedCapAsFull (cteCap srcCTE) c slot
   \<lbrace>\<lambda>r. valid_cap' cap\<rbrace>" apply (clarsimp simp:setUntypedCapAsFull_def split:if_splits) apply (intro conjI impI) apply (clarsimp simp:updateCap_def) apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' cap and cte_wp_at' ((=) srcCTE) slot\<rbrace> setUntypedCapAsFull (cteCap srcCTE) c slot \<lbrace>\<lambda>r. valid_cap' cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c \<and> capPtr (cteCap srcCTE) = capPtr c \<and> capBlockSize (cteCap srcCTE) = capBlockSize c \<longrightarrow> \<lbrace>valid_cap' cap and cte_wp_at' ((=) srcCTE) slot\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c)) (cteCap srcCTE)) \<lbrace>\<lambda>r. valid_cap' cap\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c \<longrightarrow> isUntypedCap c \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c) \<longrightarrow> \<lbrace>valid_cap' cap and cte_wp_at' ((=) srcCTE) slot\<rbrace> return () \<lbrace>\<lambda>r. valid_cap' cap\<rbrace>) proof (prove)
goal (2 subgoals):
 1. isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c \<and> capPtr (cteCap srcCTE) = capPtr c \<and> capBlockSize (cteCap srcCTE) = capBlockSize c \<Longrightarrow> \<lbrace>valid_cap' cap and cte_wp_at' ((=) srcCTE) slot\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c)) (cteCap srcCTE)) \<lbrace>\<lambda>r. valid_cap' cap\<rbrace>
 2. capPtr (cteCap srcCTE) = capPtr c \<longrightarrow> isUntypedCap c \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c \<Longrightarrow> \<lbrace>valid_cap' cap and cte_wp_at' ((=) srcCTE) slot\<rbrace> return () \<lbrace>\<lambda>r. valid_cap' cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isUntypedCap (cteCap srcCTE); isUntypedCap c; capPtr (cteCap srcCTE) = capPtr c; capBlockSize (cteCap srcCTE) = capBlockSize c\<rbrakk> \<Longrightarrow> \<lbrace>valid_cap' cap and cte_wp_at' ((=) srcCTE) slot\<rbrace> do cte <- getCTE slot;
setCTE slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c)) (cteCap srcCTE)) cte)
od \<lbrace>\<lambda>r. valid_cap' cap\<rbrace>
 2. capPtr (cteCap srcCTE) = capPtr c \<longrightarrow> isUntypedCap c \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c \<Longrightarrow> \<lbrace>valid_cap' cap and cte_wp_at' ((=) srcCTE) slot\<rbrace> return () \<lbrace>\<lambda>r. valid_cap' cap\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma cteCap_update_simps:
  "cteCap_update f srcCTE = CTE (f (cteCap srcCTE)) (cteMDBNode srcCTE)" apply (case_tac srcCTE) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cteCap_update f srcCTE = CTE (f (cteCap srcCTE)) (cteMDBNode srcCTE) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. srcCTE = CTE x1 x2 \<Longrightarrow> cteCap_update f srcCTE = CTE (f (cteCap srcCTE)) (cteMDBNode srcCTE) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma mdb_inv_preserve_sym:"mdb_inv_preserve a b \<Longrightarrow> mdb_inv_preserve b a" by (simp add:mdb_inv_preserve_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_inv_preserve a b \<Longrightarrow> mdb_inv_preserve b a
theory CSpace1_R

lemma mdb_inv_preserve_refl[simp]:
  "mdb_inv_preserve m m" by (simp add:mdb_inv_preserve_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_inv_preserve m m
theory CSpace1_R

lemma (in mdb_insert_abs_sib) next_slot_no_parent':
  "\<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None\<rbrakk>
    \<Longrightarrow> next_slot p t (m(dest := None)) = next_slot p t m" by (insert next_slot_no_parent, simp add: n_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = None\<rbrakk> \<Longrightarrow> next_slot p t (m(dest := None)) = next_slot p t m
theory CSpace1_R

lemma no_parent_next_not_child_None:
  "\<lbrakk>m p = None; finite_depth m\<rbrakk> \<Longrightarrow> next_not_child p t m = None" apply(rule next_not_child_NoneI) apply(fastforce simp: descendants_of_def cdt_parent_defs dest: tranclD2) apply(simp add: next_sib_def) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = None; finite_depth m\<rbrakk> \<Longrightarrow> next_not_child p t m = None proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m p = None; finite_depth m\<rbrakk> \<Longrightarrow> \<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None
 2. \<lbrakk>m p = None; finite_depth m\<rbrakk> \<Longrightarrow> next_sib p t m = None
 3. \<lbrakk>m p = None; finite_depth m\<rbrakk> \<Longrightarrow> finite_depth m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = None; finite_depth m\<rbrakk> \<Longrightarrow> next_sib p t m = None
 2. \<lbrakk>m p = None; finite_depth m\<rbrakk> \<Longrightarrow> finite_depth m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = None; finite_depth m\<rbrakk> \<Longrightarrow> finite_depth m proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma (in mdb_insert_abs_sib) next_slot':
  "\<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []\<rbrakk>
    \<Longrightarrow> next_slot p (t(src_p := list_insert_after (t src_p) src dest))
        (m(dest := Some src_p)) =
       (if p = src then Some dest
        else if p = dest then next_slot src t m else next_slot p t m)" by (insert next_slot, simp add: n_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []\<rbrakk> \<Longrightarrow> next_slot p (t(src_p := list_insert_after (t src_p) src dest)) (m(dest \<mapsto> src_p)) = (if p = src then Some dest else if p = dest then next_slot src t m else next_slot p t m)