[STATEMENT]
lemma (in callee_invariant_on) weight_exec_gpv:
  assumes callee: "\<And>s x. \<lbrakk> x \<in> outs_\<I> \<I>; I s \<rbrakk> \<Longrightarrow> lossless_spmf (callee s x)"
  and WT_gpv: "\<I> \<turnstile>g gpv \<surd>"
  and I: "I s"
  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]
including lifting_syntax
[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]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
assume "\<exists>(Rep :: 's' \<Rightarrow> 's) Abs. type_definition Rep Abs {s. I s}"
[PROOF STATE]
proof (state)
this:
\<exists>Rep Abs. type_definition Rep Abs {s. I s}

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Rep Abs. type_definition Rep Abs {s. I s}
[PROOF STEP]
obtain Rep :: "'s' \<Rightarrow> 's" and Abs where td: "type_definition Rep Abs {s. I s}"
[PROOF STATE]
proof (prove)
using this:
\<exists>Rep Abs. type_definition Rep Abs {s. I s}

goal (1 subgoal):
 1. (\<And>Rep Abs. type_definition Rep Abs {s. I s} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
type_definition Rep Abs {s. I s}

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
type_definition Rep Abs {s. I s}
[PROOF STEP]
interpret td: type_definition Rep Abs "{s. I s}"
[PROOF STATE]
proof (prove)
using this:
type_definition Rep Abs {s. I s}

goal (1 subgoal):
 1. type_definition Rep Abs {s. I s}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
define cr where "cr \<equiv> \<lambda>x y. x = Rep y"
[PROOF STATE]
proof (state)
this:
cr \<equiv> \<lambda>x y. x = Rep y

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have [transfer_rule]: "bi_unique cr" "right_total cr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bi_unique cr &&& right_total cr
[PROOF STEP]
using td cr_def
[PROOF STATE]
proof (prove)
using this:
type_definition Rep Abs {s. I s}
cr \<equiv> \<lambda>x y. x = Rep y

goal (1 subgoal):
 1. bi_unique cr &&& right_total cr
[PROOF STEP]
by(rule typedef_bi_unique typedef_right_total)+
[PROOF STATE]
proof (state)
this:
bi_unique cr
right_total cr

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have [transfer_domain_rule]: "Domainp cr = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Domainp cr = I
[PROOF STEP]
using type_definition_Domainp[OF td cr_def]
[PROOF STATE]
proof (prove)
using this:
Domainp cr = (\<lambda>x. x \<in> {s. I s})

goal (1 subgoal):
 1. Domainp cr = I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Domainp cr = I

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
let ?C = "eq_onp (\<lambda>x. x \<in> outs_\<I> \<I>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
define callee' where "callee' \<equiv> (Rep ---> id ---> map_spmf (map_prod id Abs)) callee"
[PROOF STATE]
proof (state)
this:
callee' \<equiv> (Rep ---> id ---> map_spmf (map_prod id Abs)) callee

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have [transfer_rule]: "(cr ===> ?C ===> rel_spmf (rel_prod (=) cr)) callee callee'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr ===> eq_onp (\<lambda>x. x \<in> outs_\<I> \<I>) ===> rel_spmf (rel_prod (=) cr)) callee callee'
[PROOF STEP]
by(auto simp add: callee'_def rel_fun_def cr_def spmf_rel_map prod.rel_map td.Abs_inverse eq_onp_def intro!: rel_spmf_reflI intro: td.Rep[simplified] dest: callee_invariant)
[PROOF STATE]
proof (state)
this:
(cr ===> eq_onp (\<lambda>x. x \<in> outs_\<I> \<I>) ===> rel_spmf (rel_prod (=) cr)) callee callee'

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
define s' where "s' \<equiv> Abs s"
[PROOF STATE]
proof (state)
this:
s' \<equiv> Abs s

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have [transfer_rule]: "cr s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr s s'
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
I s

goal (1 subgoal):
 1. cr s s'
[PROOF STEP]
by(simp add: cr_def s'_def td.Abs_inverse)
[PROOF STATE]
proof (state)
this:
cr s s'

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have [transfer_rule]: "rel_\<I> ?C (=) \<I> \<I>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_\<I> (eq_onp (\<lambda>x. x \<in> outs_\<I> \<I>)) (=) \<I> \<I>
[PROOF STEP]
by(rule rel_\<I>I)(auto simp add: rel_set_eq set_relator_eq_onp eq_onp_same_args dest: eq_onp_to_eq)
[PROOF STATE]
proof (state)
this:
rel_\<I> (eq_onp (\<lambda>x. x \<in> outs_\<I> \<I>)) (=) \<I> \<I>

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
note [transfer_rule] = bi_unique_eq_onp bi_unique_eq
[PROOF STATE]
proof (state)
this:
bi_unique (eq_onp ?P)
bi_unique (=)

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
define gpv' where "gpv' \<equiv> restrict_gpv \<I> gpv"
[PROOF STATE]
proof (state)
this:
gpv' \<equiv> restrict_gpv \<I> gpv

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have [transfer_rule]: "rel_gpv (=) ?C gpv' gpv'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_gpv (=) (eq_onp (\<lambda>x. x \<in> outs_\<I> \<I>)) gpv' gpv'
[PROOF STEP]
by(fold eq_onp_top_eq_eq)(auto simp add: gpv.rel_eq_onp eq_onp_same_args pred_gpv_def gpv'_def dest: in_outs'_restrict_gpvD)
[PROOF STATE]
proof (state)
this:
rel_gpv (=) (eq_onp (\<lambda>x. x \<in> outs_\<I> \<I>)) gpv' gpv'

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
define weight_spmf' :: "('c \<times> 's') spmf \<Rightarrow> real" where "weight_spmf' \<equiv> weight_spmf"
[PROOF STATE]
proof (state)
this:
weight_spmf' \<equiv> weight_spmf

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
define weight_spmf'' :: "('c \<times> 's) spmf \<Rightarrow> real" where "weight_spmf'' \<equiv> weight_spmf"
[PROOF STATE]
proof (state)
this:
weight_spmf'' \<equiv> weight_spmf

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have [transfer_rule]: "(rel_spmf (rel_prod (=) cr) ===> (=)) weight_spmf'' weight_spmf'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_spmf (rel_prod (=) cr) ===> (=)) weight_spmf'' weight_spmf'
[PROOF STEP]
by(simp add: weight_spmf'_def weight_spmf''_def weight_spmf_parametric)
[PROOF STATE]
proof (state)
this:
(rel_spmf (rel_prod (=) cr) ===> (=)) weight_spmf'' weight_spmf'

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have [rule_format]: "\<And>s. \<forall>x \<in> outs_\<I> \<I>. lossless_spmf (callee' s x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>x\<in>outs_\<I> \<I>. lossless_spmf (callee' s x)
[PROOF STEP]
by(transfer)(blast intro: callee)
[PROOF STATE]
proof (state)
this:
?x \<in> outs_\<I> \<I> \<Longrightarrow> lossless_spmf (callee' ?s ?x)

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x \<in> outs_\<I> \<I> \<Longrightarrow> lossless_spmf (callee' ?s ?x)

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have "\<I> \<turnstile>g gpv' \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<turnstile>g gpv' \<surd>
[PROOF STEP]
by(simp add: gpv'_def)
[PROOF STATE]
proof (state)
this:
\<I> \<turnstile>g gpv' \<surd>

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<I> \<turnstile>g gpv' \<surd>

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have "\<And>s. \<I> \<turnstile>c callee' s \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<I> \<turnstile>c callee' s \<surd>
[PROOF STEP]
by transfer(rule WT_callee)
[PROOF STATE]
proof (state)
this:
\<I> \<turnstile>c callee' ?s1 \<surd>

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x \<in> outs_\<I> \<I> \<Longrightarrow> lossless_spmf (callee' ?s ?x)
\<I> \<turnstile>g gpv' \<surd>
\<I> \<turnstile>c callee' ?s1 \<surd>
[PROOF STEP]
have **: "weight_gpv \<I> gpv' \<le> weight_spmf' (exec_gpv callee' gpv' s')"
[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' ?s1 \<surd>

goal (1 subgoal):
 1. weight_gpv \<I> gpv' \<le> weight_spmf' (exec_gpv callee' gpv' s')
[PROOF STEP]
unfolding weight_spmf'_def
[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' ?s1 \<surd>

goal (1 subgoal):
 1. weight_gpv \<I> gpv' \<le> weight_spmf (exec_gpv callee' gpv' s')
[PROOF STEP]
by(rule weight_exec_gpv)
[PROOF STATE]
proof (state)
this:
weight_gpv \<I> gpv' \<le> 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]
have [transfer_rule]: "((=) ===> ?C ===> rel_spmf (rel_prod (=) (=))) callee callee"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> eq_onp (\<lambda>x. x \<in> outs_\<I> \<I>) ===> rel_spmf (rel_prod (=) (=))) callee callee
[PROOF STEP]
by(simp add: rel_fun_def eq_onp_def prod.rel_eq)
[PROOF STATE]
proof (state)
this:
((=) ===> eq_onp (\<lambda>x. x \<in> outs_\<I> \<I>) ===> rel_spmf (rel_prod (=) (=))) callee callee

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have "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]
using **
[PROOF STATE]
proof (prove)
using this:
weight_gpv \<I> gpv' \<le> 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 transfer
[PROOF STATE]
proof (state)
this:
weight_gpv \<I> gpv' \<le> 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]
also
[PROOF STATE]
proof (state)
this:
weight_gpv \<I> gpv' \<le> 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]
have "exec_gpv callee gpv' s = exec_gpv callee gpv s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_gpv callee gpv' s = exec_gpv callee gpv s
[PROOF STEP]
unfolding gpv'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_gpv callee (restrict_gpv \<I> gpv) s = exec_gpv callee gpv s
[PROOF STEP]
using WT_gpv I
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd>
I s

goal (1 subgoal):
 1. exec_gpv callee (restrict_gpv \<I> gpv) s = exec_gpv callee gpv s
[PROOF STEP]
by(rule exec_gpv_restrict_gpv_invariant)
[PROOF STATE]
proof (state)
this:
exec_gpv callee gpv' s = 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:
exec_gpv callee gpv' s = exec_gpv callee gpv s

goal (1 subgoal):
 1. weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have "weight_gpv \<I> gpv' = weight_gpv \<I> gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight_gpv \<I> gpv' = weight_gpv \<I> gpv
[PROOF STEP]
using WT_gpv
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. weight_gpv \<I> gpv' = weight_gpv \<I> gpv
[PROOF STEP]
by(simp add: gpv'_def expectation_gpv_restrict_gpv weight_gpv_def)
[PROOF STATE]
proof (state)
this:
weight_gpv \<I> gpv' = weight_gpv \<I> gpv

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:
weight_gpv \<I> gpv \<le> weight_spmf'' (exec_gpv callee gpv s)
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
weight_gpv \<I> gpv \<le> 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_spmf''_def)
[PROOF STATE]
proof (state)
this:
weight_gpv \<I> gpv \<le> 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]
}
[PROOF STATE]
proof (state)
this:
\<exists>Rep Abs. type_definition Rep Abs {s. I s} \<Longrightarrow> weight_gpv \<I> gpv \<le> 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]
from this[cancel_type_definition] I
[PROOF STATE]
proof (chain)
picking this:
{s. I s} \<noteq> {} \<Longrightarrow> weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
I s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{s. I s} \<noteq> {} \<Longrightarrow> weight_gpv \<I> gpv \<le> weight_spmf (exec_gpv callee gpv s)
I s

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pgen_lossless_gpvI [intro?]: "expectation_gpv fail \<I> (\<lambda>_. 1) gpv = 1 \<Longrightarrow> pgen_lossless_gpv fail \<I> gpv" for fail
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv fail \<I> (\<lambda>_. 1) gpv = 1 \<Longrightarrow> pgen_lossless_gpv fail \<I> gpv
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def)


[STATEMENT]
lemma pgen_lossless_gpvD: "pgen_lossless_gpv fail \<I> gpv \<Longrightarrow> expectation_gpv fail \<I> (\<lambda>_. 1) gpv = 1" for fail
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pgen_lossless_gpv fail \<I> gpv \<Longrightarrow> expectation_gpv fail \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def)


[STATEMENT]
lemma lossless_imp_plossless_gpv:
  assumes "lossless_gpv \<I> gpv" "\<I> \<turnstile>g gpv \<surd>"
  shows "plossless_gpv \<I> gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plossless_gpv \<I> gpv
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. expectation_gpv 0 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
show "expectation_gpv 0 \<I> (\<lambda>_. 1) gpv = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 0 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lossless_gpv \<I> gpv
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. expectation_gpv 0 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
proof(induction rule: lossless_WT_gpv_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> lossless_gpv \<I> (c input); \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> \<I> \<turnstile>g c input \<surd>; \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) (c input) = 1\<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = 1
[PROOF STEP]
case (lossless_gpv p)
[PROOF STATE]
proof (state)
this:
lossless_spmf p
IO ?out ?c \<in> set_spmf p \<Longrightarrow> ?out \<in> outs_\<I> \<I>
\<lbrakk>IO ?out ?c \<in> set_spmf p; ?out \<in> outs_\<I> \<I> \<Longrightarrow> ?input \<in> responses_\<I> \<I> ?out\<rbrakk> \<Longrightarrow> lossless_gpv \<I> (?c ?input)
\<lbrakk>IO ?out ?c \<in> set_spmf p; ?out \<in> outs_\<I> \<I> \<Longrightarrow> ?input \<in> responses_\<I> \<I> ?out\<rbrakk> \<Longrightarrow> \<I> \<turnstile>g ?c ?input \<surd>
\<lbrakk>IO ?out ?c \<in> set_spmf p; ?out \<in> outs_\<I> \<I> \<Longrightarrow> ?input \<in> responses_\<I> \<I> ?out\<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) (?c ?input) = 1

goal (1 subgoal):
 1. \<And>p. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> lossless_gpv \<I> (c input); \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> \<I> \<turnstile>g c input \<surd>; \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) (c input) = 1\<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = 1
[PROOF STEP]
have "expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = nn_integral (measure_spmf p) (case_generat (\<lambda>_. 1) (\<lambda>out c. INF r\<in>responses_\<I> \<I> out. 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = integral\<^sup>N (measure_spmf p) (case_generat (\<lambda>_. 1) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. 1))
[PROOF STEP]
by(subst expectation_gpv.simps)(clarsimp split: generat.split cong: INF_cong simp add: lossless_gpv.IH intro!: nn_integral_cong_AE)
[PROOF STATE]
proof (state)
this:
expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = integral\<^sup>N (measure_spmf p) (case_generat (\<lambda>_. 1) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. 1))

