Theory Converter

theory Converter imports
  Resource
begin

section ‹Converters›

subsection ‹Type definition›

codatatype ('a, results'_converter: 'b, outs'_converter: 'out, 'in) converter
  = Converter (run_converter: "'a ⇒ ('b × ('a, 'b, 'out, 'in) converter, 'out, 'in) gpv")
  for map: map_converter'
    rel: rel_converter'
    pred: pred_converter'

lemma case_converter_conv_run_converter: "case_converter f conv = f (run_converter conv)"
  by(fact converter.case_eq_if)

subsection ‹Functor›

context 
  fixes a :: "'a ⇒ 'a'"
    and b :: "'b ⇒ 'b'"
    and out :: "'out ⇒ 'out'"
    and "inn" :: "'in ⇒ 'in'"
begin

primcorec map_converter :: "('a', 'b, 'out, 'in') converter ⇒ ('a, 'b', 'out', 'in) converter" where
  "run_converter (map_converter conv) = 
   map_gpv (map_prod b map_converter) out ∘ map_gpv' id id inn ∘ run_converter conv ∘ a"

lemma map_converter_sel [simp]:
  "run_converter (map_converter conv) a' = map_gpv' (map_prod b map_converter) out inn (run_converter conv (a a'))"
  by(simp add: map_gpv_conv_map_gpv' map_gpv'_comp)

declare map_converter.sel [simp del]

lemma map_converter_ctr [simp, code]:
  "map_converter (Converter f) = Converter (map_fun a (map_gpv' (map_prod b map_converter) out inn) f)"
  by(rule converter.expand; simp add: fun_eq_iff)

end

