Theory L_Transform

theory L_Transform
imports
  Validity
  Bisimilarity_Implies_Equivalence
  FL_Equivalence_Implies_Bisimilarity
begin

section ‹\texorpdfstring{$L$}{L}-Transform›

subsection ‹States›

text ‹The intuition is that states of kind~‹AC› can perform ordinary actions, and states of
kind~‹EF› can commit effects.›

datatype ('state,'effect) L_state =
    AC "'effect × 'effect fs_set × 'state"
  | EF "'effect fs_set × 'state"

instantiation L_state :: (pt,pt) pt
begin

  fun permute_L_state :: "perm ⇒ ('a,'b) L_state ⇒ ('a,'b) L_state" where
    "p ∙ (AC x) = AC (p ∙ x)"
  | "p ∙ (EF x) = EF (p ∙ x)"

  instance
  proof
    fix x :: "('a,'b) L_state"
    show "0 ∙ x = x" by (cases x, simp_all)
  next
    fix p q and x :: "('a,'b) L_state"
    show "(p + q) ∙ x = p ∙ q ∙ x" by (cases x, simp_all)
  qed

end

declare permute_L_state.simps [eqvt]

lemma supp_AC [simp]: "supp (AC x) = supp x"
unfolding supp_def by simp

lemma supp_EF [simp]: "supp (EF x) = supp x"
unfolding supp_def by simp

instantiation L_state :: (fs,fs) fs
begin

  instance
  proof
    fix x :: "('a,'b) L_state"
    show "finite (supp x)"
      by (cases x) (simp add: finite_supp)+
  qed

end


subsection ‹Actions and binding names›

datatype ('act,'effect) L_action =
    Act 'act
  | Eff 'effect

instantiation L_action :: (pt,pt) pt
begin

  fun permute_L_action :: "perm ⇒ ('a,'b) L_action ⇒ ('a,'b) L_action" where
    "p ∙ (Act α) = Act (p ∙ α)"
  | "p ∙ (Eff f) = Eff (p ∙ f)"

  instance
  proof
    fix x :: "('a,'b) L_action"
    show "0 ∙ x = x" by (cases x, simp_all)
  next
    fix p q and x :: "('a,'b) L_action"
    show "(p + q) ∙ x = p ∙ q ∙ x" by (cases x, simp_all)
  qed

end

declare permute_L_action.simps [eqvt]

lemma supp_Act [simp]: "supp (Act α) = supp α"
unfolding supp_def by simp

lemma supp_Eff [simp]: "supp (Eff f) = supp f"
unfolding supp_def by simp

instantiation L_action :: (fs,fs) fs
begin

  instance
  proof
    fix x :: "('a,'b) L_action"
    show "finite (supp x)"
      by (cases x) (simp add: finite_supp)+
  qed

end

instantiation L_action :: (bn,fs) bn
begin

  fun bn_L_action :: "('a,'b) L_action ⇒ atom set" where
    "bn_L_action (Act α) = bn α"
  | "bn_L_action (Eff _) = {}"

  instance
  proof
    fix p and α :: "('a,'b) L_action"
    show "p ∙ bn α = bn (p ∙ α)"
      by (cases α) (simp add: bn_eqvt, simp)
  next
    fix α :: "('a,'b) L_action"
    show "finite (bn α)"
      by (cases α) (simp add: bn_finite, simp)
  qed

end


subsection ‹Satisfaction›

context effect_nominal_ts
begin

  fun L_satisfies :: "('state,'effect) L_state ⇒ 'pred ⇒ bool" (infix ‹⊢⇩L› 70) where
    "AC (_,_,P) ⊢⇩L φ ⟷ P ⊢ φ"
  | "EF _       ⊢⇩L φ ⟷ False"

  lemma L_satisfies_eqvt: assumes "P⇩L ⊢⇩L φ" shows "(p ∙ P⇩L) ⊢⇩L (p ∙ φ)"
  proof (cases P⇩L)
    case (AC fFP)
    with assms have "snd (snd fFP) ⊢ φ"
      by (metis L_satisfies.simps(1) prod.collapse)
    then have "snd (snd (p ∙ fFP)) ⊢ p ∙ φ"
      by (metis satisfies_eqvt snd_eqvt)
    then show ?thesis
      using AC by (metis L_satisfies.simps(1) permute_L_state.simps(1) prod.collapse)
  next
    case EF
    with assms have "False"
      by simp
    then show ?thesis ..
  qed

end


subsection ‹Transitions›

