[STATEMENT]
lemma (in callee_invariant_on) plossless_exec_gpv:
  assumes lossless: "plossless_gpv \<I> gpv"
    and WT: "\<I> \<turnstile>g gpv \<surd>"
    and callee: "\<And>s x. \<lbrakk> x \<in> outs_\<I> \<I>; I s \<rbrakk> \<Longrightarrow> lossless_spmf (callee s x)"
    and I: "I s"
  shows "lossless_spmf (exec_gpv callee gpv s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (exec_gpv callee gpv s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lossless_spmf (exec_gpv callee gpv s)
[PROOF STEP]
interpret raw_converter_invariant \<I> \<I>' "\<lambda>s x. lift_spmf (callee s x)" I for \<I>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. raw_converter_invariant \<I> \<I>' (\<lambda>s x. lift_spmf (callee s x)) I
[PROOF STEP]
by(rule raw_converter_invariant)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lossless_spmf (exec_gpv callee gpv s)
[PROOF STEP]
have "plossless_gpv \<I>_full (inline (\<lambda>s x. lift_spmf (callee s x)) gpv s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plossless_gpv \<I>_full (inline (\<lambda>s x. lift_spmf (callee s x)) gpv s)
[PROOF STEP]
using lossless WT
[PROOF STATE]
proof (prove)
using this:
plossless_gpv \<I> gpv
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. plossless_gpv \<I>_full (inline (\<lambda>s x. lift_spmf (callee s x)) gpv s)
[PROOF STEP]
by(rule plossless_inline)(simp_all add: callee I)
[PROOF STATE]
proof (state)
this:
plossless_gpv \<I>_full (inline (\<lambda>s x. lift_spmf (callee s x)) gpv s)

goal (1 subgoal):
 1. lossless_spmf (exec_gpv callee gpv s)
[PROOF STEP]
from this[THEN plossless_gpv_lossless_spmfD]
[PROOF STATE]
proof (chain)
picking this:
\<I>_full \<turnstile>g inline (\<lambda>s x. lift_spmf (callee s x)) gpv s \<surd> \<Longrightarrow> lossless_spmf (the_gpv (inline (\<lambda>s x. lift_spmf (callee s x)) gpv s))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<I>_full \<turnstile>g inline (\<lambda>s x. lift_spmf (callee s x)) gpv s \<surd> \<Longrightarrow> lossless_spmf (the_gpv (inline (\<lambda>s x. lift_spmf (callee s x)) gpv s))

goal (1 subgoal):
 1. lossless_spmf (exec_gpv callee gpv s)
[PROOF STEP]
unfolding exec_gpv_conv_inline1
[PROOF STATE]
proof (prove)
using this:
\<I>_full \<turnstile>g inline (\<lambda>s x. lift_spmf (callee s x)) gpv s \<surd> \<Longrightarrow> lossless_spmf (the_gpv (inline (\<lambda>s x. lift_spmf (callee s x)) gpv s))

goal (1 subgoal):
 1. lossless_spmf (map_spmf projl (inline1 (\<lambda>s c. lift_spmf (callee s c)) gpv s))
[PROOF STEP]
by(simp add: inline_sel)
[PROOF STATE]
proof (state)
this:
lossless_spmf (exec_gpv callee gpv s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expectation_gpv_mk_lossless_gpv:
  fixes \<I> y
  defines "rhs \<equiv> expectation_gpv 0 \<I> (\<lambda>_. y)"
  assumes WT: "\<I>' \<turnstile>g gpv \<surd>"
    and outs: "outs_\<I> \<I> = outs_\<I> \<I>'"
  shows "expectation_gpv 0 \<I>' (\<lambda>_. y) gpv \<le> rhs (mk_lossless_gpv (responses_\<I> \<I>') x gpv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 0 \<I>' (\<lambda>_. y) gpv \<le> rhs (mk_lossless_gpv (responses_\<I> \<I>') x gpv)
[PROOF STEP]
using WT
[PROOF STATE]
proof (prove)
using this:
\<I>' \<turnstile>g gpv \<surd>

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

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

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

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I>' (\<lambda>a. y) gpv; \<And>gpv. \<I>' \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv' gpv \<le> rhs (mk_lossless_gpv (responses_\<I> \<I>') x gpv); \<I>' \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. y) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I>' out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> rhs (mk_lossless_gpv (responses_\<I> \<I>') x gpv)
[PROOF STEP]
case step [unfolded rhs_def]: (step expectation_gpv')
[PROOF STATE]
proof (state)
this:
expectation_gpv' ?gpv \<le> expectation_gpv 0 \<I>' (\<lambda>a. y) ?gpv
\<I>' \<turnstile>g ?gpv \<surd> \<Longrightarrow> expectation_gpv' ?gpv \<le> expectation_gpv 0 \<I> (\<lambda>_. y) (mk_lossless_gpv (responses_\<I> \<I>') x ?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>' (\<lambda>a. y) gpv; \<And>gpv. \<I>' \<turnstile>g gpv \<surd> \<Longrightarrow> expectation_gpv' gpv \<le> rhs (mk_lossless_gpv (responses_\<I> \<I>') x gpv); \<I>' \<turnstile>g gpv \<surd>\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. y) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I>' out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> rhs (mk_lossless_gpv (responses_\<I> \<I>') x gpv)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> y | 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> rhs (mk_lossless_gpv (responses_\<I> \<I>') x gpv)
[PROOF STEP]
using step.prems outs
[PROOF STATE]
proof (prove)
using this:
\<I>' \<turnstile>g gpv \<surd>
outs_\<I> \<I> = outs_\<I> \<I>'

goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> y | 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> rhs (mk_lossless_gpv (responses_\<I> \<I>') x gpv)
[PROOF STEP]
unfolding rhs_def
[PROOF STATE]
proof (prove)
using this:
\<I>' \<turnstile>g gpv \<surd>
outs_\<I> \<I> = outs_\<I> \<I>'

goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> y | 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> expectation_gpv 0 \<I> (\<lambda>_. y) (mk_lossless_gpv (responses_\<I> \<I>') x gpv)
[PROOF STEP]
apply(subst expectation_gpv.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<I>' \<turnstile>g gpv \<surd>; outs_\<I> \<I> = outs_\<I> \<I>'\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (\<lambda>x. y) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I>' out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> integral\<^sup>N (measure_spmf (the_gpv (mk_lossless_gpv (responses_\<I> \<I>') x gpv))) (case_generat (\<lambda>x. y) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv 0 \<I> (\<lambda>_. y) (c r))) + 0 * ennreal (pmf (the_gpv (mk_lossless_gpv (responses_\<I> \<I>') x gpv)) None)
[PROOF STEP]
apply(clarsimp intro!: nn_integral_mono_AE INF_mono split!: generat.split if_split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22a m. \<lbrakk>\<I>' \<turnstile>g gpv \<surd>; outs_\<I> \<I> = outs_\<I> \<I>'; IO x21 x22a \<in> set_spmf (the_gpv gpv); m \<in> responses_\<I> \<I> x21; m \<in> responses_\<I> \<I>' x21\<rbrakk> \<Longrightarrow> \<exists>r\<in>responses_\<I> \<I>' x21. expectation_gpv' (x22a r) \<le> expectation_gpv 0 \<I> (\<lambda>_. y) (mk_lossless_gpv (responses_\<I> \<I>') x (x22a m))
 2. \<And>x21 x22a m. \<lbrakk>\<I>' \<turnstile>g gpv \<surd>; outs_\<I> \<I> = outs_\<I> \<I>'; IO x21 x22a \<in> set_spmf (the_gpv gpv); m \<in> responses_\<I> \<I> x21; m \<notin> responses_\<I> \<I>' x21\<rbrakk> \<Longrightarrow> \<exists>r\<in>responses_\<I> \<I>' x21. expectation_gpv' (x22a r) \<le> y
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<I>' \<turnstile>g gpv \<surd>; outs_\<I> \<I> = outs_\<I> \<I>'; IO x21_ x22a_ \<in> set_spmf (the_gpv gpv); m_ \<in> responses_\<I> \<I> x21_; m_ \<in> responses_\<I> \<I>' x21_\<rbrakk> \<Longrightarrow> \<exists>r\<in>responses_\<I> \<I>' x21_. expectation_gpv' (x22a_ r) \<le> expectation_gpv 0 \<I> (\<lambda>_. y) (mk_lossless_gpv (responses_\<I> \<I>') x (x22a_ m_))
[PROOF STEP]
by(frule (1) WT_gpv_OutD)(auto simp add: in_outs_\<I>_iff_responses_\<I> intro!: bexI step.IH[unfolded rhs_def] dest: WT_gpv_ContD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22a m. \<lbrakk>\<I>' \<turnstile>g gpv \<surd>; outs_\<I> \<I> = outs_\<I> \<I>'; IO x21 x22a \<in> set_spmf (the_gpv gpv); m \<in> responses_\<I> \<I> x21; m \<notin> responses_\<I> \<I>' x21\<rbrakk> \<Longrightarrow> \<exists>r\<in>responses_\<I> \<I>' x21. expectation_gpv' (x22a r) \<le> y
[PROOF STEP]
apply(frule (1) WT_gpv_OutD; clarsimp simp add: in_outs_\<I>_iff_responses_\<I> ex_in_conv[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22a m x. \<lbrakk>\<I>' \<turnstile>g gpv \<surd>; outs_\<I> \<I> = outs_\<I> \<I>'; IO x21 x22a \<in> set_spmf (the_gpv gpv); m \<in> responses_\<I> \<I> x21; m \<notin> responses_\<I> \<I>' x21; x \<in> responses_\<I> \<I>' x21\<rbrakk> \<Longrightarrow> \<exists>r\<in>responses_\<I> \<I>' x21. expectation_gpv' (x22a r) \<le> y
[PROOF STEP]
subgoal for out c input input'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<I>' \<turnstile>g gpv \<surd>; outs_\<I> \<I> = outs_\<I> \<I>'; IO out c \<in> set_spmf (the_gpv gpv); input \<in> responses_\<I> \<I> out; input \<notin> responses_\<I> \<I>' out; input' \<in> responses_\<I> \<I>' out\<rbrakk> \<Longrightarrow> \<exists>r\<in>responses_\<I> \<I>' out. expectation_gpv' (c r) \<le> y
[PROOF STEP]
using step.hyps[of "c input'"] expectation_gpv_const_le[of \<I>' "c input'" 0 y]
[PROOF STATE]
proof (prove)
using this:
expectation_gpv' (c input') \<le> expectation_gpv 0 \<I>' (\<lambda>a. y) (c input')
\<I>' \<turnstile>g c input' \<surd> \<Longrightarrow> expectation_gpv 0 \<I>' (\<lambda>_. y) (c input') \<le> max y 0

goal (1 subgoal):
 1. \<lbrakk>\<I>' \<turnstile>g gpv \<surd>; outs_\<I> \<I> = outs_\<I> \<I>'; IO out c \<in> set_spmf (the_gpv gpv); input \<in> responses_\<I> \<I> out; input \<notin> responses_\<I> \<I>' out; input' \<in> responses_\<I> \<I>' out\<rbrakk> \<Longrightarrow> \<exists>r\<in>responses_\<I> \<I>' out. expectation_gpv' (c r) \<le> y
[PROOF STEP]
by- (drule (2) WT_gpv_ContD, fastforce intro: rev_bexI simp add: max_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> y | 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> rhs (mk_lossless_gpv (responses_\<I> \<I>') x gpv)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma plossless_gpv_mk_lossless_gpv:
  assumes "plossless_gpv \<I> gpv"
    and "\<I> \<turnstile>g gpv \<surd>"
    and "outs_\<I> \<I> = outs_\<I> \<I>'"
  shows "plossless_gpv \<I>' (mk_lossless_gpv (responses_\<I> \<I>) x gpv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plossless_gpv \<I>' (mk_lossless_gpv (responses_\<I> \<I>) x gpv)
[PROOF STEP]
using assms expectation_gpv_mk_lossless_gpv[OF assms(2), of \<I>' 1 x]
[PROOF STATE]
proof (prove)
using this:
plossless_gpv \<I> gpv
\<I> \<turnstile>g gpv \<surd>
outs_\<I> \<I> = outs_\<I> \<I>'
outs_\<I> \<I>' = outs_\<I> \<I> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (mk_lossless_gpv (responses_\<I> \<I>) x gpv)

goal (1 subgoal):
 1. plossless_gpv \<I>' (mk_lossless_gpv (responses_\<I> \<I>) x gpv)
[PROOF STEP]
unfolding pgen_lossless_gpv_def
[PROOF STATE]
proof (prove)
using this:
expectation_gpv 0 \<I> (\<lambda>_. 1) gpv = 1
\<I> \<turnstile>g gpv \<surd>
outs_\<I> \<I> = outs_\<I> \<I>'
outs_\<I> \<I>' = outs_\<I> \<I> \<Longrightarrow> expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (mk_lossless_gpv (responses_\<I> \<I>) x gpv)

goal (1 subgoal):
 1. expectation_gpv 0 \<I>' (\<lambda>_. 1) (mk_lossless_gpv (responses_\<I> \<I>) x gpv) = 1
[PROOF STEP]
by -(rule antisym[OF expectation_gpv_const_le[THEN order_trans]]; simp add: WT_gpv_mk_lossless_gpv)


[STATEMENT]
lemma (in callee_invariant_on) exec_gpv_mk_lossless_gpv:
  assumes "\<I> \<turnstile>g gpv \<surd>"
    and "I s"
  shows "exec_gpv callee (mk_lossless_gpv (responses_\<I> \<I>) x gpv) s = exec_gpv callee gpv s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_gpv callee (mk_lossless_gpv (responses_\<I> \<I>) x gpv) s = exec_gpv callee gpv s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd>
I s

goal (1 subgoal):
 1. exec_gpv callee (mk_lossless_gpv (responses_\<I> \<I>) x gpv) s = exec_gpv callee gpv s
[PROOF STEP]
proof(induction arbitrary: gpv s rule: exec_gpv_fixp_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. spmf.admissible (\<lambda>f. \<forall>xa. \<I> \<turnstile>g xa \<surd> \<longrightarrow> (\<forall>xb. I xb \<longrightarrow> f (mk_lossless_gpv (responses_\<I> \<I>) x xa, xb) = f (xa, xb)))
 2. \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> return_pmf None = return_pmf None
 3. \<And>exec_gpv gpv s. \<lbrakk>\<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> exec_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) s = exec_gpv gpv s; \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> the_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv (c x) y)) = the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv (c x) y))
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. spmf.admissible (\<lambda>f. \<forall>xa. \<I> \<turnstile>g xa \<surd> \<longrightarrow> (\<forall>xb. I xb \<longrightarrow> f (mk_lossless_gpv (responses_\<I> \<I>) x xa, xb) = f (xa, xb)))
 2. \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> return_pmf None = return_pmf None
 3. \<And>exec_gpv gpv s. \<lbrakk>\<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> exec_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) s = exec_gpv gpv s; \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> the_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv (c x) y)) = the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv (c x) y))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf.admissible (\<lambda>f. \<forall>xa. \<I> \<turnstile>g xa \<surd> \<longrightarrow> (\<forall>xb. I xb \<longrightarrow> f (mk_lossless_gpv (responses_\<I> \<I>) x xa, xb) = f (xa, xb)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
spmf.admissible (\<lambda>f. \<forall>xa. \<I> \<turnstile>g xa \<surd> \<longrightarrow> (\<forall>xb. I xb \<longrightarrow> f (mk_lossless_gpv (responses_\<I> \<I>) x xa, xb) = f (xa, xb)))

goal (2 subgoals):
 1. \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> return_pmf None = return_pmf None
 2. \<And>exec_gpv gpv s. \<lbrakk>\<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> exec_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) s = exec_gpv gpv s; \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> the_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv (c x) y)) = the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv (c x) y))
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:
\<I> \<turnstile>g gpv \<surd>
I s

