[STATEMENT]
lemma INF_mono_lfp [partial_function_mono]:
  "(\<And>x. lfp.mono_body (\<lambda>f. F f x)) \<Longrightarrow> lfp.mono_body (\<lambda>f. INF x\<in>M. F f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. monotone lfp.le_fun (\<le>) (\<lambda>f. F f x)) \<Longrightarrow> monotone lfp.le_fun (\<le>) (\<lambda>f. \<Sqinter> (F f ` M))
[PROOF STEP]
by(rule monotoneI)(blast dest: monotoneD intro: INF_mono)


[STATEMENT]
lemma monotone_ennreal_add1: "monotone (\<le>) (\<le>) (\<lambda>x. x + y :: ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>x. x + y)
[PROOF STEP]
by(auto intro!: monotoneI)


[STATEMENT]
lemma monotone_ennreal_add2: "monotone (\<le>) (\<le>) (\<lambda>y. x + y :: ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono ((+) x)
[PROOF STEP]
by(auto intro!: monotoneI)


[STATEMENT]
lemma mono2mono_ennreal_add[THEN lfp.mono2mono2, cont_intro, simp]:
  shows monotone_eadd: "monotone (rel_prod (\<le>) (\<le>)) (\<le>) (\<lambda>(x, y). x + y :: ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (rel_prod (\<le>) (\<le>)) (\<le>) (\<lambda>(x, y). x + y)
[PROOF STEP]
by(simp add: monotone_ennreal_add1 monotone_ennreal_add2)


[STATEMENT]
lemma ennreal_add_partial_function_mono [partial_function_mono]:
  "\<lbrakk> monotone (fun_ord (\<le>)) (\<le>) f; monotone (fun_ord (\<le>)) (\<le>) g \<rbrakk>
  \<Longrightarrow> monotone (fun_ord (\<le>)) (\<le>) (\<lambda>x. f x + g x :: ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monotone (fun_ord (\<le>)) (\<le>) f; monotone (fun_ord (\<le>)) (\<le>) g\<rbrakk> \<Longrightarrow> monotone (fun_ord (\<le>)) (\<le>) (\<lambda>x. f x + g x)
[PROOF STEP]
by(rule mono2mono_ennreal_add)


[STATEMENT]
lemma expectation_gpv_fixp_induct [case_names adm bottom step]:
  assumes "lfp.admissible P"
    and "P (\<lambda>_. 0)"
    and "\<And>expectation_gpv'. \<lbrakk> \<And>gpv. expectation_gpv' gpv \<le> expectation_gpv gpv; P expectation_gpv' \<rbrakk> \<Longrightarrow>
         P (\<lambda>gpv. (\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> INF r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv)) + fail * pmf (the_gpv gpv) None)"
  shows "P expectation_gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P local.expectation_gpv
[PROOF STEP]
by(rule expectation_gpv.fixp_induct)(simp_all add: bot_ennreal_def assms fun_ord_def)


[STATEMENT]
lemma expectation_gpv_Done [simp]: "expectation_gpv (Done x) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.expectation_gpv (Generative_Probabilistic_Value.Done x) = f x
[PROOF STEP]
by(subst expectation_gpv.simps)(simp add: measure_spmf_return_spmf nn_integral_return)


[STATEMENT]
lemma expectation_gpv_Fail [simp]: "expectation_gpv Fail = fail"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.expectation_gpv Fail = fail
[PROOF STEP]
by(subst expectation_gpv.simps) simp


[STATEMENT]
lemma expectation_gpv_lift_spmf [simp]:
  "expectation_gpv (lift_spmf p) = (\<integral>\<^sup>+ x. f x \<partial>measure_spmf p) + fail * pmf p None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.expectation_gpv (lift_spmf p) = integral\<^sup>N (measure_spmf p) f + fail * ennreal (pmf p None)
[PROOF STEP]
by(subst expectation_gpv.simps)(auto simp add: o_def pmf_map vimage_def measure_pmf_single)


[STATEMENT]
lemma expectation_gpv_Pause [simp]:
  "expectation_gpv (Pause out c) = (INF r\<in>responses_\<I> \<I> out. expectation_gpv (c r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.expectation_gpv (Generative_Probabilistic_Value.Pause out c) = (\<Sqinter>r\<in>responses_\<I> \<I> out. local.expectation_gpv (c r))
[PROOF STEP]
by(subst expectation_gpv.simps)(simp add: measure_spmf_return_spmf nn_integral_return)


[STATEMENT]
lemma expectation_gpv_parametric':
  includes lifting_syntax notes weight_spmf'_parametric[transfer_rule]
  shows "((=) ===> rel_\<I> C R ===> (A ===> (=)) ===> rel_gpv'' A C R ===> (=)) expectation_gpv expectation_gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> rel_\<I> C R ===> (A ===> (=)) ===> rel_gpv'' A C R ===> (=)) expectation_gpv expectation_gpv
