Theory Constructive_Cryptography

section ‹Security›

theory Constructive_Cryptography imports
  Wiring
begin

definition "advantage 𝒜 res1 res2 = ¦spmf (connect 𝒜 res1) True - spmf (connect 𝒜 res2) True¦"

locale constructive_security_aux =
  fixes real_resource :: "security ⇒ ('a + 'e, 'b + 'f) resource"
    and ideal_resource :: "security ⇒ ('c + 'e, 'd + 'f) resource"
    and sim :: "security ⇒ ('a, 'b, 'c, 'd) converter"
    and ℐ_real :: "security ⇒ ('a, 'b) ℐ"
    and ℐ_ideal :: "security ⇒ ('c, 'd) ℐ"
    and ℐ_common :: "security ⇒ ('e, 'f) ℐ"
    and bound :: "security ⇒ enat"
    and lossless :: "bool"
  assumes WT_real [WT_intro]: "⋀η. ℐ_real η ⊕⇩ℐ ℐ_common η ⊢res real_resource η √"
    and WT_ideal [WT_intro]: "⋀η. ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢res ideal_resource η √"
    and WT_sim [WT_intro]: "⋀η. ℐ_real η, ℐ_ideal η ⊢⇩C sim η √"
    and adv: "⋀𝒜 :: security ⇒ ('a + 'e, 'b + 'f) distinguisher. 
    ⟦ ⋀η. ℐ_real η ⊕⇩ℐ ℐ_common η ⊢g 𝒜 η √; 
      ⋀η. interaction_bounded_by (λ_. True) (𝒜 η) (bound η);
      ⋀η. lossless ⟹ plossless_gpv (ℐ_real η ⊕⇩ℐ ℐ_common η) (𝒜 η) ⟧
    ⟹ negligible (λη. advantage (𝒜 η) (sim η |⇩= 1⇩C ⊳ ideal_resource η) (real_resource η))"


locale constructive_security =
  constructive_security_aux real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common bound lossless
  for real_resource :: "security ⇒ ('a + 'e, 'b + 'f) resource"
    and ideal_resource :: "security ⇒ ('c + 'e, 'd + 'f) resource"
    and sim :: "security ⇒ ('a, 'b, 'c, 'd) converter"
    and ℐ_real :: "security ⇒ ('a, 'b) ℐ"
    and ℐ_ideal :: "security ⇒ ('c, 'd) ℐ"
    and ℐ_common :: "security ⇒ ('e, 'f) ℐ"
    and bound :: "security ⇒ enat"
    and lossless :: "bool"
    and w :: "security ⇒ ('c, 'd, 'a, 'b) wiring"
  +
  assumes correct: "∃cnv. ∀𝒟 :: security ⇒ ('c + 'e, 'd + 'f) distinguisher.
    (∀η. ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √) 
  ⟶ (∀η. interaction_bounded_by (λ_. True) (𝒟 η) (bound η))
  ⟶ (∀η. lossless ⟶ plossless_gpv (ℐ_ideal η ⊕⇩ℐ ℐ_common η) (𝒟 η))
  ⟶ (∀η. wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)) ∧
       negligible (λη. advantage (𝒟 η) (ideal_resource η) (cnv η |⇩= 1⇩C ⊳ real_resource η))"

locale constructive_security2 =
  constructive_security_aux real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common bound lossless
  for real_resource :: "security ⇒ ('a + 'e, 'b + 'f) resource"
    and ideal_resource :: "security ⇒ ('c + 'e, 'd + 'f) resource"
    and sim :: "security ⇒ ('a, 'b, 'c, 'd) converter"
    and ℐ_real :: "security ⇒ ('a, 'b) ℐ"
    and ℐ_ideal :: "security ⇒ ('c, 'd) ℐ"
    and ℐ_common :: "security ⇒ ('e, 'f) ℐ"
    and bound :: "security ⇒ enat"
    and lossless :: "bool"
    and w :: "security ⇒ ('c, 'd, 'a, 'b) wiring"
  +
  assumes sim: "∃cnv. ∀η. wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η) ∧ wiring (ℐ_ideal η) (ℐ_ideal η) (cnv η ⊙ sim η) (id, id)"
begin

lemma constructive_security:
  "constructive_security real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common bound lossless w"