goal (1 subgoal):
 1. \<And>p. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> lossless_gpv \<I> (c input); \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> \<I> \<turnstile>g c input \<surd>; \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) (c input) = 1\<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = integral\<^sup>N (measure_spmf p) (case_generat (\<lambda>_. 1) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. 1))

goal (1 subgoal):
 1. \<And>p. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> lossless_gpv \<I> (c input); \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> \<I> \<turnstile>g c input \<surd>; \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) (c input) = 1\<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = 1
[PROOF STEP]
have "\<dots> = nn_integral (measure_spmf p) (\<lambda>_. 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (measure_spmf p) (case_generat (\<lambda>_. 1) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. 1)) = \<integral>\<^sup>+ _. 1 \<partial>measure_spmf p
[PROOF STEP]
by(intro nn_integral_cong_AE)(auto split: generat.split dest!: lossless_gpv.hyps(2) simp add: in_outs_\<I>_iff_responses_\<I>)
[PROOF STATE]
proof (state)
this:
integral\<^sup>N (measure_spmf p) (case_generat (\<lambda>_. 1) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. 1)) = \<integral>\<^sup>+ _. 1 \<partial>measure_spmf p

goal (1 subgoal):
 1. \<And>p. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> lossless_gpv \<I> (c input); \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> \<I> \<turnstile>g c input \<surd>; \<And>out c input. \<lbrakk>IO out c \<in> set_spmf p; out \<in> outs_\<I> \<I> \<Longrightarrow> input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) (c input) = 1\<rbrakk> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = \<integral>\<^sup>+ _. 1 \<partial>measure_spmf p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = \<integral>\<^sup>+ _. 1 \<partial>measure_spmf p

