theory Prop_Superposition
imports Entailment_Definition.Partial_Herbrand_Interpretation Ordered_Resolution_Prover.Herbrand_Interpretation
begin
section ‹Superposition›
no_notation Herbrand_Interpretation.true_cls (infix "⊨" 50)
notation Herbrand_Interpretation.true_cls (infix "⊨h" 50)
no_notation Herbrand_Interpretation.true_clss (infix "⊨s" 50)
notation Herbrand_Interpretation.true_clss (infix "⊨hs" 50)
lemma herbrand_interp_iff_partial_interp_cls:
"S ⊨h C ⟷ {Pos P|P. P∈S} ∪ {Neg P|P. P∉S} ⊨ C"
unfolding Herbrand_Interpretation.true_cls_def Partial_Herbrand_Interpretation.true_cls_def
by auto
lemma herbrand_consistent_interp:
"consistent_interp ({Pos P|P. P∈S} ∪ {Neg P|P. P∉S})"
unfolding consistent_interp_def by auto
lemma herbrand_total_over_set:
"total_over_set ({Pos P|P. P∈S} ∪ {Neg P|P. P∉S}) T"
unfolding total_over_set_def by auto
lemma herbrand_total_over_m:
"total_over_m ({Pos P|P. P∈S} ∪ {Neg P|P. P∉S}) T"
unfolding total_over_m_def by (auto simp add: herbrand_total_over_set)
lemma herbrand_interp_iff_partial_interp_clss:
"S ⊨hs C ⟷ {Pos P|P. P∈S} ∪ {Neg P|P. P∉S} ⊨s C"
unfolding true_clss_def Ball_def herbrand_interp_iff_partial_interp_cls
Partial_Herbrand_Interpretation.true_clss_def by auto
definition clss_lt :: "'a::wellorder clause_set ⇒ 'a clause ⇒ 'a clause_set" where
"clss_lt N C = {D ∈ N. D < C}"
notation (latex output)
clss_lt ("_<^bsup>_<^esup>")
locale selection =
fixes S :: "'a clause ⇒ 'a clause"
assumes
S_selects_subseteq: "⋀C. S C ≤# C" and
S_selects_neg_lits: "⋀C L. L ∈# S C ⟹ is_neg L"
locale ground_resolution_with_selection =
selection S for S :: "('a :: wellorder) clause ⇒ 'a clause"
begin
context
fixes N :: "'a clause set"
begin
text ‹We do not create an equivalent of @{term δ}, but we directly defined @{term N⇩C} by inlining
the definition.›
function
production :: "'a clause ⇒ 'a interp"
where
"production C =
{A. C ∈ N ∧ C ≠ {#} ∧ Max_mset C = Pos A ∧ count C (Pos A) ≤ 1
∧ ¬ (⋃D ∈ {D. D < C}. production D) ⊨h C ∧ S C = {#}}"
by auto
termination by (relation "{(D, C). D < C}") (auto simp: wf_less_multiset)
declare production.simps[simp del]
definition interp :: "'a clause ⇒ 'a interp" where
"interp C = (⋃D ∈ {D. D < C}. production D)"
lemma production_unfold:
"production C = {A. C ∈ N ∧ C ≠ {#} ∧ Max_mset C = Pos A∧ count C (Pos A) ≤ 1 ∧ ¬ interp C ⊨h C ∧ S C = {#}}"
unfolding interp_def by (rule production.simps)
abbreviation "productive A ≡ (production A ≠ {})"
abbreviation produces :: "'a clause ⇒ 'a ⇒ bool" where
"produces C A ≡ production C = {A}"
lemma producesD:
"produces C A ⟹ C ∈ N ∧ C ≠ {#} ∧ Pos A = Max_mset C ∧ count C (Pos A) ≤ 1 ∧
¬ interp C ⊨h C ∧ S C = {#}"
unfolding production_unfold by auto
lemma "produces C A ⟹ Pos A ∈# C"
by (simp add: Max_in_lits producesD)
lemma interp'_def_in_set:
"interp C = (⋃D ∈ {D ∈ N. D < C}. production D)"
unfolding interp_def apply auto
unfolding production_unfold apply auto
done
lemma production_iff_produces:
"produces D A ⟷ A ∈ production D"
unfolding production_unfold by auto
definition Interp :: "'a clause ⇒ 'a interp" where
"Interp C = interp C ∪ production C"
lemma
assumes "produces C P"
shows "Interp C ⊨h C"
unfolding Interp_def assms using producesD[OF assms]
by (metis Max_in_lits Un_insert_right insertI1 pos_literal_in_imp_true_cls)
definition INTERP :: "'a interp" where
"INTERP = (⋃D ∈N. production D)"
lemma interp_subseteq_Interp[simp]: "interp C ⊆ Interp C"
unfolding Interp_def by simp
lemma Interp_as_UNION: "Interp C = (⋃D ∈ {D. D ≤ C}. production D)"
unfolding Interp_def interp_def less_eq_multiset_def by fast
lemma productive_not_empty: "productive C ⟹ C ≠ {#}"
unfolding production_unfold by auto
lemma productive_imp_produces_Max_literal: "productive C ⟹ produces C (atm_of (Max_mset C))"
unfolding production_unfold by (auto simp del: atm_of_Max_lit)
lemma productive_imp_produces_Max_atom: "productive C ⟹ produces C (Max (atms_of C))"
unfolding atms_of_def Max_atm_of_set_mset_commute[OF productive_not_empty]
by (rule productive_imp_produces_Max_literal)
lemma produces_imp_Max_literal: "produces C A ⟹ A = atm_of (Max_mset C)"
by (metis Max_singleton insert_not_empty productive_imp_produces_Max_literal)
lemma produces_imp_Max_atom: "produces C A ⟹ A = Max (atms_of C)"
by (metis Max_singleton insert_not_empty productive_imp_produces_Max_atom)
lemma produces_imp_Pos_in_lits: "produces C A ⟹ Pos A ∈# C"
by (auto intro: Max_in_lits dest!: producesD)
lemma productive_in_N: "productive C ⟹ C ∈ N"
unfolding production_unfold by auto
lemma produces_imp_atms_leq: "produces C A ⟹ B ∈ atms_of C ⟹ B ≤ A"
by (metis Max_ge finite_atms_of insert_not_empty productive_imp_produces_Max_atom
singleton_inject)
lemma produces_imp_neg_notin_lits: "produces C A ⟹ Neg A ∉# C"
by (rule pos_Max_imp_neg_notin) (auto dest: producesD)
lemma less_eq_imp_interp_subseteq_interp: "C ≤ D ⟹ interp C ⊆ interp D"
unfolding interp_def by auto (metis order.strict_trans2)
lemma less_eq_imp_interp_subseteq_Interp: "C ≤ D ⟹ interp C ⊆ Interp D"
unfolding Interp_def using less_eq_imp_interp_subseteq_interp by blast
lemma less_imp_production_subseteq_interp: "C < D ⟹ production C ⊆ interp D"
unfolding interp_def by fast
lemma less_eq_imp_production_subseteq_Interp: "C ≤ D ⟹ production C ⊆ Interp D"
unfolding Interp_def using less_imp_production_subseteq_interp
by (metis le_imp_less_or_eq le_supI1 sup_ge2)
lemma less_imp_Interp_subseteq_interp: "C < D ⟹ Interp C ⊆ interp D"
unfolding Interp_def
by (auto simp: less_eq_imp_interp_subseteq_interp less_imp_production_subseteq_interp)
lemma less_eq_imp_Interp_subseteq_Interp: "C ≤ D ⟹ Interp C ⊆ Interp D"
using less_imp_Interp_subseteq_interp
unfolding Interp_def by (metis le_imp_less_or_eq le_supI2 subset_refl sup_commute)
lemma false_Interp_to_true_interp_imp_less_multiset: "A ∉ Interp C ⟹ A ∈ interp D ⟹ C < D"
using less_eq_imp_interp_subseteq_Interp not_less by blast
lemma false_interp_to_true_interp_imp_less_multiset: "A ∉ interp C ⟹ A ∈ interp D ⟹ C < D"
using less_eq_imp_interp_subseteq_interp not_less by blast
lemma false_Interp_to_true_Interp_imp_less_multiset: "A ∉ Interp C ⟹ A ∈ Interp D ⟹ C < D"
using less_eq_imp_Interp_subseteq_Interp not_less by blast
lemma false_interp_to_true_Interp_imp_le_multiset: "A ∉ interp C ⟹ A ∈ Interp D ⟹ C ≤ D"
using less_imp_Interp_subseteq_interp not_less by blast
lemma interp_subseteq_INTERP: "interp C ⊆ INTERP"
unfolding interp_def INTERP_def by (auto simp: production_unfold)
lemma production_subseteq_INTERP: "production C ⊆ INTERP"
unfolding INTERP_def using production_unfold by blast
lemma Interp_subseteq_INTERP: "Interp C ⊆ INTERP"
unfolding Interp_def by (auto intro!: interp_subseteq_INTERP production_subseteq_INTERP)
text ‹This lemma corresponds to \cwref{prop:prop:suppmcprop}{theorem 2.7.7 page 77}.›
lemma produces_imp_in_interp:
assumes a_in_c: "Neg A ∈# C" and d: "produces D A"
shows "A ∈ interp C"
proof -
from d have "Max_mset D = Pos A"
using production_unfold by blast
then have "D < {#Neg A#}"
by (meson Max_pos_neg_less_multiset multi_member_last)
moreover have "{#Neg A#} ≤ C"
by (rule subset_eq_imp_le_multiset) (rule mset_subset_eq_single[OF a_in_c])
ultimately show ?thesis
using d by (blast dest: less_eq_imp_interp_subseteq_interp less_imp_production_subseteq_interp)
qed
lemma neg_notin_Interp_not_produce: "Neg A ∈# C ⟹ A ∉ Interp D ⟹ C ≤ D ⟹ ¬ produces D'' A"
by (auto dest: produces_imp_in_interp less_eq_imp_interp_subseteq_Interp)
lemma in_production_imp_produces: "A ∈ production C ⟹ produces C A"
by (metis insert_absorb productive_imp_produces_Max_atom singleton_insert_inj_eq')
lemma not_produces_imp_notin_production: "¬ produces C A ⟹ A ∉ production C"
by (metis in_production_imp_produces)
lemma not_produces_imp_notin_interp: "(⋀D. ¬ produces D A) ⟹ A ∉ interp C"
unfolding interp_def by (fast intro!: in_production_imp_produces)
text ‹
The results below corresponds to Lemma 3.4.
\begin{nit}
If $D = D'$ and $D$ is productive, $I^D \subseteq I_{D'}$ does not hold.
\end{nit}
›
lemma true_Interp_imp_general:
assumes
c_le_d: "C ≤ D" and
d_lt_d': "D < D'" and
c_at_d: "Interp D ⊨h C" and
subs: "interp D' ⊆ (⋃C ∈ CC. production C)"
shows "(⋃C ∈ CC. production C) ⊨h C"
proof (cases "∃A. Pos A ∈# C ∧ A ∈ Interp D")
case True
then obtain A where a_in_c: "Pos A ∈# C" and a_at_d: "A ∈ Interp D"
by blast
from a_at_d have "A ∈ interp D'"
using d_lt_d' less_imp_Interp_subseteq_interp by blast
then show ?thesis
using subs a_in_c by (blast dest: contra_subsetD)
next
case False
then obtain A where a_in_c: "Neg A ∈# C" and "A ∉ Interp D"
using c_at_d unfolding true_cls_def by blast
then have "⋀D''. ¬ produces D'' A"
using c_le_d neg_notin_Interp_not_produce by simp
then show ?thesis
using a_in_c subs not_produces_imp_notin_production by auto
qed
lemma true_Interp_imp_interp: "C ≤ D ⟹ D < D' ⟹ Interp D ⊨h C ⟹ interp D' ⊨h C"
using interp_def true_Interp_imp_general by simp
lemma true_Interp_imp_Interp: "C ≤ D ⟹ D < D' ⟹ Interp D ⊨h C ⟹ Interp D' ⊨h C"
using Interp_as_UNION interp_subseteq_Interp true_Interp_imp_general by simp
lemma true_Interp_imp_INTERP: "C ≤ D ⟹ Interp D ⊨h C ⟹ INTERP ⊨h C"
using INTERP_def interp_subseteq_INTERP
true_Interp_imp_general[OF _ le_multiset_right_total]
by simp
lemma true_interp_imp_general:
assumes
c_le_d: "C ≤ D" and
d_lt_d': "D < D'" and
c_at_d: "interp D ⊨h C" and
subs: "interp D' ⊆ (⋃C ∈ CC. production C)"
shows "(⋃C ∈ CC. production C) ⊨h C"
proof (cases "∃A. Pos A ∈# C ∧ A ∈ interp D")
case True
then obtain A where a_in_c: "Pos A ∈# C" and a_at_d: "A ∈ interp D"
by blast
from a_at_d have "A ∈ interp D'"
using d_lt_d' less_eq_imp_interp_subseteq_interp[OF less_imp_le] by blast
then show ?thesis
using subs a_in_c by (blast dest: contra_subsetD)
next
case False
then obtain A where a_in_c: "Neg A ∈# C" and "A ∉ interp D"
using c_at_d unfolding true_cls_def by blast
then have "⋀D''. ¬ produces D'' A"
using c_le_d by (auto dest: produces_imp_in_interp less_eq_imp_interp_subseteq_interp)
then show ?thesis
using a_in_c subs not_produces_imp_notin_production by auto
qed
text ‹This lemma corresponds to \cwref{prop:prop:suppmcprop}{theorem 2.7.7 page 77}. Here the strict
maximality is important›
lemma true_interp_imp_interp: "C ≤ D ⟹ D < D' ⟹ interp D ⊨h C ⟹ interp D' ⊨h C"
using interp_def true_interp_imp_general by simp
lemma true_interp_imp_Interp: "C ≤ D ⟹ D < D' ⟹ interp D ⊨h C ⟹ Interp D' ⊨h C"
using Interp_as_UNION interp_subseteq_Interp[of D'] true_interp_imp_general by simp
lemma true_interp_imp_INTERP: "C ≤ D ⟹ interp D ⊨h C ⟹ INTERP ⊨h C"
using INTERP_def interp_subseteq_INTERP
true_interp_imp_general[OF _ le_multiset_right_total]
by simp
lemma productive_imp_false_interp: "productive C ⟹ ¬ interp C ⊨h C"
unfolding production_unfold by auto
text ‹This lemma corresponds to \cwref{prop:prop:suppmcprop}{theorem 2.7.7 page 77}. Here the strict
maximality is important›
lemma cls_gt_double_pos_no_production:
assumes D: "{#Pos P, Pos P#} < C"
shows "¬produces C P"
proof -
let ?D = "{#Pos P, Pos P#}"
note D' = D[unfolded less_multiset⇩H⇩O]
consider
(P) "count C (Pos P) ≥ 2"
| (Q) Q where "Q > Pos P" and "Q ∈# C "
using HOL.spec[OF HOL.conjunct2[OF D'], of "Pos P"] by (auto split: if_split_asm)
then show ?thesis
proof cases
case Q
have "Q ∈ set_mset C"
using Q(2) by (auto split: if_split_asm)
then have "Max_mset C > Pos P"
using Q(1) Max_gr_iff by blast
then show ?thesis
unfolding production_unfold by auto
next
case P
then show ?thesis
unfolding production_unfold by auto
qed
qed
text ‹This lemma corresponds to \cwref{prop:prop:suppmcprop}{theorem 2.7.7 page 77}.›
lemma
assumes D: "C+{#Neg P#} < D"
shows "production D ≠ {P}"
proof -
note D' = D[unfolded less_multiset⇩H⇩O]
consider
(P) "Neg P ∈# D"
| (Q) Q where "Q > Neg P" and "count D Q > count (C + {#Neg P#}) Q"
using HOL.spec[OF HOL.conjunct2[OF D'], of "Neg P"] count_greater_zero_iff by fastforce
then show ?thesis
proof cases
case Q
have "Q ∈ set_mset D"
using Q(2) gr_implies_not0 by fastforce
then have "Max_mset D > Neg P"
using Q(1) Max_gr_iff by blast
then have "Max_mset D > Pos P"
using less_trans[of "Pos P" "Neg P" "Max_mset D"] by auto
then show ?thesis
unfolding production_unfold by auto
next
case P
then have "Max_mset D > Pos P"
by (meson Max_ge finite_set_mset le_less_trans linorder_not_le pos_less_neg)
then show ?thesis
unfolding production_unfold by auto
qed
qed
lemma in_interp_is_produced:
assumes "P ∈ INTERP"
shows "∃D. D +{#Pos P#} ∈ N ∧ produces (D +{#Pos P#}) P"
using assms unfolding INTERP_def UN_iff production_iff_produces Ball_def
by (metis ground_resolution_with_selection.produces_imp_Pos_in_lits insert_DiffM2
ground_resolution_with_selection_axioms not_produces_imp_notin_production)
end
end
subsection ‹We can now define the rules of the calculus›
inductive superposition_rules :: "'a clause ⇒ 'a clause ⇒ 'a clause ⇒ bool" where
factoring: "superposition_rules (C + {#Pos P#} + {#Pos P#}) B (C + {#Pos P#})" |
superposition_l: "superposition_rules (C⇩1 + {#Pos P#}) (C⇩2 + {#Neg P#}) (C⇩1+ C⇩2)"
inductive superposition :: "'a clause_set ⇒ 'a clause_set ⇒ bool" where
superposition: "A ∈ N ⟹ B ∈ N ⟹ superposition_rules A B C
⟹ superposition N (N ∪ {C})"
definition abstract_red :: "'a::wellorder clause ⇒ 'a clause_set ⇒ bool" where
"abstract_red C N = (clss_lt N C ⊨p C)"
lemma herbrand_true_clss_true_clss_cls_herbrand_true_clss:
assumes
AB: "A ⊨hs B" and
BC: "B ⊨p C"
shows "A ⊨h C"
proof -
let ?I = "{Pos P |P. P ∈ A} ∪ {Neg P |P. P ∉ A}"
have B: "?I ⊨s B" using AB
by (auto simp add: herbrand_interp_iff_partial_interp_clss)
have IH: "⋀I. total_over_set I (atms_of C) ⟹ total_over_m I B ⟹ consistent_interp I
⟹ I ⊨s B ⟹ I ⊨ C" using BC
by (auto simp add: true_clss_cls_def)
show ?thesis
unfolding herbrand_interp_iff_partial_interp_cls
by (auto intro: IH[of ?I] simp add: herbrand_total_over_set herbrand_total_over_m
herbrand_consistent_interp B)
qed
lemma abstract_red_subset_mset_abstract_red:
assumes
abstr: "abstract_red C N" and
c_lt_d: "C ⊆# D"
shows "abstract_red D N"
proof -
have "{D ∈ N. D < C} ⊆ {D' ∈ N. D' < D}"
using subset_eq_imp_le_multiset[OF c_lt_d]
by (metis (no_types, lifting) Collect_mono order.strict_trans2)
then show ?thesis
using abstr unfolding abstract_red_def clss_lt_def
by (metis (no_types, lifting) c_lt_d subset_mset.diff_add true_clss_cls_mono_r'
true_clss_cls_subset)
qed
lemma true_clss_cls_extended:
assumes
"A ⊨p B" and
tot: "total_over_m I A" and
cons: "consistent_interp I" and
I_A: "I ⊨s A"
shows "I ⊨ B"
proof -
let ?I = "I ∪ {Pos P|P. P ∈ atms_of B ∧ P ∉ atms_of_s I}"
have "consistent_interp ?I"
using cons unfolding consistent_interp_def atms_of_s_def atms_of_def
apply (auto 1 5 simp add: image_iff)
by (metis atm_of_uminus literal.sel(1))
moreover have tot_I: "total_over_m ?I (A ∪ {B})"
proof -
obtain aa :: "'a set ⇒ 'a literal set ⇒ 'a" where
f2: "∀x0 x1. (∃v2. v2 ∈ x0 ∧ Pos v2 ∉ x1 ∧ Neg v2 ∉ x1)
⟷ (aa x0 x1 ∈ x0 ∧ Pos (aa x0 x1) ∉ x1 ∧ Neg (aa x0 x1) ∉ x1)"
by moura
have "∀a. a ∉ atms_of_ms A ∨ Pos a ∈ I ∨ Neg a ∈ I"
using tot by (simp add: total_over_m_def total_over_set_def)
then have "aa (atms_of_ms A ∪ atms_of_ms {B}) (I ∪ {Pos a |a. a ∈ atms_of B ∧ a ∉ atms_of_s I})
∉ atms_of_ms A ∪ atms_of_ms {B} ∨ Pos (aa (atms_of_ms A ∪ atms_of_ms {B})
(I ∪ {Pos a |a. a ∈ atms_of B ∧ a ∉ atms_of_s I})) ∈ I
∪ {Pos a |a. a ∈ atms_of B ∧ a ∉ atms_of_s I}
∨ Neg (aa (atms_of_ms A ∪ atms_of_ms {B})
(I ∪ {Pos a |a. a ∈ atms_of B ∧ a ∉ atms_of_s I})) ∈ I
∪ {Pos a |a. a ∈ atms_of B ∧ a ∉ atms_of_s I}"
by auto
then have "total_over_set (I ∪ {Pos a |a. a ∈ atms_of B ∧ a ∉ atms_of_s I})
(atms_of_ms A ∪ atms_of_ms {B})"
using f2 by (meson total_over_set_def)
then show ?thesis
by (simp add: total_over_m_def)
qed
moreover have "?I ⊨s A"
using I_A by auto
ultimately have 1: "?I ⊨ B"
using ‹A⊨pB› unfolding true_clss_cls_def by auto
let ?I' = "I ∪ {Neg P|P. P ∈ atms_of B ∧ P ∉ atms_of_s I}"
have "consistent_interp ?I'"
using cons unfolding consistent_interp_def atms_of_s_def atms_of_def
apply (auto 1 5 simp add: image_iff)
by (metis atm_of_uminus literal.sel(2))
moreover have tot: "total_over_m ?I' (A ∪ {B})"
by (smt Un_iff in_atms_of_s_decomp mem_Collect_eq tot total_over_m_empty total_over_m_insert
total_over_m_union total_over_set_def total_union)
moreover have "?I' ⊨s A"
using I_A by auto
ultimately have 2: "?I' ⊨ B"
using ‹A⊨pB› unfolding true_clss_cls_def by auto
define BB where
‹BB = {P. P ∈ atms_of B ∧ P ∉ atms_of_s I}›
have 1: ‹I ∪ Pos ` BB ⊨ B›
using 1 unfolding BB_def by (simp add: setcompr_eq_image)
have 2: ‹I ∪ Neg ` BB ⊨ B›
using 2 unfolding BB_def by (simp add: setcompr_eq_image)
have ‹finite BB›
unfolding BB_def by auto
then show ?thesis
using 1 2 apply (induction BB)
subgoal by auto
subgoal for x BB
using remove_literal_in_model_tautology[of ‹I ∪ Pos ` BB›]
apply -
apply (rule ccontr)
apply (auto simp: Partial_Herbrand_Interpretation.true_cls_def total_over_set_def total_over_m_def
atms_of_ms_def)
oops
lemma
assumes
CP: "¬ clss_lt N ({#C#} + {#E#}) ⊨p {#C#} + {#Neg P#}" and
"clss_lt N ({#C#} + {#E#}) ⊨p {#E#} + {#Pos P#} ∨ clss_lt N ({#C#} + {#E#}) ⊨p {#C#} + {#Neg P#}"
shows "clss_lt N ({#C#} + {#E#}) ⊨p {#E#} + {#Pos P#}"
oops
locale ground_ordered_resolution_with_redundancy =
ground_resolution_with_selection +
fixes redundant :: "'a::wellorder clause ⇒ 'a clause_set ⇒ bool"
assumes
redundant_iff_abstract: "redundant A N ⟷ abstract_red A N"
begin
definition saturated :: "'a clause_set ⇒ bool" where
"saturated N ⟷
(∀A B C. A ∈ N ⟶ B ∈ N ⟶ ¬redundant A N ⟶ ¬redundant B N ⟶
superposition_rules A B C ⟶ redundant C N ∨ C ∈ N)"
lemma (in -)
assumes ‹A ⊨p C + E›
shows ‹A ⊨p add_mset L C ∨ A ⊨p add_mset (-L) E›
proof clarify
assume ‹¬ A ⊨p add_mset (- L) E›
then obtain I' where
tot': ‹total_over_m I' (A ∪ {add_mset (-L) E})› and
cons': ‹consistent_interp I'› and
I'_A: ‹I' ⊨s A› and
I'_uL_E: ‹¬I' ⊨ add_mset (-L) E›
unfolding true_clss_cls_def by auto
have ‹- L ∉ I'› ‹¬ I' ⊨ E›
using I'_uL_E by auto
moreover have ‹atm_of L ∈ atm_of ` I'›
using tot' unfolding total_over_m_def total_over_set_def
by (cases L) force+
ultimately have ‹L ∈ I'›
by (auto simp: image_iff atm_of_eq_atm_of)
show ‹A ⊨p add_mset L C›
unfolding true_clss_cls_def
proof (intro allI impI conjI)
fix I
assume
tot: ‹total_over_m I (A ∪ {add_mset L C})› and
cons: ‹consistent_interp I› and
I_A: ‹I ⊨s A›
let ?I = "I ∪ {Pos P|P. P ∈ atms_of E ∧ P ∉ atms_of_s I}"
have in_C_pm_I: ‹L ∈# C ⟹ L ∈ I ∨ -L ∈ I› for L
using tot by (cases L) (force simp: total_over_m_def total_over_set_def atms_of_def)+
have "consistent_interp ?I"
using cons unfolding consistent_interp_def atms_of_s_def atms_of_def
apply (auto 1 5 simp add: image_iff)
by (metis atm_of_uminus literal.sel(1))
moreover {
have tot_I: "total_over_m ?I (A ∪ {E})"
using tot total_over_set_def total_union by force
then have tot_I: "total_over_m ?I (A ∪ {C+E})"
using total_union[OF tot] by auto}
moreover have "?I ⊨s A"
using I_A by auto
ultimately have 1: "?I ⊨ C + E"
using assms unfolding true_clss_cls_def by auto
then show ‹I ⊨ add_mset L C›
unfolding Partial_Herbrand_Interpretation.true_cls_def
apply (auto simp: true_cls_def dest: in_C_pm_I)
oops
lemma
assumes
saturated: "saturated N" and
finite: "finite N" and
empty: "{#} ∉ N"
shows "INTERP N ⊨hs N"
proof (rule ccontr)
let ?N⇩ℐ = "INTERP N"
assume "¬ ?thesis"
then have not_empty: "{E∈N. ¬?N⇩ℐ ⊨h E} ≠ {}"
unfolding true_clss_def Ball_def by auto
define D where "D = Min {E∈N. ¬?N⇩ℐ ⊨h E}"
have [simp]: "D ∈ N"
unfolding D_def
by (metis (mono_tags, lifting) Min_in not_empty finite mem_Collect_eq rev_finite_subset subsetI)
have not_d_interp: "¬?N⇩ℐ ⊨h D"
unfolding D_def
by (metis (mono_tags, lifting) Min_in finite mem_Collect_eq not_empty rev_finite_subset subsetI)
have cls_not_D: "⋀E. E ∈ N ⟹ E ≠ D ⟹ ¬?N⇩ℐ ⊨h E ⟹ D ≤ E"
using finite D_def by auto
obtain C L where D: "D = C + {#L#}" and LSD: "L ∈# S D ∨ (S D = {#} ∧ Max_mset D = L)"
proof (cases "S D = {#}")
case False
then obtain L where "L ∈# S D"
using Max_in_lits by blast
moreover {
then have "L ∈# D"
using S_selects_subseteq[of D] by auto
then have "D = (D - {#L#}) + {#L#}"
by auto }
ultimately show ?thesis using that by blast
next
let ?L = "Max_mset D"
case True
moreover {
have "?L ∈# D"
by (metis (no_types, lifting) Max_in_lits ‹D ∈ N› empty)
then have "D = (D - {#?L#}) + {#?L#}"
by auto }
ultimately show ?thesis using that by blast
qed
have red: "¬redundant D N"
proof (rule ccontr)
assume red[simplified]: "~~redundant D N"
have "∀E < D. E ∈ N ⟶ ?N⇩ℐ ⊨h E"
using cls_not_D unfolding not_le[symmetric] by fastforce
then have "?N⇩ℐ ⊨hs clss_lt N D"
unfolding clss_lt_def true_clss_def Ball_def by blast
then show False
using red not_d_interp unfolding abstract_red_def redundant_iff_abstract
using herbrand_true_clss_true_clss_cls_herbrand_true_clss by fast
qed
consider
(L) P where "L = Pos P" and "S D = {#}" and "Max_mset D = Pos P"
| (Lneg) P where "L = Neg P"
using LSD S_selects_neg_lits[of L D] by (cases L) auto
then show False
proof cases
case L note P = this(1) and S = this(2) and max = this(3)
have "count D L > 1"
proof (rule ccontr)
assume "~ ?thesis"
then have count: "count D L = 1"
unfolding D by (auto simp: not_in_iff)
have "¬?N⇩ℐ⊨h D"
using not_d_interp true_interp_imp_INTERP ground_resolution_with_selection_axioms
by blast
then have "produces N D P"
using not_empty empty finite ‹D ∈ N› count L
true_interp_imp_INTERP unfolding production_iff_produces unfolding production_unfold
by (auto simp add: max not_empty)
then have "INTERP N ⊨h D"
unfolding D
by (metis pos_literal_in_imp_true_cls produces_imp_Pos_in_lits
production_subseteq_INTERP singletonI subsetCE)
then show False
using not_d_interp by blast
qed
then have "Pos P ∈# C"
by (simp add: P D)
then obtain C' where C':"D = C' + {#Pos P#} + {#Pos P#}"
unfolding D by (metis (full_types) P insert_DiffM2)
have sup: "superposition_rules D D (D - {#L#})"
unfolding C' L by (auto simp add: superposition_rules.simps)
have "C' + {#Pos P#} < C' + {#Pos P#} + {#Pos P#}"
by auto
moreover have "¬?N⇩ℐ ⊨h (D - {#L#})"
using not_d_interp unfolding C' L by auto
ultimately have "C' + {#Pos P#} ∉ N"
using C' P cls_not_D by fastforce
have "D - {#L#} < D"
unfolding C' L by auto
have c'_p_p: "C' + {#Pos P#} + {#Pos P#} - {#Pos P#} = C' + {#Pos P#}"
by auto
have "redundant (C' + {#Pos P#}) N"
using saturated red sup ‹D ∈ N›‹C' + {#Pos P#} ∉ N› unfolding saturated_def C' L c'_p_p
by blast
moreover have "C' + {#Pos P#} ⊆# C' + {#Pos P#} + {#Pos P#}"
by auto
ultimately show False
using red unfolding C' redundant_iff_abstract by (blast dest:
abstract_red_subset_mset_abstract_red)
next
case Lneg note L = this(1)
have P: "P ∈ ?N⇩ℐ"
using not_d_interp unfolding D true_cls_def L by (auto split: if_split_asm)
then obtain E where
DPN: "E + {#Pos P#} ∈ N" and
prod: "production N (E + {#Pos P#}) = {P}"
using in_interp_is_produced by blast
have ‹¬ ?N⇩ℐ ⊨h C›
using not_d_interp P unfolding D Lneg by auto
then have uL_C: ‹Pos P ∉# C›
using P unfolding Lneg by blast
have sup_EC: "superposition_rules (E + {#Pos P#}) (C + {#Neg P#}) (E + C)"
using superposition_l by fast
then have "superposition N (N ∪ {E+C})"
using DPN ‹D ∈ N› unfolding D L by (auto simp add: superposition.simps)
have
PMax: "Pos P = Max_mset (E + {#Pos P#})" and
"count (E + {#Pos P#}) (Pos P) ≤ 1" and
"S (E + {#Pos P#}) = {#}" and
"¬interp N (E + {#Pos P#}) ⊨h E + {#Pos P#}"
using prod unfolding production_unfold by auto
have "Neg P ∉# E"
using prod produces_imp_neg_notin_lits by force
then have "⋀y. y ∈# (E + {#Pos P#}) ⟹
count (E + {#Pos P#}) (Neg P) < count (C + {#Neg P#}) (Neg P)"
using count_greater_zero_iff by fastforce
moreover have "⋀y. y ∈# (E + {#Pos P#}) ⟹ y < Neg P"
using PMax by (metis DPN Max_less_iff empty finite_set_mset pos_less_neg
set_mset_eq_empty_iff)
moreover have "E + {#Pos P#} ≠ C + {#Neg P#}"
using prod produces_imp_neg_notin_lits by force
ultimately have "E + {#Pos P#} < C + {#Neg P#}"
unfolding less_multiset⇩H⇩O by (metis count_greater_zero_iff less_iff_Suc_add zero_less_Suc)
have ce_lt_d: "C + E < D"
unfolding D L by (simp add: ‹⋀y. y ∈# E + {#Pos P#} ⟹ y < Neg P› ex_gt_imp_less_multiset)
have "?N⇩ℐ ⊨h E + {#Pos P#}"
using ‹P ∈ ?N⇩ℐ› by blast
have "?N⇩ℐ ⊨h C+E ∨ C+E ∉ N"
using ce_lt_d cls_not_D unfolding D_def by fastforce
have Pos_P_C_E: "Pos P ∉# C+E"
using D ‹P ∈ ground_resolution_with_selection.INTERP S N›
‹count (E + {#Pos P#}) (Pos P) ≤ 1› multi_member_skip not_d_interp
by (auto simp: not_in_iff)
then have "⋀y. y ∈# C+E ⟹ count (C+E) (Pos P) < count (E + {#Pos P#}) (Pos P)"
using set_mset_def by fastforce
have "¬redundant (C + E) N"
proof (rule ccontr)
assume red'[simplified]: "¬ ?thesis"
have abs: "clss_lt N (C + E) ⊨p C + E"
using redundant_iff_abstract red' unfolding abstract_red_def by auto
moreover
have ‹clss_lt N (C + E) ⊆ clss_lt N (E + {#Pos P#})›
using ce_lt_d Pos_P_C_E uL_C apply (auto simp: clss_lt_def D L)
using Pos_P_C_E unfolding less_multiset⇩H⇩O
apply (auto split: if_splits)
sorry
then have "clss_lt N (E + {#Pos P#}) ⊨p E + {#Pos P#} ∨
clss_lt N (C + {#Neg P#}) ⊨p C + {#Neg P#}"
proof clarify
assume CP: "¬ clss_lt N (C + {#Neg P#}) ⊨p C + {#Neg P#}"
{ fix I
assume
"total_over_m I (clss_lt N (C + E) ∪ {E + {#Pos P#}})" and
"consistent_interp I" and
"I ⊨s clss_lt N (C + E)"
then have "I ⊨ C + E"
using abs sorry
moreover have "¬ I ⊨ C + {#Neg P#}"
using CP unfolding true_clss_cls_def
sorry
ultimately have "I ⊨ E + {#Pos P#}" by auto
}
then show "clss_lt N (E + {#Pos P#}) ⊨p E + {#Pos P#}"
unfolding true_clss_cls_def sorry
qed
then have "clss_lt N (C + E) ⊨p E + {#Pos P#} ∨ clss_lt N (C + E) ⊨p C + {#Neg P#}"
proof clarify
assume CP: "¬ clss_lt N (C + E) ⊨p C + {#Neg P#}"
{ fix I
assume
"total_over_m I (clss_lt N (C + E) ∪ {E + {#Pos P#}})" and
"consistent_interp I" and
"I ⊨s clss_lt N (C + E)"
then have "I ⊨ C + E"
using abs sorry
moreover have "¬ I ⊨ C + {#Neg P#}"
using CP unfolding true_clss_cls_def
sorry
ultimately have "I ⊨ E + {#Pos P#}" by auto
}
then show "clss_lt N (C + E) ⊨p E + {#Pos P#}"
unfolding true_clss_cls_def by auto
qed
moreover have "clss_lt N (C + E) ⊆ clss_lt N (C + {#Neg P#})"
using ce_lt_d order.strict_trans2 unfolding clss_lt_def D L
by (blast dest: less_imp_le)
ultimately have "redundant (C + {#Neg P#}) N ∨ clss_lt N (C + E) ⊨p E + {#Pos P#} "
unfolding redundant_iff_abstract abstract_red_def using true_clss_cls_subset by blast
show False
sorry
qed
moreover have "¬ redundant (E + {#Pos P#}) N"
sorry
ultimately have CEN: "C + E ∈ N"
using ‹D∈N› ‹E + {#Pos P#}∈N› saturated sup_EC red unfolding saturated_def D L
by (metis union_commute)
have CED: "C + E ≠ D"
using D ce_lt_d by auto
have interp: "¬ INTERP N ⊨h C + E"
sorry
show False
using cls_not_D[OF CEN CED interp] ce_lt_d unfolding INTERP_def less_eq_multiset_def by auto
qed
qed
end
lemma tautology_is_redundant:
assumes "tautology C"
shows "abstract_red C N"
using assms unfolding abstract_red_def true_clss_cls_def tautology_def by auto
lemma subsumed_is_redundant:
assumes AB: "A ⊂# B"
and AN: "A ∈ N"
shows "abstract_red B N"
proof -
have "A ∈ clss_lt N B" using AN AB unfolding clss_lt_def
by (auto dest: subset_eq_imp_le_multiset simp add: dual_order.order_iff_strict)
then show ?thesis
using AB unfolding abstract_red_def true_clss_cls_def Partial_Herbrand_Interpretation.true_clss_def
by blast
qed
inductive redundant :: "'a clause ⇒ 'a clause_set ⇒ bool" where
subsumption: "A ∈ N ⟹ A ⊂# B ⟹ redundant B N"
lemma redundant_is_redundancy_criterion:
fixes A :: "'a :: wellorder clause" and N :: "'a :: wellorder clause_set"
assumes "redundant A N"
shows "abstract_red A N"
using assms
proof (induction rule: redundant.induct)
case (subsumption A B N)
then show ?case
using subsumed_is_redundant[of A N B] unfolding abstract_red_def clss_lt_def by auto
qed
lemma redundant_mono:
"redundant A N ⟹ A ⊆# B ⟹ redundant B N"
apply (induction rule: redundant.induct)
by (meson subset_mset.less_le_trans subsumption)
locale truc =
selection S for S :: "nat clause ⇒ nat clause"
begin
end
end