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