goal (1 subgoal):
 1. expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = 1
[PROOF STEP]
by(simp add: measure_spmf.emeasure_eq_measure lossless_weight_spmfD lossless_gpv.hyps(1))
[PROOF STATE]
proof (state)
this:
expectation_gpv 0 \<I> (\<lambda>_. 1) (GPV p) = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
expectation_gpv 0 \<I> (\<lambda>_. 1) gpv = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_imp_pfinite_gpv:
  assumes "finite_gpv \<I> gpv" "\<I> \<turnstile>g gpv \<surd>"
  shows "pfinite_gpv \<I> gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pfinite_gpv \<I> gpv
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
show "expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite_gpv \<I> gpv
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
proof(induction rule: finite_gpv_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>gpv. \<lbrakk>\<And>out c input. \<lbrakk>IO out c \<in> set_spmf (the_gpv gpv); input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> finite_gpv \<I> (c input); \<And>out c input. \<lbrakk>IO out c \<in> set_spmf (the_gpv gpv); input \<in> responses_\<I> \<I> out; \<I> \<turnstile>g c input \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) (c input) = 1; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
case (finite_gpv gpv)
[PROOF STATE]
proof (state)
this:
\<lbrakk>IO ?out ?c \<in> set_spmf (the_gpv gpv); ?input \<in> responses_\<I> \<I> ?out\<rbrakk> \<Longrightarrow> finite_gpv \<I> (?c ?input)
\<lbrakk>IO ?out ?c \<in> set_spmf (the_gpv gpv); ?input \<in> responses_\<I> \<I> ?out; \<I> \<turnstile>g ?c ?input \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) (?c ?input) = 1
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. \<And>gpv. \<lbrakk>\<And>out c input. \<lbrakk>IO out c \<in> set_spmf (the_gpv gpv); input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> finite_gpv \<I> (c input); \<And>out c input. \<lbrakk>IO out c \<in> set_spmf (the_gpv gpv); input \<in> responses_\<I> \<I> out; \<I> \<turnstile>g c input \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) (c input) = 1; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>IO ?out ?c \<in> set_spmf (the_gpv gpv); ?input \<in> responses_\<I> \<I> ?out\<rbrakk> \<Longrightarrow> finite_gpv \<I> (?c ?input)
\<lbrakk>IO ?out ?c \<in> set_spmf (the_gpv gpv); ?input \<in> responses_\<I> \<I> ?out; \<I> \<turnstile>g ?c ?input \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) (?c ?input) = 1
\<I> \<turnstile>g gpv \<surd>
[PROOF STEP]
have "expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = nn_integral (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>_. 1) (\<lambda>out c. INF r\<in>responses_\<I> \<I> out. 1)) + pmf (the_gpv gpv) None"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>IO ?out ?c \<in> set_spmf (the_gpv gpv); ?input \<in> responses_\<I> \<I> ?out\<rbrakk> \<Longrightarrow> finite_gpv \<I> (?c ?input)
\<lbrakk>IO ?out ?c \<in> set_spmf (the_gpv gpv); ?input \<in> responses_\<I> \<I> ?out; \<I> \<turnstile>g ?c ?input \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) (?c ?input) = 1
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>_. 1) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. 1)) + ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
by(subst expectation_gpv.simps)(clarsimp intro!: nn_integral_cong_AE INF_cong[OF refl] split!: generat.split simp add: WT_gpv_ContD)
[PROOF STATE]
proof (state)
this:
expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>_. 1) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. 1)) + ennreal (pmf (the_gpv gpv) None)