[PROOF STEP]
unfolding expectation_gpv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> rel_\<I> C R ===> (A ===> (=)) ===> rel_gpv'' A C R ===> (=)) (\<lambda>fail \<I> f. lfp.fixp_fun (\<lambda>expectation_gpv gpv. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None))) (\<lambda>fail \<I> f. lfp.fixp_fun (\<lambda>expectation_gpv gpv. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None)))
[PROOF STEP]
apply(rule rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x = y \<Longrightarrow> (rel_\<I> C R ===> (A ===> (=)) ===> rel_gpv'' A C R ===> (=)) (\<lambda>\<I> f. lfp.fixp_fun (\<lambda>expectation_gpv gpv. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv (c r)) \<partial>measure_spmf (the_gpv gpv) + x * ennreal (pmf (the_gpv gpv) None))) (\<lambda>\<I> f. lfp.fixp_fun (\<lambda>expectation_gpv gpv. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv (c r)) \<partial>measure_spmf (the_gpv gpv) + y * ennreal (pmf (the_gpv gpv) None)))
[PROOF STEP]
apply(rule rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; rel_\<I> C R xa ya\<rbrakk> \<Longrightarrow> ((A ===> (=)) ===> rel_gpv'' A C R ===> (=)) (\<lambda>f. lfp.fixp_fun (\<lambda>expectation_gpv gpv. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> xa out. expectation_gpv (c r)) \<partial>measure_spmf (the_gpv gpv) + x * ennreal (pmf (the_gpv gpv) None))) (\<lambda>f. lfp.fixp_fun (\<lambda>expectation_gpv gpv. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> ya out. expectation_gpv (c r)) \<partial>measure_spmf (the_gpv gpv) + y * ennreal (pmf (the_gpv gpv) None)))
[PROOF STEP]
apply(rule rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya xb yb. \<lbrakk>x = y; rel_\<I> C R xa ya; (A ===> (=)) xb yb\<rbrakk> \<Longrightarrow> (rel_gpv'' A C R ===> (=)) (lfp.fixp_fun (\<lambda>expectation_gpv gpv. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> xb x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> xa out. expectation_gpv (c r)) \<partial>measure_spmf (the_gpv gpv) + x * ennreal (pmf (the_gpv gpv) None))) (lfp.fixp_fun (\<lambda>expectation_gpv gpv. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> yb x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> ya out. expectation_gpv (c r)) \<partial>measure_spmf (the_gpv gpv) + y * ennreal (pmf (the_gpv gpv) None)))
[PROOF STEP]
apply(rule fixp_lfp_parametric_eq[OF expectation_gpv.mono expectation_gpv.mono])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya xb yb. \<lbrakk>x = y; rel_\<I> C R xa ya; (A ===> (=)) xb yb\<rbrakk> \<Longrightarrow> ((rel_gpv'' A C R ===> (=)) ===> rel_gpv'' A C R ===> (=)) (\<lambda>expectation_gpv xc. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> xb x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> xa out. expectation_gpv (c r)) \<partial>measure_spmf (the_gpv xc) + x * ennreal (pmf (the_gpv xc) None)) (\<lambda>expectation_gpv x. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> yb x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> ya out. expectation_gpv (c r)) \<partial>measure_spmf (the_gpv x) + y * ennreal (pmf (the_gpv x) None))
[PROOF STEP]
apply(fold nn_integral_spmf_def Set.is_empty_def pmf_None_eq_weight_spmf[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya xb yb. \<lbrakk>x = y; rel_\<I> C R xa ya; (A ===> (=)) xb yb\<rbrakk> \<Longrightarrow> ((rel_gpv'' A C R ===> (=)) ===> rel_gpv'' A C R ===> (=)) (\<lambda>expectation_gpv xc. nn_integral_spmf (the_gpv xc) (\<lambda>generat. case generat of Pure x \<Rightarrow> xb x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> xa out. expectation_gpv (c r)) + x * ennreal (1 - weight_spmf (the_gpv xc))) (\<lambda>expectation_gpv x. nn_integral_spmf (the_gpv x) (\<lambda>generat. case generat of Pure x \<Rightarrow> yb x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> ya out. expectation_gpv (c r)) + y * ennreal (1 - weight_spmf (the_gpv x)))
[PROOF STEP]
apply(simp only: weight_spmf'_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya xb yb. \<lbrakk>x = y; rel_\<I> C R xa ya; (A ===> (=)) xb yb\<rbrakk> \<Longrightarrow> ((rel_gpv'' A C R ===> (=)) ===> rel_gpv'' A C R ===> (=)) (\<lambda>expectation_gpv x. nn_integral_spmf (the_gpv x) (\<lambda>generat. case generat of Pure x \<Rightarrow> xb x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> xa out. expectation_gpv (c r)) + y * ennreal (1 - weight_spmf' (the_gpv x))) (\<lambda>expectation_gpv x. nn_integral_spmf (the_gpv x) (\<lambda>generat. case generat of Pure x \<Rightarrow> yb x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> ya out. expectation_gpv (c r)) + y * ennreal (1 - weight_spmf' (the_gpv x)))
[PROOF STEP]
subgoal premises [transfer_rule]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((rel_gpv'' A C R ===> (=)) ===> rel_gpv'' A C R ===> (=)) (\<lambda>expectation_gpv x. nn_integral_spmf (the_gpv x) (\<lambda>generat. case generat of Pure x \<Rightarrow> xb_ x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> xa_ out. expectation_gpv (c r)) + y_ * ennreal (1 - weight_spmf' (the_gpv x))) (\<lambda>expectation_gpv x. nn_integral_spmf (the_gpv x) (\<lambda>generat. case generat of Pure x \<Rightarrow> yb_ x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> ya_ out. expectation_gpv (c r)) + y_ * ennreal (1 - weight_spmf' (the_gpv x)))
[PROOF STEP]
supply the_gpv_parametric'[transfer_rule]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((rel_gpv'' A C R ===> (=)) ===> rel_gpv'' A C R ===> (=)) (\<lambda>expectation_gpv x. nn_integral_spmf (the_gpv x) (\<lambda>generat. case generat of Pure x \<Rightarrow> xb_ x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> xa_ out. expectation_gpv (c r)) + y_ * ennreal (1 - weight_spmf' (the_gpv x))) (\<lambda>expectation_gpv x. nn_integral_spmf (the_gpv x) (\<lambda>generat. case generat of Pure x \<Rightarrow> yb_ x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> ya_ out. expectation_gpv (c r)) + y_ * ennreal (1 - weight_spmf' (the_gpv x)))
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma expectation_gpv_parametric [transfer_rule]:
  includes lifting_syntax
  shows "((=) ===> rel_\<I> C (=) ===> (A ===> (=)) ===> rel_gpv A C ===> (=)) expectation_gpv expectation_gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> rel_\<I> C (=) ===> (A ===> (=)) ===> rel_gpv A C ===> (=)) expectation_gpv expectation_gpv
[PROOF STEP]
using expectation_gpv_parametric'[of C "(=)" A]
[PROOF STATE]
proof (prove)
using this:
((=) ===> rel_\<I> C (=) ===> (A ===> (=)) ===> rel_gpv'' A C (=) ===> (=)) expectation_gpv expectation_gpv

goal (1 subgoal):
 1. ((=) ===> rel_\<I> C (=) ===> (A ===> (=)) ===> rel_gpv A C ===> (=)) expectation_gpv expectation_gpv
[PROOF STEP]
by(simp add: rel_gpv_conv_rel_gpv'')


[STATEMENT]
lemma expectation_gpv_cong:
  fixes fail fail'
  assumes fail: "fail = fail'"
  and \<I>: "\<I> = \<I>'"
  and gpv: "gpv = gpv'"
  and f: "\<And>x. x \<in> results_gpv \<I>' gpv' \<Longrightarrow> f x = g x"
  shows "expectation_gpv fail \<I> f gpv = expectation_gpv fail' \<I>' g gpv'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv = expectation_gpv fail' \<I>' g gpv'
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
?x \<in> results_gpv \<I>' gpv' \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv = expectation_gpv fail' \<I>' g gpv'
[PROOF STEP]
unfolding \<I>[symmetric] gpv[symmetric] fail[symmetric]
[PROOF STATE]
proof (prove)
using this:
?x \<in> results_gpv \<I> gpv \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv = expectation_gpv fail \<I> g gpv
[PROOF STEP]
proof(induction arbitrary: gpv rule: parallel_fixp_induct_1_1[OF complete_lattice_partial_function_definitions complete_lattice_partial_function_definitions expectation_gpv.mono expectation_gpv.mono expectation_gpv_def expectation_gpv_def, case_names adm bottom step])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. (\<forall>x. x \<in> results_gpv \<I> xa \<longrightarrow> f x = g x) \<longrightarrow> fst x xa = snd x xa)
 2. \<And>gpv. (\<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x) \<Longrightarrow> \<Squnion> {} = \<Squnion> {}
 3. \<And>fa ga gpv. \<lbrakk>\<And>gpv. (\<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x) \<Longrightarrow> fa gpv = ga gpv; \<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat g (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. ga (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. (\<forall>x. x \<in> results_gpv \<I> xa \<longrightarrow> f x = g x) \<longrightarrow> fst x xa = snd x xa)
 2. \<And>gpv. (\<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x) \<Longrightarrow> \<Squnion> {} = \<Squnion> {}
 3. \<And>fa ga gpv. \<lbrakk>\<And>gpv. (\<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x) \<Longrightarrow> fa gpv = ga gpv; \<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat g (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. ga (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. (\<forall>x. x \<in> results_gpv \<I> xa \<longrightarrow> f x = g x) \<longrightarrow> fst x xa = snd x xa)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. (\<forall>x. x \<in> results_gpv \<I> xa \<longrightarrow> f x = g x) \<longrightarrow> fst x xa = snd x xa)

goal (2 subgoals):
 1. \<And>gpv. (\<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x) \<Longrightarrow> \<Squnion> {} = \<Squnion> {}
 2. \<And>fa ga gpv. \<lbrakk>\<And>gpv. (\<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x) \<Longrightarrow> fa gpv = ga gpv; \<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat g (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. ga (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:
?x \<in> results_gpv \<I> gpv \<Longrightarrow> f ?x = g ?x

goal (2 subgoals):
 1. \<And>gpv. (\<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x) \<Longrightarrow> \<Squnion> {} = \<Squnion> {}
 2. \<And>fa ga gpv. \<lbrakk>\<And>gpv. (\<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x) \<Longrightarrow> fa gpv = ga gpv; \<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat g (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. ga (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> {} = \<Squnion> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Squnion> {} = \<Squnion> {}

goal (1 subgoal):
 1. \<And>fa ga gpv. \<lbrakk>\<And>gpv. (\<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x) \<Longrightarrow> fa gpv = ga gpv; \<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat g (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. ga (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case (step expectation_gpv' expectation_gpv'')
[PROOF STATE]
proof (state)
this:
(\<And>x. x \<in> results_gpv \<I> ?gpv \<Longrightarrow> f x = g x) \<Longrightarrow> expectation_gpv' ?gpv = expectation_gpv'' ?gpv
?x \<in> results_gpv \<I> gpv \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. \<And>fa ga gpv. \<lbrakk>\<And>gpv. (\<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x) \<Longrightarrow> fa gpv = ga gpv; \<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat g (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. ga (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) = \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> g x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
by(rule arg_cong2[where f="(+)"] nn_integral_cong_AE)+(clarsimp simp add: step.prems results_gpv.intros split!: generat.split intro!: INF_cong[OF refl] step.IH)+
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) = \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> g x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expectation_gpv_cong_fail:
  "colossless_gpv \<I> gpv \<Longrightarrow> expectation_gpv fail \<I> f gpv = expectation_gpv fail' \<I> f gpv" for fail
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. colossless_gpv \<I> gpv \<Longrightarrow> expectation_gpv fail \<I> f gpv = expectation_gpv fail' \<I> f gpv
[PROOF STEP]
proof(induction arbitrary: gpv rule: parallel_fixp_induct_1_1[OF complete_lattice_partial_function_definitions complete_lattice_partial_function_definitions expectation_gpv.mono expectation_gpv.mono expectation_gpv_def expectation_gpv_def, case_names adm bottom step])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. colossless_gpv \<I> xa \<longrightarrow> fst x xa = snd x xa)
 2. \<And>gpv. colossless_gpv \<I> gpv \<Longrightarrow> \<Squnion> {} = \<Squnion> {}
 3. \<And>fa g gpv. \<lbrakk>\<And>gpv. colossless_gpv \<I> gpv \<Longrightarrow> fa gpv = g gpv; colossless_gpv \<I> gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. colossless_gpv \<I> xa \<longrightarrow> fst x xa = snd x xa)
 2. \<And>gpv. colossless_gpv \<I> gpv \<Longrightarrow> \<Squnion> {} = \<Squnion> {}
 3. \<And>fa g gpv. \<lbrakk>\<And>gpv. colossless_gpv \<I> gpv \<Longrightarrow> fa gpv = g gpv; colossless_gpv \<I> gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. colossless_gpv \<I> xa \<longrightarrow> fst x xa = snd x xa)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. colossless_gpv \<I> xa \<longrightarrow> fst x xa = snd x xa)

goal (2 subgoals):
 1. \<And>gpv. colossless_gpv \<I> gpv \<Longrightarrow> \<Squnion> {} = \<Squnion> {}
 2. \<And>fa g gpv. \<lbrakk>\<And>gpv. colossless_gpv \<I> gpv \<Longrightarrow> fa gpv = g gpv; colossless_gpv \<I> gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:
colossless_gpv \<I> gpv

goal (2 subgoals):
 1. \<And>gpv. colossless_gpv \<I> gpv \<Longrightarrow> \<Squnion> {} = \<Squnion> {}
 2. \<And>fa g gpv. \<lbrakk>\<And>gpv. colossless_gpv \<I> gpv \<Longrightarrow> fa gpv = g gpv; colossless_gpv \<I> gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> {} = \<Squnion> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Squnion> {} = \<Squnion> {}

goal (1 subgoal):
 1. \<And>fa g gpv. \<lbrakk>\<And>gpv. colossless_gpv \<I> gpv \<Longrightarrow> fa gpv = g gpv; colossless_gpv \<I> gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case (step expectation_gpv' expectation_gpv'')
[PROOF STATE]
proof (state)
this:
colossless_gpv \<I> ?gpv \<Longrightarrow> expectation_gpv' ?gpv = expectation_gpv'' ?gpv
colossless_gpv \<I> gpv

goal (1 subgoal):
 1. \<And>fa g gpv. \<lbrakk>\<And>gpv. colossless_gpv \<I> gpv \<Longrightarrow> fa gpv = g gpv; colossless_gpv \<I> gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
from colossless_gpv_lossless_spmfD[OF step.prems]
[PROOF STATE]
proof (chain)
picking this:
lossless_spmf (the_gpv gpv)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lossless_spmf (the_gpv gpv)

goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) = \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
by(auto simp add: lossless_iff_pmf_None intro!: nn_integral_cong_AE INF_cong step.IH intro: colossless_gpv_continuationD[OF step.prems] split: generat.split)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) = \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail' * ennreal (pmf (the_gpv gpv) None)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expectation_gpv_mono:
  fixes fail fail'
  assumes fail: "fail \<le> fail'"
  and fg: "f \<le> g"
  shows "expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
proof(induction arbitrary: gpv rule: parallel_fixp_induct_1_1[OF complete_lattice_partial_function_definitions complete_lattice_partial_function_definitions expectation_gpv.mono expectation_gpv.mono expectation_gpv_def expectation_gpv_def, case_names adm bottom step])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. fst x xa \<le> snd x xa)
 2. \<And>gpv. \<Squnion> {} \<le> \<Squnion> {}
 3. \<And>fa ga gpv. (\<And>gpv. fa gpv \<le> ga gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat g (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. ga (c r))) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. fst x xa \<le> snd x xa)
 2. \<And>gpv. \<Squnion> {} \<le> \<Squnion> {}
 3. \<And>fa ga gpv. (\<And>gpv. fa gpv \<le> ga gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat g (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. ga (c r))) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. fst x xa \<le> snd x xa)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. fst x xa \<le> snd x xa)

goal (2 subgoals):
 1. \<And>gpv. \<Squnion> {} \<le> \<Squnion> {}
 2. \<And>fa ga gpv. (\<And>gpv. fa gpv \<le> ga gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat g (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. ga (c r))) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>gpv. \<Squnion> {} \<le> \<Squnion> {}
 2. \<And>fa ga gpv. (\<And>gpv. fa gpv \<le> ga gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat g (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. ga (c r))) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> {} \<le> \<Squnion> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Squnion> {} \<le> \<Squnion> {}

goal (1 subgoal):
 1. \<And>fa ga gpv. (\<And>gpv. fa gpv \<le> ga gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat g (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. ga (c r))) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case (step expectation_gpv' expectation_gpv'')
[PROOF STATE]
proof (state)
this:
expectation_gpv' ?gpv \<le> expectation_gpv'' ?gpv

goal (1 subgoal):
 1. \<And>fa ga gpv. (\<And>gpv. fa gpv \<le> ga gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat g (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. ga (c r))) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> g x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail' * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
by(intro add_mono mult_right_mono fail nn_integral_mono_AE)
      (auto split: generat.split simp add: fg[THEN le_funD] INF_mono rev_bexI step.IH)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> g x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail' * ennreal (pmf (the_gpv gpv) None)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expectation_gpv_mono_strong:
  fixes fail fail'
  assumes fail: "\<not> colossless_gpv \<I> gpv \<Longrightarrow> fail \<le> fail'"
  and fg: "\<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> f x \<le> g x"
  shows "expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
let ?fail = "if colossless_gpv \<I> gpv then fail' else fail"
    and ?f = "\<lambda>x. if x \<in> results_gpv \<I> gpv then f x else g x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
have "expectation_gpv fail \<I> f gpv = expectation_gpv ?fail \<I> f gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv = expectation_gpv (if colossless_gpv \<I> gpv then fail' else fail) \<I> f gpv
[PROOF STEP]
by(simp cong: expectation_gpv_cong_fail)
[PROOF STATE]
proof (state)
this:
expectation_gpv fail \<I> f gpv = expectation_gpv (if colossless_gpv \<I> gpv then fail' else fail) \<I> f gpv

goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation_gpv fail \<I> f gpv = expectation_gpv (if colossless_gpv \<I> gpv then fail' else fail) \<I> f gpv

goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
have "\<dots> = expectation_gpv ?fail \<I> ?f gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv (if colossless_gpv \<I> gpv then fail' else fail) \<I> f gpv = expectation_gpv (if colossless_gpv \<I> gpv then fail' else fail) \<I> (\<lambda>x. if x \<in> results_gpv \<I> gpv then f x else g x) gpv
[PROOF STEP]
by(rule expectation_gpv_cong; simp)
[PROOF STATE]
proof (state)
this:
expectation_gpv (if colossless_gpv \<I> gpv then fail' else fail) \<I> f gpv = expectation_gpv (if colossless_gpv \<I> gpv then fail' else fail) \<I> (\<lambda>x. if x \<in> results_gpv \<I> gpv then f x else g x) gpv

goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation_gpv (if colossless_gpv \<I> gpv then fail' else fail) \<I> f gpv = expectation_gpv (if colossless_gpv \<I> gpv then fail' else fail) \<I> (\<lambda>x. if x \<in> results_gpv \<I> gpv then f x else g x) gpv

goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
have "\<dots> \<le> expectation_gpv fail' \<I> g gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv (if colossless_gpv \<I> gpv then fail' else fail) \<I> (\<lambda>x. if x \<in> results_gpv \<I> gpv then f x else g x) gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> colossless_gpv \<I> gpv \<Longrightarrow> fail \<le> fail'
?x \<in> results_gpv \<I> gpv \<Longrightarrow> f ?x \<le> g ?x

goal (1 subgoal):
 1. expectation_gpv (if colossless_gpv \<I> gpv then fail' else fail) \<I> (\<lambda>x. if x \<in> results_gpv \<I> gpv then f x else g x) gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
by(simp add: expectation_gpv_mono le_fun_def)
[PROOF STATE]
proof (state)
this:
expectation_gpv (if colossless_gpv \<I> gpv then fail' else fail) \<I> (\<lambda>x. if x \<in> results_gpv \<I> gpv then f x else g x) gpv \<le> expectation_gpv fail' \<I> g gpv

goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv

goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
expectation_gpv fail \<I> f gpv \<le> expectation_gpv fail' \<I> g gpv

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expectation_gpv_bind [simp]:
  fixes \<I> f g fail
  defines "expectation_gpv1 \<equiv> expectation_gpv fail \<I> f"
  and "expectation_gpv2 \<equiv> expectation_gpv fail \<I> (expectation_gpv fail \<I> f \<circ> g)"
  shows "expectation_gpv1 (bind_gpv gpv g) = expectation_gpv2 gpv" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv1 (gpv \<bind> g) = expectation_gpv2 gpv
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. expectation_gpv1 (gpv \<bind> g) \<le> expectation_gpv2 gpv
 2. expectation_gpv2 gpv \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
note [simp] = case_map_generat o_def
    and [cong del] = generat.case_cong_weak
[PROOF STATE]
proof (state)
this:
(case map_generat ?a ?b ?d ?r of Pure x \<Rightarrow> pure x | IO x xa \<Rightarrow> ?io x xa) = (case ?r of Pure x \<Rightarrow> (pure \<circ> ?a) x | IO out x \<Rightarrow> (?io (?b out) \<circ> ?d) x)
?f \<circ> ?g = (\<lambda>x. ?f (?g x))
?generat = ?generat' \<Longrightarrow> (case ?generat of Pure x \<Rightarrow> ?f1.0 x | IO x xa \<Rightarrow> ?f2.0 x xa) = (case ?generat' of Pure x \<Rightarrow> ?f1.0 x | IO x xa \<Rightarrow> ?f2.0 x xa)

goal (2 subgoals):
 1. expectation_gpv1 (gpv \<bind> g) \<le> expectation_gpv2 gpv
 2. expectation_gpv2 gpv \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
show "?lhs \<le> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv1 (gpv \<bind> g) \<le> expectation_gpv2 gpv
[PROOF STEP]
unfolding expectation_gpv1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv fail \<I> f (gpv \<bind> g) \<le> expectation_gpv2 gpv
[PROOF STEP]
proof(induction arbitrary: gpv rule: expectation_gpv_fixp_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. lfp.admissible (\<lambda>a. \<forall>x. a (x \<bind> g) \<le> expectation_gpv2 x)
 2. \<And>gpv. 0 \<le> expectation_gpv2 gpv
 3. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. expectation_gpv' (gpv \<bind> g) \<le> expectation_gpv2 gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (gpv \<bind> g))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (gpv \<bind> g)) None) \<le> expectation_gpv2 gpv
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. lfp.admissible (\<lambda>a. \<forall>x. a (x \<bind> g) \<le> expectation_gpv2 x)
 2. \<And>gpv. 0 \<le> expectation_gpv2 gpv
 3. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. expectation_gpv' (gpv \<bind> g) \<le> expectation_gpv2 gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (gpv \<bind> g))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (gpv \<bind> g)) None) \<le> expectation_gpv2 gpv
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfp.admissible (\<lambda>a. \<forall>x. a (x \<bind> g) \<le> expectation_gpv2 x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lfp.admissible (\<lambda>a. \<forall>x. a (x \<bind> g) \<le> expectation_gpv2 x)

goal (2 subgoals):
 1. \<And>gpv. 0 \<le> expectation_gpv2 gpv
 2. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. expectation_gpv' (gpv \<bind> g) \<le> expectation_gpv2 gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (gpv \<bind> g))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (gpv \<bind> g)) None) \<le> expectation_gpv2 gpv
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>gpv. 0 \<le> expectation_gpv2 gpv
 2. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. expectation_gpv' (gpv \<bind> g) \<le> expectation_gpv2 gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (gpv \<bind> g))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (gpv \<bind> g)) None) \<le> expectation_gpv2 gpv
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> expectation_gpv2 gpv
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> expectation_gpv2 gpv

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. expectation_gpv' (gpv \<bind> g) \<le> expectation_gpv2 gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (gpv \<bind> g))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (gpv \<bind> g)) None) \<le> expectation_gpv2 gpv
[PROOF STEP]
case (step expectation_gpv')
[PROOF STATE]
proof (state)
this:
expectation_gpv' ?gpv \<le> expectation_gpv fail \<I> f ?gpv
expectation_gpv' (?gpv \<bind> g) \<le> expectation_gpv2 ?gpv

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. expectation_gpv' (gpv \<bind> g) \<le> expectation_gpv2 gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (gpv \<bind> g))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (gpv \<bind> g)) None) \<le> expectation_gpv2 gpv
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (gpv \<bind> g)) + fail * ennreal (pmf (the_gpv (gpv \<bind> g)) None) \<le> expectation_gpv2 gpv
[PROOF STEP]
unfolding expectation_gpv2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (gpv \<bind> g)) + fail * ennreal (pmf (the_gpv (gpv \<bind> g)) None) \<le> expectation_gpv fail \<I> (expectation_gpv fail \<I> f \<circ> g) gpv
[PROOF STEP]
apply(rewrite bind_gpv.sel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g)))) (the_gpv gpv \<bind> case_generat (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x))) (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))) + fail * ennreal (pmf (the_gpv (gpv \<bind> g)) None) \<le> expectation_gpv fail \<I> (expectation_gpv fail \<I> f \<circ> g) gpv
[PROOF STEP]
apply(simp add: map_spmf_bind_spmf measure_spmf_bind)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) \<bind> (\<lambda>x. measure_spmf (map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g)))) (case x of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input)))))) + fail * ennreal (pmf (the_gpv gpv \<bind> (\<lambda>generat. if is_Pure generat then the_gpv (g (generat.result generat)) else return_spmf (IO (generat.output generat) (\<lambda>input. continuation generat input \<bind> g)))) None) \<le> expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) gpv
[PROOF STEP]
apply(rewrite nn_integral_bind[where B="measure_spmf _"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>generat. case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<in> borel_measurable (measure_spmf ?uu37)
 2. (\<lambda>x. measure_spmf (map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g)))) (case x of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input)))))) \<in> measure_spmf (the_gpv gpv) \<rightarrow>\<^sub>M subprob_algebra (measure_spmf ?uu37)
 3. \<integral>\<^sup>+ generat. \<integral>\<^sup>+ y. (case y of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g)))) (case generat of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input))))) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv \<bind> (\<lambda>generat. if is_Pure generat then the_gpv (g (generat.result generat)) else return_spmf (IO (generat.output generat) (\<lambda>input. continuation generat input \<bind> g)))) None) \<le> expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) gpv
