Tree Derivation

The TreeDerivation is the tree version of the ChaseDerivation. Since we allow rules to feature disjunctions, there are multiple possible results for a given trigger. The ChaseDerivation picks one possible choice. For the TreeDerivation, we consider all possiblities at once. That is, the tree branches out for the disjunctions.

We try to mimic much of the machinery introduced for ChaseDerivation but we will see that some of this requires a different approach. Most prominently, we now need to consider addresses of nodes in the tree to be able to define a proper predecessor relation.

The TreeDerivation Structure

The backbone of the TreeDerivation is a FiniteDegreeTree of ChaseNodes with a couple of 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 child nodes or there is no trigger and consequently the derivation stops at this point. This is expressed by the two auxiliary definitions above.
3. No triggers are active on leaf nodes.
4. For each trigger, there exists a depth in the tree from which on the trigger is never active anymore.

Conditions 3 and 4 together are "fairness", i.e. each trigger must eventually be non-active. Fairness ensures that the chase result (or in this case each fact set in the chase result) is indeed a model.

structure TreeDerivation {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

• tree : FiniteDegreeTree N
• isSome_root : self.tree.root.isSome = true
• triggers_exist (t2 : FiniteDegreeTree N) : t2 <:+ self.tree → ∀ (before : N), before ∈ t2.root → ChaseNode.succ_list before t2.childNodes
• fairness_leaves (leaf : N) : leaf ∈ self.tree.leaves → ∀ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules), ¬trg.val.active (ChaseNode.outgoingFacts obs rules leaf)
• fairness_infinite_branches (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) : ∃ (i : Nat), ∀ (ns : List Nat), ns.length ≥ i → ∀ (node : N), node ∈ self.tree.get? ns → ¬trg.val.active (ChaseNode.outgoingFacts obs rules node)

Basic Definitions

Here we introduce some auxiliary definitions and theorems and we lift some of the machinery of the underlying FiniteDegreeTree to TreeDerivation.

def TreeDerivation.toFiniteDegreeTreeWithRoot {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] (td : TreeDerivation N obs rules) : FiniteDegreeTree.FiniteDegreeTreeWithRoot N

We can convert a TreeDerivation directly to a FiniteDegreeTree.FiniteDegreeTreeWithRoot.

Equations

• td.toFiniteDegreeTreeWithRoot = ⟨td.tree, ⋯⟩

@[instance_reducible]

instance TreeDerivation.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 (TreeDerivation N obs rules)

Membership of ChaseNodes in the TreeDerivation directly corresponds to membership in the FiniteDegreeTree.

Equations

• TreeDerivation.instMembership = { mem := fun (td : TreeDerivation N obs rules) (node : N) => node ∈ td.tree }

theorem TreeDerivation.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] {td : TreeDerivation N obs rules} {e : N} : e ∈ td ↔ ∃ (ns : List Nat), td.tree.get? ns = some e

An element is a member of the tree iff it occurs at some address.

def TreeDerivation.derivation_for_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] (td : TreeDerivation N obs rules) (t2 : FiniteDegreeTree N) (suffix : t2 <:+ td.tree) (t2_root_some : t2.root.isSome = true) : TreeDerivation N obs rules

Each subtree of the underlying FiniteDegreeTree is itself a TreeDerivation as long as its root is not none.

Equations

• td.derivation_for_suffix t2 suffix t2_root_some = { tree := t2, isSome_root := t2_root_some, triggers_exist := ⋯, fairness_leaves := ⋯, fairness_infinite_branches := ⋯ }

def TreeDerivation.root {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] (td : TreeDerivation N obs rules) : N

The root of the TreeDerivation is the initial ChaseNode. We know that this is never none.

Equations

• td.root = td.tree.root.get ⋯

theorem TreeDerivation.root_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] {td : TreeDerivation N obs rules} : td.root ∈ td

The root is a member.

The (immediate) ChildNodes

For a TreeDerivation derivation, its childNodes are the ChaseNodes immediately following the root. We mainly introduce a couple of theorems here that abstract away the triggers_exist condition from the TreeDerivation definition.

def TreeDerivation.childNodes {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] (td : TreeDerivation N obs rules) : List N

Equations

• td.childNodes = td.tree.childNodes

theorem TreeDerivation.mem_of_mem_childNodes {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] {td : TreeDerivation N obs rules} (n : N) : n ∈ td.childNodes → n ∈ td

Each child node is a member.

theorem TreeDerivation.isSome_origin_of_mem_childNodes {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] {td : TreeDerivation N obs rules} (n : N) : n ∈ td.childNodes → (ChaseNode.origin n).isSome = true

The origin of the childNodes needs to be set.

theorem TreeDerivation.active_trigger_origin_of_mem_childNodes {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] {td : TreeDerivation N obs rules} {n : N} (mem : n ∈ td.childNodes) : ((ChaseNode.origin n).get ⋯).fst.val.active (ChaseNode.outgoingFacts obs rules td.root)

The trigger used to derive the childNodes is active for head.

theorem TreeDerivation.childNodes_ne_nil_iff_trg_ex {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] {td : TreeDerivation N obs rules} : td.childNodes ≠ [] ↔ ∃ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules), trg.val.active (ChaseNode.outgoingFacts obs rules td.root)

The childNodes are not nil if and only if some trigger is active on root.

