[STATEMENT]
lemma expectation_gpv_try_gpv [simp]:
  fixes fail \<I> f gpv'
  defines "expectation_gpv1 \<equiv> expectation_gpv fail \<I> f"
    and "expectation_gpv2 \<equiv> expectation_gpv (expectation_gpv fail \<I> f gpv') \<I> f"
  shows "expectation_gpv1 (try_gpv gpv gpv') = expectation_gpv2 gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv1 (TRY gpv ELSE gpv') = expectation_gpv2 gpv
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. expectation_gpv1 (TRY gpv ELSE gpv') \<le> expectation_gpv2 gpv
 2. expectation_gpv2 gpv \<le> expectation_gpv1 (TRY gpv ELSE gpv')
[PROOF STEP]
show "expectation_gpv1 (try_gpv gpv gpv') \<le> expectation_gpv2 gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv1 (TRY gpv ELSE gpv') \<le> expectation_gpv2 gpv
[PROOF STEP]
unfolding expectation_gpv1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv fail \<I> f (TRY gpv ELSE gpv') \<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 (TRY x ELSE gpv') \<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' (TRY gpv ELSE gpv') \<le> expectation_gpv2 gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (TRY gpv ELSE gpv'))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE gpv')) 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 (TRY x ELSE gpv') \<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' (TRY gpv ELSE gpv') \<le> expectation_gpv2 gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (TRY gpv ELSE gpv'))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE gpv')) None) \<le> expectation_gpv2 gpv
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfp.admissible (\<lambda>a. \<forall>x. a (TRY x ELSE gpv') \<le> expectation_gpv2 x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lfp.admissible (\<lambda>a. \<forall>x. a (TRY x ELSE gpv') \<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' (TRY gpv ELSE gpv') \<le> expectation_gpv2 gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (TRY gpv ELSE gpv'))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE gpv')) 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' (TRY gpv ELSE gpv') \<le> expectation_gpv2 gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (TRY gpv ELSE gpv'))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE gpv')) 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' (TRY gpv ELSE gpv') \<le> expectation_gpv2 gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (TRY gpv ELSE gpv'))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE gpv')) None) \<le> expectation_gpv2 gpv
[PROOF STEP]
case step [unfolded expectation_gpv2_def]: (step expectation_gpv')
[PROOF STATE]
proof (state)
this:
expectation_gpv' ?gpv \<le> expectation_gpv fail \<I> f ?gpv
expectation_gpv' (TRY ?gpv ELSE gpv') \<le> expectation_gpv (expectation_gpv fail \<I> f gpv') \<I> f ?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' (TRY gpv ELSE gpv') \<le> expectation_gpv2 gpv\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (TRY gpv ELSE gpv'))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE gpv')) 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 (TRY gpv ELSE gpv')) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE gpv')) 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 (TRY gpv ELSE gpv')) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE gpv')) None) \<le> expectation_gpv (expectation_gpv fail \<I> f gpv') \<I> f gpv
[PROOF STEP]
apply(rewrite expectation_gpv.simps)
[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 (TRY gpv ELSE gpv')) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE 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 (expectation_gpv fail \<I> f gpv') \<I> f (c r)) \<partial>measure_spmf (the_gpv gpv) + expectation_gpv fail \<I> f gpv' * ennreal (pmf (the_gpv gpv) None)
[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> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (TRY gpv ELSE gpv')) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE 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 (expectation_gpv fail \<I> f gpv') \<I> f (c r)) \<partial>measure_spmf (the_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 fail \<I> f (c r)) \<partial>measure_spmf (the_gpv gpv') + fail * ennreal (pmf (the_gpv gpv') None)) * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
apply(simp add: pmf_map_spmf_None nn_integral_try_spmf o_def generat.map_comp case_map_generat distrib_right cong del: generat.case_cong_weak)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. (case map_generat (\<lambda>x. x) (\<lambda>x. x) (\<lambda>x input. TRY x input ELSE gpv') 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 gpv) + \<integral>\<^sup>+ x. (case map_generat (\<lambda>x. x) (\<lambda>x. x) (\<lambda>x. x) 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 gpv') * ennreal (pmf (the_gpv gpv) None) + fail * ennreal (pmf (the_gpv gpv) None * 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 (expectation_gpv fail \<I> f gpv') \<I> f (c r)) \<partial>measure_spmf (the_gpv gpv) + (integral\<^sup>N (measure_spmf (the_gpv gpv')) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv fail \<I> f (c r))) * ennreal (pmf (the_gpv gpv) None) + fail * ennreal (pmf (the_gpv gpv') None) * ennreal (pmf (the_gpv gpv) None))
[PROOF STEP]
apply(simp add: mult_ac add.assoc ennreal_mult)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fail * (ennreal (pmf (the_gpv gpv') None) * ennreal (pmf (the_gpv gpv) None)) = \<top> \<or> \<integral>\<^sup>+ x. (case map_generat (\<lambda>x. x) (\<lambda>x. x) (\<lambda>x input. TRY x input ELSE gpv') 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 gpv) + ennreal (pmf (the_gpv gpv) None) * \<integral>\<^sup>+ x. (case map_generat (\<lambda>x. x) (\<lambda>x. x) (\<lambda>x. x) 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 gpv') \<le> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv (expectation_gpv fail \<I> f gpv') \<I> f (c r))) + 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. expectation_gpv fail \<I> f (c r)))
[PROOF STEP]
apply(intro disjI2 add_mono mult_left_mono nn_integral_mono; clarsimp split: generat.split intro!: INF_mono step elim!: rev_bexI)
[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 (TRY gpv ELSE gpv')) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE gpv')) None) \<le> expectation_gpv2 gpv

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