[PROOF STEP]
apply(simp_all add: space_subprob_algebra)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (case generat of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input)))) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv \<bind> (\<lambda>generat. if is_Pure generat then the_gpv (g (generat.result generat)) else return_spmf (IO (generat.output generat) (\<lambda>input. continuation generat input \<bind> g)))) None) \<le> expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) gpv
[PROOF STEP]
apply(rewrite expectation_gpv.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (case generat of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input)))) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv \<bind> (\<lambda>generat. if is_Pure generat then the_gpv (g (generat.result generat)) else return_spmf (IO (generat.output generat) (\<lambda>input. continuation generat input \<bind> g)))) None) \<le> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> expectation_gpv fail \<I> f (g x) | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
apply(simp add: pmf_bind_spmf_None distrib_left nn_integral_eq_integral[symmetric] measure_spmf.integrable_const_bound[where B=1] pmf_le_1 nn_integral_cmult[symmetric] nn_integral_add[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fail * ennreal (pmf (the_gpv gpv) None) = \<top> \<or> \<integral>\<^sup>+ x. \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (case x of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input)))) + fail * ennreal (pmf (if is_Pure x then the_gpv (g (generat.result x)) else return_spmf (IO (generat.output x) (\<lambda>input. continuation x input \<bind> g))) None) \<partial>measure_spmf (the_gpv gpv) \<le> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. expectation_gpv fail \<I> f (g x)) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (c r)))
[PROOF STEP]
apply(rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (case x of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input)))) + fail * ennreal (pmf (if is_Pure x then the_gpv (g (generat.result x)) else return_spmf (IO (generat.output x) (\<lambda>input. continuation x input \<bind> g))) None) \<partial>measure_spmf (the_gpv gpv) \<le> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. expectation_gpv fail \<I> f (g x)) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (c r)))
[PROOF STEP]
apply(rule nn_integral_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (case x of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input)))) + fail * ennreal (pmf (if is_Pure x then the_gpv (g (generat.result x)) else return_spmf (IO (generat.output x) (\<lambda>input. continuation x input \<bind> g))) None) \<le> (case x of Pure x \<Rightarrow> expectation_gpv fail \<I> f (g x) | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (c r))
[PROOF STEP]
apply(clarsimp split!: generat.split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. Pure x1 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) (map_generat id id ((\<circ>) Inl) x) of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (g x1)) + fail * ennreal (pmf (the_gpv (g x1)) None) \<le> expectation_gpv fail \<I> f (g x1)
 2. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (return_spmf (IO x21 (\<lambda>input. Inr (x22 input)))) \<le> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (x22 r))
