theory Corres_D

lemma split_return_throw_thingy:
  "\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>,\<lbrace>\<lambda>ft. (=) s\<rbrace>;
     \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv);
        nf' \<Longrightarrow> no_fail P' g \<rbrakk>
     \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P'
             (f \<sqinter> throwError e) (g >>=E h)" apply (simp add: bindE_def) apply (rule corres_guard_imp) apply (rule_tac Q'="\<lambda>rv. P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))"
               in corres_symb_exec_r[where P=P and P'=P'], simp_all) apply (case_tac rv) apply (simp add: lift_def) apply (rule corres_alternate2, simp) apply (rule corres_gen_asm2) apply (simp add: lift_def isRight_def) apply (clarsimp simp add: validE_def valid_def) apply (erule meta_allE, drule(1) bspec) apply (auto simp: isRight_def split: sum.split_asm)[1] apply (simp add: validE_def) apply (rule hoare_strengthen_post, assumption) apply (simp split: sum.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (g >>=E h) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (g >>= lift h) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) ?Q ?Q' (f \<sqinter> throwError e) (g >>= lift h)
 2. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. \<And>rv. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P (P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))) (f \<sqinter> throwError e) (lift h rv)
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>rv. P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))\<rbrace>
 3. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv a. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; rv = Inl a\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P (P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))) (f \<sqinter> throwError e) (lift h rv)
 2. \<And>rv b. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; rv = Inr b\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P (P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))) (f \<sqinter> throwError e) (lift h rv)
 3. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>rv. P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))\<rbrace>
 4. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv a. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; rv = Inl a\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (throwError a)
 2. \<And>rv b. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; rv = Inr b\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P (P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))) (f \<sqinter> throwError e) (lift h rv)
 3. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>rv. P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))\<rbrace>
 4. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv b. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; rv = Inr b\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P (P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))) (f \<sqinter> throwError e) (lift h rv)
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>rv. P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))\<rbrace>
 3. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv b. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; rv = Inr b; isRight rv \<longrightarrow> rvP (theRight rv)\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (lift h rv)
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>rv. P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))\<rbrace>
 3. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>rv. P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))\<rbrace>
 2. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>s. \<forall>x\<in>fst (g s). case x of (Inl e, s') \<Rightarrow> s = s' | (Inr ra, s') \<Rightarrow> s' = s \<and> rvP ra; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s; (a, b) \<in> fst (g s)\<rbrakk> \<Longrightarrow> P' b \<and> (isRight a \<longrightarrow> rvP (theRight a))
 2. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s; (a, b) \<in> fst (g s); case (a, b) of (Inl e, s') \<Rightarrow> s = s' | (Inr ra, s') \<Rightarrow> s' = s \<and> rvP ra\<rbrakk> \<Longrightarrow> P' b \<and> (isRight a \<longrightarrow> rvP (theRight a))
 2. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>v sa. case v of Inl e \<Rightarrow> s = sa | Inr r \<Rightarrow> sa = s \<and> rvP r\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>v sa. case v of Inl e \<Rightarrow> s = sa | Inr r \<Rightarrow> sa = s \<and> rvP r\<rbrace>; \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); nf' \<Longrightarrow> no_fail P' g; P' s; case rv of Inl e \<Rightarrow> s = sa | Inr r \<Rightarrow> sa = s \<and> rvP r\<rbrakk> \<Longrightarrow> s = sa proof (prove)
goal:
No subgoals!