goal (2 subgoals):
 1. \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> return_pmf None = return_pmf None
 2. \<And>exec_gpv gpv s. \<lbrakk>\<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> exec_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) s = exec_gpv gpv s; \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> the_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv (c x) y)) = the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv (c x) y))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_pmf None = return_pmf None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
return_pmf None = return_pmf None

goal (1 subgoal):
 1. \<And>exec_gpv gpv s. \<lbrakk>\<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> exec_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) s = exec_gpv gpv s; \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> the_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv (c x) y)) = the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv (c x) y))
[PROOF STEP]
case (step exec_gpv')
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<I> \<turnstile>g ?gpv \<surd>; I ?s\<rbrakk> \<Longrightarrow> exec_gpv' (mk_lossless_gpv (responses_\<I> \<I>) x ?gpv) ?s = exec_gpv' ?gpv ?s
\<I> \<turnstile>g gpv \<surd>
I s

goal (1 subgoal):
 1. \<And>exec_gpv gpv s. \<lbrakk>\<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> exec_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) s = exec_gpv gpv s; \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> the_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv (c x) y)) = the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv (c x) y))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv' (c x) y)) = the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv' (c x) y))
[PROOF STEP]
using step.prems WT_gpv_OutD[OF step.prems(1)]
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd>
I s
IO ?out ?c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> ?out \<in> outs_\<I> \<I>

goal (1 subgoal):
 1. the_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv' (c x) y)) = the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv' (c x) y))
[PROOF STEP]
by(clarsimp simp add: bind_map_spmf intro!: bind_spmf_cong[OF refl] split!: generat.split if_split)
      (force intro!: step.IH dest: WT_callee[THEN WT_calleeD] WT_gpv_OutD callee_invariant WT_gpv_ContD)+