[PROOF STEP]
apply(rewrite expectation_gpv.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. Pure x1 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) (map_generat id id ((\<circ>) Inl) x) of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (g x1)) + fail * ennreal (pmf (the_gpv (g x1)) None) \<le> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (the_gpv (g x1)) + fail * ennreal (pmf (the_gpv (g x1)) None)
 2. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (return_spmf (IO x21 (\<lambda>input. Inr (x22 input)))) \<le> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (x22 r))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. Pure x1 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> fail * ennreal (pmf (the_gpv (g x1)) None) = \<top> \<or> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) (map_generat id id ((\<circ>) Inl) x) of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (g x1)) \<le> integral\<^sup>N (measure_spmf (the_gpv (g x1))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)))
 2. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (return_spmf (IO x21 (\<lambda>input. Inr (x22 input)))) \<le> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (x22 r))
[PROOF STEP]
apply(rule disjI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. Pure x1 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) (map_generat id id ((\<circ>) Inl) x) of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (g x1)) \<le> integral\<^sup>N (measure_spmf (the_gpv (g x1))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)))
 2. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (return_spmf (IO x21 (\<lambda>input. Inr (x22 input)))) \<le> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (x22 r))
[PROOF STEP]
apply(rule nn_integral_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x. \<lbrakk>Pure x1 \<in> space (measure_spmf (the_gpv gpv)); x \<in> space (measure_spmf (the_gpv (g x1)))\<rbrakk> \<Longrightarrow> (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) (map_generat id id ((\<circ>) Inl) x) of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (case x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r))
 2. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (return_spmf (IO x21 (\<lambda>input. Inr (x22 input)))) \<le> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (x22 r))
