Theory Standard_Redundancy
section ‹The Standard Redundancy Criterion›
theory Standard_Redundancy
imports Proving_Process
begin
text ‹
This material is based on Section 4.2.2 (``The Standard Redundancy Criterion'') of Bachmair and
Ganzinger's chapter.
›
locale standard_redundancy_criterion =
inference_system Γ for Γ :: "('a :: wellorder) inference set"
begin
definition redundant_infer :: "'a clause set ⇒ 'a inference ⇒ bool" where
"redundant_infer N γ ⟷
(∃DD. set_mset DD ⊆ N ∧ (∀I. I ⊨m DD + side_prems_of γ ⟶ I ⊨ concl_of γ)
∧ (∀D. D ∈# DD ⟶ D < main_prem_of γ))"
definition Rf :: "'a clause set ⇒ 'a clause set" where
"Rf N = {C. ∃DD. set_mset DD ⊆ N ∧ (∀I. I ⊨m DD ⟶ I ⊨ C) ∧ (∀D. D ∈# DD ⟶ D < C)}"
definition Ri :: "'a clause set ⇒ 'a inference set" where
"Ri N = {γ ∈ Γ. redundant_infer N γ}"
lemma tautology_Rf:
assumes "Pos A ∈# C"
assumes "Neg A ∈# C"
shows "C ∈ Rf N"
proof -
have "set_mset {#} ⊆ N ∧ (∀I. I ⊨m {#} ⟶ I ⊨ C) ∧ (∀D. D ∈# {#} ⟶ D < C)"
using assms by auto
then show "C ∈ Rf N"
unfolding Rf_def by blast
qed
lemma tautology_redundant_infer:
assumes
pos: "Pos A ∈# concl_of ι" and
neg: "Neg A ∈# concl_of ι"
shows "redundant_infer N ι"
by (metis empty_iff empty_subsetI neg pos pos_neg_in_imp_true redundant_infer_def set_mset_empty)
lemma contradiction_Rf: "{#} ∈ N ⟹ Rf N = UNIV - {{#}}"
unfolding Rf_def by force
text ‹
The following results correspond to Lemma 4.5. The lemma ‹wlog_non_Rf› generalizes the core of
the argument.
›
lemma Rf_mono: "N ⊆ N' ⟹ Rf N ⊆ Rf N'"
unfolding Rf_def by auto
lemma wlog_non_Rf:
assumes ex: "∃DD. set_mset DD ⊆ N ∧ (∀I. I ⊨m DD + CC ⟶ I ⊨ E) ∧ (∀D'. D' ∈# DD ⟶ D' < D)"
shows "∃DD. set_mset DD ⊆ N - Rf N ∧ (∀I. I ⊨m DD + CC ⟶ I ⊨ E) ∧ (∀D'. D' ∈# DD ⟶ D' < D)"
proof -
from ex obtain DD0 where
dd0: "DD0 ∈ {DD. set_mset DD ⊆ N ∧ (∀I. I ⊨m DD + CC ⟶ I ⊨ E) ∧ (∀D'. D' ∈# DD ⟶ D' < D)}"
by blast
have "∃DD. set_mset DD ⊆ N ∧ (∀I. I ⊨m DD + CC ⟶ I ⊨ E) ∧ (∀D'. D' ∈# DD ⟶ D' < D) ∧
(∀DD'. set_mset DD' ⊆ N ∧ (∀I. I ⊨m DD' + CC ⟶ I ⊨ E) ∧ (∀D'. D' ∈# DD' ⟶ D' < D) ⟶
DD ≤ DD')"
using wf_eq_minimal[THEN iffD1, rule_format, OF wf_less_multiset dd0]
unfolding not_le[symmetric] by blast
then obtain DD where
dd_subs_n: "set_mset DD ⊆ N" and
ddcc_imp_e: "∀I. I ⊨m DD + CC ⟶ I ⊨ E" and
dd_lt_d: "∀D'. D' ∈# DD ⟶ D' < D" and
d_min: "∀DD'. set_mset DD' ⊆ N ∧ (∀I. I ⊨m DD' + CC ⟶ I ⊨ E) ∧ (∀D'. D' ∈# DD' ⟶ D' < D) ⟶
DD ≤ DD'"
by blast
have "∀Da. Da ∈# DD ⟶ Da ∉ Rf N"
proof clarify
fix Da
assume
da_in_dd: "Da ∈# DD" and
da_rf: "Da ∈ Rf N"
from da_rf obtain DD' where
dd'_subs_n: "set_mset DD' ⊆ N" and
dd'_imp_da: "∀I. I ⊨m DD' ⟶ I ⊨ Da" and
dd'_lt_da: "∀D'. D' ∈# DD' ⟶ D' < Da"
unfolding Rf_def by blast
define DDa where
"DDa = DD - {#Da#} + DD'"
have "set_mset DDa ⊆ N"
unfolding DDa_def using dd_subs_n dd'_subs_n
by (meson contra_subsetD in_diffD subsetI union_iff)
moreover have "∀I. I ⊨m DDa + CC ⟶ I ⊨ E"
using dd'_imp_da ddcc_imp_e da_in_dd unfolding DDa_def true_cls_mset_def
by (metis in_remove1_mset_neq union_iff)
moreover have "∀D'. D' ∈# DDa ⟶ D' < D"
using dd_lt_d dd'_lt_da da_in_dd unfolding DDa_def
by (metis insert_DiffM2 order.strict_trans union_iff)
moreover have "DDa < DD"
unfolding DDa_def
by (meson da_in_dd dd'_lt_da mset_lt_single_right_iff single_subset_iff union_le_diff_plus)
ultimately show False
using d_min unfolding less_eq_multiset_def by (auto intro!: antisym)
qed
then show ?thesis
using dd_subs_n ddcc_imp_e dd_lt_d by auto
qed
lemma Rf_imp_ex_non_Rf:
assumes "C ∈ Rf N"
shows "∃CC. set_mset CC ⊆ N - Rf N ∧ (∀I. I ⊨m CC ⟶ I ⊨ C) ∧ (∀C'. C' ∈# CC ⟶ C' < C)"
using assms by (auto simp: Rf_def intro: wlog_non_Rf[of _ "{#}", simplified])
lemma Rf_subs_Rf_diff_Rf: "Rf N ⊆ Rf (N - Rf N)"
proof
fix C
assume c_rf: "C ∈ Rf N"
then obtain CC where
cc_subs: "set_mset CC ⊆ N - Rf N" and
cc_imp_c: "∀I. I ⊨m CC ⟶ I ⊨ C" and
cc_lt_c: "∀C'. C' ∈# CC ⟶ C' < C"
using Rf_imp_ex_non_Rf by blast
have "∀D. D ∈# CC ⟶ D ∉ Rf N"
using cc_subs by (simp add: subset_iff)
then have cc_nr:
"⋀C DD. C ∈# CC ⟹ set_mset DD ⊆ N ⟹ ∀I. I ⊨m DD ⟶ I ⊨ C ⟹ ∃D. D ∈# DD ∧ ¬ D < C"
unfolding Rf_def by auto metis
have "set_mset CC ⊆ N"
using cc_subs by auto
then have "set_mset CC ⊆
N - {C. ∃DD. set_mset DD ⊆ N ∧ (∀I. I ⊨m DD ⟶ I ⊨ C) ∧ (∀D. D ∈# DD ⟶ D < C)}"
using cc_nr by blast
then show "C ∈ Rf (N - Rf N)"
using cc_imp_c cc_lt_c unfolding Rf_def by auto
qed
lemma Rf_eq_Rf_diff_Rf: "Rf N = Rf (N - Rf N)"
by (metis Diff_subset Rf_mono Rf_subs_Rf_diff_Rf subset_antisym)
text ‹
The following results correspond to Lemma 4.6.
›
lemma Ri_mono: "N ⊆ N' ⟹ Ri N ⊆ Ri N'"
unfolding Ri_def redundant_infer_def by auto
lemma Ri_subs_Ri_diff_Rf: "Ri N ⊆ Ri (N - Rf N)"
proof
fix γ
assume γ_ri: "γ ∈ Ri N"
then obtain CC D E where γ: "γ = Infer CC D E"
by (cases γ)
have cc: "CC = side_prems_of γ" and d: "D = main_prem_of γ" and e: "E = concl_of γ"
unfolding γ by simp_all
obtain DD where
"set_mset DD ⊆ N" and "∀I. I ⊨m DD + CC ⟶ I ⊨ E" and "∀C. C ∈# DD ⟶ C < D"
using γ_ri unfolding Ri_def redundant_infer_def cc d e by blast
then obtain DD' where
"set_mset DD' ⊆ N - Rf N" and "∀I. I ⊨m DD' + CC ⟶ I ⊨ E" and "∀D'. D' ∈# DD' ⟶ D' < D"
using wlog_non_Rf by atomize_elim blast
then show "γ ∈ Ri (N - Rf N)"
using γ_ri unfolding Ri_def redundant_infer_def d cc e by blast
qed
lemma Ri_eq_Ri_diff_Rf: "Ri N = Ri (N - Rf N)"
by (metis Diff_subset Ri_mono Ri_subs_Ri_diff_Rf subset_antisym)
lemma Ri_subset_Γ: "Ri N ⊆ Γ"
unfolding Ri_def by blast
lemma Rf_indep: "N' ⊆ Rf N ⟹ Rf N ⊆ Rf (N - N')"
by (metis Diff_cancel Diff_eq_empty_iff Diff_mono Rf_eq_Rf_diff_Rf Rf_mono)
lemma Ri_indep: "N' ⊆ Rf N ⟹ Ri N ⊆ Ri (N - N')"
by (metis Diff_mono Ri_eq_Ri_diff_Rf Ri_mono order_refl)
lemma Rf_model:
assumes "I ⊨s N - Rf N"
shows "I ⊨s N"
proof -
have "I ⊨s Rf (N - Rf N)"
unfolding true_clss_def
by (subst Rf_def, simp add: true_cls_mset_def, metis assms subset_eq true_clss_def)
then have "I ⊨s Rf N"
using Rf_subs_Rf_diff_Rf true_clss_mono by blast
then show ?thesis
using assms by (metis Un_Diff_cancel true_clss_union)
qed
lemma Rf_sat: "satisfiable (N - Rf N) ⟹ satisfiable N"
by (metis Rf_model)
text ‹
The following corresponds to Theorem 4.7:
›
sublocale redundancy_criterion Γ Rf Ri
by unfold_locales (rule Ri_subset_Γ, (elim Rf_mono Ri_mono Rf_indep Ri_indep Rf_sat)+)
end
locale standard_redundancy_criterion_reductive =
standard_redundancy_criterion + reductive_inference_system
begin
text ‹
The following corresponds to Theorem 4.8:
›
lemma Ri_effective:
assumes
in_γ: "γ ∈ Γ" and
concl_of_in_n_un_rf_n: "concl_of γ ∈ N ∪ Rf N"
shows "γ ∈ Ri N"
proof -
obtain CC D E where
γ: "γ = Infer CC D E"
by (cases γ)
then have cc: "CC = side_prems_of γ" and d: "D = main_prem_of γ" and e: "E = concl_of γ"
unfolding γ by simp_all
note e_in_n_un_rf_n = concl_of_in_n_un_rf_n[folded e]
{
assume "E ∈ N"
moreover have "E < D"
using Γ_reductive e d in_γ by auto
ultimately have
"set_mset {#E#} ⊆ N" and "∀I. I ⊨m {#E#} + CC ⟶ I ⊨ E" and "∀D'. D' ∈# {#E#} ⟶ D' < D"
by simp_all
then have "redundant_infer N γ"
using redundant_infer_def cc d e by blast
}
moreover
{
assume "E ∈ Rf N"
then obtain DD where
dd_sset: "set_mset DD ⊆ N" and
dd_imp_e: "∀I. I ⊨m DD ⟶ I ⊨ E" and
dd_lt_e: "∀C'. C' ∈# DD ⟶ C' < E"
unfolding Rf_def by blast
from dd_lt_e have "∀Da. Da ∈# DD ⟶ Da < D"
using d e in_γ Γ_reductive less_trans by blast
then have "redundant_infer N γ"
using redundant_infer_def dd_sset dd_imp_e cc d e by blast
}
ultimately show "γ ∈ Ri N"
using in_γ e_in_n_un_rf_n unfolding Ri_def by blast
qed
sublocale effective_redundancy_criterion Γ Rf Ri
unfolding effective_redundancy_criterion_def
by (intro conjI redundancy_criterion_axioms, unfold_locales, rule Ri_effective)
lemma contradiction_Rf: "{#} ∈ N ⟹ Ri N = Γ"
unfolding Ri_def redundant_infer_def using Γ_reductive le_multiset_empty_right
by (force intro: exI[of _ "{#{#}#}"] le_multiset_empty_left)
end
locale standard_redundancy_criterion_counterex_reducing =
standard_redundancy_criterion + counterex_reducing_inference_system
begin
text ‹
The following result corresponds to Theorem 4.9.
›
lemma saturated_upto_complete_if:
assumes
satur: "saturated_upto N" and
unsat: "¬ satisfiable N"
shows "{#} ∈ N"
proof (rule ccontr)
assume ec_ni_n: "{#} ∉ N"
define M where
"M = N - Rf N"
have ec_ni_m: "{#} ∉ M"
unfolding M_def using ec_ni_n by fast
have "I_of M ⊨s M"
proof (rule ccontr)
assume "¬ I_of M ⊨s M"
then obtain D where
d_in_m: "D ∈ M" and
d_cex: "¬ I_of M ⊨ D" and
d_min: "⋀C. C ∈ M ⟹ C < D ⟹ I_of M ⊨ C"
using ex_min_counterex by meson
then obtain γ CC E where
γ: "γ = Infer CC D E" and
cc_subs_m: "set_mset CC ⊆ M" and
cc_true: "I_of M ⊨m CC" and
γ_in: "γ ∈ Γ" and
e_cex: "¬ I_of M ⊨ E" and
e_lt_d: "E < D"
using Γ_counterex_reducing[OF ec_ni_m] not_less by metis
have cc: "CC = side_prems_of γ" and d: "D = main_prem_of γ" and e: "E = concl_of γ"
unfolding γ by simp_all
have "γ ∈ Ri N"
by (rule subsetD[OF satur[unfolded saturated_upto_def inferences_from_def infer_from_def]])
(simp add: γ_in d_in_m cc_subs_m cc[symmetric] d[symmetric] M_def[symmetric])
then have "γ ∈ Ri M"
unfolding M_def using Ri_indep by fast
then obtain DD where
dd_subs_m: "set_mset DD ⊆ M" and
dd_cc_imp_d: "∀I. I ⊨m DD + CC ⟶ I ⊨ E" and
dd_lt_d: "∀C. C ∈# DD ⟶ C < D"
unfolding Ri_def redundant_infer_def cc d e by blast
from dd_subs_m dd_lt_d have "I_of M ⊨m DD"
using d_min unfolding true_cls_mset_def by (metis contra_subsetD)
then have "I_of M ⊨ E"
using dd_cc_imp_d cc_true by auto
then show False
using e_cex by auto
qed
then have "I_of M ⊨s N"
using M_def Rf_model by blast
then show False
using unsat by blast
qed
theorem saturated_upto_complete:
assumes "saturated_upto N"
shows "¬ satisfiable N ⟷ {#} ∈ N"
using assms saturated_upto_complete_if true_clss_def by auto
end
end