[PROOF STATE]
proof (state)
this:
the_gpv (mk_lossless_gpv (responses_\<I> \<I>) x gpv) \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv' (c x) y)) = the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (x, s)) (\<lambda>out c. callee s out \<bind> (\<lambda>(x, y). exec_gpv' (c x) y))

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (3 subgoals):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. fst x (map_gpv' g h k xa) = snd x xa)
 2. \<And>gpv. \<Squnion> {} = \<Squnion> {}
 3. \<And>fa ga gpv. (\<And>gpv. fa (map_gpv' g h k gpv) = ga gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (map_gpv' g h k gpv))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv (map_gpv' g h k gpv)) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (f \<circ> g) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> (map_\<I> h k \<I>) out. ga (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. fst x (map_gpv' g h k 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. fst x (map_gpv' g h k xa) = snd x xa)

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

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

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

goal (1 subgoal):
 1. \<And>fa ga gpv. (\<And>gpv. fa (map_gpv' g h k gpv) = ga gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (map_gpv' g h k gpv))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv (map_gpv' g h k gpv)) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (f \<circ> g) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> (map_\<I> h k \<I>) out. ga (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
have "pmf (the_gpv (map_gpv' g h k gpv)) None = pmf (the_gpv gpv) None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (the_gpv (map_gpv' g h k gpv)) None = pmf (the_gpv gpv) None
[PROOF STEP]
by(simp add: pmf_map_spmf_None)
[PROOF STATE]
proof (state)
this:
pmf (the_gpv (map_gpv' g h k gpv)) None = pmf (the_gpv gpv) None

goal (1 subgoal):
 1. \<And>fa ga gpv. (\<And>gpv. fa (map_gpv' g h k gpv) = ga gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (map_gpv' g h k gpv))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. fa (c r))) + fail * ennreal (pmf (the_gpv (map_gpv' g h k gpv)) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat (f \<circ> g) (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> (map_\<I> h k \<I>) out. ga (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pmf (the_gpv (map_gpv' g h k gpv)) None = pmf (the_gpv gpv) None
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
pmf (the_gpv (map_gpv' g h k gpv)) None = pmf (the_gpv gpv) None

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. exp1 (c r)) \<partial>measure_spmf (the_gpv (map_gpv' g h k gpv)) + fail * ennreal (pmf (the_gpv (map_gpv' g h k gpv)) None) = \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> (f \<circ> g) x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> (map_\<I> h k \<I>) out. exp2 (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
by simp
      (auto simp add: nn_integral_measure_spmf step.IH image_comp
        split: generat.split intro!: nn_integral_cong)
[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. exp1 (c r)) \<partial>measure_spmf (the_gpv (map_gpv' g h k gpv)) + fail * ennreal (pmf (the_gpv (map_gpv' g h k gpv)) None) = \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> (f \<circ> g) x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> (map_\<I> h k \<I>) out. exp2 (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma plossless_gpv_map_gpv' [simp]:
  "pgen_lossless_gpv b \<I> (map_gpv' f g h gpv) \<longleftrightarrow> pgen_lossless_gpv b (map_\<I> g h \<I>) gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pgen_lossless_gpv b \<I> (map_gpv' f g h gpv) = pgen_lossless_gpv b (map_\<I> g h \<I>) gpv
[PROOF STEP]
unfolding pgen_lossless_gpv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (expectation_gpv b \<I> (\<lambda>_. 1) (map_gpv' f g h gpv) = 1) = (expectation_gpv b (map_\<I> g h \<I>) (\<lambda>_. 1) gpv = 1)
[PROOF STEP]
by(simp add: o_def)


[STATEMENT]
lemma lsnd_empty_impl: "set_empty lsnd_\<alpha> lsnd_invar lsnd_empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_empty lsnd_\<alpha> (\<lambda>_. True) lsnd_empty
[PROOF STEP]
by (unfold_locales) (auto simp add: lsnd_defs)


[STATEMENT]
lemma lsnd_memb_impl: "set_memb lsnd_\<alpha> lsnd_invar lsnd_memb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_memb lsnd_\<alpha> (\<lambda>_. True) lsnd_memb
[PROOF STEP]
by (unfold_locales)(auto simp add: lsnd_defs in_set_member)


[STATEMENT]
lemma lsnd_ins_impl: "set_ins lsnd_\<alpha> lsnd_invar lsnd_ins"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_ins lsnd_\<alpha> (\<lambda>_. True) lsnd_ins
[PROOF STEP]
by (unfold_locales) (auto simp add: lsnd_defs in_set_member)


[STATEMENT]
lemma lsnd_ins_dj_impl: "set_ins_dj lsnd_\<alpha> lsnd_invar lsnd_ins_dj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_ins_dj lsnd_\<alpha> (\<lambda>_. True) lsnd_ins_dj
[PROOF STEP]
by (unfold_locales) (auto simp add: lsnd_defs)


[STATEMENT]
lemma lsnd_delete_impl: "set_delete lsnd_\<alpha> lsnd_invar lsnd_delete"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_delete lsnd_\<alpha> (\<lambda>_. True) lsnd_delete
[PROOF STEP]
by (unfold_locales) (auto simp add: lsnd_delete_def lsnd_\<alpha>_def remove_rev_alt_def)


[STATEMENT]
lemma lsnd_\<alpha>_finite[simp, intro!]: "finite (lsnd_\<alpha> l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (lsnd_\<alpha> l)
[PROOF STEP]
by (auto simp add: lsnd_defs)


[STATEMENT]
lemma lsnd_is_finite_set: "finite_set lsnd_\<alpha> lsnd_invar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_set lsnd_\<alpha> (\<lambda>_. True)
[PROOF STEP]
by (unfold_locales) (auto simp add: lsnd_defs)


[STATEMENT]
lemma lsnd_iteratei_impl: "poly_set_iteratei lsnd_\<alpha> lsnd_invar lsnd_iteratei"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_set_iteratei lsnd_\<alpha> (\<lambda>_. True) lsnd_iteratei
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> finite (lsnd_\<alpha> s)
 2. \<And>s. True \<Longrightarrow> set_iterator (lsnd_iteratei s) (lsnd_\<alpha> s)
[PROOF STEP]
fix l :: "'a list"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> finite (lsnd_\<alpha> s)
 2. \<And>s. True \<Longrightarrow> set_iterator (lsnd_iteratei s) (lsnd_\<alpha> s)
[PROOF STEP]
show "finite (lsnd_\<alpha> l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (lsnd_\<alpha> l)
[PROOF STEP]
unfolding lsnd_\<alpha>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set l)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (lsnd_\<alpha> l)

goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> set_iterator (lsnd_iteratei s) (lsnd_\<alpha> s)
[PROOF STEP]
show "set_iterator (lsnd_iteratei l) (lsnd_\<alpha> l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator (lsnd_iteratei l) (lsnd_\<alpha> l)
[PROOF STEP]
apply (rule set_iterator_I [of "remdups l"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. distinct (remdups l)
 2. lsnd_\<alpha> l = set (remdups l)
 3. lsnd_iteratei l = foldli (remdups l)
[PROOF STEP]
apply (simp_all add: lsnd_\<alpha>_def lsnd_iteratei_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
set_iterator (lsnd_iteratei l) (lsnd_\<alpha> l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lsnd_isEmpty_impl: "set_isEmpty lsnd_\<alpha> lsnd_invar lsnd_isEmpty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_isEmpty lsnd_\<alpha> (\<lambda>_. True) lsnd_isEmpty
[PROOF STEP]
by(unfold_locales)(auto simp add: lsnd_defs)


[STATEMENT]
lemma lsnd_union_impl: "set_union lsnd_\<alpha> lsnd_invar lsnd_\<alpha> lsnd_invar lsnd_\<alpha> lsnd_invar lsnd_union"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_union lsnd_\<alpha> (\<lambda>_. True) lsnd_\<alpha> (\<lambda>_. True) lsnd_\<alpha> (\<lambda>_. True) lsnd_union
[PROOF STEP]
by(unfold_locales)(auto simp add: lsnd_defs)


[STATEMENT]
lemma lsnd_union_dj_impl: "set_union_dj lsnd_\<alpha> lsnd_invar lsnd_\<alpha> lsnd_invar lsnd_\<alpha> lsnd_invar lsnd_union_dj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_union_dj lsnd_\<alpha> (\<lambda>_. True) lsnd_\<alpha> (\<lambda>_. True) lsnd_\<alpha> (\<lambda>_. True) lsnd_union_dj
[PROOF STEP]
by(unfold_locales)(auto simp add: lsnd_defs)


[STATEMENT]
lemma lsnd_to_list_impl: "set_to_list lsnd_\<alpha> lsnd_invar lsnd_to_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_to_list lsnd_\<alpha> (\<lambda>_. True) lsnd_to_list
[PROOF STEP]
by(unfold_locales)(auto simp add: lsnd_defs)


[STATEMENT]
lemma list_to_lsnd_impl: "list_to_set lsnd_\<alpha> lsnd_invar list_to_lsnd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_to_set lsnd_\<alpha> (\<lambda>_. True) list_to_lsnd
[PROOF STEP]
by(unfold_locales)(auto simp add: lsnd_defs)


[STATEMENT]
lemma pi_lsnd[proper_it]:
  "proper_it' lsnd_iteratei lsnd_iteratei"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it' lsnd_iteratei lsnd_iteratei
[PROOF STEP]
apply (rule proper_it'I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. proper_it (lsnd_iteratei s) (lsnd_iteratei s)
[PROOF STEP]
unfolding lsnd_iteratei_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. proper_it (foldli (remdups s)) (foldli (remdups s))
[PROOF STEP]
by (intro icf_proper_iteratorI)


[STATEMENT]
lemma is_fas_alt:
  "is_fas G EC = acyclic ((g_E G \<inter> ((g_E G)\<^sup>* `` g_V0 G \<times> UNIV) - EC))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_fas G EC = acyclic (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)
[PROOF STEP]
unfolding is_fas_def acyclic_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (\<exists>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<in> (g_E G - EC)\<^sup>+)) = (\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+)
[PROOF STEP]
proof (clarsimp, safe)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - EC)\<^sup>+; (x, x) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - EC)\<^sup>+; (x, x) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume A: "(u,u) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+"
[PROOF STATE]
proof (state)
this:
(u, u) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - EC)\<^sup>+; (x, x) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "(u,u)\<in>(g_E G - EC)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(u, u) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+

goal (1 subgoal):
 1. (u, u) \<in> (g_E G - EC)\<^sup>+
[PROOF STEP]
by (rule trancl_mono) blast
[PROOF STATE]
proof (state)
this:
(u, u) \<in> (g_E G - EC)\<^sup>+

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - EC)\<^sup>+; (x, x) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(u, u) \<in> (g_E G - EC)\<^sup>+

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - EC)\<^sup>+; (x, x) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
(u, u) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+
[PROOF STEP]
have "u \<in> (g_E G)\<^sup>* `` g_V0 G"
[PROOF STATE]
proof (prove)
using this:
(u, u) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+

goal (1 subgoal):
 1. u \<in> (g_E G)\<^sup>* `` g_V0 G
[PROOF STEP]
by (cases rule: converse_tranclE) auto
[PROOF STATE]
proof (state)
this:
u \<in> (g_E G)\<^sup>* `` g_V0 G

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - EC)\<^sup>+; (x, x) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<in> (g_E G)\<^sup>* `` g_V0 G

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - EC)\<^sup>+; (x, x) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - EC)\<^sup>+"
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - EC)\<^sup>+

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - EC)\<^sup>+; (x, x) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(u, u) \<in> (g_E G - EC)\<^sup>+
u \<in> (g_E G)\<^sup>* `` g_V0 G
\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - EC)\<^sup>+
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(u, u) \<in> (g_E G - EC)\<^sup>+
u \<in> (g_E G)\<^sup>* `` g_V0 G
\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - EC)\<^sup>+

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