theorem TreeDerivation.facts_childNodes {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] {td : TreeDerivation N obs rules} {n : N} (mem : n ∈ td.childNodes) : ChaseNode.ingoingFacts obs rules n = ChaseNode.outgoingFacts obs rules td.root ∪ (ChaseNode.origin_result n ⋯).toSet

The fact set of each of the childNodes consists exactly of the facts from root and the result of the trigger that introduces the child node.

TreeDerivation Subtrees

We define a suffix/subtree relation on TreeDerivation simply as the subtree relation of the underlying FiniteDegreeTree.

@[implicit_reducible]

def TreeDerivation.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] (td1 td2 : TreeDerivation N obs rules) : Prop

Equations

• (td1 <:+ td2) = (td1.tree <:+ td2.tree)

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

Equations

• TreeDerivation.«term_<:+_» = Lean.ParserDescr.trailingNode `TreeDerivation.«term_<:+_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <:+ ") (Lean.ParserDescr.cat `term 51))

theorem TreeDerivation.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] {td1 td2 : TreeDerivation N obs rules} : td1 <:+ td2 ↔ td1.tree <:+ td2.tree

theorem TreeDerivation.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 : TreeDerivation N obs rules} (suffix : cd1 <:+ cd2) (node : N) : node ∈ cd1 → node ∈ cd2

Members of our subtrees are also our members.

Child Trees

We can drop the root of a TreeDerivation and obtain a (possibly empty) list of childTrees, which are again TreeDerivations.

def TreeDerivation.childTrees {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] (td : TreeDerivation N obs rules) : List (TreeDerivation N obs rules)

We obtain the child trees of the FiniteDegreeTree and convert each of them into a TreeDerivation using derivation_for_suffix. We know that all of those trees have non-none roots.

Equations

• td.childTrees = List.map (fun (t : { x : FiniteDegreeTree.FiniteDegreeTreeWithRoot N // x ∈ td.tree.childTrees }) => td.derivation_for_suffix t.val.val ⋯ ⋯) td.tree.childTrees.attach

theorem TreeDerivation.mem_childTrees_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] {td : TreeDerivation N obs rules} (c : TreeDerivation N obs rules) : c ∈ td.childTrees ↔ c.toFiniteDegreeTreeWithRoot ∈ td.tree.childTrees

Membership in childTrees can be boiled down to membership in FiniteDegreeTree.childTrees.

theorem TreeDerivation.childNodes_eq {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] {td : TreeDerivation N obs rules} : td.childNodes = List.map root td.childTrees

childNodes can be expressed by mapping each childTrees to its root.

theorem TreeDerivation.IsSuffix_of_mem_childTrees {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] {td : TreeDerivation N obs rules} (td2 : TreeDerivation N obs rules) : td2 ∈ td.childTrees → td2 <:+ td

Each childTrees is a suffix.

theorem TreeDerivation.mem_iff_eq_root_or_mem_child {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] {td : TreeDerivation N obs rules} {node : N} : node ∈ td ↔ node = td.root ∨ ∃ (child : TreeDerivation N obs rules), child ∈ td.childTrees ∧ node ∈ child

A node is a member if and only if it is either the root or it is a member of a child tree.

theorem TreeDerivation.suffix_iff_eq_or_suffix_childTree {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] {td1 td2 : TreeDerivation N obs rules} : td1 <:+ td2 ↔ td1 = td2 ∨ ∃ (td3 : TreeDerivation N obs rules), td3 ∈ td2.childTrees ∧ td1 <:+ td3

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

Induction Principle for Members

Similar to FiniteDegreeTree.mem_rec, we define an induction principle to show properties of ChaseNodes in a TreeDerivation.

Looking ahead a bit, we will also want to define a predecessor relation on nodes in the tree as we did for nodes in a ChaseDerivation. This is not so elegant here though as the same node might indeed occur multiple times in the tree. Therefore, we are going to associate each node with its address in the tree to tell them apart. Since we are doing this anyway, it makes sense to define the induction principle already with respect to this kind of node.

NodeWithAddress

The NodeWithAddress is a structure of a ChaseNode, an address (i.e. a List Nat), and a proof that the chase node is indeed at the given address. We also introduce a couple of covenience functions and theorems for the NodeWithAddress.

structure TreeDerivation.NodeWithAddress {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] (td : TreeDerivation N obs rules) : Type u

• node : N
• address : List Nat
• eq : td.tree.get? self.address = some self.node

def TreeDerivation.NodeWithAddress.subderivation {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] {td : TreeDerivation N obs rules} (node : td.NodeWithAddress) : TreeDerivation N obs rules

Each NodeWithAddress induces a subderivation in the TreeDerivation.

Equations

• node.subderivation = td.derivation_for_suffix (td.tree.drop node.address) ⋯ ⋯

def TreeDerivation.NodeWithAddress.cast_for_new_root_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] {td : TreeDerivation N obs rules} (new_root : td.NodeWithAddress) (node : new_root.subderivation.NodeWithAddress) : td.NodeWithAddress

We can cast a node for one of our subderivations into our own node.

Equations

• new_root.cast_for_new_root_node node = { node := node.node, address := new_root.address ++ node.address, eq := ⋯ }

def TreeDerivation.NodeWithAddress.root {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] (td : TreeDerivation N obs rules) : td.NodeWithAddress

The NodeWithAddress version of TreeDerivation.root.

Equations

• TreeDerivation.NodeWithAddress.root td = { node := td.root, address := [], eq := ⋯ }

def TreeDerivation.NodeWithAddress.childNodes {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] {td : TreeDerivation N obs rules} (node : td.NodeWithAddress) : List td.NodeWithAddress

The child nodes of a given NodeWithAddress.

Equations

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

theorem TreeDerivation.NodeWithAddress.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] {td : TreeDerivation N obs rules} (node : td.NodeWithAddress) : node.node ∈ td

