Theory Canonical_Models

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

theory Canonical_Models
  imports Skolem_Normal_Form
begin


inductive_set terms_set :: ‹(nat × nat) set ⇒ nterm set› for fns :: ‹(nat × nat) set› where
  vars: ‹(Var v) ∈ terms_set fns›
| fn: ‹(Fun f ts) ∈ terms_set fns›
  if ‹(f, length ts) ∈ fns› ‹⋀t. t ∈ set ts ⟹ t ∈ terms_set fns›

lemma struct_terms_set [iff]: ‹struct (terms_set A)›
  by (metis empty_iff struct.intro terms_set.vars)

(* STUPID_CANONDOM_LEMMA in HOL Light *)
lemma stupid_canondom: ‹t ∈ terms_set (fst ℒ) ⟹ functions_term t ⊆ (fst ℒ)›
  by (induction t rule: terms_set.induct) auto

(* FINITE_SUBSET_INSTANCE in HOL Light *)
lemma finite_subset_instance: ‹finite t' ⟹ t' ⊆ {φ ⋅⇩f⇩m σ |σ φ. P σ ∧ φ ∈ s} ⟹
  (∃t. finite t ∧ t ⊆ s ∧ t' ⊆ {φ ⋅⇩f⇩m σ |σ φ. P σ ∧ φ ∈ t})›
proof (induction t' rule: finite.induct)
  case emptyI
  then show ?case by blast
next
  case (insertI A a)
  obtain φa where phi_in: ‹φa ∈ s› and phi_ex_subs: ‹∃σ. P σ ∧ a = φa ⋅⇩f⇩m σ›
    using insertI(3) by auto
  obtain Φ where Phi_subs: ‹Φ ⊆ s› and ‹finite Φ› and Phi_set: ‹A ⊆ {φ ⋅⇩f⇩m σ |σ φ. P σ ∧ φ ∈ Φ}›
    using insertI(3) insertI(2) by auto
  then have ‹finite (φa ▹ Φ)›
    by auto
  moreover have ‹(φa ▹ Φ) ⊆ s›
    using phi_in Phi_subs by auto
  moreover have ‹a ▹ A ⊆ {φ ⋅⇩f⇩m σ |σ φ. P σ ∧ φ ∈ (φa ▹ Φ)}›
    using phi_ex_subs Phi_set by blast
  ultimately show ?case by blast
qed

(* FINITE_SUBSET_SKOLEM in HOL Light *)
lemma finite_subset_skolem: ‹finite u ⟹ u ⊆ {skolem φ |φ. φ ∈ s} ⟹
  (∃t. finite t ∧ t ⊆ s ∧ u = {skolem φ |φ. φ ∈ t})›
proof (induction u rule: finite.induct)
  case emptyI
  then show ?case by auto
next
  case (insertI A a)
  obtain φa where phi_in: ‹φa ∈ s› and phi_ex_subs: ‹a = skolem φa›
    using insertI(3) by auto
  obtain Φ where Phi_subs: ‹Φ ⊆ s› and ‹finite Φ› and Phi_set: ‹A = {skolem φ |φ. φ ∈ Φ}›
    using insertI(3) insertI(2) by auto
  then have ‹finite (φa ▹ Φ)›
    by auto
  moreover have ‹(φa ▹ Φ) ⊆ s›
    using phi_in Phi_subs by auto
  moreover have ‹a ▹ A = {skolem φ |φ. φ ∈ (φa ▹ Φ)}›
    using phi_ex_subs Phi_set by blast
  ultimately show ?case
    by blast
qed

(* VALUATION_EXISTS in HOL Light *)
lemma valuation_exists: ‹¬ (dom M = {}) ⟹ ∃β. is_valuation M β›
  unfolding dom_def is_valuation_def by fast

(* HOLDS_ITLIST_EXISTS in HOL Light *)
lemma holds_itlist_exists: 
  ‹(M❙,β ⊨ (foldr (λx p. ❙∃x❙. p) xs φ)) ⟷ 
     (∃as. length as = length xs ∧ set as ⊆ dom M ∧ 
           (M❙,(foldr (λu β. β(fst u := snd u)) (rev (zip xs as)) β) ⊨ φ))›
proof (induction xs arbitrary: β φ)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  show ?case
    by (force simp add: Cons length_Suc_conv simp flip: fun_upd_def)
qed

definition canonical :: ‹(nat × nat) set × (nat × nat) set ⇒ nterm intrp ⇒ bool› where
‹canonical ℒ ℳ ≡ (dom ℳ = terms_set (fst ℒ) ∧ (∀f. intrp_fn ℳ f = Fun f))›

(* Slight deviation from the HOL Light definition where "Atom p ts" appears on the left, which is
   forbidden in Isabelle, I don't see how to define it only for atoms and obtain a propositional
   interpretation: *)
(* prop_of_model in HOL Light *)
definition pintrp_of_intrp :: ‹'m intrp ⇒ (nat ⇒ 'm) ⇒ (form ⇒ bool)› where
  ‹pintrp_of_intrp ℳ β = (λφ. ℳ❙,β ⊨ φ)›

(* the predicates are not defined exactly in the same way here and in HOL Light, 
   I replaced the predicate d with the set of all valid atoms and the function returns the list
   of accepted arguments for a given predicate instead of being a Boolean for compatibility.
*)
definition 
  canon_of_prop :: ‹((nat × nat) set × (nat × nat) set) ⇒ (form ⇒ bool) ⇒ nterm intrp› where
  ‹canon_of_prop ℒ I ≡ Abs_intrp (terms_set (fst ℒ), Fun, (λp. {ts. I (Atom p ts)}))›

lemma dom_canon_of_prop [simp]: ‹dom (canon_of_prop ℒ I) = terms_set (fst ℒ)›
  by (simp add: canon_of_prop_def)

lemma intrp_fn_canon_of_prop [simp]: ‹intrp_fn (canon_of_prop ℒ I) = Fun›
  by (simp add: canon_of_prop_def)

lemma intrp_rel_canon_of_prop [simp]: ‹intrp_rel (canon_of_prop ℒ I) = (λp. {ts. I (Atom p ts)})›
  by (simp add: canon_of_prop_def)

lemma pholds_pintrp_of_intrp:
  ‹qfree φ ⟹ (pintrp_of_intrp ℳ β) ⊨⇩p φ ⟷ ℳ❙,β ⊨ φ›
  unfolding pintrp_of_intrp_def by (induction φ) simp+

(* PROP_OF_CANON_OF_PROP in HOL Light *)
lemma intrp_of_canon_of_prop [simp]:
  ‹pintrp_of_intrp (canon_of_prop ℒ I) Var (Atom p ts) = I (Atom p ts)›
proof -
  have §: ‹terms_set (fst ℒ) ≠ {}›
    using terms_set.vars by auto
  have ‹∀t ∈ set ts. ⟦t⟧⇗Abs_intrp (terms_set (fst ℒ), Fun, λp. {ts. I (form.Atom p ts)}),Var⇖ = t› 
  proof (induction ts)
    case Nil
    then show ?case by simp
  next
    case (Cons t ts)
    have ‹⟦t⟧⇗Abs_intrp (terms_set (fst ℒ), Fun, λp. {ts. I (form.Atom p ts)}),Var⇖ = t›
    proof (induction t)
      case (Var x)
      then show ?case
        by simp
    next
      case Fun
      then show ?case
        by (simp add: § struct_def map_idI)
    qed
    with Cons show ?case
      by simp
  qed
  then show ?thesis
    by (simp add: § struct_def canon_of_prop_def pintrp_of_intrp_def holds_def map_idI)
qed

(* HOLDS_CANON_OF_PROP in HOL Light *)
lemma holds_canon_of_prop:
  assumes ‹qfree φ› shows ‹(canon_of_prop ℒ I)❙,Var ⊨ φ ⟷ I ⊨⇩p φ›
proof -
  have ‹pintrp_of_intrp (canon_of_prop ℒ I) Var ⊨⇩p φ ⟷ I ⊨⇩p φ›
    using assms
    by (induction φ) auto
  with assms show ?thesis
    using pholds_pintrp_of_intrp by blast
qed

(* HOLDS_CANON_OF_PROP_GENERAL in HOL Light *)
(* It is strange to apply a valuation to a formula anyway, it is a kind of misuse of the fact that 
    valuations for canonical models and substitutions have the same type *)
lemma holds_canon_of_prop_general: 
  assumes ‹qfree φ› shows ‹(canon_of_prop ℒ I)❙,β ⊨ φ ⟷ I ⊨⇩p (φ ⋅⇩f⇩m β)›
proof -
  have ‹pintrp_of_intrp (canon_of_prop ℒ I) β ⊨⇩p φ ⟷ I ⊨⇩p (φ ⋅⇩f⇩m β)›
    using assms
  proof (induction φ)
    case Atom
    have ‹⟦t⟧⇗Abs_intrp (terms_set (fst ℒ), Fun, λp. {ts. I (form.Atom p ts)}),β⇖ = t ⋅ β› for t
      using term_subst_eval by (metis empty_iff intrp_fn_Abs_is_fst_snd struct_def terms_set.simps)
    moreover have ‹struct (terms_set (fst ℒ))›
      by (metis empty_iff struct.intro terms_set.vars)
    ultimately show ?case
      by (simp add: canon_of_prop_def pintrp_of_intrp_def Atom)
  qed auto
  with assms show ?thesis
    by (simp add: pholds_pintrp_of_intrp)
qed

(* CANONICAL_CANON_OF_PROP in HOL Light *)
lemma canonical_canon_of_prop: ‹canonical ℒ (canon_of_prop ℒ I)›
  unfolding canonical_def canon_of_prop_def
  by (metis dom_Abs_is_fst emptyE intrp_fn_Abs_is_fst_snd struct_def terms_set.vars)

(* INTERPRETATION_CANON_OF_PROP in hol-ligh *)
lemma interpretation_canon_of_prop: ‹is_interpretation ℒ (canon_of_prop ℒ I)›
  unfolding is_interpretation_def canon_of_prop_def
  by (metis (no_types, lifting) canonical_canon_of_prop canonical_def dom_Abs_is_fst 
      intrp_fn_Abs_is_fst_snd intrp_is_struct subset_code(1) terms_set.fn)

(* PROP_VALID_IMP_FOL_VALID in HOL Light *)
lemma prop_valid_imp_fol_valid: ‹qfree φ ∧ (∀I. I ⊨⇩p φ) ⟹ (∀ℳ β. ℳ❙,β ⊨ φ)›
  using pholds_pintrp_of_intrp by fast

(* FOL_VALID_IMP_PROP_VALID *)
lemma fol_valid_imp_prop_valid: ‹qfree φ ∧ (∀ℳ β. canonical (language {φ}) ℳ ⟶ ℳ❙,β ⊨ φ)
  ⟹ ∀I. I ⊨⇩p φ›
  using canonical_canon_of_prop holds_canon_of_prop by blast

(* SATISFIES_PSATISFIES *)
lemma satisfies_psatisfies: ‹⟦φ ∈ Φ; Φ ⊆ {φ. qfree φ}; satisfies ℳ Φ; is_valuation ℳ β⟧ ⟹
  psatisfies (pintrp_of_intrp ℳ β) Φ›
  using pholds_pintrp_of_intrp satisfies_def by blast

(* PSATISFIES_INSTANCES in HOL Light *)
lemma psatisfies_instances:
  assumes qf: ‹Φ ⊆ {φ. qfree φ}›
    and ps: ‹psatisfies I {φ ⋅⇩f⇩m β |φ β. (∀x. β x ∈ terms_set (fst ℒ)) ∧ φ ∈ Φ}›
  shows ‹satisfies (canon_of_prop ℒ I) Φ›
  unfolding satisfies_def is_valuation_def
  by (smt (verit, best) dom_canon_of_prop holds_canon_of_prop_general mem_Collect_eq ps qf 
      subset_iff)

(* SATISFIES_INSTANCES in HOL Light *)
lemma satisfies_instances:
  assumes ‹is_interpretation (language Ξ) ℳ›
  shows ‹satisfies ℳ {φ ⋅⇩f⇩m σ |φ σ. φ ∈ Φ ∧ (∀x. σ x ∈ terms_set (fst (language Ξ)))} ⟷
         satisfies ℳ Φ›
  unfolding satisfies_def mem_Collect_eq
proof (intro iffI strip)
  fix β φ
  assume ℳ: ‹∀β φ. is_valuation ℳ β ⟶ φ ∈ Φ ⟶ ℳ❙,β ⊨ φ› ‹is_valuation ℳ β›
    and ‹∃φ' σ. φ = φ' ⋅⇩f⇩m σ ∧ φ' ∈ Φ ∧ (∀x. σ x ∈ terms_set (fst (language Ξ)))›
  then obtain φ' σ where σ: ‹φ = φ' ⋅⇩f⇩m σ› ‹φ' ∈ Φ› ‹∀x. σ x ∈ terms_set (functions_forms Ξ)›
    by (auto simp add: language_def)
  with ℳ assms have ‹ℳ❙,(λv. ⟦σ v⟧⇗ℳ,β⇖) ⊨ φ'›
    by (metis (no_types, lifting) eq_fst_iff interpretation_eval interpretation_sublanguage 
        is_valuation_def language_def stupid_canondom)
  with assms show ‹ℳ❙,β ⊨ φ›
    by (simp add: σ swap_subst_eval)
qed (metis subst_var terms_set.vars)

(* COMPACT_CANON_QFREE in HOL Light *)
(* I don't see the point of ‹language Ξ› here instead of, e.g., ℒ *)
lemma compact_canon_qfree:
  assumes qf: ‹Φ ⊆ {φ. qfree φ}›
  and int: ‹⋀Ψ. ⟦finite Ψ; Ψ ⊆ Φ⟧ 
             ⟹ ∃ℳ::'a intrp. is_interpretation (language Ξ) ℳ ∧ dom ℳ ≠ {} ∧ satisfies ℳ Ψ›
  obtains 𝒞 where ‹is_interpretation (language Ξ) 𝒞› ‹canonical (language Ξ) 𝒞› ‹satisfies 𝒞 Φ›
proof -
  define Γ where ‹Γ ≡ λX. {φ ⋅⇩f⇩m β |β φ. (∀x. β x ∈ terms_set (fst (language Ξ))) ∧ φ ∈ X}›
  have ‹psatisfiable (Γ Φ)›
    unfolding psatisfiable_def
  proof (rule compact_prop)
    fix Θ 
    assume ‹finite Θ› ‹Θ ⊆ Γ Φ›
    then have ‹∃Ψ. finite Ψ ∧ Ψ ⊆ Φ ∧ Θ ⊆ Γ Ψ›
      using finite_subset_instance Γ_def by force
    then obtain Ψ where Ψ: ‹finite Ψ› ‹Ψ ⊆ Φ› ‹Θ ⊆ Γ Ψ›
      by auto
    have ‹psatisfiable Θ›
    proof (rule psatisfiable_mono)
      obtain ℳ::‹'a intrp› where ℳ: ‹is_interpretation (language Ξ) ℳ› ‹dom ℳ ≠ {}›
        ‹satisfies ℳ Ψ›
        using int Ψ by meson
      then obtain β where β: ‹is_valuation ℳ β›
        by (meson valuation_exists)
      moreover have ‹Γ Ψ ⊆ {φ. qfree φ}›
        using Γ_def Ψ qf qfree_formsubst by auto
      moreover have ‹satisfies ℳ (Γ Ψ)›
        using ℳ unfolding Γ_def
        by (smt (verit, del_insts) mem_Collect_eq satisfies_def satisfies_instances)
      ultimately show ‹psatisfiable (Γ Ψ)›
        by (meson psatisfiable_def satisfies_psatisfies)
    qed (use Ψ in auto)
    then show ‹∃I. psatisfies I Θ›
      using psatisfiable_def by blast
  qed (use qf qfree_formsubst Γ_def in force)
  with qf that show thesis
    unfolding Γ_def psatisfiable_def
    by (smt (verit, ccfv_threshold) canonical_canon_of_prop interpretation_canon_of_prop 
        mem_Collect_eq psatisfies_instances)
qed

(* INTERPRETATION_RESTRICTLANGUAGE in HOL Light *)
lemma interpretation_restrictlanguage: 
  ‹Ψ ⊆ Φ ⟹ is_interpretation (language Φ) ℳ ⟹ is_interpretation (language Ψ) ℳ›
  unfolding is_interpretation_def language_def functions_forms_def predicates_def
  by (metis Union_mono fstI image_mono in_mono)

(* INTERPRETATION_EXTENDLANGUAGE in HOL Light *)
lemma interpretation_extendlanguage: 
  fixes ℳ:: ‹'a intrp›
  assumes int: ‹is_interpretation (language Ψ) ℳ› and ‹dom ℳ ≠ {}›
    and ‹satisfies ℳ Ψ›
  obtains 𝒩 where ‹dom 𝒩 = dom ℳ› ‹intrp_rel 𝒩 = intrp_rel ℳ› 
                    ‹is_interpretation (language Φ) 𝒩› ‹satisfies 𝒩 Ψ›
proof
  define m where ‹m ≡ (SOME a. a ∈ dom ℳ)›
  have m: ‹m ∈ dom ℳ›
    by (simp add: ‹dom ℳ ≠ {}› m_def some_in_eq)
  define 𝒩 where ‹𝒩 ≡ Abs_intrp
                    (dom ℳ, 
                     (λg zs. if (g,length zs) ∈ functions_forms Ψ then intrp_fn ℳ g zs else m),
                     intrp_rel ℳ)›
  show eq: ‹dom 𝒩 = dom ℳ› ‹intrp_rel 𝒩 = intrp_rel ℳ›
    by (simp_all add: 𝒩_def)
  show ‹is_interpretation (language Φ) 𝒩›
  proof -
    have §: ‹fst (language Ψ) = functions_forms Ψ›
      by (simp add: language_def)
    obtain β where ‹is_valuation ℳ (β ℳ)›
      by (meson ‹dom ℳ ≠ {}› valuation_exists)
    then have ‹∀n. β ℳ n ∈ dom ℳ›
      using is_valuation_def by blast
    with eq m int show ?thesis
      unfolding 𝒩_def is_interpretation_def
      by (smt (verit, ccfv_SIG) § intrp_fn_Abs_is_fst_snd intrp_is_struct)
  qed
  show ‹satisfies 𝒩 Ψ›
    unfolding satisfies_def
  proof (intro strip)
    fix β φ
    assume β: ‹is_valuation 𝒩 β› and ‹φ ∈ Ψ›
    then have ‹is_valuation ℳ β›
      by (simp add: eq is_valuation_def)
    then have ‹ℳ❙,β ⊨ φ›
      using ‹φ ∈ Ψ› ‹satisfies ℳ Ψ› by (simp add: satisfies_def)
    moreover
    have ‹(𝒩❙,β ⊨ φ) ⟷ (ℳ❙,β ⊨ φ)›
    proof (intro holds_cong)
      fix f :: nat and ts :: ‹'a list›
      assume ‹(f, length ts) ∈ functions_form φ›
      then show ‹intrp_fn 𝒩 f ts = intrp_fn ℳ f ts›
        using 𝒩_def ‹φ ∈ Ψ› functions_forms_def by auto
    qed (auto simp: eq)
    ultimately show ‹𝒩❙,β ⊨ φ› by auto
  qed
qed

(* COMPACT_LS in HOL Light *)
theorem compact_ls:
  assumes ‹⋀Ψ. ⟦finite Ψ; Ψ ⊆ Φ⟧ 
             ⟹ ∃ℳ::'a intrp. is_interpretation (language Φ) ℳ ∧ dom ℳ ≠ {} ∧ satisfies ℳ Ψ›
  obtains 𝒞::‹nterm intrp› where ‹is_interpretation (language Φ) 𝒞› ‹dom 𝒞 ≠ {}› ‹satisfies 𝒞 Φ›
proof -
  have ‹∃ℳ::'a intrp. is_interpretation(language (skolem ` Φ)) ℳ ∧
                dom ℳ ≠ {} ∧ satisfies ℳ Ψ› 
    if Ψ: ‹finite Ψ› ‹Ψ ⊆ skolem ` Φ› for Ψ
    by (smt (verit, ccfv_threshold) assms finite_subset_image interpretation_extendlanguage 
             interpretation_restrictlanguage skolem_satisfiable that)
  with compact_canon_qfree skolem_qfree
  obtain 𝒞 where 𝒞: ‹is_interpretation (language (skolem ` Φ)) 𝒞› 
    ‹canonical (language (skolem ` Φ)) 𝒞› 
    ‹satisfies 𝒞 (skolem ` Φ)›
    by blast
  have ‹dom 𝒞 ≠ {}›
    using struct_def by blast
  with skolem_satisfiable[of Φ] 𝒞 that show thesis
    by metis
qed

(* CANON in HOL Light *)
lemma canon:
  assumes ‹is_interpretation (language Φ) ℳ› ‹dom ℳ ≠ {}› ‹satisfies ℳ Φ›
  obtains 𝒞::‹nterm intrp› where ‹is_interpretation (language Φ) 𝒞› ‹dom 𝒞 ≠ {}› ‹satisfies 𝒞 Φ›
  using compact_ls assms unfolding satisfies_def by blast

(* LOWMOD in HOL Light *)
definition lowmod :: ‹nterm intrp ⇒ nat intrp› where
  ‹lowmod ℳ ≡ Abs_intrp (num_of_term ` (dom ℳ), 
    (λg ns. num_of_term (intrp_fn ℳ g (map term_of_num ns))), 
    (λp. {ns. (map term_of_num ns) ∈ intrp_rel ℳ p}))›

lemma dom_lowmod [simp]: ‹dom (lowmod ℳ) = num_of_term ` (dom ℳ)›
  by (metis (no_types, lifting) dom_Abs_is_fst image_is_empty intrp_is_struct lowmod_def struct_def)

lemma intrp_fn_lowmod [simp]: ‹intrp_fn (lowmod ℳ) f ns = num_of_term (intrp_fn ℳ f (map term_of_num ns))›
  by (metis dom_lowmod intrp_fn_Abs_is_fst_snd intrp_is_struct lowmod_def)

lemma intrp_rel_lowmod [simp]: ‹intrp_rel (lowmod ℳ) p = {ns. (map term_of_num ns) ∈ intrp_rel ℳ p}›
  by (metis (no_types, lifting) dom_lowmod intrp_is_struct intrp_rel_Abs_is_snd_snd lowmod_def)

lemma is_valuation_lowmod: ‹is_valuation (lowmod 𝒞) (num_of_term ∘ β) ⟷ is_valuation 𝒞 β›
  by (simp add: is_valuation_def image_iff num_of_term_inj)

(* LOWMOD_DOM_EMPTY in HOL Light *)
lemma lowmod_dom_empty: ‹dom (lowmod ℳ) = {} ⟷ dom ℳ = {}›
  by simp

(* LOWMOD_TERMVAL in HOL Light *)
lemma lowmod_termval: 
  assumes ‹is_valuation (lowmod ℳ) β›
  shows ‹eval t (lowmod ℳ) β = num_of_term (eval t ℳ (term_of_num ∘ β))›
proof (induction t)
  case (Var x)
  then show ?case 
    using assms unfolding is_valuation_def
    by (metis (no_types, lifting) comp_apply dom_lowmod eval.simps(1) image_iff term_of_num_of_term)
next
  case (Fun f args)
  then show ?case
    using assms unfolding is_valuation_def comp_apply intrp_fn_lowmod eval.simps
    by (smt (verit) concat_map map_eq_conv term_of_num_of_term)
qed

(* LOWMOD_HOLDS in HOL Light *)
lemma lowmod_holds:
  assumes ‹is_valuation (lowmod ℳ) β›
  shows  ‹(lowmod ℳ)❙,β ⊨ φ ⟷ ℳ❙,(term_of_num ∘ β) ⊨ φ›
  using assms
proof (induction φ arbitrary: β)
  case (Atom x1 x2)
  then show ?case
    using lowmod_termval [OF Atom] by (simp add: comp_def)
next
  case (Forall x1 φ)
  then have ‹⋀a. a ∈ dom ℳ ⟹ is_valuation (lowmod ℳ) (β(x1 := num_of_term a))›
    by (simp add: valuation_valmod)
  with Forall show ?case
    apply simp
    by (smt (verit, best) fun_upd_apply holds_indep_β_if term_of_num_of_term)
qed auto

(* LOWMOD_INTERPRETATION in HOL Light *)
lemma lowmod_intrp: ‹is_interpretation ℒ (lowmod ℳ) = is_interpretation ℒ ℳ›
proof
  have inj: ‹inj num_of_term›
    by (meson injI num_of_term_inj)
  show ‹is_interpretation ℒ (lowmod ℳ) ⟹ is_interpretation ℒ ℳ›
    unfolding is_interpretation_def dom_lowmod intrp_fn_lowmod inj_image_mem_iff [OF inj]
    by (metis (no_types, lifting) concat_map image_mono image_set length_map map_idI term_of_num_of_term)
  show ‹is_interpretation ℒ ℳ ⟹ is_interpretation ℒ (lowmod ℳ)›
    unfolding is_interpretation_def dom_lowmod intrp_fn_lowmod subset_iff
    by (smt (verit, best) image_iff length_map list.set_map term_of_num_of_term)
qed

(* LS in HOL Light *)
lemma loewenheim_skolem: 
  assumes ‹is_interpretation (language Φ) ℳ› ‹dom ℳ ≠ {}› 
  assumes ‹⋀φ. φ ∈ Φ ⟹ qfree φ› ‹satisfies ℳ Φ›
  obtains 𝒩 :: ‹nat intrp› where ‹is_interpretation (language Φ) 𝒩› ‹dom 𝒩 ≠ {}› ‹satisfies 𝒩 Φ›
proof -
  obtain 𝒞::‹nterm intrp› where 𝒞: ‹is_interpretation (language Φ) 𝒞› ‹dom 𝒞 ≠ {}› ‹satisfies 𝒞 Φ›
    using assms canon by blast
  show ?thesis
  proof
    show ‹is_interpretation (language Φ) (lowmod 𝒞)›
      by (simp add: 𝒞 lowmod_intrp)
    show ‹dom (lowmod 𝒞) ≠ {}›
      by (simp add: 𝒞)
    show ‹satisfies (lowmod 𝒞) Φ›
      using 𝒞 unfolding satisfies_def
      by (smt (verit, ccfv_SIG) comp_apply dom_lowmod image_iff is_valuation_def lowmod_holds term_of_num_of_term)
  qed
qed

(* UNIFORMITY in HOL Light *)
theorem uniformity:
  assumes ‹qfree φ› 
          ‹⋀𝒞::nterm intrp. ⋀β. ⟦dom 𝒞 ≠ {}; is_valuation 𝒞 β⟧ ⟹ 𝒞❙,β ⊨ foldr Exists xs φ›
  obtains σs where ‹⋀σ x. σ ∈ set σs ⟹ σ x ∈ terms_set (fst (language {φ}))›
                   ‹⋀I. I ⊨⇩p (foldr (λφ ψ. φ ❙∨ ψ) (map (λσ. φ ⋅⇩f⇩m σ) σs) ❙⊥)›
proof -
  define A where ‹A ≡ formsubst φ ` {σ. ∀x. σ x ∈ terms_set (fst (language {φ}))}›
  have ‹∃φ' ∈ A. I ⊨⇩p φ'› for I
  proof -
    have *: False if ‹satisfies (canon_of_prop (language {φ}) I) {❙¬ φ}›
    proof -
      obtain β where β: ‹is_valuation (canon_of_prop (language {φ}) I) β›
        by (metis struct_def valuation_exists intrp_is_struct)
      then have ‹canon_of_prop (language {φ}) I❙, β ⊨ foldr Exists xs φ›
        using assms struct_def by fastforce
      then obtain as where len: ‹length as = length xs› 
             and sub: ‹set as ⊆ terms_set (fst (language {φ}))›
             and sat0: ‹canon_of_prop (language {φ}) I❙, 
                       foldr (λu β. β(fst u := snd u)) (rev (zip xs as)) β ⊨ φ›
        by (force simp add: holds_itlist_exists)
      define F where ‹F ≡ λas::nterm list. λxs::nat list. foldr (λu β. β(fst u := snd u)) (rev (zip xs as))›
      have F_Cons: ‹F (a#as) (x#xs) β = F as xs ((β(x := a)))› for a as x xs β
        by (simp add: F_def)
      have sat: ‹canon_of_prop (language {φ}) I❙, F as xs β ⊨ φ›
        using sat0 by (simp add: F_def)
      have ‹⟦length as = length xs;
             set as ⊆ dom (canon_of_prop (language {φ}) I);
             is_valuation (canon_of_prop (language {φ}) I) β⟧
            ⟹ is_valuation (canon_of_prop (language {φ}) I) (F as xs β)›
        for xs as
      proof (induction xs arbitrary: as β)
        case Nil
        then show ?case
          by (simp add: F_def is_valuation_def)
      next
        case (Cons x xs as β)
        then obtain a as' where aas': ‹as = a#as'› ‹length as' = length xs›
          by (metis length_Suc_conv)
        with Cons show ?case
          by (simp add: is_valuation_def aas' F_Cons)
      qed
      then have ‹is_valuation (canon_of_prop (language {φ}) I) (F as xs β)›
        by (metis (no_types, lifting) β dom_canon_of_prop len sub)
      then show ?thesis
        using sat satisfies_def that by (force simp: F_def)
    qed
    then show ?thesis
      using psatisfies_instances [of concl: ‹language {φ}› I ‹{❙¬ φ}›] ‹qfree φ›
      by (force simp: A_def)
  qed
  then obtain Φ where Φ: ‹set Φ ⊆ A› ‹⋀I. I ⊨⇩p foldr (❙∨) Φ ❙⊥›
    by (smt (verit, ccfv_threshold) A_def assms(1) compact_disj image_iff qfree_formsubst)
  show thesis
  proof
    define sf where ‹sf ≡ λq. @σ. (∀i. σ i ∈ terms_set (fst (language {φ}))) ∧ q = φ ⋅⇩f⇩m σ›
    have sf_works: ‹(∀i. sf a i ∈ terms_set (fst (language {φ}))) ∧ a = φ ⋅⇩f⇩m (sf a)›
      if ‹a ∈ A› for a
      using that unfolding A_def sf_def image_iff Bex_def mem_Collect_eq
      by (rule someI_ex)
    show ‹σ i ∈ terms_set (fst (language {φ}))›
      if ‹σ ∈ set (map sf Φ)› for σ i
    proof -
      have *: ‹set Θ ⊆ A ⟹  σ ∈ set (map sf Θ) ⟹ σ i ∈ terms_set (fst (language {φ}))› for Θ
        by (induction Θ) (auto simp: sf_works)
      then show ?thesis
        using Φ that by fastforce
    qed
    show ‹I ⊨⇩p foldr (❙∨) (map ((⋅⇩f⇩m) φ) (map sf Φ)) ❙⊥› for I
      using Φ(2) [of I] Φ(1)
    by (induction Φ) (use sf_works in force)+
  qed
qed

end