[PROOF STEP]
apply(clarsimp split: generat.split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x21 x22. \<lbrakk>Pure x1 \<in> space (measure_spmf (the_gpv gpv)); IO x21 x22 \<in> space (measure_spmf (the_gpv (g x1)))\<rbrakk> \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r)) \<le> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv fail \<I> f (x22 r))
 2. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (return_spmf (IO x21 (\<lambda>input. Inr (x22 input)))) \<le> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (x22 r))
[PROOF STEP]
apply(rule INF_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x21 x22 m. \<lbrakk>Pure x1 \<in> space (measure_spmf (the_gpv gpv)); IO x21 x22 \<in> space (measure_spmf (the_gpv (g x1))); m \<in> responses_\<I> \<I> x21\<rbrakk> \<Longrightarrow> \<exists>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r) \<le> expectation_gpv fail \<I> f (x22 m)
 2. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (return_spmf (IO x21 (\<lambda>input. Inr (x22 input)))) \<le> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (x22 r))
[PROOF STEP]
apply(erule rev_bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x21 x22 m. \<lbrakk>Pure x1 \<in> space (measure_spmf (the_gpv gpv)); IO x21 x22 \<in> space (measure_spmf (the_gpv (g x1)))\<rbrakk> \<Longrightarrow> expectation_gpv' (x22 m) \<le> expectation_gpv fail \<I> f (x22 m)
 2. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (return_spmf (IO x21 (\<lambda>input. Inr (x22 input)))) \<le> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (x22 r))
