Theory SCL_FOL
theory SCL_FOL
imports
Main
"HOL-Library.FSet"
Saturation_Framework.Calculus
Saturation_Framework_Extensions.Clausal_Calculus
Ordered_Resolution_Prover.Clausal_Logic
Ordered_Resolution_Prover.Abstract_Substitution
Ordered_Resolution_Prover.Herbrand_Interpretation
First_Order_Terms.Subsumption
First_Order_Terms.Term
First_Order_Terms.Unification
Abstract_Renaming_Apart
Ordered_Resolution_Prover_Extra
begin
section ‹Extra Lemmas›
subsection ‹Set Extra›
lemma not_in_iff: "L ∉ xs ⟷ (∀y∈xs. L ≠ y)"
by auto
lemma disjoint_iff': "A ∩ B = {} ⟷ (∀a ∈ A. a ∉ B) ∧ (∀b ∈ B. b ∉ A)"
by blast
lemma set_filter_insert_conv:
"{x ∈ insert y S. P x} = (if P y then insert y else id) {x ∈ S. P x}"
by auto
lemma not_empty_if_mem: "x ∈ X ⟹ X ≠ {}"
by blast
subsection ‹Finite Set Extra›
lemma finite_induct' [case_names empty singleton insert_insert, induct set: finite]:
assumes "finite F"
assumes "P {}"
and singleton: "⋀x. P {x}"
and insert_insert: "⋀x y F. finite F ⟹ x ≠ y ⟹ x ∉ F ⟹ y ∉ F ⟹ P (insert y F) ⟹ P (insert x (insert y F))"
shows "P F"
using ‹finite F›
proof induct
show "P {}" by fact
next
fix x F
assume F: "finite F" and P: "P F"
thus "P (insert x F)"
proof (induction F rule: finite.induct)
case emptyI
show ?case by (rule singleton)
next
case (insertI F y)
show ?case
proof (cases "x = y")
case True
then show ?thesis
by (simp add: insertI.prems)
next
case x_neq_y: False
show ?thesis
proof (cases "x ∈ F ∨ y ∈ F")
case True
then show ?thesis
by (metis insertCI insertI.IH insertI.prems insert_absorb)
next
case False
show ?thesis
proof (rule insert_insert)
show "finite F" using insertI by simp
next
show "x ≠ y" by (rule x_neq_y)
next
show "x ∉ F" using False by simp
next
show "y ∉ F" using False by simp
next
show "P (insert y F)"
by (simp add: insertI.prems)
qed
qed
qed
qed
qed
subsection ‹Product Type Extra›
lemma insert_Times: "insert a A × B = Pair a ` B ∪ A × B"
by blast
lemma Times_insert: "A × insert b B = (λx. (x, b)) ` A ∪ A × B"
by blast
lemma insert_Times_insert':
"insert a A × insert b B = insert (a, b) ((Pair a ` B) ∪ ((λx. (x, b)) ` A) ∪ (A × B))"
(is "?lhs = ?rhs")
unfolding insert_Times_insert by auto
subsection ‹List Extra›
lemma lt_lengthD:
assumes i_lt_xs: "i < length xs"
shows "∃xs1 xi xs2. xs = xs1 @ xi # xs2 ∧ length xs1 = i"
using assms
by (metis Cons_nth_drop_Suc add_diff_cancel_left' add_diff_cancel_right'
canonically_ordered_monoid_add_class.lessE id_take_nth_drop length_append length_drop)
lemma lt_lt_lengthD:
assumes i_lt_xs: "i < length xs" and j_lt_xs: "j < length xs" and
i_lt_j: "i < j"
shows "∃xs1 xi xs2 xj xs3. xs = xs1 @ xi # xs2 @ xj # xs3 ∧ length xs1 = i ∧
length (xs1 @ xi # xs2) = j"
proof -
from i_lt_xs obtain xs1 xi xs' where "xs = xs1 @ xi # xs'" and "length xs1 = i"
using lt_lengthD by blast
with j_lt_xs obtain xs2 xj xs3 where "xs = xs1 @ xi # xs2 @ xj # xs3" and "length (xs1 @ xi # xs2) = j"
using lt_lengthD
by (smt (verit, del_insts) append.assoc append_Cons append_eq_append_conv i_lt_j list.inject)
thus ?thesis
using ‹length xs1 = i› by blast
qed
subsection ‹Sublist Extra›
lemma not_mem_strict_suffix:
shows "strict_suffix xs (y # ys) ⟹ y ∉ set ys ⟹ y ∉ set xs"
unfolding strict_suffix_def suffix_def
by (metis Cons_eq_append_conv Un_iff set_append)
lemma not_mem_strict_suffix':
shows "strict_suffix xs (y # ys) ⟹ f y ∉ f ` set ys ⟹ f y ∉ f ` set xs"
using not_mem_strict_suffix[of "map f xs" "f y" "map f ys", unfolded list.set_map]
using map_mono_strict_suffix[of _ "_ # _", unfolded list.map]
by fast
subsection ‹Multiset Extra›
lemma multp⇩D⇩M_implies_one_step:
"multp⇩D⇩M R M N ⟹ ∃I J K. N = I + J ∧ M = I + K ∧ J ≠ {#} ∧ (∀k∈#K. ∃x∈#J. R k x)"
unfolding multp⇩D⇩M_def
by (metis subset_mset.le_imp_diff_is_add)
lemma multp⇩H⇩O_implies_one_step:
"multp⇩H⇩O R M N ⟹ ∃I J K. N = I + J ∧ M = I + K ∧ J ≠ {#} ∧ (∀k∈#K. ∃x∈#J. R k x)"
by (metis multp⇩D⇩M_implies_one_step multp⇩H⇩O_imp_multp⇩D⇩M)
lemma Multiset_Bex_plus_iff: "(∃x ∈# (M1 + M2). P x) ⟷ (∃x ∈# M1. P x) ∨ (∃x ∈# M2. P x)"
by auto
lemma multp_singleton_rightD:
assumes "multp R M {#x#}" and "transp R"
shows "y ∈# M ⟹ R y x"
using multp_implies_one_step[OF ‹transp R› ‹multp R M {#x#}›]
by (metis add_cancel_left_left set_mset_single single_is_union singletonD)
subsubsection ‹Calculus Extra›
lemma (in consequence_relation) entails_one_formula: "N ⊨ U ⟹ D ∈ U ⟹ N ⊨ {D}"
using entail_set_all_formulas by blast
subsection ‹Clausal Calculus Extra›
subsubsection ‹Clausal Calculus Only›
lemma true_cls_iff_set_mset_eq: "set_mset C = set_mset D ⟹ I ⊫ C ⟷ I ⊫ D"
by (simp add: true_cls_def)
lemma true_clss_if_set_mset_eq: "(∀D ∈ 𝒟. ∃C ∈ 𝒞. set_mset D = set_mset C) ⟹ I ⊫s 𝒞 ⟹ I ⊫s 𝒟"
using true_cls_iff_set_mset_eq by (metis true_clss_def)
lemma entails_clss_insert: "N ⊫e insert C U ⟷ N ⊫e {C} ∧ N ⊫e U"
by auto
lemma Collect_lits_from_atms_conv: "{L. P (atm_of L)} = (⋃x ∈ {x. P x}. {Pos x, Neg x})"
(is "?lhs = ?rhs")
proof (rule Set.equalityI; rule Set.subsetI)
fix L
show "L ∈ ?lhs ⟹ L ∈ ?rhs"
by (cases L) simp_all
next
fix L
show "L ∈ ?rhs ⟹ L ∈ ?lhs"
by auto
qed
subsubsection ‹Clausal Calculus and Abstract Substitution›
lemma (in substitution) is_ground_lit_Pos[simp]: "is_ground_atm atm ⟹ is_ground_lit (Pos atm)"
by (simp add: is_ground_lit_def)
lemma (in substitution) is_ground_lit_Neg[simp]: "is_ground_atm atm ⟹ is_ground_lit (Neg atm)"
by (simp add: is_ground_lit_def)
subsection ‹First Order Terms Extra›
subsubsection ‹First Order Terms Only›
lemma atm_of_eq_uminus_if_lit_eq: "L = - K ⟹ atm_of L = atm_of K"
by (cases L; cases K) simp_all
lemma subst_subst_eq_subst_subst_if_subst_eq_substI:
assumes "t ⋅ σ = u ⋅ δ" and
t_inter_δ_empty: "vars_term t ∩ subst_domain δ = {}" and
u_inter_σ_empty: "vars_term u ∩ subst_domain σ = {}"
shows
"range_vars σ ∩ subst_domain δ = {} ⟹ t ⋅ σ ⋅ δ = u ⋅ σ ⋅ δ"
"range_vars δ ∩ subst_domain σ = {} ⟹ t ⋅ δ ⋅ σ = u ⋅ δ ⋅ σ"
proof -
from u_inter_σ_empty have "u ⋅ σ ⋅ δ = u ⋅ δ"
by (simp add: subst_apply_term_ident)
with ‹t ⋅ σ = u ⋅ δ› show "range_vars σ ∩ subst_domain δ = {} ⟹ t ⋅ σ ⋅ δ = u ⋅ σ ⋅ δ"
unfolding subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs[OF _ t_inter_δ_empty]
by simp
from t_inter_δ_empty have "t ⋅ δ ⋅ σ = t ⋅ σ"
by (simp add: subst_apply_term_ident)
with ‹t ⋅ σ = u ⋅ δ› show "range_vars δ ∩ subst_domain σ = {} ⟹ t ⋅ δ ⋅ σ = u ⋅ δ ⋅ σ"
unfolding subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs[OF _ u_inter_σ_empty]
by simp
qed
lemma subst_compose_in_unifiersI:
assumes "t ⋅ σ = u ⋅ δ" and
"vars_term t ∩ subst_domain δ = {}" and
"vars_term u ∩ subst_domain σ = {}"
shows
"range_vars σ ∩ subst_domain δ = {} ⟹ σ ∘⇩s δ ∈ unifiers {(t, u)}"
"range_vars δ ∩ subst_domain σ = {} ⟹ δ ∘⇩s σ ∈ unifiers {(t, u)}"
using subst_subst_eq_subst_subst_if_subst_eq_substI(1)[OF assms]
using subst_subst_eq_subst_subst_if_subst_eq_substI(2)[OF assms]
by (simp_all add: unifiers_def)
lemma subst_ident_if_not_in_domain: "x ∉ subst_domain μ ⟹ μ x = Var x"
by (simp add: subst_domain_def)
lemma "is_renaming (Var(x := Var x'))"
proof (unfold is_renaming_def, intro conjI allI)
fix y show "is_Var ((Var(x := Var x')) y)"
by simp
next
show "inj_on (Var(x := Var x')) (subst_domain (Var(x := Var x')))"
apply (rule inj_onI)
apply (simp add: subst_domain_def)
by presburger
qed
lemma ex_mgu_if_subst_eq_subst_and_disj_vars:
fixes t u :: "('f, 'v) Term.term" and σ⇩t σ⇩u :: "('f, 'v) subst"
assumes "t ⋅ σ⇩t = u ⋅ σ⇩u" and "vars_term t ∩ vars_term u = {}"
shows "∃μ :: ('f, 'v) subst. Unification.mgu t u = Some μ"
proof -
from assms obtain σ :: "('f, 'v) subst" where "t ⋅ σ = u ⋅ σ"
using vars_term_disjoint_imp_unifier by metis
thus ?thesis
using ex_mgu_if_subst_apply_term_eq_subst_apply_term
by metis
qed
lemma restrict_subst_domain_subst_composition:
fixes σ⇩A σ⇩B A B
assumes
distinct_domains: "A ∩ B = {}" and
distinct_range: "∀x ∈ A. vars_term (σ⇩A x) ∩ subst_domain σ⇩B = {}"
defines "σ ≡ restrict_subst_domain A σ⇩A ∘⇩s σ⇩B"
shows "x ∈ A ⟹ σ x = σ⇩A x" "x ∈ B ⟹ σ x = σ⇩B x"
proof -
assume "x ∈ A"
hence "restrict_subst_domain A σ⇩A x = σ⇩A x"
by (simp add: restrict_subst_domain_def)
moreover have "σ⇩A x ⋅ σ⇩B = σ⇩A x"
using distinct_range
by (simp add: ‹x ∈ A› subst_apply_term_ident)
ultimately show "σ x = σ⇩A x"
by (simp add: σ_def subst_compose_def)
next
assume "x ∈ B"
hence "restrict_subst_domain A σ⇩A x = Var x"
using distinct_domains
by (metis Int_iff empty_iff restrict_subst_domain_def)
then show "σ x = σ⇩B x"
by (simp add: σ_def subst_compose_def)
qed
lemma merge_substs_on_disjoint_domains:
fixes σ⇩A σ⇩B A B
assumes distinct_domains: "A ∩ B = {}"
defines "σ ≡ (λx. if x ∈ A then σ⇩A x else if x ∈ B then σ⇩B x else Var x)"
shows
"x ∈ A ⟹ σ x = σ⇩A x"
"x ∈ B ⟹ σ x = σ⇩B x"
"x ∉ A ∪ B ⟹ σ x = Var x"
proof -
show "x ∈ A ⟹ σ x = σ⇩A x"
by (simp add: σ_def)
next
assume "x ∈ B"
moreover hence "x ∉ A"
using distinct_domains by auto
ultimately show "σ x = σ⇩B x"
by (simp add: σ_def)
next
show "x ∉ A ∪ B ⟹ σ x = Var x"
by (simp add: σ_def)
qed
definition is_grounding_merge where
"is_grounding_merge γ A γ⇩A B γ⇩B ⟷
A ∩ B = {} ⟶ (∀x ∈ A. vars_term (γ⇩A x) = {}) ⟶ (∀x ∈ B. vars_term (γ⇩B x) = {}) ⟶
(∀x ∈ A. γ x = γ⇩A x) ∧ (∀x ∈ B. γ x = γ⇩B x)"
lemma is_grounding_merge_if_mem_then_else[simp]:
fixes γ⇩A γ⇩B A B
defines "γ ≡ (λx. if x ∈ A then γ⇩A x else γ⇩B x)"
shows "is_grounding_merge γ A γ⇩A B γ⇩B"
unfolding is_grounding_merge_def
by (auto simp: γ_def)
lemma is_grounding_merge_restrict_subst_domain_comp[simp]:
fixes γ⇩A γ⇩B A B
defines "γ ≡ restrict_subst_domain A γ⇩A ∘⇩s γ⇩B"
shows "is_grounding_merge γ A γ⇩A B γ⇩B"
unfolding is_grounding_merge_def
proof (intro impI)
assume disjoint: "A ∩ B = {}" and
ball_A_ground: "∀x∈A. vars_term (γ⇩A x) = {}" and
ball_B_ground: "∀x∈B. vars_term (γ⇩B x) = {}"
from ball_A_ground have "∀x∈A. vars_term (γ⇩A x) ∩ subst_domain γ⇩B = {}"
by simp
thus "(∀x∈A. γ x = γ⇩A x) ∧ (∀x∈B. γ x = γ⇩B x)"
using restrict_subst_domain_subst_composition[OF disjoint, of γ⇩A γ⇩B]
by (simp_all add: γ_def)
qed
subsubsection ‹First Order Terms And Abstract Substitution›
no_notation subst_apply_term (infixl "⋅" 67)
no_notation subst_compose (infixl "∘⇩s" 75)
global_interpretation substitution_ops subst_apply_term Var subst_compose .
notation subst_atm_abbrev (infixl "⋅a" 67)
notation subst_atm_list (infixl "⋅al" 67)
notation subst_lit (infixl "⋅l" 67)
notation subst_cls (infixl "⋅" 67)
notation subst_clss (infixl "⋅cs" 67)
notation subst_cls_list (infixl "⋅cl" 67)
notation subst_cls_lists (infixl "⋅⋅cl" 67)
notation comp_subst_abbrev (infixl "⊙" 67)
abbreviation vars_lit :: "('f, 'v) Term.term literal ⇒ 'v set" where
"vars_lit L ≡ vars_term (atm_of L)"
definition vars_cls :: "('f, 'v) term clause ⇒ 'v set" where
"vars_cls C = Union (set_mset (image_mset vars_lit C))"
definition vars_clss :: "('f, 'v) term clause set ⇒ 'v set" where
"vars_clss N = (⋃C ∈ N. vars_cls C)"
lemma vars_clss_empty[simp]: "vars_clss {} = {}"
by (simp add: vars_clss_def)
lemma vars_clss_insert[simp]: "vars_clss (insert C N) = vars_cls C ∪ vars_clss N"
by (simp add: vars_clss_def)
lemma vars_clss_union[simp]: "vars_clss (CC ∪ DD) = vars_clss CC ∪ vars_clss DD"
by (simp add: vars_clss_def)
lemma vars_cls_empty[simp]: "vars_cls {#} = {}"
unfolding vars_cls_def by simp
lemma finite_vars_cls[simp]: "finite (vars_cls C)"
unfolding vars_cls_def by simp
lemma vars_cls_plus_iff: "vars_cls (C + D) = vars_cls C ∪ vars_cls D"
unfolding vars_cls_def by simp
lemma vars_cls_subset_vars_cls_if_subset_mset: "C ⊆# D ⟹ vars_cls C ⊆ vars_cls D"
by (auto simp add: vars_cls_def)
lemma is_ground_atm_iff_vars_empty: "is_ground_atm t ⟷ vars_term t = {}"
by (metis (mono_tags, opaque_lifting) equals0D equals0I is_ground_atm_def subst_apply_term_empty
subst_def subst_simps(1) term.distinct(1) term_subst_eq term_subst_eq_rev)
lemma is_ground_lit_iff_vars_empty: "is_ground_lit L ⟷ vars_lit L = {}"
by (simp add: is_ground_atm_iff_vars_empty is_ground_lit_def)
lemma is_ground_cls_iff_vars_empty: "is_ground_cls C ⟷ vars_cls C = {}"
by (auto simp: is_ground_cls_def is_ground_lit_iff_vars_empty vars_cls_def)
lemma is_ground_atm_is_ground_on_var:
assumes "is_ground_atm (A ⋅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 ⋅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_cls C"
shows "is_ground_atm (σ v)"
proof -
from v_in_C obtain L where L_p: "L ∈# C" "v ∈ vars_lit L"
unfolding vars_cls_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 vars_atm_subset_subst_domain_if_grounding:
assumes "is_ground_atm (t ⋅a γ)"
shows "vars_term t ⊆ subst_domain γ"
using assms
by (metis empty_iff is_ground_atm_iff_vars_empty is_ground_atm_is_ground_on_var subsetI
subst_ident_if_not_in_domain term.set_intros(3))
lemma vars_lit_subset_subst_domain_if_grounding:
assumes "is_ground_lit (L ⋅l γ)"
shows "vars_lit L ⊆ subst_domain γ"
using assms vars_atm_subset_subst_domain_if_grounding
by (metis atm_of_subst_lit is_ground_lit_def)
lemma vars_cls_subset_subst_domain_if_grounding:
assumes "is_ground_cls (C ⋅ σ)"
shows "vars_cls C ⊆ subst_domain σ"
proof (rule Set.subsetI)
fix x assume "x ∈ vars_cls C"
thus "x ∈ subst_domain σ"
unfolding subst_domain_def mem_Collect_eq
by (metis assms empty_iff is_ground_atm_iff_vars_empty is_ground_cls_is_ground_on_var
term.set_intros(3))
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 same_on_vars_clause:
assumes "∀v ∈ vars_cls 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_cls_def)
lemma same_on_lits_clause:
assumes "∀L ∈# C. subst_lit L σ = subst_lit L τ"
shows "subst_cls C σ = subst_cls C τ"
using assms unfolding subst_cls_def
by simp