Theory Proving_Process
section ‹Theorem Proving Processes›
theory Proving_Process
imports Unordered_Ground_Resolution Lazy_List_Chain
begin
text ‹
This material corresponds to Section 4.1 (``Theorem Proving Processes'') of Bachmair and Ganzinger's
chapter.
The locale assumptions below capture conditions R1 to R3 of Definition 4.1.
‹Rf› denotes $\mathcal{R}_{\mathcal{F}}$; ‹Ri› denotes $\mathcal{R}_{\mathcal{I}}$.
›
locale redundancy_criterion = inference_system +
fixes
Rf :: "'a clause set ⇒ 'a clause set" and
Ri :: "'a clause set ⇒ 'a inference set"
assumes
Ri_subset_Γ: "Ri N ⊆ Γ" and
Rf_mono: "N ⊆ N' ⟹ Rf N ⊆ Rf N'" and
Ri_mono: "N ⊆ N' ⟹ Ri N ⊆ Ri N'" and
Rf_indep: "N' ⊆ Rf N ⟹ Rf N ⊆ Rf (N - N')" and
Ri_indep: "N' ⊆ Rf N ⟹ Ri N ⊆ Ri (N - N')" and
Rf_sat: "satisfiable (N - Rf N) ⟹ satisfiable N"
begin
definition saturated_upto :: "'a clause set ⇒ bool" where
"saturated_upto N ⟷ inferences_from (N - Rf N) ⊆ Ri N"
inductive "derive" :: "'a clause set ⇒ 'a clause set ⇒ bool" (infix "▹" 50) where
deduction_deletion: "N - M ⊆ concls_of (inferences_from M) ⟹ M - N ⊆ Rf N ⟹ M ▹ N"
lemma derive_subset: "M ▹ N ⟹ N ⊆ M ∪ concls_of (inferences_from M)"
by (meson Diff_subset_conv derive.cases)
end
locale sat_preserving_redundancy_criterion =
sat_preserving_inference_system "Γ :: ('a :: wellorder) inference set" + redundancy_criterion
begin
lemma deriv_sat_preserving:
assumes
deriv: "chain (▹) Ns" and
sat_n0: "satisfiable (lhd Ns)"
shows "satisfiable (Sup_llist Ns)"
proof -
have len_ns: "llength Ns > 0"
using deriv by (case_tac Ns) simp+
{
fix DD
assume fin: "finite DD" and sset_lun: "DD ⊆ Sup_llist Ns"
then obtain k where
dd_sset: "DD ⊆ Sup_upto_llist Ns (enat k)"
using finite_Sup_llist_imp_Sup_upto_llist by blast
have "satisfiable (Sup_upto_llist Ns k)"
proof (induct k)
case 0
then show ?case
using len_ns sat_n0
unfolding Sup_upto_llist_def true_clss_def lhd_conv_lnth[OF chain_not_lnull[OF deriv]]
by auto
next
case (Suc k)
show ?case
proof (cases "enat (Suc k) ≥ llength Ns")
case True
then have "Sup_upto_llist Ns (enat k) = Sup_upto_llist Ns (enat (Suc k))"
unfolding Sup_upto_llist_def using le_Suc_eq by auto
then show ?thesis
using Suc by simp
next
case False
then have "lnth Ns k ▹ lnth Ns (Suc k)"
using deriv by (auto simp: chain_lnth_rel)
then have "lnth Ns (Suc k) ⊆ lnth Ns k ∪ concls_of (inferences_from (lnth Ns k))"
by (rule derive_subset)
moreover have "lnth Ns k ⊆ Sup_upto_llist Ns k"
unfolding Sup_upto_llist_def using False Suc_ile_eq linear by blast
ultimately have "lnth Ns (Suc k)
⊆ Sup_upto_llist Ns k ∪ concls_of (inferences_from (Sup_upto_llist Ns k))"
by clarsimp (metis UnCI UnE image_Un inferences_from_mono le_iff_sup)
moreover have "Sup_upto_llist Ns (Suc k) = Sup_upto_llist Ns k ∪ lnth Ns (Suc k)"
unfolding Sup_upto_llist_def using False by (force elim: le_SucE)
moreover have
"satisfiable (Sup_upto_llist Ns k ∪ concls_of (inferences_from (Sup_upto_llist Ns k)))"
using Suc Γ_sat_preserving unfolding sat_preserving_inference_system_def by simp
ultimately show ?thesis
by (metis le_iff_sup true_clss_union)
qed
qed
then have "satisfiable DD"
using dd_sset unfolding Sup_upto_llist_def by (blast intro: true_clss_mono)
}
then show ?thesis
using ground_resolution_without_selection.clausal_logic_compact[THEN iffD1] by metis
qed
text ‹
This corresponds to Lemma 4.2:
›
lemma
assumes deriv: "chain (▹) Ns"
shows
Rf_Sup_subset_Rf_Liminf: "Rf (Sup_llist Ns) ⊆ Rf (Liminf_llist Ns)" and
Ri_Sup_subset_Ri_Liminf: "Ri (Sup_llist Ns) ⊆ Ri (Liminf_llist Ns)" and
sat_limit_iff: "satisfiable (Liminf_llist Ns) ⟷ satisfiable (lhd Ns)"
proof -
{
fix C i j
assume
c_in: "C ∈ lnth Ns i" and
c_ni: "C ∉ Rf (Sup_llist Ns)" and
j: "j ≥ i" and
j': "enat j < llength Ns"
from c_ni have c_ni': "⋀i. enat i < llength Ns ⟹ C ∉ Rf (lnth Ns i)"
using Rf_mono lnth_subset_Sup_llist Sup_llist_def by (blast dest: contra_subsetD)
have "C ∈ lnth Ns j"
using j j'
proof (induct j)
case 0
then show ?case
using c_in by blast
next
case (Suc k)
then show ?case
proof (cases "i < Suc k")
case True
have "i ≤ k"
using True by linarith
moreover have "enat k < llength Ns"
using Suc.prems(2) Suc_ile_eq by (blast intro: dual_order.strict_implies_order)
ultimately have c_in_k: "C ∈ lnth Ns k"
using Suc.hyps by blast
have rel: "lnth Ns k ▹ lnth Ns (Suc k)"
using Suc.prems deriv by (auto simp: chain_lnth_rel)
then show ?thesis
using c_in_k c_ni' Suc.prems(2) by cases auto
next
case False
then show ?thesis
using Suc c_in by auto
qed
qed
}
then have lu_ll: "Sup_llist Ns - Rf (Sup_llist Ns) ⊆ Liminf_llist Ns"
unfolding Sup_llist_def Liminf_llist_def by blast
have rf: "Rf (Sup_llist Ns - Rf (Sup_llist Ns)) ⊆ Rf (Liminf_llist Ns)"
using lu_ll Rf_mono by simp
have ri: "Ri (Sup_llist Ns - Rf (Sup_llist Ns)) ⊆ Ri (Liminf_llist Ns)"
using lu_ll Ri_mono by simp
show "Rf (Sup_llist Ns) ⊆ Rf (Liminf_llist Ns)"
using rf Rf_indep by blast
show "Ri (Sup_llist Ns) ⊆ Ri (Liminf_llist Ns)"
using ri Ri_indep by blast
show "satisfiable (Liminf_llist Ns) ⟷ satisfiable (lhd Ns)"
proof
assume "satisfiable (lhd Ns)"
then have "satisfiable (Sup_llist Ns)"
using deriv deriv_sat_preserving by simp
then show "satisfiable (Liminf_llist Ns)"
using true_clss_mono[OF Liminf_llist_subset_Sup_llist] by blast
next
assume "satisfiable (Liminf_llist Ns)"
then have "satisfiable (Sup_llist Ns - Rf (Sup_llist Ns))"
using true_clss_mono[OF lu_ll] by blast
then have "satisfiable (Sup_llist Ns)"
using Rf_sat by blast
then show "satisfiable (lhd Ns)"
using deriv true_clss_mono lhd_subset_Sup_llist chain_not_lnull by metis
qed
qed
lemma
assumes "chain (▹) Ns"
shows
Rf_limit_Sup: "Rf (Liminf_llist Ns) = Rf (Sup_llist Ns)" and
Ri_limit_Sup: "Ri (Liminf_llist Ns) = Ri (Sup_llist Ns)"
using assms
by (auto simp: Rf_Sup_subset_Rf_Liminf Rf_mono Ri_Sup_subset_Ri_Liminf Ri_mono
Liminf_llist_subset_Sup_llist subset_antisym)
end
text ‹
The assumption below corresponds to condition R4 of Definition 4.1.
›
locale effective_redundancy_criterion = redundancy_criterion +
assumes Ri_effective: "γ ∈ Γ ⟹ concl_of γ ∈ N ∪ Rf N ⟹ γ ∈ Ri N"
begin
definition fair_clss_seq :: "'a clause set llist ⇒ bool" where
"fair_clss_seq Ns ⟷ (let N' = Liminf_llist Ns - Rf (Liminf_llist Ns) in
concls_of (inferences_from N' - Ri N') ⊆ Sup_llist Ns ∪ Rf (Sup_llist Ns))"
end
locale sat_preserving_effective_redundancy_criterion =
sat_preserving_inference_system "Γ :: ('a :: wellorder) inference set" +
effective_redundancy_criterion
begin
sublocale sat_preserving_redundancy_criterion
..
text ‹
The result below corresponds to Theorem 4.3.
›
theorem fair_derive_saturated_upto:
assumes
deriv: "chain (▹) Ns" and
fair: "fair_clss_seq Ns"
shows "saturated_upto (Liminf_llist Ns)"
unfolding saturated_upto_def
proof
fix γ
let ?N' = "Liminf_llist Ns - Rf (Liminf_llist Ns)"
assume γ: "γ ∈ inferences_from ?N'"
show "γ ∈ Ri (Liminf_llist Ns)"
proof (cases "γ ∈ Ri ?N'")
case True
then show ?thesis
using Ri_mono by blast
next
case False
have "concls_of (inferences_from ?N' - Ri ?N') ⊆ Sup_llist Ns ∪ Rf (Sup_llist Ns)"
using fair unfolding fair_clss_seq_def Let_def .
then have "concl_of γ ∈ Sup_llist Ns ∪ Rf (Sup_llist Ns)"
using False γ by auto
moreover
{
assume "concl_of γ ∈ Sup_llist Ns"
then have "γ ∈ Ri (Sup_llist Ns)"
using γ Ri_effective inferences_from_def by blast
then have "γ ∈ Ri (Liminf_llist Ns)"
using deriv Ri_Sup_subset_Ri_Liminf by fast
}
moreover
{
assume "concl_of γ ∈ Rf (Sup_llist Ns)"
then have "concl_of γ ∈ Rf (Liminf_llist Ns)"
using deriv Rf_Sup_subset_Rf_Liminf by blast
then have "γ ∈ Ri (Liminf_llist Ns)"
using γ Ri_effective inferences_from_def by auto
}
ultimately show "γ ∈ Ri (Liminf_llist Ns)"
by blast
qed
qed
end
text ‹
This corresponds to the trivial redundancy criterion defined on page 36 of
Section 4.1.
›
locale trivial_redundancy_criterion = inference_system
begin
definition Rf :: "'a clause set ⇒ 'a clause set" where
"Rf _ = {}"
definition Ri :: "'a clause set ⇒ 'a inference set" where
"Ri N = {γ. γ ∈ Γ ∧ concl_of γ ∈ N}"
sublocale effective_redundancy_criterion Γ Rf Ri
by unfold_locales (auto simp: Rf_def Ri_def)
lemma saturated_upto_iff: "saturated_upto N ⟷ concls_of (inferences_from N) ⊆ N"
unfolding saturated_upto_def inferences_from_def Rf_def Ri_def by auto
end
text ‹
The following lemmas corresponds to the standard extension of a redundancy criterion defined on
page 38 of Section 4.1.
›
lemma redundancy_criterion_standard_extension:
assumes "Γ ⊆ Γ'" and "redundancy_criterion Γ Rf Ri"
shows "redundancy_criterion Γ' Rf (λN. Ri N ∪ (Γ' - Γ))"
using assms unfolding redundancy_criterion_def by (intro conjI) ((auto simp: rev_subsetD)[5], sat)
lemma redundancy_criterion_standard_extension_saturated_upto_iff:
assumes "Γ ⊆ Γ'" and "redundancy_criterion Γ Rf Ri"
shows "redundancy_criterion.saturated_upto Γ Rf Ri M ⟷
redundancy_criterion.saturated_upto Γ' Rf (λN. Ri N ∪ (Γ' - Γ)) M"
using assms redundancy_criterion.saturated_upto_def redundancy_criterion.saturated_upto_def
redundancy_criterion_standard_extension
unfolding inference_system.inferences_from_def by blast
lemma redundancy_criterion_standard_extension_effective:
assumes "Γ ⊆ Γ'" and "effective_redundancy_criterion Γ Rf Ri"
shows "effective_redundancy_criterion Γ' Rf (λN. Ri N ∪ (Γ' - Γ))"
using assms redundancy_criterion_standard_extension[of Γ]
unfolding effective_redundancy_criterion_def effective_redundancy_criterion_axioms_def by auto
lemma redundancy_criterion_standard_extension_fair_iff:
assumes "Γ ⊆ Γ'" and "effective_redundancy_criterion Γ Rf Ri"
shows "effective_redundancy_criterion.fair_clss_seq Γ' Rf (λN. Ri N ∪ (Γ' - Γ)) Ns ⟷
effective_redundancy_criterion.fair_clss_seq Γ Rf Ri Ns"
using assms redundancy_criterion_standard_extension_effective[of Γ Γ' Rf Ri]
effective_redundancy_criterion.fair_clss_seq_def[of Γ Rf Ri Ns]
effective_redundancy_criterion.fair_clss_seq_def[of Γ' Rf "(λN. Ri N ∪ (Γ' - Γ))" Ns]
unfolding inference_system.inferences_from_def Let_def by auto
theorem redundancy_criterion_standard_extension_fair_derive_saturated_upto:
assumes
subs: "Γ ⊆ Γ'" and
red: "redundancy_criterion Γ Rf Ri" and
red': "sat_preserving_effective_redundancy_criterion Γ' Rf (λN. Ri N ∪ (Γ' - Γ))" and
deriv: "chain (redundancy_criterion.derive Γ' Rf) Ns" and
fair: "effective_redundancy_criterion.fair_clss_seq Γ' Rf (λN. Ri N ∪ (Γ' - Γ)) Ns"
shows "redundancy_criterion.saturated_upto Γ Rf Ri (Liminf_llist Ns)"
proof -
have "redundancy_criterion.saturated_upto Γ' Rf (λN. Ri N ∪ (Γ' - Γ)) (Liminf_llist Ns)"
by (rule sat_preserving_effective_redundancy_criterion.fair_derive_saturated_upto
[OF red' deriv fair])
then show ?thesis
by (rule redundancy_criterion_standard_extension_saturated_upto_iff[THEN iffD2, OF subs red])
qed
end