Theory Purification

theory Purification

imports Run_Adversary

begin
context o2h_setting
begin

unbundle cblinfun_syntax
unbundle lattice_syntax
unbundle register_syntax

section ‹Purification of the Adversary›

text ‹Purification of composed kraus maps.›

definition purify_comp_kraus :: 
  "nat ⇒ (nat ⇒ ('a::chilbert_space, 'b::chilbert_space, 'c) kraus_family) ⇒ (nat ⇒ 'a ⇒⇩C⇩L 'b) set" where
  "purify_comp_kraus n 𝔈 = PiE {0..<n+1} (λi. (fst ` (Rep_kraus_family (𝔈 i))))"


definition comp_upto :: "(nat ⇒ ('a::chilbert_space) ⇒⇩C⇩L 'a) ⇒ nat ⇒ 'a ⇒⇩C⇩L 'a" where
  "comp_upto f n = fold (λi x. f i o⇩C⇩L x) [0..<n+1] id_cblinfun"


text ‹Some auxiliary lemmas on injectivity, Fst and finiteness.›

lemma Rep_kf_id:
  "Rep_kraus_family kf_id = {(id_cblinfun :: 'a ⇒⇩C⇩L 'a::{chilbert_space,not_singleton},())}"
  by (simp add: kf_id_def kf_of_op.rep_eq del: kf_of_op_id)

lemma fst_Rep_kf_Fst:
  fixes 𝔈 :: "('a ell2, 'b ell2, unit) kraus_family"
  shows "fst ` (Rep_kraus_family (kf_Fst 𝔈)) =  Fst ` (fst ` (Rep_kraus_family 𝔈))"
proof (transfer, safe, goal_cases)
  case (1 𝔈 x a aa)
  then have "aa ∈fst `𝔈" by (metis fst_conv image_eqI)
  then show ?case by (auto simp add: Fst_def)
next
  case (2 𝔈 x xa a)
  then show ?case by (auto simp add: Fst_def image_comp)
qed


lemma inj_on_Fst:
  shows "inj_on Fst A"
  unfolding Fst_def inj_on_def using inj_tensor_left[OF id_cblinfun_not_0] unfolding inj_def by auto


lemma finite_kf_Fst:
  fixes 𝔈 :: "('mem ell2, 'mem ell2, unit) kraus_family"
  assumes "finite (Rep_kraus_family 𝔈)"
  shows "finite (Rep_kraus_family (kf_Fst 𝔈))"
  using assms by transfer auto

lemma finite_kf_id:
  "finite (Rep_kraus_family kf_id)"
  by (simp add: kf_of_op.rep_eq flip: kf_of_op_id)


lemma inj_on_fst_Rep_kraus_family:
  fixes 𝔈 :: "('a ell2,'b ell2,unit) kraus_family"
  shows "inj_on fst (Rep_kraus_family 𝔈)"
  unfolding inj_on_def by fastforce


lemma comp_kraus_maps_set_finite:
  assumes "⋀i. i<n+1 ⟹ finite (Rep_kraus_family (𝔈 i))"
  shows "finite (purify_comp_kraus n 𝔈)"
  unfolding purify_comp_kraus_def by (intro finite_PiE) (auto simp add: assms)


text ‹Showing conditions of Kraus maps.›


lemma norm_square_in_kraus_map:
  fixes 𝔈 :: "('a ell2,'a ell2,unit) kraus_family"
  assumes "kf_bound 𝔈 ≤ id_cblinfun"
  assumes "U ∈ fst ` Rep_kraus_family 𝔈"
  shows "U* o⇩C⇩L U ≤ id_cblinfun"
proof -
  have *: "{(U, ())} ⊆ Rep_kraus_family 𝔈" using assms(2) by auto
  show ?thesis using kf_bound_geq_sum[OF *] assms(1) by auto
qed

