theory VSpace_C

lemma ccorres_pre_getObject_pde:
  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
  shows   "ccorres r xf
                  (\<lambda>s. (\<forall>pde. ko_at' pde p s \<longrightarrow> P pde s))
                  {s. \<forall>pde pde'. cslift s (pde_Ptr p) = Some pde' \<and> cpde_relation pde pde'
                           \<longrightarrow> s \<in> P' pde}
                          hs (getObject p >>= (\<lambda>rv. f rv)) c" apply (rule ccorres_guard_imp2) apply (rule ccorres_symb_exec_l) apply (rule ccorres_guard_imp2) apply (rule cc) apply (rule conjI) apply (rule_tac Q="ko_at' rv p s" in conjunct1) apply assumption apply assumption apply (wp getPDE_wp empty_fail_getObject | simp)+ apply clarsimp apply (erule cmap_relationE1 [OF rf_sr_cpde_relation],
         erule ko_at_projectKO_opt) apply simp done

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