The NodeWithAddress is a member.

theorem TreeDerivation.NodeWithAddress.eq_of_address_eq {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] {td : TreeDerivation N obs rules} {n1 n2 : td.NodeWithAddress} : n1.address = n2.address → n1 = n2

Two NodeWithAddress are equal if their addresses are.

def TreeDerivation.NodeWithAddress.decEq {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] {td : TreeDerivation N obs rules} (n1 n2 : td.NodeWithAddress) : Decidable (n1 = n2)

NodeWithAddress has DecidableEq based on its address.

Equations

• n1.decEq n2 = if eq : n1.address = n2.address then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TreeDerivation.NodeWithAddress.instDecidableEq {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] {td : TreeDerivation N obs rules} : DecidableEq td.NodeWithAddress

Equations

• TreeDerivation.NodeWithAddress.instDecidableEq = TreeDerivation.NodeWithAddress.decEq

theorem TreeDerivation.NodeWithAddress.IsSuffix_subderivation {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] {td : TreeDerivation N obs rules} {node : td.NodeWithAddress} : node.subderivation <:+ td

subderivation is indeed a subtree.

theorem TreeDerivation.NodeWithAddress.root_subderivation {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] {td : TreeDerivation N obs rules} {node : td.NodeWithAddress} : root node.subderivation = { node := node.node, address := [], eq := ⋯ }

The root of the subderivation is the node itself with empty address.

@[simp]

theorem TreeDerivation.NodeWithAddress.root_subderivation' {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] {td : TreeDerivation N obs rules} {node : td.NodeWithAddress} : node.subderivation.root = node.node

The root of the subderivation is the node itself.

@[simp]

theorem TreeDerivation.NodeWithAddress.subderivation_root {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] {td : TreeDerivation N obs rules} : (root td).subderivation = td

The subderivation of the root is the original TreeDerivation.

theorem TreeDerivation.NodeWithAddress.childNodes_subderivation {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] {td : TreeDerivation N obs rules} {node : td.NodeWithAddress} : node.subderivation.childNodes = (td.tree.drop node.address).childNodes

Unfolds the childNodes and subderivation definitions to an expression on the underlying tree.

@[simp]

theorem TreeDerivation.NodeWithAddress.length_childNodes {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] {td : TreeDerivation N obs rules} {node : td.NodeWithAddress} : node.childNodes.length = node.subderivation.childNodes.length

NodeWithAddress.childNodes has the same length as TreeDerivation.childNodes.

theorem TreeDerivation.NodeWithAddress.childNodes_eq_childNodes {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] {td : TreeDerivation N obs rules} {node : td.NodeWithAddress} : node.subderivation.childNodes = List.map NodeWithAddress.node node.childNodes

NodeWithAddress.childNodes and TreeDerivation.childNodes are (almost) equal.

theorem TreeDerivation.NodeWithAddress.mem_childNodes_of_mem_childNodes {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] {td : TreeDerivation N obs rules} {node n : td.NodeWithAddress} : n ∈ node.childNodes → n.node ∈ node.subderivation.childNodes

Membership for NodeWithAddress.childNodes and TreeDerivation.childNodes is (almost) the same.

@[simp]

theorem TreeDerivation.NodeWithAddress.node_getElem_childNodes {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] {td : TreeDerivation N obs rules} {node : td.NodeWithAddress} (i : Nat) (lt : i < node.childNodes.length) : node.childNodes[i].node = node.subderivation.childNodes[i]

Getting specific elements from child nodes can be translated between NodeWithAddress.childNodes and TreeDerivation.childNodes.

@[simp]

theorem TreeDerivation.NodeWithAddress.address_getElem_childNodes {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] {td : TreeDerivation N obs rules} {node : td.NodeWithAddress} (i : Nat) (lt : i < node.childNodes.length) : node.childNodes[i].address = node.address ++ [i]

Getting specific element addresses from child nodes can be translated between NodeWithAddress.childNodes and TreeDerivation.childNodes.

theorem TreeDerivation.NodeWithAddress.cast_for_new_root_node_mem_chilNodes_cast_for_new_root_node_of_mem_childNodes {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] {td : TreeDerivation N obs rules} {new_root : td.NodeWithAddress} {n1 n2 : new_root.subderivation.NodeWithAddress} : n2 ∈ n1.childNodes → new_root.cast_for_new_root_node n2 ∈ (new_root.cast_for_new_root_node n1).childNodes

We can lift membership in childNodes along cast_for_new_root_node.

theorem TreeDerivation.NodeWithAddress.subderivation_mem_childTrees_of_mem_childNodes {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] {td : TreeDerivation N obs rules} {node node2 : td.NodeWithAddress} : node2 ∈ node.childNodes → node2.subderivation ∈ node.subderivation.childTrees

The subderivation for a child node is a child tree.

theorem TreeDerivation.NodeWithAddress.triggers_exist {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] {td : TreeDerivation N obs rules} (node : td.NodeWithAddress) : ChaseNode.succ_list node.node node.subderivation.childNodes

The triggers_exist property expressed in terms of the NodeWithAddress.

