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)
syntax_consts
  "_FVar" ⇌ FVar and
  "_FCon" ⇌ FCon and
  "_FAbs" ⇌ FAbs
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 = []" and "C = C'"
| replace_left_app: "(G · H)⦉« # p ← C⦊ ⊳ (G' · H)" if "p ∈ positions G" and "G⦉p ← C⦊ ⊳ G'"
| replace_right_app: "(G · H)⦉» # p ← C⦊ ⊳ (G · H')" if "p ∈ positions H" and "H⦉p ← C⦊ ⊳ H'"
| replace_abs: "(λx⇘γ⇙. E)⦉« # p ← C⦊ ⊳ (λx⇘γ⇙. E')" if "p ∈ positions E" and "E⦉p ← C⦊ ⊳ E'"

lemma is_replacement_at_implies_in_positions:
  assumes "C⦉p ← A⦊ ⊳ D"
  shows "p ∈ positions C"
  using assms by (induction rule: is_replacement_at.induct) auto

declare is_replacement_at.intros [intro!]

lemma is_replacement_at_existence:
  assumes "p ∈ positions C"
  obtains D where "C⦉p ← A⦊ ⊳ D"
using assms proof (induction C arbitrary: p thesis)
  case (FApp C⇩1 C⇩2)
  from FApp.prems(2) consider
    (a) "p = []"
  | (b) "∃p'. p = « # p' ∧ p' ∈ positions C⇩1"
  | (c) "∃p'. p = » # p' ∧ p' ∈ positions C⇩2"
    by fastforce
  then show ?case
  proof cases
    case a
    with FApp.prems(1) show ?thesis
      by blast
  next
    case b
    with FApp.prems(1) show ?thesis
      using FApp.IH(1) and replace_left_app by meson
  next
    case c
    with FApp.prems(1) show ?thesis
      using FApp.IH(2) and replace_right_app by meson
  qed