lemma norm_in_kraus_map:
  fixes 𝔈 :: "('a ell2,'a ell2,unit) kraus_family"
  assumes "kf_bound 𝔈 ≤ id_cblinfun"
  assumes "U ∈ fst ` Rep_kraus_family 𝔈"
  shows "norm U ≤ 1"
  using norm_square_in_kraus_map[OF assms] cond_to_norm_1 by auto

lemma purify_comp_kraus_in_kraus_family:
  assumes "UA ∈ purify_comp_kraus n 𝔈" "j<n+1"
  shows "UA j ∈ fst ` Rep_kraus_family (𝔈 j)"
proof (intro PiE_mem[of UA "{0..<n+1}"])
  show "UA ∈ (Π⇩E a∈{0..<n+1}. fst ` Rep_kraus_family (𝔈 a))" 
    using assms(1) unfolding purify_comp_kraus_def by auto
  show "j ∈ {0..<n+1}" using assms(2) by auto
qed

lemma norm_in_purify_comp_kraus:
  fixes 𝔈 :: "nat ⇒ ('a ell2, 'a ell2, unit) kraus_family"
  assumes "⋀i. i<n+1 ⟹ kf_bound (𝔈 i) ≤ id_cblinfun"
  assumes "UA ∈ purify_comp_kraus n 𝔈" 
  shows "⋀i. i<n+1 ⟹ norm (UA i) ≤ 1"
proof -
  fix i assume i: "i<n+1"
  have "UA i ∈ fst ` Rep_kraus_family (𝔈 i)"
    using purify_comp_kraus_in_kraus_family[OF assms(2) ‹i<n+1›] by auto
  then show "norm (UA i) ≤ 1" using norm_in_kraus_map assms(1) i by auto
qed


lemma run_pure_adv_tc_over:
  assumes "m > n"
  shows "run_pure_adv_tc n (UA(m := x)) UB init' X' Y' H = run_pure_adv_tc n UA UB init' X' Y' H"
  using assms by (induct n arbitrary: m x) auto

lemma run_pure_adv_tc_Fst_over:
  assumes "m > n"
  shows "run_pure_adv_tc n (Fst o UA(m := x)) UB init' X' Y' H = 
       run_pure_adv_tc n (Fst o UA) UB init' X' Y' H"
  using assms by (induct n arbitrary: m x) auto




text ‹Purifications of the adversarial runs.›

