Theory FL_Bisimilarity_Implies_Equivalence

theory FL_Bisimilarity_Implies_Equivalence

section ‹\texorpdfstring{$F/L$}{F/L}-Bisimilarity Implies Logical Equivalence›

context indexed_effect_nominal_ts

  lemma FL_bisimilarity_implies_equivalence_Act:
    assumes "f fs F"
    and "bn α ♯* (F, f)"
    and "x  𝒜[L (α, F, f)]"
    and "P Q. P ∼⋅[L (α, F, f)] Q  P  x  Q  x"
    and "P ∼⋅[F] Q"
    and "P  Act f α x"
    shows "Q  Act f α x"
  proof -
    have "finite (supp (fQ, F, f))"
      by (fact finite_supp)
    with P  Act f α x obtain α' x' P' where eq: "Act f α x = Act f α' x'" and trans: "fP  α',P'" and valid: "P'  x'" and fresh: "bn α' ♯* (fQ, F, f)"
      by (metis FL_valid_Act_strong)

    from P ∼⋅[F] Q and f fs F and fresh and trans obtain Q' where trans': "fQ  α',Q'" and bisim': "P' ∼⋅[L (α',F,f)] Q'"
      by (metis FL_bisimilar_simulation_step)

    from eq obtain p where p_α: "α' = p  α" and p_x: "x' = p  x"
        and fresh_p: "(supp x - bn α) ♯* p  (supp α - bn α) ♯* p"
        and supp_p: "supp p  bn α  p  bn α"
      by (metis Act_eq_iff_perm_renaming)

    from valid and p_x have "-p  P'  x"
      by (metis permute_minus_cancel(2) FL_valid_eqvt)

    moreover from fresh and p_α have "(p  bn α) ♯* (F, f)"
      by (simp add: bn_eqvt fresh_star_Pair)
    with bn α ♯* (F, f) and supp_p have "supp (F, f) ♯* p"
      by (meson UnE fresh_def fresh_star_def subsetCE)
    then have "supp F ♯* p" and "supp f ♯* p"
      by (simp add: fresh_star_Un supp_Pair)+

    with bisim' and p_α have "(-p  P') ∼⋅[L (α, F, f)] (-p  Q')"
      by (metis FL_bisimilar_eqvt L_eqvt' permute_minus_cancel(2) supp_perm_eq)

    ultimately have "-p  Q'  x"
      using P Q. P ∼⋅[L (α, F, f)] Q  P  x  Q  x by metis

    with p_x have "Q'  x'"
      by (metis permute_minus_cancel(1) FL_valid_eqvt)

    with eq and trans' show "Q  Act f α x"
      unfolding FL_valid_Act by metis

  theorem FL_bisimilarity_implies_equivalence: assumes "P ∼⋅[F] Q" shows "FL_logically_equivalent F P Q"
  unfolding FL_logically_equivalent_def proof
    fix x :: "('idx, 'pred, 'act, 'effect) formula"
    show "x  𝒜[F]  P  x  Q  x"
      assume "x  𝒜[F]" then show "P  x  Q  x"
      using assms proof (induction x arbitrary: P Q)
        case Conj then show ?case
          by simp
        case Not then show ?case
          by simp
        case Pred then show ?case
          by (metis FL_bisimilar_is_L_bisimulation is_L_bisimulation_def symp_def FL_valid_Pred)
        case Act then show ?case
          by (metis FL_bisimilar_symp FL_bisimilarity_implies_equivalence_Act sympE)