goal (1 subgoal):
 1. expectation_gpv2 gpv \<le> expectation_gpv1 (TRY gpv ELSE gpv')
[PROOF STEP]
show "expectation_gpv2 gpv \<le> expectation_gpv1 (try_gpv gpv gpv')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv2 gpv \<le> expectation_gpv1 (TRY gpv ELSE gpv')
[PROOF STEP]
unfolding expectation_gpv2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv (expectation_gpv fail \<I> f gpv') \<I> f gpv \<le> expectation_gpv1 (TRY gpv ELSE 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 \<le> expectation_gpv1 (TRY x ELSE gpv'))
 2. \<And>gpv. 0 \<le> expectation_gpv1 (TRY gpv ELSE gpv')
 3. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv (expectation_gpv fail \<I> f gpv') \<I> f gpv; \<And>gpv. expectation_gpv' gpv \<le> expectation_gpv1 (TRY gpv ELSE gpv')\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + expectation_gpv fail \<I> f gpv' * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv1 (TRY gpv ELSE gpv')
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

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

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

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

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

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv (expectation_gpv fail \<I> f gpv') \<I> f gpv; \<And>gpv. expectation_gpv' gpv \<le> expectation_gpv1 (TRY gpv ELSE gpv')\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + expectation_gpv fail \<I> f gpv' * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv1 (TRY gpv ELSE 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) + expectation_gpv fail \<I> f gpv' * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv1 (TRY gpv ELSE gpv')
[PROOF STEP]
unfolding expectation_gpv1_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) + expectation_gpv fail \<I> f gpv' * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv fail \<I> f (TRY gpv ELSE gpv')
[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> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + expectation_gpv fail \<I> f gpv' * 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 (TRY gpv ELSE gpv')) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE gpv')) None)
[PROOF STEP]
apply(rewrite in "\<hole> \<le> _" expectation_gpv.simps)
[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) + (\<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') + fail * ennreal (pmf (the_gpv gpv') None)) * 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 (TRY gpv ELSE gpv')) + fail * ennreal (pmf (the_gpv (TRY gpv ELSE gpv')) None)
[PROOF STEP]
apply(simp add: pmf_map_spmf_None nn_integral_try_spmf o_def generat.map_comp case_map_generat distrib_left ennreal_mult mult_ac id_def[symmetric] generat.map_id cong del: generat.case_cong_weak)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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. expectation_gpv fail \<I> f (c r))) = \<top> \<or> fail * (ennreal (pmf (the_gpv gpv') None) * ennreal (pmf (the_gpv gpv) None)) = \<top> \<or> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ x. (case map_generat id id (\<lambda>x input. TRY x input ELSE gpv') 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)
[PROOF STEP]
apply(rule disjI2 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> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (case map_generat id id (\<lambda>x input. TRY x input ELSE gpv') 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))
[PROOF STEP]
apply(clarsimp split: generat.split intro!: INF_mono step(2) elim!: rev_bexI)
[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) + expectation_gpv fail \<I> f gpv' * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv1 (TRY gpv ELSE gpv')

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expectation_gpv_restrict_gpv:
  "\<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv fail \<I> f (restrict_gpv \<I> gpv) = expectation_gpv fail \<I> f gpv" for fail
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv fail \<I> f (restrict_gpv \<I> gpv) = expectation_gpv fail \<I> f 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. \<I> \<turnstile>g x \<surd> \<longrightarrow> a (restrict_gpv \<I> x) = a x)
 2. \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> 0 = 0
 3. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv' (restrict_gpv \<I> gpv) = expectation_gpv' gpv; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (restrict_gpv \<I> gpv))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (restrict_gpv \<I> gpv)) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

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

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

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

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

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv' (restrict_gpv \<I> gpv) = expectation_gpv' gpv; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (restrict_gpv \<I> gpv))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv (restrict_gpv \<I> gpv)) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (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 (restrict_gpv \<I> gpv)) + fail * ennreal (pmf (the_gpv (restrict_gpv \<I> 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]
apply(simp add: pmf_map vimage_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 (map_pmf (case_option None (case_generat (Some \<circ> Pure) (\<lambda>out c. if out \<in> outs_\<I> \<I> then Some (IO out (\<lambda>input. if input \<in> responses_\<I> \<I> out then restrict_gpv \<I> (c input) else Fail)) else None))) (the_gpv gpv)) + fail * ennreal (measure_pmf.prob (the_gpv gpv) {x. (case x of None \<Rightarrow> None | Some (Pure xa) \<Rightarrow> (Some \<circ> Pure) xa | Some (IO out c) \<Rightarrow> if out \<in> outs_\<I> \<I> then Some (IO out (\<lambda>input. if input \<in> responses_\<I> \<I> out then restrict_gpv \<I> (c input) else Fail)) else None) = 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]
apply(rule arg_cong2[where f="(+)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 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_pmf (case_option None (case_generat (Some \<circ> Pure) (\<lambda>out c. if out \<in> outs_\<I> \<I> then Some (IO out (\<lambda>input. if input \<in> responses_\<I> \<I> out then restrict_gpv \<I> (c input) else Fail)) else None))) (the_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)
 2. fail * ennreal (measure_pmf.prob (the_gpv gpv) {x. (case x of None \<Rightarrow> None | Some (Pure xa) \<Rightarrow> (Some \<circ> Pure) xa | Some (IO out c) \<Rightarrow> if out \<in> outs_\<I> \<I> then Some (IO out (\<lambda>input. if input \<in> responses_\<I> \<I> out then restrict_gpv \<I> (c input) else Fail)) else None) = None}) = fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
subgoal
[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_pmf (case_option None (case_generat (Some \<circ> Pure) (\<lambda>out c. if out \<in> outs_\<I> \<I> then Some (IO out (\<lambda>input. if input \<in> responses_\<I> \<I> out then restrict_gpv \<I> (c input) else Fail)) else None))) (the_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)
[PROOF STEP]
by(clarsimp simp add: measure_spmf_def nn_integral_distr nn_integral_restrict_space step.IH WT_gpv_ContD[OF step.prems] AE_measure_pmf_iff in_set_spmf[symmetric] WT_gpv_OutD[OF step.prems] split!: option.split generat.split intro!: nn_integral_cong_AE INF_cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fail * ennreal (measure_pmf.prob (the_gpv gpv) {x. (case x of None \<Rightarrow> None | Some (Pure xa) \<Rightarrow> (Some \<circ> Pure) xa | Some (IO out c) \<Rightarrow> if out \<in> outs_\<I> \<I> then Some (IO out (\<lambda>input. if input \<in> responses_\<I> \<I> out then restrict_gpv \<I> (c input) else Fail)) else None) = None}) = fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
apply(simp add: measure_pmf_single[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fail * ennreal (measure_pmf.prob (the_gpv gpv) {x. (case x of None \<Rightarrow> None | Some (Pure xa) \<Rightarrow> (Some \<circ> Pure) xa | Some (IO out c) \<Rightarrow> if out \<in> outs_\<I> \<I> then Some (IO out (\<lambda>input. if input \<in> responses_\<I> \<I> out then restrict_gpv \<I> (c input) else Fail)) else None) = None}) = fail * ennreal (measure_pmf.prob (the_gpv gpv) {None})
[PROOF STEP]
apply(rule arg_cong[where f="\<lambda>x. _ * ennreal x"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.prob (the_gpv gpv) {x. (case x of None \<Rightarrow> None | Some (Pure xa) \<Rightarrow> (Some \<circ> Pure) xa | Some (IO out c) \<Rightarrow> if out \<in> outs_\<I> \<I> then Some (IO out (\<lambda>input. if input \<in> responses_\<I> \<I> out then restrict_gpv \<I> (c input) else Fail)) else None) = None} = measure_pmf.prob (the_gpv gpv) {None}
[PROOF STEP]
apply(rule measure_pmf.finite_measure_eq_AE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. AE x in measure_pmf (the_gpv gpv). (x \<in> {x. (case x of None \<Rightarrow> None | Some (Pure xa) \<Rightarrow> (Some \<circ> Pure) xa | Some (IO out c) \<Rightarrow> if out \<in> outs_\<I> \<I> then Some (IO out (\<lambda>input. if input \<in> responses_\<I> \<I> out then restrict_gpv \<I> (c input) else Fail)) else None) = None}) = (x \<in> {None})
 2. {x. (case x of None \<Rightarrow> None | Some (Pure xa) \<Rightarrow> (Some \<circ> Pure) xa | Some (IO out c) \<Rightarrow> if out \<in> outs_\<I> \<I> then Some (IO out (\<lambda>input. if input \<in> responses_\<I> \<I> out then restrict_gpv \<I> (c input) else Fail)) else None) = None} \<in> measure_pmf.events (the_gpv gpv)
 3. {None} \<in> measure_pmf.events (the_gpv gpv)
[PROOF STEP]
apply(auto simp add: AE_measure_pmf_iff in_set_spmf[symmetric] intro: WT_gpv_OutD[OF step.prems] split: option.split_asm generat.split_asm if_split_asm)
[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 (restrict_gpv \<I> gpv)) + fail * ennreal (pmf (the_gpv (restrict_gpv \<I> 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_const_le: "\<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv fail \<I> (\<lambda>_. c) gpv \<le> max c fail" for fail
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv fail \<I> (\<lambda>_. c) gpv \<le> max c fail
[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. \<I> \<turnstile>g x \<surd> \<longrightarrow> a x \<le> max c fail)
 2. \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> 0 \<le> max c fail
 3. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (\<lambda>a. c) gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv' gpv \<le> max c fail; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> max c fail
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

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

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

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

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

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (\<lambda>a. c) gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv' gpv \<le> max c fail; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> max c fail
[PROOF STEP]
have "integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. INF r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> integral\<^sup>N (measure_spmf (the_gpv gpv)) (\<lambda>_. max c fail)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ _. max c fail \<partial>measure_spmf (the_gpv gpv)
[PROOF STEP]
using step.prems
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ _. max c fail \<partial>measure_spmf (the_gpv gpv)
[PROOF STEP]
by(intro nn_integral_mono_AE)(auto 4 4 split: generat.split intro: INF_lower2 step.IH WT_gpv_ContD[OF step.prems] dest!: WT_gpv_OutD simp add: in_outs_\<I>_iff_responses_\<I>)
[PROOF STATE]
proof (state)
this:
integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ _. max c fail \<partial>measure_spmf (the_gpv gpv)

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (\<lambda>a. c) gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv' gpv \<le> max c fail; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> max c fail
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ _. max c fail \<partial>measure_spmf (the_gpv gpv)

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (\<lambda>a. c) gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv' gpv \<le> max c fail; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> max c fail
[PROOF STEP]
have "\<dots> + fail * pmf (the_gpv gpv) None \<le> \<dots> + max c fail * pmf (the_gpv gpv) None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ _. max c fail \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ _. max c fail \<partial>measure_spmf (the_gpv gpv) + max c fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
by(intro add_left_mono mult_right_mono) simp_all
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ _. max c fail \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ _. max c fail \<partial>measure_spmf (the_gpv gpv) + max c fail * ennreal (pmf (the_gpv gpv) None)

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (\<lambda>a. c) gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv' gpv \<le> max c fail; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> max c fail
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ _. max c fail \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ _. max c fail \<partial>measure_spmf (the_gpv gpv) + max c fail * ennreal (pmf (the_gpv gpv) None)

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (\<lambda>a. c) gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv' gpv \<le> max c fail; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> max c fail
[PROOF STEP]
have "\<dots> \<le> max c fail"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ _. max c fail \<partial>measure_spmf (the_gpv gpv) + max c fail * ennreal (pmf (the_gpv gpv) None) \<le> max c fail
[PROOF STEP]
by(simp add: measure_spmf.emeasure_eq_measure pmf_None_eq_weight_spmf ennreal_minus[symmetric])
      (metis (no_types, opaque_lifting) add_diff_eq_iff_ennreal distrib_left ennreal_le_1 le_max_iff_disj max.cobounded2 mult.commute mult.left_neutral weight_spmf_le_1)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ _. max c fail \<partial>measure_spmf (the_gpv gpv) + max c fail * ennreal (pmf (the_gpv gpv) None) \<le> max c fail

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv fail \<I> (\<lambda>a. c) gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv' gpv \<le> max c fail; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> max c fail
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> x + fail * ennreal (pmf (the_gpv gpv) None) \<le> y + fail * ennreal (pmf (the_gpv gpv) None)) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> max c fail
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> x + fail * ennreal (pmf (the_gpv gpv) None) \<le> y + fail * ennreal (pmf (the_gpv gpv) None)) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> max c fail

goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> c | 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> max c fail
[PROOF STEP]
by(simp add: add_mono)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> c | 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> max c fail

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expectation_gpv_no_results:
   "\<lbrakk> results_gpv \<I> gpv = {}; \<I> \<turnstile>g gpv \<surd> \<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> f gpv = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>results_gpv \<I> gpv = {}; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> f gpv = 0
[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. results_gpv \<I> x = {} \<longrightarrow> \<I> \<turnstile>g x \<surd> \<longrightarrow> a x = 0)
 2. \<And>gpv. \<lbrakk>results_gpv \<I> gpv = {}; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> 0 = 0
 3. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv. \<lbrakk>results_gpv \<I> gpv = {}; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv' gpv = 0; results_gpv \<I> gpv = {}; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) = 0
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

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

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

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

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

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv. \<lbrakk>results_gpv \<I> gpv = {}; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv' gpv = 0; results_gpv \<I> gpv = {}; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) = 0
[PROOF STEP]
have "results_gpv \<I> (c x) = {}" if "IO out c \<in> set_spmf (the_gpv gpv)" "x \<in> responses_\<I> \<I> out"
    for out c x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. results_gpv \<I> (c x) = {}
[PROOF STEP]
using that step.prems(1)
[PROOF STATE]
proof (prove)
using this:
IO out c \<in> set_spmf (the_gpv gpv)
x \<in> responses_\<I> \<I> out
results_gpv \<I> gpv = {}

goal (1 subgoal):
 1. results_gpv \<I> (c x) = {}
[PROOF STEP]
by(auto intro: results_gpv.IO)
[PROOF STATE]
proof (state)
this:
\<lbrakk>IO ?out ?c \<in> set_spmf (the_gpv gpv); ?x \<in> responses_\<I> \<I> ?out\<rbrakk> \<Longrightarrow> results_gpv \<I> (?c ?x) = {}

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv. \<lbrakk>results_gpv \<I> gpv = {}; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv' gpv = 0; results_gpv \<I> gpv = {}; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>IO ?out ?c \<in> set_spmf (the_gpv gpv); ?x \<in> responses_\<I> \<I> ?out\<rbrakk> \<Longrightarrow> results_gpv \<I> (?c ?x) = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>IO ?out ?c \<in> set_spmf (the_gpv gpv); ?x \<in> responses_\<I> \<I> ?out\<rbrakk> \<Longrightarrow> results_gpv \<I> (?c ?x) = {}

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) + 0 * ennreal (pmf (the_gpv gpv) None) = 0
[PROOF STEP]
using step.prems
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>IO ?out ?c \<in> set_spmf (the_gpv gpv); ?x \<in> responses_\<I> \<I> ?out\<rbrakk> \<Longrightarrow> results_gpv \<I> (?c ?x) = {}
results_gpv \<I> gpv = {}
\<I> \<turnstile>g gpv \<surd>

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) + 0 * ennreal (pmf (the_gpv gpv) None) = 0
[PROOF STEP]
by(auto 4 4 intro!: nn_integral_zero' split: generat.split intro: results_gpv.Pure cong: INF_cong simp add: step.IH WT_gpv_ContD INF_constant in_outs_\<I>_iff_responses_\<I> dest: WT_gpv_OutD)
[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) + 0 * ennreal (pmf (the_gpv gpv) None) = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expectation_gpv_cmult:
  fixes fail
  assumes "0 < c" and "c \<noteq> \<top>"
  shows "c * expectation_gpv fail \<I> f gpv = expectation_gpv (c * fail) \<I> (\<lambda>x. c * f x) gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * expectation_gpv fail \<I> f gpv = expectation_gpv (c * fail) \<I> (\<lambda>x. c * f x) 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. c * fst x xa = snd x xa)
 2. \<And>gpv. c * \<Squnion> {} = \<Squnion> {}
 3. \<And>fa g gpv. (\<And>gpv. c * fa gpv = g gpv) \<Longrightarrow> c * (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 (\<lambda>x. c * f x) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + c * 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. c * fst x xa = snd x xa)
 2. \<And>gpv. c * \<Squnion> {} = \<Squnion> {}
 3. \<And>fa g gpv. (\<And>gpv. c * fa gpv = g gpv) \<Longrightarrow> c * (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 (\<lambda>x. c * f x) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + c * 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. c * 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. c * fst x xa = snd x xa)

goal (2 subgoals):
 1. \<And>gpv. c * \<Squnion> {} = \<Squnion> {}
 2. \<And>fa g gpv. (\<And>gpv. c * fa gpv = g gpv) \<Longrightarrow> c * (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 (\<lambda>x. c * f x) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + c * fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>gpv. c * \<Squnion> {} = \<Squnion> {}
 2. \<And>fa g gpv. (\<And>gpv. c * fa gpv = g gpv) \<Longrightarrow> c * (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 (\<lambda>x. c * f x) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + c * fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * \<Squnion> {} = \<Squnion> {}
[PROOF STEP]
by(simp add: bot_ennreal_def)
[PROOF STATE]
proof (state)
this:
c * \<Squnion> {} = \<Squnion> {}

goal (1 subgoal):
 1. \<And>fa g gpv. (\<And>gpv. c * fa gpv = g gpv) \<Longrightarrow> c * (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 (\<lambda>x. c * f x) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + c * fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case (step expectation_gpv' expectation_gpv'')
[PROOF STATE]
proof (state)
this:
c * expectation_gpv' ?gpv = expectation_gpv'' ?gpv

goal (1 subgoal):
 1. \<And>fa g gpv. (\<And>gpv. c * fa gpv = g gpv) \<Longrightarrow> c * (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 (\<lambda>x. c * f x) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + c * fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * (\<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> c * f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (the_gpv gpv) + c * fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < c
c \<noteq> \<top>

goal (1 subgoal):
 1. c * (\<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> c * f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (the_gpv gpv) + c * fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
apply(simp add: distrib_left mult_ac nn_integral_cmult[symmetric] generat.case_distrib[where h="(*) _"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < c; c \<noteq> \<top>\<rbrakk> \<Longrightarrow> c * (fail * ennreal (pmf (the_gpv gpv) None)) = \<top> \<or> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c * f x) (\<lambda>x1 x2. c * (\<Sqinter>r\<in>responses_\<I> \<I> x1. expectation_gpv' (x2 r)))) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. c * f x) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)))
[PROOF STEP]
apply(subst INF_mult_left_ennreal, simp_all add: step.IH)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
c * (\<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> c * f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (the_gpv gpv) + c * fail * ennreal (pmf (the_gpv gpv) None)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expectation_gpv_le_exec_gpv:
  assumes callee: "\<And>s x. x \<in> outs_\<I> \<I> \<Longrightarrow> lossless_spmf (callee s x)"
    and WT_gpv: "\<I> \<turnstile>g gpv \<surd>"
    and WT_callee: "\<And>s. \<I> \<turnstile>c callee s \<surd>"
  shows "expectation_gpv 0 \<I> f gpv \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (exec_gpv callee gpv s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 0 \<I> f gpv \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (exec_gpv callee gpv s)
[PROOF STEP]
using WT_gpv
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. expectation_gpv 0 \<I> f gpv \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (exec_gpv callee gpv s)
[PROOF STEP]
proof(induction arbitrary: gpv s rule: parallel_fixp_induct_1_2[OF complete_lattice_partial_function_definitions partial_function_definitions_spmf expectation_gpv.mono exec_gpv.mono expectation_gpv_def exec_gpv_def, case_names adm bottom step])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ccpo.admissible (prod_lub lfp.lub_fun spmf.lub_fun) (rel_prod lfp.le_fun spmf.le_fun) (\<lambda>x. \<forall>xa. \<I> \<turnstile>g xa \<surd> \<longrightarrow> (\<forall>xb. fst x xa \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (curry (snd x) xa xb)))
 2. \<And>gpv s. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> \<Squnion> {} \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (lub_spmf {})
 3. \<And>fa g gpv s. \<lbrakk>\<And>gpv s. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> fa gpv \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (g gpv s); \<I> \<turnstile>g gpv \<surd>\<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))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). g (c x) y)))
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. ccpo.admissible (prod_lub lfp.lub_fun spmf.lub_fun) (rel_prod lfp.le_fun spmf.le_fun) (\<lambda>x. \<forall>xa. \<I> \<turnstile>g xa \<surd> \<longrightarrow> (\<forall>xb. fst x xa \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (curry (snd x) xa xb)))
 2. \<And>gpv s. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> \<Squnion> {} \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (lub_spmf {})
 3. \<And>fa g gpv s. \<lbrakk>\<And>gpv s. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> fa gpv \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (g gpv s); \<I> \<turnstile>g gpv \<surd>\<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))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). g (c x) y)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccpo.admissible (prod_lub lfp.lub_fun spmf.lub_fun) (rel_prod lfp.le_fun spmf.le_fun) (\<lambda>x. \<forall>xa. \<I> \<turnstile>g xa \<surd> \<longrightarrow> (\<forall>xb. fst x xa \<le> \<integral>\<^sup>+ a. (case a of (x, s) \<Rightarrow> f x) \<partial>measure_spmf (curry (snd x) xa xb)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ccpo.admissible (prod_lub lfp.lub_fun spmf.lub_fun) (rel_prod lfp.le_fun spmf.le_fun) (\<lambda>x. \<forall>xa. \<I> \<turnstile>g xa \<surd> \<longrightarrow> (\<forall>xb. fst x xa \<le> \<integral>\<^sup>+ a. (case a of (x, s) \<Rightarrow> f x) \<partial>measure_spmf (curry (snd x) xa xb)))

goal (2 subgoals):
 1. \<And>gpv s. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> \<Squnion> {} \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (lub_spmf {})
 2. \<And>fa g gpv s. \<lbrakk>\<And>gpv s. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> fa gpv \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (g gpv s); \<I> \<turnstile>g gpv \<surd>\<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))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). g (c x) y)))
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:
\<I> \<turnstile>g gpv \<surd>

goal (2 subgoals):
 1. \<And>gpv s. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> \<Squnion> {} \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (lub_spmf {})
 2. \<And>fa g gpv s. \<lbrakk>\<And>gpv s. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> fa gpv \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (g gpv s); \<I> \<turnstile>g gpv \<surd>\<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))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). g (c x) y)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> {} \<le> \<integral>\<^sup>+ a. (case a of (x, s) \<Rightarrow> f x) \<partial>measure_spmf (lub_spmf {})
[PROOF STEP]
by(simp add: bot_ennreal_def)
[PROOF STATE]
proof (state)
this:
\<Squnion> {} \<le> \<integral>\<^sup>+ a. (case a of (x, s) \<Rightarrow> f x) \<partial>measure_spmf (lub_spmf {})

goal (1 subgoal):
 1. \<And>fa g gpv s. \<lbrakk>\<And>gpv s. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> fa gpv \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (g gpv s); \<I> \<turnstile>g gpv \<surd>\<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))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). g (c x) y)))
