Theory Syntax

section ‹Syntax›

theory Syntax
  imports
    "HOL-Library.Sublist"
    Utilities
begin

subsection ‹Type symbols›

datatype type =
  TInd ("i")
| TBool ("o")
| TFun type type (infixr "→" 101)

primrec type_size :: "type ⇒ nat" where
  "type_size i = 1"
| "type_size o = 1"
| "type_size (α → β) = Suc (type_size α + type_size β)"

primrec subtypes :: "type ⇒ type set" where
  "subtypes i = {}"
| "subtypes o = {}"
| "subtypes (α → β) = {α, β} ∪ subtypes α ∪ subtypes β"

lemma subtype_size_decrease:
  assumes "α ∈ subtypes β"
  shows "type_size α < type_size β"
  using assms by (induction rule: type.induct) force+

lemma subtype_is_not_type:
  assumes "α ∈ subtypes β"
  shows "α ≠ β"
  using assms and subtype_size_decrease by blast

lemma fun_type_atoms_in_subtypes:
  assumes "k < length ts"
  shows "ts ! k ∈ subtypes (foldr (→) ts γ)"
  using assms by (induction ts arbitrary: k) (cases k, use less_Suc_eq_0_disj in ‹fastforce+›)

lemma fun_type_atoms_neq_fun_type:
  assumes "k < length ts"
  shows "ts ! k ≠ foldr (→) ts γ"
  by (fact fun_type_atoms_in_subtypes[OF assms, THEN subtype_is_not_type])

subsection ‹Variables›

text ‹
  Unfortunately, the Nominal package does not support multi-sort atoms yet; therefore, we need to
  implement this support from scratch.
›

type_synonym var = "nat × type"

abbreviation var_name :: "var ⇒ nat" where
  "var_name ≡ fst"

abbreviation var_type :: "var ⇒ type" where
  "var_type ≡ snd"

lemma fresh_var_existence:
  assumes "finite (vs :: var set)"
  obtains x where "(x, α) ∉ vs"
  using ex_new_if_finite[OF infinite_UNIV_nat]
proof -
  from assms obtain x where "x ∉ var_name ` vs"
    using ex_new_if_finite[OF infinite_UNIV_nat] by fastforce
  with that show ?thesis
    by force
qed

lemma fresh_var_name_list_existence:
  assumes "finite (ns :: nat set)"
  obtains ns' where "length ns' = n" and "distinct ns'" and "lset ns' ∩ ns = {}"
using assms proof (induction n arbitrary: thesis)
  case 0
  then show ?case
    by simp
next
  case (Suc n)
  from assms obtain ns' where "length ns' = n" and "distinct ns'" and "lset ns' ∩ ns = {}"
    using Suc.IH by blast
  moreover from assms obtain n' where "n' ∉ lset ns' ∪ ns"
    using ex_new_if_finite[OF infinite_UNIV_nat] by blast
  ultimately
    have "length (n' # ns') = Suc n" and "distinct (n' # ns')" and "lset (n' # ns') ∩ ns = {}"
    by simp_all
  with Suc.prems(1) show ?case
    by blast
qed

lemma fresh_var_list_existence:
  fixes xs :: "var list"
  and ns :: "nat set"
  assumes "finite ns"
  obtains vs' :: "var list"
  where "length vs' = length xs"
  and "distinct vs'"
  and "var_name ` lset vs' ∩ (ns ∪ var_name ` lset xs) = {}"
  and "map var_type vs' = map var_type xs"
