Theory bpel_bisimulation

theory bpel_bisimulation
imports bpel_semantics bpel_translator
(*
Created by Yongwang Zhao (zhaoyw@buaa.edu.cn)
School of Computer Science & Engineering, Beihang University, China
*)

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) ⟶bpel (P',t) ⟶ (∃Q'. Γ ⊢ (Q,s) ─es→ (Q',t) ∧ (Γ ⊢ (P',t) ≃ (Q',t)) ) ⟹
     ∀Q' t. Γ ⊢ (Q,s) ─es→ (Q',t) ⟶ (∃P'. (P,s) ⟶bpel (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) ⟶bpel (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) ⟶bpel (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"
  ("_ ⊢ _ ≃eh _" [80,0,80] 81)
  for Γ :: 'Env
  where
    "∀P' t. (P,s) ⟶eh (P',t) ⟶ (∃Q'. Γ ⊢ (Q,s) ─es→ (Q',t) ∧ (Γ ⊢ (P',t) ≃ (Q',t)) ) ⟹
     ∀Q' t. Γ ⊢ (Q,s) ─es→ (Q',t) ⟶ (∃P'. (P,s) ⟶eh (P',t) ∧ (Γ ⊢ (P',t) ≃ (Q',t)) ) ⟹
     Q = compile_eh P ⟹
     Γ ⊢ (P,s) ≃eh (Q,s)"

inductive_cases bpel_bisim_es_strong_eh_cases: "Γ ⊢ (P, s) ≃eh (Q, s)"
thm bpel_bisim_es_strong_eh_cases

lemma bisim_eh_bpel_step: "Γ ⊢ (P,s) ≃eh (Q,s) ⟹
  ∀P' t. (P,s) ⟶eh (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) ≃eh (Q,s) ⟹
∀Q' t. Γ ⊢ (Q,s) ─es→ (Q',t) ⟶ (∃P'. (P,s) ⟶eh (P',t) ∧ (Γ ⊢ (P',t) ≃ (Q',t)) )"
  using bpel_bisim_es_strong_eh_cases by metis

lemma bisim_eh_compile: "Γ ⊢ (P,s) ≃eh (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 ⟶bpel 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) ⟶bpel (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) ⟶bpel (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
         (* by (smt comps_of_def fst_conv hd_Cons_tl list.distinct(1) list.inject
                mem_Collect_eq prod.collapse snd_conv)*)
        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
    (*with es_bpel*) 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 (* shameful that it could not be proved automatically *)
    from tr tr1 have bstep: "(bpel, s) ⟶bpel (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) ⟶bpel (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 ⟶bpel 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) ⟶bpel (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) ⟶bpel (P',t) ⟶ (∃Q'. Γ ⊢ (Q,s) ─es→ (Q',t) ∧ (∀s. Γ ⊢ (P',s) ≃ (Q',s)) ) ⟹
     ∀Q' t. Γ ⊢ (Q,s) ─es→ (Q',t) ⟶ (∃P'. (P,s) ⟶bpel (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) ⟶bpel (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