Auxiliary Theorems for the Core Chase

We introduce a few auxiliary theorems on GroundTermMappings and cores here. Most notably, we prove that every finite set has a weak core. Eventually, these theorems should move to more appropriate places.

theorem GroundTermMapping.applyFact_eq_self_of_isIdOnConstants_of_isFunctionFree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {h : GroundTermMapping sig} (idOnConst : h.isIdOnConstants) {f : Fact sig} : f.isFunctionFree → h.applyFact f = f

Applying a mapping that is the id on all constants on a function free fact does not change the fact as it only contains constants.

theorem GroundTermMapping.isHomomorphism_id_of_subset {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {A B : FactSet sig} (sub : A ⊆ B) : isHomomorphism id A B

For two sets in a subset relation, the id mapping is always a homomorphism from the subset to its superset.

theorem FactSet.homSubset_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {fs : FactSet sig} : fs.homSubset fs

The homSubset relation is reflexive.

theorem FactSet.homSubset_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {A B C : FactSet sig} : A.homSubset B → B.homSubset C → A.homSubset C

The homSubset relation is transitive.

theorem FactSet.isWeakCore_empty {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : ∅.isWeakCore

The empty fact set is a weak core.

theorem FactSet.isWeakCore_list_of_each_homSubset_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {l : List (Fact sig)} : (∀ (sub : List (Fact sig)), homSubset (CustomBasicDatastructures.List.toSet sub) (CustomBasicDatastructures.List.toSet l) → CustomBasicDatastructures.List.toSet sub = CustomBasicDatastructures.List.toSet l) → isWeakCore (CustomBasicDatastructures.List.toSet l)

If a list has no proper homomorphic sublist, then the list forms a weak core.

theorem FactSet.exists_weak_core_for_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (l : List (Fact sig)) : ∃ (wc : FactSet sig), wc.isWeakCore ∧ wc.homSubset (CustomBasicDatastructures.List.toSet l)

Every list has a weak core. I.e. it is either itself a weak core or has a proper homomorphic sublist that is a weak core.

theorem FactSet.exists_weak_core_for_set_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {fs : FactSet sig} (fin : CustomBasicDatastructures.Set.finite fs) : ∃ (wc : FactSet sig), wc.isWeakCore ∧ wc.homSubset fs

Each finite fact set has a weak core.

theorem Database.isWeakCore {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (db : Database sig) : db.toFactSet.val.isWeakCore

Each Database is a weak core.