theory CSpaceAcc_C

lemma ccorres_pre_getNotification:
  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
  shows   "ccorres r xf
           (\<lambda>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s)
           ({s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn})
           hs (getNotification p >>= (\<lambda>rv. f rv)) c" apply (rule ccorres_guard_imp) apply (rule ccorres_symb_exec_l) defer apply wp[1] apply (rule get_ntfn_sp') apply simp apply assumption defer apply (rule ccorres_guard_imp) apply (rule cc) apply simp apply assumption apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s) {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} hs (getNotification p >>= f) c proof (prove)
goal (3 subgoals):
 1. ccorres r xf ?Q ?Q' hs (getNotification p >>= f) c
 2. \<And>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (6 subgoals):
 1. \<And>rv. ccorres r xf (?Q4 rv) (?Q'4 rv) hs (f rv) c
 2. \<And>s. \<lbrace>(=) s\<rbrace> getNotification p \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getNotification p \<lbrace>?Q4\<rbrace>
 4. empty_fail (getNotification p)
 5. \<And>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s \<Longrightarrow> ?Q s
 6. \<And>s. s \<in> {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} \<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 (6 subgoals):
 1. \<And>s. \<lbrace>(=) s\<rbrace> getNotification p \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getNotification p \<lbrace>?Q4\<rbrace>
 3. empty_fail (getNotification p)
 4. \<And>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s \<Longrightarrow> ?Q s
 5. \<And>s. s \<in> {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q4 rv s \<longrightarrow> s' \<in> ?Q'4 rv}
 6. \<And>rv. ccorres r xf (?Q4 rv) (?Q'4 rv) hs (f rv) c proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q\<rbrace> getNotification p \<lbrace>?Q4\<rbrace>
 2. empty_fail (getNotification p)
 3. \<And>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s \<Longrightarrow> ?Q s
 4. \<And>s. s \<in> {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} \<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 (4 subgoals):
 1. empty_fail (getNotification p)
 2. \<And>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} \<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}
 4. \<And>rv. ccorres r xf (?Q and ko_at' rv p) (?Q'4 rv) hs (f rv) c proof (prove)
goal (3 subgoals):
 1. \<And>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s \<Longrightarrow> ?Q s
 2. \<And>s. s \<in> {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} \<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 proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<in> {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s) and ko_at' rv p) s \<longrightarrow> s' \<in> ?Q'4 rv}
 2. \<And>rv. ccorres r xf ((\<lambda>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s) and ko_at' rv p) (?Q'4 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>rv. ccorres r xf ((\<lambda>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s) and ko_at' rv p) (?Q'4 rv) hs (f rv) c
 2. \<And>s. s \<in> {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s) and ko_at' rv p) s \<longrightarrow> s' \<in> ?Q'4 rv} proof (prove)
goal (4 subgoals):
 1. \<And>rv. ccorres r xf (?Q14 rv) (?Q'14 rv) hs (f rv) c
 2. \<And>rv s. ((\<lambda>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s) and ko_at' rv p) s \<Longrightarrow> ?Q14 rv s
 3. \<And>rv s. s \<in> ?Q'4 rv \<Longrightarrow> s \<in> ?Q'14 rv
 4. \<And>s. s \<in> {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s) and ko_at' rv p) s \<longrightarrow> s' \<in> ?Q'4 rv} proof (prove)
goal (3 subgoals):
 1. \<And>rv s. ((\<lambda>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn 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. s \<in> {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s) and ko_at' rv p) s \<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. s \<in> {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s) and ko_at' rv p) s \<longrightarrow> s' \<in> ?Q'4 rv} proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> {s'. \<forall>ntfn s. (s, s') \<in> rf_sr \<and> ko_at' ntfn p s \<longrightarrow> s' \<in> P' ntfn} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. \<forall>ntfn. ko_at' ntfn p s \<longrightarrow> P ntfn s) and ko_at' rv p) s \<longrightarrow> s' \<in> P' rv} proof (prove)
goal:
No subgoals!