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, opaque_lifting) 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, opaque_lifting) 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, opaque_lifting) 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 ⟹ (⋀