Theory FOL_Syntax

(* Title:        Part of the proof of compactness of first-order logic following Harrison's one in
 *               HOL-Light
 * Author:       Sophie Tourret <sophie.tourret at inria.fr>, 2023 *)

theory FOL_Syntax
  imports
    Main
    Propositional_Proof_Systems.Compactness
    First_Order_Terms.Term
    First_Order_Terms.Subterm_and_Context
begin

(* Comments starting with != indicate discrepancies with Harrison's formalisation *)

no_notation Not ("❙¬")
no_notation And (infix "❙∧" 68)
no_notation Or  (infix "❙∨" 68)

(* ---------------------------------------------------------------------------------------*)
(* To remove once the following have been integrated to the AFP in First_Order_Terms.Term *)
lemma count_terms: ✐‹contributor ‹Sophie Tourret››
  "OFCLASS(('f::countable, 'v::countable) term,countable_class)" 
  by countable_datatype

instance "term" :: (countable, countable) countable
  ✐‹contributor ‹Sophie Tourret››
  using count_terms by simp
(* ---------------------------------------------------------------------------------------*)

type_synonym nterm = ‹(nat, nat) term›

lemma count_nterms: "OFCLASS(nterm,countable_class)"
  using count_terms by simp

instance formula :: (countable) countable
  by countable_datatype

term "test (0, [Var 0])"

abbreviation functions_term :: ‹nterm ⇒ (nat × nat) set› where
  ‹functions_term t ≡ funas_term t›

datatype form =
  Bot (‹❙⊥›)
| Atom (pred:nat) (args:‹nterm list›)
| Implies form form (infixl ‹❙⟶› 85)
| Forall nat form (‹❙∀ _❙. _› [0, 70] 70)

fun functions_form :: ‹form ⇒ (nat × nat) set› where
  ‹functions_form ❙⊥ = {}›
| ‹functions_form (Atom p ts) = (⋃ t ∈ set ts. functions_term t)› 
| ‹functions_form (φ ❙⟶ ψ) = functions_form φ ∪ functions_form ψ›
| ‹functions_form (❙∀ x❙. φ) = functions_form φ›

fun predicates_form :: ‹form ⇒ (nat × nat) set› where
  ‹predicates_form ❙⊥ = {}›
| ‹predicates_form (Atom p ts) = {(p, length ts)}›
| ‹predicates_form (φ ❙⟶ ψ) = predicates_form φ ∪ predicates_form ψ›
| ‹predicates_form (❙∀ x❙. φ) = predicates_form φ›

definition functions_forms :: ‹form set ⇒ (nat × nat) set› where
  ‹functions_forms fms ≡ ⋃f ∈ fms. functions_form f›

definition predicates :: ‹form set ⇒ (nat × nat) set› where
  ‹predicates fms ≡ ⋃f ∈ fms. predicates_form f›

definition language :: ‹form set ⇒ ((nat × nat) set × (nat × nat) set)› where
  ‹language fms = (functions_forms fms, predicates fms)›

lemma lang_singleton: ‹language {p} = (functions_form p, predicates_form p)›
  unfolding language_def functions_forms_def predicates_def by simp

abbreviation Not :: ‹form ⇒ form› (‹❙¬ _› [90] 90) where
  ‹❙¬ φ ≡ φ ❙⟶ ❙⊥›

abbreviation Top :: ‹form› (‹❙⊤›) where
  ‹❙⊤ ≡ ❙¬ ❙⊥›

abbreviation Or :: ‹form ⇒ form ⇒ form›
  (infixl ‹❙∨› 84) where
  ‹φ ❙∨ ψ ≡ (φ ❙⟶ ψ) ❙⟶ ψ›

abbreviation And :: ‹form ⇒ form ⇒ form›
  (infixl ‹❙∧› 84) where
  ‹φ ❙∧ ψ ≡ ❙¬ (❙¬ φ ❙∨ ❙¬ ψ)›

abbreviation Equiv :: ‹form ⇒ form ⇒ form›
  (infix ‹❙⟷› 70) where
  ‹φ ❙⟷ ψ ≡ (φ ❙⟶ ψ ❙∧ ψ ❙⟶ φ)› 

abbreviation Exists :: ‹nat ⇒ form ⇒ form›
  (‹❙∃ _❙. _› [0, 70] 70) where
  ‹❙∃ x❙. φ ≡ ❙¬ (❙∀ x❙. ❙¬ φ)›

lemma ex_all_distinct: ‹❙∀x❙. φ ≠ ❙∃y❙. ψ›
  by simp

abbreviation FVT :: ‹nterm ⇒ nat set› where
  ‹FVT ≡ vars_term›

fun FV :: ‹form ⇒ nat set› where
  ‹FV ❙⊥ = {}›
| ‹FV (Atom _ ts) = (⋃ a ∈ set ts. FVT a)›
| ‹FV (φ ❙⟶ ψ) = FV φ ∪ FV ψ›
| ‹FV (❙∀ x❙. φ) = FV φ - {x}›

lemma FV_all_subs: ‹FV φ ⊆ FV (❙∀ x❙. φ) ∪ {x}›
  by fastforce

lemma FV_exists: ‹FV (❙∃x❙. φ) = FV φ - {x}›
  by simp

lemma finite_FV: ‹finite (FV φ)›
  by (induction φ, auto)

fun BV :: ‹form ⇒ nat set› where
  ‹BV ❙⊥ = {}›
| ‹BV (Atom _ args') = {}›
| ‹BV (φ ❙⟶ ψ) = BV φ ∪ BV ψ›
| ‹BV (❙∀ x❙. φ) = BV φ ∪ {x}›

lemma finite_BV: ‹finite (BV φ)›
  by (induction φ, auto)

(* != substitutions over terms are defined in the Term theory *)

definition variant :: ‹nat set ⇒ nat› where
  ‹variant s = Max s + 1›

lemma variant_finite: ‹finite s ⟹ ¬ (variant s ∈ s)›
  unfolding variant_def using Max_ge less_le_not_le by auto

lemma variant_form: ‹¬ variant (FV φ) ∈ FV φ›
  using variant_finite finite_FV by blast

fun formsubst :: ‹form ⇒ (nat, nat) subst ⇒ form› (infixl ‹⋅⇩f⇩m› 75) where
  ‹❙⊥ ⋅⇩f⇩m _ = ❙⊥› 
| ‹(Atom p ts) ⋅⇩f⇩m σ = Atom p [t ⋅ σ. t ← ts]›
| ‹(φ ❙⟶ ψ) ⋅⇩f⇩m σ = (φ ⋅⇩f⇩m σ) ❙⟶ (ψ ⋅⇩f⇩m σ)›
| ‹(❙∀ x❙. φ) ⋅⇩f⇩m σ =
    (let σ' = σ(x := Var x);
         z = if ∃ y. y ∈ FV (❙∀ x❙. φ) ∧ x ∈ FVT (σ' y)
             then variant (FV (φ ⋅⇩f⇩m σ')) else x in
    ❙∀ z❙. (φ ⋅⇩f⇩m σ(x := Var z)))›

fun formsubst2 :: ‹form ⇒ (nat, nat) subst ⇒ form› (infixl ‹⋅⇩f⇩m2› 75) where
  ‹❙⊥ ⋅⇩f⇩m2 _ = ❙⊥› 
| ‹(Atom p ts) ⋅⇩f⇩m2 σ = Atom p [t ⋅ σ. t ← ts]›
| ‹(φ ❙⟶ ψ) ⋅⇩f⇩m2 σ = (φ ⋅⇩f⇩m2 σ) ❙⟶ (ψ ⋅⇩f⇩m2 σ)›
| ‹(❙∀ x❙. φ) ⋅⇩f⇩m2 σ = (let σ' = σ(x := Var x) in
    (if ∃ y. y ∈ FV (❙∀ x❙. φ) ∧ x ∈ FVT (σ' y)
    then (let z = variant (FV (φ ⋅⇩f⇩m2 σ')) in
      ❙∀ z❙. (φ ⋅⇩f⇩m2 σ(x := Var z)))
    else ❙∀ x❙. (φ ⋅⇩f⇩m2 σ')))›

lemma formsubst_def_switch: ‹φ ⋅⇩f⇩m σ = φ ⋅⇩f⇩m2 σ›
proof (induction φ arbitrary: σ rule: form.induct)
  case Bot
  then show ?case
    by fastforce
next
  case (Atom x1 x2)
  then show ?case
    by fastforce
next
  case (Implies x1 x2)
  then show ?case
    by fastforce
next
  case (Forall x1 x2)
  then show ?case
    by (smt (verit, best) formsubst.simps(4) formsubst2.simps(4))
qed

lemma termsubst_valuation: ‹∀x∈FVT t. σ x = σ' x ⟹ t ⋅ σ = t ⋅ σ'›
  using eval_same_vars by blast

lemma termsetsubst_valuation: ‹∀y ∈ T. ∀x∈FVT y. σ x = σ' x ⟹ t ∈ T ⟹ t ⋅ σ = t ⋅ σ'›
  using termsubst_valuation by fast

lemma formsubst_valuation: ‹∀x∈(FV φ). (Var x) ⋅ σ = (Var x) ⋅ σ' ⟹ φ ⋅⇩f⇩m σ = φ ⋅⇩f⇩m σ'›
proof (induction φ arbitrary: σ σ' rule:form.induct)
  case Bot
  then show ?case by simp
next
  case (Atom x1 x2)
  then show ?case
    using termsetsubst_valuation
    by auto
next
  case (Implies x1 x2)
  then show ?case by simp
next
  case (Forall x φ)
  define σ'' where "σ'' = σ(x := Var x)"
  define σ''' where "σ''' = σ'(x := Var x)"
  have ex_var_equiv: ‹∃ y. y ∈ FV (❙∀ x❙. φ) ∧ x ∈ FVT (σ'' y) ≡ ∃ y. y ∈ FV (❙∀ x❙. φ) ∧ x ∈ FVT (σ''' y)›
    using σ''_def σ'''_def Forall(2)
    by (smt (verit, ccfv_threshold) eval_term.simps(1) fun_upd_other fun_upd_same)
  have sig_x_subst: ‹∀y∈FV φ. Var y ⋅ σ(x := Var z) = Var y ⋅ σ'(x := Var z)› for z
    using Forall(2) by simp
  show ?case
  proof (cases ‹∃ y. y ∈ FV (❙∀ x❙. φ) ∧ x ∈ FVT (σ'' y)›)
    case True
    then have ‹(❙∀ x❙. φ) ⋅⇩f⇩m σ = (let z = variant (FV (φ ⋅⇩f⇩m σ'')) in ❙∀ z❙. (φ ⋅⇩f⇩m σ(x := Var z)))›
      by (simp add: σ''_def)
    also have ‹... = (let z = variant (FV (φ ⋅⇩f⇩m σ''')) in ❙∀ z❙. (φ ⋅⇩f⇩m σ'(x := Var z)))›
      using sig_x_subst σ'''_def by (metis Forall.IH σ''_def)
    also have ‹... = (❙∀ x❙. φ) ⋅⇩f⇩m σ'›
      using True σ'''_def ex_var_equiv formsubst.simps(4) by presburger
    finally show ?thesis .
  next
    case False
    then show ?thesis
      using Forall.IH σ'''_def σ''_def ex_var_equiv sig_x_subst by auto
  qed
qed

(* != needed in HOL-Light but seems trivial in modern Isabelle/HOL *)
lemma ‹{x. ∃y. y ∈ (s ∪ t) ∧ P x y} = {x. ∃y. y ∈ s ∧ P x y} ∪ {x. ∃y. y ∈ t ∧ P x y}›
  by blast

lemma formsubst_structure_bot: ‹φ ⋅⇩f⇩m σ = ❙⊥ ⟷ φ = ❙⊥›
  by (smt (verit) form.distinct(5) form.simps(5) form.simps(7) formsubst.elims)

lemma formsubst_structure_pred: ‹(∃p ts. φ ⋅⇩f⇩m σ = Atom p ts) ⟷ (∃p ts. φ = Atom p ts)›
proof (cases φ)
  case (Forall x ψ)
  then show ?thesis
    using formsubst_def_switch by (metis (no_types, lifting) form.distinct(10) formsubst.simps(4))
qed auto

lemma formsubst_structure_imp: ‹(∃φ1 φ2. φ ⋅⇩f⇩m σ = φ1 ❙⟶ φ2) ⟷ (∃ψ1 ψ2. φ = ψ1 ❙⟶ ψ2)›
proof (cases φ)
  case (Forall x ψ)
  then show ?thesis
    using formsubst_def_switch
    by (metis (no_types, lifting) form.distinct(11) formsubst.simps(4))
qed auto

lemma formsubst_structure_all: ‹(∃x ψ. φ ⋅⇩f⇩m σ = (❙∀x❙. ψ)) ⟷ (∃x ψ. φ = (❙∀x❙. ψ))›
proof (cases φ)
  case (Forall x ψ)
  then show ?thesis
    using formsubst_def_switch
    by (metis (no_types, lifting) formsubst.simps(4))
qed auto

lemma formsubst_structure_not: ‹(∃ψ. φ ⋅⇩f⇩m σ = Not ψ) ⟷ (∃ψ. φ = Not ψ)›
  using formsubst_structure_imp formsubst_structure_bot
  by (metis form.sel(4) formsubst.simps(3))

lemma formsubst_structure_not_all_imp: 
  ‹(∃x ψ. φ ⋅⇩f⇩m σ = (❙∀x❙. ψ) ❙⟶ ❙⊥) ⟷ (∃x ψ. φ = (❙∀x❙. ψ) ❙⟶ ❙⊥)›
proof (cases φ)
  case Bot
  then show ?thesis by simp
next
  case (Atom p ts)
  then show ?thesis by simp
next
  case (Implies φ1 φ2)
  then show ?thesis
    by (metis form.inject(2) formsubst.simps(3) formsubst_structure_all formsubst_structure_not)
next
  case (Forall y ψ)
  then show ?thesis
    by (metis form.distinct(11) formsubst_structure_not)
qed

lemma formsubst_structure_all_not: 
  ‹(∃x ψ. φ ⋅⇩f⇩m σ = (❙∀x❙. ψ ❙⟶ ❙⊥)) ⟷ (∃x ψ. φ = (❙∀x❙. ψ ❙⟶ ❙⊥))›
proof
  show ‹∃x ψ. φ = ❙∀ x❙. ψ ❙⟶ ❙⊥ ⟹ ∃x ψ. φ ⋅⇩f⇩m σ = ❙∀ x❙. ψ ❙⟶ ❙⊥›
    by (smt (verit, ccfv_threshold) formsubst.simps(1) formsubst.simps(3) formsubst.simps(4))
next
  assume ‹∃x ψ. φ ⋅⇩f⇩m σ = ❙∀x❙. ψ ❙⟶ ❙⊥›
  then obtain z ψ' where phi_sub_is: ‹φ ⋅⇩f⇩m σ = ❙∀z❙. ψ' ❙⟶ ❙⊥›
    by blast
  then obtain x φ' where phi_is: ‹φ = ❙∀x❙. φ'›
    using formsubst_structure_all by blast
  then have ‹∃σ'. φ' ⋅⇩f⇩m σ' = ψ' ❙⟶ ❙⊥›
    using phi_sub_is
    by (metis (no_types, lifting) form.sel(6) formsubst.simps(4))
  then obtain σ' where ‹φ' ⋅⇩f⇩m σ' = ψ' ❙⟶ ❙⊥›
    by blast
  then have ‹∃ψ. φ' = ψ ❙⟶ ❙⊥›
    using formsubst_structure_imp formsubst_structure_not by blast
  then show ‹∃x ψ. φ = ❙∀x❙. ψ ❙⟶ ❙⊥›
    using phi_is by blast
qed

lemma formsubst_structure_ex: ‹(∃x ψ. φ ⋅⇩f⇩m σ = (❙∃x❙. ψ)) ⟷ (∃x ψ. φ = (❙∃x❙. ψ))›
proof
  assume ‹∃x ψ. φ ⋅⇩f⇩m σ = (❙∃x❙. ψ)›
  then show ‹∃x ψ. φ = (❙∃x❙. ψ)›
    by (metis form.inject(2) formsubst.simps(3) formsubst_structure_all_not formsubst_structure_not)
next
  assume ‹(∃x ψ. φ = (❙∃x❙. ψ))›
  then show ‹∃x ψ. φ ⋅⇩f⇩m σ = (❙∃x❙. ψ)›
    by (smt (verit, ccfv_threshold) formsubst.simps(1) formsubst.simps(3) formsubst.simps(4))
qed 

lemma formsubst_structure: ‹(φ ⋅⇩f⇩m σ = ❙⊥ ⟷ φ = ❙⊥) ∧ 
  ((∃p ts. φ ⋅⇩f⇩m σ = Atom p ts) ⟷ (∃p ts. φ = Atom p ts)) ∧
  ((∃φ1 φ2. φ ⋅⇩f⇩m σ = φ1 ❙⟶ φ2) ⟷ (∃ψ1 ψ2. φ = ψ1 ❙⟶ ψ2)) ∧ 
  ((∃x ψ. φ ⋅⇩f⇩m σ = (❙∀x❙. ψ)) ⟷ (∃x ψ. φ = (❙∀x❙. ψ)))›
  using formsubst_structure_bot formsubst_structure_pred formsubst_structure_imp formsubst_structure_all
  by auto

lemma formsubst_fv: ‹FV (φ ⋅⇩f⇩m σ) = {x. ∃y. y ∈ (FV φ) ∧ x ∈ FVT ((Var y) ⋅ σ)}›
proof (induction φ arbitrary: σ rule:form.induct)
  case (Atom x1 x2)
  have ‹FV (Atom x1 x2 ⋅⇩f⇩m σ) = (⋃a ∈ set x2. FVT (a  ⋅ σ))›
    by auto
  also have ‹... = {x. ∃y. y ∈ (⋃a ∈ set x2. FVT a) ∧ x ∈ FVT ((Var y) ⋅ σ)}›
  proof 
    show ‹(⋃a∈set x2. FVT (a ⋅ σ)) ⊆ {x. ∃y. y ∈ (⋃a∈set x2. FVT a) ∧ x ∈ FVT (Var y ⋅ σ)}›
    proof
      fix v
      assume ‹v ∈ (⋃a∈set x2. FVT (a ⋅ σ))›
      then obtain a where a_is: ‹a ∈ set x2› ‹v ∈ FVT (a ⋅ σ)›
        by auto
      then obtain ya where ‹ya ∈ FVT a› ‹v ∈ FVT (Var ya ⋅ σ)›
        using eval_term.simps(1) vars_term_subst_apply_term by force
      then show ‹v ∈ {x. ∃y. y ∈ (⋃a∈set x2. FVT a) ∧ x ∈ FVT (Var y ⋅ σ)}›
        using a_is by auto
    qed
  next
    show ‹{x. ∃y. y ∈ (⋃a∈set x2. FVT a) ∧ x ∈ FVT (Var y ⋅ σ)} ⊆ (⋃a∈set x2. FVT (a ⋅ σ))›
    proof
      fix v
      assume ‹v ∈ {x. ∃y. y ∈ (⋃a∈set x2. FVT a) ∧ x ∈ FVT (Var y ⋅ σ)}›
      then obtain yv where ‹yv ∈ (⋃a∈set x2. FVT a)› ‹v ∈ FVT (Var yv ⋅ σ)›
        by auto
      then show ‹v ∈ (⋃a∈set x2. FVT (a ⋅ σ))›
        using vars_term_subst_apply_term by fastforce
    qed
  qed
  also have ‹... = {x. ∃y. y ∈ (FV (Atom x1 x2)) ∧ x ∈ FVT ((Var y) ⋅ σ)}›
    by auto
  finally show ?case .
next
  case (Forall x φ)
  define σ' where "σ' = σ(x := Var x)"
  show ?case
  proof (cases "∃ y. y ∈ FV (❙∀ x❙. φ) ∧ x ∈ FVT (σ' y)")
    case True
    then obtain y where y_in: ‹y ∈ FV (❙∀ x❙. φ)› and x_in: ‹x ∈ FVT (σ' y)›
      by blast
    then have y_neq_x: ‹y ≠ x› by simp
    then have y_in2: ‹y ∈ FV φ›
      using y_in by fastforce
    have x_in2: ‹x ∈ FVT (Var y ⋅ σ)›
      using x_in y_neq_x unfolding σ'_def by simp
  
    define z where "z = variant (FV (φ ⋅⇩f⇩m σ'))"
    have x_in3: ‹x ∈ FVT (Var y ⋅ σ(x := Var z))›
      using x_in2 y_neq_x by simp

    have ‹(❙∀ x❙. φ) ⋅⇩f⇩m σ = ❙∀ z❙. (φ ⋅⇩f⇩m σ(x := Var z))›
      using z_def formsubst_def_switch
      by (smt (verit, ccfv_threshold) True σ'_def formsubst.simps(4))
    then have ‹FV ((❙∀ x❙. φ) ⋅⇩f⇩m σ) = {xa. ∃y. y ∈ FV φ ∧ xa ∈ FVT (Var y ⋅ σ(x := Var z))} - {z}›
      using Forall[of "σ(x := Var z)"] using FV.simps(4) by presburger
    also have ‹... = {xa. ∃y. y ∈ FV φ - {x} ∧ xa ∈ FVT (Var y ⋅ σ)}›
    proof
      show ‹{xa. ∃y. y ∈ FV φ ∧ xa ∈ FVT (Var y ⋅ σ(x := Var z))} - {z} ⊆ 
        {xa. ∃y. y ∈ FV φ - {x} ∧ xa ∈ FVT (Var y ⋅ σ)}›
      proof
        fix xa
        assume xa_in: ‹xa ∈ {xa. ∃y. y ∈ FV φ ∧ xa ∈ FVT (Var y ⋅ σ(x := Var z))} - {z}›
        then obtain ya where ya_in: ‹ya ∈ FV φ› and xa_image: ‹xa ∈ FVT (Var ya ⋅ σ(x := Var z))›
          by blast
        have ya_neq_x: ‹ya ≠ x› using xa_image xa_in by fastforce
        then have ‹xa ∈ FVT (Var ya ⋅ σ)› using xa_image by simp
        moreover have ‹ya ∈ FV φ - {x}›
          using ya_neq_x ya_in by blast
        ultimately show ‹xa ∈ {xa. ∃y. y ∈ FV φ - {x} ∧ xa ∈ FVT (Var y ⋅ σ)}›
          by auto
      qed
    next
      show ‹{xa. ∃y. y ∈ FV φ - {x} ∧ xa ∈ FVT (Var y ⋅ σ)} ⊆ 
        {xa. ∃y. y ∈ FV φ ∧ xa ∈ FVT (Var y ⋅ σ(x := Var z))} - {z}›
      proof
        fix xa
        assume xa_in: ‹xa ∈ {xa. ∃y. y ∈ FV φ - {x} ∧ xa ∈ FVT (Var y ⋅ σ)}›
        then obtain ya where ya_in:  ‹ya ∈ FV φ - {x}› and xa_image: ‹xa ∈ FVT (Var ya ⋅ σ)›
          by blast
        have ya_neq: ‹ya ≠ x› using ya_in by blast
        then have xa_in2: ‹xa ∈ FVT (Var ya ⋅ σ(x := Var z))› using xa_image by simp
        then have ‹xa ∈ FV (φ ⋅⇩f⇩m σ(x := Var z))› 
          using ya_in Forall by force
        then have ‹xa ∈ FV (φ ⋅⇩f⇩m σ')›
          using ya_neq Forall xa_image ya_in unfolding σ'_def by auto
        then have ‹xa ≠ z› using z_def unfolding variant_def
          by (metis Max_ge Suc_eq_plus1 finite_FV lessI less_le_not_le)
        moreover have ‹ya ∈ FV φ› using ya_in by blast
        ultimately show ‹xa ∈ {xa. ∃y. y ∈ FV φ ∧ xa ∈ FVT (Var y ⋅ σ(x := Var z))} - {z}›
          using xa_in2 by blast
      qed
    qed
    finally show ?thesis by simp
  next
    case False
    then have ‹(❙∀ x❙. φ) ⋅⇩f⇩m σ = ❙∀ x❙. (φ ⋅⇩f⇩m σ')›
      using formsubst_def_switch σ'_def by fastforce
    then have ‹FV ((❙∀ x❙. φ) ⋅⇩f⇩m σ) = {z. ∃y. y ∈ FV φ ∧ z ∈ FVT (Var y ⋅ σ')} - {x}›
      using Forall by simp
    also have ‹... = {z. ∃y. y ∈ FV (❙∀ x❙. φ) ∧ z ∈ FVT (Var y ⋅ σ)}›
      using False unfolding σ'_def by auto
    finally show ?thesis .
  qed
qed auto

lemma subst_var [simp]: ‹φ ⋅⇩f⇩m Var = φ›
  by (induction φ) auto

lemma formsubst_rename: ‹FV (φ ⋅⇩f⇩m (subst x (Var y))) - {y} = FV φ - {x} - {y}›
proof (cases "y = x")
  case True
  then have ‹subst x (Var y) = Var›
    by simp
  then have ‹FV (φ ⋅⇩f⇩m (subst x (Var y))) = FV φ›
    using subst_var by metis
  then show ?thesis
    using True by simp
next
  case False
  show ?thesis
  proof
    show ‹FV (φ ⋅⇩f⇩m subst x (Var y)) - {y} ⊆ FV φ - {x} - {y}›
    proof
      fix v
      assume v_in: ‹v ∈ FV (φ ⋅⇩f⇩m subst x (Var y)) - {y}›
      moreover have ‹v ≠ x›
        using v_in
        by (smt (verit, ccfv_threshold) DiffE Term.term.simps(17) eval_term.simps(1)
            formsubst_fv fun_upd_other insert_iff mem_Collect_eq subst_def subst_simps(1))
      moreover have ‹v ∈ FV φ›
        by (smt (verit, del_insts) DiffE Term.term.simps(17) eval_term.simps(1) formsubst_fv 
            fun_upd_other mem_Collect_eq subst_def subst_simps(1) subst_var v_in)
      ultimately show ‹v ∈ FV φ - {x} - {y}›
        by blast
    qed
  next
    show ‹FV φ - {x} - {y} ⊆ FV (φ ⋅⇩f⇩m subst x (Var y)) - {y}›
      using formsubst_fv False by (smt (verit, del_insts) Diff_iff Term.term.simps(17) 
          mem_Collect_eq singleton_iff subsetI subst_ident)
  qed
qed

lemma termsubst_functions_term:
  ‹functions_term (t ⋅ σ) = functions_term t ∪ {x. ∃y. y ∈ FVT t ∧ x ∈ functions_term ((Var y) ⋅ σ)}›
  by (induction t arbitrary: σ) auto

lemma formsubst_functions_form: 
  ‹functions_form (φ ⋅⇩f⇩m σ) = functions_form φ ∪ {x. ∃y. y ∈ FV φ ∧ x ∈ functions_term ((Var y) ⋅ σ)}›
proof (induction φ arbitrary: σ)
  case Bot
  then show ?case by simp
next
  case (Atom p ts)
  show ?case
    using termsubst_functions_term by auto
next
  case (Implies φ ψ)
  then show ?case by auto
next
  case (Forall x φ)
  define σ' where ‹σ' = σ(x := Var x)›
  define z where ‹z = variant (FV (φ ⋅⇩f⇩m2 σ'))›
  have fun_terms_set_eq: ‹{xa. ∃y. y ∈ FV (❙∀ x❙. φ) ∧ xa ∈ functions_term (Var y ⋅ σ)} =
    (if (∃y. y ∈ FV (❙∀x❙. φ) ∧ x ∈ FVT (σ' y))
    then {xa. ∃y. y ∈ FV φ ∧ xa ∈ functions_term ((Var y) ⋅ σ(x := Var z))}
    else {x. ∃y. y ∈ FV φ ∧ x ∈ functions_term ((Var y) ⋅ σ')})› (is "?lhs = ?rhs")
  proof
    show ‹?lhs ⊆ ?rhs›
    proof
      fix v
      assume v_in: "v ∈ ?lhs"
      have ‹∃y. y ∈ FV (❙∀x❙. φ) ∧ x ∈ FVT (σ' y) ⟹ v ∈ {xa. ∃y. y ∈ FV φ ∧ xa ∈ functions_term ((Var y) ⋅ σ(x := Var z))}›
        using v_in by auto
      moreover have ‹∄y. y ∈ FV (❙∀x❙. φ) ∧ x ∈ FVT (σ' y) ⟹ v ∈ {x. ∃y. y ∈ FV φ ∧ x ∈ functions_term ((Var y) ⋅ σ')}›
        using v_in σ'_def by auto
      ultimately show "v ∈ ?rhs"
        by argo
    qed
  next
    show ‹?rhs ⊆ ?lhs›
    proof
      fix v
      assume v_in: ‹v ∈ ?rhs›
      have ‹∃y. y ∈ FV (❙∀x❙. φ) ∧ x ∈ FVT (σ' y) ⟹ v ∈ ?lhs›
        using v_in by (smt (verit, del_insts) Diff_empty Diff_insert0 FV.simps(4)
            Term.term.simps(17) empty_iff eval_term.simps(1) eval_with_fresh_var fun_upd_same
            funas_term.simps(1) insertE insert_Diff mem_Collect_eq)
      moreover have ‹∄y. y ∈ FV (❙∀x❙. φ) ∧ x ∈ FVT (σ' y) ⟹ v ∈ ?lhs›
        using v_in by (smt (verit, ccfv_threshold) Diff_iff FV.simps(4) σ'_def empty_iff
            eval_term.simps(1) fun_upd_other fun_upd_same funas_term.simps(1) insertE
            mem_Collect_eq)
      ultimately show ‹v ∈ ?lhs›
        by argo
    qed
  qed
  have ‹functions_form ((❙∀x❙. φ) ⋅⇩f⇩m σ) = functions_form ((❙∀ x❙. φ) ⋅⇩f⇩m2 σ)›
    using formsubst_def_switch by simp
  also have ‹... = (if (∃y. y ∈ FV (❙∀x❙. φ) ∧ x ∈ FVT (σ' y))
    then functions_form (❙∀ z❙. (φ ⋅⇩f⇩m2 σ(x := Var z)))
    else functions_form (❙∀ x❙. (φ ⋅⇩f⇩m2 σ')))›
    using σ'_def z_def by (smt (verit) formsubst2.simps(4))
  also have ‹... = (if (∃y. y ∈ FV (❙∀x❙. φ) ∧ x ∈ FVT (σ' y))
    then functions_form φ ∪ {xa. ∃y. y ∈ FV φ ∧ xa ∈ functions_term ((Var y) ⋅ σ(x := Var z))}
    else functions_form φ ∪ {x. ∃y. y ∈ FV φ ∧ x ∈ functions_term ((Var y) ⋅ σ')})›
    using formsubst_def_switch Forall by auto
  also have ‹... = functions_form φ ∪ (if (∃y. y ∈ FV (❙∀x❙. φ) ∧ x ∈ FVT (σ' y))
    then {xa. ∃y. y ∈ FV φ ∧ xa ∈ functions_term ((Var y) ⋅ σ(x := Var z))}
    else {x. ∃y. y ∈ FV φ ∧ x ∈ functions_term ((Var y) ⋅ σ')})›
    by auto
  finally show ?case
    using fun_terms_set_eq by auto
qed

lemma formsubst_predicates: ‹predicates_form (φ ⋅⇩f⇩m σ) = predicates_form φ›
proof (induction φ arbitrary: σ rule: predicates_form.induct)
  case (4 x φ)
  then show ?case
    by (metis (no_types, lifting) formsubst.simps(4) predicates_form.simps(4))
qed auto

lemma formsubst_language_rename: ‹language {φ ⋅⇩f⇩m subst x (Var y)} = language {φ}›
  using lang_singleton formsubst_predicates formsubst_functions_form by (simp add: subst_def)

end