goal (1 subgoal):
 1. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix u v0
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume 1: "v0\<in>g_V0 G" and 2: "(v0,u)\<in>(g_E G)\<^sup>*" and 3: "(u,u)\<in>(g_E G - EC)\<^sup>+"
[PROOF STATE]
proof (state)
this:
v0 \<in> g_V0 G
(v0, u) \<in> (g_E G)\<^sup>*
(u, u) \<in> (g_E G - EC)\<^sup>+

goal (1 subgoal):
 1. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "(u, u) \<in> (Restr (g_E G - EC) ((g_E G)\<^sup>* `` g_V0 G))\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, u) \<in> (Restr (g_E G - EC) ((g_E G)\<^sup>* `` g_V0 G))\<^sup>+
[PROOF STEP]
apply (rule trancl_restrict_reachable[OF 3, where S="(g_E G)\<^sup>* `` g_V0 G"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (g_E G - EC) `` (g_E G)\<^sup>* `` g_V0 G \<subseteq> (g_E G)\<^sup>* `` g_V0 G
 2. u \<in> (g_E G)\<^sup>* `` g_V0 G
[PROOF STEP]
apply (rule order_trans[OF _ rtrancl_image_unfold_right])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (g_E G - EC) `` (g_E G)\<^sup>* `` g_V0 G \<subseteq> g_E G `` (g_E G)\<^sup>* `` g_V0 G
 2. u \<in> (g_E G)\<^sup>* `` g_V0 G
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
v0 \<in> g_V0 G
(v0, u) \<in> (g_E G)\<^sup>*

goal (2 subgoals):
 1. (g_E G - EC) `` (g_E G)\<^sup>* `` g_V0 G \<subseteq> g_E G `` (g_E G)\<^sup>* `` g_V0 G
 2. u \<in> (g_E G)\<^sup>* `` g_V0 G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, u) \<in> (Restr (g_E G - EC) ((g_E G)\<^sup>* `` g_V0 G))\<^sup>+

goal (1 subgoal):
 1. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "(u, u) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(u, u) \<in> (Restr (g_E G - EC) ((g_E G)\<^sup>* `` g_V0 G))\<^sup>+

goal (1 subgoal):
 1. (u, u) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+
[PROOF STEP]
by (rule trancl_mono) auto
[PROOF STATE]
proof (state)
this:
(u, u) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+

goal (1 subgoal):
 1. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(u, u) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+

goal (1 subgoal):
 1. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+"
[PROOF STATE]
proof (state)
this:
\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+

goal (1 subgoal):
 1. \<And>u x. \<lbrakk>\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+; (x, u) \<in> (g_E G)\<^sup>*; x \<in> g_V0 G; (u, u) \<in> (g_E G - EC)\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(u, u) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+
\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(u, u) \<in> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+
\<forall>x. (x, x) \<notin> (g_E G \<inter> (g_E G)\<^sup>* `` g_V0 G \<times> UNIV - EC)\<^sup>+

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fas_more_cong: "state.more s = state.more s' \<Longrightarrow> fas s = fas s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state.more s = state.more s' \<Longrightarrow> fas s = fas s'
[PROOF STEP]
by (cases s, cases s', simp)


[STATEMENT]
lemma [simp]: "s\<lparr> state.more := \<lparr> fas = foo \<rparr> \<rparr> = s \<lparr> fas := foo \<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<lparr>state.more := \<lparr>fas = foo\<rparr>\<rparr> = s\<lparr>fas := foo\<rparr>
[PROOF STEP]
by (cases s) simp


[STATEMENT]
lemma fasI:
  assumes "graph G"
  assumes "finite ((g_E G)\<^sup>* `` g_V0 G)"
  shows "fas G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Feedback_Arcs.fas G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Feedback_Arcs.fas G
[PROOF STEP]
interpret graph G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph G
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Feedback_Arcs.fas G
[PROOF STEP]
interpret fb_graph G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb_graph G
[PROOF STEP]
by (rule fb_graphI_fr[OF assms(2)])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Feedback_Arcs.fas G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Feedback_Arcs.fas G
[PROOF STEP]
by unfold_locales fact
[PROOF STATE]
proof (state)
this:
Feedback_Arcs.fas G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in fas) i_fas_eq_back: "is_invar (\<lambda>s. fas_state.fas s = back_edges s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar (\<lambda>s. fas_state.fas s = back_edges s)
[PROOF STEP]
apply (induct rule: establish_invarI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. on_init fas_params \<le>\<^sub>n SPEC (\<lambda>x. fas_state.fas (empty_state x) = back_edges (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G fas_params s; fas_state.fas s = back_edges s; cond s; \<not> is_break fas_params s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root fas_params v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G fas_params (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> fas_state.fas (s'\<lparr>state.more := x\<rparr>) = back_edges (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G fas_params s; fas_state.fas s = back_edges s; cond s; \<not> is_break fas_params s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish fas_params u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G fas_params (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> fas_state.fas (s'\<lparr>state.more := x\<rparr>) = back_edges (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G fas_params s; fas_state.fas s = back_edges s; cond s; \<not> is_break fas_params s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge fas_params u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G fas_params (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> fas_state.fas (s'\<lparr>state.more := x\<rparr>) = back_edges (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G fas_params s; fas_state.fas s = back_edges s; cond s; \<not> is_break fas_params s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge fas_params u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G fas_params (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> fas_state.fas (s'\<lparr>state.more := x\<rparr>) = back_edges (s'\<lparr>state.more := x\<rparr>))
 6. \<And>s s' u v. \<lbrakk>DFS_invar G fas_params s; fas_state.fas s = back_edges s; cond s; \<not> is_break fas_params s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover fas_params u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G fas_params (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> fas_state.fas (s'\<lparr>state.more := x\<rparr>) = back_edges (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
apply (simp_all add: cond_def cong: fas_more_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fas_state.fas (empty_state \<lparr>fas_state.fas = {}\<rparr>) = {}
[PROOF STEP]
apply (simp add: empty_state_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma find_fas_correct_aux:
    assumes NC: "\<not>cond s"
    shows "is_fas G (fas_state.fas s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_fas G (fas_state.fas s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_fas G (fas_state.fas s)
[PROOF STEP]
note [simp] = fas_eq_back
[PROOF STATE]
proof (state)
this:
fas_state.fas s = back_edges s

goal (1 subgoal):
 1. is_fas G (fas_state.fas s)
[PROOF STEP]
from nc_edges_covered[OF NC] edges_disjoint
[PROOF STATE]
proof (chain)
picking this:
\<not> is_break fas_params s \<Longrightarrow> E \<inter> reachable \<times> UNIV = tree_edges s \<union> cross_edges s \<union> back_edges s
back_edges s \<inter> cross_edges s = {}
back_edges s \<inter> tree_edges s = {}
cross_edges s \<inter> tree_edges s = {}
[PROOF STEP]
have
      "E \<inter> reachable \<times> UNIV - back_edges s = tree_edges s \<union> cross_edges s"
[PROOF STATE]
proof (prove)
using this:
\<not> is_break fas_params s \<Longrightarrow> E \<inter> reachable \<times> UNIV = tree_edges s \<union> cross_edges s \<union> back_edges s
back_edges s \<inter> cross_edges s = {}
back_edges s \<inter> tree_edges s = {}
cross_edges s \<inter> tree_edges s = {}

goal (1 subgoal):
 1. E \<inter> reachable \<times> UNIV - back_edges s = tree_edges s \<union> cross_edges s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E \<inter> reachable \<times> UNIV - back_edges s = tree_edges s \<union> cross_edges s

goal (1 subgoal):
 1. is_fas G (fas_state.fas s)
[PROOF STEP]
with tree_cross_acyclic
[PROOF STATE]
proof (chain)
picking this:
acyclic (tree_edges s \<union> cross_edges s)
E \<inter> reachable \<times> UNIV - back_edges s = tree_edges s \<union> cross_edges s
[PROOF STEP]
show "is_fas G (fas_state.fas s)"
[PROOF STATE]
proof (prove)
using this:
acyclic (tree_edges s \<union> cross_edges s)
E \<inter> reachable \<times> UNIV - back_edges s = tree_edges s \<union> cross_edges s

goal (1 subgoal):
 1. is_fas G (fas_state.fas s)
[PROOF STEP]
unfolding is_fas_alt
[PROOF STATE]
proof (prove)
using this:
acyclic (tree_edges s \<union> cross_edges s)
E \<inter> reachable \<times> UNIV - back_edges s = tree_edges s \<union> cross_edges s

goal (1 subgoal):
 1. acyclic (E \<inter> reachable \<times> UNIV - fas_state.fas s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_fas G (fas_state.fas s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_fas_correct:
  assumes "graph G"
  assumes "finite ((g_E G)\<^sup>* `` g_V0 G)"
  shows "find_fas G \<le> SPEC (is_fas G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_fas G \<le> SPEC (is_fas G)
[PROOF STEP]
unfolding find_fas_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (graph G) \<bind> (\<lambda>_. ASSERT (finite ((g_E G)\<^sup>* `` g_V0 G)) \<bind> (\<lambda>_. param_DFS_defs.it_dfsT G fas_params \<bind> (\<lambda>s. RETURN (fas_state.fas s)))) \<le> SPEC (is_fas G)
[PROOF STEP]
proof (refine_vcg le_ASSERTI order_trans[OF DFS.it_dfsT_correct], clarsimp_all)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G)\<rbrakk> \<Longrightarrow> DFS G fas_params
 4. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); DFS_invar G fas_params x; \<not> param_DFS_defs.cond G fas_params x\<rbrakk> \<Longrightarrow> is_fas G (fas_state.fas x)
[PROOF STEP]
interpret graph G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph G
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G)\<rbrakk> \<Longrightarrow> DFS G fas_params
 4. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); DFS_invar G fas_params x; \<not> param_DFS_defs.cond G fas_params x\<rbrakk> \<Longrightarrow> is_fas G (fas_state.fas x)
[PROOF STEP]
assume "finite ((g_E G)\<^sup>* `` g_V0 G)"
[PROOF STATE]
proof (state)
this:
finite ((g_E G)\<^sup>* `` g_V0 G)

goal (4 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G)\<rbrakk> \<Longrightarrow> DFS G fas_params
 4. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); DFS_invar G fas_params x; \<not> param_DFS_defs.cond G fas_params x\<rbrakk> \<Longrightarrow> is_fas G (fas_state.fas x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite ((g_E G)\<^sup>* `` g_V0 G)
[PROOF STEP]
interpret fb_graph G
[PROOF STATE]
proof (prove)
using this:
finite ((g_E G)\<^sup>* `` g_V0 G)

goal (1 subgoal):
 1. fb_graph G
[PROOF STEP]
by (rule fb_graphI_fr)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G)\<rbrakk> \<Longrightarrow> DFS G fas_params
 4. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); DFS_invar G fas_params x; \<not> param_DFS_defs.cond G fas_params x\<rbrakk> \<Longrightarrow> is_fas G (fas_state.fas x)
[PROOF STEP]
interpret fas
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Feedback_Arcs.fas G
[PROOF STEP]
by unfold_locales fact
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G)\<rbrakk> \<Longrightarrow> DFS G fas_params
 4. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); DFS_invar G fas_params x; \<not> param_DFS_defs.cond G fas_params x\<rbrakk> \<Longrightarrow> is_fas G (fas_state.fas x)
[PROOF STEP]
show "DFS G fas_params"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DFS G fas_params
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
this:
DFS G fas_params

goal (3 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); DFS_invar G fas_params x; \<not> param_DFS_defs.cond G fas_params x\<rbrakk> \<Longrightarrow> is_fas G (fas_state.fas x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); DFS_invar G fas_params x; \<not> param_DFS_defs.cond G fas_params x\<rbrakk> \<Longrightarrow> is_fas G (fas_state.fas x)
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); DFS_invar G fas_params x; \<not> param_DFS_defs.cond G fas_params x\<rbrakk> \<Longrightarrow> is_fas G (fas_state.fas x)
[PROOF STEP]
assume "DFS_invar G fas_params s"
[PROOF STATE]
proof (state)
this:
DFS_invar G fas_params s

goal (3 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); DFS_invar G fas_params x; \<not> param_DFS_defs.cond G fas_params x\<rbrakk> \<Longrightarrow> is_fas G (fas_state.fas x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
DFS_invar G fas_params s
[PROOF STEP]
interpret DFS_invar G fas_params s
[PROOF STATE]
proof (prove)
using this:
DFS_invar G fas_params s

goal (1 subgoal):
 1. DFS_invar G fas_params s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); DFS_invar G fas_params x; \<not> param_DFS_defs.cond G fas_params x\<rbrakk> \<Longrightarrow> is_fas G (fas_state.fas x)
[PROOF STEP]
interpret fas_invar G s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fas_invar G s
[PROOF STEP]
by unfold_locales fact
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); DFS_invar G fas_params x; \<not> param_DFS_defs.cond G fas_params x\<rbrakk> \<Longrightarrow> is_fas G (fas_state.fas x)
[PROOF STEP]
assume "\<not>fas.cond TYPE('b) G s"
[PROOF STATE]
proof (state)
this:
\<not> param_DFS_defs.cond G fas_params s

goal (3 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); DFS_invar G fas_params x; \<not> param_DFS_defs.cond G fas_params x\<rbrakk> \<Longrightarrow> is_fas G (fas_state.fas x)
[PROOF STEP]
thus "is_fas G (fas_state.fas s)"
[PROOF STATE]
proof (prove)
using this:
\<not> param_DFS_defs.cond G fas_params s

goal (1 subgoal):
 1. is_fas G (fas_state.fas s)
[PROOF STEP]
by (rule find_fas_correct_aux)
[PROOF STATE]
proof (state)
this:
is_fas G (fas_state.fas s)

goal (2 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
[PROOF STEP]
qed (rule assms)+


[STATEMENT]
lemma fas_impl: "(si,s)\<in>fas_rel
  \<Longrightarrow> fas_state_impl.fas si = fas_state.fas s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (si, s) \<in> fas_rel \<Longrightarrow> fas_state_impl.fas si = fas_state.fas s
[PROOF STEP]
by (cases si, cases s, simp add: simple_state_rel_def fas_erel_def)


[STATEMENT]
lemma find_fas_impl_refine: "find_fas_impl G \<le> \<Down>Id (find_fas G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_fas_impl G \<le> \<Down> Id (find_fas G)
[PROOF STEP]
unfolding find_fas_impl_def find_fas_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (graph G) \<bind> (\<lambda>_. ASSERT (finite ((g_E G)\<^sup>* `` g_V0 G)) \<bind> (\<lambda>_. tailrec_impl_defs.tailrec_implT G (gen_param_dfs_defs.gds (pre_simple_impl.gbs G) fas_params_impl simple_state.more_update) \<bind> (\<lambda>s. RETURN (fas_state_impl.fas s)))) \<le> \<Down> Id (ASSERT (graph G) \<bind> (\<lambda>_. ASSERT (finite ((g_E G)\<^sup>* `` g_V0 G)) \<bind> (\<lambda>_. param_DFS_defs.it_dfsT G fas_params \<bind> (\<lambda>s. RETURN (fas_state.fas s)))))
[PROOF STEP]
apply (refine_vcg fas.impl_refine)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); graph G; finite ((g_E G)\<^sup>* `` g_V0 G)\<rbrakk> \<Longrightarrow> ??.Feedback_Arcs.fas G
 2. \<And>s sa. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); graph G; finite ((g_E G)\<^sup>* `` g_V0 G); (s, sa) \<in> fas_rel\<rbrakk> \<Longrightarrow> (fas_state_impl.fas s, fas_state.fas sa) \<in> Id
[PROOF STEP]
apply (simp_all add: fas_impl fasI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [autoref_rules]:
  fixes ns_rel vis_rel frel erel
  defines "R \<equiv> \<langle>ns_rel,vis_rel,\<langle>frel,erel\<rangle>fas_state_erel\<rangle>ss_impl_rel"
  shows
    "(fas_state_impl'_ext, fas_state_impl_ext) \<in> frel \<rightarrow> erel \<rightarrow> \<langle>frel,erel\<rangle>fas_state_erel"
    "(fas_impl, fas_state_impl.fas) \<in> R \<rightarrow> frel"
    "(fas_state_impl'.fas_impl_update, fas_update) \<in> (frel \<rightarrow> frel) \<rightarrow> R \<rightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fas_state_impl'_ext, fas_state_impl_ext) \<in> frel \<rightarrow> erel \<rightarrow> \<langle>frel, erel\<rangle>fas_state_erel &&& (fas_impl, fas_state_impl.fas) \<in> R \<rightarrow> frel &&& (fas_impl_update, fas_state_impl.fas_update) \<in> (frel \<rightarrow> frel) \<rightarrow> R \<rightarrow> R
[PROOF STEP]
unfolding fas_state_erel_def ss_impl_rel_def R_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fas_state_impl'_ext, fas_state_impl_ext) \<in> frel \<rightarrow> erel \<rightarrow> {(\<lparr>fas_impl = fi, \<dots> = mi\<rparr>, \<lparr>fas_state_impl.fas = f, \<dots> = m\<rparr>) |fi mi f m. (fi, f) \<in> frel \<and> (mi, m) \<in> erel} &&& (fas_impl, fas_state_impl.fas) \<in> {(\<lparr>ss_stack_impl = si, ss_on_stack_impl = osi, ss_visited_impl = visi, \<dots> = mi\<rparr>, \<lparr>ss_stack = s, on_stack = os, visited = vis, \<dots> = m\<rparr>) |si osi visi mi s os vis m. (si, s) \<in> ns_rel \<and> (osi, os) \<in> vis_rel \<and> (visi, vis) \<in> vis_rel \<and> (mi, m) \<in> {(\<lparr>fas_impl = fi, \<dots> = mi\<rparr>, \<lparr>fas_state_impl.fas = f, \<dots> = m\<rparr>) |fi mi f m. (fi, f) \<in> frel \<and> (mi, m) \<in> erel}} \<rightarrow> frel &&& (fas_impl_update, fas_state_impl.fas_update) \<in> (frel \<rightarrow> frel) \<rightarrow> {(\<lparr>ss_stack_impl = si, ss_on_stack_impl = osi, ss_visited_impl = visi, \<dots> = mi\<rparr>, \<lparr>ss_stack = s, on_stack = os, visited = vis, \<dots> = m\<rparr>) |si osi visi mi s os vis m. (si, s) \<in> ns_rel \<and> (osi, os) \<in> vis_rel \<and> (visi, vis) \<in> vis_rel \<and> (mi, m) \<in> {(\<lparr>fas_impl = fi, \<dots> = mi\<rparr>, \<lparr>fas_state_impl.fas = f, \<dots> = m\<rparr>) |fi mi f m. (fi, f) \<in> frel \<and> (mi, m) \<in> erel}} \<rightarrow> {(\<lparr>ss_stack_impl = si, ss_on_stack_impl = osi, ss_visited_impl = visi, \<dots> = mi\<rparr>, \<lparr>ss_stack = s, on_stack = os, visited = vis, \<dots> = m\<rparr>) |si osi visi mi s os vis m. (si, s) \<in> ns_rel \<and> (osi, os) \<in> vis_rel \<and> (visi, vis) \<in> vis_rel \<and> (mi, m) \<in> {(\<lparr>fas_impl = fi, \<dots> = mi\<rparr>, \<lparr>fas_state_impl.fas = f, \<dots> = m\<rparr>) |fi mi f m. (fi, f) \<in> frel \<and> (mi, m) \<in> erel}}
[PROOF STEP]
by (auto, parametricity)


[STATEMENT]
lemma find_fas_code_refine[refine]:
  fixes V :: "('vi\<times>'v) set"
  assumes "is_bounded_hashcode V eq bhc"
  assumes "(eq,(=)) \<in> V \<rightarrow> V \<rightarrow> bool_rel"
  assumes "is_valid_def_hm_size TYPE ('vi) sz"
  assumes 2: "(Gi, G) \<in> \<langle>Rm, V\<rangle>g_impl_rel_ext"
  shows "RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down>(\<langle>V\<times>\<^sub>rV\<rangle>ahs_rel (prod_bhc bhc bhc)) (find_fas G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) (find_fas G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) (find_fas G)
[PROOF STEP]
note find_fas_code.refine[OF assms]
[PROOF STATE]
proof (state)
this:
RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) (find_fas_impl G)

goal (1 subgoal):
 1. RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) (find_fas G)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) (find_fas_impl G)

