Theory FO_Ordered_Resolution_Prover
section ‹An Ordered Resolution Prover for First-Order Clauses›
theory FO_Ordered_Resolution_Prover
imports FO_Ordered_Resolution
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 RP prover defined in Figure 5 and
its related lemmas and theorems, including Lemmas 4.10 and 4.11 and Theorem 4.13 (completeness).
›
definition is_least :: "(nat ⇒ bool) ⇒ nat ⇒ bool" where
"is_least P n ⟷ P n ∧ (∀n' < n. ¬ P n')"
lemma least_exists: "P n ⟹ ∃n. is_least P n"
using exists_least_iff unfolding is_least_def by auto
text ‹
The following corresponds to page 42 and 43 of Section 4.3, from the explanation of RP to
Lemma 4.10.
›
type_synonym 'a state = "'a clause set × 'a clause set × 'a clause set"
locale FO_resolution_prover =
FO_resolution subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu less_atm +
selection S
for
S :: "('a :: wellorder) clause ⇒ 'a clause" and
subst_atm :: "'a ⇒ 's ⇒ 'a" and
id_subst :: "'s" and
comp_subst :: "'s ⇒ 's ⇒ 's" and
renamings_apart :: "'a clause list ⇒ 's list" and
atm_of_atms :: "'a list ⇒ 'a" and
mgu :: "'a set set ⇒ 's option" and
less_atm :: "'a ⇒ 'a ⇒ bool" +
assumes
sel_stable: "⋀ρ C. is_renaming ρ ⟹ S (C ⋅ ρ) = S C ⋅ ρ"
begin
fun N_of_state :: "'a state ⇒ 'a clause set" where
"N_of_state (N, P, Q) = N"
fun P_of_state :: "'a state ⇒ 'a clause set" where
"P_of_state (N, P, Q) = P"
text ‹
‹O› denotes relation composition in Isabelle, so the formalization uses ‹Q› instead.
›
fun Q_of_state :: "'a state ⇒ 'a clause set" where
"Q_of_state (N, P, Q) = Q"
abbreviation clss_of_state :: "'a state ⇒ 'a clause set" where
"clss_of_state St ≡ N_of_state St ∪ P_of_state St ∪ Q_of_state St"
abbreviation grounding_of_state :: "'a state ⇒ 'a clause set" where
"grounding_of_state St ≡ grounding_of_clss (clss_of_state St)"
interpretation ord_FO_resolution: inference_system "ord_FO_Γ S" .
text ‹
The following inductive predicate formalizes the resolution prover in Figure 5.
›
inductive RP :: "'a state ⇒ 'a state ⇒ bool" (infix ‹↝› 50) where
tautology_deletion: "Neg A ∈# C ⟹ Pos A ∈# C ⟹ (N ∪ {C}, P, Q) ↝ (N, P, Q)"
| forward_subsumption: "D ∈ P ∪ Q ⟹ subsumes D C ⟹ (N ∪ {C}, P, Q) ↝ (N, P, Q)"
| backward_subsumption_P: "D ∈ N ⟹ strictly_subsumes D C ⟹ (N, P ∪ {C}, Q) ↝ (N, P, Q)"
| backward_subsumption_Q: "D ∈ N ⟹ strictly_subsumes D C ⟹ (N, P, Q ∪ {C}) ↝ (N, P, Q)"
| forward_reduction: "D + {#L'#} ∈ P ∪ Q ⟹ - L = L' ⋅l σ ⟹ D ⋅ σ ⊆# C ⟹
(N ∪ {C + {#L#}}, P, Q) ↝ (N ∪ {C}, P, Q)"
| backward_reduction_P: "D + {#L'#} ∈ N ⟹ - L = L' ⋅l σ ⟹ D ⋅ σ ⊆# C ⟹
(N, P ∪ {C + {#L#}}, Q) ↝ (N, P ∪ {C}, Q)"
| backward_reduction_Q: "D + {#L'#} ∈ N ⟹ - L = L' ⋅l σ ⟹ D ⋅ σ ⊆# C ⟹
(N, P, Q ∪ {C + {#L#}}) ↝ (N, P ∪ {C}, Q)"
| clause_processing: "(N ∪ {C}, P, Q) ↝ (N, P ∪ {C}, Q)"
| inference_computation: "N = concls_of (ord_FO_resolution.inferences_between Q C) ⟹
({}, P ∪ {C}, Q) ↝ (N, P, Q ∪ {C})"
lemma final_RP: "¬ ({}, {}, Q) ↝ St"
by (auto elim: RP.cases)
definition Sup_state :: "'a state llist ⇒ 'a state" where
"Sup_state Sts =
(Sup_llist (lmap N_of_state Sts), Sup_llist (lmap P_of_state Sts),
Sup_llist (lmap Q_of_state Sts))"
definition Liminf_state :: "'a state llist ⇒ 'a state" where
"Liminf_state Sts =
(Liminf_llist (lmap N_of_state Sts), Liminf_llist (lmap P_of_state Sts),
Liminf_llist (lmap Q_of_state Sts))"
context
fixes Sts Sts' :: "'a state llist"
assumes Sts: "lfinite Sts" "lfinite Sts'" "¬ lnull Sts" "¬ lnull Sts'" "llast Sts' = llast Sts"
begin
lemma
N_of_Liminf_state_fin: "N_of_state (Liminf_state Sts') = N_of_state (Liminf_state Sts)" and
P_of_Liminf_state_fin: "P_of_state (Liminf_state Sts') = P_of_state (Liminf_state Sts)" and
Q_of_Liminf_state_fin: "Q_of_state (Liminf_state Sts') = Q_of_state (Liminf_state Sts)"
using Sts by (simp_all add: Liminf_state_def lfinite_Liminf_llist llast_lmap)
lemma Liminf_state_fin: "Liminf_state Sts' = Liminf_state Sts"
using N_of_Liminf_state_fin P_of_Liminf_state_fin Q_of_Liminf_state_fin
by (simp add: Liminf_state_def)
end
context
fixes Sts Sts' :: "'a state llist"
assumes Sts: "¬ lfinite Sts" "emb Sts Sts'"
begin
lemma
N_of_Liminf_state_inf: "N_of_state (Liminf_state Sts') ⊆ N_of_state (Liminf_state Sts)" and
P_of_Liminf_state_inf: "P_of_state (Liminf_state Sts') ⊆ P_of_state (Liminf_state Sts)" and
Q_of_Liminf_state_inf: "Q_of_state (Liminf_state Sts') ⊆ Q_of_state (Liminf_state Sts)"
using Sts by (simp_all add: Liminf_state_def emb_Liminf_llist_infinite emb_lmap)
lemma clss_of_Liminf_state_inf:
"clss_of_state (Liminf_state Sts') ⊆ clss_of_state (Liminf_state Sts)"
using N_of_Liminf_state_inf P_of_Liminf_state_inf Q_of_Liminf_state_inf by blast
end
definition fair_state_seq :: "'a state llist ⇒ bool" where
"fair_state_seq Sts ⟷ N_of_state (Liminf_state Sts) = {} ∧ P_of_state (Liminf_state Sts) = {}"
text ‹
The following formalizes Lemma 4.10.
›
context
fixes Sts :: "'a state llist"
begin
definition S_Q :: "'a clause ⇒ 'a clause" where
"S_Q = S_M S (Q_of_state (Liminf_state Sts))"
interpretation sq: selection S_Q
unfolding S_Q_def using S_M_selects_subseteq S_M_selects_neg_lits selection_axioms
by unfold_locales auto
interpretation gr: ground_resolution_with_selection S_Q
by unfold_locales
interpretation sr: standard_redundancy_criterion_reductive gr.ord_Γ
by unfold_locales
interpretation sr: standard_redundancy_criterion_counterex_reducing gr.ord_Γ
"ground_resolution_with_selection.INTERP S_Q"
by unfold_locales
text ‹
The extension of ordered resolution mentioned in 4.10. We let it consist of all sound rules.
›
definition ground_sound_Γ:: "'a inference set" where
"ground_sound_Γ = {Infer CC D E | CC D E. (∀I. I ⊨m CC ⟶ I ⊨ D ⟶ I ⊨ E)}"
text ‹
We prove that we indeed defined an extension.
›
lemma gd_ord_Γ_ngd_ord_Γ: "gr.ord_Γ ⊆ ground_sound_Γ"
unfolding ground_sound_Γ_def using gr.ord_Γ_def gr.ord_resolve_sound by fastforce
lemma sound_ground_sound_Γ: "sound_inference_system ground_sound_Γ"
unfolding sound_inference_system_def ground_sound_Γ_def by auto
lemma sat_preserving_ground_sound_Γ: "sat_preserving_inference_system ground_sound_Γ"
using sound_ground_sound_Γ sat_preserving_inference_system.intro
sound_inference_system.Γ_sat_preserving by blast
definition sr_ext_Ri :: "'a clause set ⇒ 'a inference set" where
"sr_ext_Ri N = sr.Ri N ∪ (ground_sound_Γ - gr.ord_Γ)"
interpretation sr_ext:
sat_preserving_redundancy_criterion ground_sound_Γ sr.Rf sr_ext_Ri
unfolding sat_preserving_redundancy_criterion_def sr_ext_Ri_def
using sat_preserving_ground_sound_Γ redundancy_criterion_standard_extension gd_ord_Γ_ngd_ord_Γ
sr.redundancy_criterion_axioms by auto
lemma strict_subset_subsumption_redundant_clause:
assumes
sub: "D ⋅ σ ⊂# C" and
ground_σ: "is_ground_subst σ"
shows "C ∈ sr.Rf (grounding_of_cls D)"
proof -
from sub have "∀I. I ⊨ D ⋅ σ ⟶ I ⊨ C"
unfolding true_cls_def by blast
moreover have "C > D ⋅ σ"
using sub by (simp add: subset_imp_less_mset)
moreover have "D ⋅ σ ∈ grounding_of_cls D"
using ground_σ by (metis (mono_tags) mem_Collect_eq substitution_ops.grounding_of_cls_def)
ultimately have "set_mset {#D ⋅ σ#} ⊆ grounding_of_cls D"
"(∀I. I ⊨m {#D ⋅ σ#} ⟶ I ⊨ C)"
"(∀D'. D' ∈# {#D ⋅ σ#} ⟶ D' < C)"
by auto
then show ?thesis
using sr.Rf_def by blast
qed
lemma strict_subset_subsumption_redundant_clss:
assumes
"D ⋅ σ ⊂# C" and
"is_ground_subst σ" and
"D ∈ CC"
shows "C ∈ sr.Rf (grounding_of_clss CC)"
using assms
proof -
have "C ∈ sr.Rf (grounding_of_cls D)"
using strict_subset_subsumption_redundant_clause assms by auto
then show ?thesis
using assms unfolding grounding_of_clss_def
by (metis (no_types) sr.Rf_mono sup_ge1 SUP_absorb contra_subsetD)
qed
lemma strict_subset_subsumption_grounding_redundant_clss:
assumes
Dσ_subset_C: "D ⋅ σ ⊂# C" and
D_in_St: "D ∈ CC"
shows "grounding_of_cls C ⊆ sr.Rf (grounding_of_clss CC)"
proof
fix Cμ
assume "Cμ ∈ grounding_of_cls C"
then obtain μ where
μ_p: "Cμ = C ⋅ μ ∧ is_ground_subst μ"
unfolding grounding_of_cls_def by auto
have DσμCμ: "D ⋅ σ ⋅ μ ⊂# C ⋅ μ"
using Dσ_subset_C subst_subset_mono by auto
then show "Cμ ∈ sr.Rf (grounding_of_clss CC)"
using μ_p strict_subset_subsumption_redundant_clss[of D "σ ⊙ μ" "C ⋅ μ"] D_in_St by auto
qed
lemma derive_if_remove_subsumed:
assumes
"D ∈ clss_of_state St" and
"subsumes D C"
shows "sr_ext.derive (grounding_of_state St ∪ grounding_of_cls C) (grounding_of_state St)"
proof -
from assms obtain σ where
"D ⋅ σ = C ∨ D ⋅ σ ⊂# C"
by (auto simp: subsumes_def subset_mset_def)
then have "D ⋅ σ = C ∨ D ⋅ σ ⊂# C"
by (simp add: subset_mset_def)
then show ?thesis
proof
assume "D ⋅ σ = C"
then have "grounding_of_cls C ⊆ grounding_of_cls D"
using subst_cls_eq_grounding_of_cls_subset_eq
by (auto dest: sym)
then have "(grounding_of_state St ∪ grounding_of_cls C) = grounding_of_state St"
using assms unfolding grounding_of_clss_def by auto
then show ?thesis
by (auto intro: sr_ext.derive.intros)
next
assume a: "D ⋅ σ ⊂# C"
then have "grounding_of_cls C ⊆ sr.Rf (grounding_of_state St)"
using strict_subset_subsumption_grounding_redundant_clss assms by auto
then show ?thesis
unfolding grounding_of_clss_def by (force intro: sr_ext.derive.intros)
qed
qed
lemma reduction_in_concls_of:
assumes
"Cμ ∈ grounding_of_cls C" and
"D + {#L'#} ∈ CC" and
"- L = L' ⋅l σ" and
"D ⋅ σ ⊆# C"
shows "Cμ ∈ concls_of (sr_ext.inferences_from (grounding_of_clss (CC ∪ {C + {#L#}})))"
proof -
from assms
obtain μ where
μ_p: "Cμ = C ⋅ μ ∧ is_ground_subst μ"
unfolding grounding_of_cls_def by auto
define γ where
"γ = Infer {#(C + {#L#}) ⋅ μ#} ((D + {#L'#}) ⋅ σ ⋅ μ) (C ⋅ μ)"
have "(D + {#L'#}) ⋅ σ ⋅ μ ∈ grounding_of_clss (CC ∪ {C + {#L#}})"
unfolding grounding_of_clss_def grounding_of_cls_def
by (rule UN_I[of "D + {#L'#}"], use assms(2) in simp,
metis (mono_tags, lifting) μ_p is_ground_comp_subst mem_Collect_eq subst_cls_comp_subst)
moreover have "(C + {#L#}) ⋅ μ ∈ grounding_of_clss (CC ∪ {C + {#L#}})"
using μ_p unfolding grounding_of_clss_def grounding_of_cls_def by auto
moreover have
"∀I. I ⊨ D ⋅ σ ⋅ μ + {#- (L ⋅l μ)#} ⟶ I ⊨ C ⋅ μ + {#L ⋅l μ#} ⟶ I ⊨ D ⋅ σ ⋅ μ + C ⋅ μ"
by auto
then have "∀I. I ⊨ (D + {#L'#}) ⋅ σ ⋅ μ ⟶ I ⊨ (C + {#L#}) ⋅ μ ⟶ I ⊨ D ⋅ σ ⋅ μ + C ⋅ μ"
using assms
by (metis add_mset_add_single subst_cls_add_mset subst_cls_union subst_minus)
then have "∀I. I ⊨ (D + {#L'#}) ⋅ σ ⋅ μ ⟶ I ⊨ (C + {#L#}) ⋅ μ ⟶ I ⊨ C ⋅ μ"
using assms by (metis (no_types, lifting) subset_mset.le_iff_add subst_cls_union true_cls_union)
then have "∀I. I ⊨m {#(D + {#L'#}) ⋅ σ ⋅ μ#} ⟶ I ⊨ (C + {#L#}) ⋅ μ ⟶ I ⊨ C ⋅ μ"
by (meson true_cls_mset_singleton)
ultimately have "γ ∈ sr_ext.inferences_from (grounding_of_clss (CC ∪ {C + {#L#}}))"
unfolding sr_ext.inferences_from_def unfolding ground_sound_Γ_def infer_from_def γ_def by auto
then have "C ⋅ μ ∈ concls_of (sr_ext.inferences_from (grounding_of_clss (CC ∪ {C + {#L#}})))"
using image_iff unfolding γ_def by fastforce
then show "Cμ ∈ concls_of (sr_ext.inferences_from (grounding_of_clss (CC ∪ {C + {#L#}})))"
using μ_p by auto
qed
lemma reduction_derivable:
assumes
"D + {#L'#} ∈ CC" and
"- L = L' ⋅l σ" and
"D ⋅ σ ⊆# C"
shows "sr_ext.derive (grounding_of_clss (CC ∪ {C + {#L#}})) (grounding_of_clss (CC ∪ {C}))"
proof -
from assms have "grounding_of_clss (CC ∪ {C}) - grounding_of_clss (CC ∪ {C + {#L#}})
⊆ concls_of (sr_ext.inferences_from (grounding_of_clss (CC ∪ {C + {#L#}})))"
using reduction_in_concls_of unfolding grounding_of_clss_def by auto
moreover
have "grounding_of_cls (C + {#L#}) ⊆ sr.Rf (grounding_of_clss (CC ∪ {C}))"
using strict_subset_subsumption_grounding_redundant_clss[of C "id_subst"]
by auto
then have "grounding_of_clss (CC ∪ {C + {#L#}}) - grounding_of_clss (CC ∪ {C})
⊆ sr.Rf (grounding_of_clss (CC ∪ {C}))"
unfolding grounding_of_clss_def by auto
ultimately show
"sr_ext.derive (grounding_of_clss (CC ∪ {C + {#L#}})) (grounding_of_clss (CC ∪ {C}))"
using sr_ext.derive.intros[of "grounding_of_clss (CC ∪ {C})"
"grounding_of_clss (CC ∪ {C + {#L#}})"]
by auto
qed
text ‹
The following corresponds the part of Lemma 4.10 that states we have a theorem proving process:
›
lemma RP_ground_derive:
"St ↝ St' ⟹ sr_ext.derive (grounding_of_state St) (grounding_of_state St')"
proof (induction rule: RP.induct)
case (tautology_deletion A C N P Q)
{
fix Cσ
assume "Cσ ∈ grounding_of_cls C"
then obtain σ where
"Cσ = C ⋅ σ"
unfolding grounding_of_cls_def by auto
then have "Neg (A ⋅a σ) ∈# Cσ ∧ Pos (A ⋅a σ) ∈# Cσ"
using tautology_deletion Neg_Melem_subst_atm_subst_cls Pos_Melem_subst_atm_subst_cls by auto
then have "Cσ ∈ sr.Rf (grounding_of_state (N, P, Q))"
using sr.tautology_Rf by auto
}
then have "grounding_of_state (N ∪ {C}, P, Q) - grounding_of_state (N, P, Q)
⊆ sr.Rf (grounding_of_state (N, P, Q))"
unfolding grounding_of_clss_def by auto
moreover have "grounding_of_state (N, P, Q) - grounding_of_state (N ∪ {C}, P, Q) = {}"
unfolding grounding_of_clss_def by auto
ultimately show ?case
using sr_ext.derive.intros[of "grounding_of_state (N, P, Q)"
"grounding_of_state (N ∪ {C}, P, Q)"]
by auto
next
case (forward_subsumption D P Q C N)
then show ?case
using derive_if_remove_subsumed[of D "(N, P, Q)" C] unfolding grounding_of_clss_def
by (simp add: sup_commute sup_left_commute)
next
case (backward_subsumption_P D N C P Q)
then show ?case
using derive_if_remove_subsumed[of D "(N, P, Q)" C] strictly_subsumes_def
unfolding grounding_of_clss_def by (simp add: sup_commute sup_left_commute)
next
case (backward_subsumption_Q D N C P Q)
then show ?case
using derive_if_remove_subsumed[of D "(N, P, Q)" C] strictly_subsumes_def
unfolding grounding_of_clss_def by (simp add: sup_commute sup_left_commute)
next
case (forward_reduction D L' P Q L σ C N)
then show ?case
using reduction_derivable[of _ _ "N ∪ P ∪ Q"] by force
next
case (backward_reduction_P D L' N L σ C P Q)
then show ?case
using reduction_derivable[of _ _ "N ∪ P ∪ Q"] by force
next
case (backward_reduction_Q D L' N L σ C P Q)
then show ?case
using reduction_derivable[of _ _ "N ∪ P ∪ Q"] by force
next
case (clause_processing N C P Q)
then show ?case
using sr_ext.derive.intros by auto
next
case (inference_computation N Q C P)
{
fix Eμ
assume "Eμ ∈ grounding_of_clss N"
then obtain μ E where
E_μ_p: "Eμ = E ⋅ μ ∧ E ∈ N ∧ is_ground_subst μ"
unfolding grounding_of_clss_def grounding_of_cls_def by auto
then have E_concl: "E ∈ concls_of (ord_FO_resolution.inferences_between Q C)"
using inference_computation by auto
then obtain γ where
γ_p: "γ ∈ ord_FO_Γ S ∧ infer_from (Q ∪ {C}) γ ∧ C ∈# prems_of γ ∧ concl_of γ = E"
unfolding ord_FO_resolution.inferences_between_def by auto
then obtain CC CAs D AAs As σ where
γ_p2: "γ = Infer CC D E ∧ ord_resolve_rename S CAs D AAs As σ E ∧ mset CAs = CC"
unfolding ord_FO_Γ_def by auto
define ρ where
"ρ = hd (renamings_apart (D # CAs))"
define ρs where
"ρs = tl (renamings_apart (D # CAs))"
define γ_ground where
"γ_ground = Infer (mset (CAs ⋅⋅cl ρs) ⋅cm σ ⋅cm μ) (D ⋅ ρ ⋅ σ ⋅ μ) (E ⋅ μ)"
have "∀I. I ⊨m mset (CAs ⋅⋅cl ρs) ⋅cm σ ⋅cm μ ⟶ I ⊨ D ⋅ ρ ⋅ σ ⋅ μ ⟶ I ⊨ E ⋅ μ"
using ord_resolve_rename_ground_inst_sound[of _ _ _ _ _ _ _ _ _ _ μ] ρ_def ρs_def E_μ_p γ_p2
by auto
then have "γ_ground ∈ {Infer cc d e | cc d e. ∀I. I ⊨m cc ⟶ I ⊨ d ⟶ I ⊨ e}"
unfolding γ_ground_def by auto
moreover have "set_mset (prems_of γ_ground) ⊆ grounding_of_state ({}, P ∪ {C}, Q)"
proof -
have "D = C ∨ D ∈ Q"
unfolding γ_ground_def using E_μ_p γ_p2 γ_p unfolding infer_from_def
unfolding grounding_of_clss_def grounding_of_cls_def by simp
then have "D ⋅ ρ ⋅ σ ⋅ μ ∈ grounding_of_cls C ∨ (∃x ∈ Q. D ⋅ ρ ⋅ σ ⋅ μ ∈ grounding_of_cls x)"
using E_μ_p
unfolding grounding_of_cls_def
by (metis (mono_tags, lifting) is_ground_comp_subst mem_Collect_eq subst_cls_comp_subst)
then have "(D ⋅ ρ ⋅ σ ⋅ μ ∈ grounding_of_cls C ∨
(∃x ∈ P. D ⋅ ρ ⋅ σ ⋅ μ ∈ grounding_of_cls x) ∨
(∃x ∈ Q. D ⋅ ρ ⋅ σ ⋅ μ ∈ grounding_of_cls x))"
by metis
moreover have "∀i < length (CAs ⋅⋅cl ρs ⋅cl σ ⋅cl μ). (CAs ⋅⋅cl ρs ⋅cl σ ⋅cl μ) ! i ∈
{C ⋅ σ |σ. is_ground_subst σ} ∪
((⋃C ∈ P. {C ⋅ σ | σ. is_ground_subst σ}) ∪ (⋃C∈Q. {C ⋅ σ | σ. is_ground_subst σ}))"
proof (rule, rule)
fix i
assume "i < length (CAs ⋅⋅cl ρs ⋅cl σ ⋅cl μ)"
then have a: "i < length CAs ∧ i < length ρs"
by simp
moreover from a have "CAs ! i ∈ {C} ∪ Q"
using γ_p2 γ_p unfolding infer_from_def
by (metis (no_types, lifting) Un_subset_iff inference.sel(1) set_mset_union
sup_commute nth_mem_mset subsetCE)
ultimately have "(CAs ⋅⋅cl ρs ⋅cl σ ⋅cl μ) ! i ∈
{C ⋅ σ |σ. is_ground_subst σ} ∨
((CAs ⋅⋅cl ρs ⋅cl σ ⋅cl μ) ! i ∈ (⋃C∈P. {C ⋅ σ |σ. is_ground_subst σ}) ∨
(CAs ⋅⋅cl ρs ⋅cl σ ⋅cl μ) ! i ∈ (⋃C ∈ Q. {C ⋅ σ | σ. is_ground_subst σ}))"
using E_μ_p γ_p2 γ_p
unfolding γ_ground_def infer_from_def grounding_of_clss_def grounding_of_cls_def
apply -
apply (cases "CAs ! i = C")
subgoal
apply (rule disjI1)
apply (rule Set.CollectI)
apply (rule_tac x = "(ρs ! i) ⊙ σ ⊙ μ" in exI)
using ρs_def using renamings_apart_length by (auto; fail)
subgoal
apply (rule disjI2)
apply (rule disjI2)
apply (rule_tac a = "CAs ! i" in UN_I)
subgoal by blast
subgoal
apply (rule Set.CollectI)
apply (rule_tac x = "(ρs ! i) ⊙ σ ⊙ μ" in exI)
using ρs_def using renamings_apart_length by (auto; fail)
done
done
then show "(CAs ⋅⋅cl ρs ⋅cl σ ⋅cl μ) ! i ∈ {C ⋅ σ |σ. is_ground_subst σ} ∪
((⋃C ∈ P. {C ⋅ σ |σ. is_ground_subst σ}) ∪ (⋃C ∈ Q. {C ⋅ σ |σ. is_ground_subst σ}))"
by blast
qed
then have "∀x ∈# mset (CAs ⋅⋅cl ρs ⋅cl σ ⋅cl μ). x ∈ {C ⋅ σ |σ. is_ground_subst σ} ∪
((⋃C ∈ P. {C ⋅ σ |σ. is_ground_subst σ}) ∪ (⋃C ∈ Q. {C ⋅ σ |σ. is_ground_subst σ}))"
by (metis (lifting) in_set_conv_nth set_mset_mset)
then have "set_mset (mset (CAs ⋅⋅cl ρs) ⋅cm σ ⋅cm μ) ⊆
grounding_of_cls C ∪ grounding_of_clss P ∪ grounding_of_clss Q"
unfolding grounding_of_cls_def grounding_of_clss_def
using mset_subst_cls_list_subst_cls_mset by auto
ultimately show ?thesis
unfolding γ_ground_def grounding_of_clss_def by auto
qed
ultimately have
"E ⋅ μ ∈ concls_of (sr_ext.inferences_from (grounding_of_state ({}, P ∪ {C}, Q)))"
unfolding sr_ext.inferences_from_def inference_system.inferences_from_def ground_sound_Γ_def
infer_from_def
using γ_ground_def by (metis (mono_tags, lifting) image_eqI inference.sel(3) mem_Collect_eq)
then have "Eμ ∈ concls_of (sr_ext.inferences_from (grounding_of_state ({}, P ∪ {C}, Q)))"
using E_μ_p by auto
}
then have "grounding_of_state (N, P, Q ∪ {C}) - grounding_of_state ({}, P ∪ {C}, Q)
⊆ concls_of (sr_ext.inferences_from (grounding_of_state ({}, P ∪ {C}, Q)))"
unfolding grounding_of_clss_def by auto
moreover have "grounding_of_state ({}, P ∪ {C}, Q) - grounding_of_state (N, P, Q ∪ {C}) = {}"
unfolding grounding_of_clss_def by auto
ultimately show ?case
using sr_ext.derive.intros[of "(grounding_of_state (N, P, Q ∪ {C}))"
"(grounding_of_state ({}, P ∪ {C}, Q))"] by auto
qed
text ‹
A useful consequence:
›
theorem RP_model: "St ↝ St' ⟹ I ⊨s grounding_of_state St' ⟷ I ⊨s grounding_of_state St"
proof (drule RP_ground_derive, erule sr_ext.derive.cases, hypsubst)
let
?gSt = "grounding_of_state St" and
?gSt' = "grounding_of_state St'"
assume
deduct: "?gSt' - ?gSt ⊆ concls_of (sr_ext.inferences_from ?gSt)" (is "_ ⊆ ?concls") and
delete: "?gSt - ?gSt' ⊆ sr.Rf ?gSt'"
show "I ⊨s ?gSt' ⟷ I ⊨s ?gSt"
proof
assume bef: "I ⊨s ?gSt"
then have "I ⊨s ?concls"
unfolding ground_sound_Γ_def inference_system.inferences_from_def true_clss_def
true_cls_mset_def
by (auto simp add: image_def infer_from_def dest!: spec[of _ I])
then have diff: "I ⊨s ?gSt' - ?gSt"
using deduct by (blast intro: true_clss_mono)
then show "I ⊨s ?gSt'"
using bef unfolding true_clss_def by blast
next
assume aft: "I ⊨s ?gSt'"
have "I ⊨s ?gSt' ∪ sr.Rf ?gSt'"
by (rule sr.Rf_model) (smt (verit) Diff_eq_empty_iff Diff_subset Un_Diff aft
standard_redundancy_criterion.Rf_mono sup_bot.right_neutral sup_ge1 true_clss_mono)
then have "I ⊨s sr.Rf ?gSt'"
using true_clss_union by blast
then have diff: "I ⊨s ?gSt - ?gSt'"
using delete by (blast intro: true_clss_mono)
then show "I ⊨s ?gSt"
using aft unfolding true_clss_def by blast
qed
qed
text ‹
Another formulation of the part of Lemma 4.10 that states we have a theorem proving process:
›
lemma ground_derive_chain: "chain (↝) Sts ⟹ chain sr_ext.derive (lmap grounding_of_state Sts)"
using RP_ground_derive by (simp add: chain_lmap[of "(↝)"])
text ‹
The following is used prove to Lemma 4.11:
›
lemma Sup_llist_grounding_of_state_ground:
assumes "C ∈ Sup_llist (lmap grounding_of_state Sts)"
shows "is_ground_cls C"
proof -
have "∃j. enat j < llength (lmap grounding_of_state Sts)
∧ C ∈ lnth (lmap grounding_of_state Sts) j"
using assms Sup_llist_imp_exists_index by fast
then show ?thesis
unfolding grounding_of_clss_def grounding_of_cls_def by auto
qed
lemma Liminf_grounding_of_state_ground:
"C ∈ Liminf_llist (lmap grounding_of_state Sts) ⟹ is_ground_cls C"
using Liminf_llist_subset_Sup_llist[of "lmap grounding_of_state Sts"]
Sup_llist_grounding_of_state_ground
by blast
lemma in_Sup_llist_in_Sup_state:
assumes "C ∈ Sup_llist (lmap grounding_of_state Sts)"
shows "∃D σ. D ∈ clss_of_state (Sup_state Sts) ∧ D ⋅ σ = C ∧ is_ground_subst σ"
proof -
from assms obtain i where
i_p: "enat i < llength Sts ∧ C ∈ lnth (lmap grounding_of_state Sts) i"
using Sup_llist_imp_exists_index by fastforce
then obtain D σ where
"D ∈ clss_of_state (lnth Sts i) ∧ D ⋅ σ = C ∧ is_ground_subst σ"
using assms unfolding grounding_of_clss_def grounding_of_cls_def by fastforce
then have "D ∈ clss_of_state (Sup_state Sts) ∧ D ⋅ σ = C ∧ is_ground_subst σ"
using i_p unfolding Sup_state_def
by (metis (no_types, lifting) UnCI UnE contra_subsetD N_of_state.simps P_of_state.simps
Q_of_state.simps llength_lmap lnth_lmap lnth_subset_Sup_llist)
then show ?thesis
by auto
qed
lemma
N_of_state_Liminf: "N_of_state (Liminf_state Sts) = Liminf_llist (lmap N_of_state Sts)" and
P_of_state_Liminf: "P_of_state (Liminf_state Sts) = Liminf_llist (lmap P_of_state Sts)"
unfolding Liminf_state_def by auto
lemma eventually_removed_from_N:
assumes
d_in: "D ∈ N_of_state (lnth Sts i)" and
fair: "fair_state_seq Sts" and
i_Sts: "enat i < llength Sts"
shows "∃l. D ∈ N_of_state (lnth Sts l) ∧ D ∉ N_of_state (lnth Sts (Suc l)) ∧ i ≤ l
∧ enat (Suc l) < llength Sts"
proof (rule ccontr)
assume a: "¬ ?thesis"
have "i ≤ l ⟹ enat l < llength Sts ⟹ D ∈ N_of_state (lnth Sts l)" for l
using d_in by (induction l, blast, metis a Suc_ile_eq le_SucE less_imp_le)
then have "D ∈ Liminf_llist (lmap N_of_state Sts)"
unfolding Liminf_llist_def using i_Sts by auto
then show False
using fair unfolding fair_state_seq_def by (simp add: N_of_state_Liminf)
qed
lemma eventually_removed_from_P:
assumes
d_in: "D ∈ P_of_state (lnth Sts i)" and
fair: "fair_state_seq Sts" and
i_Sts: "enat i < llength Sts"
shows "∃l. D ∈ P_of_state (lnth Sts l) ∧ D ∉ P_of_state (lnth Sts (Suc l)) ∧ i ≤ l
∧ enat (Suc l) < llength Sts"
proof (rule ccontr)
assume a: "¬ ?thesis"
have "i ≤ l ⟹ enat l < llength Sts ⟹ D ∈ P_of_state (lnth Sts l)" for l
using d_in by (induction l, blast, metis a Suc_ile_eq le_SucE less_imp_le)
then have "D ∈ Liminf_llist (lmap P_of_state Sts)"
unfolding Liminf_llist_def using i_Sts by auto
then show False
using fair unfolding fair_state_seq_def by (simp add: P_of_state_Liminf)
qed
lemma instance_if_subsumed_and_in_limit:
assumes
deriv: "chain (↝) Sts" and
ns: "Gs = lmap grounding_of_state Sts" and
c: "C ∈ Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
d: "D ∈ clss_of_state (lnth Sts i)" "enat i < llength Sts" "subsumes D C"
shows "∃σ. D ⋅ σ = C ∧ is_ground_subst σ"
proof -
let ?Ps = "λi. P_of_state (lnth Sts i)"
let ?Qs = "λi. Q_of_state (lnth Sts i)"
have ground_C: "is_ground_cls C"
using c using Liminf_grounding_of_state_ground ns by auto
have derivns: "chain sr_ext.derive Gs"
using ground_derive_chain deriv ns by auto
have "∃σ. D ⋅ σ = C"
proof (rule ccontr)
assume "∄σ. D ⋅ σ = C"
moreover from d(3) obtain τ_proto where
"D ⋅ τ_proto ⊆# C" unfolding subsumes_def
by blast
then obtain τ where
τ_p: "D ⋅ τ ⊆# C ∧ is_ground_subst τ"
using ground_C by (metis is_ground_cls_mono make_ground_subst subset_mset.order_refl)
ultimately have subsub: "D ⋅ τ ⊂# C"
using subset_mset.le_imp_less_or_eq by auto
moreover have "is_ground_subst τ"
using τ_p by auto
moreover have "D ∈ clss_of_state (lnth Sts i)"
using d by auto
ultimately have "C ∈ sr.Rf (grounding_of_state (lnth Sts i))"
using strict_subset_subsumption_redundant_clss by auto
then have "C ∈ sr.Rf (Sup_llist Gs)"
using d ns by (smt (verit) contra_subsetD llength_lmap lnth_lmap lnth_subset_Sup_llist sr.Rf_mono)
then have "C ∈ sr.Rf (Liminf_llist Gs)"
unfolding ns using local.sr_ext.Rf_limit_Sup derivns ns by auto
then show False
using c by auto
qed
then obtain σ where
"D ⋅ σ = C ∧ is_ground_subst σ"
using ground_C by (metis make_ground_subst)
then show ?thesis
by auto
qed
lemma from_Q_to_Q_inf:
assumes
deriv: "chain (↝) Sts" and
fair: "fair_state_seq Sts" and
ns: "Gs = lmap grounding_of_state Sts" and
c: "C ∈ Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
d: "D ∈ Q_of_state (lnth Sts i)" "enat i < llength Sts" "subsumes D C" and
d_least: "∀E ∈ {E. E ∈ (clss_of_state (Sup_state Sts)) ∧ subsumes E C}.
¬ strictly_subsumes E D"
shows "D ∈ Q_of_state (Liminf_state Sts)"
proof -
let ?Ps = "λi. P_of_state (lnth Sts i)"
let ?Qs = "λi. Q_of_state (lnth Sts i)"
have ground_C: "is_ground_cls C"
using c using Liminf_grounding_of_state_ground ns by auto
have derivns: "chain sr_ext.derive Gs"
using ground_derive_chain deriv ns by auto
have "∃σ. D ⋅ σ = C ∧ is_ground_subst σ"
using instance_if_subsumed_and_in_limit[OF deriv] c d unfolding ns by blast
then obtain σ where
σ: "D ⋅ σ = C" "is_ground_subst σ"
by auto
have in_Sts_in_Sts_Suc:
"∀l ≥ i. enat (Suc l) < llength Sts ⟶ D ∈ Q_of_state (lnth Sts l) ⟶
D ∈ Q_of_state (lnth Sts (Suc l))"
proof (rule, rule, rule, rule)
fix l
assume
len: "i ≤ l" and
llen: "enat (Suc l) < llength Sts" and
d_in_q: "D ∈ Q_of_state (lnth Sts l)"
have "lnth Sts l ↝ lnth Sts (Suc l)"
using llen deriv chain_lnth_rel by blast
then show "D ∈ Q_of_state (lnth Sts (Suc l))"
proof (cases rule: RP.cases)
case (backward_subsumption_Q D' N D_removed P Q)
moreover
{
assume "D_removed = D"
then obtain D_subsumes where
D_subsumes_p: "D_subsumes ∈ N ∧ strictly_subsumes D_subsumes D"
using backward_subsumption_Q by auto
moreover from D_subsumes_p have "subsumes D_subsumes C"
using d subsumes_trans unfolding strictly_subsumes_def by blast
moreover from backward_subsumption_Q have "D_subsumes ∈ clss_of_state (Sup_state Sts)"
using D_subsumes_p llen
by (metis (no_types) UnI1 N_of_state.simps llength_lmap lnth_lmap lnth_subset_Sup_llist
rev_subsetD Sup_state_def)
ultimately have False
using d_least unfolding subsumes_def by auto
}
ultimately show ?thesis
using d_in_q by auto
next
case (backward_reduction_Q E L' N L σ D' P Q)
{
assume "D' + {#L#} = D"
then have D'_p: "strictly_subsumes D' D ∧ D' ∈ ?Ps (Suc l)"
using subset_strictly_subsumes[of D' D] backward_reduction_Q by auto
then have subc: "subsumes D' C"
using d(3) subsumes_trans unfolding strictly_subsumes_def by auto
from D'_p have "D' ∈ clss_of_state (Sup_state Sts)"
using llen by (metis (no_types) UnI1 P_of_state.simps llength_lmap lnth_lmap
lnth_subset_Sup_llist subsetCE sup_ge2 Sup_state_def)
then have False
using d_least D'_p subc by auto
}
then show ?thesis
using backward_reduction_Q d_in_q by auto
qed (use d_in_q in auto)
qed
have D_in_Sts: "D ∈ Q_of_state (lnth Sts l)" and D_in_Sts_Suc: "D ∈ Q_of_state (lnth Sts (Suc l))"
if l_i: "l ≥ i" and enat: "enat (Suc l) < llength Sts" for l
proof -
show "D ∈ Q_of_state (lnth Sts l)"
using l_i enat
apply (induction "l - i" arbitrary: l)
subgoal using d by auto
subgoal using d(1) in_Sts_in_Sts_Suc
by (metis (no_types, lifting) Suc_ile_eq add_Suc_right add_diff_cancel_left' le_SucE
le_Suc_ex less_imp_le)
done
then show "D ∈ Q_of_state (lnth Sts (Suc l))"
using l_i enat in_Sts_in_Sts_Suc by blast
qed
have "i ≤ x ⟹ enat x < llength Sts ⟹ D ∈ Q_of_state (lnth Sts x)" for x
apply (cases x)
subgoal using d(1) by (auto intro!: exI[of _ i] simp: less_Suc_eq)
subgoal for x'
using d(1) D_in_Sts_Suc[of x'] by (cases ‹i ≤ x'›) (auto simp: not_less_eq_eq)
done
then have "D ∈ Liminf_llist (lmap Q_of_state Sts)"
unfolding Liminf_llist_def by (auto intro!: exI[of _ i] simp: d)
then show ?thesis
unfolding Liminf_state_def by auto
qed
lemma from_P_to_Q:
assumes
deriv: "chain (↝) Sts" and
fair: "fair_state_seq Sts" and
ns: "Gs = lmap grounding_of_state Sts" and
c: "C ∈ Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
d: "D ∈ P_of_state (lnth Sts i)" "enat i < llength Sts" "subsumes D C" and
d_least: "∀E ∈ {E. E ∈ (clss_of_state (Sup_state Sts)) ∧ subsumes E C}.
¬ strictly_subsumes E D"
shows "∃l. D ∈ Q_of_state (lnth Sts l) ∧ enat l < llength Sts"
proof -
let ?Ns = "λi. N_of_state (lnth Sts i)"
let ?Ps = "λi. P_of_state (lnth Sts i)"
let ?Qs = "λi. Q_of_state (lnth Sts i)"
have ground_C: "is_ground_cls C"
using c using Liminf_grounding_of_state_ground ns by auto
have derivns: "chain sr_ext.derive Gs"
using ground_derive_chain deriv ns by auto
have "∃σ. D ⋅ σ = C ∧ is_ground_subst σ"
using instance_if_subsumed_and_in_limit[OF deriv] ns c d by blast
then obtain σ where
σ: "D ⋅ σ = C" "is_ground_subst σ"
by auto
obtain l where
l_p: "D ∈ P_of_state (lnth Sts l) ∧ D ∉ P_of_state (lnth Sts (Suc l)) ∧ i ≤ l
∧ enat (Suc l) < llength Sts"
using fair using eventually_removed_from_P d unfolding ns by auto
then have l_Gs: "enat (Suc l) < llength Gs"
using ns by auto
from l_p have "lnth Sts l ↝ lnth Sts (Suc l)"
using deriv using chain_lnth_rel by auto
then show ?thesis
proof (cases rule: RP.cases)
case (backward_subsumption_P D' N D_twin P Q)
note lrhs = this(1,2) and D'_p = this(3,4)
then have twins: "D_twin = D" "?Ns (Suc l) = N" "?Ns l = N" "?Ps (Suc l) = P"
"?Ps l = P ∪ {D_twin}" "?Qs (Suc l) = Q" "?Qs l = Q"
using l_p by auto
note D'_p = D'_p[unfolded twins(1)]
then have subc: "subsumes D' C"
unfolding strictly_subsumes_def subsumes_def using σ
by (metis subst_cls_comp_subst subst_cls_mono_mset)
from D'_p have "D' ∈ clss_of_state (Sup_state Sts)"
unfolding twins(2)[symmetric] using l_p
by (metis (no_types) UnI1 N_of_state.simps llength_lmap lnth_lmap lnth_subset_Sup_llist
subsetCE Sup_state_def)
then have False
using d_least D'_p subc by auto
then show ?thesis
by auto
next
case (backward_reduction_P E L' N L σ D' P Q)
then have twins: "D' + {#L#} = D" "?Ns (Suc l) = N" "?Ns l = N" "?Ps (Suc l) = P ∪ {D'}"
"?Ps l = P ∪ {D' + {#L#}}" "?Qs (Suc l) = Q" "?Qs l = Q"
using l_p by auto
then have D'_p: "strictly_subsumes D' D ∧ D' ∈ ?Ps (Suc l)"
using subset_strictly_subsumes[of D' D] by auto
then have subc: "subsumes D' C"
using d(3) subsumes_trans unfolding strictly_subsumes_def by auto
from D'_p have "D' ∈ clss_of_state (Sup_state Sts)"
using l_p by (metis (no_types) UnI1 P_of_state.simps llength_lmap lnth_lmap
lnth_subset_Sup_llist subsetCE sup_ge2 Sup_state_def)
then have False
using d_least D'_p subc by auto
then show ?thesis
by auto
next
case (inference_computation N Q D_twin P)
then have twins: "D_twin = D" "?Ps (Suc l) = P" "?Ps l = P ∪ {D_twin}"
"?Qs (Suc l) = Q ∪ {D_twin}" "?Qs l = Q"
using l_p by auto
then show ?thesis
using d σ l_p by auto
qed (use l_p in auto)
qed
lemma from_N_to_P_or_Q:
assumes
deriv: "chain (↝) Sts" and
fair: "fair_state_seq Sts" and
ns: "Gs = lmap grounding_of_state Sts" and
c: "C ∈ Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
d: "D ∈ N_of_state (lnth Sts i)" "enat i < llength Sts" "subsumes D C" and
d_least: "∀E ∈ {E. E ∈ (clss_of_state (Sup_state Sts)) ∧ subsumes E C}. ¬ strictly_subsumes E D"
shows "∃l D' σ'. D' ∈ P_of_state (lnth Sts l) ∪ Q_of_state (lnth Sts l) ∧
enat l < llength Sts ∧
(∀E ∈ {E. E ∈ (clss_of_state (Sup_state Sts)) ∧ subsumes E C}. ¬ strictly_subsumes E D') ∧
D' ⋅ σ' = C ∧ is_ground_subst σ' ∧ subsumes D' C"
proof -
let ?Ns = "λi. N_of_state (lnth Sts i)"
let ?Ps = "λi. P_of_state (lnth Sts i)"
let ?Qs = "λi. Q_of_state (lnth Sts i)"
have ground_C: "is_ground_cls C"
using c using Liminf_grounding_of_state_ground ns by auto
have derivns: "chain sr_ext.derive Gs"
using ground_derive_chain deriv ns by auto
have "∃σ. D ⋅ σ = C ∧ is_ground_subst σ"
using instance_if_subsumed_and_in_limit[OF deriv] ns c d by blast
then obtain σ where
σ: "D ⋅ σ = C" "is_ground_subst σ"
by auto
from c have no_taut: "¬ (∃A. Pos A ∈# C ∧ Neg A ∈# C)"
using sr.tautology_Rf by auto
have "∃l. D ∈ N_of_state (lnth Sts l)
∧ D ∉ N_of_state (lnth Sts (Suc l)) ∧ i ≤ l ∧ enat (Suc l) < llength Sts"
using fair using eventually_removed_from_N d unfolding ns by auto
then obtain l where
l_p: "D ∈ N_of_state (lnth Sts l) ∧ D ∉ N_of_state (lnth Sts (Suc l)) ∧ i ≤ l
∧ enat (Suc l) < llength Sts"
by auto
then have l_Gs: "enat (Suc l) < llength Gs"
using ns by auto
from l_p have "lnth Sts l ↝ lnth Sts (Suc l)"
using deriv using chain_lnth_rel by auto
then show ?thesis
proof (cases rule: RP.cases)
case (tautology_deletion A D_twin N P Q)
then have "D_twin = D"
using l_p by auto
then have "Pos (A ⋅a σ) ∈# C ∧ Neg (A ⋅a σ) ∈# C"
using tautology_deletion(3,4) σ
by (metis Melem_subst_cls eql_neg_lit_eql_atm eql_pos_lit_eql_atm)
then have False
using no_taut by metis
then show ?thesis
by blast
next
case (forward_subsumption D' P Q D_twin N)
note lrhs = this(1,2) and D'_p = this(3,4)
then have twins: "D_twin = D" "?Ns (Suc l) = N" "?Ns l = N ∪ {D_twin}" "?Ps (Suc l) = P "
"?Ps l = P" "?Qs (Suc l) = Q" "?Qs l = Q"
using l_p by auto
note D'_p = D'_p[unfolded twins(1)]
from D'_p(2) have subs: "subsumes D' C"
using d(3) by (blast intro: subsumes_trans)
moreover have "D' ∈ clss_of_state (Sup_state Sts)"
using twins D'_p l_p unfolding Sup_state_def
by simp (metis (no_types) contra_subsetD llength_lmap lnth_lmap lnth_subset_Sup_llist)
ultimately have "¬ strictly_subsumes D' D"
using d_least by auto
then have "subsumes D D'"
unfolding strictly_subsumes_def using D'_p by auto
then have v: "variants D D'"
using D'_p unfolding variants_iff_subsumes by auto
then have mini: "∀E ∈ {E ∈ clss_of_state (Sup_state Sts). subsumes E C}.
¬ strictly_subsumes E D'"
using d_least D'_p neg_strictly_subsumes_variants[of _ D D'] by auto
from v have "∃σ'. D' ⋅ σ' = C"
using σ variants_imp_exists_substitution variants_sym by (metis subst_cls_comp_subst)
then have "∃σ'. D' ⋅ σ' = C ∧ is_ground_subst σ'"
using ground_C by (meson make_ground_subst refl)
then obtain σ' where
σ'_p: "D' ⋅ σ' = C ∧ is_ground_subst σ'"
by metis
show ?thesis
using D'_p twins l_p subs mini σ'_p by auto
next
case (forward_reduction E L' P Q L σ D' N)
then have twins: "D' + {#L#} = D" "?Ns (Suc l) = N ∪ {D'}" "?Ns l = N ∪ {D' + {#L#}}"
"?Ps (Suc l) = P " "?Ps l = P" "?Qs (Suc l) = Q" "?Qs l = Q"
using l_p by auto
then have D'_p: "strictly_subsumes D' D ∧ D' ∈ ?Ns (Suc l)"
using subset_strictly_subsumes[of D' D] by auto
then have subc: "subsumes D' C"
using d(3) subsumes_trans unfolding strictly_subsumes_def by blast
from D'_p have "D' ∈ clss_of_state (Sup_state Sts)"
using l_p by (metis (no_types) UnI1 N_of_state.simps llength_lmap lnth_lmap
lnth_subset_Sup_llist subsetCE Sup_state_def)
then have False
using d_least D'_p subc by auto
then show ?thesis
by auto
next
case (clause_processing N D_twin P Q)
then have twins: "D_twin = D" "?Ns (Suc l) = N" "?Ns l = N ∪ {D}" "?Ps (Suc l) = P ∪ {D}"
"?Ps l = P" "?Qs (Suc l) = Q" "?Qs l = Q"
using l_p by auto
then show ?thesis
using d σ l_p d_least by blast
qed (use l_p in auto)
qed
lemma eventually_in_Qinf:
assumes
deriv: "chain (↝) Sts" and
D_p: "D ∈ clss_of_state (Sup_state Sts)"
"subsumes D C" "∀E ∈ {E. E ∈ (clss_of_state (Sup_state Sts)) ∧ subsumes E C}.
¬ strictly_subsumes E D" and
fair: "fair_state_seq Sts" and
ns: "Gs = lmap grounding_of_state Sts" and
c: "C ∈ Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
ground_C: "is_ground_cls C"
shows "∃D' σ'. D' ∈ Q_of_state (Liminf_state Sts) ∧ D' ⋅ σ' = C ∧ is_ground_subst σ'"
proof -
let ?Ns = "λi. N_of_state (lnth Sts i)"
let ?Ps = "λi. P_of_state (lnth Sts i)"
let ?Qs = "λi. Q_of_state (lnth Sts i)"
from D_p obtain i where
i_p: "i < llength Sts" "D ∈ ?Ns i ∨ D ∈ ?Ps i ∨ D ∈ ?Qs i"
unfolding Sup_state_def
by simp_all (metis (no_types) Sup_llist_imp_exists_index llength_lmap lnth_lmap)
have derivns: "chain sr_ext.derive Gs"
using ground_derive_chain deriv ns by auto
have "∃σ. D ⋅ σ = C ∧ is_ground_subst σ"
using instance_if_subsumed_and_in_limit[OF deriv ns c] D_p i_p by blast
then obtain σ where
σ: "D ⋅ σ = C" "is_ground_subst σ"
by blast
{
assume a: "D ∈ ?Ns i"
then obtain D' σ' l where D'_p:
"D' ∈ ?Ps l ∪ ?Qs l"
"D' ⋅ σ' = C"
"enat l < llength Sts"
"is_ground_subst σ'"
"∀E ∈ {E. E ∈ (clss_of_state (Sup_state Sts)) ∧ subsumes E C}. ¬ strictly_subsumes E D'"
"subsumes D' C"
using from_N_to_P_or_Q deriv fair ns c i_p(1) D_p(2) D_p(3) by blast
then obtain l' where
l'_p: "D' ∈ ?Qs l'" "l' < llength Sts"
using from_P_to_Q[OF deriv fair ns c _ D'_p(3) D'_p(6) D'_p(5)] by blast
then have "D' ∈ Q_of_state (Liminf_state Sts)"
using from_Q_to_Q_inf[OF deriv fair ns c _ l'_p(2)] D'_p by auto
then have ?thesis
using D'_p by auto
}
moreover
{
assume a: "D ∈ ?Ps i"
then obtain l' where
l'_p: "D ∈ ?Qs l'" "l' < llength Sts"
using from_P_to_Q[OF deriv fair ns c a i_p(1) D_p(2) D_p(3)] by auto
then have "D ∈ Q_of_state (Liminf_state Sts)"
using from_Q_to_Q_inf[OF deriv fair ns c l'_p(1) l'_p(2)] D_p(3) σ(1) σ(2) D_p(2) by auto
then have ?thesis
using D_p σ by auto
}
moreover
{
assume a: "D ∈ ?Qs i"
then have "D ∈ Q_of_state (Liminf_state Sts)"
using from_Q_to_Q_inf[OF deriv fair ns c a i_p(1)] σ D_p(2,3) by auto
then have ?thesis
using D_p σ by auto
}
ultimately show ?thesis
using i_p by auto
qed
text ‹
The following corresponds to Lemma 4.11:
›
lemma fair_imp_Liminf_minus_Rf_subset_ground_Liminf_state:
assumes
deriv: "chain (↝) Sts" and
fair: "fair_state_seq Sts" and
ns: "Gs = lmap grounding_of_state Sts"
shows "Liminf_llist Gs - sr.Rf (Liminf_llist Gs)
⊆ grounding_of_clss (Q_of_state (Liminf_state Sts))"
proof
let ?Ns = "λi. N_of_state (lnth Sts i)"
let ?Ps = "λi. P_of_state (lnth Sts i)"
let ?Qs = "λi. Q_of_state (lnth Sts i)"
have SQinf: "clss_of_state (Liminf_state Sts) = Liminf_llist (lmap Q_of_state Sts)"
using fair unfolding fair_state_seq_def Liminf_state_def by auto
fix C
assume C_p: "C ∈ Liminf_llist Gs - sr.Rf (Liminf_llist Gs)"
then have "C ∈ Sup_llist Gs"
using Liminf_llist_subset_Sup_llist[of Gs] by blast
then obtain D_proto where
"D_proto ∈ clss_of_state (Sup_state Sts) ∧ subsumes D_proto C"
using in_Sup_llist_in_Sup_state unfolding ns subsumes_def by blast
then obtain D where
D_p: "D ∈ clss_of_state (Sup_state Sts)"
"subsumes D C"
"∀E ∈ {E. E ∈ clss_of_state (Sup_state Sts) ∧ subsumes E C}. ¬ strictly_subsumes E D"
using strictly_subsumes_has_minimum[of "{E. E ∈ clss_of_state (Sup_state Sts) ∧ subsumes E C}"]
by auto
have ground_C: "is_ground_cls C"
using C_p using Liminf_grounding_of_state_ground ns by auto
have "∃D' σ'. D' ∈ Q_of_state (Liminf_state Sts) ∧ D' ⋅ σ' = C ∧ is_ground_subst σ'"
using eventually_in_Qinf[of D C Gs] using D_p(1-3) deriv fair ns C_p ground_C by auto
then obtain D' σ' where
D'_p: "D' ∈ Q_of_state (Liminf_state Sts) ∧ D' ⋅ σ' = C ∧ is_ground_subst σ'"
by blast
then have "D' ∈ clss_of_state (Liminf_state Sts)"
by simp
then have "C ∈ grounding_of_state (Liminf_state Sts)"
unfolding grounding_of_clss_def grounding_of_cls_def using D'_p by auto
then show "C ∈ grounding_of_clss (Q_of_state (Liminf_state Sts))"
using SQinf fair fair_state_seq_def by auto
qed
text ‹
The following corresponds to (one direction of) Theorem 4.13:
›
lemma subseteq_Liminf_state_eventually_always:
fixes CC
assumes
"finite CC" and
"CC ≠ {}" and
"CC ⊆ Q_of_state (Liminf_state Sts)"
shows "∃j. enat j < llength Sts ∧ (∀j' ≥ enat j. j' < llength Sts ⟶ CC ⊆ Q_of_state (lnth Sts j'))"
proof -
from assms(3) have "∀C ∈ CC. ∃j. enat j < llength Sts ∧
(∀j' ≥ enat j. j' < llength Sts ⟶ C ∈ Q_of_state (lnth Sts j'))"
unfolding Liminf_state_def Liminf_llist_def by force
then obtain f where
f_p: "∀C ∈ CC. f C < llength Sts ∧ (∀j' ≥ enat (f C). j' < llength Sts ⟶ C ∈ Q_of_state (lnth Sts j'))"
by moura
define j :: nat where
"j = Max (f ` CC)"
have "enat j < llength Sts"
unfolding j_def using f_p assms(1)
by (metis (mono_tags) Max_in assms(2) finite_imageI imageE image_is_empty)
moreover have "∀C j'. C ∈ CC ⟶ enat j ≤ j' ⟶ j' < llength Sts ⟶ C ∈ Q_of_state (lnth Sts j')"
proof (intro allI impI)
fix C :: "'a clause" and j' :: nat
assume a: "C ∈ CC" "enat j ≤ enat j'" "enat j' < llength Sts"
then have "f C ≤ j'"
unfolding j_def using assms(1) Max.bounded_iff by auto
then show "C ∈ Q_of_state (lnth Sts j')"
using f_p a by auto
qed
ultimately show ?thesis
by auto
qed
lemma empty_clause_in_Q_of_Liminf_state:
assumes
deriv: "chain (↝) Sts" and
fair: "fair_state_seq Sts" and
empty_in: "{#} ∈ Liminf_llist (lmap grounding_of_state Sts)"
shows "{#} ∈ Q_of_state (Liminf_state Sts)"
proof -
define Gs :: "'a clause set llist" where
ns: "Gs = lmap grounding_of_state Sts"
from empty_in have in_Liminf_not_Rf: "{#} ∈ Liminf_llist Gs - sr.Rf (Liminf_llist Gs)"
unfolding ns sr.Rf_def by auto
then have "{#} ∈ grounding_of_clss (Q_of_state (Liminf_state Sts))"
using fair_imp_Liminf_minus_Rf_subset_ground_Liminf_state[OF deriv fair ns] by auto
then show ?thesis
unfolding grounding_of_clss_def grounding_of_cls_def by auto
qed
lemma grounding_of_state_Liminf_state_subseteq:
"grounding_of_state (Liminf_state Sts) ⊆ Liminf_llist (lmap grounding_of_state Sts)"
proof
fix C :: "'a clause"
assume "C ∈ grounding_of_state (Liminf_state Sts)"
then obtain D σ where
D_σ_p: "D ∈ clss_of_state (Liminf_state Sts)" "D ⋅ σ = C" "is_ground_subst σ"
unfolding grounding_of_clss_def grounding_of_cls_def by auto
then have ii: "D ∈ Liminf_llist (lmap N_of_state Sts)
∨ D ∈ Liminf_llist (lmap P_of_state Sts) ∨ D ∈ Liminf_llist (lmap Q_of_state Sts)"
unfolding Liminf_state_def by simp
then have "C ∈ Liminf_llist (lmap grounding_of_clss (lmap N_of_state Sts))
∨ C ∈ Liminf_llist (lmap grounding_of_clss (lmap P_of_state Sts))
∨ C ∈ Liminf_llist (lmap grounding_of_clss (lmap Q_of_state Sts))"
unfolding Liminf_llist_def grounding_of_clss_def grounding_of_cls_def
using D_σ_p
apply -
apply (erule disjE)
subgoal
apply (rule disjI1)
using D_σ_p by auto
subgoal
apply (erule disjE)
subgoal
apply (rule disjI2)
apply (rule disjI1)
using D_σ_p by auto
subgoal
apply (rule disjI2)
apply (rule disjI2)
using D_σ_p by auto
done
done
then show "C ∈ Liminf_llist (lmap grounding_of_state Sts)"
unfolding Liminf_llist_def grounding_of_clss_def by auto
qed
theorem RP_sound:
assumes
deriv: "chain (↝) Sts" and
"{#} ∈ clss_of_state (Liminf_state Sts)"
shows "¬ satisfiable (grounding_of_state (lhd Sts))"
proof -
from assms have "{#} ∈ grounding_of_state (Liminf_state Sts)"
unfolding grounding_of_clss_def by (force intro: ex_ground_subst)
then have "{#} ∈ Liminf_llist (lmap grounding_of_state Sts)"
using grounding_of_state_Liminf_state_subseteq by auto
then have "¬ satisfiable (Liminf_llist (lmap grounding_of_state Sts))"
using true_clss_def by auto
then have "¬ satisfiable (lhd (lmap grounding_of_state Sts))"
using sr_ext.sat_limit_iff ground_derive_chain deriv by blast
then show ?thesis
using chain_not_lnull deriv by fastforce
qed
theorem RP_saturated_if_fair:
assumes
deriv: "chain (↝) Sts" and
fair: "fair_state_seq Sts" and
empty_Q0: "Q_of_state (lhd Sts) = {}"
shows "sr.saturated_upto (Liminf_llist (lmap grounding_of_state Sts))"
proof -
define Gs :: "'a clause set llist" where
ns: "Gs = lmap grounding_of_state Sts"
let ?N = "λi. grounding_of_state (lnth Sts i)"
let ?Ns = "λi. N_of_state (lnth Sts i)"
let ?Ps = "λi. P_of_state (lnth Sts i)"
let ?Qs = "λi. Q_of_state (lnth Sts i)"
have ground_ns_in_ground_limit_st:
"Liminf_llist Gs - sr.Rf (Liminf_llist Gs) ⊆ grounding_of_clss (Q_of_state (Liminf_state Sts))"
using fair deriv fair_imp_Liminf_minus_Rf_subset_ground_Liminf_state ns by blast
have derivns: "chain sr_ext.derive Gs"
using ground_derive_chain deriv ns by auto
{
fix γ :: "'a inference"
assume γ_p: "γ ∈ gr.ord_Γ"
let ?CC = "side_prems_of γ"
let ?DA = "main_prem_of γ"
let ?E = "concl_of γ"
assume a: "set_mset ?CC ∪ {?DA}
⊆ Liminf_llist (lmap grounding_of_state Sts)
- sr.Rf (Liminf_llist (lmap grounding_of_state Sts))"
have ground_ground_Liminf: "is_ground_clss (Liminf_llist (lmap grounding_of_state Sts))"
using Liminf_grounding_of_state_ground unfolding is_ground_clss_def by auto
have ground_cc: "is_ground_clss (set_mset ?CC)"
using a ground_ground_Liminf is_ground_clss_def by auto
have ground_da: "is_ground_cls ?DA"
using a grounding_ground singletonI ground_ground_Liminf
by (simp add: Liminf_grounding_of_state_ground)
from γ_p obtain CAs AAs As where
CAs_p: "gr.ord_resolve CAs ?DA AAs As ?E ∧ mset CAs = ?CC"
unfolding gr.ord_Γ_def by auto
have DA_CAs_in_ground_Liminf:
"{?DA} ∪ set CAs ⊆ grounding_of_clss (Q_of_state (Liminf_state Sts))"
using a CAs_p fair unfolding fair_state_seq_def
by (metis (no_types, lifting) Un_empty_left ground_ns_in_ground_limit_st a ns set_mset_mset
subset_trans sup_commute)
then have ground_cas: "is_ground_cls_list CAs"
using CAs_p unfolding is_ground_cls_list_def by auto
have "∃σ. ord_resolve S_Q CAs ?DA AAs As σ ?E"
by (rule ground_ord_resolve_imp_ord_resolve[OF ground_da ground_cas
gr.ground_resolution_with_selection_axioms CAs_p[THEN conjunct1]])
then obtain σ where
σ_p: "ord_resolve S_Q CAs ?DA AAs As σ ?E"
by auto
then obtain ηs' η' η2' CAs' DA' AAs' As' τ' E' where s_p:
"is_ground_subst η'"
"is_ground_subst_list ηs'"
"is_ground_subst η2'"
"ord_resolve_rename S CAs' DA' AAs' As' τ' E'"
"CAs' ⋅⋅cl ηs' = CAs"
"DA' ⋅ η' = ?DA"
"E' ⋅ η2' = ?E"
"{DA'} ∪ set CAs' ⊆ Q_of_state (Liminf_state Sts)"
using ord_resolve_rename_lifting[OF sel_stable, of "Q_of_state (Liminf_state Sts)" CAs ?DA]
σ_p[unfolded S_Q_def] selection_axioms DA_CAs_in_ground_Liminf by metis
from this(8) have "∃j. enat j < llength Sts ∧ (set CAs' ∪ {DA'} ⊆ ?Qs j)"
unfolding Liminf_llist_def
using subseteq_Liminf_state_eventually_always[of "{DA'} ∪ set CAs'"] by auto
then obtain j where
j_p: "is_least (λj. enat j < llength Sts ∧ set CAs' ∪ {DA'} ⊆ ?Qs j) j"
using least_exists[of "λj. enat j < llength Sts ∧ set CAs' ∪ {DA'} ⊆ ?Qs j"] by force
then have j_p': "enat j < llength Sts" "set CAs' ∪ {DA'} ⊆ ?Qs j"
unfolding is_least_def by auto
then have jn0: "j ≠ 0"
using empty_Q0 by (metis bot_eq_sup_iff gr_implies_not_zero insert_not_empty llength_lnull
lnth_0_conv_lhd sup.orderE)
then have j_adds_CAs': "¬ set CAs' ∪ {DA'} ⊆ ?Qs (j - 1)" "set CAs' ∪ {DA'} ⊆ ?Qs j"
using j_p unfolding is_least_def
apply (metis (no_types) One_nat_def Suc_diff_Suc Suc_ile_eq diff_diff_cancel diff_zero
less_imp_le less_one neq0_conv zero_less_diff)
using j_p'(2) by blast
have "lnth Sts (j - 1) ↝ lnth Sts j"
using j_p'(1) jn0 deriv chain_lnth_rel[of _ _ "j - 1"] by force
then obtain C' where C'_p:
"?Ns (j - 1) = {}"
"?Ps (j - 1) = ?Ps j ∪ {C'}"
"?Qs j = ?Qs (j - 1) ∪ {C'}"
"?Ns j = concls_of (ord_FO_resolution.inferences_between (?Qs (j - 1)) C')"
"C' ∈ set CAs' ∪ {DA'}"
"C' ∉ ?Qs (j - 1)"
using j_adds_CAs' by (induction rule: RP.cases) auto
have "E' ∈ ?Ns j"
proof -
have "E' ∈ concls_of (ord_FO_resolution.inferences_between (Q_of_state (lnth Sts (j - 1))) C')"
unfolding infer_from_def ord_FO_Γ_def inference_system.inferences_between_def
apply (rule_tac x = "Infer (mset CAs') DA' E'" in image_eqI)
subgoal by auto
subgoal
unfolding infer_from_def
by (rule ord_resolve_rename.cases[OF s_p(4)]) (use s_p(4) C'_p(3,5) j_p'(2) in force)
done
then show ?thesis
using C'_p(4) by auto
qed
then have "E' ∈ clss_of_state (lnth Sts j)"
using j_p' by auto
then have "?E ∈ grounding_of_state (lnth Sts j)"
using s_p(7) s_p(3) unfolding grounding_of_clss_def grounding_of_cls_def by force
then have "γ ∈ sr.Ri (grounding_of_state (lnth Sts j))"
using sr.Ri_effective γ_p by auto
then have "γ ∈ sr_ext_Ri (?N j)"
unfolding sr_ext_Ri_def by auto
then have "γ ∈ sr_ext_Ri (Sup_llist (lmap grounding_of_state Sts))"
using j_p' contra_subsetD llength_lmap lnth_lmap lnth_subset_Sup_llist sr_ext.Ri_mono by (smt (verit))
then have "γ ∈ sr_ext_Ri (Liminf_llist (lmap grounding_of_state Sts))"
using sr_ext.Ri_limit_Sup[of Gs] derivns ns by blast
}
then have "sr_ext.saturated_upto (Liminf_llist (lmap grounding_of_state Sts))"
unfolding sr_ext.saturated_upto_def sr_ext.inferences_from_def infer_from_def sr_ext_Ri_def
by auto
then show ?thesis
using gd_ord_Γ_ngd_ord_Γ sr.redundancy_criterion_axioms
redundancy_criterion_standard_extension_saturated_upto_iff[of gr.ord_Γ]
unfolding sr_ext_Ri_def by auto
qed
corollary RP_complete_if_fair:
assumes
deriv: "chain (↝) Sts" and
fair: "fair_state_seq Sts" and
empty_Q0: "Q_of_state (lhd Sts) = {}" and
unsat: "¬ satisfiable (grounding_of_state (lhd Sts))"
shows "{#} ∈ Q_of_state (Liminf_state Sts)"
proof -
have "¬ satisfiable (Liminf_llist (lmap grounding_of_state Sts))"
using unsat sr_ext.sat_limit_iff[OF ground_derive_chain] chain_not_lnull deriv by fastforce
moreover have "sr.saturated_upto (Liminf_llist (lmap grounding_of_state Sts))"
by (rule RP_saturated_if_fair[OF deriv fair empty_Q0, simplified])
ultimately have "{#} ∈ Liminf_llist (lmap grounding_of_state Sts)"
using sr.saturated_upto_complete_if by auto
then show ?thesis
using empty_clause_in_Q_of_Liminf_state[OF deriv fair] by auto
qed
end
end
end