goal (1 subgoal):
 1. \<And>gpv. \<lbrakk>\<And>out c input. \<lbrakk>IO out c \<in> set_spmf (the_gpv gpv); input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> finite_gpv \<I> (c input); \<And>out c input. \<lbrakk>IO out c \<in> set_spmf (the_gpv gpv); input \<in> responses_\<I> \<I> out; \<I> \<turnstile>g c input \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) (c input) = 1; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>_. 1) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. 1)) + ennreal (pmf (the_gpv gpv) None)

goal (1 subgoal):
 1. \<And>gpv. \<lbrakk>\<And>out c input. \<lbrakk>IO out c \<in> set_spmf (the_gpv gpv); input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> finite_gpv \<I> (c input); \<And>out c input. \<lbrakk>IO out c \<in> set_spmf (the_gpv gpv); input \<in> responses_\<I> \<I> out; \<I> \<turnstile>g c input \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) (c input) = 1; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
have "\<dots> = nn_integral (measure_spmf (the_gpv gpv)) (\<lambda>_. 1) + pmf (the_gpv gpv) None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>_. 1) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. 1)) + ennreal (pmf (the_gpv gpv) None) = \<integral>\<^sup>+ _. 1 \<partial>measure_spmf (the_gpv gpv) + ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
by(intro arg_cong2[where f="(+)"] nn_integral_cong_AE)
        (auto split: generat.split dest!: WT_gpv_OutD[OF finite_gpv.prems] simp add: in_outs_\<I>_iff_responses_\<I>)
[PROOF STATE]
proof (state)
this:
integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>_. 1) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. 1)) + ennreal (pmf (the_gpv gpv) None) = \<integral>\<^sup>+ _. 1 \<partial>measure_spmf (the_gpv gpv) + ennreal (pmf (the_gpv gpv) None)

goal (1 subgoal):
 1. \<And>gpv. \<lbrakk>\<And>out c input. \<lbrakk>IO out c \<in> set_spmf (the_gpv gpv); input \<in> responses_\<I> \<I> out\<rbrakk> \<Longrightarrow> finite_gpv \<I> (c input); \<And>out c input. \<lbrakk>IO out c \<in> set_spmf (the_gpv gpv); input \<in> responses_\<I> \<I> out; \<I> \<turnstile>g c input \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) (c input) = 1; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = \<integral>\<^sup>+ _. 1 \<partial>measure_spmf (the_gpv gpv) + ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = \<integral>\<^sup>+ _. 1 \<partial>measure_spmf (the_gpv gpv) + ennreal (pmf (the_gpv gpv) None)

goal (1 subgoal):
 1. expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
by(simp add: measure_spmf.emeasure_eq_measure ennreal_plus[symmetric] del: ennreal_plus)
        (simp add: pmf_None_eq_weight_spmf)
[PROOF STATE]
proof (state)
this:
expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma plossless_gpv_lossless_spmfD:
  assumes lossless: "plossless_gpv \<I> gpv"
  and WT: "\<I> \<turnstile>g gpv \<surd>"
  shows "lossless_spmf (the_gpv gpv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
have "1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
using lossless
[PROOF STATE]
proof (prove)
using this:
plossless_gpv \<I> gpv

goal (1 subgoal):
 1. 1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
by(auto dest: pgen_lossless_gpvD simp add: weight_gpv_def)
[PROOF STATE]
proof (state)
this:
1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv

goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv

goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
have "\<dots> = \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | IO out c \<Rightarrow> INF r\<in>responses_\<I> \<I> out. expectation_gpv 0 \<I> (\<lambda>_. 1) (c r)) \<partial>measure_spmf (the_gpv gpv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 0 \<I> (\<lambda>_. 1) gpv = \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv 0 \<I> (\<lambda>_. 1) (c r)) \<partial>measure_spmf (the_gpv gpv)
[PROOF STEP]
by(subst expectation_gpv.simps)(auto)
[PROOF STATE]
proof (state)
this:
expectation_gpv 0 \<I> (\<lambda>_. 1) gpv = \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv 0 \<I> (\<lambda>_. 1) (c r)) \<partial>measure_spmf (the_gpv gpv)

goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation_gpv 0 \<I> (\<lambda>_. 1) gpv = \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv 0 \<I> (\<lambda>_. 1) (c r)) \<partial>measure_spmf (the_gpv gpv)

goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
have "\<dots> \<le> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | IO out c \<Rightarrow> 1) \<partial>measure_spmf (the_gpv gpv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv 0 \<I> (\<lambda>_. 1) (c r)) \<partial>measure_spmf (the_gpv gpv) \<le> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | _ \<Rightarrow> 1) \<partial>measure_spmf (the_gpv gpv)
[PROOF STEP]
apply(rule nn_integral_mono_AE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in measure_spmf (the_gpv gpv). (case x of Pure x \<Rightarrow> 1 | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv 0 \<I> (\<lambda>_. 1) (c r)) \<le> (case x of Pure x \<Rightarrow> 1 | _ \<Rightarrow> 1)
[PROOF STEP]
apply(clarsimp split: generat.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv 0 \<I> (\<lambda>_. 1) (x22 r)) \<le> 1
[PROOF STEP]
apply(frule WT_gpv_OutD[OF WT])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>IO x21 x22 \<in> set_spmf (the_gpv gpv); x21 \<in> outs_\<I> \<I>\<rbrakk> \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv 0 \<I> (\<lambda>_. 1) (x22 r)) \<le> 1
[PROOF STEP]
using expectation_gpv_const_le[of \<I> _ 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. \<And>x21 x22. \<lbrakk>IO x21 x22 \<in> set_spmf (the_gpv gpv); x21 \<in> outs_\<I> \<I>\<rbrakk> \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv 0 \<I> (\<lambda>_. 1) (x22 r)) \<le> 1
[PROOF STEP]
apply(auto simp add: in_outs_\<I>_iff_responses_\<I> max_def intro: INF_lower2 WT_gpv_ContD[OF WT] dest: WT_gpv_OutD[OF WT])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv 0 \<I> (\<lambda>_. 1) (c r)) \<partial>measure_spmf (the_gpv gpv) \<le> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | _ \<Rightarrow> 1) \<partial>measure_spmf (the_gpv gpv)

goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv 0 \<I> (\<lambda>_. 1) (c r)) \<partial>measure_spmf (the_gpv gpv) \<le> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | _ \<Rightarrow> 1) \<partial>measure_spmf (the_gpv gpv)

goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
have "\<dots> = weight_spmf (the_gpv gpv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | _ \<Rightarrow> 1) \<partial>measure_spmf (the_gpv gpv) = ennreal (weight_spmf (the_gpv gpv))
[PROOF STEP]
by(auto simp add: weight_spmf_eq_nn_integral_spmf nn_integral_measure_spmf intro!: nn_integral_cong split: generat.split)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> 1 | _ \<Rightarrow> 1) \<partial>measure_spmf (the_gpv gpv) = ennreal (weight_spmf (the_gpv gpv))

goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 \<le> ennreal (weight_spmf (the_gpv gpv))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 \<le> ennreal (weight_spmf (the_gpv gpv))

goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
using weight_spmf_le_1[of "the_gpv gpv"]
[PROOF STATE]
proof (prove)
using this:
1 \<le> ennreal (weight_spmf (the_gpv gpv))
weight_spmf (the_gpv gpv) \<le> 1

goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
by(simp add: lossless_spmf_def)
[PROOF STATE]
proof (state)
this:
lossless_spmf (the_gpv gpv)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma plossless_iff_colossless_pfinite:
  assumes WT: "\<I> \<turnstile>g gpv \<surd>"
  shows "plossless_gpv \<I> gpv \<longleftrightarrow> colossless_gpv \<I> gpv \<and> pfinite_gpv \<I> gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plossless_gpv \<I> gpv = (colossless_gpv \<I> gpv \<and> pfinite_gpv \<I> gpv)
[PROOF STEP]
proof(intro iffI conjI; (elim conjE)?)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. plossless_gpv \<I> gpv \<Longrightarrow> colossless_gpv \<I> gpv
 2. plossless_gpv \<I> gpv \<Longrightarrow> pfinite_gpv \<I> gpv
 3. \<lbrakk>colossless_gpv \<I> gpv; pfinite_gpv \<I> gpv\<rbrakk> \<Longrightarrow> plossless_gpv \<I> gpv
[PROOF STEP]
assume *: "plossless_gpv \<I> gpv"
[PROOF STATE]
proof (state)
this:
plossless_gpv \<I> gpv

goal (3 subgoals):
 1. plossless_gpv \<I> gpv \<Longrightarrow> colossless_gpv \<I> gpv
 2. plossless_gpv \<I> gpv \<Longrightarrow> pfinite_gpv \<I> gpv
 3. \<lbrakk>colossless_gpv \<I> gpv; pfinite_gpv \<I> gpv\<rbrakk> \<Longrightarrow> plossless_gpv \<I> gpv
[PROOF STEP]
show "colossless_gpv \<I> gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. colossless_gpv \<I> gpv
[PROOF STEP]
using * WT
[PROOF STATE]
proof (prove)
using this:
plossless_gpv \<I> gpv
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. colossless_gpv \<I> gpv
[PROOF STEP]
proof(coinduction arbitrary: gpv)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>gpva. \<lbrakk>plossless_gpv \<I> gpva; \<I> \<turnstile>g gpva \<surd>\<rbrakk> \<Longrightarrow> lossless_spmf (the_gpv gpva) \<and> (\<forall>out c input. IO out c \<in> set_spmf (the_gpv gpva) \<longrightarrow> input \<in> responses_\<I> \<I> out \<longrightarrow> (\<exists>gpv. c input = gpv \<and> plossless_gpv \<I> gpv \<and> \<I> \<turnstile>g gpv \<surd>) \<or> colossless_gpv \<I> (c input))
[PROOF STEP]
case (colossless_gpv gpv)
[PROOF STATE]
proof (state)
this:
plossless_gpv \<I> gpv
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. \<And>gpva. \<lbrakk>plossless_gpv \<I> gpva; \<I> \<turnstile>g gpva \<surd>\<rbrakk> \<Longrightarrow> lossless_spmf (the_gpv gpva) \<and> (\<forall>out c input. IO out c \<in> set_spmf (the_gpv gpva) \<longrightarrow> input \<in> responses_\<I> \<I> out \<longrightarrow> (\<exists>gpv. c input = gpv \<and> plossless_gpv \<I> gpv \<and> \<I> \<turnstile>g gpv \<surd>) \<or> colossless_gpv \<I> (c input))
[PROOF STEP]
have ?lossless_spmf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
using colossless_gpv
[PROOF STATE]
proof (prove)
using this:
plossless_gpv \<I> gpv
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv)
[PROOF STEP]
by(rule plossless_gpv_lossless_spmfD)
[PROOF STATE]
proof (state)
this:
lossless_spmf (the_gpv gpv)

goal (1 subgoal):
 1. \<And>gpva. \<lbrakk>plossless_gpv \<I> gpva; \<I> \<turnstile>g gpva \<surd>\<rbrakk> \<Longrightarrow> lossless_spmf (the_gpv gpva) \<and> (\<forall>out c input. IO out c \<in> set_spmf (the_gpv gpva) \<longrightarrow> input \<in> responses_\<I> \<I> out \<longrightarrow> (\<exists>gpv. c input = gpv \<and> plossless_gpv \<I> gpv \<and> \<I> \<turnstile>g gpv \<surd>) \<or> colossless_gpv \<I> (c input))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lossless_spmf (the_gpv gpv)

goal (1 subgoal):
 1. \<And>gpva. \<lbrakk>plossless_gpv \<I> gpva; \<I> \<turnstile>g gpva \<surd>\<rbrakk> \<Longrightarrow> lossless_spmf (the_gpv gpva) \<and> (\<forall>out c input. IO out c \<in> set_spmf (the_gpv gpva) \<longrightarrow> input \<in> responses_\<I> \<I> out \<longrightarrow> (\<exists>gpv. c input = gpv \<and> plossless_gpv \<I> gpv \<and> \<I> \<turnstile>g gpv \<surd>) \<or> colossless_gpv \<I> (c input))
