Theory FL_Formula

theory FL_Formula
imports
  Nominal_Bounded_Set
  Nominal_Wellfounded
  Residual
  FL_Transition_System
begin

section ‹Infinitary Formulas With Effects›

subsection ‹Infinitely branching trees›

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

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

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

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

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

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

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

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

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

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

end

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

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

declare permute_Tree.simps(1) [simp del]

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

lemma supp_rel_cong [fundef_cong]:
  "⟦ x=x'; ⋀a b. R ((a ⇌ b) ∙ x') x' ⟷ R' ((a ⇌ b) ∙ x') x' ⟧ ⟹ supp_rel R x = supp_rel R' x'"
by (simp add: supp_rel_def)

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

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

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

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

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

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

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

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

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

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

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

text ‹Here it comes \ldots›

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

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

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

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

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

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

lemma alpha_Tree_eqvt': "t1 =α t2 ⟷ p ∙ t1 =α p ∙ t2"
proof (induction t1 t2 rule: alpha_Tree_induct')
  case (alpha_tConj tset1 tset2) show ?case
  proof
    assume *: "tConj tset1 =α tConj tset2"
    {
      fix x
      assume "x ∈ set_bset (p ∙ tset1)"
      then obtain x' where 1: "x' ∈ set_bset tset1" and 2: "x = p ∙ x'"
        by (metis imageE permute_bset.rep_eq permute_set_eq_image)
      from 1 obtain y' where 3: "y' ∈ set_bset tset2" and 4: "x' =α y'"
        using "*" by (metis (mono_tags, lifting) FL_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) FL_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"
      by (simp add: rel_bset_def rel_set_def)
  next
    assume *: "p ∙ tConj tset1 =α p ∙ tConj tset2"
    {
      fix x
      assume 1: "x ∈ set_bset tset1"
      then have "p ∙ x ∈ set_bset (p ∙ tset1)"
        by (metis mem_permute_iff set_bset_eqvt)
      then obtain y' where 2: "y' ∈ set_bset (p ∙ tset2)" and 3: "p ∙ x =α y'"
        using "*" by (metis FL_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 FL_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"
      by (simp add: rel_bset_def rel_set_def)
  qed
next
  case (alpha_tAct f1 α1 t1 f2 α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 f1 α1 t1 =α tAct f2 α2 t2"
    then obtain q where 0: "f1 = f2" and 1: "(bn α1, t1) ≈set (=α) (supp_rel (=α)) q (bn α2, t2)" and 2: "(bn α1, α1) ≈set (=) supp q (bn α2, α2)"
      by auto
    from 1 and t1 and t2 have "supp_rel (=α) (p ∙ t1) - bn (p ∙ α1) = supp_rel (=α) (p ∙ t2) - bn (p ∙ α2)"
      by (metis Diff_eqvt alpha_set bn_eqvt)
    moreover from 1 and t1 have "(supp_rel (=α) (p ∙ t1) - bn (p ∙ α1)) ♯* (p + q - p)"
      by (metis Diff_eqvt alpha_set bn_eqvt fresh_star_permute_iff permute_perm_def)
    moreover from 1 and alpha_tAct.IH(1) have "p ∙ q ∙ t1 =α p ∙ t2"
      by (simp add: alpha_set)
    moreover from 2 have "p ∙ q ∙ -p ∙ bn (p ∙ α1) = bn (p ∙ α2)"
      by (simp add: alpha_set bn_eqvt)
    ultimately have "(bn (p ∙ α1), p ∙ t1) ≈set (=α) (supp_rel (=α)) (p + q - p) (bn (p ∙ α2), p ∙ t2)"
      by (simp add: alpha_set)
    moreover from 2 have "(bn (p ∙ α1), p ∙ α1) ≈set (=) supp (p + q - p) (bn (p ∙ α2), p ∙ α2)"
      by (simp add: alpha_set) (metis (mono_tags, lifting) Diff_eqvt bn_eqvt fresh_star_permute_iff permute_minus_cancel(2) permute_perm_def supp_eqvt)
    ultimately show "p ∙ tAct f1 α1 t1 =α p ∙ tAct f2 α2 t2" using 0
      by auto
  next
    assume "p ∙ tAct f1 α1 t1 =α p ∙ tAct f2 α2 t2"
    then obtain q where 0: "f1 = f2" and 1: "(bn (p ∙ α1), p ∙ t1) ≈set (=α) (supp_rel (=α)) q (bn (p ∙ α2), p ∙ t2)" and 2: "(bn (p ∙ α1), p ∙ α1) ≈set (=) supp q (bn (p ∙ α2), p ∙ α2)"
      by auto
    {
      from 1 and t1 and t2 have "supp_rel (=α) t1 - bn α1 = supp_rel (=α) t2 - bn α2"
        by (metis (no_types, lifting) Diff_eqvt alpha_set bn_eqvt permute_eq_iff)
      moreover with 1 and t2 have "(supp_rel (=α) t1 - bn α1) ♯* (- p + q + p)"
        by (auto simp add: fresh_star_def fresh_perm alphas) (metis (no_types, lifting) DiffI bn_eqvt mem_permute_iff permute_minus_cancel(2))
      moreover from 1 have "- p ∙ q ∙ p ∙ t1 =α t2"
        using alpha_tAct.IH(1) by (simp add: alpha_set) (metis (no_types, lifting) permute_eqvt permute_minus_cancel(2))
      moreover from 1 have "- p ∙ q ∙ p ∙ bn α1 = bn α2"
        by (metis alpha_set bn_eqvt permute_minus_cancel(2))
      ultimately have "(bn α1, t1) ≈set (=α) (supp_rel (=α)) (-p + q + p) (bn α2, t2)"
        by (simp add: alpha_set)
    }
    moreover
    {
      from 2 have "supp α1 - bn α1 = supp α2 - bn α2"
        by (metis (no_types, lifting) Diff_eqvt alpha_set bn_eqvt permute_eq_iff supp_eqvt)
      moreover with 2 have "(supp α1 - bn α1) ♯* (-p + q + p)"
        by (auto simp add: fresh_star_def fresh_perm alphas) (metis (no_types, lifting) DiffI bn_eqvt mem_permute_iff permute_minus_cancel(1) supp_eqvt)
      moreover from 2 have "-p ∙ q ∙ p ∙ α1 = α2"
        by (simp add: alpha_set)
      moreover have "-p ∙ q ∙ p ∙ bn α1 = bn α2"
        by (simp add: bn_eqvt calculation(3))
      ultimately have "(bn α1, α1) ≈set (=) supp (-p + q + p) (bn α2, α2)"
        by (simp add: alpha_set)
    }
    ultimately show "tAct f1 α1 t1 =α tAct f2 α2 t2" using 0
      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,'d) 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,'d) 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 f1 α1 t1 f2 α2 t2)
    then obtain p where "f1=f2 ∧ (bn α1, t1) ≈set (=α) (supp_rel (=α)) p (bn α2, t2) ∧ (bn α1, α1) ≈set (=) supp p (bn α2, α2)"
      by auto
    then have "f1=f2 ∧ (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,'d) 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 f1 α1 t1 f2 α2 t2) show ?case
    proof (cases z)
      fix f α t
      assume z: "z = tAct f α t"
      obtain p where 1: "f1=f2 ∧ (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: "f2=f ∧ (bn α2, t2) ≈set (=α) (supp_rel (=α)) q (bn α, t) ∧ (bn α2, α2) ≈set (=) supp q (bn α, α)"
        using tAct.prems z by auto
      have "f1=f ∧ (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)
          moreover have "f1=f"
            using 1 and 2 by simp
          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 f1 α1 t1 =α z"
        using z by auto
    qed (insert tAct.prems, auto)
  qed
qed

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

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

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

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

lemma alpha_Tree_tAct:
  assumes "t1 =α t2"
  shows "tAct f α t1 =α tAct f α 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 f φ) = supp f ∪ supp φ"
unfolding supp_rel_def supp_def by (simp add: Collect_imp_eq Collect_neg_eq)


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 f α t) = supp f ∪ (supp α ∪ supp_rel (=α) t - bn α)"
proof
  show "supp f ∪ (supp α ∪ supp_rel (=α) t - bn α) ⊆ supp_rel (=α) (tAct f α t)"
  proof
    fix x
    assume "x ∈ supp f ∪ (supp α ∪ supp_rel (=α) t - bn α)"
    moreover
    {
      assume x1: "x ∈ supp f"
      from x1 have "infinite {b. (x ⇌ b) ∙ f ≠ f}"
        unfolding supp_def ..
      then have "infinite ({b. (x ⇌ b) ∙ f ≠ f} - supp f)"
        by (simp add: finite_supp)
      moreover
      {
        fix b
        assume "b ∈ {b. (x ⇌ b) ∙ f ≠ f} - supp f"
        then have b1: "(x ⇌ b) ∙ f ≠ f" and b2: "b ∉ supp f"
          by simp+
        then have "sort_of x = sort_of b"
          using swap_different_sorts by fastforce
        then have "(x ⇌ b) ∙ supp f ≠ supp f"
          using b2 x1 using swap_set_in by blast
        then have "b ∈ {b. ¬ (x ⇌ b) ∙ tAct f α t =α tAct f α t}"
          by auto
      }
      ultimately have "infinite {b. ¬ (x ⇌ b) ∙ tAct f α t =α tAct f α t}"
        by (rule infinite_mono)
      then have "x ∈ supp_rel (=α) (tAct f α t)"
        unfolding supp_rel_def ..
    }
    moreover
    {
      assume x1: "x ∈ supp α" and x2: "x ∉ bn α"
      from x1 have "infinite {b. (x ⇌ b) ∙ α ≠ α}"
        unfolding supp_def ..
      then have "infinite ({b. (x ⇌ b) ∙ α ≠ α} - supp α)"
        by (simp add: finite_supp)
      moreover
      {
        fix b
        assume "b ∈ {b. (x ⇌ b) ∙ α ≠ α} - supp α"
        then have b1: "(x ⇌ b) ∙ α ≠ α" and b2: "b ∉ supp α - bn α"
          by simp+
        from b1 have "sort_of x = sort_of b"
          using swap_different_sorts by fastforce
        then have "(x ⇌ b) ∙ (supp α - bn α) ≠ supp α - bn α"
          using b2 x1 x2 by (simp add: swap_set_in)
        then have "b ∈ {b. ¬ (x ⇌ b) ∙ tAct f α t =α tAct f α t}"
          by (auto simp add: alpha_set Diff_eqvt bn_eqvt)
      }
      ultimately have "infinite {b. ¬ (x ⇌ b) ∙ tAct f α t =α tAct f α t}"
        by (rule infinite_mono)
      then have "x ∈ supp_rel (=α) (tAct f α t)"
        unfolding supp_rel_def ..
    }
    moreover
    {
      assume x1: "x ∈ supp_rel (=α) t" and x2: "x ∉ bn α"
      from x1 have "infinite {b. ¬ (x ⇌ b) ∙ t =α t}"
        unfolding supp_rel_def ..
      then have "infinite ({b. ¬ (x ⇌ b) ∙ t =α t} - supp_rel (=α) t)"
        using assms by simp
      moreover
      {
        fix b
        assume "b ∈ {b. ¬ (x ⇌ b) ∙ t =α t} - supp_rel (=α) t"
        then have b1: "¬ (x ⇌ b) ∙ t =α t" and b2: "b ∉ supp_rel (=α) t - bn α"
          by simp+
        from b1 have "(x ⇌ b) ∙ t ≠ t"
          by (metis alpha_Tree_reflp reflpE)
        then have "sort_of x = sort_of b"
          using swap_different_sorts by fastforce
        then have "(x ⇌ b) ∙ (supp_rel (=α) t - bn α) ≠ supp_rel (=α) t - bn α"
          using b2 x1 x2 by (simp add: swap_set_in)
        then have "supp_rel (=α) ((x ⇌ b) ∙ t) - bn ((x ⇌ b) ∙ α) ≠ supp_rel (=α) t - bn α"
          by (simp add: Diff_eqvt bn_eqvt)
        then have "b ∈ {b. ¬ (x ⇌ b) ∙ tAct f α t =α tAct f α t}"
          by (simp add: alpha_set)
      }
      ultimately have "infinite {b. ¬ (x ⇌ b) ∙ tAct f α t =α tAct f α t}"
        by (rule infinite_mono)
      then have "x ∈ supp_rel (=α) (tAct f α t)"
        unfolding supp_rel_def ..
    }
    ultimately show "x ∈ supp_rel (=α) (tAct f α t)"
      by auto
  qed
next
  show "supp_rel (=α) (tAct f α t) ⊆ supp f ∪ (supp α ∪ supp_rel (=α) t - bn α)"
  proof
    fix x
    assume "x ∈ supp_rel (=α) (tAct f α t)"
    then have *: "infinite {b. ¬ (x ⇌ b) ∙ tAct f α t =α tAct f α t}"
      unfolding supp_rel_def ..
    moreover
    {
      fix b
      assume "¬ (x ⇌ b) ∙ tAct f α t =α tAct f α t"
      then have "(x ⇌ b) ∙ f ≠ f ∨ (x ⇌ b) ∙ α ≠ α ∨ ¬ (x ⇌ b) ∙ t =α t"
        using alpha_Tree_tAct by force
    }
    ultimately have "infinite {b. (x ⇌ b) ∙ f ≠ f ∨ (x ⇌ b) ∙ α ≠ α ∨ ¬ (x ⇌ b) ∙ t =α t}"
      using infinite_mono mem_Collect_eq by force
    then have "infinite {b. (x ⇌ b) ∙ f ≠ f} ∨ infinite {b. (x ⇌ b) ∙ α ≠ α} ∨ infinite {b. ¬ (x ⇌ b) ∙ t =α t}"
      by (metis (mono_tags) finite_Collect_disjI)
    then have "x ∈ supp f ∪ supp α ∪ supp_rel (=α) t"
      by (simp add: supp_def supp_rel_def)
    moreover
    {
      assume **: "x ∈ bn α ∧ x ∉ supp f"
      from "*" obtain b where b0: "¬ (x ⇌ b) ∙ tAct f α t =α tAct f α t" and b1: "b ∉ supp f" and b2: "b ∉ supp α" and b3: "b ∉ supp_rel (=α) t"
        using assms by (metis (no_types, lifting) UnCI finite_UnI finite_supp infinite_mono mem_Collect_eq)
      let ?p = "(x ⇌ b)"
      have "supp_rel (=α) ((x ⇌ b) ∙ t) - bn ((x ⇌ b) ∙ α) = supp_rel (=α) t - bn α"
        using "**" and b3 by (metis (no_types, lifting) Diff_eqvt Diff_iff alpha_Tree_eqvt' alpha_Tree_eqvt_aux bn_eqvt swap_set_not_in)
      moreover then have "(supp_rel (=α) ((x ⇌ b) ∙ t) - bn ((x ⇌ b) ∙ α)) ♯* ?p"
        using "**" and b3 by (metis Diff_iff fresh_perm fresh_star_def swap_atom_simps(3))
      moreover have "?p ∙ (x ⇌ b) ∙ t =α t"
        using alpha_Tree_reflp reflpE by force
      moreover have "?p ∙ bn ((x ⇌ b) ∙ α) = bn α"
        by (simp add: bn_eqvt)
      moreover have "supp ((x ⇌ b) ∙ α) - bn ((x ⇌ b) ∙ α) = supp α - bn α"
        using "**" and b2 by (metis (mono_tags, 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 "∃p. (bn ((x ⇌ b) ∙ α), (x ⇌ b) ∙ t) ≈set (=α) supp_rel (=α) p (bn α, t) ∧
                           (bn ((x ⇌ b) ∙ α), (x ⇌ b) ∙ α) ≈set (=) supp p (bn α, α)"
         by (auto simp add: alpha_set.simps)
        moreover have "(x ⇌ b) ∙ f = f" using "**" and b1
           by (simp add: fresh_def swap_fresh_fresh)
      ultimately have "(x ⇌ b) ∙ tAct f α t =α tAct f α t"
        by simp
      with b0 have "False" ..
    }
    ultimately show "x ∈ supp f ∪ (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,'eff) Treeα = "('idx,'pred::pt,'act::bn,'eff::fs) 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, fs) pt
begin

  lift_definition permute_Treeα :: "perm ⇒ ('a,'b,'c,'d) Treeα ⇒ ('a,'b,'c,'d) 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,'eff) Treeα set['idx] ⇒ ('idx,'pred::pt,'act::bn,'eff::fs) 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,'eff) Treeα ⇒ ('idx,'pred::pt,'act::bn,'eff::fs) Treeα" is
  tNot
by simp

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

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

text ‹The lifted constructors are equivariant.›

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

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

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

lemma Actα_eqvt [eqvt, simp]: "p ∙ Actα f α tα = Actα (p ∙ f) (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α f1 φ1 = Predα f2 φ2 ⟷ f1 = f2 ∧ φ1 = φ2"
proof
  assume "Predα f1 φ1 = Predα f2 φ2"
  then have "(tPred f1 φ1 :: ('e, 'b, 'f, 'd) Tree) =α tPred f2 φ2"  ― ‹note the unrelated type› (* WHY? *)
    by (metis Predα.abs_eq Treeα.abs_eq_iff)
  then show "f1 = f2 ∧ φ1 = φ2"
    using alpha_Tree.cases by auto
next
  assume "f1 = f2 ∧ φ1 = φ2" then show "Predα f1 φ1 = Predα f2 φ2"
    by simp
qed

lemma Actα_eq_iff: "Actα f1 α1 t1 = Actα f2 α2 t2 ⟷ tAct f1 α1 (rep_Treeα t1) =α tAct f2 α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α f φ"
  and "Conjα tsetα ≠ Actα f α tα"
  and "Notα tα ≠ Predα f φ"
  and "Notα t1α ≠ Actα f α t2α"
  and "Predα f1 φ ≠ Actα f2 α 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α f φ) = supp f ∪ supp φ"
unfolding supp_def by (simp add: Collect_imp_eq Collect_neg_eq)

lemma supp_Actα [simp]:
  assumes "finite (supp tα)"
  shows "supp (Actα f α tα) = supp f ∪ (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) (* Patience *)


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 "⋀f pred. P (Predα f pred)"
    and "⋀f act tα. P tα ⟹ P (Actα f act tα)"
  shows "P tα"
proof (rule Treeα.abs_induct)
  fix t show "P (abs_Treeα t)"
    proof (induction t)
      case (tConj tset)
        let ?tsetα = "map_bset abs_Treeα tset"
        have "abs_Treeα (tConj tset) = Conjα ?tsetα"
          by (simp add: Conjα.abs_eq)
        then show ?case
          using assms(1) tConj.IH by (metis imageE map_bset.rep_eq)
    next
      case tNot then show ?case
        using assms(2) by (metis Notα.abs_eq)
    next
      case tPred show ?case
        using assms(3) by (metis Predα.abs_eq)
    next
      case tAct then show ?case
        using assms(4) by (metis Actα.abs_eq)
    qed
qed

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


subsection ‹Hereditarily finitely supported trees›

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

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

inductive hereditarily_fs :: "('idx,'pred::fs,'act::bn,'eff::fs) 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α f φ)"
| Actα: "hereditarily_fs tα ⟹ hereditarily_fs (Actα f α 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α f α tα = Actα f' α' 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,'eff::fs) formula = "{tα::('idx,'pred,'act,'eff) 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, fs) pt
begin

  lift_definition permute_formula :: "perm ⇒ ('a,'b,'c,'d) formula ⇒ ('a,'b,'c,'d) 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) 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,'eff) formula set['idx] ⇒ ('idx,'pred::fs,'act::bn,'eff::fs) formula" where
  "Conj xset = Abs_formula (Conjα (map_bset Rep_formula xset))"

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

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

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

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

lift_definition Act :: "'eff ⇒ 'act ⇒ ('idx,'pred,'act,'eff) formula ⇒ ('idx,'pred::fs,'act::bn,'eff::fs) 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 f φ = Pred (p ∙ f) (p ∙ φ)"
by transfer simp

lemma Act_eqvt [eqvt, simp]: "p ∙ Act f α x = Act (p ∙ f) (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 f φ) = supp f ∪ supp φ"
by (metis Pred.rep_eq supp_Predα supp_Rep_formula)

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


text ‹The lifted constructors are injective (partially 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 f1 φ1 = Pred f2 φ2 ⟷ f1 = f2 ∧ φ1 = φ2"
by (metis Pred.rep_eq Predα_eq_iff)

lemma Act_eq_iff: "Act f1 α1 x1 = Act f2 α2 x2 ⟷ Actα f1 α1 (Rep_formula x1) = Actα f2 α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 f1 α1 x1 = Act f2 α2 x2 ⟷
  f1 = f2 ∧ (∃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 have "f1 = f2"
    by (metis Act_eq_iff Actα_eq_iff alpha_tAct)
  moreover from * obtain p where alpha: "(bn α1, rep_Treeα (Rep_formula x1)) ≈set (=α) (supp_rel (=α)) p (bn α2, rep_Treeα (Rep_formula x2))" and eq: "(bn α1, α1) ≈set (=) supp p (bn α2, α2)"
    by (metis Act_eq_iff Actα_eq_iff alpha_tAct)
  from alpha have "supp x1 - bn α1 = supp x2 - bn α2"
    by (metis alpha_set.simps supp_Rep_formula supp_alpha_supp_rel)
  moreover from alpha have "(supp x1 - bn α1) ♯* p"
    by (metis alpha_set.simps supp_Rep_formula supp_alpha_supp_rel)
  moreover from alpha have "p ∙ x1 = x2"
    by (metis Rep_formula_eqvt Rep_formula_inject Treeα.abs_eq_iff Treeα_abs_rep alpha_Tree_permute_rep_commute alpha_set.simps)
  moreover from eq have "supp α1 - bn α1 = supp α2 - bn α2"
    by (metis alpha_set.simps)
  moreover from eq have "(supp α1 - bn α1) ♯* p"
    by (metis alpha_set.simps)
  moreover from eq have "p ∙ α1 = α2"
    by (simp add: alpha_set.simps)
  ultimately show "?r"
    by metis
next
  assume *: "?r"
  then have "f1 = f2"
    by metis
  moreover from * obtain p where 1: "supp x1 - bn α1 = supp x2 - bn α2" and 2: "(supp x1 - bn α1) ♯* p" and 3: "p ∙ x1 = x2"
    and 4: "supp α1 - bn α1 = supp α2 - bn α2" and 5: "(supp α1 - bn α1) ♯* p" and 6: "p ∙ α1 = α2"
    by metis
  from 1 2 3 6 have "(bn α1, rep_Treeα (Rep_formula x1)) ≈set (=α) (supp_rel (=α)) p (bn α2, rep_Treeα (Rep_formula x2))"
    by (metis (no_types, lifting) Rep_formula_eqvt alpha_Tree_permute_rep_commute alpha_set.simps bn_eqvt supp_Rep_formula supp_alpha_supp_rel)
  moreover from 4 5 6 have "(bn α1, α1) ≈set (=) supp p (bn α2, α2)"
    by (simp add: alpha_set.simps bn_eqvt)
  ultimately show "Act f1 α1 x1 = Act f2 α2 x2"
    by (metis Act_eq_iff Actα_eq_iff alpha_tAct)
qed

lemma Act_eq_iff_perm_renaming: "Act f1 α1 x1 = Act f2 α2 x2 ⟷
  f1 = f2 ∧ (∃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 have "f1 = f2"
    by (metis Act_eq_iff_perm)
  moreover from ‹?l› 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 f φ"
  and "finite (supp xset) ⟹ Conj xset ≠ Act f α x"
  and "Not x ≠ Pred f φ"
  and "Not x1 ≠ Act f α x2"
  and "Pred f1 φ ≠ Act f2 α 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 f φ"
    by (metis Conj_rep_eq Pred.rep_eq Treeα_free(2))
next
  show "finite (supp xset) ⟹ Conj xset ≠ Act f α x"
    by (metis Conj_rep_eq Act.rep_eq Treeα_free(3))
next
  show "Not x ≠ Pred f φ"
    by (metis Not.rep_eq Pred.rep_eq Treeα_free(4))
next
  show "Not x1 ≠ Act f α x2"
    by (metis Not.rep_eq Act.rep_eq Treeα_free(5))
next
  show "Pred f1 φ ≠ Act f2 α x"
    by (metis Pred.rep_eq Act.rep_eq Treeα_free(6))
qed


subsection ‹\texorpdfstring{$F/L$}{F/L}-formulas›

context effect_nominal_ts
begin

text ‹The predicate~@{term is_FL_formula} will characterise exactly those formulas in a particular
set~$A^{F/L}$.›

inductive is_FL_formula :: "'effect first ⇒ ('idx,'pred,'act,'effect) formula ⇒ bool"
where
  Conj: "finite (supp xset) ⟹ (⋀x. x ∈ set_bset xset ⟹ is_FL_formula F x) ⟹ is_FL_formula F (Conj xset)"
| Not:  "is_FL_formula F x ⟹ is_FL_formula F (Not x)"
| Pred: "f ∈fs F ⟹ is_FL_formula F (Pred f φ)"
| Act:  "f ∈fs F ⟹ bn α ♯* (F,f) ⟹ is_FL_formula (L (α,F,f)) x ⟹ is_FL_formula F (Act f α x)"

abbreviation in_𝒜 :: "('idx,'pred,'act,'effect) formula ⇒ 'effect first ⇒ bool"
  ("_ ∈ 𝒜[_]" [51,0] 50) where
  "x ∈ 𝒜[F] ≡ is_FL_formula F x"

declare is_FL_formula.induct [case_names Conj Not Pred Act, induct type: formula]

lemma is_FL_formula_eqvt [eqvt]: "x ∈ 𝒜[F] ⟹ p ∙ x ∈ 𝒜[p ∙ F]"
proof (erule is_FL_formula.induct)
  fix xset :: "('a, 'pred, 'act, 'effect) formula set['a]" and F
  assume 1: "finite (supp xset)" and 2: "⋀x. x ∈ set_bset xset ⟹ p ∙ x ∈ 𝒜[p ∙ F]"
  from 1 have "finite (supp (p ∙ xset))"
    by (metis permute_finite supp_eqvt)
  moreover from 2 have "⋀x. x ∈ set_bset (p ∙ xset) ⟹ x ∈ 𝒜[p ∙ F]"
    by (metis (mono_tags) imageE permute_set_eq_image set_bset_eqvt)
  ultimately show "p ∙ Conj xset ∈ 𝒜[p ∙ F]"
    using 1 by (simp add: Conj)
next
  fix F and x :: "('a, 'pred, 'act, 'effect) formula"
  assume "p ∙ x ∈ 𝒜[p ∙ F]"
  then show "p ∙ Not x ∈ 𝒜[p ∙ F]"
    by (simp add: Not)
next
  fix f and F :: "'effect first" and φ
  assume "f ∈fs F"
  then show "p ∙ Pred f φ ∈ 𝒜[p ∙ F]"
    by (simp add: Pred)
next
  fix f F α and x :: "('a, 'pred, 'act, 'effect) formula"
  assume "f ∈fs F" and "bn α ♯* (F,f)" and "p ∙ x ∈ 𝒜[p ∙ L (α, F, f)]"
  then show "p ∙ Act f α x ∈ 𝒜[p ∙ F]"
    by (metis (mono_tags, lifting) Act Act_eqvt L_eqvt' Pair_eqvt bn_eqvt fresh_star_permute_iff member_fs_set_permute_iff)
qed

end

subsection ‹Induction over infinitary formulas›

(* Not needed yet for F/L-formulas, so not done. *)

subsection ‹Strong induction over infinitary formulas›

(* Not needed yet for F/L-formulas, so not done. *)

end