# Theory Nominal_Bounded_Set

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

section ‹Bounded Sets Equipped With a Permutation Action›

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)"

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)"
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"
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: "∀b∈bn α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)"
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. x∈X ⟹ 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. x∈X ⟹ 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)"
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"
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)"

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)"

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'"

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'"

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')"

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

lemma abs_Tree⇩p_eq [simp]: "abs_Tree⇩p (p ∙ t) = abs_Tree⇩p t"
by (metis hull_relp.simps Tree⇩p.abs_eq_iff)

lemma permute_rep_abs_Tree⇩p:
obtains p where "rep_Tree⇩p (abs_Tree⇩p t) = p ∙ t"
by (metis Quotient3_Tree⇩p Tree⇩p.abs_eq_iff rep_abs_rsp hull_relp.simps)

lift_definition Tree_wf⇩p :: "('idx,'pred::pt,'act::bn) Tree⇩p rel" is
Tree_wf .

lemma Tree_wf⇩pI [simp]:
assumes "(a, b) ∈ Tree_wf"
shows "(abs_Tree⇩p (p ∙ a), abs_Tree⇩p b) ∈ Tree_wf⇩p"
using assms by (metis (erased, lifting) Tree⇩p.abs_eq_iff Tree_wf⇩p.abs_eq hull_relp.intros map_prod_simp rev_image_eqI)

lemma Tree_wf⇩p_trivialI [simp]:
assumes "(a, b) ∈ Tree_wf"
shows "(abs_Tree⇩p a, abs_Tree⇩p b) ∈ Tree_wf⇩p"
using assms by (metis Tree_wf⇩pI permute_zero)

lemma Tree_wf⇩pE:
assumes "(a⇩p, b⇩p) ∈ Tree_wf⇩p"
obtains a b where "a⇩p = abs_Tree⇩p a" and "b⇩p = abs_Tree⇩p b" and "(a,b) ∈ Tree_wf"
using assms by (metis Pair_inject Tree_wf⇩p.abs_eq prod_fun_imageE)