theorem TreeDerivation.NodeWithAddress.eq_root_or_mem_child {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] {td : TreeDerivation N obs rules} {node : td.NodeWithAddress} : node = root td ∨ ∃ (child : td.NodeWithAddress), child ∈ (root td).childNodes ∧ ∃ (node' : child.subderivation.NodeWithAddress), child.cast_for_new_root_node node' = node

A node is a member if and only if it is either the root or it is a member of a child tree.

Now we are ready for the actual induction principle on NodeWithAddresss in a TreeDerivation.

theorem TreeDerivation.mem_rec_address {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] {td : TreeDerivation N obs rules} {motive : td.NodeWithAddress → Prop} (root : motive (NodeWithAddress.root td)) (step : ∀ (new_root : td.NodeWithAddress), motive new_root → ∀ (c : td.NodeWithAddress), c ∈ new_root.childNodes → motive c) (node : td.NodeWithAddress) : motive node

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

theorem TreeDerivation.mem_some_childTree_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] {td : TreeDerivation N obs rules} {node : N} : (∃ (t : TreeDerivation N obs rules), t ∈ td.childTrees ∧ node ∈ t) ↔ ∃ (td2 : TreeDerivation N obs rules), td2 <:+ td ∧ node ∈ td2.childNodes

A node is a member of some element of childTrees if and only if there is a subderivation where the node occurs in the childNodes. Part of this proof uses the induction principle defined above.

theorem TreeDerivation.mem_subderivation_childNodes_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] {td : TreeDerivation N obs rules} {node : td.NodeWithAddress} : (∃ (child : td.NodeWithAddress), child ∈ (NodeWithAddress.root td).childNodes ∧ ∃ (node' : child.subderivation.NodeWithAddress), child.cast_for_new_root_node node' = node) ↔ ∃ (node' : td.NodeWithAddress), node ∈ node'.childNodes

If a node occurs in the subderivation of a child of the root, then this node also occurs as the child node of some node in the tree. This is essentially the NodeWithAddress version of mem_some_childTree_iff above and uses essentially the same proof for the first direction.

Only Finitely many Generated Facts

The generated facts of node in a TreeDerivation 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 TreeDerivation.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] (td : TreeDerivation 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

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

theorem TreeDerivation.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) {td : TreeDerivation N obs rules} (start_eq : ChaseNode.ingoingFacts obs rules td.root = ChaseNode.outgoingFacts obs rules td.root) {node : N} (mem : node ∈ td) : Set.finite (td.generatedFacts node)

The generatedFacts are always finite.

Predecessor Relation

Opposed to the ChaseDerivation, we define the predecessor relation direclty using addresses here. This is because ChaseNodes may indeed occur multiple times in a TreeDerivation (just not in the same branch) and therefore the approach used in ChaseDerivation would not quite work. In particular, note that the TreeDerivation has no equivalent for ChaseDerivation.suffix_of_suffix_of_suffix_of_head_mem.

Also, even with the address approach, the relation is not total here (which is expected for a tree).

def TreeDerivation.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] {td : TreeDerivation N obs rules} (n1 n2 : td.NodeWithAddress) : Prop

Node $n$ is a predecessor of node $m$ if the address of $n$ is a prefix of the address of $m$. Predecessor can therefore also be understood as ancestor in the tree.

Equations

• (n1 ≼ n2) = (n1.address <+: n2.address)

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

Equations

• TreeDerivation.«term_≼_» = Lean.ParserDescr.trailingNode `TreeDerivation.«term_≼_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≼ ") (Lean.ParserDescr.cat `term 51))

theorem TreeDerivation.predecessor_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] {td : TreeDerivation N obs rules} {n1 n2 : td.NodeWithAddress} : n1 ≼ n2 ↔ ∃ (n2' : n1.subderivation.NodeWithAddress), n1.cast_for_new_root_node n2' = n2

A node n1 is a predecessor of another node n2 if and only if there exists a node in the subderivation of n1 that is equal to n2 (when casting it back to a node of the original TreeDerivation).

theorem TreeDerivation.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] {td : TreeDerivation N obs rules} {new_root : td.NodeWithAddress} {n1 n2 : new_root.subderivation.NodeWithAddress} : n1 ≼ n2 → new_root.cast_for_new_root_node n1 ≼ new_root.cast_for_new_root_node 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 TreeDerivation.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] {td : TreeDerivation N obs rules} {node : td.NodeWithAddress} : node ≼ node

The predecessor relation is reflexive.

theorem TreeDerivation.predecessor_antisymm {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] {td : TreeDerivation N obs rules} {n1 n2 : td.NodeWithAddress} : n1 ≼ n2 → n2 ≼ n1 → n1 = n2

The predecessor relation is antisymmetric.

theorem TreeDerivation.predecessor_trans {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] {td : TreeDerivation N obs rules} {n1 n2 n3 : td.NodeWithAddress} : n1 ≼ n2 → n2 ≼ n3 → n1 ≼ n3

The predecessor relation is transitive.

theorem TreeDerivation.node_prec_childNodes {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] {td : TreeDerivation N obs rules} {node : td.NodeWithAddress} (n : td.NodeWithAddress) : n ∈ node.childNodes → node ≼ n

Each node is the predecessor of its childNodes.

theorem TreeDerivation.mem_subderivation_of_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] {td : TreeDerivation N obs rules} {n1 n2 : td.NodeWithAddress} : n1 ≼ n2 → n2.node ∈ n1.subderivation

If n2 is a successor of n1, then n2 must occurs in the subtree induced by n1.

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

