theory Untyped_R

lemma updateCap_cte_cap_wp_to':
  "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. p' \<in> cte_refs' (cteCap cte) (irq_node' s) \<and> P (cteCap cte)
                           \<longrightarrow> p' \<in> cte_refs' cap (irq_node' s) \<and> P cap) p s
        \<and> ex_cte_cap_wp_to' P p' s\<rbrace>
     updateCap p cap
   \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P p'\<rbrace>" apply (simp add: ex_cte_cap_wp_to'_def cte_wp_at_ctes_of updateCap_def) apply (rule hoare_pre, (wp getCTE_wp | wps)+) apply (clarsimp simp: cte_wp_at_ctes_of) apply (rule_tac x=cref in exI) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. p' \<in> cte_refs' (cteCap cte) (irq_node' s) \<and> P (cteCap cte) \<longrightarrow> p' \<in> cte_refs' cap (irq_node' s) \<and> P cap) p s \<and> ex_cte_cap_wp_to' P p' s\<rbrace> updateCap p cap \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P p'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>cte. ctes_of s p = Some cte \<and> (p' \<in> cte_refs' (cteCap cte) (irq_node' s) \<and> P (cteCap cte) \<longrightarrow> p' \<in> cte_refs' cap (irq_node' s) \<and> P cap)) \<and> (\<exists>cref cte. ctes_of s cref = Some cte \<and> P (cteCap cte) \<and> p' \<in> cte_refs' (cteCap cte) (irq_node' s))\<rbrace> do cte <- getCTE p;
setCTE p (cteCap_update (\<lambda>_. cap) cte)
od \<lbrace>\<lambda>rv s. \<exists>cref cte. ctes_of s cref = Some cte \<and> P (cteCap cte) \<and> p' \<in> cte_refs' (cteCap cte) (irq_node' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>cte. ctes_of s p = Some cte \<and> (p' \<in> cte_refs' (cteCap cte) (irq_node' s) \<and> P (cteCap cte) \<longrightarrow> p' \<in> cte_refs' cap (irq_node' s) \<and> P cap)) \<and> (\<exists>cref cte. ctes_of s cref = Some cte \<and> P (cteCap cte) \<and> p' \<in> cte_refs' (cteCap cte) (irq_node' s)) \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> (\<exists>cref ctea. ((ctes_of s)(p \<mapsto> cteCap_update (\<lambda>_. cap) cte)) cref = Some ctea \<and> P (cteCap ctea) \<and> p' \<in> cte_refs' (cteCap ctea) (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea. \<lbrakk>p' \<in> cte_refs' (cteCap cte) (irq_node' s) \<and> P (cteCap cte) \<longrightarrow> p' \<in> cte_refs' cap (irq_node' s) \<and> P cap; ctes_of s cref = Some ctea; P (cteCap ctea); p' \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> \<exists>cref. (cref = p \<longrightarrow> P cap \<and> p' \<in> cte_refs' cap (irq_node' s)) \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> P (cteCap cte) \<and> p' \<in> cte_refs' (cteCap cte) (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea. \<lbrakk>p' \<in> cte_refs' (cteCap cte) (irq_node' s) \<and> P (cteCap cte) \<longrightarrow> p' \<in> cte_refs' cap (irq_node' s) \<and> P cap; ctes_of s cref = Some ctea; P (cteCap ctea); p' \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> (cref = p \<longrightarrow> P cap \<and> p' \<in> cte_refs' cap (irq_node' s)) \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> P (cteCap cte) \<and> p' \<in> cte_refs' (cteCap cte) (irq_node' s))) proof (prove)
goal:
No subgoals!