Constant Mappings

A ConstantMapping is a TermMapping from constants to GroundTerms. This is very similar to a GroundSubstitution only that it maps constants instead of variables

@[reducible, inline]

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

Equations

• ConstantMapping sig = TermMapping sig.C (GroundTerm sig)

def ConstantMapping.id {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : ConstantMapping sig

The id ConstantMapping is the GroundTerm.const constructor.

Equations

• ConstantMapping.id = GroundTerm.const

@[reducible, inline]

abbrev ConstantMapping.apply_pre_ground_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) : TermMapping (PreGroundTerm sig) (PreGroundTerm sig)

We apply a ConstantMapping to a PreGroundTerm by applying it to all leaves.

Equations

• g.apply_pre_ground_term = FiniteTree.mapLeaves fun (c : sig.C) => (g c).val

theorem ConstantMapping.apply_pre_ground_term_id {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (t : FiniteTree (SkolemFS sig) sig.C) : id.apply_pre_ground_term t = t

Applying the ConstantMapping.id on a PreGroundTerm yields the same term.

theorem ConstantMapping.apply_pre_ground_term_arity_ok {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) (t : FiniteTree (SkolemFS sig) sig.C) (arity_ok : PreGroundTerm.arity_ok t = true) : PreGroundTerm.arity_ok (g.apply_pre_ground_term t) = true

Applying a ConstantMapping to a PreGroundTerm retains the PreGroundTerm.arity_ok property.

theorem ConstantMapping.apply_pre_ground_term_congr_left {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g g2 : ConstantMapping sig) (t : PreGroundTerm sig) : (∀ (c : sig.C), c ∈ FiniteTree.leaves t → g c = g2 c) → g.apply_pre_ground_term t = g2.apply_pre_ground_term t

Mapping the same term using two ConstantMappings yields the same term if the mappings agree on all leaves of the term.

theorem ConstantMapping.apply_pre_ground_term_eq_self_of_id_on_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) (t : PreGroundTerm sig) (id_on_constants : ∀ (c : sig.C), c ∈ FiniteTree.leaves t → g c = GroundTerm.const c) : g.apply_pre_ground_term t = t

If the ConstantMapping is the id on the leaves of a term, applying the mapping to the term is also the id.

def ConstantMapping.apply_ground_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) : TermMapping (GroundTerm sig) (GroundTerm sig)

We lift ConstantMappings to GroundTerms in the obvious way.

Equations

• g.apply_ground_term t = ⟨g.apply_pre_ground_term t.val, ⋯⟩

theorem ConstantMapping.apply_ground_term_constant {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) (c : sig.C) : g.apply_ground_term (GroundTerm.const c) = g c

Applying a ConstantMapping to a GroundTerm.const is the same as directly applying the mapping to the underlying constant.

theorem ConstantMapping.apply_ground_term_func {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) (func : SkolemFS sig) (ts : List (GroundTerm sig)) (arity_ok : ts.length = func.arity) : g.apply_ground_term (GroundTerm.func func ts arity_ok) = GroundTerm.func func (List.map g.apply_ground_term ts) ⋯

Applyign a ConstantMapping to a GroundTerm.func is the same as applying the mapping to all child terms.

theorem ConstantMapping.apply_ground_term_swap_apply_skolem_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) (subs : GroundSubstitution sig) (t : SkolemTerm sig) : (∀ (c : sig.C), t ≠ SkolemTerm.const c) → g.apply_ground_term (subs.apply_skolem_term t) = GroundSubstitution.apply_skolem_term (g.apply_ground_term ∘ subs) t

For a non-constant SkolemTerm, if we apply a ConstantMapping after a GroundSubstitution, we can instead apply the substitution that is the composition of the ConstantMapping after the GroundSubstitution. Note that this does not work for constants since the ConstantMapping might map it some something else, whereas the composed substitution maps each constant to itself.

theorem ConstantMapping.apply_ground_term_congr_left {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g g2 : ConstantMapping sig) (t : GroundTerm sig) : (∀ (c : sig.C), c ∈ t.constants → g c = g2 c) → g.apply_ground_term t = g2.apply_ground_term t

Mapping the same term using two ConstantMappings yields the same term if the mappings agree on all constants of the term.

theorem ConstantMapping.apply_ground_term_eq_self_of_id_on_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) (t : GroundTerm sig) (id_on_constants : ∀ (c : sig.C), c ∈ t.constants → g c = GroundTerm.const c) : g.apply_ground_term t = t

If the ConstantMapping is the id on the constants of a term, applying the mapping to the term is also the id.

@[reducible, inline]

abbrev ConstantMapping.apply_fact {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) : Fact sig → Fact sig

We lift ConstantMappings to Facts in the obvious way.

Equations

• g.apply_fact = g.apply_ground_term.apply_generalized_atom

theorem ConstantMapping.apply_fact_eq_groundTermMapping_applyFact {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) (f : Fact sig) : g.apply_fact f = GroundTermMapping.applyFact g.apply_ground_term f

Applying a ConstantMapping to a fact can be seens as applying a GroundTermMapping to the fact.

theorem ConstantMapping.apply_fact_swap_apply_to_function_free_atom {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) (trg : PreTrigger sig) (a : FunctionFreeAtom sig) (h : ∀ (d : sig.C), d ∈ a.constants → g d = GroundTerm.const d) (i : Nat) : g.apply_fact (trg.apply_to_function_free_atom i a) = { rule := trg.rule, subs := g.apply_ground_term ∘ trg.subs }.apply_to_function_free_atom i a

Consider a ConstantMapping, a PreTrigger, and a FunctionFreeAtom. If the constant mapping if the id on all constants in the atom, then applying the mapping after the trigger is the same a applying a trigger where the constant mapping is composed with the original substitution.

theorem ConstantMapping.apply_fact_congr_left {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g g2 : ConstantMapping sig) (f : Fact sig) : (∀ (c : sig.C), c ∈ f.constants → g c = g2 c) → g.apply_fact f = g2.apply_fact f

Mapping the same fact using two ConstantMappings yields the same fact if the mappings agree on all constants of the fact.

theorem ConstantMapping.apply_fact_eq_self_of_id_on_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) (f : Fact sig) (id_on_constants : ∀ (c : sig.C), c ∈ f.constants → g c = GroundTerm.const c) : g.apply_fact f = f

If the ConstantMapping is the id on the constants of a fact, applying the mapping to the fact is also the id.

@[reducible, inline]

abbrev ConstantMapping.apply_fact_set {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : ConstantMapping sig) : FactSet sig → FactSet sig

We lift ConstantMapping s to FactSet`s in the obvious way.

Equations

• g.apply_fact_set = g.apply_ground_term.apply_generalized_atom_set