def TreeDerivation.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] {td : TreeDerivation N obs rules} (n1 n2 : td.NodeWithAddress) : 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 TreeDerivation.«term_≺_» : Lean.TrailingParserDescr

Equations

• TreeDerivation.«term_≺_» = Lean.ParserDescr.trailingNode `TreeDerivation.«term_≺_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺ ") (Lean.ParserDescr.cat `term 51))

theorem TreeDerivation.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] {td : TreeDerivation N obs rules} {new_root : td.NodeWithAddress} {n1 n2 : new_root.subderivation.NodeWithAddress} : n1 ≺ n2 → new_root.cast_for_new_root_node n1 ≺ new_root.cast_for_new_root_node n2

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

theorem TreeDerivation.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] {td : TreeDerivation N obs rules} {n : td.NodeWithAddress} : ¬n ≺ n

The strict predecessor relation is irreflexive.

theorem TreeDerivation.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] {td : TreeDerivation N obs rules} {n1 n2 : td.NodeWithAddress} : n1 ≼ n2 → n1 = n2 ∨ n1 ≺ n2

A predecessor is either equal or a strict predecessor.

theorem TreeDerivation.strict_predecessor_asymmetric {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] {td : TreeDerivation N obs rules} {n1 n2 : td.NodeWithAddress} : n1 ≺ n2 → ¬n2 ≺ n1

The strict predecessor relation is asymmetric.

theorem TreeDerivation.strict_predecessor_trans {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] {td : TreeDerivation N obs rules} {n1 n2 n3 : td.NodeWithAddress} : n1 ≺ n2 → n2 ≺ n3 → n1 ≺ n3

The strict predecessor relation is transitive.

theorem TreeDerivation.strict_prec_of_prec_of_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] {td : TreeDerivation N obs rules} {n1 n2 n3 : td.NodeWithAddress} : n1 ≼ n2 → n2 ≺ n3 → n1 ≺ n3

The strict predecessor relation is transitive with respect to the regular predecessor relation.

theorem TreeDerivation.strict_prec_of_strict_prec_of_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] {td : TreeDerivation N obs rules} {n1 n2 n3 : td.NodeWithAddress} : n1 ≺ n2 → n2 ≼ n3 → n1 ≺ n3

The strict predecessor relation is transitive with respect to the regular predecessor relation.

theorem TreeDerivation.length_address_lt_of_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] {td : TreeDerivation N obs rules} {n1 n2 : td.NodeWithAddress} : n1 ≺ n2 → n1.address.length < n2.address.length

If a node is a strict predecessor, the length of its address is strictly smaller.

def TreeDerivation.next_on_path_to_succ {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] {td : TreeDerivation N obs rules} {n1 n2 : td.NodeWithAddress} (succ : n1 ≺ n2) : td.NodeWithAddress

If n2 is a strict successor of n1, we can find the child of n1 that is on the path to n2.

Equations

• TreeDerivation.next_on_path_to_succ succ = n1.childNodes[(List.drop n1.address.length n2.address).head ⋯]

@[simp]

theorem TreeDerivation.length_address_next_on_path_to_succ {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] {td : TreeDerivation N obs rules} {n1 n2 : td.NodeWithAddress} (succ : n1 ≺ n2) : (next_on_path_to_succ succ).address.length = n1.address.length + 1

The node that is next on the path from n1 to n2 has an address with the length of n1's address plus one.

theorem TreeDerivation.next_on_path_to_succ_mem_childNodes {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] {td : TreeDerivation N obs rules} {n1 n2 : td.NodeWithAddress} (succ : n1 ≺ n2) : next_on_path_to_succ succ ∈ n1.childNodes

The node that is next on the path from n1 to n2 is a child of n1.

theorem TreeDerivation.next_on_path_to_succ_is_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] {td : TreeDerivation N obs rules} {n1 n2 : td.NodeWithAddress} (succ : n1 ≺ n2) : next_on_path_to_succ succ ≼ n2

The node that is next on the path from n1 to n2 is a predecessor of n2 (not necessarily a strict one).

theorem TreeDerivation.mem_childNodes_of_some_node_of_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] {td : TreeDerivation N obs rules} {n1 n2 : td.NodeWithAddress} : n1 ≺ n2 → ∃ (n3 : td.NodeWithAddress), n1 ≼ n3 ∧ n2 ∈ n3.childNodes

If a node is a strict successor of another, then it occurs as the child of a node which is at least a regular successor.

theorem TreeDerivation.wellFounded_pred {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] {td : TreeDerivation N obs rules} : WellFounded strict_predecessor

The strict_predecessor relation is WellFounded.

@[instance_reducible]

instance TreeDerivation.instWellFoundedRelationNodeWithAddress {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] {td : TreeDerivation N obs rules} : WellFoundedRelation td.NodeWithAddress

Equations

• TreeDerivation.instWellFoundedRelationNodeWithAddress = { rel := TreeDerivation.strict_predecessor, wf := ⋯ }

Minimal Nodes with given Properties

If a property hold for a given node in the chase, then there must be a "first" node for which this property holds. That means that this node is minimal with respect to the ≺ relation. The result follows by the well foundedness of the ≺ relation.

theorem TreeDerivation.prop_for_node_has_minimal_such_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] {td : TreeDerivation N obs rules} (prop : td.NodeWithAddress → Prop) (n : td.NodeWithAddress) : prop n → ∃ (n2 : td.NodeWithAddress), prop n2 ∧ n2 ≼ n ∧ ∀ (n3 : td.NodeWithAddress), n3 ≺ n2 → ¬prop n3