lemma map_converter_id14: "map_converter id b out id res = map_converter' b out res"
  by(coinduction arbitrary: res)
    (auto 4 3 intro!: rel_funI simp add: converter.map_sel gpv.rel_map map_gpv_conv_map_gpv'[symmetric] intro!: gpv.rel_refl_strong)

lemma map_converter_id [simp]: "map_converter id id id id conv = conv"
  by(simp add: map_converter_id14 converter.map_id)

lemma map_converter_compose [simp]:
  "map_converter a b f g (map_converter a' b' f' g' conv) = map_converter (a' ∘ a) (b ∘ b') (f ∘ f') (g' ∘ g) conv"
  by(coinduction arbitrary: conv)
    (auto 4 3 intro!: rel_funI gpv.rel_refl_strong simp add: rel_gpv_map_gpv' map_gpv'_comp o_def prod.map_comp)

functor converter: map_converter by(simp_all add: o_def fun_eq_iff)

subsection ‹Set functions with interfaces›

context fixes ℐ :: "('a, 'b) ℐ" and ℐ' :: "('out, 'in) ℐ" begin

qualified inductive outsp_converter :: "'out ⇒ ('a, 'b, 'out, 'in) converter ⇒ bool" for out where
  Out: "outsp_converter out conv" if "out ∈ outs_gpv ℐ' (run_converter conv a)" "a ∈ outs_ℐ ℐ"
| Cont: "outsp_converter out conv" 
if "(b, conv') ∈ results_gpv ℐ' (run_converter conv a)" "outsp_converter out conv'" "a ∈ outs_ℐ ℐ"

definition outs_converter :: "('a, 'b, 'out, 'in) converter ⇒ 'out set"
  where "outs_converter conv ≡ {x. outsp_converter x conv}"

qualified inductive resultsp_converter :: "'b ⇒ ('a, 'b, 'out, 'in) converter ⇒ bool" for b where
  Result: "resultsp_converter b conv"
if "(b, conv') ∈ results_gpv ℐ' (run_converter conv a)" "a ∈ outs_ℐ ℐ"
| Cont: "resultsp_converter b conv"
if "(b', conv') ∈ results_gpv ℐ' (run_converter conv a)" "resultsp_converter b conv'" "a ∈ outs_ℐ ℐ"

definition results_converter :: "('a, 'b, 'out, 'in) converter ⇒ 'b set"
  where "results_converter conv = {b. resultsp_converter b conv}"

end

lemma outsp_converter_outs_converter_eq [pred_set_conv]: "Converter.outsp_converter ℐ ℐ' x = (λconv. x ∈ outs_converter ℐ ℐ' conv)"
  by(simp add: outs_converter_def)

context begin
local_setup ‹Local_Theory.map_background_naming (Name_Space.mandatory_path "outs_converter")›

lemmas intros [intro?] = outsp_converter.intros[to_set]
  and Out = outsp_converter.Out[to_set]
  and Cont = outsp_converter.Cont[to_set]
  and induct [consumes 1, case_names Out Cont, induct set: outs_converter] = outsp_converter.induct[to_set]
  and cases [consumes 1, case_names Out Cont, cases set: outs_converter] = outsp_converter.cases[to_set]
  and simps = outsp_converter.simps[to_set]
end

inductive_simps outs_converter_Converter [to_set, simp]: "Converter.outsp_converter ℐ ℐ' x (Converter conv)"

lemma resultsp_converter_results_converter_eq [pred_set_conv]:
  "Converter.resultsp_converter ℐ ℐ' x = (λconv. x ∈ results_converter ℐ ℐ' conv)"
  by(simp add: results_converter_def)

context begin
local_setup ‹Local_Theory.map_background_naming (Name_Space.mandatory_path "results_converter")›

lemmas intros [intro?] = resultsp_converter.intros[to_set]
  and Result = resultsp_converter.Result[to_set]
  and Cont = resultsp_converter.Cont[to_set]
  and induct [consumes 1, case_names Result Cont, induct set: results_converter] = resultsp_converter.induct[to_set]
  and cases [consumes 1, case_names Result Cont, cases set: results_converter] = resultsp_converter.cases[to_set]
  and simps = resultsp_converter.simps[to_set]
end

inductive_simps results_converter_Converter [to_set, simp]: "Converter.resultsp_converter ℐ ℐ' x (Converter conv)"

subsection ‹Relator›

coinductive rel_converter 
  :: "('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool) ⇒ ('out ⇒ 'out' ⇒ bool) ⇒ ('in ⇒ 'in' ⇒ bool) 
  ⇒ ('a, 'c, 'out, 'in) converter ⇒ ('b, 'd, 'out', 'in') converter ⇒ bool"
  for A B C R where
    rel_converterI:
    "rel_fun A (rel_gpv'' (rel_prod B (rel_converter A B C R)) C R) (run_converter conv1) (run_converter conv2) 
  ⟹ rel_converter A B C R conv1 conv2"

lemma rel_converter_coinduct [consumes 1, case_names rel_converter, coinduct pred: rel_converter]:
  assumes "X conv1 conv2"
    and "⋀conv1 conv2. X conv1 conv2 ⟹
         rel_fun A (rel_gpv'' (rel_prod B (λconv1 conv2. X conv1 conv2 ∨ rel_converter A B C R conv1 conv2)) C R)
            (run_converter conv1) (run_converter conv2)"
  shows "rel_converter A B C R conv1 conv2"
  using assms(1) by(rule rel_converter.coinduct)(simp add: assms(2))

lemma rel_converter_simps [simp, code]:
  "rel_converter A B C R (Converter f) (Converter g) ⟷ 
  rel_fun A (rel_gpv'' (rel_prod B (rel_converter A B C R)) C R) f g" 
  by(subst rel_converter.simps) simp

lemma rel_converterD:
  "rel_converter A B C R conv1 conv2 
  ⟹ rel_fun A (rel_gpv'' (rel_prod B (rel_converter A B C R)) C R) (run_converter conv1) (run_converter conv2)"
  by(blast elim: rel_converter.cases)

lemma rel_converter_eq14: "rel_converter (=) B C (=) = rel_converter' B C" (is "?lhs = ?rhs")
proof(intro ext iffI)
  show "?rhs conv1 conv2" if "?lhs conv1 conv2" for conv1 conv2 using that
    by(coinduction arbitrary: conv1 conv2)(auto elim: rel_converter.cases simp add: rel_gpv_conv_rel_gpv'')
  show "?lhs conv1 conv2" if "?rhs conv1 conv2" for conv1 conv2 using that
    by(coinduction arbitrary: conv1 conv2)
      (auto 4 4 elim: converter.rel_cases intro: gpv.rel_mono_strong simp add: rel_fun_def rel_gpv_conv_rel_gpv''[symmetric])
qed

lemma rel_converter_eq [relator_eq]: "rel_converter (=) (=) (=) (=) = (=)"
  by(simp add: rel_converter_eq14 converter.rel_eq)

lemma rel_converter_mono [relator_mono]:
  assumes "A' ≤ A" "B ≤ B'" "C ≤ C'" "R' ≤ R"
  shows "rel_converter A B C R ≤ rel_converter A' B' C' R'"
proof
  show "rel_converter A' B' C' R' conv1 conv2" if "rel_converter A B C R conv1 conv2" for conv1 conv2 using that
    by(coinduct)(auto dest: rel_converterD elim!: rel_gpv''_mono[THEN predicate2D, rotated -1] prod.rel_mono_strong rel_fun_mono intro: assms[THEN predicate2D])
qed

lemma rel_converter_conversep: "rel_converter A¯¯ B¯¯ C¯¯ R¯¯ = (rel_converter A B C R)¯¯"
proof(intro ext iffI; simp)
  show "rel_converter A B C R conv1 conv2" if "rel_converter A¯¯ B¯¯ C¯¯ R¯¯ conv2 conv1"
    for A :: "'a1 ⇒ 'a2 ⇒ bool" and B :: "'b1 ⇒ 'b2 ⇒ bool" and C :: "'c1 ⇒ 'c2 ⇒ bool" and R :: "'r1 ⇒ 'r2 ⇒ bool"
      and conv2 conv1
    using that apply(coinduct)
    apply(drule rel_converterD)
    apply(rewrite in ⌑ conversep_iff[symmetric])
    apply(subst rel_fun_conversep[symmetric])
    apply(subst rel_gpv''_conversep[symmetric])
    apply(erule rel_fun_mono, blast)
    by(auto simp add: prod.rel_conversep[symmetric] rel_fun_def conversep_iff[abs_def]
        elim: prod.rel_mono_strong rel_gpv''_mono[THEN predicate2D, rotated -1])

  from this[of "A¯¯" "B¯¯" "C¯¯" "R¯¯"]
  show "rel_converter A¯¯ B¯¯ C¯¯ R¯¯ conv2 conv1" if "rel_converter A B C R conv1 conv2" for conv1 conv2
    using that by simp
qed

lemma rel_converter_map_converter'1:
  "rel_converter A B C R (map_converter' f g conv1) conv2 = rel_converter A (λx. B (f x)) (λx. C (g x)) R conv1 conv2"
  (is "?lhs = ?rhs")
proof
  show ?rhs if ?lhs using that
    by(coinduction arbitrary: conv1 conv2)
      (drule rel_converterD, auto intro: prod.rel_mono elim!: rel_fun_mono rel_gpv''_mono[THEN predicate2D, rotated -1]
        simp add: map_gpv'_id rel_gpv''_map_gpv map_converter.sel map_converter_id14[symmetric] rel_fun_comp spmf_rel_map prod.rel_map[abs_def])
  show ?lhs if ?rhs using that
    by(coinduction arbitrary: conv1 conv2)
      (drule rel_converterD, auto intro: prod.rel_mono elim!: rel_fun_mono rel_gpv''_mono[THEN predicate2D, rotated -1]
        simp add: map_gpv'_id rel_gpv''_map_gpv map_converter.sel map_converter_id14[symmetric] rel_fun_comp spmf_rel_map prod.rel_map[abs_def])
qed

lemma rel_converter_map_converter'2:
  "rel_converter A B C R conv1 (map_converter' f g conv2) = rel_converter A (λx y. B x (f y)) (λx y. C x (g y)) R conv1 conv2"
  using rel_converter_map_converter'1[of "conversep A" "conversep B" "conversep C" "conversep R" f g conv2 conv1]
  apply(rewrite in "⌑ = _" conversep_iff[symmetric])
  apply(rewrite in "_ = ⌑" conversep_iff[symmetric])
  apply(simp only: rel_converter_conversep[symmetric])
  apply(simp only: conversep_iff[abs_def])
  done

lemmas converter_rel_map' = rel_converter_map_converter'1[abs_def] rel_converter_map_converter'2

lemma rel_converter_pos_distr [relator_distr]:
  "rel_converter A B C R OO rel_converter A' B' C' R' ≤ rel_converter (A OO A') (B OO B') (C OO C') (R OO R')"
proof(rule predicate2I)
  show "rel_converter (A OO A') (B OO B') (C OO C') (R OO R') conv1 conv3"
    if "(rel_converter A B C R OO rel_converter A' B' C' R') conv1 conv3"
    for conv1 conv3 using that
    apply(coinduction arbitrary: conv1 conv3)
    apply(erule relcomppE)
    apply(drule rel_converterD)+
    apply(rule rel_fun_mono)
      apply(rule pos_fun_distr[THEN predicate2D])
      apply(erule (1) relcomppI)
     apply simp
    apply(rule rel_gpv''_mono[THEN predicate2D, rotated -1])
       apply(erule rel_gpv''_pos_distr[THEN predicate2D])
    by(auto simp add:  prod.rel_compp[symmetric] intro: prod.rel_mono)
qed

lemma left_unique_rel_converter:
  "⟦ left_total A; left_unique B; left_unique C; left_total R ⟧ ⟹ left_unique (rel_converter A B C R)"
  unfolding left_unique_alt_def left_total_alt_def rel_converter_conversep[symmetric]
  by(subst rel_converter_eq[symmetric], rule order_trans[OF rel_converter_pos_distr], erule (3) rel_converter_mono)

lemma right_unique_rel_converter:
  "⟦ right_total A; right_unique B; right_unique C; right_total R ⟧ ⟹ right_unique (rel_converter A B C R)"
  unfolding right_unique_alt_def right_total_alt_def rel_converter_conversep[symmetric]
  by(subst rel_converter_eq[symmetric], rule order_trans[OF rel_converter_pos_distr], erule (3) rel_converter_mono)

lemma bi_unique_rel_converter [transfer_rule]:
  "⟦ bi_total A; bi_unique B; bi_unique C; bi_total R ⟧ ⟹ bi_unique (rel_converter A B C R)"
  unfolding bi_unique_alt_def bi_total_alt_def by(blast intro: left_unique_rel_converter right_unique_rel_converter)


definition rel_witness_converter :: "('a ⇒ 'e ⇒ bool) ⇒ ('e ⇒ 'c ⇒ bool) ⇒ ('b ⇒ 'd ⇒ bool) ⇒ ('out ⇒ 'out' ⇒ bool) ⇒ ('in ⇒ 'in'' ⇒ bool) ⇒ ('in'' ⇒ 'in' ⇒ bool)
  ⇒ ('a, 'b, 'out, 'in) converter × ('c, 'd, 'out', 'in') converter ⇒ ('e, 'b × 'd, 'out × 'out', 'in'') converter" where
  "rel_witness_converter A A' B C R R' = corec_converter (λ(conv1, conv2).
   map_gpv (map_prod id Inr ∘ rel_witness_prod) id ∘ 
   rel_witness_gpv (rel_prod B (rel_converter (A OO A') B C (R OO R'))) C R R' ∘ 
   rel_witness_fun A A' (run_converter conv1, run_converter conv2))"

lemma rel_witness_converter_sel [simp]:
  "run_converter (rel_witness_converter A A' B C R R' (conv1, conv2)) =
   map_gpv (map_prod id (rel_witness_converter A A' B C R R') ∘ rel_witness_prod) id ∘ 
   rel_witness_gpv (rel_prod B (rel_converter (A OO A') B C (R OO R'))) C R R' ∘ 
   rel_witness_fun A A' (run_converter conv1, run_converter conv2)"
  by(auto simp add: rel_witness_converter_def o_def fun_eq_iff gpv.map_comp intro!: gpv.map_cong)

lemma assumes "rel_converter (A OO A') B C (R OO R') conv conv'"
  and A: "left_unique A" "right_total A"
  and A': "right_unique A'" "left_total A'"
  and R: "left_unique R" "right_total R"
  and R': "right_unique R'" "left_total R'"
shows rel_witness_converter1: "rel_converter A (λb (b', c). b = b' ∧ B b' c) (λc (c', d). c = c' ∧ C c' d) R conv (rel_witness_converter A A' B C R R' (conv, conv'))" (is "?thesis1")
  and rel_witness_converter2: "rel_converter A' (λ(b, c') c. c = c' ∧ B b c') (λ(c, d') d. d = d' ∧ C c d') R' (rel_witness_converter A A' B C R R' (conv, conv')) conv'" (is "?thesis2")
proof -
  show ?thesis1 using assms(1)
  proof(coinduction arbitrary: conv conv')
    case rel_converter
    from this[THEN rel_converterD] show ?case
      apply(simp add: rel_fun_comp)
      apply(erule rel_fun_mono[OF rel_witness_fun1[OF _ A A']]; clarsimp simp add: rel_gpv''_map_gpv)
      apply(erule rel_gpv''_mono[THEN predicate2D, rotated -1, OF rel_witness_gpv1[OF _ R R']]; auto)
      done
  qed
  show ?thesis2 using assms(1)
  proof(coinduction arbitrary: conv conv')
    case rel_converter
    from this[THEN rel_converterD] show ?case
      apply(simp add: rel_fun_comp)
      apply(erule rel_fun_mono[OF rel_witness_fun2[OF _ A A']]; clarsimp simp add: rel_gpv''_map_gpv)
      apply(erule rel_gpv''_mono[THEN predicate2D, rotated -1, OF rel_witness_gpv2[OF _ R R']]; auto)
      done
  qed
qed

lemma rel_converter_neg_distr [relator_distr]:
  assumes A: "left_unique A" "right_total A"
    and A': "right_unique A'" "left_total A'"
    and R: "left_unique R" "right_total R"
    and R': "right_unique R'" "left_total R'"
  shows "rel_converter (A OO A') (B OO B') (C OO C') (R OO R') ≤ rel_converter A B C R OO rel_converter A' B' C' R'"
proof(rule predicate2I relcomppI)+
  fix conv conv''
  assume *: "rel_converter (A OO A') (B OO B') (C OO C') (R OO R') conv conv''"
  let ?conv' = "map_converter' (relcompp_witness B B') (relcompp_witness C C') (rel_witness_converter A A' (B OO B') (C OO C') R R' (conv, conv''))"
  show "rel_converter A B C R conv ?conv'" using rel_witness_converter1[OF * A A' R R'] unfolding converter_rel_map'
    by(rule rel_converter_mono[THEN predicate2D, rotated -1]; clarify del: relcomppE elim!: relcompp_witness)
  show "rel_converter A' B' C' R' ?conv' conv''" using rel_witness_converter2[OF * A A' R R'] unfolding converter_rel_map'
    by(rule rel_converter_mono[THEN predicate2D, rotated -1]; clarify del: relcomppE elim!: relcompp_witness)
qed

lemma left_total_rel_converter:
  "⟦ left_unique A; right_total A; left_total B; left_total C; left_unique R; right_total R ⟧
  ⟹ left_total (rel_converter A B C R)"
  unfolding left_unique_alt_def left_total_alt_def rel_converter_conversep[symmetric]
  apply(subst rel_converter_eq[symmetric])
  apply(rule order_trans[rotated])
   apply(rule rel_converter_neg_distr; simp add: left_unique_alt_def)
  apply(rule rel_converter_mono; assumption)
  done

lemma right_total_rel_converter:
  "⟦ right_unique A; left_total A; right_total B; right_total C; right_unique R; left_total R ⟧
   ⟹ right_total (rel_converter A B C R)"
  unfolding right_unique_alt_def right_total_alt_def rel_converter_conversep[symmetric]
  apply(subst rel_converter_eq[symmetric])
  apply(rule order_trans[rotated])
   apply(rule rel_converter_neg_distr; simp add: right_unique_alt_def)
  apply(rule rel_converter_mono; assumption)
  done

lemma bi_total_rel_converter [transfer_rule]:
  "⟦ bi_total A; bi_unique A; bi_total B; bi_total C; bi_total R; bi_unique R ⟧ 
  ⟹ bi_total (rel_converter A B C R)"
  unfolding bi_total_alt_def bi_unique_alt_def
  by(blast intro: left_total_rel_converter right_total_rel_converter)

inductive pred_converter :: "'a set ⇒ ('b ⇒ bool) ⇒ ('out ⇒ bool) ⇒ 'in set ⇒ ('a, 'b, 'out, 'in) converter ⇒ bool"
  for A B C R conv where
    "pred_converter A B C R conv" if
    "∀x∈results_converter (ℐ_uniform A UNIV) (ℐ_uniform UNIV R) conv. B x" 
    "∀out∈outs_converter (ℐ_uniform A UNIV) (ℐ_uniform UNIV R) conv. C out"

lemma pred_gpv'_mono_weak: (* TODO: Generalize to R' ⊆ R *)
  "pred_gpv' A C R ≤ pred_gpv' A' C' R" if "A ≤ A'" "C ≤ C'"
  using that by(auto 4 3 simp add: pred_gpv'.simps)

lemma Domainp_rel_converter_le:
  "Domainp (rel_converter A B C R) ≤ pred_converter (Collect (Domainp A)) (Domainp B) (Domainp C) (Collect (Domainp R))"
  (is "?lhs ≤ ?rhs")
proof(intro predicate1I pred_converter.intros strip)
  fix conv
  assume *: "?lhs conv"  
  let ?ℐ = "ℐ_uniform (Collect (Domainp A)) UNIV" and ?ℐ' = "ℐ_uniform UNIV (Collect (Domainp R))"
  show "Domainp B x" if "x ∈ results_converter ?ℐ ?ℐ' conv" for x using that *
    apply(induction)
     apply clarsimp
     apply(erule rel_converter.cases; clarsimp)
     apply(drule (1) rel_funD)
     apply(drule Domainp_rel_gpv''_le[THEN predicate1D, OF DomainPI])
     apply(erule pred_gpv'.cases)
     apply fastforce
    apply clarsimp
    apply(erule rel_converter.cases; clarsimp)
    apply(drule (1) rel_funD)
    apply(drule Domainp_rel_gpv''_le[THEN predicate1D, OF DomainPI])
    apply(erule pred_gpv'.cases)
    apply fastforce
    done
  show "Domainp C x" if "x ∈ outs_converter ?ℐ ?ℐ' conv" for x using that *
    apply induction
     apply clarsimp
     apply(erule rel_converter.cases; clarsimp)
     apply(drule (1) rel_funD)
     apply(drule Domainp_rel_gpv''_le[THEN predicate1D, OF DomainPI])
     apply(erule pred_gpv'.cases)
     apply fastforce
    apply clarsimp
    apply(erule rel_converter.cases; clarsimp)
    apply(drule (1) rel_funD)
    apply(drule Domainp_rel_gpv''_le[THEN predicate1D, OF DomainPI])
    apply(erule pred_gpv'.cases)
    apply fastforce
    done
qed

lemma rel_converter_Grp:
  "rel_converter (BNF_Def.Grp UNIV f)¯¯ (BNF_Def.Grp B g) (BNF_Def.Grp C h) (BNF_Def.Grp UNIV k)¯¯ =
   BNF_Def.Grp {conv. results_converter (ℐ_uniform (range f) UNIV) (ℐ_uniform UNIV (range k)) conv ⊆ B ∧ 
    outs_converter (ℐ_uniform (range f) UNIV) (ℐ_uniform UNIV (range k)) conv ⊆ C}
    (map_converter f g h k)"
  (is "?lhs = ?rhs")
  including lifting_syntax
proof(intro ext GrpI iffI CollectI conjI subsetI)
  let ?ℐ = "ℐ_uniform (range f) UNIV" and ?ℐ' = "ℐ_uniform UNIV (range k)"
  fix conv conv'
  assume *: "?lhs conv conv'"
  then show "map_converter f g h k conv = conv'"
    apply(coinduction arbitrary: conv conv')
    apply(drule rel_converterD)
    apply(unfold map_converter.sel)
    apply(subst (2) map_fun_def[symmetric])
    apply(subst map_fun2_id)
    apply(subst rel_fun_comp)
    apply(rule rel_fun_map_fun1)
    apply(erule rel_fun_mono, simp)
    apply(simp add: gpv.rel_map)
    by (auto simp add: rel_gpv_conv_rel_gpv'' prod.rel_map intro!: predicate2I rel_gpv''_map_gpv'1
        elim!: rel_gpv''_mono[THEN predicate2D, rotated -1] prod.rel_mono_strong GrpE)
  show "b ∈ B" if "b ∈ results_converter ?ℐ ?ℐ' conv" for b using * that
    by - (drule Domainp_rel_converter_le[THEN predicate1D, OF DomainPI]
        , auto simp add: Domainp_conversep Rangep_Grp iff: Grp_iff elim: pred_converter.cases)
  show "out ∈ C" if "out ∈ outs_converter ?ℐ ?ℐ' conv" for out using * that
    by - (drule Domainp_rel_converter_le[THEN predicate1D, OF DomainPI]
        , auto simp add: Domainp_conversep Rangep_Grp iff: Grp_iff elim: pred_converter.cases)
next
  let ?abr1="λconv. results_converter (ℐ_uniform (range f) UNIV) (ℐ_uniform UNIV (range k)) conv ⊆ B"
  let ?abr2="λconv. outs_converter (ℐ_uniform (range f) UNIV) (ℐ_uniform UNIV (range k)) conv ⊆ C"

  fix conv conv'
  assume "?rhs conv conv'"
  hence  *: "conv' = map_converter f g h k conv" and f1: "?abr1 conv" and f2: "?abr2 conv" by(auto simp add: Grp_iff)

  have[intro]: "?abr1 conv ⟹ ?abr2 conv ⟹ z ∈ run_converter conv ` range f ⟹
       out ∈ outs_gpv (ℐ_uniform UNIV (range k)) z ⟹ BNF_Def.Grp C h out (h out)" for conv z out
    by(auto simp add: Grp_iff elim:  outs_converter.Out elim!: subsetD)

  from f1 f2 show "?lhs conv conv'" unfolding *
    apply(coinduction arbitrary: conv)
    apply(unfold map_converter.sel)
    apply(subst (2) map_fun_def[symmetric])
    apply(subst map_fun2_id)
    apply(subst rel_fun_comp)
    apply(rule rel_fun_map_fun2)
    apply(rule rel_fun_refl_eq_onp)
    apply(unfold map_gpv_conv_map_gpv' gpv.comp comp_id)
    apply(subst map_gpv'_id12)
    apply(rule rel_gpv''_map_gpv'2)
    apply(unfold rel_gpv''_map_gpv)
    apply(rule rel_gpv''_refl_eq_on)
     apply(simp add: prod.rel_map)
     apply(rule prod.rel_refl_strong)
      apply(clarsimp simp add: Grp_iff)
    by (auto intro: results_converter.Result results_converter.Cont outs_converter.Cont elim!: subsetD)
qed

context 
  includes lifting_syntax 
  notes [transfer_rule] = map_gpv_parametric'
begin

lemma Converter_parametric [transfer_rule]:
  "((A ===> rel_gpv'' (rel_prod B (rel_converter A B C R)) C R) ===> rel_converter A B C R) Converter Converter"
  by(rule rel_funI)(simp)

lemma run_converter_parametric [transfer_rule]:
  "(rel_converter A B C R ===> A ===> rel_gpv'' (rel_prod B (rel_converter A B C R)) C R)
  run_converter run_converter"
  by(rule rel_funI)(auto dest: rel_converterD)

lemma corec_converter_parametric [transfer_rule]:
  "((S ===> A ===> rel_gpv'' (rel_prod B (rel_sum (rel_converter A B C R) S)) C R) ===> S ===> rel_converter A B C R)
   corec_converter corec_converter"
proof((rule rel_funI)+, goal_cases)
  case (1 f g s1 s2)
  then show ?case 
    by(coinduction arbitrary: s1 s2)
      (drule 1(1)[THEN rel_funD]
        , auto 4 4 simp add: rel_fun_comp prod.rel_map[abs_def] rel_gpv''_map_gpv prod.rel_map split: sum.split 
        intro: prod.rel_mono elim!: rel_fun_mono rel_gpv''_mono[THEN predicate2D, rotated -1])
qed

lemma map_converter_parametric [transfer_rule]:
  "((A' ===> A) ===> (B ===> B') ===> (C ===> C') ===> (R' ===> R) ===> rel_converter A B C R ===> rel_converter A' B' C' R')
  map_converter map_converter"
  unfolding map_converter_def by(transfer_prover)

lemma map_converter'_parametric [transfer_rule]:
  "((B ===> B') ===> (C ===> C') ===> rel_converter (=) B C (=) ===> rel_converter (=) B' C' (=))
  map_converter' map_converter'"
  unfolding map_converter_id14[symmetric] by transfer_prover

lemma case_converter_parametric [transfer_rule]:
  "(((A ===> rel_gpv'' (rel_prod B (rel_converter A B C R)) C R) ===> X) ===> rel_converter A B C R ===> X)
  case_converter case_converter"
  unfolding case_converter_conv_run_converter by transfer_prover

end

subsection ‹Well-typing›

coinductive WT_converter :: "('a, 'b) ℐ ⇒ ('out, 'in) ℐ ⇒ ('a, 'b, 'out, 'in) converter ⇒ bool"
  ("_,/ _ ⊢⇩C/ _ √" [100, 0, 0] 99)
  for ℐ ℐ' where
    WT_converterI: "ℐ, ℐ' ⊢⇩C conv √" if
    "⋀q. q ∈ outs_ℐ ℐ ⟹ ℐ' ⊢g run_converter conv q √"
    "⋀q r conv'. ⟦ q ∈ outs_ℐ ℐ; (r, conv') ∈ results_gpv ℐ' (run_converter conv q) ⟧ ⟹ r ∈ responses_ℐ ℐ q ∧ ℐ, ℐ' ⊢⇩C conv' √"

lemma WT_converter_coinduct[consumes 1, case_names WT_converter, case_conclusion WT_converter WT_gpv results_gpv, coinduct pred: WT_converter]:
  assumes "X conv"
    and "⋀conv q r conv'. ⟦ X conv; q ∈ outs_ℐ ℐ ⟧
  ⟹ ℐ' ⊢g run_converter conv q √ ∧
      ((r, conv') ∈ results_gpv ℐ' (run_converter conv q) ⟶ r ∈ responses_ℐ ℐ q ∧ (X conv' ∨ ℐ, ℐ' ⊢⇩C conv' √))"
  shows "ℐ, ℐ' ⊢⇩C conv √"
  using assms(1) by(rule WT_converter.coinduct)(blast dest: assms(2))

lemma WT_converterD:
  assumes "ℐ, ℐ' ⊢⇩C conv √" "q ∈ outs_ℐ ℐ"
  shows WT_converterD_WT: "ℐ' ⊢g run_converter conv q √"
    and WT_converterD_results: "(r, conv') ∈ results_gpv ℐ' (run_converter conv q) ⟹ r ∈ responses_ℐ ℐ q ∧ ℐ, ℐ' ⊢⇩C conv' √"
  using assms by(auto elim: WT_converter.cases)

lemma WT_converterD':
  assumes "ℐ, ℐ' ⊢⇩C conv √" "q ∈ outs_ℐ ℐ"
  shows "ℐ' ⊢g run_converter conv q √ ∧ (∀(r, conv') ∈ results_gpv ℐ' (run_converter conv q). r ∈ responses_ℐ ℐ q ∧ ℐ, ℐ' ⊢⇩C conv' √)"
  using assms by(auto elim: WT_converter.cases)

lemma WT_converter_bot1 [simp]: "bot, ℐ ⊢⇩C conv √"
  by(rule WT_converter.intros) auto

lemma WT_converter_mono: 
  "⟦ ℐ1,ℐ2 ⊢⇩C conv √; ℐ1' ≤ ℐ1; ℐ2 ≤ ℐ2' ⟧  ⟹ ℐ1',ℐ2' ⊢⇩C conv √ "
  apply(coinduction arbitrary: conv)
  apply(auto)
    apply(drule WT_converterD_WT)
     apply(erule (1) outs_ℐ_mono[THEN subsetD])
    apply(erule WT_gpv_mono)
     apply(erule outs_ℐ_mono)
    apply(erule (1) responses_ℐ_mono)
   apply(frule WT_converterD_results)
     apply(erule (1) outs_ℐ_mono[THEN subsetD])
    apply(erule results_gpv_mono[THEN subsetD])
     apply(erule WT_converterD_WT)
     apply(erule (1) outs_ℐ_mono[THEN subsetD])
    apply simp
   apply clarify
   apply(erule (2) responses_ℐ_mono[THEN subsetD])
  apply(frule WT_converterD_results)
    apply(erule (1) outs_ℐ_mono[THEN subsetD])
   apply(erule results_gpv_mono[THEN subsetD])
    apply(erule WT_converterD_WT)
    apply(erule (1) outs_ℐ_mono[THEN subsetD])
   apply simp
  apply simp
  done

lemma callee_invariant_on_run_resource [simp]: "callee_invariant_on run_resource (WT_resource ℐ) ℐ"
  by(unfold_locales)(auto dest: WT_resourceD intro: WT_calleeI)

interpretation run_resource: callee_invariant_on run_resource "WT_resource ℐ" ℐ for ℐ
  by simp

lemma raw_converter_invariant_run_converter: "raw_converter_invariant ℐ ℐ' run_converter (WT_converter ℐ ℐ')"
  by(unfold_locales)(auto dest: WT_converterD)

interpretation run_converter: raw_converter_invariant ℐ ℐ' run_converter "WT_converter ℐ ℐ'" for ℐ ℐ'
  by(rule raw_converter_invariant_run_converter)

lemma WT_converter_ℐ_full: "ℐ_full, ℐ_full ⊢⇩C conv √"
  by(coinduction arbitrary: conv)(auto)

lemma WT_converter_map_converter [WT_intro]:
  "ℐ, ℐ' ⊢⇩C map_converter f g f' g' conv √" if 
  *: "map_ℐ (inv_into UNIV f) (inv_into UNIV g) ℐ, map_ℐ f' g' ℐ' ⊢⇩C conv √"
  and f: "inj f" and g: "surj g"
  using *
proof(coinduction arbitrary: conv)
  case (WT_converter q r conv' conv)
  have "?WT_gpv" using WT_converter
    by(auto intro!: WT_gpv_map_gpv' elim: WT_converterD_WT simp add: inv_into_f_f[OF f])
  moreover
  have "?results_gpv"
  proof(intro strip conjI disjI1)
    assume "(r, conv') ∈ results_gpv ℐ' (run_converter (map_converter f g f' g' conv) q)"
    then obtain r' conv''
      where results: "(r', conv'') ∈ results_gpv (map_ℐ f' g' ℐ') (run_converter conv (f q))"
        and r: "r = g r'"
        and conv': "conv' = map_converter f g f' g' conv''"
      by auto
    from WT_converterD_results[OF WT_converter(1), of "f q"] WT_converter(2) results 
    have r': "r' ∈ inv_into UNIV g ` responses_ℐ ℐ q"
      and WT': "map_ℐ (inv_into UNIV f) (inv_into UNIV g) ℐ, map_ℐ f' g' ℐ' ⊢⇩C conv'' √"
      by(auto simp add: inv_into_f_f[OF f])
    from r' r show "r ∈ responses_ℐ ℐ q" by(auto simp add: surj_f_inv_f[OF g])

    show "∃conv. conv' = map_converter f g f' g' conv ∧
       map_ℐ (inv_into UNIV f) (inv_into UNIV g) ℐ, map_ℐ f' g' ℐ' ⊢⇩C conv √"
      using conv' WT' by(auto)
  qed
  ultimately show ?case ..
qed


subsection ‹Losslessness›

coinductive plossless_converter :: "('a, 'b) ℐ ⇒ ('out, 'in) ℐ ⇒ ('a, 'b, 'out, 'in) converter ⇒ bool"
  for ℐ ℐ' where
    plossless_converterI: "plossless_converter ℐ ℐ' conv" if
    "⋀a. a ∈ outs_ℐ ℐ ⟹ plossless_gpv ℐ' (run_converter conv a)"
    "⋀a b conv'. ⟦ a ∈ outs_ℐ ℐ; (b, conv') ∈ results_gpv ℐ' (run_converter conv a) ⟧ ⟹ plossless_converter ℐ ℐ' conv'"

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

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

lemma plossless_converter_bot1 [simp]: "plossless_converter bot ℐ conv"
  by(rule plossless_converterI) auto

lemma plossless_converter_mono:
  assumes *: "plossless_converter ℐ1 ℐ2 conv"
    and le: "outs_ℐ ℐ1' ⊆ outs_ℐ ℐ1" "ℐ2 ≤ ℐ2'"
    and WT: "ℐ1, ℐ2 ⊢⇩C conv √"
  shows "plossless_converter ℐ1' ℐ2' conv"
  using * WT
  apply(coinduction arbitrary: conv)
  apply(drule plossless_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: plossless_gpv_mono[OF _ le(2)] results_gpv_mono[OF le(2), THEN subsetD] dest: bspec)

lemma raw_converter_invariant_run_plossless_converter: "raw_converter_invariant ℐ ℐ' run_converter (λconv. plossless_converter ℐ ℐ' conv ∧ ℐ,ℐ' ⊢⇩C conv √)"
  by(unfold_locales)(auto dest: WT_converterD plossless_converterD)

interpretation run_plossless_converter: raw_converter_invariant
  ℐ ℐ' run_converter "λconv. plossless_converter ℐ ℐ' conv ∧ ℐ,ℐ' ⊢⇩C conv √" for ℐ ℐ'
  by(rule raw_converter_invariant_run_plossless_converter)

named_theorems plossless_intro "Introduction rules for probabilistic losslessness"

subsection ‹Operations›

context
  fixes callee :: "'s ⇒ 'a ⇒ ('b × 's, 'out, 'in) gpv"
begin

primcorec converter_of_callee :: "'s ⇒ ('a, 'b, 'out, 'in) converter" where
  "run_converter (converter_of_callee s) = (λa. map_gpv (map_prod id converter_of_callee) id (callee s a))"

end

lemma converter_of_callee_parametric [transfer_rule]: includes lifting_syntax shows
  "((S ===> A ===> rel_gpv'' (rel_prod B S) C R) ===> S ===> rel_converter A B C R)
  converter_of_callee converter_of_callee"
  unfolding converter_of_callee_def supply map_gpv_parametric'[transfer_rule] by transfer_prover

lemma map_converter_of_callee:
  "map_converter f g h k (converter_of_callee callee s) =
   converter_of_callee (map_fun id (map_fun f (map_gpv' (map_prod g id) h k)) callee) s"
proof(coinduction arbitrary: s)
  case Eq_converter
  have *: "map_gpv' (map_prod g id) h k gpv = map_gpv (map_prod g id) id (map_gpv' id h k gpv)" for gpv
    by(simp add: map_gpv_conv_map_gpv' gpv.compositionality)
  show ?case
    by(auto simp add: rel_fun_def map_gpv'_map_gpv_swap gpv.rel_map * intro!: gpv.rel_refl_strong)
qed

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

text ‹
  We can define two versions of parallel composition. One that attaches to the same interface 
  and one that attach to different interfaces. We choose the one variant where both attach to the same interface
  because (1) this is more general and (2) we do not have to assume that the resource respects the parallel composition. 
›

primcorec parallel_converter
  :: "('a, 'b, 'out, 'in) converter ⇒ ('c, 'd, 'out, 'in) converter ⇒ ('a + 'c, 'b + 'd, 'out, 'in) converter"
  where
    "run_converter (parallel_converter conv1 conv2) = (λac. case ac of
     Inl a ⇒ map_gpv (map_prod Inl (λconv1'. parallel_converter conv1' conv2)) id (run_converter conv1 a)
   | Inr b ⇒ map_gpv (map_prod Inr (λconv2'. parallel_converter conv1 conv2')) id (run_converter conv2 b))"

lemma parallel_callee_parametric [transfer_rule]: includes lifting_syntax shows
  "(rel_converter A B C R ===> rel_converter A' B' C R ===> rel_converter (rel_sum A A') (rel_sum B B') C R)
   parallel_converter parallel_converter"
  unfolding parallel_converter_def supply map_gpv_parametric'[transfer_rule] by transfer_prover

lemma parallel_converter_assoc:
  "parallel_converter (parallel_converter conv1 conv2) conv3 =
   map_converter rsuml lsumr id id (parallel_converter conv1 (parallel_converter 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 plossless_parallel_converter [plossless_intro]:
  "⟦ plossless_converter ℐ1 ℐ conv1; plossless_converter ℐ2 ℐ conv2; ℐ1, ℐ ⊢⇩C conv1 √; ℐ2, ℐ ⊢⇩C conv2 √ ⟧
  ⟹ plossless_converter (ℐ1 ⊕⇩ℐ ℐ2) ℐ (parallel_converter conv1 conv2)"
  by(coinduction arbitrary: conv1 conv2)
    (clarsimp; erule PlusE; drule (1) plossless_converterD; drule (1) WT_converterD'; fastforce)

primcorec id_converter :: "('a, 'b, 'a, 'b) converter" where
  "run_converter id_converter = (λa.
   map_gpv (map_prod id (λ_. id_converter)) id (Pause a (λb. Done (b, ()))))"

lemma id_converter_parametric [transfer_rule]: "rel_converter A B A B id_converter id_converter"
  unfolding id_converter_def 
  supply map_gpv_parametric'[transfer_rule] Done_parametric'[transfer_rule] Pause_parametric'[transfer_rule]
  by transfer_prover

lemma converter_of_callee_id_oracle [simp]:
  "converter_of_callee id_oracle s = id_converter"
  by(coinduction) (auto simp add: id_oracle_def)

lemma conv_callee_plus_id_left: "converter_of_callee (plus_intercept id_oracle callee) s =
  parallel_converter id_converter (converter_of_callee callee s) "
  by (coinduction arbitrary: callee s)
    (clarsimp split!: sum.split intro!: rel_funI
      , force simp add: gpv.rel_map id_oracle_def, force simp add: gpv.rel_map intro!: gpv.rel_refl)

lemma conv_callee_plus_id_right: "converter_of_callee (plus_intercept callee id_oracle) s =
  parallel_converter (converter_of_callee callee s) id_converter"
  by (coinduction arbitrary: callee s)
    (clarsimp split!: sum.split intro!: rel_funI
      , (force intro: gpv.rel_refl | simp add: gpv.rel_map id_oracle_def)+)

lemma plossless_id_converter [simp, plossless_intro]: "plossless_converter ℐ ℐ id_converter"
  by(coinduction) auto

lemma WT_converter_id [simp, intro, WT_intro]: "ℐ, ℐ ⊢⇩C id_converter √"
  by(coinduction) auto

lemma WT_map_converter_idD:
  "ℐ,ℐ' ⊢⇩C map_converter id id f g id_converter √ ⟹ ℐ ≤ map_ℐ f g ℐ'"
  unfolding le_ℐ_def by(auto 4 3 dest: WT_converterD)


definition fail_converter :: "('a, 'b, 'out, 'in) converter" where
  "fail_converter = Converter (λ_. Fail)"

lemma fail_converter_sel [simp]: "run_converter fail_converter a = Fail"
  by(simp add: fail_converter_def)

lemma fail_converter_parametric [transfer_rule]: "rel_converter A B C R fail_converter fail_converter"
  unfolding fail_converter_def supply Fail_parametric'[transfer_rule] by transfer_prover

lemma plossless_fail_converter [simp]: "plossless_converter ℐ ℐ' fail_converter ⟷ ℐ = bot" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show ?rhs if ?lhs using that by(cases)(auto intro!: ℐ_eqI)
qed simp

lemma plossless_fail_converterI [plossless_intro]: "plossless_converter bot ℐ' fail_converter"
  by simp

lemma WT_fail_converter [simp, WT_intro]: "ℐ, ℐ' ⊢⇩C fail_converter √"
  by(rule WT_converter.intros) simp_all

lemma map_converter_id_move_left:
  "map_converter f g f' g' id_converter = map_converter (f' ∘ f) (g ∘ g') id id id_converter"
  by coinduction(simp add: rel_funI)

lemma map_converter_id_move_right:
  "map_converter f g f' g' id_converter = map_converter id id (f' ∘ f) (g ∘ g') id_converter"
  by coinduction(simp add: rel_funI)


text ‹
  And here is the version for parallel composition that assumes disjoint interfaces.
›
primcorec parallel_converter2
  :: "('a, 'b, 'out, 'in) converter ⇒ ('c, 'd, 'out', 'in') converter ⇒ ('a + 'c, 'b + 'd, 'out + 'out', 'in + 'in') converter"
  where
    "run_converter (parallel_converter2 conv1 conv2) = (λac. case ac of
     Inl a ⇒ map_gpv (map_prod Inl (λconv1'. parallel_converter2 conv1' conv2)) id (left_gpv (run_converter conv1 a))
   | Inr b ⇒ map_gpv (map_prod Inr (λconv2'. parallel_converter2 conv1 conv2')) id (right_gpv (run_converter conv2 b)))"

lemma parallel_converter2_parametric [transfer_rule]: includes lifting_syntax shows
  "(rel_converter A B C R ===> rel_converter A' B' C' R' 
   ===> rel_converter (rel_sum A A') (rel_sum B B') (rel_sum C C') (rel_sum R R'))
  parallel_converter2 parallel_converter2"
  unfolding parallel_converter2_def
  supply left_gpv_parametric'[transfer_rule] right_gpv_parametric'[transfer_rule] map_gpv_parametric'[transfer_rule]
  by transfer_prover

lemma map_converter_parallel_converter2:
  "map_converter (map_sum f f') (map_sum g g') (map_sum h h') (map_sum k k') (parallel_converter2 conv1 conv2) =
   parallel_converter2 (map_converter f g h k conv1) (map_converter f' g' h' k' conv2)"
  using parallel_converter2_parametric[of
      "conversep (BNF_Def.Grp UNIV f)" "BNF_Def.Grp UNIV g"  "BNF_Def.Grp UNIV h"  "conversep (BNF_Def.Grp UNIV k)"
      "conversep (BNF_Def.Grp UNIV f')" "BNF_Def.Grp UNIV g'"  "BNF_Def.Grp UNIV h'"  "conversep (BNF_Def.Grp UNIV k')"]
  unfolding sum.rel_conversep sum.rel_Grp
  by(simp add: rel_converter_Grp rel_fun_def Grp_iff)

lemma WT_converter_parallel_converter2 [WT_intro]:
  assumes "ℐ1,ℐ2 ⊢⇩C conv1 √"
    and "ℐ1',ℐ2' ⊢⇩C conv2 √"
  shows "ℐ1 ⊕⇩ℐ ℐ1',ℐ2 ⊕⇩ℐ ℐ2' ⊢⇩C parallel_converter2 conv1 conv2 √"
  using assms
  apply(coinduction arbitrary: conv1 conv2)
  apply(clarsimp split!: sum.split)
  subgoal by(auto intro: WT_gpv_left_gpv dest: WT_converterD_WT)
  subgoal by(auto dest: WT_converterD_results)
  subgoal by(auto dest: WT_converterD_results)
  subgoal by(auto intro: WT_gpv_right_gpv dest: WT_converterD_WT)
  subgoal by(auto dest: WT_converterD_results)
  subgoal by(auto 4 3 dest: WT_converterD_results)
  done

lemma plossless_parallel_converter2 [plossless_intro]:
  assumes "plossless_converter ℐ1 ℐ1' conv1"
    and "plossless_converter ℐ2 ℐ2' conv2"
  shows "plossless_converter (ℐ1 ⊕⇩ℐ ℐ2) (ℐ1' ⊕⇩ℐ ℐ2') (parallel_converter2 conv1 conv2)"
  using assms
  by(coinduction arbitrary: conv1 conv2)
    ((rule exI conjI refl)+ | auto dest: plossless_converterD)+

lemma parallel_converter2_map1_out:
  "parallel_converter2 (map_converter f g h k conv1) conv2 =
   map_converter (map_sum f id) (map_sum g id) (map_sum h id) (map_sum k id) (parallel_converter2 conv1 conv2)"
  by(simp add: map_converter_parallel_converter2)

lemma parallel_converter2_map2_out:
  "parallel_converter2 conv1 (map_converter f g h k conv2) =
   map_converter (map_sum id f) (map_sum id g) (map_sum id h) (map_sum id k) (parallel_converter2 conv1 conv2)"
  by(simp add: map_converter_parallel_converter2)


primcorec left_interface :: "('a, 'b, 'out, 'in) converter ⇒ ('a, 'b, 'out + 'out', 'in + 'in') converter" where
  "run_converter (left_interface conv) = (λa. map_gpv (map_prod id left_interface) id (left_gpv (run_converter conv a)))"

lemma left_interface_parametric [transfer_rule]: includes lifting_syntax shows
  "(rel_converter A B C R ===> rel_converter A B (rel_sum C C') (rel_sum R R')) left_interface left_interface"
  unfolding left_interface_def
  supply left_gpv_parametric'[transfer_rule] map_gpv_parametric'[transfer_rule] by transfer_prover

primcorec right_interface :: "('a, 'b, 'out, 'in) converter ⇒ ('a, 'b, 'out' + 'out, 'in' + 'in) converter" where
  "run_converter (right_interface conv) = (λa. map_gpv (map_prod id right_interface) id (right_gpv (run_converter conv a)))"

lemma right_interface_parametric [transfer_rule]: includes lifting_syntax shows
  "(rel_converter A B C' R' ===> rel_converter A B (rel_sum C C') (rel_sum R R')) right_interface right_interface"
  unfolding right_interface_def
  supply right_gpv_parametric'[transfer_rule] map_gpv_parametric'[transfer_rule] by transfer_prover

lemma parallel_converter2_alt_def:
  "parallel_converter2 conv1 conv2 = parallel_converter (left_interface conv1) (right_interface conv2)"
  by(coinduction arbitrary: conv1 conv2 rule: converter.coinduct_strong)
    (auto 4 5 intro!: rel_funI gpv.rel_refl_strong split: sum.split simp add: gpv.rel_map)

lemma conv_callee_parallel_id_left: "converter_of_callee (parallel_intercept id_oracle callee) (s, s') =
  parallel_converter2 (id_converter) (converter_of_callee callee s')"
  apply (coinduction arbitrary: callee s')
  apply (rule rel_funI)
  apply (clarsimp simp add: gpv.rel_map left_gpv_map[of _ _ _ "id"] 
      right_gpv_map[of _ _ _ "id"] split!: sum.split)
   apply (force simp add: id_oracle_def split!: sum.split)
  apply (rule gpv.rel_refl)
  by force+

lemma conv_callee_parallel_id_right: "converter_of_callee (parallel_intercept callee id_oracle) (s, s') =
  parallel_converter2 (converter_of_callee callee s) (id_converter)"
  apply (coinduction arbitrary: callee s)
  apply (rule rel_funI)
  apply (clarsimp simp add: gpv.rel_map left_gpv_map[of _ _ _ "id"] 
      right_gpv_map[of _ _ _ "id"] split!: sum.split)
   apply (rule gpv.rel_refl)
  by (force simp add: id_oracle_def  split!: sum.split)+

lemma conv_callee_parallel: "converter_of_callee (parallel_intercept callee1 callee2) (s,s') 
  = parallel_converter2 (converter_of_callee callee1 s) (converter_of_callee callee2 s')"
  apply (coinduction arbitrary: callee1 callee2 s s')
  apply (clarsimp simp add: gpv.rel_map left_gpv_map[of _ _ _ "id"] right_gpv_map[of _ _ _ "id"] intro!: rel_funI split!: sum.split)
   apply (rule gpv.rel_refl)
    apply force+
  apply (rule gpv.rel_refl)
  by force+

lemma WT_converter_parallel_converter [WT_intro]:
  assumes "ℐ1, ℐ ⊢⇩C conv1 √"
    and "ℐ2, ℐ ⊢⇩C conv2 √"
  shows "ℐ1 ⊕⇩ℐ ℐ2, ℐ ⊢⇩C parallel_converter conv1 conv2 √"
  using assms by(coinduction arbitrary: conv1 conv2)(auto 4 4 dest: WT_converterD intro!: imageI)

primcorec converter_of_resource :: "('a, 'b) resource ⇒ ('a, 'b, 'c, 'd) converter" where
  "run_converter (converter_of_resource res) = (λx. map_gpv (map_prod id converter_of_resource) id (lift_spmf (run_resource res x)))"

lemma WT_converter_of_resource [WT_intro]:
  assumes "ℐ ⊢res res √"
  shows "ℐ, ℐ' ⊢⇩C converter_of_resource res √"
  using assms by(coinduction arbitrary: res)(auto dest: WT_resourceD)

lemma plossless_converter_of_resource [plossless_intro]:
  assumes "lossless_resource ℐ res"
  shows "plossless_converter ℐ ℐ' (converter_of_resource res)"
  using assms by(coinduction arbitrary: res)(auto 4 3 dest: lossless_resourceD)

lemma plossless_converter_of_callee:
  assumes "⋀s x. x ∈ outs_ℐ ℐ1 ⟹ plossless_gpv ℐ2 (callee s x) ∧ (∀(y, s')∈results_gpv ℐ2 (callee s x). y ∈ responses_ℐ ℐ1 x)"
  shows "plossless_converter ℐ1 ℐ2 (converter_of_callee callee s)"
  apply(coinduction arbitrary: s)
  subgoal for x s by(drule assms[where s=s]) auto
  done

context 
  fixes A :: "'a set"
  and ℐ :: "('c, 'd) ℐ"
begin

primcorec restrict_converter :: "('a, 'b, 'c, 'd) converter ⇒ ('a, 'b, 'c, 'd) converter"
  where 
  "run_converter (restrict_converter cnv) = (λa. if a ∈ A then
     map_gpv (map_prod id (λcnv'. restrict_converter cnv')) id (restrict_gpv ℐ (run_converter cnv a))
   else Fail)"

end

lemma WT_restrict_converter [WT_intro]:
  assumes "ℐ,ℐ' ⊢⇩C cnv √"
  shows "ℐ,ℐ' ⊢⇩C restrict_converter A ℐ' cnv √"
  using assms by(coinduction arbitrary: cnv)(auto dest: WT_converterD dest!: in_results_gpv_restrict_gpvD)

lemma pgen_lossless_restrict_gpv [simp]:
  "ℐ ⊢g gpv √ ⟹ pgen_lossless_gpv b ℐ (restrict_gpv ℐ gpv) = pgen_lossless_gpv b ℐ gpv"
  unfolding pgen_lossless_gpv_def by(simp add: expectation_gpv_restrict_gpv)

lemma plossless_restrict_converter [simp]:
  assumes "plossless_converter ℐ ℐ' conv"
    and "ℐ,ℐ' ⊢⇩C conv √"
    and "outs_ℐ ℐ ⊆ A"
  shows "plossless_converter ℐ ℐ' (restrict_converter A ℐ' conv)"
  using assms
  by(coinduction arbitrary: conv)
    (auto dest!: in_results_gpv_restrict_gpvD WT_converterD' plossless_converterD)

lemma plossless_map_converter:
  "plossless_converter ℐ ℐ' (map_converter f g h k conv)"
  if "plossless_converter (map_ℐ (inv_into UNIV f) (inv_into UNIV g) ℐ) (map_ℐ h k ℐ') conv" "inj f"
  using that
  by(coinduction arbitrary: conv)(auto dest!: plossless_converterD[where a="f _"])



subsection ‹Attaching converters to resources›

primcorec "attach" :: "('a, 'b, 'out, 'in) converter ⇒ ('out, 'in) resource ⇒ ('a, 'b) resource" where
  "run_resource (attach conv res) = (λa. 
   map_spmf (λ((b, conv'), res'). (b, attach conv' res')) (exec_gpv run_resource (run_converter conv a) res))"

lemma attach_parametric [transfer_rule]: includes lifting_syntax shows
  "(rel_converter A B C R ===> rel_resource C R ===> rel_resource A B) attach attach"
  unfolding attach_def
  supply exec_gpv_parametric'[transfer_rule] by transfer_prover

lemma attach_map_converter:
  "attach (map_converter f g h k conv) res = map_resource f g (attach conv (map_resource h k res))"
  using attach_parametric[of "conversep (BNF_Def.Grp UNIV f)" "BNF_Def.Grp UNIV g" "BNF_Def.Grp UNIV h" "conversep (BNF_Def.Grp UNIV k)"]
  unfolding rel_converter_Grp rel_resource_Grp
  by (simp, rewrite at "rel_fun _ (rel_fun ⌑ _)" in asm conversep_iff[symmetric, abs_def])
    (simp add: rel_resource_conversep[symmetric] rel_fun_def Grp_iff conversep_conversep rel_resource_Grp)

lemma WT_resource_attach [WT_intro]: "⟦ ℐ, ℐ' ⊢⇩C conv √; ℐ' ⊢res res √ ⟧ ⟹ ℐ ⊢res attach conv res √"
  by(coinduction arbitrary: conv res)
    (auto 4 3 intro!: exI dest: run_resource.in_set_spmf_exec_gpv_into_results_gpv WT_converterD intro: run_resource.exec_gpv_invariant)

lemma lossless_attach [plossless_intro]:
  assumes "plossless_converter ℐ ℐ' conv"
    and "lossless_resource ℐ' res"
    and "ℐ, ℐ' ⊢⇩C conv √" "ℐ' ⊢res res √"
  shows "lossless_resource ℐ (attach conv res)"
  using assms
proof(coinduction arbitrary: res conv)
  case (lossless_resource a res conv)
  from plossless_converterD[OF lossless_resource(1,5)] have lossless: "plossless_gpv ℐ' (run_converter conv a)"
    "⋀b conv'. (b, conv') ∈ results_gpv ℐ' (run_converter conv a) ⟹ plossless_converter ℐ ℐ' conv'" by auto
  from WT_converterD'[OF lossless_resource(3,5)] have WT: "ℐ' ⊢g run_converter conv a √"
    "⋀b conv'. (b, conv') ∈ results_gpv ℐ' (run_converter conv a) ⟹ b ∈ responses_ℐ ℐ a ∧ ℐ, ℐ' ⊢⇩C conv' √" by auto
  have ?lossless using lossless(1) WT(1) lossless_resource(2,4)
    by(auto intro: run_lossless_resource.plossless_exec_gpv dest: lossless_resourceD)
  moreover have ?step (is "∀(b, res')∈?set. ?P b res' ∨ _")
  proof(safe)
    fix b res''
    assume "(b, res'') ∈ ?set"
    then obtain conv' res' where *: "((b, conv'), res') ∈ set_spmf (exec_gpv run_resource (run_converter conv a) res)"
      and [simp]: "res'' = attach conv' res'" by auto
    from run_lossless_resource.in_set_spmf_exec_gpv_into_results_gpv[OF *, of ℐ'] lossless_resource(2,4) WT
    have conv': "(b, conv') ∈ results_gpv ℐ' (run_converter conv a)" by auto
    from run_lossless_resource.exec_gpv_invariant[OF *, of ℐ'] WT(2)[OF this] WT(1) lossless(2)[OF this] lossless_resource
    show "?P b res''" by auto
  qed
  ultimately show ?case ..
qed


definition attach_callee
  :: "('s ⇒ 'a ⇒ ('b × 's, 'out, 'in) gpv) 
  ⇒ ('s' ⇒ 'out ⇒ ('in × 's') spmf)
  ⇒ ('s × 's' ⇒ 'a ⇒ ('b × 's × 's') spmf)" where
  "attach_callee callee oracle = (λ(s, s') q. map_spmf rprodl (exec_gpv oracle (callee s q) s'))"

lemma attach_callee_simps [simp]:
  "attach_callee callee oracle (s, s') q = map_spmf rprodl (exec_gpv oracle (callee s q) s')"
  by(simp add: attach_callee_def)

lemma attach_CNV_RES:
  "attach (converter_of_callee callee s) (resource_of_oracle res s') = 
   resource_of_oracle (attach_callee callee res) (s, s')"
  by(coinduction arbitrary: s s')
    (clarsimp simp add: spmf_rel_map rel_fun_def exec_gpv_map_gpv_id
      , rule exec_gpv_parametric[where S="λl r. l = resource_of_oracle res r" and A="(=)" and CALL="(=)", THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_spmf_mono]
      , auto 4 3 simp add: rel_fun_def spmf_rel_map gpv.rel_eq intro!: rel_spmf_reflI)

lemma attach_stateless_callee:
  "attach_callee (stateless_callee callee) oracle = extend_state_oracle (λs q. exec_gpv oracle (callee q) s)"
  by(simp add: attach_callee_def stateless_callee_def fun_eq_iff exec_gpv_map_gpv_id spmf.map_comp o_def split_def apfst_def map_prod_def)

lemma attach_id_converter [simp]: "attach id_converter res = res"
  by(coinduction arbitrary: res)(auto simp add: rel_fun_def spmf_rel_map split_def map_spmf_conv_bind_spmf[symmetric] intro!: rel_spmf_reflI)

lemma attach_callee_parallel_intercept: includes lifting_syntax shows
  "attach_callee (parallel_intercept callee1 callee2) (plus_oracle oracle1 oracle2) =
   (rprodl ---> id ---> map_spmf (map_prod id lprodr)) (plus_oracle (lift_state_oracle extend_state_oracle (attach_callee callee1 oracle1)) (extend_state_oracle (attach_callee callee2 oracle2)))"
proof ((rule ext)+, clarify, goal_cases)
  case (1 s1 s2 s q)
  then show ?case by(cases q) (auto simp add: exec_gpv_plus_oracle_left exec_gpv_plus_oracle_right spmf.map_comp apfst_def o_def prod.map_comp split_def exec_gpv_map_gpv_id intro!: map_spmf_cong)
qed

lemma attach_callee_id_oracle [simp]:
  "attach_callee id_oracle oracle = extend_state_oracle oracle"
  by(clarsimp simp add: fun_eq_iff id_oracle_def map_spmf_conv_bind_spmf split_def)

lemma attach_parallel2: "attach (parallel_converter2 conv1 conv2) (parallel_resource res1 res2)
  = parallel_resource (attach conv1 res1) (attach conv2 res2)"
  apply(coinduction arbitrary: conv1 conv2 res1 res2)
  apply simp
  apply(rule rel_funI)
  apply clarsimp
  apply(simp split!: sum.split)
  subgoal for conv1 conv2 res1 res2 a
    apply(simp add: exec_gpv_map_gpv_id spmf_rel_map)
    apply(rule rel_spmf_mono)
     apply(rule
        exec_gpv_parametric'[where ?S = "λres1res2 res1. res1res2 = parallel_resource res1 res2" 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
          ])
    subgoal by(auto simp add: rel_fun_def spmf_rel_map intro!: rel_spmf_reflI)
    subgoal by (simp add: left_gpv_Inl_transfer)
    subgoal by blast
    apply clarsimp
    apply(rule exI conjI refl)+
    done
  subgoal for conv1 conv2 res1 res2 a
    apply(simp add: exec_gpv_map_gpv_id spmf_rel_map)
    apply(rule rel_spmf_mono)
     apply(rule
        exec_gpv_parametric'[where ?S = "λres1res2 res2. res1res2 = parallel_resource res1 res2" 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
          ])
    subgoal by(auto simp add: rel_fun_def spmf_rel_map intro: rel_spmf_reflI)
    subgoal by (simp add: right_gpv_Inr_transfer)
    subgoal by blast
    apply clarsimp
    apply(rule exI conjI refl)+
    done
  done

subsection ‹Composing converters›

primcorec comp_converter :: "('a, 'b, 'out, 'in) converter ⇒ ('out, 'in, 'out', 'in') converter ⇒ ('a, 'b, 'out', 'in') converter" where
  "run_converter (comp_converter conv1 conv2) = (λa.
  map_gpv (λ((b, conv1'), conv2'). (b, comp_converter conv1' conv2')) id (inline run_converter (run_converter conv1 a) conv2))"

lemma comp_converter_parametric [transfer_rule]: includes lifting_syntax shows
  "(rel_converter A B C R ===> rel_converter C R C' R' ===> rel_converter A B C' R')
  comp_converter comp_converter"
  unfolding comp_converter_def
  supply inline_parametric'[transfer_rule] map_gpv_parametric'[transfer_rule] by transfer_prover

lemma comp_converter_map_converter1:
  fixes conv' :: "('a, 'b, 'out, 'in) converter" shows
    "comp_converter (map_converter f g h k conv) conv' = map_converter f g id id (comp_converter conv (map_converter h k id id conv'))"
  using comp_converter_parametric[of
      "conversep (BNF_Def.Grp UNIV f)" "BNF_Def.Grp UNIV g" "BNF_Def.Grp UNIV h" "conversep (BNF_Def.Grp UNIV k)"
      "BNF_Def.Grp UNIV (id :: 'out ⇒ _)" "conversep (BNF_Def.Grp UNIV (id :: 'in ⇒ _))"
      ]
  apply(unfold rel_converter_Grp)
  apply(simp add: rel_fun_def Grp_iff)
  apply(rewrite at "∀_ _ _. ⌑ ⟶ _" in asm conversep_iff[symmetric])
  apply(unfold rel_converter_conversep[symmetric] conversep_conversep eq_alt[symmetric])
  apply(rewrite in "rel_converter _ _ ⌑ _" in asm conversep_eq)
  apply(rewrite in "rel_converter _ _ _ ⌑" in asm conversep_eq[symmetric])
  apply(rewrite in "rel_converter _ _ ⌑ _" in asm eq_alt)
  apply(rewrite in "rel_converter _ _ _ ⌑" in asm eq_alt)
  apply(unfold rel_converter_Grp)
  apply(simp add: Grp_iff)
  done

lemma comp_converter_map_converter2:
  fixes conv :: "('a, 'b, 'out, 'in) converter" shows
    "comp_converter conv (map_converter f g h k conv') = map_converter id id h k (comp_converter (map_converter id id f g conv) conv')"
  using comp_converter_parametric[of
      "BNF_Def.Grp UNIV (id :: 'a ⇒ _)" "conversep (BNF_Def.Grp UNIV (id :: 'b ⇒ _))"
      "conversep (BNF_Def.Grp UNIV f)" "BNF_Def.Grp UNIV g" "BNF_Def.Grp UNIV h" "conversep (BNF_Def.Grp UNIV k)"
      ]
  apply(unfold rel_converter_Grp)
  apply(simp add: rel_fun_def Grp_iff)
  apply(rewrite at "∀_ _. ⌑ ⟶ _" in asm conversep_iff[symmetric])
  apply(unfold rel_converter_conversep[symmetric] conversep_conversep rel_converter_Grp)
  apply simp
  apply(unfold eq_alt[symmetric])
  apply(rewrite in "rel_converter _ ⌑" in asm conversep_eq)
  apply(rewrite in "rel_converter ⌑ _" in asm conversep_eq[symmetric])
  apply(rewrite in "rel_converter ⌑ _" in asm eq_alt)
  apply(rewrite in "rel_converter _ ⌑" in asm eq_alt)
  apply(unfold rel_converter_Grp)
  apply(simp add: Grp_iff)
  done

lemma attach_compose:
  "attach (comp_converter conv1 conv2) res = attach conv1 (attach conv2 res)"
  apply(coinduction arbitrary: conv1 conv2 res)
  apply(auto intro!: rel_funI simp add: spmf_rel_map exec_gpv_map_gpv_id exec_gpv_inline o_def split_beta)
  including lifting_syntax
  apply(rule rel_spmf_mono)
   apply(rule exec_gpv_parametric[where A="(=)" and CALL="(=)" and S="λ(l, r) s2. s2 = attach l r", THEN rel_funD, THEN rel_funD, THEN rel_funD])
     prefer 4
     apply clarsimp
  by(auto simp add: case_prod_def spmf_rel_map gpv.rel_eq split_def intro!: rel_funI rel_spmf_reflI)


lemma comp_converter_assoc:
  "comp_converter (comp_converter conv1 conv2) conv3 = comp_converter conv1 (comp_converter conv2 conv3)"
  apply(coinduction arbitrary: conv1 conv2 conv3)
  apply(rule rel_funI)
  apply(clarsimp simp add: gpv.rel_map inline_map_gpv)
  apply(subst inline_assoc)
  apply(simp add: gpv.rel_map)
  including lifting_syntax
  apply(rule gpv.rel_mono_strong)
    apply(rule inline_parametric[where C="(=)" and C'="(=)" and A="(=)" and S="λ(l, r) s2. s2 = comp_converter l r", THEN rel_funD, THEN rel_funD, THEN rel_funD])
      prefer 4
      apply clarsimp
  by(auto simp add: gpv.rel_eq gpv.rel_map split_beta intro!: rel_funI gpv.rel_refl_strong)


lemma comp_converter_assoc_left:
  assumes "comp_converter conv1 conv2 = conv3"
  shows "comp_converter conv1 (comp_converter conv2 conv) = comp_converter conv3 conv"
  by(fold comp_converter_assoc)(simp add: assms)

lemma comp_converter_attach_left:
  assumes "comp_converter conv1 conv2 = conv3"
  shows "attach conv1 (attach conv2 res) = attach conv3 res"
  by(fold attach_compose)(simp add: assms)  

lemmas comp_converter_eqs = 
  asm_rl[where psi="x = y" for x y :: "(_, _, _, _) converter"]
  comp_converter_assoc_left
  comp_converter_attach_left

lemma WT_converter_comp [WT_intro]:
  "⟦ ℐ, ℐ' ⊢⇩C conv √; ℐ', ℐ'' ⊢⇩C conv' √ ⟧ ⟹ ℐ, ℐ'' ⊢⇩C comp_converter conv conv' √"
  by(coinduction arbitrary: conv conv')
    (auto; auto 4 4 dest: WT_converterD run_converter.results_gpv_inline intro: run_converter.WT_gpv_inline_invar[where ℐ=ℐ' and ℐ'=ℐ''])

lemma plossless_comp_converter [plossless_intro]:
  assumes "plossless_converter ℐ ℐ' conv"
    and "plossless_converter ℐ' ℐ'' conv'"
    and "ℐ, ℐ' ⊢⇩C conv √" "ℐ', ℐ'' ⊢⇩C conv' √"
  shows "plossless_converter ℐ ℐ'' (comp_converter conv conv')"
  using assms
proof(coinduction arbitrary: conv conv')
  case (plossless_converter a conv conv')
  have conv1: "plossless_gpv ℐ' (run_converter conv a)" 
    using plossless_converter(1, 5) by(simp add: plossless_converterD)
  have conv2: "ℐ' ⊢g run_converter conv a √"
    using plossless_converter(3, 5) by(simp add: WT_converterD)
  have ?plossless using plossless_converter(2,4,5)
    by(auto intro: run_plossless_converter.plossless_inline[OF conv1] dest: plossless_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 ℐ'' (inline run_converter (run_converter conv a) conv')" 
      by auto
    from run_plossless_converter.results_gpv_inline[OF inline conv2] plossless_converter(2,4)
    have run: "(b, conv1) ∈ results_gpv ℐ' (run_converter conv a)"
      and *: "plossless_converter ℐ' ℐ'' conv2" "ℐ', ℐ'' ⊢⇩C conv2 √" by auto
    with WT_converterD(2)[OF plossless_converter(3,5) run] plossless_converterD[THEN conjunct2, rule_format, OF plossless_converter(1,5) run]
    show "?P b conv''" by auto
  qed
  ultimately show ?case ..
qed

lemma comp_converter_id_left: "comp_converter id_converter conv = conv"
  by (coinduction arbitrary:conv)
    (auto simp add: gpv.rel_map split_def map_gpv_conv_bind[symmetric]  intro!:rel_funI gpv.rel_refl_strong)

lemma comp_converter_id_right: "comp_converter conv id_converter = conv"
proof -
  have lem4: "inline run_converter gpv id_converter = inline id_oracle gpv id_converter" for gpv
    by (simp only: gpv.rel_eq[symmetric])
      (rule gpv.rel_mono_strong
        , rule inline_parametric[where A="(=)" and C="(=)" and C'="(=)" and S="λl r. l = r ∧ r = id_converter", THEN rel_funD, THEN rel_funD, THEN rel_funD]
        , auto simp add: id_oracle_def intro!: rel_funI  gpv.rel_refl_strong)
  show ?thesis
    by (coinduction arbitrary:conv)
      (auto simp add: lem4 gpv.rel_map intro!:rel_funI gpv.rel_refl_strong)
qed

lemma comp_coverter_of_callee: "comp_converter (converter_of_callee callee1 s1) (converter_of_callee callee2 s2)
  = converter_of_callee (λ(s1, s2) q. map_gpv rprodl id (inline callee2 (callee1 s1 q) s2)) (s1, s2)"
  apply (coinduction arbitrary: callee1 s1 callee2 s2)
  apply (rule rel_funI)
  apply (clarsimp simp add: gpv.rel_map inline_map_gpv)
  subgoal for cal1 s1 cal2 s2 y
    apply (rule gpv.rel_mono_strong)
      apply (rule inline_parametric[where A="(=)" and C="(=)" and C'="(=)" and S="λc s. c = converter_of_callee cal2 s", THEN rel_funD, THEN rel_funD, THEN rel_funD])
        apply(auto simp add: gpv.rel_eq rel_fun_def gpv.rel_map intro!: gpv.rel_refl_strong)
    by (auto simp add: rprodl_def intro!:exI)
  done

lemmas comp_converter_of_callee' = comp_converter_eqs[OF comp_coverter_of_callee]

lemma comp_converter_parallel2: "comp_converter (parallel_converter2 conv1l conv1r) (parallel_converter2 conv2l conv2r) =
  parallel_converter2 (comp_converter conv1l conv2l) (comp_converter conv1r conv2r)"
  apply (coinduction arbitrary: conv1l conv1r conv2l conv2r)
  apply (rule rel_funI)
  apply (clarsimp simp add: gpv.rel_map inline_map_gpv split!: sum.split)
  subgoal for conv1l conv1r conv2l conv2r input
    apply(subst left_gpv_map[where h=id])
    apply(simp add: gpv.rel_map left_gpv_inline)
    apply(unfold rel_gpv_conv_rel_gpv'')
    apply(rule rel_gpv''_mono[THEN predicate2D, rotated -1])
       apply(rule inline_parametric'[where S="λc1 c2. c1 = parallel_converter2 c2 conv2r" and C="λl r. l = Inl r" and R="λl r. l = Inl r" and C' = "(=)" and R'="(=)",
          THEN rel_funD, THEN rel_funD, THEN rel_funD])
    subgoal by(auto split: sum.split simp add: gpv.rel_map rel_gpv_conv_rel_gpv''[symmetric] intro!:  gpv.rel_refl_strong rel_funI)
        apply(rule left_gpv_Inl_transfer)
       apply(auto 4 6 simp add: sum.map_id)
    done
  subgoal for conv1l conv1r conv2l conv2r input
    apply(subst right_gpv_map[where h=id])
    apply(simp add: gpv.rel_map right_gpv_inline)
    apply(unfold rel_gpv_conv_rel_gpv'')
    apply(rule rel_gpv''_mono[THEN predicate2D, rotated -1])
       apply(rule inline_parametric'[where S="λc1 c2. c1 = parallel_converter2 conv2l c2" and C="λl r. l = Inr r" and R="λl r. l = Inr r" and C' = "(=)" and R'="(=)",
          THEN rel_funD, THEN rel_funD, THEN rel_funD])
    subgoal by(auto split: sum.split simp add: gpv.rel_map rel_gpv_conv_rel_gpv''[symmetric] intro!:  gpv.rel_refl_strong rel_funI)
        apply(rule right_gpv_Inr_transfer)
       apply(auto 4 6 simp add: sum.map_id)
    done
  done

lemmas comp_converter_parallel2' = comp_converter_eqs[OF comp_converter_parallel2]

lemma comp_converter_map1_out:
  "comp_converter (map_converter f g id id conv) conv' = map_converter f g id id (comp_converter conv conv')"
  by(simp add: comp_converter_map_converter1)

lemma parallel_converter2_comp1_out:
  "parallel_converter2 (comp_converter conv conv') conv'' = comp_converter (parallel_converter2 conv id_converter) (parallel_converter2 conv' conv'')"
  by(simp add: comp_converter_parallel2 comp_converter_id_left)

lemma parallel_converter2_comp2_out:
  "parallel_converter2 conv'' (comp_converter conv conv') = comp_converter (parallel_converter2 id_converter conv) (parallel_converter2 conv'' conv')"
  by(simp add: comp_converter_parallel2 comp_converter_id_left)

subsection ‹Interaction bound›

coinductive interaction_any_bounded_converter :: "('a, 'b, 'c, 'd) converter ⇒ enat ⇒ bool" where
  "interaction_any_bounded_converter conv n" if
  "⋀a. interaction_any_bounded_by (run_converter conv a) n"
  "⋀a b conv'. (b, conv') ∈ results'_gpv (run_converter conv a) ⟹ interaction_any_bounded_converter conv' n"

lemma interaction_any_bounded_converterD:
  assumes "interaction_any_bounded_converter conv n"
  shows "interaction_any_bounded_by (run_converter conv a) n ∧ (∀(b, conv')∈results'_gpv (run_converter conv a). interaction_any_bounded_converter conv' n)"
  using assms
  by(auto elim: interaction_any_bounded_converter.cases)

lemma interaction_any_bounded_converter_mono:
  assumes "interaction_any_bounded_converter conv n"
    and "n ≤ m"
  shows "interaction_any_bounded_converter conv m"
  using assms
  by(coinduction arbitrary: conv)(auto elim: interaction_any_bounded_converter.cases intro: interaction_bounded_by_mono)

lemma interaction_any_bounded_converter_trivial [simp]: "interaction_any_bounded_converter conv ∞"
  by(coinduction arbitrary: conv)
    (auto simp add: interaction_bounded_by.simps)

lemmas interaction_any_bounded_converter_start = 
  interaction_any_bounded_converter_mono
  interaction_bounded_by_mono

method interaction_bound_converter_start = (rule interaction_any_bounded_converter_start)
method interaction_bound_converter_step uses add simp =
  ((match conclusion in "interaction_bounded_by _ _ _" ⇒ fail ¦ "interaction_any_bounded_converter _ _" ⇒ fail ¦ _ ⇒ ‹solves ‹clarsimp simp add: simp››) | rule add interaction_bound)
method interaction_bound_converter_rec uses add simp = 
  (interaction_bound_converter_step add: add simp: simp; (interaction_bound_converter_rec add: add simp: simp)?)
method interaction_bound_converter uses add simp =
  ((* use in *) interaction_bound_converter_start, interaction_bound_converter_rec add: add simp: simp)

lemma interaction_any_bounded_converter_id [interaction_bound]:
  "interaction_any_bounded_converter id_converter 1"
  by(coinduction) simp

lemma raw_converter_invariant_interaction_any_bounded_converter:
  "raw_converter_invariant ℐ_full ℐ_full run_converter (λconv. interaction_any_bounded_converter conv n)"
  by(unfold_locales)(auto simp add: results_gpv_ℐ_full dest: interaction_any_bounded_converterD)

lemma interaction_bounded_by_left_gpv [interaction_bound]:
  assumes "interaction_bounded_by consider gpv n"
    and "⋀x. consider' (Inl x) ⟹ consider x"
  shows "interaction_bounded_by consider' (left_gpv gpv) n"
proof -
  define ib :: "('b, 'a, 'c) gpv ⇒ _" where "ib ≡ interaction_bound consider"
  have "interaction_bound consider' (left_gpv gpv) ≤ ib gpv"
  proof(induction arbitrary: gpv rule: interaction_bound_fixp_induct)
    case (step interaction_bound')
    show ?case unfolding ib_def
      apply(subst interaction_bound.simps)
      apply(rule SUP_least)
      apply(clarsimp split!: generat.split if_split)
       apply(rule SUP_upper2, assumption)
       apply(clarsimp split!: if_split simp add: assms(2))
       apply(rule SUP_mono)
      subgoal for … input
        by(cases input)(auto 4 3 intro: step.IH[unfolded ib_def] order_trans[OF step.hyps(1)])
      apply(rule SUP_upper2, assumption)
      apply(clarsimp split!: if_split)
       apply(rule order_trans, rule ile_eSuc)
       apply(simp)
       apply(rule SUP_mono)
      subgoal for … input
        by(cases input)(auto 4 3 intro: step.IH[unfolded ib_def] order_trans[OF step.hyps(1)])
      apply(rule SUP_mono)
      subgoal for … input
        by(cases input)(auto 4 3 intro: step.IH[unfolded ib_def] order_trans[OF step.hyps(1)])
      done
  qed simp_all
  then show ?thesis using assms(1)
    by(auto simp add: ib_def interaction_bounded_by.simps intro: order_trans)
qed

lemma interaction_bounded_by_right_gpv [interaction_bound]:
  assumes "interaction_bounded_by consider gpv n"
    and "⋀x. consider' (Inr x) ⟹ consider x"
  shows "interaction_bounded_by consider' (right_gpv gpv) n"
proof -
  define ib :: "('b, 'a, 'c) gpv ⇒ _" where "ib ≡ interaction_bound consider"
  have "interaction_bound consider' (right_gpv gpv) ≤ ib gpv"
  proof(induction arbitrary: gpv rule: interaction_bound_fixp_induct)
    case (step interaction_bound')
    show ?case unfolding ib_def
      apply(subst interaction_bound.simps)
      apply(rule SUP_least)
      apply(clarsimp split!: generat.split if_split)
       apply(rule SUP_upper2, assumption)
       apply(clarsimp split!: if_split simp add: assms(2))
       apply(rule SUP_mono)
      subgoal for … input
        by(cases input)(auto 4 3 intro: step.IH[unfolded ib_def] order_trans[OF step.hyps(1)])
      apply(rule SUP_upper2, assumption)
      apply(clarsimp split!: if_split)
       apply(rule order_trans, rule ile_eSuc)
       apply(simp)
       apply(rule SUP_mono)
      subgoal for … input
        by(cases input)(auto 4 3 intro: step.IH[unfolded ib_def] order_trans[OF step.hyps(1)])
      apply(rule SUP_mono)
      subgoal for … input
        by(cases input)(auto 4 3 intro: step.IH[unfolded ib_def] order_trans[OF step.hyps(1)])
      done
  qed simp_all
  then show ?thesis using assms(1)
    by(auto simp add: ib_def interaction_bounded_by.simps intro: order_trans)
qed

lemma interaction_any_bounded_converter_parallel_converter2:
  assumes "interaction_any_bounded_converter conv1 n"
    and "interaction_any_bounded_converter conv2 n"
  shows "interaction_any_bounded_converter (parallel_converter2 conv1 conv2) n"
  using assms
  by(coinduction arbitrary: conv1 conv2)
    (auto 4 4 split: sum.split intro!: interaction_bounded_by_map_gpv_id intro: interaction_bounded_by_left_gpv interaction_bounded_by_right_gpv elim: interaction_any_bounded_converter.cases)

lemma interaction_any_bounded_converter_parallel_converter2' [interaction_bound]:
  assumes "interaction_any_bounded_converter conv1 n"
    and "interaction_any_bounded_converter conv2 m"
  shows "interaction_any_bounded_converter (parallel_converter2 conv1 conv2) (max n m)"
  by(rule interaction_any_bounded_converter_parallel_converter2; rule assms[THEN interaction_any_bounded_converter_mono]; simp)

lemma interaction_any_bounded_converter_compose [interaction_bound]:
  assumes "interaction_any_bounded_converter conv1 n"
    and "interaction_any_bounded_converter conv2 m"
  shows "interaction_any_bounded_converter (comp_converter conv1 conv2) (n * m)"
proof -
  have [simp]: "⟦interaction_any_bounded_converter conv1 n; interaction_any_bounded_converter conv2 m⟧ ⟹
    interaction_any_bounded_by (inline run_converter (run_converter conv1 x) conv2) (n * m)" for conv1 conv2 x
    by (rule interaction_bounded_by_inline_invariant[where I="λconv2. interaction_any_bounded_converter conv2 m" and consider'="λ_. True"])
      (auto dest: interaction_any_bounded_converterD)

  show ?thesis using assms
    by(coinduction arbitrary: conv1 conv2)
      ((clarsimp simp add: results_gpv_ℐ_full[symmetric] | intro conjI strip interaction_bounded_by_map_gpv_id)+
        , drule raw_converter_invariant.results_gpv_inline[OF raw_converter_invariant_interaction_any_bounded_converter]
        , (rule exI conjI refl WT_gpv_full |  auto simp add: results_gpv_ℐ_full dest: interaction_any_bounded_converterD
          raw_converter_invariant.results_gpv_inline[OF raw_converter_invariant_interaction_any_bounded_converter])+ )
qed

lemma interaction_any_bounded_converter_of_callee [interaction_bound]:
  assumes "⋀s x. interaction_any_bounded_by (conv s x) n"
  shows "interaction_any_bounded_converter (converter_of_callee conv s) n"
  by(coinduction arbitrary: s)(auto intro!: interaction_bounded_by_map_gpv_id assms)

lemma interaction_any_bounded_converter_map_converter [interaction_bound]:
  assumes "interaction_any_bounded_converter conv n"
    and "surj k"
  shows "interaction_any_bounded_converter (map_converter f g h k conv) n"
  using assms
  by(coinduction arbitrary: conv)
    (auto 4 3 simp add: assms results'_gpv_map_gpv'[OF ‹surj k›]  intro: assms  interaction_any_bounded_by_map_gpv' dest: interaction_any_bounded_converterD)

lemma interaction_any_bounded_converter_parallel_converter:
  assumes "interaction_any_bounded_converter conv1 n"
    and "interaction_any_bounded_converter conv2 n"
  shows "interaction_any_bounded_converter (parallel_converter conv1 conv2) n"
  using assms
  by(coinduction arbitrary: conv1 conv2)
    (auto 4 4 split: sum.split intro!: interaction_bounded_by_map_gpv_id elim: interaction_any_bounded_converter.cases)

lemma interaction_any_bounded_converter_parallel_converter' [interaction_bound]:
  assumes "interaction_any_bounded_converter conv1 n"
    and "interaction_any_bounded_converter conv2 m"
  shows "interaction_any_bounded_converter (parallel_converter conv1 conv2) (max n m)"
  by(rule interaction_any_bounded_converter_parallel_converter; rule assms[THEN interaction_any_bounded_converter_mono]; simp)

lemma interaction_any_bounded_converter_converter_of_resource:
  "interaction_any_bounded_converter (converter_of_resource res) n"
  by(coinduction arbitrary: res)(auto intro: interaction_bounded_by_map_gpv_id)

lemma interaction_any_bounded_converter_converter_of_resource' [interaction_bound]:
  "interaction_any_bounded_converter (converter_of_resource res) 0"
  by(rule interaction_any_bounded_converter_converter_of_resource)

lemma interaction_any_bounded_converter_restrict_converter [interaction_bound]:
  "interaction_any_bounded_converter (restrict_converter A ℐ cnv) bound"
  if "interaction_any_bounded_converter cnv bound"
  using that
  by(coinduction arbitrary: cnv)
    (auto 4 3 dest: interaction_any_bounded_converterD dest!: in_results'_gpv_restrict_gpvD intro!: interaction_bound)

end