Theory bpel_translator_correct

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

section ‹Correctness of Translating from BPEL to PiCore›

theory bpel_translator_correct
  imports bpel_bisimulation
begin

subsection ‹lemmas of IMP language and its rely-guarantee proof system ›

lemma ctrans_step_rev: "(P,s)-c*→(Q,t) ⟹ P ≠ Q ⟹ ∃P' s'. (P,s)-c→(P',s') ∧ (P',s')-c*→(Q,t)"
  by (meson converse_rtranclE2 prod.inject)

lemma ctrans_step: "(P,s)-c→(P',s') ⟹ (P',s')-c*→(Q,t) ⟹ (P,s)-c*→(Q,t)"
  using converse_rtrancl_into_rtrancl by simp

lemma no_ctran_from_none: ‹¬ (None, s) -c→ c›
  apply(unfold not_def) apply(rule impI) apply(erule ctran.cases, auto) done

lemma ctrans_from_skip_cases:
  ‹(Some SKIP, s) -c*→ (None, t) ⟹ (s = t ⟹ P) ⟹ P›
  apply(erule converse_rtranclE)
   apply blast
  apply(erule ctran.cases, auto simp add: Skip_def)
  apply(erule converse_rtranclE)
   apply simp
  using no_ctran_from_none by metis

lemma ctrans_from_basic_cases_aux:
  ‹(Some (Basic f), s) -c*→ (None, t) ⟹ t = f s›
  apply(erule converse_rtranclE)
   apply blast
  apply(erule ctran.cases, auto)
  apply(erule converse_rtranclE)
   apply blast
  using no_ctran_from_none by fast

lemma ctrans_from_basic_cases:
  ‹(Some (Basic f), s) -c*→ (None, t) ⟹ (t = f s ⟹ P) ⟹ P›
  using ctrans_from_basic_cases_aux by metis

lemma ctrans_from_basic_seq_basic_cases_aux:
  ‹(Some (Basic f1;; Basic f2), s) -c*→ (None, t) ⟹ t = f2 (f1 s)›
  apply(erule converse_rtranclE)
   apply blast
  apply(erule ctran.cases, auto)
   apply(erule ctran.cases; simp)
   apply(erule converse_rtranclE)
    apply blast
   apply(erule ctran.cases; simp)
   apply(erule converse_rtranclE)
    apply blast
  using no_ctran_from_none apply fast
  apply(erule ctran.cases, auto)
  done

lemma ctrans_from_basic_seq_basic_cases:
  ‹(Some (Basic f1;; Basic f2), s) -c*→ (None, t) ⟹ (t = f2 (f1 s) ⟹ P) ⟹ P›
  using ctrans_from_basic_seq_basic_cases_aux by metis

inductive_cases basic_tran: "(Some(Basic f), s) -c→ (P, t)"
thm basic_tran

inductive_cases seq_tran1: "(Some(Seq P0 P1), s) -c→ (Some(Seq P2 P1), t)"
thm seq_tran1

inductive_cases seq_tran2: "(Some(Seq P0 P1), s) -c→ (Some P1, t)"
thm seq_tran2

thm estran_from_basic_cases

subsection ‹compile preserved by step›

subsection‹correct translation of Flow›

lemma EJoin_cases2: "Γ ⊢ (EJoin es1 es2, s, x) ─es[a]→ (Q, t, y) ⟹
  (∃es1'. (Γ ⊢ (es1,s,x) ─es[a]→ (es1',t,y)) ∧ Q = EJoin es1' es2)
∨ (∃es2'. (Γ ⊢ (es2,s,x) ─es[a]→ (es2',t,y)) ∧ Q = EJoin es1 es2')
∨ es1 = fin ∧ es2 = fin ∧ Q = fin ∧ s = t ∧ Act a = Cmd"
  apply(rule estran_p.cases) by auto

lemma flow_cor1:
  assumes bp1: "⋀bp' s t. Γ ⊢ (compile bp1, s) ─es→ (bp'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys, t) ⟹
                            ∃P'. (bp1, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ bp' = compile P'"
  assumes bp2: "⋀bp' s t. Γ ⊢ (compile bp2, s) ─es→ (bp'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys, t) ⟹
                            ∃P'. (bp2, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ bp' = compile P'"
  assumes estep: "Γ ⊢ (compile (Flow bp1 bp2), s) ─es→ (bp'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys, t)"
  shows "∃P'. (Flow bp1 bp2, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ bp' = compile P'"
