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: "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:
"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
"∀x∈results_converter (ℐ_uniform A UNIV) (ℐ_uniform UNIV R) conv. B x"
"∀out∈outs_converter (ℐ_uniform A UNIV) (ℐ_uniform UNIV R) conv. C out"
lemma pred_gpv'_mono_weak:
"pred_gpv' A C R ≤ pred_gpv' A' C' R" if "A ≤ A'" "C ≤ C'"
using that by(auto 4 3 simp add: pred_gpv'.simps)
lemma Domainp_rel_converter_le:
"Domainp (rel_converter A B C R) ≤ pred_converter (Collect (Domainp A)) (Domainp B) (Domainp C) (Collect (Domainp R))"
(is "?lhs ≤ ?rhs")
proof(intro predicate1I pred_converter.intros strip)
fix conv
assume *: "?lhs conv"
let ?ℐ = "ℐ_uniform (Collect (Domainp A)) UNIV" and ?ℐ' = "ℐ_uniform UNIV (Collect (Domainp R))"
show "Domainp B x" if "x ∈ results_converter ?ℐ ?ℐ' conv" for x using that *
apply(induction)
apply clarsimp
apply(erule rel_converter.cases; clarsimp)
apply(drule (1) rel_funD)
apply(drule Domainp_rel_gpv''_le[THEN predicate1D, OF DomainPI])
apply(erule pred_gpv'.cases)
apply fastforce
apply clarsimp
apply(erule rel_converter.cases; clarsimp)
apply(drule (1) rel_funD)
apply(drule Domainp_rel_gpv''_le[THEN predicate1D, OF DomainPI])
apply(erule pred_gpv'.cases)
apply fastforce
done
show "Domainp C x" if "x ∈ outs_converter ?ℐ ?ℐ' conv" for x using that *
apply induction
apply clarsimp
apply(erule rel_converter.cases; clarsimp)
apply(drule (1) rel_funD)
apply(drule Domainp_rel_gpv''_le[THEN predicate1D, OF DomainPI])
apply(erule pred_gpv'.cases)
apply fastforce
apply clarsimp
apply(erule rel_converter.cases; clarsimp)
apply(drule (1) rel_funD)
apply(drule Domainp_rel_gpv''_le[THEN predicate1D, OF DomainPI])
apply(erule pred_gpv'.cases)
apply fastforce
done
qed
lemma rel_converter_Grp:
"rel_converter (BNF_Def.Grp UNIV f)¯¯ (BNF_Def.Grp B g) (BNF_Def.Grp C h) (BNF_Def.Grp UNIV k)¯¯ =
BNF_Def.Grp {conv. results_converter (ℐ_uniform (range f) UNIV) (ℐ_uniform UNIV (range k)) conv ⊆ B ∧
outs_converter (ℐ_uniform (range f) UNIV) (ℐ_uniform UNIV (range k)) conv ⊆ C}
(map_converter f g h k)"
(is "?lhs = ?rhs")
including lifting_syntax
proof(intro ext GrpI iffI CollectI conjI subsetI)
let ?ℐ = "ℐ_uniform (range f) UNIV" and ?ℐ' = "ℐ_uniform UNIV (range k)"
fix conv conv'
assume *: "?lhs conv conv'"
then show "map_converter f g h k conv = conv'"
apply(coinduction arbitrary: conv conv')
apply(drule rel_converterD)
apply(unfold map_converter.sel)
apply(subst (2) map_fun_def[symmetric])
apply(subst map_fun2_id)
apply(subst rel_fun_comp)
apply(rule rel_fun_map_fun1)
apply(erule rel_fun_mono, simp)
apply(simp add: gpv.rel_map)
by (auto simp add: rel_gpv_conv_rel_gpv'' prod.rel_map intro!: predicate2I rel_gpv''_map_gpv'1
elim!: rel_gpv''_mono[THEN predicate2D, rotated -1] prod.rel_mono_strong GrpE)
show "b ∈ B" if "b ∈ results_converter ?ℐ ?ℐ' conv" for b using * that
by - (drule Domainp_rel_converter_le[THEN predicate1D, OF DomainPI]
, auto simp add: Domainp_conversep Rangep_Grp iff: Grp_iff elim: pred_converter.cases)
show "out ∈ C" if "out ∈ outs_converter ?ℐ ?ℐ' conv" for out using * that
by - (drule Domainp_rel_converter_le[THEN predicate1D, OF DomainPI]
, auto simp add: Domainp_conversep Rangep_Grp iff: Grp_iff elim: pred_converter.cases)
next
let ?abr1="λconv. results_converter (ℐ_uniform (range f) UNIV) (ℐ_uniform UNIV (range k)) conv ⊆ B"
let ?abr2="λconv. outs_converter (ℐ_uniform (range f) UNIV) (ℐ_uniform UNIV (range k)) conv ⊆ C"
fix conv conv'
assume "?rhs conv conv'"
hence *: "conv' = map_converter f g h k conv" and f1: "?abr1 conv" and f2: "?abr2 conv" by(auto simp add: Grp_iff)
have[intro]: "?abr1 conv ⟹ ?abr2 conv ⟹ z ∈ run_converter conv ` range f ⟹
out ∈ outs_gpv (ℐ_uniform UNIV (range k)) z ⟹ BNF_Def.Grp C h out (h out)" for conv z out
by(auto simp add: Grp_iff elim: outs_converter.Out elim!: subsetD)
from f1 f2 show "?lhs conv conv'" unfolding *
apply(coinduction arbitrary: conv)
apply(unfold map_converter.sel)
apply(subst (2) map_fun_def[symmetric])
apply(subst map_fun2_id)
apply(subst rel_fun_comp)
apply(rule rel_fun_map_fun2)
apply(rule rel_fun_refl_eq_onp)
apply(unfold map_gpv_conv_map_gpv' gpv.comp comp_id)
apply(subst map_gpv'_id12)
apply(rule rel_gpv''_map_gpv'2)
apply(unfold rel_gpv''_map_gpv)
apply(rule rel_gpv''_refl_eq_on)
apply(simp add: prod.rel_map)
apply(rule prod.rel_refl_strong)
apply(clarsimp simp add: Grp_iff)
by (auto intro: results_converter.Result results_converter.Cont outs_converter.Cont elim!: subsetD)
qed
context
includes lifting_syntax
notes [transfer_rule] = map_gpv_parametric'
begin
lemma Converter_parametric [transfer_rule]:
"((A ===> rel_gpv'' (rel_prod B (rel_converter A B C R)) C R) ===> rel_converter A B C R) Converter Converter"
by(rule rel_funI)(simp)
lemma run_converter_parametric [transfer_rule]:
"(rel_converter A B C R ===> A ===> rel_gpv'' (rel_prod B (rel_converter A B C R)) C R)
run_converter run_converter"
by(rule rel_funI)(auto dest: rel_converterD)
lemma corec_converter_parametric [transfer_rule]:
"((S ===> A ===> rel_gpv'' (rel_prod B (rel_sum (rel_converter A B C R) S)) C R) ===> S ===> rel_converter A B C R)
corec_converter corec_converter"
proof((rule rel_funI)+, goal_cases)
case (1 f g s1 s2)
then show ?case
by(coinduction arbitrary: s1 s2)
(drule 1(1)[THEN rel_funD]
, auto 4 4 simp add: rel_fun_comp prod.rel_map[abs_def] rel_gpv''_map_gpv prod.rel_map split: sum.split
intro: prod.rel_mono elim!: rel_fun_mono rel_gpv''_mono[THEN predicate2D, rotated -1])
qed
lemma map_converter_parametric [transfer_rule]:
"((A' ===> A) ===> (B ===> B') ===> (C ===> C') ===> (R' ===> R) ===> rel_converter A B C R ===> rel_converter A' B' C' R')
map_converter map_converter"
unfolding map_converter_def by(transfer_prover)
lemma map_converter'_parametric [transfer_rule]:
"((B ===> B') ===> (C ===> C') ===> rel_converter (=) B C (=) ===> rel_converter (=) B' C' (=))
map_converter' map_converter'"
unfolding map_converter_id14[symmetric] by transfer_prover
lemma case_converter_parametric [transfer_rule]:
"(((A ===> rel_gpv'' (rel_prod B (rel_converter A B C R)) C R) ===> X) ===> rel_converter A B C R ===> X)
case_converter case_converter"
unfolding case_converter_conv_run_converter by transfer_prover
end
subsection ‹Well-typing›
coinductive WT_converter :: "('a, 'b) ℐ ⇒ ('out, 'in) ℐ ⇒ ('a, 'b, 'out, 'in) converter ⇒ bool"
("_,/ _ ⊢⇩C/ _ √" [100, 0, 0] 99)
for ℐ ℐ' where
WT_converterI: "ℐ, ℐ' ⊢⇩C conv √" if
"⋀q. q ∈ outs_ℐ ℐ ⟹ ℐ' ⊢g run_converter conv q √"
"⋀q r conv'. ⟦ q ∈ outs_ℐ ℐ; (r, conv') ∈ results_gpv ℐ' (run_converter conv q) ⟧ ⟹ r ∈ responses_ℐ ℐ q ∧ ℐ, ℐ' ⊢⇩C conv' √"
lemma WT_converter_coinduct[consumes 1, case_names WT_converter, case_conclusion WT_converter WT_gpv results_gpv, coinduct pred: WT_converter]:
assumes "X conv"
and "⋀conv q r conv'. ⟦ X conv; q ∈ outs_ℐ ℐ ⟧
⟹ ℐ' ⊢g run_converter conv q √ ∧
((r, conv') ∈ results_gpv ℐ' (run_converter conv q) ⟶ r ∈ responses_ℐ ℐ q ∧ (X conv' ∨ ℐ, ℐ' ⊢⇩C conv' √))"
shows "ℐ, ℐ' ⊢⇩C conv √"
using assms(1) by(rule WT_converter.coinduct)(blast dest: assms(2))
lemma WT_converterD:
assumes "ℐ, ℐ' ⊢⇩C conv √" "q ∈ outs_ℐ ℐ"
shows WT_converterD_WT: "ℐ' ⊢g run_converter conv q √"
and WT_converterD_results: "(r, conv') ∈ results_gpv ℐ' (run_converter conv q) ⟹ r ∈ responses_ℐ ℐ q ∧ ℐ, ℐ' ⊢⇩C conv' √"
using assms by(auto elim: WT_converter.cases)
lemma WT_converterD':
assumes "ℐ, ℐ' ⊢⇩C conv √" "q ∈ outs_ℐ ℐ"
shows "ℐ' ⊢g run_converter conv q √ ∧ (∀(r, conv') ∈ results_gpv ℐ' (run_converter conv q). r ∈ responses_ℐ ℐ q ∧ ℐ, ℐ' ⊢⇩C conv' √)"
using assms by(auto elim: WT_converter.cases)
lemma WT_converter_bot1 [simp]: "bot, ℐ ⊢⇩C conv √"
by(rule WT_converter.intros) auto
lemma WT_converter_mono:
"⟦ ℐ1,ℐ2 ⊢⇩C conv √; ℐ1' ≤ ℐ1; ℐ2 ≤ ℐ2' ⟧ ⟹ ℐ1',ℐ2' ⊢⇩C conv √ "
apply(coinduction arbitrary: conv)
apply(auto)
apply(drule WT_converterD_WT)
apply(erule (1) outs_ℐ_mono[THEN subsetD])
apply(erule WT_gpv_mono)
apply(erule outs_ℐ_mono)
apply(erule (1) responses_ℐ_mono)
apply(frule WT_converterD_results)
apply(erule (1) outs_ℐ_mono[THEN subsetD])
apply(erule results_gpv_mono[THEN subsetD])
apply(erule WT_converterD_WT)
apply(erule (1) outs_ℐ_mono[THEN subsetD])
apply simp
apply clarify
apply(erule (2) responses_ℐ_mono[THEN subsetD])
apply(frule WT_converterD_results)
apply(erule (1) outs_ℐ_mono[THEN subsetD])
apply(erule results_gpv_mono[THEN subsetD])
apply(erule WT_converterD_WT)
apply(erule (1) outs_ℐ_mono[THEN subsetD])
apply simp
apply simp
done
lemma callee_invariant_on_run_resource [simp]: "callee_invariant_on run_resource (WT_resource ℐ) ℐ"
by(unfold_locales)(auto dest: WT_resourceD intro: WT_calleeI)
interpretation run_resource: callee_invariant_on run_resource "WT_resource ℐ" ℐ for ℐ
by simp
lemma raw_converter_invariant_run_converter: "raw_converter_invariant ℐ ℐ' run_converter (WT_converter ℐ ℐ')"
by(unfold_locales)(auto dest: WT_converterD)
interpretation run_converter: raw_converter_invariant ℐ ℐ' run_converter "WT_converter ℐ ℐ'" for ℐ ℐ'
by(rule raw_converter_invariant_run_converter)
lemma WT_converter_ℐ_full: "ℐ_full, ℐ_full ⊢⇩C conv √"
by(coinduction arbitrary: conv)(auto)
lemma WT_converter_map_converter [WT_intro]:
"ℐ, ℐ' ⊢⇩C map_converter f g f' g' conv √" if
*: "map_ℐ (inv_into UNIV f) (inv_into UNIV g) ℐ, map_ℐ f' g' ℐ' ⊢⇩C conv √"
and f: "inj f" and g: "surj g"
using *
proof(coinduction arbitrary: conv)
case (WT_converter q r conv' conv)
have "?WT_gpv" using WT_converter
by(auto intro!: WT_gpv_map_gpv' elim: WT_converterD_WT simp add: inv_into_f_f[OF f])
moreover
have "?results_gpv"
proof(intro strip conjI disjI1)
assume "(r, conv') ∈ results_gpv ℐ' (run_converter (map_converter f g f' g' conv) q)"
then obtain r' conv''
where results: "(r', conv'') ∈ results_gpv (map_ℐ f' g' ℐ') (run_converter conv (f q))"
and r: "r = g r'"
and conv': "conv' = map_converter f g f' g' conv''"
by auto
from WT_converterD_results[OF WT_converter(1), of "f q"] WT_converter(2) results
have r': "r' ∈ inv_into UNIV g ` responses_ℐ ℐ q"
and WT': "map_ℐ (inv_into UNIV f) (inv_into UNIV g) ℐ, map_ℐ f' g' ℐ' ⊢⇩C conv'' √"
by(auto simp add: inv_into_f_f[OF f])
from r' r show "r ∈ responses_ℐ ℐ q" by(auto simp add: surj_f_inv_f[OF g])
show "∃conv. conv' = map_converter f g f' g' conv ∧
map_ℐ (inv_into UNIV f) (inv_into UNIV g) ℐ, map_ℐ f' g' ℐ' ⊢⇩C conv √"
using conv' WT' by(auto)
qed
ultimately show ?case ..
qed
subsection ‹Losslessness›
coinductive plossless_converter :: "('a, 'b) ℐ ⇒ ('out, 'in) ℐ ⇒ ('a, 'b, 'out, 'in) converter ⇒ bool"
for ℐ ℐ' where
plossless_converterI: "plossless_converter ℐ ℐ' conv" if
"⋀a. a ∈ outs_ℐ ℐ ⟹ plossless_gpv ℐ' (run_converter conv a)"
"⋀a b conv'. ⟦ a ∈ outs_ℐ ℐ; (b, conv') ∈ results_gpv ℐ' (run_converter conv a) ⟧ ⟹ plossless_converter ℐ ℐ' conv'"
lemma plossless_converter_coinduct[consumes 1, case_names plossless_converter, case_conclusion plossless_converter plossless step, coinduct pred: plossless_converter]:
assumes "X conv"
and step: "⋀conv a. ⟦ X conv; a ∈ outs_ℐ ℐ ⟧ ⟹ plossless_gpv ℐ' (run_converter conv a) ∧
(∀(b, conv') ∈ results_gpv ℐ' (run_converter conv a). X conv' ∨ plossless_converter ℐ ℐ' conv')"
shows "plossless_converter ℐ ℐ' conv"
using assms(1) by(rule plossless_converter.coinduct)(auto dest: step)
lemma plossless_converterD:
"⟦ plossless_converter ℐ ℐ' conv; a ∈ outs_ℐ ℐ ⟧
⟹ plossless_gpv ℐ' (run_converter conv a) ∧
(∀(b, conv') ∈ results_gpv ℐ' (run_converter conv a). plossless_converter ℐ ℐ' conv')"
by(auto elim: plossless_converter.cases)
lemma plossless_converter_bot1 [simp]: "plossless_converter bot ℐ conv"
by(rule plossless_converterI) auto
lemma plossless_converter_mono:
assumes *: "plossless_converter ℐ1 ℐ2 conv"
and le: "outs_ℐ ℐ1' ⊆ outs_ℐ ℐ1" "ℐ2 ≤ ℐ2'"
and WT: "ℐ1, ℐ2 ⊢⇩C conv √"
shows "plossless_converter ℐ1' ℐ2' conv"
using * WT
apply(coinduction arbitrary: conv)
apply(drule plossless_converterD)
apply(erule le(1)[THEN subsetD])
apply(drule WT_converterD')
apply(erule le(1)[THEN subsetD])
using le(2)[THEN responses_ℐ_mono]
by(auto intro: plossless_gpv_mono[OF _ le(2)] results_gpv_mono[OF le(2), THEN subsetD] dest: bspec)
lemma raw_converter_invariant_run_plossless_converter: "raw_converter_invariant ℐ ℐ' run_converter (λconv. plossless_converter ℐ ℐ' conv ∧ ℐ,ℐ' ⊢⇩C conv √)"
by(unfold_locales)(auto dest: WT_converterD plossless_converterD)
interpretation run_plossless_converter: raw_converter_invariant
ℐ ℐ' run_converter "λconv. plossless_converter ℐ ℐ' conv ∧ ℐ,ℐ' ⊢⇩C conv √" for ℐ ℐ'
by(rule raw_converter_invariant_run_plossless_converter)
named_theorems plossless_intro "Introduction rules for probabilistic losslessness"
subsection ‹Operations›
context
fixes callee :: "'s ⇒ 'a ⇒ ('b × 's, 'out, 'in) gpv"
begin
primcorec converter_of_callee :: "'s ⇒ ('a, 'b, 'out, 'in) converter" where
"run_converter (converter_of_callee s) = (λa. map_gpv (map_prod id converter_of_callee) id (callee s a))"
end
lemma converter_of_callee_parametric [transfer_rule]: includes lifting_syntax shows
"((S ===> A ===> rel_gpv'' (rel_prod B S) C R) ===> S ===> rel_converter A B C R)
converter_of_callee converter_of_callee"
unfolding converter_of_callee_def supply map_gpv_parametric'[transfer_rule] by transfer_prover
lemma map_converter_of_callee:
"map_converter f g h k (converter_of_callee callee s) =
converter_of_callee (map_fun id (map_fun f (map_gpv' (map_prod g id) h k)) callee) s"
proof(coinduction arbitrary: s)
case Eq_converter
have *: "map_gpv' (map_prod g id) h k gpv = map_gpv (map_prod g id) id (map_gpv' id h k gpv)" for gpv
by(simp add: map_gpv_conv_map_gpv' gpv.compositionality)
show ?case
by(auto simp add: rel_fun_def map_gpv'_map_gpv_swap gpv.rel_map * intro!: gpv.rel_refl_strong)
qed
lemma WT_converter_of_callee:
assumes WT: "⋀s q. q ∈ outs_ℐ ℐ ⟹ ℐ' ⊢g callee s q √"
and res: "⋀s q r s'. ⟦ q ∈ outs_ℐ ℐ; (r, s') ∈ results_gpv ℐ' (callee s q) ⟧ ⟹ r ∈ responses_ℐ ℐ q"
shows "ℐ, ℐ' ⊢⇩C converter_of_callee callee s √"
by(coinduction arbitrary: s)(auto simp add: WT res)
text ‹
We can define two versions of parallel composition. One that attaches to the same interface
and one that attach to different interfaces. We choose the one variant where both attach to the same interface
because (1) this is more general and (2) we do not have to assume that the resource respects the parallel composition.
›
primcorec parallel_converter
:: "('a, 'b, 'out, 'in) converter ⇒ ('c, 'd, 'out, 'in) converter ⇒ ('a + 'c, 'b + 'd, 'out, 'in) converter"
where
"run_converter (parallel_converter conv1 conv2) = (λac. case ac of
Inl a ⇒ map_gpv (map_prod Inl (λconv1'. parallel_converter conv1' conv2)) id (run_converter conv1 a)
| Inr b ⇒ map_gpv (map_prod Inr (λconv2'. parallel_converter conv1 conv2')) id (run_converter conv2 b))"
lemma parallel_callee_parametric [transfer_rule]: includes lifting_syntax shows
"(rel_converter A B C R ===> rel_converter A' B' C R ===> rel_converter (rel_sum A A') (rel_sum B B') C R)
parallel_converter parallel_converter"
unfolding parallel_converter_def supply map_gpv_parametric'[transfer_rule] by transfer_prover
lemma parallel_converter_assoc:
"parallel_converter (parallel_converter conv1 conv2) conv3 =
map_converter rsuml lsumr id id (parallel_converter conv1 (parallel_converter conv2 conv3))"
by(coinduction arbitrary: conv1 conv2 conv3)
(auto 4 5 intro!: rel_funI gpv.rel_refl_strong split: sum.split simp add: gpv.rel_map map_gpv'_id map_gpv_conv_map_gpv'[symmetric])
lemma plossless_parallel_converter [plossless_intro]:
"⟦ plossless_converter ℐ1 ℐ conv1; plossless_converter ℐ2 ℐ conv2; ℐ1, ℐ ⊢⇩C conv1 √; ℐ2, ℐ ⊢⇩C conv2 √ ⟧
⟹ plossless_converter (ℐ1 ⊕⇩ℐ ℐ2) ℐ (parallel_converter conv1 conv2)"
by(coinduction arbitrary: conv1 conv2)
(clarsimp; erule PlusE; drule (1) plossless_converterD; drule (1) WT_converterD'; fastforce)
primcorec id_converter :: "('a, 'b, 'a, 'b) converter" where
"run_converter id_converter = (λa.
map_gpv (map_prod id (λ_. id_converter)) id (Pause a (λb. Done (b, ()))))"
lemma id_converter_parametric [transfer_rule]: "rel_converter A B A B id_converter id_converter"
unfolding id_converter_def
supply map_gpv_parametric'[transfer_rule] Done_parametric'[transfer_rule] Pause_parametric'[transfer_rule]
by transfer_prover
lemma converter_of_callee_id_oracle [simp]:
"converter_of_callee id_oracle s = id_converter"
by(coinduction) (auto simp add: id_oracle_def)
lemma conv_callee_plus_id_left: "converter_of_callee (plus_intercept id_oracle callee) s =
parallel_converter id_converter (converter_of_callee callee s) "
by (coinduction arbitrary: callee s)
(clarsimp split!: sum.split intro!: rel_funI
, force simp add: gpv.rel_map id_oracle_def, force simp add: gpv.rel_map intro!: gpv.rel_refl)
lemma conv_callee_plus_id_right: "converter_of_callee (plus_intercept callee id_oracle) s =
parallel_converter (converter_of_callee callee s) id_converter"
by (coinduction arbitrary: callee s)
(clarsimp split!: sum.split intro!: rel_funI
, (force intro: gpv.rel_refl | simp add: gpv.rel_map id_oracle_def)+)
lemma plossless_id_converter [simp, plossless_intro]: "plossless_converter ℐ ℐ id_converter"
by(coinduction) auto
lemma WT_converter_id [simp, intro, WT_intro]: "ℐ, ℐ ⊢⇩C id_converter √"
by(coinduction) auto
lemma WT_map_converter_idD:
"ℐ,ℐ' ⊢⇩C map_converter id id f g id_converter √ ⟹ ℐ ≤ map_ℐ f g ℐ'"
unfolding le_ℐ_def by(auto 4 3 dest: WT_converterD)
definition fail_converter :: "('a, 'b, 'out, 'in) converter" where
"fail_converter = Converter (λ_. Fail)"
lemma fail_converter_sel [simp]: "run_converter fail_converter a = Fail"
by(simp add: fail_converter_def)
lemma fail_converter_parametric [transfer_rule]: "rel_converter A B C R fail_converter fail_converter"
unfolding fail_converter_def supply Fail_parametric'[transfer_rule] by transfer_prover
lemma plossless_fail_converter [simp]: "plossless_converter ℐ ℐ' fail_converter ⟷ ℐ = bot" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
show ?rhs if ?lhs using that by(cases)(auto intro!: ℐ_eqI)
qed simp
lemma plossless_fail_converterI [plossless_intro]: "plossless_converter bot ℐ' fail_converter"
by simp
lemma WT_fail_converter [simp, WT_intro]: "ℐ, ℐ' ⊢⇩C fail_converter √"
by(rule WT_converter.intros) simp_all
lemma map_converter_id_move_left:
"map_converter f g f' g' id_converter = map_converter (f' ∘ f) (g ∘ g') id id id_converter"
by coinduction(simp add: rel_funI)
lemma map_converter_id_move_right:
"map_converter f g f' g' id_converter = map_converter id id (f' ∘ f) (g ∘ g') id_converter"
by coinduction(simp add: rel_funI)
text ‹
And here is the version for parallel composition that assumes disjoint interfaces.
›
primcorec parallel_converter2
:: "('a, 'b, 'out, 'in) converter ⇒ ('c, 'd, 'out', 'in') converter ⇒ ('a + 'c, 'b + 'd, 'out + 'out', 'in + 'in') converter"
where
"run_converter (parallel_converter2 conv1 conv2) = (λac. case ac of
Inl a ⇒ map_gpv (map_prod Inl (λconv1'. parallel_converter2 conv1' conv2)) id (left_gpv (run_converter conv1 a))
| Inr b ⇒ map_gpv (map_prod Inr (λconv2'. parallel_converter2 conv1 conv2')) id (right_gpv (run_converter conv2 b)))"
lemma parallel_converter2_parametric [transfer_rule]: includes lifting_syntax shows
"(rel_converter A B C R ===> rel_converter A' B' C' R'
===> rel_converter (rel_sum A A') (rel_sum B B') (rel_sum C C') (rel_sum R R'))
parallel_converter2 parallel_converter2"
unfolding parallel_converter2_def
supply left_gpv_parametric'[transfer_rule] right_gpv_parametric'[transfer_rule] map_gpv_parametric'[transfer_rule]
by transfer_prover
lemma map_converter_parallel_converter2:
"map_converter (map_sum f f') (map_sum g g') (map_sum h h') (map_sum k k') (parallel_converter2 conv1 conv2) =
parallel_converter2 (map_converter f g h k conv1) (map_converter f' g' h' k' conv2)"
using parallel_converter2_parametric[of
"conversep (BNF_Def.Grp UNIV f)" "BNF_Def.Grp UNIV g" "BNF_Def.Grp UNIV h" "conversep (BNF_Def.Grp UNIV k)"
"conversep (BNF_Def.Grp UNIV f')" "BNF_Def.Grp UNIV g'" "BNF_Def.Grp UNIV h'" "conversep (BNF_Def.Grp UNIV k')"]
unfolding sum.rel_conversep sum.rel_Grp
by(simp add: rel_converter_Grp rel_fun_def Grp_iff)
lemma WT_converter_parallel_converter2 [WT_intro]:
assumes "ℐ1,ℐ2 ⊢⇩C conv1 √"
and "ℐ1',ℐ2' ⊢⇩C conv2 √"
shows "ℐ1 ⊕⇩ℐ ℐ1',ℐ2 ⊕⇩ℐ ℐ2' ⊢⇩C parallel_converter2 conv1 conv2 √"
using assms
apply(coinduction arbitrary: conv1 conv2)
apply(clarsimp split!: sum.split)
subgoal by(auto intro: WT_gpv_left_gpv dest: WT_converterD_WT)
subgoal by(auto dest: WT_converterD_results)
subgoal by(auto dest: WT_converterD_results)
subgoal by(auto intro: WT_gpv_right_gpv dest: WT_converterD_WT)
subgoal by(auto dest: WT_converterD_results)
subgoal by(auto 4 3 dest: WT_converterD_results)
done
lemma plossless_parallel_converter2 [plossless_intro]:
assumes "plossless_converter ℐ1 ℐ1' conv1"
and "plossless_converter ℐ2 ℐ2' conv2"
shows "plossless_converter (ℐ1 ⊕⇩ℐ ℐ2) (ℐ1' ⊕⇩ℐ ℐ2') (parallel_converter2 conv1 conv2)"
using assms
by(coinduction arbitrary: conv1 conv2)
((rule exI conjI refl)+ | auto dest: plossless_converterD)+
lemma parallel_converter2_map1_out:
"parallel_converter2 (map_converter f g h k conv1) conv2 =
map_converter (map_sum f id) (map_sum g id) (map_sum h id) (map_sum k id) (parallel_converter2 conv1 conv2)"
by(simp add: map_converter_parallel_converter2)
lemma parallel_converter2_map2_out:
"parallel_converter2 conv1 (map_converter f g h k conv2) =
map_converter (map_sum id f) (map_sum id g) (map_sum id h) (map_sum id k) (parallel_converter2 conv1 conv2)"
by(simp add: map_converter_parallel_converter2)
primcorec left_interface :: "('a, 'b, 'out, 'in) converter ⇒ ('a, 'b, 'out + 'out', 'in + 'in') converter" where
"run_converter (left_interface conv) = (λa. map_gpv (map_prod id left_interface) id (left_gpv (run_converter conv a)))"
lemma left_interface_parametric [transfer_rule]: includes lifting_syntax shows
"(rel_converter A B C R ===> rel_converter A B (rel_sum C C') (rel_sum R R')) left_interface left_interface"
unfolding left_interface_def
supply left_gpv_parametric'[transfer_rule] map_gpv_parametric'[transfer_rule] by transfer_prover
primcorec right_interface :: "('a, 'b, 'out, 'in) converter ⇒ ('a, 'b, 'out' + 'out, 'in' + 'in) converter" where
"run_converter (right_interface conv) = (λa. map_gpv (map_prod id right_interface) id (right_gpv (run_converter conv a)))"
lemma right_interface_parametric [transfer_rule]: includes lifting_syntax shows
"(rel_converter A B C' R' ===> rel_converter A B (rel_sum C C') (rel_sum R R')) right_interface right_interface"
unfolding right_interface_def
supply right_gpv_parametric'[transfer_rule] map_gpv_parametric'[transfer_rule] by transfer_prover
lemma parallel_converter2_alt_def:
"parallel_converter2 conv1 conv2 = parallel_converter (left_interface conv1) (right_interface conv2)"
by(coinduction arbitrary: conv1 conv2 rule: converter.coinduct_strong)
(auto 4 5 intro!: rel_funI gpv.rel_refl_strong split: sum.split simp add: gpv.rel_map)
lemma conv_callee_parallel_id_left: "converter_of_callee (parallel_intercept id_oracle callee) (s, s') =
parallel_converter2 (id_converter) (converter_of_callee callee s')"
apply (coinduction arbitrary: callee s')
apply (rule rel_funI)
apply (clarsimp simp add: gpv.rel_map left_gpv_map[of _ _ _ "id"]
right_gpv_map[of _ _ _ "id"] split!: sum.split)
apply (force simp add: id_oracle_def split!: sum.split)
apply (rule gpv.rel_refl)
by force+
lemma conv_callee_parallel_id_right: "converter_of_callee (parallel_intercept callee id_oracle) (s, s') =
parallel_converter2 (converter_of_callee callee s) (id_converter)"
apply (coinduction arbitrary: callee s)
apply (rule rel_funI)
apply (clarsimp simp add: gpv.rel_map left_gpv_map[of _ _ _ "id"]
right_gpv_map[of _ _ _ "id"] split!: sum.split)
apply (rule gpv.rel_refl)
by (force simp add: id_oracle_def split!: sum.split)+
lemma conv_callee_parallel: "converter_of_callee (parallel_intercept callee1 callee2) (s,s')
= parallel_converter2 (converter_of_callee callee1 s) (converter_of_callee callee2 s')"
apply (coinduction arbitrary: callee1 callee2 s s')
apply (clarsimp simp add: gpv.rel_map left_gpv_map[of _ _ _ "id"] right_gpv_map[of _ _ _ "id"] intro!: rel_funI split!: sum.split)
apply (rule gpv.rel_refl)
apply force+
apply (rule gpv.rel_refl)
by force+
lemma WT_converter_parallel_converter [WT_intro]:
assumes "ℐ1, ℐ ⊢⇩C conv1 √"
and "ℐ2, ℐ ⊢⇩C conv2 √"
shows "ℐ1 ⊕⇩ℐ ℐ2, ℐ ⊢⇩C parallel_converter conv1 conv2 √"
using assms by(coinduction arbitrary: conv1 conv2)(auto 4 4 dest: WT_converterD intro!: imageI)
primcorec converter_of_resource :: "('a, 'b) resource ⇒ ('a, 'b, 'c, 'd) converter" where
"run_converter (converter_of_resource res) = (λx. map_gpv (map_prod id converter_of_resource) id (lift_spmf (run_resource res x)))"
lemma WT_converter_of_resource [WT_intro]:
assumes "ℐ ⊢res res √"
shows "ℐ, ℐ' ⊢⇩C converter_of_resource res √"
using assms by(coinduction arbitrary: res)(auto dest: WT_resourceD)
lemma plossless_converter_of_resource [plossless_intro]:
assumes "lossless_resource ℐ res"
shows "plossless_converter ℐ ℐ' (converter_of_resource res)"
using assms by(coinduction arbitrary: res)(auto 4 3 dest: lossless_resourceD)
lemma plossless_converter_of_callee:
assumes "⋀s x. x ∈ outs_ℐ ℐ1 ⟹ plossless_gpv ℐ2 (callee s x) ∧ (∀(y, s')∈results_gpv ℐ2 (callee s x). y ∈ responses_ℐ ℐ1 x)"
shows "plossless_converter ℐ1 ℐ2 (converter_of_callee callee s)"
apply(coinduction arbitrary: s)
subgoal for x s by(drule assms[where s=s]) auto
done
context
fixes A :: "'a set"
and ℐ :: "('c, 'd) ℐ"
begin
primcorec restrict_converter :: "('a, 'b, 'c, 'd) converter ⇒ ('a, 'b, 'c, 'd) converter"
where
"run_converter (restrict_converter cnv) = (λa. if a ∈ A then
map_gpv (map_prod id (λcnv'. restrict_converter cnv')) id (restrict_gpv ℐ (run_converter cnv a))
else Fail)"
end
lemma WT_restrict_converter [WT_intro]:
assumes "ℐ,ℐ' ⊢⇩C cnv √"
shows "ℐ,ℐ' ⊢⇩C restrict_converter A ℐ' cnv √"
using assms by(coinduction arbitrary: cnv)(auto dest: WT_converterD dest!: in_results_gpv_restrict_gpvD)
lemma pgen_lossless_restrict_gpv [simp]:
"ℐ ⊢g gpv √ ⟹ pgen_lossless_gpv b ℐ (restrict_gpv ℐ gpv) = pgen_lossless_gpv b ℐ gpv"
unfolding pgen_lossless_gpv_def by(simp add: expectation_gpv_restrict_gpv)
lemma plossless_restrict_converter [simp]:
assumes "plossless_converter ℐ ℐ' conv"
and "ℐ,ℐ' ⊢⇩C conv √"
and "outs_ℐ ℐ ⊆ A"
shows "plossless_converter ℐ ℐ' (restrict_converter A ℐ' conv)"
using assms
by(coinduction arbitrary: conv)
(auto dest!: in_results_gpv_restrict_gpvD WT_converterD' plossless_converterD)
lemma plossless_map_converter:
"plossless_converter ℐ ℐ' (map_converter f g h k conv)"
if "plossless_converter (map_ℐ (inv_into UNIV f) (inv_into UNIV g) ℐ) (map_ℐ h k ℐ') conv" "inj f"
using that
by(coinduction arbitrary: conv)(auto dest!: plossless_converterD[where a="f _"])
subsection ‹Attaching converters to resources›
primcorec "attach" :: "('a, 'b, 'out, 'in) converter ⇒ ('out, 'in) resource ⇒ ('a, 'b) resource" where
"run_resource (attach conv res) = (λa.
map_spmf (λ((b, conv'), res'). (b, attach conv' res')) (exec_gpv run_resource (run_converter conv a) res))"
lemma attach_parametric [transfer_rule]: includes lifting_syntax shows
"(rel_converter A B C R ===> rel_resource C R ===> rel_resource A B) attach attach"
unfolding attach_def
supply exec_gpv_parametric'[transfer_rule] by transfer_prover
lemma attach_map_converter:
"attach (map_converter f g h k conv) res = map_resource f g (attach conv (map_resource h k res))"
using attach_parametric[of "conversep (BNF_Def.Grp UNIV f)" "BNF_Def.Grp UNIV g" "BNF_Def.Grp UNIV h" "conversep (BNF_Def.Grp UNIV k)"]
unfolding rel_converter_Grp rel_resource_Grp
by (simp, rewrite at "rel_fun _ (rel_fun ⌑ _)" in asm conversep_iff[symmetric, abs_def])
(simp add: rel_resource_conversep[symmetric] rel_fun_def Grp_iff conversep_conversep rel_resource_Grp)
lemma WT_resource_attach [WT_intro]: "⟦ ℐ, ℐ' ⊢⇩C conv √; ℐ' ⊢res res √ ⟧ ⟹ ℐ ⊢res attach conv res √"
by(coinduction arbitrary: conv res)
(auto 4 3 intro!: exI dest: run_resource.in_set_spmf_exec_gpv_into_results_gpv WT_converterD intro: run_resource.exec_gpv_invariant)
lemma lossless_attach [plossless_intro]:
assumes "plossless_converter ℐ ℐ' conv"
and "lossless_resource ℐ' res"
and "ℐ, ℐ' ⊢⇩C conv √" "ℐ' ⊢res res √"
shows "lossless_resource ℐ (attach conv res)"
using assms
proof(coinduction arbitrary: res conv)
case (lossless_resource a res conv)
from plossless_converterD[OF lossless_resource(1,5)] have lossless: "plossless_gpv ℐ' (run_converter conv a)"
"⋀b conv'. (b, conv') ∈ results_gpv ℐ' (run_converter conv a) ⟹ plossless_converter ℐ ℐ' conv'" by auto
from WT_converterD'[OF lossless_resource(3,5)] have WT: "ℐ' ⊢g run_converter conv a √"
"⋀b conv'. (b, conv') ∈ results_gpv ℐ' (run_converter conv a) ⟹ b ∈ responses_ℐ ℐ a ∧ ℐ, ℐ' ⊢⇩C conv' √" by auto
have ?lossless using lossless(1) WT(1) lossless_resource(2,4)
by(auto intro: run_lossless_resource.plossless_exec_gpv dest: lossless_resourceD)
moreover have ?step (is "∀(b, res')∈?set. ?P b res' ∨ _")
proof(safe)
fix b res''
assume "(b, res'') ∈ ?set"
then obtain conv' res' where *: "((b, conv'), res') ∈ set_spmf (exec_gpv run_resource (run_converter conv a) res)"
and [simp]: "res'' = attach conv' res'" by auto
from run_lossless_resource.in_set_spmf_exec_gpv_into_results_gpv[OF *, of ℐ'] lossless_resource(2,4) WT
have conv': "(b, conv') ∈ results_gpv ℐ' (run_converter conv a)" by auto
from run_lossless_resource.exec_gpv_invariant[OF *, of ℐ'] WT(2)[OF this] WT(1) lossless(2)[OF this] lossless_resource
show "?P b res''" by auto
qed
ultimately show ?case ..
qed
definition attach_callee
:: "('s ⇒ 'a ⇒ ('b × 's, 'out, 'in) gpv)
⇒ ('s' ⇒ 'out ⇒ ('in × 's') spmf)
⇒ ('s × 's' ⇒ 'a ⇒ ('b × 's × 's') spmf)" where
"attach_callee callee oracle = (λ(s, s') q. map_spmf rprodl (exec_gpv oracle (callee s q) s'))"
lemma attach_callee_simps [simp]:
"attach_callee callee oracle (s, s') q = map_spmf rprodl (exec_gpv oracle (callee s q) s')"
by(simp add: attach_callee_def)
lemma attach_CNV_RES:
"attach (converter_of_callee callee s) (resource_of_oracle res s') =
resource_of_oracle (attach_callee callee res) (s, s')"
by(coinduction arbitrary: s s')
(clarsimp simp add: spmf_rel_map rel_fun_def exec_gpv_map_gpv_id
, rule exec_gpv_parametric[where S="λl r. l = resource_of_oracle res r" and A="(=)" and CALL="(=)", THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_spmf_mono]
, auto 4 3 simp add: rel_fun_def spmf_rel_map gpv.rel_eq intro!: rel_spmf_reflI)
lemma attach_stateless_callee:
"attach_callee (stateless_callee callee) oracle = extend_state_oracle (λs q. exec_gpv oracle (callee q) s)"
by(simp add: attach_callee_def stateless_callee_def fun_eq_iff exec_gpv_map_gpv_id spmf.map_comp o_def split_def apfst_def map_prod_def)
lemma attach_id_converter [simp]: "attach id_converter res = res"
by(coinduction arbitrary: res)(auto simp add: rel_fun_def spmf_rel_map split_def map_spmf_conv_bind_spmf[symmetric] intro!: rel_spmf_reflI)
lemma attach_callee_parallel_intercept: includes lifting_syntax shows
"attach_callee (parallel_intercept callee1 callee2) (plus_oracle oracle1 oracle2) =
(rprodl ---> id ---> map_spmf (map_prod id lprodr)) (plus_oracle (lift_state_oracle extend_state_oracle (attach_callee callee1 oracle1)) (extend_state_oracle (attach_callee callee2 oracle2)))"
proof ((rule ext)+, clarify, goal_cases)
case (1 s1 s2 s q)
then show ?case by(cases q) (auto simp add: exec_gpv_plus_oracle_left exec_gpv_plus_oracle_right spmf.map_comp apfst_def o_def prod.map_comp split_def exec_gpv_map_gpv_id intro!: map_spmf_cong)
qed
lemma attach_callee_id_oracle [simp]:
"attach_callee id_oracle oracle = extend_state_oracle oracle"
by(clarsimp simp add: fun_eq_iff id_oracle_def map_spmf_conv_bind_spmf split_def)
lemma attach_parallel2: "attach (parallel_converter2 conv1 conv2) (parallel_resource res1 res2)
= parallel_resource (attach conv1 res1) (attach conv2 res2)"
apply(coinduction arbitrary: conv1 conv2 res1 res2)
apply simp
apply(rule rel_funI)
apply clarsimp
apply(simp split!: sum.split)
subgoal for conv1 conv2 res1 res2 a
apply(simp add: exec_gpv_map_gpv_id spmf_rel_map)
apply(rule rel_spmf_mono)
apply(rule
exec_gpv_parametric'[where ?S = "λres1res2 res1. res1res2 = parallel_resource res1 res2" and
A="(=)" and CALL="λl r. l = Inl r" and R="λl r. l = Inl r",
THEN rel_funD, THEN rel_funD, THEN rel_funD
])
subgoal by(auto simp add: rel_fun_def spmf_rel_map intro!: rel_spmf_reflI)
subgoal by (simp add: left_gpv_Inl_transfer)
subgoal by blast
apply clarsimp
apply(rule exI conjI refl)+
done
subgoal for conv1 conv2 res1 res2 a
apply(simp add: exec_gpv_map_gpv_id spmf_rel_map)
apply(rule rel_spmf_mono)
apply(rule
exec_gpv_parametric'[where ?S = "λres1res2 res2. res1res2 = parallel_resource res1 res2" and
A="(=)" and CALL="λl r. l = Inr r" and R="λl r. l = Inr r",
THEN rel_funD, THEN rel_funD, THEN rel_funD
])
subgoal by(auto simp add: rel_fun_def spmf_rel_map intro: rel_spmf_reflI)
subgoal by (simp add: right_gpv_Inr_transfer)
subgoal by blast
apply clarsimp
apply(rule exI conjI refl)+
done
done
subsection ‹Composing converters›
primcorec comp_converter :: "('a, 'b, 'out, 'in) converter ⇒ ('out, 'in, 'out', 'in') converter ⇒ ('a, 'b, 'out', 'in') converter" where
"run_converter (comp_converter conv1 conv2) = (λa.
map_gpv (λ((b, conv1'), conv2'). (b, comp_converter conv1' conv2')) id (inline run_converter (run_converter conv1 a) conv2))"
lemma comp_converter_parametric [transfer_rule]: includes lifting_syntax shows
"(rel_converter A B C R ===> rel_converter C R C' R' ===> rel_converter A B C' R')
comp_converter comp_converter"
unfolding comp_converter_def
supply inline_parametric'[transfer_rule] map_gpv_parametric'[transfer_rule] by transfer_prover
lemma comp_converter_map_converter1:
fixes conv' :: "('a, 'b, 'out, 'in) converter" shows
"comp_converter (map_converter f g h k conv) conv' = map_converter f g id id (comp_converter conv (map_converter h k id id conv'))"
using comp_converter_parametric[of
"conversep (BNF_Def.Grp UNIV f)" "BNF_Def.Grp UNIV g" "BNF_Def.Grp UNIV h" "conversep (BNF_Def.Grp UNIV k)"
"BNF_Def.Grp UNIV (id :: 'out ⇒ _)" "conversep (BNF_Def.Grp UNIV (id :: 'in ⇒ _))"
]
apply(unfold rel_converter_Grp)
apply(simp add: rel_fun_def Grp_iff)
apply(rewrite at "∀_ _ _. ⌑ ⟶ _" in asm conversep_iff[symmetric])
apply(unfold rel_converter_conversep[symmetric] conversep_conversep eq_alt[symmetric])
apply(rewrite in "rel_converter _ _ ⌑ _" in asm conversep_eq)
apply(rewrite in "rel_converter _ _ _ ⌑" in asm conversep_eq[symmetric])
apply(rewrite in "rel_converter _ _ ⌑ _" in asm eq_alt)
apply(rewrite in "rel_converter _ _ _ ⌑" in asm eq_alt)
apply(unfold rel_converter_Grp)
apply(simp add: Grp_iff)
done
lemma comp_converter_map_converter2:
fixes conv :: "('a, 'b, 'out, 'in) converter" shows
"comp_converter conv (map_converter f g h k conv') = map_converter id id h k (comp_converter (map_converter id id f g conv) conv')"
using comp_converter_parametric[of
"BNF_Def.Grp UNIV (id :: 'a ⇒ _)" "conversep (BNF_Def.Grp UNIV (id :: 'b ⇒ _))"
"conversep (BNF_Def.Grp UNIV f)" "BNF_Def.Grp UNIV g" "BNF_Def.Grp UNIV h" "conversep (BNF_Def.Grp UNIV k)"
]
apply(unfold rel_converter_Grp)
apply(simp add: rel_fun_def Grp_iff)
apply(rewrite at "∀_ _. ⌑ ⟶ _" in asm conversep_iff[symmetric])
apply(unfold rel_converter_conversep[symmetric] conversep_conversep rel_converter_Grp)
apply simp
apply(unfold eq_alt[symmetric])
apply(rewrite in "rel_converter _ ⌑" in asm conversep_eq)
apply(rewrite in "rel_converter ⌑ _" in asm conversep_eq[symmetric])
apply(rewrite in "rel_converter ⌑ _" in asm eq_alt)
apply(rewrite in "rel_converter _ ⌑" in asm eq_alt)
apply(unfold rel_converter_Grp)
apply(simp add: Grp_iff)
done
lemma attach_compose:
"attach (comp_converter conv1 conv2) res = attach conv1 (attach conv2 res)"
apply(coinduction arbitrary: conv1 conv2 res)
apply(auto intro!: rel_funI simp add: spmf_rel_map exec_gpv_map_gpv_id exec_gpv_inline o_def split_beta)
including lifting_syntax
apply(rule rel_spmf_mono)
apply(rule exec_gpv_parametric[where A="(=)" and CALL="(=)" and S="λ(l, r) s2. s2 = attach l r", THEN rel_funD, THEN rel_funD, THEN rel_funD])
prefer 4
apply clarsimp
by(auto simp add: case_prod_def spmf_rel_map gpv.rel_eq split_def intro!: rel_funI rel_spmf_reflI)
lemma comp_converter_assoc:
"comp_converter (comp_converter conv1 conv2) conv3 = comp_converter conv1 (comp_converter conv2 conv3)"
apply(coinduction arbitrary: conv1 conv2 conv3)
apply(rule rel_funI)
apply(clarsimp simp add: gpv.rel_map inline_map_gpv)
apply(subst inline_assoc)
apply(simp add: gpv.rel_map)
including lifting_syntax
apply(rule gpv.rel_mono_strong)
apply(rule inline_parametric[where C="(=)" and C'="(=)" and A="(=)" and S="λ(l, r) s2. s2 = comp_converter l r", THEN rel_funD, THEN rel_funD, THEN rel_funD])
prefer 4
apply clarsimp
by(auto simp add: gpv.rel_eq gpv.rel_map split_beta intro!: rel_funI gpv.rel_refl_strong)
lemma comp_converter_assoc_left:
assumes "comp_converter conv1 conv2 = conv3"
shows "comp_converter conv1 (comp_converter conv2 conv) = comp_converter conv3 conv"
by(fold comp_converter_assoc)(simp add: assms)
lemma comp_converter_attach_left:
assumes "comp_converter conv1 conv2 = conv3"
shows "attach conv1 (attach conv2 res) = attach conv3 res"
by(fold attach_compose)(simp add: assms)
lemmas comp_converter_eqs =
asm_rl[where psi="x = y" for x y :: "(_, _, _, _) converter"]
comp_converter_assoc_left
comp_converter_attach_left
lemma WT_converter_comp [WT_intro]:
"⟦ ℐ, ℐ' ⊢⇩C conv √; ℐ', ℐ'' ⊢⇩C conv' √ ⟧ ⟹ ℐ, ℐ'' ⊢⇩C comp_converter conv conv' √"
by(coinduction arbitrary: conv conv')
(auto; auto 4 4 dest: WT_converterD run_converter.results_gpv_inline intro: run_converter.WT_gpv_inline_invar[where ℐ=ℐ' and ℐ'=ℐ''])
lemma plossless_comp_converter [plossless_intro]:
assumes "plossless_converter ℐ ℐ' conv"
and "plossless_converter ℐ' ℐ'' conv'"
and "ℐ, ℐ' ⊢⇩C conv √" "ℐ', ℐ'' ⊢⇩C conv' √"
shows "plossless_converter ℐ ℐ'' (comp_converter conv conv')"
using assms
proof(coinduction arbitrary: conv conv')
case (plossless_converter a conv conv')
have conv1: "plossless_gpv ℐ' (run_converter conv a)"
using plossless_converter(1, 5) by(simp add: plossless_converterD)
have conv2: "ℐ' ⊢g run_converter conv a √"
using plossless_converter(3, 5) by(simp add: WT_converterD)
have ?plossless using plossless_converter(2,4,5)
by(auto intro: run_plossless_converter.plossless_inline[OF conv1] dest: plossless_converterD intro: conv2)
moreover have ?step (is "∀(b, conv')∈?res. ?P b conv' ∨ _")
proof(clarify)
fix b conv''
assume "(b, conv'') ∈ ?res"
then obtain conv1 conv2 where [simp]: "conv'' = comp_converter conv1 conv2"
and inline: "((b, conv1), conv2) ∈ results_gpv ℐ'' (inline run_converter (run_converter conv a) conv')"
by auto
from run_plossless_converter.results_gpv_inline[OF inline conv2] plossless_converter(2,4)
have run: "(b, conv1) ∈ results_gpv ℐ' (run_converter conv a)"
and *: "plossless_converter ℐ' ℐ'' conv2" "ℐ', ℐ'' ⊢⇩C conv2 √" by auto
with WT_converterD(2)[OF plossless_converter(3,5) run] plossless_converterD[THEN conjunct2, rule_format, OF plossless_converter(1,5) run]
show "?P b conv''" by auto
qed
ultimately show ?case ..
qed
lemma comp_converter_id_left: "comp_converter id_converter conv = conv"
by (coinduction arbitrary:conv)
(auto simp add: gpv.rel_map split_def map_gpv_conv_bind[symmetric] intro!:rel_funI gpv.rel_refl_strong)
lemma comp_converter_id_right: "comp_converter conv id_converter = conv"
proof -
have lem4: "inline run_converter gpv id_converter = inline id_oracle gpv id_converter" for gpv
by (simp only: gpv.rel_eq[symmetric])
(rule gpv.rel_mono_strong
, rule inline_parametric[where A="(=)" and C="(=)" and C'="(=)" and S="λl r. l = r ∧ r = id_converter", THEN rel_funD, THEN rel_funD, THEN rel_funD]
, auto simp add: id_oracle_def intro!: rel_funI gpv.rel_refl_strong)
show ?thesis
by (coinduction arbitrary:conv)
(auto simp add: lem4 gpv.rel_map intro!:rel_funI gpv.rel_refl_strong)
qed
lemma comp_coverter_of_callee: "comp_converter (converter_of_callee callee1 s1) (converter_of_callee callee2 s2)
= converter_of_callee (λ(s1, s2) q. map_gpv rprodl id (inline callee2 (callee1 s1 q) s2)) (s1, s2)"
apply (coinduction arbitrary: callee1 s1 callee2 s2)
apply (rule rel_funI)
apply (clarsimp simp add: gpv.rel_map inline_map_gpv)
subgoal for cal1 s1 cal2 s2 y
apply (rule gpv.rel_mono_strong)
apply (rule inline_parametric[where A="(=)" and C="(=)" and C'="(=)" and S="λc s. c = converter_of_callee cal2 s", THEN rel_funD, THEN rel_funD, THEN rel_funD])
apply(auto simp add: gpv.rel_eq rel_fun_def gpv.rel_map intro!: gpv.rel_refl_strong)
by (auto simp add: rprodl_def intro!:exI)
done
lemmas comp_converter_of_callee' = comp_converter_eqs[OF comp_coverter_of_callee]
lemma comp_converter_parallel2: "comp_converter (parallel_converter2 conv1l conv1r) (parallel_converter2 conv2l conv2r) =
parallel_converter2 (comp_converter conv1l conv2l) (comp_converter conv1r conv2r)"
apply (coinduction arbitrary: conv1l conv1r conv2l conv2r)
apply (rule rel_funI)
apply (clarsimp simp add: gpv.rel_map inline_map_gpv split!: sum.split)
subgoal for conv1l conv1r conv2l conv2r input
apply(subst left_gpv_map[where h=id])
apply(simp add: gpv.rel_map left_gpv_inline)
apply(unfold rel_gpv_conv_rel_gpv'')
apply(rule rel_gpv''_mono[THEN predicate2D, rotated -1])
apply(rule inline_parametric'[where S="λc1 c2. c1 = parallel_converter2 c2 conv2r" and C="λl r. l = Inl r" and R="λl r. l = Inl r" and C' = "(=)" and R'="(=)",
THEN rel_funD, THEN rel_funD, THEN rel_funD])
subgoal by(auto split: sum.split simp add: gpv.rel_map rel_gpv_conv_rel_gpv''[symmetric] intro!: gpv.rel_refl_strong rel_funI)
apply(rule left_gpv_Inl_transfer)
apply(auto 4 6 simp add: sum.map_id)
done
subgoal for conv1l conv1r conv2l conv2r input
apply(subst right_gpv_map[where h=id])
apply(simp add: gpv.rel_map right_gpv_inline)
apply(unfold rel_gpv_conv_rel_gpv'')
apply(rule rel_gpv''_mono[THEN predicate2D, rotated -1])
apply(rule inline_parametric'[where S="λc1 c2. c1 = parallel_converter2 conv2l c2" and C="λl r. l = Inr r" and R="λl r. l = Inr r" and C' = "(=)" and R'="(=)",
THEN rel_funD, THEN rel_funD, THEN rel_funD])
subgoal by(auto split: sum.split simp add: gpv.rel_map rel_gpv_conv_rel_gpv''[symmetric] intro!: gpv.rel_refl_strong rel_funI)
apply(rule right_gpv_Inr_transfer)
apply(auto 4 6 simp add: sum.map_id)
done
done
lemmas comp_converter_parallel2' = comp_converter_eqs[OF comp_converter_parallel2]
lemma comp_converter_map1_out:
"comp_converter (map_converter f g id id conv) conv' = map_converter f g id id (comp_converter conv conv')"
by(simp add: comp_converter_map_converter1)
lemma parallel_converter2_comp1_out:
"parallel_converter2 (comp_converter conv conv') conv'' = comp_converter (parallel_converter2 conv id_converter) (parallel_converter2 conv' conv'')"
by(simp add: comp_converter_parallel2 comp_converter_id_left)
lemma parallel_converter2_comp2_out:
"parallel_converter2 conv'' (comp_converter conv conv') = comp_converter (parallel_converter2 id_converter conv) (parallel_converter2 conv'' conv')"
by(simp add: comp_converter_parallel2 comp_converter_id_left)
subsection ‹Interaction bound›
coinductive interaction_any_bounded_converter :: "('a, 'b, 'c, 'd) converter ⇒ enat ⇒ bool" where
"interaction_any_bounded_converter conv n" if
"⋀a. interaction_any_bounded_by (run_converter conv a) n"
"⋀a b conv'. (b, conv') ∈ results'_gpv (run_converter conv a) ⟹ interaction_any_bounded_converter conv' n"
lemma interaction_any_bounded_converterD:
assumes "interaction_any_bounded_converter conv n"
shows "interaction_any_bounded_by (run_converter conv a) n ∧ (∀(b, conv')∈results'_gpv (run_converter conv a). interaction_any_bounded_converter conv' n)"
using assms
by(auto elim: interaction_any_bounded_converter.cases)
lemma interaction_any_bounded_converter_mono:
assumes "interaction_any_bounded_converter conv n"
and "n ≤ m"
shows "interaction_any_bounded_converter conv m"
using assms
by(coinduction arbitrary: conv)(auto elim: interaction_any_bounded_converter.cases intro: interaction_bounded_by_mono)
lemma interaction_any_bounded_converter_trivial [simp]: "interaction_any_bounded_converter conv ∞"
by(coinduction arbitrary: conv)
(auto simp add: interaction_bounded_by.simps)
lemmas interaction_any_bounded_converter_start =
interaction_any_bounded_converter_mono
interaction_bounded_by_mono
method interaction_bound_converter_start = (rule interaction_any_bounded_converter_start)
method interaction_bound_converter_step uses add simp =
((match conclusion in "interaction_bounded_by _ _ _" ⇒ fail ¦ "interaction_any_bounded_converter _ _" ⇒ fail ¦ _ ⇒ ‹solves ‹clarsimp simp add: simp››) | rule add interaction_bound)
method interaction_bound_converter_rec uses add simp =
(interaction_bound_converter_step add: add simp: simp; (interaction_bound_converter_rec add: add simp: simp)?)
method interaction_bound_converter uses add simp =
( 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)
endTheory 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_ℐ ℐ ∧ (∀input∈responses_ℐ ℐ 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:
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: "∀x∈set_spmf p. I1 x"
and I2: "∀y∈set_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)
endTheory Wiring
section ‹Wiring›
theory Wiring imports
Distinguisher
begin
subsection ‹Notation›
hide_const (open) Resumption.Pause Monomorphic_Monad.Pause Monomorphic_Monad.Done
no_notation Sublist.parallel (infixl "∥" 50)
no_notation plus_oracle (infix "⊕⇩O" 500)
notation Resource ("§R§")
notation Converter ("§C§")
alias RES = resource_of_oracle
alias CNV = converter_of_callee
alias id_intercept = "id_oracle"
notation id_oracle ("1⇩I")
notation plus_oracle (infixr "⊕⇩O" 504)
notation parallel_oracle (infixr "‡⇩O" 504)
notation plus_intercept (infixr "⊕⇩I" 504)
notation parallel_intercept (infixr "‡⇩I" 504)
notation parallel_resource (infixr "∥" 501)
notation parallel_converter (infixr "|⇩∝" 501)
notation parallel_converter2 (infixr "|⇩=" 501)
notation comp_converter (infixr "⊙" 502)
notation fail_converter ("⊥⇩C")
notation id_converter ("1⇩C")
notation "attach" (infixr "⊳" 500)
subsection ‹Wiring primitives›
primrec swap_sum :: "'a + 'b ⇒ 'b + 'a" where
"swap_sum (Inl x) = Inr x"
| "swap_sum (Inr y) = Inl y"
definition swap⇩C :: "('a + 'b, 'c + 'd, 'b + 'a, 'd + 'c) converter" where
"swap⇩C = map_converter swap_sum swap_sum id id 1⇩C"
definition rassocl⇩C :: "('a + ('b + 'c), 'd + ('e + 'f), ('a + 'b) + 'c, ('d + 'e) + 'f) converter" where
"rassocl⇩C = map_converter lsumr rsuml id id 1⇩C"
definition lassocr⇩C :: "(('a + 'b) + 'c, ('d + 'e) + 'f, 'a + ('b + 'c), 'd + ('e + 'f)) converter" where
"lassocr⇩C = map_converter rsuml lsumr id id 1⇩C"
definition swap_rassocl where "swap_rassocl ≡ lassocr⇩C ⊙ (1⇩C |⇩= swap⇩C) ⊙ rassocl⇩C"
definition swap_lassocr where "swap_lassocr ≡ rassocl⇩C ⊙ (swap⇩C |⇩= 1⇩C) ⊙ lassocr⇩C"
definition parallel_wiring :: "(('a + 'b) + ('e + 'f), ('c + 'd) + ('g + 'h), ('a + 'e) + ('b + 'f), ('c + 'g) + ('d + 'h)) converter" where
"parallel_wiring = lassocr⇩C ⊙ (1⇩C |⇩= swap_lassocr) ⊙ rassocl⇩C"
lemma WT_lassocr⇩C [WT_intro]: "(ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3, ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3) ⊢⇩C lassocr⇩C √"
by(coinduction)(auto simp add: lassocr⇩C_def)
lemma WT_rassocl⇩C [WT_intro]: "ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3), (ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3 ⊢⇩C rassocl⇩C √"
by(coinduction)(auto simp add: rassocl⇩C_def)
lemma WT_swap⇩C [WT_intro]: "ℐ1 ⊕⇩ℐ ℐ2, ℐ2 ⊕⇩ℐ ℐ1 ⊢⇩C swap⇩C √"
by(coinduction)(auto simp add: swap⇩C_def)
lemma WT_swap_lassocr [WT_intro]: "ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3), ℐ2 ⊕⇩ℐ (ℐ1 ⊕⇩ℐ ℐ3) ⊢⇩C swap_lassocr √"
unfolding swap_lassocr_def
by(rule WT_converter_comp WT_lassocr⇩C WT_rassocl⇩C WT_converter_parallel_converter2 WT_converter_id WT_swap⇩C)+
lemma WT_swap_rassocl [WT_intro]: "(ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3, (ℐ1 ⊕⇩ℐ ℐ3) ⊕⇩ℐ ℐ2 ⊢⇩C swap_rassocl √"
unfolding swap_rassocl_def
by(rule WT_converter_comp WT_lassocr⇩C WT_rassocl⇩C WT_converter_parallel_converter2 WT_converter_id WT_swap⇩C)+
lemma WT_parallel_wiring [WT_intro]:
"(ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ (ℐ3 ⊕⇩ℐ ℐ4), (ℐ1 ⊕⇩ℐ ℐ3) ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ4) ⊢⇩C parallel_wiring √"
unfolding parallel_wiring_def
by(rule WT_converter_comp WT_lassocr⇩C WT_rassocl⇩C WT_converter_parallel_converter2 WT_converter_id WT_swap_lassocr)+
lemma map_swap_sum_plus_oracle: includes lifting_syntax shows
"(id ---> swap_sum ---> map_spmf (map_prod swap_sum id)) (oracle1 ⊕⇩O oracle2) =
(oracle2 ⊕⇩O oracle1)"
proof ((rule ext)+; goal_cases)
case (1 s q)
then show ?case by (cases q) (simp_all add: spmf.map_comp o_def apfst_def prod.map_comp id_def)
qed
lemma map_ℐ_rsuml_lsumr [simp]: "map_ℐ rsuml lsumr (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) = ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3)"
proof(rule ℐ_eqI[OF Set.set_eqI], goal_cases)
case (1 x)
then show ?case by(cases x rule: rsuml.cases) auto
qed (auto simp add: image_image)
lemma map_ℐ_lsumr_rsuml [simp]: "map_ℐ lsumr rsuml ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3) = (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3))"
proof(rule ℐ_eqI[OF Set.set_eqI], goal_cases)
case (1 x)
then show ?case by(cases x rule: lsumr.cases) auto
qed (auto simp add: image_image)
lemma map_ℐ_swap_sum [simp]: "map_ℐ swap_sum swap_sum (ℐ1 ⊕⇩ℐ ℐ2) = ℐ2 ⊕⇩ℐ ℐ1"
proof(rule ℐ_eqI[OF Set.set_eqI], goal_cases)
case (1 x)
then show ?case by(cases x) auto
qed (auto simp add: image_image)
definition parallel_resource1_wiring :: "('a + ('b + 'c), 'd + ('e + 'f), 'b + ('a + 'c), 'e + ('d + 'f)) converter" where
"parallel_resource1_wiring = swap_lassocr"
lemma WT_parallel_resource1_wiring [WT_intro]: "ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3), ℐ2 ⊕⇩ℐ (ℐ1 ⊕⇩ℐ ℐ3) ⊢⇩C parallel_resource1_wiring √"
unfolding parallel_resource1_wiring_def by(rule WT_swap_lassocr)
lemma plossless_rassocl⇩C [plossless_intro]: "plossless_converter (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3) rassocl⇩C"
by coinduction (auto simp add: rassocl⇩C_def)
lemma plossless_lassocr⇩C [plossless_intro]: "plossless_converter ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ ℐ3) (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) lassocr⇩C"
by coinduction (auto simp add: lassocr⇩C_def)
lemma plossless_swap⇩C [plossless_intro]: "plossless_converter (ℐ1 ⊕⇩ℐ ℐ2) (ℐ2 ⊕⇩ℐ ℐ1) swap⇩C"
by coinduction (auto simp add: swap⇩C_def)
lemma plossless_swap_lassocr [plossless_intro]:
"plossless_converter (ℐ1 ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ3)) (ℐ2 ⊕⇩ℐ (ℐ1 ⊕⇩ℐ ℐ3)) swap_lassocr"
unfolding swap_lassocr_def by(rule plossless_intro WT_intro)+
lemma rsuml_lsumr_parallel_converter2:
"map_converter id id rsuml lsumr ((conv1 |⇩= conv2) |⇩= conv3) =
map_converter rsuml lsumr id id (conv1 |⇩= conv2 |⇩= conv3)"
by(coinduction arbitrary: conv1 conv2 conv3, clarsimp split!: sum.split simp add: rel_fun_def map_gpv_conv_map_gpv'[symmetric])
((subst left_gpv_map[where h=id] | subst right_gpv_map[where h=id])+
, simp add:gpv.map_comp sum.map_id0 o_def prod.map_comp id_def[symmetric]
, subst map_gpv'_map_gpv_swap, (subst rsuml_lsumr_left_gpv_left_gpv | subst rsuml_lsumr_left_gpv_right_gpv | subst rsuml_lsumr_right_gpv)
, auto 4 4 intro!: gpv.rel_refl_strong simp add: gpv.rel_map)+
lemma comp_lassocr⇩C: "((conv1 |⇩= conv2) |⇩= conv3) ⊙ lassocr⇩C = lassocr⇩C ⊙ (conv1 |⇩= conv2 |⇩= conv3)"
unfolding lassocr⇩C_def
by(subst comp_converter_map_converter2)
(simp add: comp_converter_id_right comp_converter_map1_out comp_converter_id_left rsuml_lsumr_parallel_converter2)
lemmas comp_lassocr⇩C' = comp_converter_eqs[OF comp_lassocr⇩C]
lemma lsumr_rsuml_parallel_converter2:
"map_converter id id lsumr rsuml (conv1 |⇩= (conv2 |⇩= conv3)) =
map_converter lsumr rsuml id id ((conv1 |⇩= conv2) |⇩= conv3)"
by(coinduction arbitrary: conv1 conv2 conv3, clarsimp split!: sum.split simp add: rel_fun_def map_gpv_conv_map_gpv'[symmetric])
((subst left_gpv_map[where h=id] | subst right_gpv_map[where h=id])+
, simp add:gpv.map_comp sum.map_id0 o_def prod.map_comp id_def[symmetric]
, subst map_gpv'_map_gpv_swap, (subst lsumr_rsuml_left_gpv | subst lsumr_rsuml_right_gpv_left_gpv | subst lsumr_rsuml_right_gpv_right_gpv)
, auto 4 4 intro!: gpv.rel_refl_strong simp add: gpv.rel_map)+
lemma comp_rassocl⇩C:
"(conv1 |⇩= conv2 |⇩= conv3) ⊙ rassocl⇩C = rassocl⇩C ⊙ ((conv1 |⇩= conv2) |⇩= conv3)"
unfolding rassocl⇩C_def
by(subst comp_converter_map_converter2)
(simp add: comp_converter_id_right comp_converter_map1_out comp_converter_id_left lsumr_rsuml_parallel_converter2)
lemmas comp_rassocl⇩C' = comp_converter_eqs[OF comp_rassocl⇩C]
lemma swap_sum_right_gpv:
"map_gpv' id swap_sum swap_sum (right_gpv gpv) = left_gpv gpv"
by(coinduction arbitrary: gpv)
(auto 4 3 simp add: spmf_rel_map generat.rel_map intro!: rel_spmf_reflI rel_generat_reflI rel_funI split: sum.split intro: exI[where x=Fail])
lemma swap_sum_left_gpv:
"map_gpv' id swap_sum swap_sum (left_gpv gpv) = right_gpv gpv"
by(coinduction arbitrary: gpv)
(auto 4 3 simp add: spmf_rel_map generat.rel_map intro!: rel_spmf_reflI rel_generat_reflI rel_funI split: sum.split intro: exI[where x=Fail])
lemma swap_sum_parallel_converter2:
"map_converter id id swap_sum swap_sum (conv1 |⇩= conv2) =
map_converter swap_sum swap_sum id id (conv2 |⇩= conv1)"
by(coinduction arbitrary: conv1 conv2, clarsimp simp add: rel_fun_def map_gpv_conv_map_gpv'[symmetric] split!: sum.split)
(subst map_gpv'_map_gpv_swap, (subst swap_sum_right_gpv | subst swap_sum_left_gpv),
auto 4 4 intro!: gpv.rel_refl_strong simp add: gpv.rel_map)+
lemma comp_swap⇩C: "(conv1 |⇩= conv2) ⊙ swap⇩C = swap⇩C ⊙ (conv2 |⇩= conv1)"
unfolding swap⇩C_def
by(subst comp_converter_map_converter2)
(simp add: comp_converter_id_right comp_converter_map1_out comp_converter_id_left swap_sum_parallel_converter2)
lemmas comp_swap⇩C' = comp_converter_eqs[OF comp_swap⇩C]
lemma comp_swap_lassocr: "(conv1 |⇩= conv2 |⇩= conv3) ⊙ swap_lassocr = swap_lassocr ⊙ (conv2 |⇩= conv1 |⇩= conv3)"
unfolding swap_lassocr_def comp_rassocl⇩C' comp_converter_assoc comp_converter_parallel2' comp_swap⇩C' comp_converter_id_right
by(subst (9) comp_converter_id_left[symmetric], subst comp_converter_parallel2[symmetric])
(simp add: comp_converter_assoc comp_lassocr⇩C)
lemmas comp_swap_lassocr' = comp_converter_eqs[OF comp_swap_lassocr]
lemma comp_parallel_wiring:
"((C1 |⇩= C2) |⇩= (C3 |⇩= C4)) ⊙ parallel_wiring = parallel_wiring ⊙ ((C1 |⇩= C3) |⇩= (C2 |⇩= C4))"
unfolding parallel_wiring_def comp_lassocr⇩C' comp_converter_assoc comp_converter_parallel2' comp_swap_lassocr'
by(subst comp_converter_id_right[THEN trans, OF comp_converter_id_left[symmetric]], subst comp_converter_parallel2[symmetric])
(simp add: comp_converter_assoc comp_rassocl⇩C)
lemmas comp_parallel_wiring' = comp_converter_eqs[OF comp_parallel_wiring]
lemma attach_converter_of_resource_conv_parallel_resource:
"converter_of_resource res |⇩∝ 1⇩C ⊳ res' = res ∥ res'"
by(coinduction arbitrary: res res')
(auto 4 3 simp add: rel_fun_def map_lift_spmf spmf.map_comp o_def prod.map_comp spmf_rel_map bind_map_spmf map_spmf_conv_bind_spmf[symmetric] split_def split!: sum.split intro!: rel_spmf_reflI)
lemma attach_converter_of_resource_conv_parallel_resource2:
" 1⇩C |⇩∝ converter_of_resource res ⊳ res' = res' ∥ res"
by(coinduction arbitrary: res res')
(auto 4 3 simp add: rel_fun_def map_lift_spmf spmf.map_comp o_def prod.map_comp spmf_rel_map bind_map_spmf map_spmf_conv_bind_spmf[symmetric] split_def split!: sum.split intro!: rel_spmf_reflI)
lemma plossless_parallel_wiring [plossless_intro]:
"plossless_converter ((ℐ1 ⊕⇩ℐ ℐ2) ⊕⇩ℐ (ℐ3 ⊕⇩ℐ ℐ4)) ((ℐ1 ⊕⇩ℐ ℐ3) ⊕⇩ℐ (ℐ2 ⊕⇩ℐ ℐ4)) parallel_wiring"
unfolding parallel_wiring_def by(rule plossless_intro WT_intro)+
lemma run_converter_lassocr [simp]:
"run_converter lassocr⇩C x = Pause (rsuml x) (λx. Done (lsumr x, lassocr⇩C))"
by(simp add: lassocr⇩C_def o_def)
lemma run_converter_rassocl [simp]:
"run_converter rassocl⇩C x = Pause (lsumr x) (λx. Done (rsuml x, rassocl⇩C))"
by(simp add: rassocl⇩C_def o_def)
lemma run_converter_swap [simp]: "run_converter swap⇩C x = Pause (swap_sum x) (λx. Done (swap_sum x, swap⇩C))"
by(simp add: swap⇩C_def o_def)
definition lassocr_swap_sum where "lassocr_swap_sum = rsuml ∘ map_sum swap_sum id ∘ lsumr"
lemma run_converter_swap_lassocr [simp]:
"run_converter swap_lassocr x = Pause (lassocr_swap_sum x) (
case lsumr x of Inl _ ⇒ (λy. case lsumr y of Inl _ ⇒ Done (lassocr_swap_sum y, swap_lassocr) | _ ⇒ Fail)
| Inr _ ⇒ (λy. case lsumr y of Inl _ ⇒ Fail | Inr _ ⇒ Done (lassocr_swap_sum y, swap_lassocr)))"
by(subst sum.case_distrib[where h="λx. inline _ x _"] |
simp add: bind_rpv_def inline_map_gpv split_def map_gpv_conv_bind[symmetric] swap_lassocr_def o_def cong del: sum.case_cong)+
(cases x rule: lsumr.cases, simp_all add: o_def lassocr_swap_sum_def gpv.map_comp fun_eq_iff cong: sum.case_cong split: sum.split)
definition parallel_sum_wiring where "parallel_sum_wiring = lsumr ∘ map_sum id lassocr_swap_sum ∘ rsuml"
lemma run_converter_parallel_wiring:
"run_converter parallel_wiring x = Pause (parallel_sum_wiring x) (
case rsuml x of Inl _ ⇒ (λy. case rsuml y of Inl _ ⇒ Done (parallel_sum_wiring y, parallel_wiring) | _ ⇒ Fail)
| Inr x ⇒ (case lsumr x of Inl _ ⇒ (λy. case rsuml y of Inl _ ⇒ Fail | Inr x ⇒ (case lsumr x of Inl _ ⇒ Done (parallel_sum_wiring y, parallel_wiring) | Inr _ ⇒ Fail))
| Inr _ ⇒ (λy. case rsuml y of Inl _ ⇒ Fail | Inr x ⇒ (case lsumr x of Inl _ ⇒ Fail | Inr _ ⇒ Done (parallel_sum_wiring y, parallel_wiring)))))"
by(simp add: parallel_wiring_def o_def cong del: sum.case_cong add: split_def map_gpv_conv_bind[symmetric])
(subst sum.case_distrib[where h="λx. right_rpv x _"] |
subst sum.case_distrib[where h="λx. inline _ x _"] |
subst sum.case_distrib[where h=right_gpv] |
(auto simp add: inline_map_gpv bind_rpv_def gpv.map_comp fun_eq_iff parallel_sum_wiring_def
parallel_wiring_def[symmetric] sum.case_distrib o_def intro: sym cong del: sum.case_cong split!: sum.split))+
lemma bound_lassocr⇩C