Branches and Chase Result

Here, we define the branches of the TreeDerivation. It should be no surprise that these are ChaseDerivations.

def TreeDerivation.derivationSkeleton_for_branch {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] (td : TreeDerivation N obs rules) (branch : PossiblyInfiniteList N) (branch_mem : branch ∈ td.tree.branches) : ChaseDerivationSkeleton N obs rules

Each branch of the underlying tree can be transformed into a proper ChaseDerivationSkeleton.

Equations

• td.derivationSkeleton_for_branch branch branch_mem = { branch := branch, isSome_head := ⋯, triggers_exist := ⋯ }

def TreeDerivation.derivation_for_branch {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] (td : TreeDerivation N obs rules) (branch : PossiblyInfiniteList N) (branch_mem : branch ∈ td.tree.branches) : ChaseDerivation N obs rules

Each branch of the underlying tree can be transformed into a proper ChaseDerivation.

Equations

• td.derivation_for_branch branch branch_mem = { toChaseDerivationSkeleton := td.derivationSkeleton_for_branch branch branch_mem, triggers_active := ⋯, fairness := ⋯ }

def TreeDerivation.branches {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] (td : TreeDerivation N obs rules) : Set (ChaseDerivation N obs rules)

The branches of the TreeDerivation are defined as all the ChaseDerivation that occur as branches in the tree.

Equations

• td.branches branch = (branch.branch ∈ td.tree.branches)

theorem TreeDerivation.branches_eq {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] {td : TreeDerivation N obs rules} : td.branches = fun (b : ChaseDerivation N obs rules) => b.head = td.root ∧ (td.childTrees = [] ∧ b.next = none ∨ ∃ (td2 : TreeDerivation N obs rules), td2 ∈ td.childTrees ∧ ∃ (next : N), ∃ (next_eq : next ∈ b.next), b.tail ⋯ ∈ td2.branches)

We lift FiniteDegreeTree.branches_eq to a similar version for TreeDerivations.

theorem TreeDerivation.derivation_for_branch_mem_branches {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] {td : TreeDerivation N obs rules} {branch : PossiblyInfiniteList N} {branch_mem : branch ∈ td.tree.branches} : td.derivation_for_branch branch branch_mem ∈ td.branches

Each ChaseDerivation constructed using derivation_for_branch occurs in branches.

Terms in the Chase

We make some general observations about certain terms that might occur in the chase.

1. Constants can only originate directly from rules or from the initial fact set. No other constants can be introduced.
2. Functional terms can either also originate from the initial fact set or they are introduced as fresh terms by a trigger.

The second observation entails that the precense of a functional term that does not occur in the initial fact set implies that the trigger that introduces this term must have been applied in some node.

theorem TreeDerivation.constants_node_subset_constants_fs_union_constants_rules {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) {td child : TreeDerivation N obs rules} (child_mem : child ∈ td.childTrees) {node : N} (node_mem : node ∈ child) : (ChaseNode.ingoingFacts obs rules node).constants ⊆ (ChaseNode.outgoingFacts obs rules td.root).constants ∪ rules.head_constants

Constants in the chase can only come from the initial fact set or from a constant in a rule.

theorem TreeDerivation.functional_term_originates_from_some_trigger {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) {td child : TreeDerivation N obs rules} (child_mem : child ∈ td.childTrees) (node : child.NodeWithAddress) {t : GroundTerm sig} (t_is_func : ∃ (func : SkolemFS sig), ∃ (ts : List (GroundTerm sig)), ∃ (arity_ok : ts.length = func.arity), t = GroundTerm.func func ts arity_ok) (t_mem : t ∈ (ChaseNode.ingoingFacts obs rules node.node).terms) : t ∈ (ChaseNode.outgoingFacts obs rules td.root).terms ∨ ∃ (node2 : child.NodeWithAddress), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length), orig ∈ ChaseNode.origin node2.node ∧ t ∈ orig.fst.val.fresh_terms_for_head_disjunct ↑orig.snd ⋯

Each functional term in the chase originates as a fresh term from a trigger if it was not already part of the initial fact set.

theorem TreeDerivation.trigger_introducing_functional_term_occurs_in_chase {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) {td child : TreeDerivation N obs rules} (child_mem : child ∈ td.childTrees) (node : child.NodeWithAddress) {t : GroundTerm sig} (t_mem_node : t ∈ (ChaseNode.ingoingFacts obs rules node.node).terms) {trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules} {disj_idx : Nat} {lt : disj_idx < trg.val.rule.head.length} (t_mem_trg : t ∈ trg.val.fresh_terms_for_head_disjunct disj_idx lt) : t ∈ (ChaseNode.outgoingFacts obs rules td.root).terms ∨ ∃ (node2 : child.NodeWithAddress), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length), orig ∈ ChaseNode.origin node2.node ∧ orig.fst.equiv trg ∧ ↑orig.snd = disj_idx

If a functional term occurs in the chase, then the trigger that introduces this term must have been used in the chase, unless the term already occurs in the initial fact set.

Derivation Generation

We lift FiniteDegreeTree.generate_branch to TreeDerivation using a generator over NodeWithAddress and combine it with FiniteDegreeTree.generate_branch_mem_branches to obtain a ChaseDerivation directly.

