Theory FOL_Semantics

(* 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_Semantics
  imports FOL_Syntax
begin

locale struct =
  fixes
    M :: ‹'m set› and
    FN :: ‹nat ⇒ 'm list ⇒ 'm› and
    REL :: ‹nat ⇒ 'm list set› (* in hol-ligh a boolean is returned instead *)
  assumes
    M_nonempty: ‹M ≠ {}›

typedef 'm intrp =
  ‹{ (M :: 'm set, FN :: nat ⇒ 'm list ⇒ 'm, REL :: nat ⇒ 'm list set). struct M}›
  using struct.intro
  by fastforce

declare Abs_intrp_inverse [simp] Rep_intrp_inverse [simp]

setup_lifting type_definition_intrp

lift_definition dom :: ‹'m intrp ⇒ 'm set› is fst .
lift_definition intrp_fn :: ‹'m intrp ⇒ (nat ⇒ 'm list ⇒ 'm)› is ‹fst ∘ snd› .
lift_definition intrp_rel :: ‹'m intrp ⇒ (nat ⇒ 'm list set)› is ‹snd ∘ snd› .

lemma intrp_is_struct [iff]: ‹struct (dom ℳ)›
  by transfer auto 

lemma dom_Abs_is_fst [simp]: ‹struct M ⟹ dom (Abs_intrp (M, FN, REL)) = M›
  by (simp add: dom.rep_eq) 

lemma intrp_fn_Abs_is_fst_snd [simp]: ‹struct M ⟹ intrp_fn (Abs_intrp (M, FN, REL)) = FN›
  by (simp add: intrp_fn.rep_eq) 

lemma intrp_rel_Abs_is_snd_snd [simp]: 
  ‹struct M ⟹ intrp_rel (Abs_intrp (M, FN, REL)) = REL›
  by (simp add: intrp_rel.rep_eq) 

(* in HOL Light: valuation *)
definition is_valuation :: ‹'m intrp ⇒ (nat ⇒ 'm) ⇒ bool› where
  ‹is_valuation ℳ β ⟷ (∀ v. β v ∈ dom ℳ)› 

lemma valuation_valmod: ‹⟦is_valuation ℳ β; a ∈ dom ℳ⟧ ⟹ is_valuation ℳ (β(x := a))›
  by (simp add: is_valuation_def)

fun eval (* HOL Light: termval *)
  :: ‹nterm ⇒ 'm intrp ⇒ (nat ⇒ 'm) ⇒ 'm›
  (‹⟦_⟧⇗_,_⇖› [50, 0, 0] 70) where
  ‹⟦Var v⟧⇗_,β⇖ = β v›
| ‹⟦Fun f ts⟧⇗ℳ,β⇖ = intrp_fn ℳ f [⟦t⟧⇗ℳ,β⇖. t ← ts]› 

definition list_all :: ‹('a ⇒ bool) ⇒ 'a list ⇒ bool› where
  [simp]: ‹list_all P ls ⟷ (fold (λl b. b ∧ P l) ls True)›

(*TERMSUBST_TERMVAL*)
lemma term_subst_eval: ‹intrp_fn M = Fun ⟹ t ⋅ v = eval t M v›
  by (induction t) auto

(*TERMVAL_TRIV*)
lemma term_eval_triv[simp]: ‹intrp_fn M = Fun ⟹ eval t M Var = t›
  by (metis subst_apply_term_empty term_subst_eval)

lemma fold_bool_prop: ‹(fold (λl b. b ∧ P l) ls b) = (b ∧ (∀l∈set ls. P l))›
  by (induction ls arbitrary: b) auto

lemma list_all_set: ‹list_all P ls = (∀l∈set ls. P l)›
  unfolding list_all_def using fold_bool_prop by auto

hide_const lang

definition is_interpretation where
  ‹is_interpretation lang ℳ ⟷ 
    ((∀f l. (f, length(l)) ∈ fst lang ∧ set l ⊆ dom ℳ ⟶ intrp_fn ℳ f l ∈ dom ℳ))›

lemma interpretation_sublanguage: ‹funs2 ⊆ funs1 ⟹ is_interpretation (funs1, pred1) ℳ
  ⟹ is_interpretation (funs2, preds2) ℳ›
  unfolding is_interpretation_def by auto

(*INTERPRETATION_TERMVAL in HOL Light*)
lemma interpretation_eval:
  assumes ℳ: ‹is_interpretation (functions_term t,any) ℳ› and val: ‹is_valuation ℳ β›
  shows ‹⟦t⟧⇗ℳ,β⇖ ∈ dom ℳ›
  using ℳ
proof (induction t)
  case (Var x)
  with val show ?case
    by (simp add: is_valuation_def)
next
  case (Fun f ts)
  then have ‹⟦t⟧⇗ℳ,β⇖ ∈ dom ℳ› if ‹t ∈ set ts› for t
    by (meson interpretation_sublanguage supt.arg supt_imp_funas_term_subset that)
  then show ?case
    using Fun by (simp add: is_interpretation_def image_subsetI)
qed

(* Notation Warning: To prevent ambiguity with tuples, the comma is *bold* *)
fun holds
  :: ‹'m intrp ⇒ (nat ⇒ 'm) ⇒ form ⇒ bool› (‹_,_ ⊨ _› [30, 30, 80] 80) where
  ‹ℳ,β ⊨ ⊥ ⟷ False›
