Chase Derivation Skeleton

It is time to define the chase [BV84]. We are going to introduce slightly different representations and the ChaseDerivationSkeleton is arguably the most basic but also most versatile one.

We only demand a PossiblyInfiniteList of ChaseNodes that is non-empty such that the next ChaseNode always results from a trigger application. However, we do not care so far if the trigger is active or even loaded. We also do not care here whether the derivation is "fair".

The ChaseDerivation Structure

The backbone of the ChaseDerivationSkeleton is a PossiblyInfiniteList of ChaseNodes with two conditions.

1. We enforce that there is at least an initial ChaseNode.
2. At each step in the derivation, either there exists a trigger that yields the next node or there is no next node.

structure ChaseDerivationSkeleton {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (N : Type u) (obs : ObsolescenceCondition sig) (rules : RuleSet sig) [CN : ChaseNode N obs rules] : Type u

• branch : PossiblyInfiniteList N
• isSome_head : self.branch.head.isSome = true
• triggers_exist (b2 : PossiblyInfiniteList N) : b2 <:+ self.branch → ∀ (before : N), before ∈ b2.head → ∀ (after : N), after ∈ b2.tail.head → ChaseNode.succ before after

Basic Definitions

Here we introduce some auxiliary definitions and theorems and we lift some of the machinery of the underlying PossiblyInfiniteList to ChaseDerivationSkeleton.

@[instance_reducible]

instance ChaseDerivationSkeleton.instMembership {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] : Membership N (ChaseDerivationSkeleton N obs rules)

Membership of ChaseNodes in the ChaseDerivationSkeleton directly corresponds to membership in the PossiblyInfiniteList.

Equations

• ChaseDerivationSkeleton.instMembership = { mem := fun (cd : ChaseDerivationSkeleton N obs rules) (node : N) => node ∈ cd.branch }

theorem ChaseDerivationSkeleton.mem_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {e : N} : e ∈ cd ↔ ∃ (n : Nat), cd.branch.get? n = some e

An element is a member of the derivation iff it occurs at some index in the underlying branch.

def ChaseDerivationSkeleton.derivation_for_branch_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (cd : ChaseDerivationSkeleton N obs rules) (l2 : PossiblyInfiniteList N) (suffix : l2 <:+ cd.branch) (l2_head_some : l2.head.isSome = true) : ChaseDerivationSkeleton N obs rules

Each suffix of the underlying PossiblyInfiniteList is itself a ChaseDerivationSkeleton as long as its head is not none.

Equations

• cd.derivation_for_branch_suffix l2 suffix l2_head_some = { branch := l2, isSome_head := l2_head_some, triggers_exist := ⋯ }

def ChaseDerivationSkeleton.head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (cd : ChaseDerivationSkeleton N obs rules) : N

The head of the ChaseDerivationSkeleton is the initial ChaseNode. We know that this is never none.

Equations

• cd.head = cd.branch.head.get ⋯

theorem ChaseDerivationSkeleton.head_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} : cd.head ∈ cd

The head is a member.

The "next" ChaseNode

For a ChaseDerivationSkeleton derivation, its next node is the ChaseNode immediately following the head. We mainly introduce a couple of theorems here that abstract away the triggers_exist condition from the ChaseDerivationSkeleton definition.

def ChaseDerivationSkeleton.next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (cd : ChaseDerivationSkeleton N obs rules) : Option N

Equations

• cd.next = cd.branch.tail.head

theorem ChaseDerivationSkeleton.next_mem_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} (next : N) : next ∈ cd.next → next ∈ cd

The next node is a member.

theorem ChaseDerivationSkeleton.isSome_origin_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {next : N} (eq : cd.next = some next) : (ChaseNode.origin next).isSome = true

The origin of the next ChaseNode needs to be set.

theorem ChaseDerivationSkeleton.facts_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {next : N} (eq : cd.next = some next) : ChaseNode.ingoingFacts obs rules next = ChaseNode.outgoingFacts obs rules cd.head ∪ (ChaseNode.origin_result next ⋯).toSet

The fact set of the next ChaseNode consists exactly of the facts from head and the result of the trigger that introduces next.

ChaseDerivationSkeleton Suffixes

We define a suffix relation on ChaseDerivationSkeleton simply as the suffix relation of the underlying PossiblyInfiniteList.

@[implicit_reducible]

def ChaseDerivationSkeleton.IsSuffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (cd1 cd2 : ChaseDerivationSkeleton N obs rules) : Prop

Equations

• (cd1 <:+ cd2) = (cd1.branch <:+ cd2.branch)

