Renaming Constants apart in a GroundSubstitution and PreTrigger

We lift the PreGroundTerm.rename_constants_apart functionality to GroundSubstitution and PreTrigger. This pretty much happens in the obvious way and apart from being technical, this is not interesting.

def GroundSubstitution.rename_constants_apart_for_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] (subs : GroundSubstitution sig) (forbidden_constants : List sig.C) : List sig.V → GroundSubstitution sig

Equations

• One or more equations did not get rendered due to their size.
• subs.rename_constants_apart_for_vars forbidden_constants [] = subs

theorem GroundSubstitution.rename_constants_apart_for_vars_constants_fresh {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] (subs : GroundSubstitution sig) (forbidden_constants : List sig.C) (vars : List sig.V) (v : sig.V) : v ∈ vars → ∀ (c : sig.C), c ∈ (subs.rename_constants_apart_for_vars forbidden_constants vars v).constants → ¬c ∈ forbidden_constants

def PreTrigger.rename_constants_apart {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] (trg : PreTrigger sig) (forbidden_constants : List sig.C) : PreTrigger sig

Equations

• trg.rename_constants_apart forbidden_constants = { rule := trg.rule, subs := trg.subs.rename_constants_apart_for_vars forbidden_constants trg.rule.body.vars.eraseDupsKeepRight }

theorem PreTrigger.rename_constants_apart_constants_fresh {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] (trg : PreTrigger sig) (forbidden_constants : List sig.C) (c : sig.C) : c ∈ List.flatMap GroundTerm.constants (List.map (trg.rename_constants_apart forbidden_constants).subs trg.rule.body.vars.eraseDupsKeepRight) → ¬c ∈ forbidden_constants