theory CCorresLemmas

lemma ccorres_call_getter_setter_dc:
  assumes cul: "ccorresG sr \<Gamma> r' xf' P (i ` P') [] getter (Call f)"
    and   gsr: "\<And>x x' s t rv.
                 \<lbrakk> (x, t) \<in> sr; r' rv (xf' t); ((), x') \<in> fst (setter rv x) \<rbrakk>
                 \<Longrightarrow> (x', g s t (clean s t)) \<in> sr"
    and   ist: "\<And>x s. (x, s) \<in> sr \<Longrightarrow> (x, i s) \<in> sr"
    and    ef: "\<And>val. empty_fail (setter val)"
  shows "ccorresG sr \<Gamma> dc xfdc P P' hs
           (getter >>= setter)
           (call i f clean (\<lambda>s t. Basic (g s t)))" apply (rule ccorres_guard_imp) apply (rule monadic_rewrite_ccorres_assemble[rotated]) apply (rule monadic_rewrite_is_refl) apply (rule add_remove_return) apply (rule ccorres_seq_skip'[THEN iffD1]) apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_call_getter_setter) apply (fastforce intro: cul) apply (fastforce intro: gsr) apply (simp add: gsr) apply (fastforce intro: ist) apply (fastforce intro: ef) apply (rule ceqv_refl) apply (fastforce intro: ccorres_return_Skip) apply wpsimp apply (clarsimp simp: guard_is_UNIV_def) apply wpsimp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG sr \<Gamma> dc xfdc P P' hs (getter >>= setter) (call i f clean (\<lambda>s t. Basic (g s t))) proof (prove)
goal (3 subgoals):
 1. ccorresG sr \<Gamma> dc xfdc ?Q ?Q' hs (getter >>= setter) (call i f clean (\<lambda>s t. Basic (g s t)))
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> P' \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (4 subgoals):
 1. monadic_rewrite ?F4 ?E4 ?Q4 (getter >>= setter) ?f4
 2. ccorresG sr \<Gamma> dc xfdc ?P4 ?Q' hs ?f4 (call i f clean (\<lambda>s t. Basic (g s t)))
 3. \<And>s. P s \<Longrightarrow> (?P4 and ?Q4) s
 4. \<And>s. s \<in> P' \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (4 subgoals):
 1. getter >>= setter = ?f4
 2. ccorresG sr \<Gamma> dc xfdc ?P4 ?Q' hs ?f4 (call i f clean (\<lambda>s t. Basic (g s t)))
 3. \<And>s. P s \<Longrightarrow> (?P4 and (\<lambda>_. True)) s
 4. \<And>s. s \<in> P' \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. ccorresG sr \<Gamma> dc xfdc ?P4 ?Q' hs (do do val <- getter;
setter val;
return val
od;
return ()
od) (call i f clean (\<lambda>s t. Basic (g s t)))
 2. \<And>s. P s \<Longrightarrow> (?P4 and (\<lambda>_. True)) s
 3. \<And>s. s \<in> P' \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. ccorresG sr \<Gamma> dc xfdc ?P4 ?Q' hs (do do val <- getter;
setter val;
return val
od;
return ()
od) (call i f clean (\<lambda>s t. Basic (g s t));;
SKIP)
 2. \<And>s. P s \<Longrightarrow> (?P4 and (\<lambda>_. True)) s
 3. \<And>s. s \<in> P' \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (7 subgoals):
 1. ccorresG sr \<Gamma> ?r'13 ?xf'13 ?P13 ?Q' [] (do val <- getter;
setter val;
return val
od) (call i f clean (\<lambda>s t. Basic (g s t)))
 2. \<And>rv' t t'. ceqv \<Gamma> ?xf'13 rv' t t' SKIP (?d'13 rv')
 3. \<And>rv rv'. ?r'13 rv rv' \<Longrightarrow> ccorresG sr \<Gamma> dc xfdc (?Q13 rv) (?Q'13 rv rv') hs (K_bind (return ()) rv) (?d'13 rv')
 4. \<lbrace>?R13\<rbrace> do val <- getter;
setter val;
return val
od \<lbrace>?Q13\<rbrace>
 5. guard_is_UNIV ?r'13 ?xf'13 ?Q'13
 6. \<And>s. P s \<Longrightarrow> (?P13 and ?R13 and (\<lambda>_. True)) s
 7. \<And>s. s \<in> P' \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (11 subgoals):
 1. ccorresG sr \<Gamma> ?r'19 ?xf'19 ?P13 (i ` ?Q') [] getter (Call f)
 2. \<And>x x' s t rv rv'. \<lbrakk>(x, t) \<in> sr; ?r'19 rv (?xf'19 t); (rv', x') \<in> fst (setter rv x)\<rbrakk> \<Longrightarrow> (x', g s t (clean s t)) \<in> sr
 3. \<And>s t rv. ?r'19 rv (?xf'19 t) \<Longrightarrow> ?r'13 rv (?xf'13 (g s t (clean s t)))
 4. \<And>x s. (x, s) \<in> sr \<Longrightarrow> (x, i s) \<in> sr
 5. \<And>val. empty_fail (setter val)
 6. \<And>rv' t t'. ceqv \<Gamma> ?xf'13 rv' t t' SKIP (?d'13 rv')
 7. \<And>rv rv'. ?r'13 rv rv' \<Longrightarrow> ccorresG sr \<Gamma> dc xfdc (?Q13 rv) (?Q'13 rv rv') hs (K_bind (return ()) rv) (?d'13 rv')
 8. \<lbrace>?R13\<rbrace> do val <- getter;
setter val;
return val
od \<lbrace>?Q13\<rbrace>
 9. guard_is_UNIV ?r'13 ?xf'13 ?Q'13
 10. \<And>s. P s \<Longrightarrow> (?P13 and ?R13 and (\<lambda>_. True)) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x x' s t rv rv'. \<lbrakk>(x, t) \<in> sr; r' rv (xf' t); (rv', x') \<in> fst (setter rv x)\<rbrakk> \<Longrightarrow> (x', g s t (clean s t)) \<in> sr
 2. \<And>s t rv. r' rv (xf' t) \<Longrightarrow> ?r'13 rv (?xf'13 (g s t (clean s t)))
 3. \<And>x s. (x, s) \<in> sr \<Longrightarrow> (x, i s) \<in> sr
 4. \<And>val. empty_fail (setter val)
 5. \<And>rv' t t'. ceqv \<Gamma> ?xf'13 rv' t t' SKIP (?d'13 rv')
 6. \<And>rv rv'. ?r'13 rv rv' \<Longrightarrow> ccorresG sr \<Gamma> dc xfdc (?Q13 rv) (?Q'13 rv rv') hs (K_bind (return ()) rv) (?d'13 rv')
 7. \<lbrace>?R13\<rbrace> do val <- getter;
setter val;
return val
od \<lbrace>?Q13\<rbrace>
 8. guard_is_UNIV ?r'13 ?xf'13 ?Q'13
 9. \<And>s. P s \<Longrightarrow> (P and ?R13 and (\<lambda>_. True)) s
 10. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' proof (prove)
goal (9 subgoals):
 1. \<And>s t rv. r' rv (xf' t) \<Longrightarrow> ?r'13 rv (?xf'13 (g s t (clean s t)))
 2. \<And>x s. (x, s) \<in> sr \<Longrightarrow> (x, i s) \<in> sr
 3. \<And>val. empty_fail (setter val)
 4. \<And>rv' t t'. ceqv \<Gamma> ?xf'13 rv' t t' SKIP (?d'13 rv')
 5. \<And>rv rv'. ?r'13 rv rv' \<Longrightarrow> ccorresG sr \<Gamma> dc xfdc (?Q13 rv) (?Q'13 rv rv') hs (K_bind (return ()) rv) (?d'13 rv')
 6. \<lbrace>?R13\<rbrace> do val <- getter;
setter val;
return val
od \<lbrace>?Q13\<rbrace>
 7. guard_is_UNIV ?r'13 ?xf'13 ?Q'13
 8. \<And>s. P s \<Longrightarrow> (P and ?R13 and (\<lambda>_. True)) s
 9. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' proof (prove)
goal (8 subgoals):
 1. \<And>x s. (x, s) \<in> sr \<Longrightarrow> (x, i s) \<in> sr
 2. \<And>val. empty_fail (setter val)
 3. \<And>rv' t t'. ceqv \<Gamma> (\<lambda>a. True) rv' t t' SKIP (?d'13 rv')
 4. \<And>rv rv'. rv' \<Longrightarrow> ccorresG sr \<Gamma> dc xfdc (?Q13 rv) (?Q'13 rv rv') hs (K_bind (return ()) rv) (?d'13 rv')
 5. \<lbrace>?R13\<rbrace> do val <- getter;
setter val;
return val
od \<lbrace>?Q13\<rbrace>
 6. guard_is_UNIV (\<lambda>a b. b) (\<lambda>a. True) ?Q'13
 7. \<And>s. P s \<Longrightarrow> (P and ?R13 and (\<lambda>_. True)) s
 8. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' proof (prove)
goal (7 subgoals):
 1. \<And>val. empty_fail (setter val)
 2. \<And>rv' t t'. ceqv \<Gamma> (\<lambda>a. True) rv' t t' SKIP (?d'13 rv')
 3. \<And>rv rv'. rv' \<Longrightarrow> ccorresG sr \<Gamma> dc xfdc (?Q13 rv) (?Q'13 rv rv') hs (K_bind (return ()) rv) (?d'13 rv')
 4. \<lbrace>?R13\<rbrace> do val <- getter;
setter val;
return val
od \<lbrace>?Q13\<rbrace>
 5. guard_is_UNIV (\<lambda>a b. b) (\<lambda>a. True) ?Q'13
 6. \<And>s. P s \<Longrightarrow> (P and ?R13 and (\<lambda>_. True)) s
 7. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' proof (prove)
goal (6 subgoals):
 1. \<And>rv' t t'. ceqv \<Gamma> (\<lambda>a. True) rv' t t' SKIP (?d'13 rv')
 2. \<And>rv rv'. rv' \<Longrightarrow> ccorresG sr \<Gamma> dc xfdc (?Q13 rv) (?Q'13 rv rv') hs (K_bind (return ()) rv) (?d'13 rv')
 3. \<lbrace>?R13\<rbrace> do val <- getter;
setter val;
return val
od \<lbrace>?Q13\<rbrace>
 4. guard_is_UNIV (\<lambda>a b. b) (\<lambda>a. True) ?Q'13
 5. \<And>s. P s \<Longrightarrow> (P and ?R13 and (\<lambda>_. True)) s
 6. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. rv' \<Longrightarrow> ccorresG sr \<Gamma> dc xfdc (?Q13 rv) (?Q'13 rv rv') hs (K_bind (return ()) rv) SKIP
 2. \<lbrace>?R13\<rbrace> do val <- getter;
setter val;
return val
od \<lbrace>?Q13\<rbrace>
 3. guard_is_UNIV (\<lambda>a b. b) (\<lambda>a. True) ?Q'13
 4. \<And>s. P s \<Longrightarrow> (P and ?R13 and (\<lambda>_. True)) s
 5. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' proof (prove)
goal (4 subgoals):
 1. \<lbrace>?R13\<rbrace> do val <- getter;
setter val;
return val
od \<lbrace>\<lambda>a b. True\<rbrace>
 2. guard_is_UNIV (\<lambda>a b. b) (\<lambda>a. True) (\<lambda>a b. UNIV)
 3. \<And>s. P s \<Longrightarrow> (P and ?R13 and (\<lambda>_. True)) s
 4. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' proof (prove)
goal (3 subgoals):
 1. guard_is_UNIV (\<lambda>a b. b) (\<lambda>a. True) (\<lambda>a b. UNIV)
 2. \<And>s. P s \<Longrightarrow> (P and (\<lambda>_. True) and (\<lambda>_. True)) s
 3. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> (P and (\<lambda>_. True) and (\<lambda>_. True)) s
 2. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' proof (prove)
goal:
No subgoals!