[PROOF STEP]
case (step expectation_gpv'' exec_gpv')
[PROOF STATE]
proof (state)
this:
\<I> \<turnstile>g ?gpv \<surd> \<Longrightarrow> expectation_gpv'' ?gpv \<le> \<integral>\<^sup>+ a. (case a of (x, s) \<Rightarrow> f x) \<partial>measure_spmf (exec_gpv' ?gpv ?s)
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. \<And>fa g gpv s. \<lbrakk>\<And>gpv s. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> fa gpv \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (g gpv s); \<I> \<turnstile>g gpv \<surd>\<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))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). g (c x) y)))
[PROOF STEP]
have *: "(INF r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (bind_spmf (callee s out) (\<lambda>(r, s'). exec_gpv' (c r) s'))" (is "?lhs \<le> ?rhs")
    if "IO out c \<in> set_spmf (the_gpv gpv)" for out c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
from step.prems that
[PROOF STATE]
proof (chain)
picking this:
\<I> \<turnstile>g gpv \<surd>
IO out c \<in> set_spmf (the_gpv gpv)
[PROOF STEP]
have out: "out \<in> outs_\<I> \<I>"
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd>
IO out c \<in> set_spmf (the_gpv gpv)

goal (1 subgoal):
 1. out \<in> outs_\<I> \<I>
