Session Modal_Logics_for_NTS

Theory Nominal_Bounded_Set

theory Nominal_Bounded_Set
imports
  Nominal2.Nominal2
  "HOL-Cardinals.Bounded_Set"
begin

section ‹Bounded Sets Equipped With a Permutation Action›

text ‹Additional lemmas about bounded sets.›

interpretation bset_lifting: bset_lifting .

lemma Abs_bset_inverse' [simp]:
  assumes "|A| <o natLeq +c |UNIV :: 'k set|"
  shows "set_bset (Abs_bset A :: 'a set['k]) = A"
by (metis Abs_bset_inverse assms mem_Collect_eq)

text ‹Bounded sets are equipped with a permutation action, provided their elements are.›

instantiation bset :: (pt,type) pt
begin

  lift_definition permute_bset :: "perm  'a set['b]  'a set['b]" is
    permute
  proof -
    fix p and A :: "'a set"
    have "|p  A| ≤o |A|" by (simp add: permute_set_eq_image)
    also assume "|A| <o natLeq +c |UNIV :: 'b set|"
    finally show "|p  A| <o natLeq +c |UNIV :: 'b set|" .
  qed

  instance
  by standard (transfer, simp)+

end

lemma Abs_bset_eqvt [simp]:
  assumes "|A| <o natLeq +c |UNIV :: 'k set|"
  shows "p  (Abs_bset A :: 'a::pt set['k]) = Abs_bset (p  A)"
