[STATEMENT]
lemma inline_left_gpv_merge_exception_converter:
  "bind_gpv (inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpv))) merge_exception_converter) (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) =
   bind_gpv (left_gpv (map_gpv' id id option_of_exception (gpv_stop gpv))) (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpv))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) = left_gpv (map_gpv' id id option_of_exception (gpv_stop gpv)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))
[PROOF STEP]
apply(coinduction arbitrary: gpv rule: gpv.coinduct_strong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>gpva. rel_spmf (rel_generat (=) (=) (rel_fun (=) (\<lambda>gpv gpv'. (\<exists>gpva. gpv = inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpva))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<and> gpv' = left_gpv (map_gpv' id id option_of_exception (gpv_stop gpva)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))) \<or> gpv = gpv'))) (the_gpv (inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpva))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')))) (the_gpv (left_gpv (map_gpv' id id option_of_exception (gpv_stop gpva)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))))
[PROOF STEP]
apply(simp add: bind_gpv.sel inline_sel map_bind_spmf bind_map_spmf del: bind_gpv_sel')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>gpva. rel_spmf (rel_generat (=) (=) (rel_fun (=) (\<lambda>gpv gpv'. (\<exists>gpva. gpv = inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpva))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<and> gpv' = left_gpv (map_gpv' id id option_of_exception (gpv_stop gpva)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))) \<or> gpv = gpv'))) (inline1 run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpva))) merge_exception_converter \<bind> map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')))))) \<circ> (case_generat (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (case x of (x, conv') \<Rightarrow> case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')))) (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))) \<circ> case_sum Pure (\<lambda>(out, oracle, rpv). IO out (\<lambda>input. oracle input \<bind> (\<lambda>(x, y). inline run_converter (rpv x) y))))) (the_gpv gpva \<bind> map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter)))))) \<circ> (case_generat (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter)))) (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))) \<circ> map_generat id Inl left_rpv \<circ> map_generat id id (map_fun option_of_exception (map_gpv' id id option_of_exception)) \<circ> map_generat Some id (\<lambda>rpv. case_option (Done None) (\<lambda>input'. gpv_stop (rpv input')))))
[PROOF STEP]
apply(subst inline1_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>gpva. rel_spmf (rel_generat (=) (=) (rel_fun (=) (\<lambda>gpv gpv'. (\<exists>gpva. gpv = inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpva))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<and> gpv' = left_gpv (map_gpv' id id option_of_exception (gpv_stop gpva)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))) \<or> gpv = gpv'))) (the_gpv (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpva))) \<bind> case_generat (\<lambda>x. return_spmf (Inl (x, merge_exception_converter))) (\<lambda>out rpv. the_gpv (run_converter merge_exception_converter out) \<bind> case_generat (\<lambda>(x, y). inline1 run_converter (rpv x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', rpv)))) \<bind> map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')))))) \<circ> (case_generat (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (case x of (x, conv') \<Rightarrow> case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')))) (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))) \<circ> case_sum Pure (\<lambda>(out, oracle, rpv). IO out (\<lambda>input. oracle input \<bind> (\<lambda>(x, y). inline run_converter (rpv x) y))))) (the_gpv gpva \<bind> map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter)))))) \<circ> (case_generat (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter)))) (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))) \<circ> map_generat id Inl left_rpv \<circ> map_generat id id (map_fun option_of_exception (map_gpv' id id option_of_exception)) \<circ> map_generat Some id (\<lambda>rpv. case_option (Done None) (\<lambda>input'. gpv_stop (rpv input')))))
[PROOF STEP]
apply(clarsimp simp add: bind_map_spmf intro!: rel_spmf_bind_reflI simp add: generat.map_comp case_map_generat o_def split!: generat.split intro!: rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>gpva out' c' y. \<lbrakk>IO out' c' \<in> set_spmf (the_gpv gpva); (case case merge_exception y of Fault \<Rightarrow> (Fault, const_converter Fault) | OK y' \<Rightarrow> (OK y', merge_exception_converter) of (x, xa) \<Rightarrow> inline run_converter (map_gpv' id id option_of_exception (case x of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (left_rpv c' input'))) xa) \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<noteq> left_rpv (\<lambda>input'. map_gpv' id id option_of_exception (case input' of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (c' input'))) y \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))\<rbrakk> \<Longrightarrow> \<exists>gpv. (case case merge_exception y of Fault \<Rightarrow> (Fault, const_converter Fault) | OK y' \<Rightarrow> (OK y', merge_exception_converter) of (x, xa) \<Rightarrow> inline run_converter (map_gpv' id id option_of_exception (case x of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (left_rpv c' input'))) xa) \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) = inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpv))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<and> left_rpv (\<lambda>input'. map_gpv' id id option_of_exception (case input' of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (c' input'))) y \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter)) = left_gpv (map_gpv' id id option_of_exception (gpv_stop gpv)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))
[PROOF STEP]
subgoal for gpv out c input
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IO out c \<in> set_spmf (the_gpv gpv); (case case merge_exception input of Fault \<Rightarrow> (Fault, const_converter Fault) | OK y' \<Rightarrow> (OK y', merge_exception_converter) of (x, xa) \<Rightarrow> inline run_converter (map_gpv' id id option_of_exception (case x of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (left_rpv c input'))) xa) \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<noteq> left_rpv (\<lambda>input'. map_gpv' id id option_of_exception (case input' of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (c input'))) input \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))\<rbrakk> \<Longrightarrow> \<exists>gpv. (case case merge_exception input of Fault \<Rightarrow> (Fault, const_converter Fault) | OK y' \<Rightarrow> (OK y', merge_exception_converter) of (x, xa) \<Rightarrow> inline run_converter (map_gpv' id id option_of_exception (case x of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (left_rpv c input'))) xa) \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) = inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpv))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<and> left_rpv (\<lambda>input'. map_gpv' id id option_of_exception (case input' of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (c input'))) input \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter)) = left_gpv (map_gpv' id id option_of_exception (gpv_stop gpv)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))
[PROOF STEP]
by(cases input; auto split!: exception.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done