Theory Wiring

section ‹Wiring›

theory Wiring imports
  Distinguisher
begin

subsection ‹Notation›
hide_const (open) Resumption.Pause Monomorphic_Monad.Pause Monomorphic_Monad.Done

no_notation Sublist.parallel (infixl "∥" 50)
no_notation plus_oracle (infix "⊕⇩O" 500)

notation Resource ("§R§")
notation Converter ("§C§")

alias RES = resource_of_oracle
alias CNV = converter_of_callee

alias id_intercept = "id_oracle"
notation id_oracle ("1⇩I")

notation plus_oracle (infixr "⊕⇩O" 504)
notation parallel_oracle (infixr "‡⇩O" 504)

notation plus_intercept (infixr "⊕⇩I" 504)
notation parallel_intercept (infixr "‡⇩I" 504)

notation parallel_resource (infixr "∥" 501) 

notation parallel_converter (infixr "|⇩∝" 501)
notation parallel_converter2 (infixr "|⇩=" 501)
notation comp_converter (infixr "⊙" 502)

notation fail_converter ("⊥⇩C")
notation id_converter ("1⇩C")

notation "attach" (infixr "⊳" 500)

subsection ‹Wiring primitives›

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

definition swap⇩C :: "('a + 'b, 'c + 'd, 'b + 'a, 'd + 'c) converter" where
  "swap⇩C = map_converter swap_sum swap_sum id id 1⇩C"

definition rassocl⇩C :: "('a + ('b + 'c), 'd + ('e + 'f), ('a + 'b) + 'c, ('d + 'e) + 'f) converter" where
  "rassocl⇩C = map_converter lsumr rsuml id id 1⇩C"
definition lassocr⇩C :: "(('a + 'b) + 'c, ('d + 'e) + 'f, 'a + ('b + 'c), 'd + ('e + 'f)) converter" where
  "lassocr⇩C = map_converter rsuml lsumr id id 1⇩C"

definition swap_rassocl where "swap_rassocl ≡ lassocr⇩C ⊙ (1⇩C |⇩= swap⇩C) ⊙ rassocl⇩C"
definition swap_lassocr where "swap_lassocr ≡ rassocl⇩C ⊙ (swap⇩C |⇩= 1⇩C) ⊙ lassocr⇩C"

definition parallel_wiring :: "(('a + 'b) + ('e + 'f), ('c + 'd) + ('g + 'h), ('a + 'e) + ('b + 'f), ('c + 'g) + ('d + 'h)) converter" where
  "parallel_wiring = lassocr⇩C ⊙ (1⇩C |⇩= swap_lassocr) ⊙ rassocl⇩C"

lemma WT_lassocr⇩C [WT_intro]: "(ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3, ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3) ⊢⇩C lassocr⇩C √"
  by(coinduction)(auto simp add: lassocr⇩C_def)

lemma WT_rassocl⇩C [WT_intro]: "ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3), (ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3 ⊢⇩C rassocl⇩C √"
  by(coinduction)(auto simp add: rassocl⇩C_def)

lemma WT_swap⇩C [WT_intro]: "ℐ1 ⊕⇩ℐ ℐ2, ℐ2 ⊕⇩ℐ ℐ1 ⊢⇩C swap⇩C √"
  by(coinduction)(auto simp add: swap⇩C_def)

lemma WT_swap_lassocr [WT_intro]: "ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3), ℐ2 ⊕⇩ℐ (ℐ1 ⊕⇩ℐ ℐ3) ⊢⇩C swap_lassocr √"
  unfolding swap_lassocr_def
  by(rule WT_converter_comp WT_lassocr⇩C WT_rassocl⇩C WT_converter_parallel_converter2 WT_converter_id WT_swap⇩C)+

lemma WT_swap_rassocl [WT_intro]: "(ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3, (ℐ1 ⊕⇩ℐ ℐ3) ⊕⇩ℐ ℐ2 ⊢⇩C swap_rassocl √"
  unfolding swap_rassocl_def
  by(rule WT_converter_comp WT_lassocr⇩C WT_rassocl⇩C WT_converter_parallel_converter2 WT_converter_id WT_swap⇩C)+

