RuleSet

@[reducible, inline]

abbrev RuleSet (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Type (max (max u_3 u_2) u_1)

A RuleSet is a Set (Rule sig).

Equations

• RuleSet sig = CustomBasicDatastructures.Set (Rule sig)

def RuleSet.isDeterministic {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : Prop

A RuleSet is is deterministic if each rule is.

Equations

• rs.isDeterministic = ∀ (r : Rule sig), r ∈ rs → r.isDeterministic = true

def RuleSet.predicates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : CustomBasicDatastructures.Set sig.P

The predicate symbols of a RuleSet are the predicate symbols from all rules.

Equations

• rs.predicates p = ∃ (r : Rule sig), r ∈ rs ∧ p ∈ r.predicates

def RuleSet.constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : CustomBasicDatastructures.Set sig.C

The constants of a RuleSet are the constants from all rules.

Equations

• rs.constants c = ∃ (r : Rule sig), r ∈ rs ∧ c ∈ r.constants

def RuleSet.head_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : CustomBasicDatastructures.Set sig.C

The head constants of a RuleSet are the head constants from all rules.

Equations

• rs.head_constants c = ∃ (r : Rule sig), r ∈ rs ∧ c ∈ r.head_constants

def RuleSet.skolem_functions {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : CustomBasicDatastructures.Set (SkolemFS sig)

The Skolem function symbols of a RuleSet are the Skolem function symbols from all rules.

Equations

• rs.skolem_functions f = ∃ (r : Rule sig), r ∈ rs ∧ f ∈ r.skolem_functions

theorem RuleSet.predicates_finite_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : CustomBasicDatastructures.Set.finite rs → rs.predicates.finite

If the RuleSet is finite, so are the RuleSet.predicates.

theorem RuleSet.constants_finite_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : CustomBasicDatastructures.Set.finite rs → rs.constants.finite

If the RuleSet is finite, so are the RuleSet.constants.

theorem RuleSet.head_constants_finite_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : CustomBasicDatastructures.Set.finite rs → rs.head_constants.finite

If the RuleSet is finite, so are the RuleSet.head_constants.

theorem RuleSet.skolem_functions_finite_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : CustomBasicDatastructures.Set.finite rs → rs.skolem_functions.finite

If the RuleSet is finite, so are the RuleSet.skolem_functions.

theorem RuleSet.head_constants_subset_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : RuleSet sig) : rs.head_constants ⊆ rs.constants

The RuleSet.head_constants are a subset of the RuleSet.constants.