proof -
  from assms(1) have "finite (ns ∪ var_name ` lset xs)"
    by blast
  then obtain ns'
    where "length ns' = length xs"
    and "distinct ns'"
    and "lset ns' ∩ (ns ∪ var_name ` lset xs) = {}"
    by (rule fresh_var_name_list_existence)
  define vs'' where "vs'' = zip ns' (map var_type xs)"
  from vs''_def and ‹length ns' = length xs› have "length vs'' = length xs"
    by simp
  moreover from vs''_def and ‹distinct ns'› have "distinct vs''"
    by (simp add: distinct_zipI1)
  moreover have "var_name ` lset vs'' ∩ (ns ∪ var_name ` lset xs) = {}"
    unfolding vs''_def
    using ‹length ns' = length xs› and ‹lset ns' ∩ (ns ∪ var_name ` lset xs) = {}›
    by (metis length_map set_map map_fst_zip)
  moreover from vs''_def have "map var_type vs'' = map var_type xs"
    by (simp add: ‹length ns' = length xs›)
  ultimately show ?thesis
    by (fact that)
qed

subsection ‹Constants›

type_synonym con = "nat × type"

subsection ‹Formulas›

datatype form =
  FVar var
| FCon con
| FApp form form (infixl "·" 200)
| FAbs var form

syntax
  "_FVar" :: "nat ⇒ type ⇒ form" ("_⇘_⇙" [899, 0] 900)
  "_FCon" :: "nat ⇒ type ⇒ form" ("⦃_⦄⇘_⇙" [899, 0] 900)
  "_FAbs" :: "nat ⇒ type ⇒ form ⇒ form" ("(4λ_⇘_⇙./ _)" [0, 0, 104] 104)
translations
  "x⇘α⇙" ⇌ "CONST FVar (x, α)"
  "⦃c⦄⇘α⇙" ⇌ "CONST FCon (c, α)"
  "λx⇘α⇙. A" ⇌ "CONST FAbs (x, α) A"

subsection ‹Generalized operators›

text ‹Generalized application. We define ‹·⇧𝒬⇩⋆ A [B⇩1, B⇩2, …, B⇩n]› as ‹A · B⇩1 · B⇩2 · ⋯ · B⇩n›:›

definition generalized_app :: "form ⇒ form list ⇒ form" ("·⇧𝒬⇩⋆ _ _" [241, 241] 241) where
  [simp]: "·⇧𝒬⇩⋆ A Bs = foldl (·) A Bs"

text ‹Generalized abstraction. We define ‹λ⇧𝒬⇩⋆ [x⇩1, …, x⇩n] A› as ‹λx⇩1. ⋯ λx⇩n. A›:›

definition generalized_abs :: "var list ⇒ form ⇒ form" ("λ⇧𝒬⇩⋆ _ _" [141, 141] 141) where
  [simp]: "λ⇧𝒬⇩⋆ vs A = foldr (λ(x, α) B. λx⇘α⇙. B) vs A"

fun form_size :: "form ⇒ nat" where
  "form_size (x⇘α⇙) = 1"
| "form_size (⦃c⦄⇘α⇙) = 1"
| "form_size (A · B) = Suc (form_size A + form_size B)"
| "form_size (λx⇘α⇙. A) = Suc (form_size A)"

fun form_depth :: "form ⇒ nat" where
  "form_depth (x⇘α⇙) = 0"
| "form_depth (⦃c⦄⇘α⇙) = 0"
| "form_depth (A · B) = Suc (max (form_depth A) (form_depth B))"
| "form_depth (λx⇘α⇙. A) = Suc (form_depth A)"

subsection ‹Subformulas›

fun subforms :: "form ⇒ form set" where
  "subforms (x⇘α⇙) = {}"
| "subforms (⦃c⦄⇘α⇙) = {}"
| "subforms (A · B) = {A, B}"
| "subforms (λx⇘α⇙. A) = {A}"

datatype direction = Left ("«") | Right ("»")
type_synonym position = "direction list"

fun positions :: "form ⇒ position set" where
  "positions (x⇘α⇙) = {[]}"
| "positions (⦃c⦄⇘α⇙) = {[]}"
| "positions (A · B) = {[]} ∪ {« # p | p. p ∈ positions A} ∪ {» # p | p. p ∈ positions B}"
| "positions (λx⇘α⇙. A) = {[]} ∪ {« # p | p. p ∈ positions A}"

lemma empty_is_position [simp]:
  shows "[] ∈ positions A"
  by (cases A rule: positions.cases) simp_all

fun subform_at :: "form ⇒ position ⇀ form" where
  "subform_at A [] = Some A"
| "subform_at (A · B) (« # p) = subform_at A p"
| "subform_at (A · B) (» # p) = subform_at B p"
| "subform_at (λx⇘α⇙. A) (« # p) = subform_at A p"
| "subform_at _ _ = None"

fun is_subform_at :: "form ⇒ position ⇒ form ⇒ bool" ("(_ ≼⇘_⇙/ _)" [51,0,51] 50) where
  "is_subform_at A [] A' = (A = A')"
| "is_subform_at C (« # p) (A · B) = is_subform_at C p A"
| "is_subform_at C (» # p) (A · B) = is_subform_at C p B"
| "is_subform_at C (« # p) (λx⇘α⇙. A) = is_subform_at C p A"
| "is_subform_at _ _ _ = False"

lemma is_subform_at_alt_def:
  shows "A' ≼⇘p⇙ A = (case subform_at A p of Some B ⇒ B = A' | None ⇒ False)"
  by (induction A' p A rule: is_subform_at.induct) auto

lemma superform_existence:
  assumes "B ≼⇘p @ [d]⇙ C"
  obtains A where "B ≼⇘[d]⇙ A" and "A ≼⇘p⇙ C"
  using assms by (induction B p C rule: is_subform_at.induct) auto

lemma subform_at_subforms_con:
  assumes "⦃c⦄⇘α⇙ ≼⇘p⇙ C"
  shows "∄A. A ≼⇘p @ [d]⇙ C"
  using assms by (induction "⦃c⦄⇘α⇙" p C rule: is_subform_at.induct) auto

lemma subform_at_subforms_var:
  assumes "x⇘α⇙ ≼⇘p⇙ C"
  shows "∄A. A ≼⇘p @ [d]⇙ C"
  using assms by (induction "x⇘α⇙" p C rule: is_subform_at.induct) auto

lemma subform_at_subforms_app:
  assumes "A · B ≼⇘p⇙ C"
  shows "A ≼⇘p @ [«]⇙ C" and "B ≼⇘p @ [»]⇙ C"
  using assms by (induction "A · B" p C rule: is_subform_at.induct) auto

lemma subform_at_subforms_abs:
  assumes "λx⇘α⇙. A ≼⇘p⇙ C"
  shows "A ≼⇘p @ [«]⇙ C"
  using assms by (induction "λx⇘α⇙. A" p C rule: is_subform_at.induct) auto

lemma is_subform_implies_in_positions:
  assumes "B ≼⇘p⇙ A"
  shows "p ∈ positions A"
  using assms by (induction rule: is_subform_at.induct) simp_all

lemma subform_size_decrease:
  assumes "A ≼⇘p⇙ B" and "p ≠ []"
  shows "form_size A < form_size B"
  using assms by (induction A p B rule: is_subform_at.induct) force+

lemma strict_subform_is_not_form:
  assumes "p ≠ []" and "A' ≼⇘p⇙ A"
  shows "A' ≠ A"
  using assms and subform_size_decrease by blast

lemma no_right_subform_of_abs:
  shows "∄B. B ≼⇘» # p⇙ λx⇘α⇙. A"
  by simp

lemma subforms_from_var:
  assumes "A ≼⇘p⇙ x⇘α⇙"
  shows "A = x⇘α⇙" and "p = []"
  using assms by (auto elim: is_subform_at.elims)

lemma subforms_from_con:
  assumes "A ≼⇘p⇙ ⦃c⦄⇘α⇙"
  shows "A = ⦃c⦄⇘α⇙" and "p = []"
  using assms by (auto elim: is_subform_at.elims)

lemma subforms_from_app:
  assumes "A ≼⇘p⇙ B · C"
  shows "
    (A = B · C ∧ p = []) ∨
    (A ≠ B · C ∧
      (∃p' ∈ positions B. p = « # p' ∧ A ≼⇘p'⇙ B) ∨ (∃p' ∈ positions C. p = » # p' ∧ A ≼⇘p'⇙ C))"
  using assms and strict_subform_is_not_form
  by (auto simp add: is_subform_implies_in_positions elim: is_subform_at.elims)

lemma subforms_from_abs:
  assumes "A ≼⇘p⇙ λx⇘α⇙. B"
  shows "(A = λx⇘α⇙. B ∧ p = []) ∨ (A ≠ λx⇘α⇙. B ∧ (∃p' ∈ positions B. p = « # p' ∧ A ≼⇘p'⇙ B))"
  using assms and strict_subform_is_not_form
  by (auto simp add: is_subform_implies_in_positions elim: is_subform_at.elims)

lemma leftmost_subform_in_generalized_app:
  shows "B ≼⇘replicate (length As) «⇙ ·⇧𝒬⇩⋆ B As"
  by (induction As arbitrary: B) (simp_all, metis replicate_append_same subform_at_subforms_app(1))

lemma self_subform_is_at_top:
  assumes "A ≼⇘p⇙ A"
  shows "p = []"
  using assms and strict_subform_is_not_form by blast

lemma at_top_is_self_subform:
  assumes "A ≼⇘[]⇙ B"
  shows "A = B"
  using assms by (auto elim: is_subform_at.elims)

lemma is_subform_at_uniqueness:
  assumes "B ≼⇘p⇙ A" and "C ≼⇘p⇙ A"
  shows "B = C"
  using assms by (induction A arbitrary: p B C) (auto elim: is_subform_at.elims)

lemma is_subform_at_existence:
  assumes "p ∈ positions A"
  obtains B where "B ≼⇘p⇙ A"
  using assms by (induction A arbitrary: p) (auto elim: is_subform_at.elims, blast+)

lemma is_subform_at_transitivity:
  assumes "A ≼⇘p⇩1⇙ B" and "B ≼⇘p⇩2⇙ C"
  shows "A ≼⇘p⇩2 @ p⇩1⇙ C"
  using assms by (induction B p⇩2 C arbitrary: A p⇩1 rule: is_subform_at.induct) simp_all

lemma subform_nesting:
  assumes "strict_prefix p' p"
  and "B ≼⇘p'⇙ A"
  and "C ≼⇘p⇙ A"
  shows "C ≼⇘drop (length p') p⇙ B"
proof -
  from assms(1) have "p ≠ []"
    using strict_prefix_simps(1) by blast
  with assms(1,3) show ?thesis
  proof (induction p arbitrary: C rule: rev_induct)
    case Nil
    then show ?case
      by blast
  next
    case (snoc d p'')
    then show ?case
    proof (cases "p'' = p'")
      case True
      obtain A' where "C ≼⇘[d]⇙ A'" and "A' ≼⇘p'⇙ A"
        by (fact superform_existence[OF snoc.prems(2)[unfolded True]])
      from ‹A' ≼⇘p'⇙ A› and assms(2) have "A' = B"
        by (rule is_subform_at_uniqueness)
      with ‹C ≼⇘[d]⇙ A'› have "C ≼⇘[d]⇙ B"
        by (simp only:)
      with True show ?thesis
        by auto
    next
      case False
      with snoc.prems(1) have "strict_prefix p' p''"
        using prefix_order.dual_order.strict_implies_order by fastforce
      then have "p'' ≠ []"
        by force
      moreover from snoc.prems(2) obtain A' where "C ≼⇘[d]⇙ A'" and "A' ≼⇘p''⇙ A"
        using superform_existence by blast
      ultimately have "A' ≼⇘drop (length p') p''⇙ B"
        using snoc.IH and ‹strict_prefix p' p''› by blast
      with ‹C ≼⇘[d]⇙ A'› and snoc.prems(1) show ?thesis
        using is_subform_at_transitivity and prefix_length_less by fastforce
    qed
  qed
qed

lemma loop_subform_impossibility:
  assumes "B ≼⇘p⇙ A"
  and "strict_prefix p' p"
  shows "¬ B ≼⇘p'⇙ A"
  using assms and prefix_length_less and self_subform_is_at_top and subform_nesting by fastforce

lemma nested_subform_size_decreases:
  assumes "strict_prefix p' p"
  and "B ≼⇘p'⇙ A"
  and "C ≼⇘p⇙ A"
  shows "form_size C < form_size B"
proof -
  from assms(1) have "p ≠ []"
    by force
  have "C ≼⇘drop (length p') p⇙ B"
    by (fact subform_nesting[OF assms])
  moreover have "drop (length p') p ≠ []"
    using prefix_length_less[OF assms(1)] by force
  ultimately show ?thesis
    using subform_size_decrease by simp
qed

definition is_subform :: "form ⇒ form ⇒ bool" (infix "≼" 50) where
  [simp]: "A ≼ B = (∃p. A ≼⇘p⇙ B)"

instantiation form :: ord
begin

definition
  "A ≤ B ⟷ A ≼ B"

definition
  "A < B ⟷ A ≼ B ∧ A ≠ B"

instance ..

end

instance form :: preorder
proof (standard, unfold less_eq_form_def less_form_def)
  fix A
  show "A ≼ A"
    unfolding is_subform_def using is_subform_at.simps(1) by blast
next
  fix A and B and C
  assume "A ≼ B" and "B ≼ C"
  then show "A ≼ C"
    unfolding is_subform_def using is_subform_at_transitivity by blast
next
  fix A and B
  show "A ≼ B ∧ A ≠ B ⟷ A ≼ B ∧ ¬ B ≼ A"
    unfolding is_subform_def
    by (metis is_subform_at.simps(1) not_less_iff_gr_or_eq subform_size_decrease)
qed

lemma position_subform_existence_equivalence:
  shows "p ∈ positions A ⟷ (∃A'. A' ≼⇘p⇙ A)"
  by (meson is_subform_at_existence is_subform_implies_in_positions)

lemma position_prefix_is_position:
  assumes "p ∈ positions A" and "prefix p' p"
  shows "p' ∈ positions A"
using assms proof (induction p rule: rev_induct)
  case Nil
  then show ?case
    by simp
next
  case (snoc d p'')
  from snoc.prems(1) have "p'' ∈ positions A"
    by (meson position_subform_existence_equivalence superform_existence)
  with snoc.prems(1,2) show ?case
    using snoc.IH by fastforce
qed

subsection ‹Free and bound variables›

consts vars :: "'a ⇒ var set"

overloading
  "vars_form" ≡ "vars :: form ⇒ var set"
  "vars_form_set" ≡ "vars :: form set ⇒ var set" (* abuse of notation *)
begin

fun vars_form :: "form ⇒ var set" where
  "vars_form (x⇘α⇙) = {(x, α)}"
| "vars_form (⦃c⦄⇘α⇙) = {}"
| "vars_form (A · B) = vars_form A ∪ vars_form B"
| "vars_form (λx⇘α⇙. A) = vars_form A ∪ {(x, α)}"

fun vars_form_set :: "form set ⇒ var set" where
  "vars_form_set S = (⋃A ∈ S. vars A)"

end

abbreviation var_names :: "'a ⇒ nat set" where
  "var_names 𝒳 ≡ var_name ` (vars 𝒳)"

lemma vars_form_finiteness:
  fixes A :: form
  shows "finite (vars A)"
  by (induction rule: vars_form.induct) simp_all

lemma vars_form_set_finiteness:
  fixes S :: "form set"
  assumes "finite S"
  shows "finite (vars S)"
  using assms unfolding vars_form_set.simps using vars_form_finiteness by blast

lemma form_var_names_finiteness:
  fixes A :: form
  shows "finite (var_names A)"
  using vars_form_finiteness by blast

lemma form_set_var_names_finiteness:
  fixes S :: "form set"
  assumes "finite S"
  shows "finite (var_names S)"
  using assms and vars_form_set_finiteness by blast

consts free_vars :: "'a ⇒ var set"

overloading
  "free_vars_form" ≡ "free_vars :: form ⇒ var set"
  "free_vars_form_set" ≡ "free_vars :: form set ⇒ var set" (* abuse of notation *)
begin

fun free_vars_form :: "form ⇒ var set" where
  "free_vars_form (x⇘α⇙) = {(x, α)}"
| "free_vars_form (⦃c⦄⇘α⇙) = {}"
| "free_vars_form (A · B) = free_vars_form A ∪ free_vars_form B"
| "free_vars_form (λx⇘α⇙. A) = free_vars_form A - {(x, α)}"

fun free_vars_form_set :: "form set ⇒ var set" where
  "free_vars_form_set S = (⋃A ∈ S. free_vars A)"

end

abbreviation free_var_names :: "'a ⇒ nat set" where
  "free_var_names 𝒳 ≡ var_name ` (free_vars 𝒳)"

lemma free_vars_form_finiteness:
  fixes A :: form
  shows "finite (free_vars A)"
  by (induction rule: free_vars_form.induct) simp_all

lemma free_vars_of_generalized_app:
  shows "free_vars (·⇧𝒬⇩⋆ A Bs) = free_vars A ∪ free_vars (lset Bs)"
  by (induction Bs arbitrary: A) auto

lemma free_vars_of_generalized_abs:
  shows "free_vars (λ⇧𝒬⇩⋆ vs A) = free_vars A - lset vs"
  by (induction vs arbitrary: A) auto

lemma free_vars_in_all_vars:
  fixes A :: form
  shows "free_vars A ⊆ vars A"
proof (induction A)
  case (FVar v)
  then show ?case
    using surj_pair[of v] by force
next
  case (FCon k)
  then show ?case
    using surj_pair[of k] by force
next
  case (FApp A B)
  have "free_vars (A · B) = free_vars A ∪ free_vars B"
    using free_vars_form.simps(3) .
  also from FApp.IH have "… ⊆ vars A ∪ vars B"
    by blast
  also have "… = vars (A · B)"
    using vars_form.simps(3)[symmetric] .
  finally show ?case
    by (simp only:)
next
  case (FAbs v A)
  then show ?case
    using surj_pair[of v] by force
qed

lemma free_vars_in_all_vars_set:
  fixes S :: "form set"
  shows "free_vars S ⊆ vars S"
  using free_vars_in_all_vars by fastforce

lemma singleton_form_set_vars:
  shows "vars {FVar y} = {y}"
  using surj_pair[of y] by force

fun bound_vars where
  "bound_vars (x⇘α⇙) = {}"
| "bound_vars (⦃c⦄⇘α⇙) = {}"
| "bound_vars (B · C) = bound_vars B ∪ bound_vars C"
| "bound_vars (λx⇘α⇙. B) = {(x, α)} ∪ bound_vars B"

lemma vars_is_free_and_bound_vars:
  shows "vars A = free_vars A ∪ bound_vars A"
  by (induction A) auto

fun binders_at :: "form ⇒ position ⇒ var set" where
  "binders_at (A · B) (« # p) = binders_at A p"
| "binders_at (A · B) (» # p) = binders_at B p"
| "binders_at (λx⇘α⇙. A) (« # p) = {(x, α)} ∪ binders_at A p"
| "binders_at A [] = {}"
| "binders_at A p = {}"

lemma binders_at_concat:
  assumes "A' ≼⇘p⇙ A"
  shows "binders_at A (p @ p') = binders_at A p ∪ binders_at A' p'"
  using assms by (induction p A rule: is_subform_at.induct) auto

subsection ‹Free and bound occurrences›

definition occurs_at :: "var ⇒ position ⇒ form ⇒ bool" where
  [iff]: "occurs_at v p B ⟷ (FVar v ≼⇘p⇙ B)"

lemma occurs_at_alt_def:
  shows "occurs_at v [] (FVar v') ⟷ (v = v')"
  and "occurs_at v p (⦃c⦄⇘α⇙) ⟷ False"
  and "occurs_at v (« # p) (A · B) ⟷ occurs_at v p A"
  and "occurs_at v (» # p) (A · B) ⟷ occurs_at v p B"
  and "occurs_at v (« # p) (λx⇘α⇙. A) ⟷ occurs_at v p A"
  and "occurs_at v (d # p) (FVar v') ⟷ False"
  and "occurs_at v (» # p) (λx⇘α⇙. A) ⟷ False"
  and "occurs_at v [] (A · B) ⟷ False"
  and "occurs_at v [] (λx⇘α⇙. A) ⟷ False"
  by (fastforce elim: is_subform_at.elims)+

definition occurs :: "var ⇒ form ⇒ bool" where
  [iff]: "occurs v B ⟷ (∃p ∈ positions B. occurs_at v p B)"

lemma occurs_in_vars:
  assumes "occurs v A"
  shows "v ∈ vars A"
  using assms by (induction A) force+

abbreviation strict_prefixes where
  "strict_prefixes xs ≡ [ys ← prefixes xs. ys ≠ xs]"

definition in_scope_of_abs :: "var ⇒ position ⇒ form ⇒ bool" where
  [iff]: "in_scope_of_abs v p B ⟷ (
    p ≠ [] ∧
    (
      ∃p' ∈ lset (strict_prefixes p).
        case (subform_at B p') of
          Some (FAbs v' _) ⇒ v = v'
        | _ ⇒ False
    )
  )"

lemma in_scope_of_abs_alt_def:
  shows "
    in_scope_of_abs v p B
    ⟷
    p ≠ [] ∧ (∃p' ∈ positions B. ∃C. strict_prefix p' p ∧ FAbs v C ≼⇘p'⇙ B)"
proof
  assume "in_scope_of_abs v p B"
  then show "p ≠ [] ∧ (∃p' ∈ positions B. ∃C. strict_prefix p' p ∧ FAbs v C ≼⇘p'⇙ B)"
    by (induction rule: subform_at.induct) force+
next
  assume "p ≠ [] ∧ (∃p' ∈ positions B. ∃C. strict_prefix p' p ∧ FAbs v C ≼⇘p'⇙ B)"
  then show "in_scope_of_abs v p B"
    by (induction rule: subform_at.induct) fastforce+
qed

lemma in_scope_of_abs_in_left_app:
  shows "in_scope_of_abs v (« # p) (A · B) ⟷ in_scope_of_abs v p A"
  by force

lemma in_scope_of_abs_in_right_app:
  shows "in_scope_of_abs v (» # p) (A · B) ⟷ in_scope_of_abs v p B"
  by force

lemma in_scope_of_abs_in_app:
  assumes "in_scope_of_abs v p (A · B)"
  obtains p' where "(p = « # p' ∧ in_scope_of_abs v p' A) ∨ (p = » # p' ∧ in_scope_of_abs v p' B)"
proof -
  from assms obtain d and p' where "p = d # p'"
    unfolding in_scope_of_abs_def by (meson list.exhaust)
  then show ?thesis
  proof (cases d)
    case Left
    with assms and ‹p = d # p'› show ?thesis
      using that and in_scope_of_abs_in_left_app by simp
  next
    case Right
    with assms and ‹p = d # p'› show ?thesis
      using that and in_scope_of_abs_in_right_app by simp
  qed
qed

lemma not_in_scope_of_abs_in_app:
  assumes "
    ∀p'.
      (p = « # p' ⟶ ¬ in_scope_of_abs v' p' A)
      ∧
      (p = » # p' ⟶ ¬ in_scope_of_abs v' p' B)"
  shows "¬ in_scope_of_abs v' p (A · B)"
  using assms and in_scope_of_abs_in_app by metis

lemma in_scope_of_abs_in_abs:
  shows "in_scope_of_abs v (« # p) (FAbs v' B) ⟷ v = v' ∨ in_scope_of_abs v p B"
proof
  assume "in_scope_of_abs v (« # p) (FAbs v' B)"
  then obtain p' and C
    where "p' ∈ positions (FAbs v' B)"
    and "strict_prefix p' (« # p)"
    and "FAbs v C ≼⇘p'⇙ FAbs v' B"
    unfolding in_scope_of_abs_alt_def by blast
  then show "v = v' ∨ in_scope_of_abs v p B"
  proof (cases p')
    case Nil
    with ‹FAbs v C ≼⇘p'⇙ FAbs v' B› have "v = v'"
      by auto
    then show ?thesis
      by simp
  next
    case (Cons d p'')
    with ‹strict_prefix p' (« # p)› have "d = «"
      by simp
    from ‹FAbs v C ≼⇘p'⇙ FAbs v' B› and Cons have "p'' ∈ positions B"
      by
        (cases "(FAbs v C, p', FAbs v' B)" rule: is_subform_at.cases)
        (simp_all add: is_subform_implies_in_positions)
    moreover from ‹FAbs v C ≼⇘p'⇙ FAbs v' B› and Cons and ‹d = «› have "FAbs v C ≼⇘p''⇙ B"
      by (metis is_subform_at.simps(4) old.prod.exhaust)
    moreover from ‹strict_prefix p' (« # p)› and Cons have "strict_prefix p'' p"
      by auto
    ultimately have "in_scope_of_abs v p B"
      using in_scope_of_abs_alt_def by auto
    then show ?thesis
      by simp
  qed
next
  assume "v = v' ∨ in_scope_of_abs v p B"
  then show "in_scope_of_abs v (« # p) (FAbs v' B)"
    unfolding in_scope_of_abs_alt_def
    using position_subform_existence_equivalence and surj_pair[of v']
    by force
qed

lemma not_in_scope_of_abs_in_var:
  shows "¬ in_scope_of_abs v p (FVar v')"
  unfolding in_scope_of_abs_def by (cases p) simp_all

lemma in_scope_of_abs_in_vars:
  assumes "in_scope_of_abs v p A"
  shows "v ∈ vars A"
using assms proof (induction A arbitrary: p)
  case (FVar v')
  then show ?case
    using not_in_scope_of_abs_in_var by blast
next
  case (FCon k)
  then show ?case
    using in_scope_of_abs_alt_def by (blast elim: is_subform_at.elims(2))
next
  case (FApp B C)
  from FApp.prems obtain d and p' where "p = d # p'"
    unfolding in_scope_of_abs_def by (meson neq_Nil_conv)
  then show ?case
  proof (cases d)
    case Left
    with FApp.prems and ‹p = d # p'› have "in_scope_of_abs v p' B"
      using in_scope_of_abs_in_left_app by blast
    then have "v ∈ vars B"
      by (fact FApp.IH(1))
    then show ?thesis
      by simp
  next
    case Right
    with FApp.prems and ‹p = d # p'› have "in_scope_of_abs v p' C"
      using in_scope_of_abs_in_right_app by blast
    then have "v ∈ vars C"
      by (fact FApp.IH(2))
    then show ?thesis
      by simp
  qed
next
  case (FAbs v' B)
  then show ?case
  proof (cases "v = v'")
    case True
    then show ?thesis
      using surj_pair[of v] by force
  next
    case False
    with FAbs.prems obtain p' and d where "p = d # p'"
      unfolding in_scope_of_abs_def by (meson neq_Nil_conv)
    then show ?thesis
    proof (cases d)
      case Left
      with FAbs.prems and False and ‹p = d # p'› have "in_scope_of_abs v p' B"
        using in_scope_of_abs_in_abs by blast
      then have "v ∈ vars B"
        by (fact FAbs.IH)
      then show ?thesis
        using surj_pair[of v'] by force
    next
      case Right
      with FAbs.prems and ‹p = d # p'› and False show ?thesis
        by (cases rule: is_subform_at.cases) auto
    qed
  qed
qed

lemma binders_at_alt_def:
  assumes "p ∈ positions A"
  shows "binders_at A p = {v | v. in_scope_of_abs v p A}"
  using assms and in_set_prefixes by (induction rule: binders_at.induct) auto

definition is_bound_at :: "var ⇒ position ⇒ form ⇒ bool" where
  [iff]: "is_bound_at v p B ⟷ occurs_at v p B ∧ in_scope_of_abs v p B"

lemma not_is_bound_at_in_var:
  shows "¬ is_bound_at v p (FVar v')"
  by (fastforce elim: is_subform_at.elims(2))

lemma not_is_bound_at_in_con:
  shows "¬ is_bound_at v p (FCon k)"
  by (fastforce elim: is_subform_at.elims(2))

lemma is_bound_at_in_left_app:
  shows "is_bound_at v (« # p) (B · C) ⟷ is_bound_at v p B"
  by auto

lemma is_bound_at_in_right_app:
  shows "is_bound_at v (» # p) (B · C) ⟷ is_bound_at v p C"
  by auto

lemma is_bound_at_from_app:
  assumes "is_bound_at v p (B · C)"
  obtains p' where "(p = « # p' ∧ is_bound_at v p' B) ∨ (p = » # p' ∧ is_bound_at v p' C)"
proof -
  from assms obtain d and p' where "p = d # p'"
    using subforms_from_app by blast
  then show ?thesis
  proof (cases d)
    case Left
    with assms and that and ‹p = d # p'› show ?thesis
      using is_bound_at_in_left_app by simp
  next
    case Right
    with assms and that and ‹p = d # p'› show ?thesis
      using is_bound_at_in_right_app by simp
  qed
qed

lemma is_bound_at_from_abs:
  assumes "is_bound_at v (« # p) (FAbs v' B)"
  shows "v = v' ∨ is_bound_at v p B"
  using assms by (fastforce elim: is_subform_at.elims)

lemma is_bound_at_from_absE:
  assumes "is_bound_at v p (FAbs v' B)"
  obtains p' where "p = « # p'" and "v = v' ∨ is_bound_at v p' B"
proof -
  obtain x and α where "v' = (x, α)"
    by fastforce
  with assms obtain p' where "p = « # p'"
    using subforms_from_abs by blast
  with assms and that show ?thesis
    using is_bound_at_from_abs by simp
qed

lemma is_bound_at_to_abs:
  assumes "(v = v' ∧ occurs_at v p B) ∨ is_bound_at v p B"
  shows "is_bound_at v (« # p) (FAbs v' B)"
unfolding is_bound_at_def proof
  from assms(1) show "occurs_at v (« # p) (FAbs v' B)"
    using surj_pair[of v'] by force
  from assms show "in_scope_of_abs v (« # p) (FAbs v' B)"
    using in_scope_of_abs_in_abs by auto
qed

lemma is_bound_at_in_bound_vars:
  assumes "p ∈ positions A"
  and "is_bound_at v p A ∨ v ∈ binders_at A p"
  shows "v ∈ bound_vars A"
using assms proof (induction A arbitrary: p)
  case (FApp B C)
  from FApp.prems(2) consider (a) "is_bound_at v p (B · C)" | (b) "v ∈ binders_at (B · C) p"
    by blast
  then show ?case
  proof cases
    case a
    then have "p ≠ []"
      using occurs_at_alt_def(8) by blast
    then obtain d and p' where "p = d # p'"
      by (meson list.exhaust)
    with ‹p ∈ positions (B · C)›
    consider (a⇩1) "p = « # p'" and "p' ∈ positions B" | (a⇩2) "p = » # p'" and "p' ∈ positions C"
      by force
    then show ?thesis
    proof cases
      case a⇩1
      from a⇩1(1) and ‹is_bound_at v p (B · C)› have "is_bound_at v p' B"
        using is_bound_at_in_left_app by blast
      with a⇩1(2) have "v ∈ bound_vars B"
        using FApp.IH(1) by blast
      then show ?thesis
        by simp
    next
      case a⇩2
      from a⇩2(1) and ‹is_bound_at v p (B · C)› have "is_bound_at v p' C"
        using is_bound_at_in_right_app by blast
      with a⇩2(2) have "v ∈ bound_vars C"
        using FApp.IH(2) by blast
      then show ?thesis
        by simp
    qed
  next
    case b
    then have "p ≠ []"
      by force
    then obtain d and p' where "p = d # p'"
      by (meson list.exhaust)
    with ‹p ∈ positions (B · C)›
    consider (b⇩1) "p = « # p'" and "p' ∈ positions B" | (b⇩2) "p = » # p'" and "p' ∈ positions C"
      by force
    then show ?thesis
    proof cases
      case b⇩1
      from b⇩1(1) and ‹v ∈ binders_at (B · C) p› have "v ∈ binders_at B p'"
        by force
      with b⇩1(2) have "v ∈ bound_vars B"
        using FApp.IH(1) by blast
      then show ?thesis
        by simp
    next
      case b⇩2
      from b⇩2(1) and ‹v ∈ binders_at (B · C) p› have "v ∈ binders_at C p'"
        by force
      with b⇩2(2) have "v ∈ bound_vars C"
        using FApp.IH(2) by blast
      then show ?thesis
        by simp
    qed
  qed
next
  case (FAbs v' B)
  from FAbs.prems(2) consider (a) "is_bound_at v p (FAbs v' B)" | (b) "v ∈ binders_at (FAbs v' B) p"
    by blast
  then show ?case
  proof cases
    case a
    then have "p ≠ []"
      using occurs_at_alt_def(9) by force
    with ‹p ∈ positions (FAbs v' B)› obtain p' where "p = « # p'" and "p' ∈ positions B"
      by (cases "FAbs v' B" rule: positions.cases) fastforce+
    from ‹p = « # p'› and ‹is_bound_at v p (FAbs v' B)› have "v = v' ∨ is_bound_at v p' B"
      using is_bound_at_from_abs by blast
    then consider (a⇩1) "v = v'" | (a⇩2) "is_bound_at v p' B"
      by blast
    then show ?thesis
    proof cases
      case a⇩1
      then show ?thesis
        using surj_pair[of v'] by fastforce
    next
      case a⇩2
      then have "v ∈ bound_vars B"
        using ‹p' ∈ positions B› and FAbs.IH by blast
      then show ?thesis
        using surj_pair[of v'] by fastforce
    qed
  next
    case b
    then have "p ≠ []"
      by force
    with FAbs.prems(1) obtain p' where "p = « # p'" and "p' ∈ positions B"
      by (cases "FAbs v' B" rule: positions.cases) fastforce+
    with b consider (b⇩1) "v = v'" | (b⇩2) "v ∈ binders_at B p'"
      by (cases "FAbs v' B" rule: positions.cases) fastforce+
    then show ?thesis
    proof cases
      case b⇩1
      then show ?thesis
        using surj_pair[of v'] by fastforce
    next
      case b⇩2
      then have "v ∈ bound_vars B"
        using ‹p' ∈ positions B› and FAbs.IH by blast
      then show ?thesis
        using surj_pair[of v'] by fastforce
    qed
  qed
qed fastforce+

lemma bound_vars_in_is_bound_at:
  assumes "v ∈ bound_vars A"
  obtains p where "p ∈ positions A" and "is_bound_at v p A ∨ v ∈ binders_at A p"
using assms proof (induction A arbitrary: thesis rule: bound_vars.induct)
  case (3 B C)
  from ‹v ∈ bound_vars (B · C)› consider (a) "v ∈ bound_vars B" | (b) "v ∈ bound_vars C"
    by fastforce
  then show ?case
  proof cases
    case a
    with "3.IH"(1) obtain p where "p ∈ positions B" and "is_bound_at v p B ∨ v ∈ binders_at B p"
      by blast
    from ‹p ∈ positions B› have "« # p ∈ positions (B · C)"
      by simp
    from ‹is_bound_at v p B ∨ v ∈ binders_at B p›
    consider (a⇩1) "is_bound_at v p B" | (a⇩2) "v ∈ binders_at B p"
      by blast
    then show ?thesis
    proof cases
      case a⇩1
      then have "is_bound_at v (« # p) (B · C)"
        using is_bound_at_in_left_app by blast
      then show ?thesis
        using "3.prems"(1) and is_subform_implies_in_positions by blast
    next
      case a⇩2
      then have "v ∈ binders_at (B · C) (« # p)"
        by simp
      then show ?thesis
        using "3.prems"(1) and ‹« # p ∈ positions (B · C)› by blast
    qed
  next
    case b
    with "3.IH"(2) obtain p where "p ∈ positions C" and "is_bound_at v p C ∨ v ∈ binders_at C p"
      by blast
    from ‹p ∈ positions C› have "» # p ∈ positions (B · C)"
      by simp
    from ‹is_bound_at v p C ∨ v ∈ binders_at C p›
    consider (b⇩1) "is_bound_at v p C" | (b⇩2) "v ∈ binders_at C p"
      by blast
    then show ?thesis
    proof cases
      case b⇩1
      then have "is_bound_at v (» # p) (B · C)"
        using is_bound_at_in_right_app by blast
      then show ?thesis
        using "3.prems"(1) and is_subform_implies_in_positions by blast
    next
      case b⇩2
      then have "v ∈ binders_at (B · C) (» # p)"
        by simp
      then show ?thesis
        using "3.prems"(1) and ‹» # p ∈ positions (B · C)› by blast
    qed
  qed
next
  case (4 x α B)
  from ‹v ∈ bound_vars (λx⇘α⇙. B)› consider (a) "v = (x, α)" | (b) "v ∈ bound_vars B"
    by force
  then show ?case
  proof cases
    case a
    then have "v ∈ binders_at (λx⇘α⇙. B) [«]"
      by simp
    then show ?thesis
      using "4.prems"(1) and is_subform_implies_in_positions by fastforce
  next
    case b
    with "4.IH"(1) obtain p where "p ∈ positions B" and "is_bound_at v p B ∨ v ∈ binders_at B p"
      by blast
    from ‹p ∈ positions B› have "« # p ∈ positions (λx⇘α⇙. B)"
      by simp
    from ‹is_bound_at v p B ∨ v ∈ binders_at B p›
    consider (b⇩1) "is_bound_at v p B" | (b⇩2) "v ∈ binders_at B p"
      by blast
    then show ?thesis
    proof cases
      case b⇩1
      then have "is_bound_at v (« # p) (λx⇘α⇙. B)"
        using is_bound_at_to_abs by blast
      then show ?thesis
        using "4.prems"(1) and ‹« # p ∈ positions (λx⇘α⇙. B)› by blast
    next
      case b⇩2
      then have "v ∈ binders_at (λx⇘α⇙. B) (« # p)"
        by simp
      then show ?thesis
        using "4.prems"(1) and ‹« # p ∈ positions (λx⇘α⇙. B)› by blast
    qed
  qed
qed simp_all

lemma bound_vars_alt_def:
  shows "bound_vars A = {v | v p. p ∈ positions A ∧ (is_bound_at v p A ∨ v ∈ binders_at A p)}"
  using bound_vars_in_is_bound_at and is_bound_at_in_bound_vars
  by (intro subset_antisym subsetI CollectI, metis) blast

definition is_free_at :: "var ⇒ position ⇒ form ⇒ bool" where
  [iff]: "is_free_at v p B ⟷ occurs_at v p B ∧ ¬ in_scope_of_abs v p B"

lemma is_free_at_in_var:
  shows "is_free_at v [] (FVar v') ⟷ v = v'"
  by simp

lemma not_is_free_at_in_con:
  shows "¬ is_free_at v [] (⦃c⦄⇘α⇙)"
  by simp

lemma is_free_at_in_left_app:
  shows "is_free_at v (« # p) (B · C) ⟷ is_free_at v p B"
  by auto

lemma is_free_at_in_right_app:
  shows "is_free_at v (» # p) (B · C) ⟷ is_free_at v p C"
  by auto

lemma is_free_at_from_app:
  assumes "is_free_at v p (B · C)"
  obtains p' where "(p = « # p' ∧ is_free_at v p' B) ∨ (p = » # p' ∧ is_free_at v p' C)"
proof -
  from assms obtain d and p' where "p = d # p'"
    using subforms_from_app by blast
  then show ?thesis
  proof (cases d)
    case Left
    with assms and that and ‹p = d # p'› show ?thesis
      using is_free_at_in_left_app by blast
  next
    case Right
    with assms and that and ‹p = d # p'› show ?thesis
      using is_free_at_in_right_app by blast
  qed
qed

lemma is_free_at_from_abs:
  assumes "is_free_at v (« # p) (FAbs v' B)"
  shows "is_free_at v p B"
  using assms by (fastforce elim: is_subform_at.elims)

lemma is_free_at_from_absE:
  assumes "is_free_at v p (FAbs v' B)"
  obtains p' where "p = « # p'" and "is_free_at v p' B"
proof -
  obtain x and α where "v' = (x, α)"
    by fastforce
  with assms obtain p' where "p = « # p'"
    using subforms_from_abs by blast
  with assms and that show ?thesis
    using is_free_at_from_abs by blast
qed

lemma is_free_at_to_abs:
  assumes "is_free_at v p B" and "v ≠ v'"
  shows "is_free_at v (« # p) (FAbs v' B)"
unfolding is_free_at_def proof
  from assms(1) show "occurs_at v (« # p) (FAbs v' B)"
    using surj_pair[of v'] by fastforce
  from assms show "¬ in_scope_of_abs v (« # p) (FAbs v' B)"
    unfolding is_free_at_def using in_scope_of_abs_in_abs by presburger
qed

lemma is_free_at_in_free_vars:
  assumes "p ∈ positions A" and "is_free_at v p A"
  shows "v ∈ free_vars A"
using assms proof (induction A arbitrary: p)
  case (FApp B C)
  from ‹is_free_at v p (B · C)› have "p ≠ []"
    using occurs_at_alt_def(8) by blast
  then obtain d and p' where "p = d # p'"
    by (meson list.exhaust)
  with ‹p ∈ positions (B · C)›
  consider (a) "p = « # p'" and "p' ∈ positions B" | (b) "p = » # p'" and "p' ∈ positions C"
    by force
  then show ?case
  proof cases
    case a
    from a(1) and ‹is_free_at v p (B · C)› have "is_free_at v p' B"
      using is_free_at_in_left_app by blast
    with a(2) have "v ∈ free_vars B"
      using FApp.IH(1) by blast
    then show ?thesis
      by simp
  next
    case b
    from b(1) and ‹is_free_at v p (B · C)› have "is_free_at v p' C"
      using is_free_at_in_right_app by blast
    with b(2) have "v ∈ free_vars C"
      using FApp.IH(2) by blast
    then show ?thesis
      by simp
  qed
next
  case (FAbs v' B)
  from ‹is_free_at v p (FAbs v' B)› have "p ≠ []"
    using occurs_at_alt_def(9) by force
  with ‹p ∈ positions (FAbs v' B)› obtain p' where "p = « # p'" and "p' ∈ positions B"
    by (cases "FAbs v' B" rule: positions.cases) fastforce+
  moreover from ‹p = « # p'› and ‹is_free_at v p (FAbs v' B)› have "is_free_at v p' B"
    using is_free_at_from_abs by blast
  ultimately have "v ∈ free_vars B"
    using FAbs.IH by simp
  moreover from ‹p = « # p'› and ‹is_free_at v p (FAbs v' B)› have "v ≠ v'"
    using in_scope_of_abs_in_abs by blast
  ultimately show ?case
    using surj_pair[of v'] by force
qed fastforce+

lemma free_vars_in_is_free_at:
  assumes "v ∈ free_vars A"
  obtains p where "p ∈ positions A" and "is_free_at v p A"
using assms proof (induction A arbitrary: thesis rule: free_vars_form.induct)
  case (3 A B)
  from ‹v ∈ free_vars (A · B)› consider (a) "v ∈ free_vars A" | (b) "v ∈ free_vars B"
    by fastforce
  then show ?case
  proof cases
    case a
    with "3.IH"(1) obtain p where "p ∈ positions A" and "is_free_at v p A"
      by blast
    from ‹p ∈ positions A› have "« # p ∈ positions (A · B)"
      by simp
    moreover from ‹is_free_at v p A› have "is_free_at v (« # p) (A · B)"
      using is_free_at_in_left_app by blast
    ultimately show ?thesis
      using "3.prems"(1) by presburger
  next
    case b
    with "3.IH"(2) obtain p where "p ∈ positions B" and "is_free_at v p B"
      by blast
    from ‹p ∈ positions B› have "» # p ∈ positions (A · B)"
      by simp
    moreover from ‹is_free_at v p B› have "is_free_at v (» # p) (A · B)"
      using is_free_at_in_right_app by blast
    ultimately show ?thesis
      using "3.prems"(1) by presburger
  qed
next
  case (4 x α A)
  from ‹v ∈ free_vars (λx⇘α⇙. A)› have "v ∈ free_vars A - {(x, α)}" and "v ≠ (x, α)"
    by simp_all
  then have "v ∈ free_vars A"
    by blast
  with "4.IH" obtain p where "p ∈ positions A" and "is_free_at v p A"
    by blast
  from ‹p ∈ positions A› have "« # p ∈ positions (λx⇘α⇙. A)"
    by simp
  moreover from ‹is_free_at v p A› and ‹v ≠ (x, α)› have "is_free_at v (« # p) (λx⇘α⇙. A)"
    using is_free_at_to_abs by blast
  ultimately show ?case
    using "4.prems"(1) by presburger
qed simp_all

lemma free_vars_alt_def:
  shows "free_vars A = {v | v p. p ∈ positions A ∧ is_free_at v p A}"
  using free_vars_in_is_free_at and is_free_at_in_free_vars
  by (intro subset_antisym subsetI CollectI, metis) blast

text ‹
  In the following definition, note that the variable immeditately preceded by ‹λ› counts as a bound
  variable:
›

definition is_bound :: "var ⇒ form ⇒ bool" where
  [iff]: "is_bound v B ⟷ (∃p ∈ positions B. is_bound_at v p B ∨ v ∈ binders_at B p)"

lemma is_bound_in_app_homomorphism:
  shows "is_bound v (A · B) ⟷ is_bound v A ∨ is_bound v B"
proof
  assume "is_bound v (A · B)"
  then obtain p where "p ∈ positions (A · B)" and "is_bound_at v p (A · B) ∨ v ∈ binders_at (A · B) p"
    by auto
  then have "p ≠ []"
    by fastforce
  with ‹p ∈ positions (A · B)› obtain p' and d where "p = d # p'"
    by auto
  from ‹is_bound_at v p (A · B) ∨ v ∈ binders_at (A · B) p›
  consider (a) "is_bound_at v p (A · B)" | (b) "v ∈ binders_at (A · B) p"
    by blast
  then show "is_bound v A ∨ is_bound v B"
  proof cases
    case a
    then show ?thesis
    proof (cases d)
      case Left
      then have "p' ∈ positions A"
        using ‹p = d # p'› and ‹p ∈ positions (A · B)› by fastforce
      moreover from ‹is_bound_at v p (A · B)› have "occurs_at v p' A"
        using Left and ‹p = d # p'› and is_subform_at.simps(2) by force
      moreover from ‹is_bound_at v p (A · B)› have "in_scope_of_abs v p' A"
        using Left and ‹p = d # p'› by fastforce
      ultimately show ?thesis
        by auto
    next
      case Right
      then have "p' ∈ positions B"
        using ‹p = d # p'› and ‹p ∈ positions (A · B)› by fastforce
      moreover from ‹is_bound_at v p (A · B)› have "occurs_at v p' B"
        using Right and ‹p = d # p'› and is_subform_at.simps(3) by force
      moreover from ‹is_bound_at v p (A · B)› have "in_scope_of_abs v p' B"
        using Right and ‹p = d # p'› by fastforce
      ultimately show ?thesis
        by auto
    qed
  next
    case b
    then show ?thesis
    proof (cases d)
      case Left
      then have "p' ∈ positions A"
        using ‹p = d # p'› and ‹p ∈ positions (A · B)› by fastforce
      moreover from ‹v ∈ binders_at (A · B) p› have "v ∈ binders_at A p'"
        using Left and ‹p = d # p'› by force
      ultimately show ?thesis
        by auto
    next
      case Right
      then have "p' ∈ positions B"
        using ‹p = d # p'› and ‹p ∈ positions (A · B)› by fastforce
      moreover from ‹v ∈ binders_at (A · B) p› have "v ∈ binders_at B p'"
        using Right and ‹p = d # p'› by force
      ultimately show ?thesis
        by auto
    qed
  qed
next
  assume "is_bound v A ∨ is_bound v B"
  then show "is_bound v (A · B)"
  proof (rule disjE)
    assume "is_bound v A"
    then obtain p where "p ∈ positions A" and "is_bound_at v p A ∨ v ∈ binders_at A p"
      by auto
    from ‹p ∈ positions A› have "« # p ∈ positions (A · B)"
      by auto
    from ‹is_bound_at v p A ∨ v ∈ binders_at A p›
    consider (a) "is_bound_at v p A" | (b) "v ∈ binders_at A p"
      by blast
    then show "is_bound v (A · B)"
    proof cases
      case a
      then have "occurs_at v (« # p) (A · B)"
        by auto
      moreover from a have "is_bound_at v (« # p) (A · B)"
        by force
      ultimately show "is_bound v (A · B)"
        using ‹« # p ∈ positions (A · B)› by blast
    next
      case b
      then have "v ∈ binders_at (A · B) (« # p)"
        by auto
      then show "is_bound v (A · B)"
        using ‹« # p ∈ positions (A · B)› by blast
    qed
  next
    assume "is_bound v B"
    then obtain p where "p ∈ positions B" and "is_bound_at v p B ∨ v ∈ binders_at B p"
      by auto
    from ‹p ∈ positions B› have "» # p ∈ positions (A · B)"
      by auto
    from ‹is_bound_at v p B ∨ v ∈ binders_at B p›
    consider (a) "is_bound_at v p B" | (b) "v ∈ binders_at B p"
      by blast
    then show "is_bound v (A · B)"
    proof cases
      case a
      then have "occurs_at v (» # p) (A · B)"
        by auto
      moreover from a have "is_bound_at v (» # p) (A · B)"
        by force
      ultimately show "is_bound v (A · B)"
        using ‹» # p ∈ positions (A · B)› by blast
    next
      case b
      then have "v ∈ binders_at (A · B) (» # p)"
        by auto
      then show "is_bound v (A · B)"
        using ‹» # p ∈ positions (A · B)› by blast
    qed
  qed
qed

lemma is_bound_in_abs_body:
  assumes "is_bound v A"
  shows "is_bound v (λx⇘α⇙. A)"
using assms unfolding is_bound_def proof
  fix p
  assume "p ∈ positions A" and "is_bound_at v p A ∨ v ∈ binders_at A p"
  moreover from ‹p ∈ positions A› have "« # p ∈ positions (λx⇘α⇙. A)"
    by simp
  ultimately consider (a) "is_bound_at v p A" | (b) "v ∈ binders_at A p"
    by blast
  then show "∃p ∈ positions (λx⇘α⇙. A). is_bound_at v p (λx⇘α⇙. A) ∨ v ∈ binders_at (λx⇘α⇙. A) p"
  proof cases
    case a
    then have "is_bound_at v (« # p) (λx⇘α⇙. A)"
      by force
    with ‹« # p ∈ positions (λx⇘α⇙. A)› show ?thesis
      by blast
  next
    case b
    then have "v ∈ binders_at (λx⇘α⇙. A) (« # p)"
      by simp
    with ‹« # p ∈ positions (λx⇘α⇙. A)› show ?thesis
      by blast
  qed
qed

lemma absent_var_is_not_bound:
  assumes "v ∉ vars A"
  shows "¬ is_bound v A"
  using assms and binders_at_alt_def and in_scope_of_abs_in_vars by blast

lemma bound_vars_alt_def2:
  shows "bound_vars A = {v ∈ vars A. is_bound v A}"
  unfolding bound_vars_alt_def using absent_var_is_not_bound by fastforce

definition is_free :: "var ⇒ form ⇒ bool" where
  [iff]: "is_free v B ⟷ (∃p ∈ positions B. is_free_at v p B)"

subsection ‹Free variables for a formula in another formula›

definition is_free_for :: "form ⇒ var ⇒ form ⇒ bool" where
  [iff]: "is_free_for A v B ⟷
    (
      ∀v' ∈ free_vars A.
        ∀p ∈ positions B.
          is_free_at v p B ⟶ ¬ in_scope_of_abs v' p B
    )"

lemma is_free_for_absent_var [intro]:
  assumes "v ∉ vars B"
  shows "is_free_for A v B"
  using assms and occurs_def and is_free_at_def and occurs_in_vars by blast

lemma is_free_for_in_var [intro]:
  shows "is_free_for A v (x⇘α⇙)"
  using subforms_from_var(2) by force

lemma is_free_for_in_con [intro]:
  shows "is_free_for A v (⦃c⦄⇘α⇙)"
  using subforms_from_con(2) by force

lemma is_free_for_from_app:
  assumes "is_free_for A v (B · C)"
  shows "is_free_for A v B" and "is_free_for A v C"
proof -
  {
    fix v'
    assume "v' ∈ free_vars A"
    then have "∀p ∈ positions B. is_free_at v p B ⟶ ¬ in_scope_of_abs v' p B"
    proof (intro ballI impI)
      fix p
      assume "v' ∈ free_vars A" and "p ∈ positions B" and "is_free_at v p B"
      from ‹p ∈ positions B› have "« # p ∈ positions (B · C)"
        by simp
      moreover from ‹is_free_at v p B› have "is_free_at v (« # p) (B · C)"
        using is_free_at_in_left_app by blast
      ultimately have "¬ in_scope_of_abs v' (« # p) (B · C)"
        using assms and ‹v' ∈ free_vars A› by blast
      then show "¬ in_scope_of_abs v' p B"
        by simp
    qed
  }
  then show "is_free_for A v B"
    by force
next
  {
    fix v'
    assume "v' ∈ free_vars A"
    then have "∀p ∈ positions C. is_free_at v p C ⟶ ¬ in_scope_of_abs v' p C"
    proof (intro ballI impI)
      fix p
      assume "v' ∈ free_vars A" and "p ∈ positions C" and "is_free_at v p C"
      from ‹p ∈ positions C› have "» # p ∈ positions (B · C)"
        by simp
      moreover from ‹is_free_at v p C› have "is_free_at v (» # p) (B · C)"
        using is_free_at_in_right_app by blast
      ultimately have "¬ in_scope_of_abs v' (» # p) (B · C)"
        using assms and ‹v' ∈ free_vars A› by blast
      then show "¬ in_scope_of_abs v' p C"
        by simp
    qed
  }
  then show "is_free_for A v C"
    by force
qed

lemma is_free_for_to_app [intro]:
  assumes "is_free_for A v B" and "is_free_for A v C"
  shows "is_free_for A v (B · C)"
unfolding is_free_for_def proof (intro ballI impI)
  fix v' and p
  assume "v' ∈ free_vars A" and "p ∈ positions (B · C)" and "is_free_at v p (B · C)"
  from ‹is_free_at v p (B · C)› have "p ≠ []"
    using occurs_at_alt_def(8) by force
  then obtain d and p' where "p = d # p'"
    by (meson list.exhaust)
  with ‹p ∈ positions (B · C)›
  consider (b) "p = « # p'" and "p' ∈ positions B" | (c) "p = » # p'" and "p' ∈ positions C"
    by force
  then show "¬ in_scope_of_abs v' p (B · C)"
  proof cases
    case b
    from b(1) and ‹is_free_at v p (B · C)› have "is_free_at v p' B"
      using is_free_at_in_left_app by blast
    with assms(1) and ‹v' ∈ free_vars A› and ‹p' ∈ positions B› have "¬ in_scope_of_abs v' p' B"
      by simp
    with b(1) show ?thesis
      using in_scope_of_abs_in_left_app by simp
  next
    case c
    from c(1) and ‹is_free_at v p (B · C)› have "is_free_at v p' C"
      using is_free_at_in_right_app by blast
    with assms(2) and ‹v' ∈ free_vars A› and ‹p' ∈ positions C› have "¬ in_scope_of_abs v' p' C"
      by simp
    with c(1) show ?thesis
      using in_scope_of_abs_in_right_app by simp
  qed
qed

lemma is_free_for_in_app:
  shows "is_free_for A v (B · C) ⟷ is_free_for A v B ∧ is_free_for A v C"
  using is_free_for_from_app and is_free_for_to_app by iprover

lemma is_free_for_to_abs [intro]:
  assumes "is_free_for A v B" and "(x, α) ∉ free_vars A"
  shows "is_free_for A v (λx⇘α⇙. B)"
unfolding is_free_for_def proof (intro ballI impI)
  fix v' and p
  assume "v' ∈ free_vars A" and "p ∈ positions (λx⇘α⇙. B)" and "is_free_at v p (λx⇘α⇙. B)"
  from ‹is_free_at v p (λx⇘α⇙. B)› have "p ≠ []"
    using occurs_at_alt_def(9) by force
  with ‹p ∈ positions (λx⇘α⇙. B)› obtain p' where "p = « # p'" and "p' ∈ positions B"
    by force
  then show "¬ in_scope_of_abs v' p (λx⇘α⇙. B)"
  proof -
    from ‹p = « # p'› and ‹is_free_at v p (λx⇘α⇙. B)› have "is_free_at v p' B"
      using is_free_at_from_abs by blast
    with assms(1) and ‹v' ∈ free_vars A› and ‹p' ∈ positions B› have "¬ in_scope_of_abs v' p' B"
      by force
    moreover from ‹v' ∈ free_vars A› and assms(2) have "v' ≠ (x, α)"
      by blast
    ultimately show ?thesis
      using ‹p = « # p'› and in_scope_of_abs_in_abs by auto
  qed
qed

lemma is_free_for_from_abs:
  assumes "is_free_for A v (λx⇘α⇙. B)" and "v ≠ (x, α)"
  shows "is_free_for A v B"
unfolding is_free_for_def proof (intro ballI impI)
  fix v' and p
  assume "v' ∈ free_vars A" and "p ∈ positions B" and "is_free_at v p B"
  then show "¬ in_scope_of_abs v' p B"
  proof -
    from ‹is_free_at v p B› and assms(2) have "is_free_at v (« # p) (λx⇘α⇙. B)"
      by (rule is_free_at_to_abs)
    moreover from ‹p ∈ positions B› have "« # p ∈ positions (λx⇘α⇙. B)"
      by simp
    ultimately have "¬ in_scope_of_abs v' (« # p) (λx⇘α⇙. B)"
      using assms and ‹v' ∈ free_vars A› by blast
    then show ?thesis
      using in_scope_of_abs_in_abs by blast
  qed
qed

lemma closed_is_free_for [intro]:
  assumes "free_vars A = {}"
  shows "is_free_for A v B"
  using assms by force

lemma is_free_for_closed_form [intro]:
  assumes "free_vars B = {}"
  shows "is_free_for A v B"
  using assms and is_free_at_in_free_vars by blast

lemma is_free_for_alt_def:
  shows "
    is_free_for A v B
    ⟷
    (
      ∄p.
      (
        p ∈ positions B ∧ is_free_at v p B ∧ p ≠ [] ∧
        (∃v' ∈ free_vars A. ∃p' C. strict_prefix p' p ∧ FAbs v' C ≼⇘p'⇙ B)
      )
    )"
  unfolding is_free_for_def
  using in_scope_of_abs_alt_def and is_subform_implies_in_positions
  by meson

lemma binding_var_not_free_for_in_abs:
  assumes "is_free x B" and "x ≠ w"
  shows "¬ is_free_for (FVar w) x (FAbs w B)"
proof (rule ccontr)
  assume "¬ ¬ is_free_for (FVar w) x (FAbs w B)"
  then have "
    ∀v' ∈ free_vars (FVar w). ∀p ∈ positions (FAbs w B). is_free_at x p (FAbs w B)
      ⟶ ¬ in_scope_of_abs v' p (FAbs w B)"
    by force
  moreover have "free_vars (FVar w) = {w}"
    using surj_pair[of w] by force
  ultimately have "
    ∀p ∈ positions (FAbs w B). is_free_at x p (FAbs w B) ⟶ ¬ in_scope_of_abs w p (FAbs w B)"
    by blast
  moreover from assms(1) obtain p where "is_free_at x p B"
    by fastforce
  from this and assms(2) have "is_free_at x (« # p) (FAbs w B)"
    by (rule is_free_at_to_abs)
  moreover from this have "« # p ∈ positions (FAbs w B)"
    using is_subform_implies_in_positions by force
  ultimately have "¬ in_scope_of_abs w (« # p) (FAbs w B)"
    by blast
  moreover have "in_scope_of_abs w (« # p) (FAbs w B)"
    using in_scope_of_abs_in_abs by blast
  ultimately show False
    by contradiction
qed

lemma absent_var_is_free_for [intro]:
  assumes "x ∉ vars A"
  shows "is_free_for (FVar x) y A"
  using in_scope_of_abs_in_vars and assms and surj_pair[of x] by fastforce

lemma form_is_free_for_absent_var [intro]:
  assumes "x ∉ vars A"
  shows "is_free_for B x A"
  using assms and occurs_in_vars by fastforce

lemma form_with_free_binder_not_free_for:
  assumes "v ≠ v'" and "v' ∈ free_vars A" and "v ∈ free_vars B"
  shows "¬ is_free_for A v (FAbs v' B)"
proof -
  from assms(3) obtain p where "p ∈ positions B" and "is_free_at v p B"
    using free_vars_in_is_free_at by blast
  then have "« # p ∈ positions (FAbs v' B)" and "is_free_at v (« # p) (FAbs v' B)"
    using surj_pair[of v'] and is_free_at_to_abs[OF ‹is_free_at v p B› assms(1)] by force+
  moreover have "in_scope_of_abs v' (« # p) (FAbs v' B)"
    using in_scope_of_abs_in_abs by blast
  ultimately show ?thesis
    using assms(2) by blast
qed

subsection ‹Replacement of subformulas›

inductive
  is_replacement_at :: "form ⇒ position ⇒ form ⇒ form ⇒ bool"
  ("(4_⦉_ ← _⦊ ⊳ _)" [1000, 0, 0, 0] 900)
where
  pos_found: "A⦉p ← C⦊ ⊳ C'" if "p