goal (1 subgoal):
 1. RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) (find_fas G)
[PROOF STEP]
note find_fas_impl_refine
[PROOF STATE]
proof (state)
this:
find_fas_impl ?G \<le> \<Down> Id (find_fas ?G)

goal (1 subgoal):
 1. RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) (find_fas G)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) (find_fas G)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) (find_fas G)

goal (1 subgoal):
 1. RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) (find_fas G)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) (find_fas G)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem find_fas_code_autoref[autoref_rules]:
  fixes V :: "('vi\<times>'v) set" and bhc
  defines "RR \<equiv> \<langle>\<langle>V\<times>\<^sub>rV\<rangle>ahs_rel (prod_bhc bhc bhc)\<rangle>nres_rel"
  assumes BHC: "SIDE_GEN_ALGO (is_bounded_hashcode V eq bhc)"
  assumes EQ: "GEN_OP eq (=) (V \<rightarrow> V \<rightarrow> bool_rel)"
  assumes VDS: "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE ('vi) sz)"
  assumes 2: "(Gi, G) \<in> \<langle>Rm, V\<rangle>g_impl_rel_ext"
  shows "(RETURN (find_fas_code eq bhc sz Gi),
    (OP find_fas
      ::: \<langle>Rm, V\<rangle>g_impl_rel_ext \<rightarrow> RR)$G)\<in>RR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (RETURN (find_fas_code eq bhc sz Gi), (OP find_fas ::: \<langle>Rm, V\<rangle>g_impl_rel_ext \<rightarrow> RR) $ G) \<in> RR