[PROOF STEP]
by(rule WT_gpvD)
[PROOF STATE]
proof (state)
this:
out \<in> outs_\<I> \<I>

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
have "?lhs = \<integral>\<^sup>+ _. ?lhs \<partial>measure_spmf (callee s out)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) = \<integral>\<^sup>+ _. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (callee s out)
[PROOF STEP]
using callee[OF out, THEN lossless_weight_spmfD]
[PROOF STATE]
proof (prove)
using this:
weight_spmf (callee ?s1 out) = 1

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) = \<integral>\<^sup>+ _. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (callee s out)
[PROOF STEP]
by(simp add: measure_spmf.emeasure_eq_measure)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) = \<integral>\<^sup>+ _. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (callee s out)

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) = \<integral>\<^sup>+ _. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (callee s out)

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
have "\<dots> \<le> \<integral>\<^sup>+ (r, s'). expectation_gpv'' (c r) \<partial>measure_spmf (callee s out)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ _. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (callee s out) \<le> \<integral>\<^sup>+ (r, s'). expectation_gpv'' (c r) \<partial>measure_spmf (callee s out)
[PROOF STEP]
by(rule nn_integral_mono_AE)(auto intro: WT_calleeD[OF WT_callee _ out] INF_lower)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ _. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (callee s out) \<le> \<integral>\<^sup>+ (r, s'). expectation_gpv'' (c r) \<partial>measure_spmf (callee s out)

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ _. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (callee s out) \<le> \<integral>\<^sup>+ (r, s'). expectation_gpv'' (c r) \<partial>measure_spmf (callee s out)

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
have "\<dots> \<le> \<integral>\<^sup>+ (r, s'). \<integral>\<^sup>+ (x, _). f x \<partial>measure_spmf (exec_gpv' (c r) s') \<partial>measure_spmf (callee s out)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ (r, s'). expectation_gpv'' (c r) \<partial>measure_spmf (callee s out) \<le> \<integral>\<^sup>+ (r, s'). \<integral>\<^sup>+ (x, uu_). f x \<partial>measure_spmf (exec_gpv' (c r) s') \<partial>measure_spmf (callee s out)
[PROOF STEP]
by(rule nn_integral_mono_AE)(auto intro!: step.IH intro: WT_gpv_ContD[OF step.prems that] WT_calleeD[OF WT_callee _ out])
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ (r, s'). expectation_gpv'' (c r) \<partial>measure_spmf (callee s out) \<le> \<integral>\<^sup>+ (r, s'). \<integral>\<^sup>+ (x, uu_). f x \<partial>measure_spmf (exec_gpv' (c r) s') \<partial>measure_spmf (callee s out)

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ (r, s'). expectation_gpv'' (c r) \<partial>measure_spmf (callee s out) \<le> \<integral>\<^sup>+ (r, s'). \<integral>\<^sup>+ (x, uu_). f x \<partial>measure_spmf (exec_gpv' (c r) s') \<partial>measure_spmf (callee s out)

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
have "\<dots> = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ (r, s'). \<integral>\<^sup>+ (x, uu_). f x \<partial>measure_spmf (exec_gpv' (c r) s') \<partial>measure_spmf (callee s out) = \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
by(simp add: measure_spmf_bind split_def nn_integral_bind[where B="measure_spmf _"] o_def space_subprob_algebra)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ (r, s'). \<integral>\<^sup>+ (x, uu_). f x \<partial>measure_spmf (exec_gpv' (c r) s') \<partial>measure_spmf (callee s out) = \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s out \<bind> (\<lambda>(r, s'). exec_gpv' (c r) s'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
IO ?out ?c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> ?out. expectation_gpv'' (?c r)) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (callee s ?out \<bind> (\<lambda>(r, s'). exec_gpv' (?c r) s'))

goal (1 subgoal):
 1. \<And>fa g gpv s. \<lbrakk>\<And>gpv s. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> fa gpv \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (g gpv s); \<I> \<turnstile>g gpv \<surd>\<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))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ (x, s). f x \<partial>measure_spmf (the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). g (c x) y)))