[PROOF STEP]
apply(rule step.hyps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (return_spmf (IO x21 (\<lambda>input. Inr (x22 input)))) \<le> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (x22 r))
[PROOF STEP]
apply(clarsimp simp add: measure_spmf_return_spmf nn_integral_return)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> (\<Sqinter>x\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 x \<bind> g)) \<le> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (x22 r))
[PROOF STEP]
apply(rule INF_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 m. \<lbrakk>IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)); m \<in> responses_\<I> \<I> x21\<rbrakk> \<Longrightarrow> \<exists>x\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 x \<bind> g) \<le> expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (x22 m)
[PROOF STEP]
apply(erule rev_bexI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 m. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> expectation_gpv' (x22 m \<bind> g) \<le> expectation_gpv fail \<I> (\<lambda>x. expectation_gpv fail \<I> f (g x)) (x22 m)
[PROOF STEP]
apply(rule step.IH[unfolded expectation_gpv2_def o_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (gpv \<bind> g)) + fail * ennreal (pmf (the_gpv (gpv \<bind> g)) None) \<le> expectation_gpv2 gpv

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
expectation_gpv1 (gpv \<bind> g) \<le> expectation_gpv2 gpv

goal (1 subgoal):
 1. expectation_gpv2 gpv \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
show "?rhs \<le> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv2 gpv \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
unfolding expectation_gpv2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv fail \<I> (expectation_gpv fail \<I> f \<circ> g) gpv \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
proof(induction arbitrary: gpv rule: expectation_gpv_fixp_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. lfp.admissible (\<lambda>a. \<forall>x. a x \<le> expectation_gpv1 (x \<bind> g))
 2. \<And>gpv. 0 \<le> expectation_gpv1 (gpv \<bind> g)
 3. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (expectation_gpv fail \<I> f \<circ> g) gpv; \<And>gpv. expectation_gpv' gpv \<le> expectation_gpv1 (gpv \<bind> g)\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (expectation_gpv fail \<I> f \<circ> g) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. lfp.admissible (\<lambda>a. \<forall>x. a x \<le> expectation_gpv1 (x \<bind> g))
 2. \<And>gpv. 0 \<le> expectation_gpv1 (gpv \<bind> g)
 3. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (expectation_gpv fail \<I> f \<circ> g) gpv; \<And>gpv. expectation_gpv' gpv \<le> expectation_gpv1 (gpv \<bind> g)\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (expectation_gpv fail \<I> f \<circ> g) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfp.admissible (\<lambda>a. \<forall>x. a x \<le> expectation_gpv1 (x \<bind> g))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lfp.admissible (\<lambda>a. \<forall>x. a x \<le> expectation_gpv1 (x \<bind> g))

goal (2 subgoals):
 1. \<And>gpv. 0 \<le> expectation_gpv1 (gpv \<bind> g)
 2. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (expectation_gpv fail \<I> f \<circ> g) gpv; \<And>gpv. expectation_gpv' gpv \<le> expectation_gpv1 (gpv \<bind> g)\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (expectation_gpv fail \<I> f \<circ> g) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>gpv. 0 \<le> expectation_gpv1 (gpv \<bind> g)
 2. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (expectation_gpv fail \<I> f \<circ> g) gpv; \<And>gpv. expectation_gpv' gpv \<le> expectation_gpv1 (gpv \<bind> g)\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (expectation_gpv fail \<I> f \<circ> g) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> expectation_gpv1 (gpv \<bind> g)

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (expectation_gpv fail \<I> f \<circ> g) gpv; \<And>gpv. expectation_gpv' gpv \<le> expectation_gpv1 (gpv \<bind> g)\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (expectation_gpv fail \<I> f \<circ> g) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
case (step expectation_gpv')
[PROOF STATE]
proof (state)
this:
expectation_gpv' ?gpv \<le> expectation_gpv fail \<I> (expectation_gpv fail \<I> f \<circ> g) ?gpv
expectation_gpv' ?gpv \<le> expectation_gpv1 (?gpv \<bind> g)

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (expectation_gpv fail \<I> f \<circ> g) gpv; \<And>gpv. expectation_gpv' gpv \<le> expectation_gpv1 (gpv \<bind> g)\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (expectation_gpv fail \<I> f \<circ> g) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> (expectation_gpv fail \<I> f \<circ> g) x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv1 (gpv \<bind> g)
[PROOF STEP]
unfolding expectation_gpv1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> (expectation_gpv fail \<I> f \<circ> g) x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv fail \<I> f (gpv \<bind> g)
[PROOF STEP]
apply(rewrite in "_ \<le> \<hole>" expectation_gpv.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> (expectation_gpv fail \<I> f \<circ> g) x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (the_gpv (gpv \<bind> g)) + fail * ennreal (pmf (the_gpv (gpv \<bind> g)) None)
[PROOF STEP]
apply(rewrite bind_gpv.sel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> (expectation_gpv fail \<I> f \<circ> g) x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g)))) (the_gpv gpv \<bind> case_generat (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x))) (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))) + fail * ennreal (pmf (the_gpv (gpv \<bind> g)) None)
[PROOF STEP]
apply(simp add: measure_spmf_bind)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> expectation_gpv fail \<I> f (g x) | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (the_gpv gpv) \<bind> (\<lambda>x. measure_spmf (case x of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input))))) + fail * ennreal (pmf (the_gpv gpv \<bind> (\<lambda>generat. if is_Pure generat then the_gpv (g (generat.result generat)) else return_spmf (IO (generat.output generat) (\<lambda>input. continuation generat input \<bind> g)))) None)
[PROOF STEP]
apply(rewrite nn_integral_bind[where B="measure_spmf _"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>x. case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<in> borel_measurable (measure_spmf ?uu69)
 2. (\<lambda>x. measure_spmf (case x of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input))))) \<in> measure_spmf (the_gpv gpv) \<rightarrow>\<^sub>M subprob_algebra (measure_spmf ?uu69)
 3. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> expectation_gpv fail \<I> f (g x) | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) y of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (case x of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input)))) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv \<bind> (\<lambda>generat. if is_Pure generat then the_gpv (g (generat.result generat)) else return_spmf (IO (generat.output generat) (\<lambda>input. continuation generat input \<bind> g)))) None)
