Theory S_Transform

theory S_Transform
imports
  Bisimilarity_Implies_Equivalence
  Equivalence_Implies_Bisimilarity
  Weak_Bisimilarity_Implies_Equivalence
  Weak_Equivalence_Implies_Bisimilarity
  Weak_Expressive_Completeness
begin

section ‹\texorpdfstring{$S$}{S}-Transform: State Predicates as Actions›

subsection ‹Actions and binding names›

datatype ('act,'pred) S_action =
    Act 'act
  | Pred 'pred

instantiation S_action :: (pt,pt) pt
begin

  fun permute_S_action :: "perm ⇒ ('a,'b) S_action ⇒ ('a,'b) S_action" where
    "p ∙ (Act α) = Act (p ∙ α)"
  | "p ∙ (Pred φ) = Pred (p ∙ φ)"

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

end

declare permute_S_action.simps [eqvt]

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

lemma supp_Pred [simp]: "supp (Pred φ) = supp φ"
unfolding supp_def by simp

instantiation S_action :: (fs,fs) fs
begin

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

end

instantiation S_action :: (bn,fs) bn
begin

  fun bn_S_action :: "('a,'b) S_action ⇒ atom set" where
    "bn_S_action (Act α) = bn α"
  | "bn_S_action (Pred _) = {}"

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

end


subsection ‹Satisfaction›

context nominal_ts
begin

  text ‹Here our formalization differs from the informal presentation, where the $S$-transform does
  not have any predicates. In Isabelle/HOL, there are no empty types; we use type @{typ unit}
  instead. However, it is clear from the following definition of the satisfaction relation that the
  single element of this type is not actually used in any meaningful way.›

  definition S_satisfies :: "'state ⇒ unit ⇒ bool" (infix ‹⊢⇩S› 70) where
    "P ⊢⇩S φ ⟷ False"

  lemma S_satisfies_eqvt: assumes "P ⊢⇩S φ" shows "(p ∙ P) ⊢⇩S (p ∙ φ)"
  using assms by (simp add: S_satisfies_def)

end


subsection ‹Transitions›

