theory IpcCancel_C

lemma ccorres_pre_getEndpoint [ccorres_pre]:
  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
  shows   "ccorres r xf
           (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s))
           ({s'. \<forall>ep. cendpoint_relation (cslift s') ep (the (cslift s' (Ptr p))) \<longrightarrow> s' \<in> P' ep})
           hs (getEndpoint p >>= (\<lambda>rv. f rv)) c" apply (rule ccorres_guard_imp) apply (rule ccorres_symb_exec_l2) defer defer apply (rule get_ep_sp') apply assumption apply clarsimp prefer 3 apply (clarsimp simp add: getEndpoint_def exs_getObject objBits_simps') defer apply (rule ccorres_guard_imp) apply (rule cc) apply simp apply assumption apply (drule spec, erule mp) apply (drule cmap_relation_ep) apply (drule (1) cmap_relation_ko_atD) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s)) {s'. \<forall>ep. cendpoint_relation (cslift s') ep (the (cslift s' (ep_Ptr p))) \<longrightarrow> s' \<in> P' ep} hs (getEndpoint p >>= f) c proof (prove)
goal (3 subgoals):
 1. ccorres r xf ?Q ?Q' hs (getEndpoint p >>= f) c
 2. \<And>s. (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s)) s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> {s'. \<forall>ep. cendpoint_relation (cslift s') ep (the (cslift s' (ep_Ptr p))) \<longrightarrow> s' \<in> P' ep} \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (5 subgoals):
 1. \<And>rv. ccorres r xf (?Q4 rv) (?Q'4 rv) hs (f rv) c
 2. \<And>s. ?Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getEndpoint p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getEndpoint p \<lbrace>?Q4\<rbrace>
 4. \<And>s. (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s)) s \<Longrightarrow> ?Q s
 5. \<And>s. s \<in> {s'. \<forall>ep. cendpoint_relation (cslift s') ep (the (cslift s' (ep_Ptr p))) \<longrightarrow> s' \<in> P' ep} \<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 (5 subgoals):
 1. \<And>s. ?Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getEndpoint p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getEndpoint p \<lbrace>?Q4\<rbrace>
 3. \<And>s. (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s)) s \<Longrightarrow> ?Q s
 4. \<And>s. s \<in> {s'. \<forall>ep. cendpoint_relation (cslift s') ep (the (cslift s' (ep_Ptr p))) \<longrightarrow> s' \<in> P' ep} \<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 (5 subgoals):
 1. \<lbrace>?Q\<rbrace> getEndpoint p \<lbrace>?Q4\<rbrace>
 2. \<And>s. (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s)) s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> {s'. \<forall>ep. cendpoint_relation (cslift s') ep (the (cslift s' (ep_Ptr p))) \<longrightarrow> s' \<in> P' ep} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q4 rv s \<longrightarrow> s' \<in> ?Q'4 rv}
 4. \<And>rv. ccorres r xf (?Q4 rv) (?Q'4 rv) hs (f rv) c
 5. \<And>s. ?Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getEndpoint p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s)) s \<Longrightarrow> ?Q s
 2. \<And>s. s \<in> {s'. \<forall>ep. cendpoint_relation (cslift s') ep (the (cslift s' (ep_Ptr p))) \<longrightarrow> s' \<in> P' ep} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?Q and ko_at' rv p) s \<longrightarrow> s' \<in> ?Q'4 rv}
 3. \<And>rv. ccorres r xf (?Q and ko_at' rv p) (?Q'4 rv) hs (f rv) c
 4. \<And>s. ?Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getEndpoint p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. s \<in> {s'. \<forall>ep. cendpoint_relation (cslift s') ep (the (cslift s' (ep_Ptr p))) \<longrightarrow> s' \<in> P' ep} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s) and ko_at' rv p) s \<longrightarrow> s' \<in> ?Q'4 rv}
 2. \<And>rv. ccorres r xf (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s) and ko_at' rv p) (?Q'4 rv) hs (f rv) c
 3. \<And>s. (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getEndpoint p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s rv sa. \<lbrakk>\<forall>ep. cendpoint_relation (cslift s) ep (the (cslift s (ep_Ptr p))) \<longrightarrow> s \<in> P' ep; (sa, s) \<in> rf_sr; ep_at' p sa; \<forall>ep. ko_at' ep p sa \<longrightarrow> P ep sa; ko_at' rv p sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 rv
 2. \<And>rv. ccorres r xf (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s) and ko_at' rv p) (?Q'4 rv) hs (f rv) c
 3. \<And>s. (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getEndpoint p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getEndpoint p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>s rv sa. \<lbrakk>\<forall>ep. cendpoint_relation (cslift s) ep (the (cslift s (ep_Ptr p))) \<longrightarrow> s \<in> P' ep; (sa, s) \<in> rf_sr; ep_at' p sa; \<forall>ep. ko_at' ep p sa \<longrightarrow> P ep sa; ko_at' rv p sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 rv
 3. \<And>rv. ccorres r xf (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s) and ko_at' rv p) (?Q'4 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>s rv sa. \<lbrakk>\<forall>ep. cendpoint_relation (cslift s) ep (the (cslift s (ep_Ptr p))) \<longrightarrow> s \<in> P' ep; (sa, s) \<in> rf_sr; ep_at' p sa; \<forall>ep. ko_at' ep p sa \<longrightarrow> P ep sa; ko_at' rv p sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 rv
 2. \<And>rv. ccorres r xf (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s) and ko_at' rv p) (?Q'4 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>rv. ccorres r xf (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s) and ko_at' rv p) (?Q'4 rv) hs (f rv) c
 2. \<And>s rv sa. \<lbrakk>\<forall>ep. cendpoint_relation (cslift s) ep (the (cslift s (ep_Ptr p))) \<longrightarrow> s \<in> P' ep; (sa, s) \<in> rf_sr; ep_at' p sa; \<forall>ep. ko_at' ep p sa \<longrightarrow> P ep sa; ko_at' rv p 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. (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s) and ko_at' rv p) 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>ep. cendpoint_relation (cslift s) ep (the (cslift s (ep_Ptr p))) \<longrightarrow> s \<in> P' ep; (sa, s) \<in> rf_sr; ep_at' p sa; \<forall>ep. ko_at' ep p sa \<longrightarrow> P ep sa; ko_at' rv p sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 rv proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s) and ko_at' rv p) 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>ep. cendpoint_relation (cslift s) ep (the (cslift s (ep_Ptr p))) \<longrightarrow> s \<in> P' ep; (sa, s) \<in> rf_sr; ep_at' p sa; \<forall>ep. ko_at' ep p sa \<longrightarrow> P ep sa; ko_at' rv p 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>ep. cendpoint_relation (cslift s) ep (the (cslift s (ep_Ptr p))) \<longrightarrow> s \<in> P' ep; (sa, s) \<in> rf_sr; ep_at' p sa; \<forall>ep. ko_at' ep p sa \<longrightarrow> P ep sa; ko_at' rv p sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 rv proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>\<forall>ep. cendpoint_relation (cslift s) ep (the (cslift s (ep_Ptr p))) \<longrightarrow> s \<in> P' ep; (sa, s) \<in> rf_sr; ep_at' p sa; \<forall>ep. ko_at' ep p sa \<longrightarrow> P ep sa; ko_at' rv p sa\<rbrakk> \<Longrightarrow> s \<in> P' rv proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>(sa, s) \<in> rf_sr; ep_at' p sa; \<forall>ep. ko_at' ep p sa \<longrightarrow> P ep sa; ko_at' rv p sa\<rbrakk> \<Longrightarrow> cendpoint_relation (cslift s) rv (the (cslift s (ep_Ptr p))) proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>ep_at' p sa; \<forall>ep. ko_at' ep p sa \<longrightarrow> P ep sa; ko_at' rv p sa; cmap_relation (map_to_eps (ksPSpace sa)) (cslift s) ep_Ptr (cendpoint_relation (cslift s))\<rbrakk> \<Longrightarrow> cendpoint_relation (cslift s) rv (the (cslift s (ep_Ptr p))) proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>ep_at' p sa; \<forall>ep. ko_at' ep p sa \<longrightarrow> P ep sa; ko_at' rv p sa; \<exists>ko'. cslift s (ep_Ptr p) = Some ko' \<and> cendpoint_relation (cslift s) rv ko'\<rbrakk> \<Longrightarrow> cendpoint_relation (cslift s) rv (the (cslift s (ep_Ptr p))) proof (prove)
goal:
No subgoals!