def ChaseDerivationSkeleton.«term_<:+_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem ChaseDerivationSkeleton.IsSuffix_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd1 cd2 : ChaseDerivationSkeleton N obs rules} : cd1 <:+ cd2 ↔ ∃ (m : Nat), cd2.branch.drop m = cd1.branch

Unfolds the definition of the suffix relation.

theorem ChaseDerivationSkeleton.mem_of_mem_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd1 cd2 : ChaseDerivationSkeleton N obs rules} (suffix : cd1 <:+ cd2) (node : N) : node ∈ cd1 → node ∈ cd2

Members of our suffix are also our members.

theorem ChaseDerivationSkeleton.subderivation_of_node_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {node : N} (node_mem : node ∈ cd) : ∃ (cd2 : ChaseDerivationSkeleton N obs rules), cd2.head = node ∧ cd2 <:+ cd

Each ChaseNode in the ChaseDerivationSkeleton induces a subderivation.

Tail

If next exists, we can drop the first element from the ChaseDerivationSkeleton and obtain a new ChaseDerivationSkeleton, which, inspired by the PossiblyInfiniteList, we call the tail.

def ChaseDerivationSkeleton.tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (cd : ChaseDerivationSkeleton N obs rules) (next_some : cd.next.isSome = true) : ChaseDerivationSkeleton N obs rules

Equations

• cd.tail next_some = cd.derivation_for_branch_suffix cd.branch.tail ⋯ next_some

theorem ChaseDerivationSkeleton.head_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {next_some : cd.next.isSome = true} : some (cd.tail next_some).head = cd.next

The head of the tail is next.

@[simp]

theorem ChaseDerivationSkeleton.head_tail' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {next_some : cd.next.isSome = true} : (cd.tail next_some).head = cd.next.get next_some

The head of the tail is next.

theorem ChaseDerivationSkeleton.next_mem_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {next_some : cd.next.isSome = true} (next : N) : next ∈ cd.next → next ∈ cd.tail next_some

next is a member of the tail.

theorem ChaseDerivationSkeleton.mem_iff_eq_head_or_mem_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {node : N} : node ∈ cd ↔ node = cd.head ∨ ∃ (h : cd.next.isSome = true), node ∈ cd.tail h

A node is a member if and only if it is either the head or it is a member of the tail.

theorem ChaseDerivationSkeleton.suffix_iff_eq_or_suffix_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd1 cd2 : ChaseDerivationSkeleton N obs rules} : cd1 <:+ cd2 ↔ cd1 = cd2 ∨ ∃ (h : cd2.next.isSome = true), cd1 <:+ cd2.tail h

A derivation is a suffix of another if and only if both are the same or the first is a suffix of the second's tail.

Induction Principle for Members

Similar to PossiblyInfiniteList.mem_rec, we define an induction principle to show properties of ChaseNodes in a ChaseDerivationSkeleton. For this, we introduce ChaseDerivationSkeleton.Node as the subtype of ChaseNode that features a membership proof.

@[reducible, inline]

