theory CSpaceAcc_C

lemma ccorres_pre_getCTE:
  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
  shows   "ccorres r xf
                  (\<lambda>s. (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s))
                  {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte') }
                          hs (getCTE p >>= (\<lambda>rv. f rv)) c" apply (rule ccorres_guard_imp) apply (rule ccorres_symb_exec_l) defer apply wp[1] apply (rule getCTE_sp) apply simp apply assumption apply clarsimp defer apply (rule ccorres_guard_imp) apply (rule cc) apply (simp add: cte_wp_at_ctes_of) apply assumption apply (simp add: cte_wp_at_ctes_of) apply (drule (1) rf_sr_ctes_of_clift) apply clarsimp apply (simp add: c_valid_cte_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s) {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte')} hs (getCTE p >>= f) c proof (prove)
goal (3 subgoals):
 1. ccorres r xf ?Q ?Q' hs (getCTE p >>= f) c
 2. \<And>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte')} \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (6 subgoals):
 1. \<And>rv. ccorres r xf (?Q4 rv) (?Q'4 rv) hs (f rv) c
 2. \<And>s. \<lbrace>(=) s\<rbrace> getCTE p \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCTE p \<lbrace>?Q4\<rbrace>
 4. empty_fail (getCTE p)
 5. \<And>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s \<Longrightarrow> ?Q s
 6. \<And>s. s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte')} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q4 rv s \<longrightarrow> s' \<in> ?Q'4 rv} proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrace>(=) s\<rbrace> getCTE p \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getCTE p \<lbrace>?Q4\<rbrace>
 3. empty_fail (getCTE p)
 4. \<And>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s \<Longrightarrow> ?Q s
 5. \<And>s. s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte')} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q4 rv s \<longrightarrow> s' \<in> ?Q'4 rv}
 6. \<And>rv. ccorres r xf (?Q4 rv) (?Q'4 rv) hs (f rv) c proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q\<rbrace> getCTE p \<lbrace>?Q4\<rbrace>
 2. empty_fail (getCTE p)
 3. \<And>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s \<Longrightarrow> ?Q s
 4. \<And>s. s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte')} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q4 rv s \<longrightarrow> s' \<in> ?Q'4 rv}
 5. \<And>rv. ccorres r xf (?Q4 rv) (?Q'4 rv) hs (f rv) c proof (prove)
goal (4 subgoals):
 1. empty_fail (getCTE p)
 2. \<And>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte')} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (cte_wp_at' (\<lambda>c. c = rv) p and ?Q) s \<longrightarrow> s' \<in> ?Q'4 rv}
 4. \<And>rv. ccorres r xf (cte_wp_at' (\<lambda>c. c = rv) p and ?Q) (?Q'4 rv) hs (f rv) c proof (prove)
goal (3 subgoals):
 1. \<And>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s \<Longrightarrow> ?Q s
 2. \<And>s. s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte')} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (cte_wp_at' (\<lambda>c. c = rv) p and ?Q) s \<longrightarrow> s' \<in> ?Q'4 rv}
 3. \<And>rv. ccorres r xf (cte_wp_at' (\<lambda>c. c = rv) p and ?Q) (?Q'4 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte')} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (cte_wp_at' (\<lambda>c. c = rv) p and (\<lambda>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s)) s \<longrightarrow> s' \<in> ?Q'4 rv}
 2. \<And>rv. ccorres r xf (cte_wp_at' (\<lambda>c. c = rv) p and (\<lambda>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s)) (?Q'4 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>s rv sa. \<lbrakk>\<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte'); (sa, s) \<in> rf_sr; cte_wp_at' (\<lambda>c. c = rv) p sa; \<forall>cte. ctes_of sa p = Some cte \<longrightarrow> P cte sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 rv
 2. \<And>rv. ccorres r xf (cte_wp_at' (\<lambda>c. c = rv) p and (\<lambda>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s)) (?Q'4 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>rv. ccorres r xf (cte_wp_at' (\<lambda>c. c = rv) p and (\<lambda>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s)) (?Q'4 rv) hs (f rv) c
 2. \<And>s rv sa. \<lbrakk>\<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte'); (sa, s) \<in> rf_sr; cte_wp_at' (\<lambda>c. c = rv) p sa; \<forall>cte. ctes_of sa p = Some cte \<longrightarrow> P cte sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 rv proof (prove)
goal (4 subgoals):
 1. \<And>rv. ccorres r xf (?Q21 rv) (?Q'21 rv) hs (f rv) c
 2. \<And>rv s. (cte_wp_at' (\<lambda>c. c = rv) p and (\<lambda>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s)) s \<Longrightarrow> ?Q21 rv s
 3. \<And>rv s. s \<in> ?Q'4 rv \<Longrightarrow> s \<in> ?Q'21 rv
 4. \<And>s rv sa. \<lbrakk>\<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte'); (sa, s) \<in> rf_sr; cte_wp_at' (\<lambda>c. c = rv) p sa; \<forall>cte. ctes_of sa p = Some cte \<longrightarrow> P cte sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 rv proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (cte_wp_at' (\<lambda>c. c = rv) p and (\<lambda>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s)) s \<Longrightarrow> P rv s
 2. \<And>rv s. s \<in> ?Q'4 rv \<Longrightarrow> s \<in> P' rv
 3. \<And>s rv sa. \<lbrakk>\<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte'); (sa, s) \<in> rf_sr; cte_wp_at' (\<lambda>c. c = rv) p sa; \<forall>cte. ctes_of sa p = Some cte \<longrightarrow> P cte sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 rv proof (prove)
goal (2 subgoals):
 1. \<And>rv s. s \<in> ?Q'4 rv \<Longrightarrow> s \<in> P' rv
 2. \<And>s rv sa. \<lbrakk>\<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte'); (sa, s) \<in> rf_sr; cte_wp_at' (\<lambda>c. c = rv) p sa; \<forall>cte. ctes_of sa p = Some cte \<longrightarrow> P cte sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 rv proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>\<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte'); (sa, s) \<in> rf_sr; cte_wp_at' (\<lambda>c. c = rv) p sa; \<forall>cte. ctes_of sa p = Some cte \<longrightarrow> P cte sa\<rbrakk> \<Longrightarrow> s \<in> P' rv proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>\<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte'); (sa, s) \<in> rf_sr; ctes_of sa p = Some rv; P rv sa\<rbrakk> \<Longrightarrow> s \<in> P' rv proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>\<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte'); ctes_of sa p = Some rv; P rv sa; \<exists>cte'. cslift s (cte_Ptr p) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> rv = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> s \<in> P' rv proof (prove)
goal (1 subgoal):
 1. \<And>s sa cte' y. \<lbrakk>ctes_of sa p = Some (cte_to_H y); P (cte_to_H y) sa; cslift s (cte_Ptr p) = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; \<not> cl_valid_cte y\<rbrakk> \<Longrightarrow> s \<in> P' (cte_to_H y) proof (prove)
goal:
No subgoals!