lemma wf_Tree_wf⇩p: "wf Tree_wf⇩p"
proof (rule wf_subset[of "inv_image (hull_rel O Tree_wf) rep_Tree⇩p"])
show "wf (inv_image (hull_rel O Tree_wf) rep_Tree⇩p)"
by (metis Tree_wf_eqvt' wf_Tree_wf wf_hull_rel_relcomp wf_inv_image)
next
show "Tree_wf⇩p ⊆ inv_image (hull_rel O Tree_wf) rep_Tree⇩p"
proof (standard, case_tac "x", clarify)
fix a⇩p b⇩p :: "('d, 'e, 'f) Tree⇩p"
assume "(a⇩p, b⇩p) ∈ Tree_wf⇩p"
then obtain a b where 1: "a⇩p = abs_Tree⇩p a" and 2: "b⇩p = abs_Tree⇩p b" and 3: "(a,b) ∈ Tree_wf"
by (rule Tree_wf⇩pE)
from 1 obtain p where 4: "rep_Tree⇩p a⇩p = p ∙ a"
by (metis permute_rep_abs_Tree⇩p)
from 2 obtain q where 5: "rep_Tree⇩p b⇩p = q ∙ b"
by (metis permute_rep_abs_Tree⇩p)
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 "(a⇩p, b⇩p) ∈ inv_image (hull_rel O Tree_wf) rep_Tree⇩p"
using 4 5 by auto
qed
qed

fun alpha_Tree_termination :: "('a, 'b, 'c) Tree × ('a, 'b, 'c) Tree ⇒ ('a, 'b::pt, 'c::bn) Tree⇩p set" where
"alpha_Tree_termination (t1, t2) = {abs_Tree⇩p t1, abs_Tree⇩p 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_wf⇩p) alpha_Tree_termination"
show "wf ?R"
by (metis max_ext_wf wf_Tree_wf⇩p 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"
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"
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 "∃y∈set_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 "∃x∈set_bset (p ∙ tset1). x =⇩α y" ..
}
ultimately show "p ∙ tConj tset1 =⇩α p ∙ tConj tset2"
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 "∃y∈set_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 "∃x∈set_bset tset1. x =⇩α y" ..
}
ultimately show "tConj tset1 =⇩α tConj tset2"
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"
moreover from 2 have "p ∙ q ∙ -p ∙ bn (p ∙ α1) = bn (p ∙ α2)"
ultimately have "(bn (p ∙ α1), p ∙ t1) ≈set (=⇩α) (supp_rel (=⇩α)) (p + q - p) (bn (p ∙ α2), p ∙ t2)"
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)"
}
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"
moreover have "-p ∙ q ∙ p ∙ bn α1 = bn α2"
ultimately have "(bn α1, α1) ≈set (=) supp (-p + q + p) (bn α2, α2)"
}
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
next
case tNot then show ?case
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
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 α)"
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 α"
then have "b ∈ {b. ¬ (x ⇌ b) ∙ tAct α t =⇩α tAct α t}"
}
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"
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 α"
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"
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⇩α))"
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⇩α)"
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 ∙ φ)"

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⇩α"
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⇩α"
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"

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"
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)"
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: "∀b∈bn α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⇩α'"
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"
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"
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"
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) ⟷ (∀t∈set_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"
next
fix P :: 'state and t :: "('idx,'pred,'act) Tree"
show "((P, t), (P, tNot t)) ∈ ?R"
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"
}
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 ⟷ (∀x∈set_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"
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"
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''"
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"
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 ⟷ (∃x∈set_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)"
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"

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"
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 ("'(∈⇩f⇩s')") and
member_fs_set ("(_/ ∈⇩f⇩s _)" [51, 51] 50)

lemma member_fs_set_permute_iff [simp]: "p ∙ x ∈⇩f⇩s p ∙ X ⟷ x ∈⇩f⇩s X"

lemma member_fs_set_eqvt [eqvt]: "x ∈⇩f⇩s X ⟹ p ∙ x ∈⇩f⇩s 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 ∙ ⟨f⟩P = ⟨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 ∈⇩f⇩s F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))) ∧
(∀P Q. R F P Q ⟶ (∀f. f ∈⇩f⇩s F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶
⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,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 ∈⇩f⇩s F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))" (is ?T)
proof (clarify)
fix P Q f φ
assume pR: "(p ∙ R) F P Q" and effect: "f ∈⇩f⇩s F" and satisfies: "⟨f⟩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) ∈⇩f⇩s (-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 "⟨f⟩Q ⊢ φ"
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 ∈⇩f⇩s F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶
⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,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 ∈⇩f⇩s F" and fresh: "bn α ♯* (⟨f⟩Q, F, f)" and trans: "⟨f⟩P → ⟨α,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) ∈⇩f⇩s (-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 "⟨f⟩Q → ⟨α, 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')"
ultimately show "∃Q'. ⟨f⟩Q → ⟨α,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 ∈⇩f⇩s F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))" (is ?S)
by (auto simp add: is_L_bisimulation_def FL_bisimilar_def)
moreover have "∀P Q. P ∼⋅[F] Q ⟶ (∀f. f ∈⇩f⇩s F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶
⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,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 ∈⇩f⇩s F" and "bn α ♯* (⟨f⟩Q, F, f)" and "⟨f⟩P → ⟨α,P'⟩"
obtains Q' where "⟨f⟩Q → ⟨α,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 ∈⇩f⇩s F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))"
using FL_bisimilar_is_L_bisimulation is_L_bisimulation_def by auto
moreover have "⋀F. ∀P Q. ?FL_bisim F P Q ⟶
(∀f. f ∈⇩f⇩s F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶
⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,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 ∈⇩f⇩s F" and fresh: "bn α ♯* (⟨f⟩Q, F, f)" and trans: "⟨f⟩P → ⟨α,P'⟩"
― ‹rename~@{term "⟨α,P'⟩"} to avoid~@{term "(⟨f⟩R, F)"}, without touching~@{term "(⟨f⟩Q, F, f)"}›
obtain p where 1: "(p ∙ bn α) ♯* (⟨f⟩R, F, f)" and 2: "supp (⟨α,P'⟩, (⟨f⟩Q, F, f)) ♯* p"
proof (rule at_set_avoiding2[of "bn α" "(⟨f⟩R, F, f)" "(⟨α,P'⟩, (⟨f⟩Q, F, f))", THEN exE])
show "finite (bn α)" by (fact bn_finite)
next
show "finite (supp (⟨f⟩R, F, f))" by (fact finite_supp)
next
show "finite (supp (⟨α,P'⟩, (⟨f⟩Q, F, f)))" by (simp add: finite_supp supp_Pair)
next
show "bn α ♯* (⟨α,P'⟩, (⟨f⟩Q, 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 (⟨f⟩Q, F, f) ♯* p"
from 3 have "⟨p ∙ α, p ∙ P'⟩ = ⟨α,P'⟩"
using supp_perm_eq by fastforce
then obtain pR' where 5: "⟨f⟩R → ⟨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 ∙ α) ♯* (⟨f⟩Q, F, f)"
by (metis bn_eqvt fresh_star_permute_iff supp_perm_eq)
then obtain pQ' where 7: "⟨f⟩Q → ⟨p ∙ α, pQ'⟩" and 8: "pR' ∼⋅[L (p ∙ α,F,f)] pQ'"
using RQ effect 5 by (metis FL_bisimilar_simulation_step)
from 4 have "supp (⟨f⟩Q) ♯* p"
with 7 have "⟨f⟩Q → ⟨α, -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')"
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'. ⟨f⟩Q → ⟨α,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)"

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)"

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'"

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'"

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')"

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

lemma abs_Tree⇩p_eq [simp]: "abs_Tree⇩p (p ∙ t) = abs_Tree⇩p t"
by (metis hull_relp.simps Tree⇩p.abs_eq_iff)

lemma permute_rep_abs_Tree⇩p:
obtains p where "rep_Tree⇩p (abs_Tree⇩p t) = p ∙ t"
by (metis Quotient3_Tree⇩p Tree⇩p.abs_eq_iff rep_abs_rsp hull_relp.simps)

lift_definition Tree_wf⇩p :: "('idx,'pred::pt,'act::bn,'eff::fs) Tree⇩p rel" is
Tree_wf .

lemma Tree_wf⇩pI [simp]:
assumes "(a, b) ∈ Tree_wf"
shows "(abs_Tree⇩p (p ∙ a), abs_Tree⇩p b) ∈ Tree_wf⇩p"
using assms by (metis (erased, lifting) Tree⇩p.abs_eq_iff Tree_wf⇩p.abs_eq hull_relp.intros map_prod_simp rev_image_eqI)

lemma Tree_wf⇩p_trivialI [simp]:
assumes "(a, b) ∈ Tree_wf"
shows "(abs_Tree⇩p a, abs_Tree⇩p b) ∈ Tree_wf⇩p"
using assms by (metis Tree_wf⇩pI permute_zero)

lemma Tree_wf⇩pE:
assumes "(a⇩p, b⇩p) ∈ Tree_wf⇩p"
obtains a b where "a⇩p = abs_Tree⇩p a" and "b⇩p = abs_Tree⇩p b" and "(a,b) ∈ Tree_wf"
using assms by (metis (erased, lifting) Pair_inject Tree_wf⇩p.abs_eq prod_fun_imageE) (* DIFF *)

lemma wf_Tree_wf⇩p: "wf Tree_wf⇩p"
apply (rule wf_subset[of "inv_image (hull_rel O Tree_wf) rep_Tree⇩p"])
apply (metis Tree_wf_eqvt' wf_Tree_wf wf_hull_rel_relcomp wf_inv_image)
apply (auto elim!: Tree_wf⇩pE)
apply (rename_tac t1 t2)
apply (rule_tac t=t1 in permute_rep_abs_Tree⇩p)
apply (rule_tac t=t2 in permute_rep_abs_Tree⇩p)
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) Tree⇩p set" where
"alpha_Tree_termination (t1, t2) = {abs_Tree⇩p t1, abs_Tree⇩p 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_wf⇩p) alpha_Tree_termination"
show "wf ?R"
by (metis max_ext_wf wf_Tree_wf⇩p 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 =