proof
  from sim obtain cnv
    where w: "⋀η. wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)"
      and inverse: "⋀η. wiring (ℐ_ideal η) (ℐ_ideal η) (cnv η ⊙ sim η) (id, id)"
    by blast
  show "∃cnv. ∀𝒟. (∀η. ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √)
    ⟶ (∀η. interaction_any_bounded_by (𝒟 η) (bound η))
    ⟶ (∀η. lossless ⟶ plossless_gpv (ℐ_ideal η ⊕⇩ℐ ℐ_common η) (𝒟 η))
    ⟶ (∀η. wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)) ∧
        negligible (λη. advantage (𝒟 η) (ideal_resource η) (cnv η |⇩= 1⇩C ⊳ real_resource η))"
  proof(intro strip exI conjI)
    fix 𝒟 :: "security ⇒ ('c + 'e, 'd + 'f) distinguisher"
    assume WT_D [rule_format, WT_intro]: "∀η. ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √"
      and bound [rule_format, interaction_bound]: "∀η. interaction_bounded_by (λ_. True) (𝒟 η) (bound η)"
      and lossless [rule_format]: "∀η. lossless ⟶ plossless_gpv (ℐ_ideal η ⊕⇩ℐ ℐ_common η) (𝒟 η)"
    
    show "wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)" for η by fact

    let ?A = "λη. outs_ℐ (ℐ_ideal η)"
    let ?cnv = "λη. restrict_converter (?A η) (ℐ_real η) (cnv η)"
    let ?𝒜 = "λη. absorb (𝒟 η) (?cnv η |⇩= 1⇩C)"

    have eq: "advantage (𝒟 η) (ideal_resource η) (cnv η |⇩= 1⇩C ⊳ real_resource η) =
    advantage (?𝒜 η) (sim η |⇩= 1⇩C ⊳ ideal_resource η) (real_resource η)" for η
    proof -
      from w[of η] have [WT_intro]: "ℐ_ideal η, ℐ_real η ⊢⇩C cnv η √" by cases
      have "ℐ_ideal η, ℐ_ideal η ⊢⇩C ?cnv η ⊙ sim η ∼ cnv η ⊙ sim η"
        by(rule eq_ℐ_comp_cong eq_ℐ_restrict_converter WT_intro order_refl eq_ℐ_converter_reflI)+
      also from inverse[of η] have "ℐ_ideal η, ℐ_ideal η ⊢⇩C cnv η ⊙ sim η ∼ 1⇩C" by cases simp
      finally have inverse': "ℐ_ideal η, ℐ_ideal η ⊢⇩C ?cnv η ⊙ sim η ∼ 1⇩C" .
      hence "ℐ_ideal η ⊕⇩ℐ ℐ_common η, ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢⇩C ?cnv η ⊙ sim η |⇩= 1⇩C ∼ 1⇩C |⇩= 1⇩C"
        by(rule parallel_converter2_eq_ℐ_cong)(intro eq_ℐ_converter_reflI WT_intro)
      also have "ℐ_ideal η ⊕⇩ℐ ℐ_common η, ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢⇩C 1⇩C |⇩= 1⇩C ∼ 1⇩C"
        by(rule parallel_converter2_id_id)
      also
      have eq1: "connect (𝒟 η) (?cnv η |⇩= 1⇩C ⊳ sim η |⇩= 1⇩C ⊳ ideal_resource η) = 
        connect (𝒟 η) (1⇩C ⊳ ideal_resource η)"
        unfolding attach_compose[symmetric] comp_converter_parallel2 comp_converter_id_right
        by(rule connect_eq_resource_cong WT_intro eq_ℐ_attach_on' calculation)+(fastforce intro: WT_intro)+

      have *: "ℐ_ideal η ⊕⇩ℐ ℐ_common η, ℐ_real η ⊕⇩ℐ ℐ_common η ⊢⇩C ?cnv η |⇩= 1⇩C ∼ cnv η |⇩= 1⇩C"
        by(rule parallel_converter2_eq_ℐ_cong eq_ℐ_restrict_converter)+(auto intro: WT_intro eq_ℐ_converter_reflI)
      have eq2: "connect (𝒟 η) (?cnv η |⇩= 1⇩C ⊳ real_resource η) = connect (𝒟 η) (cnv η |⇩= 1⇩C ⊳ real_resource η)"
        by(rule connect_eq_resource_cong WT_intro eq_ℐ_attach_on' *)+(auto intro: WT_intro)
      show ?thesis unfolding advantage_def by(simp add: distinguish_attach[symmetric] eq1 eq2)
    qed
    have "ℐ_real η ⊕⇩ℐ ℐ_common η ⊢g ?𝒜 η √" for η
    proof -
      from w have [WT_intro]: "ℐ_ideal η, ℐ_real η ⊢⇩C cnv η √" by cases
      show ?thesis by(rule WT_intro)+
    qed
    moreover
    have "interaction_any_bounded_by (absorb (𝒟 η) (?cnv η |⇩= 1⇩C)) (bound η)" for η
    proof -
      from w[of η] obtain f g where [simp]: "w η = (f, g)"
        and [WT_intro]: "ℐ_ideal η, ℐ_real η ⊢⇩C cnv η √"
        and eq: "ℐ_ideal η, ℐ_real η ⊢⇩C cnv η ∼ map_converter id id f g 1⇩C" by cases
      from eq_ℐ_restrict_converter_cong[OF eq order_refl]
      have *: "restrict_converter (?A η) (ℐ_real η) (cnv η) =
      restrict_converter (?A η) (ℐ_real η) (map_converter f g id id 1⇩C)"
        by(subst map_converter_id_move_right) simp
      show ?thesis unfolding * by interaction_bound_converter simp
    qed
    moreover have "plossless_gpv (ℐ_real η ⊕⇩ℐ ℐ_common η) (?𝒜 η)"
      if "lossless" for η 
    proof -
      from w[of η] obtain f g where [simp]: "w η = (f, g)"
        and cnv [WT_intro]: "ℐ_ideal η, ℐ_real η ⊢⇩C cnv η √"
        and eq: "ℐ_ideal η, ℐ_real η ⊢⇩C cnv η ∼ map_converter id id f g 1⇩C" by cases
      from eq_ℐ_converterD_WT1[OF eq cnv] have ℐ: "ℐ_ideal η ≤ map_ℐ f g (ℐ_real η)"
        by(rule WT_map_converter_idD)
      with WT_converter_id have [WT_intro]: "ℐ_ideal η, map_ℐ f g (ℐ_real η) ⊢⇩C 1⇩C √" 
        by(rule WT_converter_mono) simp
      have id: "plossless_converter (ℐ_ideal η) (map_ℐ f g (ℐ_real η)) 1⇩C"
        by(rule plossless_converter_mono)(rule plossless_id_converter order_refl ℐ WT_intro)+
      show ?thesis unfolding eq_ℐ_restrict_converter_cong[OF eq order_refl]
        by(rule plossless_gpv_absorb lossless[OF that] plossless_parallel_converter2 plossless_restrict_converter plossless_map_converter)+
          (fastforce intro: WT_intro id WT_converter_map_converter)+
    qed
    ultimately show "negligible (λη. advantage (𝒟 η) (ideal_resource η) (cnv η |⇩= 1⇩C ⊳ real_resource η))"
      unfolding eq by(rule adv)
  qed
qed

sublocale constructive_security real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common bound lossless w
  by(rule constructive_security)

end

subsection ‹Composition theorems›

theorem composability:
  fixes real
  assumes "constructive_security middle ideal sim_inner ℐ_middle ℐ_inner ℐ_common bound_inner lossless_inner w1"
  assumes "constructive_security real middle sim_outer ℐ_real ℐ_middle ℐ_common bound_outer lossless_outer w2"
  and bound [interaction_bound]: "⋀η. interaction_any_bounded_converter (sim_outer η) (bound_sim η)"
  and bound_le: "⋀η. bound_outer η * max (bound_sim η) 1 ≤ bound_inner η"
  and lossless_sim [plossless_intro]: "⋀η. lossless_inner ⟹ plossless_converter (ℐ_real η) (ℐ_middle η) (sim_outer η)"
  shows "constructive_security real ideal (λη. sim_outer η ⊙ sim_inner η) ℐ_real ℐ_inner ℐ_common bound_outer (lossless_outer ∨ lossless_inner) (λη. w1 η ∘⇩w w2 η)"
proof
  interpret inner: constructive_security middle ideal sim_inner ℐ_middle ℐ_inner ℐ_common bound_inner lossless_inner w1 by fact
  interpret outer: constructive_security real middle sim_outer ℐ_real ℐ_middle ℐ_common bound_outer lossless_outer w2 by fact

  show "ℐ_real η ⊕⇩ℐ ℐ_common η ⊢res real η √"
    and "ℐ_inner η ⊕⇩ℐ ℐ_common η ⊢res ideal η √"
    and "ℐ_real η, ℐ_inner η ⊢⇩C sim_outer η ⊙ sim_inner η √" for η by(rule WT_intro)+

  { fix 𝒜 :: "security ⇒ ('g + 'b, 'h + 'd) distinguisher"
    assume WT [WT_intro]: "ℐ_real η ⊕⇩ℐ ℐ_common η ⊢g 𝒜 η √" for η
    assume bound_outer [interaction_bound]: "interaction_bounded_by (λ_. True) (𝒜 η) (bound_outer η)" for η
    assume lossless [plossless_intro]:
      "lossless_outer ∨ lossless_inner ⟹ plossless_gpv (ℐ_real η ⊕⇩ℐ ℐ_common η) (𝒜 η)" for η

    let ?𝒜 = "λη. absorb (𝒜 η) (sim_outer η |⇩= 1⇩C)"
    have "ℐ_middle η ⊕⇩ℐ ℐ_common η ⊢g ?𝒜 η √" for η by(rule WT_intro)+
    moreover have "interaction_any_bounded_by (?𝒜 η) (bound_inner η)" for η
      by interaction_bound_converter(rule bound_le)
    moreover have "plossless_gpv (ℐ_middle η ⊕⇩ℐ ℐ_common η) (?𝒜 η)" if lossless_inner for η
      by(rule plossless_intro WT_intro | simp add: that)+
    ultimately have "negligible (λη. advantage (?𝒜 η) (sim_inner η |⇩= 1⇩C ⊳ ideal η) (middle η))"
      by(rule inner.adv)
    also have "negligible (λη. advantage (𝒜 η) (sim_outer η |⇩= 1⇩C ⊳ middle η) (real η))"
      by(rule outer.adv[OF WT bound_outer lossless]) simp
    finally (negligible_plus)
    show "negligible (λη. advantage (𝒜 η) (sim_outer η ⊙ sim_inner η |⇩= 1⇩C ⊳ ideal η) (real η))"
      apply(rule negligible_mono)
      apply(simp add: bigo_def)
      apply(rule exI[where x=1])
      apply simp
      apply(rule always_eventually)
      apply(clarsimp simp add: advantage_def)
      apply(rule order_trans)
       apply(rule abs_diff_triangle_ineq2)
      apply(rule add_right_mono)
      apply(clarsimp simp add: advantage_def distinguish_attach[symmetric] attach_compose[symmetric] comp_converter_parallel2 comp_converter_id_left)
      done
  next
    from inner.correct obtain cnv_inner
      where correct_inner: "⋀𝒟. ⟦ ⋀η. ℐ_inner η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √;
             ⋀η. interaction_any_bounded_by (𝒟 η) (bound_inner η);
             ⋀η. lossless_inner ⟹ plossless_gpv (ℐ_inner η ⊕⇩ℐ ℐ_common η) (𝒟 η) ⟧
           ⟹ (∀η. wiring (ℐ_inner η) (ℐ_middle η) (cnv_inner η) (w1 η)) ∧
               negligible (λη. advantage (𝒟 η) (ideal η) (cnv_inner η |⇩= 1⇩C ⊳ middle η))"
      by blast
    from outer.correct obtain cnv_outer
      where correct_outer: "⋀𝒟. ⟦ ⋀η. ℐ_middle η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √;
             ⋀η. interaction_any_bounded_by (𝒟 η) (bound_outer η);
             ⋀η. lossless_outer ⟹ plossless_gpv (ℐ_middle η ⊕⇩ℐ ℐ_common η) (𝒟 η) ⟧
           ⟹ (∀η. wiring (ℐ_middle η) (ℐ_real η) (cnv_outer η) (w2 η)) ∧
               negligible (λη. advantage (𝒟 η) (middle η) (cnv_outer η |⇩= 1⇩C ⊳ real η))"
      by blast
    show "∃cnv. ∀𝒟. (∀η. ℐ_inner η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √) ⟶
               (∀η. interaction_any_bounded_by (𝒟 η) (bound_outer η)) ⟶
               (∀η. lossless_outer ∨ lossless_inner ⟶ plossless_gpv (ℐ_inner η ⊕⇩ℐ ℐ_common η) (𝒟 η)) ⟶
               (∀η. wiring (ℐ_inner η) (ℐ_real η) (cnv η) (w1 η ∘⇩w w2 η)) ∧
               negligible (λη. advantage (𝒟 η) (ideal η) (cnv η |⇩= 1⇩C ⊳ real η))"
    proof(intro exI strip conjI)
      fix 𝒟 :: "security ⇒ ('e + 'b, 'f + 'd) distinguisher"
      assume WT_D [rule_format, WT_intro]: "∀η. ℐ_inner η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √"
        and bound [rule_format, interaction_bound]: "∀η. interaction_bounded_by (λ_. True) (𝒟 η) (bound_outer η)"
        and lossless [rule_format]: "∀η. lossless_outer ∨ lossless_inner ⟶ plossless_gpv (ℐ_inner η ⊕⇩ℐ ℐ_common η) (𝒟 η)"

      let ?cnv = "λη. cnv_inner η ⊙ cnv_outer η"

      have bound': "interaction_any_bounded_by (𝒟 η) (bound_inner η)" for η using bound[of η] bound_le[of η]
        by(clarsimp elim!: interaction_bounded_by_mono order_trans[rotated] simp add: max_def)
          (metis (full_types) linorder_linear more_arith_simps(6) mult_left_mono zero_le)
      from correct_inner[OF WT_D bound' lossless]
      have w1: "⋀η. wiring (ℐ_inner η) (ℐ_middle η) (cnv_inner η) (w1 η)"
        and adv1: "negligible (λη. advantage (𝒟 η) (ideal η) (cnv_inner η |⇩= 1⇩C ⊳ middle η))"
        by auto

      obtain f g where WT_inner [WT_intro]: "⋀η. ℐ_inner η, ℐ_middle η ⊢⇩C cnv_inner η √"
        and fg [simp]: "⋀η. w1 η = (f η, g η)"
        and eq1: "⋀η. ℐ_inner η, ℐ_middle η ⊢⇩C cnv_inner η ∼ map_converter id id (f η) (g η) 1⇩C"
        using w1
        apply(atomize_elim)
        apply(fold all_conj_distrib)
        apply(subst choice_iff[symmetric])+
        apply(fastforce elim!: wiring.cases)
        done

      from w1 have [WT_intro]: "ℐ_inner η, ℐ_middle η ⊢⇩C cnv_inner η √" for η by cases

      let ?𝒟 = "λη. absorb (𝒟 η) (map_converter id id (f η) (g η) 1⇩C |⇩= 1⇩C)"
      have ℐ: "ℐ_inner η ≤ map_ℐ (f η) (g η) (ℐ_middle η)" for η
        using eq_ℐ_converterD_WT1[OF eq1 WT_inner, of η] by(rule WT_map_converter_idD)
      with WT_converter_id have [WT_intro]: "ℐ_inner η, map_ℐ (f η) (g η) (ℐ_middle η) ⊢⇩C 1⇩C √" 
        for η by(rule WT_converter_mono) simp

      have WT_D': "ℐ_middle η ⊕⇩ℐ ℐ_common η ⊢g ?𝒟 η √" for η by(rule WT_intro | simp)+
      have bound': "interaction_any_bounded_by (?𝒟 η) (bound_outer η)" for η
        by(subst map_converter_id_move_left)(interaction_bound; simp)
      have [simp]: "plossless_converter (ℐ_inner η) (map_ℐ (f η) (g η) (ℐ_middle η)) 1⇩C " for η
        using plossless_id_converter _ ℐ[of η] by(rule plossless_converter_mono) auto
      from lossless
      have "plossless_gpv (ℐ_middle η ⊕⇩ℐ ℐ_common η) (?𝒟 η)" if lossless_outer for η
        by(rule plossless_gpv_absorb)(auto simp add: that intro!: WT_intro plossless_parallel_converter2 plossless_map_converter)
      from correct_outer[OF WT_D' bound' this]
      have w2: "⋀η. wiring (ℐ_middle η) (ℐ_real η) (cnv_outer η) (w2 η)"
        and adv2: "negligible (λη. advantage (?𝒟 η) (middle η) (cnv_outer η |⇩= 1⇩C ⊳ real η))"
        by auto
      from w2 have [WT_intro]: "ℐ_middle η, ℐ_real η ⊢⇩C cnv_outer η √" for η by cases

      show "wiring (ℐ_inner η) (ℐ_real η) (?cnv η) (w1 η ∘⇩w w2 η)" for η
        using w1 w2 by(rule wiring_comp_converterI)

      have eq1': "connect (𝒟 η) (cnv_inner η |⇩= 1⇩C ⊳ middle η) = connect (?𝒟 η) (middle η)" for η
        unfolding distinguish_attach[symmetric]
        by(rule connect_eq_resource_cong WT_intro eq_ℐ_attach_on' parallel_converter2_eq_ℐ_cong eq1 eq_ℐ_converter_reflI order_refl)+
      have eq2': "connect (?𝒟 η) (cnv_outer η |⇩= 1⇩C ⊳ real η) = connect (𝒟 η) (?cnv η |⇩= 1⇩C ⊙ 1⇩C ⊳ real η)" for η
        unfolding distinguish_attach[symmetric] attach_compose comp_converter_parallel2[symmetric]
        by(rule connect_eq_resource_cong WT_intro eq_ℐ_attach_on' parallel_converter2_eq_ℐ_cong eq1[symmetric] eq_ℐ_converter_reflI order_refl|simp)+

      show "negligible (λη. advantage (𝒟 η) (ideal η) (?cnv η |⇩= 1⇩C ⊳ real η))"
        using negligible_plus[OF adv1 adv2] unfolding advantage_def eq1' eq2' comp_converter_id_right
        by(rule negligible_le) simp
    qed
  }
qed

theorem (in constructive_security) lifting:
  assumes WT_conv [WT_intro]: "⋀η. ℐ_common' η, ℐ_common η ⊢⇩C conv η √"
    and bound [interaction_bound]: "⋀η. interaction_any_bounded_converter (conv η) (bound_conv η)"
    and bound_le: "⋀η. bound' η * max (bound_conv η) 1 ≤ bound η"
    and lossless [plossless_intro]: "⋀η. lossless ⟹ plossless_converter (ℐ_common' η) (ℐ_common η) (conv η)"
  shows "constructive_security
     (λη. 1⇩C |⇩= conv η ⊳ real_resource η) (λη. 1⇩C |⇩= conv η ⊳ ideal_resource η) sim
     ℐ_real ℐ_ideal ℐ_common' bound' lossless w"
proof
  fix 𝒜 :: "security ⇒ ('a + 'g, 'b + 'h) distinguisher"
  assume WT_𝒜 [WT_intro]: "ℐ_real η ⊕⇩ℐ ℐ_common' η ⊢g 𝒜 η √" for η
  assume bound_𝒜 [interaction_bound]: "interaction_any_bounded_by (𝒜 η) (bound' η)" for η
  assume lossless_𝒜 [plossless_intro]: "lossless ⟹ plossless_gpv (ℐ_real η ⊕⇩ℐ ℐ_common' η) (𝒜 η)" for η

  let ?𝒜 = "λη. absorb (𝒜 η) (1⇩C |⇩= conv η)"

  have ideal: "connect (𝒜 η) (sim η |⇩= 1⇩C ⊳ 1⇩C |⇩= conv η ⊳ ideal_resource η) = connect (?𝒜 η) (sim η |⇩= 1⇩C ⊳ ideal_resource η)" for η
    by(simp add: distinguish_attach[symmetric] attach_compose[symmetric] comp_converter_parallel2 comp_converter_id_left comp_converter_id_right)
  have real: "connect (𝒜 η) (1⇩C |⇩= conv η ⊳ real_resource η) = connect (?𝒜 η) (real_resource η)" for η
    by(simp add: distinguish_attach[symmetric])
  have "ℐ_real η ⊕⇩ℐ ℐ_common η ⊢g ?𝒜 η √" for η by(rule WT_intro)+
  moreover have "interaction_any_bounded_by (?𝒜 η) (bound η)" for η
    by interaction_bound_converter(use bound_le[of η] in ‹simp add: max.commute›)
  moreover have " plossless_gpv (ℐ_real η ⊕⇩ℐ ℐ_common η) (absorb (𝒜 η) (1⇩C |⇩= conv η))" if lossless for η
    by(rule plossless_intro WT_intro | simp add: that)+
  ultimately show "negligible (λη. advantage (𝒜 η) (sim η |⇩= 1⇩C ⊳ 1⇩C |⇩= conv η ⊳ ideal_resource η) (1⇩C |⇩= conv η ⊳ real_resource η))"
    unfolding advantage_def ideal real by(rule adv[unfolded advantage_def])
next
  from correct obtain cnv 
    where correct': "⋀𝒟. ⟦ ⋀η. ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √;
          ⋀η. interaction_any_bounded_by (𝒟 η) (bound η);
          ⋀η. lossless ⟹ plossless_gpv (ℐ_ideal η ⊕⇩ℐ ℐ_common η) (𝒟 η) ⟧
          ⟹ (∀η. wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)) ∧
              negligible (λη. advantage (𝒟 η) (ideal_resource η) (cnv η |⇩= 1⇩C ⊳ real_resource η))"
    by blast
  show "∃cnv. ∀𝒟. (∀η. ℐ_ideal η ⊕⇩ℐ ℐ_common' η ⊢g 𝒟 η √) ⟶
         (∀η. interaction_any_bounded_by (𝒟 η) (bound' η)) ⟶
         (∀η. lossless ⟶ plossless_gpv (ℐ_ideal η ⊕⇩ℐ ℐ_common' η) (𝒟 η)) ⟶
         (∀η. wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)) ∧
         negligible (λη. advantage (𝒟 η) (1⇩C |⇩= conv η ⊳ ideal_resource η) (cnv η |⇩= 1⇩C ⊳ 1⇩C |⇩= conv η ⊳ real_resource η))"
  proof(intro exI conjI strip)
    fix 𝒟 :: "security ⇒ ('c + 'g, 'd + 'h) distinguisher"
    assume WT_D [rule_format, WT_intro]: "∀η. ℐ_ideal η ⊕⇩ℐ ℐ_common' η ⊢g 𝒟 η √"
      and bound [rule_format, interaction_bound]: "∀η. interaction_bounded_by (λ_. True) (𝒟 η) (bound' η)"
      and lossless [rule_format]: "∀η. lossless ⟶ plossless_gpv (ℐ_ideal η ⊕⇩ℐ ℐ_common' η) (𝒟 η)"

    let ?𝒟 = "λη. absorb (𝒟 η) (1⇩C |⇩= conv η)"
    have WT_D' [WT_intro]: "ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢g ?𝒟 η √" for η by(rule WT_intro)+
    have bound': "interaction_any_bounded_by (?𝒟 η) (bound η)" for η
      by interaction_bound(use bound_le[of η] in ‹auto simp add: max_def split: if_split_asm›)
    have "plossless_gpv (ℐ_ideal η ⊕⇩ℐ ℐ_common η) (?𝒟 η)" if lossless for η
      by(rule lossless that WT_intro plossless_intro)+
    from correct'[OF WT_D' bound' this]
    have w1: "wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)" 
      and adv': "negligible (λη. advantage (?𝒟 η) (ideal_resource η) (cnv η |⇩= 1⇩C ⊳ real_resource η))" for η
      by auto
    show "wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)" for η by(rule w1)
    have "cnv η |⇩= 1⇩C ⊳ 1⇩C |⇩= conv η ⊳ real_resource η = 1⇩C |⇩= conv η ⊳ cnv η |⇩= 1⇩C ⊳ real_resource η" for η
      by(simp add: attach_compose[symmetric] comp_converter_parallel2 comp_converter_id_left comp_converter_id_right)
    with adv'
    show "negligible (λη. advantage (𝒟 η) (1⇩C |⇩= conv η ⊳ ideal_resource η) (cnv η |⇩= 1⇩C ⊳ 1⇩C |⇩= conv η ⊳ real_resource η))"
      by(simp add: advantage_def distinguish_attach[symmetric])
  qed
qed(rule WT_intro)+

theorem constructive_security_trivial:
  fixes res
  assumes [WT_intro]: "⋀η. ℐ η ⊕⇩ℐ ℐ_common η ⊢res res η √"
  shows "constructive_security res res (λ_. 1⇩C) ℐ ℐ ℐ_common bound lossless (λ_. (id, id))"
proof
  show "ℐ η ⊕⇩ℐ ℐ_common η ⊢res res η √" and "ℐ η, ℐ η ⊢⇩C 1⇩C √" for η by(rule WT_intro)+

  fix 𝒜 :: "security ⇒ ('a + 'b, 'c + 'd) distinguisher"
  assume WT [WT_intro]: "ℐ η ⊕⇩ℐ ℐ_common η ⊢g 𝒜 η √" for η
  have "connect (𝒜 η) (1⇩C |⇩= 1⇩C ⊳ res η) = connect (𝒜 η) (1⇩C ⊳ res η)" for η
    by(rule connect_eq_resource_cong[OF WT])(fastforce intro: WT_intro eq_ℐ_attach_on' parallel_converter2_id_id)+
  then show "negligible (λη. advantage (𝒜 η) (1⇩C |⇩= 1⇩C ⊳ res η) (res η))"
    unfolding advantage_def by simp
next
  show "∃cnv. ∀𝒟. (∀η. ℐ η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √) ⟶
         (∀η. interaction_any_bounded_by (𝒟 η) (bound η)) ⟶
         (∀η. lossless ⟶ plossless_gpv (ℐ η ⊕⇩ℐ ℐ_common η) (𝒟 η)) ⟶
         (∀η. wiring (ℐ η) (ℐ η) (cnv η) (id, id)) ∧
         negligible (λη. advantage (𝒟 η) (res η) (cnv η |⇩= 1⇩C ⊳ res η))"
  proof(intro exI strip conjI)
    fix 𝒟 :: "security ⇒ ('a + 'b, 'c + 'd) distinguisher"
    assume WT_D [rule_format, WT_intro]: "∀η. ℐ η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √"
      and bound [rule_format, interaction_bound]: "∀η. interaction_bounded_by (λ_. True) (𝒟 η) (bound η)"
      and lossless [rule_format]: "∀η. lossless ⟶ plossless_gpv (ℐ η ⊕⇩ℐ ℐ_common η) (𝒟 η)"
    show "wiring (ℐ η) (ℐ η) 1⇩C (id, id)" for η by simp
    have "connect (𝒟 η) (1⇩C |⇩= 1⇩C ⊳ res η) = connect (𝒟 η) (1⇩C ⊳ res η)" for η
      by(rule connect_eq_resource_cong)(rule WT_intro eq_ℐ_attach_on' parallel_converter2_id_id order_refl)+
    then show "negligible (λη. advantage (𝒟 η) (res η) (1⇩C |⇩= 1⇩C ⊳ res η))"
      by(auto simp add: advantage_def)
  qed
qed

theorem parallel_constructive_security:
  assumes "constructive_security real1 ideal1 sim1 ℐ_real1 ℐ_inner1 ℐ_common1 bound1 lossless1 w1"
  assumes "constructive_security real2 ideal2 sim2 ℐ_real2 ℐ_inner2 ℐ_common2 bound2 lossless2 w2"
    (* TODO: add symmetric case for lossless1/2 *)
    and lossless_real1 [plossless_intro]: "⋀η. lossless2 ⟹ lossless_resource (ℐ_real1 η ⊕⇩ℐ ℐ_common1 η) (real1 η)"
    and lossless_sim2 [plossless_intro]: "⋀η. lossless1 ⟹ plossless_converter (ℐ_real2 η) (ℐ_inner2 η) (sim2 η)"
    and lossless_ideal2 [plossless_intro]: "⋀η. lossless1 ⟹ lossless_resource (ℐ_inner2 η ⊕⇩ℐ ℐ_common2 η) (ideal2 η)"
  shows "constructive_security (λη. parallel_wiring ⊳ real1 η ∥ real2 η) (λη. parallel_wiring ⊳ ideal1 η ∥ ideal2 η) (λη. sim1 η |⇩= sim2 η) 
    (λη. ℐ_real1 η ⊕⇩ℐ ℐ_real2 η) (λη. ℐ_inner1 η ⊕⇩ℐ ℐ_inner2 η) (λη. ℐ_common1 η ⊕⇩ℐ ℐ_common2 η)
    (λη. min (bound1 η) (bound2 η)) (lossless1 ∨ lossless2) (λη. w1 η |⇩w w2 η)"
proof
  interpret sec1: constructive_security real1 ideal1 sim1 ℐ_real1 ℐ_inner1 ℐ_common1 bound1 lossless1 w1 by fact
  interpret sec2: constructive_security real2 ideal2 sim2 ℐ_real2 ℐ_inner2 ℐ_common2 bound2 lossless2 w2 by fact

  show "(ℐ_real1 η ⊕⇩ℐ ℐ_real2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η) ⊢res parallel_wiring ⊳ real1 η ∥ real2 η √"
    and "(ℐ_inner1 η ⊕⇩ℐ ℐ_inner2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η) ⊢res parallel_wiring ⊳ ideal1 η ∥ ideal2 η √"
    and "ℐ_real1 η ⊕⇩ℐ ℐ_real2 η, ℐ_inner1 η ⊕⇩ℐ ℐ_inner2 η ⊢⇩C sim1 η |⇩= sim2 η √" for η by(rule WT_intro)+

  fix 𝒜 :: "security ⇒ (('a + 'g) + 'b + 'h, ('c + 'i) + 'd + 'j) distinguisher"
  assume WT [WT_intro]: "(ℐ_real1 η ⊕⇩ℐ ℐ_real2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η) ⊢g 𝒜 η √" for η
  assume bound [interaction_bound]: "interaction_any_bounded_by (𝒜 η) (min (bound1 η) (bound2 η))" for η
  assume lossless [plossless_intro]: "lossless1 ∨ lossless2 ⟹ plossless_gpv ((ℐ_real1 η ⊕⇩ℐ ℐ_real2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η)) (𝒜 η)" for η

  let ?𝒜 = "λη. absorb (𝒜 η) (parallel_wiring ⊙ parallel_converter (converter_of_resource (real1 η)) 1⇩C)"

  have *:"ℐ_uniform (outs_ℐ ((ℐ_real1 η ⊕⇩ℐ ℐ_real2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η)))
     UNIV,(ℐ_real1 η ⊕⇩ℐ ℐ_common1 η) ⊕⇩ℐ (ℐ_inner2 η ⊕⇩ℐ ℐ_common2 η) ⊢⇩C
    ((1⇩C |⇩= sim2 η) |⇩= 1⇩C) ⊙ parallel_wiring ∼ ((1⇩C |⇩= sim2 η) |⇩= 1⇩C |⇩= 1⇩C) ⊙ parallel_wiring" for η
    by(rule eq_ℐ_comp_cong, rule eq_ℐ_converter_mono)
      (auto simp add: le_ℐ_def intro: parallel_converter2_eq_ℐ_cong eq_ℐ_converter_reflI WT_converter_parallel_converter2
        WT_converter_id sec2.WT_sim parallel_converter2_id_id[symmetric] eq_ℐ_converter_reflI WT_parallel_wiring)

  have **: "outs_ℐ ((ℐ_real1 η ⊕⇩ℐ ℐ_real2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η)) ⊢⇩R
    ((1⇩C |⇩= sim2 η) |⇩= 1⇩C |⇩= 1⇩C) ⊙ parallel_wiring ⊳ real1 η ∥ ideal2 η ∼
    parallel_wiring ⊙ (converter_of_resource (real1 η) |⇩∝ 1⇩C) ⊳ sim2 η |⇩= 1⇩C ⊳ ideal2 η" for η
    unfolding comp_parallel_wiring
    by(rule eq_resource_on_trans, rule eq_ℐ_attach_on[where conv'="parallel_wiring ⊙ (1⇩C |⇩= sim2 η |⇩= 1⇩C)"]
        , (rule WT_intro)+, rule eq_ℐ_comp_cong, rule eq_ℐ_converter_mono)
      (auto simp add: le_ℐ_def attach_compose attach_parallel2 attach_converter_of_resource_conv_parallel_resource
        intro: WT_intro parallel_converter2_eq_ℐ_cong parallel_converter2_id_id eq_ℐ_converter_reflI)

  have ideal2:
    "connect (𝒜 η) ((1⇩C |⇩= sim2 η) |⇩= 1⇩C ⊳ parallel_wiring ⊳ real1 η ∥ ideal2 η) =
     connect (?𝒜 η) (sim2 η |⇩= 1⇩C ⊳ ideal2 η)" for η
    unfolding distinguish_attach[symmetric]
  proof (rule connect_eq_resource_cong[OF WT, rotated], goal_cases)
    case 2
    then show ?case 
      by(subst attach_compose[symmetric], rule eq_resource_on_trans
          , rule eq_ℐ_attach_on[where conv'="((1⇩C |⇩= sim2 η) |⇩= 1⇩C |⇩= 1⇩C) ⊙ parallel_wiring"])
        ((rule WT_intro)+ | intro * | intro ** )+
  qed (rule WT_intro)+
  have real2: "connect (𝒜 η) (parallel_wiring ⊳ real1 η ∥ real2 η) = connect (?𝒜 η) (real2 η)" for η
    unfolding distinguish_attach[symmetric]
    by(simp add: attach_compose attach_converter_of_resource_conv_parallel_resource)
  have "ℐ_real2 η ⊕⇩ℐ ℐ_common2 η ⊢g ?𝒜 η √" for η by(rule WT_intro)+
  moreover have "interaction_any_bounded_by (?𝒜 η) (bound2 η)" for η
    by interaction_bound_converter simp
  moreover have "plossless_gpv (ℐ_real2 η ⊕⇩ℐ ℐ_common2 η) (?𝒜 η)" if "lossless2" for η 
    by(rule plossless_intro WT_intro | simp add: that)+
  ultimately
  have negl2: "negligible (λη. advantage (𝒜 η)
     ((1⇩C |⇩= sim2 η) |⇩= 1⇩C ⊳ parallel_wiring ⊳ real1 η ∥ ideal2 η)
     (parallel_wiring ⊳ real1 η ∥ real2 η))"
    unfolding advantage_def ideal2 real2 by(rule sec2.adv[unfolded advantage_def])

  let ?𝒜 = "λη. absorb (𝒜 η) (parallel_wiring ⊙ parallel_converter 1⇩C (converter_of_resource (sim2 η |⇩= 1⇩C ⊳ ideal2 η)))"
  have ideal1: 
    "connect (𝒜 η) ((sim1 η |⇩= sim2 η) |⇩= 1⇩C ⊳ parallel_wiring ⊳ ideal1 η ∥ ideal2 η) =
     connect (?𝒜 η) (sim1 η |⇩= 1⇩C ⊳ ideal1 η)" for η
  proof -
    have *: "ℐ_uniform ((outs_ℐ (ℐ_real1 η) <+> outs_ℐ (ℐ_real2 η)) <+>  outs_ℐ (ℐ_common1 η) <+> 
      outs_ℐ (ℐ_common2 η)) UNIV,(ℐ_inner1 η ⊕⇩ℐ ℐ_common1 η) ⊕⇩ℐ (ℐ_inner2 η ⊕⇩ℐ ℐ_common2 η) ⊢⇩C
    ((sim1 η |⇩= sim2 η) |⇩= 1⇩C) ⊙ parallel_wiring ∼ ((sim1 η |⇩= sim2 η) |⇩= 1⇩C |⇩= 1⇩C) ⊙ parallel_wiring"
      by(rule eq_ℐ_comp_cong, rule eq_ℐ_converter_mono)
        (auto simp add: le_ℐ_def comp_parallel_wiring' attach_compose attach_parallel2 attach_converter_of_resource_conv_parallel_resource2
          intro: WT_intro parallel_converter2_id_id[symmetric] eq_ℐ_converter_reflI parallel_converter2_eq_ℐ_cong eq_ℐ_converter_mono)

    have **:"((outs_ℐ (ℐ_real1 η) <+> outs_ℐ (ℐ_real2 η)) <+> outs_ℐ (ℐ_common1 η) <+> outs_ℐ (ℐ_common2 η)) ⊢⇩R
    (sim1 η |⇩= sim2 η) |⇩= 1⇩C ⊳ parallel_wiring ⊳ ideal1 η ∥ ideal2 η ∼
    parallel_wiring ⊙ (1⇩C |⇩∝ converter_of_resource (sim2 η |⇩= 1⇩C ⊳ ideal2 η)) ⊳  sim1 η |⇩= 1⇩C ⊳ ideal1 η"
      unfolding attach_compose[symmetric]
      by(rule eq_resource_on_trans, rule eq_ℐ_attach_on[where conv'="((sim1 η |⇩= sim2 η) |⇩= 1⇩C |⇩= 1⇩C) ⊙ parallel_wiring"])
        ((rule WT_intro)+ | intro * | auto simp add: le_ℐ_def comp_parallel_wiring' attach_compose 
          attach_parallel2 attach_converter_of_resource_conv_parallel_resource2 intro: WT_intro *)+

    show ?thesis
      unfolding distinguish_attach[symmetric] using WT
      by(rule connect_eq_resource_cong) (simp add: **, (rule WT_intro)+)
  qed

  have real1:
    "connect (𝒜 η) ((1⇩C |⇩= sim2 η) |⇩= 1⇩C ⊳ parallel_wiring ⊳ real1 η ∥ ideal2 η) =
     connect (?𝒜 η) (real1 η)" for η
  proof -
    have **: "ℐ_uniform (outs_ℐ ((ℐ_real1 η ⊕⇩ℐ ℐ_real2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η)))
     UNIV,(ℐ_real1 η ⊕⇩ℐ ℐ_common1 η) ⊕⇩ℐ (ℐ_inner2 η ⊕⇩ℐ ℐ_common2 η) ⊢⇩C
      ((1⇩C |⇩= sim2 η) |⇩= 1⇩C) ⊙ parallel_wiring ∼ ((1⇩C |⇩= sim2 η) |⇩= 1⇩C |⇩= 1⇩C) ⊙ parallel_wiring" 
      by(rule eq_ℐ_comp_cong, rule eq_ℐ_converter_mono)
        (auto simp add: le_ℐ_def intro: WT_intro parallel_converter2_eq_ℐ_cong WT_converter_parallel_converter2
          parallel_converter2_id_id[symmetric] eq_ℐ_converter_reflI WT_parallel_wiring)

    have *: "outs_ℐ ((ℐ_real1 η ⊕⇩ℐ ℐ_real2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η)) ⊢⇩R
    parallel_wiring ⊙ ((1⇩C |⇩= 1⇩C) |⇩= sim2 η |⇩= 1⇩C) ⊳ real1 η ∥ ideal2 η ∼
    parallel_wiring ⊙ (1⇩C |⇩∝ converter_of_resource (sim2 η |⇩= 1⇩C ⊳ ideal2 η)) ⊳ real1 η"
      by(rule eq_resource_on_trans, rule eq_ℐ_attach_on[where conv'="parallel_wiring ⊙ (1⇩C |⇩= sim2 η |⇩= 1⇩C)"]
          , (rule WT_intro)+, rule eq_ℐ_comp_cong, rule eq_ℐ_converter_mono)
        (auto simp add: le_ℐ_def attach_compose attach_converter_of_resource_conv_parallel_resource2 attach_parallel2 
          intro: WT_intro parallel_converter2_eq_ℐ_cong parallel_converter2_id_id eq_ℐ_converter_reflI)

    show ?thesis
      unfolding distinguish_attach[symmetric] using WT
      by(rule connect_eq_resource_cong, fold attach_compose)
        (rule eq_resource_on_trans[where res'="((1⇩C |⇩= sim2 η) |⇩= 1⇩C |⇩= 1⇩C) ⊙ parallel_wiring ⊳ real1 η ∥ ideal2 η"]
          , (rule eq_ℐ_attach_on, (intro * ** | subst comp_parallel_wiring | rule eq_ℐ_attach_on | (rule WT_intro eq_ℐ_attach_on)+ )+))
  qed

  have "ℐ_real1 η ⊕⇩ℐ ℐ_common1 η ⊢g ?𝒜 η √" for η by(rule WT_intro)+
  moreover have "interaction_any_bounded_by (?𝒜 η) (bound1 η)" for η
    by interaction_bound_converter simp
  moreover have "plossless_gpv (ℐ_real1 η ⊕⇩ℐ ℐ_common1 η) (?𝒜 η)" if "lossless1" for η 
    by(rule plossless_intro WT_intro | simp add: that)+
  ultimately
  have negl1: "negligible (λη. advantage (𝒜 η) 
     ((sim1 η |⇩= sim2 η) |⇩= 1⇩C ⊳ parallel_wiring ⊳ ideal1 η ∥ ideal2 η)
     ((1⇩C |⇩= sim2 η) |⇩= 1⇩C ⊳ parallel_wiring ⊳ real1 η ∥ ideal2 η))"
    unfolding advantage_def ideal1 real1 by(rule sec1.adv[unfolded advantage_def])

  from negligible_plus[OF negl1 negl2]
  show "negligible (λη. advantage (𝒜 η) ((sim1 η |⇩= sim2 η) |⇩= 1⇩C ⊳ parallel_wiring ⊳ ideal1 η ∥ ideal2 η)
         (parallel_wiring ⊳ real1 η ∥ real2 η))"
    by(rule negligible_mono) (auto simp add: advantage_def intro!: eventuallyI landau_o.big_mono )
next
  interpret sec1: constructive_security real1 ideal1 sim1 ℐ_real1 ℐ_inner1 ℐ_common1 bound1 lossless1 w1 by fact
  interpret sec2: constructive_security real2 ideal2 sim2 ℐ_real2 ℐ_inner2 ℐ_common2 bound2 lossless2 w2 by fact
  from sec1.correct obtain cnv1
    where correct1: "⋀𝒟. ⟦ ⋀η. ℐ_inner1 η ⊕⇩ℐ ℐ_common1 η ⊢g 𝒟 η √;
      ⋀η. interaction_any_bounded_by (𝒟 η) (bound1 η);
      ⋀η. lossless1 ⟹ plossless_gpv (ℐ_inner1 η ⊕⇩ℐ ℐ_common1 η) (𝒟 η) ⟧
     ⟹ (∀η. wiring (ℐ_inner1 η) (ℐ_real1 η) (cnv1 η) (w1 η)) ∧
         negligible (λη. advantage (𝒟 η) (ideal1 η) (cnv1 η |⇩= 1⇩C ⊳ real1 η))"
    by blast
  from sec2.correct obtain cnv2
    where correct2: "⋀𝒟. ⟦ ⋀η. ℐ_inner2 η ⊕⇩ℐ ℐ_common2 η ⊢g 𝒟 η √;
      ⋀η. interaction_any_bounded_by (𝒟 η) (bound2 η);
      ⋀η. lossless2 ⟹ plossless_gpv (ℐ_inner2 η ⊕⇩ℐ ℐ_common2 η) (𝒟 η) ⟧
     ⟹ (∀η. wiring (ℐ_inner2 η) (ℐ_real2 η) (cnv2 η) (w2 η)) ∧
         negligible (λη. advantage (𝒟 η) (ideal2 η) (cnv2 η |⇩= 1⇩C ⊳ real2 η))"
    by blast
  show "∃cnv. ∀𝒟. (∀η. (ℐ_inner1 η ⊕⇩ℐ ℐ_inner2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η) ⊢g 𝒟 η √) ⟶
       (∀η. interaction_any_bounded_by (𝒟 η) (min (bound1 η) (bound2 η))) ⟶
       (∀η. lossless1 ∨ lossless2 ⟶ plossless_gpv ((ℐ_inner1 η ⊕⇩ℐ ℐ_inner2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η)) (𝒟 η)) ⟶
       (∀η. wiring (ℐ_inner1 η ⊕⇩ℐ ℐ_inner2 η) (ℐ_real1 η ⊕⇩ℐ ℐ_real2 η) (cnv η) (w1 η |⇩w w2 η)) ∧
       negligible (λη. advantage (𝒟 η) (parallel_wiring ⊳ ideal1 η ∥ ideal2 η) (cnv η |⇩= 1⇩C ⊳ parallel_wiring ⊳ real1 η ∥ real2 η))"
  proof(intro exI strip conjI)
    fix 𝒟 :: "security ⇒ (('e + 'k) + 'b + 'h, ('f + 'l) + 'd + 'j) distinguisher"
    assume WT_D [rule_format, WT_intro]: "∀η. (ℐ_inner1 η ⊕⇩ℐ ℐ_inner2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η) ⊢g 𝒟 η √"
      and bound [rule_format, interaction_bound]: "∀η. interaction_any_bounded_by (𝒟 η) (min (bound1 η) (bound2 η))"
      and lossless [rule_format, plossless_intro]: "∀η. lossless1 ∨ lossless2 ⟶ plossless_gpv ((ℐ_inner1 η ⊕⇩ℐ ℐ_inner2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η)) (𝒟 η)"

    let ?cnv = "λη. cnv1 η |⇩= cnv2 η"

    let ?𝒟1 = "λη. absorb (𝒟 η) (parallel_wiring ⊙ parallel_converter 1⇩C (converter_of_resource (ideal2 η)))"
    have WT1: "ℐ_inner1 η ⊕⇩ℐ ℐ_common1 η ⊢g ?𝒟1 η √" for η by(rule WT_intro)+
    have bound1: "interaction_any_bounded_by (?𝒟1 η) (bound1 η)" for η by interaction_bound simp
    have "plossless_gpv (ℐ_inner1 η ⊕⇩ℐ ℐ_common1 η) (?𝒟1 η)" if lossless1 for η
      by(rule plossless_intro WT_intro | simp add: that)+
    from correct1[OF WT1 bound1 this]
    have w1: "wiring (ℐ_inner1 η) (ℐ_real1 η) (cnv1 η) (w1 η)" 
      and adv1: "negligible (λη. advantage (?𝒟1 η) (ideal1 η) (cnv1 η |⇩= 1⇩C ⊳ real1 η))" for η
      by auto

    from w1 obtain f g where fg: "⋀η. w1 η = (f η, g η)"
      and [WT_intro]: "⋀η. ℐ_inner1 η, ℐ_real1 η ⊢⇩C cnv1 η √" 
      and eq1: "⋀η. ℐ_inner1 η, ℐ_real1 η ⊢⇩C cnv1 η ∼ map_converter id id (f η) (g η) 1⇩C"
      apply atomize_elim
      apply(fold all_conj_distrib)
      apply(subst choice_iff[symmetric])+
      apply(fastforce elim!: wiring.cases)
      done
    have ℐ1: "ℐ_inner1 η ≤ map_ℐ (f η) (g η) (ℐ_real1 η)" for η
      using eq_ℐ_converterD_WT1[OF eq1] by(rule WT_map_converter_idD)(rule WT_intro)
    with WT_converter_id order_refl have [WT_intro]: "ℐ_inner1 η, map_ℐ (f η) (g η) (ℐ_real1 η) ⊢⇩C 1⇩C √" for η
      by(rule WT_converter_mono)
    have lossless1 [plossless_intro]: "plossless_converter (ℐ_inner1 η) (ℐ_real1 η) (map_converter id id (f η) (g η) 1⇩C)" for η
      by(rule plossless_map_converter)(rule plossless_intro order_refl ℐ1 WT_intro plossless_converter_mono | simp)+

    let ?𝒟2 = "λη. absorb (𝒟 η) (parallel_wiring ⊙ parallel_converter (converter_of_resource (map_converter id id (f η) (g η) 1⇩C |⇩= 1⇩C ⊳ real1 η)) 1⇩C)"
    have WT2: "ℐ_inner2 η ⊕⇩ℐ ℐ_common2 η ⊢g ?𝒟2 η √" for η by(rule WT_intro | simp)+
    have bound2: "interaction_any_bounded_by (?𝒟2 η) (bound2 η)" for η by interaction_bound simp
    have "plossless_gpv (ℐ_inner2 η ⊕⇩ℐ ℐ_common2 η) (?𝒟2 η)" if lossless2 for η
      by(rule plossless_intro WT_intro | simp add: that)+
    from correct2[OF WT2 bound2 this]
    have w2: "wiring (ℐ_inner2 η) (ℐ_real2 η) (cnv2 η) (w2 η)" 
      and adv2: "negligible (λη. advantage (?𝒟2 η) (ideal2 η) (cnv2 η |⇩= 1⇩C ⊳ real2 η))" for η
      by auto

    from w2 have [WT_intro]: "ℐ_inner2 η, ℐ_real2 η ⊢⇩C cnv2 η √" for η by cases

    have *: "connect (𝒟 η) (?cnv η |⇩= 1⇩C ⊳ parallel_wiring ⊳ real1 η ∥ real2 η) =
      connect (?𝒟2 η) (cnv2 η |⇩= 1⇩C ⊳ real2 η)" for η
    proof -
      have "outs_ℐ ((ℐ_inner1 η ⊕⇩ℐ ℐ_inner2 η) ⊕⇩ℐ (ℐ_common1 η ⊕⇩ℐ ℐ_common2 η)) ⊢⇩R
         ?cnv η |⇩= 1⇩C ⊳ parallel_wiring ⊳ real1 η ∥ real2 η ∼ 
         (map_converter id id (f η) (g η) 1⇩C |⇩= cnv2 η) |⇩= (1⇩C |⇩= 1⇩C) ⊳ parallel_wiring ⊳ real1 η ∥ real2 η"
        by(rule eq_ℐ_attach_on' WT_intro parallel_converter2_eq_ℐ_cong eq1 eq_ℐ_converter_reflI parallel_converter2_id_id[symmetric])+ simp
      also have "(map_converter id id (f η) (g η) 1⇩C |⇩= cnv2 η) |⇩= (1⇩C |⇩= 1⇩C) ⊳ parallel_wiring ⊳ real1 η ∥ real2 η =
        parallel_wiring ⊳ (map_converter id id (f η) (g η) 1⇩C |⇩= 1⇩C ⊳ real1 η) ∥ (cnv2 η |⇩= 1⇩C ⊳ real2 η)"
        by(simp add: comp_parallel_wiring' attach_compose attach_parallel2)
      finally show ?thesis
        by(auto intro!: connect_eq_resource_cong[OF WT_D] intro: WT_intro simp add: distinguish_attach[symmetric] attach_compose attach_converter_of_resource_conv_parallel_resource)
    qed

    have **: "connect (?𝒟2 η) (ideal2 η) = connect (?𝒟1 η) (cnv1 η |⇩= 1⇩C ⊳ real1 η)" for η
    proof -
      have "connect (?𝒟2 η) (ideal2 η) = 
        connect (𝒟 η) (parallel_wiring ⊳ ((map_converter id id (f η) (g η) 1⇩C |⇩= 1⇩C) |⇩= 1⇩C) ⊳ (real1 η ∥ ideal2 η))"
        by(simp add: distinguish_attach[symmetric] attach_converter_of_resource_conv_parallel_resource attach_compose attach_parallel2)
      also have "… = connect (𝒟 η) (parallel_wiring ⊳ ((cnv1 η |⇩= 1⇩C) |⇩= 1⇩C) ⊳ (real1 η ∥ ideal2 η))"
        unfolding attach_compose[symmetric] using WT_D
        by(rule connect_eq_resource_cong[symmetric])
          (rule eq_ℐ_attach_on' WT_intro eq_ℐ_comp_cong eq_ℐ_converter_reflI parallel_converter2_eq_ℐ_cong eq1 | simp)+
      also have "… = connect (?𝒟1 η) (cnv1 η |⇩= 1⇩C ⊳ real1 η)"
        by(simp add: distinguish_attach[symmetric] attach_converter_of_resource_conv_parallel_resource2 attach_compose attach_parallel2)
      finally show ?thesis .
    qed

    have ***: "connect (?𝒟1 η) (ideal1 η) = connect (𝒟 η) (parallel_wiring ⊳ ideal1 η ∥ ideal2 η)" for η
      by(auto intro!: connect_eq_resource_cong[OF WT_D] simp add: attach_converter_of_resource_conv_parallel_resource2 distinguish_attach[symmetric] attach_compose intro: WT_intro)

    show "wiring (ℐ_inner1 η ⊕⇩ℐ ℐ_inner2 η) (ℐ_real1 η ⊕⇩ℐ ℐ_real2 η) (?cnv η) (w1 η |⇩w w2 η)" for η
      using w1 w2 by(rule wiring_parallel_converter2)
    from negligible_plus[OF adv1 adv2]
    show "negligible (λη. advantage (𝒟 η) (parallel_wiring ⊳ ideal1 η ∥ ideal2 η) (?cnv η |⇩= 1⇩C ⊳ parallel_wiring ⊳ real1 η ∥ real2 η))"
      by(rule negligible_le)(simp add: advantage_def * ** ***)
  qed
qed

theorem (in constructive_security) parallel_realisation1:
  assumes WT_res: "⋀η. ℐ_res η ⊕⇩ℐ ℐ_common' η ⊢res res η √"
    and lossless_res: "⋀η. lossless ⟹ lossless_resource (ℐ_res η ⊕⇩ℐ ℐ_common' η) (res η)"
  shows "constructive_security (λη. parallel_wiring ⊳ res η ∥ real_resource η)
    (λη. parallel_wiring ⊳ (res η ∥ ideal_resource η)) (λη. parallel_converter2 id_converter (sim η)) 
    (λη. ℐ_res η ⊕⇩ℐ ℐ_real η) (λη. ℐ_res η ⊕⇩ℐ ℐ_ideal η) (λη. ℐ_common' η ⊕⇩ℐ ℐ_common η) bound lossless (λη. (id, id) |⇩w w η)"
  by(rule parallel_constructive_security[OF constructive_security_trivial[where lossless=False and bound="λ_. ∞", OF WT_res], simplified, OF _ lossless_res])
    unfold_locales

theorem (in constructive_security) parallel_realisation2:
  assumes WT_res: "⋀η. ℐ_res η ⊕⇩ℐ ℐ_common' η ⊢res res η √"
    and lossless_res: "⋀η. lossless ⟹ lossless_resource (ℐ_res η ⊕⇩ℐ ℐ_common' η) (res η)"
  shows "constructive_security (λη. parallel_wiring ⊳ real_resource η ∥ res η)
    (λη. parallel_wiring ⊳ (ideal_resource η ∥ res η)) (λη. parallel_converter2 (sim η) id_converter) 
    (λη. ℐ_real η ⊕⇩ℐ ℐ_res η) (λη. ℐ_ideal η ⊕⇩ℐ ℐ_res η) (λη. ℐ_common η ⊕⇩ℐ ℐ_common' η) bound lossless (λη. w η |⇩w (id, id))"
  by(rule parallel_constructive_security[OF _ constructive_security_trivial[where lossless=False and bound="λ_. ∞", OF WT_res], simplified, OF _ lossless_res])
    unfold_locales

theorem (in constructive_security) parallel_resource1:
  assumes WT_res [WT_intro]: "⋀η. ℐ_res η ⊢res res η √"
    and lossless_res [plossless_intro]: "⋀η. lossless ⟹ lossless_resource (ℐ_res η) (res η)"
  shows "constructive_security (λη. parallel_resource1_wiring ⊳ res η ∥ real_resource η)
    (λη. parallel_resource1_wiring ⊳ res η ∥ ideal_resource η) sim 
    ℐ_real ℐ_ideal (λη. ℐ_res η ⊕⇩ℐ ℐ_common η) bound lossless w"
proof
  fix 𝒜 :: "security ⇒ ('a + 'g + 'e, 'b + 'h + 'f) distinguisher"
  assume WT [WT_intro]: "ℐ_real η ⊕⇩ℐ (ℐ_res η ⊕⇩ℐ ℐ_common η) ⊢g 𝒜 η √" for η
  assume bound [interaction_bound]: "interaction_any_bounded_by (𝒜 η) (bound η)" for η
  assume lossless [plossless_intro]: "lossless ⟹ plossless_gpv (ℐ_real η ⊕⇩ℐ (ℐ_res η ⊕⇩ℐ ℐ_common η)) (𝒜 η)" for η

  let ?𝒜 = "λη. absorb (𝒜 η) (swap_lassocr ⊙ parallel_converter (converter_of_resource (res η)) 1⇩C)"
  have ideal:
    "connect (𝒜 η) (sim η |⇩= 1⇩C ⊳ parallel_resource1_wiring ⊳ res η ∥ ideal_resource η) =
     connect (?𝒜 η) (sim η |⇩= 1⇩C ⊳ ideal_resource η)" for η
  proof -
    have[intro]: "ℐ_uniform (outs_ℐ (ℐ_real η) <+> outs_ℐ (ℐ_res η) <+> outs_ℐ (ℐ_common η))
     UNIV,ℐ_ideal η ⊕⇩ℐ (ℐ_res η ⊕⇩ℐ ℐ_common η) ⊢⇩C  sim η |⇩= 1⇩C ∼ sim η |⇩= 1⇩C |⇩= 1⇩C " 
      by(rule eq_ℐ_converter_mono) (auto simp add: le_ℐ_def intro!: 
          WT_intro parallel_converter2_id_id[symmetric] parallel_converter2_eq_ℐ_cong eq_ℐ_converter_reflI)

    have *: "outs_ℐ (ℐ_real η ⊕⇩ℐ (ℐ_res η ⊕⇩ℐ ℐ_common η)) ⊢⇩R  (sim η |⇩= 1⇩C) ⊙ parallel_resource1_wiring ⊳ res η ∥ ideal_resource η ∼
      swap_lassocr ⊙ (converter_of_resource (res η) |⇩∝ 1⇩C) ⊳ sim η |⇩= 1⇩C ⊳ ideal_resource η" 
      by (rule eq_resource_on_trans[where res'="(sim η |⇩= 1⇩C |⇩= 1⇩C) ⊙ parallel_resource1_wiring ⊳ res η ∥ ideal_resource η"], 
          rule eq_ℐ_attach_on, (rule  WT_intro)+, rule eq_ℐ_comp_cong)
        (auto simp add: parallel_resource1_wiring_def comp_swap_lassocr attach_compose attach_parallel2 
          attach_converter_of_resource_conv_parallel_resource intro!: WT_intro eq_ℐ_converter_reflI)  

    show ?thesis
      unfolding distinguish_attach[symmetric] using WT
      by(rule connect_eq_resource_cong, subst attach_compose[symmetric])
        (intro *, (rule WT_intro)+)
  qed
  have real:
    "connect (𝒜 η) (parallel_resource1_wiring ⊳ res η ∥ real_resource η) =
     connect (?𝒜 η) (real_resource η)" for η
    unfolding distinguish_attach[symmetric]
    by(simp add: attach_compose attach_converter_of_resource_conv_parallel_resource parallel_resource1_wiring_def)
  have "ℐ_real η ⊕⇩ℐ ℐ_common η ⊢g ?𝒜 η √" for η by(rule WT_intro)+
  moreover have "interaction_any_bounded_by (?𝒜 η) (bound η)" for η
    by interaction_bound_converter simp
  moreover have "plossless_gpv (ℐ_real η ⊕⇩ℐ ℐ_common η) (?𝒜 η)" if lossless for η 
    by(rule plossless_intro WT_intro | simp add: that)+
  ultimately show "negligible (λη. advantage (𝒜 η) (sim η |⇩= 1⇩C ⊳
                        parallel_resource1_wiring ⊳ res η ∥ ideal_resource η)
                       (parallel_resource1_wiring ⊳ res η ∥ real_resource η))"
    unfolding advantage_def ideal real by(rule adv[unfolded advantage_def])
next
  from correct obtain cnv 
    where correct': "⋀𝒟. ⟦ ⋀η. ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √;
          ⋀η. interaction_any_bounded_by (𝒟 η) (bound η);
          ⋀η. lossless ⟹ plossless_gpv (ℐ_ideal η ⊕⇩ℐ ℐ_common η) (𝒟 η) ⟧
          ⟹ (∀η. wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)) ∧
              negligible (λη. advantage (𝒟 η) (ideal_resource η) (cnv η |⇩= 1⇩C ⊳ real_resource η))"
    by blast
  show "∃cnv. ∀𝒟. (∀η. ℐ_ideal η ⊕⇩ℐ (ℐ_res η ⊕⇩ℐ ℐ_common η) ⊢g 𝒟 η √) ⟶
        (∀η. interaction_any_bounded_by (𝒟 η) (bound η)) ⟶
        (∀η. lossless ⟶ plossless_gpv (ℐ_ideal η ⊕⇩ℐ (ℐ_res η ⊕⇩ℐ ℐ_common η)) (𝒟 η)) ⟶
        (∀η. wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)) ∧
        negligible (λη. advantage (𝒟 η) (parallel_resource1_wiring ⊳ res η ∥ ideal_resource η)
          (cnv η |⇩= 1⇩C ⊳ parallel_resource1_wiring ⊳ res η ∥ real_resource η))"
  proof(intro exI conjI strip)
    fix 𝒟 :: "security ⇒ ('c + 'g + 'e, 'd + 'h + 'f) distinguisher"
    assume WT_D [rule_format, WT_intro]: "∀η. ℐ_ideal η ⊕⇩ℐ (ℐ_res η ⊕⇩ℐ ℐ_common η) ⊢g 𝒟 η √"
      and bound [rule_format, interaction_bound]: "∀η. interaction_any_bounded_by (𝒟 η) (bound η)"
      and lossless [rule_format, plossless_intro]: "∀η. lossless ⟶ plossless_gpv (ℐ_ideal η ⊕⇩ℐ (ℐ_res η ⊕⇩ℐ ℐ_common η)) (𝒟 η)"

    let ?𝒟 = "λη. absorb (𝒟 η) (swap_lassocr ⊙ parallel_converter (converter_of_resource (res η)) 1⇩C)"
    have WT': "ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢g ?𝒟 η √" for η by(rule WT_intro)+
    have bound': "interaction_any_bounded_by (?𝒟 η) (bound η)" for η by interaction_bound simp
    have lossless': "plossless_gpv (ℐ_ideal η ⊕⇩ℐ ℐ_common η) (?𝒟 η)" if lossless for η
      by(rule plossless_intro WT_intro that)+
    from correct'[OF WT' bound' lossless']
    have w: "wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)" 
      and adv: "negligible (λη. advantage (?𝒟 η) (ideal_resource η) (cnv η |⇩= 1⇩C ⊳ real_resource η))"
      for η by auto
    show  "wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)" for η by(rule w)
    from w have [WT_intro]: "ℐ_ideal η, ℐ_real η ⊢⇩C cnv η √" for η by cases
    have "connect (𝒟 η) (swap_lassocr ⊳ res η ∥ (cnv η |⇩= 1⇩C ⊳ real_resource η)) =
      connect (𝒟 η) (cnv η |⇩= 1⇩C ⊳ swap_lassocr ⊳ res η ∥ real_resource η)" for η
    proof -
      have "connect (𝒟 η) (cnv η |⇩= 1⇩C ⊳ swap_lassocr ⊳ res η ∥ real_resource η) =
        connect (𝒟 η) (cnv η |⇩= 1⇩C |⇩= 1⇩C ⊳ swap_lassocr ⊳ res η ∥ real_resource η)"
        by(rule connect_eq_resource_cong[OF WT_D])                                                                
          (rule eq_ℐ_attach_on' WT_intro parallel_converter2_eq_ℐ_cong eq_ℐ_converter_reflI parallel_converter2_id_id[symmetric] | simp)+
      also have "… = connect (𝒟 η) (swap_lassocr ⊳ res η ∥ (cnv η |⇩= 1⇩C ⊳ real_resource η))"
        by(simp add: comp_swap_lassocr' attach_compose attach_parallel2)
      finally show ?thesis by simp
    qed
    with adv show "negligible (λη. advantage (𝒟 η) (parallel_resource1_wiring ⊳ res η ∥ ideal_resource η)
          (cnv η |⇩= 1⇩C ⊳ parallel_resource1_wiring ⊳ res η ∥ real_resource η))"
      by(simp add: advantage_def distinguish_attach[symmetric] attach_compose attach_converter_of_resource_conv_parallel_resource parallel_resource1_wiring_def)
  qed
qed(rule WT_intro)+

end