theory CSpace_R

lemma updateCapFreeIndex_dlist:
  assumes preserve:"\<And>m m'. mdb_inv_preserve m m' \<Longrightarrow> mdb_inv_preserve (Q m) (Q m')"
  shows
 "\<lbrace>\<lambda>s. P (valid_dlist (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s\<rbrace>
  updateCap src (capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))
 \<lbrace>\<lambda>r s. P (valid_dlist (Q (ctes_of s)))\<rbrace>" apply (wp updateCap_ctes_of_wp) apply (subgoal_tac "mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src
              (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE)))))") apply (drule mdb_inv_preserve.preserve_stuff) apply simp apply (rule preserve) apply (rule mdb_inv_preserve_updateCap) apply (clarsimp simp:cte_wp_at_ctes_of)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (valid_dlist (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE)) \<lbrace>\<lambda>r s. P (valid_dlist (Q (ctes_of s)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (valid_dlist (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s \<Longrightarrow> P (valid_dlist (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE)))))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P (valid_dlist (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s; mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE)))))\<rbrakk> \<Longrightarrow> P (valid_dlist (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))))
 2. \<And>s. P (valid_dlist (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P (valid_dlist (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s; valid_dlist (Q (ctes_of s)) = valid_dlist (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) \<and> ut_revocable' (Q (ctes_of s)) = ut_revocable' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) \<and> class_links (Q (ctes_of s)) = class_links (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) \<and> distinct_zombies (Q (ctes_of s)) = distinct_zombies (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) \<and> caps_contained' (Q (ctes_of s)) = caps_contained' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) \<and> mdb_chunked (Q (ctes_of s)) = mdb_chunked (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) \<and> valid_badges (Q (ctes_of s)) = valid_badges (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) \<and> untyped_mdb' (Q (ctes_of s)) = untyped_mdb' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) \<and> irq_control (Q (ctes_of s)) = irq_control (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE)))))\<rbrakk> \<Longrightarrow> P (valid_dlist (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))))
 2. \<And>s. P (valid_dlist (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. P (valid_dlist (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. P (valid_dlist (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE)))) proof (prove)
goal (2 subgoals):
 1. \<And>s. P (valid_dlist (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s \<Longrightarrow> ctes_of s src = Some srcCTE
 2. \<And>s. P (valid_dlist (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s \<Longrightarrow> isUntypedCap (cteCap srcCTE) proof (prove)
goal:
No subgoals!