Validity of Functional Terms in the Chase #
Since for all the backtrackings we always require that Skolem function terms are "valid" in various ways, here we actually show that every term introduced in the chase is valid in this sense.
theorem
ChaseDerivation.term_ruleIds_valid
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{rules : RuleSet sig}
{cd : ChaseDerivation obs rules}
{node : ChaseNode obs rules}
(node_mem : node ∈ cd)
(rl : RuleList sig)
:
(∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ rules.rules) →
(∀ (t : GroundTerm sig), t ∈ cd.head.facts.terms → GroundTerm.skolem_ruleIds_valid rl t) →
∀ (t : GroundTerm sig), t ∈ node.facts.terms → GroundTerm.skolem_ruleIds_valid rl t
theorem
ChaseDerivation.trigger_ruleIds_valid_of_loaded
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{rules : RuleSet sig}
{cd : ChaseDerivation obs rules}
{node : ChaseNode obs rules}
(node_mem : node ∈ cd)
(rl : RuleList sig)
:
(∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ rules.rules) →
(∀ (t : GroundTerm sig), t ∈ cd.head.facts.terms → GroundTerm.skolem_ruleIds_valid rl t) →
∀ (trg : PreTrigger sig), trg.loaded node.facts → PreTrigger.skolem_ruleIds_valid rl trg
theorem
ChaseDerivation.term_disjIdx_valid_aux
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{rules : RuleSet sig}
{cd : ChaseDerivation obs rules}
{node : ChaseNode obs rules}
(node_mem : node ∈ cd)
(rl : RuleList sig)
:
(∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ rules.rules) →
∀ (h_head : ∀ (t : GroundTerm sig), t ∈ cd.head.facts.terms → GroundTerm.skolem_ruleIds_valid rl t),
(∀ (t : GroundTerm sig) (t_mem : t ∈ cd.head.facts.terms), GroundTerm.skolem_disjIdx_valid rl t ⋯) →
∀ (t : GroundTerm sig),
t ∈ node.facts.terms → ∀ (h : GroundTerm.skolem_ruleIds_valid rl t), GroundTerm.skolem_disjIdx_valid rl t h
theorem
ChaseDerivation.term_disjIdx_valid
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{rules : RuleSet sig}
{cd : ChaseDerivation obs rules}
{node : ChaseNode obs rules}
(node_mem : node ∈ cd)
(rl : RuleList sig)
(rl_rs_eq : ∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ rules.rules)
(head_ruleIds_valid : ∀ (t : GroundTerm sig), t ∈ cd.head.facts.terms → GroundTerm.skolem_ruleIds_valid rl t)
(head_valid : ∀ (t : GroundTerm sig) (t_mem : t ∈ cd.head.facts.terms), GroundTerm.skolem_disjIdx_valid rl t ⋯)
(t : GroundTerm sig)
(t_mem : t ∈ node.facts.terms)
:
theorem
ChaseDerivation.trigger_disjIdx_valid_of_loaded
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{rules : RuleSet sig}
{cd : ChaseDerivation obs rules}
{node : ChaseNode obs rules}
(node_mem : node ∈ cd)
(rl : RuleList sig)
(rl_rs_eq : ∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ rules.rules)
(head_ruleIds_valid : ∀ (t : GroundTerm sig), t ∈ cd.head.facts.terms → GroundTerm.skolem_ruleIds_valid rl t)
(head_valid : ∀ (t : GroundTerm sig) (t_mem : t ∈ cd.head.facts.terms), GroundTerm.skolem_disjIdx_valid rl t ⋯)
(trg : PreTrigger sig)
(trg_loaded : trg.loaded node.facts)
:
PreTrigger.skolem_disjIdx_valid rl trg ⋯
theorem
ChaseDerivation.term_rule_arity_valid_aux
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{rules : RuleSet sig}
{cd : ChaseDerivation obs rules}
{node : ChaseNode obs rules}
(node_mem : node ∈ cd)
(rl : RuleList sig)
:
(∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ rules.rules) →
∀ (h_head : ∀ (t : GroundTerm sig), t ∈ cd.head.facts.terms → GroundTerm.skolem_ruleIds_valid rl t),
(∀ (t : GroundTerm sig) (t_mem : t ∈ cd.head.facts.terms), GroundTerm.skolem_rule_arity_valid rl t ⋯) →
∀ (t : GroundTerm sig),
t ∈ node.facts.terms → ∀ (h : GroundTerm.skolem_ruleIds_valid rl t), GroundTerm.skolem_rule_arity_valid rl t h
theorem
ChaseDerivation.term_rule_arity_valid
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{rules : RuleSet sig}
{cd : ChaseDerivation obs rules}
{node : ChaseNode obs rules}
(node_mem : node ∈ cd)
(rl : RuleList sig)
(rl_rs_eq : ∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ rules.rules)
(head_ruleIds_valid : ∀ (t : GroundTerm sig), t ∈ cd.head.facts.terms → GroundTerm.skolem_ruleIds_valid rl t)
(head_valid : ∀ (t : GroundTerm sig) (t_mem : t ∈ cd.head.facts.terms), GroundTerm.skolem_rule_arity_valid rl t ⋯)
(t : GroundTerm sig)
(t_mem : t ∈ node.facts.terms)
:
theorem
ChaseDerivation.trigger_rule_arity_valid_of_loaded
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{rules : RuleSet sig}
{cd : ChaseDerivation obs rules}
{node : ChaseNode obs rules}
(node_mem : node ∈ cd)
(rl : RuleList sig)
(rl_rs_eq : ∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ rules.rules)
(head_ruleIds_valid : ∀ (t : GroundTerm sig), t ∈ cd.head.facts.terms → GroundTerm.skolem_ruleIds_valid rl t)
(head_valid : ∀ (t : GroundTerm sig) (t_mem : t ∈ cd.head.facts.terms), GroundTerm.skolem_rule_arity_valid rl t ⋯)
(trg : PreTrigger sig)
(trg_loaded : trg.loaded node.facts)
:
PreTrigger.skolem_rule_arity_valid rl trg ⋯
theorem
ChaseBranch.term_ruleIds_valid
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{kb : KnowledgeBase sig}
{cb : ChaseBranch obs kb}
{node : ChaseNode obs kb.rules}
(node_mem : node ∈ cb.toChaseDerivation)
(rl : RuleList sig)
:
theorem
ChaseBranch.trigger_ruleIds_valid_of_loaded
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{kb : KnowledgeBase sig}
{cb : ChaseBranch obs kb}
{node : ChaseNode obs kb.rules}
(node_mem : node ∈ cb.toChaseDerivation)
(rl : RuleList sig)
:
theorem
ChaseBranch.term_disjIdx_valid
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{kb : KnowledgeBase sig}
{cb : ChaseBranch obs kb}
{node : ChaseNode obs kb.rules}
(node_mem : node ∈ cb.toChaseDerivation)
(rl : RuleList sig)
(rl_rs_eq : ∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ kb.rules.rules)
(t : GroundTerm sig)
(t_mem : t ∈ node.facts.terms)
:
theorem
ChaseBranch.trigger_disjIdx_valid_of_loaded
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{kb : KnowledgeBase sig}
{cb : ChaseBranch obs kb}
{node : ChaseNode obs kb.rules}
(node_mem : node ∈ cb.toChaseDerivation)
(rl : RuleList sig)
(rl_rs_eq : ∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ kb.rules.rules)
(trg : PreTrigger sig)
(trg_loaded : trg.loaded node.facts)
:
PreTrigger.skolem_disjIdx_valid rl trg ⋯
theorem
ChaseBranch.term_rule_arity_valid
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{kb : KnowledgeBase sig}
{cb : ChaseBranch obs kb}
{node : ChaseNode obs kb.rules}
(node_mem : node ∈ cb.toChaseDerivation)
(rl : RuleList sig)
(rl_rs_eq : ∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ kb.rules.rules)
(t : GroundTerm sig)
(t_mem : t ∈ node.facts.terms)
:
theorem
ChaseBranch.trigger_rule_arity_valid_of_loaded
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : ObsoletenessCondition sig}
{kb : KnowledgeBase sig}
{cb : ChaseBranch obs kb}
{node : ChaseNode obs kb.rules}
(node_mem : node ∈ cb.toChaseDerivation)
(rl : RuleList sig)
(rl_rs_eq : ∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ kb.rules.rules)
(trg : PreTrigger sig)
(trg_loaded : trg.loaded node.facts)
:
PreTrigger.skolem_rule_arity_valid rl trg ⋯