theory Corres_UL_C

lemma ccorres_to_vcg_with_prop:
  "\<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a; \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>\<rbrakk>
   \<Longrightarrow> \<Gamma> \<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel}
           c {t'. \<exists>(rv, t) \<in> fst (a s). (t, t') \<in> srel \<and> rrel rv (xf t') \<and> R rv t}" apply (rule hoare_complete) apply (clarsimp simp: HoarePartialDef.valid_def cvalid_def no_fail_def) apply (drule_tac x=s in spec) apply clarsimp apply (frule (5) ccorres_empty_handler_abrupt) apply (fastforce elim!: ccorresE EHOther simp: unif_rrel_simps valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a; \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c {t'. \<exists>(rv, t)\<in>fst (a s). (t, t') \<in> srel \<and> rrel rv (xf t') \<and> R rv t} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a; \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/{}\<^esub> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c {t'. \<exists>(rv, t)\<in>fst (a s). (t, t') \<in> srel \<and> rrel rv (xf t') \<and> R rv t},{} proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; \<forall>s. Q s \<longrightarrow> \<not> snd (a s); \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P s; Q s; x \<in> P'; (s, x) \<in> srel\<rbrakk> \<Longrightarrow> t \<in> Normal ` {t'. \<exists>x\<in>fst (a s). case x of (rv, t) \<Rightarrow> (t, t') \<in> srel \<and> rrel rv (xf t') \<and> R rv t} proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P s; Q s; x \<in> P'; (s, x) \<in> srel; Q s \<longrightarrow> \<not> snd (a s)\<rbrakk> \<Longrightarrow> t \<in> Normal ` {t'. \<exists>x\<in>fst (a s). case x of (rv, t) \<Rightarrow> (t, t') \<in> srel \<and> rrel rv (xf t') \<and> R rv t} proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P s; Q s; x \<in> P'; (s, x) \<in> srel; \<not> snd (a s)\<rbrakk> \<Longrightarrow> t \<in> Normal ` {t'. \<exists>x\<in>fst (a s). case x of (rv, t) \<Rightarrow> (t, t') \<in> srel \<and> rrel rv (xf t') \<and> R rv t} proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P s; Q s; x \<in> P'; (s, x) \<in> srel; \<not> snd (a s); \<not> isAbr t\<rbrakk> \<Longrightarrow> t \<in> Normal ` {t'. \<exists>x\<in>fst (a s). case x of (rv, t) \<Rightarrow> (t, t') \<in> srel \<and> rrel rv (xf t') \<and> R rv t} proof (prove)
goal:
No subgoals!