| ‹ℳ,β ⊨ Atom p ts ⟷ [⟦t⟧⇗ℳ,β⇖. t ← ts] ∈ intrp_rel ℳ p›
| ‹ℳ,β ⊨ φ ⟶ ψ ⟷ ((ℳ,β ⊨ φ) ⟶ (ℳ,β ⊨ ψ))›
| ‹ℳ,β ⊨ (∀x. φ) ⟷ (∀a ∈ dom ℳ. ℳ,β(x := a) ⊨ φ)›

lemma holds_exists: ‹ℳ,β ⊨ (∃x. φ) ⟷ (∃a ∈ dom ℳ. ℳ,β(x := a) ⊨ φ)›
  by simp

lemma holds_indep_β_if:
  ‹∀ v ∈ FV φ. β1 v = β2 v ⟹ ℳ,β1 ⊨ φ ⟷ ℳ,β2 ⊨ φ›
proof (induction φ arbitrary: β1 β2)
  case Bot
  then show ?case
    by simp
next
  case (Atom p ts)
  then have ‹∀ t ∈ set ts. ∀ v ∈ FVT t. β1 v = β2 v›
    by simp 
  then have ‹[⟦t⟧⇗ℳ,β1⇖. t ← ts] = [⟦t⟧⇗ℳ,β2⇖. t ← ts]›
  proof (induction ts) 
    case Nil
    then show ?case
      by simp
  next
    case (Cons a ts)
    then show ?case
    proof (induction a)
      case (Var x)
      then show ?case
        by simp 
    next
      case (Fun f ts')
      then have ‹∀ t ∈ set ts'. ∀ v ∈ FVT t. β1 v = β2 v›
        by simp 
      then have ‹[⟦t⟧⇗ℳ,β1⇖. t ← ts'] = [⟦t⟧⇗ℳ,β2⇖. t ← ts']›
        using Cons.IH Fun.IH Fun.prems(2)
        by force
      then have ‹intrp_fn ℳ f [⟦t⟧⇗ℳ,β1⇖. t ← ts'] = intrp_fn ℳ f [⟦t⟧⇗ℳ,β2⇖. t ← ts']›
        by argo 
      then show ?case
        using Cons.IH Fun.prems(2)
        by force 
    qed
  qed
  then have ‹[⟦t⟧⇗ℳ,β1⇖. t ← ts] ∈ intrp_rel ℳ p ⟷ [⟦t⟧⇗ℳ,β2⇖. t ← ts] ∈ intrp_rel ℳ p›
    by argo
  then show ?case
    by simp
next
  case (Implies φ ψ)
  then have
    ‹∀v ∈ FV φ. β1 v = β2 v› and
    ‹∀v ∈ FV ψ. β1 v = β2 v›
    by auto
  then have
    ‹ℳ,β1 ⊨ φ ⟷ ℳ,β2 ⊨ φ› and
    ‹ℳ,β1 ⊨ ψ ⟷ ℳ,β2 ⊨ ψ›
    using Implies.IH by auto
  then show ?case
    by simp
next
  case (Forall x φ)
  then have ‹∀a ∈ dom ℳ. (ℳ,β1(x := a) ⊨ φ) = (ℳ,β2(x := a) ⊨ φ)›
    by simp
  then show ?case 
    by simp
qed

lemma holds_indep_intrp_if:
  fixes
    φ :: form and
    ℳ ℳ' :: ‹'m intrp› 
  assumes
    dom_eq: ‹dom ℳ = dom ℳ'› and
    rel_eq: ‹∀ p. intrp_rel ℳ p = intrp_rel ℳ' p› and
    fn_eq: ‹∀ f ts. (f, length ts) ∈ functions_form φ ⟶ intrp_fn ℳ f ts = intrp_fn ℳ' f ts›
  shows
    ‹∀β.  ℳ,β ⊨ φ ⟷ ℳ',β ⊨ φ›
  using fn_eq
proof (intro allI impI, induction φ)
  case (Atom p ts)

  have all_fn_sym_in: ‹(⋃ t ∈ set ts. functions_term t) ⊆ functions_form (Atom p ts)› (is ‹?A ⊆ _›)
    by simp 

  have eval_tm_eq: ‹⟦t⟧⇗ℳ,β⇖ = ⟦t⟧⇗ℳ',β⇖›
    if ‹functions_term t ⊆ functions_form (Atom p ts)› 
    for t 
    using that
  proof (induction t) 
    case (Fun f ts') 

    have ‹∀ t' ∈ set ts'. functions_term t' ⊆ functions_form (Atom p ts)›
      using Fun.prems
      by auto
    moreover have ‹(f, length [⟦t'⟧⇗ℳ,β⇖. t' ← ts']) ∈ functions_form (Atom p ts)›
      using Fun.prems
      by fastforce 
    ultimately show ?case
      using Fun.IH Atom.prems(1)[rule_format, of f ‹[⟦t'⟧⇗ℳ,β⇖. t' ← ts']›] 
      by (smt (verit, del_insts) eval.simps(2) map_eq_conv)
  qed auto 

  have ‹ℳ,β ⊨ Atom p ts ⟷ [⟦t⟧⇗ℳ,β⇖. t ← ts] ∈ intrp_rel ℳ p›
    by simp
  also have ‹... ⟷ [⟦t⟧⇗ℳ,β⇖. t ← ts] ∈ intrp_rel ℳ' p›
    by (simp add: rel_eq)
  also have ‹... ⟷ [⟦t⟧⇗ℳ',β⇖. t ← ts] ∈ intrp_rel ℳ' p›
    using eval_tm_eq all_fn_sym_in
    by (metis (mono_tags, lifting) UN_subset_iff map_eq_conv)
  also have ‹... ⟷ ℳ',β ⊨ Atom p ts›
    by auto 
  finally show ?case .
next
  case (Forall x φ)

  have ‹ℳ,β ⊨ (∀ x. φ) ⟷ (∀ a ∈ dom ℳ. ℳ,β(x := a) ⊨ φ)›
    by simp 
  also have ‹... = (∀ a ∈ dom ℳ. ℳ',β(x := a) ⊨ φ)›
    using Forall.IH Forall.prems by simp
  also have ‹... = (∀ a ∈ dom ℳ'. ℳ',β(x := a) ⊨ φ)›
    by (simp add: dom_eq)
  also have ‹... = (ℳ',β ⊨ (∀ x. φ))›
    by auto 
  finally show ?case . 
qed auto

text ‹the above in a more idiomatic form (it is a congruence rule)›
corollary holds_cong:
  assumes
    ‹dom ℳ = dom ℳ'›
    ‹⋀p. intrp_rel ℳ p = intrp_rel ℳ' p›
    ‹⋀f ts. (f, length ts) ∈ functions_form φ ⟹ intrp_fn ℳ f ts = intrp_fn ℳ' f ts›
  shows ‹ℳ,β ⊨ φ ⟷ ℳ',β ⊨ φ›
  using assms holds_indep_intrp_if by blast

abbreviation (input) ‹termsubst ℳ β σ v ≡ ⟦σ v⟧⇗ℳ,β⇖›

(* HOL Light: termval_termsubst *)
lemma subst_lemma_terms: ‹⟦t ⋅ σ⟧⇗ℳ,β⇖ = ⟦t⟧⇗ℳ,termsubst ℳ β σ⇖›
proof (induction t)
  case (Var v)
  then show ?case
    by auto 
next
  case (Fun f ts)

  have ‹⟦Fun f ts ⋅ σ⟧⇗ℳ,β⇖ = ⟦Fun f [t ⋅ σ. t ← ts]⟧⇗ℳ,β⇖›
    by auto
  also have ‹... = intrp_fn ℳ f [⟦t⟧⇗ℳ,β⇖. t ← [t ⋅ σ. t ← ts]]›
    by auto 
  also have ‹... = intrp_fn ℳ f [⟦t ⋅ σ⟧⇗ℳ,β⇖. t ← ts]›
    unfolding map_map
    by (meson comp_apply)
  also have ‹... = intrp_fn ℳ f [⟦t⟧⇗ℳ,termsubst ℳ β σ⇖. t ← ts]›
    using Fun.IH
    by (smt (verit, best) map_eq_conv) 
  also have ‹... = ⟦Fun f ts⟧⇗ℳ,termsubst ℳ β σ⇖›
    by auto 
  finally show ?case .
qed

lemma eval_indep_β_if:
  assumes ‹∀ v ∈ FVT t. β v = β' v›
  shows ‹⟦t⟧⇗ℳ,β⇖ = ⟦t⟧⇗ℳ,β'⇖›
    using assms
proof (induction t)
  case (Var v)
  then show ?case
    by auto 
next
  case (Fun f ts)
  then show ?case
    by (smt (verit, ccfv_SIG) eval.simps(2) map_eq_conv term.set_intros(4)) 
qed

lemma concat_map: ‹[f t. t ← [g t. t ← ts]] = [f (g t). t ← ts]› by simp

(* more general than HOL Light: holds_formsubst1 holds_rename *)
lemma swap_subst_eval: ‹ℳ,β ⊨ (φ ⋅fm σ) ⟷ ℳ,(λv. termsubst ℳ β σ v) ⊨ φ›
proof (induction φ arbitrary: σ β)
  case (Atom p ts)
  have ‹ℳ,β ⊨ (Atom p ts ⋅fm σ) ⟷ ℳ,β ⊨ (Atom p [t ⋅ σ. t ← ts])›
    by auto
  also have ‹... ⟷ [⟦t⟧⇗ℳ,β⇖. t ← [t ⋅ σ. t ← ts]] ∈ intrp_rel ℳ p›
    by auto
  also have ‹... ⟷ [⟦t ⋅ σ⟧⇗ℳ,β⇖. t ← ts] ∈ intrp_rel ℳ p›
    using concat_map[of "λt. ⟦t⟧⇗ℳ,β⇖" "λt. t ⋅ σ"] by presburger
  also have ‹... ⟷ [⟦t⟧⇗ℳ,termsubst ℳ β σ⇖. t ← ts] ∈ intrp_rel ℳ p›
    using subst_lemma_terms[of _ σ ℳ β] by auto
  finally show ?case
    by simp
next
  case (Forall x φ)
  define σ' where "σ' = σ(x := Var x)"
  show ?case
  proof (cases ‹∃ y. y ∈ FV (∀ x. φ) ∧ x ∈ FVT (σ' y)›)
    case False
    then have ‹(∀x. φ) ⋅fm σ = ∀x. (φ ⋅fm σ')›
      using formsubst_def_switch σ'_def by fastforce
    then have ‹ℳ,β ⊨ ((∀x. φ) ⋅fm σ) = (∀a ∈ dom ℳ. ℳ,β(x := a) ⊨ (φ ⋅fm σ'))›
      by auto
    also have ‹... = (∀a ∈ dom ℳ. ℳ,(λv. ⟦σ' v⟧⇗ℳ,β(x := a)⇖) ⊨ φ)›
      using Forall by blast
    also have ‹... = (∀a ∈ dom ℳ. ℳ,(λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a) ⊨ φ)›
    proof
      assume forward: ‹∀a ∈ dom ℳ. ℳ,(λv. ⟦σ' v⟧⇗ℳ,β(x := a)⇖) ⊨ φ›
      show ‹∀a ∈ dom ℳ. ℳ,(λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a) ⊨ φ›
      proof
        fix a
        assume ‹a ∈ dom ℳ›
        then have ‹ℳ,(λv. ⟦σ' v⟧⇗ℳ,β(x := a)⇖) ⊨ φ›
          using forward by blast
        moreover have ‹∀v∈FV φ. (λv. ⟦σ' v⟧⇗ℳ,β(x := a)⇖) v = ((λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a)) v›
        proof
          fix v
          assume ‹v ∈ FV φ›
          then have ‹v ≠ x ⟹ ⟦σ' v⟧⇗ℳ,β(x := a)⇖ = ((λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a)) v›
            by (metis (mono_tags, lifting) DiffI FV.simps(4) False eval_indep_β_if fun_upd_other singletonD)
          moreover have ‹v = x ⟹ ⟦σ' v⟧⇗ℳ,β(x := a)⇖ = ((λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a)) v›
            using σ'_def by auto
          ultimately show ‹⟦σ' v⟧⇗ℳ,β(x := a)⇖ = ((λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a)) v›
            by simp
        qed
        ultimately show ‹ℳ,(λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a) ⊨ φ›
          using holds_indep_β_if by fast
      qed
    next
      assume backward: ‹∀a ∈ dom ℳ. ℳ,(λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a) ⊨ φ›
      show ‹∀a ∈ dom ℳ. ℳ,(λv. ⟦σ' v⟧⇗ℳ,β(x := a)⇖) ⊨ φ›
      proof
        fix a
        assume ‹a ∈ dom ℳ›
        then have ‹ℳ,(λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a) ⊨ φ›
          using backward by blast
        moreover have ‹∀v∈FV φ. (λv. ⟦σ' v⟧⇗ℳ,β(x := a)⇖) v = ((λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a)) v›
        proof
          fix v
          assume ‹v ∈ FV φ›
          then have ‹v ≠ x ⟹ ⟦σ' v⟧⇗ℳ,β(x := a)⇖ = ((λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a)) v›
            by (metis (mono_tags, lifting) DiffI FV.simps(4) False eval_indep_β_if fun_upd_other singletonD)
          moreover have ‹v = x ⟹ ⟦σ' v⟧⇗ℳ,β(x := a)⇖ = ((λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a)) v›
            using σ'_def by auto
          ultimately show ‹⟦σ' v⟧⇗ℳ,β(x := a)⇖ = ((λv. ⟦σ' v⟧⇗ℳ,β⇖)(x := a)) v›
            by simp
        qed
        ultimately show ‹ℳ,(λv. ⟦σ' v⟧⇗ℳ,β(x := a)⇖) ⊨ φ›
          using holds_indep_β_if by fast
      qed
    qed
    also have ‹... = (ℳ,(λv. ⟦σ v⟧⇗ℳ,β⇖) ⊨ (∀ x. φ))›
      by (smt (verit, ccfv_SIG) σ'_def fun_upd_apply holds.simps(4) holds_indep_β_if)
    finally show ?thesis .
  next
    case True
    then have x_ex: ‹∃y. y ∈ FV φ - {x} ∧ x ∈ FVT (σ' y)›
      by simp
    then have x_in: ‹x ∈ FV (φ ⋅fm σ')›
      using formsubst_fv
      by auto
    define z where ‹z = variant (FV (φ ⋅fm σ'))›
    then have ‹z ≠ x›
      using x_in variant_form by auto
    have ‹(∀ x. φ) ⋅fm σ =  ∀ z. (φ ⋅fm σ(x := Var z))›
      using z_def True formsubst_def_switch σ'_def by (smt (verit, best) formsubst.simps(4))
    then have ‹ℳ,β ⊨ ((∀x. φ) ⋅fm σ) = (∀a ∈ dom ℳ. ℳ,β(z := a) ⊨ (φ ⋅fm σ(x := Var z)))›
      by auto
    also have ‹... = (∀a ∈ dom ℳ. ℳ,(λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖) ⊨ φ)›
      using Forall by blast
    also have ‹... = (∀a ∈ dom ℳ. ℳ,(λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a) ⊨ φ)›
    proof
      assume forward: ‹∀a∈dom ℳ. ℳ,(λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖) ⊨ φ›
      show ‹∀a∈dom ℳ. ℳ,(λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a) ⊨ φ›
      proof
        fix a
        assume ‹a ∈ dom ℳ›
        then have ‹ℳ,(λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖) ⊨ φ›
          using forward by blast
        moreover have ‹∀v∈FV φ. (λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖) v = 
          ((λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a)) v›
        proof
          fix v
          assume v_in: ‹v ∈ FV φ›
          then have ‹v ≠ x ⟹ z ∉ FVT (σ v)›
            using z_def variant_form by (smt (verit, ccfv_threshold) σ'_def eval_term.simps(1) 
              formsubst_fv fun_upd_other mem_Collect_eq)
          then have ‹v ≠ x ⟹ ⟦σ v⟧⇗ℳ,β(z := a)⇖ = ⟦σ v⟧⇗ℳ,β⇖›
            by (simp add: eval_indep_β_if)
          then have ‹v ≠ x ⟹
            (λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖) v = ((λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a)) v›
            by auto
          moreover have ‹v = x ⟹
            (λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖) v = ((λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a)) v›
            by auto
          ultimately show 
            ‹⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖ = ((λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a)) v›
            by auto
        qed
        ultimately show ‹ℳ,(λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a) ⊨ φ›
          using holds_indep_β_if by fast
      qed
    next
      assume backward: ‹∀a∈dom ℳ. ℳ,(λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a) ⊨ φ›
      show ‹∀a∈dom ℳ. ℳ,(λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖) ⊨ φ›
      proof
        fix a
        assume ‹a ∈ dom ℳ›
        then have ‹ℳ,(λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a) ⊨ φ›
          using backward by auto
        moreover have ‹∀v∈FV φ. (λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖) v = 
          ((λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a)) v›
        proof
          fix v
          assume v_in: ‹v ∈ FV φ›
          then have ‹v ≠ x ⟹ z ∉ FVT (σ v)›
            using z_def variant_form by (smt (verit, ccfv_threshold) σ'_def eval_term.simps(1) 
              formsubst_fv fun_upd_other mem_Collect_eq)
          then have ‹v ≠ x ⟹ ⟦σ v⟧⇗ℳ,β(z := a)⇖ = ⟦σ v⟧⇗ℳ,β⇖›
            by (simp add: eval_indep_β_if)
          then have ‹v ≠ x ⟹
            (λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖) v = ((λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a)) v›
            by auto
          moreover have ‹v = x ⟹
            (λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖) v = ((λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a)) v›
            by auto
          ultimately show 
            ‹⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖ = ((λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β⇖)(x := a)) v›
            by auto
        qed
        ultimately show ‹ℳ,(λv. ⟦(σ(x := Var z)) v⟧⇗ℳ,β(z := a)⇖) ⊨ φ›
          using holds_indep_β_if by fast
      qed
    qed
    also have ‹... = (∀a ∈ dom ℳ. ℳ,(λv. ⟦σ v⟧⇗ℳ,β⇖)(x := a) ⊨ φ)›
      by (smt (verit, ccfv_SIG) fun_upd_apply holds_indep_β_if)
    also have ‹... = (ℳ,(λv. ⟦σ v⟧⇗ℳ,β⇖) ⊨ (∀ x. φ))›
      by auto
    finally show ?thesis .
  qed
qed auto

definition satisfies :: ‹'m intrp ⇒ form set ⇒ bool› where
  ‹satisfies ℳ S ≡ (∀β φ. is_valuation ℳ β ⟶ φ ∈ S ⟶ ℳ,β ⊨ φ)›

lemma satisfies_iff_satisfies_sing: ‹satisfies M S ⟷ (∀φ∈S. satisfies M {φ})›
  by (auto simp: satisfies_def)


end