theory Untyped_R

lemma updateFreeIndex_descendants_of':
  "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (K idx') cap) ptr s \<and> isUntypedCap cap \<and>
        P ((swp descendants_of') (null_filter' (ctes_of s)))\<rbrace>
   updateCap ptr (capFreeIndex_update (\<lambda>_. index) cap)
   \<lbrace>\<lambda>r s. P ((swp descendants_of') (null_filter' (ctes_of s)))\<rbrace>" apply (wp updateCap_ctes_of_wp) apply clarsimp apply (erule subst[rotated,where P = P]) apply (rule ext) apply (clarsimp simp:null_filter_descendants_of'[OF null_filter_simp']) apply (rule mdb_inv_preserve.descendants_of) apply (clarsimp simp:cte_wp_at_ctes_of) apply (frule_tac m="ctes_of s" and index=index in mdb_inv_preserve_updateCap) apply (clarsimp simp: isCap_simps) apply (clarsimp simp: isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (K idx') cap) ptr s \<and> isUntypedCap cap \<and> P (swp descendants_of' (null_filter' (ctes_of s)))\<rbrace> updateCap ptr (capFreeIndex_update (\<lambda>_. index) cap) \<lbrace>\<lambda>r s. P (swp descendants_of' (null_filter' (ctes_of s)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (K idx') cap) ptr s \<and> isUntypedCap cap \<and> P (swp descendants_of' (null_filter' (ctes_of s))) \<Longrightarrow> P (swp descendants_of' (null_filter' (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (\<lambda>y. idx') cap) ptr s; isUntypedCap cap; P (swp descendants_of' (null_filter' (ctes_of s)))\<rbrakk> \<Longrightarrow> P (\<lambda>a. descendants_of' a (null_filter' (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (\<lambda>y. idx') cap) ptr s; isUntypedCap cap\<rbrakk> \<Longrightarrow> swp descendants_of' (null_filter' (ctes_of s)) = (\<lambda>a. descendants_of' a (null_filter' (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (\<lambda>y. idx') cap) ptr s; isUntypedCap cap\<rbrakk> \<Longrightarrow> swp descendants_of' (null_filter' (ctes_of s)) x = descendants_of' x (null_filter' (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (\<lambda>y. idx') cap) ptr s; isUntypedCap cap\<rbrakk> \<Longrightarrow> descendants_of' x (ctes_of s) = descendants_of' x (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (\<lambda>y. idx') cap) ptr s; isUntypedCap cap\<rbrakk> \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte idx'. \<lbrakk>isUntypedCap cap; ctes_of s ptr = Some cte; cteCap cte = capFreeIndex_update (\<lambda>y. idx') cap\<rbrakk> \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte idx'. \<lbrakk>isUntypedCap cap; ctes_of s ptr = Some cte; cteCap cte = capFreeIndex_update (\<lambda>y. idx') cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 2. \<And>s cte idx'. \<lbrakk>isUntypedCap cap; ctes_of s ptr = Some cte; cteCap cte = capFreeIndex_update (\<lambda>y. idx') cap; mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap cte))))\<rbrakk> \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte idx'. \<lbrakk>isUntypedCap cap; ctes_of s ptr = Some cte; cteCap cte = capFreeIndex_update (\<lambda>y. idx') cap; mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap cte))))\<rbrakk> \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))) proof (prove)
goal:
No subgoals!