lemma WT_parallel_wiring [WT_intro]:
  "(ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ (ℐ3 ⊕⇩ℐ ℐ4), (ℐ1 ⊕⇩ℐ ℐ3) ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ4) ⊢⇩C parallel_wiring √"
  unfolding parallel_wiring_def 
  by(rule WT_converter_comp WT_lassocr⇩C WT_rassocl⇩C WT_converter_parallel_converter2 WT_converter_id WT_swap_lassocr)+

lemma map_swap_sum_plus_oracle: includes lifting_syntax shows
  "(id ---> swap_sum ---> map_spmf (map_prod swap_sum id)) (oracle1 ⊕⇩O oracle2) =
   (oracle2 ⊕⇩O oracle1)"
proof ((rule ext)+; goal_cases)
  case (1 s q)
  then show ?case by (cases q) (simp_all add: spmf.map_comp o_def apfst_def prod.map_comp id_def)
qed

lemma map_ℐ_rsuml_lsumr [simp]: "map_ℐ rsuml lsumr (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) = ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3)"
proof(rule ℐ_eqI[OF Set.set_eqI], goal_cases)
  case (1 x)
  then show ?case by(cases x rule: rsuml.cases) auto
qed (auto simp add: image_image)

lemma map_ℐ_lsumr_rsuml [simp]: "map_ℐ lsumr rsuml ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3) = (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3))"
proof(rule ℐ_eqI[OF Set.set_eqI], goal_cases)
  case (1 x)
  then show ?case by(cases x rule: lsumr.cases) auto
qed (auto simp add: image_image)

lemma map_ℐ_swap_sum [simp]: "map_ℐ swap_sum swap_sum (ℐ1 ⊕⇩ℐ ℐ2) = ℐ2 ⊕⇩ℐ ℐ1"
proof(rule ℐ_eqI[OF Set.set_eqI], goal_cases)
  case (1 x)
  then show ?case by(cases x) auto
qed (auto simp add: image_image)

definition parallel_resource1_wiring :: "('a + ('b + 'c), 'd + ('e + 'f), 'b + ('a + 'c), 'e + ('d + 'f)) converter" where
  "parallel_resource1_wiring = swap_lassocr"

lemma WT_parallel_resource1_wiring [WT_intro]: "ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3), ℐ2 ⊕⇩ℐ (ℐ1 ⊕⇩ℐ ℐ3) ⊢⇩C parallel_resource1_wiring √"
  unfolding parallel_resource1_wiring_def by(rule WT_swap_lassocr)

lemma plossless_rassocl⇩C [plossless_intro]: "plossless_converter (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3) rassocl⇩C"
  by coinduction (auto simp add: rassocl⇩C_def)

lemma plossless_lassocr⇩C [plossless_intro]: "plossless_converter ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3) (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) lassocr⇩C"
  by coinduction (auto simp add: lassocr⇩C_def)

lemma plossless_swap⇩C [plossless_intro]: "plossless_converter (ℐ1 ⊕⇩ℐ ℐ2) (ℐ2 ⊕⇩ℐ ℐ1) swap⇩C"
  by coinduction (auto simp add: swap⇩C_def)

lemma plossless_swap_lassocr [plossless_intro]:
  "plossless_converter (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) (ℐ2 ⊕⇩ℐ (ℐ1 ⊕⇩ℐ ℐ3)) swap_lassocr"
  unfolding swap_lassocr_def by(rule plossless_intro WT_intro)+

