Strict Constant Mappings

A StrictConstantMapping is an even more confined version of a ConstantMapping where constants are really just mapped to (other) constants and not arbitrary GroundTerms.

@[reducible, inline]

abbrev StrictConstantMapping (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Type u_3

The StrictConstantMapping is simply defined as a TermMapping.

Equations

• StrictConstantMapping sig = TermMapping sig.C sig.C

@[reducible, inline]

abbrev StrictConstantMapping.toConstantMapping {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) : ConstantMapping sig

A StrictConstantMapping can be transformed to a ConstantMapping in the obvious way.

Equations

• g.toConstantMapping = GroundTerm.const ∘ g

def StrictConstantMapping.apply_var_or_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) : TermMapping (VarOrConst sig) (VarOrConst sig)

We lift StrictConstantMappings to VarOrConst in the obvious way.

Equations

• g.apply_var_or_const (VarOrConst.var v) = VarOrConst.var v
• g.apply_var_or_const (VarOrConst.const c) = VarOrConst.const (g c)

theorem StrictConstantMapping.apply_var_or_const_filterVars_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) (vocs : List (VarOrConst sig)) : VarOrConst.filterVars (List.map g.apply_var_or_const vocs) = VarOrConst.filterVars vocs

Applying a StrictConstantMapping to a VarOrConst does not influence the result of VarOrConst.filterVars.

theorem StrictConstantMapping.map_leaves_eq_leaves_mapLeaves {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) (t : FiniteTree (SkolemFS sig) sig.C) : List.map g t.leaves = (FiniteTree.mapLeaves (fun (c : sig.C) => (g.toConstantMapping c).val) t).leaves

Mapping over the leaves of a PreGroundTerm is the same as calling the FiniteTree.mapLeaves with the toConstantMapping version of the StrictConstantMapping.

@[reducible, inline]

abbrev StrictConstantMapping.apply_function_free_atom {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) : FunctionFreeAtom sig → FunctionFreeAtom sig

We lift StrictConstantMappings to FunctionFreeAtoms in the obvious way.

Equations

• g.apply_function_free_atom = g.apply_var_or_const.apply_generalized_atom

theorem StrictConstantMapping.apply_function_free_atom_vars_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) (a : FunctionFreeAtom sig) : (g.apply_function_free_atom a).variables = a.variables

Applying a StrictConstantMapping to a FunctionFreeAtom does not change the variables.

@[reducible, inline]

abbrev StrictConstantMapping.apply_function_free_conj {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) : FunctionFreeConjunction sig → FunctionFreeConjunction sig

We lift StrictConstantMappings to FunctionFreeConjunctions in the obvious way.

Equations

• g.apply_function_free_conj = g.apply_var_or_const.apply_generalized_atom_list

theorem StrictConstantMapping.apply_function_free_conj_vars_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) (conj : FunctionFreeConjunction sig) : (g.apply_function_free_conj conj).vars = conj.vars

Applying a StrictConstantMapping to a FunctionFreeConjunction does not change the variables.