theory Corres_UL_C

lemma ccorres_symb_exec_r:
  assumes cul: "ccorres_underlying sr E r xf arrel axf R Q' hs a y"
  and     ex:  "E \<turnstile> R' m Q', {}"
  and   pres:  "\<And>s. R s \<Longrightarrow> E \<turnstile> (R' \<inter> {s'. (s, s') \<in> sr}) m {s'. (s, s') \<in> sr}"
  shows "ccorres_underlying sr E r xf arrel axf R R' hs a (m ;; y)" apply - apply (rule ccorres_guard_imp) apply (subst return_bind [symmetric, where f = "\<lambda>x. a"], rule ccorres_split_nothrow') apply (rule ccorres_return [where r = "\<lambda>x y. True"]) apply (drule pres, simp) apply (rule ccorres_guard_imp) apply (rule cul) apply assumption apply simp apply wp apply (rule ex) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr E r xf arrel axf R R' hs a (m;;
y) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr E r xf arrel axf R R' hs a (m;;
y) proof (prove)
goal (3 subgoals):
 1. ccorres_underlying sr E r xf arrel axf ?Q ?Q' hs a (m;;
y)
 2. \<And>s. R s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> R' \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (6 subgoals):
 1. ccorres_underlying sr E ?r'7 ?xf'7 dc axf ?P7 ?P'7 hs (return ?x5) m
 2. \<And>x. ccorres_underlying sr E r xf arrel axf (?Q7 x) (?Q'7 \<inter> {s. ?r'7 x (?xf'7 s)}) hs a y
 3. \<lbrace>?R7\<rbrace> return ?x5 \<lbrace>?Q7\<rbrace>
 4. E\<turnstile>\<^bsub>/?F7\<^esub> ?R'7 m ?Q'7
 5. \<And>s. R s \<Longrightarrow> (?P7 and ?R7) s
 6. \<And>s. s \<in> R' \<Longrightarrow> s \<in> ?P'7 \<inter> ?R'7 proof (prove)
goal (6 subgoals):
 1. \<And>s. ?P7 s \<Longrightarrow> E\<turnstile> (?P'7 \<inter> {s'. (s, s') \<in> sr}) m {s'. (s, s') \<in> sr \<and> True}
 2. \<And>x. ccorres_underlying sr E r xf arrel axf (?Q7 x) (?Q'7 \<inter> \<lbrace>True\<rbrace>) hs a y
 3. \<lbrace>?R7\<rbrace> return ?x5 \<lbrace>?Q7\<rbrace>
 4. E\<turnstile>\<^bsub>/?F7\<^esub> ?R'7 m ?Q'7
 5. \<And>s. R s \<Longrightarrow> (?P7 and ?R7) s
 6. \<And>s. s \<in> R' \<Longrightarrow> s \<in> ?P'7 \<inter> ?R'7 proof (prove)
goal (5 subgoals):
 1. \<And>x. ccorres_underlying sr E r xf arrel axf (?Q7 x) (?Q'7 \<inter> \<lbrace>True\<rbrace>) hs a y
 2. \<lbrace>?R7\<rbrace> return ?x5 \<lbrace>?Q7\<rbrace>
 3. E\<turnstile>\<^bsub>/?F7\<^esub> ?R'7 m ?Q'7
 4. \<And>s. R s \<Longrightarrow> (R and ?R7) s
 5. \<And>s. s \<in> R' \<Longrightarrow> s \<in> R' \<inter> ?R'7 proof (prove)
goal (7 subgoals):
 1. \<And>x. ccorres_underlying sr E r xf arrel axf (?Q16 x) (?Q'16 x) hs a y
 2. \<And>x s. ?Q7 x s \<Longrightarrow> ?Q16 x s
 3. \<And>x s. s \<in> ?Q'7 \<inter> \<lbrace>True\<rbrace> \<Longrightarrow> s \<in> ?Q'16 x
 4. \<lbrace>?R7\<rbrace> return ?x5 \<lbrace>?Q7\<rbrace>
 5. E\<turnstile>\<^bsub>/?F7\<^esub> ?R'7 m ?Q'7
 6. \<And>s. R s \<Longrightarrow> (R and ?R7) s
 7. \<And>s. s \<in> R' \<Longrightarrow> s \<in> R' \<inter> ?R'7 proof (prove)
goal (6 subgoals):
 1. \<And>x s. ?Q7 x s \<Longrightarrow> R s
 2. \<And>x s. s \<in> ?Q'7 \<inter> \<lbrace>True\<rbrace> \<Longrightarrow> s \<in> Q'
 3. \<lbrace>?R7\<rbrace> return ?x5 \<lbrace>?Q7\<rbrace>
 4. E\<turnstile>\<^bsub>/?F7\<^esub> ?R'7 m ?Q'7
 5. \<And>s. R s \<Longrightarrow> (R and ?R7) s
 6. \<And>s. s \<in> R' \<Longrightarrow> s \<in> R' \<inter> ?R'7 proof (prove)
goal (5 subgoals):
 1. \<And>x s. s \<in> ?Q'7 \<inter> \<lbrace>True\<rbrace> \<Longrightarrow> s \<in> Q'
 2. \<lbrace>?R7\<rbrace> return ?x5 \<lbrace>\<lambda>x. R\<rbrace>
 3. E\<turnstile>\<^bsub>/?F7\<^esub> ?R'7 m ?Q'7
 4. \<And>s. R s \<Longrightarrow> (R and ?R7) s
 5. \<And>s. s \<in> R' \<Longrightarrow> s \<in> R' \<inter> ?R'7 proof (prove)
goal (4 subgoals):
 1. \<lbrace>?R7\<rbrace> return ?x5 \<lbrace>\<lambda>x. R\<rbrace>
 2. E\<turnstile>\<^bsub>/?F7\<^esub> ?R'7 m Q'
 3. \<And>s. R s \<Longrightarrow> (R and ?R7) s
 4. \<And>s. s \<in> R' \<Longrightarrow> s \<in> R' \<inter> ?R'7 proof (prove)
goal (3 subgoals):
 1. E\<turnstile>\<^bsub>/?F7\<^esub> ?R'7 m Q'
 2. \<And>s. R s \<Longrightarrow> (R and R) s
 3. \<And>s. s \<in> R' \<Longrightarrow> s \<in> R' \<inter> ?R'7 proof (prove)
goal (2 subgoals):
 1. \<And>s. R s \<Longrightarrow> (R and R) s
 2. \<And>s. s \<in> R' \<Longrightarrow> s \<in> R' \<inter> R' proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> R' \<Longrightarrow> s \<in> R' \<inter> R' proof (prove)
goal:
No subgoals!