Session Constructive_Cryptography

Theory Resource

theory Resource imports
  CryptHOL.CryptHOL
begin

section ‹Resources›

subsection ‹Type definition›

codatatype ('a, 'b) resource
  = Resource (run_resource: "'a  ('b × ('a, 'b) resource) spmf")
  for map: map_resource'
    rel: rel_resource'

lemma case_resource_conv_run_resource: "case_resource f res = f (run_resource res)"
  by(fact resource.case_eq_if)

subsection ‹Functor›

context 
  fixes a :: "'a  'a'"
    and b :: "'b  'b'"
begin

primcorec map_resource :: "('a', 'b) resource  ('a, 'b') resource" where
  "run_resource (map_resource res) = map_spmf (map_prod b map_resource)  (run_resource res)  a"

lemma map_resource_sel [simp]:
  "run_resource (map_resource res) a' = map_spmf (map_prod b map_resource) (run_resource res (a a'))"
  by simp

declare map_resource.sel [simp del]

lemma map_resource_ctr [simp, code]:
  "map_resource (Resource f) = Resource (map_spmf (map_prod b map_resource)  f  a)"
  by(rule resource.expand; simp add: fun_eq_iff)

end

lemma map_resource_id1: "map_resource id f res = map_resource' f res"
  by(coinduction arbitrary: res)(auto simp add: rel_fun_def spmf_rel_map resource.map_sel intro!: rel_spmf_reflI)

lemma map_resource_id [simp]: "map_resource id id res = res"
  by(simp add: map_resource_id1 resource.map_id)

lemma map_resource_compose [simp]:
  "map_resource a b (map_resource a' b' res) = map_resource (a'  a) (b  b') res"
  by(coinduction arbitrary: res)(auto 4 3 intro!: rel_funI rel_spmf_reflI simp add: spmf_rel_map)

functor resource: map_resource by(simp_all add: o_def fun_eq_iff)

subsection ‹Relator›

coinductive rel_resource :: "('a  'b  bool)  ('c  'd  bool)  ('a, 'c) resource  ('b, 'd) resource  bool"
  for A B where
    rel_resourceI:
    "rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1) (run_resource res2) 
   rel_resource A B res1 res2"

lemma rel_resource_coinduct [consumes 1, case_names rel_resource, coinduct pred: rel_resource]:
  assumes "X res1 res2"
    and "res1 res2. X res1 res2 
         rel_fun A (rel_spmf (rel_prod B (λres1 res2. X res1 res2  rel_resource A B res1 res2)))
            (run_resource res1) (run_resource res2)"
  shows "rel_resource A B res1 res2"
  using assms(1) by(rule rel_resource.coinduct)(simp add: assms(2))

lemma rel_resource_simps [simp, code]:
  "rel_resource A B (Resource f) (Resource g)  rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) f g" 
  by(subst rel_resource.simps) simp

lemma rel_resourceD:
  "rel_resource A B res1 res2  rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1) (run_resource res2)"
  by(blast elim: rel_resource.cases)

lemma rel_resource_eq1: "rel_resource (=) = rel_resource'"
proof(intro ext iffI)
  show "rel_resource' B res1 res2" if "rel_resource (=) B res1 res2" for B res1 res2 using that
    by(coinduction arbitrary: res1 res2)(auto elim: rel_resource.cases)
  show "rel_resource (=) B res1 res2" if "rel_resource' B res1 res2" for B res1 res2 using that
    by(coinduction arbitrary: res1 res2)(auto 4 4 elim: resource.rel_cases intro: spmf_rel_mono_strong simp add: rel_fun_def)
qed

lemma rel_resource_eq: (* [relator_eq] *) "rel_resource (=) (=) = (=)"
  by(simp add: rel_resource_eq1 resource.rel_eq)

lemma rel_resource_mono:
  assumes "A'  A" "B  B'"
  shows "rel_resource A B  rel_resource A' B'"
proof
  show "rel_resource A' B' res1 res2" if "rel_resource A B res1 res2" for res1 res2 using that
    by(coinduct)(auto dest: rel_resourceD elim!: rel_spmf_mono prod.rel_mono_strong rel_fun_mono intro: assms[THEN predicate2D])
qed

lemma rel_resource_conversep: "rel_resource A¯¯ B¯¯ = (rel_resource A B)¯¯"
proof(intro ext iffI; simp)
  show "rel_resource A B res1 res2" if "rel_resource A¯¯ B¯¯ res2 res1"
    for A :: "'a1  'a2  bool" and B :: "'c1  'c2  bool" and res1 res2
    using that by(coinduct)
      (drule rel_resourceD, rewrite in  conversep_iff[symmetric] 
        , subst rel_fun_conversep[symmetric], subst spmf_rel_conversep[symmetric], erule rel_fun_mono
        , auto simp add: prod.rel_conversep[symmetric] rel_fun_def conversep_iff[abs_def]  elim:rel_spmf_mono prod.rel_mono_strong)

  from this[of "A¯¯" "B¯¯"]
  show "rel_resource A¯¯ B¯¯ res2 res1" if "rel_resource A B res1 res2" for res1 res2 using that by simp
qed

lemma rel_resource_map_resource'1:
  "rel_resource A B (map_resource' f res1) res2 = rel_resource A (λx. B (f x)) res1 res2"
  (is "?lhs = ?rhs")
proof
  show ?rhs if ?lhs using that
    by(coinduction arbitrary: res1 res2)
      (drule rel_resourceD, auto simp add: map_resource.sel map_resource_id1[symmetric] rel_fun_comp spmf_rel_map prod.rel_map[abs_def]
        elim!: rel_fun_mono rel_spmf_mono prod.rel_mono[THEN predicate2D, rotated -1])

  show ?lhs if ?rhs using that
    by(coinduction arbitrary: res1 res2)
      (drule rel_resourceD, auto simp add: map_resource.sel map_resource_id1[symmetric] rel_fun_comp spmf_rel_map prod.rel_map[abs_def]
        elim!: rel_fun_mono rel_spmf_mono prod.rel_mono[THEN predicate2D, rotated -1])
qed

lemma rel_resource_map_resource'2:
  "rel_resource A B res1 (map_resource' f res2) = rel_resource A (λx y. B x (f y)) res1 res2"
  using rel_resource_map_resource'1[of "conversep A" "conversep B" f res2 res1]
  by(rewrite in " = _" conversep_iff[symmetric]
      , rewrite in "_ = " conversep_iff[symmetric])
    (simp only: rel_resource_conversep[symmetric]
      , simp only: conversep_iff[abs_def])

lemmas resource_rel_map' = rel_resource_map_resource'1[abs_def] rel_resource_map_resource'2

lemma rel_resource_pos_distr:
  "rel_resource A B OO rel_resource A' B'  rel_resource (A OO A') (B OO B')"
proof(rule predicate2I)
  show "rel_resource (A OO A') (B OO B') res1 res3"
    if "(rel_resource A B OO rel_resource A' B') res1 res3"
    for res1 res3 using that
    apply(coinduction arbitrary: res1 res3)
    apply(erule relcomppE)
    apply(drule rel_resourceD)+
    apply(rule rel_fun_mono)
      apply(rule pos_fun_distr[THEN predicate2D])
      apply(erule (1) relcomppI)
     apply simp
    apply(rule rel_spmf_mono)
     apply(erule rel_spmf_pos_distr[THEN predicate2D])
    apply(auto simp add: prod.rel_compp[symmetric] elim: prod.rel_mono[THEN predicate2D, rotated -1])
    done
qed

lemma left_unique_rel_resource:
  " left_total A; left_unique B   left_unique (rel_resource A B)"
  unfolding left_unique_alt_def left_total_alt_def rel_resource_conversep[symmetric]
  apply(subst rel_resource_eq[symmetric])
  apply(rule order_trans[OF rel_resource_pos_distr])
  apply(erule (1) rel_resource_mono)
  done

lemma right_unique_rel_resource:
  " right_total A; right_unique B   right_unique (rel_resource A B)"
  unfolding right_unique_alt_def right_total_alt_def rel_resource_conversep[symmetric]
  apply(subst rel_resource_eq[symmetric])
  apply(rule order_trans[OF rel_resource_pos_distr])
  apply(erule (1) rel_resource_mono)
  done

lemma bi_unique_rel_resource [transfer_rule]:
  " bi_total A; bi_unique B   bi_unique (rel_resource A B)"
  unfolding bi_unique_alt_def bi_total_alt_def by(blast intro: left_unique_rel_resource right_unique_rel_resource)


