Theory More_CC

theory More_CC imports
  Constructive_Cryptography.Constructive_Cryptography
begin

section ‹Material for Isabelle library›

lemma eq_alt_conversep: "(=) = (BNF_Def.Grp UNIV id)¯¯"
  by(simp add: Grp_def fun_eq_iff)

parametric_constant 
  swap_parametric [transfer_rule]: prod.swap_def 

lemma Sigma_parametric [transfer_rule]: includes lifting_syntax shows
  "(rel_set A ===> (A ===> rel_set B) ===> rel_set (rel_prod A B)) Sigma Sigma"
  unfolding Sigma_def by transfer_prover

lemma empty_eq_Plus [simp]: "{} = A <+> B ⟷ A = {} ∧ B = {}"
  by auto

lemma insert_Inl_Plus [simp]: "insert (Inl x) (A <+> B) = insert x A <+> B" by auto

lemma insert_Inr_Plus [simp]: "insert (Inr x) (A <+> B) = A <+> insert x B" by auto

lemma map_sum_image_Plus [simp]: "map_sum f g ` (A <+> B) = f ` A <+> g ` B"
  by(auto intro: rev_image_eqI)

lemma Plus_subset_Plus_iff [simp]: "A <+> B ⊆ C <+> D ⟷ A ⊆ C ∧ B ⊆ D"
  by auto

lemma map_sum_eq_Inl_iff: "map_sum f g x = Inl y ⟷ (∃x'. x = Inl x' ∧ y = f x')"
  by(cases x) auto

lemma map_sum_eq_Inr_iff: "map_sum f g x = Inr y ⟷ (∃x'. x = Inr x' ∧ y = g x')"
  by(cases x) auto

lemma surj_map_sum: "surj (map_sum f g)" if "surj f" "surj g"
  apply(safe; simp)
  subgoal for x using that 
    by(cases x)(auto 4 3 intro: image_eqI[where x="Inl _"] image_eqI[where x="Inr _"])
  done

lemma bij_map_sumI [simp]: "bij (map_sum f g)" if "bij f" "bij g"
  using that by(clarsimp simp add: bij_def sum.inj_map surj_map_sum)

lemma inv_map_sum [simp]:
  "⟦ bij f; bij g ⟧ ⟹ inv_into UNIV (map_sum f g) = map_sum (inv_into UNIV f) (inv_into UNIV g)"
  by(rule inj_imp_inv_eq)(simp_all add: sum.map_comp sum.inj_map bij_def surj_iff sum.map_id)


context conditionally_complete_lattice begin

lemma admissible_le1I:
  "ccpo.admissible lub ord (λx. f x ≤ y)"
  if "cont lub ord Sup (≤) f"
  by(rule ccpo.admissibleI)(auto simp add: that[THEN contD] intro!: cSUP_least)

lemma admissible_le1_mcont [cont_intro]:
  "ccpo.admissible lub ord (λx. f x ≤ y)" if "mcont lub ord Sup (≤) f"
  using that by(simp add: admissible_le1I mcont_def)

end

lemma eq_alt_conversep2: "(=) = ((BNF_Def.Grp UNIV id)¯¯)¯¯"
  by(auto simp add: Grp_def fun_eq_iff)

lemma nn_integral_indicator_singleton1 [simp]:
  assumes [measurable]: "{y} ∈ sets M"
  shows "(∫⇧+x. indicator {y} x * f x ∂M) = emeasure M {y} * f y"
  by(simp add: mult.commute)

lemma nn_integral_indicator_singleton1' [simp]:
  assumes "{y} ∈ sets M"
  shows "(∫⇧+x. indicator {x} y * f x ∂M) = emeasure M {y} * f y"
  by(subst nn_integral_indicator_singleton1[symmetric, OF assms])(rule nn_integral_cong; simp split: split_indicator)

subsection ‹Probabilities›

lemma pmf_eq_1_iff: "pmf p x = 1 ⟷ p = return_pmf x" (is "?lhs = ?rhs")
proof(rule iffI)
  assume ?lhs
  have "pmf p i = 0" if "x ≠ i" for i
  proof(rule antisym)
    have "pmf p i + 1 ≤ pmf p i + pmf p x" using ‹?lhs› by simp
    also have "… = measure (measure_pmf p) {i, x}" using that
      by(subst measure_pmf.finite_measure_eq_sum_singleton)(simp_all add: pmf.rep_eq)
    also have "… ≤ 1" by(rule measure_pmf.subprob_measure_le_1)
    finally show "pmf p i ≤ 0" by simp
  qed(rule pmf_nonneg)
  then show ?rhs if ?lhs
    by(intro pmf_eqI)(auto simp add: that split: split_indicator)
qed simp

lemma measure_spmf_cong: "measure (measure_spmf p) A = measure (measure_spmf p) B"
  if "A ∩ set_spmf p = B ∩ set_spmf p"
proof -
  have "measure (measure_spmf p) A = measure (measure_spmf p) (A ∩ set_spmf p) + measure (measure_spmf p) (A - set_spmf p)"
    by(subst measure_spmf.finite_measure_Union[symmetric])(auto intro: arg_cong2[where f=measure])
  also have "measure (measure_spmf p) (A - set_spmf p) = 0" by(simp add: measure_spmf_zero_iff)
  also have "0 = measure (measure_spmf p) (B - set_spmf p)" by(simp add: measure_spmf_zero_iff)
  also have "measure (measure_spmf p) (A ∩ set_spmf p) + … = measure (measure_spmf p) B"
    unfolding that by(subst measure_spmf.finite_measure_Union[symmetric])(auto intro: arg_cong2[where f=measure])
  finally show ?thesis .
qed

definition weight_spmf' where "weight_spmf' = weight_spmf"
lemma weight_spmf'_parametric [transfer_rule]: "rel_fun (rel_spmf A) (=) weight_spmf' weight_spmf'"
  unfolding weight_spmf'_def by(rule weight_spmf_parametric)

lemma bind_spmf_to_nat_on:
  "bind_spmf (map_spmf (to_nat_on (set_spmf p)) p) (λn. f (from_nat_into (set_spmf p) n)) = bind_spmf p f"
  by(simp add: bind_map_spmf cong: bind_spmf_cong)

lemma try_cond_spmf_fst:
  "try_spmf (cond_spmf_fst p x) q = (if x ∈ fst ` set_spmf p then cond_spmf_fst p x else q)"
  by (metis cond_spmf_fst_eq_return_None lossless_cond_spmf_fst try_spmf_lossless try_spmf_return_None)

lemma measure_try_spmf:
  "measure (measure_spmf (try_spmf p q)) A = measure (measure_spmf p) A + pmf p None * measure (measure_spmf q) A"
