Theory Converter_Rewrite
theory Converter_Rewrite imports
Converter
begin
section ‹Equivalence of converters restricted by interfaces›
coinductive eq_resource_on :: "'a set ⇒ ('a, 'b) resource ⇒ ('a, 'b) resource ⇒ bool" (‹_ ⊢⇩R/ _ ∼/ _› [100, 99, 99] 99)
for A where
eq_resource_onI: "A ⊢⇩R res ∼ res'" if
"⋀a. a ∈ A ⟹ rel_spmf (rel_prod (=) (eq_resource_on A)) (run_resource res a) (run_resource res' a)"
lemma eq_resource_on_coinduct [consumes 1, case_names eq_resource_on, coinduct pred: eq_resource_on]:
assumes "X res res'"
and "⋀res res' a. ⟦ X res res'; a ∈ A ⟧
⟹ rel_spmf (rel_prod (=) (λres res'. X res res' ∨ A ⊢⇩R res ∼ res')) (run_resource res a) (run_resource res' a)"
shows "A ⊢⇩R res ∼ res'"
using assms(1) by(rule eq_resource_on.coinduct)(auto dest: assms(2))
lemma eq_resource_onD:
assumes "A ⊢⇩R res ∼ res'" "a ∈ A"
shows "rel_spmf (rel_prod (=) (eq_resource_on A)) (run_resource res a) (run_resource res' a)"
using assms by(auto elim: eq_resource_on.cases)
lemma eq_resource_on_refl [simp]: "A ⊢⇩R res ∼ res"
by(coinduction arbitrary: res)(auto intro: rel_spmf_reflI)
lemma eq_resource_on_reflI: "res = res' ⟹ A ⊢⇩R res ∼ res'"
by(simp add: eq_resource_on_refl)
lemma eq_resource_on_sym: "A ⊢⇩R res ∼ res'" if "A ⊢⇩R res' ∼ res"
using that
by(coinduction arbitrary: res res')
(drule (1) eq_resource_onD, rewrite in "⌑" conversep_iff[symmetric]
, auto simp add: spmf_rel_conversep[symmetric] elim!: rel_spmf_mono)
lemma eq_resource_on_trans [trans]: "A ⊢⇩R res ∼ res''" if "A ⊢⇩R res ∼ res'" "A ⊢⇩R res' ∼ res''"
using that by(coinduction arbitrary: res res' res'')
((drule (1) eq_resource_onD)+, drule (1) rel_spmf_OO_trans, auto elim!:rel_spmf_mono)
lemma eq_resource_on_UNIV_D [simp]: "res = res'" if "UNIV ⊢⇩R res ∼ res'"
using that by(coinduction arbitrary: res res')(auto dest: eq_resource_onD)
lemma eq_resource_on_UNIV_iff: "UNIV ⊢⇩R res ∼ res' ⟷ res = res'"
by(auto dest: eq_resource_on_UNIV_D)
lemma eq_resource_on_mono: "⟦ A' ⊢⇩R res ∼ res'; A ⊆ A' ⟧ ⟹ A ⊢⇩R res ∼ res'"
by(coinduction arbitrary: res res')(auto dest: eq_resource_onD elim!: rel_spmf_mono)
lemma eq_resource_on_empty [simp]: "{} ⊢⇩R res ∼ res'"
by(rule eq_resource_onI; simp)
lemma eq_resource_on_resource_of_oracleI:
includes lifting_syntax
fixes S
assumes sim: "(S ===> eq_on A ===> rel_spmf (rel_prod (=) S)) r1 r2"
and S: "S s1 s2"
shows "A ⊢⇩R resource_of_oracle r1 s1 ∼ resource_of_oracle r2 s2"
using S by(coinduction arbitrary: s1 s2)
(drule sim[THEN rel_funD, THEN rel_funD], simp add: eq_on_def
, fastforce simp add: eq_on_def spmf_rel_map elim: rel_spmf_mono)
lemma exec_gpv_eq_resource_on:
assumes "outs_ℐ ℐ ⊢⇩R res ∼ res'"
and "ℐ ⊢g gpv √"
and "ℐ ⊢res res √"
shows "rel_spmf (rel_prod (=) (eq_resource_on (outs_ℐ ℐ))) (exec_gpv run_resource gpv res) (exec_gpv run_resource gpv res')"
using assms
proof(induction arbitrary: res res' gpv rule: exec_gpv_fixp_induct)
case (step exec_gpv')
have[simp]: "⟦(s, r1) ∈ set_spmf (run_resource res g1); (s, r2) ∈ set_spmf (run_resource res' g1);
IO g1 g2 ∈ set_spmf (the_gpv gpv); outs_ℐ ℐ ⊢⇩R r1 ∼ r2⟧ ⟹ rel_spmf (rel_prod (=) (eq_resource_on (outs_ℐ ℐ)))
(exec_gpv' (g2 s) r1) (exec_gpv' (g2 s) r2)" for g1 g2 r1 s r2
by(rule step.IH, simp, rule WT_gpv_ContD[OF step.prems(2)], assumption)
(auto elim: outs_gpv.IO WT_calleeD[OF run_resource.WT_callee, OF step.prems(3)]
dest!: WT_resourceD[OF step.prems(3), rotated 1] intro: WT_gpv_outs_gpv[THEN subsetD, OF step.prems(2)])
show ?case
by(clarsimp intro!: rel_spmf_bind_reflI step.prems split!: generat.split)
(rule rel_spmf_bindI', rule eq_resource_onD[OF step.prems(1)]
, auto elim: outs_gpv.IO intro: eq_resource_onD[OF step.prems(1)] WT_gpv_outs_gpv[THEN subsetD, OF step.prems(2)])
qed simp_all
inductive eq_ℐ_generat :: "('a ⇒ 'b ⇒ bool) ⇒ ('out, 'in) ℐ ⇒ ('c ⇒ 'd ⇒ bool) ⇒ ('a, 'out, 'in ⇒ 'c) generat ⇒ ('b, 'out, 'in ⇒ 'd) generat ⇒ bool"
for A ℐ D where
Pure: "eq_ℐ_generat A ℐ D (Pure x) (Pure y)" if "A x y"
| IO: "eq_ℐ_generat A ℐ D (IO out c) (IO out c')" if "out ∈ outs_ℐ ℐ" "⋀input. input ∈ responses_ℐ ℐ out ⟹ D (c input) (c' input)"
hide_fact (open) Pure IO
inductive_simps eq_ℐ_generat_simps [simp, code]:
"eq_ℐ_generat A ℐ D (Pure x) (Pure y)"
"eq_ℐ_generat A ℐ D (IO out c) (Pure y)"
"eq_ℐ_generat A ℐ D (Pure x) (IO out' c')"
"eq_ℐ_generat A ℐ D (IO out c) (IO out' c')"
inductive_simps eq_ℐ_generat_iff1:
"eq_ℐ_generat A ℐ D (Pure x) g'"
"eq_ℐ_generat A ℐ D (IO out c) g'"
inductive_simps eq_ℐ_generat_iff2:
"eq_ℐ_generat A ℐ D g (Pure x)"
"eq_ℐ_generat A ℐ D g (IO out c)"
lemma eq_ℐ_generat_mono':
"⟦ eq_ℐ_generat A ℐ D x y; ⋀x y. A x y ⟹ A' x y; ⋀x y. D x y ⟹ D' x y; ℐ ≤ ℐ' ⟧
⟹ eq_ℐ_generat A' ℐ' D' x y"
by(auto 4 4 elim!: eq_ℐ_generat.cases simp add: le_ℐ_def)
lemma eq_ℐ_generat_mono: "eq_ℐ_generat A ℐ D ≤ eq_ℐ_generat A' ℐ' D'" if "A ≤ A'" "D ≤ D'" "ℐ ≤ ℐ'"
using that by(auto elim!: eq_ℐ_generat_mono' dest: predicate2D)
lemma eq_ℐ_generat_mono'' [mono]:
"⟦ ⋀x y. A x y ⟶ A' x y; ⋀x y. D x y ⟶ D' x y ⟧
⟹ eq_ℐ_generat A ℐ D x y ⟶ eq_ℐ_generat A' ℐ D' x y"
by(auto elim: eq_ℐ_generat_mono')
lemma eq_ℐ_generat_conversep: "eq_ℐ_generat A¯¯ ℐ D¯¯ = (eq_ℐ_generat A ℐ D)¯¯"
by(fastforce elim: eq_ℐ_generat.cases)
lemma eq_ℐ_generat_reflI:
assumes "⋀x. x ∈ generat_pures generat ⟹ A x x"
and "⋀out c. generat = IO out c ⟹ out ∈ outs_ℐ ℐ ∧ (∀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