Theory FO_Ordered_Resolution
section ‹First-Order Ordered Resolution Calculus with Selection›
theory FO_Ordered_Resolution
imports Abstract_Substitution Ordered_Ground_Resolution Standard_Redundancy
begin
text ‹
This material is based on Section 4.3 (``A Simple Resolution Prover for First-Order Clauses'') of
Bachmair and Ganzinger's chapter. Specifically, it formalizes the ordered resolution calculus for
first-order standard clauses presented in Figure 4 and its related lemmas and theorems, including
soundness and Lemma 4.12 (the lifting lemma).
The following corresponds to pages 41--42 of Section 4.3, until Figure 5 and its explanation.
›
locale FO_resolution = mgu subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu
for
subst_atm :: "'a :: wellorder ⇒ 's ⇒ 'a" and
id_subst :: "'s" and
comp_subst :: "'s ⇒ 's ⇒ 's" and
renamings_apart :: "'a literal multiset list ⇒ 's list" and
atm_of_atms :: "'a list ⇒ 'a" and
mgu :: "'a set set ⇒ 's option" +
fixes
less_atm :: "'a ⇒ 'a ⇒ bool"
assumes
less_atm_stable: "less_atm A B ⟹ less_atm (A ⋅a σ) (B ⋅a σ)" and
less_atm_ground: "is_ground_atm A ⟹ is_ground_atm B ⟹ less_atm A B ⟹ A < B"
begin
subsection ‹Library›
lemma Bex_cartesian_product: "(∃xy ∈ A × B. P xy) ≡ (∃x ∈ A. ∃y ∈ B. P (x, y))"
by simp
lemma eql_map_neg_lit_eql_atm:
assumes "map (λL. L ⋅l η) (map Neg As') = map Neg As"
shows "As' ⋅al η = As"
using assms by (induction As' arbitrary: As) auto
lemma instance_list:
assumes "negs (mset As) = SDA' ⋅ η"
shows "∃As'. negs (mset As') = SDA' ∧ As' ⋅al η = As"
proof -
from assms have negL: "∀L ∈# SDA'. is_neg L"
using Melem_subst_cls subst_lit_in_negs_is_neg by metis
from assms have "{#L ⋅l η. L ∈# SDA'#} = mset (map Neg As)"
using subst_cls_def by auto
then have "∃NAs'. map (λL. L ⋅l η) NAs' = map Neg As ∧ mset NAs' = SDA'"
using image_mset_of_subset_list[of "λL. L ⋅l η" SDA' "map Neg As"] by auto
then obtain As' where As'_p:
"map (λL. L ⋅l η) (map Neg As') = map Neg As ∧ mset (map Neg As') = SDA'"
by (metis (no_types, lifting) Neg_atm_of_iff negL ex_map_conv set_mset_mset)
have "negs (mset As') = SDA'"
using As'_p by auto
moreover have "map (λL. L ⋅l η) (map Neg As') = map Neg As"
using As'_p by auto
then have "As' ⋅al η = As"
using eql_map_neg_lit_eql_atm by auto
ultimately show ?thesis
by blast
qed
lemma map2_add_mset_map:
assumes "length AAs' = n" and "length As' = n"
shows "map2 add_mset (As' ⋅al η) (AAs' ⋅aml η) = map2 add_mset As' AAs' ⋅aml η"
using assms
proof (induction n arbitrary: AAs' As')
case (Suc n)
then have "map2 add_mset (tl (As' ⋅al η)) (tl (AAs' ⋅aml η)) = map2 add_mset (tl As') (tl AAs') ⋅aml η"
by simp
moreover have Succ: "length (As' ⋅al η) = Suc n" "length (AAs' ⋅aml η) = Suc n"
using Suc(3) Suc(2) by auto
then have "length (tl (As' ⋅al η)) = n" "length (tl (AAs' ⋅aml η)) = n"
by auto
then have "length (map2 add_mset (tl (As' ⋅al η)) (tl (AAs' ⋅aml η))) = n"
"length (map2 add_mset (tl As') (tl AAs') ⋅aml η) = n"
using Suc(2,3) by auto
ultimately have "∀i < n. tl (map2 add_mset ( (As' ⋅al η)) ((AAs' ⋅aml η))) ! i =
tl (map2 add_mset (As') (AAs') ⋅aml η) ! i"
using Suc(2,3) Succ by (simp add: map2_tl map_tl subst_atm_mset_list_def del: subst_atm_list_tl)
moreover have nn: "length (map2 add_mset ((As' ⋅al η)) ((AAs' ⋅aml η))) = Suc n"
"length (map2 add_mset (As') (AAs') ⋅aml η) = Suc n"
using Succ Suc by auto
ultimately have "∀i. i < Suc n ⟶ i > 0 ⟶
map2 add_mset (As' ⋅al η) (AAs' ⋅aml η) ! i = (map2 add_mset As' AAs' ⋅aml η) ! i"
by (auto simp: subst_atm_mset_list_def gr0_conv_Suc subst_atm_mset_def)
moreover have "add_mset (hd As' ⋅a η) (hd AAs' ⋅am η) = add_mset (hd As') (hd AAs') ⋅am η"
unfolding subst_atm_mset_def by auto
then have "(map2 add_mset (As' ⋅al η) (AAs' ⋅aml η)) ! 0 = (map2 add_mset (As') (AAs') ⋅aml η) ! 0"
using Suc by (simp add: Succ(2) subst_atm_mset_def)
ultimately have "∀i < Suc n. (map2 add_mset (As' ⋅al η) (AAs' ⋅aml η)) ! i =
(map2 add_mset (As') (AAs') ⋅aml η) ! i"
using Suc by auto
then show ?case
using nn list_eq_iff_nth_eq by metis
qed auto
context
fixes S :: "'a clause ⇒ 'a clause"
begin
subsection ‹Calculus›
text ‹
The following corresponds to Figure 4.
›
definition maximal_wrt :: "'a ⇒ 'a literal multiset ⇒ bool" where
"maximal_wrt A C ⟷ (∀B ∈ atms_of C. ¬ less_atm A B)"
definition strictly_maximal_wrt :: "'a ⇒ 'a literal multiset ⇒ bool" where
"strictly_maximal_wrt A C ≡ ∀B ∈ atms_of C. A ≠ B ∧ ¬ less_atm A B"
lemma strictly_maximal_wrt_maximal_wrt: "strictly_maximal_wrt A C ⟹ maximal_wrt A C"
unfolding maximal_wrt_def strictly_maximal_wrt_def by auto
lemma maximal_wrt_subst: "maximal_wrt (A ⋅a σ) (C ⋅ σ) ⟹ maximal_wrt A C"
unfolding maximal_wrt_def using in_atms_of_subst less_atm_stable by blast
lemma strictly_maximal_wrt_subst:
"strictly_maximal_wrt (A ⋅a σ) (C ⋅ σ) ⟹ strictly_maximal_wrt A C"
unfolding strictly_maximal_wrt_def using in_atms_of_subst less_atm_stable by blast
inductive eligible :: "'s ⇒ 'a list ⇒ 'a clause ⇒ bool" where
eligible:
"S DA = negs (mset As) ∨ S DA = {#} ∧ length As = 1 ∧ maximal_wrt (As ! 0 ⋅a σ) (DA ⋅ σ) ⟹
eligible σ As DA"
inductive
ord_resolve
:: "'a clause list ⇒ 'a clause ⇒ 'a multiset list ⇒ 'a list ⇒ 's ⇒ 'a clause ⇒ bool"
where
ord_resolve:
"length CAs = n ⟹
length Cs = n ⟹
length AAs = n ⟹
length As = n ⟹
n ≠ 0 ⟹
(∀i < n. CAs ! i = Cs ! i + poss (AAs ! i)) ⟹
(∀i < n. AAs ! i ≠ {#}) ⟹
Some σ = mgu (set_mset ` set (map2 add_mset As AAs)) ⟹
eligible σ As (D + negs (mset As)) ⟹
(∀i < n. strictly_maximal_wrt (As ! i ⋅a σ) (Cs ! i ⋅ σ)) ⟹
(∀i < n. S (CAs ! i) = {#}) ⟹
ord_resolve CAs (D + negs (mset As)) AAs As σ ((∑⇩# (mset Cs) + D) ⋅ σ)"
inductive
ord_resolve_rename
:: "'a clause list ⇒ 'a clause ⇒ 'a multiset list ⇒ 'a list ⇒ 's ⇒ 'a clause ⇒ bool"
where
ord_resolve_rename:
"length CAs = n ⟹
length AAs = n ⟹
length As = n ⟹
(∀i < n. poss (AAs ! i) ⊆# CAs ! i) ⟹
negs (mset As) ⊆# DA ⟹
ρ = hd (renamings_apart (DA # CAs)) ⟹
ρs = tl (renamings_apart (DA # CAs)) ⟹
ord_resolve (CAs ⋅⋅cl ρs) (DA ⋅ ρ) (AAs ⋅⋅aml ρs) (As ⋅al ρ) σ E ⟹
ord_resolve_rename CAs DA AAs As σ E"
lemma ord_resolve_empty_main_prem: "¬ ord_resolve Cs {#} AAs As σ E"
by (simp add: ord_resolve.simps)
lemma ord_resolve_rename_empty_main_prem: "¬ ord_resolve_rename Cs {#} AAs As σ E"
by (simp add: ord_resolve_empty_main_prem ord_resolve_rename.simps)
subsection ‹Soundness›
text ‹
Soundness is not discussed in the chapter, but it is an important property.
›
lemma ord_resolve_ground_inst_sound:
assumes
res_e: "ord_resolve CAs DA AAs As σ E" and
cc_inst_true: "I ⊨m mset CAs ⋅cm σ ⋅cm η" and
d_inst_true: "I ⊨ DA ⋅ σ ⋅ η" and
ground_subst_η: "is_ground_subst η"
shows "I ⊨ E ⋅ η"
using res_e
proof (cases rule: ord_resolve.cases)
case (ord_resolve n Cs D)
note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and
aas_len = this(5) and as_len = this(6) and cas = this(8) and mgu = this(10) and
len = this(1)
have len: "length CAs = length As"
using as_len cas_len by auto
have "is_ground_subst (σ ⊙ η)"
using ground_subst_η by (rule is_ground_comp_subst)
then have cc_true: "I ⊨m mset CAs ⋅cm σ ⋅cm η" and d_true: "I ⊨ DA ⋅ σ ⋅ η"
using cc_inst_true d_inst_true by auto
from mgu have unif: "∀i < n. ∀A∈#AAs ! i. A ⋅a σ = As ! i ⋅a σ"
using mgu_unifier as_len aas_len by blast
show "I ⊨ E ⋅ η"
proof (cases "∀A ∈ set As. A ⋅a σ ⋅a η ∈ I")
case True
then have "¬ I ⊨ negs (mset As) ⋅ σ ⋅ η"
unfolding true_cls_def[of I] by auto
then have "I ⊨ D ⋅ σ ⋅ η"
using d_true da by auto
then show ?thesis
unfolding e by auto
next
case False
then obtain i where a_in_aa: "i < length CAs" and a_false: "(As ! i) ⋅a σ ⋅a η ∉ I"
using da len by (metis in_set_conv_nth)
define C where "C ≡ Cs ! i"
define BB where "BB ≡ AAs ! i"
have c_cf': "C ⊆# ∑⇩# (mset CAs)"
unfolding C_def using a_in_aa cas cas_len
by (metis less_subset_eq_Union_mset mset_subset_eq_add_left subset_mset.trans)
have c_in_cc: "C + poss BB ∈# mset CAs"
using C_def BB_def a_in_aa cas_len in_set_conv_nth cas by fastforce
{
fix B
assume "B ∈# BB"
then have "B ⋅a σ = (As ! i) ⋅a σ"
using unif a_in_aa cas_len unfolding BB_def by auto
}
then have "¬ I ⊨ poss BB ⋅ σ ⋅ η"
using a_false by (auto simp: true_cls_def)
moreover have "I ⊨ (C + poss BB) ⋅ σ ⋅ η"
using c_in_cc cc_true true_cls_mset_true_cls[of I "mset CAs ⋅cm σ ⋅cm η"] by force
ultimately have "I ⊨ C ⋅ σ ⋅ η"
by simp
then show ?thesis
unfolding e subst_cls_union using c_cf' C_def a_in_aa cas_len cs_len
by (metis (no_types, lifting) mset_subset_eq_add_left nth_mem_mset set_mset_mono sum_mset.remove true_cls_mono subst_cls_mono)
qed
qed
text ‹
The previous lemma is not only used to prove soundness, but also the following lemma which is
used to prove Lemma 4.10.
›
lemma ord_resolve_rename_ground_inst_sound:
assumes
"ord_resolve_rename CAs DA AAs As σ E" and
"ρs = tl (renamings_apart (DA # CAs))" and
"ρ = hd (renamings_apart (DA # CAs))" and
"I ⊨m (mset (CAs ⋅⋅cl ρs)) ⋅cm σ ⋅cm η" and
"I ⊨ DA ⋅ ρ ⋅ σ ⋅ η" and
"is_ground_subst η"
shows "I ⊨ E ⋅ η"
using assms by (cases rule: ord_resolve_rename.cases) (fast intro: ord_resolve_ground_inst_sound)
text ‹
Here follows the soundness theorem for the resolution rule.
›
theorem ord_resolve_sound:
assumes
res_e: "ord_resolve CAs DA AAs As σ E" and
cc_d_true: "⋀σ. is_ground_subst σ ⟹ I ⊨m (mset CAs + {#DA#}) ⋅cm σ" and
ground_subst_η: "is_ground_subst η"
shows "I ⊨ E ⋅ η"
proof (use res_e in ‹cases rule: ord_resolve.cases›)
case (ord_resolve n Cs D)
note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4)
and aas_len = this(5) and as_len = this(6) and cas = this(8) and mgu = this(10)
have ground_subst_σ_η: "is_ground_subst (σ ⊙ η)"
using ground_subst_η by (rule is_ground_comp_subst)
have cas_true: "I ⊨m mset CAs ⋅cm σ ⋅cm η"
using cc_d_true ground_subst_σ_η by fastforce
have da_true: "I ⊨ DA ⋅ σ ⋅ η"
using cc_d_true ground_subst_σ_η by fastforce
show "I ⊨ E ⋅ η"
using ord_resolve_ground_inst_sound[OF res_e cas_true da_true] ground_subst_η by auto
qed
lemma subst_sound:
assumes
"⋀σ. is_ground_subst σ ⟹ I ⊨ C ⋅ σ" and
"is_ground_subst η"
shows "I ⊨ C ⋅ ρ ⋅ η"
using assms is_ground_comp_subst subst_cls_comp_subst by metis
lemma subst_sound_scl:
assumes
len: "length P = length CAs" and
true_cas: "⋀σ. is_ground_subst σ ⟹ I ⊨m mset CAs ⋅cm σ" and
ground_subst_η: "is_ground_subst η"
shows "I ⊨m mset (CAs ⋅⋅cl P) ⋅cm η"
proof -
from true_cas have "⋀CA. CA∈# mset CAs ⟹ (⋀σ. is_ground_subst σ ⟹ I ⊨ CA ⋅ σ)"
unfolding true_cls_mset_def by force
then have "∀i < length CAs. ∀σ. is_ground_subst σ ⟶ (I ⊨ CAs ! i ⋅ σ)"
using in_set_conv_nth by auto
then have true_cp: "∀i < length CAs. ∀σ. is_ground_subst σ ⟶ I ⊨ CAs ! i ⋅ P ! i ⋅ σ"
using subst_sound len by auto
{
fix CA
assume "CA ∈# mset (CAs ⋅⋅cl P)"
then obtain i where
i_x: "i < length (CAs ⋅⋅cl P)" "CA = (CAs ⋅⋅cl P) ! i"
by (metis in_mset_conv_nth)
then have "∀σ. is_ground_subst σ ⟶ I ⊨ CA ⋅ σ"
using true_cp unfolding subst_cls_lists_def by (simp add: len)
}
then show ?thesis
using assms unfolding true_cls_mset_def by auto
qed
text ‹
Here follows the soundness theorem for the resolution rule with renaming.
›
lemma ord_resolve_rename_sound:
assumes
res_e: "ord_resolve_rename CAs DA AAs As σ E" and
cc_d_true: "⋀σ. is_ground_subst σ ⟹ I ⊨m ((mset CAs) + {#DA#}) ⋅cm σ" and
ground_subst_η: "is_ground_subst η"
shows "I ⊨ E ⋅ η"
using res_e
proof (cases rule: ord_resolve_rename.cases)
case (ord_resolve_rename n ρ ρs)
note ρs = this(7) and res = this(8)
have len: "length ρs = length CAs"
using ρs renamings_apart_length by auto
have "⋀σ. is_ground_subst σ ⟹ I ⊨m (mset (CAs ⋅⋅cl ρs) + {#DA ⋅ ρ#}) ⋅cm σ"
using subst_sound_scl[OF len, of I] subst_sound cc_d_true by auto
then show "I ⊨ E ⋅ η"
using ground_subst_η ord_resolve_sound[OF res] by simp
qed
subsection ‹Other Basic Properties›
lemma ord_resolve_unique:
assumes
"ord_resolve CAs DA AAs As σ E" and
"ord_resolve CAs DA AAs As σ' E'"
shows "σ = σ' ∧ E = E'"
using assms
proof (cases rule: ord_resolve.cases[case_product ord_resolve.cases], intro conjI)
case (ord_resolve_ord_resolve CAs n Cs AAs As σ'' DA CAs' n' Cs' AAs' As' σ''' DA')
note res = this(1-17) and res' = this(18-34)
show σ: "σ = σ'"
using res(3-5,14) res'(3-5,14) by (metis option.inject)
have "Cs = Cs'"
using res(1,3,7,8,12) res'(1,3,7,8,12) by (metis add_right_imp_eq nth_equalityI)
moreover have "DA = DA'"
using res(2,4) res'(2,4) by fastforce
ultimately show "E = E'"
using res(5,6) res'(5,6) σ by blast
qed
lemma ord_resolve_rename_unique:
assumes
"ord_resolve_rename CAs DA AAs As σ E" and
"ord_resolve_rename CAs DA AAs As σ' E'"
shows "σ = σ' ∧ E = E'"
using assms unfolding ord_resolve_rename.simps using ord_resolve_unique by meson
lemma ord_resolve_max_side_prems: "ord_resolve CAs DA AAs As σ E ⟹ length CAs ≤ size DA"
by (auto elim!: ord_resolve.cases)
lemma ord_resolve_rename_max_side_prems:
"ord_resolve_rename CAs DA AAs As σ E ⟹ length CAs ≤ size DA"
by (elim ord_resolve_rename.cases, drule ord_resolve_max_side_prems, simp add: renamings_apart_length)
subsection ‹Inference System›
definition ord_FO_Γ :: "'a inference set" where
"ord_FO_Γ = {Infer (mset CAs) DA E | CAs DA AAs As σ E. ord_resolve_rename CAs DA AAs As σ E}"
interpretation ord_FO_resolution: inference_system ord_FO_Γ .
lemma finite_ord_FO_resolution_inferences_between:
assumes fin_cc: "finite CC"
shows "finite (ord_FO_resolution.inferences_between CC C)"
proof -
let ?CCC = "CC ∪ {C}"
define all_AA where "all_AA = (⋃D ∈ ?CCC. atms_of D)"
define max_ary where "max_ary = Max (size ` ?CCC)"
define CAS where "CAS = {CAs. CAs ∈ lists ?CCC ∧ length CAs ≤ max_ary}"
define AS where "AS = {As. As ∈ lists all_AA ∧ length As ≤ max_ary}"
define AAS where "AAS = {AAs. AAs ∈ lists (mset ` AS) ∧ length AAs ≤ max_ary}"
note defs = all_AA_def max_ary_def CAS_def AS_def AAS_def
let ?infer_of =
"λCAs DA AAs As. Infer (mset CAs) DA (THE E. ∃σ. ord_resolve_rename CAs DA AAs As σ E)"
let ?Z = "{γ | CAs DA AAs As σ E γ. γ = Infer (mset CAs) DA E
∧ ord_resolve_rename CAs DA AAs As σ E ∧ infer_from ?CCC γ ∧ C ∈# prems_of γ}"
let ?Y = "{Infer (mset CAs) DA E | CAs DA AAs As σ E.
ord_resolve_rename CAs DA AAs As σ E ∧ set CAs ∪ {DA} ⊆ ?CCC}"
let ?X = "{?infer_of CAs DA AAs As | CAs DA AAs As. CAs ∈ CAS ∧ DA ∈ ?CCC ∧ AAs ∈ AAS ∧ As ∈ AS}"
let ?W = "CAS × ?CCC × AAS × AS"
have fin_w: "finite ?W"
unfolding defs using fin_cc by (simp add: finite_lists_length_le lists_eq_set)
have "?Z ⊆ ?Y"
by (force simp: infer_from_def)
also have "… ⊆ ?X"
proof -
{
fix CAs DA AAs As σ E
assume
res_e: "ord_resolve_rename CAs DA AAs As σ E" and
da_in: "DA ∈ ?CCC" and
cas_sub: "set CAs ⊆ ?CCC"
have "E = (THE E. ∃σ. ord_resolve_rename CAs DA AAs As σ E)
∧ CAs ∈ CAS ∧ AAs ∈ AAS ∧ As ∈ AS" (is "?e ∧ ?cas ∧ ?aas ∧ ?as")
proof (intro conjI)
show ?e
using res_e ord_resolve_rename_unique by (blast intro: the_equality[symmetric])
next
show ?cas
unfolding CAS_def max_ary_def using cas_sub
ord_resolve_rename_max_side_prems[OF res_e] da_in fin_cc
by (auto simp add: Max_ge_iff)
next
show ?aas
using res_e
proof (cases rule: ord_resolve_rename.cases)
case (ord_resolve_rename n ρ ρs)
note len_cas = this(1) and len_aas = this(2) and len_as = this(3) and
aas_sub = this(4) and as_sub = this(5) and res_e' = this(8)
show ?thesis
unfolding AAS_def
proof (clarify, intro conjI)
show "AAs ∈ lists (mset ` AS)"
unfolding AS_def image_def
proof clarsimp
fix AA
assume "AA ∈ set AAs"
then obtain i where
i_lt: "i < n" and
aa: "AA = AAs ! i"
by (metis in_set_conv_nth len_aas)
have casi_in: "CAs ! i ∈ ?CCC"
using i_lt len_cas cas_sub nth_mem by blast
have pos_aa_sub: "poss AA ⊆# CAs ! i"
using aa aas_sub i_lt by blast
then have "set_mset AA ⊆ atms_of (CAs ! i)"
by (metis atms_of_poss lits_subseteq_imp_atms_subseteq set_mset_mono)
also have aa_sub: "… ⊆ all_AA"
unfolding all_AA_def using casi_in by force
finally have aa_sub: "set_mset AA ⊆ all_AA"
.
have "size AA = size (poss AA)"
by simp
also have "… ≤ size (CAs ! i)"
by (rule size_mset_mono[OF pos_aa_sub])
also have "… ≤ max_ary"
unfolding max_ary_def using fin_cc casi_in by auto
finally have sz_aa: "size AA ≤ max_ary"
.
let ?As' = "sorted_list_of_multiset AA"
have "?As' ∈ lists all_AA"
using aa_sub by auto
moreover have "length ?As' ≤ max_ary"
using sz_aa by simp
moreover have "AA = mset ?As'"
by simp
ultimately show "∃xa. xa ∈ lists all_AA ∧ length xa ≤ max_ary ∧ AA = mset xa"
by blast
qed
next
have "length AAs = length As"
unfolding len_aas len_as ..
also have "… ≤ size DA"
using as_sub size_mset_mono by fastforce
also have "… ≤ max_ary"
unfolding max_ary_def using fin_cc da_in by auto
finally show "length AAs ≤ max_ary"
.
qed
qed
next
show ?as
unfolding AS_def
proof (clarify, intro conjI)
have "set As ⊆ atms_of DA"
using res_e[simplified ord_resolve_rename.simps]
by (metis atms_of_negs lits_subseteq_imp_atms_subseteq set_mset_mono set_mset_mset)
also have "… ⊆ all_AA"
unfolding all_AA_def using da_in by blast
finally show "As ∈ lists all_AA"
unfolding lists_eq_set by simp
next
have "length As ≤ size DA"
using res_e[simplified ord_resolve_rename.simps]
ord_resolve_rename_max_side_prems[OF res_e] by auto
also have "size DA ≤ max_ary"
unfolding max_ary_def using fin_cc da_in by auto
finally show "length As ≤ max_ary"
.
qed
qed
}
then show ?thesis
by simp fast
qed
also have "… ⊆ (λ(CAs, DA, AAs, As). ?infer_of CAs DA AAs As) ` ?W"
unfolding image_def Bex_cartesian_product by fast
finally show ?thesis
unfolding inference_system.inferences_between_def ord_FO_Γ_def mem_Collect_eq
by (fast intro: rev_finite_subset[OF finite_imageI[OF fin_w]])
qed
lemma ord_FO_resolution_inferences_between_empty_empty:
"ord_FO_resolution.inferences_between {} {#} = {}"
unfolding ord_FO_resolution.inferences_between_def inference_system.inferences_between_def
infer_from_def ord_FO_Γ_def
using ord_resolve_rename_empty_main_prem by auto
subsection ‹Lifting›
text ‹
The following corresponds to the passage between Lemmas 4.11 and 4.12.
›
context
fixes M :: "'a clause set"
assumes select: "selection S"
begin
interpretation selection
by (rule select)
definition S_M :: "'a literal multiset ⇒ 'a literal multiset" where
"S_M C =
(if C ∈ grounding_of_clss M then
(SOME C'. ∃D σ. D ∈ M ∧ C = D ⋅ σ ∧ C' = S D ⋅ σ ∧ is_ground_subst σ)
else
S C)"
lemma S_M_grounding_of_clss:
assumes "C ∈ grounding_of_clss M"
obtains D σ where
"D ∈ M ∧ C = D ⋅ σ ∧ S_M C = S D ⋅ σ ∧ is_ground_subst σ"
proof (atomize_elim, unfold S_M_def eqTrueI[OF assms] if_True, rule someI_ex)
from assms show "∃C' D σ. D ∈ M ∧ C = D ⋅ σ ∧ C' = S D ⋅ σ ∧ is_ground_subst σ"
by (auto simp: grounding_of_clss_def grounding_of_cls_def)
qed
lemma S_M_not_grounding_of_clss: "C ∉ grounding_of_clss M ⟹ S_M C = S C"
unfolding S_M_def by simp
lemma S_M_selects_subseteq: "S_M C ⊆# C"
by (metis S_M_grounding_of_clss S_M_not_grounding_of_clss S_selects_subseteq subst_cls_mono_mset)
lemma S_M_selects_neg_lits: "L ∈# S_M C ⟹ is_neg L"
by (metis Melem_subst_cls S_M_grounding_of_clss S_M_not_grounding_of_clss S_selects_neg_lits
subst_lit_is_neg)
end
end
text ‹
The following corresponds to Lemma 4.12:
›
lemma ground_resolvent_subset:
assumes
gr_cas: "is_ground_cls_list CAs" and
gr_da: "is_ground_cls DA" and
res_e: "ord_resolve S CAs DA AAs As σ E"
shows "E ⊆# ∑⇩# (mset CAs) + DA"
using res_e
proof (cases rule: ord_resolve.cases)
case (ord_resolve n Cs D)
note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4)
and aas_len = this(5) and as_len = this(6) and cas = this(8) and mgu = this(10)
then have cs_sub_cas: "∑⇩# (mset Cs) ⊆# ∑⇩# (mset CAs)"
using subseteq_list_Union_mset cas_len cs_len by force
then have cs_sub_cas: "∑⇩# (mset Cs) ⊆# ∑⇩# (mset CAs)"
using subseteq_list_Union_mset cas_len cs_len by force
then have gr_cs: "is_ground_cls_list Cs"
using gr_cas by simp
have d_sub_da: "D ⊆# DA"
by (simp add: da)
then have gr_d: "is_ground_cls D"
using gr_da is_ground_cls_mono by auto
have "is_ground_cls (∑⇩# (mset Cs) + D)"
using gr_cs gr_d by auto
with e have "E = ∑⇩# (mset Cs) + D"
by auto
then show ?thesis
using cs_sub_cas d_sub_da by (auto simp: subset_mset.add_mono)
qed
lemma ord_resolve_obtain_clauses:
assumes
res_e: "ord_resolve (S_M S M) CAs DA AAs As σ E" and
select: "selection S" and
grounding: "{DA} ∪ set CAs ⊆ grounding_of_clss M" and
n: "length CAs = n" and
d: "DA = D + negs (mset As)" and
c: "(∀i < n. CAs ! i = Cs ! i + poss (AAs ! i))" "length Cs = n" "length AAs = n"
obtains DA0 η0 CAs0 ηs0 As0 AAs0 D0 Cs0 where
"length CAs0 = n"
"length ηs0 = n"
"DA0 ∈ M"
"DA0 ⋅ η0 = DA"
"S DA0 ⋅ η0 = S_M S M DA"
"∀CA0 ∈ set CAs0. CA0 ∈ M"
"CAs0 ⋅⋅cl ηs0 = CAs"
"map S CAs0 ⋅⋅cl ηs0 = map (S_M S M) CAs"
"is_ground_subst η0"
"is_ground_subst_list ηs0"
"As0 ⋅al η0 = As"
"AAs0 ⋅⋅aml ηs0 = AAs"
"length As0 = n"
"D0 ⋅ η0 = D"
"DA0 = D0 + (negs (mset As0))"
"S_M S M (D + negs (mset As)) ≠ {#} ⟹ negs (mset As0) = S DA0"
"length Cs0 = n"
"Cs0 ⋅⋅cl ηs0 = Cs"
"∀i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)"
"length AAs0 = n"
using res_e
proof (cases rule: ord_resolve.cases)
case (ord_resolve n_twin Cs_twins D_twin)
note da = this(1) and e = this(2) and cas = this(8) and mgu = this(10) and eligible = this(11)
from ord_resolve have "n_twin = n" "D_twin = D"
using n d by auto
moreover have "Cs_twins = Cs"
using c cas n calculation(1) ‹length Cs_twins = n_twin› by (auto simp add: nth_equalityI)
ultimately
have nz: "n ≠ 0" and cs_len: "length Cs = n" and aas_len: "length AAs = n" and as_len: "length As = n"
and da: "DA = D + negs (mset As)" and eligible: "eligible (S_M S M) σ As (D + negs (mset As))"
and cas: "∀i<n. CAs ! i = Cs ! i + poss (AAs ! i)"
using ord_resolve by force+
note n = ‹n ≠ 0› ‹length CAs = n› ‹length Cs = n› ‹length AAs = n› ‹length As = n›
interpret S: selection S by (rule select)
have "∀CA ∈ set CAs. ∃CA0 ηc0. CA0 ∈ M ∧ CA0 ⋅ ηc0 = CA ∧ S CA0 ⋅ ηc0 = S_M S M CA ∧ is_ground_subst ηc0"
using grounding S_M_grounding_of_clss select by (metis (no_types) le_supE subset_iff)
then have "∀i < n. ∃CA0 ηc0. CA0 ∈ M ∧ CA0 ⋅ ηc0 = (CAs ! i) ∧ S CA0 ⋅ ηc0 = S_M S M (CAs ! i) ∧ is_ground_subst ηc0"
using n by force
then obtain ηs0f CAs0f where f_p:
"∀i < n. CAs0f i ∈ M"
"∀i < n. (CAs0f i) ⋅ (ηs0f i) = (CAs ! i)"
"∀i < n. S (CAs0f i) ⋅ (ηs0f i) = S_M S M (CAs ! i)"
"∀i < n. is_ground_subst (ηs0f i)"
using n by (metis (no_types))
define ηs0 where
"ηs0 = map ηs0f [0 ..<n]"
define CAs0 where
"CAs0 = map CAs0f [0 ..<n]"
have "length ηs0 = n" "length CAs0 = n"
unfolding ηs0_def CAs0_def by auto
note n = ‹length ηs0 = n› ‹length CAs0 = n› n
have CAs0_in_M: "∀CA0 ∈ set CAs0. CA0 ∈ M"
unfolding CAs0_def using f_p(1) by auto
have CAs0_to_CAs: "CAs0 ⋅⋅cl ηs0 = CAs"
unfolding CAs0_def ηs0_def using f_p(2) by (auto simp: n intro: nth_equalityI)
have SCAs0_to_SMCAs: "(map S CAs0) ⋅⋅cl ηs0 = map (S_M S M) CAs"
unfolding CAs0_def ηs0_def using f_p(3) n by (force intro: nth_equalityI)
have sub_ground: "∀ηc0 ∈ set ηs0. is_ground_subst ηc0"
unfolding ηs0_def using f_p n by force
then have "is_ground_subst_list ηs0"
using n unfolding is_ground_subst_list_def by auto
obtain AAs0 Cs0 where AAs0_Cs0_p:
"AAs0 ⋅⋅aml ηs0 = AAs" "length Cs0 = n" "Cs0 ⋅⋅cl ηs0 = Cs"
"∀i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)" "length AAs0 = n"
proof -
have "∀i < n. ∃AA0. AA0 ⋅am ηs0 ! i = AAs ! i ∧ poss AA0 ⊆# CAs0 ! i"
proof (rule, rule)
fix i
assume "i < n"
have "CAs0 ! i ⋅ ηs0 ! i = CAs ! i"
using ‹i < n› ‹CAs0 ⋅⋅cl ηs0 = CAs› n by force
moreover have "poss (AAs ! i) ⊆# CAs !i"
using ‹i < n› cas by auto
ultimately obtain poss_AA0 where
nn: "poss_AA0 ⋅ ηs0 ! i = poss (AAs ! i) ∧ poss_AA0 ⊆# CAs0 ! i"
using cas image_mset_of_subset unfolding subst_cls_def by metis
then have l: "∀L ∈# poss_AA0. is_pos L"
unfolding subst_cls_def by (metis Melem_subst_cls imageE literal.disc(1)
literal.map_disc_iff set_image_mset subst_cls_def subst_lit_def)
define AA0 where
"AA0 = image_mset atm_of poss_AA0"
have na: "poss AA0 = poss_AA0"
using l unfolding AA0_def by auto
then have "AA0 ⋅am ηs0 ! i = AAs ! i"
using nn by (metis (mono_tags) literal.inject(1) multiset.inj_map_strong subst_cls_poss)
moreover have "poss AA0 ⊆# CAs0 ! i"
using na nn by auto
ultimately show "∃AA0. AA0 ⋅am ηs0 ! i = AAs ! i ∧ poss AA0 ⊆# CAs0 ! i"
by blast
qed
then obtain AAs0f where
AAs0f_p: "∀i < n. AAs0f i ⋅am ηs0 ! i = AAs ! i ∧ (poss (AAs0f i)) ⊆# CAs0 ! i"
by metis
define AAs0 where "AAs0 = map AAs0f [0 ..<n]"
then have "length AAs0 = n"
by auto
note n = n ‹length AAs0 = n›
from AAs0_def have "∀i < n. AAs0 ! i ⋅am ηs0 ! i = AAs ! i"
using AAs0f_p by auto
then have AAs0_AAs: "AAs0 ⋅⋅aml ηs0 = AAs"
using n by (auto intro: nth_equalityI)
from AAs0_def have AAs0_in_CAs0: "∀i < n. poss (AAs0 ! i) ⊆# CAs0 ! i"
using AAs0f_p by auto
define Cs0 where
"Cs0 = map2 (-) CAs0 (map poss AAs0)"
have "length Cs0 = n"
using Cs0_def n by auto
note n = n ‹length Cs0 = n›
have "∀i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)"
using AAs0_in_CAs0 Cs0_def n by auto
then have "Cs0 ⋅⋅cl ηs0 = Cs"
using ‹CAs0 ⋅⋅cl ηs0 = CAs› AAs0_AAs cas n by (auto intro: nth_equalityI)
show ?thesis
using that
‹AAs0 ⋅⋅aml ηs0 = AAs› ‹Cs0 ⋅⋅cl ηs0 = Cs› ‹∀i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)›
‹length AAs0 = n› ‹length Cs0 = n›
by blast
qed
have "∃DA0 η0. DA0 ∈ M ∧ DA = DA0 ⋅ η0 ∧ S DA0 ⋅ η0 = S_M S M DA ∧ is_ground_subst η0"
using grounding S_M_grounding_of_clss select by (metis le_supE singletonI subsetCE)
then obtain DA0 η0 where
DA0_η0_p: "DA0 ∈ M ∧ DA = DA0 ⋅ η0 ∧ S DA0 ⋅ η0 = S_M S M DA ∧ is_ground_subst η0"
by auto
have DA0_in_M: "DA0 ∈ M"
using DA0_η0_p by auto
have DA0_to_DA: "DA0 ⋅ η0 = DA"
using DA0_η0_p by auto
have SDA0_to_SMDA: "S DA0 ⋅ η0 = S_M S M DA"
using DA0_η0_p by auto
have "is_ground_subst η0"
using DA0_η0_p by auto
obtain D0 As0 where D0As0_p:
"As0 ⋅al η0 = As" "length As0 = n" "D0 ⋅ η0 = D" "DA0 = D0 + (negs (mset As0))"
"S_M S M (D + negs (mset As)) ≠ {#} ⟹ negs (mset As0) = S DA0"
proof -
{
assume a: "S_M S M (D + negs (mset As)) = {#} ∧ length As = (Suc 0)
∧ maximal_wrt (As ! 0 ⋅a σ) ((D + negs (mset As)) ⋅ σ)"
then have as: "mset As = {#As ! 0#}"
by (auto intro: nth_equalityI)
then have "negs (mset As) = {#Neg (As ! 0)#}"
by (simp add: ‹mset As = {#As ! 0#}›)
then have "DA = D + {#Neg (As ! 0)#}"
using da by auto
then obtain L where "L ∈# DA0 ∧ L ⋅l η0 = Neg (As ! 0)"
using DA0_to_DA by (metis Melem_subst_cls mset_subset_eq_add_right single_subset_iff)
then have "Neg (atm_of L) ∈# DA0 ∧ Neg (atm_of L) ⋅l η0 = Neg (As ! 0)"
by (metis Neg_atm_of_iff literal.sel(2) subst_lit_is_pos)
then have "[atm_of L] ⋅al η0 = As ∧ negs (mset [atm_of L]) ⊆# DA0"
using as subst_lit_def by auto
then have "∃As0. As0 ⋅al η0 = As ∧ negs (mset As0) ⊆# DA0
∧ (S_M S M (D + negs (mset As)) ≠ {#} ⟶ negs (mset As0) = S DA0)"
using a by blast
}
moreover
{
assume "S_M S M (D + negs (mset As)) = negs (mset As)"
then have "negs (mset As) = S DA0 ⋅ η0"
using da ‹S DA0 ⋅ η0 = S_M S M DA› by auto
then have "∃As0. negs (mset As0) = S DA0 ∧ As0 ⋅al η0 = As"
using instance_list[of As "S DA0" η0] S.S_selects_neg_lits by auto
then have "∃As0. As0 ⋅al η0 = As ∧ negs (mset As0) ⊆# DA0
∧ (S_M S M (D + negs (mset As)) ≠ {#} ⟶ negs (mset As0) = S DA0)"
using S.S_selects_subseteq by auto
}
ultimately have "∃As0. As0 ⋅al η0 = As ∧ (negs (mset As0)) ⊆# DA0
∧ (S_M S M (D + negs (mset As)) ≠ {#} ⟶ negs (mset As0) = S DA0)"
using eligible unfolding eligible.simps by auto
then obtain As0 where
As0_p: "As0 ⋅al η0 = As ∧ negs (mset As0) ⊆# DA0
∧ (S_M S M (D + negs (mset As)) ≠ {#} ⟶ negs (mset As0) = S DA0)"
by blast
then have "length As0 = n"
using as_len by auto
note n = n this
have "As0 ⋅al η0 = As"
using As0_p by auto
define D0 where
"D0 = DA0 - negs (mset As0)"
then have "DA0 = D0 + negs (mset As0)"
using As0_p by auto
then have "D0 ⋅ η0 = D"
using DA0_to_DA da As0_p by auto
have "S_M S M (D + negs (mset As)) ≠ {#} ⟹ negs (mset As0) = S DA0"
using As0_p by blast
then show ?thesis
using that ‹As0 ⋅al η0 = As› ‹D0 ⋅ η0= D› ‹DA0 = D0 + (negs (mset As0))› ‹length As0 = n›
by metis
qed
show ?thesis
using that[OF n(2,1) DA0_in_M DA0_to_DA SDA0_to_SMDA CAs0_in_M CAs0_to_CAs SCAs0_to_SMCAs
‹is_ground_subst η0› ‹is_ground_subst_list ηs0› ‹As0 ⋅al η0 = As›
‹AAs0 ⋅⋅aml ηs0 = AAs›
‹length As0 = n›
‹D0 ⋅ η0 = D›
‹DA0 = D0 + (negs (mset As0))›
‹S_M S M (D + negs (mset As)) ≠ {#} ⟹ negs (mset As0) = S DA0›
‹length Cs0 = n›
‹Cs0 ⋅⋅cl ηs0 = Cs›
‹∀i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)›
‹length AAs0 = n›]
by auto
qed
lemma ord_resolve_rename_lifting:
assumes
sel_stable: "⋀ρ C. is_renaming ρ ⟹ S (C ⋅ ρ) = S C ⋅ ρ" and
res_e: "ord_resolve (S_M S M) CAs DA AAs As σ E" and
select: "selection S" and
grounding: "{DA} ∪ set CAs ⊆ grounding_of_clss M"
obtains ηs η η2 CAs0 DA0 AAs0 As0 E0 τ where
"is_ground_subst η"
"is_ground_subst_list ηs"
"is_ground_subst η2"
"ord_resolve_rename S CAs0 DA0 AAs0 As0 τ E0"
"CAs0 ⋅⋅cl ηs = CAs" "DA0 ⋅ η = DA" "E0 ⋅ η2 = E"
"{DA0} ∪ set CAs0 ⊆ M"
"length CAs0 = length CAs"
"length ηs = length CAs"
using res_e
proof (cases rule: ord_resolve.cases)
case (ord_resolve n Cs D)
note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and
aas_len = this(5) and as_len = this(6) and nz = this(7) and cas = this(8) and
aas_not_empt = this(9) and mgu = this(10) and eligible = this(11) and str_max = this(12) and
sel_empt = this(13)
have sel_ren_list_inv:
"⋀ρs Cs. length ρs = length Cs ⟹ is_renaming_list ρs ⟹ map S (Cs ⋅⋅cl ρs) = map S Cs ⋅⋅cl ρs"
using sel_stable unfolding is_renaming_list_def by (auto intro: nth_equalityI)
note n = ‹n ≠ 0› ‹length CAs = n› ‹length Cs = n› ‹length AAs = n› ‹length As = n›
interpret S: selection S by (rule select)
obtain DA0 η0 CAs0 ηs0 As0 AAs0 D0 Cs0 where as0:
"length CAs0 = n"
"length ηs0 = n"
"DA0 ∈ M"
"DA0 ⋅ η0 = DA"
"S DA0 ⋅ η0 = S_M S M DA"
"∀CA0 ∈ set CAs0. CA0 ∈ M"
"CAs0 ⋅⋅cl ηs0 = CAs"
"map S CAs0 ⋅⋅cl ηs0 = map (S_M S M) CAs"
"is_ground_subst η0"
"is_ground_subst_list ηs0"
"As0 ⋅al η0 = As"
"AAs0 ⋅⋅aml ηs0 = AAs"
"length As0 = n"
"D0 ⋅ η0 = D"
"DA0 = D0 + (negs (mset As0))"
"S_M S M (D + negs (mset As)) ≠ {#} ⟹ negs (mset As0) = S DA0"
"length Cs0 = n"
"Cs0 ⋅⋅cl ηs0 = Cs"
"∀i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)"
"length AAs0 = n"
using ord_resolve_obtain_clauses[of S M CAs DA, OF res_e select grounding n(2) ‹DA = D + negs (mset As)›
‹∀i<n. CAs ! i = Cs ! i + poss (AAs ! i)› ‹length Cs = n› ‹length AAs = n›, of thesis] by blast
note n = ‹length CAs0 = n› ‹length ηs0 = n› ‹length As0 = n› ‹length AAs0 = n› ‹length Cs0 = n› n
have "length (renamings_apart (DA0 # CAs0)) = Suc n"
using n renamings_apart_length by auto
note n = this n
define ρ where
"ρ = hd (renamings_apart (DA0 # CAs0))"
define ρs where
"ρs = tl (renamings_apart (DA0 # CAs0))"
define DA0' where
"DA0' = DA0 ⋅ ρ"
define D0' where
"D0' = D0 ⋅ ρ"
define As0' where
"As0' = As0 ⋅al ρ"
define CAs0' where
"CAs0' = CAs0 ⋅⋅cl ρs"
define Cs0' where
"Cs0' = Cs0 ⋅⋅cl ρs"
define AAs0' where
"AAs0' = AAs0 ⋅⋅aml ρs"
define η0' where
"η0' = inv_renaming ρ ⊙ η0"
define ηs0' where
"ηs0' = map inv_renaming ρs ⊙s ηs0"
have renames_DA0: "is_renaming ρ"
using renamings_apart_length renamings_apart_renaming unfolding ρ_def
by (metis length_greater_0_conv list.exhaust_sel list.set_intros(1) list.simps(3))
have renames_CAs0: "is_renaming_list ρs"
using renamings_apart_length renamings_apart_renaming unfolding ρs_def
by (metis is_renaming_list_def length_greater_0_conv list.set_sel(2) list.simps(3))
have "length ρs = n"
unfolding ρs_def using n by auto
note n = n ‹length ρs = n›
have "length As0' = n"
unfolding As0'_def using n by auto
have "length CAs0' = n"
using as0(1) n unfolding CAs0'_def by auto
have "length Cs0' = n"
unfolding Cs0'_def using n by auto
have "length AAs0' = n"
unfolding AAs0'_def using n by auto
have "length ηs0' = n"
using as0(2) n unfolding ηs0'_def by auto
note n = ‹length CAs0' = n› ‹length ηs0' = n› ‹length As0' = n› ‹length AAs0' = n› ‹length Cs0' = n› n
have DA0'_DA: "DA0' ⋅ η0' = DA"
using as0(4) unfolding η0'_def DA0'_def using renames_DA0 by simp
have D0'_D: "D0' ⋅ η0' = D"
using as0(14) unfolding η0'_def D0'_def using renames_DA0 by simp
have As0'_As: "As0' ⋅al η0' = As"
using as0(11) unfolding η0'_def As0'_def using renames_DA0 by auto
have "S DA0' ⋅ η0' = S_M S M DA"
using as0(5) unfolding η0'_def DA0'_def using renames_DA0 sel_stable by auto
have CAs0'_CAs: "CAs0' ⋅⋅cl ηs0' = CAs"
using as0(7) unfolding CAs0'_def ηs0'_def using renames_CAs0 n by auto
have Cs0'_Cs: "Cs0' ⋅⋅cl ηs0' = Cs"
using as0(18) unfolding Cs0'_def ηs0'_def using renames_CAs0 n by auto
have AAs0'_AAs: "AAs0' ⋅⋅aml ηs0' = AAs"
using as0(12) unfolding ηs0'_def AAs0'_def using renames_CAs0 using n by auto
have "map S CAs0' ⋅⋅cl ηs0' = map (S_M S M) CAs"
unfolding CAs0'_def ηs0'_def using as0(8) n renames_CAs0 sel_ren_list_inv by auto
have DA0'_split: "DA0' = D0' + negs (mset As0')"
using as0(15) DA0'_def D0'_def As0'_def by auto
then have D0'_subset_DA0': "D0' ⊆# DA0'"
by auto
from DA0'_split have negs_As0'_subset_DA0': "negs (mset As0') ⊆# DA0'"
by auto
have CAs0'_split: "∀i<n. CAs0' ! i = Cs0' ! i + poss (AAs0' ! i)"
using as0(19) CAs0'_def Cs0'_def AAs0'_def n by auto
then have "∀i<n. Cs0' ! i ⊆# CAs0' ! i"
by auto
from CAs0'_split have poss_AAs0'_subset_CAs0': "∀i<n. poss (AAs0' ! i) ⊆# CAs0' ! i"
by auto
then have AAs0'_in_atms_of_CAs0': "∀i < n. ∀A∈#AAs0' ! i. A ∈ atms_of (CAs0' ! i)"
by (auto simp add: atm_iff_pos_or_neg_lit)
have as0':
"S_M S M (D + negs (mset As)) ≠ {#} ⟹ negs (mset As0') = S DA0'"
proof -
assume a: "S_M S M (D + negs (mset As)) ≠ {#}"
then have "negs (mset As0) ⋅ ρ = S DA0 ⋅ ρ"
using as0(16) unfolding ρ_def by metis
then show "negs (mset As0') = S DA0'"
using As0'_def DA0'_def using sel_stable[of ρ DA0] renames_DA0 by auto
qed
have vd: "var_disjoint (DA0' # CAs0')"
unfolding DA0'_def CAs0'_def using renamings_apart_var_disjoint
unfolding ρ_def ρs_def
by (metis length_greater_0_conv list.exhaust_sel n(6) subst_cls_lists_Cons zero_less_Suc)
from vd DA0'_DA CAs0'_CAs have "∃η. ∀i < Suc n. ∀S. S ⊆# (DA0' # CAs0') ! i ⟶ S ⋅ (η0'#ηs0') ! i = S ⋅ η"
unfolding var_disjoint_def using n by auto
then obtain η where η_p: "∀i < Suc n. ∀S. S ⊆# (DA0' # CAs0') ! i ⟶ S ⋅ (η0'#ηs0') ! i = S ⋅ η"
by auto
have η_p_lit: "∀i < Suc n. ∀L. L ∈# (DA0' # CAs0') ! i ⟶ L ⋅l (η0'#ηs0') ! i = L ⋅l η"
proof (rule, rule, rule, rule)
fix i :: "nat" and L :: "'a literal"
assume a:
"i < Suc n"
"L ∈# (DA0' # CAs0') ! i"
then have "∀S. S ⊆# (DA0' # CAs0') ! i ⟶ S ⋅ (η0' # ηs0') ! i = S ⋅ η"
using η_p by auto
then have "{# L #} ⋅ (η0' # ηs0') ! i = {# L #} ⋅ η"
using a by (meson single_subset_iff)
then show "L ⋅l (η0' # ηs0') ! i = L ⋅l η" by auto
qed
have η_p_atm: "∀i < Suc n. ∀A. A ∈ atms_of ((DA0' # CAs0') ! i) ⟶ A ⋅a (η0'#ηs0') ! i = A ⋅a η"
proof (rule, rule, rule, rule)
fix i :: "nat" and A :: "'a"
assume a:
"i < Suc n"
"A ∈ atms_of ((DA0' # CAs0') ! i)"
then obtain L where L_p: "atm_of L = A ∧ L ∈# (DA0' # CAs0') ! i"
unfolding atms_of_def by auto
then have "L ⋅l (η0'#ηs0') ! i = L ⋅l η"
using η_p_lit a by auto
then show "A ⋅a (η0' # ηs0') ! i = A ⋅a η"
using L_p unfolding subst_lit_def by (cases L) auto
qed
have DA0'_DA: "DA0' ⋅ η = DA"
using DA0'_DA η_p by auto
have "D0' ⋅ η = D" using η_p D0'_D n D0'_subset_DA0' by auto
have "As0' ⋅al η = As"
proof (rule nth_equalityI)
show "length (As0' ⋅al η) = length As"
using n by auto
next
fix i
show "i<length (As0' ⋅al η) ⟹ (As0' ⋅al η) ! i = As ! i"
proof -
assume a: "i < length (As0' ⋅al η)"
have A_eq: "∀A. A ∈ atms_of DA0' ⟶ A ⋅a η0' = A ⋅a η"
using η_p_atm n by force
have "As0' ! i ∈ atms_of DA0'"
using negs_As0'_subset_DA0' unfolding atms_of_def
using a n by force
then have "As0' ! i ⋅a η0' = As0' ! i ⋅a η"
using A_eq by simp
then show "(As0' ⋅al η) ! i = As ! i"
using As0'_As ‹length As0' = n› a by auto
qed
qed
interpret selection
by (rule select)
have "S DA0' ⋅ η = S_M S M DA"
using ‹S DA0' ⋅ η0' = S_M S M DA› η_p S.S_selects_subseteq by auto
from η_p have η_p_CAs0': "∀i < n. (CAs0' ! i) ⋅ (ηs0' ! i) = (CAs0'! i) ⋅ η"
using n by auto
then have "CAs0' ⋅⋅cl ηs0' = CAs0' ⋅cl η"
using n by (auto intro: nth_equalityI)
then have CAs0'_η_fo_CAs: "CAs0' ⋅cl η = CAs"
using CAs0'_CAs η_p n by auto
from η_p have "∀i < n. S (CAs0' ! i) ⋅ ηs0' ! i = S (CAs0' ! i) ⋅ η"
using S.S_selects_subseteq n by auto
then have "map S CAs0' ⋅⋅cl ηs0' = map S CAs0' ⋅cl η"
using n by (auto intro: nth_equalityI)
then have SCAs0'_η_fo_SMCAs: "map S CAs0' ⋅cl η = map (S_M S M) CAs"
using ‹map S CAs0' ⋅⋅cl ηs0' = map (S_M S M) CAs› by auto
have "Cs0' ⋅cl η = Cs"
proof (rule nth_equalityI)
show "length (Cs0' ⋅cl η) = length Cs"
using n by auto
next
fix i
show "i<length (Cs0' ⋅cl η) ⟹ (Cs0' ⋅cl η) ! i = Cs ! i"
proof -
assume "i < length (Cs0' ⋅cl η)"
then have a: "i < n"
using n by force
have "(Cs0' ⋅⋅cl ηs0') ! i = Cs ! i"
using Cs0'_Cs a n by force
moreover
have η_p_CAs0': "∀S. S ⊆# CAs0' ! i ⟶ S ⋅ ηs0' ! i = S ⋅ η"
using η_p a by force
have "Cs0' ! i ⋅ ηs0' ! i = (Cs0' ⋅cl η) ! i"
using η_p_CAs0' ‹∀i<n. Cs0' ! i ⊆# CAs0' ! i› a n by force
then have "(Cs0' ⋅⋅cl ηs0') ! i = (Cs0' ⋅cl η) ! i "
using a n by force
ultimately show "(Cs0' ⋅cl η) ! i = Cs ! i"
by auto
qed
qed
have AAs0'_AAs: "AAs0' ⋅aml η = AAs"
proof (rule nth_equalityI)
show "length (AAs0' ⋅aml η) = length AAs"
using n by auto
next
fix i
show "i<length (AAs0' ⋅aml η) ⟹ (AAs0' ⋅aml η) ! i = AAs ! i"
proof -
assume a: "i < length (AAs0' ⋅aml η)"
then have "i < n"
using n by force
then have "∀A. A ∈ atms_of ((DA0' # CAs0') ! Suc i) ⟶ A ⋅a (η0' # ηs0') ! Suc i = A ⋅a η"
using η_p_atm n by force
then have A_eq: "∀A. A ∈ atms_of (CAs0' ! i) ⟶ A ⋅a ηs0' ! i = A ⋅a η"
by auto
have AAs_CAs0': "∀A ∈# AAs0' ! i. A ∈ atms_of (CAs0' ! i)"
using AAs0'_in_atms_of_CAs0' unfolding atms_of_def
using a n by force
then have "AAs0' ! i ⋅am ηs0' ! i = AAs0' ! i ⋅am η"
unfolding subst_atm_mset_def using A_eq unfolding subst_atm_mset_def by auto
then show "(AAs0' ⋅aml η) ! i = AAs ! i"
using AAs0'_AAs ‹length AAs0' = n› ‹length ηs0' = n› a by auto
qed
qed
obtain τ φ where τφ:
"Some τ = mgu (set_mset ` set (map2 add_mset As0' AAs0'))"
"τ ⊙ φ = η ⊙ σ"
proof -
have uu: "is_unifiers σ (set_mset ` set (map2 add_mset (As0' ⋅al η) (AAs0' ⋅aml η)))"
using mgu mgu_sound is_mgu_def unfolding ‹AAs0' ⋅aml η = AAs› using ‹As0' ⋅al η = As› by auto
have ησuni: "is_unifiers (η ⊙ σ) (set_mset ` set (map2 add_mset As0' AAs0'))"
proof -
have "set_mset ` set (map2 add_mset As0' AAs0' ⋅aml η) =
set_mset ` set (map2 add_mset As0' AAs0') ⋅ass η"
unfolding subst_atmss_def subst_atm_mset_list_def using subst_atm_mset_def subst_atms_def
by (simp add: image_image subst_atm_mset_def subst_atms_def)
then have "is_unifiers σ (set_mset ` set (map2 add_mset As0' AAs0') ⋅ass η)"
using uu by (auto simp: n map2_add_mset_map)
then show ?thesis
using is_unifiers_comp by auto
qed
then obtain τ where
τ_p: "Some τ = mgu (set_mset ` set (map2 add_mset As0' AAs0'))"
using mgu_complete
by (metis (mono_tags, opaque_lifting) List.finite_set finite_imageI finite_set_mset image_iff)
moreover then obtain φ where φ_p: "τ ⊙ φ = η ⊙ σ"
by (metis (mono_tags, opaque_lifting) finite_set ησuni finite_imageI finite_set_mset image_iff
mgu_sound set_mset_mset substitution_ops.is_mgu_def)
ultimately show thesis
using that by auto
qed
have eligible0': "eligible S τ As0' (D0' + negs (mset As0'))"
proof -
have "S_M S M (D + negs (mset As)) = negs (mset As) ∨ S_M S M (D + negs (mset As)) = {#} ∧
length As = 1 ∧ maximal_wrt (As ! 0 ⋅a σ) ((D + negs (mset As)) ⋅ σ)"
using eligible unfolding eligible.simps by auto
then show ?thesis
proof
assume "S_M S M (D + negs (mset As)) = negs (mset As)"
then have "S_M S M (D + negs (mset As)) ≠ {#}"
using n by force
then have "S (D0' + negs (mset As0')) = negs (mset As0')"
using as0' DA0'_split by auto
then show ?thesis
unfolding eligible.simps[simplified] by auto
next
assume asm: "S_M S M (D + negs (mset As)) = {#} ∧ length As = 1 ∧
maximal_wrt (As ! 0 ⋅a σ) ((D + negs (mset As)) ⋅ σ)"
then have "S (D0' + negs (mset As0')) = {#}"
using ‹D0' ⋅ η = D›[symmetric] ‹As0' ⋅al η = As›[symmetric] ‹S (DA0') ⋅ η = S_M S M (DA)›
da DA0'_split subst_cls_empty_iff by metis
moreover from asm have l: "length As0' = 1"
using ‹As0' ⋅al η = As› by auto
moreover from asm have "maximal_wrt (As0' ! 0 ⋅a (τ ⊙ φ)) ((D0' + negs (mset As0')) ⋅ (τ ⊙ φ))"
using ‹As0' ⋅al η = As› ‹D0' ⋅ η = D› using l τφ by auto
then have "maximal_wrt (As0' ! 0 ⋅a τ ⋅a φ) ((D0' + negs (mset As0')) ⋅ τ ⋅ φ)"
by auto
then have "maximal_wrt (As0' ! 0 ⋅a τ) ((D0' + negs (mset As0')) ⋅ τ)"
using maximal_wrt_subst by blast
ultimately show ?thesis
unfolding eligible.simps[simplified] by auto
qed
qed
have maximality: "∀i < n. strictly_maximal_wrt (As0' ! i ⋅a τ) (Cs0' ! i ⋅ τ)"
proof -
from str_max have "∀i < n. strictly_maximal_wrt ((As0' ⋅al η) ! i ⋅a σ) ((Cs0' ⋅cl η) ! i ⋅ σ)"
using ‹As0' ⋅al η = As› ‹Cs0' ⋅cl η = Cs› by simp
then have "∀i < n. strictly_maximal_wrt (As0' ! i ⋅a (τ ⊙ φ)) (Cs0' ! i ⋅ (τ ⊙ φ))"
using n τφ by simp
then have "∀i < n. strictly_maximal_wrt (As0' ! i ⋅a τ ⋅a φ) (Cs0' ! i ⋅ τ ⋅ φ)"
by auto
then show "∀i < n. strictly_maximal_wrt (As0' ! i ⋅a τ) (Cs0' ! i ⋅ τ)"
using strictly_maximal_wrt_subst τφ by blast
qed
have nothing_selected: "∀i < n. S (CAs0' ! i) = {#}"
proof -
have "∀i < n. (map S CAs0' ⋅cl η) ! i = map (S_M S M) CAs ! i"
by (simp add: ‹map S CAs0' ⋅cl η = map (S_M S M) CAs›)
then have "∀i < n. S (CAs0' ! i) ⋅ η = S_M S M (CAs ! i)"
using n by auto
then have "∀i < n. S (CAs0' ! i) ⋅ η = {#}"
using sel_empt ‹∀i < n. S (CAs0' ! i) ⋅ η = S_M S M (CAs ! i)› by auto
then show "∀i < n. S (CAs0' ! i) = {#}"
using subst_cls_empty_iff by blast
qed
have "∀i < n. AAs0' ! i ≠ {#}"
using n aas_not_empt ‹AAs0' ⋅aml η = AAs› by auto
define E0' where
"E0' = ((∑⇩# (mset Cs0')) + D0') ⋅ τ"
have res_e0': "ord_resolve S CAs0' DA0' AAs0' As0' τ E0'"
using ord_resolve.intros[of CAs0' n Cs0' AAs0' As0' τ S D0',
OF _ _ _ _ _ _ ‹∀i < n. AAs0' ! i ≠ {#}› τφ(1) eligible0'
‹∀i < n. strictly_maximal_wrt (As0' ! i ⋅a τ) (Cs0' ! i ⋅ τ)› ‹∀i < n. S (CAs0' ! i) = {#}›]
unfolding E0'_def using DA0'_split n ‹∀i<n. CAs0' ! i = Cs0' ! i + poss (AAs0' ! i)› by blast
have e0'φe: "E0' ⋅ φ = E"
proof -
have "E0' ⋅ φ = ((∑⇩# (mset Cs0')) + D0') ⋅ (τ ⊙ φ)"
unfolding E0'_def by auto
also have "… = (∑⇩# (mset Cs0') + D0') ⋅ (η ⊙ σ)"
using τφ by auto
also have "… = (∑⇩# (mset Cs) + D) ⋅ σ"
using ‹Cs0' ⋅cl η = Cs› ‹D0' ⋅ η = D› by auto
also have "… = E"
using e by auto
finally show e0'φe: "E0' ⋅ φ = E"
.
qed
obtain η2 where
ground_η2: "is_ground_subst η2" "E0' ⋅ η2 = E"
proof -
have "is_ground_cls_list CAs" "is_ground_cls DA"
using grounding grounding_ground unfolding is_ground_cls_list_def by auto
then have "is_ground_cls E"
using res_e ground_resolvent_subset by (force intro: is_ground_cls_mono)
then show thesis
using that e0'φe make_ground_subst by auto
qed
have ‹length CAs0 = length CAs›
using n by simp
have ‹length ηs0 = length CAs›
using n by simp
have "ord_resolve S (CAs0 ⋅⋅cl ρs) (DA0 ⋅ ρ) (AAs0 ⋅⋅aml ρs) (As0 ⋅al ρ) τ E0'"
using res_e0' As0'_def ρ_def AAs0'_def ρs_def DA0'_def ρ_def CAs0'_def ρs_def by simp
moreover have "∀i<n. poss (AAs0 ! i) ⊆# CAs0 ! i"
using as0(19) by auto
moreover have "negs (mset As0) ⊆# DA0"
using local.as0(15) by auto
ultimately have "ord_resolve_rename S CAs0 DA0 AAs0 As0 τ E0'"
using ord_resolve_rename[of CAs0 n AAs0 As0 DA0 ρ ρs S τ E0'] ρ_def ρs_def n by auto
then show thesis
using that[of η0 ηs0 η2 CAs0 DA0] ‹is_ground_subst η0› ‹is_ground_subst_list ηs0›
‹is_ground_subst η2› ‹CAs0 ⋅⋅cl ηs0 = CAs› ‹DA0 ⋅ η0 = DA› ‹E0' ⋅ η2 = E› ‹DA0 ∈ M›
‹∀CA ∈ set CAs0. CA ∈ M› ‹length CAs0 = length CAs› ‹length ηs0 = length CAs›
by blast
qed
lemma ground_ord_resolve_ground:
assumes
select: "selection S" and
CAs_p: "ground_resolution_with_selection.ord_resolve S CAs DA AAs As E" and
ground_cas: "is_ground_cls_list CAs" and
ground_da: "is_ground_cls DA"
shows "is_ground_cls E"
proof -
have a1: "atms_of E ⊆ (⋃CA ∈ set CAs. atms_of CA) ∪ atms_of DA"
using ground_resolution_with_selection.ord_resolve_atms_of_concl_subset[OF _ CAs_p]
ground_resolution_with_selection.intro[OF select] by blast
{
fix L :: "'a literal"
assume "L ∈# E"
then have "atm_of L ∈ atms_of E"
by (meson atm_of_lit_in_atms_of)
then have "is_ground_atm (atm_of L)"
using a1 ground_cas ground_da is_ground_cls_imp_is_ground_atm is_ground_cls_list_def
by auto
}
then show ?thesis
unfolding is_ground_cls_def is_ground_lit_def by simp
qed
lemma ground_ord_resolve_imp_ord_resolve:
assumes
ground_da: ‹is_ground_cls DA› and
ground_cas: ‹is_ground_cls_list CAs› and
gr: "ground_resolution_with_selection S_G" and
gr_res: ‹ground_resolution_with_selection.ord_resolve S_G CAs DA AAs As E›
shows ‹∃σ. ord_resolve S_G CAs DA AAs As σ E›
proof (cases rule: ground_resolution_with_selection.ord_resolve.cases[OF gr gr_res])
case (1 CAs n Cs AAs As D)
note cas = this(1) and da = this(2) and aas = this(3) and as = this(4) and e = this(5) and
cas_len = this(6) and cs_len = this(7) and aas_len = this(8) and as_len = this(9) and
nz = this(10) and casi = this(11) and aas_not_empt = this(12) and as_aas = this(13) and
eligibility = this(14) and str_max = this(15) and sel_empt = this(16)
have len_aas_len_as: "length AAs = length As"
using aas_len as_len by auto
from as_aas have "∀i < n. ∀A ∈# add_mset (As ! i) (AAs ! i). A = As ! i"
by simp
then have "∀i < n. card (set_mset (add_mset (As ! i) (AAs ! i))) ≤ Suc 0"
using all_the_same by metis
then have "∀i < length AAs. card (set_mset (add_mset (As ! i) (AAs ! i))) ≤ Suc 0"
using aas_len by auto
then have "∀AA ∈ set (map2 add_mset As AAs). card (set_mset AA) ≤ Suc 0"
using set_map2_ex[of AAs As add_mset, OF len_aas_len_as] by auto
then have "is_unifiers id_subst (set_mset ` set (map2 add_mset As AAs))"
unfolding is_unifiers_def is_unifier_def by auto
moreover have "finite (set_mset ` set (map2 add_mset As AAs))"
by auto
moreover have "∀AA ∈ set_mset ` set (map2 add_mset As AAs). finite AA"
by auto
ultimately obtain σ where
σ_p: "Some σ = mgu (set_mset ` set (map2 add_mset As AAs))"
using mgu_complete by metis
have ground_elig: "ground_resolution_with_selection.eligible S_G As (D + negs (mset As))"
using eligibility by simp
have ground_cs: "∀i < n. is_ground_cls (Cs ! i)"
using cas cas_len cs_len casi ground_cas nth_mem unfolding is_ground_cls_list_def by force
have ground_set_as: "is_ground_atms (set As)"
using da ground_da by (metis atms_of_negs is_ground_cls_is_ground_atms_atms_of
is_ground_cls_union set_mset_mset)
then have ground_mset_as: "is_ground_atm_mset (mset As)"
unfolding is_ground_atm_mset_def is_ground_atms_def by auto
have ground_as: "is_ground_atm_list As"
using ground_set_as is_ground_atm_list_def is_ground_atms_def by auto
have ground_d: "is_ground_cls D"
using ground_da da by simp
from as_len nz have atms:
"atms_of D ∪ set As ≠ {}"
"finite (atms_of D ∪ set As)"
by auto
then have "Max (atms_of D ∪ set As) ∈ atms_of D ∪ set As"
using Max_in by metis
then have is_ground_Max: "is_ground_atm (Max (atms_of D ∪ set As))"
using ground_d ground_mset_as is_ground_cls_imp_is_ground_atm
unfolding is_ground_atm_mset_def by auto
have "maximal_wrt (Max (atms_of D ∪ set As)) (D + negs (mset As))"
unfolding maximal_wrt_def
by clarsimp (metis atms Max_less_iff UnCI ground_d ground_set_as infinite_growing
is_ground_Max is_ground_atms_def is_ground_cls_imp_is_ground_atm less_atm_ground)
moreover have
"Max (atms_of D ∪ set As) ⋅a σ = Max (atms_of D ∪ set As)" and
"D ⋅ σ + negs (mset As ⋅am σ) = D + negs (mset As)"
using ground_elig is_ground_Max ground_mset_as ground_d by auto
ultimately have fo_elig: "eligible S_G σ As (D + negs (mset As))"
using ground_elig unfolding ground_resolution_with_selection.eligible.simps[OF gr]
ground_resolution_with_selection.maximal_wrt_def[OF gr] eligible.simps
by auto
have "∀i < n. strictly_maximal_wrt (As ! i) (Cs ! i)"
using str_max[unfolded ground_resolution_with_selection.strictly_maximal_wrt_def[OF gr]]
ground_as[unfolded is_ground_atm_list_def] ground_cs as_len less_atm_ground
unfolding strictly_maximal_wrt_def by clarsimp (fastforce simp: is_ground_cls_as_atms)+
then have ll: "∀i < n. strictly_maximal_wrt (As ! i ⋅a σ) (Cs ! i ⋅ σ)"
by (simp add: ground_as ground_cs as_len)
have ground_e: "is_ground_cls E"
using ground_d ground_cs cs_len unfolding e is_ground_cls_def
by simp (metis in_mset_sum_list2 in_set_conv_nth)
show ?thesis
using cas da aas as e ground_e ord_resolve.intros[OF cas_len cs_len aas_len as_len nz casi
aas_not_empt σ_p fo_elig ll sel_empt]
by auto
qed
end
end