def TreeDerivation.generate_branch {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] {β : Type u_4} (td : TreeDerivation N obs rules) (start : β) (generator : β → Option β) (mapper : β → td.NodeWithAddress) : PossiblyInfiniteList N

We lift FiniteDegreeTree.generate_branch to TreeDerivation.

Equations

• td.generate_branch start generator mapper = FiniteDegreeTree.generate_branch (some start) generator fun (b : β) => (mapper b).subderivation.toFiniteDegreeTreeWithRoot

theorem TreeDerivation.generate_branch_mem_tree_branches {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] {β : Type u_1} {td : TreeDerivation N obs rules} {start : β} {generator : β → Option β} {mapper : β → td.NodeWithAddress} (next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes) (maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []) : td.generate_branch start generator mapper ∈ (mapper start).subderivation.tree.branches

We lift FiniteDegreeTree.generate_branch_mem_branches to TreeDerivation.

def TreeDerivation.generate_subderivation {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] {β : Type u_4} (td : TreeDerivation N obs rules) (start : β) (generator : β → Option β) (mapper : β → td.NodeWithAddress) (next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes) (maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []) : ChaseDerivation N obs rules

We can genearte a ChaseDerivation within a TreeDerivation using a generator function that ensures that the cnsecutive elements are children of each other and that the genearted derivation is maximal.

Equations

• td.generate_subderivation start generator mapper next_is_child maximal = (mapper start).subderivation.derivation_for_branch (td.generate_branch start generator mapper) ⋯

theorem TreeDerivation.generate_subderivation_mem_branches {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] {β : Type u_1} {td : TreeDerivation N obs rules} {start : β} {generator : β → Option β} {mapper : β → td.NodeWithAddress} {next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes} {maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []} (start_eq : mapper start = NodeWithAddress.root td) : td.generate_subderivation start generator mapper next_is_child maximal ∈ td.branches

The result of generate_subderivation occurs in TreeDerivation.branches if it starts on the root of the tree.

@[simp]

theorem TreeDerivation.head_generate_subderivation {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] {β : Type u_1} {td : TreeDerivation N obs rules} {start : β} {generator : β → Option β} {mapper : β → td.NodeWithAddress} {next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes} {maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []} : (td.generate_subderivation start generator mapper next_is_child maximal).head = (mapper start).node

The head for the derivation produced by generate_subderivation is exactly the mapped start value.

@[simp]

theorem TreeDerivation.next_generate_subderivation {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] {β : Type u_1} {td : TreeDerivation N obs rules} {start : β} {generator : β → Option β} {mapper : β → td.NodeWithAddress} {next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes} {maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []} : (td.generate_subderivation start generator mapper next_is_child maximal).next = Option.map NodeWithAddress.node (Option.map mapper (generator start))

The next node for the derivation produced by generate_subderivation is exactly the mapped value after the first generator application.

theorem TreeDerivation.tail_generate_subderivation {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] {β : Type u_1} {td : TreeDerivation N obs rules} {start : β} {generator : β → Option β} {mapper : β → td.NodeWithAddress} {next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes} {maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []} (next : β) (next_mem : next ∈ generator start) : (td.generate_subderivation start generator mapper next_is_child maximal).tail ⋯ = td.generate_subderivation next generator mapper next_is_child maximal

The tail for the derivation produced by generate_subderivation is exactly the generated derivation when applying the generator once initially.

theorem TreeDerivation.mem_generate_subderivation {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] {β : Type u_1} {td : TreeDerivation N obs rules} {start : β} {generator : β → Option β} {mapper : β → td.NodeWithAddress} {next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes} {maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []} {node : N} : node ∈ td.generate_subderivation start generator mapper next_is_child maximal ↔ ∃ (n : Nat), node ∈ Option.map NodeWithAddress.node (Option.map mapper (Function.repeat_fun (fun (x : Option β) => x.bind generator) n (some start)))

A node occurs in generate_subderivation iff there is an appropriate number of repetitions for the generator function.

RegularTreeDerivation

As for the RegularChaseDerivation, we consider the special case of TreeDerivation where the node type is fixed to be RegularChaseNode to talk about Skolem and restricted chase (but not core chase). We abbreviate fixing this node type by introducing the RegularTreeDerivation.

@[reducible, inline]

abbrev RegularTreeDerivation {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

• RegularTreeDerivation obs rules = TreeDerivation (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 branches of the TreeDerivation. This has a couple of convenient implications. For example, the root of a TreeDerivation can never occur in its childTrees.

theorem RegularTreeDerivation.facts_node_subset_every_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : RegularTreeDerivation obs rules} (node : RegularChaseNode obs rules) : node ∈ td → (TreeDerivation.root td).facts ⊆ node.facts

Each member's facts contain the root facts.

theorem RegularTreeDerivation.root_not_mem_childTrees {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : RegularTreeDerivation obs rules} : ¬∃ (t : TreeDerivation (RegularChaseNode obs rules) obs rules), t ∈ TreeDerivation.childTrees td ∧ TreeDerivation.root td ∈ t

The root cannot occur in the childTrees. Otherwise, it would be introduced using a trigger but then this trigger is already obsolete since all the facts from root already occur in the very beginning. We use ObsolescenceCondition.contains_trg_result_implies_cond here.

theorem RegularTreeDerivation.eq_of_suffix_of_root_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td1 td2 : RegularTreeDerivation obs rules} (suffix : td1 <:+ td2) (root_mem : TreeDerivation.root td2 ∈ td1) : td1 = td2

