Theory IsaFoR_Term
section ‹Integration of \textsf{IsaFoR} Terms and the Knuth--Bendix Order›
text ‹
This theory implements the abstract interface for atoms and substitutions using
the \textsf{IsaFoR} library.
›
theory IsaFoR_Term
imports
Deriving.Derive
Ordered_Resolution_Prover.Abstract_Substitution
First_Order_Terms.Unification
First_Order_Terms.Subsumption
"HOL-Cardinals.Wellorder_Extension"
Open_Induction.Restricted_Predicates
Knuth_Bendix_Order.KBO
begin
hide_const (open) mgu
abbreviation subst_apply_literal ::
"('f, 'v) term literal ⇒ ('f, 'v, 'w) gsubst ⇒ ('f, 'w) term literal" (infixl "⋅lit" 60) where
"L ⋅lit σ ≡ map_literal (λA. A ⋅ σ) L"
definition subst_apply_clause ::
"('f, 'v) term clause ⇒ ('f, 'v, 'w) gsubst ⇒ ('f, 'w) term clause" (infixl "⋅cls" 60) where
"C ⋅cls σ = image_mset (λL. L ⋅lit σ) C"
abbreviation vars_lit :: "('f, 'v) term literal ⇒ 'v set" where
"vars_lit L ≡ vars_term (atm_of L)"
definition vars_clause :: "('f, 'v) term clause ⇒ 'v set" where
"vars_clause C = Union (set_mset (image_mset vars_lit C))"
definition vars_clause_list :: "('f, 'v) term clause list ⇒ 'v set" where
"vars_clause_list Cs = Union (vars_clause ` set Cs) "
definition vars_partitioned :: "('f,'v) term clause list ⇒ bool" where
"vars_partitioned Cs ⟷
(∀i < length Cs. ∀j < length Cs. i ≠ j ⟶ (vars_clause (Cs ! i) ∩ vars_clause (Cs ! j)) = {})"
lemma vars_clause_mono: "S ⊆# C ⟹ vars_clause S ⊆ vars_clause C"
unfolding vars_clause_def by auto
interpretation substitution_ops "(⋅)" Var "(∘⇩s)" .
lemma is_ground_atm_is_ground_on_var:
assumes "is_ground_atm (A ⋅ σ)" and "v ∈ vars_term A"
shows "is_ground_atm (σ v)"
using assms proof (induction A)
case (Var x)
then show ?case by auto
next
case (Fun f ts)
then show ?case unfolding is_ground_atm_def
by auto
qed
lemma is_ground_lit_is_ground_on_var:
assumes ground_lit: "is_ground_lit (subst_lit L σ)" and v_in_L: "v ∈ vars_lit L"
shows "is_ground_atm (σ v)"
proof -
let ?A = "atm_of L"
from v_in_L have A_p: "v ∈ vars_term ?A"
by auto
then have "is_ground_atm (?A ⋅ σ)"
using ground_lit unfolding is_ground_lit_def by auto
then show ?thesis
using A_p is_ground_atm_is_ground_on_var by metis
qed
lemma is_ground_cls_is_ground_on_var:
assumes
ground_clause: "is_ground_cls (subst_cls C σ)" and
v_in_C: "v ∈ vars_clause C"
shows "is_ground_atm (σ v)"
proof -
from v_in_C obtain L where L_p: "L ∈# C" "v ∈ vars_lit L"
unfolding vars_clause_def by auto
then have "is_ground_lit (subst_lit L σ)"
using ground_clause unfolding is_ground_cls_def subst_cls_def by auto
then show ?thesis
using L_p is_ground_lit_is_ground_on_var by metis
qed
lemma is_ground_cls_list_is_ground_on_var:
assumes ground_list: "is_ground_cls_list (subst_cls_list Cs σ)"
and v_in_Cs: "v ∈ vars_clause_list Cs"
shows "is_ground_atm (σ v)"
proof -
from v_in_Cs obtain C where C_p: "C ∈ set Cs" "v ∈ vars_clause C"
unfolding vars_clause_list_def by auto
then have "is_ground_cls (subst_cls C σ)"
using ground_list unfolding is_ground_cls_list_def subst_cls_list_def by auto
then show ?thesis
using C_p is_ground_cls_is_ground_on_var by metis
qed
lemma same_on_vars_lit:
assumes "∀v ∈ vars_lit L. σ v = τ v"
shows "subst_lit L σ = subst_lit L τ"
using assms
proof (induction L)
case (Pos x)
then have "∀v ∈ vars_term x. σ v = τ v ⟹ subst_atm_abbrev x σ = subst_atm_abbrev x τ"
using term_subst_eq by metis+
then show ?case
unfolding subst_lit_def using Pos by auto
next
case (Neg x)
then have "∀v ∈ vars_term x. σ v = τ v ⟹ subst_atm_abbrev x σ = subst_atm_abbrev x τ"
using term_subst_eq by metis+
then show ?case
unfolding subst_lit_def using Neg by auto
qed
lemma in_list_of_mset_in_S:
assumes "i < length (list_of_mset S)"
shows "list_of_mset S ! i ∈# S"
proof -
from assms have "list_of_mset S ! i ∈ set (list_of_mset S)"
by auto
then have "list_of_mset S ! i ∈# mset (list_of_mset S)"
by (meson in_multiset_in_set)
then show ?thesis
by auto
qed
lemma same_on_vars_clause:
assumes "∀v ∈ vars_clause S. σ v = τ v"
shows "subst_cls S σ = subst_cls S τ"
by (smt assms image_eqI image_mset_cong2 mem_simps(9) same_on_vars_lit set_image_mset
subst_cls_def vars_clause_def)