Theory Ground_FOL_Compactness

(* 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 Ground_FOL_Compactness  
imports
    FOL_Semantics
begin


fun qfree :: ‹form ⇒ bool› where
  ‹qfree ❙⊥ = True›
| ‹qfree (Atom p ts) = True›
| ‹qfree (φ ❙⟶ ψ) = (qfree φ ∧ qfree ψ)›
| ‹qfree (❙∀ x❙. φ) = False›

lemma qfree_iff_BV_empty: "qfree φ ⟷ BV φ = {}"
  by (induction φ) auto

lemma qfree_no_quantif: ‹qfree r ⟹ ¬(∃x p. r = ❙∀x❙. p) ∧ ¬(∃x p. r = ❙∃x❙. p)›
  using qfree.simps(3) qfree.simps(4) by blast

lemma qfree_formsubst: ‹qfree φ ≡ qfree (φ ⋅⇩f⇩m σ)›
proof (induction φ)
  case (Forall x φ)
  then show ?case 
    using formsubst_def_switch by (metis (no_types, lifting) formsubst.simps(4) qfree_no_quantif)
qed simp+

(* != propositional compactness is not proved as in Harrison.
      Instead the existing AFP entry is reused *)

fun form_to_formula :: "form ⇒ (nat×nterm list) formula" where
  ‹form_to_formula ❙⊥ = ⊥›
| ‹form_to_formula (Atom p ts) = formula.Atom (p,ts)›
| ‹form_to_formula (φ ❙⟶ ψ) = Imp (form_to_formula φ) (form_to_formula ψ)›
| ‹form_to_formula (❙∀ x❙. φ) = ⊥›

fun pholds :: ‹(form ⇒ bool) ⇒ form ⇒ bool› (‹_ ⊨⇩p _› [30, 80] 80) where
  ‹I ⊨⇩p ❙⊥ ⟷ False›
| ‹I ⊨⇩p Atom p ts ⟷ I (Atom p ts)›
| ‹I ⊨⇩p φ ❙⟶ ψ ⟷ ((I ⊨⇩p φ) ⟶ (I ⊨⇩p ψ))›
| ‹I ⊨⇩p (❙∀ x❙. φ) ⟷ I (❙∀ x❙. φ)›

definition psatisfiable :: "form set ⇒ bool" where
  ‹psatisfiable S ≡ ∃I. ∀φ∈S. I ⊨⇩p φ›

abbreviation psatisfies where ‹psatisfies I Φ ≡ ∀φ∈Φ. pholds I φ›

definition val_to_prop_val :: "(form ⇒ bool) ⇒ ((nat × nterm list) ⇒ bool)" where
  ‹val_to_prop_val I = (λx. I (Atom (fst x) (snd x)))›

lemma pholds_Not: ‹I ⊨⇩p Not φ ⟷ ¬ (I ⊨⇩p φ)›
  by simp

lemma pentails_equiv: ‹qfree φ ⟹ (I ⊨⇩p φ ≡ (val_to_prop_val I) ⊨ (form_to_formula φ))›
proof (induction φ)
  case Bot
  then show ?case
    unfolding val_to_prop_val_def by simp
next
  case (Atom x1 x2)
  then show ?case
    unfolding val_to_prop_val_def by simp
next
  case (Implies φ1 φ2)
  then have ‹qfree φ1› and ‹qfree φ2› by simp+
  then have ‹I ⊨⇩p φ1 = val_to_prop_val I ⊨ form_to_formula φ1› and
            ‹I ⊨⇩p φ2 = val_to_prop_val I ⊨ form_to_formula φ2›
    using Implies(1) Implies(2) by simp+
  then show ?case by simp
next
  case (Forall x1 φ)
  then have False by simp
  then show ?case by simp
qed

lemma pentails_equiv_set:
  assumes all_qfree: ‹∀φ∈S. qfree φ›
  shows ‹psatisfiable S ≡ sat (form_to_formula ` S)›
proof -
  {
    assume psat_s: ‹psatisfiable S›
    then obtain I where I_is: ‹∀φ∈S. I ⊨⇩p φ›
      unfolding psatisfiable_def by blast
    define 𝒜 where ‹𝒜 = val_to_prop_val I›
    then have ‹∀φ∈S. 𝒜 ⊨ (form_to_formula φ)›
      using pentails_equiv all_qfree I_is by blast
    then have ‹sat (form_to_formula ` S)›
      unfolding sat_def by blast
  }
  moreover {
    assume ‹sat (form_to_formula ` S)›
    then obtain 𝒜 where a_is: ‹∀φ∈S. 𝒜 ⊨ form_to_formula φ›
      by (meson image_eqI sat_def)
    define I where i_is: ‹I = (λx. 𝒜 (pred x, args x))›
    then have ‹𝒜 = val_to_prop_val I›
      unfolding val_to_prop_val_def by simp
    then have ‹∀φ∈S. I ⊨⇩p φ›
      using pentails_equiv all_qfree a_is by blast
    then have ‹psatisfiable S›
      unfolding psatisfiable_def by auto
  }
  ultimately show ‹psatisfiable S ≡ sat (form_to_formula ` S)›
    by argo
qed

definition finsat :: "form set ⇒ bool" where
  ‹finsat S ≡ ∀T⊆S. finite T ⟶ psatisfiable T›

lemma finsat_fin_sat_eq:
  assumes all_qfree: ‹∀φ∈S. qfree φ›
  shows ‹finsat S ⟷ fin_sat (form_to_formula ` S)›
proof 
    assume finsat_s: ‹finsat S›
    then show ‹fin_sat (form_to_formula ` S)›
      unfolding fin_sat_def finsat_def 
      by (metis (no_types, opaque_lifting) assms finite_subset_image pentails_equiv_set subset_eq)
  next
    assume fin_sat_s: ‹fin_sat (form_to_formula ` S)›
    show ‹finsat S›
      unfolding finsat_def
      by (meson assms compactness fin_sat_s pentails_equiv_set psatisfiable_def subsetD)
qed

lemma psatisfiable_mono: ‹psatisfiable S  ⟹ T ⊆ S ⟹ psatisfiable T›
  unfolding psatisfiable_def by blast

lemma finsat_mono: ‹finsat S ⟹ T ⊆ S ⟹ finsat T›
  unfolding finsat_def by blast

lemma finsat_satisfiable: ‹psatisfiable S ⟹ finsat S›
  unfolding psatisfiable_def finsat_def by blast

lemma prop_compactness: ‹(∀φ ∈ S. qfree φ) ⟹ finsat S = psatisfiable S›
  by (simp add: compactness finsat_fin_sat_eq finsat_satisfiable pentails_equiv_set)

text ‹as above, more in the style of HOL Light›
lemma compact_prop:
  assumes ‹⋀B. ⟦finite B; B ⊆ A⟧ ⟹ ∃I. psatisfies I B› and ‹⋀φ. φ ∈ A ⟶ qfree φ›
  shows ‹∃I. psatisfies I A›
  by (metis assms finsat_def prop_compactness psatisfiable_def)

text ‹Three results required for the FOL uniformity theorem›

lemma compact_prop_alt:
  assumes ‹⋀I. ∃φ∈A. I ⊨⇩p φ› ‹⋀φ. φ ∈ A ⟶ qfree φ›
  obtains B where ‹finite B› ‹B ⊆ A› ‹⋀I. ∃φ∈B. I ⊨⇩p φ›
proof -
  have ‹⋀φ. φ ∈ FOL_Syntax.Not ` A ⟶ qfree φ›
    using assms by force
  moreover
  have ‹∄I. psatisfies I (FOL_Syntax.Not ` A)›
    by (simp add: assms) 
  ultimately obtain B where B: ‹finite B› ‹B ⊆ (FOL_Syntax.Not ` A)› ‹⋀I. ∃r∈B. ¬ (I ⊨⇩p r)›
    using compact_prop [of ‹FOL_Syntax.Not ` A›] by fastforce
  show thesis
  proof
    show ‹finite (Not -` B)›
      using form.inject by (metis ‹finite B› finite_vimageI injI)
    show ‹Not -` B ⊆ A›
      using B by auto
    show ‹∃φ ∈ Not -` B. I ⊨⇩p φ› for I
      using B by force
  qed
qed

lemma finite_disj_lemma:
  assumes ‹finite A›
  shows ‹∃Φ. set Φ ⊆ A ∧ (∀I. I ⊨⇩p foldr (❙∨) Φ ❙⊥ ⟷ (∃φ∈A. I ⊨⇩p φ))›
  using assms
proof (induction A)
  case empty
  then show ?case
    by auto
next
  case (insert φ A)
  then obtain Φ where ‹set Φ ⊆ A› ‹∀I. I ⊨⇩p foldr (❙∨) Φ ❙⊥ ⟷ (∃φ∈A. I ⊨⇩p φ)›
    by blast
  then show ?case 
    by (force simp: intro!: exI [where x="φ#Φ"])
qed

lemma compact_disj:
  assumes ‹⋀I. ∃φ∈A. I ⊨⇩p φ› ‹⋀φ. φ ∈ A ⟶ qfree φ›
  obtains Φ where ‹set Φ ⊆ A› ‹⋀I. I ⊨⇩p foldr (❙∨) Φ ❙⊥›
  by (smt (verit, best) assms compact_prop_alt finite_disj_lemma order_trans)

end