By root_not_mem_childTrees, if we have a subtree but our root occurs in the subtree, then our subtree is equal to us.

Only Finitely many Generated Facts

Here we cover the special case for RegularTreeDerivations.

theorem RegularTreeDerivation.facts_node_eq_union_initial_and_generated {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : RegularTreeDerivation obs rules} {node : RegularChaseNode obs rules} (mem : node ∈ td) : node.facts = (TreeDerivation.root td).facts ∪ TreeDerivation.generatedFacts td node

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

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

The generatedFacts are always finite.

Predecessor Relation

Here we cover the special case for RegularChaseDerivationSkeletons.

theorem RegularTreeDerivation.facts_node_subset_of_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : RegularTreeDerivation obs rules} {node1 node2 : TreeDerivation.NodeWithAddress td} : node1 ≼ node2 → node1.node.facts ⊆ node2.node.facts

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

theorem RegularTreeDerivation.node_strict_prec_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : RegularTreeDerivation obs rules} {node : TreeDerivation.NodeWithAddress td} (n : TreeDerivation.NodeWithAddress td) : n ∈ node.childNodes → node ≺ n

Each node is a strict predecessor of its childNodes.

theorem RegularTreeDerivation.facts_not_subset_of_strict_predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : RegularTreeDerivation obs rules} {n1 n2 : TreeDerivation.NodeWithAddress td} : n1 ≺ n2 → ¬n2.node.facts ⊆ n1.node.facts

The facts of a strict successor cannot be a subset of our facts. This is because strict successor nodes can only be introduced by active triggers. But if a trigger only produces facts that already exist, then it cannot be active.

Chase Result

The chase result is the set of the results of all the ChaseDerivations in the tree branches. We already know from the ChaseDerivation that each element of TreeDerivation.result is therefore a model of the rules.

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

The result is the set of FactSets that correspond to the results of the branches.

Equations

• td.result = (TreeDerivation.branches td).map fun (deriv : ChaseDerivation (RegularChaseNode obs rules) obs rules) => RegularChaseDerivationSkeleton.result deriv.toChaseDerivationSkeleton

theorem RegularTreeDerivation.result_models_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : RegularTreeDerivation obs rules} (fs : FactSet sig) : fs ∈ td.result → fs.modelsRules rules

Each element of the result models the rules.

Terms in the Chase

We make some general observations about certain terms that might occur in the chase.

1. Constants can only originate directly from rules or from the initial fact set. No other constants can be introduced.
2. Functional terms can either also originate from the initial fact set or they are introduced as fresh terms by a trigger.

The second observation entails that the precense of a functional term that does not occur in the initial fact set implies that the trigger that introduces this term must have been applied in some node.

theorem RegularTreeDerivation.constants_node_subset_constants_fs_union_constants_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : RegularTreeDerivation obs rules} {node : RegularChaseNode obs rules} (node_mem : node ∈ td) : node.facts.constants ⊆ (TreeDerivation.root td).facts.constants ∪ rules.head_constants

Constants in the chase can only come from the initial fact set or from a constant in a rule.

theorem RegularTreeDerivation.functional_term_originates_from_some_trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : RegularTreeDerivation obs rules} (node : TreeDerivation.NodeWithAddress td) {t : GroundTerm sig} (t_is_func : ∃ (func : SkolemFS sig), ∃ (ts : List (GroundTerm sig)), ∃ (arity_ok : ts.length = func.arity), t = GroundTerm.func func ts arity_ok) (t_mem : t ∈ node.node.facts.terms) : t ∈ (TreeDerivation.root td).facts.terms ∨ ∃ (node2 : TreeDerivation.NodeWithAddress td), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length), orig ∈ node2.node.origin ∧ t ∈ orig.fst.val.fresh_terms_for_head_disjunct ↑orig.snd ⋯

Each functional term in the chase originates as a fresh term from a trigger if it was not already part of the initial fact set.

theorem RegularTreeDerivation.trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : RegularTreeDerivation obs rules} (node : TreeDerivation.NodeWithAddress td) {t : GroundTerm sig} (t_mem_node : t ∈ node.node.facts.terms) {trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules} {disj_idx : Nat} {lt : disj_idx < trg.val.rule.head.length} (t_mem_trg : t ∈ trg.val.fresh_terms_for_head_disjunct disj_idx lt) : t ∈ (TreeDerivation.root td).facts.terms ∨ ∃ (node2 : TreeDerivation.NodeWithAddress td), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length), orig ∈ node2.node.origin ∧ orig.fst.equiv trg ∧ ↑orig.snd = disj_idx

If a functional term occurs in the chase, then the trigger that introduces this term must have been used in the chase, unless the term already occurs in the initial fact set.

theorem RegularTreeDerivation.result_of_trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : RegularTreeDerivation obs rules} (node : TreeDerivation.NodeWithAddress td) {t : GroundTerm sig} (t_mem_node : t ∈ node.node.facts.terms) {trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules} {disj_idx : Nat} {lt : disj_idx < trg.val.rule.head.length} (t_mem_trg : t ∈ trg.val.fresh_terms_for_head_disjunct disj_idx lt) : t ∈ (TreeDerivation.root td).facts.terms ∨ trg.val.mapped_head[disj_idx].toSet ⊆ node.node.facts

If a functional term occurs in the chase, then the result of the trigger that introduces this term is contained in the current node, unless the functional term already occurs in the initial fact set.