Chase Tree Result is Universal Model Set

This whole file is dedicated to showing that the result of a ChaseTree is a universal model set [BMMP16]. More precisely, we want to show the universality part as we have already shown in ChaseTree.result_models_kb that each element of the result is a model. So what exactly remains to be shown?

We aim to show that for a given ChaseTree for a KnowledgeBase and any model $M$ of the KnowledgeBase, we can pick a fact set $F$ from the result of the chase tree such that there is a homomorphism from $F$ to $M$. This result is shown in chaseTreeResultIsUniversal.

The proof works by step-wise construction of both a branch in the chase tree as well as a suitable homomorphism. The constructions builds both at the same time. One step of the construction is done by the hom_step function below, which calls hom_step_of_trg_ex for the heavy lifting. The base of the construction is simply an empty branch and the id mapping. In each step of the construction, we consider an InductiveHomomorphismResult, which we define to be a pair of a node in the chase tree and a GroundTermMapping such that the mapping is a homomorphism from the node into the model $M$.

In the proof of chaseTreeResultIsUniversal, we leverage the TreeDerivation.generate_subderivation function with hom_step as the generator function. Besides that, all the homomorphisms from the individual steps need to be combined into a single function. The definition is not too hard and all relevant properties are also not too hard to show once we can establish that the homomorphisms for each step always extend the previous one.

theorem chaseTreeResultIsUniversal {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} (ct : ChaseTree obs kb) (m : FactSet sig) : m.modelsKb kb → ∃ (fs : FactSet sig), ∃ (h : GroundTermMapping sig), fs ∈ ct.result ∧ h.isHomomorphism fs m

As outlined at the very top of this file, we now use TreeDerivation.generate_subderivation with the hom_step generator to obtain the branch in the tree that yields the result FactSet for which the combined GroundTermMappings form a homomorphism into the target model.