definition rel_witness_resource :: "('a  'e  bool)  ('e  'c  bool)  ('b  'd  bool)  ('a, 'b) resource × ('c, 'd) resource  ('e, 'b × 'd) resource" where
  "rel_witness_resource A A' B = corec_resource (λ(res1, res2).
   map_spmf (map_prod id Inr  rel_witness_prod)  
   rel_witness_spmf (rel_prod B (rel_resource (A OO A') B))  
   rel_witness_fun A A' (run_resource res1, run_resource res2))"

lemma rel_witness_resource_sel [simp]:
  "run_resource (rel_witness_resource A A' B (res1, res2)) =
   map_spmf (map_prod id (rel_witness_resource A A' B)  rel_witness_prod)  
   rel_witness_spmf (rel_prod B (rel_resource (A OO A') B))  
   rel_witness_fun A A' (run_resource res1, run_resource res2)"
  by(auto simp add: rel_witness_resource_def o_def fun_eq_iff spmf.map_comp intro!: map_spmf_cong)

lemma assumes "rel_resource (A OO A') B res res'"
  and A: "left_unique A" "right_total A"
  and A': "right_unique A'" "left_total A'"
shows rel_witness_resource1: "rel_resource A (λb (b', c). b = b'  B b' c) res (rel_witness_resource A A' B (res, res'))" (is "?thesis1")
  and rel_witness_resource2: "rel_resource A' (λ(b, c') c. c = c'  B b c') (rel_witness_resource A A' B (res, res')) res'" (is "?thesis2")
proof -
  show ?thesis1 using assms(1)
  proof(coinduction arbitrary: res res')
    case rel_resource
    from this[THEN rel_resourceD] show ?case
      by(simp add: rel_fun_comp)
        (erule rel_fun_mono[OF rel_witness_fun1[OF _ A A']]
          , auto simp add: spmf_rel_map elim!: rel_spmf_mono[OF rel_witness_spmf1])
  qed
  show ?thesis2 using assms(1)
  proof(coinduction arbitrary: res res')
    case rel_resource
    from this[THEN rel_resourceD] show ?case
      by(simp add: rel_fun_comp)
        (erule rel_fun_mono[OF rel_witness_fun2[OF _ A A']]
          , auto simp add: spmf_rel_map elim!: rel_spmf_mono[OF rel_witness_spmf2])
  qed
qed

lemma rel_resource_neg_distr:
  assumes A: "left_unique A" "right_total A"
    and A': "right_unique A'" "left_total A'"
  shows "rel_resource (A OO A') (B OO B')  rel_resource A B OO rel_resource A' B'"
proof(rule predicate2I relcomppI)+
  fix res res''
  assume *: "rel_resource (A OO A') (B OO B') res res''"
  let ?res' = "map_resource' (relcompp_witness B B') (rel_witness_resource A A' (B OO B') (res, res''))"
  show "rel_resource A B res ?res'" using rel_witness_resource1[OF * A A'] unfolding resource_rel_map'
    by(rule rel_resource_mono[THEN predicate2D, rotated -1]; clarify del: relcomppE elim!: relcompp_witness)
  show "rel_resource A' B' ?res' res''" using rel_witness_resource2[OF * A A'] unfolding resource_rel_map'
    by(rule rel_resource_mono[THEN predicate2D, rotated -1]; clarify del: relcomppE elim!: relcompp_witness)
qed

lemma left_total_rel_resource:
  " left_unique A; right_total A; left_total B   left_total (rel_resource A B)"
  unfolding left_unique_alt_def left_total_alt_def rel_resource_conversep[symmetric]
  apply(subst rel_resource_eq[symmetric])
  apply(rule order_trans[rotated])
   apply(rule rel_resource_neg_distr; simp add: left_unique_alt_def)
  apply(rule rel_resource_mono; assumption)
  done

lemma right_total_rel_resource:
  " right_unique A; left_total A; right_total B   right_total (rel_resource A B)"
  unfolding right_unique_alt_def right_total_alt_def rel_resource_conversep[symmetric]
  apply(subst rel_resource_eq[symmetric])
  apply(rule order_trans[rotated])
   apply(rule rel_resource_neg_distr; simp add: right_unique_alt_def)
  apply(rule rel_resource_mono; assumption)
  done

lemma bi_total_rel_resource [transfer_rule]:
  " bi_total A; bi_unique A; bi_total B   bi_total (rel_resource A B)"
  unfolding bi_total_alt_def bi_unique_alt_def
  by(blast intro: left_total_rel_resource right_total_rel_resource)

context includes lifting_syntax begin

lemma Resource_parametric [transfer_rule]:
  "((A ===> rel_spmf (rel_prod B (rel_resource A B))) ===> rel_resource A B) Resource Resource"
  by(rule rel_funI)(simp)

lemma run_resource_parametric [transfer_rule]:
  "(rel_resource A B ===> A ===> rel_spmf (rel_prod B (rel_resource A B))) run_resource run_resource"
  by(rule rel_funI)(auto dest: rel_resourceD)

lemma corec_resource_parametric [transfer_rule]:
  "((S ===> A ===> rel_spmf (rel_prod B (rel_sum (rel_resource A B) S))) ===> S ===> rel_resource A B)
   corec_resource corec_resource"
proof((rule rel_funI)+, goal_cases)
  case (1 f g s1 s2)
  then show ?case using 1(2)
    by (coinduction arbitrary: s1 s2)
      (drule 1(1)[THEN rel_funD], auto 4 4 simp add: rel_fun_comp spmf_rel_map prod.rel_map[abs_def] split: sum.split elim!: rel_fun_mono rel_spmf_mono elim: prod.rel_mono[THEN predicate2D, rotated -1])
qed

lemma map_resource_parametric [transfer_rule]:
  "((A' ===> A) ===> (B ===> B') ===> rel_resource A B ===> rel_resource A' B') map_resource map_resource"
  unfolding map_resource_def by(transfer_prover)

lemma map_resource'_parametric [transfer_rule]:
  "((B ===> B') ===> rel_resource (=) B ===> rel_resource (=) B') map_resource' map_resource'"
  unfolding map_resource_id1[symmetric] by transfer_prover

lemma case_resource_parametric [transfer_rule]:
  "(((A ===> rel_spmf (rel_prod B (rel_resource A B))) ===> C) ===> rel_resource A B ===> C)
  case_resource case_resource"
  unfolding case_resource_conv_run_resource by transfer_prover

end

lemma rel_resource_Grp:
  "rel_resource (conversep (BNF_Def.Grp UNIV f)) (BNF_Def.Grp UNIV g) = BNF_Def.Grp UNIV (map_resource f g)"
proof((rule ext iffI)+, goal_cases)
  case (1 res res')
  have *: "rel_resource (λa b. b = f a)¯¯ (λa b. b = g a) res res'  res' = map_resource f g res"
    by(rule sym, subst (3) map_resource_id[symmetric], subst rel_resource_eq[symmetric])
      (erule map_resource_parametric[THEN rel_funD, THEN rel_funD, THEN rel_funD, rotated -1]
        , auto simp add: rel_fun_def)

  from 1 show ?case unfolding Grp_def using * by (clarsimp simp add: * simp del: conversep_iff)
next
  case (2 _ _)
  then show ?case 
    by(clarsimp simp add: Grp_iff, subst map_resource_id[symmetric])
      (rule map_resource_parametric[THEN rel_funD, THEN rel_funD, THEN rel_funD, rotated -1]
        , subst rel_resource_eq, auto simp add: Grp_iff rel_fun_def)
qed

subsection ‹Losslessness›

coinductive lossless_resource :: "('a, 'b) ('a, 'b) resource  bool"
  for  where
    lossless_resourceI: "lossless_resource  res" if
    "a. a  outs_ℐ   lossless_spmf (run_resource res a)"
    "a b res'.  a  outs_ℐ ; (b, res')  set_spmf (run_resource res a)   lossless_resource  res'"

lemma lossless_resource_coinduct [consumes 1, case_names lossless_resource, case_conclusion lossless_resource lossless step, coinduct pred: lossless_resource]:
  assumes "X res"
    and "res a.  X res; a  outs_ℐ    lossless_spmf (run_resource res a) 
          ((b, res')  set_spmf (run_resource res a). X res'  lossless_resource  res')"
  shows "lossless_resource  res"
  using assms(1) by(rule lossless_resource.coinduct)(auto dest: assms(2))

lemma lossless_resourceD:
  " lossless_resource  res; a  outs_ℐ  
   lossless_spmf (run_resource res a)  ((x, res')set_spmf (run_resource res a). lossless_resource  res')"
  by(auto elim: lossless_resource.cases)

lemma lossless_resource_mono:
  assumes "lossless_resource ℐ' res"
    and le: "outs_ℐ   outs_ℐ ℐ'"
  shows "lossless_resource  res"
  using assms(1)
  by(coinduction arbitrary: res)(auto dest: lossless_resourceD intro: subsetD[OF le])

lemma lossless_resource_mono': 
  " lossless_resource ℐ' res;   ℐ'   lossless_resource  res"
  by(erule lossless_resource_mono)(simp add: le_ℐ_def)


subsection ‹Operations›

context fixes "oracle" :: "'s  'a  ('b × 's) spmf" begin

primcorec resource_of_oracle :: "'s  ('a, 'b) resource" where
  "run_resource (resource_of_oracle s) = (λa. map_spmf (map_prod id resource_of_oracle) (oracle s a))"

end

lemma resource_of_oracle_parametric [transfer_rule]: includes lifting_syntax shows
  "((S ===> A ===> rel_spmf (rel_prod B S)) ===> S ===> rel_resource A B) resource_of_oracle resource_of_oracle"
  unfolding resource_of_oracle_def by transfer_prover

lemma map_resource_resource_of_oracle:
  "map_resource f g (resource_of_oracle oracle s) = resource_of_oracle (map_fun id (map_fun f (map_spmf (map_prod g id))) oracle) s"
  for s :: 's
  using resource_of_oracle_parametric[of "BNF_Def.Grp UNIV (id :: 's  _)" "conversep (BNF_Def.Grp UNIV f)" "BNF_Def.Grp UNIV g"]
  unfolding prod.rel_Grp option.rel_Grp pmf.rel_Grp rel_fun_Grp rel_resource_Grp
  by simp
    (subst (asm) (1 2) eq_alt[symmetric]
      , subst (asm) (1 2) conversep_eq[symmetric]
      , subst (asm) (1 2) eq_alt
      , unfold rel_fun_Grp, simp add: rel_fun_Grp rel_fun_def Grp_iff)

lemma (in callee_invariant_on) lossless_resource_of_oracle:
  assumes *: "s x.  x  outs_ℐ ; I s   lossless_spmf (callee s x)"
    and "I s" 
  shows "lossless_resource  (resource_of_oracle callee s)"
  using I s by(coinduction arbitrary: s)(auto intro: * dest: callee_invariant)

context includes lifting_syntax begin

lemma resource_of_oracle_rprodl: includes lifting_syntax shows
  "resource_of_oracle ((rprodl ---> id ---> map_spmf (map_prod id lprodr)) oracle) ((s1, s2), s3) = 
    resource_of_oracle oracle (s1, s2, s3)"
  by(rule resource_of_oracle_parametric[of "BNF_Def.Grp UNIV rprodl" "(=)" "(=)", THEN rel_funD, THEN rel_funD, unfolded rel_resource_eq])
    (auto simp add: Grp_iff rel_fun_def spmf_rel_map intro!: rel_spmf_reflI)

lemma resource_of_oracle_extend_state_oracle [simp]:
  "resource_of_oracle (extend_state_oracle oracle) (s', s) = resource_of_oracle oracle s"
  by(rule resource_of_oracle_parametric[of "conversep (BNF_Def.Grp UNIV (λs. (s', s)))" "(=)" "(=)", THEN rel_funD, THEN rel_funD, unfolded rel_resource_eq])
    (auto simp add: Grp_iff rel_fun_def spmf_rel_map intro!: rel_spmf_reflI)

end

lemma exec_gpv_resource_of_oracle:
  "exec_gpv run_resource gpv (resource_of_oracle oracle s) = map_spmf (map_prod id (resource_of_oracle oracle)) (exec_gpv oracle gpv s)"
  by(subst spmf.map_id[symmetric], fold pmf.rel_eq)
    (rule pmf.map_transfer[THEN rel_funD, THEN rel_funD, rotated]
      , rule exec_gpv_parametric[where S="λres s. res = resource_of_oracle oracle s" and CALL="(=)" and A="(=)", THEN rel_funD, THEN rel_funD, THEN rel_funD]
      , auto simp add: gpv.rel_eq rel_fun_def spmf_rel_map elim: option.rel_cases intro!: rel_spmf_reflI)

primcorec parallel_resource :: "('a, 'b) resource  ('c, 'd) resource  ('a + 'c, 'b + 'd) resource" where
  "run_resource (parallel_resource res1 res2) = 
   (λac. case ac of Inl a  map_spmf (map_prod Inl (λres1'. parallel_resource res1' res2)) (run_resource res1 a)
         | Inr c  map_spmf (map_prod Inr (λres2'. parallel_resource res1 res2')) (run_resource res2 c))"

lemma parallel_resource_parametric [transfer_rule]: includes lifting_syntax shows
  "(rel_resource A B ===> rel_resource C D ===> rel_resource (rel_sum A C) (rel_sum B D))
   parallel_resource parallel_resource"
  unfolding parallel_resource_def by transfer_prover

text ‹
  We cannot define the analogue of @{term plus_oracle} because we no longer have access to the state,
  so state sharing is not possible!  So we can only compose resources, but we cannot build one
  resource with several interfaces this way!
›

lemma resource_of_parallel_oracle:
  "resource_of_oracle (parallel_oracle oracle1 oracle2) (s1, s2) =
   parallel_resource (resource_of_oracle oracle1 s1) (resource_of_oracle oracle2 s2)"
  by(coinduction arbitrary: s1 s2)
    (auto 4 3 simp add: rel_fun_def spmf_rel_map split: sum.split intro!: rel_spmf_reflI)

lemma parallel_resource_assoc: ― ‹There's still an ugly map operation in there to rebalance the interface trees, but well...›
  "parallel_resource (parallel_resource res1 res2) res3 = 
   map_resource rsuml lsumr (parallel_resource res1 (parallel_resource res2 res3))"
  by(coinduction arbitrary: res1 res2 res3)
    (auto 4 5 intro!: rel_funI rel_spmf_reflI simp add: spmf_rel_map split: sum.split)


lemma lossless_parallel_resource:
  assumes "lossless_resource  res1" "lossless_resource ℐ' res2"
  shows "lossless_resource (  ℐ') (parallel_resource res1 res2)"
  using assms
  by(coinduction arbitrary: res1 res2)(clarsimp; erule PlusE; simp; frule (1) lossless_resourceD; auto 4 3)

subsection ‹Well-typing›

coinductive WT_resource :: "('a, 'b) ('a, 'b) resource  bool" ("_ /⊢res _ " [100, 0] 99)
  for  where
    WT_resourceI: " ⊢res res "
  if "q r res'.  q  outs_ℐ ; (r, res')  set_spmf (run_resource res q)   r  responses_ℐ  q   ⊢res res' " 

lemma WT_resource_coinduct [consumes 1, case_names WT_resource, case_conclusion WT_resource response WT_resource, coinduct pred: WT_resource]:
  assumes "X res"
    and "res q r res'.  X res; q  outs_ℐ ; (r, res')  set_spmf (run_resource res q) 
        r  responses_ℐ  q  (X res'   ⊢res res' )"
  shows " ⊢res res "
  using assms(1) by(rule WT_resource.coinduct)(blast dest: assms(2))

lemma WT_resourceD:
  assumes " ⊢res res " "q  outs_ℐ " "(r, res')  set_spmf (run_resource res q)"
  shows "r  responses_ℐ  q   ⊢res res' "
  using assms by(auto elim: WT_resource.cases)

lemma WT_resource_of_oracle [simp]:
  assumes "s.  ⊢c oracle s "
  shows " ⊢res resource_of_oracle oracle s "
  by(coinduction arbitrary: s)(auto dest: WT_calleeD[OF assms])

lemma WT_resource_bot [simp]: "bot ⊢res res "
  by(rule WT_resource.intros)auto

lemma WT_resource_full: "ℐ_full ⊢res res "
  by(coinduction arbitrary: res)(auto)

lemma (in callee_invariant_on) WT_resource_of_oracle:
  "I s   ⊢res resource_of_oracle callee s "
  by(coinduction arbitrary: s)(auto dest: callee_invariant')

named_theorems WT_intro "Interface typing introduction rules"

lemmas [WT_intro] = WT_gpv_map_gpv' WT_gpv_map_gpv

lemma WT_parallel_resource [WT_intro]:
  assumes "ℐ1 ⊢res res1 "
    and "ℐ2 ⊢res res2 "
  shows "ℐ1  ℐ2 ⊢res parallel_resource res1 res2 "
  using assms
  by(coinduction arbitrary: res1 res2)(auto 4 4 intro!: imageI dest: WT_resourceD)

lemma callee_invariant_run_resource: "callee_invariant_on run_resource (λres.   ⊢res res ) "
  by(unfold_locales)(auto dest: WT_resourceD intro: WT_calleeI)

lemma callee_invariant_run_lossless_resource:
  "callee_invariant_on run_resource (λres. lossless_resource  res   ⊢res res ) "
  by(unfold_locales)(auto dest: WT_resourceD lossless_resourceD intro: WT_calleeI)

interpretation run_lossless_resource:
  callee_invariant_on run_resource "λres. lossless_resource  res   ⊢res res "  for 
  by(rule callee_invariant_run_lossless_resource)

end

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
    "xresults_converter (ℐ_uniform A UNIV) (ℐ_uniform UNIV R) conv. B x" 
    "outouts_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 ¦ _  solvesclarsimp 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

Theory Converter_Rewrite

theory Converter_Rewrite imports
  Converter
begin

section ‹Equivalence of converters restricted by interfaces›

coinductive eq_resource_on :: "'a set  ('a, 'b) resource  ('a, 'b) resource  bool" ("_ R/ _ / _" [100, 99, 99] 99)
  for A where
    eq_resource_onI: "A R res  res'" if
    "a. a  A  rel_spmf (rel_prod (=) (eq_resource_on A)) (run_resource res a) (run_resource res' a)"

lemma eq_resource_on_coinduct [consumes 1, case_names eq_resource_on, coinduct pred: eq_resource_on]:
  assumes "X res res'"
    and "res res' a.  X res res'; a  A 
       rel_spmf (rel_prod (=) (λres res'. X res res'  A R res  res')) (run_resource res a) (run_resource res' a)"
  shows "A R res  res'"
  using assms(1) by(rule eq_resource_on.coinduct)(auto dest: assms(2))

lemma eq_resource_onD:
  assumes "A R res  res'" "a  A"
  shows "rel_spmf (rel_prod (=) (eq_resource_on A)) (run_resource res a) (run_resource res' a)"
  using assms by(auto elim: eq_resource_on.cases)

lemma eq_resource_on_refl [simp]: "A R res  res"
  by(coinduction arbitrary: res)(auto intro: rel_spmf_reflI)

lemma eq_resource_on_reflI: "res = res'  A R res  res'"
  by(simp add: eq_resource_on_refl)

lemma eq_resource_on_sym: "A R res  res'" if "A R res'  res"
  using that
  by(coinduction arbitrary: res res')
    (drule (1) eq_resource_onD, rewrite in "" conversep_iff[symmetric]
      , auto simp add: spmf_rel_conversep[symmetric] elim!: rel_spmf_mono)

lemma eq_resource_on_trans [trans]: "A R res  res''" if "A R res  res'" "A R res'  res''"
  using that by(coinduction arbitrary: res res' res'')
    ((drule (1) eq_resource_onD)+, drule (1) rel_spmf_OO_trans, auto elim!:rel_spmf_mono) 

lemma eq_resource_on_UNIV_D [simp]: "res = res'" if "UNIV R res  res'"
  using that by(coinduction arbitrary: res res')(auto dest: eq_resource_onD)

lemma eq_resource_on_UNIV_iff: "UNIV R res  res'  res = res'"
  by(auto dest: eq_resource_on_UNIV_D)

lemma eq_resource_on_mono: " A' R res  res'; A  A'   A R res  res'"
  by(coinduction arbitrary: res res')(auto dest: eq_resource_onD elim!: rel_spmf_mono)

lemma eq_resource_on_empty [simp]: "{} R res  res'"
  by(rule eq_resource_onI; simp)

lemma eq_resource_on_resource_of_oracleI:
  includes lifting_syntax 
  fixes S
  assumes sim: "(S ===> eq_on A ===> rel_spmf (rel_prod (=) S)) r1 r2"
    and S: "S s1 s2"
  shows "A R resource_of_oracle r1 s1  resource_of_oracle r2 s2"
  using S  by(coinduction arbitrary: s1 s2)
    (drule sim[THEN rel_funD, THEN rel_funD], simp add: eq_on_def
      , fastforce simp add: eq_on_def spmf_rel_map elim: rel_spmf_mono)

lemma exec_gpv_eq_resource_on:
  assumes "outs_ℐ  R res  res'"
    and " ⊢g gpv "
    and " ⊢res res "
  shows "rel_spmf (rel_prod (=) (eq_resource_on (outs_ℐ ))) (exec_gpv run_resource gpv res) (exec_gpv run_resource gpv res')"
  using assms
proof(induction arbitrary: res res' gpv rule: exec_gpv_fixp_induct)
  case (step exec_gpv')
  have[simp]: "(s, r1)  set_spmf (run_resource res g1); (s, r2)  set_spmf (run_resource res' g1);
    IO g1 g2  set_spmf (the_gpv gpv); outs_ℐ  R r1  r2  rel_spmf (rel_prod (=) (eq_resource_on (outs_ℐ ))) 
        (exec_gpv' (g2 s) r1) (exec_gpv' (g2 s) r2)" for g1 g2 r1 s r2
    by(rule step.IH, simp, rule WT_gpv_ContD[OF step.prems(2)], assumption)
      (auto elim: outs_gpv.IO WT_calleeD[OF run_resource.WT_callee, OF step.prems(3)]
        dest!: WT_resourceD[OF step.prems(3), rotated 1] intro: WT_gpv_outs_gpv[THEN subsetD, OF step.prems(2)])

  show ?case
    by(clarsimp intro!: rel_spmf_bind_reflI step.prems split!: generat.split)
      (rule rel_spmf_bindI', rule eq_resource_onD[OF step.prems(1)]
        , auto elim: outs_gpv.IO intro:  eq_resource_onD[OF step.prems(1)] WT_gpv_outs_gpv[THEN subsetD, OF step.prems(2)])
qed simp_all

inductive eq_ℐ_generat :: "('a  'b  bool)  ('out, 'in) ('c  'd  bool)  ('a, 'out, 'in  'c) generat  ('b, 'out, 'in  'd) generat  bool"
  for A  D where
    Pure: "eq_ℐ_generat A  D (Pure x) (Pure y)" if "A x y"
  | IO: "eq_ℐ_generat A  D (IO out c) (IO out c')" if "out  outs_ℐ " "input. input  responses_ℐ  out  D (c input) (c' input)"

hide_fact (open) Pure IO

inductive_simps eq_ℐ_generat_simps [simp, code]:
  "eq_ℐ_generat A  D (Pure x) (Pure y)"
  "eq_ℐ_generat A  D (IO out c) (Pure y)"
  "eq_ℐ_generat A  D (Pure x) (IO out' c')"
  "eq_ℐ_generat A  D (IO out c) (IO out' c')"

inductive_simps eq_ℐ_generat_iff1:
  "eq_ℐ_generat A  D (Pure x) g'"
  "eq_ℐ_generat A  D (IO out c) g'"

inductive_simps eq_ℐ_generat_iff2:
  "eq_ℐ_generat A  D g (Pure x)"
  "eq_ℐ_generat A  D g (IO out c)"

lemma eq_ℐ_generat_mono':
  " eq_ℐ_generat A  D x y; x y. A x y  A' x y; x y. D x y  D' x y;   ℐ' 
   eq_ℐ_generat A' ℐ' D' x y"
  by(auto 4 4 elim!: eq_ℐ_generat.cases simp add: le_ℐ_def)

lemma eq_ℐ_generat_mono: "eq_ℐ_generat A  D  eq_ℐ_generat A' ℐ' D'" if "A  A'" "D  D'" "  ℐ'"
  using that by(auto elim!: eq_ℐ_generat_mono' dest: predicate2D)

lemma eq_ℐ_generat_mono'' [mono]:
  " x y. A x y  A' x y; x y. D x y  D' x y 
   eq_ℐ_generat A  D x y  eq_ℐ_generat A'  D' x y"
  by(auto elim: eq_ℐ_generat_mono')

lemma eq_ℐ_generat_conversep: "eq_ℐ_generat A¯¯  D¯¯ = (eq_ℐ_generat A  D)¯¯"
  by(fastforce elim: eq_ℐ_generat.cases)

lemma eq_ℐ_generat_reflI:
  assumes  "x. x  generat_pures generat  A x x"
    and "out c. generat = IO out c  out  outs_ℐ   (inputresponses_ℐ  out. D (c input) (c input))"
  shows "eq_ℐ_generat A  D generat generat"
  using assms by(cases generat) auto

lemma eq_ℐ_generat_relcompp:
  "eq_ℐ_generat A  D OO eq_ℐ_generat A'  D' = eq_ℐ_generat (A OO A')  (D OO D')"
  by(auto 4 3 intro!: ext elim!: eq_ℐ_generat.cases simp add: eq_ℐ_generat_iff1 eq_ℐ_generat_iff2 relcompp.simps) metis

lemma eq_ℐ_generat_map1:
  "eq_ℐ_generat A  D (map_generat f id ((∘) g) generat) generat' 
   eq_ℐ_generat (λx. A (f x))  (λx. D (g x)) generat generat'"
  by(cases generat; cases generat') auto

lemma eq_ℐ_generat_map2:
  "eq_ℐ_generat A  D generat (map_generat f id ((∘) g) generat') 
   eq_ℐ_generat (λx y. A x (f y))  (λx y. D x (g y)) generat generat'"
  by(cases generat; cases generat') auto

lemmas eq_ℐ_generat_map [simp] = 
  eq_ℐ_generat_map1[abs_def] eq_ℐ_generat_map2
  eq_ℐ_generat_map1[where g=id, unfolded fun.map_id0, abs_def] eq_ℐ_generat_map2[where g=id, unfolded fun.map_id0]

lemma eq_ℐ_generat_into_rel_generat:
  "eq_ℐ_generat A ℐ_full D generat generat'  rel_generat A (=) (rel_fun (=) D) generat generat'"
  by(erule eq_ℐ_generat.cases) auto

coinductive eq_ℐ_gpv :: "('a  'b  bool)  ('out, 'in) ('a, 'out, 'in) gpv  ('b, 'out, 'in) gpv  bool"
  for A  where
    eq_ℐ_gpvI: "eq_ℐ_gpv A  gpv gpv'" 
  if "rel_spmf (eq_ℐ_generat A  (eq_ℐ_gpv A )) (the_gpv gpv) (the_gpv gpv')"

lemma eq_ℐ_gpv_coinduct [consumes 1, case_names eq_ℐ_gpv, coinduct pred: eq_ℐ_gpv]:
  assumes "X gpv gpv'"
    and "gpv gpv'. X gpv gpv'
       rel_spmf (eq_ℐ_generat A  (λgpv gpv'. X gpv gpv'  eq_ℐ_gpv A  gpv gpv')) (the_gpv gpv) (the_gpv gpv')"
  shows "eq_ℐ_gpv A  gpv gpv'"
  using assms(1) by(rule eq_ℐ_gpv.coinduct)(blast dest: assms(2))

lemma eq_ℐ_gpvD:
  "eq_ℐ_gpv A  gpv gpv'  rel_spmf (eq_ℐ_generat A  (eq_ℐ_gpv A )) (the_gpv gpv) (the_gpv gpv')"
  by(blast elim!: eq_ℐ_gpv.cases)

lemma eq_ℐ_gpv_Done [intro!]: "A x y  eq_ℐ_gpv A  (Done x) (Done y)"
  by(rule eq_ℐ_gpvI) simp

lemma eq_ℐ_gpv_Done_iff [simp]: "eq_ℐ_gpv A  (Done x) (Done y)  A x y"
  by(auto dest: eq_ℐ_gpvD)

lemma eq_ℐ_gpv_Pause:
  " out  outs_ℐ ; input. input  responses_ℐ  out  eq_ℐ_gpv A  (rpv input) (rpv' input) 
   eq_ℐ_gpv A  (Pause out rpv) (Pause out rpv')"
  by(rule eq_ℐ_gpvI) simp

lemma eq_ℐ_gpv_mono: "eq_ℐ_gpv A   eq_ℐ_gpv A' ℐ'" if A: "A  A'" "  ℐ'"
proof
  show "eq_ℐ_gpv A' ℐ' gpv gpv'" if "eq_ℐ_gpv A  gpv gpv'" for gpv gpv' using that
    by(coinduction arbitrary: gpv gpv')
      (drule eq_ℐ_gpvD, auto dest: eq_ℐ_gpvD elim: rel_spmf_mono eq_ℐ_generat_mono[OF A(1) _ A(2), THEN predicate2D, rotated -1])
qed

lemma eq_ℐ_gpv_mono':
  " eq_ℐ_gpv A  gpv gpv'; x y. A x y  A' x y;   ℐ'   eq_ℐ_gpv A' ℐ' gpv gpv'"
  by(blast intro: eq_ℐ_gpv_mono[THEN predicate2D])

lemma eq_ℐ_gpv_mono'' [mono]:
  "eq_ℐ_gpv A  gpv gpv'  eq_ℐ_gpv A'  gpv gpv'" if "x y. A x y  A' x y"
  using that by(blast intro: eq_ℐ_gpv_mono')

lemma eq_ℐ_gpv_conversep: "eq_ℐ_gpv A¯¯  = (eq_ℐ_gpv A )¯¯"
proof(intro ext iffI; simp)
  show "eq_ℐ_gpv A  gpv gpv'" if "eq_ℐ_gpv A¯¯  gpv' gpv" for A and gpv gpv' using that
    by(coinduction arbitrary: gpv gpv')
      (drule eq_ℐ_gpvD, rewrite in  conversep_iff[symmetric]
        , auto simp add: pmf.rel_conversep[symmetric] option.rel_conversep[symmetric] eq_ℐ_generat_conversep[symmetric] elim: eq_ℐ_generat_mono' rel_spmf_mono)

  from this[of "conversep A"] show "eq_ℐ_gpv A¯¯  gpv' gpv" if "eq_ℐ_gpv A  gpv gpv'" for gpv gpv'
    using that by simp
qed

lemma eq_ℐ_gpv_reflI:
  " x. x  results_gpv  gpv  A x x;  ⊢g gpv    eq_ℐ_gpv A  gpv gpv"
  by(coinduction arbitrary: gpv)(auto intro!: rel_spmf_reflI eq_ℐ_generat_reflI elim!: generat.set_cases intro: results_gpv.intros dest: WT_gpvD)

lemma eq_ℐ_gpv_into_rel_gpv: "eq_ℐ_gpv A ℐ_full gpv gpv'  rel_gpv A (=) gpv gpv'"
  by(coinduction arbitrary: gpv gpv')
    (drule eq_ℐ_gpvD, auto elim: spmf_rel_mono_strong generat.rel_mono_strong dest: eq_ℐ_generat_into_rel_generat )

lemma eq_ℐ_gpv_relcompp: "eq_ℐ_gpv (A OO A')  = eq_ℐ_gpv A  OO eq_ℐ_gpv A' " (is "?lhs = ?rhs")
proof(intro ext iffI relcomppI; (elim relcomppE)?)
  fix gpv gpv''
  assume *: "?lhs gpv gpv''"
  define middle where "middle = corec_gpv (λ(gpv, gpv'').
    map_spmf (map_generat (relcompp_witness A A') (relcompp_witness (=) (=)) ((∘) Inr  rel_witness_fun (=) (=))  
              rel_witness_generat)
    (rel_witness_spmf (eq_ℐ_generat (A OO A')  (eq_ℐ_gpv (A OO A') )) (the_gpv gpv, the_gpv gpv'')))"
  have middle_sel [simp]: "the_gpv (middle (gpv, gpv'')) = 
     map_spmf (map_generat (relcompp_witness A A') (relcompp_witness (=) (=)) ((∘) middle  rel_witness_fun (=) (=))  
              rel_witness_generat)
    (rel_witness_spmf (eq_ℐ_generat (A OO A')  (eq_ℐ_gpv (A OO A') )) (the_gpv gpv, the_gpv gpv''))"
    for gpv gpv'' by(auto simp add: middle_def spmf.map_comp o_def generat.map_comp)
  show "eq_ℐ_gpv A  gpv (middle (gpv, gpv''))" using *
    by(coinduction arbitrary: gpv gpv'')
      (drule eq_ℐ_gpvD, simp add: spmf_rel_map, erule rel_witness_spmf1[THEN rel_spmf_mono]
        , auto 4 3 del: relcomppE elim!: relcompp_witness eq_ℐ_generat.cases)

  show "eq_ℐ_gpv A'  (middle (gpv, gpv'')) gpv''" using *
    by(coinduction arbitrary: gpv gpv'')
      (drule eq_ℐ_gpvD, simp add: spmf_rel_map, erule rel_witness_spmf2[THEN rel_spmf_mono]
        , auto 4 3 del: relcomppE elim: rel_witness_spmf2[THEN rel_spmf_mono] elim!: relcompp_witness eq_ℐ_generat.cases)
next
  show "?lhs gpv gpv''" if "eq_ℐ_gpv A  gpv gpv'" and "eq_ℐ_gpv A'  gpv' gpv''" for gpv gpv' gpv'' using that
    by(coinduction arbitrary: gpv gpv' gpv'')
      ((drule eq_ℐ_gpvD)+, simp, drule (1) rel_spmf_OO_trans, erule rel_spmf_mono
        , auto simp add: eq_ℐ_generat_relcompp elim: eq_ℐ_generat_mono')
qed

lemma eq_ℐ_gpv_map_gpv1: "eq_ℐ_gpv A  (map_gpv f id gpv) gpv'  eq_ℐ_gpv (λx. A (f x))  gpv gpv'" (is "?lhs  ?rhs")
proof
  show ?rhs if ?lhs using that
    by(coinduction arbitrary: gpv gpv')
      (drule eq_ℐ_gpvD, auto simp add: gpv.map_sel spmf_rel_map elim!: rel_spmf_mono eq_ℐ_generat_mono')
  show ?lhs if ?rhs using that
    by(coinduction arbitrary: gpv gpv')
      (drule eq_ℐ_gpvD, auto simp add: gpv.map_sel spmf_rel_map elim!: rel_spmf_mono eq_ℐ_generat_mono')
qed

lemma eq_ℐ_gpv_map_gpv2: "eq_ℐ_gpv A  gpv (map_gpv f id gpv') = eq_ℐ_gpv (λx y. A x (f y))  gpv gpv'"
  using eq_ℐ_gpv_map_gpv1[of "conversep A"  f gpv' gpv]
  by(rewrite in "_ = " conversep_iff[symmetric] , simp add: eq_ℐ_gpv_conversep[symmetric])
    (subst (asm) eq_ℐ_gpv_conversep , simp add: conversep_iff[abs_def])

lemmas eq_ℐ_gpv_map_gpv [simp] = eq_ℐ_gpv_map_gpv1[abs_def] eq_ℐ_gpv_map_gpv2

lemma (in callee_invariant_on) eq_ℐ_exec_gpv:
  " eq_ℐ_gpv A  gpv gpv'; I s   rel_spmf (rel_prod A (eq_onp I)) (exec_gpv callee gpv s) (exec_gpv callee gpv' s)"
proof(induction arbitrary: s gpv gpv' rule: parallel_fixp_induct_2_2[OF partial_function_definitions_spmf partial_function_definitions_spmf exec_gpv.mono exec_gpv.mono exec_gpv_def exec_gpv_def, unfolded lub_spmf_empty, case_names adm bottom step])
  case adm show ?case by simp
  case bottom show ?case by simp
  case (step exec_gpv' exec_gpv'')
  show ?case using step.prems
    by - (drule eq_ℐ_gpvD, erule rel_spmf_bindI
        , auto split!: generat.split simp add: eq_onp_same_args 
        intro: WT_callee[THEN WT_calleeD] callee_invariant step.IH intro!: rel_spmf_bind_reflI)
qed

lemma eq_ℐ_gpv_coinduct_bind [consumes 1, case_names eq_ℐ_gpv]:
  fixes gpv :: "('a, 'out, 'in) gpv" and gpv' :: "('a', 'out, 'in) gpv"
  assumes X: "X gpv gpv'"
    and step: "gpv gpv'. X gpv gpv'
       rel_spmf (eq_ℐ_generat A  (λgpv gpv'. X gpv gpv'  eq_ℐ_gpv A  gpv gpv'  
      (gpv'' gpv''' (B :: 'b  'b'  bool) f g. gpv = bind_gpv gpv'' f  gpv' = bind_gpv gpv''' g  eq_ℐ_gpv B  gpv'' gpv'''  (rel_fun B X) f g))) (the_gpv gpv) (the_gpv gpv')"
  shows "eq_ℐ_gpv A  gpv gpv'"
proof -
  fix x y
  define gpv'' :: "('b, 'out, 'in) gpv" where "gpv''  Done x"
  define f :: "'b  ('a, 'out, 'in) gpv" where "f  λ_. gpv"
  define gpv''' :: "('b', 'out, 'in) gpv" where "gpv'''  Done y"
  define g :: "'b'  ('a', 'out, 'in) gpv" where "g  λ_. gpv'"
  have "eq_ℐ_gpv (λx y. X (f x) (g y))  gpv'' gpv'''" using X
    by(simp add: f_def g_def gpv''_def gpv'''_def)
  then have "eq_ℐ_gpv A  (bind_gpv gpv'' f) (bind_gpv gpv''' g)"
    by(coinduction arbitrary: gpv'' f gpv''' g)
      (drule eq_ℐ_gpvD, (clarsimp simp add: bind_gpv.sel spmf_rel_map simp del: bind_gpv_sel' elim!: rel_spmf_bindI split!: generat.split dest!: step)
        , erule rel_spmf_mono, (erule eq_ℐ_generat.cases; clarsimp), (erule meta_allE, erule (1) meta_impE)
        , (fastforce | force intro: exI[where x="Done _"] elim!: eq_ℐ_gpv_mono' dest: rel_funD)+)

  then show ?thesis unfolding gpv''_def gpv'''_def f_def g_def by simp
qed

context
  fixes S :: "'s1  's2  bool"
    and callee1 :: "'s1  'out  ('in × 's1, 'out', 'in') gpv"
    and callee2 :: "'s2  'out  ('in × 's2, 'out', 'in') gpv"
    and  :: "('out, 'in) ℐ"
    and ℐ' :: "('out', 'in') ℐ"
  assumes callee: "s1 s2 q.  S s1 s2; q  outs_ℐ    eq_ℐ_gpv (rel_prod (eq_onp (λr. r  responses_ℐ  q)) S) ℐ' (callee1 s1 q) (callee2 s2 q)"
begin

lemma eq_ℐ_gpv_inline1:
  includes lifting_syntax
  assumes "S s1 s2" "eq_ℐ_gpv A  gpv1 gpv2"
  shows "rel_spmf (rel_sum (rel_prod A S) 
      (λ(q, rpv1, rpv2) (q', rpv1', rpv2'). q = q'  q'  outs_ℐ ℐ'  (q''  outs_ℐ . 
          (r  responses_ℐ ℐ' q'. eq_ℐ_gpv (rel_prod (eq_onp (λr'. r'  responses_ℐ  q'')) S) ℐ' (rpv1 r) (rpv1' r))  
          (r'  responses_ℐ  q''. eq_ℐ_gpv A  (rpv2 r') (rpv2' r')))))
     (inline1 callee1 gpv1 s1) (inline1 callee2 gpv2 s2)"
  using assms
proof(induction arbitrary: gpv1 gpv2 s1 s2 rule: parallel_fixp_induct_2_2[OF partial_function_definitions_spmf partial_function_definitions_spmf inline1.mono inline1.mono inline1_def inline1_def, unfolded lub_spmf_empty, case_names adm bottom step])
  case adm show ?case by simp
  case bottom show ?case by simp
  case (step inline1' inline1'')
  from step.prems show ?case
    by - (erule eq_ℐ_gpvD[THEN rel_spmf_bindI]
        , clarsimp split!: generat.split
        , erule eq_ℐ_gpvD[OF callee(1), THEN rel_spmf_bindI]
        , auto simp add: eq_onp_def intro: step.IH[THEN rel_spmf_mono] elim: eq_ℐ_gpvD[OF callee(1), THEN rel_spmf_bindI] split!: generat.split)
qed

lemma eq_ℐ_gpv_inline:
  assumes S: "S s1 s2"
    and gpv: "eq_ℐ_gpv A  gpv1 gpv2"
  shows "eq_ℐ_gpv (rel_prod A S) ℐ' (inline callee1 gpv1 s1) (inline callee2 gpv2 s2)"
  using S gpv
  by (coinduction arbitrary: gpv1 gpv2 s1 s2 rule: eq_ℐ_gpv_coinduct_bind)
    (clarsimp simp add: inline_sel spmf_rel_map, drule (1) eq_ℐ_gpv_inline1
      , fastforce split!: generat.split sum.split del: disjCI intro!: disjI2 rel_funI elim: rel_spmf_mono simp add: eq_onp_def)

end

lemma eq_ℐ_gpv_left_gpv_cong:
  "eq_ℐ_gpv A  gpv gpv'  eq_ℐ_gpv A (  ℐ') (left_gpv gpv) (left_gpv gpv')"
  by(coinduction arbitrary: gpv gpv')
    (drule eq_ℐ_gpvD, auto 4 4 simp add: spmf_rel_map elim!: rel_spmf_mono eq_ℐ_generat.cases)

lemma eq_ℐ_gpv_right_gpv_cong:
  "eq_ℐ_gpv A ℐ' gpv gpv'  eq_ℐ_gpv A (  ℐ') (right_gpv gpv) (right_gpv gpv')"
  by(coinduction arbitrary: gpv gpv')
    (drule eq_ℐ_gpvD, auto 4 4 simp add: spmf_rel_map elim!: rel_spmf_mono eq_ℐ_generat.cases)

lemma eq_ℐ_gpvD_WT1: " eq_ℐ_gpv A  gpv gpv';  ⊢g gpv     ⊢g gpv' "
  by(coinduction arbitrary: gpv gpv')(fastforce simp add: eq_ℐ_generat_iff2 dest: WT_gpv_ContD eq_ℐ_gpvD dest!: rel_setD2 set_spmf_parametric[THEN rel_funD])

lemma eq_ℐ_gpvD_results_gpv2: 
  assumes "eq_ℐ_gpv A  gpv gpv'" "y  results_gpv  gpv'"
  shows "x  results_gpv  gpv. A x y"
  using assms(2,1)
  by(induction arbitrary: gpv)
    (fastforce dest!: set_spmf_parametric[THEN rel_funD] rel_setD2 dest: eq_ℐ_gpvD simp add: eq_ℐ_generat_iff2 intro: results_gpv.intros)+


coinductive eq_ℐ_converter :: "('a, 'b) ('out, 'in) ('a, 'b, 'out, 'in) converter  ('a, 'b, 'out, 'in) converter  bool"
  ("_,_ C/ _ / _" [100, 0, 99, 99] 99)
  for  ℐ' where
    eq_ℐ_converterI: ", ℐ' C conv  conv'" if
    "q. q  outs_ℐ   eq_ℐ_gpv (rel_prod (eq_onp (λr. r  responses_ℐ  q)) (eq_ℐ_converter  ℐ')) ℐ' (run_converter conv q) (run_converter conv' q)"

lemma eq_ℐ_converter_coinduct [consumes 1, case_names eq_ℐ_converter, coinduct pred: eq_ℐ_converter]:
  assumes "X conv conv'"
    and "conv conv' q.  X conv conv'; q  outs_ℐ  
      eq_ℐ_gpv (rel_prod (eq_onp (λr. r  responses_ℐ  q)) (λconv conv'. X conv conv'  , ℐ' C conv  conv')) ℐ'
           (run_converter conv q) (run_converter conv' q)"
  shows ", ℐ' C conv  conv'"
  using assms(1) by(rule eq_ℐ_converter.coinduct)(blast dest: assms(2))

lemma eq_ℐ_converterD: 
  "eq_ℐ_gpv (rel_prod (eq_onp (λr. r  responses_ℐ  q)) (eq_ℐ_converter  ℐ')) ℐ' (run_converter conv q) (run_converter conv' q)"
  if ", ℐ' C conv  conv'" "q  outs_ℐ "
  using that by(blast elim: eq_ℐ_converter.cases)

lemma eq_ℐ_converter_reflI: ", ℐ' C conv  conv" if ", ℐ' C conv "
  using that by(coinduction arbitrary: conv)(auto intro!: eq_ℐ_gpv_reflI dest: WT_converterD simp add: eq_onp_same_args)

lemma eq_ℐ_converter_sym [sym]: ", ℐ' C conv  conv'" if ", ℐ' C conv'  conv"
  using that
  by(coinduction arbitrary: conv conv')
    (drule (1) eq_ℐ_converterD, rewrite in  conversep_iff[symmetric]
      ,  auto simp add: eq_ℐ_gpv_conversep[symmetric] eq_onp_def elim: eq_ℐ_gpv_mono')

lemma eq_ℐ_converter_trans [trans]:
  " , ℐ' C conv  conv'; , ℐ' C conv'  conv''   , ℐ' C conv  conv''"
  by(coinduction arbitrary: conv conv' conv'')
    ((drule (1) eq_ℐ_converterD)+, drule (1) eq_ℐ_gpv_relcompp[THEN fun_cong, THEN fun_cong, THEN iffD2, OF relcomppI]
      , auto simp add: eq_OO prod.rel_compp[symmetric] eq_onp_def elim!: eq_ℐ_gpv_mono')

lemma eq_ℐ_converter_mono:
  assumes *: "ℐ1, ℐ2 C conv  conv'"
    and le: "ℐ1'  ℐ1" "ℐ2  ℐ2'"
  shows "ℐ1', ℐ2' C conv  conv'"
  using *
  by(coinduction arbitrary: conv conv')
    (auto simp add: eq_onp_def dest!:eq_ℐ_converterD  intro: responses_ℐ_mono[THEN subsetD, OF le(1)] 
      elim!: eq_ℐ_gpv_mono'[OF _ _ le(2)] outs_ℐ_mono[THEN subsetD, OF le(1)])

lemma eq_ℐ_converter_eq: "conv1 = conv2" if "ℐ_full, ℐ_full C conv1  conv2"
  using that
  by(coinduction arbitrary: conv1 conv2)
    (auto simp add: eq_ℐ_gpv_into_rel_gpv eq_onp_def intro!: rel_funI elim!: gpv.rel_mono_strong eq_ℐ_gpv_into_rel_gpv dest:eq_ℐ_converterD)

lemma eq_ℐ_attach_on: (* TODO: generalise to eq_resource_on *)
  assumes "ℐ' ⊢res res " "ℐ_uniform A UNIV, ℐ' C conv  conv'"
  shows "A R attach conv res  attach conv' res"
  using assms
  by(coinduction arbitrary: conv conv' res)
    (auto 4 4 simp add: eq_onp_def spmf_rel_map dest: eq_ℐ_converterD intro!: rel_funI run_resource.eq_ℐ_exec_gpv[THEN rel_spmf_mono])

lemma eq_ℐ_attach_on':
  assumes "ℐ' ⊢res res " ", ℐ' C conv  conv'" "A  outs_ℐ "
  shows "A R attach conv res  attach conv' res"
  using assms(1) assms(2)[THEN eq_ℐ_converter_mono]
  by(rule eq_ℐ_attach_on)(use assms(3) in auto simp add: le_ℐ_def›)

lemma eq_ℐ_attach:
  " ℐ' ⊢res res ; ℐ_full, ℐ' C conv  conv'   attach conv res = attach conv' res"
  by(rule eq_resource_on_UNIV_D)(simp add: eq_ℐ_attach_on)

lemma eq_ℐ_comp_cong:
  " ℐ1, ℐ2 C conv1  conv1'; ℐ2, ℐ3 C conv2  conv2' 
   ℐ1, ℐ3 C comp_converter conv1 conv2  comp_converter conv1' conv2'"
  by(coinduction arbitrary: conv1 conv2 conv1' conv2')
    (clarsimp, rule eq_ℐ_gpv_mono'[OF eq_ℐ_gpv_inline[where S="eq_ℐ_converter ℐ2 ℐ3"]]
      , (fastforce elim!: eq_ℐ_converterD)+)

lemma comp_converter_cong: "comp_converter conv1 conv2 = comp_converter conv1' conv2'"
  if "ℐ_full,  C conv1  conv1'" ", ℐ_full C conv2  conv2'"
  by(rule eq_ℐ_converter_eq)(rule eq_ℐ_comp_cong[OF that])

lemma parallel_converter2_id_id: 
  "ℐ1  ℐ2, ℐ1  ℐ2 C parallel_converter2 id_converter id_converter  id_converter"
  by(coinduction)(auto split: sum.split intro!: eq_ℐ_gpv_Pause simp add: eq_onp_same_args)

lemma parallel_converter2_eq_ℐ_cong:
  " ℐ1, ℐ1' C conv1  conv1'; ℐ2, ℐ2' C conv2  conv2' 
   ℐ1  ℐ2, ℐ1'  ℐ2' C parallel_converter2 conv1 conv2  parallel_converter2 conv1' conv2'"
  by(coinduction arbitrary: conv1 conv2 conv1' conv2')
    (fastforce intro!: eq_ℐ_gpv_left_gpv_cong eq_ℐ_gpv_right_gpv_cong dest: eq_ℐ_converterD elim!: eq_ℐ_gpv_mono' simp add: eq_onp_def)

lemma id_converter_eq_self: ",ℐ' C id_converter  id_converter" if "  ℐ'"
  by(rule eq_ℐ_converter_mono[OF _ order_refl that])(rule eq_ℐ_converter_reflI[OF WT_converter_id])

lemma eq_ℐ_converterD_WT1:
  assumes ",ℐ' C conv1  conv2" and ",ℐ' C conv1 "
  shows ",ℐ' C conv2 "
  using assms
  by(coinduction arbitrary: conv1 conv2)
    (drule (1) eq_ℐ_converterD, auto 4 3 dest: eq_ℐ_converterD eq_ℐ_gpvD_WT1 WT_converterD_WT WT_converterD_results eq_ℐ_gpvD_results_gpv2 simp add: eq_onp_def)

lemma eq_ℐ_converterD_WT:
  assumes ",ℐ' C conv1  conv2"
  shows ",ℐ' C conv1   ,ℐ' C conv2 "
proof(rule iffI, goal_cases)
  case 1 then show ?case using assms by (auto intro: eq_ℐ_converterD_WT1) 
next
  case 2 then show ?case using assms[symmetric] by (auto intro: eq_ℐ_converterD_WT1)
qed

lemma eq_ℐ_gpv_Fail [simp]: "eq_ℐ_gpv A  Fail Fail"
  by(rule eq_ℐ_gpv.intros) simp

lemma eq_ℐ_restrict_gpv:
  assumes "eq_ℐ_gpv A  gpv gpv'"
  shows "eq_ℐ_gpv A  (restrict_gpv  gpv) gpv'"
  using assms
  by(coinduction arbitrary: gpv gpv')
    (fastforce dest: eq_ℐ_gpvD simp add: spmf_rel_map pmf.rel_map option_rel_Some1 eq_ℐ_generat_iff1 elim!: pmf.rel_mono_strong eq_ℐ_generat_mono' split: option.split generat.split)

lemma eq_ℐ_restrict_converter:
  assumes ",ℐ' C cnv "
    and "outs_ℐ   A"
  shows ",ℐ' C restrict_converter A ℐ' cnv  cnv"
  using assms(1)
  by(coinduction arbitrary: cnv)
    (use assms(2) in auto intro!: eq_ℐ_gpv_reflI eq_ℐ_restrict_gpv simp add: eq_onp_def dest: WT_converterD›)

lemma eq_ℐ_restrict_gpv_full:
  "eq_ℐ_gpv A ℐ_full (restrict_gpv  gpv) (restrict_gpv  gpv')"
  if "eq_ℐ_gpv A  gpv gpv'"
  using that
  by(coinduction arbitrary: gpv gpv')
    (fastforce dest: eq_ℐ_gpvD simp add: pmf.rel_map in_set_spmf[symmetric] elim!: pmf.rel_mono_strong split!: option.split generat.split)

lemma eq_ℐ_restrict_converter_cong:
  assumes ",ℐ' C cnv  cnv'"
    and "A  outs_ℐ "
  shows "restrict_converter A ℐ' cnv = restrict_converter A ℐ' cnv'"
  using assms
  by(coinduction arbitrary: cnv cnv')
    (fastforce intro: eq_ℐ_gpv_into_rel_gpv eq_ℐ_restrict_gpv_full elim!: eq_ℐ_gpv_mono' simp add: eq_onp_def rel_fun_def gpv.rel_map dest: eq_ℐ_converterD)

end

Theory Random_System

section ‹Trace equivalence for resources›

theory Random_System imports Converter_Rewrite begin

fun trace_callee :: "('a, 'b, 's) callee  's spmf  ('a × 'b) list  'a  'b spmf" where
  "trace_callee callee p [] x = bind_spmf p (λs. map_spmf fst (callee s x))"
| "trace_callee callee p ((a, b) # xs) x = 
   trace_callee callee (cond_spmf_fst (bind_spmf p (λs. callee s a)) b) xs x"

definition trace_callee_eq :: "('a, 'b, 's1) callee  ('a, 'b, 's2) callee  'a set  's1 spmf  's2 spmf  bool" where
  "trace_callee_eq callee1 callee2 A p q  
  (xs. set xs  A × UNIV  (x  A. trace_callee callee1 p xs x = trace_callee callee2 q xs x))"

abbreviation trace_callee_eq' :: "'a set  ('a, 'b, 's1) callee  's1  ('a, 'b, 's2) callee  's2  bool"
  ("_ C/ (_'((_)')) / (_'((_)'))" [90, 0, 0, 0, 0] 91)
  where "trace_callee_eq' A callee1 s1 callee2 s2  trace_callee_eq callee1 callee2 A (return_spmf s1) (return_spmf s2)"

lemma trace_callee_eqI:
  assumes "xs x.  set xs  A × UNIV; x  A 
     trace_callee callee1 p xs x = trace_callee callee2 q xs x"
  shows "trace_callee_eq callee1 callee2 A p q"
  using assms by(simp add: trace_callee_eq_def)

lemma trace_callee_eqD:
  assumes "trace_callee_eq callee1 callee2 A p q"
    and "set xs  A × UNIV" "x  A"
  shows "trace_callee callee1 p xs x = trace_callee callee2 q xs x"
  using assms by(simp add: trace_callee_eq_def)

lemma cond_spmf_fst_None [simp]: "cond_spmf_fst (return_pmf None) x = return_pmf None"
  by(simp)

lemma trace_callee_None [simp]:
  "trace_callee callee (return_pmf None) xs x = return_pmf None"
  by(induction xs)(auto)

proposition trace'_eqI_sim:
  fixes callee1 :: "('a, 'b, 's1) callee" and callee2 :: "('a, 'b, 's2) callee"
  assumes start: "S p q"
    and step: "p q a.  S p q; a  A  
      bind_spmf p (λs. map_spmf fst (callee1 s a)) = bind_spmf q (λs. map_spmf fst (callee2 s a))"
    and sim: "p q a res b s'.  S p q; a  A; res  set_spmf q; (b, s')  set_spmf (callee2 res a) 
       S (cond_spmf_fst (bind_spmf p (λs. callee1 s a)) b)
            (cond_spmf_fst (bind_spmf q (λs. callee2 s a)) b)"
  shows "trace_callee_eq callee1 callee2 A p q"
proof(rule trace_callee_eqI)
  fix xs :: "('a × 'b) list" and z
  assume xs: "set xs  A × UNIV" and z: "z  A"

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

fun trace_callee_aux :: "('a, 'b, 's) callee  's spmf  ('a × 'b) list  's spmf" where
  "trace_callee_aux callee p [] = p"
| "trace_callee_aux callee p ((x, y) # xs) = trace_callee_aux callee (cond_spmf_fst (bind_spmf p (λres. callee res x)) y) xs"

lemma trace_callee_conv_trace_callee_aux:
  "trace_callee callee p xs a = bind_spmf (trace_callee_aux callee p xs) (λs. map_spmf fst (callee s a))"
  by(induction xs arbitrary: p)(auto simp add: split_def)

lemma trace_callee_aux_append:
  "trace_callee_aux callee p (xs @ ys) = trace_callee_aux callee (trace_callee_aux callee p xs) ys"
  by(induction xs arbitrary: p)(auto simp add: split_def)

inductive trace_callee_closure :: "('a, 'b, 's1) callee  ('a, 'b, 's2) callee  'a set  's1 spmf  's2 spmf  's1 spmf  's2 spmf  bool"
  for callee1 callee2 A p q where
    "trace_callee_closure callee1 callee2 A p q (trace_callee_aux callee1 p xs) (trace_callee_aux callee2 q xs)" if "set xs  A × UNIV"

lemma trace_callee_closure_start: "trace_callee_closure callee1 callee2 A p q p q"
  by(simp add: trace_callee_closure.simps exI[where x="[]"])

lemma trace_callee_closure_step:
  assumes "trace_callee_eq callee1 callee2 A p q"
    and "trace_callee_closure callee1 callee2 A p q p' q'"
    and "a  A"
  shows "bind_spmf p' (λs. map_spmf fst (callee1 s a)) = bind_spmf q' (λs. map_spmf fst (callee2 s a))"
proof -
  from assms(2) obtain xs where xs: "set xs  A × UNIV" 
    and p: "p' = trace_callee_aux callee1 p xs" and q: "q' = trace_callee_aux callee2 q xs" by(cases)
  from trace_callee_eqD[OF assms(1) xs assms(3)] p q show ?thesis 
    by(simp add: trace_callee_conv_trace_callee_aux)
qed

lemma trace_callee_closure_sim:
  assumes "trace_callee_closure callee1 callee2 A p q p' q'"
    and "a  A"
  shows "trace_callee_closure callee1 callee2 A p q
     (cond_spmf_fst (bind_spmf p' (λs. callee1 s a)) b)
     (cond_spmf_fst (bind_spmf q' (λs. callee2 s a)) b)"
  using assms  proof (cases)
  case (1 xs)
  then show ?thesis by 
      (auto simp add:trace_callee_closure.simps assms trace_callee_aux_append split_def map_spmf_conv_bind_spmf intro!: exI[where x="xs @ [(a, b)]"])     
qed

proposition trace_callee_eq_complete:
  assumes "trace_callee_eq callee1 callee2 A p q"
  obtains S
  where "S p q"                          
    and "p q a.  S p q; a  A  
      bind_spmf p (λs. map_spmf fst (callee1 s a)) = bind_spmf q (λs. map_spmf fst (callee2 s a))"
    and "p q a s b s'.  S p q; a  A; s  set_spmf q; (b, s')  set_spmf (callee2 s a) 
       S (cond_spmf_fst (bind_spmf p (λs. callee1 s a)) b)
            (cond_spmf_fst (bind_spmf q (λs. callee2 s a)) b)"
  by(rule that[where S="trace_callee_closure callee1 callee2 A p q"])
    (auto intro: trace_callee_closure_start trace_callee_closure_step[OF assms] trace_callee_closure_sim)

lemma set_spmf_cond_spmf_fst: "set_spmf (cond_spmf_fst p a) = snd ` (set_spmf p  {a} × UNIV)"
  by(simp add: cond_spmf_fst_def)

lemma trace_callee_eq_run_gpv:
  fixes callee1 :: "('a, 'b, 's1) callee" and callee2 :: "('a, 'b, 's2) callee"
  assumes trace_eq: "trace_callee_eq callee1 callee2 A p q"
    and inv1: "callee_invariant_on callee1 I1 "
    and inv1: "callee_invariant_on callee2 I2 "
    and WT: " ⊢g gpv "
    and out: "outs_gpv  gpv  A"
    and pq: "lossless_spmf p" "lossless_spmf q"
    and I1: "xset_spmf p. I1 x"
    and I2: "yset_spmf q. I2 y"
  shows "bind_spmf p (run_gpv callee1 gpv) = bind_spmf q (run_gpv callee2 gpv)"
proof -
  from trace_eq obtain S where start: "S p q"
    and sim: "p q a.  S p q; a  A  
      bind_spmf p (λs. map_spmf fst (callee1 s a)) = bind_spmf q (λs. map_spmf fst (callee2 s a))"
    and S: "p q a s b s'.  S p q; a  A; s  set_spmf q; (b, s')  set_spmf (callee2 s a) 
       S (cond_spmf_fst (bind_spmf p (λs. callee1 s a)) b)
            (cond_spmf_fst (bind_spmf q (λs. callee2 s a)) b)"
    by(rule trace_callee_eq_complete) blast

  interpret I1: callee_invariant_on callee1 I1  by fact
  interpret I2: callee_invariant_on callee2 I2  by fact

  from S p q out pq WT I1 I2 show ?thesis
  proof(induction arbitrary: p q gpv rule: parallel_fixp_induct_2_2[OF partial_function_definitions_spmf partial_function_definitions_spmf exec_gpv.mono exec_gpv.mono exec_gpv_def exec_gpv_def, case_names adm bottom step])
    case (step exec_gpv' g)
    have[simp]: "generat  set_spmf (the_gpv gpv) 
         p  (λxa. map_spmf fst (case generat of 
             Pure x  return_spmf (x, xa)
           | IO out c  callee1 xa out  (λ(x, y). exec_gpv' (c x) y))) =
         q  (λxa. map_spmf fst (case generat of 
             Pure x  return_spmf (x, xa)
           | IO out c  callee2 xa out  (λ(x, y). g (c x) y)))" for generat
    proof (cases generat, goal_cases)
      case (2 out rpv)
      have [simp]: "IO out rpv  set_spmf (the_gpv gpv)  generat = IO out rpv 
        map_spmf fst (p  (λxa. callee1 xa out)) = map_spmf fst (q  (λxa. callee2 xa out))"
        unfolding map_bind_spmf o_def
        by (rule sim) (use step.prems in auto intro: outs_gpv.IO›)

      have[simp]: "IO out rpv  set_spmf (the_gpv gpv); generat = IO out rpv; x  set_spmf q; (a, b)  set_spmf (callee2 x out) 
       cond_spmf_fst (p  (λxa. callee1 xa out)) a  (λx. map_spmf fst (exec_gpv' (rpv a) x)) =
       cond_spmf_fst (q  (λxa. callee2 xa out)) a  (λx. map_spmf fst (g (rpv a) x))" for a b x
      proof (rule step.IH, goal_cases)
        case 1 then show ?case using step.prems by(auto intro!: S intro: outs_gpv.IO)
      next
        case 2
        then show ?case using step.prems by(force intro: outs_gpv.Cont dest: WT_calleeD[OF I2.WT_callee] WT_gpvD[OF step.prems(5)])
      next
        case 3
        then show ?case using sim[OF S p q, of out] step.prems(2)
          by(force simp add: bind_UNION image_Union intro: rev_image_eqI intro: outs_gpv.IO dest: arg_cong[where f="set_spmf"])
      next
        case 4
        then show ?case by(auto 4 3 simp add: bind_UNION image_Union intro: rev_image_eqI)
      next
        case 5
        then show ?case using step.prems by(auto 4 3 dest: WT_calleeD[OF I2.WT_callee] intro: WT_gpvD)
      next
        case 6
        then show ?case using step.prems by(auto simp add: bind_UNION image_Union set_spmf_cond_spmf_fst intro: I1.callee_invariant WT_gpvD)
      next
        case 7
        then show ?case using step.prems by(auto simp add: bind_UNION image_Union set_spmf_cond_spmf_fst intro: I2.callee_invariant WT_gpvD)
      qed 

      from 2 show ?case 
        by(simp add: map_bind_spmf o_def)
          (subst (1 2) bind_spmf_assoc[symmetric]
            , rewrite in "bind_spmf  _ = _" cond_spmf_fst_inverse[symmetric]
            , rewrite in "_ = bind_spmf  _" cond_spmf_fst_inverse[symmetric]
            , subst (1 2) bind_spmf_assoc
            , auto simp add: bind_map_spmf o_def intro!: bind_spmf_cong)
    qed (simp add: bind_spmf_const lossless_weight_spmfD step.prems)

    show ?case unfolding map_bind_spmf o_def by(subst (1 2) bind_commute_spmf) (auto intro: bind_spmf_cong[OF refl])
  qed simp_all
qed

lemma trace_callee_eq'_run_gpv:
  fixes callee1 :: "('a, 'b, 's1) callee" and callee2 :: "('a, 'b, 's2) callee"
  assumes trace_eq: "A C callee1(s1)  callee2(s2)"
    and inv1: "callee_invariant_on callee1 I1 "
    and inv1: "callee_invariant_on callee2 I2 "
    and WT: " ⊢g gpv "
    and out: "outs_gpv  gpv  A"
    and I1: "I1 s1"
    and I2: "I2 s2"
  shows "run_gpv callee1 gpv s1 = run_gpv callee2 gpv s2"
  using trace_callee_eq_run_gpv[OF assms(1-5)] assms(6-) by simp

abbreviation trace_eq :: "'a set  ('a, 'b) resource spmf  ('a, 'b) resource spmf  bool" where
  "trace_eq  trace_callee_eq run_resource run_resource"

abbreviation trace_eq' :: "'a set  ('a, 'b) resource  ('a, 'b) resource  bool" ("(_) R/ (_)/  (_)" [90, 90, 90] 91) where
  "A R res  res'  trace_eq A (return_spmf res) (return_spmf res')"

lemma trace_callee_resource_of_oracle2:
  "trace_callee run_resource (map_spmf (resource_of_oracle callee) p) xs x =
   trace_callee callee p xs x"
proof(induction xs arbitrary: p)
  case (Cons xy xs)
  then show ?case by (cases xy) (simp add: bind_map_spmf o_def Cons.IH[symmetric] cond_spmf_fst_def map_bind_spmf[symmetric, unfolded o_def] spmf.map_comp map_prod_vimage)
qed (simp add: map_bind_spmf bind_map_spmf o_def spmf.map_comp)

lemma trace_callee_resource_of_oracle [simp]:
  "trace_callee run_resource (return_spmf (resource_of_oracle callee s)) xs x =
   trace_callee callee (return_spmf s) xs x"
  using trace_callee_resource_of_oracle2[of callee "return_spmf s" xs x] by simp

lemma trace_eq'_resource_of_oracle [simp]:
  "A R resource_of_oracle callee1 s1  resource_of_oracle callee2 s2 =
   A C callee1(s1)  callee2(s2)"
  by(simp add: trace_callee_eq_def)

end

Theory Distinguisher

section ‹Distinguisher›

theory Distinguisher imports Random_System begin

type_synonym ('a, 'b) distinguisher = "(bool, 'a, 'b) gpv"

translations
  (type) "('a, 'b) distinguisher" <= (type) "(bool, 'a, 'b) gpv"

definition connect :: "('a, 'b) distinguisher  ('a, 'b) resource  bool spmf" where
  "connect d res = run_gpv run_resource d res"

definition absorb :: "('a, 'b) distinguisher  ('a, 'b, 'out, 'in) converter  ('out, 'in) distinguisher" where
  "absorb d conv = map_gpv fst id (inline run_converter d conv)"

lemma distinguish_attach: "connect d (attach conv res) = connect (absorb d conv) res"
proof -
  let ?R = "λres (conv', res'). res = attach conv' res'"
  have*: "rel_spmf (rel_prod (=) ?R) (exec_gpv run_resource d (attach conv res))
     (exec_gpv (λp y. map_spmf (λp. (fst (fst p), snd (fst p), snd p))
       (exec_gpv run_resource (run_converter (fst p) y) (snd p))) d (conv, res))"
    by(rule exec_gpv_parametric[where S="λres (conv', res'). res = attach conv' res'" and CALL="(=)", THEN rel_funD, THEN rel_funD, THEN rel_funD])
      (auto simp add: gpv.rel_eq spmf_rel_map split_def intro: rel_spmf_reflI intro!: rel_funI)

  show ?thesis
    by(simp add: connect_def absorb_def exec_gpv_map_gpv_id spmf.map_comp exec_gpv_inline  o_def split_def spmf_rel_eq[symmetric])
      (rule pmf.map_transfer[THEN rel_funD, THEN rel_funD]
        , rule option.map_transfer[where Rb="rel_prod (=) ?R", THEN rel_funD]
        , auto simp add: * intro: fst_transfer)
qed

lemma absorb_comp_converter: "absorb d (comp_converter conv conv') = absorb (absorb d conv) conv'"
proof -
  let ?R = "λconv (conv', conv''). conv = comp_converter conv' conv''"
  have*: "rel_gpv (rel_prod (=) ?R) (=) (inline run_converter d (comp_converter conv conv'))
   (inline (λp c2. map_gpv (λp. (fst (fst p), snd (fst p), snd p)) id (inline run_converter (run_converter (fst p) c2) (snd p)))  d (conv, conv'))"
    by(rule inline_parametric[where C="(=)", THEN rel_funD, THEN rel_funD, THEN rel_funD])
      (auto simp add: gpv.rel_eq gpv.rel_map split_def intro: gpv.rel_refl_strong intro!: rel_funI)

  show ?thesis
    by(simp add: gpv.rel_eq[symmetric] absorb_def inline_map_gpv gpv.map_comp inline_assoc o_def split_def id_def[symmetric])
      (rule gpv.map_transfer[where R1b="rel_prod (=) ?R", THEN rel_funD, THEN rel_funD, THEN rel_funD]
        , auto simp add: * intro: fst_transfer id_transfer)
qed

lemma connect_cong_trace:
  fixes res1 res2 :: "('a, 'b) resource"
  assumes trace_eq: "A R res1  res2"
    and WT: " ⊢g d "
    and out: "outs_gpv  d  A"
    and WT1: " ⊢res res1 "
    and WT2: " ⊢res res2 "
  shows "connect d res1 = connect d res2"
  unfolding connect_def using trace_eq callee_invariant_run_resource callee_invariant_run_resource WT out WT1 WT2
  by(rule trace_callee_eq'_run_gpv)

lemma distinguish_trace_eq:
  assumes distinguish: "distinguisher.  ⊢g distinguisher   connect distinguisher res = connect distinguisher res'"
    and WT1: " ⊢res res1 "
    and WT2: " ⊢res res2 "
  shows "outs_ℐ  R res  res'"
proof(rule ccontr)
  let ?P = "λxs. x. set xs  outs_ℐ  × UNIV  x  outs_ℐ   trace_callee run_resource (return_spmf res) xs x  trace_callee run_resource (return_spmf res') xs x"
  assume "¬ ?thesis"
  then have "Ex ?P" unfolding trace_callee_eq_def by auto
  with wf_strict_prefix[unfolded wfP_eq_minimal, THEN spec, of "Collect ?P"]
  obtain xs x where xs: "set xs  outs_ℐ  × UNIV"
    and x: "x  outs_ℐ "
    and neq: "trace_callee run_resource (return_spmf res) xs x  trace_callee run_resource (return_spmf res') xs x"
    and shortest: "xs' x.  strict_prefix xs' xs; set xs'   outs_ℐ  × UNIV; x  outs_ℐ  
       trace_callee run_resource (return_spmf res) xs' x = trace_callee run_resource (return_spmf res') xs' x"
    by(auto)
  have shortest: "xs' x.  strict_prefix xs' xs; x  outs_ℐ  
       trace_callee run_resource (return_spmf res) xs' x = trace_callee run_resource (return_spmf res') xs' x"
    by(rule shortest)(use xs in auto 4 3 dest: strict_prefix_setD›)

  define p where "p  return_spmf res"
  define q where "q  return_spmf res'"
  have p: "lossless_spmf p" and q: "lossless_spmf q" by(simp_all add: p_def q_def)
  from neq obtain y where y: "spmf (trace_callee run_resource p xs x) y  spmf (trace_callee run_resource q xs x) y"
    by(fastforce intro: spmf_eqI simp add: p_def q_def)
  have eq: "spmf (trace_callee run_resource p ys x) y = spmf (trace_callee run_resource q ys x) y"
    if "strict_prefix ys xs" "x  outs_ℐ " for ys x y using shortest[OF that]
    by(auto intro: spmf_eqI simp add: p_def q_def)
  define d :: "('a × 'b) list  _"
    where "d = rec_list (Pause x (λy'. Done (y = y'))) (λ(x, y) xs rec. Pause x (λinput. if input = y then rec else Done False))"
  have d_simps [simp]:
    "d [] = Pause x (λy'. Done (y = y'))"
    "d ((a, b) # xs) = Pause a (λinput. if input = b then d xs else Done False)" for a b xs
    by(simp_all add: d_def fun_eq_iff)
  have WT_d: " ⊢g d xs " using xs by(induction xs)(use x in auto)
  from distinguish[OF WT_d]
  have "spmf (bind_spmf p (connect (d xs))) True = spmf (bind_spmf q (connect (d xs))) True"
    by(simp add: p_def q_def)
  thus False using y eq xs
  proof(induction xs arbitrary: p q)
    case Nil
    then show ?case
      by(simp add: connect_def[abs_def] map_bind_spmf o_def split_def)
        (simp add: map_spmf_conv_bind_spmf[symmetric] map_bind_spmf[unfolded o_def, symmetric] spmf_map vimage_def eq_commute)
  next
    case (Cons xy xs p q)
    obtain x' y' where xy [simp]: "xy = (x', y')" by(cases xy)
    let ?p = "cond_spmf_fst (p  (λs. run_resource s x')) y'"
      and ?q = "cond_spmf_fst (q  (λs. run_resource s x')) y'"
    from Cons.prems(1)
    have "spmf ((map_spmf fst (p  (λy. run_resource y x'))  (λx. map_spmf (Pair x) (cond_spmf_fst (p  (λy. run_resource y x')) x)))  (λ(a, b). if a = y' then connect (d xs) b else return_spmf False)) True =
      spmf ((map_spmf fst (q  (λy. run_resource y x'))  (λx. map_spmf (Pair x) (cond_spmf_fst (q  (λy. run_resource y x')) x)))  (λ(a, b). if a = y' then connect (d xs) b else return_spmf False)) True"
      unfolding cond_spmf_fst_inverse
      by(clarsimp simp add: connect_def[abs_def] map_bind_spmf o_def split_def if_distrib[where f="λx. run_gpv _ x _"] cong del: if_weak_cong)
    hence "spmf ((p  (λs. map_spmf fst (run_resource s x'))) 
                (λa. if a = y' then cond_spmf_fst (p  (λy. run_resource y x')) a  connect (d xs)
                          else bind_spmf (cond_spmf_fst (p  (λy. run_resource y x')) a) (λ_. return_spmf False))) True =
      spmf ((q  (λs. map_spmf fst (run_resource s x'))) 
                (λa. if a = y' then cond_spmf_fst (q  (λy. run_resource y x')) a  connect (d xs)
                            else bind_spmf (cond_spmf_fst (q  (λy. run_resource y x')) a) (λ_. return_spmf False))) True"
      by(rule box_equals; use nothing in rule arg_cong2[where f=spmf])
        (auto simp add: map_bind_spmf bind_map_spmf o_def split_def intro!: bind_spmf_cong)
    hence "LINT a|measure_spmf (p  (λs. map_spmf fst (run_resource s x'))). (if a = y' then spmf (?p  connect (d xs)) True else 0) =
      LINT a|measure_spmf (q  (λs. map_spmf fst (run_resource s x'))). (if a = y' then spmf (?q  connect (d xs)) True else 0)"
      by(rule box_equals; use nothing in subst spmf_bind›)
        (auto intro!: Bochner_Integration.integral_cong simp add: bind_spmf_const spmf_scale_spmf)
    hence "LINT a|measure_spmf (p  (λs. map_spmf fst (run_resource s x'))). indicator {y'} a * spmf (?p  connect (d xs)) True =
      LINT a|measure_spmf (q  (λs. map_spmf fst (run_resource s x'))). indicator {y'} a * spmf (?q  connect (d xs)) True"
      by(rule box_equals; use nothing in rule Bochner_Integration.integral_cong›) auto
    hence "spmf (p  (λs. map_spmf fst (run_resource s x'))) y' * spmf (?p  connect (d xs)) True =
      spmf (q  (λs. map_spmf fst (run_resource s x'))) y' * spmf (?q  connect (d xs)) True"
      by(simp add: spmf_conv_measure_spmf)
    moreover from Cons.prems(3)[of "[]" x'] Cons.prems(4)
    have "spmf (p  (λs. map_spmf fst (run_resource s x'))) y' = spmf (q  (λs. map_spmf fst (run_resource s x'))) y'"
      by(simp)
    ultimately have "spmf (?p  connect (d xs)) True = spmf (?q  connect (d xs)) True"
      by(auto simp add: cond_spmf_fst_def)(auto 4 3 simp add: spmf_eq_0_set_spmf cond_spmf_def o_def bind_UNION intro: rev_image_eqI)
    moreover
    have "spmf (trace_callee run_resource ?p xs x) y  spmf (trace_callee run_resource ?q xs x) y"
      using Cons.prems by simp
    moreover
    have "spmf (trace_callee run_resource ?p ys x) y = spmf (trace_callee run_resource ?q ys x) y"
      if ys: "strict_prefix ys xs" and x: "x  outs_ℐ " for ys x y
      using Cons.prems(3)[of "xy # ys" x y] ys x by simp
    moreover have "set xs  outs_ℐ  × UNIV" using Cons.prems(4) by auto
    ultimately show ?case by(rule Cons.IH)
  qed
qed

lemma connect_eq_resource_cong:
  assumes " ⊢g distinguisher "
    and "outs_ℐ  R res  res'"
    and " ⊢res res "
  shows "connect distinguisher res = connect distinguisher res'"
  unfolding connect_def
  by(fold spmf_rel_eq, rule map_spmf_parametric[THEN rel_funD, THEN rel_funD, rotated])
    (auto simp add: rel_fun_def intro: assms exec_gpv_eq_resource_on )

lemma WT_gpv_absorb [WT_intro]:
  " ℐ' ⊢g gpv ; ℐ',  C conv     ⊢g absorb gpv conv "
  by(simp add: absorb_def run_converter.WT_gpv_inline_invar)

lemma plossless_gpv_absorb [plossless_intro]:
  assumes gpv: "plossless_gpv ℐ' gpv"
    and conv: "plossless_converter ℐ'  conv"
    and [WT_intro]: "ℐ' ⊢g gpv " "ℐ',  C conv "
  shows "plossless_gpv  (absorb gpv conv)"
  by(auto simp add: absorb_def intro: run_plossless_converter.plossless_inline_invariant[OF gpv] WT_intro conv dest: plossless_converterD)

lemma interaction_any_bounded_by_absorb [interaction_bound]:
  assumes gpv: "interaction_any_bounded_by gpv bound1"
    and conv: "interaction_any_bounded_converter conv bound2"
  shows "interaction_any_bounded_by (absorb gpv conv) (bound1 * bound2)"
  unfolding absorb_def
  by(rule interaction_bounded_by_map_gpv_id, rule interaction_bounded_by_inline_invariant[OF gpv, rotated 2])
    (rule conv, auto elim: interaction_any_bounded_converter.cases)

end

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 ("1I")

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 ("1C")

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 swapC :: "('a + 'b, 'c + 'd, 'b + 'a, 'd + 'c) converter" where
  "swapC = map_converter swap_sum swap_sum id id 1C"

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

definition swap_rassocl where "swap_rassocl  lassocrC  (1C |= swapC)  rassoclC"
definition swap_lassocr where "swap_lassocr  rassoclC  (swapC |= 1C)  lassocrC"

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

lemma WT_lassocrC [WT_intro]: "(ℐ1  ℐ2)  ℐ3, ℐ1  (ℐ2  ℐ3) C lassocrC "
  by(coinduction)(auto simp add: lassocrC_def)

lemma WT_rassoclC [WT_intro]: "ℐ1  (ℐ2  ℐ3), (ℐ1  ℐ2)  ℐ3 C rassoclC "
  by(coinduction)(auto simp add: rassoclC_def)

lemma WT_swapC [WT_intro]: "ℐ1  ℐ2, ℐ2  ℐ1 C swapC "
  by(coinduction)(auto simp add: swapC_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_lassocrC WT_rassoclC WT_converter_parallel_converter2 WT_converter_id WT_swapC)+

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_lassocrC WT_rassoclC WT_converter_parallel_converter2 WT_converter_id WT_swapC)+

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_lassocrC WT_rassoclC 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_rassoclC [plossless_intro]: "plossless_converter (ℐ1  (ℐ2  ℐ3)) ((ℐ1  ℐ2)  ℐ3) rassoclC"
  by coinduction (auto simp add: rassoclC_def)

lemma plossless_lassocrC [plossless_intro]: "plossless_converter ((ℐ1  ℐ2)  ℐ3) (ℐ1  (ℐ2  ℐ3)) lassocrC"
  by coinduction (auto simp add: lassocrC_def)

lemma plossless_swapC [plossless_intro]: "plossless_converter (ℐ1  ℐ2) (ℐ2  ℐ1) swapC"
  by coinduction (auto simp add: swapC_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_lassocrC: "((conv1 |= conv2) |= conv3)  lassocrC = lassocrC  (conv1 |= conv2 |= conv3)"
  unfolding lassocrC_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_lassocrC' = comp_converter_eqs[OF comp_lassocrC]

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_rassoclC:
  "(conv1 |= conv2 |= conv3)  rassoclC = rassoclC  ((conv1 |= conv2) |= conv3)"
  unfolding rassoclC_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_rassoclC' = comp_converter_eqs[OF comp_rassoclC]

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_swapC: "(conv1 |= conv2)  swapC = swapC  (conv2 |= conv1)"
  unfolding swapC_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_swapC' = comp_converter_eqs[OF comp_swapC]

lemma comp_swap_lassocr: "(conv1 |= conv2 |= conv3)  swap_lassocr = swap_lassocr  (conv2 |= conv1 |= conv3)"
  unfolding swap_lassocr_def comp_rassoclC' comp_converter_assoc comp_converter_parallel2' comp_swapC' comp_converter_id_right
  by(subst (9) comp_converter_id_left[symmetric], subst comp_converter_parallel2[symmetric])
    (simp add: comp_converter_assoc comp_lassocrC)

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_lassocrC' 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_rassoclC)

lemmas comp_parallel_wiring' = comp_converter_eqs[OF comp_parallel_wiring]

lemma attach_converter_of_resource_conv_parallel_resource:
  "converter_of_resource res | 1C  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:
  " 1C | 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 lassocrC x = Pause (rsuml x) (λx. Done (lsumr x, lassocrC))"
  by(simp add: lassocrC_def o_def)

lemma run_converter_rassocl [simp]:
  "run_converter rassoclC x = Pause (lsumr x) (λx. Done (rsuml x, rassoclC))"
  by(simp add: rassoclC_def o_def)

lemma run_converter_swap [simp]: "run_converter swapC x = Pause (swap_sum x) (λx. Done (swap_sum x, swapC))"
  by(simp add: swapC_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