[PROOF STEP]
apply(simp_all add: space_subprob_algebra)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> expectation_gpv fail \<I> f (g x) | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) y of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (case x of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input)))) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv \<bind> (\<lambda>generat. if is_Pure generat then the_gpv (g (generat.result generat)) else return_spmf (IO (generat.output generat) (\<lambda>input. continuation generat input \<bind> g)))) None)
[PROOF STEP]
apply(simp add: pmf_bind_spmf_None distrib_left nn_integral_eq_integral[symmetric] measure_spmf.integrable_const_bound[where B=1] pmf_le_1 nn_integral_cmult[symmetric] nn_integral_add[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fail * ennreal (pmf (the_gpv gpv) None) = \<top> \<or> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. expectation_gpv fail \<I> f (g x)) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) y of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (case x of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input)))) + fail * ennreal (pmf (if is_Pure x then the_gpv (g (generat.result x)) else return_spmf (IO (generat.output x) (\<lambda>input. continuation x input \<bind> g))) None) \<partial>measure_spmf (the_gpv gpv)
[PROOF STEP]
apply(rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. expectation_gpv fail \<I> f (g x)) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) y of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (case x of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input)))) + fail * ennreal (pmf (if is_Pure x then the_gpv (g (generat.result x)) else return_spmf (IO (generat.output x) (\<lambda>input. continuation x input \<bind> g))) None) \<partial>measure_spmf (the_gpv gpv)
[PROOF STEP]
apply(rule nn_integral_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> (case x of Pure x \<Rightarrow> expectation_gpv fail \<I> f (g x) | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ y. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) y of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (case x of Pure x \<Rightarrow> map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (g x)) | IO out c \<Rightarrow> return_spmf (IO out (\<lambda>input. Inr (c input)))) + fail * ennreal (pmf (if is_Pure x then the_gpv (g (generat.result x)) else return_spmf (IO (generat.output x) (\<lambda>input. continuation x input \<bind> g))) None)
[PROOF STEP]
apply(clarsimp split!: generat.split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. Pure x1 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> expectation_gpv fail \<I> f (g x1) \<le> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) (map_generat id id ((\<circ>) Inl) x) of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (the_gpv (g x1)) + fail * ennreal (pmf (the_gpv (g x1)) None)
 2. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r)) \<le> \<integral>\<^sup>+ y. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) y of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (return_spmf (IO x21 (\<lambda>input. Inr (x22 input))))
