theory Arch_C

lemma ccorres_pre_getObject_pte:
  "(\<And>rv. ccorresG rf_sr \<Gamma> r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow>
   ccorresG rf_sr \<Gamma> r xf (\<lambda>s. \<forall>pte. ko_at' pte p s \<longrightarrow> P pte s)
            {s. \<forall>pte pte'. cslift s (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte' \<longrightarrow> s \<in> P' pte} hs
     (getObject p >>= f) c" apply (rule ccorres_guard_imp2) apply (rule ccorres_symb_exec_l) apply (rule_tac P="ko_at' rv p" in ccorres_cross_over_guard) apply assumption apply (wp getObject_inv loadObject_default_inv
               getPTE_wp empty_fail_getObject | simp)+ apply clarsimp apply (erule cmap_relationE1[OF rf_sr_cpte_relation], erule ko_at_projectKO_opt) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> ccorres r xf (\<lambda>s. \<forall>pte. ko_at' pte p s \<longrightarrow> P pte s) {s. \<forall>pte pte'. cslift s (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte' \<longrightarrow> s \<in> P' pte} hs (getObject p >>= f) c proof (prove)
goal (2 subgoals):
 1. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> ccorres r xf ?Q ?Q' hs (getObject p >>= f) c
 2. \<And>s s'. \<lbrakk>\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c; (s, s') \<in> rf_sr; \<forall>pte. ko_at' pte p s \<longrightarrow> P pte s; s' \<in> {s. \<forall>pte pte'. cslift s (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte' \<longrightarrow> s \<in> P' pte}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (5 subgoals):
 1. \<And>rv. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> ccorres r xf (?Q3 rv) (?Q'3 rv) hs (f rv) c
 2. \<And>s. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> \<lbrace>(=) s\<rbrace> getObject p \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> \<lbrace>?Q\<rbrace> getObject p \<lbrace>?Q3\<rbrace>
 4. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> empty_fail (getObject p)
 5. \<And>s s'. \<lbrakk>\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c; (s, s') \<in> rf_sr; \<forall>pte. ko_at' pte p s \<longrightarrow> P pte s; s' \<in> {s. \<forall>pte pte'. cslift s (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte' \<longrightarrow> s \<in> P' pte}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q3 rv s \<longrightarrow> s' \<in> ?Q'3 rv} proof (prove)
goal (5 subgoals):
 1. \<And>rv. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> ccorres r xf (?P'8 rv) (?Q8 rv) hs (f rv) c
 2. \<And>s. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> \<lbrace>(=) s\<rbrace> getObject p \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> \<lbrace>?Q\<rbrace> getObject p \<lbrace>\<lambda>rv. ko_at' rv p and ?P'8 rv\<rbrace>
 4. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> empty_fail (getObject p)
 5. \<And>s s'. \<lbrakk>\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c; (s, s') \<in> rf_sr; \<forall>pte. ko_at' pte p s \<longrightarrow> P pte s; s' \<in> {s. \<forall>pte pte'. cslift s (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte' \<longrightarrow> s \<in> P' pte}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (ko_at' rv p and ?P'8 rv) s \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> ko_at' rv p s \<longrightarrow> s' \<in> ?Q8 rv}} proof (prove)
goal (4 subgoals):
 1. \<And>s. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> \<lbrace>(=) s\<rbrace> getObject p \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> \<lbrace>?Q\<rbrace> getObject p \<lbrace>\<lambda>rv. ko_at' rv p and P rv\<rbrace>
 3. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> empty_fail (getObject p)
 4. \<And>s s'. \<lbrakk>\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c; (s, s') \<in> rf_sr; \<forall>pte. ko_at' pte p s \<longrightarrow> P pte s; s' \<in> {s. \<forall>pte pte'. cslift s (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte' \<longrightarrow> s \<in> P' pte}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (ko_at' rv p and P rv) s \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> ko_at' rv p s \<longrightarrow> s' \<in> P' rv}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c; (s, s') \<in> rf_sr; \<forall>pte. ko_at' pte p s \<longrightarrow> P pte s; \<forall>pte. (\<exists>pte'. cslift s' (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte') \<longrightarrow> s' \<in> P' pte\<rbrakk> \<Longrightarrow> \<forall>rv. (\<exists>s. (s, s') \<in> rf_sr \<and> ko_at' rv p s \<and> P rv s) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> ko_at' rv p s) \<longrightarrow> s' \<in> P' rv proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv sa sb. \<lbrakk>\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c; (s, s') \<in> rf_sr; \<forall>pte. ko_at' pte p s \<longrightarrow> P pte s; \<forall>pte. (\<exists>pte'. cslift s' (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte') \<longrightarrow> s' \<in> P' pte; (sa, s') \<in> rf_sr; ko_at' rv p sa; P rv sa; (sb, s') \<in> rf_sr; ko_at' rv p sb\<rbrakk> \<Longrightarrow> s' \<in> P' rv proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv sa sb y'. \<lbrakk>\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c; (s, s') \<in> rf_sr; \<forall>pte. ko_at' pte p s \<longrightarrow> P pte s; \<forall>pte. (\<exists>pte'. cslift s' (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte') \<longrightarrow> s' \<in> P' pte; ko_at' rv p sa; P rv sa; (sb, s') \<in> rf_sr; ko_at' rv p sb; map_to_ptes (ksPSpace sa) p = Some rv; cpte_relation rv y'; cslift s' (pte_Ptr p) = Some y'\<rbrakk> \<Longrightarrow> s' \<in> P' rv proof (prove)
goal:
No subgoals!