abbrev ChaseDerivationSkeleton.Node {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (cd : ChaseDerivationSkeleton N obs rules) : Type u

Equations

• cd.Node = { node : N // node ∈ cd }

def ChaseDerivationSkeleton.Node.cast_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd cd2 : ChaseDerivationSkeleton N obs rules} (suffix : cd <:+ cd2) (node : cd.Node) : cd2.Node

A Node of our suffix can be cast into our Node type.

Equations

• ChaseDerivationSkeleton.Node.cast_suffix suffix node = ⟨node.val, ⋯⟩

theorem ChaseDerivationSkeleton.mem_rec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {motive : cd.Node → Prop} (head : motive ⟨cd.head, ⋯⟩) (step : ∀ (cd2 : ChaseDerivationSkeleton N obs rules) (suffix : cd2 <:+ cd), motive ⟨cd2.head, ⋯⟩ → ∀ (next : N) (next_mem : next ∈ cd2.next), motive ⟨next, ⋯⟩) (node : cd.Node) : motive node

If we want to show a motive for all nodes in a derivation, it is enough to show the motive for the head and for the next node in each abitrary subderivation where the motive already holds for the head. This can be used with the induction tactic.

theorem ChaseDerivationSkeleton.mem_tail_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {next_some : cd.next.isSome = true} {node : N} : node ∈ cd.tail next_some ↔ ∃ (cd2 : ChaseDerivationSkeleton N obs rules), cd2 <:+ cd ∧ cd2.next = some node

A node is a member of the tail if and only if there is a subderivation where the node is in the next position. Part of this proof uses the induction principle defined above.

Only Finitely many Generated Facts

The generated facts of node in a ChaseDerivationSkeleton are all facts that are not part of the initial fact set. For each node, the set of generated facts is finite since each trigger only introduces finitely many new facts.

def ChaseDerivationSkeleton.generatedFacts {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (cd : ChaseDerivationSkeleton N obs rules) (node : N) : FactSet sig

The generated facts of a chase node are the facts that orruc in the node but not in the initial chase node.

Equations

• cd.generatedFacts node f = (f ∈ ChaseNode.ingoingFacts obs rules node ∧ ¬f ∈ ChaseNode.outgoingFacts obs rules cd.head)

theorem ChaseDerivationSkeleton.generatedFacts_finite_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (out_sub_in : ChaseNode.out_sub_in) {cd : ChaseDerivationSkeleton N obs rules} (start_eq : ChaseNode.ingoingFacts obs rules cd.head = ChaseNode.outgoingFacts obs rules cd.head) {node : N} (mem : node ∈ cd) : Set.finite (cd.generatedFacts node)

The generatedFacts are always finite.

Predecessor Relation

We can define a predecessor relation (≼) on ChaseDerivation.Node. At this point, it does not have many properties. On Proper ChaseDerivations it will be a total order.

def ChaseDerivationSkeleton.predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} (n1 n2 : cd.Node) : Prop

A node $n$ is a predecessor of a node $m$ if there is a subderivation there $n$ is the head and $m$ is an arbitrary member.

Equations

• (n1 ≼ n2) = ∃ (cd2 : ChaseDerivationSkeleton N obs rules), cd2 <:+ cd ∧ cd2.head = n1.val ∧ n2.val ∈ cd2

def ChaseDerivationSkeleton.«term_≼_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem ChaseDerivationSkeleton.predecessor_of_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd cd2 : ChaseDerivationSkeleton N obs rules} {n1 n2 : cd.Node} (suffix : cd <:+ cd2) : n1 ≼ n2 → Node.cast_suffix suffix n1 ≼ Node.cast_suffix suffix n2

The predecessor relation is stable across suffixes. That is, predecessor in our suffix are also predecessor for us. We only need to cast the nodes.

theorem ChaseDerivationSkeleton.predecessor_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {node : cd.Node} : node ≼ node

The predecessor relation is reflexive.

theorem ChaseDerivationSkeleton.predecessor_total {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} (n1 n2 : cd.Node) : n1 ≼ n2 ∨ n2 ≼ n1

The predecessor relation is total.

theorem ChaseDerivationSkeleton.head_prec_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {next : N} (mem : next ∈ cd.next) : ⟨cd.head, ⋯⟩ ≼ ⟨next, ⋯⟩

The head is a predecessor of next.

We also define a strict version of the predecessor relation (≺) in the obvious way.

def ChaseDerivationSkeleton.strict_predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} (n1 n2 : cd.Node) : Prop

A node is a strict predecessor of another if it is a predecessor but not equal.

Equations

• (n1 ≺ n2) = (n1 ≼ n2 ∧ n1 ≠ n2)

def ChaseDerivationSkeleton.«term_≺_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem ChaseDerivationSkeleton.strict_predecessor_of_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd cd2 : ChaseDerivationSkeleton N obs rules} {n1 n2 : cd.Node} (suffix : cd <:+ cd2) : n1 ≺ n2 → Node.cast_suffix suffix n1 ≺ Node.cast_suffix suffix n2

As for the predecessor relation, we can show that the relation is stable across suffixes given that we cast the nodes.

