theory SyscallArgs_C

lemma ccorres_pre_getWorkUnits:
  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
  shows "ccorres r xf
   (\<lambda>s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> P rv s)
   {s. \<forall>rv. s \<in> P' rv} hs (getWorkUnits >>= f) c" apply (simp add: getWorkUnits_def) apply (rule ccorres_guard_imp) apply (rule ccorres_symb_exec_l) defer apply wp[1] apply (rule gets_sp) apply (clarsimp simp: empty_fail_def simpler_gets_def) apply assumption apply clarsimp defer apply (rule ccorres_guard_imp) apply (rule cc) apply clarsimp apply assumption apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> P rv s) {s. \<forall>rv. s \<in> P' rv} hs (getWorkUnits >>= f) c proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. P (ksWorkUnitsCompleted s) s) {s. \<forall>rv. s \<in> P' rv} hs (gets ksWorkUnitsCompleted >>= f) c proof (prove)
goal (3 subgoals):
 1. ccorres r xf ?Q6 ?Q'6 hs (gets ksWorkUnitsCompleted >>= f) c
 2. \<And>s. P (ksWorkUnitsCompleted s) s \<Longrightarrow> ?Q6 s
 3. \<And>s. s \<in> {s. \<forall>rv. s \<in> P' rv} \<Longrightarrow> s \<in> ?Q'6 proof (prove)
goal (6 subgoals):
 1. \<And>rv. ccorres r xf (?Q10 rv) (?Q'10 rv) hs (f rv) c
 2. \<And>s. \<lbrace>(=) s\<rbrace> gets ksWorkUnitsCompleted \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q6\<rbrace> gets ksWorkUnitsCompleted \<lbrace>?Q10\<rbrace>
 4. empty_fail (gets ksWorkUnitsCompleted)
 5. \<And>s. P (ksWorkUnitsCompleted s) s \<Longrightarrow> ?Q6 s
 6. \<And>s. s \<in> {s. \<forall>rv. s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q10 rv s \<longrightarrow> s' \<in> ?Q'10 rv} proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrace>(=) s\<rbrace> gets ksWorkUnitsCompleted \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrace>?Q6\<rbrace> gets ksWorkUnitsCompleted \<lbrace>?Q10\<rbrace>
 3. empty_fail (gets ksWorkUnitsCompleted)
 4. \<And>s. P (ksWorkUnitsCompleted s) s \<Longrightarrow> ?Q6 s
 5. \<And>s. s \<in> {s. \<forall>rv. s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q10 rv s \<longrightarrow> s' \<in> ?Q'10 rv}
 6. \<And>rv. ccorres r xf (?Q10 rv) (?Q'10 rv) hs (f rv) c proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q6\<rbrace> gets ksWorkUnitsCompleted \<lbrace>?Q10\<rbrace>
 2. empty_fail (gets ksWorkUnitsCompleted)
 3. \<And>s. P (ksWorkUnitsCompleted s) s \<Longrightarrow> ?Q6 s
 4. \<And>s. s \<in> {s. \<forall>rv. s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q10 rv s \<longrightarrow> s' \<in> ?Q'10 rv}
 5. \<And>rv. ccorres r xf (?Q10 rv) (?Q'10 rv) hs (f rv) c proof (prove)
goal (4 subgoals):
 1. empty_fail (gets ksWorkUnitsCompleted)
 2. \<And>s. P (ksWorkUnitsCompleted s) s \<Longrightarrow> ?Q6 s
 3. \<And>s. s \<in> {s. \<forall>rv. s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?Q6 and (\<lambda>s. ksWorkUnitsCompleted s = rv)) s \<longrightarrow> s' \<in> ?Q'10 rv}
 4. \<And>rv. ccorres r xf (?Q6 and (\<lambda>s. ksWorkUnitsCompleted s = rv)) (?Q'10 rv) hs (f rv) c proof (prove)
goal (3 subgoals):
 1. \<And>s. P (ksWorkUnitsCompleted s) s \<Longrightarrow> ?Q6 s
 2. \<And>s. s \<in> {s. \<forall>rv. s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?Q6 and (\<lambda>s. ksWorkUnitsCompleted s = rv)) s \<longrightarrow> s' \<in> ?Q'10 rv}
 3. \<And>rv. ccorres r xf (?Q6 and (\<lambda>s. ksWorkUnitsCompleted s = rv)) (?Q'10 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<in> {s. \<forall>rv. s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. P (ksWorkUnitsCompleted s) s) and (\<lambda>s. ksWorkUnitsCompleted s = rv)) s \<longrightarrow> s' \<in> ?Q'10 rv}
 2. \<And>rv. ccorres r xf ((\<lambda>s. P (ksWorkUnitsCompleted s) s) and (\<lambda>s. ksWorkUnitsCompleted s = rv)) (?Q'10 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>\<forall>rv. s \<in> P' rv; (sa, s) \<in> rf_sr; P (ksWorkUnitsCompleted sa) sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'10 (ksWorkUnitsCompleted sa)
 2. \<And>rv. ccorres r xf ((\<lambda>s. P (ksWorkUnitsCompleted s) s) and (\<lambda>s. ksWorkUnitsCompleted s = rv)) (?Q'10 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>rv. ccorres r xf ((\<lambda>s. P (ksWorkUnitsCompleted s) s) and (\<lambda>s. ksWorkUnitsCompleted s = rv)) (?Q'10 rv) hs (f rv) c
 2. \<And>s sa. \<lbrakk>\<forall>rv. s \<in> P' rv; (sa, s) \<in> rf_sr; P (ksWorkUnitsCompleted sa) sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'10 (ksWorkUnitsCompleted sa) proof (prove)
goal (4 subgoals):
 1. \<And>rv. ccorres r xf (?Q28 rv) (?Q'28 rv) hs (f rv) c
 2. \<And>rv s. ((\<lambda>s. P (ksWorkUnitsCompleted s) s) and (\<lambda>s. ksWorkUnitsCompleted s = rv)) s \<Longrightarrow> ?Q28 rv s
 3. \<And>rv s. s \<in> ?Q'10 rv \<Longrightarrow> s \<in> ?Q'28 rv
 4. \<And>s sa. \<lbrakk>\<forall>rv. s \<in> P' rv; (sa, s) \<in> rf_sr; P (ksWorkUnitsCompleted sa) sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'10 (ksWorkUnitsCompleted sa) proof (prove)
goal (3 subgoals):
 1. \<And>rv s. ((\<lambda>s. P (ksWorkUnitsCompleted s) s) and (\<lambda>s. ksWorkUnitsCompleted s = rv)) s \<Longrightarrow> P rv s
 2. \<And>rv s. s \<in> ?Q'10 rv \<Longrightarrow> s \<in> P' rv
 3. \<And>s sa. \<lbrakk>\<forall>rv. s \<in> P' rv; (sa, s) \<in> rf_sr; P (ksWorkUnitsCompleted sa) sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'10 (ksWorkUnitsCompleted sa) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. s \<in> ?Q'10 rv \<Longrightarrow> s \<in> P' rv
 2. \<And>s sa. \<lbrakk>\<forall>rv. s \<in> P' rv; (sa, s) \<in> rf_sr; P (ksWorkUnitsCompleted sa) sa\<rbrakk> \<Longrightarrow> s \<in> ?Q'10 (ksWorkUnitsCompleted sa) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>\<forall>rv. s \<in> P' rv; (sa, s) \<in> rf_sr; P (ksWorkUnitsCompleted sa) sa\<rbrakk> \<Longrightarrow> s \<in> P' (ksWorkUnitsCompleted sa) proof (prove)
goal:
No subgoals!