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.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.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

theorem GroundSubstitution.rename_constants_apart_for_vars_preserves_ruleId_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (subs : GroundSubstitution sig) (forbidden_constants : List sig.C) (vars : List sig.V) (rl : RuleList sig) (v : sig.V) : v ∈ vars → GroundTerm.skolem_ruleIds_valid rl (subs v) → GroundTerm.skolem_ruleIds_valid rl (subs.rename_constants_apart_for_vars forbidden_constants vars v)

theorem GroundSubstitution.rename_constants_apart_for_vars_preserves_disjIdx_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (subs : GroundSubstitution sig) (forbidden_constants : List sig.C) (vars : List sig.V) (rl : RuleList sig) (v : sig.V) (v_mem : v ∈ vars) (h : GroundTerm.skolem_ruleIds_valid rl (subs v)) : GroundTerm.skolem_disjIdx_valid rl (subs v) h → GroundTerm.skolem_disjIdx_valid rl (subs.rename_constants_apart_for_vars forbidden_constants vars v) ⋯

theorem GroundSubstitution.rename_constants_apart_for_vars_preserves_rule_arity_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (subs : GroundSubstitution sig) (forbidden_constants : List sig.C) (vars : List sig.V) (rl : RuleList sig) (v : sig.V) (v_mem : v ∈ vars) (h : GroundTerm.skolem_ruleIds_valid rl (subs v)) : GroundTerm.skolem_rule_arity_valid rl (subs v) h → GroundTerm.skolem_rule_arity_valid rl (subs.rename_constants_apart_for_vars forbidden_constants vars v) ⋯

def PreTrigger.rename_constants_apart {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [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.C] [DecidableEq sig.V] [DecidableEq sig.P] [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

theorem PreTrigger.rename_constants_apart_preserves_ruleId_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (trg : PreTrigger sig) (forbidden_constants : List sig.C) (rl : RuleList sig) : skolem_ruleIds_valid rl trg → skolem_ruleIds_valid rl (trg.rename_constants_apart forbidden_constants)

theorem PreTrigger.rename_constants_apart_preserves_disjIdx_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (trg : PreTrigger sig) (forbidden_constants : List sig.C) (rl : RuleList sig) (h : skolem_ruleIds_valid rl trg) : skolem_disjIdx_valid rl trg h → skolem_disjIdx_valid rl (trg.rename_constants_apart forbidden_constants) ⋯

theorem PreTrigger.rename_constants_apart_preserves_rule_arity_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (trg : PreTrigger sig) (forbidden_constants : List sig.C) (rl : RuleList sig) (h : skolem_ruleIds_valid rl trg) : skolem_rule_arity_valid rl trg h → skolem_rule_arity_valid rl (trg.rename_constants_apart forbidden_constants) ⋯