[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) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ a. (case a of (x, s) \<Rightarrow> f x) \<partial>measure_spmf (the_gpv gpv \<bind> (\<lambda>a. case a of Pure x \<Rightarrow> return_spmf (x, s) | IO out c \<Rightarrow> callee s out \<bind> (\<lambda>a. case a of (x, y) \<Rightarrow> exec_gpv' (c x) y)))
[PROOF STEP]
by(simp add: measure_spmf_bind nn_integral_bind[where B="measure_spmf _"] space_subprob_algebra)
      (simp split!: generat.split add: measure_spmf_return_spmf nn_integral_return * nn_integral_mono_AE)
[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) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ a. (case a of (x, s) \<Rightarrow> f x) \<partial>measure_spmf (the_gpv gpv \<bind> (\<lambda>a. case a of Pure x \<Rightarrow> return_spmf (x, s) | IO out c \<Rightarrow> callee s out \<bind> (\<lambda>a. case a of (x, y) \<Rightarrow> exec_gpv' (c x) y)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weight_gpv_Done [simp]: "weight_gpv \<I> (Done x) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight_gpv \<I> (Generative_Probabilistic_Value.Done x) = 1
[PROOF STEP]
by(simp add: weight_gpv_def)


[STATEMENT]
lemma weight_gpv_Fail [simp]: "weight_gpv \<I> Fail = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight_gpv \<I> Fail = 0
[PROOF STEP]
by(simp add: weight_gpv_def)


[STATEMENT]
lemma weight_gpv_lift_spmf [simp]: "weight_gpv \<I> (lift_spmf p) = weight_spmf p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight_gpv \<I> (lift_spmf p) = weight_spmf p
[PROOF STEP]
by(simp add: weight_gpv_def measure_spmf.emeasure_eq_measure)


[STATEMENT]
lemma weight_gpv_Pause [simp]:
  "(\<And>r. r \<in> responses_\<I> \<I> out \<Longrightarrow> \<I> \<turnstile>g c r \<surd>)
   \<Longrightarrow> weight_gpv \<I> (Pause out c) = (if out \<in> outs_\<I> \<I> then INF r\<in>responses_\<I> \<I> out. weight_gpv \<I> (c r) else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. r \<in> responses_\<I> \<I> out \<Longrightarrow> \<I> \<turnstile>g c r \<surd>) \<Longrightarrow> weight_gpv \<I> (Generative_Probabilistic_Value.Pause out c) = (if out \<in> outs_\<I> \<I> then \<Sqinter>r\<in>responses_\<I> \<I> out. weight_gpv \<I> (c r) else 0)
[PROOF STEP]
apply(clarsimp simp add: weight_gpv_def in_outs_\<I>_iff_responses_\<I>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. r \<in> responses_\<I> \<I> out \<Longrightarrow> \<I> \<turnstile>g c r \<surd>; responses_\<I> \<I> out \<noteq> {}\<rbrakk> \<Longrightarrow> enn2real (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv 0 \<I> (\<lambda>_. 1) (c r)) = (\<Sqinter>x\<in>responses_\<I> \<I> out. enn2real (expectation_gpv 0 \<I> (\<lambda>_. 1) (c x)))
[PROOF STEP]
apply(erule enn2real_INF)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. r \<in> responses_\<I> \<I> out \<Longrightarrow> \<I> \<turnstile>g c r \<surd>) \<Longrightarrow> \<forall>r\<in>responses_\<I> \<I> out. expectation_gpv 0 \<I> (\<lambda>_. 1) (c r) < \<top>
[PROOF STEP]
apply(clarsimp simp add: expectation_gpv_const_le[THEN le_less_trans])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma weight_gpv_nonneg: "0 \<le> weight_gpv \<I> gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> weight_gpv \<I> gpv
[PROOF STEP]
by(simp add: weight_gpv_def)


[STATEMENT]
lemma weight_gpv_le_1: "\<I> \<turnstile>g gpv \<surd> \<Longrightarrow> weight_gpv \<I> gpv \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> weight_gpv \<I> gpv \<le> 1
[PROOF STEP]
using expectation_gpv_const_le[of \<I> gpv 0 1]
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> max 1 0

goal (1 subgoal):
 1. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> weight_gpv \<I> gpv \<le> 1
[PROOF STEP]
by(simp add: weight_gpv_def enn2real_leI max_def)


[STATEMENT]
theorem weight_exec_gpv:
  assumes callee: "\<And>s x. x \<in> outs_\<I> \<I> \<Longrightarrow> lossless_spmf (callee s x)"
    and WT_gpv: "\<I> \<turnstile>g gpv \<surd>"
    and WT_callee: "\<And>s. \<I> \<turnstile>c callee s \<surd>"
  shows "weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have "expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> \<integral>\<^sup>+ (x, s). 1 \<partial>measure_spmf (exec_gpv callee gpv s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> \<integral>\<^sup>+ (x, s). 1 \<partial>measure_spmf (exec_gpv callee gpv s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> outs_\<I> \<I> \<Longrightarrow> lossless_spmf (callee ?s ?x)
\<I> \<turnstile>g gpv \<surd>
\<I> \<turnstile>c callee ?s \<surd>

goal (1 subgoal):
 1. expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> \<integral>\<^sup>+ (x, s). 1 \<partial>measure_spmf (exec_gpv callee gpv s)
[PROOF STEP]
by(rule expectation_gpv_le_exec_gpv)
[PROOF STATE]
proof (state)
this:
expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> \<integral>\<^sup>+ (x, s). 1 \<partial>measure_spmf (exec_gpv callee gpv s)

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> \<integral>\<^sup>+ (x, s). 1 \<partial>measure_spmf (exec_gpv callee gpv s)

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have "\<dots> = weight_spmf (exec_gpv callee gpv s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ (x, s). 1 \<partial>measure_spmf (exec_gpv callee gpv s) = ennreal (weight_spmf (exec_gpv callee gpv s))
[PROOF STEP]
by(simp add: split_def measure_spmf.emeasure_eq_measure)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ (x, s). 1 \<partial>measure_spmf (exec_gpv callee gpv s) = ennreal (weight_spmf (exec_gpv callee gpv s))

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> ennreal (weight_spmf (exec_gpv callee gpv s))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> ennreal (weight_spmf (exec_gpv callee gpv s))

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
by(simp add: weight_gpv_def enn2real_leI)
[PROOF STATE]
proof (state)
this:
weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)

goal:
No subgoals!
[PROOF STEP]
qed