lemma purification_run_mixed_adv:
  assumes "⋀i. i<n+1 ⟹ finite (Rep_kraus_family (𝔈 i))"
  assumes "⋀i. i<n+1 ⟹ fst ` Rep_kraus_family (𝔈 i) ≠ {}" (* Needed? *)
  shows "run_mixed_adv n 𝔈 UB init' X' Y' H = 
  (∑ UAs ∈ purify_comp_kraus n 𝔈. run_pure_adv_tc n UAs UB init' X' Y' H)"
  unfolding purify_comp_kraus_def using assms
proof (induct n)
  case 0
  have "kf_apply (𝔈 0) (tc_selfbutter init') = 
    (∑E∈fst ` (Rep_kraus_family (𝔈 0)). sandwich_tc E (tc_selfbutter init'))"
    unfolding kf_apply.rep_eq using assms 
    by (subst sum.reindex) (auto simp add: inj_on_fst_Rep_kraus_family d_gr_0) 
  moreover have "(∑UAs∈(Π⇩E i∈{0}. fst ` Rep_kraus_family (𝔈 i)).
       sandwich_tc (UAs 0) (tc_selfbutter init')) = 
    (∑E∈fst ` (Rep_kraus_family (𝔈 0)). sandwich_tc E (tc_selfbutter init'))"
    (is "?left = ?right")
  proof -
    have inj1: "inj_on (λUA. UA 0) (Π⇩E i∈{0}. fst ` Rep_kraus_family (𝔈 i))"
      by (smt (verit, best) PiE_ext inj_on_def singletonD)
    have non_empty: "(Π⇩E i∈{0}. fst ` Rep_kraus_family (𝔈 i)) ≠ {}" 
      by (metis (no_types, lifting) "0"(2) PiE_eq_empty_iff Suc_eq_plus1 singleton_iff zero_less_Suc)
    have "?left = (∑UA ∈ (λUA. UA 0) ` (Π⇩E i∈{0}. fst ` Rep_kraus_family (𝔈 i)).
       sandwich_tc UA (tc_selfbutter init'))"
      by (subst sum.reindex) (auto simp add: inj1)
    also have "… = (∑UA ∈ fst ` Rep_kraus_family (𝔈 0).
       sandwich_tc UA (tc_selfbutter init'))" 
      by (intro sum.cong) (auto simp add: image_projection_PiE non_empty)
    finally show ?thesis by auto
  qed
  ultimately show ?case by auto
next
  case (Suc d)
  have inj2: "inj_on (λ(y, g). g(Suc d := y))(fst ` Rep_kraus_family (𝔈 (Suc d)) ×
      (Π⇩E i∈{0..<Suc d}. fst ` Rep_kraus_family (𝔈 i)))"
    by (metis atLeastLessThan_iff inj_combinator less_irrefl_nat)
  let ?Φ = "sandwich_tc ((X';Y') (Uquery H) o⇩C⇩L UB d)(run_mixed_adv d 𝔈 UB init' X' Y' H)"
  let ?Ψ = "(λUAs. run_pure_adv_tc d UAs UB init' X' Y' H)"
  have kraus: "kf_apply (𝔈 (Suc d)) ?Φ = 
    (∑E∈fst ` (Rep_kraus_family (𝔈 (Suc d))). sandwich_tc E ?Φ)"
    unfolding kf_apply.rep_eq using assms 
    by (subst sum.reindex) (auto simp add: inj_on_fst_Rep_kraus_family Suc)
  also have "… = (∑UA∈fst ` Rep_kraus_family (𝔈 (Suc d)).
     (∑UAs∈(Π⇩E i∈{0..<Suc d}. fst ` Rep_kraus_family (𝔈 i)).  sandwich_tc UA
      (sandwich_tc ((X';Y') (Uquery H) o⇩C⇩L UB d) (?Ψ UAs))))" 
    using Suc by (intro sum.cong)(auto simp add: sandwich_tc_sum)
  also have "… = (∑(UA,UAs)∈fst ` Rep_kraus_family (𝔈 (Suc d))× 
    (Π⇩E i∈{0..<Suc d}. fst ` Rep_kraus_family (𝔈 i)).
    sandwich_tc UA (sandwich_tc ((X';Y') (Uquery H) o⇩C⇩L UB d) (?Ψ UAs)))"
    by (subst sum.cartesian_product) auto 
  also have "… = (∑UAs∈(λ(y, g). g(Suc d := y)) ` (fst ` Rep_kraus_family (𝔈 (Suc d)) × 
    (Π⇩E i∈ {0..<Suc d}. fst ` Rep_kraus_family (𝔈 i))).
    sandwich_tc (UAs (Suc d) o⇩C⇩L (X';Y') (Uquery H) o⇩C⇩L UB d)(?Ψ UAs))" 
    by (subst sum.reindex) (auto intro!: sum.cong simp add: o_def sandwich_tc_compose 
        run_pure_adv_tc_over inj2)
  also have "… = (∑UAs∈(Π⇩E i∈insert (Suc d) {0..<Suc d}. fst ` Rep_kraus_family (𝔈 i)).
       sandwich_tc (UAs (Suc d) o⇩C⇩L (X';Y') (Uquery H) o⇩C⇩L UB d) (?Ψ UAs))"
    by (subst PiE_insert_eq) auto
  finally show ?case by (auto simp add: set_upt_Suc)
qed


lemma purification_run_mixed_A:
  assumes "⋀i. i<d+1 ⟹ finite (Rep_kraus_family (𝔈 i))"
  assumes "⋀i. i<d+1 ⟹ fst ` Rep_kraus_family (𝔈 i) ≠ {}" (* Needed? *)
  shows "run_mixed_A 𝔈 H = (∑ UAs ∈ purify_comp_kraus d 𝔈. run_pure_A_tc UAs H)"
  unfolding run_mixed_A_def run_pure_A_tc_def using assms
  by (auto intro!: purification_run_mixed_adv)


lemma purification_run_mixed_B:
  assumes "⋀i. i<d+1 ⟹ finite (Rep_kraus_family (𝔈 i))"
  assumes "⋀i. i<d+1 ⟹ fst ` Rep_kraus_family (𝔈 i) ≠ {}" (* Needed? *)
  shows "run_mixed_B 𝔈 H S = (∑ UAs ∈ purify_comp_kraus d 𝔈. run_pure_B_tc UAs H S)"
  unfolding run_mixed_B_def run_pure_B_tc_def purify_comp_kraus_def 
  using assms
proof (induct d)
  case 0
  let ?𝔈0 = "kf_Fst (𝔈 0)"
  have finite: "finite (Rep_kraus_family ?𝔈0)" 
    using finite_kf_Fst assms(1)  by auto
  have inj1: "inj_on fst (Rep_kraus_family ?𝔈0)"
    by (rule inj_on_fst_Rep_kraus_family)
  have inj2: "inj_on Fst (fst ` Rep_kraus_family (𝔈 0))"
    using inj_on_Fst by auto
  have *: "kf_apply ?𝔈0 (tc_selfbutter init_B) = 
    (∑E∈fst ` (Rep_kraus_family ?𝔈0). sandwich_tc E (tc_selfbutter init_B))"
    unfolding kf_apply.rep_eq
    by (subst sum.reindex) (auto simp add: infsum_finite[OF finite] inj1 ) 
  have "kf_apply ?𝔈0 (tc_selfbutter init_B) = 
    (∑E∈fst ` (Rep_kraus_family (𝔈 0)). sandwich_tc (Fst E) (tc_selfbutter init_B))"
    unfolding * fst_Rep_kf_Fst by (subst sum.reindex) (auto simp add: o_def inj2)
  moreover have "(∑UAs∈(Π⇩E i∈{0}. fst ` Rep_kraus_family (𝔈 i)).
       sandwich_tc (Fst (UAs 0)) (tc_selfbutter init_B)) = 
    (∑E∈fst ` (Rep_kraus_family (𝔈 0)). sandwich_tc (Fst E) (tc_selfbutter init_B))"
    (is "?left = ?right")
  proof -
    have inj1: "inj_on (λUA. UA 0) (Π⇩E i∈{0}. fst ` Rep_kraus_family (𝔈 i))"
      by (smt (verit, best) PiE_ext inj_on_def singletonD)
    have non_empty: "(Π⇩E i∈{0}. fst ` Rep_kraus_family (𝔈 i)) ≠ {}" 
      by (smt (verit, del_insts) PiE_eq_empty_iff add_is_0 assms(2) d_gr_0 emptyE insertE not_gr0)
    have "?left = (∑UA ∈ (λUA. UA 0) ` (Π⇩E i∈{0}. fst ` Rep_kraus_family (𝔈 i)).
       sandwich_tc (Fst UA) (tc_selfbutter init_B))"
      by (subst sum.reindex) (auto simp add: inj1)
    also have "… = (∑UA ∈ fst ` Rep_kraus_family (𝔈 0).
       sandwich_tc (Fst UA) (tc_selfbutter init_B))" 
      by (intro sum.cong) (auto simp add: image_projection_PiE non_empty)
    finally show ?thesis by auto
  qed
  ultimately show ?case by auto
next
  case (Suc d)
  let ?𝔈 = "(λi. kf_Fst (𝔈 i))"
  have inj1: "inj_on (λ(y, g). g(Suc d := y))(fst ` Rep_kraus_family (𝔈 (Suc d)) ×
      (Π⇩E i∈{0..<Suc d}. fst ` Rep_kraus_family (𝔈 i)))"
    by (metis atLeastLessThan_iff inj_combinator less_irrefl_nat)
  let ?Φ = "sandwich_tc ((X_for_B;Y_for_B) (Uquery H) o⇩C⇩L US S d)
    (run_mixed_adv d ?𝔈 (US S) init_B X_for_B Y_for_B H)"
  let ?Ψ = "(λUAs. run_pure_adv_tc d UAs (US S) init_B X_for_B Y_for_B H)"
  have finite: "finite (Rep_kraus_family (kf_Fst (𝔈 (Suc d))))"
    using Suc.prems(1) finite_kf_Fst by auto
  have "kf_apply (?𝔈 (Suc d)) ?Φ = 
    (∑E∈fst ` Rep_kraus_family (kf_Fst (𝔈 (Suc d))). sandwich_tc E ?Φ)"
    by (subst sum.reindex) (auto simp add: kf_apply.rep_eq infsum_finite[OF finite] 
        inj_on_fst_Rep_kraus_family)
  also have "… =  (∑E∈fst ` Rep_kraus_family (𝔈 (Suc d)). sandwich_tc (Fst E) ?Φ)"
    unfolding fst_Rep_kf_Fst by (subst sum.reindex) (auto simp add: inj_on_Fst)
  also have "… = (∑UA∈fst ` Rep_kraus_family (𝔈 (Suc d)).
     (∑UAs∈(Π⇩E i∈{0..<Suc d}. fst ` Rep_kraus_family (𝔈 i)).  sandwich_tc (Fst UA)
      (sandwich_tc ((X_for_B;Y_for_B) (Uquery H) o⇩C⇩L US S d) (?Ψ (Fst o UAs)))))" 
    using Suc unfolding kf_Fst_def[symmetric] by (intro sum.cong)(auto simp add: sandwich_tc_sum o_def)
  also have "… = (∑(UA,UAs)∈fst ` Rep_kraus_family (𝔈 (Suc d))× 
    (Π⇩E i∈{0..<Suc d}. fst ` Rep_kraus_family (𝔈 i)).
    sandwich_tc (Fst UA) (sandwich_tc ((X_for_B;Y_for_B) (Uquery H) o⇩C⇩L US S d) (?Ψ (Fst o UAs))))"
    by (subst sum.cartesian_product) auto 
  also have "… = (∑UAs∈(λ(y, g). g(Suc d := y)) ` (fst ` Rep_kraus_family (𝔈 (Suc d)) × 
    (Π⇩E i∈ {0..<Suc d}. fst ` Rep_kraus_family (𝔈 i))).
    sandwich_tc (Fst (UAs (Suc d)) o⇩C⇩L (X_for_B;Y_for_B) (Uquery H) o⇩C⇩L US S d)(?Ψ (Fst o UAs)))" 
    by (subst sum.reindex)(use run_pure_adv_tc_Fst_over[where init' = init_B and X' = X_for_B and Y' = Y_for_B] 
        in ‹auto intro!: sum.cong simp add: o_def sandwich_tc_compose inj1›)
  also have "… = (∑UAs∈(Π⇩E i∈insert (Suc d) {0..<Suc d}. fst ` Rep_kraus_family (𝔈 i)).
       sandwich_tc (Fst (UAs (Suc d)) o⇩C⇩L (X_for_B;Y_for_B) (Uquery H) o⇩C⇩L US S d) (?Ψ (Fst o UAs)))"
    by (subst PiE_insert_eq) auto
  finally show ?case unfolding kf_Fst_def by (auto simp add: set_upt_Suc o_def)
qed


lemma purification_run_mixed_B_count_prep:
  assumes "⋀i. i<d+1 ⟹ finite (Rep_kraus_family (𝔈 i))"
  assumes "⋀i. i<d+1 ⟹ fst ` Rep_kraus_family (𝔈 i) ≠ {}" (* Needed? *)
  assumes "n<d+1"
  shows "run_mixed_adv n (λn. kf_Fst (𝔈 n)) (λn. U_S' S)
     init_B_count X_for_C Y_for_C H =
    (∑UAs∈(Π⇩E i∈{0..<n + 1}. fst ` Rep_kraus_family (𝔈 i)).
       run_pure_adv_tc n (Fst ∘ UAs) (λ_. U_S' S) init_B_count X_for_C
        Y_for_C H)"
  using assms
proof (induct n)
  case 0
  let ?𝔈0 = "kf_Fst (𝔈 0)"
  have finite: "finite (Rep_kraus_family ?𝔈0)" 
    using finite_kf_Fst assms by auto
  have inj1: "inj_on fst (Rep_kraus_family ?𝔈0)"
    by (rule inj_on_fst_Rep_kraus_family)
  have inj2: "inj_on Fst (fst ` Rep_kraus_family (𝔈 0))" using inj_on_Fst by auto
  have *: "kf_apply ?𝔈0 (tc_selfbutter init_B_count) = 
    (∑E∈fst ` (Rep_kraus_family ?𝔈0). sandwich_tc E (tc_selfbutter init_B_count))"
    unfolding kf_apply.rep_eq
    by (subst sum.reindex) (auto simp add: infsum_finite[OF finite] inj1 ) 
  have "kf_apply ?𝔈0 (tc_selfbutter init_B_count) = 
    (∑E∈fst ` (Rep_kraus_family (𝔈 0)). sandwich_tc (Fst E) (tc_selfbutter init_B_count))"
    unfolding * fst_Rep_kf_Fst by (subst sum.reindex) (auto simp add: o_def inj2)
  moreover have "(∑UAs∈(Π⇩E i∈{0}. fst ` Rep_kraus_family (𝔈 i)).
       sandwich_tc (Fst (UAs 0)) (tc_selfbutter init_B_count)) = 
    (∑E∈fst ` (Rep_kraus_family (𝔈 0)). sandwich_tc (Fst E) (tc_selfbutter init_B_count))"
    (is "?left = ?right")
  proof -
    have inj1: "inj_on (λUA. UA 0) (Π⇩E i∈{0}. fst ` Rep_kraus_family (𝔈 i))"
      by (smt (verit, best) PiE_ext inj_on_def singletonD)
    have non_empty: "(Π⇩E i∈{0}. fst ` Rep_kraus_family (𝔈 i)) ≠ {}" 
      by (smt (verit, del_insts) PiE_eq_empty_iff add_is_0 assms(2) d_gr_0 emptyE insertE not_gr0)
    have "?left = (∑UA ∈ (λUA. UA 0) ` (Π⇩E i∈{0}. fst ` Rep_kraus_family (𝔈 i)).
       sandwich_tc (Fst UA) (tc_selfbutter init_B_count))"
      by (subst sum.reindex) (auto simp add: inj1)
    also have "… = (∑UA ∈ fst ` Rep_kraus_family (𝔈 0).
       sandwich_tc (Fst UA) (tc_selfbutter init_B_count))" 
      by (intro sum.cong) (auto simp add: image_projection_PiE non_empty)
    finally show ?thesis by auto
  qed
  ultimately show ?case by auto