next
  case (FAbs v C')
  from FAbs.prems(2) consider (a) "p = []" | (b) "∃p'. p = « # p' ∧ p' ∈ positions C'"
    using surj_pair[of v] by fastforce
  then show ?case
  proof cases
    case a
    with FAbs.prems(1) show ?thesis
      by blast
  next
    case b
    with FAbs.prems(1,2) show ?thesis
      using FAbs.IH and surj_pair[of v] by blast
  qed
qed force+

lemma is_replacement_at_minimal_change:
  assumes "C⦉p ← A⦊ ⊳ D"
  shows "A ≼⇘p⇙ D"
  and "∀p' ∈ positions D. ¬ prefix p' p ∧ ¬ prefix p p' ⟶ subform_at D p' = subform_at C p'"
  using assms by (induction rule: is_replacement_at.induct) auto

lemma is_replacement_at_binders:
  assumes "C⦉p ← A⦊ ⊳ D"
  shows "binders_at D p = binders_at C p"
  using assms by (induction rule: is_replacement_at.induct) simp_all

lemma is_replacement_at_occurs:
  assumes "C⦉p ← A⦊ ⊳ D"
  and "¬ prefix p' p" and "¬ prefix p p'"
  shows "occurs_at v p' C ⟷ occurs_at v p' D"
using assms proof (induction arbitrary: p' rule: is_replacement_at.induct)
  case pos_found
  then show ?case
    by simp
next
  case replace_left_app
  then show ?case
  proof (cases p')
    case (Cons d p'')
    with replace_left_app.prems(1,2) show ?thesis
      by (cases d) (use replace_left_app.IH in force)+
  qed force
next
  case replace_right_app
  then show ?case
  proof (cases p')
    case (Cons d p'')
    with replace_right_app.prems(1,2) show ?thesis
      by (cases d) (use replace_right_app.IH in force)+
  qed force
next
  case replace_abs
  then show ?case
  proof (cases p')
    case (Cons d p'')
    with replace_abs.prems(1,2) show ?thesis
      by (cases d) (use replace_abs.IH in force)+
  qed force
qed

lemma fresh_var_replacement_position_uniqueness:
  assumes "v ∉ vars C"
  and "C⦉p ← FVar v⦊ ⊳ G"
  and "occurs_at v p' G"
  shows "p' = p"
proof (rule ccontr)
  assume "p' ≠ p"
  from assms(2) have "occurs_at v p G"
    by (simp add: is_replacement_at_minimal_change(1))
  moreover have *: "occurs_at v p' C ⟷ occurs_at v p' G" if "¬ prefix p' p" and "¬ prefix p p'"
    using assms(2) and that and is_replacement_at_occurs by blast
  ultimately show False
  proof (cases "¬ prefix p' p ∧ ¬ prefix p p'")
    case True
    with assms(3) and * have "occurs_at v p' C"
      by simp
    then have "v ∈ vars C"
      using is_subform_implies_in_positions and occurs_in_vars by fastforce
    with assms(1) show ?thesis
      by contradiction
  next
    case False
    have "FVar v ≼⇘p⇙ G"
      by (fact is_replacement_at_minimal_change(1)[OF assms(2)])
    moreover from assms(3) have "FVar v ≼⇘p'⇙ G"
      by simp
    ultimately show ?thesis
      using ‹p' ≠ p› and False and loop_subform_impossibility
      by (blast dest: prefix_order.antisym_conv2)
  qed
qed

lemma is_replacement_at_new_positions:
  assumes "C⦉p ← A⦊ ⊳ D" and "prefix p p'" and "p' ∈ positions D"
  obtains p'' where "p' = p @ p''" and "p'' ∈ positions A"
  using assms by (induction arbitrary: thesis p' rule: is_replacement_at.induct, auto) blast+

lemma replacement_override:
  assumes "C⦉p ← B⦊ ⊳ D" and "C⦉p ← A⦊ ⊳ F"
  shows "D⦉p ← A⦊ ⊳ F"
using assms proof (induction arbitrary: F rule: is_replacement_at.induct)
  case pos_found
  from pos_found.hyps(1) and pos_found.prems have "A = F"
    using is_replacement_at.simps by blast
  with pos_found.hyps(1) show ?case
    by blast
next
  case (replace_left_app p G C G' H)
  have "p ∈ positions G'"
    by (
        fact is_subform_implies_in_positions
          [OF is_replacement_at_minimal_change(1)[OF replace_left_app.hyps(2)]]
       )
  from replace_left_app.prems obtain F' where "F = F' · H" and "G⦉p ← A⦊ ⊳ F'"
    by (fastforce elim: is_replacement_at.cases)
  from ‹G⦉p ← A⦊ ⊳ F'› have "G'⦉p ← A⦊ ⊳ F'"
    by (fact replace_left_app.IH)
  with ‹p ∈ positions G'› show ?case
    unfolding ‹F = F' · H› by blast
next
  case (replace_right_app p H C H' G)
  have "p ∈ positions H'"
    by
      (
        fact is_subform_implies_in_positions
          [OF is_replacement_at_minimal_change(1)[OF replace_right_app.hyps(2)]]
      )
  from replace_right_app.prems obtain F' where "F = G · F'" and "H⦉p ← A⦊ ⊳ F'"
    by (fastforce elim: is_replacement_at.cases)
  from ‹H⦉p ← A⦊ ⊳ F'› have "H'⦉p ← A⦊ ⊳ F'"
    by (fact replace_right_app.IH)
  with ‹p ∈ positions H'› show ?case
    unfolding ‹F = G · F'› by blast
next
  case (replace_abs p E C E' x γ)
  have "p ∈ positions E'"
    by
      (
        fact is_subform_implies_in_positions
          [OF is_replacement_at_minimal_change(1)[OF replace_abs.hyps(2)]]
      )
  from replace_abs.prems obtain F' where "F = λx⇘γ⇙. F'" and "E⦉p ← A⦊ ⊳ F'"
    by (fastforce elim: is_replacement_at.cases)
  from ‹E⦉p ← A⦊ ⊳ F'› have "E'⦉p ← A⦊ ⊳ F'"
    by (fact replace_abs.IH)
  with ‹p ∈ positions E'› show ?case
    unfolding ‹F = λx⇘γ⇙. F'› by blast
qed

lemma leftmost_subform_in_generalized_app_replacement:
  shows "(·⇧𝒬⇩⋆ C As)⦉replicate (length As) « ← D⦊ ⊳ (·⇧𝒬⇩⋆ D As)"
  using is_replacement_at_implies_in_positions and replace_left_app
  by (induction As arbitrary: D rule: rev_induct) auto

subsection ‹Logical constants›

abbreviation (input) 𝔵 where "𝔵 ≡ 0"
abbreviation (input) 𝔶 where "𝔶 ≡ Suc 𝔵"
abbreviation (input) 𝔷 where "𝔷 ≡ Suc 𝔶"
abbreviation (input) 𝔣 where "𝔣 ≡ Suc 𝔷"
abbreviation (input) 𝔤 where "𝔤 ≡ Suc 𝔣"
abbreviation (input) 𝔥 where "𝔥 ≡ Suc 𝔤"
abbreviation (input) 𝔠 where "𝔠 ≡ Suc 𝔥"
abbreviation (input) 𝔠⇩Q where "𝔠⇩Q ≡ Suc 𝔠"
abbreviation (input) 𝔠⇩ι where "𝔠⇩ι ≡ Suc 𝔠⇩Q"

definition Q_constant_of_type :: "type ⇒ con" where
  [simp]: "Q_constant_of_type α = (𝔠⇩Q, α→α→o)"

definition iota_constant :: con where
  [simp]: "iota_constant ≡ (𝔠⇩ι, (i→o)→i)"

definition Q :: "type ⇒ form" (‹Q⇘_⇙›) where
  [simp]: "Q⇘α⇙ = FCon (Q_constant_of_type α)"

definition iota :: form (‹ι›) where
  [simp]: "ι = FCon iota_constant"

definition is_Q_constant_of_type :: "con ⇒ type ⇒ bool" where
  [iff]: "is_Q_constant_of_type p α ⟷ p = Q_constant_of_type α"

definition is_iota_constant :: "con ⇒ bool" where
  [iff]: "is_iota_constant p ⟷ p = iota_constant"

definition is_logical_constant :: "con ⇒ bool" where
  [iff]: "is_logical_constant p ⟷ (∃β. is_Q_constant_of_type p β) ∨ is_iota_constant p"

definition type_of_Q_constant :: "con ⇒ type" where
  [simp]: "type_of_Q_constant p = (THE α. is_Q_constant_of_type p α)"

lemma constant_cases[case_names non_logical Q_constant ι_constant, cases type: con]:
  assumes "¬ is_logical_constant p ⟹ P"
  and "⋀β. is_Q_constant_of_type p β ⟹ P"
  and "is_iota_constant p ⟹ P"
  shows "P"
  using assms by blast

subsection ‹Definitions and abbreviations›

definition equality_of_type :: "form ⇒ type ⇒ form ⇒ form" (‹(_ =⇘_⇙/ _)› [103, 0, 103] 102) where
  [simp]: "A =⇘α⇙ B = Q⇘α⇙ · A · B"

definition equivalence :: "form ⇒ form ⇒ form" (infixl ‹≡⇧𝒬› 102) where
  [simp]: "A ≡⇧𝒬 B = A =⇘o⇙ B" ― ‹more modular than the definition in \<^cite>‹"andrews:2002"››

definition true :: form (‹T⇘o⇙›) where
  [simp]: "T⇘o⇙ = Q⇘o⇙ =⇘o→o→o⇙ Q⇘o⇙"

definition false :: form (‹F⇘o⇙›) where
  [simp]: "F⇘o⇙ = λ𝔵⇘o⇙. T⇘o⇙ =⇘o→o⇙ λ𝔵⇘o⇙. 𝔵⇘o⇙"

definition PI :: "type ⇒ form" (‹∏⇘_⇙›) where
  [simp]: "∏⇘α⇙ = Q⇘α→o⇙ · (λ𝔵⇘α⇙. T⇘o⇙)"

definition forall :: "nat ⇒ type ⇒ form ⇒ form" (‹(4∀_⇘_⇙./ _)› [0, 0, 141] 141) where
  [simp]: "∀x⇘α⇙. A = ∏⇘α⇙ · (λx⇘α⇙. A)"

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

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

lemma innermost_subform_in_generalized_forall:
  assumes "vs ≠ []"
  shows "A ≼⇘foldr (λ_ p. [»,«] @ p) vs []⇙ ∀⇧𝒬⇩⋆ vs A"
  using assms by (induction vs) fastforce+

lemma innermost_replacement_in_generalized_forall:
  assumes "vs ≠ []"
  shows "(∀⇧𝒬⇩⋆ vs C)⦉foldr (λ_. (@) [»,«]) vs [] ← B⦊ ⊳ (∀⇧𝒬⇩⋆ vs B)"
using assms proof (induction vs)
  case Nil
  then show ?case
    by blast
next
  case (Cons v vs)
  obtain x and α where "v = (x, α)"
    by fastforce
  then show ?case
  proof (cases "vs = []")
    case True
    with ‹v = (x, α)› show ?thesis
      unfolding True by force
  next
    case False
    then have "foldr (λ_. (@) [»,«]) vs [] ∈ positions (∀⇧𝒬⇩⋆ vs C)"
      using innermost_subform_in_generalized_forall and is_subform_implies_in_positions by blast
    moreover from False have "(∀⇧𝒬⇩⋆ vs C)⦉foldr (λ_. (@) [»,«]) vs [] ← B⦊ ⊳ (∀⇧𝒬⇩⋆ vs B)"
      by (fact Cons.IH)
    ultimately have "(λx⇘α⇙. ∀⇧𝒬⇩⋆ vs C)⦉« # foldr (λ_. (@) [»,«]) vs [] ← B⦊ ⊳ (λx⇘α⇙. ∀⇧𝒬⇩⋆ vs B)"
      by (rule replace_abs)
    moreover have "« # foldr (λ_. (@) [»,«]) vs [] ∈ positions (λx⇘α⇙. ∀⇧𝒬⇩⋆ vs C)"
      using ‹foldr (λ_. (@) [»,«]) vs [] ∈ positions (∀⇧𝒬⇩⋆ vs C)› by simp
    ultimately have "
      (∏⇘α⇙ · (λx⇘α⇙. ∀⇧𝒬⇩⋆ vs C))⦉» # « # foldr (λ_. (@) [»,«]) vs [] ← B⦊ ⊳ (∏⇘α⇙ · (λx⇘α⇙. ∀⇧𝒬⇩⋆ vs B))"
      by blast
    then have "(∀x⇘α⇙. ∀⇧𝒬⇩⋆ vs C)⦉[»,«] @ foldr (λ_. (@) [»,«]) vs [] ← B⦊ ⊳ (∀x⇘α⇙. ∀⇧𝒬⇩⋆ vs B)"
      by simp
    then show ?thesis
      unfolding ‹v = (x, α)› and generalized_forall_def and foldr.simps(2) and o_apply
      and case_prod_conv .
  qed
qed

lemma false_is_forall:
  shows "F⇘o⇙ = ∀𝔵⇘o⇙. 𝔵⇘o⇙"
  unfolding false_def and forall_def and PI_def and equality_of_type_def ..

definition conj_fun :: form (‹∧⇘o→o→o⇙›) where
  [simp]: "∧⇘o→o→o⇙ =
    λ𝔵⇘o⇙. λ𝔶⇘o⇙.
    (
      (λ𝔤⇘o→o→o⇙. 𝔤⇘o→o→o⇙ · T⇘o⇙ · T⇘o⇙) =⇘(o→o→o)→o⇙ (λ𝔤⇘o→o→o⇙. 𝔤⇘o→o→o⇙ · 𝔵⇘o⇙ · 𝔶⇘o⇙)
    )"

definition conj_op :: "form ⇒ form ⇒ form" (infixl ‹∧⇧𝒬› 131) where
  [simp]: "A ∧⇧𝒬 B = ∧⇘o→o→o⇙ · A · B"

text ‹Generalized conjunction. We define ‹∧⇧𝒬⇩⋆ [A⇩1, …, A⇩n]› as ‹A⇩1 ∧⇧𝒬 (⋯ ∧⇧𝒬 (A⇩n⇩-⇩1 ∧⇧𝒬 A⇩n) ⋯)›:›

definition generalized_conj_op :: "form list ⇒ form" (‹∧⇧𝒬⇩⋆ _› [0] 131) where
  [simp]: "∧⇧𝒬⇩⋆ As = foldr1 (∧⇧𝒬) As"

definition imp_fun :: form (‹⊃⇘o→o→o⇙›) where ― ‹‹≡› used instead of ‹=›, see \<^cite>‹"andrews:2002"››
  [simp]: "⊃⇘o→o→o⇙ = λ𝔵⇘o⇙. λ𝔶⇘o⇙. (𝔵⇘o⇙ ≡⇧𝒬 𝔵⇘o⇙ ∧⇧𝒬 𝔶⇘o⇙)"

definition imp_op :: "form ⇒ form ⇒ form" (infixl ‹⊃⇧𝒬› 111) where
  [simp]: "A ⊃⇧𝒬 B = ⊃⇘o→o→o⇙ · A · B"

text ‹Generalized implication. We define ‹[A⇩1, …, A⇩n] ⊃⇧𝒬⇩⋆ B› as ‹A⇩1 ⊃⇧𝒬 (⋯ ⊃⇧𝒬 (A⇩n ⊃⇧𝒬 B) ⋯)›:›

definition generalized_imp_op :: "form list ⇒ form ⇒ form" (infixl ‹⊃⇧𝒬⇩⋆› 111) where
  [simp]: "As ⊃⇧𝒬⇩⋆ B = foldr (⊃⇧𝒬) As B"

text ‹
  Given the definition below, it is interesting to note that ‹∼⇧𝒬 A› and ‹F⇘o⇙ ≡⇧𝒬 A› are exactly the
  same formula, namely ‹Q⇘o⇙ · F⇘o⇙ · A›:
›

definition neg :: "form ⇒ form" (‹∼⇧𝒬 _› [141] 141) where
  [simp]: "∼⇧𝒬 A = Q⇘o⇙ · F⇘o⇙ · A"

definition disj_fun :: form (‹∨⇘o→o→o⇙›) where
  [simp]: "∨⇘o→o→o⇙ = λ𝔵⇘o⇙. λ𝔶⇘o⇙. ∼⇧𝒬 (∼⇧𝒬 𝔵⇘o⇙ ∧⇧𝒬 ∼⇧𝒬 𝔶⇘o⇙)"

definition disj_op :: "form ⇒ form ⇒ form" (infixl ‹∨⇧𝒬› 126) where
  [simp]: "A ∨⇧𝒬 B = ∨⇘o→o→o⇙ · A · B"

definition exists :: "nat ⇒ type ⇒ form ⇒ form" (‹(4∃_⇘_⇙./ _)› [0, 0, 141] 141) where
  [simp]: "∃x⇘α⇙. A = ∼⇧𝒬 (∀x⇘α⇙. ∼⇧𝒬 A)"

lemma exists_fv:
  shows "free_vars (∃x⇘α⇙. A) = free_vars A - {(x, α)}"
  by simp

definition inequality_of_type :: "form ⇒ type ⇒ form ⇒ form" (‹(_ ≠⇘_⇙/ _)› [103, 0, 103] 102) where
  [simp]: "A ≠⇘α⇙ B = ∼⇧𝒬 (A =⇘α⇙ B)"

subsection ‹Well-formed formulas›

inductive is_wff_of_type :: "type ⇒ form ⇒ bool" where
  var_is_wff: "is_wff_of_type α (x⇘α⇙)"
| con_is_wff: "is_wff_of_type α (⦃c⦄⇘α⇙)"
| app_is_wff: "is_wff_of_type β (A · B)" if "is_wff_of_type (α→β) A" and "is_wff_of_type α B"
| abs_is_wff: "is_wff_of_type (α→β) (λx⇘α⇙. A)" if "is_wff_of_type β A"

definition wffs_of_type :: "type ⇒ form set" (‹wffs⇘_⇙› [0]) where
  "wffs⇘α⇙ = {f :: form. is_wff_of_type α f}"

abbreviation wffs :: "form set" where
  "wffs ≡ ⋃α. wffs⇘α⇙"

lemma is_wff_of_type_wffs_of_type_eq [pred_set_conv]:
  shows "is_wff_of_type α = (λf. f ∈ wffs⇘α⇙)"
  unfolding wffs_of_type_def by simp

lemmas wffs_of_type_intros [intro!] = is_wff_of_type.intros[to_set]
lemmas wffs_of_type_induct [consumes 1, induct set: wffs_of_type] = is_wff_of_type.induct[to_set]
lemmas wffs_of_type_cases [consumes 1, cases set: wffs_of_type] = is_wff_of_type.cases[to_set]
lemmas wffs_of_type_simps = is_wff_of_type.simps[to_set]

lemma generalized_app_wff [intro]:
  assumes "length As = length ts"
  and "∀k < length As. As ! k ∈ wffs⇘ts ! k⇙"
  and "B ∈ wffs⇘foldr (→) ts β⇙"
  shows "·⇧𝒬⇩⋆ B As ∈ wffs⇘β⇙"
using assms proof (induction As ts arbitrary: B rule: list_induct2)
  case Nil
  then show ?case
    by simp
next
  case (Cons A As t ts)
  from Cons.prems(1) have "A ∈ wffs⇘t⇙"
    by fastforce
  moreover from Cons.prems(2) have "B ∈ wffs⇘t→foldr (→) ts β⇙"
    by auto
  ultimately have "B · A ∈ wffs⇘foldr (→) ts β⇙"
    by blast
  moreover have "∀k < length As. (A # As) ! (Suc k) = As ! k ∧ (t # ts) ! (Suc k) = ts ! k"
    by force
  with Cons.prems(1) have "∀k < length As. As ! k ∈ wffs⇘ts ! k⇙"
    by fastforce
  ultimately have "·⇧𝒬⇩⋆ (B · A) As ∈ wffs⇘β⇙"
    using Cons.IH by (simp only:)
  moreover have "·⇧𝒬⇩⋆ B (A # As) = ·⇧𝒬⇩⋆ (B · A) As"
    by simp
  ultimately show ?case
    by (simp only:)
qed

lemma generalized_abs_wff [intro]:
  assumes "B ∈ wffs⇘β⇙"
  shows "λ⇧𝒬⇩⋆ vs B ∈ wffs⇘foldr (→) (map snd vs) β⇙"
using assms proof (induction vs)
  case Nil
  then show ?case
    by simp
next
  case (Cons v vs)
  let ?δ = "foldr (→) (map snd vs) β"
  obtain x and α where "v = (x, α)"
    by fastforce
  then have "FVar v ∈ wffs⇘α⇙"
    by auto
  from Cons.prems have "λ⇧𝒬⇩⋆ vs B ∈ wffs⇘?δ⇙"
    by (fact Cons.IH)
  with ‹v = (x, α)› have "FAbs v (λ⇧𝒬⇩⋆ vs B) ∈ wffs⇘α→?δ⇙"
    by blast
  moreover from ‹v = (x, α)› have "foldr (→) (map snd (v # vs)) β = α→?δ"
    by simp
  moreover have "λ⇧𝒬⇩⋆ (v # vs) B = FAbs v (λ⇧𝒬⇩⋆ vs B)"
    by simp
  ultimately show ?case by (simp only:)
qed

lemma Q_wff [intro]:
  shows "Q⇘α⇙ ∈ wffs⇘α→α→o⇙"
  by auto

lemma iota_wff [intro]:
  shows "ι ∈ wffs⇘(i→o)→i⇙"
  by auto

lemma equality_wff [intro]:
  assumes "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘α⇙"
  shows "A =⇘α⇙ B ∈ wffs⇘o⇙"
  using assms by auto

lemma equivalence_wff [intro]:
  assumes "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  shows "A ≡⇧𝒬 B ∈ wffs⇘o⇙"
  using assms unfolding equivalence_def by blast

lemma true_wff [intro]:
  shows "T⇘o⇙ ∈ wffs⇘o⇙"
  by force

lemma false_wff [intro]:
  shows "F⇘o⇙ ∈ wffs⇘o⇙"
  by auto

lemma pi_wff [intro]:
  shows "∏⇘α⇙ ∈ wffs⇘(α→o)→o⇙"
  using PI_def by fastforce

lemma forall_wff [intro]:
  assumes "A ∈ wffs⇘o⇙"
  shows "∀x⇘α⇙. A ∈ wffs⇘o⇙"
  using assms and pi_wff unfolding forall_def by blast

lemma generalized_forall_wff [intro]:
  assumes "B ∈ wffs⇘o⇙"
  shows "∀⇧𝒬⇩⋆ vs B ∈ wffs⇘o⇙"
using assms proof (induction vs)
  case (Cons v vs)
  then show ?case
    using surj_pair[of v] by force
qed simp

lemma conj_fun_wff [intro]:
  shows "∧⇘o→o→o⇙ ∈ wffs⇘o→o→o⇙"
  by auto

lemma conj_op_wff [intro]:
  assumes "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  shows "A ∧⇧𝒬 B ∈ wffs⇘o⇙"
  using assms unfolding conj_op_def by blast

lemma imp_fun_wff [intro]:
  shows "⊃⇘o→o→o⇙ ∈ wffs⇘o→o→o⇙"
  by auto

lemma imp_op_wff [intro]:
  assumes "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  shows "A ⊃⇧𝒬 B ∈ wffs⇘o⇙"
  using assms unfolding imp_op_def by blast

lemma neg_wff [intro]:
  assumes "A ∈ wffs⇘o⇙"
  shows " ∼⇧𝒬 A ∈ wffs⇘o⇙"
  using assms by fastforce

lemma disj_fun_wff [intro]:
  shows "∨⇘o→o→o⇙ ∈ wffs⇘o→o→o⇙"
  by auto

lemma disj_op_wff [intro]:
  assumes "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  shows "A ∨⇧𝒬 B ∈ wffs⇘o⇙"
  using assms by auto

lemma exists_wff [intro]:
  assumes "A ∈ wffs⇘o⇙"
  shows "∃x⇘α⇙. A ∈ wffs⇘o⇙"
  using assms by fastforce

lemma inequality_wff [intro]:
  assumes "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘α⇙"
  shows "A ≠⇘α⇙ B ∈ wffs⇘o⇙"
  using assms by fastforce

lemma wffs_from_app:
  assumes "A · B ∈ wffs⇘β⇙"
  obtains α where "A ∈ wffs⇘α→β⇙" and "B ∈ wffs⇘α⇙"
  using assms by (blast elim: wffs_of_type_cases)

lemma wffs_from_generalized_app:
  assumes "·⇧𝒬⇩⋆ B As ∈ wffs⇘β⇙"
  obtains ts
  where "length ts = length As"
  and "∀k < length As. As ! k ∈ wffs⇘ts ! k⇙"
  and "B ∈ wffs⇘foldr (→) ts β⇙"
using assms proof (induction As arbitrary: B thesis)
  case Nil
  then show ?case
    by simp
next
  case (Cons A As)
  from Cons.prems have "·⇧𝒬⇩⋆ (B · A) As ∈ wffs⇘β⇙"
    by auto
  then obtain ts
    where "length ts = length As"
    and "∀k < length As. As ! k ∈ wffs⇘ts ! k⇙"
    and "B · A ∈ wffs⇘foldr (→) ts β⇙"
    using Cons.IH by blast
  moreover
  from ‹B · A ∈ wffs⇘foldr (→) ts β⇙› obtain t where "B ∈ wffs⇘t→foldr (→) ts β⇙" and "A ∈ wffs⇘t⇙"
    by (elim wffs_from_app)
  moreover from ‹length ts = length As› have "length (t # ts) = length (A # As)"
    by simp
  moreover from ‹A ∈ wffs⇘t⇙› and ‹∀k < length As. As ! k ∈ wffs⇘ts ! k⇙›
  have "∀k < length (A # As). (A # As) ! k ∈ wffs⇘(t # ts) ! k⇙"
    by (simp add: nth_Cons')
  moreover from ‹B ∈ wffs⇘t→foldr (→) ts β⇙› have "B ∈ wffs⇘foldr (→) (t # ts) β⇙"
    by simp
  ultimately show ?case
    using Cons.prems(1) by blast
qed

lemma wffs_from_abs:
  assumes "λx⇘α⇙. A ∈ wffs⇘γ⇙"
  obtains β where "γ = α→β" and "A ∈ wffs⇘β⇙"
  using assms by (blast elim: wffs_of_type_cases)

lemma wffs_from_equality:
  assumes "A =⇘α⇙ B ∈ wffs⇘o⇙"
  shows "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘α⇙"
  using assms by (fastforce elim: wffs_of_type_cases)+

lemma wffs_from_equivalence:
  assumes "A ≡⇧𝒬 B ∈ wffs⇘o⇙"
  shows "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  using assms unfolding equivalence_def by (fact wffs_from_equality)+

lemma wffs_from_forall:
  assumes "∀x⇘α⇙. A ∈ wffs⇘o⇙"
  shows "A ∈ wffs⇘o⇙"
  using assms unfolding forall_def and PI_def
  by (fold equality_of_type_def) (drule wffs_from_equality, blast elim: wffs_from_abs)

lemma wffs_from_conj_fun:
  assumes "∧⇘o→o→o⇙ · A · B ∈ wffs⇘o⇙"
  shows "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  using assms by (auto elim: wffs_from_app wffs_from_abs)

lemma wffs_from_conj_op:
  assumes "A ∧⇧𝒬 B ∈ wffs⇘o⇙"
  shows "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  using assms unfolding conj_op_def by (elim wffs_from_conj_fun)+

lemma wffs_from_imp_fun:
  assumes "⊃⇘o→o→o⇙ · A · B ∈ wffs⇘o⇙"
  shows "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  using assms by (auto elim: wffs_from_app wffs_from_abs)

lemma wffs_from_imp_op:
  assumes "A ⊃⇧𝒬 B ∈ wffs⇘o⇙"
  shows "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  using assms unfolding imp_op_def by (elim wffs_from_imp_fun)+

lemma wffs_from_neg:
  assumes "∼⇧𝒬 A ∈ wffs⇘o⇙"
  shows "A ∈ wffs⇘o⇙"
  using assms unfolding neg_def by (fold equality_of_type_def) (drule wffs_from_equality, blast)

lemma wffs_from_disj_fun:
  assumes "∨⇘o→o→o⇙ · A · B ∈ wffs⇘o⇙"
  shows "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  using assms by (auto elim: wffs_from_app wffs_from_abs)

lemma wffs_from_disj_op:
  assumes "A ∨⇧𝒬 B ∈ wffs⇘o⇙"
  shows "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  using assms and wffs_from_disj_fun unfolding disj_op_def by blast+

lemma wffs_from_exists:
  assumes "∃x⇘α⇙. A ∈ wffs⇘o⇙"
  shows "A ∈ wffs⇘o⇙"
  using assms unfolding exists_def using wffs_from_neg and wffs_from_forall by blast

lemma wffs_from_inequality:
  assumes "A ≠⇘α⇙ B ∈ wffs⇘o⇙"
  shows "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘α⇙"
  using assms unfolding inequality_of_type_def using wffs_from_equality and wffs_from_neg by meson+

lemma wff_has_unique_type:
  assumes "A ∈ wffs⇘α⇙" and "A ∈ wffs⇘β⇙"
  shows "α = β"
using assms proof (induction arbitrary: α β rule: form.induct)
  case (FVar v)
  obtain x and γ where "v = (x, γ)"
    by fastforce
  with FVar.prems have "α = γ" and "β = γ"
    by (blast elim: wffs_of_type_cases)+
  then show ?case ..
next
  case (FCon k)
  obtain x and γ where "k = (x, γ)"
    by fastforce
  with FCon.prems have "α = γ" and "β = γ"
    by (blast elim: wffs_of_type_cases)+
  then show ?case ..
next
  case (FApp A B)
  from FApp.prems obtain α' and β' where "A ∈ wffs⇘α'→α⇙" and "A ∈ wffs⇘β'→β⇙"
    by (blast elim: wffs_from_app)
  with FApp.IH(1) show ?case
    by blast
next
  case (FAbs v A)
  obtain x and γ where "v = (x, γ)"
    by fastforce
  with FAbs.prems obtain α' and β'
    where "α = γ→α'" and "β = γ→β'" and "A ∈ wffs⇘α'⇙" and "A ∈ wffs⇘β'⇙"
    by (blast elim: wffs_from_abs)
  with FAbs.IH show ?case
    by simp
qed

lemma wffs_of_type_o_induct [consumes 1, case_names Var Con App]:
  assumes "A ∈ wffs⇘o⇙"
  and "⋀x. 𝒫 (x⇘o⇙)"
  and "⋀c. 𝒫 (⦃c⦄⇘o⇙)"
  and "⋀A B α. A ∈ wffs⇘α→o⇙ ⟹ B ∈ wffs⇘α⇙ ⟹ 𝒫 (A · B)"
  shows "𝒫 A"
  using assms by (cases rule: wffs_of_type_cases) simp_all

lemma diff_types_implies_diff_wffs:
  assumes "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘β⇙"
  and "α ≠ β"
  shows "A ≠ B"
  using assms and wff_has_unique_type by blast

lemma is_free_for_in_generalized_app [intro]:
  assumes "is_free_for A v B" and "∀C ∈ lset Cs. is_free_for A v C"
  shows "is_free_for A v (·⇧𝒬⇩⋆ B Cs)"
using assms proof (induction Cs rule: rev_induct)
  case Nil
  then show ?case
    by simp
next
  case (snoc C Cs)
  from snoc.prems(2) have "is_free_for A v C" and "∀C ∈ lset Cs. is_free_for A v C"
    by simp_all
  with snoc.prems(1) have "is_free_for A v (·⇧𝒬⇩⋆ B Cs)"
    using snoc.IH by simp
  with ‹is_free_for A v C› show ?case
    using is_free_for_to_app by simp
qed

lemma is_free_for_in_equality [intro]:
  assumes "is_free_for A v B" and "is_free_for A v C"
  shows "is_free_for A v (B =⇘α⇙ C)"
  using assms unfolding equality_of_type_def and Q_def and Q_constant_of_type_def
  by (intro is_free_for_to_app is_free_for_in_con)

lemma is_free_for_in_equivalence [intro]:
  assumes "is_free_for A v B" and "is_free_for A v C"
  shows "is_free_for A v (B ≡⇧𝒬 C)"
  using assms unfolding equivalence_def by (rule is_free_for_in_equality)

lemma is_free_for_in_true [intro]:
  shows "is_free_for A v (T⇘o⇙)"
  by force

lemma is_free_for_in_false [intro]:
  shows "is_free_for A v (F⇘o⇙)"
  unfolding false_def by (intro is_free_for_in_equality is_free_for_closed_form) simp_all

lemma is_free_for_in_forall [intro]:
  assumes "is_free_for A v B" and "(x, α) ∉ free_vars A"
  shows "is_free_for A v (∀x⇘α⇙. B)"
unfolding forall_def and PI_def proof (fold equality_of_type_def)
  have "is_free_for A v (λ𝔵⇘α⇙. T⇘o⇙)"
    using is_free_for_to_abs[OF is_free_for_in_true assms(2)] by fastforce
  moreover have "is_free_for A v (λx⇘α⇙. B)"
    by (fact is_free_for_to_abs[OF assms])
  ultimately show "is_free_for A v (λ𝔵⇘α⇙. T⇘o⇙ =⇘α→o⇙ λx⇘α⇙. B)"
    by (iprover intro: assms(1) is_free_for_in_equality is_free_for_in_true is_free_for_to_abs)
qed

lemma is_free_for_in_generalized_forall [intro]:
  assumes "is_free_for A v B" and "lset vs ∩ free_vars A = {}"
  shows "is_free_for A v (∀⇧𝒬⇩⋆ vs B)"
using assms proof (induction vs)
  case Nil
  then show ?case
    by simp
next
  case (Cons v' vs)
  obtain x and α where "v' = (x, α)"
    by fastforce
  from Cons.prems(2) have "v' ∉ free_vars A" and "lset vs ∩ free_vars A = {}"
    by simp_all
  from Cons.prems(1) and ‹lset vs ∩ free_vars A = {}› have "is_free_for A v (∀⇧𝒬⇩⋆ vs B)"
    by (fact Cons.IH)
  from this and ‹v' ∉ free_vars A›[unfolded ‹v' = (x, α)›] have "is_free_for A v (∀x⇘α⇙. ∀⇧𝒬⇩⋆ vs B)"
    by (intro is_free_for_in_forall)
  with ‹v' = (x, α)› show ?case
    by simp
qed

lemma is_free_for_in_conj [intro]:
  assumes "is_free_for A v B" and "is_free_for A v C"
  shows "is_free_for A v (B ∧⇧𝒬 C)"
proof -
  have "free_vars ∧⇘o→o→o⇙ = {}"
    by force
  then have "is_free_for A v (∧⇘o→o→o⇙)"
    using is_free_for_closed_form by fast
  with assms have "is_free_for A v (∧⇘o→o→o⇙ · B · C)"
    by (intro is_free_for_to_app)
  then show ?thesis
    by (fold conj_op_def)
qed

lemma is_free_for_in_imp [intro]:
  assumes "is_free_for A v B" and "is_free_for A v C"
  shows "is_free_for A v (B ⊃⇧𝒬 C)"
proof -
  have "free_vars ⊃⇘o→o→o⇙ = {}"
    by force
  then have "is_free_for A v (⊃⇘o→o→o⇙)"
    using is_free_for_closed_form by fast
  with assms have "is_free_for A v (⊃⇘o→o→o⇙ · B · C)"
    by (intro is_free_for_to_app)
  then show ?thesis
    by (fold imp_op_def)
qed

lemma is_free_for_in_neg [intro]:
  assumes "is_free_for A v B"
  shows "is_free_for A v (∼⇧𝒬 B)"
  using assms unfolding neg_def and Q_def and Q_constant_of_type_def
  by (intro is_free_for_to_app is_free_for_in_false is_free_for_in_con)

lemma is_free_for_in_disj [intro]:
  assumes "is_free_for A v B" and "is_free_for A v C"
  shows "is_free_for A v (B ∨⇧𝒬 C)"
proof -
  have "free_vars ∨⇘o→o→o⇙ = {}"
    by force
  then have "is_free_for A v (∨⇘o→o→o⇙)"
    using is_free_for_closed_form by fast
  with assms have "is_free_for A v (∨⇘o→o→o⇙ · B · C)"
    by (intro is_free_for_to_app)
  then show ?thesis
    by (fold disj_op_def)
qed

lemma replacement_preserves_typing:
  assumes "C⦉p ← B⦊ ⊳ D"
  and "A ≼⇘p⇙ C"
  and "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘α⇙"
  shows "C ∈ wffs⇘β⇙ ⟷ D ∈ wffs⇘β⇙"
using assms proof (induction arbitrary: β rule: is_replacement_at.induct)
  case (pos_found p C C' A)
  then show ?case
    using diff_types_implies_diff_wffs by auto
qed (metis is_subform_at.simps(2,3,4) wffs_from_app wffs_from_abs wffs_of_type_simps)+

corollary replacement_preserves_typing':
  assumes "C⦉p ← B⦊ ⊳ D"
  and "A ≼⇘p⇙ C"
  and "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘α⇙"
  and "C ∈ wffs⇘β⇙" and "D ∈ wffs⇘γ⇙"
  shows "β = γ"
  using assms and replacement_preserves_typing and wff_has_unique_type by simp

text ‹Closed formulas and sentences:›

definition is_closed_wff_of_type :: "form ⇒ type ⇒ bool" where
  [iff]: "is_closed_wff_of_type A α ⟷ A ∈ wffs⇘α⇙ ∧ free_vars A = {}"

definition is_sentence :: "form ⇒ bool" where
  [iff]: "is_sentence A ⟷ is_closed_wff_of_type A o"

subsection ‹Substitutions›

type_synonym substitution = "(var, form) fmap"

definition is_substitution :: "substitution ⇒ bool" where
  [iff]: "is_substitution θ ⟷ (∀(x, α) ∈ fmdom' θ. θ $$! (x, α) ∈ wffs⇘α⇙)"

fun substitute :: "substitution ⇒ form ⇒ form" (‹❙S _ _› [51, 51]) where
  "❙S θ (x⇘α⇙) = (case θ $$ (x, α) of None ⇒ x⇘α⇙ | Some A ⇒ A)"
| "❙S θ (⦃c⦄⇘α⇙) = ⦃c⦄⇘α⇙"
| "❙S θ (A · B) = (❙S θ A) · (❙S θ B)"
| "❙S θ (λx⇘α⇙. A) = (if (x, α) ∉ fmdom' θ then λx⇘α⇙. ❙S θ A else λx⇘α⇙. ❙S (fmdrop (x, α) θ) A)"

lemma empty_substitution_neutrality:
  shows "❙S {$$} A = A"
  by (induction A) auto

lemma substitution_preserves_typing:
  assumes "is_substitution θ"
  and "A ∈ wffs⇘α⇙"
  shows "❙S θ A ∈ wffs⇘α⇙"
using assms(2) and assms(1)[unfolded is_substitution_def] proof (induction arbitrary: θ)
  case (var_is_wff α x)
  then show ?case
    by (cases "(x, α) ∈ fmdom' θ") (use fmdom'_notI in ‹force+›)
next
  case (abs_is_wff β A α x)
  then show ?case
  proof (cases "(x, α) ∈ fmdom' θ")
    case True
    then have "❙S θ (λx⇘α⇙. A) = λx⇘α⇙. ❙S (fmdrop (x, α) θ) A"
      by simp
    moreover from abs_is_wff.prems have "is_substitution (fmdrop (x, α) θ)"
      by fastforce
    with abs_is_wff.IH have "❙S (fmdrop (x, α) θ) A ∈ wffs⇘β⇙"
      by simp
    ultimately show ?thesis
      by auto
  next
    case False
    then have "❙S θ (λx⇘α⇙. A) = λx⇘α⇙. ❙S θ A"
      by simp
    moreover from abs_is_wff.IH have "❙S θ A ∈ wffs⇘β⇙"
      using abs_is_wff.prems by blast
    ultimately show ?thesis
      by fastforce
  qed
qed force+

lemma derived_substitution_simps:
  shows "❙S θ T⇘o⇙ = T⇘o⇙"
  and "❙S θ F⇘o⇙ = F⇘o⇙"
  and "❙S θ (∏⇘α⇙) = ∏⇘α⇙"
  and "❙S θ (∼⇧𝒬 B) = ∼⇧𝒬 (❙S θ B)"
  and "❙S θ (B =⇘α⇙ C) = (❙S θ B) =⇘α⇙ (❙S θ C)"
  and "❙S θ (B ∧⇧𝒬 C) = (❙S θ B) ∧⇧𝒬 (❙S θ C)"
  and "❙S θ (B ∨⇧𝒬 C) = (❙S θ B) ∨⇧𝒬 (❙S θ C)"
  and "❙S θ (B ⊃⇧𝒬 C) = (❙S θ B) ⊃⇧𝒬 (❙S θ C)"
  and "❙S θ (B ≡⇧𝒬 C) = (❙S θ B) ≡⇧𝒬 (❙S θ C)"
  and "❙S θ (B ≠⇘α⇙ C) = (❙S θ B) ≠⇘α⇙ (❙S θ C)"
  and "❙S θ (∀x⇘α⇙. B) = (if (x, α) ∉ fmdom' θ then ∀x⇘α⇙. ❙S θ B else ∀x⇘α⇙. ❙S (fmdrop (x, α) θ) B)"
  and "❙S θ (∃x⇘α⇙. B) = (if (x, α) ∉ fmdom' θ then ∃x⇘α⇙. ❙S θ B else ∃x⇘α⇙. ❙S (fmdrop (x, α) θ) B)"
  by auto

lemma generalized_app_substitution:
  shows "❙S θ (·⇧𝒬⇩⋆ A Bs) = ·⇧𝒬⇩⋆ (❙S θ A) (map (λB. ❙S θ B) Bs)"
  by (induction Bs arbitrary: A) simp_all

lemma generalized_abs_substitution:
  shows "❙S θ (λ⇧𝒬⇩⋆ vs A) = λ⇧𝒬⇩⋆ vs (❙S (fmdrop_set (fmdom' θ ∩ lset vs) θ) A)"
proof (induction vs arbitrary: θ)
  case Nil
  then show ?case
    by simp
next
  case (Cons v vs)
  obtain x and α where "v = (x, α)"
    by fastforce
  then show ?case
  proof (cases "v ∉ fmdom' θ")
    case True
    then have *: "fmdom' θ ∩ lset (v # vs) = fmdom' θ ∩ lset vs"
      by simp
    from True have "❙S θ (λ⇧𝒬⇩⋆ (v # vs) A) = λx⇘α⇙. ❙S θ (λ⇧𝒬⇩⋆ vs A)"
      using ‹v = (x, α)› by auto
    also have "… = λx⇘α⇙. λ⇧𝒬⇩⋆ vs (❙S (fmdrop_set (fmdom' θ ∩ lset vs) θ) A)"
      using Cons.IH by (simp only:)
    also have "… = λ⇧𝒬⇩⋆ (v # vs) (❙S (fmdrop_set (fmdom' θ ∩ lset (v # vs)) θ) A)"
      using ‹v = (x, α)› and * by auto
    finally show ?thesis .
  next
    case False
    let ?θ' = "fmdrop v θ"
    have *: "fmdrop_set (fmdom' θ ∩ lset (v # vs)) θ = fmdrop_set (fmdom' ?θ' ∩ lset vs) ?θ'"
      using False by clarsimp (metis Int_Diff Int_commute fmdrop_set_insert insert_Diff_single)
    from False have "❙S θ (λ⇧𝒬⇩⋆ (v # vs) A) = λx⇘α⇙. ❙S ?θ' (λ⇧𝒬⇩⋆ vs A)"
      using ‹v = (x, α)› by auto
    also have "… = λx⇘α⇙. λ⇧𝒬⇩⋆ vs (❙S (fmdrop_set (fmdom' ?θ' ∩ lset vs) ?θ') A)"
      using Cons.IH by (simp only:)
    also have "… = λ⇧𝒬⇩⋆ (v # vs) (❙S (fmdrop_set (fmdom' θ ∩ lset (v # vs)) θ) A)"
      using ‹v = (x, α)› and * by auto
    finally show ?thesis .
  qed
qed

lemma generalized_forall_substitution:
  shows "❙S θ (∀⇧𝒬⇩⋆ vs A) = ∀⇧𝒬⇩⋆ vs (❙S (fmdrop_set (fmdom' θ ∩ lset vs) θ) A)"
proof (induction vs arbitrary: θ)
  case Nil
  then show ?case
    by simp
next
  case (Cons v vs)
  obtain x and α where "v = (x, α)"
    by fastforce
  then show ?case
  proof (cases "v ∉ fmdom' θ")
    case True
    then have *: "fmdom' θ ∩ lset (v # vs) = fmdom' θ ∩ lset vs"
      by simp
    from True have "❙S θ (∀⇧𝒬⇩⋆ (v # vs) A) = ∀x⇘α⇙. ❙S θ (∀⇧𝒬⇩⋆ vs A)"
      using ‹v = (x, α)› by auto
    also have "… = ∀x⇘α⇙. ∀⇧𝒬⇩⋆ vs (❙S (fmdrop_set (fmdom' θ ∩ lset vs) θ) A)"
      using Cons.IH by (simp only:)
    also have "… = ∀⇧𝒬⇩⋆ (v # vs) (❙S (fmdrop_set (fmdom' θ ∩ lset (v # vs)) θ) A)"
      using ‹v = (x, α)› and * by auto
    finally show ?thesis .
  next
    case False
    let ?θ' = "fmdrop v θ"
    have *: "fmdrop_set (fmdom' θ ∩ lset (v # vs)) θ = fmdrop_set (fmdom' ?θ' ∩ lset vs) ?θ'"
      using False by clarsimp (metis Int_Diff Int_commute fmdrop_set_insert insert_Diff_single)
    from False have "❙S θ (∀⇧𝒬⇩⋆ (v # vs) A) = ∀x⇘α⇙. ❙S ?θ' (∀⇧𝒬⇩⋆ vs A)"
      using ‹v = (x, α)› by auto
    also have "… = ∀x⇘α⇙. ∀⇧𝒬⇩⋆ vs (❙S (fmdrop_set (fmdom' ?θ' ∩ lset vs) ?θ') A)"
      using Cons.IH by (simp only:)
    also have "… = ∀⇧𝒬⇩⋆ (v # vs) (❙S (fmdrop_set (fmdom' θ ∩ lset (v # vs)) θ) A)"
      using ‹v = (x, α)› and * by auto
    finally show ?thesis .
  qed
qed

lemma singleton_substitution_simps:
  shows "❙S {(x, α) ↣ A} (y⇘β⇙) = (if (x, α) ≠ (y, β) then y⇘β⇙ else A)"
  and "❙S {(x, α) ↣ A} (⦃c⦄⇘α⇙) = ⦃c⦄⇘α⇙"
  and "❙S {(x, α) ↣ A} (B · C) = (❙S {(x, α) ↣ A} B) · (❙S {(x, α) ↣ A} C)"
  and "❙S {(x, α) ↣ A} (λy⇘β⇙. B) = λy⇘β⇙. (if (x, α) = (y, β) then B else ❙S {(x, α) ↣ A} B)"
  by (simp_all add: empty_substitution_neutrality fmdrop_fmupd_same)

lemma substitution_preserves_freeness:
  assumes "y ∉ free_vars A" and "y ≠ z"
  shows "y ∉ free_vars ❙S {x ↣ FVar z} A"
using assms(1) proof (induction A rule: free_vars_form.induct)
  case (1 x' α)
  with assms(2) show ?case
    using surj_pair[of z] by (cases "x = (x', α)") force+
next
  case (4 x' α A)
  then show ?case
    using surj_pair[of z]
    by (cases "x = (x', α)") (use singleton_substitution_simps(4) in presburger, auto)
qed auto

lemma renaming_substitution_minimal_change:
  assumes "y ∉ vars A" and "y ≠ z"
  shows "y ∉ vars (❙S {x ↣ FVar z} A)"
using assms(1) proof (induction A rule: vars_form.induct)
  case (1 x' α)
  with assms(2) show ?case
    using surj_pair[of z] by (cases "x = (x', α)") force+
next
  case (4 x' α A)
  then show ?case
    using surj_pair[of z]
    by (cases "x = (x', α)") (use singleton_substitution_simps(4) in presburger, auto)
qed auto

lemma free_var_singleton_substitution_neutrality:
  assumes "v ∉ free_vars A"
  shows "❙S {v ↣ B} A = A"
  using assms
  by
    (induction A rule: free_vars_form.induct)
    (simp_all, metis empty_substitution_neutrality fmdrop_empty fmdrop_fmupd_same)

lemma identity_singleton_substitution_neutrality:
  shows "❙S {v ↣ FVar v} A = A"
  by
    (induction A rule: free_vars_form.induct)
    (simp_all add: empty_substitution_neutrality fmdrop_fmupd_same)

lemma free_var_in_renaming_substitution:
  assumes "x ≠ y"
  shows "(x, α) ∉ free_vars (❙S {(x, α) ↣ y⇘α⇙} B)"
  using assms by (induction B rule: free_vars_form.induct) simp_all

lemma renaming_substitution_preserves_form_size:
  shows "form_size (❙S {v ↣ FVar v'} A) = form_size A"
proof (induction A rule: form_size.induct)
  case (1 x α)
  then show ?case
    using form_size.elims by auto
next
  case (4 x α A)
  then show ?case
    by (cases "v = (x, α)") (use singleton_substitution_simps(4) in presburger, auto)
qed simp_all

text ‹The following lemma corresponds to X5100 in \<^cite>‹"andrews:2002"›:›

lemma substitution_composability:
  assumes "v' ∉ vars B"
  shows "❙S {v' ↣ A} ❙S {v ↣ FVar v'} B = ❙S {v ↣ A} B"
using assms proof (induction B arbitrary: v')
  case (FAbs w C)
  then show ?case
  proof (cases "v = w")
    case True
    from ‹v' ∉ vars (FAbs w C)› have "v' ∉ free_vars (FAbs w C)"
      using free_vars_in_all_vars by blast
    then have "❙S {v' ↣ A} (FAbs w C) = FAbs w C"
      by (rule free_var_singleton_substitution_neutrality)
    from ‹v = w› have "v ∉ free_vars (FAbs w C)"
      using surj_pair[of w] by fastforce
    then have "❙S {v ↣ A} (FAbs w C) = FAbs w C"
      by (fact free_var_singleton_substitution_neutrality)
    also from ‹❙S {v' ↣ A} (FAbs w C) = FAbs w C› have "… = ❙S {v' ↣ A} (FAbs w C)"
      by (simp only:)
    also from ‹v = w› have "… = ❙S {v' ↣ A} ❙S {v ↣ FVar v'} (FAbs w C)"
      using free_var_singleton_substitution_neutrality[OF ‹v ∉ free_vars (FAbs w C)›] by (simp only:)
    finally show ?thesis ..
  next
    case False
    from FAbs.prems have "v' ∉ vars C"
      using surj_pair[of w] by fastforce
    then show ?thesis
    proof (cases "v' = w")
      case True
      with FAbs.prems show ?thesis
        using vars_form.elims by auto
    next
      case False
      from ‹v ≠ w› have "❙S {v ↣ A} (FAbs w C) = FAbs w (❙S {v ↣ A} C)"
        using surj_pair[of w] by fastforce
      also from FAbs.IH have "… = FAbs w (❙S {v' ↣ A} ❙S {v ↣ FVar v'} C)"
        using ‹v' ∉ vars C› by simp
      also from ‹v' ≠ w› have "… = ❙S {v' ↣ A} (FAbs w (❙S {v ↣ FVar v'} C))"
        using surj_pair[of w] by fastforce
      also from ‹v ≠ w› have "… = ❙S {v' ↣ A} ❙S {v ↣ FVar v'} (FAbs w C)"
        using surj_pair[of w] by fastforce
      finally show ?thesis ..
    qed
  qed
qed auto

text ‹The following lemma corresponds to X5101 in \<^cite>‹"andrews:2002"›:›

lemma renaming_substitution_composability:
  assumes "z ∉ free_vars A" and "is_free_for (FVar z) x A"
  shows "❙S {z ↣ FVar y} ❙S {x ↣ FVar z} A = ❙S {x ↣ FVar y} A"
using assms proof (induction A arbitrary: z)
  case (FVar v)
  then show ?case
    using surj_pair[of v] and surj_pair[of z] by fastforce
next
  case (FCon k)
  then show ?case
    using surj_pair[of k] by fastforce
next
  case (FApp B C)
  let ?θ⇩z⇩y = "{z ↣ FVar y}" and ?θ⇩x⇩z = "{x ↣ FVar z}" and ?θ⇩x⇩y = "{x ↣ FVar y}"
  from ‹is_free_for (FVar z) x (B · C)› have "is_free_for (FVar z) x B" and "is_free_for (FVar z) x C"
    using is_free_for_from_app by iprover+
  moreover from ‹z ∉ free_vars (B · C)› have "z ∉ free_vars B" and "z ∉ free_vars C"
    by simp_all
  ultimately have *: "❙S ?θ⇩z⇩y ❙S ?θ⇩x⇩z B = ❙S ?θ⇩x⇩y B" and **: "❙S ?θ⇩z⇩y ❙S ?θ⇩x⇩z C = ❙S ?θ⇩x⇩y C"
    using FApp.IH by simp_all
  have "❙S ?θ⇩z⇩y ❙S ?θ⇩x⇩z (B · C) = (❙S ?θ⇩z⇩y ❙S ?θ⇩x⇩z B) · (❙S ?θ⇩z⇩y ❙S ?θ⇩x⇩z C)"
    by simp
  also from * and ** have "… = (❙S ?θ⇩x⇩y B) · (❙S ?θ⇩x⇩y C)"
    by (simp only:)
  also have "… = ❙S ?θ⇩x⇩y (B · C)"
    by simp
  finally show ?case .
next
  case (FAbs w B)
  let ?θ⇩z⇩y = "{z ↣ FVar y}" and ?θ⇩x⇩z = "{x ↣ FVar z}" and ?θ⇩x⇩y = "{x ↣ FVar y}"
  show ?case
  proof (cases "x = w")
    case True
    then show ?thesis
    proof (cases "z = w")
      case True
      with ‹x = w› have "x ∉ free_vars (FAbs w B)" and "z ∉ free_vars (FAbs w B)"
        using surj_pair[of w] by fastforce+
      from ‹x ∉ free_vars (FAbs w B)› have "❙S ?θ⇩x⇩y (FAbs w B) = FAbs w B"
        by (fact free_var_singleton_substitution_neutrality)
      also from ‹z ∉ free_vars (FAbs w B)› have "… = ❙S ?θ⇩z⇩y (FAbs w B)"
        by (fact free_var_singleton_substitution_neutrality[symmetric])
      also from ‹x ∉ free_vars (FAbs w B)› have "… = ❙S ?θ⇩z⇩y ❙S ?θ⇩x⇩z (FAbs w B)"
        using free_var_singleton_substitution_neutrality by simp
      finally show ?thesis ..
    next
      case False
      with ‹x = w› have "z ∉ free_vars B" and "x ∉ free_vars (FAbs w B)"
        using ‹z ∉ free_vars (FAbs w B)› and surj_pair[of w] by fastforce+
      from ‹z ∉ free_vars B› have "❙S ?θ⇩z⇩y B = B"
        by (fact free_var_singleton_substitution_neutrality)
      from ‹x ∉ free_vars (FAbs w B)› have "❙S ?θ⇩x⇩y (FAbs w B) = FAbs w B"
        by (fact free_var_singleton_substitution_neutrality)
      also from ‹❙S ?θ⇩z⇩y B = B› have "… = FAbs w (❙S ?θ⇩z⇩y B)"
        by (simp only:)
      also from ‹z ∉ free_vars (FAbs w B)› have "… = ❙S ?θ⇩z⇩y (FAbs w B)"
        by (simp add: ‹FAbs w B = FAbs w (❙S ?θ⇩z⇩y B)› free_var_singleton_substitution_neutrality)
      also from ‹x ∉ free_vars (FAbs w B)› have "… = ❙S ?θ⇩z⇩y ❙S ?θ⇩x⇩z (FAbs w B)"
        using free_var_singleton_substitution_neutrality by simp
      finally show ?thesis ..
    qed
  next
    case False
    then show ?thesis
    proof (cases "z = w")
      case True
      have "x ∉ free_vars B"
      proof (rule ccontr)
        assume "¬ x ∉ free_vars B"
        with ‹x ≠ w› have "x ∈ free_vars (FAbs w B)"
          using surj_pair[of w] by fastforce
        then obtain p where "p ∈ positions (FAbs w B)" and "is_free_at x p (FAbs w B)"
          using free_vars_in_is_free_at by blast
        with ‹is_free_for (FVar z) x (FAbs w B)› have "¬ in_scope_of_abs z p (FAbs w B)"
          by (meson empty_is_position is_free_at_in_free_vars is_free_at_in_var is_free_for_def)
        moreover obtain p' where "p = « # p'"
          using is_free_at_from_absE[OF ‹is_free_at x p (FAbs w B)›] by blast
        ultimately have "z ≠ w"
          using in_scope_of_abs_in_abs by blast
        with ‹z = w› show False
          by contradiction
      qed
      then have *: "❙S ?θ⇩x⇩y B = ❙S ?θ⇩x⇩z B"
        using free_var_singleton_substitution_neutrality by auto
      from ‹x ≠ w› have "❙S ?θ⇩x⇩y (FAbs w B) = FAbs w (❙S ?θ⇩x⇩y B)"
        using surj_pair[of w] by fastforce
      also from * have "… = FAbs w (❙S ?θ⇩x⇩z B)"
        by (simp only:)
      also from FAbs.prems(1) have "… = ❙S ?θ⇩z⇩y (FAbs w (❙S ?θ⇩x⇩z B))"
        using ‹x ∉ free_vars B› and free_var_singleton_substitution_neutrality by auto
      also from ‹x ≠ w› have "… = ❙S ?θ⇩z⇩y ❙S ?θ⇩x⇩z (FAbs w B)"
        using surj_pair[of w] by fastforce
      finally show ?thesis ..
    next
      case False
      obtain v⇩w and α where "w = (v⇩w, α)"
        by fastforce
      with ‹is_free_for (FVar z) x (FAbs w B)› and ‹x ≠ w› have "is_free_for (FVar z) x B"
        using is_free_for_from_abs by iprover
      moreover from ‹z ∉ free_vars (FAbs w B)› and ‹z ≠ w› and ‹w = (v⇩w, α)› have "z ∉ free_vars B"
        by simp
      ultimately have *: "❙S ?θ⇩z⇩y ❙S ?θ⇩x⇩z B = ❙S ?θ⇩x⇩y B"
        using FAbs.IH by simp
      from ‹x ≠ w› have "❙S ?θ⇩x⇩y (FAbs w B) = FAbs w (❙S ?θ⇩x⇩y B)"
        using ‹w = (v⇩w, α)› and free_var_singleton_substitution_neutrality by simp
      also from * have "… = FAbs w (❙S ?θ⇩z⇩y ❙S ?θ⇩x⇩z B)"
        by (simp only:)
      also from ‹z ≠ w› have "… = ❙S ?θ⇩z⇩y (FAbs w (❙S ?θ⇩x⇩z B))"
        using ‹w = (v⇩w, α)› and free_var_singleton_substitution_neutrality by simp
      also from ‹x ≠ w› have "… = ❙S ?θ⇩z⇩y ❙S ?θ⇩x⇩z (FAbs w B)"
        using ‹w = (v⇩w, α)› and free_var_singleton_substitution_neutrality by simp
      finally show ?thesis ..
    qed
  qed
qed

lemma absent_vars_substitution_preservation:
  assumes "v ∉ vars A"
  and "∀v' ∈ fmdom' θ. v ∉ vars (θ $$! v')"
  shows "v ∉ vars (❙S θ A)"
using assms proof (induction A arbitrary: θ)
  case (FVar v')
  then show ?case
    using surj_pair[of v'] by (cases "v' ∈ fmdom' θ") (use fmlookup_dom'_iff in force)+
next
  case (FCon k)
  then show ?case
    using surj_pair[of k] by fastforce
next
  case FApp
  then show ?case
    by simp
next
  case (FAbs w B)
  from FAbs.prems(1) have "v ∉ vars B"
    using vars_form.elims by auto
  then show ?case
  proof (cases "w ∈ fmdom' θ")
    case True
    from FAbs.prems(2) have "∀v' ∈ fmdom' (fmdrop w θ). v ∉ vars ((fmdrop w θ) $$! v')"
      by auto
    with ‹v ∉ vars B› have "v ∉ vars (❙S (fmdrop w θ) B)"
      by (fact FAbs.IH)
    with FAbs.prems(1) have "v ∉ vars (FAbs w (❙S (fmdrop w θ) B))"
      using surj_pair[of w] by fastforce
    moreover from True have "❙S θ (FAbs w B) = FAbs w (❙S (fmdrop w θ) B)"
      using surj_pair[of w] by fastforce
    ultimately show ?thesis
      by simp
  next
    case False
    then show ?thesis
      using FAbs.IH and FAbs.prems and surj_pair[of w] by fastforce
  qed
qed

lemma substitution_free_absorption:
  assumes "θ $$ v = None" and "v ∉ free_vars B"
  shows "❙S ({v ↣ A} ++⇩f θ) B = ❙S θ B"
using assms proof (induction B arbitrary: θ)
  case (FAbs w B)
  show ?case
  proof (cases "v ≠ w")
    case True
    with FAbs.prems(2) have "v ∉ free_vars B"
      using surj_pair[of w] by fastforce
    then show ?thesis
    proof (cases "w ∈ fmdom' θ")
      case True
      then have "❙S ({v ↣ A} ++⇩f θ) (FAbs w B) = FAbs w (❙S (fmdrop w ({v ↣ A} ++⇩f θ)) B)"
        using surj_pair[of w] by fastforce
      also from ‹v ≠ w› and True have "… = FAbs w (❙S ({v ↣ A} ++⇩f fmdrop w θ) B)"
        by (simp add: fmdrop_fmupd)
      also from FAbs.prems(1) and ‹v ∉ free_vars B› have "… = FAbs w (❙S (fmdrop w θ) B)"
        using FAbs.IH by simp
      also from True have "… = ❙S θ (FAbs w B)"
        using surj_pair[of w] by fastforce
      finally show ?thesis .
    next
      case False
      with FAbs.prems(1) have "❙S ({v ↣ A} ++⇩f θ) (FAbs w B) = FAbs w (❙S ({v ↣ A} ++⇩f θ) B)"
        using ‹v ≠ w› and surj_pair[of w] by fastforce
      also from FAbs.prems(1) and ‹v ∉ free_vars B› have "… = FAbs w (❙S θ B)"
        using FAbs.IH by simp
      also from False have "… = ❙S θ (FAbs w B)"
        using surj_pair[of w] by fastforce
      finally show ?thesis .
    qed
  next
    case False
    then have "fmdrop w ({v ↣ A} ++⇩f θ) = fmdrop w θ"
      by (simp add: fmdrop_fmupd_same)
    then show ?thesis
      using surj_pair[of w] by (metis (no_types, lifting) fmdrop_idle' substitute.simps(4))
  qed
qed fastforce+

lemma substitution_absorption:
  assumes "θ $$ v = None" and "v ∉ vars B"
  shows "❙S ({v ↣ A} ++⇩f θ) B = ❙S θ B"
  using assms by (meson free_vars_in_all_vars in_mono substitution_free_absorption)

lemma is_free_for_with_renaming_substitution:
  assumes "is_free_for A x B"
  and "y ∉ vars B"
  and "x ∉ fmdom' θ"
  and "∀v ∈ fmdom' θ. y ∉ vars (θ $$! v)"
  and "∀v ∈ fmdom' θ. is_free_for (θ $$! v) v B"
  shows "is_free_for A y (❙S ({x ↣ FVar y} ++⇩f θ) B)"
using assms proof (induction B arbitrary: θ)
  case (FVar w)
  then show ?case
  proof (cases "w = x")
    case True
    with FVar.prems(3) have "❙S ({x ↣ FVar y} ++⇩f θ) (FVar w) = FVar y"
      using surj_pair[of w] by fastforce
    then show ?thesis
      using self_subform_is_at_top by fastforce
  next
    case False
    then show ?thesis
    proof (cases "w ∈ fmdom' θ")
      case True
      from False have "❙S ({x ↣ FVar y} ++⇩f θ) (FVar w) = ❙S θ (FVar w)"
        using substitution_absorption and surj_pair[of w] by force
      also from True have "… = θ $$! w"
        using surj_pair[of w] by (metis fmdom'_notI option.case_eq_if substitute.simps(1))
      finally have "❙S ({x ↣ FVar y} ++⇩f θ) (FVar w) = θ $$! w" .
      moreover from True and FVar.prems(4) have "y ∉ vars (θ $$! w)"
        by blast
      ultimately show ?thesis
        using form_is_free_for_absent_var by presburger
    next
      case False
      with FVar.prems(3) and ‹w ≠ x› have "❙S ({x ↣ FVar y} ++⇩f θ) (FVar w) = FVar w"
        using surj_pair[of w] by fastforce
      with FVar.prems(2) show ?thesis
        using form_is_free_for_absent_var by presburger
    qed
  qed
next
  case (FCon k)
  then show ?case
    using surj_pair[of k] by fastforce
next
  case (FApp C D)
  from FApp.prems(2) have "y ∉ vars C" and "y ∉ vars D"
    by simp_all
  from FApp.prems(1) have "is_free_for A x C" and "is_free_for A x D"
    using is_free_for_from_app by iprover+
  have "∀v ∈ fmdom' θ. is_free_for (θ $$! v) v C ∧ is_free_for (θ $$! v) v D"
  proof (rule ballI)
    fix v
    assume "v ∈ fmdom' θ"
    with FApp.prems(5) have "is_free_for (θ $$! v) v (C · D)"
      by blast
    then show "is_free_for (θ $$! v) v C ∧ is_free_for (θ $$! v) v D"
      using is_free_for_from_app by iprover+
  qed
  then have
    *: "∀v ∈ fmdom' θ. is_free_for (θ $$! v) v C" and **: "∀v ∈ fmdom' θ. is_free_for (θ $$! v) v D"
    by auto
  have "❙S ({x ↣ FVar y} ++⇩f θ) (C · D) = (❙S ({x ↣ FVar y} ++⇩f θ) C) · (❙S ({x ↣ FVar y} ++⇩f θ) D)"
    by simp
  moreover have "is_free_for A y (❙S ({x ↣ FVar y} ++⇩f θ) C)"
    by (rule FApp.IH(1)[OF ‹is_free_for A x C› ‹y ∉ vars C› FApp.prems(3,4) *])
  moreover have "is_free_for A y (❙S ({x ↣ FVar y} ++⇩f θ) D)"
    by (rule FApp.IH(2)[OF ‹is_free_for A x D› ‹y ∉ vars D› FApp.prems(3,4) **])
  ultimately show ?case
    using is_free_for_in_app by simp
next
  case (FAbs w B)
  obtain x⇩w and α⇩w where "w = (x⇩w, α⇩w)"
    by fastforce
  from FAbs.prems(2) have "y ∉ vars B"
    using vars_form.elims by auto
  then show ?case
  proof (cases "w = x")
    case True
    from True and ‹x ∉ fmdom' θ› have "w ∉ fmdom' θ" and "x ∉ free_vars (FAbs w B)"
      using ‹w = (x⇩w, α⇩w)› by fastforce+
    with True have "❙S ({x ↣ FVar y} ++⇩f θ) (FAbs w B) = ❙S θ (FAbs w B)"
      using substitution_free_absorption by blast
    also have "… = FAbs w (❙S θ B)"
      using ‹w = (x⇩w, α⇩w)› ‹w ∉ fmdom' θ› substitute.simps(4) by presburger
    finally have "❙S ({x ↣ FVar y} ++⇩f θ) (FAbs w B) = FAbs w (❙S θ B)" .
    moreover from ‹❙S θ (FAbs w B) = FAbs w (❙S θ B)› have "y ∉ vars (FAbs w (❙S θ B))"
      using absent_vars_substitution_preservation[OF FAbs.prems(2,4)] by simp
    ultimately show ?thesis
      using is_free_for_absent_var by (simp only:)
  next
    case False
    obtain v⇩w and α⇩w where "w = (v⇩w, α⇩w)"
      by fastforce
    from FAbs.prems(1) and ‹w ≠ x› and ‹w = (v⇩w, α⇩w)› have "is_free_for A x B"
      using is_free_for_from_abs by iprover
    then show ?thesis
    proof (cases "w ∈ fmdom' θ")
      case True
      then have "❙S ({x ↣ FVar y} ++⇩f θ) (FAbs w B) = FAbs w (❙S (fmdrop w ({x ↣ FVar y} ++⇩f θ)) B)"
        using ‹w = (v⇩w, α⇩w)› by (simp add: fmdrop_idle')
      also from ‹w ≠ x› and True have "… = FAbs w (❙S ({x ↣ FVar y} ++⇩f fmdrop w θ) B)"
        by (simp add: fmdrop_fmupd)
      finally
      have *: "❙S ({x ↣ FVar y} ++⇩f θ) (FAbs w B) = FAbs w (❙S ({x ↣ FVar y} ++⇩f fmdrop w θ) B)" .
      have "∀v ∈ fmdom' (fmdrop w θ). is_free_for (fmdrop w θ $$! v) v B"
      proof
        fix v
        assume "v ∈ fmdom' (fmdrop w θ)"
        with FAbs.prems(5) have "is_free_for (fmdrop w θ $$! v) v (FAbs w B)"
          by auto
        moreover from ‹v ∈ fmdom' (fmdrop w θ)› have "v ≠ w"
          by auto
        ultimately show "is_free_for (fmdrop w θ $$! v) v B"
          unfolding ‹w = (v⇩w, α⇩w)› using is_free_for_from_abs by iprover
      qed
      moreover from FAbs.prems(3) have "x ∉ fmdom' (fmdrop w θ)"
        by simp
      moreover from FAbs.prems(4) have "∀v ∈ fmdom' (fmdrop w θ). y ∉ vars (fmdrop w θ $$! v)"
        by simp
      ultimately have "is_free_for A y (❙S ({x ↣ FVar y} ++⇩f fmdrop w θ) B)"
        using ‹is_free_for A x B› and ‹y ∉ vars B› and FAbs.IH by iprover
      then show ?thesis
      proof (cases "x ∉ free_vars B")
        case True
        have "y ∉ vars (❙S ({x ↣ FVar y} ++⇩f θ) (FAbs w B))"
        proof -
          have "❙S ({x ↣ FVar y} ++⇩f θ) (FAbs w B) = FAbs w (❙S ({x ↣ FVar y} ++⇩f fmdrop w θ) B)"
            using * .
          also from ‹x ∉ free_vars B› and FAbs.prems(3) have "… = FAbs w (❙S (fmdrop w θ) B)"
            using substitution_free_absorption by (simp add: fmdom'_notD)
          finally have "❙S ({x ↣ FVar y} ++⇩f θ) (FAbs w B) = FAbs w (❙S (fmdrop w θ) B)" .
          with FAbs.prems(2) and ‹w = (v⇩w, α⇩w)› and FAbs.prems(4) show ?thesis
            using absent_vars_substitution_preservation by auto
        qed
        then show ?thesis
          using is_free_for_absent_var by simp
      next
        case False
        have "w ∉ free_vars A"
        proof (rule ccontr)
          assume "¬ w ∉ free_vars A"
          with False and ‹w ≠ x› have "¬ is_free_for A x (FAbs w B)"
            using form_with_free_binder_not_free_for by simp
          with FAbs.prems(1) show False
            by contradiction
        qed
        with ‹is_free_for A y (❙S ({x ↣ FVar y} ++⇩f fmdrop w θ) B)›
        have "is_free_for A y (FAbs w (❙S ({x ↣ FVar y} ++⇩f fmdrop w θ) B))"
          unfolding ‹w = (v⇩w, α⇩w)› using is_free_for_to_abs by iprover
        with * show ?thesis
          by (simp only:)
      qed
    next
      case False
      have "∀v ∈ fmdom' θ. is_free_for (θ $$! v) v B"
      proof (rule ballI)
        fix v
        assume "v ∈ fmdom' θ"
        with FAbs.prems(5) have "is_free_for (θ $$! v) v (FAbs w B)"
          by blast
        moreover from ‹v ∈ fmdom' θ› and ‹w ∉ fmdom' θ› have "v ≠ w"
          by blast
        ultimately show "is_free_for (θ $$! v) v B"
          unfolding ‹w = (v⇩w, α⇩w)› using is_free_for_from_abs by iprover
      qed
      with ‹is_free_for A x B› and ‹y ∉ vars B› and FAbs.prems(3,4)
      have "is_free_for A y (❙S ({x ↣ FVar y} ++⇩f θ) B)"
        using FAbs.IH by iprover
      then show ?thesis
      proof (cases "x ∉ free_vars B")
        case True
        have "y ∉ vars (❙S ({x ↣ FVar y} ++⇩f θ) (FAbs w B))"
        proof -
          from False and ‹w = (v⇩w, α⇩w)› and ‹w ≠ x›
          have "❙S ({x ↣ FVar y} ++⇩f θ) (FAbs w B) = FAbs w (❙S ({x ↣ FVar y} ++⇩f θ) B)"
            by auto
          also from ‹x ∉ free_vars B› and FAbs.prems(3) have "… = FAbs w (❙S θ B)"
            using substitution_free_absorption by (simp add: fmdom'_notD)
          finally have "❙S ({x ↣ FVar y} ++⇩f θ) (FAbs w B) = FAbs w (❙S θ B)" .
          with FAbs.prems(2,4) and ‹w = (v⇩w, α⇩w)› show ?thesis
            using absent_vars_substitution_preservation by auto
        qed
        then show ?thesis
          using is_free_for_absent_var by simp
      next
        case False
        have "w ∉ free_vars A"
        proof (rule ccontr)
          assume "¬ w ∉ free_vars A"
          with False and ‹w ≠ x› have "¬ is_free_for A x (FAbs w B)"
            using form_with_free_binder_not_free_for by simp
          with FAbs.prems(1) show False
            by contradiction
        qed
        with ‹is_free_for A y (❙S ({x ↣ FVar y} ++⇩f θ) B)›
        have "is_free_for A y (FAbs w (❙S ({x ↣ FVar y} ++⇩f θ) B))"
          unfolding ‹w = (v⇩w, α⇩w)› using is_free_for_to_abs by iprover
        moreover from ‹w ∉ fmdom' θ› and ‹w ≠ x› and FAbs.prems(3)
        have "❙S ({x ↣ FVar y} ++⇩f θ) (FAbs w B) = FAbs w (❙S ({x ↣ FVar y} ++⇩f θ) B)"
          using surj_pair[of w] by fastforce
        ultimately show ?thesis
          by (simp only:)
      qed
    qed
  qed
qed

text ‹
  The following lemma allows us to fuse a singleton substitution and a simultaneous substitution,
  as long as the variable of the former does not occur anywhere in the latter:
›

lemma substitution_fusion:
  assumes "is_substitution θ" and "is_substitution {v ↣ A}"
  and "θ $$ v = None" and "∀v' ∈ fmdom' θ. v ∉ vars (θ $$! v')"
  shows "❙S {v ↣ A} ❙S θ B = ❙S ({v ↣ A} ++⇩f θ) B"
using assms(1,3,4) proof (induction B arbitrary: θ)
  case (FVar v')
  then show ?case
  proof (cases "v' ∉ fmdom' θ")
    case True
    then show ?thesis
      using surj_pair[of v'] by fastforce
  next
    case False
    then obtain A' where "θ $$ v' = Some A'"
      by (meson fmlookup_dom'_iff)
    with False and FVar.prems(3) have "v ∉ vars A'"
      by fastforce
    then have "❙S {v ↣ A} A' = A'"
      using free_var_singleton_substitution_neutrality and free_vars_in_all_vars by blast
    from ‹θ $$ v' = Some A'› have "❙S {v ↣ A} ❙S θ (FVar v') = ❙S {v ↣ A} A'"
      using surj_pair[of v'] by fastforce
    also from ‹❙S {v ↣ A} A' = A'› have "… = A'"
      by (simp only:)
    also from ‹θ $$ v' = Some A'› and ‹θ $$ v = None› have "… = ❙S ({v ↣ A} ++⇩f θ) (FVar v')"
      using surj_pair[of v'] by fastforce
    finally show ?thesis .
  qed
next
  case (FCon k)
  then show ?case
    using surj_pair[of k] by fastforce
next
  case (FApp C D)
  have "❙S {v ↣ A} ❙S θ (C · D) = ❙S {v ↣ A} ((❙S θ C) · (❙S θ D))"
    by auto
  also have "… = (❙S {v ↣ A} ❙S θ C) · (❙S {v ↣ A} ❙S θ D)"
    by simp
  also from FApp.IH have "… = (❙S ({v ↣ A} ++⇩f θ) C) · (❙S ({v ↣ A} ++⇩f θ) D)"
    using FApp.prems(1,2,3) by presburger
  also have "… = ❙S ({v ↣ A} ++⇩f θ) (C · D)"
    by simp
  finally show ?case .
next
  case (FAbs w C)
  obtain v⇩w and α where "w = (v⇩w, α)"
    by fastforce
  then show ?case
  proof (cases "v ≠ w")
    case True
    show ?thesis
    proof (cases "w ∉ fmdom' θ")
      case True
      then have "❙S {v ↣ A} ❙S θ (FAbs w C) = ❙S {v ↣ A} (FAbs w (❙S θ C))"
        by (simp add: ‹w = (v⇩w, α)›)
      also from ‹v ≠ w› have "… = FAbs w (❙S {v ↣ A} ❙S θ C)"
        by (simp add: ‹w = (v⇩w, α)›)
      also from FAbs.IH have "… = FAbs w (❙S ({v ↣ A} ++⇩f θ) C)"
        using FAbs.prems(1,2,3) by blast
      also from ‹v ≠ w› and True have "… = ❙S ({v ↣ A} ++⇩f θ) (FAbs w C)"
        by (simp add: ‹w = (v⇩w, α)›)
      finally show ?thesis .
    next
      case False
      then have "❙S {v ↣ A} ❙S θ (FAbs w C) = ❙S {v ↣ A} (FAbs w (❙S (fmdrop w θ) C))"
        by (simp add: ‹w = (v⇩w, α)›)
      also from ‹v ≠ w› have "… = FAbs w (❙S {v ↣ A} ❙S (fmdrop w θ) C)"
        by (simp add: ‹w = (v⇩w, α)›)
      also have "… = FAbs w (❙S ({v ↣ A} ++⇩f fmdrop w θ) C)"
      proof -
        from ‹is_substitution θ› have "is_substitution (fmdrop w θ)"
          by fastforce
        moreover from ‹θ $$ v = None› have "(fmdrop w θ) $$ v = None"
          by force
        moreover from FAbs.prems(3) have "∀v' ∈ fmdom' (fmdrop w θ). v ∉ vars ((fmdrop w θ) $$! v')"
          by force
        ultimately show ?thesis
          using FAbs.IH by blast
      qed
      also from ‹v ≠ w› have "… = ❙S ({v ↣ A} ++⇩f θ) (FAbs w C)"
        by (simp add: ‹w = (v⇩w, α)› fmdrop_idle')
      finally show ?thesis .
    qed
  next
    case False
    then show ?thesis
    proof (cases "w ∉ fmdom' θ")
      case True
      then have "❙S {v ↣ A} ❙S θ (FAbs w C) = ❙S {v ↣ A} (FAbs w (❙S θ C))"
        by (simp add: ‹w = (v⇩w, α)›)
      also from ‹¬ v ≠ w› have "… = FAbs w (❙S θ C)"
        using ‹w = (v⇩w, α)› and singleton_substitution_simps(4) by presburger
      also from ‹¬ v ≠ w› and True have "… = FAbs w (❙S (fmdrop w ({v ↣ A} ++⇩f θ)) C)"
        by (simp add: fmdrop_fmupd_same fmdrop_idle')
      also from ‹¬ v ≠ w› have "… = ❙S ({v ↣ A} ++⇩f θ) (FAbs w C)"
        by (simp add: ‹w = (v⇩w, α)›)
      finally show ?thesis .
    next
      case False
      then have "❙S {v ↣ A} ❙S θ (FAbs w C) = ❙S {v ↣ A} (FAbs w (❙S (fmdrop w θ) C))"
        by (simp add: ‹w = (v⇩w, α)›)
      also from ‹¬ v ≠ w› have "… = FAbs w (❙S (fmdrop w θ) C)"
        using ‹θ $$ v = None› and False by (simp add: fmdom'_notI)
      also from ‹¬ v ≠ w› have "… = FAbs w (❙S (fmdrop w ({v ↣ A} ++⇩f θ)) C)"
        by (simp add: fmdrop_fmupd_same)
      also from ‹¬ v ≠ w› and False and ‹θ $$ v = None› have "… = ❙S ({v ↣ A} ++⇩f θ) (FAbs w C)"
        by (simp add: fmdom'_notI)
      finally show ?thesis .
    qed
  qed
qed

lemma updated_substitution_is_substitution:
  assumes "v ∉ fmdom' θ" and "is_substitution (θ(v ↣ A))"
  shows "is_substitution θ"
unfolding is_substitution_def proof (intro ballI)
  fix v' :: var
  obtain x and α where "v' = (x, α)"
    by fastforce
  assume "v' ∈ fmdom' θ"
  with assms(2)[unfolded is_substitution_def] have "v' ∈ fmdom' (θ(v ↣ A))"
    by simp
  with assms(2)[unfolded is_substitution_def] have "θ(v ↣ A) $$! (x, α) ∈ wffs⇘α⇙"
    using ‹v' = (x, α)› by fastforce
  with assms(1) and ‹v' ∈ fmdom' θ› and ‹v' = (x, α)› have "θ $$! (x, α) ∈ wffs⇘α⇙"
     by (metis fmupd_lookup)
  then show "case v' of (x, α) ⇒ θ $$! (x, α) ∈ wffs⇘α⇙"
    by (simp add: ‹v' = (x, α)›)
qed

definition is_renaming_substitution where
  [iff]: "is_renaming_substitution θ ⟷ is_substitution θ ∧ fmpred (λ_ A. ∃v. A = FVar v) θ"

text ‹
  The following lemma proves that $
  \d{\textsf{S}}\;^{x^1_{\alpha_1}\;\dots\;x^n_{\alpha_n}}_{y^1_{\alpha_1}\;\dots\;y^n_{\alpha_n}} B
  =
  \d{\textsf{S}}\;^{x^1_{\alpha_1}}_{y^1_{\alpha_1}}\;\cdots\;
  \d{\textsf{S}}\;^{x^n_{\alpha_n}}_{y^n_{\alpha_n}} B$ provided that

    ▪ $x^1_{\alpha_1}\;\dots\;x^n_{\alpha_n}$ are distinct variables

    ▪ $y^1_{\alpha_1}\;\dots\;y^n_{\alpha_n}$ are distinct variables, distinct from
      $x^1_{\alpha_1}\;\dots\;x^n_{\alpha_n}$ and from all variables in ‹B› (i.e., they are fresh
      variables)

  In other words, simultaneously renaming distinct variables with fresh ones is equivalent to
  renaming each variable one at a time.
›

lemma fresh_vars_substitution_unfolding:
  fixes ps :: "(var × form) list"
  assumes "θ = fmap_of_list ps" and "is_renaming_substitution θ"
  and "distinct (map fst ps)" and "distinct (map snd ps)"
  and "vars (fmran' θ) ∩ (fmdom' θ ∪ vars B) = {}"
  shows "❙S θ B = foldr (λ(x, y) C. ❙S {x ↣ y} C) ps B"
using assms proof (induction ps arbitrary: θ)
  case Nil
  then have "θ = {$$}"
    by simp
  then have "❙S θ B = B"
    using empty_substitution_neutrality by (simp only:)
  with Nil show ?case
    by simp
next
  case (Cons p ps)
  from Cons.prems(1,2) obtain x and y where "θ $$ (fst p) = Some (FVar y)" and "p = (x, FVar y)"
    using surj_pair[of p] by fastforce
  let ?θ' = "fmap_of_list ps"
  from Cons.prems(1) and ‹p = (x, FVar y)› have "θ = fmupd x (FVar y) ?θ'"
    by simp
  moreover from Cons.prems(3) and ‹p = (x, FVar y)› have "x ∉ fmdom' ?θ'"
    by simp
  ultimately have "θ = {x ↣ FVar y} ++⇩f ?θ'"
    using fmap_singleton_comm by fastforce
  with Cons.prems(2) and ‹x ∉ fmdom' ?θ'› have "is_renaming_substitution ?θ'"
    unfolding is_renaming_substitution_def and ‹θ = fmupd x (FVar y) ?θ'›
    using updated_substitution_is_substitution by (metis fmdiff_fmupd fmdom'_notD fmpred_filter)
  from Cons.prems(2) and ‹θ = fmupd x (FVar y) ?θ'› have "is_renaming_substitution {x ↣ FVar y}"
    by auto
  have "
    foldr (λ(x, y) C. ❙S {x ↣ y} C) (p # ps) B
    =
    ❙S {x ↣ FVar y} (foldr (λ(x, y) C. ❙S {x ↣ y} C) ps B)"
    by (simp add: ‹p = (x, FVar y)›)
  also have "… = ❙S {x ↣ FVar y} ❙S ?θ' B"
  proof -
    from Cons.prems(3,4) have "distinct (map fst ps)" and "distinct (map snd ps)"
      by fastforce+
    moreover have "vars (fmran' ?θ') ∩ (fmdom' ?θ' ∪ vars B) = {}"
    proof -
      have "vars (fmran' θ) = vars ({FVar y} ∪ fmran' ?θ')"
        using ‹θ = fmupd x (FVar y) ?θ'› and ‹x ∉ fmdom' ?θ'› by (metis fmdom'_notD fmran'_fmupd)
      then have "vars (fmran' θ) = {y} ∪ vars (fmran' ?θ')"
        using singleton_form_set_vars by auto
      moreover have "fmdom' θ = {x} ∪ fmdom' ?θ'"
        by (simp add: ‹θ = {x ↣ FVar y} ++⇩f ?θ'›)
      ultimately show ?thesis
        using Cons.prems(5) by auto
    qed
    ultimately show ?thesis
      using Cons.IH and ‹is_renaming_substitution ?θ'› by simp
  qed
  also have "… = ❙S ({x ↣ FVar y} ++⇩f ?θ') B"
  proof (rule substitution_fusion)
    show "is_substitution ?θ'"
      using ‹is_renaming_substitution ?θ'› by simp
    show "is_substitution {x ↣ FVar y}"
      using ‹is_renaming_substitution {x ↣ FVar y}› by simp
    show "?θ' $$ x = None"
      using ‹x ∉ fmdom' ?θ'› by blast
    show "∀v' ∈ fmdom' ?θ'. x ∉ vars (?θ' $$! v')"
    proof -
      have "x ∈ fmdom' θ"
        using ‹θ = {x ↣ FVar y} ++⇩f ?θ'› by simp
      then have "x ∉ vars (fmran' θ)"
        using Cons.prems(5) by blast
      moreover have "{?θ' $$! v' | v'. v' ∈ fmdom' ?θ'} ⊆ fmran' θ"
        unfolding ‹θ = ?θ'(x ↣ FVar y)› using ‹?θ' $$ x = None›
        by (auto simp add: fmlookup_of_list fmlookup_dom'_iff fmran'I weak_map_of_SomeI)
      ultimately show ?thesis
        by force
    qed
  qed
  also from ‹θ = {x ↣ FVar y} ++⇩f ?θ'› have "… = ❙S θ B"
    by (simp only:)
  finally show ?case ..
qed

lemma free_vars_agreement_substitution_equality:
  assumes "fmdom' θ = fmdom' θ'"
  and "∀v ∈ free_vars A ∩ fmdom' θ. θ $$! v = θ' $$! v"
  shows "❙S θ A = ❙S θ' A"
using assms proof (induction A arbitrary: θ θ')
  case (FVar v)
  have "free_vars (FVar v) = {v}"
    using surj_pair[of v] by fastforce
  with FVar have "θ $$! v = θ' $$! v"
    by force
  with FVar.prems(1) show ?case
    using surj_pair[of v] by (metis fmdom'_notD fmdom'_notI option.collapse substitute.simps(1))
next
  case FCon
  then show ?case
    by (metis prod.exhaust_sel substitute.simps(2))
next
  case (FApp B C)
  have "❙S θ (B · C) = (❙S θ B) · (❙S θ C)"
    by simp
  also have "… = (❙S θ' B) · (❙S θ' C)"
  proof -
    have "∀v ∈ free_vars B ∩ fmdom' θ. θ $$! v = θ' $$! v"
    and "∀v ∈ free_vars C ∩ fmdom' θ. θ $$! v = θ' $$! v"
      using FApp.prems(2) by auto
    with FApp.IH(1,2) and FApp.prems(1) show ?thesis
      by blast
  qed
  finally show ?case
    by simp
next
  case (FAbs w B)
  from FAbs.prems(1,2) have *: "∀v ∈ free_vars B - {w} ∩ fmdom' θ. θ $$! v = θ' $$! v"
    using surj_pair[of w] by fastforce
  show ?case
  proof (cases "w ∈ fmdom' θ")
    case True
    then have "❙S θ (FAbs w B) = FAbs w (❙S (fmdrop w θ) B)"
      using surj_pair[of w] by fastforce
    also have "… = FAbs w (❙S (fmdrop w θ') B)"
    proof -
      from * have "∀v ∈ free_vars B ∩ fmdom' (fmdrop w θ). (fmdrop w θ) $$! v = (fmdrop w θ') $$! v"
        by simp
      moreover have "fmdom' (fmdrop w θ) = fmdom' (fmdrop w θ')"
        by (simp add: FAbs.prems(1))
      ultimately show ?thesis
        using FAbs.IH by blast
    qed
    finally show ?thesis
      using FAbs.prems(1) and True and surj_pair[of w] by fastforce
  next
    case False
    then have "❙S θ (FAbs w B) = FAbs w (❙S θ B)"
      using surj_pair[of w] by fastforce
    also have "… = FAbs w (❙S θ' B)"
    proof -
      from * have "∀v ∈ free_vars B ∩ fmdom' θ. θ $$! v = θ' $$! v"
        using False by blast
      with FAbs.prems(1) show ?thesis
        using FAbs.IH by blast
    qed
    finally show ?thesis
      using FAbs.prems(1) and False and surj_pair[of w] by fastforce
  qed
qed

text ‹
  The following lemma proves that $
  \d{\textsf{S}}\;^{x_\alpha}_{A_\alpha}\;
  \d{\textsf{S}}\;^{x^1_{\alpha_1}\;\dots\;x^n_{\alpha_n}}_{A^1_{\alpha_1}\;\dots\;A^n_{\alpha_n}} B
  =
  \d{\textsf{S}}\;{
  \begingroup \setlength\arraycolsep{2pt} \begin{matrix}
  \scriptstyle{x_\alpha} & \scriptstyle{x^1_{\alpha_1}} & \scriptstyle{\dots} & \scriptstyle{x^n_{\alpha_n}} \\
  \scriptstyle{A_\alpha} & \scriptstyle{\d{\small{\textsf{S}}}\;^{x_\alpha}_{A_\alpha} A^1_{\alpha_1}}
  & \scriptstyle{\dots} & \scriptstyle{\d{\small{\textsf{S}}}\;^{x_\alpha}_{A_\alpha} A^n_{\alpha_n}}
  \end{matrix} \endgroup} B$ provided that $x_\alpha$ is distinct from $x^1_{\alpha_1}, \dots, x^n_{\alpha_n}$
  and $A^i_{\alpha_i}$ is free for $x^i_{\alpha_i}$ in $B$:
›

lemma substitution_consolidation:
  assumes "v ∉ fmdom' θ"
  and "∀v' ∈ fmdom' θ. is_free_for (θ $$! v') v' B"
  shows "❙S {v ↣ A} ❙S θ B = ❙S ({v ↣ A} ++⇩f fmmap (λA'. ❙S {v ↣ A} A') θ) B"
using assms proof (induction B arbitrary: θ)
  case (FApp B C)
  have "∀v' ∈ fmdom' θ. is_free_for (θ $$! v') v' B ∧ is_free_for (θ $$! v') v' C"
  proof
    fix v'
    assume "v' ∈ fmdom' θ"
    with FApp.prems(2) have "is_free_for (θ $$! v') v' (B · C)"
      by blast
    then show "is_free_for (θ $$! v') v' B ∧ is_free_for (θ $$! v') v' C"
      using is_free_for_from_app by iprover
  qed
  with FApp.IH and FApp.prems(1) show ?case
    by simp
next
  case (FAbs w B)
  let ?θ' = "fmmap (λA'. ❙S {v ↣ A} A') θ"
  show ?case
  proof (cases "w ∈ fmdom' θ")
    case True
    then have "w ∈ fmdom' ?θ'"
      by simp
    with True and FAbs.prems have "v ≠ w"
      by blast
    from True have "❙S {v ↣ A} ❙S θ (FAbs w B) = ❙S {v ↣ A} (FAbs w (❙S (fmdrop w θ) B))"
      using surj_pair[of w] by fastforce
    also from ‹v ≠ w› have "… = FAbs w (❙S {v ↣ A} ❙S (fmdrop w θ) B)"
      using surj_pair[of w] by fastforce
    also have "… = FAbs w (❙S (fmdrop w ({v ↣ A} ++⇩f ?θ')) B)"
    proof -
      obtain x⇩w and α⇩w where "w = (x⇩w, α⇩w)"
        by fastforce
      have "∀v' ∈ fmdom' (fmdrop w θ). is_free_for ((fmdrop w θ) $$! v') v' B"
      proof
        fix v'
        assume "v' ∈ fmdom' (fmdrop w θ)"
        with FAbs.prems(2) have "is_free_for (θ $$! v') v' (FAbs w B)"
          by auto
        with ‹w = (x⇩w, α⇩w)› and ‹v' ∈ fmdom' (fmdrop w θ)›
        have "is_free_for (θ $$! v') v' (λx⇩w⇘α⇩w⇙. B)" and "v' ≠ (x⇩w, α⇩w)"
          by auto
        then have "is_free_for (θ $$! v') v' B"
          using is_free_for_from_abs by presburger
        with ‹v' ≠ (x⇩w, α⇩w)› and ‹w = (x⇩w, α⇩w)› show "is_free_for (fmdrop w θ $$! v') v' B"
          by simp
      qed
      moreover have "v ∉ fmdom' (fmdrop w θ)"
        by (simp add: FAbs.prems(1))
      ultimately show ?thesis
        using FAbs.IH and ‹v ≠ w› by (simp add: fmdrop_fmupd)
    qed
    finally show ?thesis
      using ‹w ∈ fmdom' ?θ'› and surj_pair[of w] by fastforce
  next
    case False
    then have "w ∉ fmdom' ?θ'"
      by simp
    from FAbs.prems have "v ∉ fmdom' ?θ'"
      by simp
    from False have *: "❙S {v ↣ A} ❙S θ (FAbs w B) = ❙S {v ↣ A} (FAbs w (❙S θ B))"
      using surj_pair[of w] by fastforce
    then show ?thesis
    proof (cases "v ≠ w")
      case True
      then have "❙S {v ↣ A} (FAbs w (❙S θ B)) = FAbs w (❙S {v ↣ A} (❙S θ B))"
        using surj_pair[of w] by fastforce
      also have "… = FAbs w (❙S ({v ↣ A} ++⇩f ?θ') B)"
      proof -
        obtain x⇩w and α⇩w where "w = (x⇩w, α⇩w)"
          by fastforce
        have "∀v' ∈ fmdom' θ. is_free_for (θ $$! v') v' B"
        proof
          fix v'
          assume "v' ∈ fmdom' θ"
          with FAbs.prems(2) have "is_free_for (θ $$! v') v' (FAbs w B)"
            by auto
          with ‹w = (x⇩w, α⇩w)› and ‹v' ∈ fmdom' θ› and False
          have "is_free_for (θ $$! v') v' (λx⇩w⇘α⇩w⇙. B)" and "v' ≠ (x⇩w, α⇩w)"
            by fastforce+
          then have "is_free_for (θ $$! v') v' B"
            using is_free_for_from_abs by presburger
          with ‹v' ≠ (x⇩w, α⇩w)› and ‹w = (x⇩w, α⇩w)› show "is_free_for (θ $$! v') v' B"
            by simp
        qed
        with FAbs.IH show ?thesis
          using FAbs.prems(1) by blast
      qed
      finally show ?thesis
      proof -
        assume "
          ❙S {v ↣ A} (FAbs w (❙S θ B)) = FAbs w (❙S ({v ↣ A} ++⇩f fmmap (substitute {v ↣ A}) θ) B)"
        moreover have "w ∉ fmdom' ({v ↣ A} ++⇩f fmmap (substitute {v ↣ A}) θ)"
          using False and True by auto
        ultimately show ?thesis
          using * and surj_pair[of w] by fastforce
      qed
    next
      case False
      then have "v ∉ free_vars (FAbs w (❙S θ B))"
        using surj_pair[of w] by fastforce
      then have **: "❙S {v ↣ A} (FAbs w (❙S θ B)) = FAbs w (❙S θ B)"
        using free_var_singleton_substitution_neutrality by blast
      also have "… = FAbs w (❙S ?θ' B)"
      proof -
        {
          fix v'
          assume "v' ∈ fmdom' θ"
          with FAbs.prems(1) have "v' ≠ v"
            by blast
          assume "v ∈ free_vars (θ $$! v')" and "v' ∈ free_vars B"
          with ‹v' ≠ v› have "¬ is_free_for (θ $$! v') v' (FAbs v B)"
            using form_with_free_binder_not_free_for by blast
          with FAbs.prems(2) and ‹v' ∈ fmdom' θ› and False have False
            by blast
        }
        then have "∀v' ∈ fmdom' θ. v ∉ free_vars (θ $$! v') ∨ v' ∉ free_vars B"
          by blast
        then have "∀v' ∈ fmdom' θ. v' ∈ free_vars B ⟶ ❙S {v ↣ A} (θ $$! v') = θ $$! v'"
          using free_var_singleton_substitution_neutrality by blast
        then have "∀v' ∈ free_vars B. θ $$! v' = ?θ' $$! v'"
          by (metis fmdom'_map fmdom'_notD fmdom'_notI fmlookup_map option.map_sel)
        then have "❙S θ B = ❙S ?θ' B"
          using free_vars_agreement_substitution_equality by (metis IntD1 fmdom'_map)
        then show ?thesis
          by simp
      qed
      also from False and FAbs.prems(1) have "… = FAbs w (❙S (fmdrop w ({v ↣ A} ++⇩f ?θ')) B)"
        by (simp add: fmdrop_fmupd_same fmdrop_idle')
      also from False have "… = ❙S ({v ↣ A} ++⇩f ?θ') (FAbs w B)"
        using surj_pair[of w] by fastforce
      finally show ?thesis
        using * and ** by (simp only:)
    qed
  qed
qed force+

lemma vars_range_substitution:
  assumes "is_substitution θ"
  and "v ∉ vars (fmran' θ)"
  shows "v ∉ vars (fmran' (fmdrop w θ))"
using assms proof (induction θ)
  case fmempty
  then show ?case
    by simp
next
  case (fmupd v' A θ)
  from fmdom'_notI[OF fmupd.hyps] and fmupd.prems(1) have "is_substitution θ"
    by (rule updated_substitution_is_substitution)
  moreover from fmupd.prems(2) and fmupd.hyps have "v ∉ vars (fmran' θ)"
    by simp
  ultimately have "v ∉ vars (fmran' (fmdrop w θ))"
    by (rule fmupd.IH)
  with fmupd.hyps and fmupd.prems(2) show ?case
    by (simp add: fmdrop_fmupd)
qed

lemma excluded_var_from_substitution:
  assumes "is_substitution θ"
  and "v ∉ fmdom' θ"
  and "v ∉ vars (fmran' θ)"
  and "v ∉ vars A"
  shows "v ∉ vars (❙S θ A)"
using assms proof (induction A arbitrary: θ)
  case (FVar v')
  then show ?case
  proof (cases "v' ∈ fmdom' θ")
    case True
    then have "θ $$! v' ∈ fmran' θ"
      by (simp add: fmlookup_dom'_iff fmran'I)
    with FVar(3) have "v ∉ vars (θ $$! v')"
      by simp
    with True show ?thesis
      using surj_pair[of v'] and fmdom'_notI by force
  next
    case False
    with FVar.prems(4) show ?thesis
      using surj_pair[of v'] by force
  qed
next
  case (FCon k)
  then show ?case
    using surj_pair[of k] by force
next
  case (FApp B C)
  then show ?case
    by auto
next
  case (FAbs w B)
  have "v ∉ vars B" and "v ≠ w"
    using surj_pair[of w] and FAbs.prems(4) by fastforce+
  then show ?case
  proof (cases "w ∉ fmdom' θ")
    case True
    then have "❙S θ (FAbs w B) = FAbs w (❙S θ B)"
      using surj_pair[of w] by fastforce
    moreover from FAbs.IH have "v ∉ vars (❙S θ B)"
      using FAbs.prems(1-3) and ‹v ∉ vars B› by blast
    ultimately show ?thesis
      using ‹v ≠ w› and surj_pair[of w] by fastforce
  next
    case False
    then have "❙S θ (FAbs w B) = FAbs w (❙S (fmdrop w θ) B)"
      using surj_pair[of w] by fastforce
    moreover have "v ∉ vars (❙S (fmdrop w θ) B)"
    proof -
      from FAbs.prems(1) have "is_substitution (fmdrop w θ)"
        by fastforce
      moreover from FAbs.prems(2) have "v ∉ fmdom' (fmdrop w θ)"
        by simp
      moreover from FAbs.prems(1,3) have "v ∉ vars (fmran' (fmdrop w θ))"
        by (fact vars_range_substitution)
      ultimately show ?thesis
        using FAbs.IH and ‹v ∉ vars B› by simp
    qed
    ultimately show ?thesis
      using ‹v ≠ w› and surj_pair[of w] by fastforce
  qed
qed

subsection ‹Renaming of bound variables›

fun rename_bound_var :: "var ⇒ nat ⇒ form ⇒ form" where
  "rename_bound_var v y (x⇘α⇙) = x⇘α⇙"
| "rename_bound_var v y (⦃c⦄⇘α⇙) = ⦃c⦄⇘α⇙"
| "rename_bound_var v y (B · C) = rename_bound_var v y B · rename_bound_var v y C"
| "rename_bound_var v y (λx⇘α⇙. B) =
    (
      if (x, α) = v then
        λy⇘α⇙. ❙S {(x, α) ↣ y⇘α⇙} (rename_bound_var v y B)
      else
        λx⇘α⇙. (rename_bound_var v y B)
    )"

lemma rename_bound_var_preserves_typing:
  assumes "A ∈ wffs⇘α⇙"
  shows "rename_bound_var (y, γ) z A ∈ wffs⇘α⇙"
using assms proof (induction A)
  case (abs_is_wff β A δ x)
  then show ?case
  proof (cases "(x, δ) = (y, γ)")
    case True
    from abs_is_wff.IH have "❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z A) ∈ wffs⇘β⇙"
      using substitution_preserves_typing by (simp add: wffs_of_type_intros(1))
    then have "λz⇘γ⇙. ❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z A) ∈ wffs⇘γ→β⇙"
      by blast
    with True show ?thesis
      by simp
  next
    case False
    from abs_is_wff.IH have "λx⇘δ⇙. rename_bound_var (y, γ) z A ∈ wffs⇘δ→β⇙"
      by blast
    with False show ?thesis
      by auto
  qed
qed auto

lemma old_bound_var_not_free_in_abs_after_renaming:
  assumes "A ∈ wffs⇘α⇙"
  and "z⇘γ⇙ ≠ y⇘γ⇙"
  and "(z, γ) ∉ vars A"
  shows "(y, γ) ∉ free_vars (rename_bound_var (y, γ) z (λy⇘γ⇙. A))"
  using assms and free_var_in_renaming_substitution by (induction A) auto

lemma rename_bound_var_free_vars:
  assumes "A ∈ wffs⇘α⇙"
  and "z⇘γ⇙ ≠ y⇘γ⇙"
  and "(z, γ) ∉ vars A"
  shows "(z, γ) ∉ free_vars (rename_bound_var (y, γ) z A)"
  using assms by (induction A) auto

lemma old_bound_var_not_free_after_renaming:
  assumes "A ∈ wffs⇘α⇙"
  and "z⇘γ⇙ ≠ y⇘γ⇙"
  and "(z, γ) ∉ vars A"
  and "(y, γ) ∉ free_vars A"
  shows "(y, γ) ∉ free_vars (rename_bound_var (y, γ) z A)"
using assms proof induction
  case (abs_is_wff β A α x)
  then show ?case
  proof (cases "(x, α) = (y, γ)")
    case True
    with abs_is_wff.hyps and abs_is_wff.prems(2) show ?thesis
      using old_bound_var_not_free_in_abs_after_renaming by auto
  next
    case False
    with abs_is_wff.prems(2,3) and assms(2) show ?thesis
      using abs_is_wff.IH by force
  qed
qed fastforce+

lemma old_bound_var_not_ocurring_after_renaming:
  assumes "A ∈ wffs⇘α⇙"
  and "z⇘γ⇙ ≠ y⇘γ⇙"
  shows "¬ occurs_at (y, γ) p (❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z A))"
using assms(1) proof (induction A arbitrary: p)
  case (var_is_wff α x)
  from assms(2) show ?case
    using subform_size_decrease by (cases "(x, α) = (y, γ)") fastforce+
next
  case (con_is_wff α c)
  then show ?case
    using occurs_at_alt_def(2) by auto
next
  case (app_is_wff α β A B)
  then show ?case
  proof (cases p)
    case (Cons d p')
    then show ?thesis
      by (cases d) (use app_is_wff.IH in auto)
  qed simp
next
  case (abs_is_wff β A α x)
  then show ?case
  proof (cases p)
    case (Cons d p')
    then show ?thesis
    proof (cases d)
      case Left
      have *: "¬ occurs_at (y, γ) p (λx⇘α⇙. ❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z A))"
        for x and α
        using Left and Cons and abs_is_wff.IH by simp
      then show ?thesis
      proof (cases "(x, α) = (y, γ)")
        case True
        with assms(2) have "
          ❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z (λx⇘α⇙. A))
          =
          λz⇘γ⇙. ❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z A)"
          using free_var_in_renaming_substitution and free_var_singleton_substitution_neutrality
          by simp
        moreover have "¬ occurs_at (y, γ) p (λz⇘γ⇙. ❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z A))"
          using Left and Cons and * by simp
        ultimately show ?thesis
          by simp
      next
        case False
        with assms(2) have "
          ❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z (λx⇘α⇙. A))
          =
          λx⇘α⇙. ❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z A)"
          by simp
        moreover have "¬ occurs_at (y, γ) p (λx⇘α⇙. ❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z A))"
          using Left and Cons and * by simp
        ultimately show ?thesis
          by simp
      qed
    qed (simp add: Cons)
  qed simp
qed

text ‹
  The following lemma states that the result of \<^term>‹rename_bound_var› does not contain bound
  occurrences of the renamed variable:
›

lemma rename_bound_var_not_bound_occurrences:
  assumes "A ∈ wffs⇘α⇙"
  and "z⇘γ⇙ ≠ y⇘γ⇙"
  and "(z, γ) ∉ vars A"
  and "occurs_at (y, γ) p (rename_bound_var (y, γ) z A)"
  shows "¬ in_scope_of_abs (z, γ) p (rename_bound_var (y, γ) z A)"
using assms(1,3,4) proof (induction arbitrary: p)
  case (var_is_wff α x)
  then show ?case
    by (simp add: subforms_from_var(2))
next
  case (con_is_wff α c)
  then show ?case
    using occurs_at_alt_def(2) by auto
next
  case (app_is_wff α β B C)
  from app_is_wff.prems(1) have "(z, γ) ∉ vars B" and "(z, γ) ∉ vars C"
    by simp_all
  from app_is_wff.prems(2)
  have "occurs_at (y, γ) p (rename_bound_var (y, γ) z B · rename_bound_var (y, γ) z C)"
    by simp
  then consider
    (a) "∃p'. p = « # p' ∧ occurs_at (y, γ) p' (rename_bound_var (y, γ) z B)"
  | (b) "∃p'. p = » # p' ∧ occurs_at (y, γ) p' (rename_bound_var (y, γ) z C)"
    using subforms_from_app by force
  then show ?case
  proof cases
    case a
    then obtain p' where "p = « # p'" and "occurs_at (y, γ) p' (rename_bound_var (y, γ) z B)"
      by blast
    then have "¬ in_scope_of_abs (z, γ) p' (rename_bound_var (y, γ) z B)"
      using app_is_wff.IH(1)[OF ‹(z, γ) ∉ vars B›] by blast
    then have "¬ in_scope_of_abs (z, γ) p (rename_bound_var (y, γ) z (B · C))" for C
      using ‹p = « # p'› and in_scope_of_abs_in_left_app by simp
    then show ?thesis
      by blast
  next
    case b
    then obtain p' where "p = » # p'" and "occurs_at (y, γ) p' (rename_bound_var (y, γ) z C)"
      by blast
    then have "¬ in_scope_of_abs (z, γ) p' (rename_bound_var (y, γ) z C)"
      using app_is_wff.IH(2)[OF ‹(z, γ) ∉ vars C›] by blast
    then have "¬ in_scope_of_abs (z, γ) p (rename_bound_var (y, γ) z (B · C))" for B
      using ‹p = » # p'› and in_scope_of_abs_in_right_app by simp
    then show ?thesis
      by blast
  qed
next
  case (abs_is_wff β A α x)
  from abs_is_wff.prems(1) have "(z, γ) ∉ vars A" and "(z, γ) ≠ (x, α)"
    by fastforce+
  then show ?case
  proof (cases "(y, γ) = (x, α)")
    case True
    then have "occurs_at (y, γ) p (λz⇘γ⇙. ❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z A))"
      using abs_is_wff.prems(2) by simp
    moreover have "¬ occurs_at (y, γ) p (λz⇘γ⇙. ❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z A))"
      using old_bound_var_not_ocurring_after_renaming[OF abs_is_wff.hyps assms(2)] and subforms_from_abs
      by fastforce
    ultimately show ?thesis
      by contradiction
  next
    case False
    then have *: "rename_bound_var (y, γ) z (λx⇘α⇙. A) = λx⇘α⇙. rename_bound_var (y, γ) z A"
      by auto
    with abs_is_wff.prems(2) have "occurs_at (y, γ) p (λx⇘α⇙. rename_bound_var (y, γ) z A)"
      by auto
    then obtain p' where "p = « # p'" and "occurs_at (y, γ) p' (rename_bound_var (y, γ) z A)"
      using subforms_from_abs by fastforce
    then have "¬ in_scope_of_abs (z, γ) p' (rename_bound_var (y, γ) z A)"
      using abs_is_wff.IH[OF ‹(z, γ) ∉ vars A›] by blast
    then have "¬ in_scope_of_abs (z, γ) (« # p') (λx⇘α⇙. rename_bound_var (y, γ) z A)"
      using ‹p = « # p'› and in_scope_of_abs_in_abs and ‹(z, γ) ≠ (x, α)› by auto
    then show ?thesis
      using * and ‹p = « # p'› by simp
  qed
qed

lemma is_free_for_in_rename_bound_var:
  assumes "A ∈ wffs⇘α⇙"
  and "z⇘γ⇙ ≠ y⇘γ⇙"
  and "(z, γ) ∉ vars A"
  shows "is_free_for (z⇘γ⇙) (y, γ) (rename_bound_var (y, γ) z A)"
proof (rule ccontr)
  assume "¬ is_free_for (z⇘γ⇙) (y, γ) (rename_bound_var (y, γ) z A)"
  then obtain p
    where "is_free_at (y, γ) p (rename_bound_var (y, γ) z A)"
    and "in_scope_of_abs (z, γ) p (rename_bound_var (y, γ) z A)"
    by force
  then show False
    using rename_bound_var_not_bound_occurrences[OF assms] by fastforce
qed

lemma renaming_substitution_preserves_bound_vars:
  shows "bound_vars (❙S {(y, γ) ↣ z⇘γ⇙} A) = bound_vars A"
proof (induction A)
  case (FAbs v A)
  then show ?case
    using singleton_substitution_simps(4) and surj_pair[of v]
    by (cases "v = (y, γ)") (presburger, force)
qed force+

lemma rename_bound_var_bound_vars:
  assumes "A ∈ wffs⇘α⇙"
  and "z⇘γ⇙ ≠ y⇘γ⇙"
  shows "(y, γ) ∉ bound_vars (rename_bound_var (y, γ) z A)"
  using assms and renaming_substitution_preserves_bound_vars by (induction A) auto

lemma old_var_not_free_not_occurring_after_rename:
  assumes "A ∈ wffs⇘α⇙"
  and "z⇘γ⇙ ≠ y⇘γ⇙"
  and "(y, γ) ∉ free_vars A"
  and "(z, γ) ∉ vars A"
  shows "(y, γ) ∉ vars (rename_bound_var (y, γ) z A)"
  using assms and rename_bound_var_bound_vars[OF assms(1,2)]
  and old_bound_var_not_free_after_renaming and vars_is_free_and_bound_vars by blast

end