by (simp add: permute_bset_def map_bset_def image_def permute_set_def) (metis (no_types, lifting) Abs_bset_inverse' assms)

lemma supp_Abs_bset [simp]:
  assumes "|A| <o natLeq +c |UNIV :: 'k set|"
  shows "supp (Abs_bset A :: 'a::pt set['k]) = supp A"
proof -
  from assms have "p. p  (Abs_bset A :: 'a::pt set['k])  Abs_bset A  p  A  A"
    by simp (metis map_bset.rep_eq permute_set_eq_image set_bset_inverse set_bset_to_set_bset)
  then show ?thesis
    unfolding supp_def by simp
qed

lemma map_bset_permute: "p  B = map_bset (permute p) B"
by transfer (auto simp add: image_def permute_set_def)

lemma set_bset_eqvt [eqvt]:
  "p  set_bset B = set_bset (p  B)"
by transfer simp

lemma map_bset_eqvt [eqvt]:
  "p  map_bset f B = map_bset (p  f) (p  B)"
by transfer simp

lemma bempty_eqvt [eqvt]: "p  bempty = bempty"
by transfer simp

lemma binsert_eqvt [eqvt]: "p  (binsert x B) = binsert (p  x) (p  B)"
by transfer simp

lemma bsingleton_eqvt [eqvt]: "p  bsingleton x = bsingleton (p  x)"
by (simp add: map_bset_permute)

end

Theory Nominal_Wellfounded

theory Nominal_Wellfounded
imports
  Nominal2.Nominal2
begin

section ‹Lemmas about Well-Foundedness and Permutations›

definition less_bool_rel :: "bool rel" where
  "less_bool_rel  {(x,y). x<y}"

lemma less_bool_rel_iff [simp]:
  "(a,b)  less_bool_rel  ¬ a  b"
by (metis less_bool_def less_bool_rel_def mem_Collect_eq split_conv)

lemma wf_less_bool_rel: "wf less_bool_rel"
by (metis less_bool_rel_iff wfUNIVI)


subsection ‹Hull and well-foundedness›

inductive_set hull_rel where
  "(p  x, x)  hull_rel"

lemma hull_relp_reflp: "reflp hull_relp"
by (metis hull_relp.intros permute_zero reflpI)

lemma hull_relp_symp: "symp hull_relp"
by (metis (poly_guards_query) hull_relp.simps permute_minus_cancel(2) sympI)

lemma hull_relp_transp: "transp hull_relp"
by (metis (full_types) hull_relp.simps permute_plus transpI)

lemma hull_relp_equivp: "equivp hull_relp"
by (metis equivpI hull_relp_reflp hull_relp_symp hull_relp_transp)

lemma hull_rel_relcomp_subset:
  assumes "eqvt R"
  shows "R O hull_rel  hull_rel O R"
proof
  fix x
  assume "x  R O hull_rel"
  then obtain x1 x2 y where x: "x = (x1,x2)" and R: "(x1,y)  R" and "(y,x2)  hull_rel"
    by auto
  then obtain p where "y = p  x2"
    by (metis hull_rel.simps)
  then have "-p  y = x2"
    by (metis permute_minus_cancel(2))
  then have "(-p  x1, x2)  R"
    using R assms by (metis Pair_eqvt eqvt_def mem_permute_iff)
  moreover have "(x1, -p  x1)  hull_rel"
    by (metis hull_rel.intros permute_minus_cancel(2))
  ultimately show "x  hull_rel O R"
    using x by auto
qed

lemma wf_hull_rel_relcomp:
  assumes "wf R" and "eqvt R"
  shows "wf (hull_rel O R)"
using assms by (metis hull_rel_relcomp_subset wf_relcomp_compatible)

lemma hull_rel_relcompI [simp]:
  assumes "(x, y)  R"
  shows "(p  x, y)  hull_rel O R"
using assms by (metis hull_rel.intros relcomp.relcompI)

lemma hull_rel_relcomp_trivialI [simp]:
  assumes "(x, y)  R"
  shows "(x, y)  hull_rel O R"
using assms by (metis hull_rel_relcompI permute_zero)

end

Theory Residual

theory Residual
imports
  Nominal2.Nominal2
begin

section ‹Residuals›

subsection ‹Binding names›

text ‹To define $\alpha$-equivalence, we require actions to be equipped with an equivariant
function~@{term bn} that gives their binding names. Actions may only bind finitely many names. This
is necessary to ensure that we can use a finite permutation to rename the binding names in an
action.›

class bn = fs +
  fixes bn :: "'a  atom set"
  assumes bn_eqvt: "p  (bn α) = bn (p  α)"
  and bn_finite: "finite (bn α)"

lemma bn_subset_supp: "bn α  supp α"
by (metis (erased, hide_lams) bn_eqvt bn_finite eqvt_at_def finite_supp supp_eqvt_at supp_finite_atom_set)


subsection ‹Raw residuals and \texorpdfstring{$\alpha$}{alpha}-equivalence›

text ‹Raw residuals are simply pairs of actions and states. Binding names in the action bind into
(the action and) the state.›

fun alpha_residual :: "('act::bn × 'state::pt)  ('act × 'state)  bool" where
  "alpha_residual (α1,P1) (α2,P2)  [bn α1]set. (α1, P1) = [bn α2]set. (α2, P2)"

text ‹$\alpha$-equivalence is equivariant.›

lemma alpha_residual_eqvt [eqvt]:
  assumes "alpha_residual r1 r2"
  shows "alpha_residual (p  r1) (p  r2)"
using assms by (cases r1, cases r2) (simp, metis Pair_eqvt bn_eqvt permute_Abs_set)

text ‹$\alpha$-equivalence is an equivalence relation.›

lemma alpha_residual_reflp: "reflp alpha_residual"
by (metis alpha_residual.simps prod.exhaust reflpI)

lemma alpha_residual_symp: "symp alpha_residual"
by (metis alpha_residual.simps prod.exhaust sympI)

lemma alpha_residual_transp: "transp alpha_residual"
by (rule transpI) (metis alpha_residual.simps prod.exhaust)

lemma alpha_residual_equivp: "equivp alpha_residual"
by (metis alpha_residual_reflp alpha_residual_symp alpha_residual_transp equivpI)


subsection ‹Residuals›

text ‹Residuals are raw residuals quotiented by $\alpha$-equivalence.›

quotient_type
  ('act,'state) residual = "'act::bn × 'state::pt" / "alpha_residual"
  by (fact alpha_residual_equivp)

lemma residual_abs_rep [simp]: "abs_residual (rep_residual res) = res"
by (metis Quotient_residual Quotient_abs_rep)

lemma residual_rep_abs [simp]: "alpha_residual (rep_residual (abs_residual r)) r"
by (metis residual.abs_eq_iff residual_abs_rep)

text ‹The permutation operation is lifted from raw residuals.›

instantiation residual :: (bn,pt) pt
begin

  lift_definition permute_residual :: "perm  ('a,'b) residual  ('a,'b) residual"
    is permute
  by (fact alpha_residual_eqvt)

  instance
  proof
    fix res :: "(_,_) residual"
    show "0  res = res"
      by transfer (metis alpha_residual_equivp equivp_reflp permute_zero)
  next
    fix p q :: perm and res :: "(_,_) residual"
    show "(p + q)  res = p  q  res"
      by transfer (metis alpha_residual_equivp equivp_reflp permute_plus)
  qed

end

text ‹The abstraction function from raw residuals to residuals is equivariant. The representation
function is equivariant modulo $\alpha$-equivalence.›

lemmas permute_residual.abs_eq [eqvt, simp]

lemma alpha_residual_permute_rep_commute [simp]: "alpha_residual (p  rep_residual res) (rep_residual (p  res))"
by (metis residual.abs_eq_iff residual_abs_rep permute_residual.abs_eq)


subsection ‹Notation for pairs as residuals›

abbreviation abs_residual_pair :: "'act::bn  'state::pt  ('act,'state) residual" ("_,_" [0,0] 1000)
where
  "α,P == abs_residual (α,P)"

lemma abs_residual_pair_eqvt [simp]: "p  α,P = p  α, p  P"
by (metis Pair_eqvt permute_residual.abs_eq)


subsection ‹Support of residuals›

text ‹We only consider finitely supported states now.›

lemma supp_abs_residual_pair: "supp α, P::'state::fs = supp (α,P) - bn α"
proof -
  have "supp α,P = supp ([bn α]set. (α, P))"
    by (simp add: supp_def residual.abs_eq_iff bn_eqvt)
  then show ?thesis by (simp add: supp_Abs)
qed

lemma bn_abs_residual_fresh [simp]: "bn α ♯* α,P::'state::fs"
by (simp add: fresh_star_def fresh_def supp_abs_residual_pair)

lemma finite_supp_abs_residual_pair [simp]: "finite (supp α, P::'state::fs)"
by (metis finite_Diff finite_supp supp_abs_residual_pair)


subsection ‹Equality between residuals›

lemma residual_eq_iff_perm: "α1,P1 = α2,P2 
  (p. supp (α1, P1) - bn α1 = supp (α2, P2) - bn α2  (supp (α1, P1) - bn α1) ♯* p  p  (α1, P1) = (α2, P2)  p  bn α1 = bn α2)"
  (is "?l  ?r")
proof
  assume *: "?l"
  then have "[bn α1]set. (α1, P1) = [bn α2]set. (α2, P2)"
    by (simp add: residual.abs_eq_iff)
  then obtain p where "(bn α1, (α1,P1)) ≈set ((=)) supp p (bn α2, (α2,P2))"
    using Abs_eq_iff(1) by blast
  then show "?r"
    by (metis (mono_tags, lifting) alpha_set.simps)
next
  assume *: "?r"
  then obtain p where "(bn α1, (α1,P1)) ≈set ((=)) supp p (bn α2, (α2,P2))"
    using alpha_set.simps by blast
  then have "[bn α1]set. (α1, P1) = [bn α2]set. (α2, P2)"
    using Abs_eq_iff(1) by blast
  then show "?l"
    by (simp add: residual.abs_eq_iff)
qed

lemma residual_eq_iff_perm_renaming: "α1,P1 = α2,P2 
  (p. supp (α1, P1) - bn α1 = supp (α2, P2) - bn α2  (supp (α1, P1) - bn α1) ♯* p  p  (α1, P1) = (α2, P2)  p  bn α1 = bn α2  supp p  bn α1  p  bn α1)"
  (is "?l  ?r")
proof
  assume "?l"
  then obtain p where p: "supp (α1, P1) - bn α1 = supp (α2, P2) - bn α2  (supp (α1, P1) - bn α1) ♯* p  p  (α1, P1) = (α2, P2)  p  bn α1 = bn α2"
    by (metis residual_eq_iff_perm)
  moreover obtain q where q_p: "bbn α1. q  b = p  b" and supp_q: "supp q  bn α1  p  bn α1"
    by (metis set_renaming_perm2)
  have "supp q  supp p"
  proof
    fix a assume *: "a  supp q" then show "a  supp p"
    proof (cases "a  bn α1")
      case True then show ?thesis
        using "*" q_p by (metis mem_Collect_eq supp_perm)
    next
      case False then have "a  p  bn α1"
        using "*" supp_q using UnE subsetCE by blast
      with False have "p  a  a"
        by (metis mem_permute_iff)
      then show ?thesis
        using fresh_def fresh_perm by blast
    qed
  qed
  with p have "(supp (α1, P1) - bn α1) ♯* q"
    by (meson fresh_def fresh_star_def subset_iff)
  moreover with p and q_p have "a. a  supp α1  q  a = p  a" and "a. a  supp P1  q  a = p  a"
    by (metis Diff_iff fresh_perm fresh_star_def UnCI supp_Pair)+
  then have "q  α1 = p  α1" and "q  P1 = p  P1"
    by (metis supp_perm_perm_eq)+
  ultimately show "?r"
    using supp_q by (metis Pair_eqvt bn_eqvt)
next
  assume "?r" then show "?l"
    by (meson residual_eq_iff_perm)
qed


subsection ‹Strong induction›

lemma residual_strong_induct:
  assumes "(act::'act::bn) (state::'state::fs) (c::'a::fs). bn act ♯* c  P c act,state"
  shows "P c residual"
proof (rule residual.abs_induct, clarify)
  fix act :: 'act and state :: 'state
  obtain p where 1: "(p  bn act) ♯* c" and 2: "supp act,state ♯* p"
    proof (rule at_set_avoiding2[of "bn act" c "act,state", THEN exE])
      show "finite (bn act)" by (fact bn_finite)
    next
      show "finite (supp c)" by (fact finite_supp)
    next
      show "finite (supp act,state)" by (fact finite_supp_abs_residual_pair)
    next
      show "bn act ♯* act,state" by (fact bn_abs_residual_fresh)
    qed metis
  from 2 have "p  act, p  state = act,state"
    using supp_perm_eq by fastforce
  then show "P c act,state"
    using assms 1 by (metis bn_eqvt)
qed


subsection ‹Other lemmas›

lemma residual_empty_bn_eq_iff:
  assumes "bn α1 = {}"
  shows "α1,P1 = α2,P2  α1 = α2  P1 = P2"
proof
  assume "α1,P1 = α2,P2"
  with assms have "[{}]set. (α1, P1) = [bn α2]set. (α2, P2)"
    by (simp add: residual.abs_eq_iff)
  then obtain p where "({}, (α1, P1)) ≈set ((=)) supp p (bn α2, (α2, P2))"
    using Abs_eq_iff(1) by blast
  then show "α1 = α2  P1 = P2"
    unfolding alpha_set using supp_perm_eq by fastforce
next
  assume "α1 = α2  P1 = P2" then show "α1,P1 = α2,P2"
    by simp
qed

― ‹The following lemma is not about residuals, but we have no better place for it.›
lemma set_bounded_supp:
  assumes "finite S" and "x. xX  supp x  S"
  shows "supp X  S"
proof -
  have "S supports X"
    unfolding supports_def proof (clarify)
    fix a b
    assume a: "a  S" and b: "b  S"
    {
      fix x
      assume "x  X"
      then have "(a  b)  x = x"
        using a b x. xX  supp x  S by (meson fresh_def subsetCE swap_fresh_fresh)
    }
    then show "(a  b)  X = X"
      by auto (metis (full_types) eqvt_bound mem_permute_iff, metis mem_permute_iff)
  qed
  then show "supp X  S"
    using assms(1) by (fact supp_is_subset)
qed

end

Theory Transition_System

theory Transition_System
imports
  Residual
begin

section ‹Nominal Transition Systems and Bisimulations›

subsection ‹Basic Lemmas›

lemma symp_eqvt [eqvt]:
  assumes "symp R" shows "symp (p  R)"
using assms unfolding symp_def by (subst permute_fun_def)+ (simp add: permute_pure)


subsection ‹Nominal transition systems›

locale nominal_ts =
  fixes satisfies :: "'state::fs  'pred::fs  bool"                (infix "" 70)
    and transition :: "'state  ('act::bn,'state) residual  bool"  (infix "" 70)
  assumes satisfies_eqvt [eqvt]: "P  φ  p  P  p  φ"
      and transition_eqvt [eqvt]: "P  αQ  p  P  p  αQ"
begin

  lemma transition_eqvt':
    assumes "P  α,Q" shows "p  P  p  α, p  Q"
  using assms by (metis abs_residual_pair_eqvt transition_eqvt)

end


subsection ‹Bisimulations›

context nominal_ts
begin

  definition is_bisimulation :: "('state  'state  bool)  bool" where
    "is_bisimulation R 
      symp R 
      (P Q. R P Q  (φ. P  φ  Q  φ)) 
      (P Q. R P Q  (α P'. bn α ♯* Q  P  α,P'  (Q'. Q  α,Q'  R P' Q')))"

  definition bisimilar :: "'state  'state  bool"  (infix "∼⋅" 100) where
    "P ∼⋅ Q  R. is_bisimulation R  R P Q"

  text @{const bisimilar} is an equivariant equivalence relation.›

  lemma is_bisimulation_eqvt (*[eqvt]*):
    assumes "is_bisimulation R" shows "is_bisimulation (p  R)"
  using assms unfolding is_bisimulation_def
  proof (clarify)
    assume 1: "symp R"
    assume 2: "P Q. R P Q  (φ. P  φ  Q  φ)"
    assume 3: "P Q. R P Q  (α P'. bn α ♯* Q  P  α,P'  (Q'. Q  α,Q'  R P' Q'))"
    have "symp (p  R)" (is ?S)
      using 1 by (simp add: symp_eqvt)
    moreover have "P Q. (p  R) P Q  (φ. P  φ  Q  φ)" (is ?T)
      proof (clarify)
        fix P Q φ
        assume *: "(p  R) P Q" and **: "P  φ"
        from * have "R (-p  P) (-p  Q)"
          by (simp add: eqvt_lambda permute_bool_def unpermute_def)
        then show "Q  φ"
          using 2 ** by (metis permute_minus_cancel(1) satisfies_eqvt)
      qed
    moreover have "P Q. (p  R) P Q  (α P'. bn α ♯* Q  P  α,P'  (Q'. Q  α,Q'  (p  R) P' Q'))" (is ?U)
      proof (clarify)
        fix P Q α P'
        assume *: "(p  R) P Q" and **: "bn α ♯* Q" and ***: "P  α,P'"
        from * have "R (-p  P) (-p  Q)"
          by (simp add: eqvt_lambda permute_bool_def unpermute_def)
        moreover have "bn (-p  α) ♯* (-p  Q)"
          using ** by (metis bn_eqvt fresh_star_permute_iff)
        moreover have "-p  P  -p  α, -p  P'"
          using *** by (metis transition_eqvt')
        ultimately obtain Q' where T: "-p  Q  -p  α,Q'" and R: "R (-p  P') Q'"
          using 3 by metis
        from T have "Q  α, p  Q'"
          by (metis permute_minus_cancel(1) transition_eqvt')
        moreover from R have "(p  R) P' (p  Q')"
          by (metis eqvt_apply eqvt_lambda permute_bool_def unpermute_def)
        ultimately show "Q'. Q  α,Q'  (p  R) P' Q'"
          by metis
      qed
    ultimately show "?S  ?T  ?U" by simp
  qed

  lemma bisimilar_eqvt (*[eqvt]*):
    assumes "P ∼⋅ Q" shows "(p  P) ∼⋅ (p  Q)"
  proof -
    from assms obtain R where *: "is_bisimulation R  R P Q"
      unfolding bisimilar_def ..
    then have "is_bisimulation (p  R)"
      by (simp add: is_bisimulation_eqvt)
    moreover from "*" have "(p  R) (p  P) (p  Q)"
      by (metis eqvt_apply permute_boolI)
    ultimately show "(p  P) ∼⋅ (p  Q)"
      unfolding bisimilar_def by auto
  qed

  lemma bisimilar_reflp: "reflp bisimilar"
  proof (rule reflpI)
    fix x
    have "is_bisimulation (=)"
      unfolding is_bisimulation_def by (simp add: symp_def)
    then show "x ∼⋅ x"
      unfolding bisimilar_def by auto
  qed

  lemma bisimilar_symp: "symp bisimilar"
  proof (rule sympI)
    fix P Q
    assume "P ∼⋅ Q"
    then obtain R where *: "is_bisimulation R  R P Q"
      unfolding bisimilar_def ..
    then have "R Q P"
      unfolding is_bisimulation_def by (simp add: symp_def)
    with "*" show "Q ∼⋅ P"
      unfolding bisimilar_def by auto
  qed

  lemma bisimilar_is_bisimulation: "is_bisimulation bisimilar"
  unfolding is_bisimulation_def proof
    show "symp (∼⋅)"
      by (fact bisimilar_symp)
  next
    show "(P Q. P ∼⋅ Q  (φ. P  φ  Q  φ)) 
      (P Q. P ∼⋅ Q  (α P'. bn α ♯* Q  P  α,P'  (Q'. Q  α,Q'  P' ∼⋅ Q')))"
      by (auto simp add: is_bisimulation_def bisimilar_def) blast
  qed

  lemma bisimilar_transp: "transp bisimilar"
  proof (rule transpI)
    fix P Q R
    assume PQ: "P ∼⋅ Q" and QR: "Q ∼⋅ R"
    let ?bisim = "bisimilar OO bisimilar"
    have "symp ?bisim"
      proof (rule sympI)
        fix P R
        assume "?bisim P R"
        then obtain Q where "P ∼⋅ Q" and "Q ∼⋅ R"
          by blast
        then have "R ∼⋅ Q" and "Q ∼⋅ P"
          by (metis bisimilar_symp sympE)+
        then show "?bisim R P"
          by blast
      qed
    moreover have "P Q. ?bisim P Q  (φ. P  φ  Q  φ)"
      using bisimilar_is_bisimulation is_bisimulation_def by auto
    moreover have "P Q. ?bisim P Q 
           (α P'. bn α ♯* Q  P  α,P'  (Q'. Q  α,Q'  ?bisim P' Q'))"
      proof (clarify)
        fix P R Q α P'
        assume PR: "P ∼⋅ R" and RQ: "R ∼⋅ Q" and fresh: "bn α ♯* Q" and trans: "P  α,P'"
        ― ‹rename~@{term "α,P'"} to avoid~@{term R}, without touching~@{term Q}
        obtain p where 1: "(p  bn α) ♯* R" and 2: "supp (α,P', Q) ♯* p"
          proof (rule at_set_avoiding2[of "bn α" R "(α,P', Q)", THEN exE])
            show "finite (bn α)" by (fact bn_finite)
          next
            show "finite (supp R)" by (fact finite_supp)
          next
            show "finite (supp (α,P', Q))" by (simp add: finite_supp supp_Pair)
          next
            show "bn α ♯* (α,P', Q)" by (simp add: fresh fresh_star_Pair)
          qed metis
        from 2 have 3: "supp α,P' ♯* p" and 4: "supp Q ♯* p"
          by (simp add: fresh_star_Un supp_Pair)+
        from 3 have "p  α, p  P' = α,P'"
          using supp_perm_eq by fastforce
        then obtain pR' where 5: "R  p  α, pR'" and 6: "(p  P') ∼⋅ pR'"
          using PR trans 1 by (metis (mono_tags, lifting) bisimilar_is_bisimulation bn_eqvt is_bisimulation_def)
        from fresh and 4 have "bn (p  α) ♯* Q"
          by (metis bn_eqvt fresh_star_permute_iff supp_perm_eq)
        then obtain pQ' where 7: "Q  p  α, pQ'" and 8: "pR' ∼⋅ pQ'"
          using RQ 5 by (metis (full_types) bisimilar_is_bisimulation is_bisimulation_def)
        from 7 have "Q  α, -p  pQ'"
          using 4 by (metis permute_minus_cancel(2) supp_perm_eq transition_eqvt')
        moreover from 6 and 8 have "?bisim P' (-p  pQ')"
          by (metis (no_types, hide_lams) bisimilar_eqvt permute_minus_cancel(2) relcompp.simps)
        ultimately show "Q'. Q  α,Q'  ?bisim P' Q'"
          by metis
      qed
    ultimately have "is_bisimulation ?bisim"
      unfolding is_bisimulation_def by metis
    moreover have "?bisim P R"
      using PQ QR by blast
    ultimately show "P ∼⋅ R"
      unfolding bisimilar_def by meson
  qed

  lemma bisimilar_equivp: "equivp bisimilar"
  by (metis bisimilar_reflp bisimilar_symp bisimilar_transp equivp_reflp_symp_transp)

  lemma bisimilar_simulation_step:
    assumes "P ∼⋅ Q" and "bn α ♯* Q" and "P  α,P'"
    obtains Q' where "Q  α,Q'" and "P' ∼⋅ Q'"
  using assms by (metis (poly_guards_query) bisimilar_is_bisimulation is_bisimulation_def)

end

end

Theory Formula

theory Formula
imports
  Nominal_Bounded_Set
  Nominal_Wellfounded
  Residual
begin

section ‹Infinitary Formulas›

subsection ‹Infinitely branching trees›

text ‹First, we define a type of trees, with a constructor~@{term tConj} that maps (potentially
infinite) sets of trees into trees. To avoid paradoxes (note that there is no injection from the
powerset of trees into the set of trees), the cardinality of the argument set must be bounded.›

datatype ('idx,'pred,'act) Tree =
    tConj "('idx,'pred,'act) Tree set['idx]"  ― ‹potentially infinite sets of trees›
  | tNot "('idx,'pred,'act) Tree"
  | tPred 'pred
  | tAct 'act "('idx,'pred,'act) Tree"

text ‹The (automatically generated) induction principle for trees allows us to prove that the
following relation over trees is well-founded. This will be useful for termination proofs when we
define functions by recursion over trees.›

inductive_set Tree_wf :: "('idx,'pred,'act) Tree rel" where
  "t  set_bset tset  (t, tConj tset)  Tree_wf"
| "(t, tNot t)  Tree_wf"
| "(t, tAct α t)  Tree_wf"

lemma wf_Tree_wf: "wf Tree_wf"
unfolding wf_def
proof (rule allI, rule impI, rule allI)
  fix P :: "('idx,'pred,'act) Tree  bool" and t
  assume "x. (y. (y, x)  Tree_wf  P y)  P x"
  then show "P t"
    proof (induction t)
      case tConj then show ?case
        by (metis Tree.distinct(2) Tree.distinct(5) Tree.inject(1) Tree_wf.cases)
    next
      case tNot then show ?case
        by (metis Tree.distinct(1) Tree.distinct(9) Tree.inject(2) Tree_wf.cases)
    next
      case tPred then show ?case
        by (metis Tree.distinct(11) Tree.distinct(3) Tree.distinct(7) Tree_wf.cases)
    next
      case tAct then show ?case
        by (metis Tree.distinct(10) Tree.distinct(6) Tree.inject(4) Tree_wf.cases)
    qed
qed

text ‹We define a permutation operation on the type of trees.›

instantiation Tree :: (type, pt, pt) pt
begin

  primrec permute_Tree :: "perm  (_,_,_) Tree  (_,_,_) Tree" where
    "p  (tConj tset) = tConj (map_bset (permute p) tset)"  ― ‹neat trick to get around the fact that~@{term tset} is not of permutation type yet›
  | "p  (tNot t) = tNot (p  t)"
  | "p  (tPred φ) = tPred (p  φ)"
  | "p  (tAct α t) = tAct (p  α) (p  t)"

  instance
  proof
    fix t :: "(_,_,_) Tree"
    show "0  t = t"
    proof (induction t)
      case tConj then show ?case
        by (simp, transfer) (auto simp: image_def)
    qed simp_all
  next
    fix p q :: perm and t :: "(_,_,_) Tree"
    show "(p + q)  t = p  q  t"
      proof (induction t)
        case tConj then show ?case
          by (simp, transfer) (auto simp: image_def)
      qed simp_all
  qed

end

text ‹Now that the type of trees---and hence the type of (bounded) sets of trees---is a permutation
type, we can massage the definition of~@{term "p  tConj tset"} into its more usual form.›

lemma permute_Tree_tConj [simp]: "p  tConj tset = tConj (p  tset)"
by (simp add: map_bset_permute)

declare permute_Tree.simps(1) [simp del]

text ‹The relation~@{const Tree_wf} is equivariant.›

lemma Tree_wf_eqvt_aux:
  assumes "(t1, t2)  Tree_wf" shows "(p  t1, p  t2)  Tree_wf"
using assms proof (induction rule: Tree_wf.induct)
  fix t :: "('a,'b,'c) Tree" and tset :: "('a,'b,'c) Tree set['a]"
  assume "t  set_bset tset" then show "(p  t, p  tConj tset)  Tree_wf"
    by (metis Tree_wf.intros(1) mem_permute_iff permute_Tree_tConj set_bset_eqvt)
next
  fix t :: "('a,'b,'c) Tree"
  show "(p  t, p  tNot t)  Tree_wf"
    by (metis Tree_wf.intros(2) permute_Tree.simps(2))
next
  fix t :: "('a,'b,'c) Tree" and α
  show "(p  t, p  tAct α t)  Tree_wf"
    by (metis Tree_wf.intros(3) permute_Tree.simps(4))
qed

lemma Tree_wf_eqvt [eqvt, simp]: "p  Tree_wf = Tree_wf"
proof
  show "p  Tree_wf  Tree_wf"
    by (auto simp add: permute_set_def) (rule Tree_wf_eqvt_aux)
next
  show "Tree_wf  p  Tree_wf"
    by (auto simp add: permute_set_def) (metis Tree_wf_eqvt_aux permute_minus_cancel(1))
qed

lemma Tree_wf_eqvt': "eqvt Tree_wf"
by (metis Tree_wf_eqvt eqvtI)

text ‹The definition of~@{const permute} for trees gives rise to the usual notion of support. The
following lemmas, one for each constructor, describe the support of trees.›

lemma supp_tConj [simp]: "supp (tConj tset) = supp tset"
unfolding supp_def by simp

lemma supp_tNot [simp]: "supp (tNot t) = supp t"
unfolding supp_def by simp

lemma supp_tPred [simp]: "supp (tPred φ) = supp φ"
unfolding supp_def by simp

lemma supp_tAct [simp]: "supp (tAct α t) = supp α  supp t"
unfolding supp_def by (simp add: Collect_imp_eq Collect_neg_eq)


subsection ‹Trees modulo \texorpdfstring{$\alpha$}{alpha}-equivalence›

text ‹We generalize the notion of support, which considers whether a permuted element is
\emph{equal} to itself, to arbitrary endorelations. This is available as @{const supp_rel} in
Nominal Isabelle.›

lemma supp_rel_eqvt [eqvt]:
  "p  supp_rel R x = supp_rel (p  R) (p  x)"
by (simp add: supp_rel_def)

text ‹Usually, the definition of $\alpha$-equivalence presupposes a notion of free variables.
However, the variables that are ``free'' in an infinitary conjunction are not necessarily those
that are free in one of the conjuncts. For instance, consider a conjunction over \emph{all} names.
Applying any permutation will yield the same conjunction, i.e., this conjunction has \emph{no} free
variables.

To obtain the correct notion of free variables for infinitary conjunctions, we initially defined
$\alpha$-equivalence and free variables via mutual recursion. In particular, we defined the free
variables of a conjunction as term @{term "fv_Tree (tConj tset) = supp_rel alpha_Tree (tConj tset)"}.

We then realized that it is not necessary to define the concept of ``free variables'' at all, but
the definition of $\alpha$-equivalence becomes much simpler (in particular, it is no longer mutually
recursive) if we directly use the support modulo $\alpha$-equivalence.›

text ‹The following lemmas and constructions are used to prove termination of our definition.›

lemma supp_rel_cong [fundef_cong]:
  " x=x'; a b. R ((a  b)  x') x'  R' ((a  b)  x') x'   supp_rel R x = supp_rel R' x'"
by (simp add: supp_rel_def)

lemma rel_bset_cong [fundef_cong]:
  " x=x'; y=y'; a b. a  set_bset x'  b  set_bset y'  R a b  R' a b   rel_bset R x y  rel_bset R' x' y'"
by (simp add: rel_bset_def rel_set_def)

lemma alpha_set_cong [fundef_cong]:
  " bs=bs'; x=x'; R (p'  x') y'  R' (p'  x') y'; f x' = f' x'; f y' = f' y'; p=p'; cs=cs'; y=y'  
    alpha_set (bs, x) R f p (cs, y)  alpha_set (bs', x') R' f' p' (cs', y')"
by (simp add: alpha_set)

quotient_type
  ('idx,'pred,'act) Treep = "('idx,'pred::pt,'act::bn) Tree" / "hull_relp"
  by (fact hull_relp_equivp)

lemma abs_Treep_eq [simp]: "abs_Treep (p  t) = abs_Treep t"
by (metis hull_relp.simps Treep.abs_eq_iff)

lemma permute_rep_abs_Treep:
  obtains p where "rep_Treep (abs_Treep t) = p  t"
by (metis Quotient3_Treep Treep.abs_eq_iff rep_abs_rsp hull_relp.simps)

lift_definition Tree_wfp :: "('idx,'pred::pt,'act::bn) Treep rel" is
  Tree_wf .

lemma Tree_wfpI [simp]:
  assumes "(a, b)  Tree_wf"
  shows "(abs_Treep (p  a), abs_Treep b)  Tree_wfp"
using assms by (metis (erased, lifting) Treep.abs_eq_iff Tree_wfp.abs_eq hull_relp.intros map_prod_simp rev_image_eqI)

lemma Tree_wfp_trivialI [simp]:
  assumes "(a, b)  Tree_wf"
  shows "(abs_Treep a, abs_Treep b)  Tree_wfp"
using assms by (metis Tree_wfpI permute_zero)

lemma Tree_wfpE:
  assumes "(ap, bp)  Tree_wfp"
  obtains a b where "ap = abs_Treep a" and "bp = abs_Treep b" and "(a,b)  Tree_wf"
using assms by (metis Pair_inject Tree_wfp.abs_eq prod_fun_imageE)

lemma wf_Tree_wfp: "wf Tree_wfp"
proof (rule wf_subset[of "inv_image (hull_rel O Tree_wf) rep_Treep"])
  show "wf (inv_image (hull_rel O Tree_wf) rep_Treep)"
    by (metis Tree_wf_eqvt' wf_Tree_wf wf_hull_rel_relcomp wf_inv_image)
next
  show "Tree_wfp  inv_image (hull_rel O Tree_wf) rep_Treep"
  proof (standard, case_tac "x", clarify)
    fix ap bp :: "('d, 'e, 'f) Treep"
    assume "(ap, bp)  Tree_wfp"
    then obtain a b where 1: "ap = abs_Treep a" and 2: "bp = abs_Treep b" and 3: "(a,b)  Tree_wf"
      by (rule Tree_wfpE)
    from 1 obtain p where 4: "rep_Treep ap = p  a"
      by (metis permute_rep_abs_Treep)
    from 2 obtain q where 5: "rep_Treep bp = q  b"
      by (metis permute_rep_abs_Treep)
    have "(p  a, q  a)  hull_rel"
      by (metis hull_rel.simps permute_minus_cancel(2) permute_plus)
    moreover from 3 have "(q  a, q  b)  Tree_wf"
      by (rule Tree_wf_eqvt_aux)
    ultimately show "(ap, bp)  inv_image (hull_rel O Tree_wf) rep_Treep"
      using 4 5 by auto
  qed
qed

fun alpha_Tree_termination :: "('a, 'b, 'c) Tree × ('a, 'b, 'c) Tree  ('a, 'b::pt, 'c::bn) Treep set" where
  "alpha_Tree_termination (t1, t2) = {abs_Treep t1, abs_Treep t2}"

text ‹Here it comes \ldots›

function (sequential)
  alpha_Tree :: "('idx,'pred::pt,'act::bn) Tree  ('idx,'pred,'act) Tree  bool" (infix "=α" 50) where
― ‹@{const alpha_Tree}
  alpha_tConj: "tConj tset1 =α tConj tset2  rel_bset alpha_Tree tset1 tset2"
| alpha_tNot: "tNot t1 =α tNot t2  t1 =α t2"
| alpha_tPred: "tPred φ1 =α tPred φ2  φ1 = φ2"
― ‹the action may have binding names›
| alpha_tAct: "tAct α1 t1 =α tAct α2 t2 
    (p. (bn α1, t1) ≈set alpha_Tree (supp_rel alpha_Tree) p (bn α2, t2)  (bn α1, α1) ≈set ((=)) supp p (bn α2, α2))"
| alpha_other: "_ =α _  False"
― ‹254 subgoals (!)›
by pat_completeness auto
termination
proof
  let ?R = "inv_image (max_ext Tree_wfp) alpha_Tree_termination"
  show "wf ?R"
    by (metis max_ext_wf wf_Tree_wfp wf_inv_image)
qed (auto simp add: max_ext.simps Tree_wf.simps simp del: permute_Tree_tConj)

text ‹We provide more descriptive case names for the automatically generated induction principle.›

lemmas alpha_Tree_induct' = alpha_Tree.induct[case_names alpha_tConj alpha_tNot
  alpha_tPred alpha_tAct "alpha_other(1)" "alpha_other(2)" "alpha_other(3)" "alpha_other(4)"
  "alpha_other(5)" "alpha_other(6)" "alpha_other(7)" "alpha_other(8)" "alpha_other(9)"
  "alpha_other(10)" "alpha_other(11)" "alpha_other(12)" "alpha_other(13)" "alpha_other(14)"
  "alpha_other(15)" "alpha_other(16)" "alpha_other(17)" "alpha_other(18)"]

lemma alpha_Tree_induct[case_names tConj tNot tPred tAct, consumes 1]:
  assumes "t1 =α t2"
  and "tset1 tset2. (a b. a  set_bset tset1  b  set_bset tset2  a =α b  P a b) 
            rel_bset (=α) tset1 tset2  P (tConj tset1) (tConj tset2)"
  and "t1 t2. t1 =α t2  P t1 t2  P (tNot t1) (tNot t2)"
  and "φ. P (tPred φ) (tPred φ)"
  and "α1 t1 α2 t2. (p. p  t1 =α t2  P (p  t1) t2) 
            (a b. ((a  b)  t1) =α t1  P ((a  b)  t1) t1)  (a b. ((a  b)  t2) =α t2  P ((a  b)  t2) t2) 
            (p. (bn α1, t1) ≈set (=α) (supp_rel (=α)) p (bn α2, t2)  (bn α1, α1) ≈set (=) supp p (bn α2, α2)) 
            P (tAct α1 t1) (tAct α2 t2)"
  shows "P t1 t2"
using assms by (induction t1 t2 rule: alpha_Tree.induct) simp_all

text ‹$\alpha$-equivalence is equivariant.›

lemma alpha_Tree_eqvt_aux:
  assumes "a b. (a  b)  t =α t  p  (a  b)  t =α p  t"
  shows "p  supp_rel (=α) t = supp_rel (=α) (p  t)"
proof -
  {
    fix a
    let ?B = "{b. ¬ ((a  b)  t) =α t}"
    let ?pB = "{b. ¬ ((p  a  b)  p  t) =α (p  t)}"
    {
      assume "finite ?B"
      moreover have "inj_on (unpermute p) ?pB"
        by (simp add: inj_on_def unpermute_def)
      moreover have "unpermute p ` ?pB  ?B"
        using assms by auto (metis (erased, lifting) eqvt_bound permute_eqvt swap_eqvt)
      ultimately have "finite ?pB"
        by (metis inj_on_finite)
    }
    moreover
    {
      assume "finite ?pB"
      moreover have "inj_on (permute p) ?B"
        by (simp add: inj_on_def)
      moreover have "permute p ` ?B  ?pB"
        using assms by auto (metis (erased, lifting) permute_eqvt swap_eqvt)
      ultimately have "finite ?B"
        by (metis inj_on_finite)
    }
    ultimately have "infinite ?B  infinite ?pB"
      by auto
  }
  then show ?thesis
    by (auto simp add: supp_rel_def permute_set_def) (metis eqvt_bound)
qed

lemma alpha_Tree_eqvt': "t1 =α t2  p  t1 =α p  t2"
proof (induction t1 t2 rule: alpha_Tree_induct')
  case (alpha_tConj tset1 tset2) show ?case
  proof
    assume *: "tConj tset1 =α tConj tset2"
    {
      fix x
      assume "x  set_bset (p  tset1)"
      then obtain x' where 1: "x'  set_bset tset1" and 2: "x = p  x'"
        by (metis imageE permute_bset.rep_eq permute_set_eq_image)
      from 1 obtain y' where 3: "y'  set_bset tset2" and 4: "x' =α y'"
        using "*" by (metis (mono_tags, lifting) Formula.alpha_tConj rel_bset.rep_eq rel_set_def)
      from 3 have "p  y'  set_bset (p  tset2)"
        by (metis mem_permute_iff set_bset_eqvt)
      moreover from 1 and 2 and 3 and 4 have "x =α p  y'"
        using alpha_tConj.IH by blast
      ultimately have "yset_bset (p  tset2). x =α y" ..
    }
    moreover
    {
      fix y
      assume "y  set_bset (p  tset2)"
      then obtain y' where 1: "y'  set_bset tset2" and 2: "p  y' = y"
        by (metis imageE permute_bset.rep_eq permute_set_eq_image)
      from 1 obtain x' where 3: "x'  set_bset tset1" and 4: "x' =α y'"
        using "*" by (metis (mono_tags, lifting) Formula.alpha_tConj rel_bset.rep_eq rel_set_def)
      from 3 have "p  x'  set_bset (p  tset1)"
        by (metis mem_permute_iff set_bset_eqvt)
      moreover from 1 and 2 and 3 and 4 have "p  x' =α y"
        using alpha_tConj.IH by blast
      ultimately have "xset_bset (p  tset1). x =α y" ..
    }
    ultimately show "p  tConj tset1 =α p  tConj tset2"
      by (simp add: rel_bset_def rel_set_def)
  next
    assume *: "p  tConj tset1 =α p  tConj tset2"
    {
      fix x
      assume 1: "x  set_bset tset1"
      then have "p  x  set_bset (p  tset1)"
        by (metis mem_permute_iff set_bset_eqvt)
      then obtain y' where 2: "y'  set_bset (p  tset2)" and 3: "p  x =α y'"
        using "*" by (metis Formula.alpha_tConj permute_Tree_tConj rel_bset.rep_eq rel_set_def)
      from 2 obtain y where 4: "y  set_bset tset2" and 5: "y' = p  y"
        by (metis imageE permute_bset.rep_eq permute_set_eq_image)
      from 1 and 3 and 4 and 5 have "x =α y"
        using alpha_tConj.IH by blast
      with 4 have "yset_bset tset2. x =α y" ..
    }
    moreover
    {
      fix y
      assume 1: "y  set_bset tset2"
      then have "p  y  set_bset (p  tset2)"
        by (metis mem_permute_iff set_bset_eqvt)
      then obtain x' where 2: "x'  set_bset (p  tset1)" and 3: "x' =α p  y"
        using "*" by (metis Formula.alpha_tConj permute_Tree_tConj rel_bset.rep_eq rel_set_def)
      from 2 obtain x where 4: "x  set_bset tset1" and 5: "p  x = x'"
        by (metis imageE permute_bset.rep_eq permute_set_eq_image)
      from 1 and 3 and 4 and 5 have "x =α y"
        using alpha_tConj.IH by blast
      with 4 have "xset_bset tset1. x =α y" ..
    }
    ultimately show "tConj tset1 =α tConj tset2"
      by (simp add: rel_bset_def rel_set_def)
  qed
next
  case (alpha_tAct α1 t1 α2 t2)
  from alpha_tAct.IH(2) have t1: "p  supp_rel (=α) t1 = supp_rel (=α) (p  t1)"
    by (rule alpha_Tree_eqvt_aux)
  from alpha_tAct.IH(3) have t2: "p  supp_rel (=α) t2 = supp_rel (=α) (p  t2)"
    by (rule alpha_Tree_eqvt_aux)
  show ?case
  proof
    assume "tAct α1 t1 =α tAct α2 t2"
    then obtain q where 1: "(bn α1, t1) ≈set (=α) (supp_rel (=α)) q (bn α2, t2)" and 2: "(bn α1, α1) ≈set (=) supp q (bn α2, α2)"
      by auto
    from 1 and t1 and t2 have "supp_rel (=α) (p  t1) - bn (p  α1) = supp_rel (=α) (p  t2) - bn (p  α2)"
      by (metis Diff_eqvt alpha_set bn_eqvt)
    moreover from 1 and t1 have "(supp_rel (=α) (p  t1) - bn (p  α1)) ♯* (p + q - p)"
      by (metis Diff_eqvt alpha_set bn_eqvt fresh_star_permute_iff permute_perm_def)
    moreover from 1 and alpha_tAct.IH(1) have "p  q  t1 =α p  t2"
      by (simp add: alpha_set)
    moreover from 2 have "p  q  -p  bn (p  α1) = bn (p  α2)"
      by (simp add: alpha_set bn_eqvt)
    ultimately have "(bn (p  α1), p  t1) ≈set (=α) (supp_rel (=α)) (p + q - p) (bn (p  α2), p  t2)"
      by (simp add: alpha_set)
    moreover from 2 have "(bn (p  α1), p  α1) ≈set (=) supp (p + q - p) (bn (p  α2), p  α2)"
      by (simp add: alpha_set) (metis (mono_tags, lifting) Diff_eqvt bn_eqvt fresh_star_permute_iff permute_minus_cancel(2) permute_perm_def supp_eqvt)
    ultimately show "p  tAct α1 t1 =α p  tAct α2 t2"
      by auto
  next
    assume "p  tAct α1 t1 =α p  tAct α2 t2"
    then obtain q where 1: "(bn (p  α1), p  t1) ≈set (=α) (supp_rel (=α)) q (bn (p  α2), p  t2)" and 2: "(bn (p  α1), p  α1) ≈set (=) supp q (bn (p  α2), p  α2)"
      by auto
    {
      from 1 and t1 and t2 have "supp_rel (=α) t1 - bn α1 = supp_rel (=α) t2 - bn α2"
        by (metis (no_types, lifting) Diff_eqvt alpha_set bn_eqvt permute_eq_iff)
      moreover with 1 and t2 have "(supp_rel (=α) t1 - bn α1) ♯* (- p + q + p)"
        by (auto simp add: fresh_star_def fresh_perm alphas) (metis (no_types, lifting) DiffI bn_eqvt mem_permute_iff permute_minus_cancel(2))
      moreover from 1 have "- p  q  p  t1 =α t2"
        using alpha_tAct.IH(1) by (simp add: alpha_set) (metis (no_types, lifting) permute_eqvt permute_minus_cancel(2))
      moreover from 1 have "- p  q  p  bn α1 = bn α2"
        by (metis alpha_set bn_eqvt permute_minus_cancel(2))
      ultimately have "(bn α1, t1) ≈set (=α) (supp_rel (=α)) (-p + q + p) (bn α2, t2)"
        by (simp add: alpha_set)
    }
    moreover
    {
      from 2 have "supp α1 - bn α1 = supp α2 - bn α2"
        by (metis (no_types, lifting) Diff_eqvt alpha_set bn_eqvt permute_eq_iff supp_eqvt)
      moreover with 2 have "(supp α1 - bn α1) ♯* (-p + q + p)"
        by (auto simp add: fresh_star_def fresh_perm alphas) (metis (no_types, lifting) DiffI bn_eqvt mem_permute_iff permute_minus_cancel(1) supp_eqvt)
      moreover from 2 have "-p  q  p  α1 = α2"
        by (simp add: alpha_set)
      moreover have "-p  q  p  bn α1 = bn α2"
        by (simp add: bn_eqvt calculation(3))
      ultimately have "(bn α1, α1) ≈set (=) supp (-p + q + p) (bn α2, α2)"
        by (simp add: alpha_set)
    }
    ultimately show "tAct α1 t1 =α tAct α2 t2"
      by auto
  qed
qed simp_all

lemma alpha_Tree_eqvt [eqvt]: "t1 =α t2  p  t1 =α p  t2"
by (metis alpha_Tree_eqvt')

text @{const alpha_Tree} is an equivalence relation.›

lemma alpha_Tree_reflp: "reflp alpha_Tree"
proof (rule reflpI)
  fix t :: "('a,'b,'c) Tree"
  show "t =α t"
  proof (induction t)
    case tConj then show ?case by (metis alpha_tConj rel_bset.rep_eq rel_setI)
  next
    case tNot then show ?case by (metis alpha_tNot)
  next
    case tPred show ?case by (metis alpha_tPred)
  next
    case tAct then show ?case by (metis (mono_tags) alpha_tAct alpha_refl(1))
  qed
qed

lemma alpha_Tree_symp: "symp alpha_Tree"
proof (rule sympI)
  fix x y :: "('a,'b,'c) Tree"
  assume "x =α y" then show "y =α x"
  proof (induction x y rule: alpha_Tree_induct)
    case tConj then show ?case
      by (simp add: rel_bset_def rel_set_def) metis
  next
    case (tAct α1 t1 α2 t2)
    then obtain p where "(bn α1, t1) ≈set (=α) (supp_rel (=α)) p (bn α2, t2)  (bn α1, α1) ≈set (=) supp p (bn α2, α2)"
      by auto
    then have "(bn α2, t2) ≈set (=α) (supp_rel (=α)) (-p) (bn α1, t1)  (bn α2, α2) ≈set (=) supp (-p) (bn α1, α1)"
      using tAct.IH by (metis (mono_tags, lifting) alpha_Tree_eqvt alpha_sym(1) permute_minus_cancel(2))
    then show ?case
      by auto
  qed simp_all
qed

lemma alpha_Tree_transp: "transp alpha_Tree"
proof (rule transpI)
  fix x y z:: "('a,'b,'c) Tree"
  assume "x =α y" and "y =α z"
  then show "x =α z"
  proof (induction x y arbitrary: z rule: alpha_Tree_induct)
    case (tConj tset_x tset_y) show ?case
      proof (cases z)
        fix tset_z
        assume z: "z = tConj tset_z"
        have "rel_bset (=α) tset_x tset_z"
          unfolding rel_bset.rep_eq rel_set_def Ball_def Bex_def
          proof
            show "x'. x'  set_bset tset_x  (z'. z'  set_bset tset_z  x' =α z')"
            proof (rule allI, rule impI)
              fix x' assume 1: "x'  set_bset tset_x"
              then obtain y' where 2: "y'  set_bset tset_y" and 3: "x' =α y'"
                by (metis rel_bset.rep_eq rel_set_def tConj.hyps)
              from 2 obtain z' where 4: "z'  set_bset tset_z" and 5: "y' =α z'"
                by (metis alpha_tConj rel_bset.rep_eq rel_set_def tConj.prems z)
              from 1 2 3 5 have "x' =α z'"
                by (rule tConj.IH)
              with 4 show "z'. z'  set_bset tset_z  x' =α z'"
                by auto
            qed
          next
            show "z'. z'  set_bset tset_z  (x'. x'  set_bset tset_x  x' =α z')"
            proof (rule allI, rule impI)
              fix z' assume 1: "z'  set_bset tset_z"
              then obtain y' where 2: "y'  set_bset tset_y" and 3: "y' =α z'"
                by (metis alpha_tConj rel_bset.rep_eq rel_set_def tConj.prems z)
              from 2 obtain x' where 4: "x'  set_bset tset_x" and 5: "x' =α y'"
                by (metis rel_bset.rep_eq rel_set_def tConj.hyps)
              from 4 2 5 3 have "x' =α z'"
                by (rule tConj.IH)
              with 4 show "x'. x'  set_bset tset_x  x' =α z'"
                by auto
            qed
          qed
        with z show "tConj tset_x =α z"
          by simp
      qed (insert tConj.prems, auto)
  next
    case tNot then show ?case
      by (cases z) simp_all
  next
    case tPred then show ?case
      by simp
  next
    case (tAct α1 t1 α2 t2) show ?case
    proof (cases z)
      fix α t
      assume z: "z = tAct α t"
      obtain p where 1: "(bn α1, t1) ≈set (=α) (supp_rel (=α)) p (bn α2, t2)  (bn α1, α1) ≈set (=) supp p (bn α2, α2)"
        using tAct.hyps by auto
      obtain q where 2: "(bn α2, t2) ≈set (=α) (supp_rel (=α)) q (bn α, t)  (bn α2, α2) ≈set (=) supp q (bn α, α)"
        using tAct.prems z by auto
      have "(bn α1, t1) ≈set (=α) (supp_rel (=α)) (q + p) (bn α, t)"
        proof -
          have "supp_rel (=α) t1 - bn α1 = supp_rel (=α) t - bn α"
            using 1 and 2 by (metis alpha_set)
          moreover have "(supp_rel (=α) t1 - bn α1) ♯* (q + p)"
            using 1 and 2 by (metis alpha_set fresh_star_plus)
          moreover have "(q + p)  t1 =α t"
            using 1 and 2 and tAct.IH by (metis (no_types, lifting) alpha_Tree_eqvt alpha_set permute_minus_cancel(1) permute_plus)
          moreover have "(q + p)  bn α1 = bn α"
            using 1 and 2 by (metis alpha_set permute_plus)
          ultimately show ?thesis
            by (metis alpha_set)
        qed
      moreover have "(bn α1, α1) ≈set (=) supp (q + p) (bn α, α)"
        using 1 and 2 by (metis (mono_tags) alpha_trans(1) permute_plus)
      ultimately show "tAct α1 t1 =α z"
        using z by auto
    qed (insert tAct.prems, auto)
  qed
qed

lemma alpha_Tree_equivp: "equivp alpha_Tree"
by (auto intro: equivpI alpha_Tree_reflp alpha_Tree_symp alpha_Tree_transp)

text ‹$alpha$-equivalent trees have the same support modulo $alpha$-equivalence.›

lemma alpha_Tree_supp_rel:
  assumes "t1 =α t2"
  shows "supp_rel (=α) t1 = supp_rel (=α) t2"
using assms proof (induction rule: alpha_Tree_induct)
  case (tConj tset1 tset2)
  have sym: "x y. rel_bset (=α) x y  rel_bset (=α) y x"
    by (meson alpha_Tree_symp bset.rel_symp sympE)
  {
    fix a b
    from tConj.hyps have *: "rel_bset (=α) ((a  b)  tset1) ((a  b)  tset2)"
      by (metis alpha_tConj alpha_Tree_eqvt permute_Tree_tConj)
    have "rel_bset (=α) ((a  b)  tset1) tset1  rel_bset (=α) ((a  b)  tset2) tset2"
      by (rule iffI) (metis "*" alpha_Tree_transp bset.rel_transp sym tConj.hyps transpE)+
  }
  then show ?case
    by (simp add: supp_rel_def)
next
  case tNot then show ?case
    by (simp add: supp_rel_def)
next
  case (tAct α1 t1 α2 t2)
  {
    fix a b
    have "tAct α1 t1 =α tAct α2 t2"
      using tAct.hyps by simp
    then have "(a  b)  tAct α1 t1 =α tAct α1 t1  (a  b)  tAct α2 t2 =α tAct α2 t2"
      by (metis (no_types, lifting) alpha_Tree_eqvt alpha_Tree_symp alpha_Tree_transp sympE transpE)
  }
  then show ?case
    by (simp add: supp_rel_def)
qed simp_all

text @{const tAct} preserves $\alpha$-equivalence.›

lemma alpha_Tree_tAct:
  assumes "t1 =α t2"
  shows "tAct α t1 =α tAct α t2"
proof -
  have "(bn α, t1) ≈set (=α) (supp_rel (=α)) 0 (bn α, t2)"
    using assms by (simp add: alpha_Tree_supp_rel alpha_set fresh_star_zero)
  moreover have "(bn α, α) ≈set (=) supp 0 (bn α, α)"
    by (metis (full_types) alpha_refl(1))
  ultimately show ?thesis
    by auto
qed

text ‹The following lemmas describe the support modulo $alpha$-equivalence.›

lemma supp_rel_tNot [simp]: "supp_rel (=α) (tNot t) = supp_rel (=α) t"
unfolding supp_rel_def by simp

lemma supp_rel_tPred [simp]: "supp_rel (=α) (tPred φ) = supp φ"
unfolding supp_rel_def supp_def by simp

text ‹The support modulo $\alpha$-equivalence of~@{term "tAct α t"} is not easily described:
when~@{term t} has infinite support (modulo $\alpha$-equivalence), the support (modulo
$\alpha$-equivalence) of~@{term "tAct α t"} may still contain names in~@{term "bn α"}. This
incongruity is avoided when~@{term t} has finite support modulo $\alpha$-equivalence.›

lemma infinite_mono: "infinite S  (x. x  S  x  T)  infinite T"
by (metis infinite_super subsetI)

lemma supp_rel_tAct [simp]:
  assumes "finite (supp_rel (=α) t)"
  shows "supp_rel (=α) (tAct α t) = supp α  supp_rel (=α) t - bn α"
proof
  show "supp α  supp_rel (=α) t - bn α  supp_rel (=α) (tAct α t)"
  proof
    fix x
    assume "x  supp α  supp_rel (=α) t - bn α"
    moreover
    {
      assume x1: "x  supp α" and x2: "x  bn α"
      from x1 have "infinite {b. (x  b)  α  α}"
        unfolding supp_def ..
      then have "infinite ({b. (x  b)  α  α} - supp α)"
        by (simp add: finite_supp)
      moreover
      {
        fix b
        assume "b  {b. (x  b)  α  α} - supp α"
        then have b1: "(x  b)  α  α" and b2: "b  supp α - bn α"
          by simp+
        from b1 have "sort_of x = sort_of b"
          using swap_different_sorts by fastforce
        then have "(x  b)  (supp α - bn α)  supp α - bn α"
          using b2 x1 x2 by (simp add: swap_set_in)
        then have "b  {b. ¬ (x  b)  tAct α t =α tAct α t}"
          by (auto simp add: alpha_set Diff_eqvt bn_eqvt)
      }
      ultimately have "infinite {b. ¬ (x  b)  tAct α t =α tAct α t}"
        by (rule infinite_mono)
      then have "x  supp_rel (=α) (tAct α t)"
        unfolding supp_rel_def ..
    }
    moreover
    {
      assume x1: "x  supp_rel (=α) t" and x2: "x  bn α"
      from x1 have "infinite {b. ¬ (x  b)  t =α t}"
        unfolding supp_rel_def ..
      then have "infinite ({b. ¬ (x  b)  t =α t} - supp_rel (=α) t)"
        using assms by simp
      moreover
      {
        fix b
        assume "b  {b. ¬ (x  b)  t =α t} - supp_rel (=α) t"
        then have b1: "¬ (x  b)  t =α t" and b2: "b  supp_rel (=α) t - bn α"
          by simp+
        from b1 have "(x  b)  t  t"
          by (metis alpha_Tree_reflp reflpE)
        then have "sort_of x = sort_of b"
          using swap_different_sorts by fastforce
        then have "(x  b)  (supp_rel (=α) t - bn α)  supp_rel (=α) t - bn α"
          using b2 x1 x2 by (simp add: swap_set_in)
        then have "supp_rel (=α) ((x  b)  t) - bn ((x  b)  α)  supp_rel (=α) t - bn α"
          by (simp add: Diff_eqvt bn_eqvt)
        then have "b  {b. ¬ (x  b)  tAct α t =α tAct α t}"
          by (simp add: alpha_set)
      }
      ultimately have "infinite {b. ¬ (x  b)  tAct α t =α tAct α t}"
        by (rule infinite_mono)
      then have "x  supp_rel (=α) (tAct α t)"
        unfolding supp_rel_def ..
    }
    ultimately show "x  supp_rel (=α) (tAct α t)"
      by auto
  qed
next
  show "supp_rel (=α) (tAct α t)  supp α  supp_rel (=α) t - bn α"
  proof
    fix x
    assume "x  supp_rel (=α) (tAct α t)"
    then have *: "infinite {b. ¬ (x  b)  tAct α t =α tAct α t}"
      unfolding supp_rel_def ..
    moreover
    {
      fix b
      assume "¬ (x  b)  tAct α t =α tAct α t"
      then have "(x  b)  α  α  ¬ (x  b)  t =α t"
        using alpha_Tree_tAct by force
    }
    ultimately have "infinite {b. (x  b)  α  α  ¬ (x  b)  t =α t}"
      by (metis (mono_tags, lifting) infinite_mono mem_Collect_eq)
    then have "infinite {b. (x  b)  α  α}  infinite {b. ¬ (x  b)  t =α t}"
      by (metis (mono_tags) finite_Collect_disjI)
    then have "x  supp α  supp_rel (=α) t"
      by (simp add: supp_def supp_rel_def)
    moreover
    {
      assume **: "x  bn α"
      from "*" obtain b where b1: "¬ (x  b)  tAct α t =α tAct α t" and b2: "b  supp α" and b3: "b  supp_rel (=α) t"
        using assms by (metis (no_types, lifting) UnCI finite_UnI finite_supp infinite_mono mem_Collect_eq)
      let ?p = "(x  b)"
      have "supp_rel (=α) ((x  b)  t) - bn ((x  b)  α) = supp_rel (=α) t - bn α"
        using "**" and b3 by (metis (no_types, lifting) Diff_eqvt Diff_iff alpha_Tree_eqvt' alpha_Tree_eqvt_aux bn_eqvt swap_set_not_in)
      moreover then have "(supp_rel (=α) ((x  b)  t) - bn ((x  b)  α)) ♯* ?p"
        using "**" and b3 by (metis Diff_iff fresh_perm fresh_star_def swap_atom_simps(3))
      moreover have "?p  (x  b)  t =α t"
        using alpha_Tree_reflp reflpE by force
      moreover have "?p  bn ((x  b)  α) = bn α"
        by (simp add: bn_eqvt)
      moreover have "supp ((x  b)  α) - bn ((x  b)  α) = supp α - bn α"
        using "**" and b2 by (metis (mono_tags, hide_lams) Diff_eqvt Diff_iff bn_eqvt supp_eqvt swap_set_not_in)
      moreover then have "(supp ((x  b)  α) - bn ((x  b)  α)) ♯* ?p"
        using "**" and b2 by (simp add: fresh_star_def fresh_def supp_perm) (metis Diff_iff swap_atom_simps(3))
      moreover have "?p  (x  b)  α = α"
        by simp
      ultimately have "(x  b)  tAct α t =α tAct α t"
        by (auto simp add: alpha_set)
      with b1 have "False" ..
    }
    ultimately show "x  supp α  supp_rel (=α) t - bn α"
      by blast
  qed
qed

text ‹We define the type of (infinitely branching) trees quotiented by $\alpha$-equivalence.›

(* FIXME: No map function defined. No relator found. *)
quotient_type
  ('idx,'pred,'act) Treeα = "('idx,'pred::pt,'act::bn) Tree" / "alpha_Tree"
  by (fact alpha_Tree_equivp)

lemma Treeα_abs_rep [simp]: "abs_Treeα (rep_Treeα tα) = tα"
by (metis Quotient_Treeα Quotient_abs_rep)

lemma Treeα_rep_abs [simp]: "rep_Treeα (abs_Treeα t) =α t"
by (metis Treeα.abs_eq_iff Treeα_abs_rep)

text ‹The permutation operation is lifted from trees.›

instantiation Treeα :: (type, pt, bn) pt
begin

  lift_definition permute_Treeα :: "perm  ('a,'b,'c) Treeα  ('a,'b,'c) Treeα"
    is permute
  by (fact alpha_Tree_eqvt)

  instance
  proof
    fix tα :: "(_,_,_) Treeα"
    show "0  tα = tα"
      by transfer (metis alpha_Tree_equivp equivp_reflp permute_zero)
  next
    fix p q :: perm and tα :: "(_,_,_) Treeα"
    show "(p + q)  tα = p  q  tα"
      by transfer (metis alpha_Tree_equivp equivp_reflp permute_plus)
  qed

end

text ‹The abstraction function from trees to trees modulo $\alpha$-equivalence is equivariant. The
representation function is equivariant modulo $\alpha$-equivalence.›

lemmas permute_Treeα.abs_eq [eqvt, simp]

lemma alpha_Tree_permute_rep_commute [simp]: "p  rep_Treeα tα =α rep_Treeα (p  tα)"
by (metis Treeα.abs_eq_iff Treeα_abs_rep permute_Treeα.abs_eq)


subsection ‹Constructors for trees modulo \texorpdfstring{$\alpha$}{alpha}-equivalence›

text ‹The constructors are lifted from trees.›

lift_definition Conjα :: "('idx,'pred,'act) Treeα set['idx]  ('idx,'pred::pt,'act::bn) Treeα" is
  tConj
by simp

lemma map_bset_abs_rep_Treeα: "map_bset abs_Treeα (map_bset rep_Treeα tsetα) = tsetα"
by (metis (full_types) Quotient_Treeα Quotient_abs_rep bset_lifting.bset_quot_map)

lemma Conjα_def': "Conjα tsetα = abs_Treeα (tConj (map_bset rep_Treeα tsetα))"
by (metis Conjα.abs_eq map_bset_abs_rep_Treeα)

lift_definition Notα :: "('idx,'pred,'act) Treeα  ('idx,'pred::pt,'act::bn) Treeα" is
  tNot
by simp

lift_definition Predα :: "'pred  ('idx,'pred::pt,'act::bn) Treeα" is
  tPred
.

lift_definition Actα :: "'act  ('idx,'pred,'act) Treeα  ('idx,'pred::pt,'act::bn) Treeα" is
  tAct
by (fact alpha_Tree_tAct)

text ‹The lifted constructors are equivariant.›

lemma Conjα_eqvt [eqvt, simp]: "p  Conjα tsetα = Conjα (p  tsetα)"
proof -
  {
    fix x
    assume "x  set_bset (p  map_bset rep_Treeα tsetα)"
    then obtain y where "y  set_bset (map_bset rep_Treeα tsetα)" and "x = p  y"
      by (metis imageE permute_bset.rep_eq permute_set_eq_image)
    then obtain tα where 1: "tα  set_bset tsetα" and 2: "x = p  rep_Treeα tα"
      by (metis imageE map_bset.rep_eq)
    let ?x' = "rep_Treeα (p  tα)"
    from 1 have "p  tα  set_bset (p  tsetα)"
      by (metis mem_permute_iff permute_bset.rep_eq)
    then have "?x'  set_bset (map_bset rep_Treeα (p  tsetα))"
      by (simp add: bset.set_map)
    moreover from 2 have "x =α ?x'"
      by (metis alpha_Tree_permute_rep_commute)
    ultimately have "x'set_bset (map_bset rep_Treeα (p  tsetα)). x =α x'"
      ..
  }
  moreover
  {
    fix y
    assume "y  set_bset (map_bset rep_Treeα (p  tsetα))"
    then obtain x where "x  set_bset (p  tsetα)" and "rep_Treeα x = y"
      by (metis imageE map_bset.rep_eq)
    then obtain tα where 1: "tα  set_bset tsetα" and 2: "rep_Treeα (p  tα) = y"
      by (metis imageE permute_bset.rep_eq permute_set_eq_image)
    let ?y' = "p  rep_Treeα tα"
    from 1 have "rep_Treeα tα  set_bset (map_bset rep_Treeα tsetα)"
      by (simp add: bset.set_map)
    then have "?y'  set_bset (p  map_bset rep_Treeα tsetα)"
      by (metis mem_permute_iff permute_bset.rep_eq)
    moreover from 2 have "?y' =α y"
      by (metis alpha_Tree_permute_rep_commute)
    ultimately have "y'set_bset (p  map_bset rep_Treeα tsetα). y' =α y"
      ..
  }
  ultimately show ?thesis
    by (simp add: Conjα_def' map_bset_eqvt rel_bset_def rel_set_def Treeα.abs_eq_iff)
qed

lemma Notα_eqvt [eqvt, simp]: "p  Notα tα = Notα (p  tα)"
by (induct tα) (simp add: Notα.abs_eq)

lemma Predα_eqvt [eqvt, simp]: "p  Predα φ = Predα (p  φ)"
by (simp add: Predα.abs_eq)

lemma Actα_eqvt [eqvt, simp]: "p  Actα α tα = Actα (p  α) (p  tα)"
by (induct tα) (simp add: Actα.abs_eq)

text ‹The lifted constructors are injective (except for~@{const Actα}).›

lemma Conjα_eq_iff [simp]: "Conjα tset1α = Conjα tset2α  tset1α = tset2α"
proof
  assume "Conjα tset1α = Conjα tset2α"
  then have "tConj (map_bset rep_Treeα tset1α) =α tConj (map_bset rep_Treeα tset2α)"
    by (metis Conjα_def' Treeα.abs_eq_iff)
  then have "rel_bset (=α) (map_bset rep_Treeα tset1α) (map_bset rep_Treeα tset2α)"
    by (auto elim: alpha_Tree.cases)
  then show "tset1α = tset2α"
    using Quotient_Treeα Quotient_rel_abs2 bset_lifting.bset_quot_map map_bset_abs_rep_Treeα by fastforce
qed (fact arg_cong)

lemma Notα_eq_iff [simp]: "Notα t1α = Notα t2α  t1α = t2α"
proof
  assume "Notα t1α = Notα t2α"
  then have "tNot (rep_Treeα t1α) =α tNot (rep_Treeα t2α)"
    by (metis Notα.abs_eq Treeα.abs_eq_iff Treeα_abs_rep)
  then have "rep_Treeα t1α =α rep_Treeα t2α"
    using alpha_Tree.cases by auto
  then show "t1α = t2α"
    by (metis Treeα.abs_eq_iff Treeα_abs_rep)
next
  assume "t1α = t2α" then show "Notα t1α = Notα t2α"
    by simp
qed

lemma Predα_eq_iff [simp]: "Predα φ1 = Predα φ2  φ1 = φ2"
proof
  assume "Predα φ1 = Predα φ2"
  then have "(tPred φ1 :: ('d, 'b, 'e) Tree) =α tPred φ2"  ― ‹note the unrelated type›
    by (metis Predα.abs_eq Treeα.abs_eq_iff)
  then show "φ1 = φ2"
    using alpha_Tree.cases by auto
next
  assume "φ1 = φ2" then show "Predα φ1 = Predα φ2"
    by simp
qed

lemma Actα_eq_iff: "Actα α1 t1 = Actα α2 t2  tAct α1 (rep_Treeα t1) =α tAct α2 (rep_Treeα t2)"
by (metis Actα.abs_eq Treeα.abs_eq_iff Treeα_abs_rep)

text ‹The lifted constructors are free (except for~@{const Actα}).›

lemma Treeα_free [simp]:
  shows "Conjα tsetα  Notα tα"
  and "Conjα tsetα  Predα φ"
  and "Conjα tsetα  Actα α tα"
  and "Notα tα  Predα φ"
  and "Notα t1α  Actα α t2α"
  and "Predα φ  Actα α tα"
by (simp add: Conjα_def' Notα_def Predα_def Actα_def Treeα.abs_eq_iff)+

text ‹The following lemmas describe the support of constructed trees modulo $\alpha$-equivalence.›

lemma supp_alpha_supp_rel: "supp tα = supp_rel (=α) (rep_Treeα tα)"
unfolding supp_def supp_rel_def by (metis (mono_tags, lifting) Collect_cong Treeα.abs_eq_iff Treeα_abs_rep alpha_Tree_permute_rep_commute)

lemma supp_Conjα [simp]: "supp (Conjα tsetα) = supp tsetα"
unfolding supp_def by simp

lemma supp_Notα [simp]: "supp (Notα tα) = supp tα"
unfolding supp_def by simp

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

lemma supp_Actα [simp]:
  assumes "finite (supp tα)"
  shows "supp (Actα α tα) = supp α  supp tα - bn α"
using assms by (metis Actα.abs_eq Treeα_abs_rep Treeα_rep_abs alpha_Tree_supp_rel supp_alpha_supp_rel supp_rel_tAct)


subsection ‹Induction over trees modulo \texorpdfstring{$\alpha$}{alpha}-equivalence›

lemma Treeα_induct [case_names Conjα Notα Predα Actα Envα, induct type: Treeα]:
  fixes tα
  assumes "tsetα. (x. x  set_bset tsetα  P x)  P (Conjα tsetα)"
    and "tα. P tα  P (Notα tα)"
    and "pred. P (Predα pred)"
    and "act tα. P tα  P (Actα act tα)"
  shows "P tα"
proof (rule Treeα.abs_induct)
  fix t show "P (abs_Treeα t)"
    proof (induction t)
      case (tConj tset)
        let ?tsetα = "map_bset abs_Treeα tset"
        have "abs_Treeα (tConj tset) = Conjα ?tsetα"
          by (simp add: Conjα.abs_eq)
        then show ?case
          using assms(1) tConj.IH by (metis imageE map_bset.rep_eq)
    next
      case tNot then show ?case
        using assms(2) by (metis Notα.abs_eq)
    next
      case tPred show ?case
        using assms(3) by (metis Predα.abs_eq)
    next
      case tAct then show ?case
        using assms(4) by (metis Actα.abs_eq)
    qed
qed

text ‹There is no (obvious) strong induction principle for trees modulo $\alpha$-equivalence: since
their support may be infinite, we may not be able to rename bound variables without also renaming
free variables.›


subsection ‹Hereditarily finitely supported trees›

text ‹We cannot obtain the type of infinitary formulas simply as the sub-type of all trees (modulo
$\alpha$-equivalence) that are finitely supported: since an infinite set of trees may be finitely
supported even though its members are not (and thus, would not be formulas), the sub-type of
\emph{all} finitely supported trees does not validate the induction principle that we desire for
formulas.

Instead, we define \emph{hereditarily} finitely supported trees. We require that environments and
state predicates are finitely supported.›

inductive hereditarily_fs :: "('idx,'pred::fs,'act::bn) Treeα  bool" where
  Conjα: "finite (supp tsetα)  (tα. tα  set_bset tsetα  hereditarily_fs tα)  hereditarily_fs (Conjα tsetα)"
| Notα: "hereditarily_fs tα  hereditarily_fs (Notα tα)"
| Predα: "hereditarily_fs (Predα φ)"
| Actα: "hereditarily_fs tα  hereditarily_fs (Actα α tα)"

text @{const hereditarily_fs} is equivariant.›

lemma hereditarily_fs_eqvt [eqvt]:
  assumes "hereditarily_fs tα"
  shows "hereditarily_fs (p  tα)"
using assms proof (induction rule: hereditarily_fs.induct)
  case Conjα then show ?case
    by (metis (erased, hide_lams) Conjα_eqvt hereditarily_fs.Conjα mem_permute_iff permute_finite permute_minus_cancel(1) set_bset_eqvt supp_eqvt)
next
  case Notα then show ?case
    by (metis Notα_eqvt hereditarily_fs.Notα)
next
  case Predα then show ?case
    by (metis Predα_eqvt hereditarily_fs.Predα)
next
  case Actα then show ?case
    by (metis Actα_eqvt hereditarily_fs.Actα)
qed

text @{const hereditarily_fs} is preserved under $\alpha$-renaming.›

lemma hereditarily_fs_alpha_renaming:
  assumes "Actα α tα = Actα α' tα'"
  shows "hereditarily_fs tα  hereditarily_fs tα'"
proof
  assume "hereditarily_fs tα"
  then show "hereditarily_fs tα'"
    using assms by (auto simp add: Actα_def Treeα.abs_eq_iff alphas) (metis Treeα.abs_eq_iff Treeα_abs_rep hereditarily_fs_eqvt permute_Treeα.abs_eq)
next
  assume "hereditarily_fs tα'"
  then show "hereditarily_fs tα"
    using assms by (auto simp add: Actα_def Treeα.abs_eq_iff alphas) (metis Treeα.abs_eq_iff Treeα_abs_rep hereditarily_fs_eqvt permute_Treeα.abs_eq permute_minus_cancel(2))
qed

text ‹Hereditarily finitely supported trees have finite support.›

lemma hereditarily_fs_implies_finite_supp:
  assumes "hereditarily_fs tα"
  shows "finite (supp tα)"
using assms by (induction rule: hereditarily_fs.induct) (simp_all add: finite_supp)


subsection ‹Infinitary formulas›

text ‹Now, infinitary formulas are simply the sub-type of hereditarily finitely supported trees.›

typedef ('idx,'pred::fs,'act::bn) formula = "{tα::('idx,'pred,'act) Treeα. hereditarily_fs tα}"
by (metis hereditarily_fs.Predα mem_Collect_eq)

text ‹We set up Isabelle's lifting infrastructure so that we can lift definitions from the type of
trees modulo $\alpha$-equivalence to the sub-type of formulas.›

(* FIXME: No relator found. *)
setup_lifting type_definition_formula

lemma Abs_formula_inverse [simp]:
  assumes "hereditarily_fs tα"
  shows "Rep_formula (Abs_formula tα) = tα"
using assms by (metis Abs_formula_inverse mem_Collect_eq)

lemma Rep_formula' [simp]: "hereditarily_fs (Rep_formula x)"
by (metis Rep_formula mem_Collect_eq)

text ‹Now we lift the permutation operation.›

instantiation formula :: (type, fs, bn) pt
begin

  lift_definition permute_formula :: "perm  ('a,'b,'c) formula  ('a,'b,'c) formula"
    is permute
  by (fact hereditarily_fs_eqvt)

  instance
  by standard (transfer, simp)+

end

text ‹The abstraction and representation functions for formulas are equivariant, and they preserve
support.›

lemma Abs_formula_eqvt [simp]:
  assumes "hereditarily_fs tα"
  shows "p  Abs_formula tα = Abs_formula (p  tα)"
by (metis assms eq_onp_same_args permute_formula.abs_eq)

lemma supp_Abs_formula [simp]:
  assumes "hereditarily_fs tα"
  shows "supp (Abs_formula tα) = supp tα"
proof -
  {
    fix p :: perm
    have "p  Abs_formula tα = Abs_formula (p  tα)"
      using assms by (metis Abs_formula_eqvt)
    moreover have "hereditarily_fs (p  tα)"
      using assms by (metis hereditarily_fs_eqvt)
    ultimately have "p  Abs_formula tα = Abs_formula tα  p  tα = tα"
      using assms by (metis Abs_formula_inverse)
  }
  then show ?thesis unfolding supp_def by simp
qed

lemmas Rep_formula_eqvt [eqvt, simp] = permute_formula.rep_eq[symmetric]

lemma supp_Rep_formula [simp]: "supp (Rep_formula x) = supp x"
by (metis Rep_formula' Rep_formula_inverse supp_Abs_formula)

lemma supp_map_bset_Rep_formula [simp]: "supp (map_bset Rep_formula xset) = supp xset"
proof
  have "eqvt (map_bset Rep_formula)"
    unfolding eqvt_def by (simp add: ext)
  then show "supp (map_bset Rep_formula xset)  supp xset"
    by (fact supp_fun_app_eqvt)
next
  {
    fix a :: atom
    have "inj (map_bset Rep_formula)"
      by (metis bset.inj_map Rep_formula_inject injI)
    then have "x y. x  y  map_bset Rep_formula x  map_bset Rep_formula y"
      by (metis inj_eq)
    then have "{b. (a  b)  xset  xset}  {b. (a  b)  map_bset Rep_formula xset  map_bset Rep_formula xset}" (is "?S  ?T")
      by auto
    then have "infinite ?S  infinite ?T"
      by (metis infinite_super)
  }
  then show "supp xset  supp (map_bset Rep_formula xset)"
    unfolding supp_def by auto
qed

text ‹Formulas are in fact finitely supported.›

instance formula :: (type, fs, bn) fs
by standard (metis Rep_formula' hereditarily_fs_implies_finite_supp supp_Rep_formula)


subsection ‹Constructors for infinitary formulas›

text ‹We lift the constructors for trees (modulo $\alpha$-equivalence) to infinitary formulas.
Since~@{const Conjα} does not necessarily yield a (hereditarily) finitely supported tree when
applied to a (potentially infinite) set of (hereditarily) finitely supported trees, we cannot use
Isabelle's {\bf lift\_definition} to define~@{term Conj}. Instead, theorems about terms of the
form~@{term "Conj xset"} will usually carry an assumption that~@{term xset} is finitely supported.›

definition Conj :: "('idx,'pred,'act) formula set['idx]  ('idx,'pred::fs,'act::bn) formula" where
  "Conj xset = Abs_formula (Conjα (map_bset Rep_formula xset))"

lemma finite_supp_implies_hereditarily_fs_Conjα [simp]:
  assumes "finite (supp xset)"
  shows "hereditarily_fs (Conjα (map_bset Rep_formula xset))"
proof (rule hereditarily_fs.Conjα)
  show "finite (supp (map_bset Rep_formula xset))"
    using assms by (metis supp_map_bset_Rep_formula)
next
  fix tα assume "tα  set_bset (map_bset Rep_formula xset)"
  then show "hereditarily_fs tα"
    by (auto simp add: bset.set_map)
qed

lemma Conj_rep_eq:
  assumes "finite (supp xset)"
  shows "Rep_formula (Conj xset) = Conjα (map_bset Rep_formula xset)"
using assms unfolding Conj_def by simp

lift_definition Not :: "('idx,'pred,'act) formula  ('idx,'pred::fs,'act::bn) formula" is
  Notα
by (fact hereditarily_fs.Notα)

lift_definition Pred :: "'pred  ('idx,'pred::fs,'act::bn) formula" is
  Predα
by (fact hereditarily_fs.Predα)

lift_definition Act :: "'act  ('idx,'pred,'act) formula  ('idx,'pred::fs,'act::bn) formula" is
  Actα
by (fact hereditarily_fs.Actα)

text ‹The lifted constructors are equivariant (in the case of~@{const Conj}, on finitely supported
arguments).›

lemma Conj_eqvt [simp]:
  assumes "finite (supp xset)"
  shows "p  Conj xset = Conj (p  xset)"
using assms unfolding Conj_def by simp

lemma Not_eqvt [eqvt, simp]: "p  Not x = Not (p  x)"
by transfer simp

lemma Pred_eqvt [eqvt, simp]: "p  Pred φ = Pred (p  φ)"
by transfer simp

lemma Act_eqvt [eqvt, simp]: "p  Act α x = Act (p  α) (p  x)"
by transfer simp

text ‹The following lemmas describe the support of constructed formulas.›

lemma supp_Conj [simp]:
  assumes "finite (supp xset)"
  shows "supp (Conj xset) = supp xset"
using assms unfolding Conj_def by simp

lemma supp_Not [simp]: "supp (Not x) = supp x"
by (metis Not.rep_eq supp_Notα supp_Rep_formula)

lemma supp_Pred [simp]: "supp (Pred φ) = supp φ"
by (metis Pred.rep_eq supp_Predα supp_Rep_formula)

lemma supp_Act [simp]: "supp (Act α x) = supp α  supp x - bn α"
by (metis Act.rep_eq finite_supp supp_Actα supp_Rep_formula)

lemma bn_fresh_Act [simp]: "bn α ♯* Act α x"
by (simp add: fresh_def fresh_star_def)

text ‹The lifted constructors are injective (except for @{const Act}).›

lemma Conj_eq_iff [simp]:
  assumes "finite (supp xset1)" and "finite (supp xset2)"
  shows "Conj xset1 = Conj xset2  xset1 = xset2"
using assms
by (metis (erased, hide_lams) Conjα_eq_iff Conj_rep_eq Rep_formula_inverse injI inj_eq bset.inj_map)

lemma Not_eq_iff [simp]: "Not x1 = Not x2  x1 = x2"
by (metis Not.rep_eq Notα_eq_iff Rep_formula_inverse)

lemma Pred_eq_iff [simp]: "Pred φ1 = Pred φ2  φ1 = φ2"
by (metis Pred.rep_eq Predα_eq_iff)

lemma Act_eq_iff: "Act α1 x1 = Act α2 x2  Actα α1 (Rep_formula x1) = Actα α2 (Rep_formula x2)"
by (metis Act.rep_eq Rep_formula_inverse)

text ‹Helpful lemmas for dealing with equalities involving~@{const Act}.›

lemma Act_eq_iff_perm: "Act α1 x1 = Act α2 x2 
  (p. supp x1 - bn α1 = supp x2 - bn α2  (supp x1 - bn α1) ♯* p  p  x1 = x2  supp α1 - bn α1 = supp α2 - bn α2  (supp α1 - bn α1) ♯* p  p  α1 = α2)"
  (is "?l  ?r")
proof
  assume "?l"
  then obtain p where alpha: "(bn α1, rep_Treeα (Rep_formula x1)) ≈set (=α) (supp_rel (=α)) p (bn α2, rep_Treeα (Rep_formula x2))" and eq: "(bn α1, α1) ≈set (=) supp p (bn α2, α2)"
    by (metis Act_eq_iff Actα_eq_iff alpha_tAct)
  from alpha have "supp x1 - bn α1 = supp x2 - bn α2"
    by (metis alpha_set.simps supp_Rep_formula supp_alpha_supp_rel)
  moreover from alpha have "(supp x1 - bn α1) ♯* p"
    by (metis alpha_set.simps supp_Rep_formula supp_alpha_supp_rel)
  moreover from alpha have "p  x1 = x2"
    by (metis Rep_formula_eqvt Rep_formula_inject Treeα.abs_eq_iff Treeα_abs_rep alpha_Tree_permute_rep_commute alpha_set.simps)
  moreover from eq have "supp α1 - bn α1 = supp α2 - bn α2"
    by (metis alpha_set.simps)
  moreover from eq have "(supp α1 - bn α1) ♯* p"
    by (metis alpha_set.simps)
  moreover from eq have "p  α1 = α2"
    by (simp add: alpha_set.simps)
  ultimately show "?r"
    by metis
next
  assume "?r"
  then obtain p where 1: "supp x1 - bn α1 = supp x2 - bn α2" and 2: "(supp x1 - bn α1) ♯* p" and 3: "p  x1 = x2"
    and 4: "supp α1 - bn α1 = supp α2 - bn α2" and 5: "(supp α1 - bn α1) ♯* p" and 6: "p  α1 = α2"
    by metis
  from 1 2 3 6 have "(bn α1, rep_Treeα (Rep_formula x1)) ≈set (=α) (supp_rel (=α)) p (bn α2, rep_Treeα (Rep_formula x2))"
    by (metis (no_types, lifting) Rep_formula_eqvt alpha_Tree_permute_rep_commute alpha_set.simps bn_eqvt supp_Rep_formula supp_alpha_supp_rel)
  moreover from 4 5 6 have "(bn α1, α1) ≈set (=) supp p (bn α2, α2)"
    by (simp add: alpha_set.simps bn_eqvt)
  ultimately show "Act α1 x1 = Act α2 x2"
    by (metis Act_eq_iff Actα_eq_iff alpha_tAct)
qed

lemma Act_eq_iff_perm_renaming: "Act α1 x1 = Act α2 x2 
  (p. supp x1 - bn α1 = supp x2 - bn α2  (supp x1 - bn α1) ♯* p  p  x1 = x2  supp α1 - bn α1 = supp α2 - bn α2  (supp α1 - bn α1) ♯* p  p  α1 = α2  supp p  bn α1  p  bn α1)"
  (is "?l  ?r")
proof
  assume "?l"
  then obtain p where p: "supp x1 - bn α1 = supp x2 - bn α2  (supp x1 - bn α1) ♯* p  p  x1 = x2  supp α1 - bn α1 = supp α2 - bn α2  (supp α1 - bn α1) ♯* p  p  α1 = α2"
    by (metis Act_eq_iff_perm)
  moreover obtain q where q_p: "bbn α1. q  b = p  b" and supp_q: "supp q  bn α1  p  bn α1"
    by (metis set_renaming_perm2)
  have "supp q  supp p"
  proof
    fix a assume *: "a  supp q" then show "a  supp p"
    proof (cases "a  bn α1")
      case True then show ?thesis
        using "*" q_p by (metis mem_Collect_eq supp_perm)
    next
      case False then have "a  p  bn α1"
        using "*" supp_q using UnE subsetCE by blast
      with False have "p  a  a"
        by (metis mem_permute_iff)
      then show ?thesis
        using fresh_def fresh_perm by blast
    qed
  qed
  with p have "(supp x1 - bn α1) ♯* q" and "(supp α1 - bn α1) ♯* q"
    by (meson fresh_def fresh_star_def subset_iff)+
  moreover with p and q_p have "a. a  supp α1  q  a = p  a" and "a. a  supp x1  q  a = p  a"
    by (metis Diff_iff fresh_perm fresh_star_def)+
  then have "q  α1 = p  α1" and "q  x1 = p  x1"
    by (metis supp_perm_perm_eq)+
  ultimately show "?r"
    using supp_q by (metis bn_eqvt)
next
  assume "?r" then show "?l"
    by (meson Act_eq_iff_perm)
qed

text ‹The lifted constructors are free (except for @{const Act}).›

lemma Tree_free [simp]:
  shows "finite (supp xset)  Conj xset  Not x"
  and "finite (supp xset)  Conj xset  Pred φ"
  and "finite (supp xset)  Conj xset  Act α x"
  and "Not x  Pred φ"
  and "Not x1  Act α x2"
  and "Pred φ  Act α x"
proof -
  show "finite (supp xset)  Conj xset  Not x"
    by (metis Conj_rep_eq Not.rep_eq Treeα_free(1))
next
  show "finite (supp xset)  Conj xset  Pred φ"
    by (metis Conj_rep_eq Pred.rep_eq Treeα_free(2))
next
  show "finite (supp xset)  Conj xset  Act α x"
    by (metis Conj_rep_eq Act.rep_eq Treeα_free(3))
next
  show "Not x  Pred φ"
    by (metis Not.rep_eq Pred.rep_eq Treeα_free(4))
next
  show "Not x1  Act α x2"
    by (metis Not.rep_eq Act.rep_eq Treeα_free(5))
next
  show "Pred φ  Act α x"
    by (metis Pred.rep_eq Act.rep_eq Treeα_free(6))
qed


subsection ‹Induction over infinitary formulas›

lemma formula_induct [case_names Conj Not Pred Act, induct type: formula]:
  fixes x
  assumes "xset. finite (supp xset)  (x. x  set_bset xset  P x)  P (Conj xset)"
    and "formula. P formula  P (Not formula)"
    and "pred. P (Pred pred)"
    and "act formula. P formula  P (Act act formula)"
  shows "P x"
proof (induction x)
  fix tα :: "('a,'b,'c) Treeα"
  assume "tα  {tα. hereditarily_fs tα}"
  then have "hereditarily_fs tα"
    by simp
  then show "P (Abs_formula tα)"
    proof (induction tα)
      case (Conjα tsetα) show ?case
        proof -
          let ?tset = "map_bset Abs_formula tsetα"
          have "tα'. tα'  set_bset tsetα  tα' = (Rep_formula  Abs_formula) tα'"
            by (simp add: Conjα.hyps)
          then have "tsetα = map_bset (Rep_formula  Abs_formula) tsetα"
            by (metis bset.map_cong0 bset.map_id id_apply)
          then have *: "tsetα = map_bset Rep_formula ?tset"
            by (metis bset.map_comp)
          then have "Abs_formula (Conjα tsetα) = Conj ?tset"
            by (metis Conj_def)
          moreover from "*" have "finite (supp ?tset)"
            using Conjα.hyps(1) by (metis supp_map_bset_Rep_formula)
          moreover have "(t. t  set_bset ?tset  P t)"
            using Conjα.IH by (metis imageE map_bset.rep_eq)
          ultimately show ?thesis
            using assms(1) by metis
        qed
    next
      case Notα then show ?case
        using assms(2) by (metis Formula.Abs_formula_inverse Not.rep_eq Rep_formula_inverse)
    next
      case Predα show ?case
        using assms(3) by (metis Pred.abs_eq)
    next
      case Actα then show ?case
        using assms(4) by (metis Formula.Abs_formula_inverse Act.rep_eq Rep_formula_inverse)
    qed
qed


subsection ‹Strong induction over infinitary formulas›

lemma formula_strong_induct_aux:
  fixes x
  assumes "xset c. finite (supp xset)  (x. x  set_bset xset  (c. P c x))  P c (Conj xset)"
    and "formula c. (c. P c formula)  P c (Not formula)"
    and "pred c. P c (Pred pred)"
    and "act formula c. bn act ♯* c  (c. P c formula)  P c (Act act formula)"
  shows "(c :: 'd::fs) p. P c (p  x)"
proof (induction x)
  case (Conj xset)
    moreover then have "finite (supp (p  xset))"
      by (metis permute_finite supp_eqvt)
    moreover have "(x c. x  set_bset (p  xset)  P c x)"
      using Conj.IH by (metis (full_types) eqvt_bound mem_permute_iff set_bset_eqvt)
    ultimately show ?case
      using assms(1) by simp
next
  case Not then show ?case
    using assms(2) by simp
next
  case Pred show ?case
    using assms(3) by simp
next
  case (Act α x) show ?case
  proof -
    ― ‹rename~@{term "bn (p  α)"} to avoid~@{term c}, without touching~@{term "Act (p  α) (p  x)"}
    obtain q where 1: "(q  bn (p  α)) ♯* c" and 2: "supp (Act (p  α) (p  x)) ♯* q"
      proof (rule at_set_avoiding2[of "bn (p  α)" c "Act (p  α) (p  x)", THEN exE])
        show "finite (bn (p  α))" by (fact bn_finite)
      next
        show "finite (supp c)" by (fact finite_supp)
      next
        show "finite (supp (Act (p  α) (p  x)))" by (simp add: finite_supp)
      next
        show "bn (p  α) ♯* Act (p  α) (p  x)" by (simp add: fresh_def fresh_star_def)
      qed metis
    from 1 have "bn (q  p  α) ♯* c"
      by (simp add: bn_eqvt)
    moreover from Act.IH have "c. P c (q  p  x)"
      by (metis permute_plus)
    ultimately have "P c (Act (q  p  α) (q  p  x))"
      using assms(4) by simp
    moreover from 2 have "Act (q  p  α) (q  p  x) = Act (p  α) (p  x)"
      using supp_perm_eq by fastforce
    ultimately show ?thesis
      by simp
  qed
qed

lemmas formula_strong_induct = formula_strong_induct_aux[where p=0, simplified]
declare formula_strong_induct [case_names Conj Not Pred Act]

end

Theory Validity

theory Validity
imports
  Transition_System
  Formula
begin

section ‹Validity›

text ‹The following is needed to prove termination of~@{term validTree}.›

definition alpha_Tree_rel where
  "alpha_Tree_rel  {(x,y). x =α y}"

lemma alpha_Tree_relI [simp]:
  assumes "x =α y" shows "(x,y)  alpha_Tree_rel"
using assms unfolding alpha_Tree_rel_def by simp

lemma alpha_Tree_relE:
  assumes "(x,y)  alpha_Tree_rel" and "x =α y  P"
  shows P
using assms unfolding alpha_Tree_rel_def by simp

lemma wf_alpha_Tree_rel_hull_rel_Tree_wf:
  "wf (alpha_Tree_rel O hull_rel O Tree_wf)"
proof (rule wf_relcomp_compatible)
  show "wf (hull_rel O Tree_wf)"
    by (metis Tree_wf_eqvt' wf_Tree_wf wf_hull_rel_relcomp)
next
  show "(hull_rel O Tree_wf) O alpha_Tree_rel  alpha_Tree_rel O (hull_rel O Tree_wf)"
  proof
    fix x :: "('d, 'e, 'f) Tree × ('d, 'e, 'f) Tree"
    assume "x  (hull_rel O Tree_wf) O alpha_Tree_rel"
    then obtain x1 x2 x3 x4 where x: "x = (x1,x4)" and 1: "(x1,x2)  hull_rel" and 2: "(x2,x3)  Tree_wf" and 3: "(x3,x4)  alpha_Tree_rel"
      by auto
    from 2 have "(x1,x4)  alpha_Tree_rel O hull_rel O Tree_wf"
      using 1 and 3 proof (induct rule: Tree_wf.induct)
        ― ‹@{const tConj}
        fix t and tset :: "('d,'e,'f) Tree set['d]"
        assume *: "t  set_bset tset" and **: "(x1,t)  hull_rel" and ***: "(tConj tset, x4)  alpha_Tree_rel"
        from "**" obtain p where x1: "x1 = p  t"
          using hull_rel.cases by blast
        from "***" have "tConj tset =α x4"
          by (rule alpha_Tree_relE)
        then obtain tset' where x4: "x4 = tConj tset'" and "rel_bset (=α) tset tset'"
          by (cases "x4") simp_all
        with "*" obtain t' where t': "t'  set_bset tset'" and "t =α t'"
          by (metis rel_bset.rep_eq rel_set_def)
        with x1 have "(x1, p  t')  alpha_Tree_rel"
          by (metis Treeα.abs_eq_iff alpha_Tree_relI permute_Treeα.abs_eq)
        moreover have "(p  t', t')  hull_rel"
          by (rule hull_rel.intros)
        moreover from x4 and t' have "(t', x4)  Tree_wf"
          by (simp add: Tree_wf.intros(1))
        ultimately show "(x1,x4)  alpha_Tree_rel O hull_rel O Tree_wf"
          by auto
      next
        ― ‹@{const tNot}
        fix t
        assume *: "(x1,t)  hull_rel" and **: "(tNot t, x4)  alpha_Tree_rel"
        from "*" obtain p where x1: "x1 = p  t"
          using hull_rel.cases by blast
        from "**" have "tNot t =α x4"
          by (rule alpha_Tree_relE)
        then obtain t' where x4: "x4 = tNot t'" and "t =α t'"
          by (cases "x4") simp_all
        with x1 have "(x1, p  t')  alpha_Tree_rel"
          by (metis Treeα.abs_eq_iff alpha_Tree_relI permute_Treeα.abs_eq x1)
        moreover have "(p  t', t')  hull_rel"
          by (rule hull_rel.intros)
        moreover from x4 have "(t', x4)  Tree_wf"
          using Tree_wf.intros(2) by blast
        ultimately show "(x1,x4)  alpha_Tree_rel O hull_rel O Tree_wf"
          by auto
      next
        ― ‹@{const tAct}
        fix α t
        assume *: "(x1,t)  hull_rel" and **: "(tAct α t, x4)  alpha_Tree_rel"
        from "*" obtain p where x1: "x1 = p  t"
          using hull_rel.cases by blast
        from "**" have "tAct α t =α x4"
          by (rule alpha_Tree_relE)
        then obtain q t' where x4: "x4 = tAct (q  α) t'" and "q  t =α t'"
          by (cases "x4") (auto simp add: alpha_set)
        with x1 have "(x1, p  -q  t')  alpha_Tree_rel"
          by (metis Treeα.abs_eq_iff alpha_Tree_relI permute_Treeα.abs_eq permute_minus_cancel(1))
        moreover have "(p  -q  t', t')  hull_rel"
          by (metis hull_rel.simps permute_plus)
        moreover from x4 have "(t', x4)  Tree_wf"
          by (simp add: Tree_wf.intros(3))
        ultimately show "(x1,x4)  alpha_Tree_rel O hull_rel O Tree_wf"
          by auto
      qed
    with x show "x  alpha_Tree_rel O hull_rel O Tree_wf"
      by simp
  qed
qed

lemma alpha_Tree_rel_relcomp_trivialI [simp]:
  assumes "(x, y)  R"
  shows "(x, y)  alpha_Tree_rel O R"
using assms unfolding alpha_Tree_rel_def
by (metis Treeα.abs_eq_iff case_prodI mem_Collect_eq relcomp.relcompI)

lemma alpha_Tree_rel_relcompI [simp]:
  assumes "x =α x'" and "(x', y)  R"
  shows "(x, y)  alpha_Tree_rel O R"
using assms unfolding alpha_Tree_rel_def
by (metis case_prodI mem_Collect_eq relcomp.relcompI)


subsection ‹Validity for infinitely branching trees›

context nominal_ts
begin

  text ‹Since we defined formulas via a manual quotient construction, we also need to define
  validity via lifting from the underlying type of infinitely branching trees. 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.›

  declare conj_cong [fundef_cong]

  function valid_Tree :: "'state  ('idx,'pred,'act) Tree  bool" where
    "valid_Tree P (tConj tset)  (tset_bset tset. valid_Tree P t)"
  | "valid_Tree P (tNot t)  ¬ valid_Tree P t"
  | "valid_Tree P (tPred φ)  P  φ"
  | "valid_Tree P (tAct α t)  (α' t' P'. tAct α t =α tAct α' t'  P  α',P'  valid_Tree P' t')"
  by pat_completeness auto
  termination proof
    let ?R = "inv_image (alpha_Tree_rel O hull_rel O Tree_wf) snd"
    {
      show "wf ?R"
        by (metis wf_alpha_Tree_rel_hull_rel_Tree_wf wf_inv_image)
    next
      fix P :: 'state and tset :: "('idx,'pred,'act) Tree set['idx]" and t
      assume "t  set_bset tset" then show "((P, t), (P, tConj tset))  ?R"
        by (simp add: Tree_wf.intros(1))
    next
      fix P :: 'state and t :: "('idx,'pred,'act) Tree"
      show "((P, t), (P, tNot t))  ?R"
        by (simp add: Tree_wf.intros(2))
    next
      fix P1 P2 :: 'state and α1 α2 :: 'act and t1 t2 :: "('idx,'pred,'act) Tree"
      assume "tAct α1 t1 =α tAct α2 t2"
      then obtain p where "t2 =α p  t1"
        by (auto simp add: alphas) (metis alpha_Tree_symp sympE)
      then show "((P2, t2), (P1, tAct α1 t1))  ?R"
        by (simp add: Tree_wf.intros(3))
    }
  qed

  text @{const valid_Tree} is equivariant.›

  lemma valid_Tree_eqvt': "valid_Tree P t  valid_Tree (p  P) (p  t)"
  proof (induction P t rule: valid_Tree.induct)
    case (1 P tset) show ?case
      proof
        assume *: "valid_Tree P (tConj tset)"
        {
          fix t
          assume "t  p  set_bset tset"
          with "1.IH" and "*" have "valid_Tree (p  P) t"
            by (metis (no_types, lifting) imageE permute_set_eq_image valid_Tree.simps(1))
        }
        then show "valid_Tree (p  P) (p  tConj tset)"
          by simp
      next
        assume *: "valid_Tree (p  P) (p  tConj tset)"
        {
          fix t
          assume "t  set_bset tset"
          with "1.IH" and "*" have "valid_Tree P t"
            by (metis mem_permute_iff permute_Tree_tConj set_bset_eqvt valid_Tree.simps(1))
        }
        then show "valid_Tree P (tConj tset)"
          by simp
      qed
  next
    case 2 then show ?case by simp
  next
    case 3 show ?case by simp (metis permute_minus_cancel(2) satisfies_eqvt)
  next
    case (4 P α t) show ?case
      proof
        assume "valid_Tree P (tAct α t)"
        then obtain α' t' P' where *: "tAct α t =α tAct α' t'  P  α',P'  valid_Tree P' t'"
          by auto
        with "4.IH" have "valid_Tree (p  P') (p  t')"
          by blast
        moreover from "*" have "p  P  p  α', p  P'"
          by (metis transition_eqvt')
        moreover from "*" have "p  tAct α t =α tAct (p  α') (p  t')"
          by (metis alpha_Tree_eqvt permute_Tree.simps(4))
        ultimately show "valid_Tree (p  P) (p  tAct α t)"
          by auto
      next
        assume "valid_Tree (p  P) (p  tAct α t)"
        then obtain α' t' P' where *: "p  tAct α t =α tAct α' t'  (p  P)  α',P'  valid_Tree P' t'"
          by auto
        then have eq: "tAct α t =α tAct (-p  α') (-p  t')"
          by (metis alpha_Tree_eqvt permute_Tree.simps(4) permute_minus_cancel(2))
        moreover from "*" have "P  -p  α', -p  P'"
          by (metis permute_minus_cancel(2) transition_eqvt')
        moreover with "4.IH" have "valid_Tree (-p  P') (-p  t')"
          using eq and "*" by simp
        ultimately show "valid_Tree P (tAct α t)"
          by auto
      qed
  qed

  lemma valid_Tree_eqvt (*[eqvt]*):
    assumes "valid_Tree P t" shows "valid_Tree (p  P) (p  t)"
  using assms by (metis valid_Tree_eqvt')

  text ‹$\alpha$-equivalent trees validate the same states.›

  lemma alpha_Tree_valid_Tree:
    assumes "t1 =α t2"
    shows "valid_Tree P t1  valid_Tree P t2"
  using assms proof (induction t1 t2 arbitrary: P rule: alpha_Tree_induct)
    case tConj then show ?case
      by auto (metis (mono_tags) rel_bset.rep_eq rel_set_def)+
  next
    case (tAct α1 t1 α2 t2) show ?case
    proof
      assume "valid_Tree P (tAct α1 t1)"
      then obtain α' t' P' where "tAct α1 t1 =α tAct α' t'  P  α',P'  valid_Tree P' t'"
        by auto
      moreover from tAct.hyps have "tAct α1 t1 =α tAct α2 t2"
        using alpha_tAct by blast
      ultimately show "valid_Tree P (tAct α2 t2)"
        by (metis Treeα.abs_eq_iff valid_Tree.simps(4))
    next
      assume "valid_Tree P (tAct α2 t2)"
      then obtain α' t' P' where "tAct α2 t2 =α tAct α' t'  P  α',P'  valid_Tree P' t'"
        by auto
      moreover from tAct.hyps have "tAct α1 t1 =α tAct α2 t2"
        using alpha_tAct by blast
      ultimately show "valid_Tree P (tAct α1 t1)"
        by (metis Treeα.abs_eq_iff valid_Tree.simps(4))
    qed
  qed simp_all


  subsection ‹Validity for trees modulo \texorpdfstring{$\alpha$}{alpha}-equivalence›

  lift_definition valid_Treeα :: "'state  ('idx,'pred,'act) Treeα  bool" is
    valid_Tree
  by (fact alpha_Tree_valid_Tree)

  lemma valid_Treeα_eqvt (*[eqvt]*):
    assumes "valid_Treeα P t" shows "valid_Treeα (p  P) (p  t)"
  using assms by transfer (fact valid_Tree_eqvt)

  lemma valid_Treeα_Conjα [simp]: "valid_Treeα P (Conjα tsetα)  (tαset_bset tsetα. valid_Treeα P tα)"
  proof -
    have "valid_Tree P (rep_Treeα (abs_Treeα (tConj (map_bset rep_Treeα tsetα))))  valid_Tree P (tConj (map_bset rep_Treeα tsetα))"
      by (metis Treeα_rep_abs alpha_Tree_valid_Tree)
    then show ?thesis
      by (simp add: valid_Treeα_def Conjα_def map_bset.rep_eq)
  qed

  lemma valid_Treeα_Notα [simp]: "valid_Treeα P (Notα tα)  ¬ valid_Treeα P tα"
  by transfer simp

  lemma valid_Treeα_Predα [simp]: "valid_Treeα P (Predα φ)  P  φ"
  by transfer simp

  lemma valid_Treeα_Actα [simp]: "valid_Treeα P (Actα α tα)  (α' tα' P'. Actα α tα = Actα α' tα'  P  α',P'  valid_Treeα P' tα')"
  proof
    assume "valid_Treeα P (Actα α tα)"
    moreover have "Actα α tα = abs_Treeα (tAct α (rep_Treeα tα))"
      by (metis Actα.abs_eq Treeα_abs_rep)
    ultimately show "α' tα' P'. Actα α tα = Actα α' tα'  P  α',P'  valid_Treeα P' tα'"
      by (metis Actα.abs_eq Treeα.abs_eq_iff valid_Tree.simps(4) valid_Treeα.abs_eq)
  next
    assume "α' tα' P'. Actα α tα = Actα α' tα'  P  α',P'  valid_Treeα P' tα'"
    moreover have "α' tα'. Actα α' tα' = abs_Treeα (tAct α' (rep_Treeα tα'))"
      by (metis Actα.abs_eq Treeα_abs_rep)
    ultimately show "valid_Treeα P (Actα α tα)"
      by (metis Treeα.abs_eq_iff valid_Tree.simps(4) valid_Treeα.abs_eq valid_Treeα.rep_eq)
  qed


  subsection ‹Validity for infinitary formulas›

  lift_definition valid :: "'state  ('idx,'pred,'act) formula  bool" (infix "" 70) is
    valid_Treeα
  .

  lemma valid_eqvt (*[eqvt]*):
    assumes "P  x" shows "(p  P)  (p  x)"
  using assms by transfer (metis valid_Treeα_eqvt)

  lemma valid_Conj [simp]:
    assumes "finite (supp xset)"
    shows "P  Conj xset  (xset_bset xset. P  x)"
  using assms by (simp add: valid_def Conj_def map_bset.rep_eq)

  lemma valid_Not [simp]: "P  Not x  ¬ P  x"
  by transfer simp

  lemma valid_Pred [simp]: "P  Pred φ  P  φ"
  by transfer simp

  lemma valid_Act: "P  Act α x  (α' x' P'. Act α x = Act α' x'  P  α',P'  P'  x')"
  proof
    assume "P  Act α x"
    moreover have "Rep_formula (Abs_formula (Actα α (Rep_formula x))) = Actα α (Rep_formula x)"
      by (metis Act.rep_eq Rep_formula_inverse)
    ultimately show "α' x' P'. Act α x = Act α' x'  P  α',P'  P'  x'"
      by (auto simp add: valid_def Act_def) (metis Abs_formula_inverse Rep_formula' hereditarily_fs_alpha_renaming)
  next
    assume "α' x' P'. Act α x = Act α' x'  P  α',P'  P'  x'"
    then show "P  Act α x"
      by (metis Act.rep_eq valid.rep_eq valid_Treeα_Actα)
  qed

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

  lemma valid_Act_strong:
    assumes "finite (supp X)"
    shows "P  Act α x  (α' x' P'. Act α x = Act α' x'  P  α',P'  P'  x'  bn α' ♯* X)"
  proof
    assume "P  Act α x"
    then obtain α' x' P' where eq: "Act α x = Act α' x'" and trans: "P  α',P'" and valid: "P'  x'"
      by (metis valid_Act)
    have "finite (bn α')"
      by (fact bn_finite)
    moreover note ‹finite (supp X)
    moreover have "finite (supp (Act α' x', α',P'))"
      by (metis finite_Diff finite_UnI finite_supp supp_Pair supp_abs_residual_pair)
    moreover have "bn α' ♯* (Act α' x', α',P')"
      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 α' x', α',P') ♯* p"
      by (metis at_set_avoiding2)
    then have "supp (Act α' x') ♯* p" and "supp α',P' ♯* p"
      by (metis fresh_star_Un supp_Pair)+
    then have "Act (p  α') (p  x') = Act α' x'" and "p  α', p  P' = α',P'"
      by (metis Act_eqvt supp_perm_eq, metis abs_residual_pair_eqvt supp_perm_eq)
    then show "α' x' P'. Act α x = Act α' x'  P  α',P'  P'  x'  bn α' ♯* X"
      using eq and trans and valid and fresh_X by (metis bn_eqvt valid_eqvt)
  next
    assume "α' x' P'. Act α x = Act α' x'  P  α',P'  P'  x'  bn α' ♯* X"
    then show "P  Act α x"
      by (metis valid_Act)
  qed

  lemma valid_Act_fresh:
    assumes "bn α ♯* P"
    shows "P  Act α x  (P'. P  α,P'  P'  x)"
  proof
    assume "P  Act α x"

    moreover have "finite (supp P)"
      by (fact finite_supp)
    ultimately obtain α' x' P' where
      eq: "Act α x = Act α' x'" and trans: "P  α',P'" and valid: "P'  x'" and fresh: "bn α' ♯* P"
      by (metis valid_Act_strong)

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

    from assms and fresh have "(bn α  p  bn α) ♯* P"
      using p_α by (metis bn_eqvt fresh_star_Un)
    then have "supp p ♯* P"
      using supp_p by (metis fresh_star_def subset_eq)
    then have p_P: "-p  P = P"
      by (metis perm_supp_eq supp_minus_perm)

    from trans have "P  α,-p  P'"
      using p_P p_α by (metis permute_minus_cancel(1) transition_eqvt')
    moreover from valid have "-p  P'  x"
      using p_x by (metis permute_minus_cancel(1) valid_eqvt)
    ultimately show "P'. P  α,P'  P'  x"
      by meson
  next
    assume "P'. P  α,P'  P'  x" then show "P  Act α x"
      by (metis valid_Act)
  qed

end

end

Theory Logical_Equivalence

theory Logical_Equivalence
imports
  Validity
begin

section ‹(Strong) Logical Equivalence›

text ‹The definition of formulas is parametric in the index type, but from now on we want to work
with a fixed (sufficiently large) index type.›

locale indexed_nominal_ts = nominal_ts satisfies transition
  for satisfies :: "'state::fs  'pred::fs  bool" (infix "" 70)
  and transition :: "'state  ('act::bn,'state) residual  bool" (infix "" 70) +
  assumes card_idx_perm: "|UNIV::perm set| <o |UNIV::'idx set|"
      and card_idx_state: "|UNIV::'state set| <o |UNIV::'idx set|"
begin

  definition logically_equivalent :: "'state  'state  bool" where
    "logically_equivalent P Q  (x::('idx,'pred,'act) formula. P  x  Q  x)"

  notation logically_equivalent (infix "=⋅" 50)

  lemma logically_equivalent_eqvt:
    assumes "P =⋅ Q" shows "p  P =⋅ p  Q"
  using assms unfolding logically_equivalent_def
  by (metis (mono_tags) permute_minus_cancel(1) valid_eqvt)

end

end

Theory Bisimilarity_Implies_Equivalence

theory Bisimilarity_Implies_Equivalence
imports
  Logical_Equivalence
begin

section ‹Bisimilarity Implies Logical Equivalence›

context indexed_nominal_ts
begin

  lemma bisimilarity_implies_equivalence_Act:
    assumes "P Q. P ∼⋅ Q  P  x  Q  x"
    and "P ∼⋅ Q"
    and "P  Act α x"
    shows "Q  Act α x"
  proof -
    have "finite (supp Q)"
      by (fact finite_supp)
    with P  Act α x obtain α' x' P' where eq: "Act α x = Act α' x'" and trans: "P  α',P'" and valid: "P'  x'" and fresh: "bn α' ♯* Q"
      by (metis valid_Act_strong)

    from P ∼⋅ Q and fresh and trans obtain Q' where trans': "Q  α',Q'" and bisim': "P' ∼⋅ Q'"
      by (metis bisimilar_simulation_step)

    from eq obtain p where px: "x' = p  x"
      by (metis Act_eq_iff_perm)

    with valid have "-p  P'  x"
      by (metis permute_minus_cancel(1) valid_eqvt)
    moreover from bisim' have "(-p  P') ∼⋅ (-p  Q')"
      by (metis bisimilar_eqvt)
    ultimately have "-p  Q'  x"
      using P Q. P ∼⋅ Q  P  x  Q  x by metis
    with px have "Q'  x'"
      by (metis permute_minus_cancel(1) valid_eqvt)

    with eq and trans' show "Q  Act α x"
      unfolding valid_Act by metis
  qed

  theorem bisimilarity_implies_equivalence: assumes "P ∼⋅ Q" shows "P =⋅ Q"
  unfolding logically_equivalent_def proof
    fix x :: "('idx, 'pred, 'act) formula"
    from assms show "P  x  Q  x"
    proof (induction x arbitrary: P Q)
      case (Conj xset) then show ?case
        by simp
    next
      case Not then show ?case
        by simp
    next
      case Pred then show ?case
        by (metis bisimilar_is_bisimulation is_bisimulation_def symp_def valid_Pred)
    next
      case (Act α x) then show ?case
        by (metis bisimilar_symp bisimilarity_implies_equivalence_Act sympE)
    qed
  qed

end

end

Theory Equivalence_Implies_Bisimilarity

theory Equivalence_Implies_Bisimilarity
imports
  Logical_Equivalence
begin

section ‹Logical Equivalence Implies Bisimilarity›

context indexed_nominal_ts
begin

  definition is_distinguishing_formula :: "('idx, 'pred, 'act) formula  'state  'state  bool"
    ("_ distinguishes _ from _" [100,100,100] 100)
  where
    "x distinguishes P from Q  P  x  ¬ Q  x"

  lemma is_distinguishing_formula_eqvt (*[eqvt]*):
    assumes "x distinguishes P from Q" shows "(p  x) distinguishes (p  P) from (p  Q)"
  using assms unfolding is_distinguishing_formula_def
  by (metis permute_minus_cancel(2) valid_eqvt)

  lemma equivalent_iff_not_distinguished: "(P =⋅ Q)  ¬(x. x distinguishes P from Q)"
  by (metis (full_types) is_distinguishing_formula_def logically_equivalent_def valid_Not)

  text ‹There exists a distinguishing formula for~@{term P} and~@{term Q} whose support is contained
  in~@{term "supp P"}.›

  lemma distinguished_bounded_support:
    assumes "x distinguishes P from Q"
    obtains y where "supp y  supp P" and "y distinguishes P from Q"
  proof -
    let ?B = "{p  x|p. supp P ♯* p}"
    have "supp P supports ?B"
    unfolding supports_def proof (clarify)
      fix a b
      assume a: "a  supp P" and b: "b  supp P"
      have "(a  b)  ?B  ?B"
      proof
        fix x'
        assume "x'  (a  b)  ?B"
        then obtain p where 1: "x' = (a  b)  p  x" and 2: "supp P ♯* p"
          by (auto simp add: permute_set_def)
        let ?q = "(a  b) + p"
        from 1 have "x' = ?q  x"
          by simp
        moreover from a and b and 2 have "supp P ♯* ?q"
          by (metis fresh_perm fresh_star_def fresh_star_plus swap_atom_simps(3))
        ultimately show "x'  ?B" by blast
      qed
      moreover have "?B  (a  b)  ?B"
      proof
        fix x'
        assume "x'  ?B"
        then obtain p where 1: "x' = p  x" and 2: "supp P ♯* p"
          by auto
        let ?q = "(a  b) + p"
        from 1 have "x' = (a  b)  ?q  x"
          by simp
        moreover from a and b and 2 have "supp P ♯* ?q"
          by (metis fresh_perm fresh_star_def fresh_star_plus swap_atom_simps(3))
        ultimately show "x'  (a  b)  ?B"
          using mem_permute_iff by blast
      qed
      ultimately show "(a  b)  ?B = ?B" ..
    qed
    then have supp_B_subset_supp_P: "supp ?B  supp P"
      by (metis (erased, lifting) finite_supp supp_is_subset)
    then have finite_supp_B: "finite (supp ?B)"
      using finite_supp rev_finite_subset by blast
    have "?B  (λp. p  x) ` UNIV"
      by auto
    then have "|?B| ≤o |UNIV :: perm set|"
      by (rule surj_imp_ordLeq)
    also have "|UNIV :: perm set| <o |UNIV :: 'idx set|"
      by (metis card_idx_perm)
    also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|"
      by (metis Cnotzero_UNIV ordLeq_csum2)
    finally have card_B: "|?B| <o natLeq +c |UNIV :: 'idx set|" .
    let ?y = "Conj (Abs_bset ?B) :: ('idx, 'pred, 'act) formula"
    from finite_supp_B and card_B and supp_B_subset_supp_P have "supp ?y  supp P"
      by simp
    moreover have "?y distinguishes P from Q"
      unfolding is_distinguishing_formula_def proof
        from assms show "P  ?y"
          by (auto simp add: card_B finite_supp_B) (metis is_distinguishing_formula_def supp_perm_eq valid_eqvt)
      next
        from assms show "¬ Q  ?y"
          by (auto simp add: card_B finite_supp_B) (metis is_distinguishing_formula_def permute_zero fresh_star_zero)
      qed
    ultimately show ?thesis ..
  qed

  lemma equivalence_is_bisimulation: "is_bisimulation logically_equivalent"
  proof -
    have "symp logically_equivalent"
      by (metis logically_equivalent_def sympI)
    moreover
    {
      fix P Q φ assume "P =⋅ Q" then have "P  φ  Q  φ"
        by (metis logically_equivalent_def valid_Pred)
    }
    moreover
    {
      fix P Q α P' assume "P =⋅ Q" and "bn α ♯* Q" and "P  α,P'"
      then have "Q'. Q  α,Q'  P' =⋅ Q'"
        proof -
          {
            let ?Q' = "{Q'. Q  α,Q'}"
            assume "Q'?Q'. ¬ P' =⋅ Q'"
            then have "Q'?Q'. x :: ('idx, 'pred, 'act) formula. x distinguishes P' from Q'"
              by (metis equivalent_iff_not_distinguished)
            then have "Q'?Q'. x :: ('idx, 'pred, 'act) formula. supp x  supp P'  x distinguishes P' from Q'"
              by (metis distinguished_bounded_support)
            then obtain f :: "'state  ('idx, 'pred, 'act) formula" where
              *: "Q'?Q'. supp (f Q')  supp P'  (f Q') distinguishes P' from Q'"
              by metis
            have "supp (f ` ?Q')  supp P'"
              by (rule set_bounded_supp, fact finite_supp, cut_tac "*", blast)
            then have finite_supp_image: "finite (supp (f ` ?Q'))"
              using finite_supp rev_finite_subset by blast
            have "|f ` ?Q'| ≤o |UNIV :: 'state set|"
              by (metis card_of_UNIV card_of_image ordLeq_transitive)
            also have "|UNIV :: 'state set| <o |UNIV :: 'idx set|"
              by (metis card_idx_state)
            also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|"
              by (metis Cnotzero_UNIV ordLeq_csum2)
            finally have card_image: "|f ` ?Q'| <o natLeq +c |UNIV :: 'idx set|" .
            let ?y = "Conj (Abs_bset (f ` ?Q')) :: ('idx, 'pred, 'act) formula"
            have "P  Act α ?y"
              unfolding valid_Act proof (standard+)
                show "P  α,P'" by fact
              next
                {
                  fix Q'
                  assume "Q  α,Q'"
                  with "*" have "P'  f Q'"
                    by (metis is_distinguishing_formula_def mem_Collect_eq)
                }
                then show "P'  ?y"
                  by (simp add: finite_supp_image card_image)
              qed
            moreover have "¬ Q  Act α ?y"
              proof
                assume "Q  Act α ?y"
                then obtain Q' where 1: "Q  α,Q'" and 2: "Q'  ?y"
                  using ‹bn α ♯* Q by (metis valid_Act_fresh)
                from 2 have "Q''. Q  α,Q''  Q'  f Q''"
                  by (simp add: finite_supp_image card_image)
                with 1 and "*" show False
                  using is_distinguishing_formula_def by blast
              qed
            ultimately have False
              by (metis P =⋅ Q logically_equivalent_def)
          }
          then show ?thesis by auto
        qed
    }
    ultimately show ?thesis
      unfolding is_bisimulation_def by metis
  qed

  theorem equivalence_implies_bisimilarity: assumes "P =⋅ Q" shows "P ∼⋅ Q"
  using assms by (metis bisimilar_def equivalence_is_bisimulation)

end

end

Theory Disjunction

theory Disjunction
imports
  Formula
  Validity
begin

section ‹Disjunction›

definition Disj :: "('idx,'pred::fs,'act::bn) formula set['idx]  ('idx,'pred,'act) formula" where
  "Disj xset = Not (Conj (map_bset Not xset))"

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

lemma Disj_eqvt [simp]:
  assumes "finite (supp xset)"
  shows "p  Disj xset = Disj (p  xset)"
using assms unfolding Disj_def by simp

lemma Disj_eq_iff [simp]:
  assumes "finite (supp xset1)" and "finite (supp xset2)"
  shows "Disj xset1 = Disj xset2  xset1 = xset2"
using assms unfolding Disj_def by (metis Conj_eq_iff Not_eq_iff bset.inj_map_strong finite_supp_map_bset_Not)

context nominal_ts
begin

  lemma valid_Disj [simp]:
    assumes "finite (supp xset)"
    shows "P  Disj xset  (xset_bset xset. P  x)"
  using assms by (simp add: Disj_def map_bset.rep_eq)

end

end

Theory Expressive_Completeness

theory Expressive_Completeness
imports
  Bisimilarity_Implies_Equivalence
  Equivalence_Implies_Bisimilarity
  Disjunction
begin

section ‹Expressive Completeness›

context indexed_nominal_ts
begin

  subsection ‹Distinguishing formulas›

  text ‹Lemma \emph{distinguished\_bounded\_support} only shows the existence of a distinguishing
    formula, without stating what this formula looks like. We now define an explicit function that
    returns a distinguishing formula, in a way that this function is equivariant (on pairs of
    non-equivalent states).

    Note that this definition uses Hilbert's choice operator~$\varepsilon$, which is not necessarily
    equivariant. This is immediately remedied by a hull construction.›

  definition distinguishing_formula :: "'state  'state  ('idx, 'pred, 'act) formula" where
    "distinguishing_formula P Q  Conj (Abs_bset {-p  (ϵx. supp x  supp (p  P)  x distinguishes (p  P) from (p  Q))|p. True})"

  ― ‹just an auxiliary lemma that will be useful further below›
  lemma distinguishing_formula_card_aux:
    "|{-p  (ϵx. supp x  supp (p  P)  x distinguishes (p  P) from (p  Q))|p. True}| <o natLeq +c |UNIV :: 'idx set|"
  proof -
    let ?some = "λp. (ϵx. supp x  supp (p  P)  x distinguishes (p  P) from (p  Q))"
    let ?B = "{-p  ?some p|p. True}"

    have "?B  (λp. -p  ?some p) ` UNIV"
      by auto
    then have "|?B| ≤o |UNIV :: perm set|"
      by (rule surj_imp_ordLeq)
    also have "|UNIV :: perm set| <o |UNIV :: 'idx set|"
      by (metis card_idx_perm)
    also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|"
      by (metis Cnotzero_UNIV ordLeq_csum2)
    finally show ?thesis .
  qed

  ― ‹just an auxiliary lemma that will be useful further below›
  lemma distinguishing_formula_supp_aux:
    assumes "¬ (P =⋅ Q)"
    shows "supp (Abs_bset {-p  (ϵx. supp x  supp (p  P)  x distinguishes (p  P) from (p  Q))|p. True} :: _ set['idx])  supp P"
  proof -
    let ?some = "λp. (ϵx. supp x  supp (p  P)  x distinguishes (p  P) from (p  Q))"
    let ?B = "{-p  ?some p|p. True}"

    {
      fix p
      from assms have "¬ (p  P =⋅ p  Q)"
        by (metis logically_equivalent_eqvt permute_minus_cancel(2))
      then have "supp (?some p)  supp (p  P)"
        using distinguished_bounded_support by (metis (mono_tags, lifting) equivalent_iff_not_distinguished someI_ex)
    }
    note supp_some = this

    {
      fix x
      assume "x  ?B"
      then obtain p where "x = -p  ?some p"
        by blast
      with supp_some have "supp (p  x)  supp (p  P)"
        by simp
      then have "supp x  supp P"
        by (metis (full_types) permute_boolE subset_eqvt supp_eqvt)
    }
    note "*" = this
    have supp_B: "supp ?B  supp P"
      by (rule set_bounded_supp, fact finite_supp, cut_tac "*", blast)

    from supp_B and distinguishing_formula_card_aux show ?thesis
      using supp_Abs_bset by blast
  qed

  lemma distinguishing_formula_eqvt [simp]:
    assumes "¬ (P =⋅ Q)"
    shows "p  distinguishing_formula P Q = distinguishing_formula (p  P) (p  Q)"
  proof -
    let ?some = "λp. (ϵx. supp x  supp (p  P)  x distinguishes (p  P) from (p  Q))"
    let ?B = "{-p  ?some p|p. True}"

    from assms have "supp (Abs_bset ?B :: _ set['idx])  supp P"
      by (rule distinguishing_formula_supp_aux)
    then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
      using finite_supp rev_finite_subset by blast
    with distinguishing_formula_card_aux have *: "p  Conj (Abs_bset ?B) = Conj (Abs_bset (p  ?B))"
      by simp

    let ?some' = "λp'. (ϵx. supp x  supp (p'  p  P)  x distinguishes (p'  p  P) from (p'  p  Q))"
    let ?B' = "{-p'  ?some' p'|p'. True}"

    have "p  ?B = ?B'"
    proof
      {
        fix px
        assume "px  p  ?B"
        then obtain x where 1: "px = p  x" and 2: "x  ?B"
          by (metis (no_types, lifting) image_iff permute_set_eq_image)
        from 2 obtain p' where 3: "x = -p'  ?some p'"
          by blast
        from 1 and 3 have "px = -(p' - p)  ?some' (p' - p)"
          by simp
        then have "px  ?B'"
          by blast
      }
      then show "p  ?B  ?B'"
        by blast
    next
      {
        fix x
        assume "x  ?B'"
        then obtain p' where "x = -p'  ?some' p'"
          by blast
        then have "x = p  -(p' + p)  ?some (p' + p)"
          by (simp add: add.inverse_distrib_swap)
        then have "x  p  ?B"
          using mem_permute_iff by blast
      }
      then show "?B'  p  ?B"
        by blast
    qed

    with "*" show ?thesis
      unfolding distinguishing_formula_def by simp
  qed

  lemma supp_distinguishing_formula:
    assumes "¬ (P =⋅ Q)"
    shows "supp (distinguishing_formula P Q)  supp P"
  proof -
    let ?some = "λp. (ϵx. supp x  supp (p  P)  x distinguishes (p  P) from (p  Q))"
    let ?B = "{- p  ?some p|p. True}"

    from assms have "supp (Abs_bset ?B :: _ set['idx])  supp P"
      by (rule distinguishing_formula_supp_aux)
    moreover from this have "finite (supp (Abs_bset ?B :: _ set['idx]))"
      using finite_supp rev_finite_subset by blast
    ultimately show ?thesis
      unfolding distinguishing_formula_def by simp
  qed

  lemma distinguishing_formula_distinguishes:
    assumes "¬ (P =⋅ Q)"
    shows "(distinguishing_formula P Q) distinguishes P from Q"
  proof -
    let ?some = "λp. (ϵx. supp x  supp (p  P)  x distinguishes (p  P) from (p  Q))"
    let ?B = "{- p  ?some p|p. True}"

    {
      fix p
      have "(?some p) distinguishes (p  P) from (p  Q)"
        using assms 
        by (metis (mono_tags, lifting) is_distinguishing_formula_eqvt distinguished_bounded_support equivalent_iff_not_distinguished someI_ex)
    }
    note some_distinguishes = this

    {
      fix P'
      from assms have "supp (Abs_bset ?B :: _ set['idx])  supp P"
        by (rule distinguishing_formula_supp_aux)
      then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
        using finite_supp rev_finite_subset by blast
      with distinguishing_formula_card_aux have "P'  distinguishing_formula P Q  (x?B. P'  x)"
        unfolding distinguishing_formula_def by simp
    }
    note valid_distinguishing_formula = this

    {
      fix p
      have "P  -p  ?some p"
        by (metis (mono_tags) is_distinguishing_formula_def permute_minus_cancel(2) some_distinguishes valid_eqvt)
    }
    then have "P  distinguishing_formula P Q"
      using valid_distinguishing_formula by blast

    moreover have "¬ Q  distinguishing_formula P Q"
      using valid_distinguishing_formula by (metis (mono_tags, lifting) is_distinguishing_formula_def mem_Collect_eq permute_minus_cancel(1) some_distinguishes valid_eqvt)

    ultimately show "(distinguishing_formula P Q) distinguishes P from Q"
      using is_distinguishing_formula_def by blast
  qed


  subsection ‹Characteristic formulas›
  
  text ‹A \emph{characteristic formula} for a state~$P$ is valid for (exactly) those states that are
    bisimilar to~$P$.›

  definition characteristic_formula :: "'state  ('idx, 'pred, 'act) formula" where
    "characteristic_formula P  Conj (Abs_bset {distinguishing_formula P Q|Q. ¬ (P =⋅ Q)})"

  ― ‹just an auxiliary lemma that will be useful further below›
  lemma characteristic_formula_card_aux:
    "|{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}| <o natLeq +c |UNIV :: 'idx set|"
  proof -
    let ?B = "{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}"

    have "?B  (distinguishing_formula P) ` UNIV"
      by auto
    then have "|?B| ≤o |UNIV :: 'state set|"
      by (rule surj_imp_ordLeq)
    also have "|UNIV :: 'state set| <o |UNIV :: 'idx set|"
      by (metis card_idx_state)
    also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|"
      by (metis Cnotzero_UNIV ordLeq_csum2)
    finally show ?thesis .
  qed

  ― ‹just an auxiliary lemma that will be useful further below›
  lemma characteristic_formula_supp_aux:
    shows "supp (Abs_bset {distinguishing_formula P Q|Q. ¬ (P =⋅ Q)} :: _ set['idx])  supp P"
  proof -
    let ?B = "{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}"

    {
      fix x
      assume "x  ?B"
      then obtain Q where "x = distinguishing_formula P Q" and "¬ (P =⋅ Q)"
        by blast
      with supp_distinguishing_formula have "supp x  supp P"
        by metis
    }
    note "*" = this
    have supp_B: "supp ?B  supp P"
      by (rule set_bounded_supp, fact finite_supp, cut_tac "*", blast)

    from supp_B and characteristic_formula_card_aux show ?thesis
      using supp_Abs_bset by blast
  qed

  lemma characteristic_formula_eqvt (*[eqvt]*) [simp]:
    "p  characteristic_formula P = characteristic_formula (p  P)"
  proof -
    let ?B = "{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}"

    have "supp (Abs_bset ?B :: _ set['idx])  supp P"
      by (fact characteristic_formula_supp_aux)
    then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
      using finite_supp rev_finite_subset by blast
    with characteristic_formula_card_aux have *: "p  Conj (Abs_bset ?B) = Conj (Abs_bset (p  ?B))"
      by simp

    let ?B' = "{distinguishing_formula (p  P) Q|Q. ¬ ((p  P) =⋅ Q)}"

    have "p  ?B = ?B'"
    proof
      {
        fix px
        assume "px  p  ?B"
        then obtain x where 1: "px = p  x" and 2: "x  ?B"
          by (metis (no_types, lifting) image_iff permute_set_eq_image)
        from 2 obtain Q where 3: "x = distinguishing_formula P Q" and 4: "¬ (P =⋅ Q)"
          by blast
        with 1 have "px = distinguishing_formula (p  P) (p  Q)"
          by simp
        moreover from 4 have "¬ ((p  P) =⋅ (p  Q))"
          by (metis logically_equivalent_eqvt permute_minus_cancel(2))
        ultimately have "px  ?B'"
          by blast
      }
      then show "p  ?B  ?B'"
        by blast
    next
      {
        fix x
        assume "x  ?B'"
        then obtain Q where 1: "x = distinguishing_formula (p  P) Q" and 2: "¬ ((p  P) =⋅ Q)"
          by blast
        from 2 have "¬ (P =⋅ (-p  Q))"
          by (metis logically_equivalent_eqvt permute_minus_cancel(1))
        moreover from this and 1 have "x = p  distinguishing_formula P (-p  Q)"
          by simp
        ultimately have "x  p  ?B"
          using mem_permute_iff by blast
      }
      then show "?B'  p  ?B"
        by blast
    qed

    with "*" show ?thesis
      unfolding characteristic_formula_def by simp
  qed

  lemma characteristic_formula_eqvt_raw [simp]:
    "p  characteristic_formula = characteristic_formula"
    by (simp add: permute_fun_def)

  lemma characteristic_formula_is_characteristic':
    "Q  characteristic_formula P  P =⋅ Q"
  proof -
    let ?B = "{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}"

    {
      fix P'
      have "supp (Abs_bset ?B :: _ set['idx])  supp P"
        by (fact characteristic_formula_supp_aux)
      then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
        using finite_supp rev_finite_subset by blast
      with characteristic_formula_card_aux have "P'  characteristic_formula P  (x?B. P'  x)"
        unfolding characteristic_formula_def by simp
    }
    note valid_characteristic_formula = this

    show ?thesis
    proof
      assume *: "Q  characteristic_formula P"
      show "P =⋅ Q"
      proof (rule ccontr)
        assume "¬ (P =⋅ Q)"
        with "*" show False
          using distinguishing_formula_distinguishes is_distinguishing_formula_def valid_characteristic_formula by auto
      qed
    next
      assume "P =⋅ Q"
      moreover have "P  characteristic_formula P"
        using distinguishing_formula_distinguishes is_distinguishing_formula_def valid_characteristic_formula by auto
      ultimately show "Q  characteristic_formula P"
        using logically_equivalent_def by blast
    qed
  qed

  lemma characteristic_formula_is_characteristic:
    "Q  characteristic_formula P  P ∼⋅ Q"
    using characteristic_formula_is_characteristic' by (meson bisimilarity_implies_equivalence equivalence_implies_bisimilarity)


  subsection ‹Expressive completeness›
  
  text ‹Every finitely supported set of states that is closed under bisimulation can be described by
    a formula; namely, by a disjunction of characteristic formulas.›

  theorem expressive_completeness:
    assumes "finite (supp S)"
    and "P Q. P  S  P ∼⋅ Q  Q  S"
    shows "P  Disj (Abs_bset (characteristic_formula ` S))  P  S"
  proof -
    let ?B = "characteristic_formula ` S"

    have "?B  characteristic_formula ` UNIV"
      by auto
    then have "|?B| ≤o |UNIV :: 'state set|"
      by (rule surj_imp_ordLeq)
    also have "|UNIV :: 'state set| <o |UNIV :: 'idx set|"
      by (metis card_idx_state)
    also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|"
      by (metis Cnotzero_UNIV ordLeq_csum2)
    finally have card_B: "|?B| <o natLeq +c |UNIV :: 'idx set|" .

    have "eqvt image" and "eqvt characteristic_formula"
      by (simp add: eqvtI)+
    then have "supp ?B  supp S"
      using supp_fun_eqvt supp_fun_app supp_fun_app_eqvt by blast
    with card_B have "supp (Abs_bset ?B :: _ set['idx])  supp S"
      using supp_Abs_bset by blast
    with ‹finite (supp S) have "finite (supp (Abs_bset ?B :: _ set['idx]))"
      using finite_supp rev_finite_subset by blast
    with card_B have "P  Disj (Abs_bset (characteristic_formula ` S))  (x?B. P  x)"
      by simp

    with P Q. P  S  P ∼⋅ Q  Q  S show ?thesis
      using characteristic_formula_is_characteristic characteristic_formula_is_characteristic' logically_equivalent_def by fastforce
  qed

end

end

Theory FS_Set

theory FS_Set
imports
  Nominal2.Nominal2
begin

section ‹Finitely Supported Sets›

text ‹We define the type of finitely supported sets (over some permutation type~@{typ "'a::pt"}).

Note that we cannot more generally define the (sub-)type of finitely supported elements for
arbitrary permutation types~@{typ "'a::pt"}: there is no guarantee that this type is non-empty.›

typedef 'a fs_set = "{x::'a::pt set. finite (supp x)}"
  by (simp add: exI[where x="{}"] supp_set_empty)

setup_lifting type_definition_fs_set

text ‹Type~@{typ "'a fs_set"} is a finitely supported permutation type.›

instantiation fs_set :: (pt) pt
begin

  lift_definition permute_fs_set :: "perm  'a fs_set  'a fs_set" is permute
    by (metis permute_finite supp_eqvt)

  instance
   apply (intro_classes)
    apply (metis (mono_tags) permute_fs_set.rep_eq Rep_fs_set_inverse permute_zero)
   apply (metis (mono_tags) permute_fs_set.rep_eq Rep_fs_set_inverse permute_plus)
  done

end

instantiation fs_set :: (pt) fs
begin

  instance
  proof (intro_classes)
    fix x :: "'a fs_set"
    from Rep_fs_set have "finite (supp (Rep_fs_set x))" by simp
    hence "finite {a. infinite {b. (a  b)  Rep_fs_set x  Rep_fs_set x}}" by (unfold supp_def)
    hence "finite {a. infinite {b. ((a  b)  x)   x}}" by transfer
    thus "finite (supp x)" by (fold supp_def)
  qed

end

text ‹Set membership.›

lift_definition member_fs_set :: "'a::pt  'a fs_set  bool" is "(∈)" .

notation
  member_fs_set ("'(∈fs')") and
  member_fs_set ("(_/ fs _)" [51, 51] 50)

lemma member_fs_set_permute_iff [simp]: "p  x fs p  X  x fs X"
by transfer (simp add: mem_permute_iff)

lemma member_fs_set_eqvt [eqvt]: "x fs X  p  x fs p  X"
by simp

end

Theory FL_Transition_System

theory FL_Transition_System
imports
  Transition_System FS_Set
begin

section ‹Nominal Transition Systems with Effects and \texorpdfstring{$F/L$}{F/L}-Bisimilarity›

subsection ‹Nominal transition systems with effects›

text ‹The paper defines an effect as a finitely supported function from states to states. It then
fixes an equivariant set~@{term } of effects. In our formalization, we avoid working with such a
(carrier) set, and instead introduce a type of (finitely supported) effects together with an
(equivariant) application operator for effects and states.

Equivariance (of the type of effects) is implicitly guaranteed (by the type of~@{const permute}).

\emph{First} represents the (finitely supported) set of effects that must be observed before
following a transition.›

type_synonym 'eff first = "'eff fs_set"

text ‹\emph{Later} is a function that represents how the set~$F$ (for \emph{first}) changes
depending on the action of a transition and the chosen effect.›

type_synonym ('a,'eff) later = "'a × 'eff first × 'eff  'eff first"

locale effect_nominal_ts = nominal_ts satisfies transition
  for satisfies :: "'state::fs  'pred::fs  bool" (infix "" 70)
  and transition :: "'state  ('act::bn,'state) residual  bool" (infix "" 70) +
  fixes effect_apply :: "'effect::fs  'state  'state" ("__" [0,101] 100)
    and L :: "('act,'effect) later"
  assumes effect_apply_eqvt: "eqvt effect_apply"  (* using [eqvt] here generates an error message *)
      and L_eqvt: "eqvt L"  ― ‹@{term L} is assumed to be equivariant.›
                            (* using [eqvt] here generates an error message *)
begin

  lemma effect_apply_eqvt_aux [simp]: "p  effect_apply = effect_apply"
  by (metis effect_apply_eqvt eqvt_def)

  lemma effect_apply_eqvt' [eqvt]: "p  fP = p  f(p  P)"
  by simp

  lemma L_eqvt_aux [simp]: "p  L = L"
  by (metis L_eqvt eqvt_def)

  lemma L_eqvt' [eqvt]: "p  L (α, P, f) = L (p  α, p  P, p  f)"
  by simp

end


subsection ‹\texorpdfstring{$L$}{L}-bisimulations and \texorpdfstring{$F/L$}{F/L}-bisimilarity›

context effect_nominal_ts
begin

  definition is_L_bisimulation:: "('effect first  'state  'state  bool)  bool" where
    "is_L_bisimulation R 
      F. symp (R F) 
          (P Q. R F P Q  (f. f fs F  (φ. fP  φ  fQ  φ))) 
          (P Q. R F P Q  (f. f fs F  (α P'. bn α ♯* (fQ, F, f) 
                  fP  α,P'  (Q'. fQ  α,Q'  R (L (α,F,f)) P' Q'))))"

  definition FL_bisimilar :: "'effect first  'state  'state  bool" where
    "FL_bisimilar F P Q  R. is_L_bisimulation R  (R F) P Q"

  abbreviation FL_bisimilar' ("_ ∼⋅[_] _" [51,0,51] 50) where
    "P ∼⋅[F] Q  FL_bisimilar F P Q"

  text @{term "FL_bisimilar"} is an equivariant relation, and (for every~@{term F}) an
    equivalence.›

  lemma is_L_bisimulation_eqvt [eqvt]:
    assumes "is_L_bisimulation R" shows "is_L_bisimulation (p  R)"
  unfolding is_L_bisimulation_def
  proof (clarify)
    fix F
    have "symp ((p  R) F)" (is ?S)
      using assms unfolding is_L_bisimulation_def by (metis eqvt_lambda symp_eqvt)
    moreover have "P Q. (p  R) F P Q  (f. f fs F  (φ. fP  φ  fQ  φ))" (is ?T)
      proof (clarify)
        fix P Q f φ
        assume pR: "(p  R) F P Q" and effect: "f fs F" and satisfies: "fP  φ"
        from pR have "R (-p  F) (-p  P) (-p  Q)"
          by (simp add: eqvt_lambda permute_bool_def unpermute_def)
        moreover have "(-p  f) fs (-p  F)"
          using effect by simp
        moreover have "-p  f(-p  P)  -p  φ"
          using satisfies by (metis effect_apply_eqvt' satisfies_eqvt)
        ultimately have "-p  f(-p  Q)  -p  φ"
          using assms unfolding is_L_bisimulation_def by auto
        then show "fQ  φ"
          by (metis (full_types) effect_apply_eqvt' permute_minus_cancel(1) satisfies_eqvt)
      qed
    moreover have "P Q. (p  R) F P Q  (f. f fs F  (α P'. bn α ♯* (fQ, F, f) 
                                fP  α,P'  (Q'. fQ  α,Q'  (p  R) (L (α, F, f)) P' Q')))" (is ?U)
      proof (clarify)
        fix P Q f α P'
        assume pR: "(p  R) F P Q" and effect: "f fs F" and fresh: "bn α ♯* (fQ, F, f)" and trans: "fP  α,P'"
        from pR have "R (-p  F) (-p  P) (-p  Q)"
          by (simp add: eqvt_lambda permute_bool_def unpermute_def)
        moreover have "(-p  f) fs (-p  F)"
          using effect by simp
        moreover have "bn (-p  α) ♯* (-p  f(-p  Q), -p  F, -p  f)"
          using fresh by (metis (full_types) effect_apply_eqvt' bn_eqvt fresh_star_Pair fresh_star_permute_iff)
        moreover have "-p  f(-p  P)  -p  α, -p  P'"
          using trans by (metis effect_apply_eqvt' transition_eqvt')
        ultimately obtain Q' where T: "-p  f(-p  Q)  -p  α,Q'" and R: "R (L (-p  α, -p  F, -p  f)) (-p  P') Q'"
          using assms unfolding is_L_bisimulation_def by meson
        from T have "fQ  α, p  Q'"
          by (metis (no_types, lifting) effect_apply_eqvt' abs_residual_pair_eqvt permute_minus_cancel(1) transition_eqvt)
        moreover from R have "(p  R) (p  L (-p  α, -p  F, -p  f)) (p  -p  P') (p  Q')"
          by (metis permute_boolI permute_fun_def permute_minus_cancel(2))
        then have "(p  R) (L (α,F,f)) P' (p  Q')"
          by (simp add: permute_self)
        ultimately show "Q'. fQ  α,Q'  (p  R) (L (α,F,f)) P' Q'"
          by metis
      qed
    ultimately show "?S  ?T  ?U" by simp
  qed

  lemma FL_bisimilar_eqvt:
    assumes "P ∼⋅[F] Q" shows "(p  P) ∼⋅[p  F] (p  Q)"
  using assms
  by (metis eqvt_apply permute_boolI is_L_bisimulation_eqvt FL_bisimilar_def)

  lemma FL_bisimilar_reflp: "reflp (FL_bisimilar F)"
  proof (rule reflpI)
    fix x
    have "is_L_bisimulation (λ_. (=))"
      unfolding is_L_bisimulation_def by (simp add: symp_def)
    then show "x ∼⋅[F] x"
      unfolding FL_bisimilar_def by auto
  qed

  lemma FL_bisimilar_symp: "symp (FL_bisimilar F)"
  proof (rule sympI)
    fix P Q
    assume "P ∼⋅[F] Q"
    then obtain R where *: "is_L_bisimulation R  R F P Q"
      unfolding FL_bisimilar_def ..
    then have "R F Q P"
      unfolding is_L_bisimulation_def by (simp add: symp_def)
    with "*" show "Q ∼⋅[F] P"
      unfolding FL_bisimilar_def by auto
  qed

  lemma FL_bisimilar_is_L_bisimulation: "is_L_bisimulation FL_bisimilar"
  unfolding is_L_bisimulation_def proof
    fix F
    have "symp (FL_bisimilar F)" (is ?R)
      by (fact FL_bisimilar_symp)
    moreover have "P Q. P ∼⋅[F] Q  (f. f fs F  (φ. fP  φ  fQ  φ))" (is ?S)
      by (auto simp add: is_L_bisimulation_def FL_bisimilar_def)
    moreover have "P Q. P ∼⋅[F] Q  (f. f fs F  (α P'. bn α ♯* (fQ, F, f) 
          fP  α,P'  (Q'. fQ  α,Q'  P' ∼⋅[L (α, F, f)] Q')))" (is ?T)
      by (auto simp add: is_L_bisimulation_def FL_bisimilar_def) blast
    ultimately show "?R  ?S  ?T"
      by metis
  qed

  lemma FL_bisimilar_simulation_step:
    assumes "P ∼⋅[F] Q" and "f fs F" and "bn α ♯* (fQ, F, f)" and "fP  α,P'"
    obtains Q' where "fQ  α,Q'" and "P' ∼⋅[L (α,F,f)] Q'"
  using assms by (metis (poly_guards_query) FL_bisimilar_is_L_bisimulation is_L_bisimulation_def)

  lemma FL_bisimilar_transp: "transp (FL_bisimilar F)"
  proof (rule transpI)
    fix P Q R
    assume PQ: "P ∼⋅[F] Q" and QR: "Q ∼⋅[F] R"
    let ?FL_bisim = "λF. (FL_bisimilar F) OO (FL_bisimilar F)"
    have "F. symp (?FL_bisim F)"
      proof (rule sympI)
        fix F P R
        assume "?FL_bisim F P R"
        then obtain Q where "P ∼⋅[F] Q" and "Q ∼⋅[F] R"
          by blast
        then have "R ∼⋅[F] Q" and "Q ∼⋅[F] P"
          by (metis FL_bisimilar_symp sympE)+
        then show "?FL_bisim F R P"
          by blast
      qed
    moreover have "F. P Q. ?FL_bisim F P Q  (f. f fs F  (φ. fP  φ  fQ  φ))"
      using FL_bisimilar_is_L_bisimulation is_L_bisimulation_def by auto
    moreover have "F. P Q. ?FL_bisim F P Q 
           (f. f fs F  (α P'. bn α ♯* (fQ, F, f) 
                     fP  α,P'  (Q'. fQ  α,Q'  ?FL_bisim (L (α,F,f)) P' Q')))"
      proof (clarify)
        fix F P R Q f α P'
        assume PR: "P ∼⋅[F] R" and RQ: "R ∼⋅[F] Q" and effect: "f fs F" and fresh: "bn α ♯* (fQ, F, f)" and trans: "fP  α,P'"
        ― ‹rename~@{term "α,P'"} to avoid~@{term "(fR, F)"}, without touching~@{term "(fQ, F, f)"}
        obtain p where 1: "(p  bn α) ♯* (fR, F, f)" and 2: "supp (α,P', (fQ, F, f)) ♯* p"
          proof (rule at_set_avoiding2[of "bn α" "(fR, F, f)" "(α,P', (fQ, F, f))", THEN exE])
            show "finite (bn α)" by (fact bn_finite)
          next
            show "finite (supp (fR, F, f))" by (fact finite_supp)
          next
            show "finite (supp (α,P', (fQ, F, f)))" by (simp add: finite_supp supp_Pair)
          next
            show "bn α ♯* (α,P', (fQ, F, f))"
              using bn_abs_residual_fresh fresh fresh_star_Pair by blast
          qed metis
        from 2 have 3: "supp α,P' ♯* p" and 4: "supp (fQ, F, f) ♯* p"
          by (simp add: fresh_star_Un supp_Pair)+
        from 3 have "p  α, p  P' = α,P'"
          using supp_perm_eq by fastforce
        then obtain pR' where 5: "fR  p  α, pR'" and 6: "(p  P') ∼⋅[L (p  α,F,f)] pR'"
          using PR effect trans 1 by (metis FL_bisimilar_simulation_step bn_eqvt)
        from fresh and 4 have "bn (p  α) ♯* (fQ, F, f)"
          by (metis bn_eqvt fresh_star_permute_iff supp_perm_eq)
        then obtain pQ' where 7: "fQ  p  α, pQ'" and 8: "pR' ∼⋅[L (p  α,F,f)] pQ'"
          using RQ effect 5 by (metis FL_bisimilar_simulation_step)
        from 4 have "supp (fQ) ♯* p"
          by (simp add: fresh_star_Un supp_Pair)
        with 7 have "fQ  α, -p  pQ'"
          by (metis permute_minus_cancel(2) supp_perm_eq transition_eqvt')
        moreover from 6 and 8 have "?FL_bisim (L (p  α, F, f)) (p  P') pQ'"
          by (metis relcompp.relcompI)
        then have "?FL_bisim (-p  L (p  α, F, f)) (-p  p  P') (-p  pQ')"
          using FL_bisimilar_eqvt by blast
        then have "?FL_bisim (L (α, -p  F, -p  f)) P' (-p  pQ')"
          by (simp add: L_eqvt')
        then have "?FL_bisim (L (α,F,f)) P' (-p  pQ')"
          using 4 by (metis fresh_star_Un permute_minus_cancel(2) supp_Pair supp_perm_eq)
        ultimately show "Q'. fQ  α,Q'  ?FL_bisim (L (α,F,f)) P' Q'"
          by metis
      qed
    ultimately have "is_L_bisimulation ?FL_bisim"
      unfolding is_L_bisimulation_def by metis
    moreover have "?FL_bisim F P R"
      using PQ QR by blast
    ultimately show "P ∼⋅[F] R"
      unfolding FL_bisimilar_def by meson
  qed

  lemma FL_bisimilar_equivp: "equivp (FL_bisimilar F)"
  by (metis FL_bisimilar_reflp FL_bisimilar_symp FL_bisimilar_transp equivp_reflp_symp_transp)

end

end

Theory FL_Formula

theory FL_Formula
imports
  Nominal_Bounded_Set
  Nominal_Wellfounded
  Residual
  FL_Transition_System
begin

section ‹Infinitary Formulas With Effects›

subsection ‹Infinitely branching trees›

text ‹First, we define a type of trees, with a constructor~@{term tConj} that maps (potentially
infinite) sets of trees into trees. To avoid paradoxes (note that there is no injection from the
powerset of trees into the set of trees), the cardinality of the argument set must be bounded.›

text ‹The effect consequence operator~⟨f⟩› is always and only used as a prefix to a
predicate or an action formula. So to simplify the representation of formula trees with effects, the
effect operator is merged into the predicate or action it precedes.›

datatype ('idx,'pred,'act,'eff) Tree =
    tConj "('idx,'pred,'act,'eff) Tree set['idx]"  ― ‹potentially infinite sets of trees›
  | tNot "('idx,'pred,'act,'eff) Tree"
  | tPred 'eff 'pred
  | tAct  'eff 'act "('idx,'pred,'act,'eff) Tree"

text ‹The (automatically generated) induction principle for trees allows us to prove that the
following relation over trees is well-founded. This will be useful for termination proofs when we
define functions by recursion over trees.›

inductive_set Tree_wf :: "('idx,'pred,'act,'eff) Tree rel" where
  "t  set_bset tset  (t, tConj tset)  Tree_wf"
| "(t, tNot t)  Tree_wf"
| "(t, tAct f α t)  Tree_wf"

lemma wf_Tree_wf: "wf Tree_wf"
unfolding wf_def
proof (rule allI, rule impI, rule allI)
  fix P :: "('idx,'pred,'act,'eff) Tree  bool" and t
  assume "x. (y. (y, x)  Tree_wf  P y)  P x"
  then show "P t"
    proof (induction t)
      case tConj then show ?case
        by (metis Tree.distinct(2) Tree.distinct(5) Tree.inject(1) Tree_wf.cases)
    next
      case tNot then show ?case
        by (metis Tree.distinct(1) Tree.distinct(9) Tree.inject(2) Tree_wf.cases)
    next
      case tPred then show ?case
        by (metis Tree.distinct(11) Tree.distinct(3) Tree.distinct(7) Tree_wf.cases)
    next
      case tAct then show ?case
        by (metis Tree.distinct(10) Tree.distinct(6) Tree.inject(4) Tree_wf.cases)
    qed
qed

text ‹We define a permutation operation on the type of trees.›

instantiation Tree :: (type, pt, pt, pt) pt
begin

  primrec permute_Tree :: "perm  (_,_,_,_) Tree  (_,_,_,_) Tree" where
    "p  (tConj tset) = tConj (map_bset (permute p) tset)"  ― ‹neat trick to get around the fact that~@{term tset} is not of permutation type yet›
  | "p  (tNot t) = tNot (p  t)"
  | "p  (tPred f φ) = tPred (p  f) (p  φ)"
  | "p  (tAct f α t) = tAct (p  f) (p  α) (p  t)"

  instance
  proof
    fix t :: "(_,_,_,_) Tree"
    show "0  t = t"
    proof (induction t)
      case tConj then show ?case
        by (simp, transfer) (auto simp: image_def)
    qed simp_all
  next
    fix p q :: perm and t :: "(_,_,_,_) Tree"
    show "(p + q)  t = p  q  t"
      proof (induction t)
        case tConj then show ?case
          by (simp, transfer) (auto simp: image_def)
      qed simp_all
  qed

end

text ‹Now that the type of trees---and hence the type of (bounded) sets of trees---is a permutation
type, we can massage the definition of~@{term "p  tConj tset"} into its more usual form.›

lemma permute_Tree_tConj [simp]: "p  tConj tset = tConj (p  tset)"
by (simp add: map_bset_permute)

declare permute_Tree.simps(1) [simp del]

text ‹The relation~@{const Tree_wf} is equivariant.›

lemma Tree_wf_eqvt_aux:
  assumes "(t1, t2)  Tree_wf" shows "(p  t1, p  t2)  Tree_wf"
using assms proof (induction rule: Tree_wf.induct)
  fix t :: "('a,'b,'c,'d) Tree" and tset :: "('a,'b,'c,'d) Tree set['a]"
  assume "t  set_bset tset" then show "(p  t, p  tConj tset)  Tree_wf"
    by (metis Tree_wf.intros(1) mem_permute_iff permute_Tree_tConj set_bset_eqvt)
next
  fix t :: "('a,'b,'c,'d) Tree"
  show "(p  t, p  tNot t)  Tree_wf"
    by (metis Tree_wf.intros(2) permute_Tree.simps(2))
next
  fix t :: "('a,'b,'c,'d) Tree" and f and  α
  show "(p  t, p  tAct f α t)  Tree_wf"
    by (metis Tree_wf.intros(3) permute_Tree.simps(4))
qed

lemma Tree_wf_eqvt [eqvt, simp]: "p  Tree_wf = Tree_wf"
proof
  show "p  Tree_wf  Tree_wf"
    by (auto simp add: permute_set_def) (rule Tree_wf_eqvt_aux)
next
  show "Tree_wf  p  Tree_wf"
    by (auto simp add: permute_set_def) (metis Tree_wf_eqvt_aux permute_minus_cancel(1))
qed

lemma Tree_wf_eqvt': "eqvt Tree_wf"
by (metis Tree_wf_eqvt eqvtI)

text ‹The definition of~@{const permute} for trees gives rise to the usual notion of support. The
following lemmas, one for each constructor, describe the support of trees.›

lemma supp_tConj [simp]: "supp (tConj tset) = supp tset"
unfolding supp_def by simp

lemma supp_tNot [simp]: "supp (tNot t) = supp t"
unfolding supp_def by simp

lemma supp_tPred [simp]: "supp (tPred f φ) = supp f  supp φ"
unfolding supp_def by (simp add: Collect_imp_eq Collect_neg_eq)

lemma supp_tAct [simp]: "supp (tAct f α t) = supp f  supp α  supp t"
unfolding supp_def by (auto simp add: Collect_imp_eq Collect_neg_eq)


subsection ‹Trees modulo \texorpdfstring{$\alpha$}{alpha}-equivalence›

text ‹We generalize the notion of support, which considers whether a permuted element is
\emph{equal} to itself, to arbitrary endorelations. This is available as @{const supp_rel} in
Nominal Isabelle.›

lemma supp_rel_eqvt [eqvt]:
  "p  supp_rel R x = supp_rel (p  R) (p  x)"
by (simp add: supp_rel_def)

text ‹Usually, the definition of $\alpha$-equivalence presupposes a notion of free variables.
However, the variables that are ``free'' in an infinitary conjunction are not necessarily those
that are free in one of the conjuncts. For instance, consider a conjunction over \emph{all} names.
Applying any permutation will yield the same conjunction, i.e., this conjunction has \emph{no} free
variables.

To obtain the correct notion of free variables for infinitary conjunctions, we initially defined
$\alpha$-equivalence and free variables via mutual recursion. In particular, we defined the free
variables of a conjunction as term @{term "fv_Tree (tConj tset) = supp_rel alpha_Tree (tConj tset)"}.

We then realized that it is not necessary to define the concept of ``free variables'' at all, but
the definition of $\alpha$-equivalence becomes much simpler (in particular, it is no longer mutually
recursive) if we directly use the support modulo $\alpha$-equivalence.›

text ‹The following lemmas and constructions are used to prove termination of our definition.›

lemma supp_rel_cong [fundef_cong]:
  " x=x'; a b. R ((a  b)  x') x'  R' ((a  b)  x') x'   supp_rel R x = supp_rel R' x'"
by (simp add: supp_rel_def)

lemma rel_bset_cong [fundef_cong]:
  " x=x'; y=y'; a b. a  set_bset x'  b  set_bset y'  R a b  R' a b   rel_bset R x y  rel_bset R' x' y'"
by (simp add: rel_bset_def rel_set_def)

lemma alpha_set_cong [fundef_cong]:
  " bs=bs'; x=x'; R (p'  x') y'  R' (p'  x') y'; f x' = f' x'; f y' = f' y'; p=p'; cs=cs'; y=y'  
    alpha_set (bs, x) R f p (cs, y)  alpha_set (bs', x') R' f' p' (cs', y')"
by (simp add: alpha_set)

quotient_type
  ('idx,'pred,'act,'eff) Treep = "('idx,'pred::pt,'act::bn,'eff::fs) Tree" / "hull_relp"
  by (fact hull_relp_equivp)

lemma abs_Treep_eq [simp]: "abs_Treep (p  t) = abs_Treep t"
by (metis hull_relp.simps Treep.abs_eq_iff)

lemma permute_rep_abs_Treep:
  obtains p where "rep_Treep (abs_Treep t) = p  t"
by (metis Quotient3_Treep Treep.abs_eq_iff rep_abs_rsp hull_relp.simps)

lift_definition Tree_wfp :: "('idx,'pred::pt,'act::bn,'eff::fs) Treep rel" is
  Tree_wf .

lemma Tree_wfpI [simp]:
  assumes "(a, b)  Tree_wf"
  shows "(abs_Treep (p  a), abs_Treep b)  Tree_wfp"
using assms by (metis (erased, lifting) Treep.abs_eq_iff Tree_wfp.abs_eq hull_relp.intros map_prod_simp rev_image_eqI)

lemma Tree_wfp_trivialI [simp]:
  assumes "(a, b)  Tree_wf"
  shows "(abs_Treep a, abs_Treep b)  Tree_wfp"
using assms by (metis Tree_wfpI permute_zero)

lemma Tree_wfpE:
  assumes "(ap, bp)  Tree_wfp"
  obtains a b where "ap = abs_Treep a" and "bp = abs_Treep b" and "(a,b)  Tree_wf"
using assms by (metis (erased, lifting) Pair_inject Tree_wfp.abs_eq prod_fun_imageE) (* DIFF *)

lemma wf_Tree_wfp: "wf Tree_wfp"
apply (rule wf_subset[of "inv_image (hull_rel O Tree_wf) rep_Treep"])
 apply (metis Tree_wf_eqvt' wf_Tree_wf wf_hull_rel_relcomp wf_inv_image)
apply (auto elim!: Tree_wfpE)
apply (rename_tac t1 t2)
apply (rule_tac t=t1 in permute_rep_abs_Treep)
apply (rule_tac t=t2 in permute_rep_abs_Treep)
apply (rename_tac p1 p2)
apply (subgoal_tac "(p2  t1, p2  t2)  Tree_wf")
 apply (subgoal_tac "(p1  t1, p2  t1)  hull_rel")
  apply (metis relcomp.relcompI)
 apply (metis hull_rel.simps permute_minus_cancel(2) permute_plus)
apply (metis Tree_wf_eqvt_aux)
done

fun alpha_Tree_termination :: "('a, 'b, 'c, 'd) Tree × ('a, 'b, 'c, 'd) Tree  ('a, 'b::pt, 'c::bn, 'd::fs) Treep set" where
  "alpha_Tree_termination (t1, t2) = {abs_Treep t1, abs_Treep t2}"

text ‹Here it comes \ldots›

function (sequential)
  alpha_Tree :: "('idx,'pred::pt,'act::bn,'eff::fs) Tree  ('idx,'pred,'act,'eff) Tree  bool" (infix "=α" 50) where
― ‹@{const alpha_Tree}
  alpha_tConj: "tConj tset1 =α tConj tset2  rel_bset alpha_Tree tset1 tset2"
| alpha_tNot: "tNot t1 =α tNot t2  t1 =α t2"
| alpha_tPred: "tPred f1 φ1 =α tPred f2 φ2  f1 = f2  φ1 = φ2"
― ‹the action may have binding names›
| alpha_tAct: "tAct f1 α1 t1 =α tAct f2 α2 t2 
    f1 = f2  (p. (bn α1, t1) ≈set alpha_Tree (supp_rel alpha_Tree) p (bn α2, t2)  (bn α1, α1) ≈set ((=)) supp p (bn α2, α2))"
| alpha_other: "_ =α _  False"
― ‹254 subgoals (!)›
by pat_completeness auto
termination
proof
  let ?R = "inv_image (max_ext Tree_wfp) alpha_Tree_termination"
  show "wf ?R"
    by (metis max_ext_wf wf_Tree_wfp wf_inv_image)
qed (auto simp add: max_ext.simps Tree_wf.simps simp del: permute_Tree_tConj)

text ‹We provide more descriptive case names for the automatically generated induction principle,
and specialize it to an induction rule for $\alpha$-equivalence.›

lemmas alpha_Tree_induct' = alpha_Tree.induct[case_names alpha_tConj alpha_tNot
  alpha_tPred alpha_tAct "alpha_other(1)" "alpha_other(2)" "alpha_other(3)" "alpha_other(4)"
  "alpha_other(5)" "alpha_other(6)" "alpha_other(7)" "alpha_other(8)" "alpha_other(9)"
  "alpha_other(10)" "alpha_other(11)" "alpha_other(12)" "alpha_other(13)" "alpha_other(14)"
  "alpha_other(15)" "alpha_other(16)" "alpha_other(17)" "alpha_other(18)"]

lemma alpha_Tree_induct[case_names tConj tNot tPred tAct, consumes 1]:
  assumes "t1 =α t2"
  and "tset1 tset2. (a b. a  set_bset tset1  b  set_bset tset2  a =α b  P a b) 
            rel_bset (=α) tset1 tset2  P (tConj tset1) (tConj tset2)"
  and "t1 t2. t1 =α t2  P t1 t2  P (tNot t1) (tNot t2)"
  and "f φ. P (tPred f φ) (tPred f φ)"
  and "f1 α1 t1 f2 α2 t2. (p. p  t1 =α t2  P (p  t1) t2)  f1 = f2 
            (p. (bn α1, t1) ≈set (=α) (supp_rel (=α)) p (bn α2, t2)  (bn α1, α1) ≈set (=) supp p (bn α2, α2)) 
            P (tAct f1 α1 t1) (tAct f2 α2 t2)"
  shows "P t1 t2"
using assms by (induction t1 t2 rule: alpha_Tree.induct) simp_all

text ‹$\alpha$-equivalence is equivariant.›

lemma alpha_Tree_eqvt_aux:
  assumes "a b. (a  b)  t =α t  p  (a  b)  t =α p  t"
  shows "p  supp_rel (=α) t = supp_rel (=α) (p  t)"
proof -
  {
    fix a
    let ?B = "{b. ¬ ((a  b)  t) =α t}"
    let ?pB =