theorem ChaseDerivationSkeleton.strict_predecessor_irreflexive {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {n : cd.Node} : ¬n ≺ n

The strict predecessor relation is irreflexive.

theorem ChaseDerivationSkeleton.strict_predecessor_total {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {n1 n2 : cd.Node} : n1 ≠ n2 → n1 ≺ n2 ∨ n2 ≺ n1

The strict predecessor relation is total.

theorem ChaseDerivationSkeleton.eq_or_strict_of_predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {n1 n2 : cd.Node} : n1 ≼ n2 → n1 = n2 ∨ n1 ≺ n2

A predecessor is either equal or a strict predecessor.

theorem ChaseDerivationSkeleton.next_prec_of_head_strict_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {cd : ChaseDerivationSkeleton N obs rules} {node : cd.Node} : ⟨cd.head, ⋯⟩ ≺ node → ∀ {next : N} (mem : next ∈ cd.next), ⟨next, ⋯⟩ ≼ node

If a node is a strict successor of the head, then it is at least a successor of the next element.

RegularChaseDerivationSkeleton

In general, the ChaseDerivationSkeleton does not enforce a specific node type to be able to define machinery for Skolem, restricted, and core chase all at the same time. Some specific results, we can only show for the Skolem and restricted chase, which is what we do here.

We use the RegularChaseDerivationSkeleton as an abbreviation for a ChaseDerivationSkeleton that uses the RegularChaseNode implementation where the ingoing and outgoing facts of each node are always the same (as opposed to the core chase where the outgoing facts would be a core of the ingoing facts).

@[reducible, inline]

abbrev RegularChaseDerivationSkeleton {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) (rules : RuleSet sig) : Type (max (max u_3 u_2) u_1)

Equations

• RegularChaseDerivationSkeleton obs rules = ChaseDerivationSkeleton (RegularChaseNode obs rules) obs rules

Subset Monotonicity of Facts in ChaseNodes

Since ChaseNodes always extend the previous facts, the fact sets can only be growing along the ChaseDerivationSkeleton.

theorem RegularChaseDerivationSkeleton.facts_node_subset_every_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : RegularChaseDerivationSkeleton obs rules} (node : RegularChaseNode obs rules) : node ∈ cd → (ChaseDerivationSkeleton.head cd).facts ⊆ node.facts

Each member's facts contain the head facts. Note that this extends to arbitrary pairs of members since each member always induces a subderivation where it acts as the head.

theorem RegularChaseDerivationSkeleton.mem_suffix_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd1 cd2 : RegularChaseDerivationSkeleton obs rules} (suffix : cd1 <:+ cd2) (node : RegularChaseNode obs rules) : node ∈ cd2 → node.facts ⊆ (ChaseDerivationSkeleton.head cd1).facts ∨ node ∈ cd1

A first implication of facts_node_subset_every_mem is that, considering one of our subderivations, each of our members either has all of its facts contained in the head of the subderivation or it is itself a member of the subderivation.

Only Finitely many Generated Facts

Here we cover the special case for RegularChaseDerivationSkeletons.

theorem RegularChaseDerivationSkeleton.facts_node_eq_union_initial_and_generated {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : RegularChaseDerivationSkeleton obs rules} {node : RegularChaseNode obs rules} (mem : node ∈ cd) : node.facts = (ChaseDerivationSkeleton.head cd).facts ∪ ChaseDerivationSkeleton.generatedFacts cd node

Each node's facts are formed by the initial facts and its generatedFacts.

theorem RegularChaseDerivationSkeleton.generatedFacts_finite_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : RegularChaseDerivationSkeleton obs rules} {node : RegularChaseNode obs rules} (mem : node ∈ cd) : Set.finite (ChaseDerivationSkeleton.generatedFacts cd node)

The generatedFacts are always finite.

Predecessor Relation

Here we cover the special case for RegularChaseDerivationSkeletons.

theorem RegularChaseDerivationSkeleton.facts_node_subset_of_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : RegularChaseDerivationSkeleton obs rules} {node1 node2 : ChaseDerivationSkeleton.Node cd} : node1 ≼ node2 → node1.val.facts ⊆ node2.val.facts

The facts of our predecessor are a subset of our facts.

Chase Result

Here, we define the result of a ChaseDerivationSkeleton, which is simply the FactSet that is the union of all facts of all ChaseNodes.

def RegularChaseDerivationSkeleton.result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : RegularChaseDerivationSkeleton obs rules) : FactSet sig

Equations

• cd.result f = ∃ (node : RegularChaseNode obs rules), node ∈ cd ∧ f ∈ node.facts

theorem RegularChaseDerivationSkeleton.facts_node_subset_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : RegularChaseDerivationSkeleton obs rules} (node : RegularChaseNode obs rules) : node ∈ cd → node.facts ⊆ cd.result

Every node's facts occur in the result.

theorem RegularChaseDerivationSkeleton.result_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd1 cd2 : RegularChaseDerivationSkeleton obs rules} (suffix : cd1 <:+ cd2) : cd1.result = cd2.result

The result of our suffix is the same our result.

theorem RegularChaseDerivationSkeleton.facts_mem_some_node_of_mem_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : RegularChaseDerivationSkeleton obs rules} (l : List (Fact sig)) : l.toSet ⊆ cd.result → ∃ (node : RegularChaseNode obs rules), node ∈ cd ∧ l.toSet ⊆ node.facts

For each (finite) list of facts in the result, there is a node that that contains all of them.

theorem RegularChaseDerivationSkeleton.trg_loaded_for_some_node_of_trg_loaded_for_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : RegularChaseDerivationSkeleton obs rules} (trg : Trigger { cond := obs.cond, monotone := ⋯ }) : trg.loaded cd.result → ∃ (node : RegularChaseNode obs rules), node ∈ cd ∧ trg.loaded node.facts

If a trigger is loaded for the result, then it is loaded for some node in the derivation.