Interaction of Backtrackings and Strict Constant Mappings on PreTrigger #
We merely lift GroundTerm.backtrackFacts_under_constant_mapping_subset_of_composing_with_subs to PreTrigger here.
theorem
PreTrigger.affected_rules_eq_of_same_skeleton
{sig : Signature}
[DecidableEq sig.C]
[DecidableEq sig.V]
[DecidableEq sig.P]
{trg trg2 : PreTrigger sig}
(same_skeleton : trg.same_skeleton trg2)
:
The affected rules for triggers with the PreTrigger.same_skeleton are the same.
theorem
PreTrigger.affected_rules_eq_of_composing_with_subs
{sig : Signature}
[DecidableEq sig.C]
[DecidableEq sig.V]
[DecidableEq sig.P]
{trg : PreTrigger sig}
(g : StrictConstantMapping sig)
:
trg.affected_rules_for_backtracking = { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs }.affected_rules_for_backtracking
Since a strict constant mapping does not change term structure, the affected rules of a trigger stay the same when a strict constant mapping is applied after the substitution.
theorem
PreTrigger.backtracking_under_constant_mapping_subset_of_composing_with_subs
{sig : Signature}
[DecidableEq sig.C]
[DecidableEq sig.V]
[DecidableEq sig.P]
[CustomBasicDatastructures.GetFreshInhabitant sig.C]
[Inhabited sig.C]
(trg : PreTrigger sig)
(g : StrictConstantMapping sig)
:
(∀ (d : sig.C), d ∈ List.flatMap Rule.constants trg.affected_rules_for_backtracking → g d = d) →
∃ (fresh_constant_remapping : StrictConstantMapping sig), (∀ (d : sig.C), ¬d ∈ trg.backtrackFacts.snd → fresh_constant_remapping d = d) ∧ (StrictConstantMapping.toConstantMapping fun (c : sig.C) =>
if c ∈ trg.backtrackFacts.snd then fresh_constant_remapping c else g c).apply_fact_set
(CustomBasicDatastructures.List.toSet trg.backtrackFacts.fst) ⊆ CustomBasicDatastructures.List.toSet
{ rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs }.backtrackFacts.fst ∧ List.map fresh_constant_remapping trg.backtrackFacts.snd = { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs }.backtrackFacts.snd