proof -
  have "emeasure (measure_spmf (try_spmf p q)) A = emeasure (measure_spmf p) A + pmf p None * emeasure (measure_spmf q) A"
    by(fold nn_integral_spmf)(simp add: spmf_try_spmf nn_integral_add ennreal_mult' nn_integral_cmult)
  then show ?thesis by(simp add: measure_spmf.emeasure_eq_measure ennreal_mult'[symmetric] ennreal_plus[symmetric] del: ennreal_plus)
qed

lemma rel_spmf_OO_trans_strong:
  "⟦ rel_spmf R p q; rel_spmf S q r ⟧ ⟹ rel_spmf (R OO eq_onp (λx. x ∈ set_spmf q) OO S) p r"
  by(auto intro: rel_spmf_OO_trans rel_spmf_reflI simp add: eq_onp_def)

lemma mcont2mcont_spmf [cont_intro]:
  "mcont lub ord Sup (≤) (λp. spmf (f p) x)"
  if "mcont lub ord lub_spmf (ord_spmf (=)) f"
  using that unfolding mcont_def
  apply safe
  subgoal by(rule monotone2monotone, rule monotone_spmf; simp)
  apply(rule contI)
  apply(subst contD[where f=f and luba=lub]; simp)
  apply(subst cont_spmf[THEN contD])
    apply(erule (2) chain_imageI[OF _ monotoneD])
   apply simp
  apply(simp add: image_image)
  done

lemma ord_spmf_try_spmf2: "ord_spmf R p (try_spmf p q)" if "rel_spmf R p p"
proof -
  have "ord_spmf R (bind_pmf p return_pmf) (try_spmf p q)" unfolding try_spmf_def
    by(rule rel_pmf_bindI[where R="rel_option R"])
       (use that in ‹auto simp add: rel_pmf_return_pmf1 elim!: option.rel_cases›)
  then show ?thesis by(simp add: bind_return_pmf')
qed

lemma ord_spmf_lossless_spmfD1:
  assumes "ord_spmf R p q"
    and "lossless_spmf p"
  shows "rel_spmf R p q"
  by (metis (no_types, lifting) assms lossless_iff_set_pmf_None option.simps(11) ord_option.cases pmf.rel_mono_strong)

lemma restrict_spmf_mono:
  "ord_spmf (=) p q ⟹ ord_spmf (=) (p ↿ A) (q ↿ A)"
  by(auto simp add: restrict_spmf_def pmf.rel_map elim!: pmf.rel_mono_strong elim: ord_option.cases)

lemma restrict_lub_spmf:
  assumes chain: "Complete_Partial_Order.chain (ord_spmf (=)) Y"
  shows "restrict_spmf (lub_spmf Y) A = lub_spmf ((λp. restrict_spmf p A) ` Y)" (is "?lhs = ?rhs")
proof(cases "Y = {}")
  case Y: False
  have chain': "Complete_Partial_Order.chain (ord_spmf (=)) ((λp. p ↿ A) ` Y)"
    using chain by(rule chain_imageI)(auto intro: restrict_spmf_mono)
  show ?thesis by(rule spmf_eqI)(simp add: spmf_lub_spmf[OF chain'] Y image_image spmf_restrict_spmf spmf_lub_spmf[OF chain])
qed simp

lemma mono2mono_restrict_spmf [THEN spmf.mono2mono]:
  shows monotone_restrict_spmf: "monotone (ord_spmf (=)) (ord_spmf (=)) (λp. p ↿ A)"
  by(rule monotoneI)(rule restrict_spmf_mono)

lemma mcont2mcont_restrict_spmf [THEN spmf.mcont2mcont, cont_intro]:
  shows  mcont_restrict_spmf: "mcont lub_spmf (ord_spmf (=)) lub_spmf (ord_spmf (=)) (λp. restrict_spmf p A)"
  using monotone_restrict_spmf by(rule mcontI)(simp add: contI restrict_lub_spmf)

lemma ord_spmf_case_option: "ord_spmf R (case x of None ⇒ a | Some y ⇒ b y) (case x of None ⇒ a' | Some y ⇒ b' y)"
  if "ord_spmf R a a'" "⋀y. ord_spmf R (b y) (b' y)" using that by(cases x) auto

lemma ord_spmf_map_spmfI: "ord_spmf (=) (map_spmf f p) (map_spmf f q)" if "ord_spmf (=) p q"
  using that by(auto simp add: pmf.rel_map elim!: pmf.rel_mono_strong ord_option.cases)

subsubsection ‹Conditional probabilities›

lemma mk_lossless_cond_spmf [simp]: "mk_lossless (cond_spmf p A) = cond_spmf p A"
  by(simp add: cond_spmf_alt)

context
  fixes p :: "'a pmf"
    and f :: "'a ⇒ 'b pmf"
    and A :: "'b set"
    and F :: "'a ⇒ real"
  defines "F ≡ λx. pmf p x * measure (measure_pmf (f x)) A / measure (measure_pmf (bind_pmf p f)) A"
begin

definition cond_bind_pmf :: "'a pmf" where "cond_bind_pmf = embed_pmf F"

lemma cond_bind_pmf_nonneg: "F x ≥ 0"
  by(simp add: F_def)

context assumes defined: "A ∩ (⋃x∈set_pmf p. set_pmf (f x)) ≠ {}" begin

private lemma nonzero: "measure (measure_pmf (bind_pmf p f)) A > 0"
  using defined by(auto 4 3 intro: measure_pmf_posI)

lemma cond_bind_pmf_prob: "(∫⇧+ x. F x ∂count_space UNIV) = 1"
proof -
  have nonzero': "(∫⇧+ x. ennreal (pmf p x) * ennreal (measure_pmf.prob (f x) A) ∂count_space UNIV) ≠ 0"
    using defined by(auto simp add: nn_integral_0_iff_AE AE_count_space pmf_eq_0_set_pmf measure_pmf_zero_iff)
  have finite: "(∫⇧+ x. ennreal (pmf p x) * ennreal (measure_pmf.prob (f x) A) ∂count_space UNIV) < ⊤" (is "?lhs < _")
  proof(rule order.strict_trans1)
    show "?lhs ≤ (∫⇧+ x. ennreal (pmf p x) * 1 ∂count_space UNIV)"
      by(rule nn_integral_mono)(simp add: mult_left_le)
    show "… < ⊤" by(simp add: nn_integral_pmf_eq_1)
  qed
  have "(∫⇧+ x. F x ∂count_space UNIV) = 
    (∑⇧+ x. ennreal (pmf p x * measure_pmf.prob (f x) A)) / emeasure (measure_pmf (bind_pmf p f)) A"
    using nonzero unfolding F_def measure_pmf.emeasure_eq_measure 
    by(simp add: divide_ennreal[symmetric] divide_ennreal_def nn_integral_multc)
  also have "… = 1" unfolding emeasure_bind_pmf 
    by(simp add: measure_pmf.emeasure_eq_measure nn_integral_measure_pmf ennreal_mult' nonzero' finite)
  finally show ?thesis .           
qed

lemma pmf_cond_bind_pmf: "pmf cond_bind_pmf x = F x"
  unfolding cond_bind_pmf_def by(rule pmf_embed_pmf[OF cond_bind_pmf_nonneg cond_bind_pmf_prob])

lemma set_cond_bind_pmf: "set_pmf cond_bind_pmf = {x∈set_pmf p. set_pmf (f x) ∩ A ≠ {}}"
  unfolding cond_bind_pmf_def 
  by(subst set_embed_pmf[OF cond_bind_pmf_nonneg cond_bind_pmf_prob])
    (auto simp add: F_def pmf_eq_0_set_pmf measure_pmf_zero_iff)

lemma cond_bind_pmf: "cond_pmf (bind_pmf p f) A = bind_pmf cond_bind_pmf (λx. cond_pmf (f x) A)"
  (is "?lhs = ?rhs")
proof(rule pmf_eqI)
  fix i
  have "ennreal (pmf ?lhs i) = ennreal (pmf ?rhs i)"
  proof(cases "i ∈ A")
    case True
    have "ennreal (pmf ?lhs i) = (∫⇧+ x. ennreal (pmf p x) * ennreal (pmf (f x) i) / ennreal (measure_pmf.prob (p ⤜ f) A) ∂count_space UNIV)"
      using True defined
      by(simp add: pmf_cond bind_UNION Int_commute divide_ennreal[symmetric] nonzero ennreal_pmf_bind)
        (simp add: divide_ennreal_def nn_integral_multc[symmetric] nn_integral_measure_pmf)
    also have "… =  (∫⇧+ x. ennreal (F x) * ennreal (pmf (cond_pmf (f x) A) i) ∂count_space UNIV)"
      using True nonzero
      apply(intro nn_integral_cong)
      subgoal for x
        by(clarsimp simp add: F_def ennreal_mult'[symmetric] divide_ennreal)
          (cases "measure_pmf.prob (f x) A = 0"; auto simp add: pmf_cond pmf_eq_0_set_pmf measure_pmf_zero_iff)
      done
    also have "… = ennreal (pmf ?rhs i)"
      by(simp add: ennreal_pmf_bind nn_integral_measure_pmf pmf_cond_bind_pmf)
    finally show ?thesis .
  next
    case False
    then show ?thesis using defined
      by(simp add: pmf_cond bind_UNION Int_commute pmf_eq_0_set_pmf set_cond_bind_pmf)
  qed 
  then show "pmf ?lhs i = pmf ?rhs i" by simp
qed

end

end


lemma cond_spmf_try1:
  "cond_spmf (try_spmf p q) A = cond_spmf p A" if "set_spmf q ∩ A = {}"
  apply(rule spmf_eqI)
  using that
  apply(auto simp add: spmf_try_spmf measure_try_spmf measure_spmf_zero_iff)
  apply(subst (2) spmf_eq_0_set_spmf[THEN iffD2])
   apply blast
  apply simp
  apply(simp add: measure_try_spmf measure_spmf_zero_iff)
  done

lemma cond_spmf_cong: "cond_spmf p A = cond_spmf p B" if "A ∩ set_spmf p = B ∩ set_spmf p"
  apply(rule spmf_eqI)
  using that by(auto simp add: measure_spmf_zero_iff spmf_eq_0_set_spmf measure_spmf_cong[OF that])

lemma cond_spmf_pair_spmf:
  "cond_spmf (pair_spmf p q) (A × B) = pair_spmf (cond_spmf p A) (cond_spmf q B)" (is "?lhs = ?rhs")
proof(rule spmf_eqI)
  show "spmf ?lhs i = spmf ?rhs i" for i
  proof(cases i)
    case i [simp]: (Pair a b)
    then show ?thesis by(simp add: measure_pair_spmf_times)
  qed
qed

lemma cond_spmf_pair_spmf1:
  "cond_spmf_fst (map_spmf (λ((x, s'), y). (f x, s', y)) (pair_spmf p q)) x =
   pair_spmf (cond_spmf_fst (map_spmf (λ(x, s'). (f x, s')) p) x) q" (is "?lhs = ?rhs")
  if "lossless_spmf q"
proof -
  have "?lhs = map_spmf (λ((_, s'), y). (s', y)) (cond_spmf (pair_spmf p q) ((λ((x, s'), y). (f x, s', y)) -` ({x} × UNIV)))" 
    by(simp add: cond_spmf_fst_def spmf.map_comp o_def split_def)
  also have "((λ((x, s'), y). (f x, s', y)) -` ({x} × UNIV)) = ((λ(x, y). (f x, y)) -` ({x} × UNIV)) × UNIV"
    by(auto)
  also have "map_spmf (λ((_, s'), y). (s', y)) (cond_spmf (pair_spmf p q) …) = ?rhs"
    by(simp add: cond_spmf_fst_def cond_spmf_pair_spmf that spmf.map_comp pair_map_spmf1 apfst_def map_prod_def split_def)
  finally show ?thesis .
qed

lemma try_cond_spmf: "try_spmf (cond_spmf p A) q = (if set_spmf p ∩ A ≠ {} then cond_spmf p A else q)"
  apply(clarsimp simp add: cond_spmf_def lossless_iff_set_pmf_None intro!: try_spmf_lossless)
  apply(subst (asm) set_cond_pmf)
   apply(auto simp add: in_set_spmf)
  done

lemma cond_spmf_try2:
  "cond_spmf (try_spmf p q) A = (if lossless_spmf p then return_pmf None else cond_spmf q A)" if "set_spmf p ∩ A = {}"
  apply(rule spmf_eqI)
  using that
  apply(auto simp add: spmf_try_spmf measure_try_spmf measure_spmf_zero_iff lossless_iff_pmf_None)
  apply(subst spmf_eq_0_set_spmf[THEN iffD2])
   apply blast
  apply(simp add: measure_spmf_zero_iff[THEN iffD2])
  done


definition cond_bind_spmf :: "'a spmf ⇒ ('a ⇒ 'b spmf) ⇒ 'b set ⇒ 'a spmf" where 
  "cond_bind_spmf p f A = 
   (if ∃x∈set_spmf p. set_spmf (f x) ∩ A ≠ {} then 
     cond_bind_pmf p (λx. case x of None ⇒ return_pmf None | Some x ⇒ f x) (Some ` A)
    else return_pmf None)"

context begin

private lemma defined: "⟦ y ∈ set_spmf (f x); y ∈ A; x ∈ set_spmf p ⟧ 
  ⟹ Some ` A ∩ (⋃x∈set_pmf p. set_pmf (case x of None ⇒ return_pmf None | Some x ⇒ f x)) ≠ {}"
  by(fastforce simp add: in_set_spmf bind_spmf_def)

lemma spmf_cond_bind_spmf [simp]:
  "spmf (cond_bind_spmf p f A) x = spmf p x * measure (measure_spmf (f x)) A / measure (measure_spmf (bind_spmf p f)) A"
  by(clarsimp simp add: cond_bind_spmf_def measure_spmf_zero_iff bind_UNION pmf_cond_bind_pmf defined split!: if_split)
     (fastforce simp add: in_set_spmf bind_spmf_def measure_measure_spmf_conv_measure_pmf)+

lemma set_cond_bind_spmf [simp]:
  "set_spmf (cond_bind_spmf p f A) = {x∈set_spmf p. set_spmf (f x) ∩ A ≠ {}}"
  by(clarsimp simp add: cond_bind_spmf_def set_spmf_def bind_UNION)
    (subst set_cond_bind_pmf; fastforce simp add: measure_measure_spmf_conv_measure_pmf)

lemma cond_bind_spmf: "cond_spmf (bind_spmf p f) A = bind_spmf (cond_bind_spmf p f A) (λx. cond_spmf (f x) A)"
  by(auto simp add: cond_spmf_def bind_UNION cond_bind_spmf_def split!: if_splits)
    (fastforce split: option.splits simp add: cond_bind_pmf set_cond_bind_pmf defined in_set_spmf bind_spmf_def intro!: bind_pmf_cong[OF refl])

end

lemma cond_spmf_fst_parametric [transfer_rule]: includes lifting_syntax shows
  "(rel_spmf (rel_prod (=) B) ===> (=) ===> rel_spmf B) cond_spmf_fst cond_spmf_fst"
  apply(rule rel_funI)+
  apply(clarsimp simp add: cond_spmf_fst_def spmf_rel_map elim!: rel_spmfE)
  subgoal for x pq
    by(subst (1 2) cond_spmf_cong[where B="fst -` ({x} × UNIV) ∩ snd -` ({x} × UNIV)"])
      (fastforce intro: rel_spmf_reflI)+
  done

lemma cond_spmf_fst_map_prod:
  "cond_spmf_fst (map_spmf (λ(x, y). (f x, g x y)) p) (f x) = map_spmf (g x) (cond_spmf_fst p x)"
  if "inj_on f (insert x (fst ` set_spmf p))"
proof -
  have "cond_spmf p ((λ(x, y). (f x, g x y)) -` ({f x} × UNIV)) = cond_spmf p (((λ(x, y). (f x, g x y)) -` ({f x} × UNIV)) ∩ set_spmf p)"
    by(rule cond_spmf_cong) simp
  also have "((λ(x, y). (f x, g x y)) -` ({f x} × UNIV)) ∩ set_spmf p = ({x} × UNIV) ∩ set_spmf p"
    using that by(auto 4 3 dest: inj_onD intro: rev_image_eqI)
  also have "cond_spmf p … = cond_spmf p ({x} × UNIV)"
    by(rule cond_spmf_cong) simp
  finally show ?thesis
    by(auto simp add: cond_spmf_fst_def spmf.map_comp o_def split_def intro: map_spmf_cong)
qed

lemma cond_spmf_fst_map_prod_inj:
  "cond_spmf_fst (map_spmf (λ(x, y). (f x, g x y)) p) (f x) =  map_spmf (g x) (cond_spmf_fst p x)"
  if "inj f"
  apply(rule cond_spmf_fst_map_prod)
  using that by(simp add: inj_on_def)

definition cond_bind_spmf_fst :: "'a spmf ⇒ ('a ⇒ 'b spmf) ⇒ 'b ⇒ 'a spmf" where
  "cond_bind_spmf_fst p f x = cond_bind_spmf p (map_spmf (λb. (b, ())) ∘ f) ({x} × UNIV)"

lemma cond_bind_spmf_fst_map_spmf_fst:
  "cond_bind_spmf_fst p (map_spmf fst ∘ f) x = cond_bind_spmf p f ({x} × UNIV)" (is "?lhs = ?rhs")
proof -
  have [simp]: "(λx. (fst x, ())) -` ({x} × UNIV) = {x} × UNIV" by auto
  have "?lhs = cond_bind_spmf p (λx. map_spmf (λx. (fst x, ())) (f x)) ({x} × UNIV)"
    by(simp add: cond_bind_spmf_fst_def spmf.map_comp o_def)
  also have "… = ?rhs" by(rule spmf_eqI)(simp add: measure_map_spmf map_bind_spmf[unfolded o_def, symmetric])
  finally show ?thesis .
qed

lemma cond_spmf_fst_bind: "cond_spmf_fst (bind_spmf p f) x = 
  bind_spmf (cond_bind_spmf_fst p (map_spmf fst ∘ f) x) (λy. cond_spmf_fst (f y) x)"
  by(simp add: cond_spmf_fst_def cond_bind_spmf map_bind_spmf cond_bind_spmf_fst_map_spmf_fst)(simp add: o_def)

lemma spmf_cond_bind_spmf_fst [simp]:
  "spmf (cond_bind_spmf_fst p f x) i = spmf p i * spmf (f i) x / spmf (bind_spmf p f) x"
  by(simp add: cond_bind_spmf_fst_def)
    (auto simp add: spmf_conv_measure_spmf measure_map_spmf map_bind_spmf[symmetric] intro!: arg_cong2[where f="(/)"] arg_cong2[where f="(*)"] arg_cong2[where f="measure"])

lemma set_cond_bind_spmf_fst [simp]:
  "set_spmf (cond_bind_spmf_fst p f x) = {y ∈ set_spmf p. x ∈ set_spmf (f y)}"
  by(auto simp add: cond_bind_spmf_fst_def intro: rev_image_eqI)

lemma map_cond_spmf_fst: "map_spmf f (cond_spmf_fst p x) = cond_spmf_fst (map_spmf (apsnd f) p) x"
  by(auto simp add: cond_spmf_fst_def spmf.map_comp intro!: map_spmf_cong arg_cong2[where f="cond_spmf"])

lemma cond_spmf_fst_try1:
  "cond_spmf_fst (try_spmf p q) x = cond_spmf_fst p x" if "x ∉ fst ` set_spmf q"
  using that
  apply(simp add: cond_spmf_fst_def)
  apply(subst cond_spmf_try1)
   apply(auto intro: rev_image_eqI)
  done

lemma cond_spmf_fst_try2:
  "cond_spmf_fst (try_spmf p q) x = (if lossless_spmf p then return_pmf None else cond_spmf_fst q x)" if "x ∉ fst ` set_spmf p"
  using that
  apply(simp add: cond_spmf_fst_def split!: if_split)
  apply (metis cond_spmf_fst_def cond_spmf_fst_eq_return_None)
  by (metis cond_spmf_fst_def cond_spmf_try2 lossless_cond_spmf lossless_cond_spmf_fst lossless_map_spmf)

lemma cond_spmf_fst_map_inj:
  "cond_spmf_fst (map_spmf (apfst f) p) (f x) = cond_spmf_fst p x" if "inj f"
  by(auto simp add: cond_spmf_fst_def spmf.map_comp intro!: map_spmf_cong arg_cong2[where f=cond_spmf] dest: injD[OF that])

lemma cond_spmf_fst_pair_spmf1:
  "cond_spmf_fst (map_spmf (λ(x, y). (f x, g x y)) (pair_spmf p q)) a =
   bind_spmf (cond_spmf_fst (map_spmf (λx. (f x, x)) p) a) (λx. map_spmf (g x) (mk_lossless q))" (is "?lhs = ?rhs")
proof -
  have "(λ(x, y). (f x, g x y)) -` ({a} × UNIV) = f -` {a} × UNIV" by(auto)
  moreover have "(λx. (f x, x)) -` ({a} × UNIV) = f -` {a}" by auto
  ultimately show ?thesis 
    by(simp add: cond_spmf_fst_def spmf.map_comp o_def split_beta cond_spmf_pair_spmf)
      (simp add: pair_spmf_alt_def map_bind_spmf o_def map_spmf_conv_bind_spmf)
qed

lemma cond_spmf_fst_return_spmf':
  "cond_spmf_fst (return_spmf (x, y)) z = (if x = z then return_spmf y else return_pmf None)"
  by(simp add: cond_spmf_fst_def)






section ‹Material for CryptHOL›

lemma left_gpv_lift_spmf [simp]: "left_gpv (lift_spmf p) = lift_spmf p"
  by(rule gpv.expand)(simp add: spmf.map_comp o_def)

lemma right_gpv_lift_spmf [simp]: "right_gpv (lift_spmf p) = lift_spmf p"
  by(rule gpv.expand)(simp add: spmf.map_comp o_def)

lemma map'_lift_spmf: "map_gpv' f g h (lift_spmf p) = lift_spmf (map_spmf f p)"
  by(rule gpv.expand)(simp add: gpv.map_sel spmf.map_comp o_def)

lemma in_set_sample_uniform [simp]: "x ∈ set_spmf (sample_uniform n) ⟷ x < n"
  by(simp add: sample_uniform_def)

lemma (in cyclic_group) inj_on_generator_iff [simp]: "⟦ x < order G; y < order G ⟧ ⟹ ❙g [^] x = ❙g [^] y ⟷ x = y"
  using inj_on_generator by(auto simp add: inj_on_def)

lemma map_ℐ_bot [simp]: "map_ℐ f g ⊥ = ⊥"
  unfolding bot_ℐ_def map_ℐ_ℐ_uniform by simp

lemma map_ℐ_Inr_plus [simp]: "map_ℐ Inr f (ℐ1 ⊕⇩ℐ ℐ2) = map_ℐ id (f ∘ Inr) ℐ2"
  by(rule ℐ_eqI) auto

lemma interaction_bound_map_gpv'_le:
  defines "ib ≡ interaction_bound" 
  shows "interaction_bound consider (map_gpv' f g h gpv) ≤ ib (consider ∘ g) gpv"
proof(induction arbitrary: gpv rule: interaction_bound_fixp_induct)
  case adm show ?case by simp
  case bottom show ?case by simp
  case (step interaction_bound')
  show ?case unfolding ib_def
    by(subst interaction_bound.simps)
      (auto simp add: image_comp ib_def split: generat.split intro!: SUP_mono rev_bexI step.IH[unfolded ib_def])
qed

lemma interaction_bounded_by_map_gpv' [interaction_bound]:
  assumes "interaction_bounded_by (consider ∘ g) gpv n"
  shows "interaction_bounded_by consider (map_gpv' f g h gpv) n"
  using assms interaction_bound_map_gpv'_le[of "consider" f g h gpv] by(simp add: interaction_bounded_by.simps)

lemma map_gpv'_bind_gpv:
  "map_gpv' f g h (bind_gpv gpv F) = bind_gpv (map_gpv' id g h gpv) (λx. map_gpv' f g h (F x))"
  by(coinduction arbitrary: gpv rule: gpv.coinduct_strong)
    (auto simp del: bind_gpv_sel' simp add: bind_gpv.sel spmf_rel_map bind_map_spmf generat.rel_map rel_fun_def intro!: rel_spmf_bind_reflI rel_spmf_reflI generat.rel_refl_strong split!: generat.split)

lemma exec_gpv_map_gpv':
  "exec_gpv callee (map_gpv' f g h gpv) s =
   map_spmf (map_prod f id) (exec_gpv (map_fun id (map_fun g (map_spmf (map_prod h id))) callee) gpv s)"
  using exec_gpv_parametric'[
    where S="(=)" and CALL="BNF_Def.Grp UNIV g" and R="conversep (BNF_Def.Grp UNIV h)" and A="BNF_Def.Grp UNIV f",
     unfolded rel_gpv''_Grp, simplified]
  apply(subst (asm) (2) conversep_eq[symmetric])
  apply(subst (asm) prod.rel_conversep)
  apply(subst (asm) (2 4) eq_alt)
  apply(subst (asm) prod.rel_Grp)
  apply simp
  apply(subst (asm) spmf_rel_conversep)
  apply(subst (asm) option.rel_Grp)
  apply(subst (asm) pmf.rel_Grp)
  apply simp
  apply(subst (asm) prod.rel_Grp)
  apply simp
  apply(subst (asm) (1 3) conversep_conversep[symmetric])
  apply(subst (asm) rel_fun_conversep)
  apply(subst (asm) rel_fun_Grp)
  apply(subst (asm) rel_fun_conversep)
  apply simp
  apply(simp add: option.rel_Grp pmf.rel_Grp fun.rel_Grp)
  apply(simp add: rel_fun_def BNF_Def.Grp_def o_def map_fun_def)
  apply(erule allE)+
  apply(drule fun_cong)
  apply(erule trans)
  apply simp                   
  done

lemma colossless_gpv_sub_gpvs:
  assumes "colossless_gpv ℐ gpv" "gpv' ∈ sub_gpvs ℐ gpv"
  shows "colossless_gpv ℐ gpv'"
using assms(2,1) by(induction)(auto dest: colossless_gpvD)

lemma pfinite_gpv_sub_gpvs:
  assumes "pfinite_gpv ℐ gpv" "gpv' ∈ sub_gpvs ℐ gpv" "ℐ ⊢g gpv √"
  shows "pfinite_gpv ℐ gpv'"
  using assms(2,1,3) by(induction)(auto dest: pfinite_gpv_ContD WT_gpvD)

lemma pfinite_gpv_id_oracle [simp]: "pfinite_gpv ℐ (id_oracle s x)" if "x ∈ outs_ℐ ℐ"
  by(simp add: id_oracle_def pgen_lossless_gpv_PauseI[OF that])

subsection ‹@{term try_gpv}›

lemma plossless_gpv_try_gpvI:
  assumes "pfinite_gpv ℐ gpv"
    and "¬ colossless_gpv ℐ gpv ⟹ plossless_gpv ℐ gpv'"
  shows "plossless_gpv ℐ (TRY gpv ELSE gpv')"
  using assms unfolding pgen_lossless_gpv_def
  by(cases "colossless_gpv ℐ gpv")(simp cong: expectation_gpv_cong_fail, simp)

lemma WT_gpv_try_gpvI [WT_intro]:
  assumes "ℐ ⊢g gpv √"
    and "¬ colossless_gpv ℐ gpv ⟹ ℐ ⊢g gpv' √"
  shows "ℐ ⊢g try_gpv gpv gpv' √"
  using assms by(coinduction arbitrary: gpv)(auto 4 4 dest: WT_gpvD colossless_gpvD split: if_split_asm)

lemma (in callee_invariant_on) exec_gpv_try_gpv:
  fixes exec_gpv1
  defines "exec_gpv1 ≡ exec_gpv"
  assumes WT: "ℐ ⊢g gpv √"
    and pfinite: "pfinite_gpv ℐ gpv"
    and I: "I s"
    and f: "⋀s. I s ⟹ f (x, s) = z"
    and lossless: "⋀s x. ⟦x ∈ outs_ℐ ℐ; I s⟧ ⟹ lossless_spmf (callee s x)"
  shows "map_spmf f (exec_gpv callee (try_gpv gpv (Done x)) s) =
    try_spmf (map_spmf f (exec_gpv1 callee gpv s)) (return_spmf z)"
  (is "?lhs = ?rhs")
proof -
  note [[show_variants]]
  have le: "ord_spmf (=) ?lhs ?rhs" using WT I
  proof(induction arbitrary: gpv s rule: exec_gpv_fixp_induct)
    case adm show ?case by simp
    case bottom show ?case by simp
    case (step exec_gpv')
    show ?case using step.prems unfolding exec_gpv1_def
      apply(subst exec_gpv.simps)
      apply(simp add: map_spmf_bind_spmf)
      apply(subst (1 2) try_spmf_def)
      apply(simp add: map_bind_pmf bind_spmf_pmf_assoc o_def)
      apply(simp add: bind_spmf_def bind_map_pmf bind_assoc_pmf)
      apply(rule rel_pmf_bindI[where R="eq_onp (λx. x ∈ set_pmf (the_gpv gpv))"])
       apply(rule pmf.rel_refl_strong)
       apply(simp add: eq_onp_def)
      apply(clarsimp split!: option.split generat.split simp add: bind_return_pmf f map_spmf_bind_spmf o_def eq_onp_def)
      apply(simp add: bind_spmf_def bind_assoc_pmf)
      subgoal for out c
        apply(rule rel_pmf_bindI[where R="eq_onp (λx. x ∈ set_pmf (callee s out))"])
         apply(rule pmf.rel_refl_strong)
         apply(simp add: eq_onp_def)
        apply(clarsimp split!: option.split simp add: eq_onp_def)
        apply(simp add: in_set_spmf[symmetric])
        apply(rule spmf.leq_trans)
         apply(rule step.IH)
          apply(frule (1) WT_gpvD)
          apply(erule (1) WT_gpvD)
          apply(drule WT_callee)
          apply(erule (2) WT_calleeD)
          apply(frule (1) WT_gpvD)
         apply(erule (2) callee_invariant)
        apply(simp add: try_spmf_def exec_gpv1_def)
        done
      done
  qed

  have "lossless_spmf ?lhs" 
    apply simp
    apply(rule plossless_exec_gpv)
       apply(rule plossless_gpv_try_gpvI)
        apply(rule pfinite)
       apply simp
      apply(rule WT_gpv_try_gpvI)
       apply(simp add: WT)
      apply simp
     apply(simp add: lossless)
    apply(simp add: I)
    done
  from ord_spmf_lossless_spmfD1[OF le this] show ?thesis by(simp add: spmf_rel_eq)
qed

lemma try_gpv_bind_gen_lossless': ― ‹generalises @{thm try_gpv_bind_gen_lossless}›
  assumes lossless: "gen_lossless_gpv b ℐ gpv"
    and WT1: "ℐ ⊢g gpv √"
    and WT2: "ℐ ⊢g gpv' √"
    and WTf: "⋀x. x ∈ results_gpv ℐ gpv ⟹ ℐ ⊢g f x √"
  shows "eq_ℐ_gpv (=) ℐ (TRY bind_gpv gpv f ELSE gpv') (bind_gpv gpv (λx. TRY f x ELSE gpv'))"
  using lossless WT1 WTf
proof(coinduction arbitrary: gpv)
  case (eq_ℐ_gpv gpv)
  note [simp] = spmf_rel_map generat.rel_map map_spmf_bind_spmf
    and [intro!] = rel_spmf_reflI rel_generat_reflI rel_funI
  show ?case using gen_lossless_gpvD[OF eq_ℐ_gpv(1)] WT_gpvD[OF eq_ℐ_gpv(2)] WT_gpvD[OF WT2] WT_gpvD[OF eq_ℐ_gpv(3)[rule_format, OF results_gpv.Pure]] WT2
    apply(auto simp del: bind_gpv_sel' simp add: bind_gpv.sel try_spmf_bind_spmf_lossless generat.map_comp o_def intro!: rel_spmf_bind_reflI rel_spmf_try_spmf split!: generat.split)
    apply(auto 4 4 intro!: eq_ℐ_gpv(3)[rule_format] eq_ℐ_gpv_reflI eq_ℐ_generat_reflI intro: results_gpv.IO WT_intro)
    done
qed

― ‹We instantiate the parameter @{term b} such that it can be used as a conditional simp rule.›
lemmas try_gpv_bind_lossless' = try_gpv_bind_gen_lossless'[where b=False]
  and try_gpv_bind_colossless' = try_gpv_bind_gen_lossless'[where b=True]

lemma try_gpv_bind_gpv:
   "try_gpv (bind_gpv gpv f) gpv' =
    bind_gpv (try_gpv (map_gpv Some id gpv) (Done None)) (λx. case x of None ⇒ gpv' | Some x' ⇒ try_gpv (f x') gpv')"
  by(coinduction arbitrary: gpv rule: gpv.coinduct_strong)
    (auto simp add: rel_fun_def generat.rel_map bind_return_pmf spmf_rel_map map_bind_spmf o_def bind_gpv.sel bind_map_spmf try_spmf_def bind_spmf_def spmf.map_comp bind_map_pmf bind_assoc_pmf gpv.map_sel simp del: bind_gpv_sel' intro!: rel_pmf_bind_reflI generat.rel_refl_strong rel_spmf_reflI split!: option.split generat.split)

lemma bind_gpv_try_gpv_map_Some:
  "bind_gpv (try_gpv (map_gpv Some id gpv) (Done None)) (λx. case x of None ⇒ Fail | Some y ⇒ f y) =
   bind_gpv gpv f"
  by(coinduction arbitrary: gpv rule: gpv.coinduct_strong)
    (auto simp add: bind_gpv.sel map_bind_spmf bind_map_spmf try_spmf_def bind_spmf_def spmf_rel_map bind_map_pmf gpv.map_sel bind_assoc_pmf bind_return_pmf generat.rel_map rel_fun_def simp del: bind_gpv_sel' intro!: rel_pmf_bind_reflI rel_spmf_reflI generat.rel_refl_strong split!: option.split generat.split)

lemma try_gpv_left_gpv:
  assumes "ℐ ⊢g gpv √" and WT2: "ℐ ⊢g gpv' √"
  shows "eq_ℐ_gpv (=) (ℐ ⊕⇩ℐ ℐ') (try_gpv (left_gpv gpv) (left_gpv gpv')) (left_gpv (try_gpv gpv gpv'))"
  using assms(1)
  apply(coinduction arbitrary: gpv)
  apply(auto simp add: map_try_spmf spmf.map_comp o_def generat.map_comp spmf_rel_map intro!: rel_spmf_try_spmf rel_spmf_reflI)
  subgoal for gpv generat by(cases generat)(auto dest: WT_gpvD)
  subgoal for gpv generat using WT2
    by(cases generat)(auto 4 4 dest: WT_gpvD intro!: eq_ℐ_gpv_reflI WT_gpv_left_gpv)
  done

lemma try_gpv_right_gpv:
  assumes "ℐ' ⊢g gpv √" and WT2: "ℐ' ⊢g gpv' √"
  shows "eq_ℐ_gpv (=) (ℐ ⊕⇩ℐ ℐ') (try_gpv (right_gpv gpv) (right_gpv gpv')) (right_gpv (try_gpv gpv gpv'))"
  using assms(1)
  apply(coinduction arbitrary: gpv)
  apply(auto simp add: map_try_spmf spmf.map_comp o_def generat.map_comp spmf_rel_map intro!: rel_spmf_try_spmf rel_spmf_reflI)
  subgoal for gpv generat by(cases generat)(auto dest: WT_gpvD)
  subgoal for gpv generat using WT2
    by(cases generat)(auto 4 4 dest: WT_gpvD intro!: eq_ℐ_gpv_reflI WT_gpv_right_gpv)
  done

lemma bind_try_Done_Fail: "bind_gpv (TRY gpv ELSE Done x) f = bind_gpv gpv f" if "f x = Fail"
  apply(coinduction arbitrary: gpv rule: gpv.coinduct_strong)
  apply(auto simp del: bind_gpv_sel' simp add: bind_gpv.sel map_bind_spmf bind_map_spmf try_spmf_def bind_spmf_def map_bind_pmf bind_assoc_pmf bind_map_pmf bind_return_pmf spmf.map_comp o_def that rel_fun_def intro!: rel_pmf_bind_reflI rel_spmf_reflI generat.rel_refl_strong split!: option.split generat.split)
  done


lemma inline_map_gpv':
  "inline callee (map_gpv' f g h gpv) s = 
   map_gpv (apfst f) id (inline (map_fun id (map_fun g (map_gpv (apfst h) id)) callee) gpv s)"
  using inline_parametric'[where S="(=)" and C="BNF_Def.Grp UNIV g" and R="conversep (BNF_Def.Grp UNIV h)" and A="BNF_Def.Grp UNIV f" and C'="(=)" and R'="(=)"]
  apply(subst (asm) (2 3 8) eq_alt_conversep)
  apply(subst (asm) (1 3 4 5) eq_alt)
  apply(subst (asm) (1) eq_alt_conversep2)
  apply(unfold prod.rel_conversep rel_gpv''_conversep prod.rel_Grp rel_gpv''_Grp)
  apply(force simp add: rel_fun_def Grp_def map_gpv_conv_map_gpv' map_fun_def[abs_def] o_def apfst_def)
  done

lemma interaction_bound_try_gpv:
  fixes "consider" defines "ib ≡ interaction_bound consider"
  shows "interaction_bound consider (try_gpv gpv gpv') ≤ ib gpv + ib gpv'"
proof(induction arbitrary: gpv gpv' rule: interaction_bound_fixp_induct)
  case adm show ?case by simp
  case bottom show ?case by simp
  case (step interaction_bound')
  show ?case unfolding ib_def
    apply(clarsimp simp add: generat.map_comp image_image o_def case_map_generat cong del: generat.case_cong split!: if_split generat.split intro!: SUP_least)
    subgoal
      apply(subst interaction_bound.simps)
      apply simp
      apply(subst Sup_image_eadd1[symmetric])
       apply clarsimp
      apply(rule SUP_upper2)
       apply(rule rev_image_eqI)
        apply simp
       apply simp
      apply(simp add: iadd_Suc)
      apply(subst Sup_image_eadd1[symmetric])
       apply simp
      apply(rule SUP_mono)
      apply simp
      apply(rule exI)
      apply(rule step.IH[unfolded ib_def])
      done
    subgoal
      apply(subst interaction_bound.simps)
      apply simp
      apply(subst Sup_image_eadd1[symmetric])
       apply clarsimp
      apply(rule SUP_upper2)
       apply(rule rev_image_eqI)
        apply simp
       apply simp
      apply(subst Sup_image_eadd1[symmetric])
       apply simp
      apply(rule SUP_upper2)
       apply(rule rev_image_eqI)
        apply simp
       apply simp
      apply(rule step.IH[unfolded ib_def])
      done
    subgoal
      apply(subst interaction_bound.simps)
      apply simp
      apply(subst Sup_image_eadd1[symmetric])
       apply clarsimp
      apply(rule SUP_upper2)
       apply(rule rev_image_eqI)
        apply simp
       apply simp
      apply(simp add: iadd_Suc)
      apply(subst Sup_image_eadd1[symmetric])
       apply simp
      apply(rule SUP_mono)
      apply simp
      apply(rule exI)
      apply(rule step.IH[unfolded ib_def])
      done
    subgoal
      apply(subst interaction_bound.simps)
      apply simp
      apply(subst Sup_image_eadd1[symmetric])
       apply clarsimp
      apply(rule SUP_upper2)
       apply(rule rev_image_eqI)
        apply simp
       apply simp
      apply(subst Sup_image_eadd1[symmetric])
       apply simp
      apply(rule SUP_upper2)
       apply(rule rev_image_eqI)
        apply simp
       apply simp
      apply(rule step.IH[unfolded ib_def])
      done
    subgoal
      apply(subst (2) interaction_bound.simps)
      apply simp
      apply(subst Sup_image_eadd2[symmetric])
       apply clarsimp
      apply simp
      apply(rule SUP_upper2)
       apply(rule rev_image_eqI)
        apply simp
       apply simp
      apply(simp add: iadd_Suc_right)
      apply(subst Sup_image_eadd2[symmetric])
       apply clarsimp
      apply(rule SUP_mono)
      apply clarsimp
      apply(rule exI)
      apply(rule order_trans)
       apply(rule step.hyps)
      apply(rule enat_le_plus_same)
      done
    subgoal
      apply(subst (2) interaction_bound.simps)
      apply simp
      apply(subst Sup_image_eadd2[symmetric])
       apply clarsimp
      apply simp
      apply(rule SUP_upper2)
       apply(rule rev_image_eqI)
        apply simp
       apply simp
      apply(subst Sup_image_eadd2[symmetric])
       apply clarsimp
      apply(rule SUP_upper2)
       apply(rule imageI)
       apply simp
      apply(rule order_trans)
       apply(rule step.hyps)
      apply(rule enat_le_plus_same)
      done
    done
qed

lemma interaction_bounded_by_try_gpv [interaction_bound]:
  "interaction_bounded_by consider (try_gpv gpv1 gpv2) (bound1 + bound2)"
  if "interaction_bounded_by consider gpv1 bound1" "interaction_bounded_by consider gpv2 bound2"
  using that interaction_bound_try_gpv[of "consider" gpv1 gpv2]
  by(simp add: interaction_bounded_by.simps)(meson add_left_mono_trans add_right_mono le_left_mono)


subsection ‹term ‹gpv_stop››

lemma interaction_bounded_by_gpv_stop [interaction_bound]:
  assumes "interaction_bounded_by consider gpv n"
  shows "interaction_bounded_by consider (gpv_stop gpv) n"
  using assms by(simp add: interaction_bounded_by.simps)

context includes ℐ.lifting begin

lift_definition stop_ℐ :: "('a, 'b) ℐ ⇒ ('a, 'b option) ℐ" is
  "λresp x. if (resp x = {}) then {} else insert None (Some ` resp x)" .

lemma outs_stop_ℐ [simp]: "outs_ℐ (stop_ℐ ℐ) = outs_ℐ ℐ"
  by transfer auto

lemma responses_stop_ℐ [simp]: 
  "responses_ℐ (stop_ℐ ℐ) x = (if x ∈ outs_ℐ ℐ then insert None (Some ` responses_ℐ ℐ x) else {})" 
  by transfer auto

lemma stop_ℐ_full [simp]: "stop_ℐ ℐ_full = ℐ_full"
  by transfer(auto simp add: fun_eq_iff notin_range_Some)

lemma stop_ℐ_uniform [simp]: 
  "stop_ℐ (ℐ_uniform A B) = (if B = {} then ⊥ else ℐ_uniform A (insert None (Some ` B)))"
  unfolding bot_ℐ_def by transfer(simp add: fun_eq_iff)

lifting_update ℐ.lifting
lifting_forget ℐ.lifting

end

lemma stop_ℐ_bot [simp]: "stop_ℐ ⊥ = ⊥"
  by(simp only: bot_ℐ_def stop_ℐ_uniform)(simp)

lemma WT_gpv_stop [simp, WT_intro]: "stop_ℐ ℐ ⊢g gpv_stop gpv √" if "ℐ ⊢g gpv √"
  using that by(coinduction arbitrary: gpv)(auto 4 3 dest: WT_gpvD)

lemma expectation_gpv_stop:
  fixes fail and gpv :: "('a, 'b, 'c) gpv"
  assumes WT: "ℐ ⊢g gpv √"
  and fail: "fail ≤ c"
  shows "expectation_gpv fail (stop_ℐ ℐ) (λ_. c) (gpv_stop gpv) = expectation_gpv fail ℐ (λ_. c) gpv" (is "?lhs = ?rhs")
proof(rule antisym)
  show "expectation_gpv fail (stop_ℐ ℐ) (λ_. c) (gpv_stop gpv) ≤ expectation_gpv fail ℐ (λ_. c) gpv"
    using WT
  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])
    case adm show ?case by simp
    case bottom show ?case by simp
    case (step f g)
    then show ?case
      apply(simp add: pmf_map_spmf_None measure_spmf_return_spmf nn_integral_return)
      apply(rule disjI2 nn_integral_mono_AE)+
      apply(auto split!: generat.split simp add: image_image dest: WT_gpvD intro!: le_infI2 INF_mono)
      done
  qed

  define stop :: "('a option, 'b, 'c option) gpv ⇒ _" where "stop = expectation_gpv fail (stop_ℐ ℐ) (λ_. c)"
  show "?rhs ≤ stop (gpv_stop gpv)" using WT
  proof(induction arbitrary: gpv rule: expectation_gpv_fixp_induct)
    case adm show ?case by simp
    case bottom show ?case by simp
    case (step expectation_gpv')
    have "expectation_gpv' gpv' ≤ c" if "ℐ ⊢g gpv' √" for gpv'
      using expectation_gpv_const_le[of ℐ gpv' fail c] fail step.hyps(1)[of gpv'] that
      by(simp add: max_def split: if_split_asm)
    then show ?case using step unfolding stop_def
      apply(subst expectation_gpv.simps)
      apply(simp add: pmf_map_spmf_None)
      apply(rule disjI2 nn_integral_mono_AE)+
      apply(clarsimp split!: generat.split simp add: image_image)
      subgoal by(auto 4 3 simp add: in_outs_ℐ_iff_responses_ℐ dest: WT_gpv_ContD intro: INF_lower2)
      subgoal by(auto intro!: INF_mono rev_bexI dest: WT_gpvD)
      done
  qed
qed

lemma pgen_lossless_gpv_stop:
  fixes fail and gpv :: "('a, 'b, 'c) gpv"
  assumes WT: "ℐ ⊢g gpv √"
  and fail: "fail ≤ 1"
  shows "pgen_lossless_gpv fail (stop_ℐ ℐ) (gpv_stop gpv) = pgen_lossless_gpv fail ℐ gpv"
  by(simp add: pgen_lossless_gpv_def expectation_gpv_stop assms)

lemma pfinite_gpv_stop [simp]:
  "pfinite_gpv (stop_ℐ ℐ) (gpv_stop gpv) ⟷ pfinite_gpv ℐ gpv" if "ℐ ⊢g gpv √"
  using that by(simp add: pgen_lossless_gpv_stop)

lemma plossless_gpv_stop [simp]:
  "plossless_gpv (stop_ℐ ℐ) (gpv_stop gpv) ⟷ plossless_gpv ℐ gpv" if "ℐ ⊢g gpv √"
  using that by(simp add: pgen_lossless_gpv_stop)

lemma results_gpv_stop_SomeD: "Some x ∈ results_gpv (stop_ℐ ℐ) (gpv_stop gpv) ⟹ x ∈ results_gpv ℐ gpv"
  by(induction gpv'≡"gpv_stop gpv" arbitrary: gpv rule: results_gpv.induct)
    (auto 4 3 intro: results_gpv.intros split: if_split_asm)

lemma Some_in_results'_gpv_gpv_stopD: "Some xy ∈ results'_gpv (gpv_stop gpv) ⟹ xy ∈ results'_gpv gpv"
  unfolding results_gpv_ℐ_full[symmetric]
  by(rule results_gpv_stop_SomeD) simp

subsection ‹term ‹exception_ℐ››

datatype 's exception = Fault | OK (ok: 's)

lemma inj_on_OK [simp]: "inj_on OK A"
  by(auto simp add: inj_on_def)

function join_exception :: "'a exception ⇒ 'b exception ⇒ ('a × 'b) exception" where
  "join_exception Fault _ = Fault"
| "join_exception _ Fault = Fault"
| "join_exception (OK a) (OK b) = OK (a, b)"
  by pat_completeness auto
termination by lexicographic_order

primrec merge_exception :: "'a exception + 'b exception ⇒ ('a + 'b) exception" where
  "merge_exception (Inl x) = map_exception Inl x"
| "merge_exception (Inr y) = map_exception Inr y"

fun option_of_exception :: "'a exception ⇒ 'a option" where
  "option_of_exception Fault = None"
| "option_of_exception (OK x) = Some x"

fun exception_of_option :: "'a option ⇒ 'a exception" where
  "exception_of_option None = Fault"
| "exception_of_option (Some x) = OK x"


lemma option_of_exception_exception_of_option [simp]: "option_of_exception (exception_of_option x) = x"
  by(cases x) simp_all

lemma exception_of_option_option_of_exception [simp]: "exception_of_option (option_of_exception x) = x"
  by(cases x) simp_all

lemma case_exception_of_option [simp]: "case_exception f g (exception_of_option x) = case_option f g x"
  by(simp split: exception.split option.split)

lemma case_option_of_exception [simp]: "case_option f g (option_of_exception x) = case_exception f g x"
  by(simp split: exception.split option.split)

lemma surj_exception_of_option [simp]: "surj exception_of_option"
  by(rule surjI[where f="option_of_exception"])(simp)

lemma surj_option_of_exception [simp]: "surj option_of_exception"
  by(rule surjI[where f="exception_of_option"])(simp)

lemma case_map_exception [simp]: "case_exception f g (map_exception h x) = case_exception f (g ∘ h) x"
  by(simp split: exception.split)

definition exception_ℐ :: "('a, 'b) ℐ ⇒ ('a, 'b exception) ℐ" where 
  "exception_ℐ ℐ = map_ℐ id exception_of_option (stop_ℐ ℐ)"

lemma outs_exception_ℐ [simp]: "outs_ℐ (exception_ℐ ℐ) = outs_ℐ ℐ"
  by(simp add: exception_ℐ_def)

lemma responses_exception_ℐ [simp]: 
  "responses_ℐ (exception_ℐ ℐ) x = (if x ∈ outs_ℐ ℐ then insert Fault (OK ` responses_ℐ ℐ x) else {})" 
  by(simp add: exception_ℐ_def image_image)

lemma map_ℐ_full [simp]: "map_ℐ f g ℐ_full = ℐ_uniform UNIV (range g)"
  unfolding ℐ_uniform_UNIV[symmetric] map_ℐ_ℐ_uniform by simp

lemma exception_ℐ_full [simp]: "exception_ℐ ℐ_full = ℐ_full"
  unfolding exception_ℐ_def by simp

lemma exception_ℐ_uniform [simp]: 
  "exception_ℐ (ℐ_uniform A B) = (if B = {} then ⊥ else ℐ_uniform A (insert Fault (OK ` B)))"
  by(simp add: exception_ℐ_def image_image)

lemma option_of_exception_ℐ [simp]: "map_ℐ id option_of_exception (exception_ℐ ℐ) = stop_ℐ ℐ"
  by(simp add: exception_ℐ_def o_def id_def[symmetric])

lemma exception_of_option_ℐ [simp]: "map_ℐ id exception_of_option (stop_ℐ ℐ) = exception_ℐ ℐ"
  by(simp add: exception_ℐ_def)

subsection ‹inline›

context raw_converter_invariant begin

context
  fixes gpv :: "('a, 'call, 'ret) gpv"
  assumes gpv: "plossless_gpv ℐ gpv" "ℐ ⊢g gpv √"
begin

lemma lossless_spmf_inline1:
  assumes lossless: "⋀s x. ⟦ x ∈ outs_ℐ ℐ; I s ⟧ ⟹ lossless_spmf (the_gpv (callee s x))"
    and I: "I s"
  shows "lossless_spmf (inline1 callee gpv s)"
proof -
  have "1 = expectation_gpv 0 ℐ (λ_. 1) gpv" using gpv by(simp add: pgen_lossless_gpv_def)
  also have "… ≤ weight_spmf (inline1 callee gpv s)" using gpv(2) I
  proof(induction arbitrary: gpv s rule: expectation_gpv_fixp_induct)
    case adm show ?case by simp
    case bottom show ?case by simp
    case (step expectation_gpv')
    { fix out c
      assume IO: "IO out c ∈ set_spmf (the_gpv gpv)"
      with step.prems have out: "out ∈ outs_ℐ ℐ" by(auto dest: WT_gpvD)
      from out[unfolded in_outs_ℐ_iff_responses_ℐ] obtain input where input: "input ∈ responses_ℐ ℐ out" by auto
      from out have "(⨅r∈responses_ℐ ℐ out. expectation_gpv' (c r)) = ∫⇧+ x. (⨅r∈responses_ℐ ℐ out. expectation_gpv' (c r)) ∂measure_spmf (the_gpv (callee s out))"
        using lossless ‹I s› by(simp add: lossless_spmf_def measure_spmf.emeasure_eq_measure)
      also have "… ≤ ∫⇧+ generat. (case generat of Pure (r, s') ⇒ weight_spmf (inline1 callee (c r) s') | _ ⇒ 1) ∂measure_spmf (the_gpv (callee s out))"
        apply(intro nn_integral_mono_AE)
        apply(clarsimp split!: generat.split)
        subgoal Pure
          apply(rule INF_lower2)
           apply(fastforce dest: results_callee[OF out ‹I s›, THEN subsetD, OF results_gpv.Pure])
          apply(rule step.IH)
           apply(fastforce intro: WT_gpvD[OF step.prems(1) IO] dest: results_callee[OF out ‹I s›, THEN subsetD, OF results_gpv.Pure])
          apply(fastforce dest: results_callee[OF out ‹I s›, THEN subsetD, OF results_gpv.Pure])
          done
        subgoal IO
          apply(rule INF_lower2[OF input])
          apply(rule order_trans)
           apply(rule step.hyps)
          apply(rule order_trans)
           apply(rule expectation_gpv_const_le)
           apply(rule WT_gpvD[OF step.prems(1) IO])
           apply(simp_all add: input)
          done
        done
      finally have "(⨅r∈responses_ℐ ℐ out. expectation_gpv' (c r)) ≤ …" . }
    then show ?case using step.prems
      apply(subst inline1.simps)
      apply(simp add: measure_spmf.emeasure_eq_measure[symmetric])
      apply(simp add: measure_spmf_bind)
      apply(subst emeasure_bind[where N="count_space UNIV"])
         apply(simp add: space_measure_spmf)
        apply(simp add: o_def)
       apply(simp)
      apply(rule nn_integral_mono_AE)
      apply(clarsimp split!: generat.split simp add: measure_spmf_return_spmf space_measure_spmf)
      apply(simp add: measure_spmf_bind)
      apply(subst emeasure_bind[where N="count_space UNIV"])
         apply(simp add: space_measure_spmf)
        apply(simp add: o_def)
       apply(simp)
      apply (simp add: measure_spmf.emeasure_eq_measure)
      apply(subst generat.case_distrib[where h="λx. measure (measure_spmf x) _"])
      apply(simp add: split_def measure_spmf_return_spmf space_measure_spmf measure_return cong del: generat.case_cong)
      done
  qed
  finally show ?thesis using weight_spmf_le_1[of "inline1 callee gpv s"] by(simp add: lossless_spmf_def)
qed

end

end

lemma (in raw_converter_invariant) inline1_try_gpv:
  defines "inline1' ≡ inline1"
  assumes WT: "ℐ ⊢g gpv √"
    and pfinite: "pfinite_gpv ℐ gpv"
    and f: "⋀s. I s ⟹ f (x, s) = z"
    and lossless: "⋀s x. ⟦ x ∈ outs_ℐ ℐ; I s ⟧ ⟹ colossless_gpv ℐ' (callee s x)"
    and I: "I s"
  shows "map_spmf (map_sum f id) (inline1 callee (try_gpv gpv (Done x)) s) =
   try_spmf (map_spmf (map_sum f (λ(out, c, rpv). (out, c, λinput. try_gpv (rpv input) (Done x)))) (inline1' callee gpv s)) (return_spmf (Inl z))"
  (is "?lhs = ?rhs")
proof -
  have le: "ord_spmf (=) ?lhs ?rhs" using WT I
  proof(induction arbitrary: gpv s rule: inline1_fixp_induct)
    case adm show ?case by simp
    case bottom show ?case by simp
    case (step inline1'')
    show ?case using step.prems unfolding inline1'_def
      apply(subst inline1.simps)
      apply(simp add: bind_map_spmf map_bind_spmf o_def)
      apply(simp add: try_spmf_def)
      apply(subst bind_spmf_pmf_assoc)
      apply(simp add: bind_map_pmf)
      apply(subst (3) bind_spmf_def)
      apply(simp add: bind_assoc_pmf)
      apply(rule rel_pmf_bindI[where R="eq_onp (λx. x ∈ set_pmf (the_gpv gpv))"])
       apply(rule pmf.rel_refl_strong)
       apply(simp add: eq_onp_def)
      apply(clarsimp simp add: eq_onp_def bind_return_pmf f split!: option.split generat.split)
      subgoal for out c
        apply(simp add: in_set_spmf[symmetric] bind_map_pmf map_bind_spmf)
        apply(subst option.case_distrib[where h=return_pmf, symmetric, abs_def])
        apply(fold map_pmf_def)
        apply(simp add: bind_spmf_def map_bind_pmf)
        apply(rule rel_pmf_bindI[where R="eq_onp (λx. x ∈ set_pmf (the_gpv (callee s out)))"])
         apply(rule pmf.rel_refl_strong)
         apply(simp add: eq_onp_def)
        apply(simp add: in_set_spmf[symmetric] bind_map_pmf map_bind_spmf eq_onp_def split!: option.split generat.split)
        apply(rule spmf.leq_trans)
         apply(rule step.IH[unfolded inline1'_def])
        subgoal
          by(auto dest: results_callee[THEN subsetD, OF _ _ results_gpv.Pure, rotated -1] WT_gpvD)
        subgoal 
          by(auto dest: results_callee[THEN subsetD, OF _ _ results_gpv.Pure, rotated -1] WT_gpvD)
        apply(simp add: try_spmf_def)
        apply(subst option.case_distrib[where h=return_pmf, symmetric, abs_def])
        apply(fold map_pmf_def)
        apply simp
        done
      done
  qed
  have "lossless_spmf ?lhs" using I
    apply simp
    apply(rule lossless_spmf_inline1)
       apply(rule plossless_gpv_try_gpvI)
        apply(rule pfinite)
       apply simp
      apply(rule WT_gpv_try_gpvI)
       apply(rule WT)
      apply simp
     apply(rule colossless_gpv_lossless_spmfD[OF lossless])
      apply simp_all
    done
  from ord_spmf_lossless_spmfD1[OF le this] show ?thesis by(simp add: spmf_rel_eq)
qed
                        
lemma (in raw_converter_invariant) inline_try_gpv:
  assumes WT: "ℐ ⊢g gpv √"
    and pfinite: "pfinite_gpv ℐ gpv"
    and f: "⋀s. I s ⟹ f (x, s) = z"
    and lossless: "⋀s x. ⟦ x ∈ outs_ℐ ℐ; I s ⟧ ⟹ colossless_gpv ℐ' (callee s x)"
    and I: "I s"
  shows "eq_ℐ_gpv (=) ℐ' (map_gpv f id (inline callee (try_gpv gpv (Done x)) s)) (try_gpv (map_gpv f id (inline callee gpv s)) (Done z))"
  (is "eq_ℐ_gpv _ _ ?lhs ?rhs")
  using WT pfinite I
proof(coinduction arbitrary: gpv s rule: eq_ℐ_gpv_coinduct_bind)
  case (eq_ℐ_gpv gpv s)
  show "?case TYPE(('ret × 's) option) TYPE(('ret × 's) option)" (is "rel_spmf (eq_ℐ_generat _ _ ?X) ?lhs ?rhs")
  proof -
   have "?lhs = map_spmf
           (λx. case x of Inl rs ⇒ Pure rs | Inr (out, oracle, rpv) ⇒ IO out (λinput. 
               map_gpv f id (bind_gpv (try_gpv (map_gpv Some id (oracle input)) (Done None)) (λxy. case xy of None ⇒ Fail | Some (x, y) ⇒ inline callee (rpv x) y))))
           (map_spmf (map_sum f id) (inline1 callee (TRY gpv ELSE Done x) s))"
      (is "_ = map_spmf ?f ?lhs2")
      by(auto simp add: gpv.map_sel inline_sel spmf.map_comp o_def bind_gpv_try_gpv_map_Some intro!: map_spmf_cong[OF refl] split: sum.split)
    also from eq_ℐ_gpv
    have "?lhs2 = TRY map_spmf (map_sum f (λ(out, c, rpv). (out, c, λinput. TRY rpv input ELSE Done x))) (inline1 callee gpv s) ELSE return_spmf (Inl z)"
      by(intro inline1_try_gpv)(auto intro: f lossless)
    also have "… = map_spmf (λy. case y of None ⇒ Inl z | Some x' ⇒ map_sum f (λ(out, c, rpv). (out, c, λinput. try_gpv (rpv input) (Done x))) x') 
        (try_spmf (map_spmf Some (inline1 callee gpv s)) (return_spmf None))"
      (is "_ = ?lhs3") by(simp add: map_try_spmf spmf.map_comp o_def)
    also have "?rhs = map_spmf (λy. case y of None ⇒ Pure z | Some (Inl x) ⇒ Pure (f x)
           | Some (Inr (out, oracle, rpv)) ⇒ IO out (λinput. try_gpv (map_gpv f id (bind_gpv (oracle input) (λ(x, y). inline callee (rpv x) y))) (Done z)))
       (try_spmf (map_spmf Some (inline1 callee gpv s)) (return_spmf None))"
      by(auto simp add: gpv.map_sel inline_sel spmf.map_comp o_def generat.map_comp spmf_rel_map map_try_spmf intro!: try_spmf_cong map_spmf_cong split: sum.split)
    moreover have "rel_spmf (eq_ℐ_generat (=) ℐ' ?X) (map_spmf ?f ?lhs3) …"
      apply(clarsimp simp add: gpv.map_sel inline_sel spmf.map_comp o_def generat.map_comp spmf_rel_map intro!: rel_spmf_reflI)
      apply(erule disjE)
      subgoal
        apply(clarsimp split!: generat.split sum.split simp add: map_gpv_id_bind_gpv)
        apply(subst (3) try_gpv_bind_gpv)
        apply(rule conjI)
         apply(erule WT_gpv_inline1[OF _ eq_ℐ_gpv(1,3)])
        apply(rule strip)+
        apply(rule disjI2)+
        subgoal for out rpv rpv' input
          apply(rule exI)
          apply(rule exI)
          apply(rule exI[where x="λx y. x = y ∧ y ∈ results_gpv ℐ' (TRY map_gpv Some id (rpv input) ELSE Done None)"])
          apply(rule exI conjI refl)+
           apply(rule eq_ℐ_gpv_reflI)
            apply(simp add: eq_onp_def)
           apply(rule WT_intro)
            apply simp
            apply(erule (1) WT_gpv_inline1[OF _ eq_ℐ_gpv(1,3)])
           apply simp
          apply(rule rel_funI)
          apply(clarsimp simp add: eq_onp_def split: if_split_asm)
          subgoal
            apply(rule exI conjI refl)+
             apply(drule (2) WT_gpv_inline1(3)[OF _ eq_ℐ_gpv(1,3)])
             apply simp
            apply(frule (2) WT_gpv_inline1(3)[OF _ eq_ℐ_gpv(1,3)])
            apply(drule (2) inline1_in_sub_gpvs[OF _ _ _ eq_ℐ_gpv(1,3)])
            apply clarsimp
            apply(erule pfinite_gpv_sub_gpvs[OF eq_ℐ_gpv(2) _ eq_ℐ_gpv(1)])
            done
          subgoal
            apply(erule disjE; clarsimp)
             apply(rule exI conjI refl)+
              apply(drule (2) WT_gpv_inline1(3)[OF _ eq_ℐ_gpv(1,3)])
              apply simp
             apply(frule (2) WT_gpv_inline1(3)[OF _ eq_ℐ_gpv(1,3)])
             apply(drule (2) inline1_in_sub_gpvs[OF _ _ _ eq_ℐ_gpv(1,3)])
             apply clarsimp
             apply(erule pfinite_gpv_sub_gpvs[OF eq_ℐ_gpv(2) _ eq_ℐ_gpv(1)])
            apply(erule notE)
            apply(drule inline1_in_sub_gpvs_callee[OF _ eq_ℐ_gpv(1,3)])
            apply clarify
            apply(drule (1) bspec)
            apply(erule colossless_gpv_sub_gpvs[rotated])
            apply(rule lossless; simp)
            done
          done
        done
      subgoal by(clarsimp split: if_split_asm)
      done
    ultimately show ?thesis by(simp only:)
  qed
qed


definition cr_prod2 :: "'a ⇒ ('b ⇒ 'c ⇒ bool) ⇒ 'b ⇒ 'a × 'c ⇒ bool" where
  "cr_prod2 x A = (λb (a, c). A b c ∧ x = a)"

lemma cr_prod2_simps [simp]: "cr_prod2 x A a (b, c) ⟷ A a c ∧ x = b"
by(simp add: cr_prod2_def)

lemma cr_prod2I: "A a b ⟹ cr_prod2 x A a (x, b)" by simp

lemma cr_prod2_Grp: "cr_prod2 x (BNF_Def.Grp A f) = BNF_Def.Grp A (λb. (x, f b))"
by(auto simp add: Grp_def fun_eq_iff)

(* A stronger version of the existing extend_state_oracle_transfer *)
lemma extend_state_oracle_transfer': includes lifting_syntax shows
  "((S ===> C ===> rel_spmf (rel_prod R S)) ===> cr_prod2 s S ===> C ===> rel_spmf (rel_prod R (cr_prod2 s S))) (λoracle. oracle) extend_state_oracle"
unfolding extend_state_oracle_def[abs_def]
apply(rule rel_funI)+
apply clarsimp
apply(drule (1) rel_funD)+
apply(auto simp add: spmf_rel_map split_def dest: rel_funD intro: rel_spmf_mono)
done

(* @Reza: This is a proof based on parametricity,
 using the relation cr_prod2 s (=) to fix the first component of the extended callee state to s *)

lemma exec_gpv_extend_state_oracle:
  "exec_gpv (extend_state_oracle callee) gpv (s, s') =
  map_spmf (λ(x, s''). (x, (s, s''))) (exec_gpv callee gpv s')"
  using exec_gpv_parametric'[THEN rel_funD, OF extend_state_oracle_transfer'[THEN rel_funD], of "(=)" "(=)" "(=)" callee callee "(=)" s]
  unfolding relator_eq rel_gpv''_eq
  apply(clarsimp simp add: rel_fun_def)
  apply(unfold eq_alt cr_prod2_Grp prod.rel_Grp option.rel_Grp pmf.rel_Grp)
  apply(simp add: Grp_def map_prod_def)
  apply(blast intro: sym)
  done





section ‹Material for Constructive Crypto›

lemma WT_resource_ℐ_uniform_UNIV [simp]: "ℐ_uniform A UNIV ⊢res res √"
  by(coinduction arbitrary: res) auto

lemma WT_converter_of_callee_invar:
  assumes WT: "⋀s q. ⟦ q ∈ outs_ℐ ℐ; I s ⟧ ⟹ ℐ' ⊢g callee s q √"
    and res: "⋀s q r s'. ⟦ (r, s') ∈ results_gpv ℐ' (callee s q); q ∈ outs_ℐ ℐ; I s  ⟧ ⟹ r ∈ responses_ℐ ℐ q ∧ I s'"
    and I: "I s"
  shows "ℐ, ℐ' ⊢⇩C converter_of_callee callee s √"
  using I by(coinduction arbitrary: s)(auto simp add: WT res)

lemma eq_ℐ_gpv_eq_OO:
  assumes "eq_ℐ_gpv (=) ℐ gpv gpv'" "eq_ℐ_gpv A ℐ gpv' gpv''"
  shows "eq_ℐ_gpv A ℐ gpv gpv''"
  using eq_ℐ_gpv_relcompp[THEN fun_cong, THEN fun_cong, THEN iffD2, OF relcomppI, OF assms]
  by(simp add: eq_OO)

lemma eq_ℐ_gpv_eq_OO2:
  assumes "eq_ℐ_gpv (=) ℐ gpv'' gpv'" "eq_ℐ_gpv A ℐ gpv gpv'"
  shows "eq_ℐ_gpv A ℐ gpv gpv''"
  using eq_ℐ_gpv_relcompp[where A'="conversep (=)", THEN fun_cong, THEN fun_cong, THEN iffD2, OF relcomppI, OF assms(2)] assms(1)
  unfolding eq_ℐ_gpv_conversep by(simp add: OO_eq)

lemma eq_ℐ_gpv_try_gpv_cong:
  assumes "eq_ℐ_gpv A ℐ gpv1 gpv1'"
    and "eq_ℐ_gpv A ℐ gpv2 gpv2'"
  shows "eq_ℐ_gpv A ℐ (try_gpv gpv1 gpv2) (try_gpv gpv1' gpv2')"
  using assms(1)
  apply(coinduction arbitrary: gpv1 gpv1')
  using assms(2)
  apply(fastforce simp add: spmf_rel_map intro!: rel_spmf_try_spmf dest: eq_ℐ_gpvD elim!: rel_spmf_mono_strong eq_ℐ_generat.cases)
  done

lemma eq_ℐ_gpv_map_gpv':
  assumes "eq_ℐ_gpv (BNF_Def.vimage2p f f' A) (map_ℐ g h ℐ) gpv1 gpv2"
  shows "eq_ℐ_gpv A ℐ (map_gpv' f g h gpv1) (map_gpv' f' g h gpv2)"
  using assms
proof(coinduction arbitrary: gpv1 gpv2)
  case eq_ℐ_gpv
  from this[THEN eq_ℐ_gpvD] show ?case
    apply(simp add: spmf_rel_map)
    apply(erule rel_spmf_mono)
    apply(auto 4 4 simp add: BNF_Def.vimage2p_def elim!: eq_ℐ_generat.cases)
    done
qed

lemma eq_ℐ_converter_map_converter:
  assumes "map_ℐ (inv_into UNIV f) (inv_into UNIV g) ℐ, map_ℐ f' g' ℐ' ⊢⇩C conv1 ∼ conv2"
    and "inj f" "surj g"
  shows "ℐ, ℐ' ⊢⇩C map_converter f g f' g' conv1 ∼ map_converter f g f' g' conv2"
  using assms(1)
proof(coinduction arbitrary: conv1 conv2)
  case eq_ℐ_converter
  from this(2) have "f q ∈ outs_ℐ (map_ℐ (inv_into UNIV f) (inv_into UNIV g) ℐ)" using assms(2) by simp
  from eq_ℐ_converter(1)[THEN eq_ℐ_converterD, OF this] show ?case using assms(2,3)
    apply simp
    apply(rule eq_ℐ_gpv_map_gpv')
    apply(simp add: BNF_Def.vimage2p_def prod.rel_map)
    apply(erule eq_ℐ_gpv_mono')
     apply(auto 4 4 simp add: eq_onp_def surj_f_inv_f)
    done
qed

lemma resource_of_oracle_run_resource: "resource_of_oracle run_resource res = res"
  by(coinduction arbitrary: res)(auto simp add: rel_fun_def spmf_rel_map intro!: rel_spmf_reflI)

lemma connect_map_gpv':
  "connect (map_gpv' f g h adv) res = map_spmf f (connect adv (map_resource g h res))"
  unfolding connect_def
  by(subst (3) resource_of_oracle_run_resource[symmetric])
    (simp add: exec_gpv_map_gpv' map_resource_resource_of_oracle spmf.map_comp exec_gpv_resource_of_oracle)

primcorec fail_resource :: "('a, 'b) resource" where
  "run_resource fail_resource = (λ_. return_pmf None)"

lemma WT_fail_resource [WT_intro]: "ℐ ⊢res fail_resource √"
  by(rule WT_resourceI) simp

context fixes y :: "'b" begin

primcorec const_resource :: "('a, 'b) resource" where
  "run_resource const_resource = (λ_. map_spmf (map_prod id (λ_. const_resource)) (return_spmf (y, ())))" 

end

lemma const_resource_sel [simp]: "run_resource (const_resource y) = (λ_. return_spmf (y, const_resource y))"
  by simp

declare const_resource.sel [simp del]

lemma lossless_const_resource [simp]: "lossless_resource ℐ (const_resource y)"
  by(coinduction) simp

lemma WT_const_resource [simp]:
  "ℐ ⊢res const_resource y √ ⟷ (∀x∈outs_ℐ ℐ. y ∈ responses_ℐ ℐ x)" (is "?lhs ⟷ ?rhs")
proof(intro iffI ballI)
  show "y ∈ responses_ℐ ℐ x" if ?lhs and "x ∈ outs_ℐ ℐ" for x using WT_resourceD[OF that] by auto
  show ?lhs if ?rhs using that by(coinduction)(auto)
qed

context fixes y :: "'b" begin

primcorec const_converter :: "('a, 'b, 'c, 'd) converter" where
  "run_converter const_converter = (λ_. map_gpv (map_prod id (λ_. const_converter)) id (Done (y, ())))"

end

lemma const_converter_sel [simp]: "run_converter (const_converter y) = (λ_. Done (y, const_converter y))"
  by simp

lemma attach_const_converter [simp]: "attach (const_converter y) res = const_resource y"
  by(coinduction)(simp add: rel_fun_def)

declare const_converter.sel [simp del]

lemma comp_const_converter [simp]: "comp_converter (const_converter x) conv = const_converter x"
  by(coinduction)(simp add: rel_fun_def)

lemma interaction_bounded_const_converter [simp, interaction_bound]: 
  "interaction_any_bounded_converter (const_converter Fault) bound"
  by(coinduction) simp


primcorec merge_exception_converter :: "('a, ('b + 'c) exception, 'a, 'b exception + 'c exception) converter" where
  "run_converter merge_exception_converter = 
   (λx. map_gpv (map_prod id (λconv. case conv of None ⇒ merge_exception_converter | Some conv' ⇒ conv')) id (
     Pause x (λy. Done (case merge_exception y of Fault ⇒ (Fault, Some (const_converter Fault))
                              | OK y' ⇒ (OK y', None)))))"

lemma merge_exception_converter_sel [simp]:
  "run_converter merge_exception_converter x =
   Pause x (λy. Done (case merge_exception y of Fault ⇒ (Fault, const_converter Fault) | OK y' ⇒ (OK y', merge_exception_converter)))"
  by(simp add: o_def fun_eq_iff split: exception.split)

declare merge_exception_converter.sel[simp del]

lemma plossless_const_converter[simp]: "plossless_converter ℐ ℐ' (const_converter x)"
  by(coinduction) auto

lemma plossless_merge_exception_converter [simp]:
  "plossless_converter (exception_ℐ (ℐ ⊕⇩ℐ ℐ')) (exception_ℐ ℐ ⊕⇩ℐ exception_ℐ ℐ') merge_exception_converter"
  by(coinduction) auto

lemma WT_const_converter [WT_intro, simp]:
  "ℐ, ℐ' ⊢⇩C const_converter x √" if "∀q ∈ outs_ℐ ℐ. x ∈ responses_ℐ ℐ q"
  by(coinduction)(auto simp add: that)

lemma WT_merge_exception_converter [WT_intro, simp]: 
  "exception_ℐ (ℐ1' ⊕⇩ℐ ℐ2'), exception_ℐ ℐ1' ⊕⇩ℐ exception_ℐ ℐ2' ⊢⇩C merge_exception_converter √"
  by(coinduction) auto

lemma inline_left_gpv_merge_exception_converter:
  "bind_gpv (inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpv))) merge_exception_converter) (λ(x, conv'). case x of None ⇒ Fail | Some x' ⇒ Done (x, conv')) =
   bind_gpv (left_gpv (map_gpv' id id option_of_exception (gpv_stop gpv))) (λx. case x of None ⇒ Fail | Some x' ⇒ Done (x, merge_exception_converter))"
  apply(coinduction arbitrary: gpv rule: gpv.coinduct_strong)
  apply(simp add: bind_gpv.sel inline_sel map_bind_spmf bind_map_spmf del: bind_gpv_sel')
  apply(subst inline1_unfold)
  apply(clarsimp simp add: bind_map_spmf intro!: rel_spmf_bind_reflI simp add: generat.map_comp case_map_generat o_def split!: generat.split intro!: rel_funI)
  subgoal for gpv out c input by(cases input; auto split!: exception.split)
  done

lemma inline_right_gpv_merge_exception_converter:
  "bind_gpv (inline run_converter (map_gpv' id id option_of_exception (gpv_stop (right_gpv gpv))) merge_exception_converter) (λ(x, conv'). case x of None ⇒ Fail | Some x' ⇒ Done (x, conv')) =
   bind_gpv (right_gpv (map_gpv' id id option_of_exception (gpv_stop gpv))) (λx. case x of None ⇒ Fail | Some x' ⇒ Done (x, merge_exception_converter))"
  apply(coinduction arbitrary: gpv rule: gpv.coinduct_strong)
  apply(simp add: bind_gpv.sel inline_sel map_bind_spmf bind_map_spmf del: bind_gpv_sel')
  apply(subst inline1_unfold)
  apply(clarsimp simp add: bind_map_spmf intro!: rel_spmf_bind_reflI simp add: generat.map_comp case_map_generat o_def split!: generat.split intro!: rel_funI)
  subgoal for gpv out c input by(cases input; auto split!: exception.split)
  done

subsection ‹@{theory Constructive_Cryptography.Wiring}›

abbreviation (input) 
  id_wiring :: "('a, 'b, 'a, 'b) wiring" (‹1⇩w›)
  where
    "id_wiring ≡ (id, id)"

definition 
  swap_lassocr⇩w :: "('a + 'b + 'c, 'd + 'e + 'f, 'b + 'a + 'c, 'e + 'd + 'f) wiring" 
  where
    "swap_lassocr⇩w ≡ rassocl⇩w ∘⇩w ((swap⇩w |⇩w 1⇩w) ∘⇩w lassocr⇩w)"

schematic_goal 
  wiring_swap_lassocr[wiring_intro]: "wiring ?ℐ1 ?ℐ2 swap_lassocr swap_lassocr⇩w"
  unfolding swap_lassocr_def swap_lassocr⇩w_def
  by(rule wiring_intro)+

definition 
  parallel_wiring⇩w :: "(('a + 'b) + ('c + 'd), ('e + 'f) + ('g + 'h),
   ('a + 'c) + ('b + 'd), ('e + 'g) + ('f + 'h)) wiring" 
  where
    "parallel_wiring⇩w ≡ lassocr⇩w ∘⇩w ((1⇩w |⇩w swap_lassocr⇩w) ∘⇩w rassocl⇩w)"

schematic_goal 
  wiring_parallel_wiring[wiring_intro]: "wiring ?ℐ1 ?ℐ2 parallel_wiring parallel_wiring⇩w"
  unfolding parallel_wiring_def parallel_wiring⇩w_def
  by(rule wiring_intro)+


lemma lassocr_inverse: "rassocl⇩C ⊙ lassocr⇩C = 1⇩C"
  unfolding rassocl⇩C_def lassocr⇩C_def
  apply(simp add: comp_converter_map1_out comp_converter_map_converter2 comp_converter_id_right)
  apply(subst map_converter_id_move_right)
  apply(simp add: o_def id_def[symmetric])
  done

lemma rassocl_inverse: "lassocr⇩C ⊙ rassocl⇩C = 1⇩C"
  unfolding rassocl⇩C_def lassocr⇩C_def
  apply(simp add: comp_converter_map1_out comp_converter_map_converter2 comp_converter_id_right)
  apply(subst map_converter_id_move_right)
  apply(simp add: o_def id_def[symmetric])
  done

lemma swap_sum_swap_sum [simp]: "swap_sum (swap_sum x) = x"
  by(cases x) simp_all

lemma inj_on_lsumr [simp]: "inj_on lsumr A"
  by(auto simp add: inj_on_def elim: lsumr.elims)

lemma inj_on_rsuml [simp]: "inj_on rsuml A"
  by(auto simp add: inj_on_def elim: rsuml.elims)

lemma bij_lsumr [simp]: "bij lsumr"
  by(rule o_bij[where g=rsuml]) auto

lemma bij_swap_sum [simp]: "bij swap_sum"
  by(rule o_bij[where g=swap_sum]) auto

lemma bij_rsuml [simp]: "bij rsuml"
  by(rule o_bij[where g=lsumr]) auto

lemma bij_lassocr_swap_sum [simp]: "bij lassocr_swap_sum"
  unfolding lassocr_swap_sum_def
  by(simp add: bij_comp)

lemma inj_lassocr_swap_sum [simp]: "inj lassocr_swap_sum"
  by(simp add: bij_is_inj)

lemma inv_rsuml [simp]: "inv_into UNIV rsuml = lsumr"
  by(rule inj_imp_inv_eq) auto

lemma inv_lsumr [simp]: "inv_into UNIV lsumr = rsuml"
  by(rule inj_imp_inv_eq) auto

lemma lassocr_swap_sum_inverse [simp]: "lassocr_swap_sum (lassocr_swap_sum x) = x"
  by(simp add: lassocr_swap_sum_def sum.map_comp o_def id_def[symmetric] sum.map_id)

lemma inv_lassocr_swap_sum [simp]: "inv_into UNIV lassocr_swap_sum = lassocr_swap_sum"
  by(rule inj_imp_inv_eq)(simp_all add: sum.map_comp sum.inj_map bij_def surj_iff sum.map_id)

lemma swap_inverse: "swap⇩C ⊙ swap⇩C = 1⇩C"
  unfolding swap⇩C_def
  apply(simp add: comp_converter_map1_out comp_converter_map_converter2 comp_converter_id_right)
  apply(subst map_converter_id_move_right)
  apply(simp add: o_def id_def[symmetric])
  done

lemma swap_lassocr_inverse: "ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3), ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3) ⊢⇩C swap_lassocr ⊙ swap_lassocr ∼ 1⇩C"
  (is "?ℐ,_ ⊢⇩C ?lhs ∼ _")
proof -
  have "?lhs = (rassocl⇩C ⊙ (swap⇩C |⇩= 1⇩C)) ⊙ (lassocr⇩C ⊙ rassocl⇩C) ⊙ ((swap⇩C |⇩= 1⇩C) ⊙ lassocr⇩C)"
    by(simp add: swap_lassocr_def comp_converter_assoc)
  also have "… = rassocl⇩C ⊙ ((swap⇩C ⊙ swap⇩C) |⇩= 1⇩C) ⊙ lassocr⇩C"
    unfolding rassocl_inverse comp_converter_id_left
    by(simp add: parallel_converter2_comp1_out comp_converter_assoc)
  also have "?ℐ,?ℐ ⊢⇩C … ∼ rassocl⇩C ⊙ 1⇩C ⊙ lassocr⇩C" unfolding swap_inverse
    by(rule eq_ℐ_converter_reflI eq_ℐ_comp_cong WT_intro parallel_converter2_id_id)+
  also have "rassocl⇩C ⊙ 1⇩C ⊙ lassocr⇩C = 1⇩C" by(simp add: comp_converter_id_left lassocr_inverse)
  finally show ?thesis .
qed

lemma parallel_wiring_inverse:
  "(ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ (ℐ3 ⊕⇩ℐ ℐ4),(ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ (ℐ3 ⊕⇩ℐ ℐ4) ⊢⇩C parallel_wiring ⊙ parallel_wiring ∼ 1⇩C"
  (is "?ℐ, _ ⊢⇩C ?lhs ∼ _")
proof -
  have "?lhs = (lassocr⇩C ⊙ (1⇩C |⇩= swap_lassocr)) ⊙ (rassocl⇩C ⊙ lassocr⇩C) ⊙ ((1⇩C |⇩= swap_lassocr) ⊙ rassocl⇩C)"
    by(simp add: parallel_wiring_def comp_converter_assoc)
  also have "… = (lassocr⇩C ⊙ (1⇩C |⇩= swap_lassocr)) ⊙ (1⇩C |⇩= swap_lassocr) ⊙ rassocl⇩C"
    by(simp add: lassocr_inverse comp_converter_id_left)
  also have "… = lassocr⇩C ⊙ (1⇩C |⇩= (swap_lassocr ⊙ swap_lassocr)) ⊙ rassocl⇩C"
    by(simp add: parallel_converter2_comp2_out comp_converter_assoc)
  also have "?ℐ,?ℐ ⊢⇩C … ∼ lassocr⇩C ⊙ (1⇩C |⇩= 1⇩C) ⊙ rassocl⇩C"
    by(rule eq_ℐ_converter_reflI eq_ℐ_comp_cong parallel_converter2_eq_ℐ_cong WT_intro swap_lassocr_inverse)+
  also have "?ℐ,?ℐ ⊢⇩C lassocr⇩C ⊙ (1⇩C |⇩= 1⇩C) ⊙ rassocl⇩C ∼ lassocr⇩C ⊙ 1⇩C ⊙ rassocl⇩C"
    by(rule eq_ℐ_converter_reflI eq_ℐ_comp_cong parallel_converter2_id_id WT_intro)+
  also have "lassocr⇩C ⊙ 1⇩C ⊙ rassocl⇩C = 1⇩C" by(simp add: comp_converter_id_left rassocl_inverse)
  finally show ?thesis .
qed

― ‹ Analogous to @{term ‹attach_wiring›} in Wiring.thy›
definition 
  attach_wiring_right :: "
    ('a, 'b, 'c, 'd) wiring ⇒ 
      ('s ⇒ 'e ⇒ ('f × 's, 'a, 'b) gpv) ⇒ ('s ⇒ 'e ⇒ ('f × 's, 'c, 'd) gpv)"
  where 
    "attach_wiring_right = (λ(f, g). map_fun id (map_fun id (map_gpv' id f g)))"

lemma 
  attach_wiring_right_simps: 
    "attach_wiring_right (f, g) = map_fun id (map_fun id (map_gpv' id f g))"
  by(simp add: attach_wiring_right_def)

lemma 
  comp_converter_of_callee_wiring:
  assumes wiring: "wiring ℐ2 ℐ3 conv w"
      and WT: "ℐ1, ℐ2 ⊢⇩C CNV callee s √"
  shows "ℐ1, ℐ3 ⊢⇩C CNV callee s ⊙ conv ∼ CNV (attach_wiring_right w callee) s"
  using wiring
proof cases
  case (wiring f g)
  from _ wiring(2) have "ℐ1,ℐ3 ⊢⇩C CNV callee s ⊙ conv ∼ CNV callee s ⊙ map_converter id id f g 1⇩C"
    by(rule eq_ℐ_comp_cong)(rule eq_ℐ_converter_reflI[OF WT])
  also have "CNV callee s ⊙ map_converter id id f g 1⇩C = map_converter id id f g (CNV callee s)"
    by(subst comp_converter_map_converter2)(simp add: comp_converter_id_right)
  also have "… = CNV (attach_wiring_right w callee) s"
    by(simp add: map_converter_of_callee attach_wiring_right_simps wiring(1) prod.map_id0)
  finally show ?thesis .
qed

lemma attach_wiring_right_comp_wiring:
  "attach_wiring_right (w1 ∘⇩w w2) callee = attach_wiring_right w2 (attach_wiring_right w1 callee)"
  by(simp add: attach_wiring_right_def comp_wiring_def split_def map_fun_def o_def map_gpv'_comp id_def fun_eq_iff)

lemma attach_wiring_comp_wiring:
  "attach_wiring (w1 ∘⇩w w2) callee = attach_wiring w1 (attach_wiring w2 callee)"
  unfolding attach_wiring_def comp_wiring_def
  by (simp add: split_def map_fun_def o_def map_gpv_conv_map_gpv' map_gpv'_comp id_def map_prod_def)




subsection ‹Probabilistic finite converter›

coinductive pfinite_converter :: "('a, 'b) ℐ ⇒ ('c, 'd) ℐ ⇒ ('a, 'b, 'c, 'd) converter ⇒ bool" 
  for ℐ ℐ' where
  pfinite_converterI: "pfinite_converter ℐ ℐ' conv" if 
  "⋀a. a ∈ outs_ℐ ℐ ⟹ pfinite_gpv ℐ' (run_converter conv a)"
  "⋀a b conv'. ⟦ a ∈ outs_ℐ ℐ; (b, conv') ∈ results_gpv ℐ' (run_converter conv a) ⟧ ⟹ pfinite_converter ℐ ℐ' conv'"

lemma pfinite_converter_coinduct[consumes 1, case_names pfinite_converter, case_conclusion pfinite_converter pfinite step, coinduct pred: pfinite_converter]:
  assumes "X conv"
    and step: "⋀conv a. ⟦ X conv; a ∈ outs_ℐ ℐ ⟧ ⟹ pfinite_gpv ℐ' (run_converter conv a) ∧
     (∀(b, conv') ∈ results_gpv ℐ' (run_converter conv a). X conv' ∨ pfinite_converter ℐ ℐ' conv')"
  shows "pfinite_converter ℐ ℐ' conv"
  using assms(1) by(rule pfinite_converter.coinduct)(auto dest: step)

lemma pfinite_converterD:
  "⟦ pfinite_converter ℐ ℐ' conv; a ∈ outs_ℐ ℐ ⟧ 
  ⟹ pfinite_gpv ℐ' (run_converter conv a) ∧
     (∀(b, conv') ∈ results_gpv ℐ' (run_converter conv a). pfinite_converter ℐ ℐ' conv')"
  by(auto elim: pfinite_converter.cases)

lemma pfinite_converter_bot1 [simp]: "pfinite_converter bot ℐ conv"
  by(rule pfinite_converterI) auto

lemma pfinite_converter_mono:
  assumes *: "pfinite_converter ℐ1 ℐ2 conv"
    and le: "outs_ℐ ℐ1' ⊆ outs_ℐ ℐ1" "ℐ2 ≤ ℐ2'"
    and WT: "ℐ1, ℐ2 ⊢⇩C conv √"
  shows "pfinite_converter ℐ1' ℐ2' conv"
  using * WT
  apply(coinduction arbitrary: conv)
  apply(drule pfinite_converterD)
   apply(erule le(1)[THEN subsetD])
  apply(drule WT_converterD')
   apply(erule le(1)[THEN subsetD])
  using le(2)[THEN responses_ℐ_mono]
  by(auto intro: pfinite_gpv_mono[OF _ le(2)] results_gpv_mono[OF le(2), THEN subsetD] dest: bspec)

context raw_converter_invariant begin
lemma pfinite_converter_of_callee:
  assumes step: "⋀x s. ⟦ x ∈ outs_ℐ ℐ; I s ⟧ ⟹ pfinite_gpv ℐ' (callee s x)"
    and I: "I s"
  shows "pfinite_converter ℐ ℐ' (converter_of_callee callee s)"
  using I
  by(coinduction arbitrary: s)(auto 4 3 simp add: step dest: results_callee)
end

lemma raw_converter_invariant_run_pfinite_converter: 
  "raw_converter_invariant ℐ ℐ' run_converter (λconv. pfinite_converter ℐ ℐ' conv ∧ ℐ,ℐ' ⊢⇩C conv √)"
  by(unfold_locales)(auto dest: WT_converterD pfinite_converterD)

interpretation run_pfinite_converter: raw_converter_invariant
  ℐ ℐ' run_converter "λconv. pfinite_converter ℐ ℐ' conv ∧ ℐ,ℐ' ⊢⇩C conv √" for ℐ ℐ'
  by(rule raw_converter_invariant_run_pfinite_converter)

named_theorems pfinite_intro "Introduction rules for probabilistic finiteness"

lemma pfinite_id_converter [pfinite_intro]: "pfinite_converter ℐ ℐ id_converter"
  by(coinduction) simp

lemma pfinite_fail_converter [pfinite_intro]: "pfinite_converter ℐ ℐ' fail_converter"
  by coinduction simp

lemma pfinite_parallel_converter2 [pfinite_intro]:
  "pfinite_converter (ℐ1 ⊕⇩ℐ ℐ2) (ℐ1' ⊕⇩ℐ ℐ2') (conv1 |⇩= conv2)"
  if "pfinite_converter ℐ1 ℐ1' conv1" "pfinite_converter ℐ2 ℐ2' conv2"
  using that by(coinduction arbitrary: conv1 conv2)(fastforce dest: pfinite_converterD)

context raw_converter_invariant begin

lemma expectation_gpv_1_le_inline:
  defines "expectation_gpv2 ≡ expectation_gpv 1 ℐ'"
  assumes callee: "⋀s x. ⟦ x ∈ outs_ℐ ℐ; I s ⟧ ⟹ pfinite_gpv ℐ' (callee s x)"
    and WT_gpv: "ℐ ⊢g gpv √"
    and I: "I s"
    and f_le_1: "⋀x. f x ≤ 1"
  shows "expectation_gpv 1 ℐ f gpv ≤ expectation_gpv2 (λ(x, s). f x) (inline callee gpv s)"
  using WT_gpv I
proof(induction arbitrary: gpv s rule: expectation_gpv_fixp_induct)
  case adm show ?case by simp
  case bottom show ?case by simp
  case (step expectation_gpv')
  have "(∫⇧+ x. (case x of Pure a ⇒ f a | IO out c ⇒ ⨅r∈responses_ℐ ℐ out. expectation_gpv' (c r)) ∂measure_spmf (the_gpv gpv)) + 1 * ennreal (pmf (the_gpv gpv) None) = 
    (∑⇧+ x. pmf (the_gpv gpv) x * (case x of Some (Pure a) ⇒ f a | Some (IO out c) ⇒ ⨅r∈responses_ℐ ℐ out. expectation_gpv' (c r) | None ⇒ 1))"
    apply(simp add: nn_integral_measure_spmf_conv_measure_pmf nn_integral_restrict_space nn_integral_measure_pmf)
    apply(subst (2) nn_integral_disjoint_pair_countspace[where B="range Some" and C="{None}", simplified, folded UNIV_option_conv, simplified])
    apply(auto simp add: mult.commute intro!: nn_integral_cong split: split_indicator)
    done
  also have "… ≤ (∑⇧+ x. pmf (the_gpv gpv) x * (case x of None ⇒ 1 | Some (Pure a) ⇒ f a | Some (IO out c) ⇒ 
          (∑⇧+ x. ennreal (pmf (the_gpv (callee s out) ⤜ case_generat (λ(x, y). inline1 callee (c x) y) (λout rpv'. return_spmf (Inr (out, rpv', c)))) x) *
            (case x of None ⇒ 1 | Some (Inl (a, s)) ⇒ f a
             | Some (Inr (r, rpv, rpv')) ⇒ ⨅x∈responses_ℐ ℐ' r. expectation_gpv 1 ℐ' (λ(x, s'). expectation_gpv 1 ℐ' (λ(x, s). f x) (inline callee (rpv' x) s')) (rpv x)))))"
    (is "nn_integral _ ?lhs ≤ nn_integral _ ?rhs")
  proof(rule nn_integral_mono)
    fix x :: "('a, 'call, ('a, 'call, 'ret) rpv) generat option"
    consider (None) "x = None" | (Pure) a where "x = Some (Pure a)" 
      | (IO) out c where "x = Some (IO out c)" "IO out c ∈ set_spmf (the_gpv gpv)"
      | (outside) out c where "x = Some (IO out c)" "IO out c ∉ set_spmf (the_gpv gpv)"
      by (metis dest_IO.elims not_None_eq)
    then show "?lhs x ≤ ?rhs x"
    proof cases
      case None then show ?thesis by simp
    next
      case Pure then show ?thesis by simp
    next
      case (IO out c)
      with step.prems have out: "out ∈ outs_ℐ ℐ" by(auto dest: WT_gpvD)
      then obtain response where resp: "response ∈ responses_ℐ ℐ out" unfolding in_outs_ℐ_iff_responses_ℐ by blast
      with out step.prems IO have WT_resp [WT_intro]: "ℐ ⊢g c response √" by(auto dest: WT_gpvD)
      have exp_resp: "expectation_gpv' (c response) ≤ 1"
        using step.hyps[of "c response"] expectation_gpv_mono[of 1 1 f "λ_. 1" ℐ "c response"] expectation_gpv_const_le[OF WT_resp, of 1 1]
        by(simp add: le_fun_def f_le_1)

      have "(⨅r∈responses_ℐ ℐ out. expectation_gpv' (c r)) = 
        (∫⇧+ generat. (⨅r∈responses_ℐ ℐ out. expectation_gpv' (c r)) ∂measure_spmf (the_gpv (callee s out))) +
        (⨅r∈responses_ℐ ℐ out. expectation_gpv' (c r)) * (1 - ennreal (weight_spmf (the_gpv (callee s out))))"
        by(simp add: measure_spmf.emeasure_eq_measure add_mult_distrib2[symmetric] semiring_class.distrib_left[symmetric] add_diff_inverse_ennreal weight_spmf_le_1)
      also have "… ≤ (∫⇧+ generat. (⨅r∈responses_ℐ ℐ out. expectation_gpv' (c r)) ∂measure_spmf (the_gpv (callee s out))) +
        1 * ennreal (pmf (the_gpv (callee s out)) None)" unfolding pmf_None_eq_weight_spmf
        by(intro add_mono mult_mono order_refl INF_lower2[OF resp])(auto simp add: ennreal_minus[symmetric] weight_spmf_le_1 exp_resp)
      also have "… = (∑⇧+ z. ennreal (pmf (the_gpv (callee s out)) z) * (case z of None ⇒ 1 | Some generat ⇒ (⨅r∈responses_ℐ ℐ out. expectation_gpv' (c r))))"
        apply(simp add: nn_integral_measure_spmf_conv_measure_pmf nn_integral_restrict_space nn_integral_measure_pmf del: nn_integral_const)
        apply(subst (2) nn_integral_disjoint_pair_countspace[where B="range Some" and C="{None}", simplified, folded UNIV_option_conv, simplified])
        apply(auto simp add: mult.commute intro!: nn_integral_cong split: split_indicator)
        done
      also have "… ≤ (∑⇧+ z. ennreal (pmf (the_gpv (callee s out)) z) *
         (case z of None ⇒ 1 | Some (IO out' rpv') ⇒ ⨅x∈responses_ℐ ℐ' out'. expectation_gpv 1 ℐ' (λ(x, s'). expectation_gpv 1 ℐ' (λ(x, s). f x) (inline callee (c x) s')) (rpv' x)
          | Some (Pure (r, s')) ⇒ (∑⇧+ x. ennreal (pmf (inline1 callee (c r) s') x) * (case x of None ⇒ 1 | Some (Inl (a, s)) ⇒ f a | Some (Inr (out', rpv, rpv')) ⇒
                  ⨅x∈responses_ℐ ℐ' out'. expectation_gpv 1 ℐ' (λ(x, s'). expectation_gpv 1 ℐ' (λ(x, s). f x) (inline callee (rpv' x) s')) (rpv x)))))"
         (is "nn_integral _ ?lhs2 ≤ nn_integral _ ?rhs2")
      proof(intro nn_integral_mono)
        fix z :: "('ret × 's, 'call', ('ret × 's, 'call', 'ret') rpv) generat option"
        consider (None) "z = None" | (Pure) x' s' where "z = Some (Pure (x', s'))" "Pure (x', s') ∈ set_spmf (the_gpv (callee s out))"
          | (IO') out' c' where "z = Some (IO out' c')" "IO out' c' ∈ set_spmf (the_gpv (callee s out))"
          | (outside) generat where "z = Some generat" "generat ∉ set_spmf (the_gpv (callee s out))"
          by (metis dest_IO.elims not_Some_eq old.prod.exhaust)
        then show "?lhs2 z ≤ ?rhs2 z"
        proof cases
          case None then show ?thesis by simp
        next
          case Pure
          hence "(x', s') ∈ results_gpv ℐ' (callee s out)" by(simp add: results_gpv.Pure)
          with results_callee step.prems out have x: "x' ∈ responses_ℐ ℐ out" and s': "I s'" by auto
          with IO out step.prems have WT_c [WT_intro]: "ℐ ⊢g c x' √" by(auto dest: WT_gpvD)
          from x have "(INF r∈responses_ℐ ℐ out. expectation_gpv' (c r)) ≤ expectation_gpv' (c x')" by(rule INF_lower)
          also have "… ≤ expectation_gpv2 (λ(x, s). f x) (inline callee (c x') s')" using WT_c s' by(rule step.IH)
          also have "… = ∫⇧+ xx. (case xx of Inl (x, _) ⇒ f x 
               | Inr (out', callee', rpv) ⇒ INF r'∈responses_ℐ ℐ' out'. expectation_gpv 1 ℐ' (λ(r, s'). expectation_gpv 1 ℐ' (λ(x, s). f x) (inline callee (rpv r) s')) (callee' r'))
            ∂measure_spmf (inline1 callee (c x') s') + ennreal (pmf (the_gpv (inline callee (c x') s')) None)"
            unfolding expectation_gpv2_def
            by(subst expectation_gpv.simps)(auto simp add: inline_sel split_def o_def intro!: nn_integral_cong split: generat.split sum.split)
          also have "… = (∑⇧+ xx. ennreal (pmf (inline1 callee (c x') s') xx) * (case xx of None ⇒ 1 | Some (Inl (x, _)) ⇒ f x 
            | Some (Inr (out', callee', rpv)) ⇒ INF r'∈responses_ℐ ℐ' out'. expectation_gpv 1 ℐ' (λ(r, s'). expectation_gpv 1 ℐ' (λ(x, s). f x) (inline callee (rpv r) s')) (callee' r')))"
            apply(subst inline_sel)
            apply(simp add: nn_integral_measure_spmf_conv_measure_pmf nn_integral_restrict_space nn_integral_measure_pmf pmf_map_spmf_None del: nn_integral_const)
            apply(subst (2) nn_integral_disjoint_pair_countspace[where B="range Some" and C="{None}", simplified, folded UNIV_option_conv, simplified])
            apply(auto simp add: mult.commute intro!: nn_integral_cong split: split_indicator)
            done
          finally show ?thesis using Pure by(simp add: mult_mono)
        next
          case IO'
          then have out': "out' ∈ outs_ℐ ℐ'" using WT_callee out step.prems by(auto dest: WT_gpvD)
          have "(INF r∈responses_ℐ ℐ out. expectation_gpv' (c r)) ≤ min (INF (r, s')∈(⋃r'∈responses_ℐ ℐ' out'. results_gpv ℐ' (c' r')). expectation_gpv' (c r)) 1"
            using IO' results_callee[OF out, of s] step.prems by(intro INF_mono min.boundedI)(auto intro: results_gpv.IO intro!: INF_lower2[OF resp] exp_resp)
          also have "… ≤ (INF r'∈responses_ℐ ℐ' out'. min (INF (r, s')∈results_gpv ℐ' (c' r'). expectation_gpv' (c r)) 1)"
            using resp out' unfolding inf_min[symmetric] in_outs_ℐ_iff_responses_ℐ
            by(subst INF_inf_const2)(auto simp add: INF_UNION)
          also have "… ≤ (INF r'∈responses_ℐ ℐ' out'. expectation_gpv 1 ℐ' (λ(r', s'). expectation_gpv 1 ℐ' (λ(x, s). f x) (inline callee (c r') s')) (c' r'))"
            (is "_ ≤ (INF r'∈_. ?r r')")
          proof(rule INF_mono, rule bexI)
            fix r'
            assume r': "r' ∈ responses_ℐ ℐ' out'"
            have fin: "pfinite_gpv ℐ' (c' r')" using callee[OF out, of s] IO' r' WT_callee[OF out, of s] step.prems by(auto dest: pfinite_gpv_ContD)
            have "min (INF (r, s')∈results_gpv ℐ' (c' r'). expectation_gpv' (c r)) 1 ≤ min (INF (r, s')∈results_gpv ℐ' (c' r'). expectation_gpv2 (λ(x, s). f x) (inline callee (c r) s')) 1"
              using IO IO' step.prems out results_callee[OF out, of s] r'
              by(intro min.mono)(auto intro!: INF_mono rev_bexI step.IH dest: WT_gpv_ContD intro: results_gpv.IO)
            also have "… ≤ ?r r'" unfolding expectation_gpv2_def using fin by(rule pfinite_INF_le_expectation_gpv)
            finally show "min (INF (r, s')∈results_gpv ℐ' (c' r'). expectation_gpv' (c r)) 1 ≤ …" .
          qed
          finally show ?thesis using IO' by(simp add: mult_mono)
        next
          case outside then show ?thesis by(simp add: in_set_spmf_iff_spmf)
        qed
      qed
      also have "… = (∑⇧+ z. ∑⇧+ x.
             ennreal (pmf (the_gpv (callee s out)) z) *
             ennreal (pmf (case z of None ⇒ return_pmf None | Some (Pure (x, xb)) ⇒ inline1 callee (c x) xb | Some (IO out rpv') ⇒ return_spmf (Inr (out, rpv', c))) x) *
             (case x of None ⇒ 1 | Some (Inl (a, s)) ⇒ f a | Some (Inr (out, rpv, rpv')) ⇒ ⨅x∈responses_ℐ ℐ' out.
                expectation_gpv 1 ℐ' (λ(x, s'). expectation_gpv 1 ℐ' (λ(x, s). f x) (inline callee (rpv' x) s')) (rpv x)))"
        (is "… = (∑⇧+ z. ∑⇧+ x. ?f x z)")
        by(auto intro!: nn_integral_cong split!: option.split generat.split simp add: mult.assoc nn_integral_cmult ennreal_indicator)
      also have "(∑⇧+ z. ∑⇧+ x. ?f x z) = (∑⇧+ x. ∑⇧+ z. ?f x z)"
        by(subst nn_integral_fst_count_space[where f="case_prod _", simplified])(simp add: nn_integral_snd_count_space[symmetric])
      also have "… = (∑⇧+ x.
              ennreal (pmf (the_gpv (callee s out) ⤜ case_generat (λ(x, y). inline1 callee (c x) y) (λout rpv'. return_spmf (Inr (out, rpv', c)))) x) *
              (case x of None ⇒ 1 | Some (Inl (a, s)) ⇒ f a | Some (Inr (r, rpv, rpv')) ⇒
                   ⨅x∈responses_ℐ ℐ' r. expectation_gpv 1 ℐ' (λ(x, s'). expectation_gpv 1 ℐ' (λ(x, s). f x) (inline callee (rpv' x) s')) (rpv x)))"
        by(simp add: bind_spmf_def ennreal_pmf_bind nn_integral_multc[symmetric] nn_integral_measure_pmf)
      finally show ?thesis using IO by(auto intro!: mult_mono)
    next
      case outside then show ?thesis by(simp add: in_set_spmf_iff_spmf)
    qed
  qed
  also have "… = (∑⇧+ y. ∑⇧+ x.
         ennreal (pmf (the_gpv gpv) y) *
         ennreal (case y of None ⇒ pmf (return_pmf None) x | Some (Pure xa) ⇒ pmf (return_spmf (Inl (xa, s))) x
                | Some (IO out rpv) ⇒
                    pmf (bind_spmf (the_gpv (callee s out)) (λgenerat' ⇒ case generat' of Pure (x, y) ⇒ inline1 callee (rpv x) y | IO out rpv' ⇒ return_spmf (Inr (out, rpv', rpv)))) x) *
         (case x of None ⇒ 1 | Some (Inl (a, s)) ⇒ f a 
         | Some (Inr (out, rpv, rpv')) ⇒ ⨅x∈responses_ℐ ℐ' out. expectation_gpv 1 ℐ' (λ(x, s'). expectation_gpv 1 ℐ' (λ(x, s). f x) (inline callee (rpv' x) s')) (rpv x)))"
    (is "_ = (∑⇧+ y. ∑⇧+ x. ?f x y)")
    by(auto intro!: nn_integral_cong split!: option.split generat.split simp add: nn_integral_cmult mult.assoc ennreal_indicator)
  also have "(∑⇧+ y. ∑⇧+ x. ?f x y) = (∑⇧+ x. ∑⇧+ y. ?f x y)"
    by(subst nn_integral_fst_count_space[where f="case_prod _", simplified])(simp add: nn_integral_snd_count_space[symmetric])
  also have "… = (∑⇧+ x. (pmf (inline1 callee gpv s) x) * (case x of None ⇒ 1 | Some (Inl (a, s)) ⇒ f a |
        Some (Inr (out, rpv, rpv')) ⇒ ⨅x∈responses_ℐ ℐ' out. expectation_gpv 1 ℐ' (λ(x, s'). expectation_gpv 1 ℐ' (λ(x, s). f x) (inline callee (rpv' x) s')) (rpv x)))"
    by(rewrite in "_ = ⌑" inline1.simps)
      (auto simp add: bind_spmf_def ennreal_pmf_bind nn_integral_multc[symmetric] nn_integral_measure_pmf intro!: nn_integral_cong split: option.split generat.split)
  also have "… = (∫⇧+ res. (case res of Inl (a, s) ⇒ f a
            | Inr (out, rpv, rpv') ⇒ ⨅x∈responses_ℐ ℐ' out. expectation_gpv 1 ℐ' (λ(x, s'). expectation_gpv 1 ℐ' (λ(x, s). f x) (inline callee (rpv' x) s')) (rpv x))
       ∂measure_spmf (inline1 callee gpv s) +
    ennreal (pmf (inline1 callee gpv s) None))"
    apply(simp add: nn_integral_measure_spmf_conv_measure_pmf nn_integral_restrict_space nn_integral_measure_pmf)
    apply(subst nn_integral_disjoint_pair_countspace[where B="range Some" and C="{None}", simplified, folded UNIV_option_conv, simplified])
    apply(auto simp add: mult.commute intro!: nn_integral_cong split: split_indicator)
    done
  also have "… = expectation_gpv2 (λ(x, s). f x) (inline callee gpv s)" unfolding expectation_gpv2_def
    by(rewrite in "_ = ⌑" expectation_gpv.simps, subst (1 2) inline_sel)
      (simp add: o_def pmf_map_spmf_None sum.case_distrib[where h="case_generat _ _"] split_def cong: sum.case_cong)
  finally show ?case .
qed

lemma pfinite_inline:
  assumes fin: "pfinite_gpv ℐ gpv"
    and WT: "ℐ ⊢g gpv √"
    and callee: "⋀s x. ⟦ x ∈ outs_ℐ ℐ; I s ⟧ ⟹ pfinite_gpv ℐ' (callee s x)"
    and I: "I s"
  shows "pfinite_gpv ℐ' (inline callee gpv s)"
unfolding pgen_lossless_gpv_def
proof(rule antisym)
  have WT': "ℐ' ⊢g inline callee gpv s √" using WT I by(rule WT_gpv_inline_invar)
  from expectation_gpv_const_le[OF WT', of 1 1]
  show "expectation_gpv 1 ℐ' (λ_. 1) (inline callee gpv s) ≤ 1" by(simp add: max_def)

  have "1 = expectation_gpv 1 ℐ (λ_. 1) gpv" using fin by(simp add: pgen_lossless_gpv_def)
  also have "… ≤ expectation_gpv 1 ℐ' (λ_. 1) (inline callee gpv s)"
    by(rule expectation_gpv_1_le_inline[unfolded split_def]; rule callee I WT WT_callee order_refl)
  finally show "1 ≤ …" .
qed

end

lemma pfinite_comp_converter [pfinite_intro]:
  "pfinite_converter ℐ1 ℐ3 (conv1 ⊙ conv2)"
  if "pfinite_converter ℐ1 ℐ2 conv1" "pfinite_converter ℐ2 ℐ3 conv2" "ℐ1,ℐ2 ⊢⇩C conv1 √" "ℐ2,ℐ3 ⊢⇩C conv2 √"
  using that 
proof(coinduction arbitrary: conv1 conv2)
  case pfinite_converter
  have conv1: "pfinite_gpv ℐ2 (run_converter conv1 a)" 
    using pfinite_converter(1, 5) by(simp add: pfinite_converterD)
  have conv2: "ℐ2 ⊢g run_converter conv1 a √"
    using pfinite_converter(3, 5) by(simp add: WT_converterD)
  have ?pfinite using pfinite_converter(2,4,5)
    by(auto intro!:run_pfinite_converter.pfinite_inline[OF conv1] dest: pfinite_converterD intro: conv2)
  moreover have ?step (is "∀(b, conv')∈?res. ?P b conv' ∨ _")
  proof(clarify)
    fix b conv''
    assume "(b, conv'') ∈ ?res"
    then obtain conv1' conv2' where [simp]: "conv'' = comp_converter conv1' conv2'" 
      and inline: "((b, conv1'), conv2') ∈ results_gpv ℐ3 (inline run_converter (run_converter conv1 a) conv2)" 
      by auto
    from run_pfinite_converter.results_gpv_inline[OF inline conv2] pfinite_converter(2,4)
    have run: "(b, conv1') ∈ results_gpv ℐ2 (run_converter conv1 a)"
      and *: "pfinite_converter ℐ2 ℐ3 conv2'" "ℐ2, ℐ3 ⊢⇩C conv2' √" by auto
    with WT_converterD(2)[OF pfinite_converter(3,5) run] pfinite_converterD[THEN conjunct2, rule_format, OF pfinite_converter(1,5) run]
    show "?P b conv''" by auto
  qed
  ultimately show ?case ..
qed

lemma pfinite_map_converter [pfinite_intro]:
  "pfinite_converter ℐ  ℐ' (map_converter f g f' g' conv)" if 
  *: "pfinite_converter (map_ℐ (inv_into UNIV f) (inv_into UNIV g) ℐ) (map_ℐ f' g' ℐ') conv"
  and f: "inj f" and g: "surj g"
  using *
proof(coinduction arbitrary: conv)
  case (pfinite_converter a conv)
  with f have a: "inv_into UNIV f (f a) ∈ outs_ℐ ℐ" by simp
  with pfinite_converterD[OF ‹pfinite_converter _ _ conv›, of "f a"] have "?pfinite" by simp
  moreover have ?step
  proof(safe)
    fix r conv'
    assume "(r, conv') ∈ results_gpv ℐ' (run_converter (map_converter f g f' g' conv) a)"
    then obtain r' conv''
      where results: "(r', conv'') ∈ results_gpv (map_ℐ f' g' ℐ') (run_converter conv (f a))"
        and r: "r = g r'"
        and conv': "conv' = map_converter f g f' g' conv''"
      by auto
    from pfinite_converterD[OF ‹pfinite_converter _ _ conv›, THEN conjunct2, rule_format, OF _ results] a r conv'
    show "∃conv. conv' = map_converter f g f' g' conv ∧
              pfinite_converter (map_ℐ (inv_into UNIV f) (inv_into UNIV g) ℐ) (map_ℐ f' g' ℐ') conv"
      by auto
  qed
  ultimately show ?case ..
qed

lemma pfinite_lassocr⇩C [pfinite_intro]: "pfinite_converter ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3) (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) lassocr⇩C"
  by(coinduction)(auto simp add: lassocr⇩C_def)

lemma pfinite_rassocl⇩C [pfinite_intro]: "pfinite_converter (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3) rassocl⇩C"
  by(coinduction)(auto simp add: rassocl⇩C_def)

lemma pfinite_swap⇩C [pfinite_intro]: "pfinite_converter (ℐ1 ⊕⇩ℐ ℐ2) (ℐ2 ⊕⇩ℐ ℐ1) swap⇩C"
  by(coinduction)(auto simp add: swap⇩C_def)

lemma pfinite_swap_lassocr [pfinite_intro]: "pfinite_converter (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) (ℐ2 ⊕⇩ℐ (ℐ1 ⊕⇩ℐ ℐ3)) swap_lassocr"
  unfolding swap_lassocr_def by(rule pfinite_intro WT_intro)+

lemma pfinite_swap_rassocl [pfinite_intro]: "pfinite_converter ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3) ((ℐ1 ⊕⇩ℐ ℐ3) ⊕⇩ℐ ℐ2) swap_rassocl"
  unfolding swap_rassocl_def by(rule pfinite_intro WT_intro)+

lemma pfinite_parallel_wiring [pfinite_intro]:
  "pfinite_converter ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ (ℐ3 ⊕⇩ℐ ℐ4)) ((ℐ1 ⊕⇩ℐ ℐ3) ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ4)) parallel_wiring"
  unfolding parallel_wiring_def by(rule pfinite_intro WT_intro)+

lemma pfinite_parallel_converter [pfinite_intro]:
  "pfinite_converter (ℐ1 ⊕⇩ℐ ℐ2) ℐ3 (conv1 |⇩∝ conv2)"
  if "pfinite_converter ℐ1 ℐ3 conv1" and "pfinite_converter ℐ2 ℐ3 conv2"
  using that by(coinduction arbitrary: conv1 conv2)(fastforce dest: pfinite_converterD)

lemma pfinite_converter_of_resource [simp, pfinite_intro]: "pfinite_converter ℐ1 ℐ2 (converter_of_resource res)"
  by(coinduction arbitrary: res) auto

subsection ‹colossless converter›

coinductive colossless_converter :: "('a, 'b) ℐ ⇒ ('c, 'd) ℐ ⇒ ('a, 'b, 'c, 'd) converter ⇒ bool"
  for ℐ ℐ' where
  colossless_converterI:
  "colossless_converter ℐ ℐ' conv" if 
    "⋀a. a ∈ outs_ℐ ℐ ⟹ colossless_gpv ℐ' (run_converter conv a)"
    "⋀a b conv'. ⟦ a ∈ outs_ℐ ℐ; (b, conv') ∈ results_gpv ℐ' (run_converter conv a) ⟧ ⟹ colossless_converter ℐ ℐ' conv'"

lemma colossless_converter_coinduct[consumes 1, case_names colossless_converter, case_conclusion colossless_converter plossless step, coinduct pred: colossless_converter]:
  assumes "X conv"
    and step: "⋀conv a. ⟦ X conv; a ∈ outs_ℐ ℐ ⟧ ⟹ colossless_gpv ℐ' (run_converter conv a) ∧
     (∀(b, conv') ∈ results_gpv ℐ' (run_converter conv a). X conv' ∨ colossless_converter ℐ ℐ' conv')"
  shows "colossless_converter ℐ ℐ' conv"
  using assms(1) by(rule colossless_converter.coinduct)(auto dest: step)

lemma colossless_converterD:
  "⟦ colossless_converter ℐ ℐ' conv; a ∈ outs_ℐ ℐ ⟧ 
  ⟹ colossless_gpv ℐ' (run_converter conv a) ∧
     (∀(b, conv') ∈ results_gpv ℐ' (run_converter conv a). colossless_converter ℐ ℐ' conv')"
  by(auto elim: colossless_converter.cases)

lemma colossless_converter_bot1 [simp]: "colossless_converter bot ℐ conv"
  by(rule colossless_converterI) auto

lemma raw_converter_invariant_run_colossless_converter: "raw_converter_invariant ℐ ℐ' run_converter (λconv. colossless_converter ℐ ℐ' conv ∧ ℐ,ℐ' ⊢⇩C conv √)"
  by(unfold_locales)(auto dest: WT_converterD colossless_converterD)

interpretation run_colossless_converter: raw_converter_invariant
  ℐ ℐ' run_converter "λconv. colossless_converter ℐ ℐ' conv ∧ ℐ,ℐ' ⊢⇩C conv √" for ℐ ℐ'
  by(rule raw_converter_invariant_run_colossless_converter)

lemma colossless_const_converter [simp]: "colossless_converter ℐ ℐ' (const_converter x)"
  by(coinduction)(auto)

subsection ‹trace equivalence›

lemma distinguish_trace_eq: (* generalized from Distinguisher.thy *)
  assumes distinguish: "⋀distinguisher. ℐ ⊢g distinguisher √ ⟹ connect distinguisher res = connect distinguisher res'"
  shows "outs_ℐ ℐ ⊢⇩R res ≈ res'"
  using assms by(rule distinguish_trace_eq)(auto intro: WT_fail_resource)

lemma attach_trace_eq':
  assumes eq: "outs_ℐ ℐ ⊢⇩R res1 ≈ res2"
    and WT1 [WT_intro]: "ℐ ⊢res res1 √"
    and WT2 [WT_intro]: "ℐ ⊢res res2 √"
    and WT_conv [WT_intro]: "ℐ',ℐ ⊢⇩C conv √"
  shows "outs_ℐ ℐ' ⊢⇩R conv ⊳ res1 ≈ conv ⊳ res2"
proof(rule distinguish_trace_eq)
  fix 𝒟 :: "('c, 'd) distinguisher"
  assume [WT_intro]: "ℐ' ⊢g 𝒟 √"
  have "connect (absorb 𝒟 conv) res1 = connect (absorb 𝒟 conv) res2" using eq 
    by(rule connect_cong_trace)(rule WT_intro | fold WT_gpv_iff_outs_gpv)+
  then show "connect 𝒟 (conv ⊳ res1) = connect 𝒟 (conv ⊳ res2)" by(simp add: distinguish_attach)
qed

lemma trace_callee_eq_trans [trans]:
  "⟦ trace_callee_eq callee1 callee2 A p q; trace_callee_eq callee2 callee3 A q r ⟧
   ⟹ trace_callee_eq callee1 callee3 A p r"
  by(simp add: trace_callee_eq_def)

lemma trace_eq'_parallel_resource:
  fixes res1 :: "('a, 'b) resource" and res2 :: "('c, 'd) resource"
  assumes 1: "trace_eq' A res1 res1'"
    and 2: "trace_eq' B res2 res2'"
  shows "trace_eq' (A <+> B) (res1 ∥ res2) (res1' ∥ res2')"
proof -
  let ?ℐ = "ℐ_uniform A (UNIV :: 'b set) ⊕⇩ℐ ℐ_uniform B (UNIV :: 'd set)"
  have "trace_eq' (outs_ℐ ?ℐ) (res1 ∥ res2) (res1' ∥ res2)"
    apply(subst (1 2) attach_converter_of_resource_conv_parallel_resource2[symmetric])
    apply(rule attach_trace_eq'[where ?ℐ = "ℐ_uniform A UNIV"]; auto simp add: 1 intro: WT_intro WT_resource_ℐ_uniform_UNIV)
    done
  also have "trace_eq' (outs_ℐ ?ℐ) (res1' ∥ res2) (res1' ∥ res2')"
    apply(subst (1 2) attach_converter_of_resource_conv_parallel_resource[symmetric])
    apply(rule attach_trace_eq'[where ?ℐ = "ℐ_uniform B UNIV"]; auto simp add: 2 intro: WT_intro WT_resource_ℐ_uniform_UNIV)
    done
  finally show ?thesis by simp
qed

proposition trace_callee_eq_coinduct [consumes 1, case_names step sim]: (* stronger version of trace'_eq_simI *)
  fixes callee1 :: "('a, 'b, 's1) callee" and callee2 :: "('a, 'b, 's2) callee"
  assumes start: "S p q"
    and step: "⋀p q a. ⟦ S p q; a ∈ A ⟧ ⟹
      bind_spmf p (λs. map_spmf fst (callee1 s a)) = bind_spmf q (λs. map_spmf fst (callee2 s a))"
    and sim: "⋀p q a res res' b s'' s'. ⟦ S p q; a ∈ A; res ∈ set_spmf p; (b, s'') ∈ set_spmf (callee1 res a); res' ∈ set_spmf q; (b, s') ∈ set_spmf (callee2 res' a) ⟧
      ⟹ S (cond_spmf_fst (bind_spmf p (λs. callee1 s a)) b)
            (cond_spmf_fst (bind_spmf q (λs. callee2 s a)) b)"
  shows "trace_callee_eq callee1 callee2 A p q"
proof(rule trace_callee_eqI)
  fix xs :: "('a × 'b) list" and z
  assume xs: "set xs ⊆ A × UNIV" and z: "z ∈ A"

  from start show "trace_callee callee1 p xs z = trace_callee callee2 q xs z" using xs
  proof(induction xs arbitrary: p q)
    case Nil
    then show ?case using z by(simp add: step)
  next
    case (Cons xy xs)
    obtain x y where xy [simp]: "xy = (x, y)" by(cases xy)
    have "trace_callee callee1 p (xy # xs) z = 
      trace_callee callee1 (cond_spmf_fst (bind_spmf p (λs. callee1 s x)) y) xs z"
      by(simp add: bind_map_spmf split_def o_def)
    also have "… = trace_callee callee2 (cond_spmf_fst (bind_spmf q (λs. callee2 s x)) y) xs z"
    proof(cases "∃s ∈ set_spmf q. ∃s'. (y, s') ∈ set_spmf (callee2 s x)")
      case True
      then obtain s s' where ss': "s ∈ set_spmf q" "(y, s') ∈ set_spmf (callee2 s x)" by blast
      from Cons have "x ∈ A" by simp
      from ss' step[THEN arg_cong[where f="set_spmf"], OF ‹S p q› this] obtain ss ss'
        where "ss ∈ set_spmf p" "(y, ss') ∈ set_spmf (callee1 ss x)" 
        by(clarsimp simp add: bind_UNION) force
      from sim[OF ‹S p q› _ this ss'] show ?thesis using Cons.prems by (auto intro: Cons.IH)
    next
      case False
      then have "cond_spmf_fst (bind_spmf q (λs. callee2 s x)) y = return_pmf None"
        by(auto simp add: bind_eq_return_pmf_None)
      moreover from step[OF ‹S p q›, of x, THEN arg_cong[where f=set_spmf], THEN eq_refl] Cons.prems False
      have "cond_spmf_fst (bind_spmf p (λs. callee1 s x)) y = return_pmf None"
        by(clarsimp simp add: bind_eq_return_pmf_None)(rule ccontr; fastforce)
      ultimately show ?thesis by(simp del: cond_spmf_fst_eq_return_None)
    qed
    also have "… = trace_callee callee2 q (xy # xs) z"
      by(simp add: split_def o_def)
    finally show ?case .
  qed
qed

proposition trace_callee_eq_coinduct_strong [consumes 1, case_names step sim, case_conclusion step lhs rhs, case_conclusion sim sim eq]:
  fixes callee1 :: "('a, 'b, 's1) callee" and callee2 :: "('a, 'b, 's2) callee"
  assumes start: "S p q"
    and step: "⋀p q a. ⟦ S p q; a ∈ A ⟧ ⟹
      bind_spmf p (λs. map_spmf fst (callee1 s a)) = bind_spmf q (λs. map_spmf fst (callee2 s a))"
    and sim: "⋀p q a res res' b s'' s'. ⟦ S p q; a ∈ A; res ∈ set_spmf p; (b, s'') ∈ set_spmf (callee1 res a); res' ∈ set_spmf q; (b, s') ∈ set_spmf (callee2 res' a) ⟧
      ⟹ S (cond_spmf_fst (bind_spmf p (λs. callee1 s a)) b)
            (cond_spmf_fst (bind_spmf q (λs. callee2 s a)) b) ∨
          trace_callee_eq callee1 callee2 A (cond_spmf_fst (bind_spmf p (λs. callee1 s a)) b) (cond_spmf_fst (bind_spmf q (λs. callee2 s a)) b)"
  shows "trace_callee_eq callee1 callee2 A p q"
proof -
  from start have "S p q ∨ trace_callee_eq callee1 callee2 A p q" by simp
  thus ?thesis
    apply(rule trace_callee_eq_coinduct)
     apply(erule disjE)
      apply(erule (1) step)
     apply(drule trace_callee_eqD[where xs="[]"]; simp)
    apply(erule disjE)
     apply(erule (5) sim)
    apply(rule disjI2)
    apply(rule trace_callee_eqI)
    apply(drule trace_callee_eqD[where xs="(_, _) # _"])
    apply simp_all
    done
qed

lemma trace_callee_return_pmf_None [simp]:
  "trace_callee_eq callee1 callee2 A (return_pmf None) (return_pmf None)"
  by(rule trace_callee_eqI) simp

lemma trace_callee_eq_sym [sym]: "trace_callee_eq callee1 callee2 A p q ⟹ trace_callee_eq callee2 callee1 A q p"
  by(simp add: trace_callee_eq_def)

lemma eq_resource_on_imp_trace_eq: "A ⊢⇩R res1 ≈ res2" if "A ⊢⇩R res1 ∼ res2"
proof -
  have "outs_ℐ (ℐ_uniform A UNIV :: ('a, 'b) ℐ) ⊢⇩R res1 ≈ res2" using that
    by -(rule distinguish_trace_eq[OF connect_eq_resource_cong], simp+)
  thus ?thesis by simp
qed

lemma advantage_nonneg: "0 ≤ advantage 𝒜 res1 res2"
  by(simp add: advantage_def)

lemma comp_converter_of_resource_conv_parallel_converter:
  "(converter_of_resource res |⇩∝ 1⇩C) ⊙ conv = converter_of_resource res |⇩∝ conv"
  by(coinduction arbitrary: res conv)
    (auto 4 3 simp add: rel_fun_def gpv.map_comp map_lift_spmf spmf_rel_map split_def map_gpv_conv_bind[symmetric] id_def[symmetric] gpv.rel_map split!: sum.split intro!: rel_spmf_reflI gpv.rel_refl_strong)

lemma comp_converter_of_resource_conv_parallel_converter2:
  "(1⇩C |⇩∝ converter_of_resource res) ⊙ conv = conv |⇩∝ converter_of_resource res"
  by(coinduction arbitrary: res conv)
    (auto 4 3 simp add: rel_fun_def gpv.map_comp map_lift_spmf spmf_rel_map split_def map_gpv_conv_bind[symmetric] id_def[symmetric] gpv.rel_map split!: sum.split intro!: rel_spmf_reflI gpv.rel_refl_strong)

lemma parallel_converter_map_converter:
  "map_converter f g f' g' conv1 |⇩∝ map_converter f'' g'' f' g' conv2 = 
   map_converter (map_sum f f'') (map_sum g g'') f' g' (conv1 |⇩∝ conv2)"
  using parallel_callee_parametric[
      where A="conversep (BNF_Def.Grp UNIV f)" and B="BNF_Def.Grp UNIV g" and C="BNF_Def.Grp UNIV f'" and R="conversep (BNF_Def.Grp UNIV g')" and A'="conversep (BNF_Def.Grp UNIV f'')" and B'="BNF_Def.Grp UNIV g''",
      unfolded rel_converter_Grp sum.rel_conversep sum.rel_Grp,
      simplified,
      unfolded rel_converter_Grp]
  by(simp add: rel_fun_def Grp_def)

lemma map_converter_parallel_converter_out2:
  "conv1 |⇩∝ map_converter f g id id conv2 = map_converter (map_sum id f) (map_sum id g) id id (conv1 |⇩∝ conv2)"
  by(rule parallel_converter_map_converter[where f=id and g=id and f'=id and g'=id, simplified])

lemma parallel_converter_assoc2:
  "parallel_converter conv1 (parallel_converter conv2 conv3) =                                   
   map_converter lsumr rsuml id id (parallel_converter (parallel_converter conv1 conv2) conv3)"
  by(coinduction arbitrary: conv1 conv2 conv3)
    (auto 4 5 intro!: rel_funI gpv.rel_refl_strong split: sum.split simp add: gpv.rel_map map_gpv'_id map_gpv_conv_map_gpv'[symmetric])

lemma parallel_converter_of_resource:
  "converter_of_resource res1 |⇩∝ converter_of_resource res2 = converter_of_resource (res1 ∥ res2)"
  by(coinduction arbitrary: res1 res2)
    (auto 4 3 simp add: rel_fun_def map_lift_spmf spmf_rel_map intro!: rel_spmf_reflI split!: sum.split)

lemma map_Inr_parallel_converter:
  "map_converter Inr f g h (conv1 |⇩∝ conv2) = map_converter id (f ∘ Inr) g h conv2"
  (is "?lhs = ?rhs")
proof -
  have "?lhs = map_converter Inr f id id (map_converter id id g h conv1 |⇩∝ map_converter id id g h conv2)"
    by(simp add: parallel_converter_map_converter sum.map_id0)
  also have "map_converter Inr f id id (conv1 |⇩∝ conv2) = map_converter id (f ∘ Inr) id id conv2" for conv1 conv2
    by(coinduction arbitrary: conv2)
      (auto simp add: rel_fun_def map_gpv_conv_map_gpv'[symmetric] gpv.rel_map intro!: gpv.rel_refl_strong)
  also have "map_converter id (f ∘ Inr) id id (map_converter id id g h conv2) = ?rhs" by simp
  finally show ?thesis .
qed

lemma map_Inl_parallel_converter:
  "map_converter Inl f g h (conv1 |⇩∝ conv2) = map_converter id (f ∘ Inl) g h conv1"
  (is "?lhs = ?rhs")
proof -
  have "?lhs = map_converter Inl f id id (map_converter id id g h conv1 |⇩∝ map_converter id id g h conv2)"
    by(simp add: parallel_converter_map_converter sum.map_id0)
  also have "map_converter Inl f id id (conv1 |⇩∝ conv2) = map_converter id (f ∘ Inl) id id conv1" for conv1 conv2
    by(coinduction arbitrary: conv1)
      (auto simp add: rel_fun_def map_gpv_conv_map_gpv'[symmetric] gpv.rel_map intro!: gpv.rel_refl_strong)
  also have "map_converter id (f ∘ Inl) id id (map_converter id id g h conv1) = ?rhs" by simp
  finally show ?thesis .
qed

lemma left_interface_parallel_converter:
  "left_interface (conv1 |⇩∝ conv2) = left_interface conv1 |⇩∝ left_interface conv2"
  by(coinduction arbitrary: conv1 conv2)
    (auto 4 3 split!: sum.split simp add: rel_fun_def gpv.rel_map left_gpv_map[where h=id] sum.map_id0 intro!: gpv.rel_refl_strong)

lemma right_interface_parallel_converter:
  "right_interface (conv1 |⇩∝ conv2) = right_interface conv1 |⇩∝ right_interface conv2"
  by(coinduction arbitrary: conv1 conv2)
    (auto 4 3 split!: sum.split simp add: rel_fun_def gpv.rel_map right_gpv_map[where h=id] sum.map_id0 intro!: gpv.rel_refl_strong)

lemma left_interface_converter_of_resource [simp]: 
  "left_interface (converter_of_resource res) = converter_of_resource res"
  by(coinduction arbitrary: res)(auto simp add: rel_fun_def map_lift_spmf spmf_rel_map intro!: rel_spmf_reflI)

lemma right_interface_converter_of_resource [simp]: 
  "right_interface (converter_of_resource res) = converter_of_resource res"
  by(coinduction arbitrary: res)(auto simp add: rel_fun_def map_lift_spmf spmf_rel_map intro!: rel_spmf_reflI)

lemma parallel_converter_swap: "map_converter swap_sum swap_sum id id (conv1 |⇩∝ conv2) = conv2 |⇩∝ conv1"
  by(coinduction arbitrary: conv1 conv2)
    (auto 4 3 split!: sum.split simp add: rel_fun_def map_gpv_conv_map_gpv'[symmetric] gpv.rel_map intro!: gpv.rel_refl_strong)

lemma eq_ℐ_converter_map_converter':
  assumes "ℐ'', map_ℐ f' g' ℐ' ⊢⇩C conv1 ∼ conv2"
    and "f ` outs_ℐ ℐ ⊆ outs_ℐ ℐ''"
    and "∀q∈outs_ℐ ℐ. g ` responses_ℐ ℐ'' (f q) ⊆ responses_ℐ ℐ q"
  shows "ℐ, ℐ' ⊢⇩C map_converter f g f' g' conv1 ∼ map_converter f g f' g' conv2"
  using assms(1)
proof(coinduction arbitrary: conv1 conv2)
  case eq_ℐ_converter
  from this(2) have "f q ∈ outs_ℐ ℐ''" using assms(2) by auto
  from eq_ℐ_converter(1)[THEN eq_ℐ_converterD, OF this] eq_ℐ_converter(2)
  show ?case
    apply simp
    apply(rule eq_ℐ_gpv_map_gpv')
    apply(simp add: BNF_Def.vimage2p_def prod.rel_map)
    apply(erule eq_ℐ_gpv_mono')
    using assms(3)
     apply(auto 4 4 simp add: eq_onp_def)
    done
qed

lemma parallel_converter_eq_ℐ_cong:
  "⟦ ℐ1, ℐ ⊢⇩C conv1 ∼ conv1'; ℐ2, ℐ ⊢⇩C conv2 ∼ conv2' ⟧
  ⟹ ℐ1 ⊕⇩ℐ ℐ2, ℐ ⊢⇩C parallel_converter conv1 conv2 ∼ parallel_converter conv1' conv2'"
  by(coinduction arbitrary: conv1 conv2 conv1' conv2')
    (fastforce dest: eq_ℐ_converterD elim!: eq_ℐ_gpv_mono' simp add: eq_onp_def)

― ‹Helper lemmas for simplyfing @{term exec_gpv}›
lemma
  exec_gpv_parallel_oracle_right: 
    "exec_gpv (oracle1 ‡⇩O oracle2) (right_gpv gpv) s = exec_gpv (†oracle2) gpv s"
  unfolding spmf_rel_eq[symmetric]
  apply (rule rel_spmf_mono)
  by (rule exec_gpv_parametric'[where S="(=)" and A="(=)" and CALL="λl r. l = Inr r" and R="λl r. l = Inr r" , THEN rel_funD, THEN rel_funD, THEN rel_funD ])
    (auto simp add: prod.rel_eq extend_state_oracle_def parallel_oracle_def split_def
      spmf_rel_map1 spmf_rel_map2 map_prod_def rel_spmf_reflI right_gpv_Inr_transfer intro!:rel_funI)

lemma
  exec_gpv_parallel_oracle_left: 
    "exec_gpv (oracle1 ‡⇩O oracle2) (left_gpv gpv) s = exec_gpv (oracle1†) gpv s" (is "?L = ?R")
  unfolding spmf_rel_eq[symmetric]
  apply (rule rel_spmf_mono)
   by (rule exec_gpv_parametric'[where S="(=)" and A="(=)" and CALL="λl r. l = Inl r" and R="λl r. l = Inl r" , THEN rel_funD, THEN rel_funD, THEN rel_funD ])
     (auto simp add: prod.rel_eq extend_state_oracle2_def parallel_oracle_def split_def
       spmf_rel_map1 spmf_rel_map2 map_prod_def rel_spmf_reflI left_gpv_Inl_transfer intro!:rel_funI)

end