theory Ipc_C

lemma ccorres_getCTE_cte_at:
  "ccorresG rf_sr \<Gamma> r xf P P' hs (getCTE p >>= f) c
     \<Longrightarrow> ccorresG rf_sr \<Gamma> r xf (\<lambda>s. cte_at' p s \<longrightarrow> P s) P' hs
            (getCTE p >>= f) c" apply (rule ccorres_guard_imp) apply (subst gets_bind_ign[where f="cte_at' p", symmetric],
           rule ccorres_symb_exec_l[OF _ _ gets_wp]) apply (rule_tac b=x in ccorres_case_bools) apply assumption apply (rule ccorres_getCTE) apply (rule ccorres_False[where P'=UNIV]) apply wp apply simp apply (clarsimp simp: cte_wp_at_ctes_of) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> ccorres r xf (\<lambda>s. cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s) P' hs (getCTE p >>= f) c proof (prove)
goal (3 subgoals):
 1. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> ccorres r xf ?Q ?Q' hs (getCTE p >>= f) c
 2. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (5 subgoals):
 1. \<And>x. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> ccorres r xf (?Q7 x) (?Q'7 x) hs (getCTE p >>= f) c
 2. \<And>s. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (cte_wp_at' (\<lambda>_. True) p) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> empty_fail (gets (cte_wp_at' (\<lambda>_. True) p))
 4. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> ?Q7 (cte_wp_at' (\<lambda>_. True) p s) s
 5. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q7 rv s \<longrightarrow> s' \<in> ?Q'7 rv} proof (prove)
goal (6 subgoals):
 1. \<And>x. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> ccorres r xf (?P14 x) (?P'14 x) hs (getCTE p >>= f) c
 2. \<And>x. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> ccorres r xf (?Q14 x) (?Q'14 x) hs (getCTE p >>= f) c
 3. \<And>s. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (cte_wp_at' (\<lambda>_. True) p) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> empty_fail (gets (cte_wp_at' (\<lambda>_. True) p))
 5. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> ?P14 (cte_wp_at' (\<lambda>_. True) p s) s) \<and> (\<not> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> ?Q14 (cte_wp_at' (\<lambda>_. True) p s) s)
 6. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (rv \<longrightarrow> ?P14 rv s) \<and> (\<not> rv \<longrightarrow> ?Q14 rv s) \<longrightarrow> s' \<in> {s. rv \<longrightarrow> s \<in> ?P'14 rv} \<inter> {s. \<not> rv \<longrightarrow> s \<in> ?Q'14 rv}} proof (prove)
goal (5 subgoals):
 1. \<And>x. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> ccorres r xf (?Q14 x) (?Q'14 x) hs (getCTE p >>= f) c
 2. \<And>s. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (cte_wp_at' (\<lambda>_. True) p) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> empty_fail (gets (cte_wp_at' (\<lambda>_. True) p))
 4. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s) \<and> (\<not> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> ?Q14 (cte_wp_at' (\<lambda>_. True) p s) s)
 5. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (rv \<longrightarrow> P s) \<and> (\<not> rv \<longrightarrow> ?Q14 rv s) \<longrightarrow> s' \<in> {s. rv \<longrightarrow> s \<in> P'} \<inter> {s. \<not> rv \<longrightarrow> s \<in> ?Q'14 rv}} proof (prove)
goal (5 subgoals):
 1. \<And>x rv. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> ccorres r xf (?P15 x rv) (?P'15 x rv) hs (f rv) c
 2. \<And>s. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (cte_wp_at' (\<lambda>_. True) p) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> empty_fail (gets (cte_wp_at' (\<lambda>_. True) p))
 4. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s) \<and> (\<not> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> ?P15 (cte_wp_at' (\<lambda>_. True) p s) cte s))
 5. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (rv \<longrightarrow> P s) \<and> (\<not> rv \<longrightarrow> (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> ?P15 rv cte s)) \<longrightarrow> s' \<in> {s. rv \<longrightarrow> s \<in> P'} \<inter> {s. \<not> rv \<longrightarrow> 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'15 rv (cte_to_H cte')}}} proof (prove)
goal (4 subgoals):
 1. \<And>s. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (cte_wp_at' (\<lambda>_. True) p) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> empty_fail (gets (cte_wp_at' (\<lambda>_. True) p))
 3. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s) \<and> (\<not> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> False))
 4. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (rv \<longrightarrow> P s) \<and> (\<not> rv \<longrightarrow> (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> False)) \<longrightarrow> s' \<in> {s. rv \<longrightarrow> s \<in> P'} \<inter> {s. \<not> rv \<longrightarrow> 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> UNIV}}} proof (prove)
goal (3 subgoals):
 1. ccorres r xf P P' hs (getCTE p >>= f) c \<Longrightarrow> empty_fail (gets (cte_wp_at' (\<lambda>_. True) p))
 2. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s) \<and> (\<not> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> False))
 3. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (rv \<longrightarrow> P s) \<and> (\<not> rv \<longrightarrow> (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> False)) \<longrightarrow> s' \<in> {s. rv \<longrightarrow> s \<in> P'} \<inter> {s. \<not> rv \<longrightarrow> 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> UNIV}}} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> P s) \<and> (\<not> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> False))
 2. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (rv \<longrightarrow> P s) \<and> (\<not> rv \<longrightarrow> (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> False)) \<longrightarrow> s' \<in> {s. rv \<longrightarrow> s \<in> P'} \<inter> {s. \<not> rv \<longrightarrow> 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> UNIV}}} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ccorres r xf P P' hs (getCTE p >>= f) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (rv \<longrightarrow> P s) \<and> (\<not> rv \<longrightarrow> (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> False)) \<longrightarrow> s' \<in> {s. rv \<longrightarrow> s \<in> P'} \<inter> {s. \<not> rv \<longrightarrow> 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> UNIV}}} proof (prove)
goal:
No subgoals!