theory VSpace_C

lemma ccorres_pre_getObject_asidpool:
  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
  shows   "ccorres r xf
                  (\<lambda>s. (\<forall>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s))
                  {s. \<forall> asidpool asidpool'. cslift s (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool'
                           \<longrightarrow> s \<in> P' asidpool}
                          hs (getObject p >>= (\<lambda>rv :: asidpool. 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 (wpsimp wp: getASID_wp empty_fail_getObject)+ apply (erule cmap_relationE1 [OF rf_sr_cpspace_asidpool_relation],
         erule ko_at_projectKO_opt) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. \<forall>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s) {s. \<forall>asidpool asidpool'. cslift s (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool' \<longrightarrow> s \<in> P' asidpool} 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>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s; s' \<in> {s. \<forall>asidpool asidpool'. cslift s (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool' \<longrightarrow> s \<in> P' asidpool}\<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>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s; s' \<in> {s. \<forall>asidpool asidpool'. cslift s (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool' \<longrightarrow> s \<in> P' asidpool}\<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>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s; s' \<in> {s. \<forall>asidpool asidpool'. cslift s (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool' \<longrightarrow> s \<in> P' asidpool}\<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>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s; s' \<in> {s. \<forall>asidpool asidpool'. cslift s (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool' \<longrightarrow> s \<in> P' asidpool}\<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>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s; s' \<in> {s. \<forall>asidpool asidpool'. cslift s (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool' \<longrightarrow> s \<in> P' asidpool}\<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>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s; s' \<in> {s. \<forall>asidpool asidpool'. cslift s (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool' \<longrightarrow> s \<in> P' asidpool}\<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>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s; s' \<in> {s. \<forall>asidpool asidpool'. cslift s (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool' \<longrightarrow> s \<in> P' asidpool}\<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>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s; s' \<in> {s. \<forall>asidpool asidpool'. cslift s (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool' \<longrightarrow> s \<in> P' asidpool}\<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' rv sa. \<lbrakk>(s, s') \<in> rf_sr; \<forall>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s; \<forall>asidpool. (\<exists>asidpool'. cslift s' (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool') \<longrightarrow> s' \<in> P' asidpool; (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>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s; \<forall>asidpool. (\<exists>asidpool'. cslift s' (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool') \<longrightarrow> s' \<in> P' asidpool; P rv sa; ko_at' rv p sa; map_to_asidpools (ksPSpace sa) p = Some rv; casid_pool_relation rv y'; cslift s' (ap_Ptr p) = Some y'\<rbrakk> \<Longrightarrow> s' \<in> P' rv proof (prove)
goal:
No subgoals!