Theory U

section‹Untyped (Unsorted) First-Order Logic›
theory U
imports TermsAndClauses
begin

text‹Even though untyped FOL is a particular case of many-typed FOL, we find 
it convenient to represent it separately.›

subsection ‹Signatures›

locale Signature =
fixes
    wtFsym :: "'fsym ⇒ bool"
and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ nat"
and parOf :: "'psym ⇒ nat"
assumes countable_wtFsym: "countable {f::'fsym. wtFsym f}"
and countable_wtPsym: "countable {p::'psym. wtPsym p}"
begin

(* Well-typed terms *)
fun wt where
"wt (Var x) ⟷ True"
|
"wt (Fn f Tl) ⟷ wtFsym f ∧ list_all wt Tl ∧ arOf f = length Tl"

lemma wt_induct[elim, consumes 1, case_names Var Fn, induct pred: wt]:
assumes T: "wt T"
and Var: "⋀ x. φ (Var x)"
and Fn:
"⋀ f Tl.
   ⟦wtFsym f; list_all wt Tl; arOf f = length Tl; list_all φ Tl⟧
 ⟹ φ (Fn f Tl)"
shows "φ T"
proof-
  have "wt T ⟶ φ T"
  apply (induct T) using Var Fn by (auto simp: list_all_iff)
  thus ?thesis using T by auto
qed

(* Well-typed substitutions *)
definition "wtSB π ≡ ∀ x. wt (π x)"

lemma wtSB_wt[simp]: "wtSB π ⟹ wt (π x)"
unfolding wtSB_def by auto

lemma wt_subst[simp]:
assumes "wtSB π" and "wt T"
shows "wt (subst π T)"
using assms by (induct T) (auto simp: list_all_length)


lemma wtSB_o:
assumes 1: "wtSB π1" and 2: "wtSB π2"
shows "wtSB (subst π1 o π2)"
using 2 unfolding wtSB_def using 1 by auto


end (* context Signature *)


subsection ‹Structures›

(* Environment *)
type_synonym 'univ env = "var ⇒ 'univ"

(* Structure *)
locale Struct = Signature wtFsym wtPsym arOf parOf
for wtFsym and wtPsym
and arOf :: "'fsym ⇒ nat"
and parOf :: "'psym ⇒ nat"
+
fixes
    D :: "'univ ⇒ bool"
and intF :: "'fsym ⇒ 'univ list ⇒ 'univ"
and intP :: "'psym ⇒ 'univ list ⇒ bool"
assumes
NE_D: "NE D" and
intF: "⟦wtFsym f; length al = arOf f; list_all D al⟧ ⟹ D (intF f al)"
and
dummy: "parOf = parOf ∧ intF = intF ∧ intP = intP"
begin

(* Well-typed environment *)
definition "wtE ξ ≡ ∀ x. D (ξ x)"

lemma wtTE_D[simp]: "wtE ξ ⟹ D (ξ x)"
unfolding wtE_def by simp

(* Interpretation of terms: *)
fun int where
"int ξ (Var x) = ξ x"
|
"int ξ (Fn f Tl) = intF f (map (int ξ) Tl)"

(* Soundness of typing w.r.t. interpretation: *)
lemma wt_int:
assumes wtE: "wtE ξ" and wt_T: "wt T"
shows "D (int ξ T)"
using wt_T apply(induct T)
apply (metis int.simps(1) wtE wtE_def)
unfolding int.simps apply(rule intF)
unfolding list_all_map comp_def by auto

lemma int_cong:
assumes "⋀x. x ∈ vars T ⟹ ξ1 x = ξ2 x"
shows "int ξ1 T = int ξ2 T"
using assms apply(induct T) apply simp_all unfolding list_all_iff
using map_ext by metis

lemma int_o:
"int (int ξ o ρ) T = int ξ (subst ρ T)"
apply(induct T) apply simp_all  unfolding list_all_iff o_def 
using map_ext by (metis (lifting, no_types))

lemmas int_subst = int_o[symmetric]

lemma int_o_subst:
"int ξ o subst ρ = int (int ξ o ρ)"
apply(rule ext) apply(subst comp_def) unfolding int_o[symmetric] ..

lemma wtE_o:
assumes 1: "wtE ξ" and 2: "wtSB ρ"
shows "wtE (int ξ o ρ)"
unfolding wtE_def apply safe
unfolding comp_def apply(rule wt_int[OF 1]) using 2 by auto

end


context Signature begin

text‹Well-typed (i.e., well-formed) atoms, literals, caluses and problems:›

fun wtA where
"wtA (Eq T1 T2) ⟷ wt T1 ∧ wt T2"
|
"wtA (Pr p Tl) ⟷ wtPsym p ∧ list_all wt Tl ∧ parOf p = length Tl"

fun wtL where
"wtL (Pos a) ⟷ wtA a"
|
"wtL (Neg a) ⟷ wtA a"

definition "wtC ≡ list_all wtL"

definition "wtPB Φ ≡ ∀ c ∈ Φ. wtC c"

end (* context Signature *)


context Struct begin

(* Satisfaction of atoms: *)
fun satA where
"satA ξ (Eq T1 T2) ⟷ int ξ T1 = int ξ T2"
|
"satA ξ (Pr r Tl) ⟷ intP r (map (int ξ) Tl)"

(* Satisfaction literals: *)
fun satL where
"satL ξ (Pos a) ⟷ satA ξ a"
|
"satL ξ (Neg a) ⟷ ¬ satA ξ a"

(* Satisfaction of clauses: *)
definition "satC ξ ≡ list_ex (satL ξ)"

(* satisfaction of problems *)
definition "satPB ξ Φ ≡ ∀ c ∈ Φ. satC ξ c"

definition "SAT Φ ≡ ∀ ξ. wtE ξ ⟶ satPB ξ Φ"

end (* context Struct *)


subsection‹Problems›

locale Problem = Signature wtFsym wtPsym arOf parOf
for wtFsym and wtPsym
and arOf :: "'fsym ⇒ nat"
and parOf :: "'psym ⇒ nat"
+
fixes Φ :: "('fsym, 'psym) prob"
assumes wt_Φ: "wtPB Φ"


subsection‹Models of a problem›

locale Model =
  Problem wtFsym wtPsym arOf parOf Φ +
  Struct wtFsym wtPsym arOf parOf D intF intP
for wtFsym and wtPsym
and arOf :: "'fsym ⇒ nat"
and parOf :: "'psym ⇒ nat"
and Φ :: "('fsym, 'psym) prob"
and D :: "'univ ⇒ bool"
and intF :: "'fsym ⇒ 'univ list ⇒ 'univ"
and intP :: "'psym ⇒ 'univ list ⇒ bool"
+
assumes SAT: "SAT Φ"


end