theory Prop_Superposition
imports Partial_Clausal_Logic "../lib/Herbrand_Interpretation"
begin
sledgehammer_params[verbose]
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_Clausal_Logic.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_Clausal_Logic.true_clss_def by auto
definition clss_lt :: "'a::wellorder clauses ⇒ 'a clause ⇒ 'a clauses" 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 (set_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 (set_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 (set_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 le_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 (set_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 (set_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 multiset_order.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 multiset_order.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 multiset_order.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 multiset_linorder.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 multiset_linorder.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 multiset_linorder.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 multiset_linorder.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.6 page 66}.›
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 (set_mset D) = Pos A"
using production_unfold by blast
hence "D #⊂# {#Neg A#}"
by (auto intro: Max_pos_neg_less_multiset)
moreover have "{#Neg A#} #⊆# C"
by (rule less_eq_imp_le_multiset) (rule mset_le_single[OF a_in_c[unfolded mem_set_mset_iff]])
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
thus ?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
hence "⋀D''. ¬ produces D'' A"
using c_le_d neg_notin_Interp_not_produce by simp
thus ?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 _ less_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 multiset_order.less_imp_le] by blast
thus ?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
hence "⋀D''. ¬ produces D'' A"
using c_le_d by (auto dest: produces_imp_in_interp less_eq_imp_interp_subseteq_interp)
thus ?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.6 page 66}. 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 _ less_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.6 page 66}. 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
thus ?thesis
proof cases
case Q
have "Q ∈ set_mset C"
using Q(2) by (auto split: split_if_asm)
then have "Max (set_mset C) > Pos P"
using Q(1) Max_gr_iff by blast
thus ?thesis
unfolding production_unfold by auto
next
case P
thus ?thesis
unfolding production_unfold by auto
qed
qed
text ‹This lemma corresponds to \cwref{prop:prop:suppmcprop}{theorem 2.7.6 page 66}.›
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"] by fastforce
thus ?thesis
proof cases
case Q
have "Q ∈ set_mset D"
using Q(2) by (auto split: split_if_asm)
then have "Max (set_mset D) > Neg P"
using Q(1) Max_gr_iff by blast
hence "Max (set_mset D) > Pos P"
using less_trans[of "Pos P" "Neg P" "Max (set_mset D)"] by auto
thus ?thesis
unfolding production_unfold by auto
next
case P
hence "Max (set_mset D) > Pos P"
by (meson Max_ge finite_set_mset le_less_trans linorder_not_le mem_set_mset_iff
pos_less_neg)
thus ?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
abbreviation "MMax M ≡ Max (set_mset M)"
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 clauses ⇒ 'a clauses ⇒ bool" where
superposition: "A ∈ N ⟹ B ∈ N ⟹ superposition_rules A B C
⟹ superposition N (N ∪ {C})"
definition abstract_red :: "'a::wellorder clause ⇒ 'a clauses ⇒ bool" where
"abstract_red C N = (clss_lt N C ⊨p C)"
lemma less_multiset[iff]: "M < N ⟷ M #⊂# N"
unfolding less_multiset_def by auto
lemma less_eq_multiset[iff]: "M ≤ N ⟷ M #⊆# N"
unfolding less_eq_multiset_def by auto
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 c_lt_d less_eq_imp_le_multiset by fastforce
thus ?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 "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)
hence "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
hence "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)
thus ?thesis
by (simp add: total_over_m_def)
qed
moreover have "?I ⊨s A"
using I_A by auto
ultimately have "?I ⊨ B"
using ‹A⊨pB› unfolding true_clss_cls_def by auto
thus ?thesis
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 clauses ⇒ bool"
assumes
redundant_iff_abstract: "redundant A N ⟷ abstract_red A N"
begin
definition saturated :: "'a clauses ⇒ 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
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"
hence not_empty: "{E∈N. ¬?N⇩ℐ ⊨h E} ≠ {}"
unfolding true_clss_def Ball_def by auto
def 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 simp del: less_eq_multiset)
obtain C L where D: "D = C + {#L#}" and LSD: "L ∈# S D ∨ (S D = {#} ∧ Max (set_mset D) = L)"
proof (cases "S D = {#}")
case False
then obtain L where "L ∈# S D"
using Max_in_lits by blast
moreover
hence "L ∈# D"
using S_selects_subseteq[of D] by auto
hence "D = (D - {#L#}) + {#L#}"
by auto
ultimately show ?thesis using that by blast
next
let ?L = "MMax D"
case True
moreover
have "?L ∈# D"
by (metis (no_types, lifting) Max_in_lits ‹D ∈ N› empty)
hence "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 not_le by fastforce
hence "?N⇩ℐ ⊨hs clss_lt N D"
unfolding clss_lt_def true_clss_def Ball_def by blast
thus 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 (set_mset D) = Pos P"
| (Lneg) P where "L = Neg P"
using LSD S_selects_neg_lits[of D L] by (cases L) auto
thus 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"
hence count: "count D L = 1"
unfolding D by auto
have "¬?N⇩ℐ⊨h D"
using not_d_interp true_interp_imp_INTERP ground_resolution_with_selection_axioms
by blast
hence "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)
hence "INTERP N ⊨h D"
unfolding D
by (metis pos_literal_in_imp_true_cls produces_imp_Pos_in_lits
production_subseteq_INTERP singletonI subsetCE)
thus False
using not_d_interp by blast
qed
then obtain C' where C':"D = C' + {#Pos P#} + {#Pos P#}"
unfolding D by (metis P add.left_neutral add_less_cancel_right count_single count_union
multi_member_split)
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"
by (metis (no_types, lifting) C' P add_diff_cancel_right' cls_not_D less_multiset
multi_self_add_other_not_self not_le)
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 ∈ ?N⇩ℐ"
using not_d_interp unfolding D true_cls_def L by (auto split: split_if_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 sup_EC: "superposition_rules (E + {#Pos P#}) (C + {#Neg P#}) (E + C)"
using superposition_l by fast
hence "superposition N (N ∪ {E+C})"
using DPN ‹D ∈ N› unfolding D L by (auto simp add: superposition.simps)
have
PMax: "Pos P = MMax (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
hence "⋀y. y ∈# (E + {#Pos P#})
⟹ count (E + {#Pos P#}) (Neg P) < count (C + {#Neg P#}) (Neg P)"
by (auto split: split_if_asm)
moreover have "⋀y. y ∈# (E + {#Pos P#}) ⟹ y < Neg P"
using PMax by (metis DPN Max_less_iff empty finite_set_mset mem_set_mset_iff 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 add.left_neutral add_lessD1)
have ce_lt_d: "C + E #⊂# D"
unfolding D L
by (metis (mono_tags, lifting) Max_pos_neg_less_multiset One_nat_def PMax count_single
less_multiset_plus_right_nonempty mult_less_trans single_not_empty union_less_mono2
zero_less_Suc)
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"
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
hence "⋀y. y ∈# C+E
⟹ count (C+E) (Pos P) < count (E + {#Pos P#}) (Pos P)"
by (auto split: split_if_asm)
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
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)"
hence "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 mult_less_trans unfolding clss_lt_def D L by force
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: less_eq_imp_le_multiset simp add: multiset_order.dual_order.order_iff_strict)
thus ?thesis
using AB unfolding abstract_red_def true_clss_cls_def Partial_Clausal_Logic.true_clss_def
by blast
qed
inductive redundant :: "'a clause ⇒ 'a clauses ⇒ bool" where
subsumption: "A ∈ N ⟹ A ⊂# B ⟹ redundant B N"
lemma redundant_is_redundancy_criterion:
fixes A :: "'a :: wellorder clause" and N :: "'a :: wellorder clauses"
assumes "redundant A N"
shows "abstract_red A N"
using assms
proof (induction rule: redundant.induct)
case (subsumption A B N)
thus ?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