[STATEMENT]
lemma expectation_gpv_\<I>_mono:
  defines "expectation_gpv' \<equiv> expectation_gpv"
  assumes le: "\<I> \<le> \<I>'"
    and WT: "\<I> \<turnstile>g gpv \<surd>"
  shows "expectation_gpv fail \<I> f gpv \<le> expectation_gpv' fail \<I>' f gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv \<le> expectation_gpv' fail \<I>' f gpv
[PROOF STEP]
using WT
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. expectation_gpv fail \<I> f gpv \<le> 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 x \<le> expectation_gpv' fail \<I>' f x)
 2. \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> 0 \<le> expectation_gpv' fail \<I>' f gpv
 3. \<And>expectation_gpv'a gpv. \<lbrakk>\<And>gpv. expectation_gpv'a gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv'a gpv \<le> expectation_gpv' fail \<I>' f 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'a (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv' fail \<I>' f gpv
[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> expectation_gpv' fail \<I>' f x)
 2. \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> 0 \<le> expectation_gpv' fail \<I>' f gpv
 3. \<And>expectation_gpv'a gpv. \<lbrakk>\<And>gpv. expectation_gpv'a gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv'a gpv \<le> expectation_gpv' fail \<I>' f 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'a (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv' fail \<I>' f gpv
[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> expectation_gpv' fail \<I>' f x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lfp.admissible (\<lambda>a. \<forall>x. \<I> \<turnstile>g x \<surd> \<longrightarrow> a x \<le> expectation_gpv' fail \<I>' f x)

goal (2 subgoals):
 1. \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> 0 \<le> expectation_gpv' fail \<I>' f gpv
 2. \<And>expectation_gpv'a gpv. \<lbrakk>\<And>gpv. expectation_gpv'a gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv'a gpv \<le> expectation_gpv' fail \<I>' f 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'a (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv' fail \<I>' f gpv
[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> expectation_gpv' fail \<I>' f gpv
 2. \<And>expectation_gpv'a gpv. \<lbrakk>\<And>gpv. expectation_gpv'a gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv'a gpv \<le> expectation_gpv' fail \<I>' f 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'a (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv' fail \<I>' f gpv
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> expectation_gpv' fail \<I>' f gpv
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> expectation_gpv' fail \<I>' f gpv

goal (1 subgoal):
 1. \<And>expectation_gpv'a gpv. \<lbrakk>\<And>gpv. expectation_gpv'a gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv'a gpv \<le> expectation_gpv' fail \<I>' f 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'a (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv' fail \<I>' f gpv
[PROOF STEP]
case step [unfolded expectation_gpv'_def]: (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' ?gpv \<le> expectation_gpv fail \<I>' f ?gpv
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. \<And>expectation_gpv'a gpv. \<lbrakk>\<And>gpv. expectation_gpv'a gpv \<le> expectation_gpv fail \<I> f gpv; \<And>gpv. \<I> \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv'a gpv \<le> expectation_gpv' fail \<I>' f 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'a (c r))) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv' fail \<I>' f 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) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv' fail \<I>' f gpv
[PROOF STEP]
unfolding expectation_gpv'_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) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv fail \<I>' f gpv
[PROOF STEP]
by(subst expectation_gpv.simps)
      (clarsimp intro!: add_mono nn_integral_mono_AE INF_mono split: generat.split
        , auto intro!: bexI step add_mono nn_integral_mono_AE INF_mono split: generat.split dest: WT_gpvD[OF step.prems] intro!: step dest: responses_\<I>_mono[OF le])
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv' fail \<I>' f gpv

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pgen_lossless_gpv_mono:
  assumes *: "pgen_lossless_gpv fail \<I> gpv"
    and le: "\<I> \<le> \<I>'"
    and WT: "\<I> \<turnstile>g gpv \<surd>"
    and fail: "fail \<le> 1"
  shows "pgen_lossless_gpv fail \<I>' gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pgen_lossless_gpv fail \<I>' gpv
[PROOF STEP]
unfolding pgen_lossless_gpv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv fail \<I>' (\<lambda>_. 1) gpv = 1
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. expectation_gpv fail \<I>' (\<lambda>_. 1) gpv \<le> 1
 2. 1 \<le> expectation_gpv fail \<I>' (\<lambda>_. 1) gpv
[PROOF STEP]
from WT le
[PROOF STATE]
proof (chain)
picking this:
\<I> \<turnstile>g gpv \<surd>
\<I> \<le> \<I>'
[PROOF STEP]
have "\<I>' \<turnstile>g gpv \<surd>"
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd>
\<I> \<le> \<I>'

goal (1 subgoal):
 1. \<I>' \<turnstile>g gpv \<surd>
[PROOF STEP]
by(rule WT_gpv_\<I>_mono)
[PROOF STATE]
proof (state)
this:
\<I>' \<turnstile>g gpv \<surd>

goal (2 subgoals):
 1. expectation_gpv fail \<I>' (\<lambda>_. 1) gpv \<le> 1
 2. 1 \<le> expectation_gpv fail \<I>' (\<lambda>_. 1) gpv
[PROOF STEP]
from expectation_gpv_const_le[OF this, of fail 1] fail
[PROOF STATE]
proof (chain)
picking this:
expectation_gpv fail \<I>' (\<lambda>_. 1) gpv \<le> max 1 fail
fail \<le> 1
[PROOF STEP]
show "expectation_gpv fail \<I>' (\<lambda>_. 1) gpv \<le> 1"
[PROOF STATE]
proof (prove)
using this:
expectation_gpv fail \<I>' (\<lambda>_. 1) gpv \<le> max 1 fail
fail \<le> 1

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

goal (1 subgoal):
 1. 1 \<le> expectation_gpv fail \<I>' (\<lambda>_. 1) gpv
[PROOF STEP]
from expectation_gpv_\<I>_mono[OF le WT, of fail "\<lambda>_. 1"] *
[PROOF STATE]
proof (chain)
picking this:
expectation_gpv fail \<I> (\<lambda>_. 1) gpv \<le> expectation_gpv fail \<I>' (\<lambda>_. 1) gpv
pgen_lossless_gpv fail \<I> gpv
[PROOF STEP]
show "expectation_gpv fail \<I>' (\<lambda>_. 1) gpv \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
expectation_gpv fail \<I> (\<lambda>_. 1) gpv \<le> expectation_gpv fail \<I>' (\<lambda>_. 1) gpv
pgen_lossless_gpv fail \<I> gpv

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma plossless_gpv_mono:
  "\<lbrakk> plossless_gpv \<I> gpv; \<I> \<le> \<I>'; \<I> \<turnstile>g gpv \<surd> \<rbrakk> \<Longrightarrow> plossless_gpv \<I>' gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>plossless_gpv \<I> gpv; \<I> \<le> \<I>'; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> plossless_gpv \<I>' gpv
[PROOF STEP]
by(erule pgen_lossless_gpv_mono; simp)


[STATEMENT]
lemma pfinite_gpv_mono:
  "\<lbrakk> pfinite_gpv \<I> gpv; \<I> \<le> \<I>'; \<I> \<turnstile>g gpv \<surd> \<rbrakk> \<Longrightarrow> pfinite_gpv \<I>' gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pfinite_gpv \<I> gpv; \<I> \<le> \<I>'; \<I> \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> pfinite_gpv \<I>' gpv
[PROOF STEP]
by(erule pgen_lossless_gpv_mono; simp)


[STATEMENT]
lemma pgen_lossless_gpv_parametric': includes lifting_syntax shows
  "((=) ===> rel_\<I> C R ===> rel_gpv'' A C R ===> (=)) pgen_lossless_gpv pgen_lossless_gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> rel_\<I> C R ===> rel_gpv'' A C R ===> (=)) pgen_lossless_gpv pgen_lossless_gpv
[PROOF STEP]
unfolding pgen_lossless_gpv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> rel_\<I> C R ===> rel_gpv'' A C R ===> (=)) (\<lambda>fail \<I> gpv. expectation_gpv fail \<I> (\<lambda>_. 1) gpv = 1) (\<lambda>fail \<I> gpv. expectation_gpv fail \<I> (\<lambda>_. 1) gpv = 1)
[PROOF STEP]
supply expectation_gpv_parametric'[transfer_rule]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> rel_\<I> C R ===> rel_gpv'' A C R ===> (=)) (\<lambda>fail \<I> gpv. expectation_gpv fail \<I> (\<lambda>_. 1) gpv = 1) (\<lambda>fail \<I> gpv. expectation_gpv fail \<I> (\<lambda>_. 1) gpv = 1)
[PROOF STEP]
by transfer_prover


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

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


[STATEMENT]
lemma pgen_lossless_gpv_map_gpv_id [simp]:
  "pgen_lossless_gpv fail \<I> (map_gpv f id gpv) = pgen_lossless_gpv fail \<I> gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pgen_lossless_gpv fail \<I> (map_gpv f id gpv) = pgen_lossless_gpv fail \<I> gpv
[PROOF STEP]
using pgen_lossless_gpv_parametric[of "BNF_Def.Grp UNIV id" "BNF_Def.Grp UNIV f"]
[PROOF STATE]
proof (prove)
using this:
rel_fun (=) (rel_fun (rel_\<I> (BNF_Def.Grp UNIV id) (=)) (rel_fun (rel_gpv (BNF_Def.Grp UNIV f) (BNF_Def.Grp UNIV id)) (=))) pgen_lossless_gpv pgen_lossless_gpv

goal (1 subgoal):
 1. pgen_lossless_gpv fail \<I> (map_gpv f id gpv) = pgen_lossless_gpv fail \<I> gpv
[PROOF STEP]
unfolding gpv.rel_Grp
[PROOF STATE]
proof (prove)
using this:
rel_fun (=) (rel_fun (rel_\<I> (BNF_Def.Grp UNIV id) (=)) (rel_fun (BNF_Def.Grp {x. results'_gpv x \<subseteq> UNIV \<and> outs'_gpv x \<subseteq> UNIV} (map_gpv f id)) (=))) pgen_lossless_gpv pgen_lossless_gpv

goal (1 subgoal):
 1. pgen_lossless_gpv fail \<I> (map_gpv f id gpv) = pgen_lossless_gpv fail \<I> gpv
[PROOF STEP]
by(auto simp add: eq_alt[symmetric] rel_\<I>_eq rel_fun_def Grp_iff)