context nominal_ts
begin

  inductive S_transition :: "'state ⇒ (('act,'pred) S_action, 'state) residual ⇒ bool" (infix ‹→⇩S› 70) where
    Act: "P → ⟨α,P'⟩ ⟹ P →⇩S ⟨Act α,P'⟩"
  | Pred: "P ⊢ φ ⟹ P →⇩S ⟨Pred φ,P⟩"

  lemma S_transition_eqvt: assumes "P →⇩S α⇩SP'" shows "(p ∙ P) →⇩S (p ∙ α⇩SP')"
  using assms by cases (simp add: S_transition.Act transition_eqvt', simp add: S_transition.Pred satisfies_eqvt)

  text ‹If there is an $S$-transition, there is an ordinary transition with the same residual---it
  is not necessary to consider alpha-variants.›

  lemma S_transition_cases [case_names Act Pred, consumes 1]: assumes "P →⇩S ⟨α⇩S,P'⟩"
    and "⋀α. α⇩S = Act α ⟹ P → ⟨α,P'⟩ ⟹ R"
    and "⋀φ. α⇩S = Pred φ ⟹ P' = P ⟹ P ⊢ φ ⟹ R"
    shows R
  using assms proof (cases rule: S_transition.cases)
    case (Act α' P'')
    let ?Act = "Act :: 'act ⇒ ('act,'pred) S_action"
    from ‹⟨α⇩S,P'⟩ = ⟨Act α',P''⟩› obtain α where "α⇩S = Act α"
      by (meson bn_S_action.elims residual_empty_bn_eq_iff)
    with ‹⟨α⇩S,P'⟩ = ⟨Act α',P''⟩› obtain p where "supp (?Act α, P') - bn (?Act α) = supp (?Act α', P'') - bn (?Act α')"
      and "(supp (?Act α, P') - bn (?Act α)) ♯* p" and "p ∙ (?Act α, P') = (?Act α', P'')" and "p ∙ bn (?Act α) = bn (?Act α')"
      by (auto simp add: residual_eq_iff_perm)
    then have "supp (α, P') - bn α = supp (α', P'') - bn α'" and "(supp (α, P') - bn α) ♯* p"
      and "p ∙ (α, P') = (α', P'')" and "p ∙ bn α = bn α'"
      by (simp_all add: supp_Pair)
    then have "⟨α,P'⟩ = ⟨α',P''⟩"
      by (metis residual_eq_iff_perm)
    with ‹α⇩S = Act α› and ‹P → ⟨α',P''⟩› show R
      using ‹⋀α. α⇩S = Act α ⟹ P → ⟨α,P'⟩ ⟹ R› by metis
  next
    case (Pred φ)
    from ‹⟨α⇩S,P'⟩ = ⟨Pred φ,P⟩› have "α⇩S = Pred φ" and "P' = P"
      by (metis bn_S_action.simps(2) residual_empty_bn_eq_iff)+
    with ‹P ⊢ φ› show R
      using ‹⋀φ. α⇩S = Pred φ ⟹ P' = P ⟹ P ⊢ φ ⟹ R› by metis
  qed

  lemma S_transition_Act_iff: "P →⇩S ⟨Act α,P'⟩ ⟷ P → ⟨α,P'⟩"
    using S_transition.Act S_transition_cases by fastforce

  lemma S_transition_Pred_iff: "P →⇩S ⟨Pred φ,P'⟩ ⟷ P' = P ∧ P ⊢ φ"
    using S_transition.Pred S_transition_cases by fastforce

end


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

context nominal_ts
begin

  interpretation S_transform: nominal_ts "(⊢⇩S)" "(→⇩S)"
  by unfold_locales (fact S_satisfies_eqvt, fact S_transition_eqvt)

  no_notation S_satisfies (infix ‹⊢⇩S› 70) ― ‹denotes @{const S_transform.S_satisfies} instead›

  notation S_transform.bisimilar (infix ‹∼⋅⇩S› 100)

  text ‹Bisimilarity is equivalent to bisimilarity in the $S$-transform.›

  lemma bisimilar_is_S_transform_bisimulation: "S_transform.is_bisimulation bisimilar"
  unfolding S_transform.is_bisimulation_def
  proof
    show "symp bisimilar"
      by (fact bisimilar_symp)
  next
    have "∀P Q. P ∼⋅ Q ⟶ (∀φ. P ⊢⇩S φ ⟶ Q ⊢⇩S φ)" (is ?S)
      by (simp add: S_transform.S_satisfies_def)
    moreover have "∀P Q. P ∼⋅ Q ⟶ (∀α⇩S P'. bn α⇩S ♯* Q ⟶ P →⇩S ⟨α⇩S,P'⟩ ⟶ (∃Q'. Q →⇩S ⟨α⇩S,Q'⟩ ∧ P' ∼⋅ Q'))" (is ?T)
      proof (clarify)
        fix P Q α⇩S P'
        assume bisim: "P ∼⋅ Q" and fresh⇩S: "bn α⇩S ♯* Q" and trans⇩S: "P →⇩S ⟨α⇩S,P'⟩"
        obtain Q' where "Q →⇩S ⟨α⇩S,Q'⟩" and "P' ∼⋅ Q'"
          using trans⇩S proof (cases rule: S_transition_cases)
            case (Act α)
            from ‹α⇩S = Act α› and fresh⇩S have "bn α ♯* Q"
              by simp
            with bisim and ‹P → ⟨α,P'⟩› obtain Q' where transQ: "Q → ⟨α,Q'⟩" and bisim': "P' ∼⋅ Q'"
              by (metis bisimilar_simulation_step)
            from ‹α⇩S = Act α› and transQ have "Q →⇩S ⟨α⇩S,Q'⟩"
              by (simp add: S_transition.Act)
            with bisim' show "thesis"
              using ‹⋀Q'. Q →⇩S ⟨α⇩S,Q'⟩ ⟹ P' ∼⋅ Q' ⟹ thesis› by blast
          next
            case (Pred φ)
            from bisim and ‹P ⊢ φ› have "Q ⊢ φ"
              by (metis is_bisimulation_def bisimilar_is_bisimulation)
            with ‹α⇩S = Pred φ› have "Q →⇩S ⟨α⇩S,Q⟩"
              by (simp add: S_transition.Pred)
            with bisim and ‹P' = P› show "thesis"
              using ‹⋀Q'. Q →⇩S ⟨α⇩S,Q'⟩ ⟹ P' ∼⋅ Q' ⟹ thesis› by blast
          qed
        then show "∃Q'. Q →⇩S ⟨α⇩S,Q'⟩ ∧ P' ∼⋅ Q'"
          by auto
      qed
    ultimately show "?S ∧ ?T"
      by metis
  qed

  lemma S_transform_bisimilar_is_bisimulation: "is_bisimulation S_transform.bisimilar"
  unfolding is_bisimulation_def
  proof
    show "symp S_transform.bisimilar"
      by (fact S_transform.bisimilar_symp)
  next
    have "∀P Q. P ∼⋅⇩S Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)" (is ?S)
    proof (clarify)
      fix P Q φ
      assume bisim: "P ∼⋅⇩S Q" and valid: "P ⊢ φ"
      from valid have "P →⇩S ⟨Pred φ,P⟩"
        by (fact S_transition.Pred)
      moreover have "bn (Pred φ) ♯* Q"
        by (simp add: fresh_star_def)
      ultimately obtain Q' where trans': "Q →⇩S ⟨Pred φ,Q'⟩"
        using bisim by (metis S_transform.bisimilar_simulation_step)
      from trans' show "Q ⊢ φ"
        using S_transition_Pred_iff by blast
    qed
    moreover have "∀P Q. P ∼⋅⇩S Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ P' ∼⋅⇩S Q'))" (is ?T)
      proof (clarify)
        fix P Q α P'
        assume bisim: "P ∼⋅⇩S Q" and fresh: "bn α ♯* Q" and trans: "P → ⟨α,P'⟩"
        from trans have "P →⇩S ⟨Act α,P'⟩"
          by (fact S_transition.Act)
        with bisim and fresh obtain Q' where trans': "Q →⇩S ⟨Act α,Q'⟩" and bisim': "P' ∼⋅⇩S Q'"
          by (metis S_transform.bisimilar_simulation_step bn_S_action.simps(1))
        from trans' have "Q → ⟨α,Q'⟩"
          by (metis S_transition_Act_iff)
        with bisim' show "∃Q'. Q → ⟨α,Q'⟩ ∧ P' ∼⋅⇩S Q'"
          by metis
      qed
    ultimately show "?S ∧ ?T"
      by metis
  qed

  theorem S_transform_bisimilar_iff: "P ∼⋅⇩S Q ⟷ P ∼⋅ Q"
  proof
    assume "P ∼⋅⇩S Q"
    then show "P ∼⋅ Q"
      by (metis S_transform_bisimilar_is_bisimulation bisimilar_def)
  next
    assume "P ∼⋅ Q"
    then show "P ∼⋅⇩S Q"
      by (metis S_transform.bisimilar_def bisimilar_is_S_transform_bisimulation)
  qed

end


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

context weak_nominal_ts
begin

  lemma weakly_bisimilar_tau_transition_weakly_bisimilar:
    assumes "P ≈⋅ R" and "P ⇒ Q" and "Q ⇒ R"
    shows "Q ≈⋅ R"
  proof -
    let ?bisim = "λS T. S ≈⋅ T ∨ {S,T} = {Q,R}"
    have "is_weak_bisimulation ?bisim"
      unfolding is_weak_bisimulation_def
    proof
      show "symp ?bisim"
        using weakly_bisimilar_symp by (simp add: insert_commute symp_def)
    next
      have "∀S T φ. ?bisim S T ∧ S ⊢ φ ⟶ (∃T'. T ⇒ T' ∧ ?bisim S T' ∧ T' ⊢ φ)" (is ?S)
      proof (clarify)
        fix S T φ
        assume bisim: "?bisim S T" and valid: "S ⊢ φ"
        from bisim show "∃T'. T ⇒ T' ∧ ?bisim S T' ∧ T' ⊢ φ"
        proof
          assume "S ≈⋅ T"
          with valid show ?thesis
            by (metis is_weak_bisimulation_def weakly_bisimilar_is_weak_bisimulation)
        next
          assume "{S, T} = {Q, R}"
          then have "S = Q ∧ T = R ∨ T = Q ∧ S = R"
            by (metis doubleton_eq_iff)
          then show ?thesis
          proof
            assume "S = Q ∧ T = R"
            with ‹P ⇒ Q› and ‹P ≈⋅ R› and valid show ?thesis
              by (metis is_weak_bisimulation_def tau_transition_trans weakly_bisimilar_is_weak_bisimulation weakly_bisimilar_tau_simulation_step)
          next
            assume "T = Q ∧ S = R"
            with ‹Q ⇒ R› and valid show ?thesis
              by (meson reflpE weakly_bisimilar_reflp)
          qed
        qed
      qed
      moreover have "∀S T. ?bisim S T ⟶ (∀α S'. bn α ♯* T ⟶ S → ⟨α,S'⟩ ⟶ (∃T'. T ⇒⟨α⟩ T' ∧ ?bisim S' T'))" (is ?T)
      proof (clarify)
        fix S T α S'
        assume bisim: "?bisim S T" and fresh: "bn α ♯* T" and trans: "S → ⟨α,S'⟩"
        from bisim show "∃T'. T ⇒⟨α⟩ T' ∧ ?bisim S' T'"
        proof
          assume "S ≈⋅ T"
          with fresh and trans show ?thesis
            by (metis is_weak_bisimulation_def weakly_bisimilar_is_weak_bisimulation)
        next
          assume "{S, T} = {Q, R}"
          then have "S = Q ∧ T = R ∨ T = Q ∧ S = R"
            by (metis doubleton_eq_iff)
          then show ?thesis
          proof
            assume "S = Q ∧ T = R"
            with ‹P ⇒ Q› and ‹P ≈⋅ R› and fresh and trans show ?thesis
              using observable_transition_stepI tau_refl weak_transition_stepI weak_transition_weakI weakly_bisimilar_weak_simulation_step by blast
          next
            assume "T = Q ∧ S = R"
            with ‹Q ⇒ R› and trans show ?thesis
              by (metis observable_transition_stepI reflpE tau_refl weak_transition_stepI weak_transition_weakI weakly_bisimilar_reflp)
          qed
        qed
      qed
      ultimately show "?S ∧ ?T"
        by metis
    qed
    then show ?thesis
      using weakly_bisimilar_def by blast
  qed

  notation S_satisfies (infix ‹⊢⇩S› 70)

  interpretation S_transform: weak_nominal_ts "(⊢⇩S)" "(→⇩S)" "Act τ"
  by unfold_locales (fact S_satisfies_eqvt, fact S_transition_eqvt, simp add: tau_eqvt)

  no_notation S_satisfies (infix ‹⊢⇩S› 70) ― ‹denotes @{const S_transform.S_satisfies} instead›

  notation S_transform.tau_transition (infix ‹⇒⇩S› 70)
  notation S_transform.observable_transition (‹_/ ⇒{_}⇩S/ _› [70, 70, 71] 71)
  notation S_transform.weak_transition (‹_/ ⇒⟨_⟩⇩S/ _› [70, 70, 71] 71)
  notation S_transform.weakly_bisimilar (infix ‹≈⋅⇩S› 100)

  lemma S_transform_tau_transition_iff: "P ⇒⇩S P' ⟷ P ⇒ P'"
  proof
    assume "P ⇒⇩S P'"
    then show "P ⇒ P'"
      by induct (simp, metis S_transition_Act_iff tau_step)
  next
    assume "P ⇒ P'"
    then show "P ⇒⇩S P'"
      by induct (simp, metis S_transform.tau_transition.simps S_transition.Act)
  qed

  lemma S_transform_observable_transition_iff: "P ⇒{Act α}⇩S P' ⟷ P ⇒{α} P'"
    unfolding S_transform.observable_transition_def observable_transition_def
    by (metis S_transform_tau_transition_iff S_transition_Act_iff)

  lemma S_transform_weak_transition_iff: "P ⇒⟨Act α⟩⇩S P' ⟷ P ⇒⟨α⟩ P'"
    by (simp add: S_transform_observable_transition_iff S_transform_tau_transition_iff weak_transition_def)

  text ‹Weak bisimilarity is equivalent to weak bisimilarity in the $S$-transform.›

  lemma weakly_bisimilar_is_S_transform_weak_bisimulation: "S_transform.is_weak_bisimulation weakly_bisimilar"
  unfolding S_transform.is_weak_bisimulation_def
  proof
    show "symp weakly_bisimilar"
      by (fact weakly_bisimilar_symp)
  next
    have "∀P Q φ. P ≈⋅ Q ∧ P ⊢⇩S φ ⟶ (∃Q'. Q ⇒⇩S Q' ∧ P ≈⋅ Q' ∧ Q' ⊢⇩S φ)" (is ?S)
      by (simp add: S_transform.S_satisfies_def)
    moreover have "∀P Q. P ≈⋅ Q ⟶ (∀α⇩S P'. bn α⇩S ♯* Q ⟶ P →⇩S ⟨α⇩S,P'⟩ ⟶ (∃Q'. Q ⇒⟨α⇩S⟩⇩S Q' ∧ P' ≈⋅ Q'))" (is ?T)
      proof (clarify)
        fix P Q α⇩S P'
        assume bisim: "P ≈⋅ Q" and fresh⇩S: "bn α⇩S ♯* Q" and trans⇩S: "P →⇩S ⟨α⇩S,P'⟩"
        obtain Q' where "Q ⇒⟨α⇩S⟩⇩S Q'" and "P' ≈⋅ Q'"
          using trans⇩S proof (cases rule: S_transition_cases)
            case (Act α)
            from ‹α⇩S = Act α› and fresh⇩S have "bn α ♯* Q"
              by simp
            with bisim and ‹P → ⟨α,P'⟩› obtain Q' where transQ: "Q ⇒⟨α⟩ Q'" and bisim': "P' ≈⋅ Q'"
              by (metis is_weak_bisimulation_def weakly_bisimilar_is_weak_bisimulation)
            from ‹α⇩S = Act α› and transQ have "Q ⇒⟨α⇩S⟩⇩S Q'"
              by (metis S_transform_weak_transition_iff)
            with bisim' show "thesis"
              using ‹⋀Q'. Q ⇒⟨α⇩S⟩⇩S Q' ⟹ P' ≈⋅ Q' ⟹ thesis› by blast
          next
            case (Pred φ)
            from bisim and ‹P ⊢ φ› obtain Q' where "Q ⇒ Q'" and "P ≈⋅ Q'" and "Q' ⊢ φ"
              by (metis is_weak_bisimulation_def weakly_bisimilar_is_weak_bisimulation)
            from ‹Q ⇒ Q'› have "Q ⇒⇩S Q'"
              by (metis S_transform_tau_transition_iff)
            moreover from ‹Q' ⊢ φ› have "Q' →⇩S ⟨Pred φ,Q'⟩"
              by (simp add: S_transition.Pred)
            ultimately have "Q ⇒⟨α⇩S⟩⇩S Q'"
              using ‹α⇩S = Pred φ› by (metis S_transform.observable_transitionI S_transform.tau_refl S_transform.weak_transition_stepI)
            with ‹P' = P› and ‹P ≈⋅ Q'› show "thesis"
              using ‹⋀Q'. Q ⇒⟨α⇩S⟩⇩S Q' ⟹ P' ≈⋅ Q' ⟹ thesis› by blast
          qed
        then show "∃Q'. Q ⇒⟨α⇩S⟩⇩S Q' ∧ P' ≈⋅ Q'"
          by auto
      qed
    ultimately show "?S ∧ ?T"
      by metis
  qed

  lemma S_transform_weakly_bisimilar_is_weak_bisimulation: "is_weak_bisimulation S_transform.weakly_bisimilar"
  unfolding is_weak_bisimulation_def
  proof
    show "symp S_transform.weakly_bisimilar"
      by (fact S_transform.weakly_bisimilar_symp)
  next
    have "∀P Q φ. P ≈⋅⇩S Q ∧ P ⊢ φ ⟶ (∃Q'. Q ⇒ Q' ∧ P ≈⋅⇩S Q' ∧ Q' ⊢ φ)" (is ?S)
    proof (clarify)
      fix P Q φ
      assume bisim: "P ≈⋅⇩S Q" and valid: "P ⊢ φ"
      from valid have "P ⇒⟨Pred φ⟩⇩S P"
        by (simp add: S_transition.Pred)
      moreover have "bn (Pred φ) ♯* Q"
        by (simp add: fresh_star_def)
      ultimately obtain Q'' where trans': "Q ⇒⟨Pred φ⟩⇩S Q''" and bisim': "P ≈⋅⇩S Q''"
        using bisim by (metis S_transform.weakly_bisimilar_weak_simulation_step)

      from trans' obtain Q' Q⇩1 where trans⇩1: "Q ⇒⇩S Q'" and trans⇩2: "Q' →⇩S ⟨Pred φ, Q⇩1⟩" and trans⇩3: "Q⇩1 ⇒⇩S Q''"
        by (auto simp add: S_transform.observable_transition_def)
      from trans⇩2 have eq: "Q⇩1 = Q'" and "Q' ⊢ φ"
        using S_transition_Pred_iff by blast+
      moreover from trans⇩1 and trans⇩3 and eq and bisim and bisim' have "P ≈⋅⇩S Q'"
        by (metis S_transform.weakly_bisimilar_equivp S_transform.weakly_bisimilar_tau_transition_weakly_bisimilar equivp_def)
      moreover from trans⇩1 have "Q ⇒ Q'"
        by (metis S_transform_tau_transition_iff)
      ultimately show "∃Q'. Q ⇒ Q' ∧ P ≈⋅⇩S Q' ∧ Q' ⊢ φ"
        by metis
    qed
    moreover have "∀P Q. P ≈⋅⇩S Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q ⇒⟨α⟩ Q' ∧ P' ≈⋅⇩S Q'))" (is ?T)
      proof (clarify)
        fix P Q α P'
        assume bisim: "P ≈⋅⇩S Q" and fresh: "bn α ♯* Q" and trans: "P → ⟨α,P'⟩"
        from trans have "P →⇩S ⟨Act α,P'⟩"
          by (fact S_transition.Act)
        with bisim and fresh obtain Q' where trans': "Q ⇒⟨Act α⟩⇩S Q'" and bisim': "P' ≈⋅⇩S Q'"
          by (metis S_transform.is_weak_bisimulation_def S_transform.weakly_bisimilar_is_weak_bisimulation bn_S_action.simps(1))
        from trans' have "Q ⇒⟨α⟩ Q'"
          by (metis S_transform_weak_transition_iff)
        with bisim' show "∃Q'. Q ⇒⟨α⟩ Q' ∧ P' ≈⋅⇩S Q'"
          by metis
      qed
    ultimately show "?S ∧ ?T"
      by metis
  qed

  theorem S_transform_weakly_bisimilar_iff: "P ≈⋅⇩S Q ⟷ P ≈⋅ Q"
  proof
    assume "P ≈⋅⇩S Q"
    then show "P ≈⋅ Q"
      by (metis S_transform_weakly_bisimilar_is_weak_bisimulation weakly_bisimilar_def)
  next
    assume "P ≈⋅ Q"
    then show "P ≈⋅⇩S Q"
      by (metis S_transform.weakly_bisimilar_def weakly_bisimilar_is_S_transform_weak_bisimulation)
  qed

end


subsection ‹Translation of (strong) formulas into formulas without predicates›

text ‹Since we defined formulas via a manual quotient construction, we also need to define the
$S$-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 (strong) formulas as arguments--we derive a version that returns formulas.›

primrec S_transform_Tree :: "('idx,'pred::fs,'act::bn) Tree ⇒ ('idx, unit, ('act,'pred) S_action) Tree⇩α" where
  "S_transform_Tree (tConj tset) = Conj⇩α (map_bset S_transform_Tree tset)"
| "S_transform_Tree (tNot t) = Not⇩α (S_transform_Tree t)"
| "S_transform_Tree (tPred φ) = Act⇩α (S_action.Pred φ) (Conj⇩α bempty)"
| "S_transform_Tree (tAct α t) = Act⇩α (S_action.Act α) (S_transform_Tree t)"

lemma S_transform_Tree_eqvt [eqvt]: "p ∙ S_transform_Tree t = S_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 S_transform_Tree} respects $\alpha$-equivalence.›

lemma alpha_Tree_S_transform_Tree:
  assumes "t1 =⇩α t2"
  shows "S_transform_Tree t1 = S_transform_Tree t2"
using assms proof (induction t1 t2 rule: alpha_Tree_induct')
  case (alpha_tConj tset1 tset2)
  then have "rel_bset (=) (map_bset S_transform_Tree tset1) (map_bset S_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 α1 t1 α2 t2)
  from ‹tAct α1 t1 =⇩α tAct α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)"
    by auto
  from * have fresh: "(supp_rel alpha_Tree t1 - bn α1) ♯* p" and alpha: "p ∙ t1 =⇩α t2" and eq: "p ∙ bn α1 = bn α2"
    by (auto simp add: alpha_set)
  from alpha_tAct.IH(2) have "supp_rel alpha_Tree (rep_Tree⇩α (S_transform_Tree t1)) ⊆ supp_rel alpha_Tree t1"
    by (metis (no_types, lifting) infinite_mono alpha_Tree_permute_rep_commute S_transform_Tree_eqvt mem_Collect_eq subsetI supp_rel_def)
  with fresh have fresh': "(supp_rel alpha_Tree (rep_Tree⇩α (S_transform_Tree t1)) - bn α1) ♯* p"
    by (meson DiffD1 DiffD2 DiffI fresh_star_def subsetCE)
  moreover from alpha have alpha': "p ∙ rep_Tree⇩α (S_transform_Tree t1) =⇩α rep_Tree⇩α (S_transform_Tree t2)"
    using alpha_tAct.IH(1) by (metis alpha_Tree_permute_rep_commute S_transform_Tree_eqvt)
  moreover from fresh' alpha' eq have "supp_rel alpha_Tree (rep_Tree⇩α (S_transform_Tree t1)) - bn α1 = supp_rel alpha_Tree (rep_Tree⇩α (S_transform_Tree t2)) - bn α2"
    by (metis (mono_tags) Diff_eqvt alpha_Tree_eqvt' alpha_Tree_eqvt_aux alpha_Tree_supp_rel atom_set_perm_eq)
  ultimately have "(bn α1, rep_Tree⇩α (S_transform_Tree t1)) ≈set alpha_Tree (supp_rel alpha_Tree) p (bn α2, rep_Tree⇩α (S_transform_Tree t2))"
    using eq by (simp add: alpha_set)
  moreover from ** have "(bn α1, S_action.Act α1) ≈set (=) supp p (bn α2, S_action.Act α2)"
    by (metis (mono_tags, lifting) S_Transform.supp_Act alpha_set permute_S_action.simps(1))
  ultimately have "Act⇩α (S_action.Act α1) (S_transform_Tree t1) = Act⇩α (S_action.Act α2) (S_transform_Tree t2)"
    by (auto simp add: Act⇩α_eq_iff)
  then show ?case
    by simp
qed simp_all

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

lift_definition S_transform_Tree⇩α :: "('idx,'pred::fs,'act::bn) Tree⇩α ⇒ ('idx, unit, ('act,'pred) S_action) Tree⇩α" is
    S_transform_Tree
  by (fact alpha_Tree_S_transform_Tree)

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

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

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

lemma S_transform_Tree⇩α_Pred⇩α [simp]: "S_transform_Tree⇩α (Pred⇩α φ) = Act⇩α (S_action.Pred φ) (Conj⇩α bempty)"
  by transfer simp

lemma S_transform_Tree⇩α_Act⇩α [simp]: "S_transform_Tree⇩α (Act⇩α α t⇩α) = Act⇩α (S_action.Act α) (S_transform_Tree⇩α t⇩α)"
  by transfer simp

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

lemma S_transform_Tree⇩α_preserves_hereditarily_fs:
  assumes "hereditarily_fs t⇩α"
  shows "hereditarily_fs (S_transform_Tree⇩α t⇩α)"
using assms proof (induct rule: hereditarily_fs.induct)
  case (Conj⇩α tset⇩α)
  then show ?case
    by (auto intro!: hereditarily_fs.Conj⇩α) (metis imageE map_bset.rep_eq)
next
  case (Not⇩α t⇩α)
  then show ?case
    by (simp add: hereditarily_fs.Not⇩α)
next
  case (Pred⇩α φ)
  have "finite (supp bempty)"
    by (simp add: eqvtI supp_fun_eqvt)
  then show ?case
    using hereditarily_fs.Act⇩α finite_supp_implies_hereditarily_fs_Conj⇩α by fastforce
next
  case (Act⇩α t⇩α α)
  then show ?case
    by (simp add: Formula.hereditarily_fs.Act⇩α)
qed

text ‹$S$-transform for (strong) formulas.›

lift_definition S_transform_formula :: "('idx,'pred::fs,'act::bn) formula ⇒ ('idx, unit, ('act,'pred) S_action) Tree⇩α" is
    S_transform_Tree⇩α
  .

lemma S_transform_formula_eqvt [eqvt]: "p ∙ S_transform_formula x = S_transform_formula (p ∙ x)"
  by transfer (simp)

lemma S_transform_formula_Conj [simp]:
  assumes "finite (supp xset)"
  shows "S_transform_formula (Conj xset) = Conj⇩α (map_bset S_transform_formula xset)"
  using assms by (simp add: Conj_def S_transform_formula_def bset.map_comp map_fun_def)

lemma S_transform_formula_Not [simp]: "S_transform_formula (Not x) = Not⇩α (S_transform_formula x)"
  by transfer simp

lemma S_transform_formula_Pred [simp]: "S_transform_formula (Formula.Pred φ) = Act⇩α (S_action.Pred φ) (Conj⇩α bempty)"
  by transfer simp

lemma S_transform_formula_Act [simp]: "S_transform_formula (Formula.Act α x) = Formula.Act⇩α (S_action.Act α) (S_transform_formula x)"
  by transfer simp

lemma S_transform_formula_hereditarily_fs [simp]: "hereditarily_fs (S_transform_formula x)"
  by transfer (fact S_transform_Tree⇩α_preserves_hereditarily_fs)

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

definition S_transform :: "('idx,'pred::fs,'act::bn) formula ⇒ ('idx, unit, ('act,'pred) S_action) formula" where
  "S_transform x = Abs_formula (S_transform_formula x)"

lemma S_transform_eqvt [eqvt]: "p ∙ S_transform x = S_transform (p ∙ x)"
  unfolding S_transform_def by simp

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

lemma S_transform_Conj [simp]:
  assumes "finite (supp xset)"
  shows "S_transform (Conj xset) = Conj (map_bset S_transform xset)"
  using assms unfolding S_transform_def by (simp, simp add: Conj_def bset.map_comp o_def)

lemma S_transform_Not [simp]: "S_transform (Not x) = Not (S_transform x)"
  unfolding S_transform_def by (simp add: Not.abs_eq eq_onp_same_args)

lemma S_transform_Pred [simp]: "S_transform (Formula.Pred φ) = Formula.Act (S_action.Pred φ) (Conj bempty)"
  unfolding S_transform_def by (simp add: Formula.Act_def Conj_rep_eq eqvtI supp_fun_eqvt)

lemma S_transform_Act [simp]: "S_transform (Formula.Act α x) = Formula.Act (S_action.Act α) (S_transform x)"
  unfolding S_transform_def by (simp, simp add: Formula.Act_def)

context nominal_ts
begin

  lemma valid_Conj_bempty [simp]: "P ⊨ Conj bempty"
  by (simp add: bempty.rep_eq eqvtI supp_fun_eqvt)

  notation S_satisfies (infix ‹⊢⇩S› 70)

  interpretation S_transform: nominal_ts "(⊢⇩S)" "(→⇩S)"
  by unfold_locales (fact S_satisfies_eqvt, fact S_transition_eqvt)

  notation S_transform.valid (infix ‹⊨⇩S› 70)

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

  theorem valid_iff_valid_S_transform: shows "P ⊨ x ⟷ P ⊨⇩S S_transform x"
  proof (induct x arbitrary: P)
    case (Conj xset)
    then show ?case
      by auto (metis imageE map_bset.rep_eq, simp add: map_bset.rep_eq)
  next
    case (Not x)
    then show ?case by simp
  next
    case (Pred φ)
    let ?φ = "Formula.Pred φ :: ('idx, 'pred, ('act,'pred) S_action) formula"
    have "bn (S_action.Pred φ :: ('act,'pred) S_action) ♯* P"
      by (simp add: fresh_star_def)
    then show ?case
      by (auto simp add: S_transform.valid_Act_fresh S_transition_Pred_iff)
  next
    case (Act α x)
    show ?case
    proof
      assume "P ⊨ Formula.Act α x"
      then obtain α' x' P' where eq: "Formula.Act α x = Formula.Act α' x'" and trans: "P → ⟨α',P'⟩" and valid: "P' ⊨ x'"
        by (metis valid_Act)
      from eq obtain p where p_x: "p ∙ x = x'" and p_α: "p ∙ α = α'"
        by (metis Act_eq_iff_perm)

      from valid have "-p ∙ P' ⊨ x"
        using p_x by (metis valid_eqvt permute_minus_cancel(2))
      then have "-p ∙ P' ⊨⇩S S_transform x"
        using Act.hyps(1) by metis
      then have "P' ⊨⇩S S_transform x'"
        by (metis (no_types, lifting) p_x S_transform.valid_eqvt S_transform_eqvt permute_minus_cancel(1))

      with eq and trans show "P ⊨⇩S S_transform (Formula.Act α x)"
        using S_transform.valid_Act S_transition.Act by fastforce
    next
      assume *: "P ⊨⇩S S_transform (Formula.Act α x)"

      ― ‹rename~@{term "bn α"} to avoid~@{term "P"}, without touching~@{term "Formula.Act α x"}›
      obtain p where 1: "(p ∙ bn α) ♯* P" and 2: "supp (Formula.Act α x) ♯* p"
      proof (rule at_set_avoiding2[of "bn α" "P" "Formula.Act α x", THEN exE])
        show "finite (bn α)" by (fact bn_finite)
      next
        show "finite (supp P)" by (fact finite_supp)
      next
        show "finite (supp (Formula.Act α x))" by (fact finite_supp)
      next
        show "bn α ♯* Formula.Act α x" by simp
      qed metis
      from 2 have eq: "Formula.Act α x = Formula.Act (p ∙ α) (p ∙ x)"
        using supp_perm_eq by fastforce

      with * have "P ⊨⇩S Formula.Act (S_action.Act (p ∙ α)) (S_transform (p ∙ x))"
        by simp
      with 1 obtain P' where trans: "P →⇩S ⟨S_action.Act (p ∙ α),P'⟩" and valid: "P' ⊨⇩S S_transform (p ∙ x)"
        by (metis S_transform.valid_Act_fresh bn_S_action.simps(1) bn_eqvt)

      from valid have "-p ∙ P' ⊨⇩S S_transform x"
        by (metis (no_types, opaque_lifting) S_transform.valid_eqvt S_transform_eqvt permute_minus_cancel(1))
      then have "-p ∙ P' ⊨ x"
        using Act.hyps(1) by metis
      then have "P' ⊨ p ∙ x"
        by (metis permute_minus_cancel(1) valid_eqvt)

      moreover from trans have "P → ⟨p ∙ α,P'⟩"
        using S_transition_Act_iff by blast

      ultimately show "P ⊨ Formula.Act α x"
        using eq valid_Act by blast
    qed
  qed

end

context indexed_nominal_ts
begin

  text ‹The following (alternative) proof of the ``$\rightarrow$'' direction of theorem
  @{thm S_transform_bisimilar_iff}, namely that bisimilarity in the $S$-transform implies
  bisimilarity in the original transition system, uses the fact that the $S$-transform(ation)
  preserves satisfaction of formulas, together with the fact that bisimilarity (in the
  $S$-transform) implies logical equivalence, and equivalence (in the original transition system)
  implies bisimilarity. However, since we proved the latter in the context of indexed nominal
  transition systems, this proof requires an indexed nominal transition system.›

  interpretation S_transform: indexed_nominal_ts "(⊢⇩S)" "(→⇩S)"
    by unfold_locales (fact S_satisfies_eqvt, fact S_transition_eqvt, fact card_idx_perm, fact card_idx_state)

  notation S_transform.bisimilar (infix ‹∼⋅⇩S› 100)

  theorem "P ∼⋅⇩S Q ⟶ P ∼⋅ Q"
  proof
    assume "P ∼⋅⇩S Q"
    then have "S_transform.logically_equivalent P Q"
      by (fact S_transform.bisimilarity_implies_equivalence)
    with valid_iff_valid_S_transform have "logically_equivalent P Q"
      using logically_equivalent_def S_transform.logically_equivalent_def by blast
    then show "P ∼⋅ Q"
      by (fact equivalence_implies_bisimilarity)
  qed

end


subsection ‹Translation of weak formulas into formulas without predicates›

context indexed_weak_nominal_ts
begin

  notation S_satisfies (infix ‹⊢⇩S› 70)

  interpretation S_transform: indexed_weak_nominal_ts "S_action.Act τ" "(⊢⇩S)" "(→⇩S)"
    by unfold_locales (fact S_satisfies_eqvt, fact S_transition_eqvt, simp add: tau_eqvt, fact card_idx_perm, fact card_idx_state, fact card_idx_nat)

  notation S_transform.valid (infix ‹⊨⇩S› 70)
  notation S_transform.weakly_bisimilar (infix ‹≈⋅⇩S› 100)

  text ‹The $S$-transform of a weak formula is not necessarily a weak formula. However, the image of
    all weak formulas under the $S$-transform is adequate for weak bisimilarity.›

  corollary "P ≈⋅⇩S Q ⟷ (∀x. weak_formula x ⟶ P ⊨⇩S S_transform x ⟷ Q ⊨⇩S S_transform x)"
    by (meson valid_iff_valid_S_transform weak_bisimilarity_implies_weak_equivalence weak_equivalence_implies_weak_bisimilarity S_transform_weakly_bisimilar_iff weakly_logically_equivalent_def)

  text ‹For every weak formula, there is an equivalent weak formula over the $S$-transform.›

  corollary
    assumes "weak_formula x"
    obtains y where "S_transform.weak_formula y" and "∀P. P ⊨ x ⟷ P ⊨⇩S y"
  proof -
    let ?S = "{P. P ⊨ x}"

    ― ‹@{term ?S} is finitely supported›
    have "supp x supports ?S"
      unfolding supports_def proof (clarify)
      fix a b
      assume a: "a ∉ supp x" and b: "b ∉ supp x"
      {
        fix P
        from a and b have "(a ⇌ b) ∙ x = x"
          by (simp add: fresh_def swap_fresh_fresh)
        then have "(a ⇌ b) ∙ P ⊨ x ⟷ P ⊨ x"
          by (metis permute_swap_cancel valid_eqvt)
      }
      note * = this
      show "(a ⇌ b) ∙ ?S = ?S"
        by auto (metis mem_Collect_eq mem_permute_iff permute_swap_cancel "*", simp add: Collect_eqvt permute_fun_def "*")
    qed
    then have "finite (supp ?S)"
      using finite_supp supports_finite by blast

    ― ‹@{term ?S} is closed under weak bisimilarity›
    moreover {
      fix P Q
      assume "P ∈ ?S" and "P ≈⋅⇩S Q"
      with ‹weak_formula x› have "Q ∈ ?S"
        using S_transform_weakly_bisimilar_iff weak_bisimilarity_implies_weak_equivalence weakly_logically_equivalent_def by auto
    }

    ultimately show ?thesis
      using S_transform.weak_expressive_completeness that by (metis (no_types, lifting) mem_Collect_eq)
  qed

end

end