next
  case (Suc n)
  define 𝔈' :: "('mem×nat) kraus_adv" where "𝔈' = (λi. kf_Fst (𝔈 i))"
  have inj1: "inj_on (λ(y, g). g(Suc n := y))(fst ` Rep_kraus_family (𝔈 (Suc n)) ×
      (Π⇩E i∈{0..<Suc n}. fst ` Rep_kraus_family (𝔈 i)))"
    by (metis atLeastLessThan_iff inj_combinator less_irrefl_nat)
  let ?Φ = "sandwich_tc ((X_for_C;Y_for_C) (Uquery H) o⇩C⇩L U_S' S)
    (run_mixed_adv n 𝔈' (λ_. U_S' S) init_B_count X_for_C Y_for_C H)"
  define Ψ where "Ψ = (λUAs. run_pure_adv_tc n UAs (λ_. U_S' S) init_B_count X_for_C Y_for_C H)"

  have finite: "finite (Rep_kraus_family (kf_Fst (𝔈 (Suc n))))"
    using Suc.prems finite_kf_Fst by auto
  have "kf_apply (𝔈' (Suc n)) ?Φ = 
    (∑E∈fst ` Rep_kraus_family (kf_Fst (𝔈 (Suc n))). sandwich_tc E ?Φ)"
    unfolding 𝔈'_def
    by (subst sum.reindex) (auto simp add: kf_apply.rep_eq infsum_finite[OF finite] 
        inj_on_fst_Rep_kraus_family)
  also have "… =  (∑E∈fst ` Rep_kraus_family (𝔈 (Suc n)). sandwich_tc (Fst E) ?Φ)"
    unfolding fst_Rep_kf_Fst by (subst sum.reindex) (auto simp add: inj_on_Fst)
  also have "… = (∑UA∈fst ` Rep_kraus_family (𝔈 (Suc n)).
     (∑UAs∈(Π⇩E i∈{0..<Suc n}. fst ` Rep_kraus_family (𝔈 i)).  sandwich_tc (Fst UA)
      (sandwich_tc ((X_for_C;Y_for_C) (Uquery H) o⇩C⇩L U_S' S) (Ψ (Fst o UAs)))))" 
    using Suc  unfolding kf_Fst_def[symmetric] Ψ_def 𝔈'_def
    by (auto simp add: sandwich_tc_sum o_def intro!: sum.cong)
  also have "… = (∑(UA,UAs)∈fst ` Rep_kraus_family (𝔈 (Suc n))× 
    (Π⇩E i∈{0..<Suc n}. fst ` Rep_kraus_family (𝔈 i)). sandwich_tc (Fst UA) 
    (sandwich_tc ((X_for_C;Y_for_C) (Uquery H) o⇩C⇩L U_S' S) (Ψ (Fst o UAs))))"
    by (subst sum.cartesian_product) auto 
  also have "… = (∑UAs∈(λ(y, g). g(Suc n := y)) ` (fst ` Rep_kraus_family (𝔈 (Suc n)) × 
    (Π⇩E i∈ {0..<Suc n}. fst ` Rep_kraus_family (𝔈 i))). sandwich_tc (Fst (UAs (Suc n)) o⇩C⇩L 
    (X_for_C;Y_for_C) (Uquery H) o⇩C⇩L U_S' S)(Ψ (Fst o UAs)))" 
    unfolding Ψ_def by (subst sum.reindex) 
      (use run_pure_adv_tc_Fst_over[where init' = init_B_count and X' = X_for_C and Y' = Y_for_C] 
        in ‹auto intro!: sum.cong simp add: o_def sandwich_tc_compose inj1›)
  also have "… = (∑UAs∈(Π⇩E i∈insert (Suc n) {0..<Suc n}. fst ` Rep_kraus_family (𝔈 i)).
    sandwich_tc (Fst (UAs (Suc n)) o⇩C⇩L (X_for_C;Y_for_C) (Uquery H) o⇩C⇩L U_S' S) 
    (Ψ (Fst o UAs)))"
    by (subst PiE_insert_eq) auto
  also have "… = (∑UAs∈(Π⇩E i∈{0..<Suc n + 1}. fst ` Rep_kraus_family (𝔈 i)).
    run_pure_adv_tc (Suc n) (Fst ∘ UAs) (λ_. U_S' S) init_B_count X_for_C Y_for_C H)"
    unfolding kf_Fst_def Ψ_def by (auto simp add: set_upt_Suc o_def intro!: sum.cong)
  finally show ?case unfolding 𝔈'_def by (auto simp add: comp_def)
qed

lemma purification_run_mixed_B_count:
  assumes "⋀i. i<d+1 ⟹ finite (Rep_kraus_family (𝔈 i))"
  assumes "⋀i. i<d+1 ⟹ fst ` Rep_kraus_family (𝔈 i) ≠ {}" (* Needed? *)
  shows "run_mixed_B_count 𝔈 H S = (∑ UAs ∈ purify_comp_kraus d 𝔈. run_pure_B_count_tc UAs H S)"
  unfolding run_mixed_B_count_def run_pure_B_count_tc_def purify_comp_kraus_def
  using purification_run_mixed_B_count_prep[where n=d, OF assms] by auto




text ‹Purification of \<^const>‹kf_Fst››


lemma purification_kf_Fst:
  assumes "⋀i. i < n + 1 ⟹ fst ` Rep_kraus_family (F i) ≠ {}"
  assumes "x ∈ purify_comp_kraus n (λn. kf_Fst (F n)::(('a × 'c) ell2, ('b × 'c) ell2, unit) kraus_family)"
  shows "∃UA. x = (λa. if a<n+1 then (Fst (UA a)::('a × 'c) ell2 ⇒⇩C⇩L ('b × 'c) ell2) else undefined)"
proof -
  have nonempty: "PiE {0..<n+1} (λi. Fst ` fst ` Rep_kraus_family (F i)
    ::(('a × 'c) ell2 ⇒⇩C⇩L ('b × 'c) ell2) set) ≠ {}"
    by (rule ccontr) (use assms in ‹auto simp add: PiE_eq_empty_iff›)
  have "x∈ PiE {0..<n+1} (λi. Fst ` fst ` Rep_kraus_family (F i))"
    using assms unfolding purify_comp_kraus_def fst_Rep_kf_Fst by auto
  then have elem: "x a ∈ (λf. f a) ` PiE {0..<n+1} (λi. Fst ` fst ` Rep_kraus_family (F i))"
    for a by blast
  have rew: "(λf. f a) ` PiE {0..<n+1} (λi. Fst ` fst ` Rep_kraus_family (F i)::
    (('a × 'c) ell2 ⇒⇩C⇩L ('b × 'c) ell2) set) = 
    (if a∈{0..<n+1}then Fst ` fst ` Rep_kraus_family (F a) else {undefined})" 
    for a by (subst image_projection_PiE) (use nonempty in ‹auto›)
  have el: "x a ∈ (if a∈{0..<n+1} then Fst ` fst ` Rep_kraus_family (F a) else {undefined})" 
    for a using elem unfolding rew by auto
  have ins: "a∈{0..<n+1} ⟹ x a ∈ Fst ` fst ` Rep_kraus_family (F a)" for a using el by meson
  then have "∃v. (v ∈ Rep_kraus_family (F a) ∧ x a = Fst(fst(v)))" if "a∈{0..<n+1}" for a
    using that by fastforce
  then obtain v where v_in: "a∈{0..<n+1} ⟹ v a ∈ Rep_kraus_family (F a)" 
    and x: "a∈{0..<n+1} ⟹ x a = (Fst (fst (v a))::('a × 'c) ell2 ⇒⇩C⇩L ('b × 'c) ell2)" for a
    by metis
  have outs: "¬a∈{0..<n+1} ⟹ x a = undefined" for a by (meson el singletonD)
  define val where "val a = (if a∈{0..<n+1} then v a else undefined)" for a
  have "x a = Fst (fst (val a))" if "a∈{0..<n+1}" for a 
    unfolding val_def using x[OF that] that by auto
  then have "x a = (if a ∈ {0..<n+1} then Fst (fst (val a)) else undefined)"
    for a by (cases "a∈{0..<n+1}", use outs in ‹auto›)
  then show ?thesis by (intro exI[of _ "(λa. fst (val a))"]) auto
qed


end

unbundle no cblinfun_syntax
unbundle no lattice_syntax
unbundle no register_syntax

end