[PROOF STEP]
unfolding RR_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (RETURN (find_fas_code eq bhc sz Gi), (OP find_fas ::: \<langle>Rm, V\<rangle>g_impl_rel_ext \<rightarrow> \<langle>\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)\<rangle>nres_rel) $ G) \<in> \<langle>\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)\<rangle>nres_rel
[PROOF STEP]
apply (rule nres_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) ((OP find_fas ::: \<langle>Rm, V\<rangle>g_impl_rel_ext \<rightarrow> \<langle>\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)\<rangle>nres_rel) $ G)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
RR \<equiv> \<langle>\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)\<rangle>nres_rel
SIDE_GEN_ALGO (is_bounded_hashcode V eq bhc)
GEN_OP eq (=) (V \<rightarrow> V \<rightarrow> bool_rel)
SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('vi) sz)
(Gi, G) \<in> \<langle>Rm, V\<rangle>g_impl_rel_ext

goal (1 subgoal):
 1. RETURN (find_fas_code eq bhc sz Gi) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)) ((OP find_fas ::: \<langle>Rm, V\<rangle>g_impl_rel_ext \<rightarrow> \<langle>\<langle>V \<times>\<^sub>r V\<rangle>ahs_rel (prod_bhc bhc bhc)\<rangle>nres_rel) $ G)
[PROOF STEP]
by (simp add: find_fas_code_refine)


[STATEMENT]
lemma is_fas_join: "is_fas G (F1 \<union> F2) \<longleftrightarrow>
  is_fas \<lparr> g_V = g_V G, g_E = g_E G - F2, g_V0 = (g_E G)\<^sup>* `` g_V0 G \<rparr> F1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_fas G (F1 \<union> F2) = is_fas \<lparr>g_V = g_V G, g_E = g_E G - F2, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> F1
[PROOF STEP]
unfolding is_fas_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (\<exists>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<in> (g_E G - (F1 \<union> F2))\<^sup>+)) = (\<not> (\<exists>u\<in>(g_E \<lparr>g_V = g_V G, g_E = g_E G - F2, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>)\<^sup>* `` g_V0 \<lparr>g_V = g_V G, g_E = g_E G - F2, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>. (u, u) \<in> (g_E \<lparr>g_V = g_V G, g_E = g_E G - F2, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> - F1)\<^sup>+))
[PROOF STEP]
apply (auto simp: set_diff_diff_left Un_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u x xa. \<lbrakk>\<forall>u\<in>(g_E G)\<^sup>* `` g_V0 G. (u, u) \<notin> (g_E G - (F1 \<union> F2))\<^sup>+; (x, u) \<in> (g_E G - F2)\<^sup>*; (xa, x) \<in> (g_E G)\<^sup>*; xa \<in> g_V0 G; (u, u) \<in> (g_E G - (F1 \<union> F2))\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis ImageI rtrancl_trans subsetCE rtrancl_mono[of "g_E G - F2" "g_E G", OF Diff_subset])


[STATEMENT]
lemma graphI_init:
  assumes "graph G"
  shows "graph \<lparr> g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G \<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. graph \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>
[PROOF STEP]
interpret graph G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph G
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. graph \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. g_V0 \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> \<subseteq> g_V \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>
 2. g_E \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> \<subseteq> g_V \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> \<times> g_V \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>
[PROOF STEP]
using reachable_V
[PROOF STATE]
proof (prove)
using this:
(g_E G)\<^sup>* `` g_V0 G \<subseteq> g_V G

goal (2 subgoals):
 1. g_V0 \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> \<subseteq> g_V \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>
 2. g_E \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> \<subseteq> g_V \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> \<times> g_V \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_E \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> \<subseteq> g_V \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> \<times> g_V \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>
[PROOF STEP]
using E_ss
[PROOF STATE]
proof (prove)
using this:
g_E G \<subseteq> g_V G \<times> g_V G

goal (1 subgoal):
 1. g_E \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> \<subseteq> g_V \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> \<times> g_V \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
graph \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_fas_init_correct:
  assumes [simp, intro!]: "graph G"
  assumes [simp, intro!]: "finite ((g_E G)\<^sup>* `` g_V0 G)"
  shows "find_fas_init G FI \<le> SPEC (\<lambda>fas. is_fas G fas \<and> FI \<subseteq> fas)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_fas_init G FI \<le> SPEC (\<lambda>fas. is_fas G fas \<and> FI \<subseteq> fas)
[PROOF STEP]
unfolding find_fas_init_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (graph G) \<bind> (\<lambda>_. ASSERT (finite ((g_E G)\<^sup>* `` g_V0 G)) \<bind> (\<lambda>_. let nodes = (g_E G)\<^sup>* `` g_V0 G in find_fas \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = nodes\<rparr> \<bind> (\<lambda>fas. RETURN (FI \<union> fas)))) \<le> SPEC (\<lambda>fas. is_fas G fas \<and> FI \<subseteq> fas)
[PROOF STEP]
apply (refine_vcg order_trans[OF find_fas_correct])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. graph G
 2. graph G \<Longrightarrow> finite ((g_E G)\<^sup>* `` g_V0 G)
 3. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G)\<rbrakk> \<Longrightarrow> graph \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>
 4. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G)\<rbrakk> \<Longrightarrow> finite ((g_E \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>)\<^sup>* `` g_V0 \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>)
 5. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); is_fas \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> x\<rbrakk> \<Longrightarrow> is_fas G (FI \<union> x)
 6. \<And>x. \<lbrakk>graph G; finite ((g_E G)\<^sup>* `` g_V0 G); is_fas \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> x\<rbrakk> \<Longrightarrow> FI \<subseteq> FI \<union> x
[PROOF STEP]
apply clarsimp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. graph \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr>
 2. finite ((g_E G - FI)\<^sup>* `` (g_E G)\<^sup>* `` g_V0 G)
 3. \<And>x. is_fas \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> x \<Longrightarrow> is_fas G (FI \<union> x)
