section ‹Bisimulation between BPEL and PiCore›
theory bpel_bisimulation
imports bpel_semantics bpel_translator
begin
subsection ‹Definition of correctness by simulation relation›
notation estran_p ("_ ⊢ _ ─es[_]→ _" [81,81] 80)
notation pestran_p ("_ ⊢ _ ─pes[_]→ _" [70,70] 60)
definition estran_nx where
‹estran_nx Γ ≡ {((P,s),(Q,t)). ∃x y. ((P,s,x),(Q,t,y))∈estran Γ}›
definition estran'
("_ ⊢ _ ─es→ _" [81,0,81] 80)
where "estran' Γ S1 S2 ≡ ((S1,S2)∈ estran_nx Γ)"
definition estrans0
("_ ⊢ _ ─es*→ _" [81,0,81] 80)
where "Γ ⊢ S1 ─es*→ S2 ≡ ((S1,S2)∈ (estran_nx Γ)⇧*)"
definition estrans1
("_ ⊢ _ ─es+→ _" [81,0,81] 80)
where "Γ ⊢ S1 ─es+→ S2 ≡ ((S1,S2)∈ (estran_nx Γ)⇧+)"
lemma fin_has_no_tran:
assumes tr: "Γ ⊢ (S,s) ─es→ (R,t)"
shows "S ≠ fin"
proof -
from tr have "∃x y a. Γ ⊢ (S,s,x) ─es[a]→ (R,t,y)"
by(simp add:estran'_def estran_def estran_nx_def)
then obtain x y a where "Γ ⊢ (S,s,x) ─es[a]→ (R,t,y)" by auto
thus ?thesis
apply(induct S) apply auto
apply(rule estran_p.cases) apply auto
apply(rule ctran.cases) apply auto
apply(rule ctran.cases) by auto
qed
definition bpel_le :: "('s,'l) BPELProc ⇒ ('s,'l) BPELProc ⇒ bool"
where "bpel_le P Q ≡ (∃s t. ((P,s), (Q,t)) ∈ activity_tran⇧*)"
text ‹
we can construct a strong bisimulation between BPEL process and its translated Event System.
This means the power of PiCore, which can simulate the BPEL process step by step, in a fine-grained way.
›
coinductive bpel_bisim_es_strong ::
"'Env ⇒ (('s,'l) BPELProc × ('s,'l) State) ⇒
((('s,'l) EventLabel, 'k, ('s,'l) State, (('s,'l) State com) option) esys × ('s,'l) State) ⇒ bool"
("_ ⊢ _ ≃ _" [80,0,80] 81)
for Γ :: 'Env
where
"∀P' t. (P,s) ⟶⇩b⇩p⇩e⇩l (P',t) ⟶ (∃Q'. Γ ⊢ (Q,s) ─es→ (Q',t) ∧ (Γ ⊢ (P',t) ≃ (Q',t)) ) ⟹
∀Q' t. Γ ⊢ (Q,s) ─es→ (Q',t) ⟶ (∃P'. (P,s) ⟶⇩b⇩p⇩e⇩l (P',t) ∧ (Γ ⊢ (P',t) ≃ (Q',t)) ) ⟹
Q = compile P ⟹
Γ ⊢ (P,s) ≃ (Q,s)"
thm bpel_bisim_es_strong.intros
thm bpel_bisim_es_strong.simps
thm bpel_bisim_es_strong.cases
thm bpel_bisim_es_strong.coinduct
inductive_cases bpel_bisim_es_strong_cases: "Γ ⊢ (P, s) ≃ (Q, s)"
thm bpel_bisim_es_strong_cases
lemma bisim_bpel_step: "Γ ⊢ (P, s) ≃ (P', s) ⟹
∀Q t. ((P, s) ⟶⇩b⇩p⇩e⇩l (Q, t)) ⟶ (∃Q'. (Γ ⊢ (P', s) ─es→ (Q', t)) ∧ (Γ ⊢ (Q, t) ≃ (Q', t)) ∧ Q' = compile Q)"
using bpel_bisim_es_strong_cases by metis
lemma bisim_es_step: "Γ ⊢ (P,s) ≃ (P',s) ⟹
∀Q' t. Γ ⊢ (P',s) ─es→ (Q',t) ⟶ (∃Q. (P,s) ⟶⇩b⇩p⇩e⇩l (Q,t) ∧ (Γ ⊢ (Q,t) ≃ (Q',t)) ∧ Q' = compile Q)"
using bpel_bisim_es_strong_cases by metis
lemma bisim_compile: "Γ ⊢ (P,s) ≃ (P',s) ⟹ P' = compile P"
using bpel_bisim_es_strong_cases .
lemma termi_bisim_fin: "Γ ⊢ (ActTerminator,s) ≃ (fin,s)"
apply(rule bpel_bisim_es_strong.intros)
using termi_has_no_tran apply fast
using fin_has_no_tran apply fast
by simp
coinductive bpel_bisim_es_strong_eh ::
"'Env ⇒ (('s,'l) EventHandler × ('s,'l) State) ⇒
((('s,'l) EventLabel, 'k, ('s,'l) State, (('s,'l) State com) option) esys × ('s,'l) State) ⇒ bool"
("_ ⊢ _ ≃⇩e⇩h _" [80,0,80] 81)
for Γ :: 'Env
where
"∀P' t. (P,s) ⟶⇩e⇩h (P',t) ⟶ (∃Q'. Γ ⊢ (Q,s) ─es→ (Q',t) ∧ (Γ ⊢ (P',t) ≃ (Q',t)) ) ⟹
∀Q' t. Γ ⊢ (Q,s) ─es→ (Q',t) ⟶ (∃P'. (P,s) ⟶⇩e⇩h (P',t) ∧ (Γ ⊢ (P',t) ≃ (Q',t)) ) ⟹
Q = compile_eh P ⟹
Γ ⊢ (P,s) ≃⇩e⇩h (Q,s)"
inductive_cases bpel_bisim_es_strong_eh_cases: "Γ ⊢ (P, s) ≃⇩e⇩h (Q, s)"
thm bpel_bisim_es_strong_eh_cases
lemma bisim_eh_bpel_step: "Γ ⊢ (P,s) ≃⇩e⇩h (Q,s) ⟹
∀P' t. (P,s) ⟶⇩e⇩h (P',t) ⟶ (∃Q'. Γ ⊢ (Q,s) ─es→ (Q',t) ∧ (Γ ⊢ (P',t) ≃ (Q',t)) )"
using bpel_bisim_es_strong_eh_cases by metis
lemma bisim_eh_es_step: "Γ ⊢ (P,s) ≃⇩e⇩h (Q,s) ⟹
∀Q' t. Γ ⊢ (Q,s) ─es→ (Q',t) ⟶ (∃P'. (P,s) ⟶⇩e⇩h (P',t) ∧ (Γ ⊢ (P',t) ≃ (Q',t)) )"
using bpel_bisim_es_strong_eh_cases by metis
lemma bisim_eh_compile: "Γ ⊢ (P,s) ≃⇩e⇩h (Q,s) ⟹ Q = compile_eh P"
using bpel_bisim_es_strong_eh_cases .
definition bpel_bisim_es'_strong ::
"'Env ⇒ ('s,'l) BPELProc ⇒
(('s,'l) EventLabel, 'k, ('s,'l) State, (('s,'l) State com) option) esys ⇒ bool"
("_ ⊢ _ ≈ _" [80,0,80] 81)
where "Γ ⊢ bpel ≈ esys ≡ (∀s. Γ ⊢ (bpel,s) ≃ (esys,s))"
subsection‹strong bisimulation on state traces›
type_synonym ('l,'k,'s,'prog) esconf_nx = "('l,'k,'s,'prog) esys × 's"
fun trace_strong_bisim ::
"('s,'l) bpelconf list ⇒ (('s,'l) EventLabel, 'k, ('s,'l) State, (('s,'l) State com) option) esconf_nx list ⇒ bool"
where "trace_strong_bisim [] [] = True" |
"trace_strong_bisim (a#as) (b#bs) = ((fst b = compile (fst a)) ∧ snd b = snd a ∧ trace_strong_bisim as bs)" |
"trace_strong_bisim _ _ = False"
lemma trace_strong_bisim_tl : "trace_strong_bisim (a#as) (b#bs) ⟹ trace_strong_bisim as bs"
by simp
lemma tr_sim_len: "trace_strong_bisim st1 st2 ⟹ length st1 = length st2"
apply(induct st1 arbitrary:st2)
subgoal for st2 apply(induct st2,auto) done
subgoal for a st1 st2 apply(induct st2,auto) done
done
inductive_set comps :: ‹(('p×'s) × ('p×'s)) set ⇒ ('p×'s) list set›
for tran :: "(('p×'s) × ('p×'s)) set" where
CompsOne[intro]: "[(P,s)] ∈ comps tran" |
CompsComp: "⟦ ((P,s),(Q,t)) ∈ tran; (Q,t)#cs ∈ comps tran ⟧ ⟹ (P,s)#(Q,t)#cs ∈ comps tran"
inductive_cases comps_cases: "(P,s)#(Q,t)#cs ∈ comps tran"
thm comps_cases
lemma comps_not_empty: "[] ∉ comps tran"
using comps.simps by fastforce
lemma comps_tail: "a#as ∈ comps tran ⟹ as ≠ [] ⟹ as ∈ comps tran"
using comps.cases by blast
definition "comps_of trs st ≡ {c. c∈comps trs ∧ hd c = st}"
lemma comps_of_nempty: "[]∉comps_of trs st"
apply(simp add:comps_of_def) using comps_not_empty by blast
definition bpel_bisim_es_strong_tr::
"'Env ⇒ (('s,'l) BPELProc × ('s,'l) State) ⇒
((('s,'l) EventLabel, 'k, ('s,'l) State, (('s,'l) State com) option) esys × ('s,'l) State) ⇒ bool"
where "bpel_bisim_es_strong_tr Γ bpel es ≡
(∀t∈comps_of activity_tran bpel. ∃t'∈comps_of (estran_nx Γ) es. trace_strong_bisim t t')
∧ (∀t'∈comps_of (estran_nx Γ) es. ∃t∈comps_of activity_tran bpel. trace_strong_bisim t t')"
lemma strong_imp_strong_tr:
"Γ ⊢ (bpel,s) ≃ (es,s) ⟹ bpel_bisim_es_strong_tr Γ (bpel,s) (es,s)"
apply(simp add:bpel_bisim_es_strong_tr_def comps_of_def) apply auto
subgoal for t
apply(induct t arbitrary: bpel es s)
using comps.cases apply blast
subgoal for a t bpel es s proof -
assume cond_tail: "⋀bpel (es::(('b, 'c) EventLabel, 'd, ('b, 'c) State, ('b, 'c) State com option) esys) s.
bpel_bisim_es_strong Γ (bpel, s) (es, s) ⟹
t ∈ comps activity_tran ⟹
hd t = (bpel, s) ⟹
∃x. x ∈ comps (estran_nx Γ) ∧ hd x = (es, s) ∧ trace_strong_bisim t x"
assume sim: "bpel_bisim_es_strong Γ (bpel, s) (es, s)"
assume at_comp: "a # t ∈ comps activity_tran"
assume at: "hd (a # t) = (bpel, s)"
from at have a: "a = (bpel,s)" by auto
show ?thesis
proof(cases t)
case Nil assume t_nil: "t = []"
moreover have "trace_strong_bisim (a # t) ([(es,s)])"
using a t_nil sim bpel_bisim_es_strong_cases
by fastforce
ultimately show ?thesis using a by force
next
case (Cons b list) assume t_list: "t = b # list"
obtain bpel' and s' where b: "b = (bpel',s')" by fastforce
with t_list at_comp have a2b: "a ⟶⇩b⇩p⇩e⇩l b" using comps_cases
by (metis old.prod.exhaust)
with sim a b obtain es' where es': "es' = compile bpel' ∧ Γ ⊢ (es,s) ─es→ (es',s')
∧ (bpel_bisim_es_strong Γ (bpel',s') (es',s'))"
using bpel_bisim_es_strong_cases by metis
from at_comp t_list have t_comp: "t ∈ comps activity_tran"
using comps_tail by blast
thm cond_tail[OF es'[THEN conjunct2, THEN conjunct2]]
from t_comp cond_tail sim t_list b es' obtain x
where x: "x ∈ comps (estran_nx Γ) ∧ hd x = (es', s') ∧ trace_strong_bisim t x"
by (meson list.sel(1))
then obtain x' where x': "x = (es',s')#x'"
by (metis comps_not_empty list.exhaust list.sel(1))
let ?x = "(es,s)#x"
from sim have "es = compile bpel" using bpel_bisim_es_strong_cases by fast
with x a have "trace_strong_bisim (a # t) ((es, s) # x)"
using trace_strong_bisim.simps(2) by fastforce
moreover
from x es' x' have "?x ∈ comps (estran_nx Γ)"
using estran'_def CompsComp by fast
ultimately show ?thesis by fastforce
qed
qed done
subgoal for t
apply(induct t arbitrary: bpel es s)
using comps.cases apply blast
subgoal for a t bpel es s
proof -
assume cond_tail: "⋀bpel es s.
bpel_bisim_es_strong Γ (bpel, s) (es, s) ⟹
t ∈ comps (estran_nx Γ) ⟹ hd t = (es, s) ⟹
∃x. x ∈ comps activity_tran ∧ hd x = (bpel, s) ∧ trace_strong_bisim x t"
assume sim: "bpel_bisim_es_strong Γ (bpel, s) (es, s)"
assume at_comp: "a # t ∈ comps (estran_nx Γ)"
assume at: "hd (a # t) = (es, s)"
from at have a: "a = (es,s)" by auto
show ?thesis
proof(cases t)
case Nil assume t_nil: "t = []"
moreover have "trace_strong_bisim ([(bpel,s)]) (a # t) "
using a t_nil sim bpel_bisim_es_strong_cases
by fastforce
ultimately show ?thesis using a by force
next
case (Cons b list) assume t_list: "t = b # list"
obtain es' and s' where b: "b = (es',s')" by fastforce
with t_list at_comp a have a2b: "Γ ⊢ a ─es→ b" using estran'_def comps_cases by metis
with sim a b obtain bpel' where es': "es' = compile bpel' ∧ (bpel,s) ⟶⇩b⇩p⇩e⇩l (bpel',s')
∧ (bpel_bisim_es_strong Γ (bpel',s') (es',s'))"
using bpel_bisim_es_strong_cases by metis
from at_comp t_list have t_comp: "t ∈ comps (estran_nx Γ)"
using comps_tail by blast
from t_comp cond_tail sim t_list b es' obtain x
where x: "x ∈ comps activity_tran ∧ hd x = (bpel', s') ∧ trace_strong_bisim x t"
by (meson list.sel(1))
then obtain x' where x': "x = (bpel',s')#x'"
by (metis comps_not_empty list.exhaust list.sel(1))
let ?x = "(bpel,s)#x"
from sim have "es = compile bpel" using bpel_bisim_es_strong_cases by fast
with x a have "trace_strong_bisim ((bpel, s) # x) (a # t)"
using trace_strong_bisim.simps(2) by fastforce
moreover
from x es' x' have "?x ∈ comps activity_tran"
using estran'_def CompsComp by fast
ultimately show ?thesis by fastforce
qed
qed
done
done
lemma bisim_strong_tr_imp_strong:
"bpel_bisim_es_strong_tr Γ (bpel,s) (es,s) ⟹ Γ ⊢ (bpel,s) ≃ (es,s)"
apply(simp add:bpel_bisim_es_strong_tr_def) apply auto
apply(coinduction arbitrary:bpel es s) apply auto
subgoal for bpel es s bpel' s'
proof -
assume btran_etran: "∀t. t ∈ comps_of activity_tran (bpel, s)
⟶ (∃x∈comps_of (estran_nx Γ) (es, s). trace_strong_bisim t x)"
assume etran_btran: "∀t'. t' ∈ comps_of (estran_nx Γ) (es, s)
⟶ (∃t∈comps_of activity_tran (bpel, s). trace_strong_bisim t t')"
assume bstep: "(bpel, s) ⟶⇩b⇩p⇩e⇩l (bpel', s')"
from bstep have step_comp: "(bpel, s)#[(bpel', s')] ∈ comps_of activity_tran (bpel, s)"
apply(simp add:comps_of_def) using comps.CompsComp[of bpel s bpel' s' activity_tran "[]"] by blast
have "[(bpel, s)] ∈ comps_of activity_tran (bpel, s)"
apply(simp add:comps_of_def) using comps.CompsOne by fast
with btran_etran[rule_format,of "[(bpel, s)]"]
have es_bpel: "es = compile bpel" apply(simp add:comps_of_def)
by (metis fst_conv list.sel(1) neq_Nil_conv trace_strong_bisim.simps(2) trace_strong_bisim.simps(3))
let ?es' = "compile bpel'"
from step_comp btran_etran[rule_format,of "(bpel, s)#[(bpel', s')]"] obtain x
where x: "x∈comps_of (estran_nx Γ) (es, s) ∧ trace_strong_bisim ((bpel, s)#[(bpel', s')]) x" by fast
with es_bpel have x1: "x = (es,s)#[(compile bpel',s')]" using trace_strong_bisim.simps
by (smt fst_conv list.exhaust snd_conv surjective_pairing)
with x have es_tran: "Γ ⊢ (es, s) ─es→ (?es', s')" apply(simp add:comps_of_def estran'_def)
using comps.cases by blast
moreover
{
fix ta
assume ta: "ta ∈ comps_of activity_tran (bpel', s')"
then have "((bpel, s)#ta) ∈ comps_of activity_tran (bpel, s)"
apply(simp add:comps_of_def) by (metis bstep comps.CompsComp comps.CompsOne list.collapse)
with btran_etran obtain x1 where x1: "x1∈comps_of (estran_nx Γ) (es, s) ∧ trace_strong_bisim ((bpel, s)#ta) x1"
by blast
then obtain x2 where x2: "x2 = tl x1" by auto
have "x2∈comps_of (estran_nx Γ) (?es', s')"
proof(cases x2)
case Nil
then show ?thesis using x1 x2 ta comps_of_nempty
by (metis list.exhaust list.sel(3) trace_strong_bisim.simps(2) trace_strong_bisim.simps(3))
next
case (Cons a list)
then show ?thesis using x1 x2 ta es_tran apply(simp add:comps_of_def)
apply(rule conjI) using comps_tail apply (metis hd_Cons_tl list.distinct(1) local.Cons tl_Nil)
apply auto using trace_strong_bisim.simps(2)[of "(bpel, s)" ta "hd x1" "tl x1"]
by (metis comps_not_empty fst_conv list.exhaust_sel prod.exhaust_sel snd_conv trace_strong_bisim.simps(2))
qed
moreover
have "trace_strong_bisim ta x2"
using x1 x2 ta trace_strong_bisim.simps(2)[of "(bpel, s)" ta "hd x1" "tl x1"]
by (metis hd_Cons_tl trace_strong_bisim.simps(3))
ultimately have "∃x::((('b, 'c) EventLabel, 'd, ('b, 'c) State, ('b, 'c) State com option) esys × ('b, 'c) State) list∈comps_of (estran_nx Γ) (?es', s'). trace_strong_bisim ta x" by blast
}
moreover
{
fix t'
assume t': "(t'::((('b, 'c) EventLabel, 'd, ('b, 'c) State, ('b, 'c) State com option) esys × ('b, 'c) State) list) ∈ comps_of (estran_nx Γ) (?es', s')"
then have "(es,s)#t' ∈ comps_of (estran_nx Γ) (es,s)"
apply(simp add:comps_of_def)
by (metis t' comps.CompsComp comps_of_nempty es_tran estran'_def list.sel(1) neq_Nil_conv)
with etran_btran obtain x1 where x1: "x1∈comps_of activity_tran (bpel, s) ∧ trace_strong_bisim x1 ((es, s) # t')"
by blast
then obtain x2 where x2: "x2 = tl x1" by auto
have "x2 ∈ comps_of activity_tran (bpel', s')"
proof(cases x2)
case Nil
then show ?thesis using x1 x2 t' comps_of_nempty
by (smt list.exhaust list.sel(3) trace_strong_bisim.simps(4) trace_strong_bisim_tl)
next
case (Cons a list)
assume x2': "x2 = a # list"
with x1 x2 have x2_comp: "x2 ∈ comps activity_tran"
by (metis (no_types, lifting) Nil_tl comps_of_def comps_tail list.collapse list.discI mem_Collect_eq)
moreover have "hd x2 = (bpel', s')"
proof -
from t' obtain t'' where "t' = (compile bpel', s')#t''"
apply(simp add:comps_of_def) apply(rule comps.cases) apply blast by simp+
then show ?thesis using x1 x2 x2' compile_inj trace_strong_bisim.elims(2)
by (smt eq_fst_iff eq_snd_iff list.distinct(1) list.exhaust_sel list.inject)
qed
ultimately show ?thesis
using comps_of_def by blast
qed
moreover
from x1 x2 have "trace_strong_bisim x2 t'"
by (metis Nil_notin_lex lexord_Nil_left lexord_lex list.sel(3) neq_Nil_conv
tr_sim_len trace_strong_bisim.simps(1) trace_strong_bisim.simps(2))
ultimately have "∃t∈comps_of activity_tran (bpel', s'). trace_strong_bisim t t'" by blast
}
ultimately
show "∃Q'. Γ ⊢ (es, s) ─es→ (Q', s') ∧
((∀ta. ta ∈ comps_of activity_tran (bpel', s') ⟶ (∃x∈comps_of (estran_nx Γ) (Q', s'). trace_strong_bisim ta x)) ∧
(∀t'. t' ∈ comps_of (estran_nx Γ) (Q', s') ⟶ (∃t∈comps_of activity_tran (bpel', s'). trace_strong_bisim t t')) ∨
bpel_bisim_es_strong Γ (bpel', s') (Q', s'))" by blast
qed
subgoal for bpel es s es' t
proof -
assume btran_etran: "∀t. t ∈ comps_of activity_tran (bpel, s) ⟶ (∃x∈comps_of (estran_nx Γ) (es, s). trace_strong_bisim t x)"
assume etran_btran: "∀t'. t' ∈ comps_of (estran_nx Γ) (es, s) ⟶ (∃t∈comps_of activity_tran (bpel, s). trace_strong_bisim t t')"
assume estep: "Γ ⊢ (es, s) ─es→ (es', t)"
have "[(es,s)]∈comps_of (estran_nx Γ) (es, s)" apply(simp add:comps_of_def) by fast
with etran_btran[rule_format, of "[(es, s)]"] have es_bpel: "compile bpel = es"
apply(simp add:comps_of_def) apply clarsimp subgoal for t apply(subgoal_tac "t=[(bpel,s)]") apply simp
by (metis (no_types, hide_lams) list.sel(1) neq_Nil_conv trace_strong_bisim.simps(3)
trace_strong_bisim.simps(4) trace_strong_bisim_tl) done
from estep have "(es,s)#[(es',t)]∈comps_of (estran_nx Γ) (es, s)"
apply(simp add:comps_of_def estran'_def) using comps.CompsComp[of es s es' t "(estran_nx Γ)" "[]"] by fast
with etran_btran obtain tr where tr: "tr∈comps_of activity_tran (bpel, s) ∧ trace_strong_bisim tr ((es,s)#[(es',t)])"
by blast
obtain bpel' where tr1: "tr = (bpel,s)#[(bpel',t)] ∧ compile bpel' = es'"
proof-
assume a: ‹⋀bpel'. tr = [(bpel, s), (bpel', t)] ∧ compile bpel' = es' ⟹ thesis›
from comps_of_nempty tr[THEN conjunct1] have ‹tr≠[]› by blast
show thesis
apply(rule a)
apply(rule conjI)
apply(insert tr[THEN conjunct2])
apply(subst(asm) hd_Cons_tl[OF ‹tr≠[]›, symmetric])
apply clarsimp
apply(subgoal_tac ‹tl tr≠[]›)
apply(subst(asm) hd_Cons_tl[of ‹tl tr›, symmetric])
apply assumption
apply (simp only: trace_strong_bisim.simps) using es_bpel
apply clarsimp apply(drule compile_inj)
apply(subgoal_tac ‹tl (tl tr) = []›)
apply(subgoal_tac ‹tr = [(fst (hd tr), snd (hd tr)), (fst (hd (tl tr)), snd (hd (tl tr)))]›)
apply fast
using ‹tr ≠ []› list.collapse apply fastforce
apply(rule ccontr)
subgoal
proof-
assume a1: ‹trace_strong_bisim (tl (tl tr)) []›
assume a2: ‹tl (tl tr) ≠ []›
from a1 hd_Cons_tl[OF a2] show False
by (metis trace_strong_bisim.simps(3))
qed
apply fastforce
by (metis (no_types, lifting) fst_conv hd_Cons_tl trace_strong_bisim.simps(2) trace_strong_bisim.simps(4))
qed
from tr tr1 have bstep: "(bpel, s) ⟶⇩b⇩p⇩e⇩l (bpel', t)" apply(simp add:comps_of_def)
using comps.cases by blast
moreover
{
fix ta
assume ta: "ta ∈ comps_of activity_tran (bpel', t)"
with bstep have "(bpel,s)#ta ∈ comps_of activity_tran (bpel,s)"
apply(simp add:comps_of_def) by (metis comps.CompsComp comps_of_nempty hd_Cons_tl ta)
with btran_etran obtain x1 where x1: "x1∈comps_of (estran_nx Γ) (es, s) ∧ trace_strong_bisim ((bpel, s)#ta) x1"
by blast
then obtain x2 where x2: "x2 = tl x1" by auto
have "x2∈comps_of (estran_nx Γ) (es', t)"
proof(cases x2)
case Nil
then show ?thesis using x1 x2 ta comps_of_nempty
by (metis list.exhaust list.sel(3) trace_strong_bisim.simps(2) trace_strong_bisim.simps(3))
next
case (Cons a list)
then show ?thesis using x1 x2 ta bstep apply(simp add:comps_of_def)
apply(rule conjI) using comps_tail apply (metis hd_Cons_tl list.distinct(1) local.Cons tl_Nil)
apply auto using trace_strong_bisim.simps(2)[of "(bpel, s)" ta "hd x1" "tl x1"]
proof -
assume a1: "x2 = a # list"
assume a2: "hd ta = (bpel', t)"
assume a3: "tl x1 = a # list"
assume a4: "trace_strong_bisim ((bpel, s) # ta) x1"
then have f5: "[] = x1 ∨ trace_strong_bisim ta x2"
using a3 a1 by (metis (no_types) list.exhaust_sel trace_strong_bisim.simps(2))
have f6: "∀ps. (ps::(('b, 'c) Activity × (_, _) State) list) = [] ∨ ¬ trace_strong_bisim ps []"
using trace_strong_bisim.elims(2) by blast
have "[] ≠ ta"
using f5 a4 a1 by force
then show "a = (es', t)"
using f6 f5 a4 a2 a1 by (metis (no_types) fst_conv list.distinct(1) list.exhaust_sel snd_conv surjective_pairing tr1 trace_strong_bisim.simps(2))
qed
qed
moreover
have "trace_strong_bisim ta x2"
using x1 x2 ta trace_strong_bisim.simps(2)[of "(bpel, s)" ta "hd x1" "tl x1"]
by (metis hd_Cons_tl trace_strong_bisim.simps(3))
ultimately have "∃x∈comps_of (estran_nx Γ) (es', t). trace_strong_bisim ta x" by blast
}
moreover
{
fix t'
assume t': "t' ∈ comps_of (estran_nx Γ) (es', t)"
then have "(es,s)#t' ∈ comps_of (estran_nx Γ) (es,s)"
apply(simp add:comps_of_def)
by (metis t' comps.CompsComp comps_of_nempty estep estran'_def list.sel(1) neq_Nil_conv)
with etran_btran obtain x1 where x1: "x1∈comps_of activity_tran (bpel, s) ∧ trace_strong_bisim x1 ((es, s) # t')"
by blast
then obtain x2 where x2: "x2 = tl x1" by auto
have "x2 ∈ comps_of activity_tran (bpel', t)"
proof(cases x2)
case Nil
then show ?thesis using x1 x2 t' comps_of_nempty
by (smt list.exhaust list.sel(3) trace_strong_bisim.simps(4) trace_strong_bisim_tl)
next
case (Cons a list)
assume x2': "x2 = a # list"
with x1 x2 have x2_comp: "x2 ∈ comps activity_tran"
by (metis (no_types, lifting) Nil_tl comps_of_def comps_tail list.collapse list.discI mem_Collect_eq)
moreover have "hd x2 = (bpel', t)" using t' x1 x2 x2' compile_inj
by (smt comps_of_def fst_conv list.distinct(1) list.exhaust_sel list.inject
mem_Collect_eq prod.collapse snd_conv tr1 trace_strong_bisim.elims(2))
ultimately show ?thesis
using comps_of_def by blast
qed
moreover
from x1 x2 have "trace_strong_bisim x2 t'"
by (metis Nil_notin_lex lexord_Nil_left lexord_lex list.sel(3) neq_Nil_conv
tr_sim_len trace_strong_bisim.simps(1) trace_strong_bisim.simps(2))
ultimately have "∃t∈comps_of activity_tran (bpel', t). trace_strong_bisim t t'" by blast
}
ultimately show ?thesis by blast
qed
subgoal for bpel es s
proof -
assume p1: "∀t. t ∈ comps_of activity_tran (bpel, s) ⟶ (∃x∈comps_of (estran_nx Γ) (es, s). trace_strong_bisim t x)"
assume "∀t'. t' ∈ comps_of (estran_nx Γ) (es, s) ⟶ (∃t∈comps_of activity_tran (bpel, s). trace_strong_bisim t t')"
have "[(bpel, s)]∈comps_of activity_tran (bpel, s)" apply(simp add:comps_of_def) using CompsOne by blast
with p1 obtain x where x: "x∈comps_of (estran_nx Γ) (es, s) ∧ trace_strong_bisim [(bpel, s)] x" by blast
hence "x=[(es,s)]" apply(simp add:comps_of_def)
by (metis (no_types, hide_lams) list.exhaust list.sel(1) trace_strong_bisim.simps(3)
trace_strong_bisim.simps(4) trace_strong_bisim_tl x)
with x show "es = compile bpel" by simp
qed
done
theorem bisim_strong_tr_eq_strong:
"bpel_bisim_es_strong_tr Γ (bpel,s) (es,s) = Γ ⊢ (bpel,s) ≃ (es,s)"
using bisim_strong_tr_imp_strong strong_imp_strong_tr by fast
subsection‹strong simulation of by coinduction and on state traces›
text‹
bpel is simulated by the translated picore.
It means that if the translated picore is safe, then bpel is safe
the equivalence of the two strong simulation does not depend on the bijection of the compile funciton.
›
coinductive bpel_sim_es_strong1 ::
"'Env ⇒ (('s,'l) BPELProc × ('s,'l) State) ⇒
((('s,'l) EventLabel, 'k, ('s,'l) State, (('s,'l) State com) option) esys × ('s,'l) State) ⇒ bool"
for Γ :: 'Env
where
"∀P' t. (P,s) ⟶⇩b⇩p⇩e⇩l (P',t) ⟶ (∃Q'. Γ ⊢ (Q,s) ─es→ (Q',t) ∧ (bpel_sim_es_strong1 Γ (P',t) (Q',t)) ) ⟹
Q = compile P ⟹
bpel_sim_es_strong1 Γ (P,s) (Q,s)"
inductive_cases bpel_sim_es_strong1_cases: "bpel_sim_es_strong1 Γ (P,s) (Q,s)"
thm bpel_sim_es_strong1_cases
definition bpel_sim_es_strong_tr::
"'Env ⇒ (('s,'l) BPELProc × ('s,'l) State) ⇒
((('s,'l) EventLabel, 'k, ('s,'l) State, (('s,'l) State com) option) esys × ('s,'l) State) ⇒ bool"
where "bpel_sim_es_strong_tr Γ bpel es ≡
(∀t∈comps_of activity_tran bpel. ∃t'∈comps_of (estran_nx Γ) es. trace_strong_bisim t t')"
lemma sim_strong1_imp_strong_tr:
"bpel_sim_es_strong1 Γ (bpel,s) (es,s) ⟹ bpel_sim_es_strong_tr Γ (bpel,s) (es,s)"
apply(simp add:bpel_sim_es_strong_tr_def comps_of_def) apply auto
subgoal for t
apply(induct t arbitrary: bpel es s)
using comps.cases apply blast
subgoal for a t bpel es s proof -
assume cond_tail: "⋀bpel (es::(('b, 'c) EventLabel, 'd, ('b, 'c) State, ('b, 'c) State com option) esys) s.
bpel_sim_es_strong1 Γ (bpel, s) (es, s) ⟹
t ∈ comps activity_tran ⟹
hd t = (bpel, s) ⟹
∃x. x ∈ comps (estran_nx Γ) ∧ hd x = (es, s) ∧ trace_strong_bisim t x"
assume sim: "bpel_sim_es_strong1 Γ (bpel, s) (es, s)"
assume at_comp: "a # t ∈ comps activity_tran"
assume at: "hd (a # t) = (bpel, s)"
from at have a: "a = (bpel,s)" by auto
show ?thesis
proof(cases t)
case Nil assume t_nil: "t = []"
moreover have "trace_strong_bisim (a # t) ([(es,s)])"
using a t_nil sim bpel_sim_es_strong1_cases
by fastforce
ultimately show ?thesis using a by force
next
case (Cons b list) assume t_list: "t = b # list"
obtain bpel' and s' where b: "b = (bpel',s')" by fastforce
with t_list at_comp have a2b: "a ⟶⇩b⇩p⇩e⇩l b" using comps_cases
by (metis old.prod.exhaust)
with sim a b obtain es' where es': "es' = compile bpel' ∧ Γ ⊢ (es,s) ─es→ (es',s')
∧ (bpel_sim_es_strong1 Γ (bpel',s') (es',s'))"
using bpel_sim_es_strong1_cases by metis
from at_comp t_list have t_comp: "t ∈ comps activity_tran"
using comps_tail by blast
from t_comp cond_tail sim t_list b es' obtain x
where x: "x ∈ comps (estran_nx Γ) ∧ hd x = (es', s') ∧ trace_strong_bisim t x"
by (meson list.sel(1))
then obtain x' where x': "x = (es',s')#x'"
by (metis comps_not_empty list.exhaust list.sel(1))
let ?x = "(es,s)#x"
from sim have "es = compile bpel" using bpel_sim_es_strong1_cases by fast
with x a have "trace_strong_bisim (a # t) ((es, s) # x)"
using trace_strong_bisim.simps(2) by fastforce
moreover
from x es' x' have "?x ∈ comps (estran_nx Γ)"
using estran'_def CompsComp by fast
ultimately show ?thesis by fastforce
qed
qed done
done
lemma sim_strong_tr_imp_strong1:
"bpel_sim_es_strong_tr Γ (bpel,s) (es,s) ⟹ bpel_sim_es_strong1 Γ (bpel,s) (es,s)"
apply(simp add:bpel_sim_es_strong_tr_def)
apply(coinduction arbitrary:bpel es s) apply auto
subgoal for bpel es s bpel' s'
proof -
assume btran_etran: "∀t. t ∈ comps_of activity_tran (bpel, s)
⟶ (∃x∈comps_of (estran_nx Γ) (es, s). trace_strong_bisim t x)"
assume bstep: "(bpel, s) ⟶⇩b⇩p⇩e⇩l (bpel', s')"
from bstep have step_comp: "(bpel, s)#[(bpel', s')] ∈ comps_of activity_tran (bpel, s)"
apply(simp add:comps_of_def) using comps.CompsComp[of bpel s bpel' s' activity_tran "[]"] by blast
have "[(bpel, s)] ∈ comps_of activity_tran (bpel, s)"
apply(simp add:comps_of_def) using comps.CompsOne by fast
with btran_etran[rule_format,of "[(bpel, s)]"]
have es_bpel: "es = compile bpel" apply(simp add:comps_of_def)
by (metis fst_conv list.sel(1) neq_Nil_conv trace_strong_bisim.simps(2) trace_strong_bisim.simps(3))
let ?es' = "compile bpel'"
from step_comp btran_etran[rule_format,of "(bpel, s)#[(bpel', s')]"] obtain x
where x: "x∈comps_of (estran_nx Γ) (es, s) ∧ trace_strong_bisim ((bpel, s)#[(bpel', s')]) x" by fast
with es_bpel have x1: "x = (es,s)#[(compile bpel',s')]" using trace_strong_bisim.simps
by (smt fst_conv list.exhaust snd_conv surjective_pairing)
with x have es_tran: "Γ ⊢ (es, s) ─es→ (?es', s')" apply(simp add:comps_of_def estran'_def)
using comps.cases by blast
moreover
{
fix ta
assume ta: "ta ∈ comps_of activity_tran (bpel', s')"
then have "((bpel, s)#ta) ∈ comps_of activity_tran (bpel, s)"
apply(simp add:comps_of_def) by (metis bstep comps.CompsComp comps.CompsOne list.collapse)
with btran_etran obtain x1 where x1: "x1∈comps_of (estran_nx Γ) (es, s) ∧ trace_strong_bisim ((bpel, s)#ta) x1"
by blast
then obtain x2 where x2: "x2 = tl x1" by auto
have "x2∈comps_of (estran_nx Γ) (?es', s')"
proof(cases x2)
case Nil
then show ?thesis using x1 x2 ta comps_of_nempty
by (metis list.exhaust list.sel(3) trace_strong_bisim.simps(2) trace_strong_bisim.simps(3))
next
case (Cons a list)
then show ?thesis using x1 x2 ta es_tran apply(simp add:comps_of_def)
apply(rule conjI) using comps_tail apply (metis hd_Cons_tl list.distinct(1) local.Cons tl_Nil)
apply auto using trace_strong_bisim.simps(2)[of "(bpel, s)" ta "hd x1" "tl x1"]
proof -
assume a1: "x2 = a # list"
assume a2: "hd ta = (bpel', s')"
assume a3: "tl x1 = a # list"
assume a4: "trace_strong_bisim ((bpel, s) # ta) x1"
then have f5: "[] = x1 ∨ trace_strong_bisim ta x2"
using a3 a1 by (metis list.exhaust_sel trace_strong_bisim.simps(2))
have "[] ≠ x1"
using a4 trace_strong_bisim.elims(2) by blast
then have "[] ≠ ta ∧ trace_strong_bisim ta x2"
using f5 a1 by force
then show "a = (compile bpel', s')"
using a2 a1 by (metis (no_types) fst_conv list.exhaust_sel prod.exhaust_sel
snd_conv trace_strong_bisim.simps(2))
qed
qed
moreover
have "trace_strong_bisim ta x2"
using x1 x2 ta trace_strong_bisim.simps(2)[of "(bpel, s)" ta "hd x1" "tl x1"]
by (metis hd_Cons_tl trace_strong_bisim.simps(3))
ultimately have "∃x::((('b, 'c) EventLabel, 'd, ('b, 'c) State, ('b, 'c) State com option) esys × ('b, 'c) State) list∈comps_of (estran_nx Γ) (?es', s'). trace_strong_bisim ta x" by blast
}
ultimately
show ?thesis by blast
qed
subgoal for bpel es s
proof -
assume p1: "∀t. t ∈ comps_of activity_tran (bpel, s) ⟶ (∃x∈comps_of (estran_nx Γ) (es, s). trace_strong_bisim t x)"
have "[(bpel, s)]∈comps_of activity_tran (bpel, s)" apply(simp add:comps_of_def) using CompsOne by blast
with p1 obtain x where x: "x∈comps_of (estran_nx Γ) (es, s) ∧ trace_strong_bisim [(bpel, s)] x" by blast
hence "x=[(es,s)]" apply(simp add:comps_of_def)
by (metis (no_types, hide_lams) list.exhaust list.sel(1) trace_strong_bisim.simps(3)
trace_strong_bisim.simps(4) trace_strong_bisim_tl x)
with x show "es = compile bpel" by simp
qed
done
lemma sim_strong_tr_eq_strong1:
"bpel_sim_es_strong_tr Γ (bpel,s) (es,s) = bpel_sim_es_strong1 Γ (bpel,s) (es,s)"
using sim_strong1_imp_strong_tr sim_strong_tr_imp_strong1 by fast
subsection ‹another definition of strong bisimulation›
coinductive bpel_bisim_es_strong' ::
"'Env ⇒ (('s,'l) BPELProc × ('s,'l) State) ⇒
((('s,'l) EventLabel, 'k, ('s,'l) State, (('s,'l) State com) option) esys × ('s,'l) State) ⇒ bool"
("_ ⊢ _ ≃⇩∀ _" [80,0,80] 81)
for Γ :: 'Env
where
"∀P' t. (P,s) ⟶⇩b⇩p⇩e⇩l (P',t) ⟶ (∃Q'. Γ ⊢ (Q,s) ─es→ (Q',t) ∧ (∀s. Γ ⊢ (P',s) ≃⇩∀ (Q',s)) ) ⟹
∀Q' t. Γ ⊢ (Q,s) ─es→ (Q',t) ⟶ (∃P'. (P,s) ⟶⇩b⇩p⇩e⇩l (P',t) ∧ (∀s. Γ ⊢ (P',s) ≃⇩∀ (Q',s)) ) ⟹
Q = compile P ⟹
Γ ⊢ (P,s) ≃⇩∀ (Q,s)"
inductive_cases bpel_bisim_es_strong'_cases: "Γ ⊢ (P,s) ≃⇩∀ (Q,s)"
thm bpel_bisim_es_strong'_cases
lemma strong'_imp_strong:
"Γ ⊢ (P,s) ≃⇩∀ (Q,s) ⟹ Γ ⊢ (P,s) ≃ (Q,s)"
apply(coinduction arbitrary: P Q s)
subgoal for P Q s
apply(rule exI[where x="P"])
apply(rule exI[where x="s"])
apply(rule exI[where x="Q"])
apply auto
apply(subgoal_tac "∃Q'. Γ ⊢ (Q, s) ─es→ (Q', t) ∧ Γ ⊢ (P',t) ≃⇩∀ (Q',t)")
prefer 2 using bpel_bisim_es_strong'_cases apply metis
apply blast
apply(subgoal_tac "∃P'. (P, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ Γ ⊢ (P',t) ≃⇩∀ (Q',t)")
prefer 2 using bpel_bisim_es_strong'_cases
apply metis apply blast
using bpel_bisim_es_strong'_cases
apply metis done
done
end