Interaction of Strict Constant Mappings and Renaming Constant Apart

For PreGroundTerm, GroundTerm, GroundSubstitution, and PreTrigger, we do the following things:

1. We define what it means for them to have the same_skeleton, which is the case if their only difference is the naming of constants in terms (but their structure is the same),
2. we show a few obvious implications of the definition in 1,
3. we show that applying a StrictConstantMapping yields something that has the same skeleton,
4. we show that for two things with the same skeleton, we can find a StrictConstantMapping that maps the renamed apart version of the first thing to the second one while mapping each constant to itself that does not occur in the renamed apart version,
5. we show that renaming constants apart does not change the skeleton.

def PreGroundTerm.same_skeleton {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (term term2 : PreGroundTerm sig) : Prop

Equations

• PreGroundTerm.same_skeleton (FiniteTree.leaf a) (FiniteTree.leaf a_1) = True
• PreGroundTerm.same_skeleton (FiniteTree.leaf a) (FiniteTree.inner a_1 a_2) = False
• PreGroundTerm.same_skeleton (FiniteTree.inner a a_1) (FiniteTree.leaf a_2) = False
• PreGroundTerm.same_skeleton (FiniteTree.inner a a_1) (FiniteTree.inner a_2 a_3) = (a = a_2 ∧ PreGroundTerm.same_skeleton_list a_1 a_3)

def PreGroundTerm.same_skeleton_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (terms terms2 : List (PreGroundTerm sig)) : Prop

Equations

• PreGroundTerm.same_skeleton_list [] [] = True
• PreGroundTerm.same_skeleton_list [] (head :: tail) = False
• PreGroundTerm.same_skeleton_list (head :: tail) [] = False
• PreGroundTerm.same_skeleton_list (head :: tail) (head_1 :: tail_1) = (head.same_skeleton head_1 ∧ PreGroundTerm.same_skeleton_list tail tail_1)

theorem PreGroundTerm.same_skeleton_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (term : PreGroundTerm sig) : term.same_skeleton term

theorem PreGroundTerm.same_skeleton_list_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (terms : List (PreGroundTerm sig)) : same_skeleton_list terms terms

theorem PreGroundTerm.same_skeleton_symm {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (term term2 : PreGroundTerm sig) : term.same_skeleton term2 → term2.same_skeleton term

theorem PreGroundTerm.same_skeleton_list_symm {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (terms terms2 : List (PreGroundTerm sig)) : same_skeleton_list terms terms2 → same_skeleton_list terms2 terms

theorem PreGroundTerm.same_skeleton_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (term term2 term3 : PreGroundTerm sig) : term.same_skeleton term2 → term2.same_skeleton term3 → term.same_skeleton term3

theorem PreGroundTerm.same_skeleton_list_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (terms terms2 terms3 : List (PreGroundTerm sig)) : same_skeleton_list terms terms2 → same_skeleton_list terms2 terms3 → same_skeleton_list terms terms3

theorem PreGroundTerm.innerLabels_eq_of_same_skeleton {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {term term2 : PreGroundTerm sig} (same_skel : term.same_skeleton term2) : FiniteTree.innerLabels term = FiniteTree.innerLabels term2

theorem PreGroundTerm.innerLabels_eq_of_same_skeleton_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {terms terms2 : List (PreGroundTerm sig)} (same_skel : same_skeleton_list terms terms2) : List.flatMap FiniteTree.innerLabels terms = List.flatMap FiniteTree.innerLabels terms2

theorem PreGroundTerm.same_skeleton_under_strict_constant_mapping {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (term : PreGroundTerm sig) (g : StrictConstantMapping sig) : term.same_skeleton (g.toConstantMapping.apply_pre_ground_term term)

theorem PreGroundTerm.same_skeleton_list_under_strict_constant_mapping {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (terms : List (PreGroundTerm sig)) (g : StrictConstantMapping sig) : same_skeleton_list terms (List.map g.toConstantMapping.apply_pre_ground_term terms)

theorem PreGroundTerm.exists_strict_constant_mapping_to_reverse_renaming {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] (term term2 : PreGroundTerm sig) (terms_same_skeleton : term.same_skeleton term2) (forbidden_constants : List sig.C) : ∃ (g : StrictConstantMapping sig), g.toConstantMapping.apply_pre_ground_term (term.rename_constants_apart forbidden_constants) = term2 ∧ ∀ (d : sig.C), ¬d ∈ FiniteTree.leaves (term.rename_constants_apart forbidden_constants) → g d = d

theorem PreGroundTerm.exists_strict_constant_mapping_to_reverse_renaming_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] (terms terms2 : List (PreGroundTerm sig)) (terms_same_skeleton : same_skeleton_list terms terms2) (forbidden_constants : List sig.C) : ∃ (g : StrictConstantMapping sig), List.map (fun (term : PreGroundTerm sig) => g.toConstantMapping.apply_pre_ground_term term) (rename_constants_apart.foldl_list terms forbidden_constants) = terms2 ∧ ∀ (d : sig.C), ¬d ∈ List.flatMap FiniteTree.leaves (rename_constants_apart.foldl_list terms forbidden_constants) → g d = d

theorem PreGroundTerm.same_skeleton_of_rename_constants_apart {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] {term : PreGroundTerm sig} {forbidden_constants : List sig.C} : (term.rename_constants_apart forbidden_constants).same_skeleton term

theorem PreGroundTerm.same_skeleton_of_rename_constants_apart_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] {terms : List (PreGroundTerm sig)} {forbidden_constants : List sig.C} : same_skeleton_list (rename_constants_apart.foldl_list terms forbidden_constants) terms

def GroundTerm.same_skeleton {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (term term2 : GroundTerm sig) : Prop

Equations

• term.same_skeleton term2 = term.val.same_skeleton term2.val

theorem GroundTerm.same_skeleton_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {c d : sig.C} : (const c).same_skeleton (const d)

theorem GroundTerm.same_skeleton_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (term : GroundTerm sig) : term.same_skeleton term

theorem GroundTerm.same_skeleton_symm {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (term term2 : GroundTerm sig) : term.same_skeleton term2 → term2.same_skeleton term

theorem GroundTerm.same_skeleton_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (term term2 term3 : GroundTerm sig) : term.same_skeleton term2 → term2.same_skeleton term3 → term.same_skeleton term3

theorem GroundTerm.functions_eq_of_same_skeleton {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {term term2 : GroundTerm sig} (same_skel : term.same_skeleton term2) : term.functions = term2.functions

theorem GroundTerm.rules_eq_of_same_skeleton {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {term term2 : GroundTerm sig} (same_skel : term.same_skeleton term2) : term.rules = term2.rules

theorem GroundTerm.same_skeleton_under_strict_constant_mapping {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (term : GroundTerm sig) (g : StrictConstantMapping sig) : term.same_skeleton (g.toConstantMapping.apply_ground_term term)

theorem GroundTerm.exists_strict_constant_mapping_to_reverse_renaming {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] (term term2 : GroundTerm sig) (terms_same_skeleton : term.same_skeleton term2) (forbidden_constants : List sig.C) : ∃ (g : StrictConstantMapping sig), g.toConstantMapping.apply_ground_term (term.rename_constants_apart forbidden_constants) = term2 ∧ ∀ (d : sig.C), ¬d ∈ (term.rename_constants_apart forbidden_constants).constants → g d = d

theorem GroundTerm.same_skeleton_of_rename_constants_apart {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] {term : GroundTerm sig} {forbidden_constants : List sig.C} : (term.rename_constants_apart forbidden_constants).same_skeleton term

def GroundSubstitution.same_skeleton_for_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (subs subs2 : GroundSubstitution sig) : List sig.V → Prop

Equations

• subs.same_skeleton_for_vars subs2 [] = True
• subs.same_skeleton_for_vars subs2 (hd :: tl) = ((subs hd).same_skeleton (subs2 hd) ∧ subs.same_skeleton_for_vars subs2 tl)

theorem GroundSubstitution.same_skeleton_for_vars_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (subs : GroundSubstitution sig) (vars : List sig.V) : subs.same_skeleton_for_vars subs vars

theorem GroundSubstitution.same_skeleton_for_vars_symm {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (subs subs2 : GroundSubstitution sig) (vars : List sig.V) : subs.same_skeleton_for_vars subs2 vars → subs2.same_skeleton_for_vars subs vars

theorem GroundSubstitution.same_skeleton_for_vars_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (subs subs2 subs3 : GroundSubstitution sig) (vars : List sig.V) : subs.same_skeleton_for_vars subs2 vars → subs2.same_skeleton_for_vars subs3 vars → subs.same_skeleton_for_vars subs3 vars

theorem GroundSubstitution.same_skeleton_of_mem_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {subs subs2 : GroundSubstitution sig} {vars : List sig.V} (same_skel : subs.same_skeleton_for_vars subs2 vars) {v : sig.V} (v_mem : v ∈ vars) : (subs v).same_skeleton (subs2 v)

theorem GroundSubstitution.same_skeleton_for_vars_under_strict_constant_mapping {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (subs : GroundSubstitution sig) (vars : List sig.V) (g : StrictConstantMapping sig) : subs.same_skeleton_for_vars (g.toConstantMapping.apply_ground_term ∘ subs) vars

theorem GroundSubstitution.exists_strict_constant_mapping_to_reverse_renaming_for_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] (subs subs2 : GroundSubstitution sig) (vars : List sig.V) (vars_nodup : vars.Nodup) (subs_same_skeleton : subs.same_skeleton_for_vars subs2 vars) (forbidden_constants : List sig.C) : ∃ (g : StrictConstantMapping sig), (∀ (v : sig.V), v ∈ vars → g.toConstantMapping.apply_ground_term (subs.rename_constants_apart_for_vars forbidden_constants vars v) = subs2 v) ∧ ∀ (d : sig.C), ¬d ∈ List.flatMap GroundTerm.constants (List.map (subs.rename_constants_apart_for_vars forbidden_constants vars) vars) → g d = d

theorem GroundSubstitution.same_skeleton_of_rename_constants_apart_for_each_var {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_mem : v ∈ vars) : (subs.rename_constants_apart_for_vars forbidden_constants vars v).same_skeleton (subs v)

theorem GroundSubstitution.same_skeleton_of_rename_constants_apart {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} : (subs.rename_constants_apart_for_vars forbidden_constants vars).same_skeleton_for_vars subs vars

def PreTrigger.same_skeleton {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg trg2 : PreTrigger sig) : Prop

Equations

• trg.same_skeleton trg2 = (trg.rule = trg2.rule ∧ trg.subs.same_skeleton_for_vars trg2.subs trg.rule.body.vars.eraseDupsKeepRight)

theorem PreTrigger.same_skeleton_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) : trg.same_skeleton trg

theorem PreTrigger.same_skeleton_symm {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg trg2 : PreTrigger sig) : trg.same_skeleton trg2 → trg2.same_skeleton trg

theorem PreTrigger.same_skeleton_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg trg2 trg3 : PreTrigger sig) : trg.same_skeleton trg2 → trg2.same_skeleton trg3 → trg.same_skeleton trg3

theorem PreTrigger.same_skeleton_under_strict_constant_mapping {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (g : StrictConstantMapping sig) : trg.same_skeleton { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs }

theorem PreTrigger.exists_strict_constant_mapping_to_reverse_renaming {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] (trg trg2 : PreTrigger sig) (trgs_same_skeleton : trg.same_skeleton trg2) (forbidden_constants : List sig.C) : ∃ (g : StrictConstantMapping sig), { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ (trg.rename_constants_apart forbidden_constants).subs }.strong_equiv trg2 ∧ ∀ (d : sig.C), ¬d ∈ List.flatMap GroundTerm.constants (List.map (trg.rename_constants_apart forbidden_constants).subs trg.rule.body.vars.eraseDupsKeepRight) → g d = d

theorem PreTrigger.same_skeleton_of_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} : (trg.rename_constants_apart forbidden_constants).same_skeleton trg