[PROOF STEP]
have ?continuation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>out c input. IO out c \<in> set_spmf (the_gpv gpv) \<longrightarrow> input \<in> responses_\<I> \<I> out \<longrightarrow> (\<exists>gpv. c input = gpv \<and> plossless_gpv \<I> gpv \<and> \<I> \<turnstile>g gpv \<surd>) \<or> colossless_gpv \<I> (c input)
[PROOF STEP]
using colossless_gpv
[PROOF STATE]
proof (prove)
using this:
plossless_gpv \<I> gpv
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. \<forall>out c input. IO out c \<in> set_spmf (the_gpv gpv) \<longrightarrow> input \<in> responses_\<I> \<I> out \<longrightarrow> (\<exists>gpv. c input = gpv \<and> plossless_gpv \<I> gpv \<and> \<I> \<turnstile>g gpv \<surd>) \<or> colossless_gpv \<I> (c input)
[PROOF STEP]
by(auto intro: plossless_gpv_ContD WT_gpv_ContD)
[PROOF STATE]
proof (state)
this:
\<forall>out c input. IO out c \<in> set_spmf (the_gpv gpv) \<longrightarrow> input \<in> responses_\<I> \<I> out \<longrightarrow> (\<exists>gpv. c input = gpv \<and> plossless_gpv \<I> gpv \<and> \<I> \<turnstile>g gpv \<surd>) \<or> colossless_gpv \<I> (c input)

goal (1 subgoal):
 1. \<And>gpva. \<lbrakk>plossless_gpv \<I> gpva; \<I> \<turnstile>g gpva \<surd>\<rbrakk> \<Longrightarrow> lossless_spmf (the_gpv gpva) \<and> (\<forall>out c input. IO out c \<in> set_spmf (the_gpv gpva) \<longrightarrow> input \<in> responses_\<I> \<I> out \<longrightarrow> (\<exists>gpv. c input = gpv \<and> plossless_gpv \<I> gpv \<and> \<I> \<turnstile>g gpv \<surd>) \<or> colossless_gpv \<I> (c input))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lossless_spmf (the_gpv gpv)
\<forall>out c input. IO out c \<in> set_spmf (the_gpv gpv) \<longrightarrow> input \<in> responses_\<I> \<I> out \<longrightarrow> (\<exists>gpv. c input = gpv \<and> plossless_gpv \<I> gpv \<and> \<I> \<turnstile>g gpv \<surd>) \<or> colossless_gpv \<I> (c input)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lossless_spmf (the_gpv gpv)
\<forall>out c input. IO out c \<in> set_spmf (the_gpv gpv) \<longrightarrow> input \<in> responses_\<I> \<I> out \<longrightarrow> (\<exists>gpv. c input = gpv \<and> plossless_gpv \<I> gpv \<and> \<I> \<turnstile>g gpv \<surd>) \<or> colossless_gpv \<I> (c input)

goal (1 subgoal):
 1. lossless_spmf (the_gpv gpv) \<and> (\<forall>out c input. IO out c \<in> set_spmf (the_gpv gpv) \<longrightarrow> input \<in> responses_\<I> \<I> out \<longrightarrow> (\<exists>gpv. c input = gpv \<and> plossless_gpv \<I> gpv \<and> \<I> \<turnstile>g gpv \<surd>) \<or> colossless_gpv \<I> (c input))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
lossless_spmf (the_gpv gpv) \<and> (\<forall>out c input. IO out c \<in> set_spmf (the_gpv gpv) \<longrightarrow> input \<in> responses_\<I> \<I> out \<longrightarrow> (\<exists>gpv. c input = gpv \<and> plossless_gpv \<I> gpv \<and> \<I> \<turnstile>g gpv \<surd>) \<or> colossless_gpv \<I> (c input))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
colossless_gpv \<I> gpv

goal (2 subgoals):
 1. plossless_gpv \<I> gpv \<Longrightarrow> pfinite_gpv \<I> gpv
 2. \<lbrakk>colossless_gpv \<I> gpv; pfinite_gpv \<I> gpv\<rbrakk> \<Longrightarrow> plossless_gpv \<I> gpv
[PROOF STEP]
show "pfinite_gpv \<I> gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pfinite_gpv \<I> gpv
[PROOF STEP]
unfolding pgen_lossless_gpv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = 1
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. expectation_gpv 1 \<I> (\<lambda>_. 1) gpv \<le> 1
 2. 1 \<le> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
from expectation_gpv_const_le[OF WT, of 1 1]
[PROOF STATE]
proof (chain)
picking this:
expectation_gpv 1 \<I> (\<lambda>_. 1) gpv \<le> max 1 1
[PROOF STEP]
show "expectation_gpv 1 \<I> (\<lambda>_. 1) gpv \<le> 1"
[PROOF STATE]
proof (prove)
using this:
expectation_gpv 1 \<I> (\<lambda>_. 1) gpv \<le> max 1 1

goal (1 subgoal):
 1. expectation_gpv 1 \<I> (\<lambda>_. 1) gpv \<le> 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
expectation_gpv 1 \<I> (\<lambda>_. 1) gpv \<le> 1

goal (1 subgoal):
 1. 1 \<le> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
have "1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
plossless_gpv \<I> gpv

goal (1 subgoal):
 1. 1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def)
[PROOF STATE]
proof (state)
this:
1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv

goal (1 subgoal):
 1. 1 \<le> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv

goal (1 subgoal):
 1. 1 \<le> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
have "\<dots> \<le> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
by(rule expectation_gpv_mono) simp_all
[PROOF STATE]
proof (state)
this:
expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv

goal (1 subgoal):
 1. 1 \<le> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 \<le> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
show "1 \<le> \<dots>"
[PROOF STATE]
proof (prove)
using this:
1 \<le> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv

goal (1 subgoal):
 1. 1 \<le> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
1 \<le> expectation_gpv 1 \<I> (\<lambda>_. 1) gpv

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pfinite_gpv \<I> gpv

goal (1 subgoal):
 1. \<lbrakk>colossless_gpv \<I> gpv; pfinite_gpv \<I> gpv\<rbrakk> \<Longrightarrow> plossless_gpv \<I> gpv
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>colossless_gpv \<I> gpv; pfinite_gpv \<I> gpv\<rbrakk> \<Longrightarrow> plossless_gpv \<I> gpv
[PROOF STEP]
show "plossless_gpv \<I> gpv" if "colossless_gpv \<I> gpv" and "pfinite_gpv \<I> gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plossless_gpv \<I> gpv
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
colossless_gpv \<I> gpv
pfinite_gpv \<I> gpv