lemma rsuml_lsumr_parallel_converter2:
  "map_converter id id rsuml lsumr ((conv1 |⇩= conv2) |⇩= conv3) = 
   map_converter rsuml lsumr id id (conv1 |⇩= conv2 |⇩= conv3)"
  by(coinduction arbitrary: conv1 conv2 conv3, clarsimp split!: sum.split simp add: rel_fun_def map_gpv_conv_map_gpv'[symmetric])
    ((subst left_gpv_map[where h=id] | subst right_gpv_map[where h=id])+
      , simp add:gpv.map_comp sum.map_id0 o_def prod.map_comp id_def[symmetric]
      , subst map_gpv'_map_gpv_swap, (subst rsuml_lsumr_left_gpv_left_gpv | subst rsuml_lsumr_left_gpv_right_gpv | subst rsuml_lsumr_right_gpv)
      , auto 4 4 intro!: gpv.rel_refl_strong simp add: gpv.rel_map)+

lemma comp_lassocr⇩C: "((conv1 |⇩= conv2) |⇩= conv3) ⊙ lassocr⇩C = lassocr⇩C ⊙ (conv1 |⇩= conv2 |⇩= conv3)"
  unfolding lassocr⇩C_def
  by(subst comp_converter_map_converter2)
    (simp add: comp_converter_id_right comp_converter_map1_out comp_converter_id_left rsuml_lsumr_parallel_converter2)

lemmas comp_lassocr⇩C' = comp_converter_eqs[OF comp_lassocr⇩C]

lemma lsumr_rsuml_parallel_converter2:
  "map_converter id id lsumr rsuml (conv1 |⇩= (conv2 |⇩= conv3)) = 
   map_converter lsumr rsuml id id ((conv1 |⇩= conv2) |⇩= conv3)"
  by(coinduction arbitrary: conv1 conv2 conv3, clarsimp split!: sum.split simp add: rel_fun_def map_gpv_conv_map_gpv'[symmetric])
    ((subst left_gpv_map[where h=id] | subst right_gpv_map[where h=id])+
      , simp add:gpv.map_comp sum.map_id0 o_def prod.map_comp id_def[symmetric]
      , subst map_gpv'_map_gpv_swap, (subst lsumr_rsuml_left_gpv | subst lsumr_rsuml_right_gpv_left_gpv | subst lsumr_rsuml_right_gpv_right_gpv)
      , auto 4 4 intro!: gpv.rel_refl_strong simp add: gpv.rel_map)+

lemma comp_rassocl⇩C:
  "(conv1 |⇩= conv2 |⇩= conv3) ⊙ rassocl⇩C = rassocl⇩C ⊙ ((conv1 |⇩= conv2) |⇩= conv3)"
  unfolding rassocl⇩C_def
  by(subst comp_converter_map_converter2)
    (simp add: comp_converter_id_right comp_converter_map1_out comp_converter_id_left lsumr_rsuml_parallel_converter2)

lemmas comp_rassocl⇩C' = comp_converter_eqs[OF comp_rassocl⇩C]

lemma swap_sum_right_gpv:
  "map_gpv' id swap_sum swap_sum (right_gpv gpv) = left_gpv gpv"
  by(coinduction arbitrary: gpv)
    (auto 4 3 simp add: spmf_rel_map generat.rel_map intro!: rel_spmf_reflI rel_generat_reflI rel_funI split: sum.split intro: exI[where x=Fail])

lemma swap_sum_left_gpv:
  "map_gpv' id swap_sum swap_sum (left_gpv gpv) = right_gpv gpv"
  by(coinduction arbitrary: gpv)
    (auto 4 3 simp add: spmf_rel_map generat.rel_map intro!: rel_spmf_reflI rel_generat_reflI rel_funI split: sum.split intro: exI[where x=Fail])

lemma swap_sum_parallel_converter2:
  "map_converter id id swap_sum swap_sum (conv1 |⇩= conv2) =
   map_converter swap_sum swap_sum id id (conv2 |⇩= conv1)"
  by(coinduction arbitrary: conv1 conv2, clarsimp simp add: rel_fun_def map_gpv_conv_map_gpv'[symmetric] split!: sum.split)
    (subst map_gpv'_map_gpv_swap, (subst swap_sum_right_gpv | subst swap_sum_left_gpv), 
      auto 4 4 intro!: gpv.rel_refl_strong simp add: gpv.rel_map)+

lemma comp_swap⇩C: "(conv1 |⇩= conv2) ⊙ swap⇩C = swap⇩C ⊙ (conv2 |⇩= conv1)"
  unfolding swap⇩C_def
  by(subst comp_converter_map_converter2)
    (simp add: comp_converter_id_right comp_converter_map1_out comp_converter_id_left swap_sum_parallel_converter2)

lemmas comp_swap⇩C' = comp_converter_eqs[OF comp_swap⇩C]

lemma comp_swap_lassocr: "(conv1 |⇩= conv2 |⇩= conv3) ⊙ swap_lassocr = swap_lassocr ⊙ (conv2 |⇩= conv1 |⇩= conv3)"
  unfolding swap_lassocr_def comp_rassocl⇩C' comp_converter_assoc comp_converter_parallel2' comp_swap⇩C' comp_converter_id_right
  by(subst (9) comp_converter_id_left[symmetric], subst comp_converter_parallel2[symmetric])
    (simp add: comp_converter_assoc comp_lassocr⇩C)

lemmas comp_swap_lassocr' = comp_converter_eqs[OF comp_swap_lassocr]

lemma comp_parallel_wiring:
  "((C1 |⇩= C2) |⇩= (C3 |⇩= C4)) ⊙ parallel_wiring = parallel_wiring ⊙ ((C1 |⇩= C3) |⇩= (C2 |⇩= C4))"
  unfolding parallel_wiring_def comp_lassocr⇩C' comp_converter_assoc comp_converter_parallel2' comp_swap_lassocr'
  by(subst comp_converter_id_right[THEN trans, OF comp_converter_id_left[symmetric]], subst comp_converter_parallel2[symmetric])
    (simp add: comp_converter_assoc comp_rassocl⇩C)

lemmas comp_parallel_wiring' = comp_converter_eqs[OF comp_parallel_wiring]

lemma attach_converter_of_resource_conv_parallel_resource:
  "converter_of_resource res |⇩∝ 1⇩C ⊳ res' = res ∥ res'"
  by(coinduction arbitrary: res res')
    (auto 4 3 simp add: rel_fun_def map_lift_spmf spmf.map_comp o_def prod.map_comp spmf_rel_map bind_map_spmf map_spmf_conv_bind_spmf[symmetric] split_def split!: sum.split intro!: rel_spmf_reflI)

lemma attach_converter_of_resource_conv_parallel_resource2:
  " 1⇩C |⇩∝ converter_of_resource res ⊳ res' = res' ∥ res"
  by(coinduction arbitrary: res res')
    (auto 4 3 simp add: rel_fun_def map_lift_spmf spmf.map_comp o_def prod.map_comp spmf_rel_map bind_map_spmf map_spmf_conv_bind_spmf[symmetric] split_def split!: sum.split intro!: rel_spmf_reflI)


lemma plossless_parallel_wiring [plossless_intro]:
  "plossless_converter ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ (ℐ3 ⊕⇩ℐ ℐ4)) ((ℐ1 ⊕⇩ℐ ℐ3) ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ4)) parallel_wiring"
  unfolding parallel_wiring_def by(rule plossless_intro WT_intro)+

lemma run_converter_lassocr [simp]:
  "run_converter lassocr⇩C x = Pause (rsuml x) (λx. Done (lsumr x, lassocr⇩C))"
  by(simp add: lassocr⇩C_def o_def)

lemma run_converter_rassocl [simp]:
  "run_converter rassocl⇩C x = Pause (lsumr x) (λx. Done (rsuml x, rassocl⇩C))"
  by(simp add: rassocl⇩C_def o_def)

lemma run_converter_swap [simp]: "run_converter swap⇩C x = Pause (swap_sum x) (λx. Done (swap_sum x, swap⇩C))"
  by(simp add: swap⇩C_def o_def)

definition lassocr_swap_sum where "lassocr_swap_sum = rsuml ∘ map_sum swap_sum id ∘ lsumr"

lemma run_converter_swap_lassocr [simp]:
  "run_converter swap_lassocr x = Pause (lassocr_swap_sum x) (
     case lsumr x of Inl _ ⇒ (λy. case lsumr y of Inl _ ⇒ Done (lassocr_swap_sum y, swap_lassocr) | _ ⇒ Fail)
          | Inr _ ⇒ (λy. case lsumr y of Inl _ ⇒ Fail | Inr _ ⇒ Done (lassocr_swap_sum y, swap_lassocr)))"
  by(subst sum.case_distrib[where h="λx. inline _ x _"] |
      simp add: bind_rpv_def inline_map_gpv split_def map_gpv_conv_bind[symmetric] swap_lassocr_def o_def cong del: sum.case_cong)+
    (cases x rule: lsumr.cases, simp_all add: o_def lassocr_swap_sum_def gpv.map_comp fun_eq_iff cong: sum.case_cong split: sum.split)

definition parallel_sum_wiring where "parallel_sum_wiring = lsumr ∘ map_sum id lassocr_swap_sum ∘ rsuml"

(* TODO: simplify the case distinctions *)
lemma run_converter_parallel_wiring:
  "run_converter parallel_wiring x = Pause (parallel_sum_wiring x) (
    case rsuml x of Inl _ ⇒ (λy. case rsuml y of Inl _ ⇒ Done (parallel_sum_wiring y, parallel_wiring) | _ ⇒ Fail)
                | Inr x ⇒ (case lsumr x of Inl _ ⇒ (λy. case rsuml y of Inl _ ⇒ Fail | Inr x ⇒ (case lsumr x of Inl _ ⇒ Done (parallel_sum_wiring y, parallel_wiring) | Inr _ ⇒ Fail))
                                          | Inr _ ⇒ (λy. case rsuml y of Inl _ ⇒ Fail | Inr x ⇒ (case lsumr x of Inl _ ⇒ Fail | Inr _ ⇒ Done (parallel_sum_wiring y, parallel_wiring)))))"
  by(simp add: parallel_wiring_def o_def cong del: sum.case_cong add: split_def map_gpv_conv_bind[symmetric])
    (subst sum.case_distrib[where h="λx. right_rpv x _"] |
      subst sum.case_distrib[where h="λx. inline _ x _"] |
      subst sum.case_distrib[where h=right_gpv] |
      (auto simp add: inline_map_gpv bind_rpv_def  gpv.map_comp fun_eq_iff parallel_sum_wiring_def 
        parallel_wiring_def[symmetric] sum.case_distrib o_def intro: sym cong del: sum.case_cong split!: sum.split))+

lemma bound_lassocr⇩C [interaction_bound]: "interaction_any_bounded_converter lassocr⇩C 1"
  unfolding lassocr⇩C_def by interaction_bound_converter simp

lemma bound_rassocl⇩C [interaction_bound]: "interaction_any_bounded_converter rassocl⇩C 1"
  unfolding rassocl⇩C_def by interaction_bound_converter simp

lemma bound_swap⇩C [interaction_bound]: "interaction_any_bounded_converter swap⇩C 1"
  unfolding swap⇩C_def by interaction_bound_converter simp

lemma bound_swap_rassocl [interaction_bound]: "interaction_any_bounded_converter swap_rassocl 1"
  unfolding swap_rassocl_def by interaction_bound_converter simp

lemma bound_swap_lassocr [interaction_bound]: "interaction_any_bounded_converter swap_lassocr 1"
  unfolding swap_lassocr_def by interaction_bound_converter simp

lemma bound_parallel_wiring [interaction_bound]: "interaction_any_bounded_converter parallel_wiring 1"
  unfolding parallel_wiring_def by interaction_bound_converter simp

subsection ‹Characterization of wirings›

type_synonym ('a, 'b, 'c, 'd) wiring = "('a ⇒ 'c) × ('d ⇒ 'b)"

inductive wiring :: "('a, 'b) ℐ ⇒ ('c, 'd) ℐ ⇒ ('a, 'b, 'c, 'd) converter ⇒ ('a, 'b, 'c, 'd) wiring ⇒ bool"
  for ℐ ℐ' cnv
  where
    wiring:
    "wiring ℐ ℐ' cnv (f, g)" if
    "ℐ,ℐ' ⊢⇩C cnv ∼ map_converter id id f g 1⇩C"
    "ℐ,ℐ' ⊢⇩C cnv √"

lemmas wiringI = wiring
hide_fact wiring

lemma wiringD:
  assumes "wiring ℐ ℐ' cnv (f, g)"
  shows wiringD_eq: "ℐ,ℐ' ⊢⇩C cnv ∼ map_converter id id f g 1⇩C"
    and wiringD_WT: "ℐ,ℐ' ⊢⇩C cnv √"
  using assms by(cases, blast)+

named_theorems wiring_intro "introduction rules for wiring"

definition apply_wiring :: "('a, 'b, 'c, 'd) wiring ⇒ ('s, 'c, 'd) oracle' ⇒ ('s, 'a, 'b) oracle'"
  where "apply_wiring = (λ(f, g). map_fun id (map_fun f (map_spmf (map_prod g id))))"

lemma apply_wiring_simps: "apply_wiring (f, g) = map_fun id (map_fun f (map_spmf (map_prod g id)))"
  by(simp add: apply_wiring_def)

lemma attach_wiring_resource_of_oracle:
  assumes wiring: "wiring ℐ1 ℐ2 conv fg"
    and WT: "ℐ2 ⊢res RES res s √"
    and outs: "outs_ℐ ℐ1 = UNIV"
  shows "conv ⊳ RES res s = RES (apply_wiring fg res) s"
  using wiring
proof cases
  case (wiring f g)
  have "ℐ_full,ℐ2 ⊢⇩C conv ∼ map_converter id id f g 1⇩C" using wiring(2)
    by(rule eq_ℐ_converter_mono)(simp_all add: le_ℐ_def outs)
  with WT have "conv ⊳ RES res s = map_converter id id f g 1⇩C ⊳ RES res s"
    by(rule eq_ℐ_attach)
  also have "… = RES (apply_wiring fg res) s"
    by(simp add: attach_map_converter map_resource_resource_of_oracle prod.map_id0 option.map_id0 map_fun_id apply_wiring_def wiring(1))
  finally show ?thesis .
qed

lemma wiring_id_converter [simp, wiring_intro]: "wiring ℐ ℐ 1⇩C (id, id)"
  using wiring.intros[of ℐ ℐ "1⇩C" id id]
  by(simp add: eq_ℐ_converter_reflI)

lemma apply_wiring_id [simp]: "apply_wiring (id, id) res = res"
  by(simp add: apply_wiring_simps prod.map_id0 option.map_id0 map_fun_id)

definition attach_wiring :: "('a, 'b, 'c, 'd) wiring ⇒ ('s ⇒ 'c ⇒ ('d × 's, 'e, 'f) gpv) ⇒ ('s ⇒ 'a ⇒ ('b × 's, 'e, 'f) gpv)"
  where "attach_wiring = (λ(f, g). map_fun id (map_fun f (map_gpv (map_prod g id) id)))"

lemma attach_wiring_simps: "attach_wiring (f, g) = map_fun id (map_fun f (map_gpv (map_prod g id) id))"
  by(simp add: attach_wiring_def)

lemma comp_wiring_converter_of_callee:
  assumes wiring: "wiring ℐ1 ℐ2 conv w"
    and WT: "ℐ2, ℐ3 ⊢⇩C CNV callee s √"
  shows "ℐ1, ℐ3 ⊢⇩C conv ⊙ CNV callee s ∼ CNV (attach_wiring w callee) s"
  using wiring
proof cases
  case (wiring f g)
  from wiring(2) have "ℐ1,ℐ3 ⊢⇩C conv ⊙ CNV callee s ∼ map_converter id id f g 1⇩C ⊙ CNV callee s"
    by(rule eq_ℐ_comp_cong)(rule eq_ℐ_converter_reflI[OF WT])
  also have "map_converter id id f g 1⇩C ⊙ CNV callee s = map_converter f g id id (CNV callee s)"
    by(subst comp_converter_map_converter1)(simp add: comp_converter_id_left)
  also have "… = CNV (attach_wiring w callee) s"
    by(simp add: map_converter_of_callee attach_wiring_simps wiring(1) map_gpv_conv_map_gpv')
  finally show ?thesis .
qed

definition comp_wiring :: "('a, 'b, 'c, 'd) wiring ⇒ ('c, 'd, 'e, 'f) wiring ⇒ ('a, 'b, 'e, 'f) wiring" (infixl "∘⇩w" 55)
  where "comp_wiring = (λ(f, g) (f', g'). (f' ∘ f, g ∘ g'))"

lemma comp_wiring_simps: "comp_wiring (f, g) (f', g') = (f' ∘ f, g ∘ g')"
  by(simp add: comp_wiring_def)

lemma wiring_comp_converterI [wiring_intro]:
  "wiring ℐ ℐ'' (conv1 ⊙ conv2) (fg ∘⇩w fg')" if "wiring ℐ ℐ' conv1 fg" "wiring ℐ' ℐ'' conv2 fg'"
proof -
  from that(1) obtain f g
    where conv1: "ℐ,ℐ' ⊢⇩C conv1 ∼ map_converter id id f g 1⇩C"
      and WT1: "ℐ, ℐ' ⊢⇩C conv1 √"
      and [simp]: "fg = (f, g)"
    by cases
  from that(2) obtain f' g' 
    where conv2: "ℐ',ℐ'' ⊢⇩C conv2 ∼ map_converter id id f' g' 1⇩C"
      and WT2: "ℐ', ℐ'' ⊢⇩C conv2 √"
      and [simp]: "fg' = (f', g')"
    by cases
  have *: "(fg ∘⇩w fg') = (f' ∘ f, g ∘ g')" by(simp add: comp_wiring_simps)
  have "ℐ,ℐ'' ⊢⇩C conv1 ⊙ conv2 ∼ map_converter id id f g 1⇩C ⊙ map_converter id id f' g' 1⇩C"
    using conv1 conv2 by(rule eq_ℐ_comp_cong)
  also have "map_converter id id f g 1⇩C ⊙ map_converter id id f' g' 1⇩C = map_converter id id (f' ∘ f) (g ∘ g') 1⇩C"
    by(simp add: comp_converter_map_converter2 comp_converter_id_right)
  also have "ℐ,ℐ'' ⊢⇩C conv1 ⊙ conv2 √" using WT1 WT2 by(rule WT_converter_comp)
  ultimately show ?thesis unfolding * ..
qed

definition parallel2_wiring
  :: "('a, 'b, 'c, 'd) wiring ⇒ ('a', 'b', 'c', 'd') wiring
   ⇒ ('a + 'a', 'b + 'b', 'c + 'c', 'd + 'd') wiring" (infix "|⇩w" 501) where
  "parallel2_wiring = (λ(f, g) (f', g'). (map_sum f f', map_sum g g'))"

lemma parallel2_wiring_simps:
  "parallel2_wiring (f, g) (f', g') = (map_sum f f', map_sum g g')"
  by(simp add: parallel2_wiring_def)

lemma wiring_parallel_converter2 [simp, wiring_intro]:
  assumes "wiring ℐ1 ℐ1' conv1 fg"
    and "wiring ℐ2 ℐ2' conv2 fg'"
  shows "wiring (ℐ1 ⊕⇩ℐ ℐ2) (ℐ1' ⊕⇩ℐ ℐ2') (conv1 |⇩= conv2) (fg |⇩w fg')"
proof -
  from assms(1) obtain f1 g1
    where conv1: "ℐ1,ℐ1' ⊢⇩C conv1 ∼ map_converter id id f1 g1 1⇩C"
      and WT1: "ℐ1, ℐ1' ⊢⇩C conv1 √"
      and [simp]: "fg = (f1, g1)"
    by cases
  from assms(2) obtain f2 g2 
    where conv2: "ℐ2,ℐ2' ⊢⇩C conv2 ∼ map_converter id id f2 g2 1⇩C"
      and WT2: "ℐ2, ℐ2' ⊢⇩C conv2 √"
      and [simp]: "fg' = (f2, g2)"
    by cases
  from eq_ℐ_converterD_WT1[OF conv1 WT1] have ℐ1: "ℐ1 ≤ map_ℐ f1 g1 ℐ1'" by(rule WT_map_converter_idD)
  from eq_ℐ_converterD_WT1[OF conv2 WT2] have ℐ2: "ℐ2 ≤ map_ℐ f2 g2 ℐ2'" by(rule WT_map_converter_idD)
  have WT': "ℐ1 ⊕⇩ℐ ℐ2, ℐ1' ⊕⇩ℐ ℐ2' ⊢⇩C map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1⇩C √"
    by(auto intro!: WT_converter_map_converter WT_converter_mono[OF WT_converter_id order_refl] ℐ1 ℐ2)
  have "ℐ1 ⊕⇩ℐ ℐ2, ℐ1' ⊕⇩ℐ ℐ2' ⊢⇩C conv1 |⇩= conv2 ∼ map_converter id id f1 g1 1⇩C |⇩= map_converter id id f2 g2 1⇩C"
    using conv1 conv2 by(rule parallel_converter2_eq_ℐ_cong)
  also have "map_converter id id f1 g1 1⇩C |⇩= map_converter id id f2 g2 1⇩C = (1⇩C |⇩= 1⇩C) ⊙ map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1⇩C"
    by(simp add: parallel_converter2_map2_out parallel_converter2_map1_out map_sum.comp sum.map_id0 comp_converter_map_converter2[of _ id id, simplified] comp_converter_id_right)
  also have "ℐ1 ⊕⇩ℐ ℐ2, ℐ1' ⊕⇩ℐ ℐ2' ⊢⇩C … ∼ 1⇩C ⊙ map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1⇩C"
    by(rule eq_ℐ_comp_cong[OF parallel_converter2_id_id])(rule eq_ℐ_converter_reflI[OF WT'])
  finally show ?thesis using WT1 WT2
    by(auto simp add: parallel2_wiring_simps comp_converter_id_left intro!: wiringI WT_converter_parallel_converter2)
qed

lemma apply_parallel2 [simp]:
  "apply_wiring (fg |⇩w fg') (res1 ⊕⇩O res2) = (apply_wiring fg res1 ⊕⇩O apply_wiring fg' res2)"
proof -
  have[simp]: "fg = (f1, g1) ⟹ fg' = (f2, g2) ⟹
       map_spmf (map_prod (map_sum g1 g2) id) ((res1 ⊕⇩O res2) s (map_sum f1 f2 q)) =
       ((λs q. map_spmf (map_prod g1 id) (res1 s (f1 q))) ⊕⇩O (λs q. map_spmf (map_prod g2 id) (res2 s (f2 q)))) s q" for f1 g1 f2 g2 s q
    by(cases q)(simp_all add: spmf.map_comp o_def apfst_def prod.map_comp split!:sum.splits)

  show ?thesis 
    by(cases fg; cases fg') (clarsimp simp add: parallel2_wiring_simps apply_wiring_simps fun_eq_iff map_fun_def o_def)
qed

lemma apply_comp_wiring [simp]: "apply_wiring (fg ∘⇩w fg') res = apply_wiring fg (apply_wiring fg' res)"
  by(cases fg; cases fg')(simp add: comp_wiring_simps apply_wiring_simps map_fun_def fun_eq_iff spmf.map_comp prod.map_comp o_def id_def)

definition lassocr⇩w :: "(('a + 'b) + 'c, ('d + 'e) + 'f, 'a + ('b + 'c), 'd + ('e + 'f)) wiring" 
  where "lassocr⇩w = (rsuml, lsumr)"

definition rassocl⇩w :: "('a + ('b + 'c), 'd + ('e + 'f), ('a + 'b) + 'c, ('d + 'e) + 'f) wiring" 
  where "rassocl⇩w = (lsumr, rsuml)"

definition swap⇩w :: "('a + 'b, 'c + 'd, 'b + 'a, 'd + 'c) wiring" where 
  "swap⇩w = (swap_sum, swap_sum)"

lemma wiring_lassocr [simp, wiring_intro]:
  "wiring ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3) (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) lassocr⇩C lassocr⇩w"
  unfolding lassocr⇩C_def lassocr⇩w_def
  by(subst map_converter_id_move_right)(auto intro!: wiringI eq_ℐ_converter_reflI WT_converter_map_converter)

lemma wiring_rassocl [simp, wiring_intro]:
  "wiring (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3) rassocl⇩C rassocl⇩w"
  unfolding rassocl⇩C_def rassocl⇩w_def
  by(subst map_converter_id_move_right)(auto intro!: wiringI eq_ℐ_converter_reflI WT_converter_map_converter)

lemma wiring_swap [simp, wiring_intro]: "wiring (ℐ1 ⊕⇩ℐ ℐ2) (ℐ2 ⊕⇩ℐ ℐ1) swap⇩C swap⇩w"
  unfolding swap⇩C_def swap⇩w_def
  by(subst map_converter_id_move_right)(auto intro!: wiringI eq_ℐ_converter_reflI WT_converter_map_converter)

lemma apply_lassocr⇩w [simp]: "apply_wiring lassocr⇩w (res1 ⊕⇩O res2 ⊕⇩O res3) = (res1 ⊕⇩O res2) ⊕⇩O res3"
  by(simp add: apply_wiring_def lassocr⇩w_def map_rsuml_plus_oracle)

lemma apply_rassocl⇩w [simp]: "apply_wiring rassocl⇩w ((res1 ⊕⇩O res2) ⊕⇩O res3) = res1 ⊕⇩O res2 ⊕⇩O res3"
  by(simp add: apply_wiring_def rassocl⇩w_def map_lsumr_plus_oracle)

lemma apply_swap⇩w [simp]: "apply_wiring swap⇩w (res1 ⊕⇩O res2) = res2 ⊕⇩O res1"
  by(simp add: apply_wiring_def swap⇩w_def map_swap_sum_plus_oracle)

end