[PROOF STEP]
apply (rule graphI_init)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. graph G
 2. finite ((g_E G - FI)\<^sup>* `` (g_E G)\<^sup>* `` g_V0 G)
 3. \<And>x. is_fas \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> x \<Longrightarrow> is_fas G (FI \<union> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite ((g_E G - FI)\<^sup>* `` (g_E G)\<^sup>* `` g_V0 G)
 2. \<And>x. is_fas \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> x \<Longrightarrow> is_fas G (FI \<union> x)
[PROOF STEP]
apply (rule finite_subset[rotated], rule assms)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (g_E G - FI)\<^sup>* `` (g_E G)\<^sup>* `` g_V0 G \<subseteq> (g_E G)\<^sup>* `` g_V0 G
 2. \<And>x. is_fas \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> x \<Longrightarrow> is_fas G (FI \<union> x)
[PROOF STEP]
apply (metis Diff_subset Image_closed_trancl reachable_mono
    rtrancl_image_unfold_right rtrancl_reflcl rtrancl_trancl_reflcl
    trancl_rtrancl_absorb)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. is_fas \<lparr>g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)\<^sup>* `` g_V0 G\<rparr> x \<Longrightarrow> is_fas G (FI \<union> x)
[PROOF STEP]
apply (simp add: is_fas_join[where ?F2.0=FI] Un_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_cast_set[autoref_rules_raw]:
  assumes PRIO_TAG_GEN_ALGO
  assumes INS: "GEN_OP ins Set.insert (Rk\<rightarrow>\<langle>Rk\<rangle>Rs2\<rightarrow>\<langle>Rk\<rangle>Rs2)"
  assumes EM: "GEN_OP emp {} (\<langle>Rk\<rangle>Rs2)"
  assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 tsl)"
  shows "(\<lambda>s. gen_union (\<lambda>x. foldli (tsl x)) ins s emp,CAST)
    \<in> (\<langle>Rk\<rangle>Rs1) \<rightarrow> (\<langle>Rk\<rangle>Rs2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. gen_union (\<lambda>x. foldli (tsl x)) ins s emp, CAST) \<in> \<langle>Rk\<rangle>Rs1 \<rightarrow> \<langle>Rk\<rangle>Rs2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>s. gen_union (\<lambda>x. foldli (tsl x)) ins s emp, CAST) \<in> \<langle>Rk\<rangle>Rs1 \<rightarrow> \<langle>Rk\<rangle>Rs2
[PROOF STEP]
note [autoref_rules] = GEN_OP_D[OF INS]
[PROOF STATE]
proof (state)
this:
(ins, insert) \<in> Rk \<rightarrow> \<langle>Rk\<rangle>Rs2 \<rightarrow> \<langle>Rk\<rangle>Rs2

goal (1 subgoal):
 1. (\<lambda>s. gen_union (\<lambda>x. foldli (tsl x)) ins s emp, CAST) \<in> \<langle>Rk\<rangle>Rs1 \<rightarrow> \<langle>Rk\<rangle>Rs2
[PROOF STEP]
note [autoref_rules] = GEN_OP_D[OF EM]
[PROOF STATE]
proof (state)
this:
(emp, {}) \<in> \<langle>Rk\<rangle>Rs2

goal (1 subgoal):
 1. (\<lambda>s. gen_union (\<lambda>x. foldli (tsl x)) ins s emp, CAST) \<in> \<langle>Rk\<rangle>Rs1 \<rightarrow> \<langle>Rk\<rangle>Rs2
[PROOF STEP]
note [autoref_ga_rules] = SIDE_GEN_ALGO_D[OF IT]
[PROOF STATE]
proof (state)
this:
is_set_to_list Rk Rs1 tsl

goal (1 subgoal):
 1. (\<lambda>s. gen_union (\<lambda>x. foldli (tsl x)) ins s emp, CAST) \<in> \<langle>Rk\<rangle>Rs1 \<rightarrow> \<langle>Rk\<rangle>Rs2
[PROOF STEP]
have 1: "CAST = (\<lambda>s. s \<union> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CAST = (\<lambda>s. s \<union> {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
CAST = (\<lambda>s. s \<union> {})

goal (1 subgoal):
 1. (\<lambda>s. gen_union (\<lambda>x. foldli (tsl x)) ins s emp, CAST) \<in> \<langle>Rk\<rangle>Rs1 \<rightarrow> \<langle>Rk\<rangle>Rs2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. gen_union (\<lambda>x. foldli (tsl x)) ins s emp, CAST) \<in> \<langle>Rk\<rangle>Rs1 \<rightarrow> \<langle>Rk\<rangle>Rs2
[PROOF STEP]
unfolding 1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. gen_union (\<lambda>x. foldli (tsl x)) ins s emp, \<lambda>s. s \<union> {}) \<in> \<langle>Rk\<rangle>Rs1 \<rightarrow> \<langle>Rk\<rangle>Rs2
[PROOF STEP]
by autoref
[PROOF STATE]
proof (state)
this:
(\<lambda>s. gen_union (\<lambda>x. foldli (tsl x)) ins s emp, CAST) \<in> \<langle>Rk\<rangle>Rs1 \<rightarrow> \<langle>Rk\<rangle>Rs2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_fas_init_impl_aux_unfolds:
  "Let (E\<^sup>*``V0) = Let (CAST (E\<^sup>*``V0))"
  "(\<lambda>S. RETURN (FI \<union> S)) = (\<lambda>S. RETURN (FI \<union> CAST S))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Let (E\<^sup>* `` V0) = Let (CAST (E\<^sup>* `` V0)) &&& (\<lambda>S. RETURN (FI \<union> S)) = (\<lambda>S. RETURN (FI \<union> CAST S))
[PROOF STEP]
by simp_all


[STATEMENT]
theorem find_fas_init_code_autoref[autoref_rules]:
  fixes V :: "('vi\<times>'v) set" and bhc
  defines "RR \<equiv> \<langle>V\<times>\<^sub>rV\<rangle>fun_set_rel"
  assumes "SIDE_GEN_ALGO (is_bounded_hashcode V eq bhc)"
  assumes "GEN_OP eq (=) (V \<rightarrow> V \<rightarrow> bool_rel)"
  assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE ('vi) sz)"
  shows "(\<lambda>Gi FIi. RETURN (find_fas_init_code eq bhc sz Gi FIi),find_fas_init)
    \<in> \<langle>Rm, V\<rangle>g_impl_rel_ext \<rightarrow> RR \<rightarrow> \<langle>RR\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>Gi FIi. RETURN (find_fas_init_code eq bhc sz Gi FIi), find_fas_init) \<in> \<langle>Rm, V\<rangle>g_impl_rel_ext \<rightarrow> RR \<rightarrow> \<langle>RR\<rangle>nres_rel
[PROOF STEP]
unfolding RR_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>Gi FIi. RETURN (find_fas_init_code eq bhc sz Gi FIi), find_fas_init) \<in> \<langle>Rm, V\<rangle>g_impl_rel_ext \<rightarrow> \<langle>V \<times>\<^sub>r V\<rangle>fun_set_rel \<rightarrow> \<langle>\<langle>V \<times>\<^sub>r V\<rangle>fun_set_rel\<rangle>nres_rel
[PROOF STEP]
apply (intro fun_relI nres_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> \<langle>Rm, V\<rangle>g_impl_rel_ext; (aa, a'a) \<in> \<langle>V \<times>\<^sub>r V\<rangle>fun_set_rel\<rbrakk> \<Longrightarrow> RETURN (find_fas_init_code eq bhc sz a aa) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>fun_set_rel) (find_fas_init a' a'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
RR \<equiv> \<langle>V \<times>\<^sub>r V\<rangle>fun_set_rel
SIDE_GEN_ALGO (is_bounded_hashcode V eq bhc)
GEN_OP eq (=) (V \<rightarrow> V \<rightarrow> bool_rel)
SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('vi) sz)

goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> \<langle>Rm, V\<rangle>g_impl_rel_ext; (aa, a'a) \<in> \<langle>V \<times>\<^sub>r V\<rangle>fun_set_rel\<rbrakk> \<Longrightarrow> RETURN (find_fas_init_code eq bhc sz a aa) \<le> \<Down> (\<langle>V \<times>\<^sub>r V\<rangle>fun_set_rel) (find_fas_init a' a'a)
[PROOF STEP]
by (simp add: find_fas_init_code.refine)


[STATEMENT]
lemma squarefree_part_0 [simp]: "squarefree_part 0 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. squarefree_part 0 = {}
[PROOF STEP]
by (simp add: squarefree_part_def)


[STATEMENT]
lemma square_part_0 [simp]: "square_part 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_part 0 = 0
[PROOF STEP]
by (simp add: square_part_def)


[STATEMENT]
lemma squarefree_decompose: "\<Prod>(squarefree_part n) * square_part n ^ 2 = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
 2. n \<noteq> 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
 2. n \<noteq> 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
[PROOF STEP]
define A s where "A = squarefree_part n" and "s = square_part n"
[PROOF STATE]
proof (state)
this:
A = squarefree_part n
s = square_part n

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
 2. n \<noteq> 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
[PROOF STEP]
have "(\<Prod>A) = (\<Prod>p\<in>A. p ^ (multiplicity p n mod 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Prod>A = (\<Prod>p\<in>A. p ^ (multiplicity p n mod 2))
[PROOF STEP]
by (intro prod.cong) (auto simp: A_def squarefree_part_def elim!: oddE)
[PROOF STATE]
proof (state)
this:
\<Prod>A = (\<Prod>p\<in>A. p ^ (multiplicity p n mod 2))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
 2. n \<noteq> 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Prod>A = (\<Prod>p\<in>A. p ^ (multiplicity p n mod 2))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
 2. n \<noteq> 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
[PROOF STEP]
have "\<dots> = (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n mod 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>A. p ^ (multiplicity p n mod 2)) = (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n mod 2))
[PROOF STEP]
by (intro prod.mono_neutral_left) (auto simp: A_def  squarefree_part_def)
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>A. p ^ (multiplicity p n mod 2)) = (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n mod 2))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
 2. n \<noteq> 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>A. p ^ (multiplicity p n mod 2)) = (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n mod 2))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
 2. n \<noteq> 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