goal (1 subgoal):
 1. plossless_gpv \<I> gpv
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def cong: expectation_gpv_cong_fail)
[PROOF STATE]
proof (state)
this:
\<lbrakk>colossless_gpv \<I> gpv; pfinite_gpv \<I> gpv\<rbrakk> \<Longrightarrow> plossless_gpv \<I> gpv

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pgen_lossless_gpv_Done [simp]: "pgen_lossless_gpv fail \<I> (Done x)" for fail
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pgen_lossless_gpv fail \<I> (Generative_Probabilistic_Value.Done x)
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def)


[STATEMENT]
lemma pgen_lossless_gpv_Fail [simp]: "pgen_lossless_gpv fail \<I> Fail \<longleftrightarrow> fail = 1" for fail
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pgen_lossless_gpv fail \<I> Fail = (fail = 1)
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def)


[STATEMENT]
lemma pgen_lossless_gpv_PauseI [simp, intro!]:
  "\<lbrakk> out \<in> outs_\<I> \<I>; \<And>r. r \<in> responses_\<I> \<I> out \<Longrightarrow> pgen_lossless_gpv fail \<I> (c r) \<rbrakk>
   \<Longrightarrow> pgen_lossless_gpv fail \<I> (Pause out c)" for fail
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>out \<in> outs_\<I> \<I>; \<And>r. r \<in> responses_\<I> \<I> out \<Longrightarrow> pgen_lossless_gpv fail \<I> (c r)\<rbrakk> \<Longrightarrow> pgen_lossless_gpv fail \<I> (Generative_Probabilistic_Value.Pause out c)
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def weight_gpv_def in_outs_\<I>_iff_responses_\<I>)


[STATEMENT]
lemma pgen_lossless_gpv_bindI [simp, intro!]:
  "\<lbrakk> pgen_lossless_gpv fail \<I> gpv; \<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> pgen_lossless_gpv fail \<I> (f x) \<rbrakk>
  \<Longrightarrow> pgen_lossless_gpv fail \<I> (bind_gpv gpv f)" for fail
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pgen_lossless_gpv fail \<I> gpv; \<And>x. x \<in> results_gpv \<I> gpv \<Longrightarrow> pgen_lossless_gpv fail \<I> (f x)\<rbrakk> \<Longrightarrow> pgen_lossless_gpv fail \<I> (gpv \<bind> f)
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def weight_gpv_def o_def cong: expectation_gpv_cong)


[STATEMENT]
lemma pgen_lossless_gpv_lift_spmf [simp]:
  "pgen_lossless_gpv fail \<I> (lift_spmf p) \<longleftrightarrow> lossless_spmf p \<or> fail = 1" for fail
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pgen_lossless_gpv fail \<I> (lift_spmf p) = (lossless_spmf p \<or> fail = 1)
[PROOF STEP]
apply(cases fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>0 \<le> r; fail = ennreal r\<rbrakk> \<Longrightarrow> pgen_lossless_gpv fail \<I> (lift_spmf p) = (lossless_spmf p \<or> fail = 1)
 2. fail = \<top> \<Longrightarrow> pgen_lossless_gpv fail \<I> (lift_spmf p) = (lossless_spmf p \<or> fail = 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> r_; fail = ennreal r_\<rbrakk> \<Longrightarrow> pgen_lossless_gpv fail \<I> (lift_spmf p) = (lossless_spmf p \<or> fail = 1)
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def lossless_spmf_def measure_spmf.emeasure_eq_measure pmf_None_eq_weight_spmf ennreal_minus ennreal_mult[symmetric] weight_spmf_le_1 ennreal_plus[symmetric] del: ennreal_plus)
    (metis add_diff_cancel_left' diff_add_cancel eq_iff_diff_eq_0 mult_cancel_right1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fail = \<top> \<Longrightarrow> pgen_lossless_gpv fail \<I> (lift_spmf p) = (lossless_spmf p \<or> fail = 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fail = \<top> \<Longrightarrow> pgen_lossless_gpv fail \<I> (lift_spmf p) = (lossless_spmf p \<or> fail = 1)
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def measure_spmf.emeasure_eq_measure ennreal_top_mult lossless_spmf_def add_top weight_spmf_conv_pmf_None)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma expectation_gpv_top_pfinite:
  assumes "pfinite_gpv \<I> gpv"
  shows "expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv = \<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv = \<top>
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv \<noteq> \<top> \<Longrightarrow> False
[PROOF STEP]
assume *: "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv \<noteq> \<top>

goal (1 subgoal):
 1. expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv \<noteq> \<top> \<Longrightarrow> False
[PROOF STEP]
have "1 = expectation_gpv 1 \<I> (\<lambda>_. 1) gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 = expectation_gpv 1 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pfinite_gpv \<I> gpv

goal (1 subgoal):
 1. 1 = expectation_gpv 1 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def)
[PROOF STATE]
proof (state)
this:
1 = expectation_gpv 1 \<I> (\<lambda>_. 1) gpv

goal (1 subgoal):
 1. expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv \<noteq> \<top> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 = expectation_gpv 1 \<I> (\<lambda>_. 1) gpv

goal (1 subgoal):
 1. expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv \<noteq> \<top> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> \<le> expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 1 \<I> (\<lambda>_. 1) gpv \<le> expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv
[PROOF STEP]
by(rule expectation_gpv_mono)(simp_all add: le_fun_def)
[PROOF STATE]
proof (state)
this:
expectation_gpv 1 \<I> (\<lambda>_. 1) gpv \<le> expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv

goal (1 subgoal):
 1. expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv \<noteq> \<top> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation_gpv 1 \<I> (\<lambda>_. 1) gpv \<le> expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv

goal (1 subgoal):
 1. expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv \<noteq> \<top> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv = 0
[PROOF STEP]
using expectation_gpv_cmult[of "2" \<top> \<I> "\<lambda>_. \<top>" gpv] *
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < 2; 2 \<noteq> \<top>\<rbrakk> \<Longrightarrow> 2 * expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv = expectation_gpv (2 * \<top>) \<I> (\<lambda>x. 2 * \<top>) gpv
expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv \<noteq> \<top>

goal (1 subgoal):
 1. expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv = 0
[PROOF STEP]
by(simp add: ennreal_mult_top) (metis ennreal_mult_cancel_left mult.commute mult_numeral_1_right not_gr_zero numeral_eq_one_iff semiring_norm(85) zero_neq_numeral)
[PROOF STATE]
proof (state)
this:
expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv = 0

goal (1 subgoal):
 1. expectation_gpv \<top> \<I> (\<lambda>_. \<top>) gpv \<noteq> \<top> \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 \<le> 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
