theory CSpace1_R

lemma updateCapFreeIndex_mdb_chain_0:
  assumes preserve:"\<And>m m'. mdb_inv_preserve m m' \<Longrightarrow> mdb_inv_preserve (Q m) (Q m')"
  shows
 "\<lbrace>\<lambda>s. P (mdb_chain_0 (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 (mdb_chain_0 (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.by_products) 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 (mdb_chain_0 (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 (mdb_chain_0 (Q (ctes_of s)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (mdb_chain_0 (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s \<Longrightarrow> P (mdb_chain_0 (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 (mdb_chain_0 (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 (mdb_chain_0 (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))))
 2. \<And>s. P (mdb_chain_0 (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 (mdb_chain_0 (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s; reply_masters_rvk_fb (Q (ctes_of s)) = reply_masters_rvk_fb (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) \<and> no_0 (Q (ctes_of s)) = no_0 (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) \<and> mdb_chain_0 (Q (ctes_of s)) = mdb_chain_0 (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))) \<and> valid_nullcaps (Q (ctes_of s)) = valid_nullcaps (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE)))))\<rbrakk> \<Longrightarrow> P (mdb_chain_0 (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap srcCTE))))))
 2. \<And>s. P (mdb_chain_0 (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 (mdb_chain_0 (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 (mdb_chain_0 (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 (mdb_chain_0 (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 (mdb_chain_0 (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!