[PROOF STEP]
have "\<dots> * s^2 = n"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n mod 2)) * s\<^sup>2 = n
[PROOF STEP]
by (simp add: s_def square_part_def prod.distrib [symmetric] power_add [symmetric]
                  power_mult [symmetric] prime_factorization_nat [symmetric] algebra_simps
                  prod_power_distrib)
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n mod 2)) * s\<^sup>2 = n

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
 2. n \<noteq> 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Prod>A * s\<^sup>2 = n
[PROOF STEP]
show "\<Prod>A * s^2 = n"
[PROOF STATE]
proof (prove)
using this:
\<Prod>A * s\<^sup>2 = n

goal (1 subgoal):
 1. \<Prod>A * s\<^sup>2 = n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Prod>A * s\<^sup>2 = n

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
[PROOF STEP]
qed simp


[STATEMENT]
lemma squarefree_part_pos [simp]: "\<Prod>(squarefree_part n) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<Prod>(squarefree_part n)
[PROOF STEP]
using prime_gt_0_nat
[PROOF STATE]
proof (prove)
using this:
prime ?p \<Longrightarrow> 0 < ?p

goal (1 subgoal):
 1. 0 < \<Prod>(squarefree_part n)
[PROOF STEP]
unfolding squarefree_part_def
[PROOF STATE]
proof (prove)
using this:
prime ?p \<Longrightarrow> 0 < ?p

goal (1 subgoal):
 1. 0 < \<Prod>{p. p \<in># prime_factorization n \<and> odd (multiplicity p n)}
[PROOF STEP]
by auto


[STATEMENT]
lemma squarefree_part_ge_Suc_0 [simp]: "\<Prod>(squarefree_part n) \<ge> Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc 0 \<le> \<Prod>(squarefree_part n)
[PROOF STEP]
using squarefree_part_pos[of n]
[PROOF STATE]
proof (prove)
using this:
0 < \<Prod>(squarefree_part n)

goal (1 subgoal):
 1. Suc 0 \<le> \<Prod>(squarefree_part n)
[PROOF STEP]
by presburger


[STATEMENT]
lemma squarefree_part_subset [intro]: "squarefree_part n \<subseteq> prime_factors n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. squarefree_part n \<subseteq> prime_factors n
[PROOF STEP]
unfolding squarefree_part_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. p \<in># prime_factorization n \<and> odd (multiplicity p n)} \<subseteq> prime_factors n
[PROOF STEP]
by auto


[STATEMENT]
lemma squarefree_part_finite [simp]: "finite (squarefree_part n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (squarefree_part n)
[PROOF STEP]
by (rule finite_subset[OF squarefree_part_subset]) simp


[STATEMENT]
lemma squarefree_part_dvd [simp]: "\<Prod>(squarefree_part n) dvd n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Prod>(squarefree_part n) dvd n
[PROOF STEP]
by (subst (2) squarefree_decompose [of n, symmetric]) simp


[STATEMENT]
lemma squarefree_part_dvd' [simp]: "p \<in> squarefree_part n \<Longrightarrow> p dvd n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> squarefree_part n \<Longrightarrow> p dvd n
[PROOF STEP]
by (rule dvd_prodD[OF _ squarefree_part_dvd]) simp_all


[STATEMENT]
lemma square_part_dvd [simp]: "square_part n ^ 2 dvd n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (square_part n)\<^sup>2 dvd n
[PROOF STEP]
by (subst (2) squarefree_decompose [of n, symmetric]) simp


[STATEMENT]
lemma square_part_dvd' [simp]: "square_part n dvd n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_part n dvd n
[PROOF STEP]
by (subst (2) squarefree_decompose [of n, symmetric]) simp


[STATEMENT]
lemma squarefree_part_le: "p \<in> squarefree_part n \<Longrightarrow> p \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> squarefree_part n \<Longrightarrow> p \<le> n
[PROOF STEP]
by (cases "n = 0") (simp_all add: dvd_imp_le)


[STATEMENT]
lemma square_part_le: "square_part n \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_part n \<le> n
[PROOF STEP]
by (cases "n = 0") (simp_all add: dvd_imp_le)


[STATEMENT]
lemma square_part_le_sqrt: "square_part n \<le> nat \<lfloor>sqrt (real n)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_part n \<le> nat \<lfloor>sqrt (real n)\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. square_part n \<le> nat \<lfloor>sqrt (real n)\<rfloor>
[PROOF STEP]
have "1 * square_part n ^ 2 \<le> \<Prod>(squarefree_part n) * square_part n ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 * (square_part n)\<^sup>2 \<le> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2
[PROOF STEP]
by (intro mult_right_mono) simp_all
[PROOF STATE]
proof (state)
this:
1 * (square_part n)\<^sup>2 \<le> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2

goal (1 subgoal):
 1. square_part n \<le> nat \<lfloor>sqrt (real n)\<rfloor>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 * (square_part n)\<^sup>2 \<le> \<Prod>(squarefree_part n) * (square_part n)\<^sup>2

goal (1 subgoal):
 1. square_part n \<le> nat \<lfloor>sqrt (real n)\<rfloor>
[PROOF STEP]
have "\<dots> = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n
[PROOF STEP]
by (rule squarefree_decompose)
[PROOF STATE]
proof (state)
this:
\<Prod>(squarefree_part n) * (square_part n)\<^sup>2 = n

goal (1 subgoal):
 1. square_part n \<le> nat \<lfloor>sqrt (real n)\<rfloor>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 * (square_part n)\<^sup>2 \<le> n
[PROOF STEP]
have "real (square_part n ^ 2) \<le> real n"
[PROOF STATE]
proof (prove)
using this:
1 * (square_part n)\<^sup>2 \<le> n

goal (1 subgoal):
 1. real ((square_part n)\<^sup>2) \<le> real n
[PROOF STEP]
by (subst of_nat_le_iff) simp
[PROOF STATE]
proof (state)
this:
real ((square_part n)\<^sup>2) \<le> real n

goal (1 subgoal):
 1. square_part n \<le> nat \<lfloor>sqrt (real n)\<rfloor>
[PROOF STEP]
hence "sqrt (real (square_part n ^ 2)) \<le> sqrt (real n)"
[PROOF STATE]
proof (prove)
using this:
real ((square_part n)\<^sup>2) \<le> real n

goal (1 subgoal):
 1. sqrt (real ((square_part n)\<^sup>2)) \<le> sqrt (real n)
[PROOF STEP]
by (subst real_sqrt_le_iff) simp_all
[PROOF STATE]
proof (state)
this:
sqrt (real ((square_part n)\<^sup>2)) \<le> sqrt (real n)

goal (1 subgoal):
 1. square_part n \<le> nat \<lfloor>sqrt (real n)\<rfloor>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sqrt (real ((square_part n)\<^sup>2)) \<le> sqrt (real n)

goal (1 subgoal):
 1. square_part n \<le> nat \<lfloor>sqrt (real n)\<rfloor>
[PROOF STEP]
have "sqrt (real (square_part n ^ 2)) = real (square_part n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (real ((square_part n)\<^sup>2)) = real (square_part n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqrt (real ((square_part n)\<^sup>2)) = real (square_part n)

goal (1 subgoal):
 1. square_part n \<le> nat \<lfloor>sqrt (real n)\<rfloor>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (square_part n) \<le> sqrt (real n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real (square_part n) \<le> sqrt (real n)

goal (1 subgoal):
 1. square_part n \<le> nat \<lfloor>sqrt (real n)\<rfloor>
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
square_part n \<le> nat \<lfloor>sqrt (real n)\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma square_part_pos [simp]: "n > 0 \<Longrightarrow> square_part n > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> 0 < square_part n
[PROOF STEP]
unfolding square_part_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> 0 < (if n = 0 then 0 else \<Prod>p\<in>prime_factors n. p ^ (multiplicity p n div 2))
[PROOF STEP]
using prime_gt_0_nat
[PROOF STATE]
proof (prove)
using this:
prime ?p \<Longrightarrow> 0 < ?p

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> 0 < (if n = 0 then 0 else \<Prod>p\<in>prime_factors n. p ^ (multiplicity p n div 2))
[PROOF STEP]
by auto


[STATEMENT]
lemma square_part_ge_Suc_0 [simp]: "n > 0 \<Longrightarrow> square_part n \<ge> Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> Suc 0 \<le> square_part n
[PROOF STEP]
using square_part_pos[of n]
[PROOF STATE]
proof (prove)
using this:
0 < n \<Longrightarrow> 0 < square_part n

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> Suc 0 \<le> square_part n
[PROOF STEP]
by presburger


[STATEMENT]
lemma zero_not_in_squarefree_part [simp]: "0 \<notin> squarefree_part n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> squarefree_part n
[PROOF STEP]
unfolding squarefree_part_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> {p. p \<in># prime_factorization n \<and> odd (multiplicity p n)}
[PROOF STEP]
by auto


[STATEMENT]
lemma multiplicity_squarefree_part:
  "prime p \<Longrightarrow> multiplicity p (\<Prod>(squarefree_part n)) = (if p \<in> squarefree_part n then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p \<Longrightarrow> multiplicity p (\<Prod>(squarefree_part n)) = (if p \<in> squarefree_part n then 1 else 0)
[PROOF STEP]
using squarefree_part_subset[of n]
[PROOF STATE]
proof (prove)
using this:
squarefree_part n \<subseteq> prime_factors n

goal (1 subgoal):
 1. prime p \<Longrightarrow> multiplicity p (\<Prod>(squarefree_part n)) = (if p \<in> squarefree_part n then 1 else 0)
[PROOF STEP]
by (intro multiplicity_prod_prime_powers_nat') auto