1 \<le> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pfinite_INF_le_expectation_gpv:
  fixes fail \<I> gpv f
  defines "c \<equiv> min (INF x\<in>results_gpv \<I> gpv. f x) fail"
  assumes fin: "pfinite_gpv \<I> gpv"
  shows "c \<le> expectation_gpv fail \<I> f gpv" (is "?lhs \<le> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
proof(cases "c > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
 2. \<not> 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < c

goal (2 subgoals):
 1. 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
 2. \<not> 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
have "c = c * expectation_gpv 1 \<I> (\<lambda>_. 1) gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = c * expectation_gpv 1 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c \<equiv> min (\<Sqinter> (f ` results_gpv \<I> gpv)) fail
pfinite_gpv \<I> gpv

goal (1 subgoal):
 1. c = c * expectation_gpv 1 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def)
[PROOF STATE]
proof (state)
this:
c = c * expectation_gpv 1 \<I> (\<lambda>_. 1) gpv

goal (2 subgoals):
 1. 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
 2. \<not> 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c = c * expectation_gpv 1 \<I> (\<lambda>_. 1) gpv

goal (2 subgoals):
 1. 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
 2. \<not> 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
have "\<dots> = expectation_gpv c \<I> (\<lambda>_. c) gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = expectation_gpv c \<I> (\<lambda>_. c) gpv
[PROOF STEP]
using fin True
[PROOF STATE]
proof (prove)
using this:
pfinite_gpv \<I> gpv
0 < c

goal (1 subgoal):
 1. c * expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = expectation_gpv c \<I> (\<lambda>_. c) gpv
[PROOF STEP]
by(cases "c = \<top>")(simp_all add: expectation_gpv_top_pfinite ennreal_top_mult expectation_gpv_cmult, simp add: pgen_lossless_gpv_def)
[PROOF STATE]
proof (state)
this:
c * expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = expectation_gpv c \<I> (\<lambda>_. c) gpv

goal (2 subgoals):
 1. 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
 2. \<not> 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c * expectation_gpv 1 \<I> (\<lambda>_. 1) gpv = expectation_gpv c \<I> (\<lambda>_. c) gpv

goal (2 subgoals):
 1. 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
 2. \<not> 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
have "\<dots> \<le> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv c \<I> (\<lambda>_. c) gpv \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
by(rule expectation_gpv_mono_strong)(auto simp add: c_def min_def intro: INF_lower2)
[PROOF STATE]
proof (state)
this:
expectation_gpv c \<I> (\<lambda>_. c) gpv \<le> expectation_gpv fail \<I> f gpv

goal (2 subgoals):
 1. 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
 2. \<not> 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<le> expectation_gpv fail \<I> f gpv

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

goal (1 subgoal):
 1. \<not> 0 < c \<Longrightarrow> c \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
qed simp


[STATEMENT]
lemma plossless_INF_le_expectation_gpv:
  fixes fail
  assumes "plossless_gpv \<I> gpv" and "\<I> \<turnstile>g gpv \<surd>"
  shows "(INF x\<in>results_gpv \<I> gpv. f x) \<le> expectation_gpv fail \<I> f gpv" (is "?lhs \<le> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> (f ` results_gpv \<I> gpv) \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Sqinter> (f ` results_gpv \<I> gpv) \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
plossless_gpv \<I> gpv
\<I> \<turnstile>g gpv \<surd>
[PROOF STEP]
have fin: "pfinite_gpv \<I> gpv" and co: "colossless_gpv \<I> gpv"
[PROOF STATE]
proof (prove)
using this:
plossless_gpv \<I> gpv
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. pfinite_gpv \<I> gpv &&& colossless_gpv \<I> gpv
[PROOF STEP]
by(simp_all add: plossless_iff_colossless_pfinite)
[PROOF STATE]
proof (state)
this:
pfinite_gpv \<I> gpv
colossless_gpv \<I> gpv

goal (1 subgoal):
 1. \<Sqinter> (f ` results_gpv \<I> gpv) \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
have "?lhs \<le> min ?lhs \<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> (f ` results_gpv \<I> gpv) \<le> min (\<Sqinter> (f ` results_gpv \<I> gpv)) \<top>
[PROOF STEP]
by(simp add: min_def)
[PROOF STATE]
proof (state)
this:
\<Sqinter> (f ` results_gpv \<I> gpv) \<le> min (\<Sqinter> (f ` results_gpv \<I> gpv)) \<top>

goal (1 subgoal):
 1. \<Sqinter> (f ` results_gpv \<I> gpv) \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Sqinter> (f ` results_gpv \<I> gpv) \<le> min (\<Sqinter> (f ` results_gpv \<I> gpv)) \<top>

goal (1 subgoal):
 1. \<Sqinter> (f ` results_gpv \<I> gpv) \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
have "\<dots> \<le> expectation_gpv \<top> \<I> f gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (\<Sqinter> (f ` results_gpv \<I> gpv)) \<top> \<le> expectation_gpv \<top> \<I> f gpv
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
pfinite_gpv \<I> gpv

goal (1 subgoal):
 1. min (\<Sqinter> (f ` results_gpv \<I> gpv)) \<top> \<le> expectation_gpv \<top> \<I> f gpv
[PROOF STEP]
by(rule pfinite_INF_le_expectation_gpv)
[PROOF STATE]
proof (state)
this:
min (\<Sqinter> (f ` results_gpv \<I> gpv)) \<top> \<le> expectation_gpv \<top> \<I> f gpv

goal (1 subgoal):
 1. \<Sqinter> (f ` results_gpv \<I> gpv) \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
min (\<Sqinter> (f ` results_gpv \<I> gpv)) \<top> \<le> expectation_gpv \<top> \<I> f gpv

goal (1 subgoal):
 1. \<Sqinter> (f ` results_gpv \<I> gpv) \<le> expectation_gpv fail \<I> f gpv
[PROOF STEP]
have "\<dots> = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv \<top> \<I> f gpv = expectation_gpv fail \<I> f gpv
[PROOF STEP]
using co
[PROOF STATE]
proof (prove)
using this:
colossless_gpv \<I> gpv

goal (1 subgoal):
 1. expectation_gpv \<top> \<I> f gpv = expectation_gpv fail \<I> f gpv
[PROOF STEP]
by(simp add: expectation_gpv_cong_fail)
[PROOF STATE]
proof (state)
this:
expectation_gpv \<top> \<I> f gpv = expectation_gpv fail \<I> f gpv

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

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

goal:
No subgoals!
[PROOF STEP]
qed