[PROOF STEP]
apply(rewrite expectation_gpv.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. Pure x1 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (the_gpv (g x1)) + fail * ennreal (pmf (the_gpv (g x1)) None) \<le> \<integral>\<^sup>+ x. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) (map_generat id id ((\<circ>) Inl) x) of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (the_gpv (g x1)) + fail * ennreal (pmf (the_gpv (g x1)) None)
 2. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r)) \<le> \<integral>\<^sup>+ y. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) y of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (return_spmf (IO x21 (\<lambda>input. Inr (x22 input))))
[PROOF STEP]
apply(simp cong del: if_weak_cong add: generat.map_comp id_def[symmetric] generat.map_id)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r)) \<le> \<integral>\<^sup>+ y. (case map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> g))) y of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r)) \<partial>measure_spmf (return_spmf (IO x21 (\<lambda>input. Inr (x22 input))))
[PROOF STEP]
apply(simp add: measure_spmf_return_spmf nn_integral_return)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r)) \<le> (\<Sqinter>x\<in>responses_\<I> \<I> x21. expectation_gpv fail \<I> f (x22 x \<bind> g))
[PROOF STEP]
apply(rule INF_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 m. \<lbrakk>IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)); m \<in> responses_\<I> \<I> x21\<rbrakk> \<Longrightarrow> \<exists>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r) \<le> expectation_gpv fail \<I> f (x22 m \<bind> g)
[PROOF STEP]
apply(erule rev_bexI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 m. IO x21 x22 \<in> space (measure_spmf (the_gpv gpv)) \<Longrightarrow> expectation_gpv' (x22 m) \<le> expectation_gpv fail \<I> f (x22 m \<bind> g)
[PROOF STEP]
apply(rule step.IH[unfolded expectation_gpv1_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> (expectation_gpv fail \<I> f \<circ> g) x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv1 (gpv \<bind> g)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
expectation_gpv2 gpv \<le> expectation_gpv1 (gpv \<bind> g)

goal:
No subgoals!
[PROOF STEP]
qed