theory IpcCancel_C

lemma ccorres_pre_getReadyQueuesL2Bitmap:
  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
  shows   "ccorres r xf
                  (\<lambda>s. d \<le> maxDomain \<and> i < l2BitmapSize
                       \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d,i) = rv \<longrightarrow> P rv s))
                  {s. \<forall>rv. (ksReadyQueuesL2Bitmap_' (globals s)).[unat d].[i] = ucast rv
                                 \<longrightarrow> s \<in> P' rv }
                          hs (getReadyQueuesL2Bitmap d i >>= (\<lambda>rv. f rv)) c" apply (rule ccorres_guard_imp) apply (rule ccorres_symb_exec_l2) defer defer apply (rule getReadyQueuesL2Bitmap_sp) apply blast apply clarsimp prefer 3 apply (clarsimp simp: bitmap_fun_defs gets_exs_valid) defer apply (rule ccorres_guard_imp) apply (rule cc) apply blast apply assumption apply (drule rf_sr_cbitmap_L2_relation) apply (clarsimp simp: cbitmap_L2_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s)) {s. \<forall>rv. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> P' rv} hs (getReadyQueuesL2Bitmap d i >>= f) c proof (prove)
goal (3 subgoals):
 1. ccorres r xf ?Q ?Q' hs (getReadyQueuesL2Bitmap d i >>= f) c
 2. \<And>s. d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s) \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> {s. \<forall>rv. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> P' rv} \<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> getReadyQueuesL2Bitmap d i \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getReadyQueuesL2Bitmap d i \<lbrace>?Q4\<rbrace>
 4. \<And>s. d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s) \<Longrightarrow> ?Q s
 5. \<And>s. s \<in> {s. \<forall>rv. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> P' rv} \<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> getReadyQueuesL2Bitmap d i \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getReadyQueuesL2Bitmap d i \<lbrace>?Q4\<rbrace>
 3. \<And>s. d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s) \<Longrightarrow> ?Q s
 4. \<And>s. s \<in> {s. \<forall>rv. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> P' rv} \<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> getReadyQueuesL2Bitmap d i \<lbrace>?Q4\<rbrace>
 2. \<And>s. d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s) \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> {s. \<forall>rv. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> P' rv} \<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> getReadyQueuesL2Bitmap d i \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s) \<Longrightarrow> ?P8 s \<and> d \<le> maxDomain \<and> i < l2BitmapSize
 2. \<And>s. s \<in> {s. \<forall>rv. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> ?P8 s \<longrightarrow> s' \<in> ?Q'4 rv}
 3. \<And>rv. ccorres r xf (\<lambda>s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> ?P8 s) (?Q'4 rv) hs (f rv) c
 4. \<And>s. ?P8 s \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<Longrightarrow> \<lbrace>(=) s\<rbrace> getReadyQueuesL2Bitmap d i \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. s \<in> {s. \<forall>rv. ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s) \<longrightarrow> s' \<in> ?Q'4 rv}
 2. \<And>rv. ccorres r xf (\<lambda>s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s)) (?Q'4 rv) hs (f rv) c
 3. \<And>s. (d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s)) \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<Longrightarrow> \<lbrace>(=) s\<rbrace> getReadyQueuesL2Bitmap d i \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s sa. \<lbrakk>s \<in> P' (ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i]); (sa, s) \<in> rf_sr; d \<le> maxDomain; i < l2BitmapSize; P (ksReadyQueuesL2Bitmap sa (d, i)) sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 (ksReadyQueuesL2Bitmap sa (d, i))
 2. \<And>rv. ccorres r xf (\<lambda>s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s)) (?Q'4 rv) hs (f rv) c
 3. \<And>s. (d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s)) \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<Longrightarrow> \<lbrace>(=) s\<rbrace> getReadyQueuesL2Bitmap d i \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. (d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s)) \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<Longrightarrow> \<lbrace>(=) s\<rbrace> getReadyQueuesL2Bitmap d i \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>s sa. \<lbrakk>s \<in> P' (ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i]); (sa, s) \<in> rf_sr; d \<le> maxDomain; i < l2BitmapSize; P (ksReadyQueuesL2Bitmap sa (d, i)) sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 (ksReadyQueuesL2Bitmap sa (d, i))
 3. \<And>rv. ccorres r xf (\<lambda>s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s)) (?Q'4 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>s \<in> P' (ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i]); (sa, s) \<in> rf_sr; d \<le> maxDomain; i < l2BitmapSize; P (ksReadyQueuesL2Bitmap sa (d, i)) sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 (ksReadyQueuesL2Bitmap sa (d, i))
 2. \<And>rv. ccorres r xf (\<lambda>s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s)) (?Q'4 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>rv. ccorres r xf (\<lambda>s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s)) (?Q'4 rv) hs (f rv) c
 2. \<And>s sa. \<lbrakk>s \<in> P' (ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i]); (sa, s) \<in> rf_sr; d \<le> maxDomain; i < l2BitmapSize; P (ksReadyQueuesL2Bitmap sa (d, i)) sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 (ksReadyQueuesL2Bitmap sa (d, i)) proof (prove)
goal (4 subgoals):
 1. \<And>rv. ccorres r xf (?Q28 rv) (?Q'28 rv) hs (f rv) c
 2. \<And>rv s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s) \<Longrightarrow> ?Q28 rv s
 3. \<And>rv s. s \<in> ?Q'4 rv \<Longrightarrow> s \<in> ?Q'28 rv
 4. \<And>s sa. \<lbrakk>s \<in> P' (ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i]); (sa, s) \<in> rf_sr; d \<le> maxDomain; i < l2BitmapSize; P (ksReadyQueuesL2Bitmap sa (d, i)) sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 (ksReadyQueuesL2Bitmap sa (d, i)) proof (prove)
goal (3 subgoals):
 1. \<And>rv s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d, i) = rv \<longrightarrow> P rv s) \<Longrightarrow> P rv s
 2. \<And>rv s. s \<in> ?Q'4 rv \<Longrightarrow> s \<in> P' rv
 3. \<And>s sa. \<lbrakk>s \<in> P' (ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i]); (sa, s) \<in> rf_sr; d \<le> maxDomain; i < l2BitmapSize; P (ksReadyQueuesL2Bitmap sa (d, i)) sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 (ksReadyQueuesL2Bitmap sa (d, i)) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. s \<in> ?Q'4 rv \<Longrightarrow> s \<in> P' rv
 2. \<And>s sa. \<lbrakk>s \<in> P' (ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i]); (sa, s) \<in> rf_sr; d \<le> maxDomain; i < l2BitmapSize; P (ksReadyQueuesL2Bitmap sa (d, i)) sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'4 (ksReadyQueuesL2Bitmap sa (d, i)) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>s \<in> P' (ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i]); (sa, s) \<in> rf_sr; d \<le> maxDomain; i < l2BitmapSize; P (ksReadyQueuesL2Bitmap sa (d, i)) sa\<rbrakk> \<Longrightarrow> s \<in> P' (ksReadyQueuesL2Bitmap sa (d, i)) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>s \<in> P' (ksReadyQueuesL2Bitmap_' (globals s).[unat d].[i]); d \<le> maxDomain; i < l2BitmapSize; P (ksReadyQueuesL2Bitmap sa (d, i)) sa; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap sa)\<rbrakk> \<Longrightarrow> s \<in> P' (ksReadyQueuesL2Bitmap sa (d, i)) proof (prove)
goal:
No subgoals!