context effect_nominal_ts
begin

  fun L_transition :: "('state,'effect) L_state ⇒ (('act,'effect) L_action, ('state,'effect) L_state) residual ⇒ bool" (infix ‹→⇩L› 70) where
    "AC (f,F,P) →⇩L αP' ⟷ (∃α P'. P → ⟨α,P'⟩ ∧ αP' = ⟨Act α, EF (L (α,F,f), P')⟩ ∧ bn α ♯* (F,f))" ― ‹note the freshness condition›
  | "EF (F,P) →⇩L αP' ⟷ (∃f. f ∈⇩f⇩s F ∧ αP' = ⟨Eff f, AC (f, F, ⟨f⟩P)⟩)"

  lemma L_transition_eqvt: assumes "P⇩L →⇩L α⇩LP⇩L'" shows "(p ∙ P⇩L) →⇩L (p ∙ α⇩LP⇩L')"
  proof (cases P⇩L)
    case AC
    {
      fix f F P
      assume *: "P⇩L = AC (f,F,P)"
      with assms obtain α P' where trans: "P → ⟨α,P'⟩" and αP': "α⇩LP⇩L' = ⟨Act α, EF (L (α,F,f), P')⟩" and fresh: "bn α ♯* (F,f)"
        by auto
      from trans have "p ∙ P → ⟨p ∙ α, p ∙ P'⟩"
        by (simp add: transition_eqvt')
      moreover from αP' have "p ∙ α⇩LP⇩L' = ⟨Act (p ∙ α), EF (L (p ∙ α, p ∙ F, p ∙ f), p ∙ P')⟩"
        by (simp add: L_eqvt')
      moreover from fresh have "bn (p ∙ α) ♯* (p ∙ F, p ∙ f)"
        by (metis bn_eqvt fresh_star_Pair fresh_star_permute_iff)
      ultimately have "p ∙ P⇩L →⇩L p ∙ α⇩LP⇩L'"
        using "*" by auto
    }
    with AC show ?thesis
      by (metis prod.collapse)
  next
    case EF
    {
      fix F P
      assume *: "P⇩L = EF (F,P)"
      with assms obtain f where "f ∈⇩f⇩s F" and "α⇩LP⇩L' = ⟨Eff f, AC (f, F, ⟨f⟩P)⟩"
        by auto
      then have "(p ∙ f) ∈⇩f⇩s (p ∙ F)" and "p ∙ α⇩LP⇩L' = ⟨Eff (p ∙ f), AC (p ∙ f, p ∙ F, ⟨p ∙ f⟩(p ∙ P))⟩"
        by simp+
      then have "p ∙ P⇩L →⇩L p ∙ α⇩LP⇩L'"
        using "*" L_transition.simps(2) Pair_eqvt permute_L_state.simps(2) by force
    }
    with EF show ?thesis
      by (metis prod.collapse)
  qed

  text ‹The binding names in the alpha-variant that witnesses the $L$-transition may be chosen fresh
  for any finitely supported context.›

  lemma L_transition_AC_strong:
    assumes "finite (supp X)" and "AC (f,F,P) →⇩L ⟨α⇩L,P⇩L'⟩"
    shows "∃α P'. P → ⟨α,P'⟩ ∧ ⟨α⇩L,P⇩L'⟩ = ⟨Act α, EF (L (α,F,f), P')⟩ ∧ bn α ♯* X"
  using assms proof -
    from ‹AC (f,F,P) →⇩L ⟨α⇩L,P⇩L'⟩› obtain α P' where transition: "P → ⟨α,P'⟩" and alpha: "⟨α⇩L,P⇩L'⟩ = ⟨Act α, EF (L (α,F,f), P')⟩" and fresh: "bn α ♯* (F,f)"
      by (metis L_transition.simps(1))
    let ?Act = "Act α :: ('act,'effect) L_action" ― ‹the type annotation prevents a type that is too polymorphic and doesn't fix~@{typ 'effect}›
    have "finite (bn α)"
      by (fact bn_finite)
    moreover note ‹finite (supp X)›
    moreover have "finite (supp (⟨?Act, EF (L (α,F,f), P')⟩, ⟨α,P'⟩, F, f))"
      by (metis finite_Diff finite_UnI finite_supp supp_Pair supp_abs_residual_pair)
    moreover from fresh have "bn α ♯* (⟨?Act, EF (L (α,F,f), P')⟩, ⟨α,P'⟩, F, f)"
      by (auto simp add: fresh_star_def fresh_def supp_Pair supp_abs_residual_pair)
    ultimately obtain p where fresh_X: "(p ∙ bn α) ♯* X" and "supp (⟨?Act, EF (L (α,F,f), P')⟩, ⟨α,P'⟩, F, f) ♯* p"
      by (metis at_set_avoiding2)
    then have "supp ⟨?Act, EF (L (α,F,f), P')⟩ ♯* p" and "supp ⟨α,P'⟩ ♯* p" and "supp (F,f) ♯* p"
      by (metis fresh_star_Un supp_Pair)+
    then have "p ∙ ⟨?Act, EF (L (α,F,f), P')⟩ = ⟨?Act, EF (L (α,F,f), P')⟩" and "p ∙ ⟨α,P'⟩ = ⟨α,P'⟩" and "p ∙ (F,f) = (F,f)"
      by (metis supp_perm_eq)+
    then have "⟨Act (p ∙ α), EF (L (p ∙ α, F, f), p ∙ P')⟩ = ⟨?Act, EF (L (α,F,f), P')⟩" and "⟨p ∙ α, p ∙ P'⟩ = ⟨α,P'⟩"
      using permute_L_action.simps(1) permute_L_state.simps(2) abs_residual_pair_eqvt L_eqvt' Pair_eqvt by auto
    then show "∃α P'. P → ⟨α,P'⟩ ∧ ⟨α⇩L,P⇩L'⟩ = ⟨Act α, EF (L (α,F,f), P')⟩ ∧ bn α ♯* X"
      using transition and alpha and fresh_X by (metis bn_eqvt)
  qed

  (* bn α ♯* (F,f) is required for the ⟵ implication as well as for the ⟶ implication;
     additionally bn α ♯* P is required for the ⟶ implication. *)

  lemma L_transition_AC_fresh:
    assumes "bn α ♯* (F,f,P)"
    shows "AC (f,F,P) →⇩L ⟨Act α, P⇩L'⟩ ⟷ (∃P'. P⇩L' = EF (L (α,F,f), P') ∧ P → ⟨α,P'⟩)"
  proof
    assume "AC (f,F,P) →⇩L ⟨Act α, P⇩L'⟩"
    moreover have "finite (supp (F,f,P))"
      by (fact finite_supp)
    ultimately obtain α' P' where trans: "P → ⟨α',P'⟩" and eq: "⟨Act α :: ('act,'effect) L_action, P⇩L'⟩ = ⟨Act α', EF (L (α',F,f), P')⟩" and fresh: "bn α' ♯* (F,f,P)"
      using L_transition_AC_strong by blast
    from eq obtain p where p: "p ∙ (Act α :: ('act,'effect) L_action, P⇩L') = (Act α', EF (L (α',F,f), P'))" and supp_p: "supp p ⊆ bn (Act α :: ('act,'effect) L_action) ∪ p ∙ bn (Act α :: ('act,'effect) L_action)"
      using residual_eq_iff_perm_renaming by metis

    from p have p_α: "p ∙ α = α'" and p_P⇩L': "p ∙ P⇩L' = EF (L (α',F,f), P')"
      by simp_all

    from supp_p and p_α and assms and fresh have "supp p ♯* (F, f, P)"
      by (simp add: bn_eqvt fresh_star_def) blast
    then have p_F: "p ∙ F = F" and p_f: "p ∙ f = f" and p_P: "p ∙ P = P"
      by (simp_all add: fresh_star_Pair perm_supp_eq)

    from p_P⇩L' have "P⇩L' = -p ∙ EF (L (α',F,f), P')"
      by (metis permute_minus_cancel(2))
    then have "P⇩L' = EF (L (α,F,f), -p ∙ P')"
      using p_α p_F p_f by simp (metis (full_types) permute_minus_cancel(2))

    moreover from trans have "P → ⟨α, -p ∙ P'⟩"
      using p_P and p_α by (metis permute_minus_cancel(2) transition_eqvt')

    ultimately show "∃P'. P⇩L' = EF (L (α,F,f), P') ∧ P → ⟨α,P'⟩"
      by blast
  next
    assume "∃P'. P⇩L' = EF (L (α,F,f), P') ∧ P → ⟨α,P'⟩"
    moreover from assms have "bn α ♯* (F,f)"
      by (simp add: fresh_star_Pair)
    ultimately show "AC (f, F, P) →⇩L ⟨Act α, P⇩L'⟩"
      using L_transition.simps(1) by blast
  qed

end


subsection ‹Translation of \texorpdfstring{$F/L$}{F/L}-formulas into formulas without effects›

text ‹Since we defined formulas via a manual quotient construction, we also need to define the
$L$-transform via lifting from the underlying type of infinitely branching trees. As before, we
cannot use {\bf nominal\_function} because that generates proof obligations where, for formulas
of the form~@{term "Conj xset"}, the assumption that~@{term xset} has finite support is missing.›

text ‹The following auxiliary function returns trees (modulo $\alpha$-equivalence) rather than
formulas. This allows us to prove equivariance for \emph{all} argument trees, without an assumption
that they are (hereditarily) finitely supported. Further below--after this auxiliary function has
been lifted to $F/L$-formulas as arguments--we derive a version that returns formulas.›

primrec L_transform_Tree :: "('idx,'pred::fs,'act::bn,'eff::fs) Tree ⇒ ('idx, 'pred, ('act,'eff) L_action) Formula.Tree⇩α" where
  "L_transform_Tree (tConj tset) = Formula.Conj⇩α (map_bset L_transform_Tree tset)"
| "L_transform_Tree (tNot t) = Formula.Not⇩α (L_transform_Tree t)"
| "L_transform_Tree (tPred f φ) = Formula.Act⇩α (Eff f) (Formula.Pred⇩α φ)"
| "L_transform_Tree (tAct f α t) = Formula.Act⇩α (Eff f) (Formula.Act⇩α (Act α) (L_transform_Tree t))"

lemma L_transform_Tree_eqvt [eqvt]: "p ∙ L_transform_Tree t = L_transform_Tree (p ∙ t)"
proof (induct t)
  case (tConj tset)
  then show ?case
    by simp (metis (no_types, opaque_lifting) bset.map_cong0 map_bset_eqvt permute_fun_def permute_minus_cancel(1))
qed simp_all

text ‹@{const L_transform_Tree} respects $\alpha$-equivalence.›

lemma alpha_Tree_L_transform_Tree:
  assumes "alpha_Tree t1 t2"
  shows "L_transform_Tree t1 = L_transform_Tree t2"
using assms proof (induction t1 t2 rule: alpha_Tree_induct')
  case (alpha_tConj tset1 tset2)
  then have "rel_bset (=) (map_bset L_transform_Tree tset1) (map_bset L_transform_Tree tset2)"
    by (simp add: bset.rel_map(1) bset.rel_map(2) bset.rel_mono_strong)
  then show ?case
    by (simp add: bset.rel_eq)
next
  case (alpha_tAct f1 α1 t1 f2 α2 t2)
  from ‹alpha_Tree (FL_Formula.Tree.tAct f1 α1 t1) (FL_Formula.Tree.tAct f2 α2 t2)›
    obtain p where *: "(bn α1, t1) ≈set alpha_Tree (supp_rel alpha_Tree) p (bn α2, t2)"
      and **: "(bn α1, α1) ≈set (=) supp p (bn α2, α2)" and "f1 = f2"
    by auto
  from * have fresh: "(supp_rel alpha_Tree t1 - bn α1) ♯* p" and alpha: "alpha_Tree (p ∙ t1) t2" and eq: "p ∙ bn α1 = bn α2"
    by (auto simp add: alpha_set)
  from alpha_tAct.IH(2) have "supp_rel Formula.alpha_Tree (Formula.rep_Tree⇩α (L_transform_Tree t1)) ⊆ supp_rel alpha_Tree t1"
    by (metis (no_types, lifting) infinite_mono Formula.alpha_Tree_permute_rep_commute L_transform_Tree_eqvt mem_Collect_eq subsetI supp_rel_def)
  with fresh have fresh': "(supp_rel Formula.alpha_Tree (Formula.rep_Tree⇩α (L_transform_Tree t1)) - bn α1) ♯* p"
    by (meson DiffD1 DiffD2 DiffI fresh_star_def subsetCE)
  moreover from alpha have alpha': "Formula.alpha_Tree (p ∙ Formula.rep_Tree⇩α (L_transform_Tree t1)) (Formula.rep_Tree⇩α (L_transform_Tree t2))"
    using alpha_tAct.IH(1) by (metis Formula.alpha_Tree_permute_rep_commute L_transform_Tree_eqvt)
  moreover from fresh' alpha' eq have "supp_rel Formula.alpha_Tree (Formula.rep_Tree⇩α (L_transform_Tree t1)) - bn α1 = supp_rel Formula.alpha_Tree (Formula.rep_Tree⇩α (L_transform_Tree t2)) - bn α2"
    by (metis (mono_tags) Diff_eqvt Formula.alpha_Tree_eqvt' Formula.alpha_Tree_eqvt_aux Formula.alpha_Tree_supp_rel atom_set_perm_eq)
  ultimately have "(bn α1, Formula.rep_Tree⇩α (L_transform_Tree t1)) ≈set Formula.alpha_Tree (supp_rel Formula.alpha_Tree) p (bn α2, Formula.rep_Tree⇩α (L_transform_Tree t2))"
    using eq by (simp add: alpha_set)
  moreover from ** have "(bn α1, Act α1) ≈set (=) supp p (bn α2, Act α2)"
    by (metis (mono_tags, lifting) L_Transform.supp_Act alpha_set permute_L_action.simps(1))
  ultimately have "Formula.Act⇩α (Act α1) (L_transform_Tree t1) = Formula.Act⇩α (Act α2) (L_transform_Tree t2)"
    by (auto simp add: Formula.Act⇩α_eq_iff)
  with ‹f1 = f2› show ?case
    by simp
qed simp_all

text ‹$L$-transform for trees modulo $\alpha$-equivalence.›

lift_definition L_transform_Tree⇩α :: "('idx,'pred::fs,'act::bn,'eff::fs) Tree⇩α ⇒ ('idx, 'pred, ('act,'eff) L_action) Formula.Tree⇩α" is
    L_transform_Tree
  by (fact alpha_Tree_L_transform_Tree)

lemma L_transform_Tree⇩α_eqvt [eqvt]: "p ∙ L_transform_Tree⇩α t⇩α = L_transform_Tree⇩α (p ∙ t⇩α)"
  by transfer (simp)

lemma L_transform_Tree⇩α_Conj⇩α [simp]: "L_transform_Tree⇩α (Conj⇩α tset⇩α) = Formula.Conj⇩α (map_bset L_transform_Tree⇩α tset⇩α)"
  by (simp add: Conj⇩α_def' L_transform_Tree⇩α.abs_eq) (metis (no_types, lifting) L_transform_Tree⇩α.rep_eq bset.map_comp bset.map_cong0 comp_apply)

lemma L_transform_Tree⇩α_Not⇩α [simp]: "L_transform_Tree⇩α (Not⇩α t⇩α) = Formula.Not⇩α (L_transform_Tree⇩α t⇩α)"
  by transfer simp

lemma L_transform_Tree⇩α_Pred⇩α [simp]: "L_transform_Tree⇩α (Pred⇩α f φ) = Formula.Act⇩α (Eff f) (Formula.Pred⇩α φ)"
  by transfer simp

lemma L_transform_Tree⇩α_Act⇩α [simp]: "L_transform_Tree⇩α (Act⇩α f α t⇩α) = Formula.Act⇩α (Eff f) (Formula.Act⇩α (Act α) (L_transform_Tree⇩α t⇩α))"
  by transfer simp

lemma finite_supp_map_bset_L_transform_Tree⇩α [simp]:
  assumes "finite (supp tset⇩α)"
  shows "finite (supp (map_bset L_transform_Tree⇩α tset⇩α))"
proof -
  have "eqvt map_bset" and "eqvt L_transform_Tree⇩α"
    by (simp add: eqvtI)+
  then have "supp (map_bset L_transform_Tree⇩α) = {}"
    using supp_fun_eqvt supp_fun_app_eqvt by blast
  then have "supp (map_bset L_transform_Tree⇩α tset⇩α) ⊆ supp tset⇩α"
    using supp_fun_app by blast
  with assms show "finite (supp (map_bset L_transform_Tree⇩α tset⇩α))"
    by (metis finite_subset)
qed

lemma L_transform_Tree⇩α_preserves_hereditarily_fs:
  assumes "hereditarily_fs t⇩α"
  shows "Formula.hereditarily_fs (L_transform_Tree⇩α t⇩α)"
using assms proof (induct rule: hereditarily_fs.induct)
  case (Conj⇩α tset⇩α)
  then show ?case
    by (auto intro!: Formula.hereditarily_fs.Conj⇩α) (metis imageE map_bset.rep_eq)
next
  case (Not⇩α t⇩α)
  then show ?case
    by (simp add: Formula.hereditarily_fs.Not⇩α)
next
  case (Pred⇩α f φ)
  then show ?case
    by (simp add: Formula.hereditarily_fs.Act⇩α Formula.hereditarily_fs.Pred⇩α)
next
  case (Act⇩α t⇩α f α)
  then show ?case
    by (simp add: Formula.hereditarily_fs.Act⇩α)
qed

text ‹$L$-transform for $F/L$-formulas.›

lift_definition L_transform_formula :: "('idx,'pred::fs,'act::bn,'eff::fs) formula ⇒ ('idx, 'pred, ('act,'eff) L_action) Formula.Tree⇩α" is
    L_transform_Tree⇩α
  .

lemma L_transform_formula_eqvt [eqvt]: "p ∙ L_transform_formula x = L_transform_formula (p ∙ x)"
  by transfer (simp)

lemma L_transform_formula_Conj [simp]:
  assumes "finite (supp xset)"
  shows "L_transform_formula (Conj xset) = Formula.Conj⇩α (map_bset L_transform_formula xset)"
  using assms by (simp add: Conj_def L_transform_formula_def bset.map_comp map_fun_def)

lemma L_transform_formula_Not [simp]: "L_transform_formula (Not x) = Formula.Not⇩α (L_transform_formula x)"
  by transfer simp

lemma L_transform_formula_Pred [simp]: "L_transform_formula (Pred f φ) = Formula.Act⇩α (Eff f) (Formula.Pred⇩α φ)"
  by transfer simp

lemma L_transform_formula_Act [simp]: "L_transform_formula (FL_Formula.Act f α x) = Formula.Act⇩α (Eff f) (Formula.Act⇩α (Act α) (L_transform_formula x))"
  by transfer simp

lemma L_transform_formula_hereditarily_fs [simp]: "Formula.hereditarily_fs (L_transform_formula x)"
  by transfer (fact L_transform_Tree⇩α_preserves_hereditarily_fs)

text ‹Finally, we define the proper $L$-transform, which returns formulas instead of trees.›

definition L_transform :: "('idx,'pred::fs,'act::bn,'eff::fs) formula ⇒ ('idx, 'pred, ('act,'eff) L_action) Formula.formula" where
  "L_transform x = Formula.Abs_formula (L_transform_formula x)"

lemma L_transform_eqvt [eqvt]: "p ∙ L_transform x = L_transform (p ∙ x)"
  unfolding L_transform_def by simp

lemma finite_supp_map_bset_L_transform [simp]:
  assumes "finite (supp xset)"
  shows "finite (supp (map_bset L_transform xset))"
proof -
  have "eqvt map_bset" and "eqvt L_transform"
    by (simp add: eqvtI)+
  then have "supp (map_bset L_transform) = {}"
    using supp_fun_eqvt supp_fun_app_eqvt by blast
  then have "supp (map_bset L_transform xset) ⊆ supp xset"
    using supp_fun_app by blast
  with assms show "finite (supp (map_bset L_transform xset))"
    by (metis finite_subset)
qed

lemma L_transform_Conj [simp]:
  assumes "finite (supp xset)"
  shows "L_transform (Conj xset) = Formula.Conj (map_bset L_transform xset)"
  using assms unfolding L_transform_def by (simp add: Formula.Conj_def bset.map_comp o_def)

lemma L_transform_Not [simp]: "L_transform (Not x) = Formula.Not (L_transform x)"
  unfolding L_transform_def by (simp add: Formula.Not_def)

lemma L_transform_Pred [simp]: "L_transform (Pred f φ) = Formula.Act (Eff f) (Formula.Pred φ)"
  unfolding L_transform_def by (simp add: Formula.Act_def Formula.Pred_def Formula.hereditarily_fs.Pred⇩α)

lemma L_transform_Act [simp]: "L_transform (FL_Formula.Act f α x) = Formula.Act (Eff f) (Formula.Act (Act α) (L_transform x))"
  unfolding L_transform_def by (simp add: Formula.Act_def Formula.hereditarily_fs.Act⇩α)

context effect_nominal_ts
begin

  interpretation L_transform: nominal_ts "(⊢⇩L)" "(→⇩L)"
  by unfold_locales (fact L_satisfies_eqvt, fact L_transition_eqvt)

  text ‹The $L$-transform preserves satisfaction of formulas in the following sense:›

  theorem FL_valid_iff_valid_L_transform:
    assumes "(x::('idx,'pred,'act,'effect) formula) ∈ 𝒜[F]"
    shows "FL_valid P x ⟷ L_transform.valid (EF (F, P)) (L_transform x)"
  using assms proof (induct x arbitrary: P)
    case (Conj xset F)
    then show ?case
      by auto (metis imageE map_bset.rep_eq, simp add: map_bset.rep_eq)
  next
    case (Not F x)
    then show ?case by simp
  next
    case (Pred f F φ)
    let ?φ = "Formula.Pred φ :: ('idx, 'pred, ('act,'effect) L_action) Formula.formula"
    show ?case
    proof
      assume "FL_valid P (Pred f φ)"
      then have "L_transform.valid (AC (f, F, ⟨f⟩P)) ?φ"
        by (simp add: L_transform.valid_Act)
      moreover from ‹f ∈⇩f⇩s F› have "EF (F, P) →⇩L ⟨Eff f, AC (f, F, ⟨f⟩P)⟩"
        by (metis L_transition.simps(2))
      ultimately show "L_transform.valid (EF (F, P)) (L_transform (Pred f φ))"
        using L_transform.valid_Act by fastforce
    next
      assume "L_transform.valid (EF (F, P)) (L_transform (Pred f φ))"
      then obtain P' where trans: "EF (F, P) →⇩L ⟨Eff f, P'⟩" and valid: "L_transform.valid P' ?φ"
        by simp (metis bn_L_action.simps(2) empty_iff fresh_star_def L_transform.valid_Act_fresh L_transform.valid_Pred L_transition.simps(2))
      from trans have "P' = AC (f, F, ⟨f⟩P)"
        by (simp add: residual_empty_bn_eq_iff)
      with valid show "FL_valid P (Pred f φ)"
        by simp
    qed
  next
    case (Act f F α x)
    show ?case
    proof
      assume "FL_valid P (FL_Formula.Act f α x)"
      then obtain α' x' P' where eq: "FL_Formula.Act f α x = FL_Formula.Act f α' x'" and trans: "⟨f⟩P → ⟨α',P'⟩" and valid: "FL_valid P' x'" and fresh: "bn α' ♯* (F, f)"
        by (metis FL_valid_Act_strong finite_supp)
      from eq obtain p where p_x: "p ∙ x = x'" and p_α: "p ∙ α = α'" and supp_p: "supp p ⊆ bn α ∪ bn α'"
        by (metis bn_eqvt FL_Formula.Act_eq_iff_perm_renaming)
      from ‹bn α ♯* (F, f)› and fresh have "supp (F, f) ♯* p"
        using supp_p by (auto simp add: fresh_star_Pair fresh_star_def supp_Pair fresh_def)
      then have "p ∙ F = F" and "p ∙ f = f"
        using supp_perm_eq by fastforce+

      from valid have "FL_valid (-p ∙ P') x"
        using p_x by (metis FL_valid_eqvt permute_minus_cancel(2))
      then have "L_transform.valid (EF (L (α, F, f), -p ∙ P')) (L_transform x)"
        using Act.hyps(4) by metis
      then have "L_transform.valid (p ∙ EF (L (α, F, f), -p ∙ P')) (p ∙ L_transform x)"
        by (fact L_transform.valid_eqvt)
      then have "L_transform.valid (EF (L (α', F, f), P')) (L_transform x')"
        using p_x and p_α and ‹p ∙ F = F› and ‹p ∙ f = f› by simp

      then have "L_transform.valid (AC (f, F, ⟨f⟩P)) (Formula.Act (Act α') (L_transform x'))"
        using trans fresh L_transform.valid_Act by fastforce
      with ‹f ∈⇩f⇩s F› and eq show "L_transform.valid (EF (F, P)) (L_transform (FL_Formula.Act f α x))"
        using L_transform.valid_Act by fastforce
    next
      assume *: "L_transform.valid (EF (F, P)) (L_transform (FL_Formula.Act f α x))"

      ― ‹rename~@{term "bn α"} to avoid~@{term "(F, f, P)"}, without touching~@{term F} or~@{term "FL_Formula.Act f α x"}›
      obtain p where 1: "(p ∙ bn α) ♯* (F, f, P)" and 2: "supp (F, FL_Formula.Act f α x) ♯* p"
      proof (rule at_set_avoiding2[of "bn α" "(F, f, P)" "(F, FL_Formula.Act f α x)", THEN exE])
        show "finite (bn α)" by (fact bn_finite)
      next
        show "finite (supp (F, f, P))" by (fact finite_supp)
      next
        show "finite (supp (F, FL_Formula.Act f α x))" by (simp add: finite_supp)
      next
        from ‹bn α ♯* (F, f)› show "bn α ♯* (F, FL_Formula.Act f α x)"
          by (simp add: fresh_star_Pair fresh_star_def fresh_def supp_Pair)
      qed metis
      from 2 have "supp F ♯* p" and Act_fresh: "supp (FL_Formula.Act f α x) ♯* p"
        by (simp add: fresh_star_Pair fresh_star_def supp_Pair)+
      from ‹supp F ♯* p› have "p ∙ F = F"
        by (metis supp_perm_eq)
      from Act_fresh have "p ∙ f = f"
        using fresh_star_Un supp_perm_eq by fastforce
      from Act_fresh have eq: "FL_Formula.Act f α x = FL_Formula.Act f (p ∙ α) (p ∙ x)"
        by (metis FL_Formula.Act_eq_iff_perm FL_Formula.Act_eqvt supp_perm_eq)

      with * obtain P' where trans: "EF (F, P) →⇩L ⟨Eff f,P'⟩" and valid: "L_transform.valid P' (Formula.Act (Act (p ∙ α)) (L_transform (p ∙ x)))"
        using L_transform_Act by (metis L_transform.valid_Act_fresh bn_L_action.simps(2) empty_iff fresh_star_def)
      from trans have P': "P' = AC (f, F, ⟨f⟩P)"
        by (simp add: residual_empty_bn_eq_iff)

      have supp_f_P: "supp (⟨f⟩P) ⊆ supp f ∪ supp P"
        using effect_apply_eqvt supp_fun_app supp_fun_app_eqvt by fastforce
      with 1 have "bn (Act (p ∙ α)) ♯* AC (f, F, ⟨f⟩P)"
        by (auto simp add: bn_eqvt fresh_star_def fresh_def supp_Pair)
      with valid obtain P'' where trans': "AC (f, F, ⟨f⟩P) →⇩L ⟨Act (p ∙ α),P''⟩" and valid': "L_transform.valid P'' (L_transform (p ∙ x))"
        using P' by (metis L_transform.valid_Act_fresh)

      from supp_f_P and 1 have "bn (p ∙ α) ♯* (F, f, ⟨f⟩P)"
        by (auto simp add: bn_eqvt fresh_star_def fresh_def supp_Pair)
      with trans' obtain P' where P'': "P'' = EF (L (p ∙ α, F, f), P')" and trans'': "⟨f⟩P → ⟨p ∙ α,P'⟩"
        by (metis L_transition_AC_fresh)

      from valid' have "L_transform.valid (-p ∙ P'') (L_transform x)"
        by (metis (mono_tags) L_transform.valid_eqvt L_transform_eqvt permute_minus_cancel(2))
      with P'' ‹p ∙ F = F› ‹p ∙ f = f› have "L_transform.valid (EF (L (α, F, f), - p ∙ P')) (L_transform x)"
        by simp (metis pemute_minus_self permute_minus_cancel(1))
      then have "FL_valid P' (p ∙ x)"
        using Act.hyps(4) by (metis FL_valid_eqvt permute_minus_cancel(1))

      with trans'' and eq show "FL_valid P (FL_Formula.Act f α x)"
        by (metis FL_valid_Act)
    qed
  qed

end


subsection ‹Bisimilarity in the \texorpdfstring{$L$}{L}-transform›

context effect_nominal_ts
begin

  (* Not quite sure why this is needed again? *)
  interpretation L_transform: nominal_ts "(⊢⇩L)" "(→⇩L)"
  by unfold_locales (fact L_satisfies_eqvt, fact L_transition_eqvt)

  notation L_transform.bisimilar (infix ‹∼⋅⇩L› 100)

  text ‹$F/L$-bisimilarity is equivalent to bisimilarity in the $L$-transform.›

  inductive L_bisimilar :: "('state,'effect) L_state ⇒ ('state,'effect) L_state ⇒ bool" where
    "P ∼⋅[F] Q ⟹ L_bisimilar (EF (F,P)) (EF (F,Q))"
  | "P ∼⋅[F] Q ⟹ f ∈⇩f⇩s F ⟹ L_bisimilar (AC (f, F, ⟨f⟩P)) (AC (f, F, ⟨f⟩Q))"

  lemma L_bisimilar_is_L_transform_bisimulation: "L_transform.is_bisimulation L_bisimilar"
  unfolding L_transform.is_bisimulation_def
  proof
    show "symp L_bisimilar"
      by (metis FL_bisimilar_symp L_bisimilar.cases L_bisimilar.intros symp_def)
  next
    have "∀P⇩L Q⇩L. L_bisimilar P⇩L Q⇩L ⟶ (∀φ. P⇩L ⊢⇩L φ ⟶ Q⇩L ⊢⇩L φ)" (is ?S)
      using FL_bisimilar_is_L_bisimulation L_bisimilar.simps is_L_bisimulation_def by auto
    moreover have "∀P⇩L Q⇩L. L_bisimilar P⇩L Q⇩L ⟶ (∀α⇩L P⇩L'. bn α⇩L ♯* Q⇩L ⟶ P⇩L →⇩L ⟨α⇩L,P⇩L'⟩ ⟶ (∃Q⇩L'. Q⇩L →⇩L ⟨α⇩L,Q⇩L'⟩ ∧ L_bisimilar P⇩L' Q⇩L'))" (is ?T)
      proof (clarify)
        fix P⇩L Q⇩L α⇩L P⇩L'
        assume L_bisim: "L_bisimilar P⇩L Q⇩L" and fresh⇩L: "bn α⇩L ♯* Q⇩L" and trans⇩L: "P⇩L →⇩L ⟨α⇩L,P⇩L'⟩"
        obtain Q⇩L' where "Q⇩L →⇩L ⟨α⇩L,Q⇩L'⟩" and "L_bisimilar P⇩L' Q⇩L'"
          using L_bisim proof (rule L_bisimilar.cases)
            fix P F Q
            assume P⇩L: "P⇩L = EF (F, P)" and Q⇩L: "Q⇩L = EF (F, Q)" and bisim: "P ∼⋅[F] Q"
            from P⇩L and trans⇩L obtain f where effect: "f ∈⇩f⇩s F" and α⇩LP⇩L': "⟨α⇩L,P⇩L'⟩ = ⟨Eff f, AC (f, F, ⟨f⟩P)⟩"
              using L_transition.simps(2) by blast
            from Q⇩L and effect have "Q⇩L →⇩L ⟨Eff f, AC (f, F, ⟨f⟩Q)⟩"
              using L_transition.simps(2) by blast
            moreover from bisim and effect have "L_bisimilar (AC (f, F, ⟨f⟩P)) (AC (f, F, ⟨f⟩Q))"
              using L_bisimilar.intros(2) by blast
            moreover from α⇩LP⇩L' have "α⇩L = Eff f" and "P⇩L' = AC (f, F, ⟨f⟩P)"
              by (metis bn_L_action.simps(2) residual_empty_bn_eq_iff)+
            ultimately show "thesis"
              using ‹⋀Q⇩L'. Q⇩L →⇩L ⟨α⇩L,Q⇩L'⟩ ⟹ L_bisimilar P⇩L' Q⇩L' ⟹ thesis› by blast
          next
            fix P F Q f
            assume P⇩L: "P⇩L = AC (f, F, ⟨f⟩P)" and Q⇩L: "Q⇩L = AC (f, F, ⟨f⟩Q)" and bisim: "P ∼⋅[F] Q" and effect: "f ∈⇩f⇩s F"
            have "finite (supp (⟨f⟩Q, F, f))"
              by (fact finite_supp)
            with P⇩L and trans⇩L obtain α P' where trans_P: "⟨f⟩P → ⟨α,P'⟩" and α⇩LP⇩L': "⟨α⇩L,P⇩L'⟩ = ⟨Act α, EF (L (α,F,f), P')⟩" and fresh: "bn α ♯* (⟨f⟩Q, F, f)"
              by (metis L_transition_AC_strong)
            from bisim and effect and fresh and trans_P obtain Q' where trans_Q: "⟨f⟩Q → ⟨α,Q'⟩" and bisim': "P' ∼⋅[L (α,F,f)] Q'"
              by (metis FL_bisimilar_simulation_step)
            from fresh have "bn α ♯* (F, f)"
              by (meson fresh_PairD(2) fresh_star_def)
            with Q⇩L and trans_Q have trans_Q⇩L: "Q⇩L →⇩L ⟨Act α, EF (L (α,F,f), Q')⟩"
              by (metis L_transition.simps(1))

            from α⇩LP⇩L' obtain p where p: "(α⇩L,P⇩L') = p ∙ (Act α, EF (L (α,F,f), P'))" and supp_p: "supp p ⊆ bn α ∪ bn α⇩L"
              by (metis (no_types, lifting) bn_L_action.simps(1) residual_eq_iff_perm_renaming)
            from supp_p and fresh and fresh⇩L and Q⇩L have "supp p ♯* (⟨f⟩Q, F, f)"
              unfolding fresh_star_def by (metis (no_types, opaque_lifting) Un_iff fresh_Pair fresh_def subsetCE supp_AC)
            then have p_fQ: "p ∙ ⟨f⟩Q = ⟨f⟩Q" and p_Ff: "p ∙ (F,f) = (F,f)"
              by (simp add: fresh_star_def perm_supp_eq)+
            from p and p_Ff have "α⇩L = Act (p ∙ α)" and "P⇩L' = EF (L (p ∙ α, F, f), p ∙ P')"
              by auto

            moreover from Q⇩L and p_fQ and p_Ff have "p ∙ Q⇩L = Q⇩L"
              by simp
            with trans_Q⇩L have "Q⇩L →⇩L p ∙ ⟨Act α, EF (L (α,F,f), Q')⟩"
              by (metis L_transform.transition_eqvt)
            then have "Q⇩L →⇩L ⟨Act (p ∙ α), EF (L (p ∙ α, F, f), p ∙ Q')⟩"
              using p_Ff by simp

            moreover from p_Ff have "p ∙ F = F" and "p ∙ f = f"
              by simp+
            with bisim' have "(p ∙ P') ∼⋅[L (p ∙ α, F, f)] (p ∙ Q')"
              by (metis FL_bisimilar_eqvt L_eqvt')
            then have "L_bisimilar (EF (L (p ∙ α, F, f), p ∙ P')) (EF (L (p ∙ α, F, f), p ∙ Q'))"
              by (metis L_bisimilar.intros(1))

            ultimately show thesis
                using ‹⋀Q⇩L'. Q⇩L →⇩L ⟨α⇩L,Q⇩L'⟩ ⟹ L_bisimilar P⇩L' Q⇩L' ⟹ thesis› by blast
          qed
        then show "∃Q⇩L'. Q⇩L →⇩L ⟨α⇩L,Q⇩L'⟩ ∧ L_bisimilar P⇩L' Q⇩L'"
          by auto
      qed
    ultimately show "?S ∧ ?T"
      by metis
  qed

  definition invL_FL_bisimilar :: "'effect first ⇒ 'state ⇒ 'state ⇒ bool" where
    "invL_FL_bisimilar F P Q ≡ EF (F,P) ∼⋅⇩L EF(F,Q)"

  lemma invL_FL_bisimilar_is_L_bisimulation: "is_L_bisimulation invL_FL_bisimilar"
  unfolding is_L_bisimulation_def
  proof
    fix F
    have "symp (invL_FL_bisimilar F)" (is ?R)
      by (metis L_transform.bisimilar_symp invL_FL_bisimilar_def symp_def)
    moreover have "∀P Q. invL_FL_bisimilar F P Q ⟶ (∀f. f ∈⇩f⇩s F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))" (is ?S)
      proof (clarify)
        fix P Q f φ
        assume bisim: "invL_FL_bisimilar F P Q" and effect: "f ∈⇩f⇩s F" and satisfies: "⟨f⟩P ⊢ φ"
        from bisim have "EF (F,P) ∼⋅⇩L EF (F,Q)"
          by (metis invL_FL_bisimilar_def)
        moreover have "bn (Eff f) ♯* EF (F,Q)"
          by (simp add: fresh_star_def)
        moreover from effect have "EF (F,P) →⇩L ⟨Eff f, AC (f, F, ⟨f⟩P)⟩"
          by (metis L_transition.simps(2))
        ultimately obtain Q⇩L' where trans: "EF (F,Q) →⇩L ⟨Eff f, Q⇩L'⟩" and L_bisim: "AC (f, F, ⟨f⟩P) ∼⋅⇩L Q⇩L'"
          by (metis L_transform.bisimilar_simulation_step)
        from trans obtain f' where "⟨Eff f :: ('act,'effect) L_action, Q⇩L'⟩ = ⟨Eff f', AC (f', F, ⟨f'⟩Q)⟩"
          by (metis L_transition.simps(2))
        then have Q⇩L': "Q⇩L' = AC (f, F, ⟨f⟩Q)"
          by (metis L_action.inject(2) bn_L_action.simps(2) residual_empty_bn_eq_iff)

        from satisfies have "AC (f, F, ⟨f⟩P) ⊢⇩L φ"
          by (metis L_satisfies.simps(1))
        with L_bisim and Q⇩L' have "AC (f, F, ⟨f⟩Q) ⊢⇩L φ"
          by (metis L_transform.bisimilar_is_bisimulation L_transform.is_bisimulation_def)
        then show "⟨f⟩Q ⊢ φ"
          by (metis L_satisfies.simps(1))
      qed
    moreover have "∀P Q. invL_FL_bisimilar F P Q ⟶ (∀f. f ∈⇩f⇩s F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶
        ⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ invL_FL_bisimilar (L (α, F, f)) P' Q')))" (is ?T)
      proof (clarify)
        fix P Q f α P'
        assume bisim: "invL_FL_bisimilar F P Q" and effect: "f ∈⇩f⇩s F" and fresh: "bn α ♯* (⟨f⟩Q, F, f)" and trans: "⟨f⟩P → ⟨α,P'⟩"
        from bisim have "EF (F,P) ∼⋅⇩L EF (F,Q)"
          by (metis invL_FL_bisimilar_def)
        moreover have "bn (Eff f) ♯* EF (F,Q)"
          by (simp add: fresh_star_def)
        moreover from effect have "EF (F,P) →⇩L ⟨Eff f, AC (f, F, ⟨f⟩P)⟩"
          by (metis L_transition.simps(2))
        ultimately obtain Q⇩L' where trans⇩L: "EF (F,Q) →⇩L ⟨Eff f, Q⇩L'⟩" and L_bisim: "AC (f, F, ⟨f⟩P) ∼⋅⇩L Q⇩L'"
          by (metis L_transform.bisimilar_simulation_step)
        from trans⇩L obtain f' where "⟨Eff f :: ('act,'effect) L_action, Q⇩L'⟩ = ⟨Eff f', AC (f', F, ⟨f'⟩Q)⟩"
          by (metis L_transition.simps(2))
        then have Q⇩L': "Q⇩L' = AC (f, F, ⟨f⟩Q)"
          by (metis L_action.inject(2) bn_L_action.simps(2) residual_empty_bn_eq_iff)

        from L_bisim and Q⇩L' have "AC (f, F, ⟨f⟩P) ∼⋅⇩L AC (f, F, ⟨f⟩Q)"
          by metis
        moreover from fresh have "bn (Act α) ♯* AC (f, F, ⟨f⟩Q)"
          by (simp add: fresh_def fresh_star_def supp_Pair)
        moreover from fresh have "bn α ♯* (F, f)"
          by (simp add: fresh_star_Pair)
        with trans have "AC (f, F, ⟨f⟩P) →⇩L ⟨Act α, EF (L (α,F,f), P')⟩"
          by (metis L_transition.simps(1))
        ultimately obtain Q⇩L'' where trans⇩L': "AC (f, F, ⟨f⟩Q) →⇩L ⟨Act α, Q⇩L''⟩" and L_bisim': "EF (L (α,F,f), P') ∼⋅⇩L Q⇩L''"
          by (metis L_transform.bisimilar_simulation_step)

        have "finite (supp (⟨f⟩Q, F, f))"
          by (fact finite_supp)
        with trans⇩L' obtain α' Q' where trans': "⟨f⟩Q → ⟨α',Q'⟩" and alpha: "⟨Act α :: ('act,'effect) L_action, Q⇩L''⟩ = ⟨Act α', EF (L (α',F,f), Q')⟩" and fresh': "bn α' ♯* (⟨f⟩Q, F,f)"
          by (metis L_transition_AC_strong)

        from alpha obtain p where p: "(Act α :: ('act,'effect) L_action, Q⇩L'') = p ∙ (Act α', EF (L (α',F,f), Q'))" and supp_p: "supp p ⊆ bn α ∪ bn α'"
          by (metis Un_commute bn_L_action.simps(1) residual_eq_iff_perm_renaming)
        from supp_p and fresh and fresh' have "supp p ♯* (⟨f⟩Q, F,f)"
          unfolding fresh_star_def by (metis (no_types, opaque_lifting) Un_iff subsetCE)
        then have p_fQ: "p ∙ ⟨f⟩Q = ⟨f⟩Q" and p_F: "p ∙ F = F" and p_f: "p ∙ f = f"
          by (simp add: fresh_star_def perm_supp_eq)+
        from p and p_F and p_f have p_α': "p ∙ α' = α" and Q⇩L'': "Q⇩L'' = EF (L (p ∙ α', F, f), p ∙ Q')"
          by auto

        from trans' and p_fQ and p_α' have "⟨f⟩Q → ⟨α, p ∙ Q'⟩"
          by (metis transition_eqvt')
        moreover from L_bisim' and Q⇩L'' and p_α' have "invL_FL_bisimilar (L (α,F,f)) P' (p ∙ Q')"
          by (metis invL_FL_bisimilar_def)
        ultimately show "∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ invL_FL_bisimilar (L (α,F,f)) P' Q'"
          by metis
      qed
    ultimately show "?R ∧ ?S ∧ ?T"
      by metis
  qed

  theorem "P ∼⋅[F] Q ⟷ EF (F,P) ∼⋅⇩L EF(F,Q)"
  proof
    assume "P ∼⋅[F] Q"
    then have "L_bisimilar (EF (F,P)) (EF (F,Q))"
        by (metis L_bisimilar.intros(1))
    then show "EF (F,P) ∼⋅⇩L EF(F,Q)"
      by (metis L_bisimilar_is_L_transform_bisimulation L_transform.bisimilar_def)
  next
    assume "EF (F, P) ∼⋅⇩L EF (F, Q)"
    then have "invL_FL_bisimilar F P Q"
      by (metis invL_FL_bisimilar_def)
    then show "P ∼⋅[F] Q"
      by (metis invL_FL_bisimilar_is_L_bisimulation FL_bisimilar_def)
  qed

end

text ‹The following (alternative) proof of the ``$\leftarrow$'' direction of this equivalence,
namely that bisimilarity in the $L$-transform implies $F/L$-bisimilarity, uses the fact that the
$L$-transform preserves satisfaction of formulas, together with the fact that bisimilarity (in the
$L$-transform) implies logical equivalence. However, since we proved the latter in the context of
indexed nominal transition systems, this proof requires an indexed nominal transition system with
effects where, additionally, the cardinality of the state set of the $L$-transform is bounded. We
could re-organize our formalization to remove this assumption: the proof of
@{thm indexed_nominal_ts.bisimilarity_implies_equivalence} does not actually make use of the
cardinality assumptions provided by indexed nominal transition systems.›

locale L_transform_indexed_effect_nominal_ts = indexed_effect_nominal_ts L satisfies transition effect_apply
  for L :: "('act::bn) × ('effect::fs) fs_set × 'effect ⇒ 'effect fs_set" 
  and satisfies :: "'state::fs ⇒ 'pred::fs ⇒ bool" (infix ‹⊢› 70)
  and transition :: "'state ⇒ ('act,'state) residual ⇒ bool" (infix ‹→› 70)
  and effect_apply :: "'effect ⇒ 'state ⇒ 'state" (‹⟨_⟩_› [0,101] 100) +
  assumes card_idx_L_transform_state: "|UNIV::('state, 'effect) L_state set| <o |UNIV::'idx set|"
begin

  interpretation L_transform: indexed_nominal_ts "(⊢⇩L)" "(→⇩L)"
    by unfold_locales (fact L_satisfies_eqvt, fact L_transition_eqvt, fact card_idx_perm, fact card_idx_L_transform_state)

  notation L_transform.bisimilar (infix ‹∼⋅⇩L› 100)

  theorem "EF (F,P) ∼⋅⇩L EF(F,Q) ⟶ P ∼⋅[F] Q"
  proof
    assume "EF (F, P) ∼⋅⇩L EF (F, Q)"
    then have "L_transform.logically_equivalent (EF (F, P)) (EF (F, Q))"
      by (fact L_transform.bisimilarity_implies_equivalence)
    with FL_valid_iff_valid_L_transform have "FL_logically_equivalent F P Q"
      using FL_logically_equivalent_def L_transform.logically_equivalent_def by blast
    then show "P ∼⋅[F] Q"
      by (fact FL_equivalence_implies_bisimilarity)
  qed

end

end