theory Corres_D

lemma corres_return_throw_thingy:
  "\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> Q rv\<rbrace>,\<lbrace>\<lambda>ft. (=) s\<rbrace>;
        nf' \<Longrightarrow> no_fail P' g; \<forall>rv. Q rv \<longrightarrow> r v rv \<rbrakk>
     \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P'
             (returnOk v \<sqinter> throwError e) (g)" apply (subst lift_returnOk_bind_triv[where g=g, symmetric]) apply (fold bindE_def, rule split_return_throw_thingy) apply assumption apply (rule corres_alternate1) apply (clarsimp simp: returnOk_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> Q rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; \<forall>rv. Q rv \<longrightarrow> r v rv\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (returnOk v \<sqinter> throwError e) g proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> Q rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; \<forall>rv. Q rv \<longrightarrow> r v rv\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (returnOk v \<sqinter> throwError e) (g >>= lift returnOk) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> Q rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; \<forall>rv. Q rv \<longrightarrow> r v rv\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> ?rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>
 2. \<And>rv. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> Q rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; \<forall>rv. Q rv \<longrightarrow> r v rv; ?rvP rv\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (returnOk v \<sqinter> throwError e) (returnOk rv)
 3. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> Q rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; \<forall>rv. Q rv \<longrightarrow> r v rv; nf'\<rbrakk> \<Longrightarrow> no_fail P' g proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> Q rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; \<forall>rv. Q rv \<longrightarrow> r v rv; Q rv\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (returnOk v \<sqinter> throwError e) (returnOk rv)
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> Q rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; \<forall>rv. Q rv \<longrightarrow> r v rv; nf'\<rbrakk> \<Longrightarrow> no_fail P' g proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> Q rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; \<forall>rv. Q rv \<longrightarrow> r v rv; Q rv\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (returnOk v) (returnOk rv)
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> Q rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; \<forall>rv. Q rv \<longrightarrow> r v rv; nf'\<rbrakk> \<Longrightarrow> no_fail P' g proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> Q rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; \<forall>rv. Q rv \<longrightarrow> r v rv; nf'\<rbrakk> \<Longrightarrow> no_fail P' g proof (prove)
goal:
No subgoals!