proof-
  term bp'
  from estep obtain x y a where a: "Γ ⊢ (compile bp1 ⋈ compile bp2, s, x) ─es[a]→ (bp', t, y)"
    apply(simp add:estran'_def estran_def estran_nx_def) by fast
  from EJoin_cases2[OF a] show ?thesis
  proof(auto)
    fix es1' :: "(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys"
    assume a1: ‹Γ ⊢ (compile bp1, s, x) ─es[a]→ (es1', t, y)›
    assume a2: ‹bp' = es1' ⋈ compile bp2›
    from a1 bp1 obtain P' where P': ‹(bp1, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ es1' = compile P'›
      apply(simp add: estran'_def estran_nx_def estran_def) by blast
    show ‹∃P'. (Flow bp1 bp2, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ es1' ⋈ compile bp2 = compile P'›
      apply(rule exI)
      apply(rule conjI)
       apply(rule flow1)
      using P' apply blast
      using P' by simp
  next
    fix es2' :: "(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys"
    assume a1: ‹Γ ⊢ (compile bp2, s, x) ─es[a]→ (es2', t, y)›
    assume a2: ‹bp' = compile bp1 ⋈ es2'›
    from a1 bp2 obtain P' where P': ‹(bp2, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ es2' = compile P'›
      apply(simp add: estran'_def estran_nx_def estran_def) by blast
    show ‹∃P'. (Flow bp1 bp2, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ compile bp1 ⋈ es2' = compile P'›
      using P' flow2 by fastforce
  next
    assume a1: ‹compile bp1 = fin›
    assume a2: ‹compile bp2 = fin›
    have *: ‹compile ActTerminator = fin› by simp
    have 1: ‹bp1 = ActTerminator› using * compile_inj a1 by metis
    have 2: ‹bp2 = ActTerminator› using * compile_inj a2 by metis
    show ‹∃P'. (Flow bp1 bp2, t) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ fin = compile P'›
      using 1 2 flow_fin by fastforce
  qed
qed

lemma flow_cor2:
  assumes bp1: "⋀bp' s t. (bp1, s) ⟶⇩b⇩p⇩e⇩l (bp', t) ⟹
                ∃Q'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys. Γ ⊢ (compile bp1, s) ─es→ (Q', t) ∧ Q' = compile bp'"
  assumes bp2: "⋀bp' s t. (bp2, s) ⟶⇩b⇩p⇩e⇩l (bp', t) ⟹
                ∃Q'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys. Γ ⊢ (compile bp2, s) ─es→ (Q', t) ∧ Q' = compile bp'"
  assumes bstep: "(Flow bp1 bp2, s) ⟶⇩b⇩p⇩e⇩l (bp', t)"
  shows "∃Q'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys. Γ ⊢ (compile (Flow bp1 bp2), s) ─es→ (Q', t) ∧ Q' = compile bp'"
proof -
  from bstep have "(∃c. bp' = Flow c bp2 ∧ (bp1,s)⟶⇩b⇩p⇩e⇩l(c,t))
        ∨ (∃d. bp' = Flow bp1 d ∧ (bp2,s)⟶⇩b⇩p⇩e⇩l(d,t))
        ∨ bp' = ActTerminator ∧ bp1 = ActTerminator ∧ bp2 = ActTerminator ∧ s = t"
    using bpel_flow_cases by blast
  then show ?thesis
  proof
    assume "∃c. bp' = Flow c bp2 ∧ (bp1, s) ⟶⇩b⇩p⇩e⇩l (c, t)"
    then obtain c where bp': "bp' = Flow c bp2 ∧ (bp1, s) ⟶⇩b⇩p⇩e⇩l (c, t)" by blast
    with bp1 have "∃Q'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys. Γ ⊢ (compile bp1, s) ─es→ (Q', t) ∧ Q' = compile c" by blast
    hence es1_tran: "Γ ⊢ ((compile bp1::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys), s) ─es→ (compile c, t)" by simp
    then obtain x y a where a: "Γ ⊢ ((compile bp1::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys), s, x) ─es[a]→ (compile c, t, y)"
      apply(simp add:estran'_def estran_def estran_nx_def) by blast
    have "Γ ⊢ ((compile (Flow bp1 bp2)::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys), s) ─es→ (compile (Flow c bp2), t)"
      apply auto apply(simp add:estran'_def estran_def estran_nx_def) apply(rule exI)+
      apply(rule EJoin1) using a by blast
    moreover have "(compile (Flow c bp2) ::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys) = compile bp'" using bp' by fast
    ultimately show ?thesis by auto
  next
    assume "(∃d. bp' = Flow bp1 d ∧ (bp2, s) ⟶⇩b⇩p⇩e⇩l (d, t)) ∨
    bp' = ActTerminator ∧ bp1 = ActTerminator ∧ bp2 = ActTerminator ∧ s = t"
    then show ?thesis
    proof
      assume " ∃d. bp' = Flow bp1 d ∧ (bp2, s) ⟶⇩b⇩p⇩e⇩l (d, t)"
      then obtain d where bp': "bp' = Flow bp1 d ∧ (bp2, s) ⟶⇩b⇩p⇩e⇩l (d, t)" by blast
      with bp2 have "∃Q'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys. Γ ⊢ (compile bp2, s) ─es→ (Q', t) ∧ Q' = compile d" by blast
      hence es2_tran: "Γ ⊢ ((compile bp2::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys), s) ─es→ (compile d, t)" by simp
      then obtain x y a where a: "Γ ⊢ ((compile bp2::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys), s,x) ─es[a]→ (compile d, t,y)"
        apply(simp add:estran'_def estran_def estran_nx_def) by blast

      have "Γ ⊢ ((compile (Flow bp1 bp2)::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys), s) ─es→ (compile (Flow bp1 d), t)"
        apply auto apply(simp add:estran'_def estran_def estran_nx_def) apply(rule exI)+
        apply(rule EJoin2) using a by blast
      moreover have "(compile (Flow bp1 d)::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys) = compile bp'" using bp' by fast
      ultimately show ?thesis by auto
    next
      assume "bp' = ActTerminator ∧ bp1 = ActTerminator ∧ bp2 = ActTerminator ∧ s = t"
      hence "Γ ⊢ (compile (Flow bp1 bp2), s) ─es→ (fin::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys, t) ∧ (fin::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys) = compile bp'"
        apply auto using EJoin_fin apply(simp add:estran'_def estran_def estran_nx_def) by fast
      then show ?thesis by auto
    qed
  qed
qed

subsection‹correctness of translating While›

lemma EWhile_i:
  "Γ ⊢ (EWhile b P, s, x) ─es[a]→ (Q, t, y) ⟹
   s = t ∧ Q = ESeq P (EWhile b P) ∧ s ∈ b ∧ P ≠ fin ∨
   s = t ∧ Q = fin ∧ s ∉ b"
  apply(rule estran_p.cases) by auto

lemma while_cor1:
  assumes bp: "⋀(bp'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys) s t. Γ ⊢ (compile bp, s) ─es→ (bp', t) ⟹ ∃P'. (bp, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ bp' = compile P'"
  assumes estep: "Γ ⊢ (compile (Activity.While x1 bp), s) ─es→ ((es'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys), t)"
  shows "∃P'. (Activity.While x1 bp, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ es' = compile P'"
proof -
  from estep obtain x y a where estep': "Γ ⊢ (compile (Activity.While x1 bp), s,x) ─es[a]→ (es', t,y)"
    apply(simp add:estran'_def estran_def estran_nx_def) by fast
  have "s = t ∧ es' = (compile bp) NEXT EWhile x1 (compile bp) ∧ s ∈ x1 ∧ compile bp ≠ (fin::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys) ∨ s = t ∧ es' = fin ∧ s ∉ x1"
    using EWhile_i[OF estep'[simplified]] .
  then show ?thesis
  proof
    assume IH: "s = t ∧ es' = (compile bp) NEXT EWhile x1 (compile bp) ∧ s ∈ x1 ∧ compile bp ≠ (fin::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys)"
    then have ‹compile bp ≠ (fin::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys)› by argo
    with compile.simps(12) compile_inj have ‹bp ≠ ActTerminator› by blast
    let ?P' = "Seqb bp (Activity.While x1 bp)"
    have "(Activity.While x1 bp, s) ⟶⇩b⇩p⇩e⇩l (?P', t)"
      using whileT IH ‹bp ≠ ActTerminator› by blast
    moreover have "es' = compile ?P'" using IH by auto
    ultimately show ?thesis by fast
  next
    assume IH: "s = t ∧ es' = fin ∧ s ∉ x1"
    have "(Activity.While x1 bp, s) ⟶⇩b⇩p⇩e⇩l (ActTerminator, t)"
      using whileF IH by blast
    moreover have "es' = compile ActTerminator" using IH by simp
    ultimately show ?thesis by fast
  qed
qed

lemma while_cor2:
  assumes bp: "⋀bp' s t. (bp, s) ⟶⇩b⇩p⇩e⇩l (bp', t) ⟹ ∃Q'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys. Γ ⊢ (compile bp, s) ─es→ (Q', t) ∧ Q' = compile bp'"
  assumes bstep: "(Activity.While x1 bp, s) ⟶⇩b⇩p⇩e⇩l (bp', t)"
  shows "∃Q'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys. Γ ⊢ (compile (Activity.While x1 bp), s) ─es→ (Q', t) ∧ Q' = compile bp'"
proof -
  have "s ∈ x1 ∧ bp' = Seqb bp (Activity.While x1 bp) ∧ s = t ∧ bp≠ActTerminator
      ∨ s ∉ x1 ∧ bp' = ActTerminator ∧ s = t" using bpel_while_cases[OF bstep] .
  then show ?thesis
  proof
    assume IH: "s ∈ x1 ∧ bp' = Seqb bp (Activity.While x1 bp) ∧ s = t ∧ bp≠ActTerminator"
    let ?Q' = "ESeq (compile bp) (compile (Activity.While x1 bp))::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys"
    have ‹bp ≠ ActTerminator› using IH by argo
    obtain x k where "Γ ⊢ (compile (Activity.While x1 bp), s,x) ─es[Cmd♯k]→ (?Q', t,x)"
    proof-
      assume a: ‹⋀(x::'c ⇒ (('a, 'b) EventLabel × ('a, 'b) State set × ('a, 'b) State com option) option) k. Γ ⊢ (compile (Activity.While x1 bp), s, x) ─es[Cmd♯k]→ (compile bp NEXT compile (Activity.While x1 bp), t, x) ⟹ thesis›
      show thesis
        apply(rule a)
        using IH apply simp
        apply(rule EWhileT[of t x1 "compile bp::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys" Γ])
         apply blast
        using ‹bp ≠ ActTerminator› bpel_translator.compile.simps(12) compile_inj by metis
    qed
    hence "Γ ⊢ (compile (Activity.While x1 bp), s) ─es→ (?Q', t)"
      apply(simp add:estran'_def estran_def estran_nx_def) by auto
    moreover have "?Q' = compile bp'" using IH by simp
    ultimately show ?thesis by fast
  next
    assume IH: "s ∉ x1 ∧ bp' = ActTerminator ∧ s = t"
    obtain x y k where "Γ ⊢ (compile (Activity.While x1 bp), s,x) ─es[Cmd♯k]→ ((fin::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys), t,y)"
      using EWhileF[of s x1 Γ "compile bp"] IH by fastforce
    hence "Γ ⊢ (compile (Activity.While x1 bp), s) ─es→ ((fin::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys), t)"
      apply(simp add:estran'_def estran_def estran_nx_def) by auto
    moreover have "fin = compile bp'" using IH by simp
    ultimately show ?thesis by fast
  qed
qed

subsection‹correctness of compile›

lemma compile_invoke_aux1_1:
  ‹(Invoke x1 x2 x3 x4 x5 ((a, b) # list) h, s) ⟶⇩b⇩p⇩e⇩l (P', t)  ⟹
   (Invoke x1 x2 x3 x4 x5 ((aa, ba) # (a, b) # list) h, s) ⟶⇩b⇩p⇩e⇩l (P', t)›
  apply(erule activity_tran.cases, auto)
    apply(rule invoke_suc)
     apply assumption
  apply (rule refl)
   apply(rule invoke_fault)
     apply assumption
    apply(rule refl)
   apply simp
  apply(rule invoke_fault)
    apply assumption
    apply(rule refl)
   apply force
  apply(rule invoke_fault)
    apply assumption
   apply(rule refl)
  by force

lemma compile_invoke_aux1:
  ‹
       (⋀aa ba x6aa bp' s t.
           aa = a ∧ ba = b ∨ (aa, ba) ∈ set list ⟹
           x6aa = ba ⟹ ∃x y a. Γ ⊢ (compile ba, s, x) ─es[a]→ (bp', t, y) ⟹ ∃P'. (ba, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ bp' = compile P') ⟹
       Γ ⊢ (OR_list
              (EAtom (l, Collect (targets_sat (targets x1)), Some (Basic (fire_sources (sources x1)))) NEXT compile b #
               map (ESeq (EAtom (l, Collect (targets_sat (targets x1)), Some (Basic (fire_sources (sources x1))))) ∘ compile ∘ snd)
                list),
             s, xa) ─es[ab]→ (bp', t, ya) ⟹
       ∃P'. (Invoke x1 x2 x3 x4 x5 ((a, b) # list) h, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ bp' = compile P'›
  apply(induct list arbitrary: a b)
    apply(simp add: estran'_def estran_nx_def estran_def)
    apply(erule estran_p.cases, auto)[]
     apply(erule estran_p.cases, auto)[]
    apply(erule estran_p.cases, auto)[]
    apply(simp add: guard_def ptrans_def body_def)
  apply(rule_tac x=b in exI)
  apply(rule conjI)
  apply(rule invoke_fault)
    apply(erule ctrans_from_basic_cases)
      apply(assumption)
    apply(erule ctrans_from_basic_cases)
      apply(assumption)
    apply simp
   apply simp

  apply simp
  apply(erule estran_p.cases, auto)[]
   apply(erule estran_p.cases, auto)[]
    apply(erule estran_p.cases, auto)[]
   apply(erule estran_p.cases, auto)[]
   apply(simp add: guard_def ptrans_def body_def)
  apply(rule_tac x=ba in exI)
  apply(rule conjI)
  apply(rule invoke_fault)
  apply assumption
     apply(erule ctrans_from_basic_cases)
     apply assumption
    apply simp
  apply(rule refl)

  apply(subgoal_tac ‹∃P'. (Invoke x1 x2 x3 x4 x5 ((a, b) # list) h, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ bp' = compile P'›)
   prefer 2 apply presburger
  apply(erule exE)
  apply(erule conjE)
  apply(rule_tac x=P' in exI)
  apply(rule conjI) prefer 2 apply assumption
  using compile_invoke_aux1_1 by metis

lemma compile_pick_aux1:
  assumes x1: ‹∀(bp':: (('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys) s t. Γ ⊢ (compile_eh x1, s) ─es→ (bp', t) ⟶ (∃x1'. (x1, s) ⟶⇩e⇩h (x1', t) ∧ bp' = compile x1')›
  assumes x2: ‹∀(bp':: (('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys) s t. Γ ⊢ (compile_eh x2, s) ─es→ (bp', t) ⟶ (∃x2'. (x2, s) ⟶⇩e⇩h (x2', t) ∧ bp' = compile x2')›
  assumes tran: ‹Γ ⊢ (compile (Pick x1 x2), s) ─es→ (bp':: (('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys, t)›
  shows ‹∃P'. (Pick x1 x2, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ bp' = compile P'›
  using tran x1[rule_format] x2[rule_format] apply(simp add: estran'_def estran_def estran_nx_def)
  apply(erule exE)+
  apply(erule estran_p.cases, auto)[]
   apply(subgoal_tac ‹∃x1'. (x1, s) ⟶⇩e⇩h (x1', t) ∧ bp' = compile x1'›)
    prefer 2 apply blast
   apply(erule exE)
   apply(rule_tac x=x1' in exI)
   apply(rule conjI)
    apply(rule pick1)
    apply argo
   apply argo
  apply(subgoal_tac ‹∃x2'. (x2, s) ⟶⇩e⇩h (x2', t) ∧ bp' = compile x2'›)
   prefer 2 apply blast
  apply(erule exE)
  apply(rule_tac x=x2' in exI)
  apply(rule conjI)
   apply(rule pick2)
   apply argo
  apply argo
  done

lemma compile_step_sim1:
  "Γ ⊢ (compile bp, s) ─es→ (bp', t) ⟹ ∃P'. (bp, s) ⟶⇩b⇩p⇩e⇩l (P', t) ∧ bp' = compile P'"
  apply(induct bp arbitrary: bp' s t)
               prefer 11 subgoal for bp1 bp2 bp' s t using flow_cor1[of Γ bp1 bp2 s bp' t] by blast
              prefer 9 subgoal for x1 bp bp' s t using while_cor1[of Γ bp x1 s bp' t] by blast
      ― ‹invoke›
  subgoal for x1 x2 x3 x4 x5 x6 x7 bp' s t
    apply(cases x7; simp)
     apply(cases x6; simp)
      apply(rule exI)
      apply(rule conjI)
       apply(rule invoke_suc)
        apply(simp add: estran'_def estran_def estran_nx_def)
        apply(erule exE)+
        apply(erule estran_p.cases, auto simp add: guard_def)[]
       apply(simp add: estran'_def estran_def estran_nx_def)
       apply(erule exE)+
       apply(erule estran_p.cases, auto)[]
       apply(simp add: ptrans_def body_def)
    using ctrans_from_basic_seq_basic_cases apply metis
      apply(simp add: estran'_def estran_def estran_nx_def)
      apply(erule exE)+
      apply(erule estran_p.cases, auto)[]
     apply(simp add: estran'_def estran_def estran_nx_def)
     apply(erule exE)+
     apply(erule estran_p.cases, auto)[]
      apply(rule exI)
      apply(rule conjI)
       apply(rule invoke_suc)
        apply(erule estran_p.cases, auto)[]
        apply(simp add: guard_def ptrans_def)
       apply(erule estran_p.cases, auto)[]
       apply(simp add: guard_def ptrans_def body_def)
       apply(erule ctrans_from_basic_seq_basic_cases)
       apply assumption
      apply(erule estran_p.cases, auto)[]
     apply(rule compile_invoke_aux1)
      apply fast
     apply assumption
    apply(cases x6; simp)
     apply(simp add: estran'_def estran_def estran_nx_def)
     apply(erule exE)+
     apply(erule estran_p.cases, auto)[]
      apply(erule estran_p.cases, auto)[]
      apply(simp add: guard_def ptrans_def body_def)
      apply(rule exI[where x=ActTerminator])
      apply(rule conjI)
       apply(rule invoke_suc)
        apply(erule ctrans_from_basic_seq_basic_cases)
        apply assumption
       apply(erule ctrans_from_basic_seq_basic_cases)
       apply assumption
      apply simp
     apply(erule estran_p.cases, auto)[]
      apply(erule estran_p.cases, auto)[]
     apply(erule estran_p.cases, auto)[]
     apply(simp add: guard_def ptrans_def body_def)
     apply(rule_tac x=a in exI)
     apply(rule conjI)
      apply(rule invoke_fault)
        apply assumption
       apply(rule ctrans_from_basic_cases[of "fire_sources (sources x1)" s t])
        apply assumption
       apply assumption
      apply simp
     apply(rule refl)
    apply(simp add: estran'_def estran_def estran_nx_def)
    apply(erule exE)+
    apply(erule estran_p.cases, auto)[]
     apply(erule estran_p.cases, auto)[]
     apply(simp add: guard_def ptrans_def body_def)
     apply(rule exI[where x=ActTerminator])
     apply(rule conjI)
      apply(rule invoke_suc)
       apply assumption
      apply(erule ctrans_from_basic_seq_basic_cases)
      apply assumption
     apply simp
    apply(erule estran_p.cases, auto)[]
     apply(erule estran_p.cases, auto)[]
      apply(erule estran_p.cases, auto)[]
     apply(erule estran_p.cases, auto)[]
     apply(simp add: guard_def ptrans_def body_def)
     apply(rule_tac x=a in exI)
     apply(rule conjI)
      apply(rule invoke_fault)
        apply assumption
       apply(rule ctrans_from_basic_cases[of "fire_sources (sources x1)" s t])
        apply assumption
       apply assumption
      apply simp
     apply(rule refl)
    apply(rule compile_invoke_aux1)
     prefer 2 apply fast
    by fast
      ― ‹receive›
  subgoal for x1 x2 x3 x4 x5 bp' s t
    apply(simp add: estran'_def estran_def estran_nx_def)
    apply(erule exE)+
    apply(erule estran_p.cases, auto)[]
    apply(simp add: guard_def ptrans_def body_def)
    apply(rule exI[where x=ActTerminator])
    apply simp
    using receive ctrans_from_basic_seq_basic_cases by metis
      ― ‹reply›
  subgoal for x1 x2 x3 x4 bp' s t
    apply(simp add: estran'_def estran_def estran_nx_def)
    apply(erule exE)+
    apply(erule estran_p.cases, auto)[]
    apply(simp add: guard_def ptrans_def body_def)
    apply(rule exI[where x=ActTerminator])
    apply simp
    using reply ctrans_from_basic_cases by metis
      ― ‹assign›
  subgoal for x1 x2 bp' s t
    apply(simp add: estran'_def estran_def estran_nx_def)
    apply(erule exE)+
    apply(erule estran_p.cases, auto)[]
    apply(simp add: guard_def ptrans_def body_def)
    apply(rule exI[where x=ActTerminator])
    apply simp
    using assign ctrans_from_basic_seq_basic_cases by metis
      ― ‹wait›
  subgoal for x1 x2 bp' s t
    apply(simp add: estran'_def estran_def estran_nx_def)
    apply(erule exE)+
    apply(erule estran_p.cases, auto)[]
    apply(simp add: guard_def ptrans_def body_def)
    apply(rule exI[where x=ActTerminator])
    apply simp
    using wait ctrans_from_basic_cases by metis
      ― ‹empty›
  subgoal for x bp' s t
    apply(simp add: estran'_def estran_def estran_nx_def)
    apply(erule exE)+
    apply(erule estran_p.cases, auto)[]
    apply(simp add: guard_def ptrans_def body_def)
    apply(rule exI[where x=ActTerminator])
    apply simp
    using empty ctrans_from_basic_cases by metis
      ― ‹seq›
  subgoal for bp1 bp2 bp' s t
    apply(simp add: estran'_def estran_def estran_nx_def)
    apply(erule exE)+
    apply(erule estran_p.cases, auto)[]
     apply(subgoal_tac ‹∃bp1'. (bp1, s) ⟶⇩b⇩p⇩e⇩l (bp1', t) ∧ es1' = compile bp1'›)
      prefer 2 apply blast
     apply(erule exE)
     apply(rule_tac x=‹Seqb bp1' bp2› in exI)
     apply(rule conjI)
      apply(rule seq)
       apply argo
      apply force
     apply simp
    apply(rule exI[where x=bp2])
    apply simp
    apply(rule seq_fin)
    apply(subgoal_tac ‹∃bp1'. (bp1, s) ⟶⇩b⇩p⇩e⇩l (bp1', t) ∧ fin = compile bp1'›)
     prefer 2 apply blast
    apply(erule exE)
    using compile_inj compile.simps(12) by metis
      ― ‹if›
  subgoal for x1 bp1 bp2 bp' s t
    apply(simp add: estran'_def estran_def estran_nx_def)
    apply(erule exE)+
    apply(erule estran_p.cases, auto)[]
     apply(rule exI[where x=bp1])
     apply(rule conjI)
      apply(erule estran_p.cases, auto)[]
       apply(erule estran_p.cases, auto)[]
      apply(erule estran_p.cases, auto)[]
      apply(simp add: guard_def ptrans_def body_def)
      apply(erule ctrans_from_skip_cases)
      apply simp
      apply(rule ifT)
      apply assumption
     apply(erule estran_p.cases, auto)[]
     apply(erule estran_p.cases, auto)[]
    apply(rule exI[where x=bp2])
    apply(rule conjI)
     apply(erule estran_p.cases, auto)[]
      apply(erule estran_p.cases, auto)[]
     apply(erule estran_p.cases, auto)[]
     apply(simp add: guard_def ptrans_def body_def)
     apply(erule ctrans_from_skip_cases)
     apply simp
     apply(rule ifF)
     apply assumption
    apply(erule estran_p.cases, auto)[]
    apply(erule estran_p.cases, auto)[]
    done
      ― ‹pick›
     apply(rule compile_pick_aux1)
       apply assumption
      apply assumption
     apply assumption
    ― ‹terminator›
  subgoal for bp' s t
    apply(simp add: estran'_def estran_def estran_nx_def)
    apply(erule exE)+
    using no_estran_from_fin by fast
      ― ‹OnMessage›
  subgoal for x1 x2 x3 x4 bp
    apply(rule allI)+
    apply(rule impI)
    apply(simp add: estran'_def estran_def estran_nx_def)
    apply(erule exE)+
    apply(erule estran_p.cases, auto)[]
     apply(erule estran_p.cases, auto)[]
    apply(erule estran_p.cases, auto)[]
    apply(simp add: guard_def ptrans_def body_def)
    apply(erule ctrans_from_basic_cases)
    apply(rule exI[where x=bp])
    apply simp
    apply(rule on_message)
    by (rule refl)
      ― ‹OnAlarm›
  subgoal for x1 bp
    apply(rule allI)+
    apply(rule impI)
    apply(simp add: estran'_def estran_def estran_nx_def)
    apply(erule exE)+
    apply(erule estran_p.cases, auto)[]
     apply(erule estran_p.cases, auto)[]
    apply(erule estran_p.cases, auto)[]
    apply(simp add: guard_def ptrans_def body_def)
    apply(erule ctrans_from_skip_cases)apply(rule exI[where x=bp])
    apply simp
    apply(rule on_alarm)
    by assumption
  done

lemma EChc1':
  ‹Γ ⊢ (es1,s) ─es→ (es1',t) ⟹ Γ ⊢ (EChc es1 es2, s) ─es→ (es1', t)›
  apply(simp add: estran'_def estran_nx_def estran_def)
  apply(erule exE)+
  apply(rule_tac x=x in exI)
  apply(rule_tac x=y in exI)
  apply(rule_tac x=a in exI)
  using EChc1 by fast

lemma EChc2':
  ‹Γ ⊢ (es2,s) ─es→ (es2',t) ⟹ Γ ⊢ (EChc es1 es2, s) ─es→ (es2', t)›
  apply(simp add: estran'_def estran_nx_def estran_def)
  apply(erule exE)+
  apply(rule_tac x=x in exI)
  apply(rule_tac x=y in exI)
  apply(rule_tac x=a in exI)
  using EChc2 by fast

lemma compile_invoke_aux2:
  ‹evh ∈ snd ` set (a#list) ⟹ targets_sat (targets fls) s ⟹
       Γ ⊢ (OR_list
              (EAtom (l, Collect (targets_sat (targets fls)), Some (Basic (fire_sources (sources fls)))) NEXT compile (snd a) #
               map (ESeq (EAtom (l, Collect (targets_sat (targets fls)), Some (Basic (fire_sources (sources fls))))) ∘ compile ∘ snd)
                list),
             s) ─es→ (compile evh, fire_sources (sources fls) s)›
  apply(induct list arbitrary:a)
   apply(simp add: estran'_def estran_nx_def estran_def)
   apply(rule exI)+
   apply(rule ESeq_fin)
   apply(rule EAtom)
     apply(simp add: body_def)
    apply(simp add: guard_def)
   apply(simp add: ptrans_def)
   apply(rule converse_rtrancl_into_rtrancl)
    apply(rule ctran.Basic)
   apply(rule rtrancl_refl)

  apply simp
  apply(erule disjE)
   apply(rule EChc1')
   apply(simp add: estran'_def estran_nx_def estran_def)
   apply(rule exI)+
   apply(rule ESeq_fin)
   apply(rule EAtom)
     apply(rule refl)
    apply(simp add: guard_def)
   apply(simp add: ptrans_def)
   apply(simp add: body_def)
   apply(rule converse_rtrancl_into_rtrancl)
    apply(rule ctran.Basic)
   apply(rule rtrancl_refl)
  apply(rule EChc2')
  by blast

⌦‹∀Q s t. (x1, s) ⟶⇩e⇩h (Q, t) ⟶ Γ ⊢ (compile_eh x1, s) ─es→ (compile Q, t)›

lemma compile_pick_aux2:
  ‹∀Q s t. (x1, s) ⟶⇩e⇩h (Q, t) ⟶ Γ ⊢ (compile_eh x1, s) ─es→ (compile Q :: (('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys, t) ⟹
   ∀Q s t. (x2, s) ⟶⇩e⇩h (Q, t) ⟶ Γ ⊢ (compile_eh x2, s) ─es→ (compile Q :: (('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys, t) ⟹
   (Pick x1 x2, s) ⟶⇩b⇩p⇩e⇩l (bp', t) ⟹
   ∃(Q'::(('a, 'b) EventLabel, 'c, ('a, 'b) State, ('a, 'b) State com option) esys). Γ ⊢ (compile (Pick x1 x2), s) ─es→ (Q', t) ∧ Q' = compile bp'›
  apply(erule activity_tran.cases; simp)
   apply(simp add: estran'_def estran_nx_def estran_def)
   apply(subgoal_tac ‹∃x y aa. Γ ⊢ (compile_eh a, s, x) ─es[aa]→ (compile Q, t, y)›)
    prefer 2 apply fast
   apply(erule exE)+
   apply(rule_tac x=x in exI)
   apply(rule_tac x=y in exI)
   apply(rule_tac x=aa in exI)
   apply(rule EChc1)
   apply simp
  apply(simp add: estran'_def estran_nx_def estran_def)
  apply(subgoal_tac ‹∃x y aa. Γ ⊢ (compile_eh b, s, x) ─es[aa]→ (compile Q, t, y)›)
   prefer 2 apply fast
  apply(erule exE)+
  apply(rule_tac x=x in exI)
  apply(rule_tac x=y in exI)
  apply(rule_tac x=aa in exI)
  apply(rule EChc2)
  apply simp
  done

lemma compile_step_sim2:
  "(bp, s) ⟶⇩b⇩p⇩e⇩l (bp', t) ⟹ ∃Q'. Γ ⊢ (compile bp, s) ─es→ (Q', t) ∧ Q' = compile bp'"
  apply(induct bp arbitrary: bp' s t)
               prefer 11 subgoal for bp1 bp2 bp' s t using flow_cor2[of bp1 Γ bp2 s bp' t] by blast
              prefer 9 subgoal for x1 bp bp' s t using while_cor2[of bp Γ x1 s bp' t] by blast
      ― ‹invoke›
  subgoal for x1 x2 x3 x4 x5 x6 x7 bp' s t
    apply(cases x7; simp)
     apply(cases x6; simp)
      apply(erule activity_tran.cases; simp)
      apply(simp add: estran'_def estran_nx_def estran_def)
      apply(rule exI)+
      apply(rule EAtom)
        apply(rule refl)
       apply(simp add: guard_def)
      apply(simp add: ptrans_def body_def)
      apply(rule converse_rtrancl_into_rtrancl)
       apply(rule Seq1)
       apply(rule ctran.Basic)
      apply(rule converse_rtrancl_into_rtrancl)
       apply(rule ctran.Basic)
      apply(rule rtrancl_refl)
     apply(erule activity_tran.cases; simp)
      apply(simp add: estran'_def estran_nx_def estran_def)
      apply(rule exI)+
      apply(rule EChc1)
      apply(rule EAtom)
        apply(rule refl)
       apply(simp add: guard_def)
      apply(simp add: ptrans_def body_def)
      apply(rule converse_rtrancl_into_rtrancl)
       apply(rule Seq1)
       apply(rule ctran.Basic)
      apply(rule converse_rtrancl_into_rtrancl)
       apply(rule ctran.Basic)
      apply(rule rtrancl_refl)
     apply(rule EChc2')
     apply(rule compile_invoke_aux2)
      apply argo
     apply assumption
    apply(cases x6; simp)
     apply(erule activity_tran.cases; simp)
      apply(simp add: estran'_def estran_nx_def estran_def)
      apply(rule exI)+
      apply(rule EChc1)
      apply(rule EAtom)
        apply(rule refl)
       apply(simp add: guard_def)
      apply(simp add: ptrans_def body_def)
      apply(rule converse_rtrancl_into_rtrancl)
       apply(rule Seq1)
       apply(rule ctran.Basic)
      apply(rule converse_rtrancl_into_rtrancl)
       apply(rule ctran.Basic)
      apply(rule rtrancl_refl)
     apply(rule EChc2')
     apply(simp add: estran'_def estran_nx_def estran_def)
     apply(rule exI)+
     apply(rule ESeq_fin)
     apply(rule EAtom)
       apply(rule refl)
      apply(simp add: guard_def)
     apply(simp add: ptrans_def body_def)
     apply(rule converse_rtrancl_into_rtrancl)
      apply(rule ctran.Basic)
     apply(rule rtrancl_refl)
    apply(erule activity_tran.cases; simp)
     apply(simp add: estran'_def estran_nx_def estran_def)
     apply(rule exI)+
     apply(rule EChc1)
     apply(rule EAtom)
       apply(rule refl)
      apply(simp add: guard_def)
     apply(simp add: ptrans_def body_def)
     apply(rule converse_rtrancl_into_rtrancl)
      apply(rule Seq1)
      apply(rule ctran.Basic)
     apply(rule converse_rtrancl_into_rtrancl)
      apply(rule ctran.Basic)
     apply(rule rtrancl_refl)
    apply(rule EChc2')
    apply(erule disjE)
     apply(rule EChc2')
     apply(rule compile_invoke_aux2)
      apply argo
     apply assumption
    apply(rule EChc1')
    apply(simp add: estran'_def estran_nx_def estran_def)
    apply(rule exI)+
    apply(rule ESeq_fin)
    apply(rule EAtom)
      apply(simp add: body_def)
     apply(simp add: guard_def)
    apply(simp add: ptrans_def)
    apply(rule converse_rtrancl_into_rtrancl)
     apply(rule ctran.Basic)
    apply(rule rtrancl_refl)
    done
      ― ‹receive›
  subgoal for x1 x2 x3 x4 x5 bp' s t
    apply(erule activity_tran.cases; simp)
    apply(simp add: estran'_def estran_nx_def estran_def)
    apply(rule exI)+
    apply(rule EAtom)
      apply(rule refl)
     apply(simp add: guard_def)
    apply(simp add: ptrans_def body_def)
    apply(rule converse_rtrancl_into_rtrancl)
     apply(rule Seq1)
     apply(rule ctran.Basic)
    apply(rule converse_rtrancl_into_rtrancl)
     apply(rule ctran.Basic)
    apply(rule rtrancl_refl)
    done
      ― ‹reply›
  subgoal for x1 x2 x3 x4 bp' s t
    apply(erule activity_tran.cases; simp)
    apply(simp add: estran'_def estran_nx_def estran_def)
    apply(rule exI)+
    apply(rule EAtom)
      apply(rule refl)
     apply(simp add: guard_def)
    apply(simp add: ptrans_def body_def)
    apply(rule converse_rtrancl_into_rtrancl)
     apply(rule ctran.Basic)
    apply(rule rtrancl_refl)
    done
      ― ‹assign›
  subgoal for x1 x2 bp' s t
    apply(erule activity_tran.cases; simp)
    apply(simp add: estran'_def estran_nx_def estran_def)
    apply(rule exI)+
    apply(rule EAtom)
      apply(rule refl)
     apply(simp add: guard_def)
    apply(simp add: ptrans_def body_def)
    apply(rule converse_rtrancl_into_rtrancl)
     apply(rule Seq1)
     apply(rule ctran.Basic)
    apply(rule converse_rtrancl_into_rtrancl)
     apply(rule ctran.Basic)
    apply(rule rtrancl_refl)
    done
      ― ‹wait›
  subgoal for x1 x2 bp' s t
    apply(erule activity_tran.cases; simp)
    apply(simp add: estran'_def estran_nx_def estran_def)
    apply(rule exI)+
    apply(rule EAtom)
      apply(rule refl)
     apply(simp add: guard_def)
    apply(simp add: ptrans_def body_def)
    apply(rule converse_rtrancl_into_rtrancl)
     apply(rule ctran.Basic)
    apply(rule rtrancl_refl)
    done
      ― ‹empty›
  subgoal for x bp' s t
    apply(erule activity_tran.cases; simp)
    apply(simp add: estran'_def estran_nx_def estran_def)
    apply(rule exI)+
    apply(rule EAtom)
      apply(rule refl)
     apply(simp add: guard_def)
    apply(simp add: ptrans_def body_def)
    apply(rule converse_rtrancl_into_rtrancl)
     apply(rule ctran.Basic)
    apply(rule rtrancl_refl)
    done
      ― ‹seq›
  subgoal for bp1 bp2 bp' s t
    apply(erule activity_tran.cases; simp)
     apply(simp add: estran'_def estran_nx_def estran_def)
     apply(subgoal_tac ‹∃x y a. Γ ⊢ (compile P, s, x) ─es[a]→ (compile P', t, y)›)
      prefer 2 apply blast
     apply(erule exE)+
     apply(rule_tac x=x in exI)
     apply(rule_tac x=y in exI)
     apply(rule_tac x=a in exI)
     apply(rule ESeq)
      apply assumption
    using compile_inj compile.simps(12) apply metis
    apply(simp add: estran'_def estran_nx_def estran_def)
    apply(subgoal_tac ‹∃x y a. Γ ⊢ (compile P, s, x) ─es[a]→ (fin, t, y)›)
     prefer 2 apply fastforce
    apply(erule exE)+
    apply(rule_tac x=x in exI)
    apply(rule_tac x=y in exI)
    apply(rule_tac x=a in exI)
    apply(rule ESeq_fin)
    apply assumption
    done
      ― ‹if›
  subgoal for x1 bp1 bp2 bp' s t
    apply(erule activity_tran.cases; simp)
     apply(simp add: estran'_def estran_nx_def estran_def)
     apply(rule exI)+
     apply(rule EChc1)
     apply(rule ESeq_fin)
     apply(rule EAtom)
       apply(rule refl)
      apply(simp add: guard_def)
     apply(simp add: ptrans_def body_def)
     apply(rule converse_rtrancl_into_rtrancl)
    unfolding Skip_def apply(rule ctran.Basic)
     apply simp
    apply(simp add: estran'_def estran_nx_def estran_def)
    apply(rule exI)+
    apply(rule EChc2)
    apply(rule ESeq_fin)
    apply(rule EAtom)
      apply(rule refl)
     apply(simp add: guard_def)
    apply(simp add: ptrans_def body_def)
    apply(rule converse_rtrancl_into_rtrancl)
     apply(rule ctran.Basic)
    apply simp
    done
      ― ‹pick›
     apply(rule compile_pick_aux2)
       apply assumption
      apply assumption
     apply assumption
    ― ‹terminator›
    apply(erule activity_tran.cases; simp)
    ― ‹on message›
  subgoal for x1 x2 x3 x4 bp
    apply(rule allI)+
    apply(rule impI)
    apply(erule evthandler_tran.cases; simp)
    apply(simp add: estran'_def estran_nx_def estran_def)
    apply(rule exI)+
    apply(rule ESeq_fin)
    apply(rule EAtom)
      apply(rule refl)
     apply(simp add: guard_def)
    apply(simp add: ptrans_def body_def)
    apply(rule converse_rtrancl_into_rtrancl)
     apply(rule ctran.Basic)
    apply simp
    done
      ― ‹on alarm›
  subgoal for x1 bp
    apply(rule allI)+
    apply(rule impI)
    apply(erule evthandler_tran.cases; simp)
    apply(simp add: estran'_def estran_nx_def estran_def)
    apply(rule exI)+
    apply(rule ESeq_fin)
    apply(rule EAtom)
      apply(rule refl)
     apply(simp add: guard_def)
    apply(simp add: ptrans_def body_def)
    apply(rule converse_rtrancl_into_rtrancl)
    unfolding Skip_def apply(rule ctran.Basic)
    apply simp
    done
  done

lemma bpel_bisim_es: "Γ ⊢ (bpel,s) ≃ (compile bpel,s)"
  apply(coinduction arbitrary: bpel s)
  apply auto
  subgoal for bpel s P' t using compile_step_sim2 by fast
  subgoal for bpel s Q' t using compile_step_sim1 by fast
  done

theorem "Γ ⊢ bp ≈ (compile bp)"
  apply(simp add:bpel_bisim_es'_strong_def)
  using bpel_bisim_es by fast

end