Theory ORD_RES_7
theory ORD_RES_7
imports
Background
Implicit_Exhaustive_Factorization
Exhaustive_Resolution
begin
section ‹ORD-RES-7 (clause-guided literal trail construction)›
context simulation_SCLFOL_ground_ordered_resolution begin
inductive ord_res_7 where
decide_neg: "
¬ trail_false_cls Γ C ⟹
linorder_lit.is_maximal_in_mset C L ⟹
linorder_trm.is_least_in_fset {|A |∈| atms_of_clss (N |∪| U⇩e⇩r).
A ≺⇩t atm_of L ∧ A |∉| trail_atms Γ|} A ⟹
Γ' = (Neg A, None) # Γ ⟹
ord_res_7 N (U⇩e⇩r, ℱ, Γ, Some C) (U⇩e⇩r, ℱ, Γ', Some C)" |
skip_defined: "
¬ trail_false_cls Γ C ⟹
linorder_lit.is_maximal_in_mset C L ⟹
¬(∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of L ∧ A |∉| trail_atms Γ) ⟹
trail_defined_lit Γ L ⟹
𝒞' = The_optional (linorder_cls.is_least_in_fset {|D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D|}) ⟹
ord_res_7 N (U⇩e⇩r, ℱ, Γ, Some C) (U⇩e⇩r, ℱ, Γ, 𝒞')" |
skip_undefined_neg: "
¬ trail_false_cls Γ C ⟹
linorder_lit.is_maximal_in_mset C L ⟹
¬(∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of L ∧ A |∉| trail_atms Γ) ⟹
¬ trail_defined_lit Γ L ⟹
is_neg L ⟹
Γ' = (L, None) # Γ ⟹
𝒞' = The_optional (linorder_cls.is_least_in_fset {|D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D|}) ⟹
ord_res_7 N (U⇩e⇩r, ℱ, Γ, Some C) (U⇩e⇩r, ℱ, Γ', 𝒞')" |
skip_undefined_pos: "
¬ trail_false_cls Γ C ⟹
linorder_lit.is_maximal_in_mset C L ⟹
¬(∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of L ∧ A |∉| trail_atms Γ) ⟹
¬ trail_defined_lit Γ L ⟹
is_pos L ⟹
¬ trail_false_cls Γ {#K ∈# C. K ≠ L#} ⟹
linorder_cls.is_least_in_fset {|D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D|} D ⟹
ord_res_7 N (U⇩e⇩r, ℱ, Γ, Some C) (U⇩e⇩r, ℱ, Γ, Some D)" |
skip_undefined_pos_ultimate: "
¬ trail_false_cls Γ C ⟹
linorder_lit.is_maximal_in_mset C L ⟹
¬(∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of L ∧ A |∉| trail_atms Γ) ⟹
¬ trail_defined_lit Γ L ⟹
is_pos L ⟹
¬ trail_false_cls Γ {#K ∈# C. K ≠ L#} ⟹
Γ' = (- L, None) # Γ ⟹
¬(∃D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D) ⟹
ord_res_7 N (U⇩e⇩r, ℱ, Γ, Some C) (U⇩e⇩r, ℱ, Γ', None)" |
production: "
¬ trail_false_cls Γ C ⟹
linorder_lit.is_maximal_in_mset C L ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of L ∧ A |∉| trail_atms Γ) ⟹
¬ trail_defined_lit Γ L ⟹
is_pos L ⟹
trail_false_cls Γ {#K ∈# C. K ≠ L#} ⟹
linorder_lit.is_greatest_in_mset C L ⟹
Γ' = (L, Some C) # Γ ⟹
𝒞' = The_optional (linorder_cls.is_least_in_fset {|D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D|}) ⟹
ord_res_7 N (U⇩e⇩r, ℱ, Γ, Some C) (U⇩e⇩r, ℱ, Γ', 𝒞')" |
factoring: "
¬ trail_false_cls Γ C ⟹
linorder_lit.is_maximal_in_mset C L ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of L ∧ A |∉| trail_atms Γ) ⟹
¬ trail_defined_lit Γ L ⟹
is_pos L ⟹
trail_false_cls Γ {#K ∈# C. K ≠ L#} ⟹
¬ linorder_lit.is_greatest_in_mset C L ⟹
ℱ' = finsert C ℱ ⟹
ord_res_7 N (U⇩e⇩r, ℱ, Γ, Some C) (U⇩e⇩r, ℱ', Γ, Some (efac C))" |
resolution_bot: "
trail_false_cls Γ E ⟹
linorder_lit.is_maximal_in_mset E L ⟹
is_neg L ⟹
map_of Γ (- L) = Some (Some D) ⟹
U⇩e⇩r' = finsert (eres D E) U⇩e⇩r ⟹
eres D E = {#} ⟹
Γ' = [] ⟹
ord_res_7 N (U⇩e⇩r, ℱ, Γ, Some E) (U⇩e⇩r', ℱ, Γ', Some {#})" |
resolution_pos: "
trail_false_cls Γ E ⟹
linorder_lit.is_maximal_in_mset E L ⟹
is_neg L ⟹
map_of Γ (- L) = Some (Some D) ⟹
U⇩e⇩r' = finsert (eres D E) U⇩e⇩r ⟹
eres D E ≠ {#} ⟹
Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ ⟹
linorder_lit.is_maximal_in_mset (eres D E) K ⟹
is_pos K ⟹
ord_res_7 N (U⇩e⇩r, ℱ, Γ, Some E) (U⇩e⇩r', ℱ, Γ', Some (eres D E))" |
resolution_neg: "
trail_false_cls Γ E ⟹
linorder_lit.is_maximal_in_mset E L ⟹
is_neg L ⟹
map_of Γ (- L) = Some (Some D) ⟹
U⇩e⇩r' = finsert (eres D E) U⇩e⇩r ⟹
eres D E ≠ {#} ⟹
Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ ⟹
linorder_lit.is_maximal_in_mset (eres D E) K ⟹
is_neg K ⟹
map_of Γ (- K) = Some (Some C) ⟹
ord_res_7 N (U⇩e⇩r, ℱ, Γ, Some E) (U⇩e⇩r', ℱ, Γ', Some C)"
lemma right_unique_ord_res_7:
fixes N :: "'f gclause fset"
shows "right_unique (ord_res_7 N)"
proof (rule right_uniqueI)
fix x y z
assume step1: "ord_res_7 N x y" and step2: "ord_res_7 N x z"
show "y = z"
using step1
proof (cases N x y rule: ord_res_7.cases)
case step_hyps1: (decide_neg Γ C L U⇩e⇩r A Γ' ℱ)
show ?thesis
using step2
unfolding step_hyps1(1)
proof (cases N "(U⇩e⇩r, ℱ, Γ, Some C)" z rule: ord_res_7.cases)
case step_hyps2: (decide_neg L2 A2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of C, THEN Uniq_D] by metis
have "A2 = A"
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
using linorder_trm.Uniq_is_least_in_fset[THEN Uniq_D] by presburger
have "Γ2' = Γ'"
using step_hyps1 step_hyps2
unfolding ‹L2 = L› ‹A2 = A› by metis
show ?thesis
unfolding step_hyps1(2) step_hyps2(1)
unfolding ‹Γ2' = Γ'› ..
next
case step_hyps2: (skip_defined L2 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (skip_undefined_neg L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos L2 D2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos_ultimate L2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (production L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of C, THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (factoring L2 ℱ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of C, THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (resolution_bot L2 D2 U⇩e⇩r2' Γ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_pos L2 D2 U⇩e⇩r2' Γ2' K2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_neg L2 D2 U⇩e⇩r2' Γ2' K2 C2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
qed
next
case step_hyps1: (skip_defined Γ C L U⇩e⇩r 𝒞' ℱ)
show ?thesis
using step2
unfolding step_hyps1(1)
proof (cases N "(U⇩e⇩r, ℱ, Γ, Some C)" z rule: ord_res_7.cases)
case step_hyps2: (decide_neg L2 A2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of C, THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (skip_defined L2 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have "𝒞2' = 𝒞'"
using step_hyps1 step_hyps2 by argo
show ?thesis
unfolding step_hyps1(2) step_hyps2(1)
unfolding ‹𝒞2' = 𝒞'› ..
next
case step_hyps2: (skip_undefined_neg L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos L2 D2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos_ultimate L2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (production L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of C, THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (factoring L2 ℱ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of C, THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (resolution_bot L2 D2 U⇩e⇩r2' Γ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_pos L2 D2 U⇩e⇩r2' Γ2' K2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_neg L2 D2 U⇩e⇩r2' Γ2' K2 C2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
qed
next
case step_hyps1: (skip_undefined_neg Γ C L U⇩e⇩r Γ' 𝒞' ℱ)
show ?thesis
using step2 unfolding step_hyps1(1)
proof (cases N "(U⇩e⇩r, ℱ, Γ, Some C)" z rule: ord_res_7.cases)
case step_hyps2: (decide_neg L2 A2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (skip_defined L2 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_neg L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have "Γ2' = Γ'"
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
have "𝒞2' = 𝒞'"
using step_hyps1 step_hyps2 by argo
show ?thesis
unfolding step_hyps1(2) step_hyps2(1)
unfolding ‹𝒞2' = 𝒞'› ‹Γ2' = Γ'› ..
next
case step_hyps2: (skip_undefined_pos L2 D2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos_ultimate L2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (production L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (factoring L2 ℱ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (resolution_bot L2 D2 U⇩e⇩r2' Γ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_pos L2 D2 U⇩e⇩r2' Γ2' K2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_neg L2 D2 U⇩e⇩r2' Γ2' K2 C2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
qed
next
case step_hyps1: (skip_undefined_pos Γ C L U⇩e⇩r ℱ D)
show ?thesis
using step2 unfolding step_hyps1(1)
proof (cases N "(U⇩e⇩r, ℱ, Γ, Some C)" z rule: ord_res_7.cases)
case step_hyps2: (decide_neg L2 A2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (skip_defined L2 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_neg L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos L2 D2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have "D2 = D"
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
by (meson Uniq_D linorder_cls.Uniq_is_least_in_fset)
show ?thesis
unfolding step_hyps1(2) step_hyps2(1)
unfolding ‹D2 = D› ..
next
case step_hyps2: (skip_undefined_pos_ultimate L2 Γ')
have False
using step_hyps1 step_hyps2
by (metis linorder_cls.is_least_in_ffilter_iff)
thus ?thesis ..
next
case step_hyps2: (production L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (factoring L2 ℱ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (resolution_bot L2 D2 U⇩e⇩r2' Γ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_pos L2 D2 U⇩e⇩r2' Γ2' K2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_neg L2 D2 U⇩e⇩r2' Γ2' K2 C2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
qed
next
case step_hyps1: (skip_undefined_pos_ultimate Γ C L U⇩e⇩r Γ' ℱ)
show ?thesis
using step2 unfolding step_hyps1(1)
proof (cases N "(U⇩e⇩r, ℱ, Γ, Some C)" z rule: ord_res_7.cases)
case step_hyps2: (decide_neg L2 A2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (skip_defined L2 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_neg L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos L2 D2)
have False
using step_hyps1 step_hyps2
by (metis linorder_cls.is_least_in_ffilter_iff)
thus ?thesis ..
next
case step_hyps2: (skip_undefined_pos_ultimate L2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have "Γ2' = Γ'"
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
show ?thesis
unfolding step_hyps1(2) step_hyps2(1)
unfolding ‹Γ2' = Γ'› ..
next
case step_hyps2: (production L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (factoring L2 ℱ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (resolution_bot L2 D2 U⇩e⇩r2' Γ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_pos L2 D2 U⇩e⇩r2' Γ2' K2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_neg L2 D2 U⇩e⇩r2' Γ2' K2 C2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
qed
next
case step_hyps1: (production Γ C L U⇩e⇩r Γ' 𝒞' ℱ)
show ?thesis
using step2
unfolding step_hyps1(1)
proof (cases N "(U⇩e⇩r, ℱ, Γ, Some C)" z rule: ord_res_7.cases)
case step_hyps2: (decide_neg L2 A2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of C, THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (skip_defined L2 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_neg L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos L2 D2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos_ultimate L2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (production L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of C, THEN Uniq_D] by metis
have "Γ2' = Γ'"
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
have "𝒞2' = 𝒞'"
using step_hyps1 step_hyps2 by argo
show ?thesis
unfolding step_hyps1(2) step_hyps2(1)
unfolding ‹Γ2' = Γ'› ‹𝒞2' = 𝒞'› ..
next
case step_hyps2: (factoring L2 ℱ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of C, THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (resolution_bot L2 D2 U⇩e⇩r2' Γ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_pos L2 D2 U⇩e⇩r2' Γ2' K2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_neg L2 D2 U⇩e⇩r2' Γ2' K2 C2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
qed
next
case step_hyps1: (factoring Γ C L U⇩e⇩r ℱ' ℱ)
show ?thesis
using step2
unfolding step_hyps1(1)
proof (cases N "(U⇩e⇩r, ℱ, Γ, Some C)" z rule: ord_res_7.cases)
case step_hyps2: (decide_neg L2 A2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of C, THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (skip_defined L2 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_neg L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos L2 D2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos_ultimate L2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (production L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of C, THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
unfolding linorder_trm.is_least_in_ffilter_iff by metis
then show ?thesis ..
next
case step_hyps2: (factoring L2 ℱ2')
have "ℱ2' = ℱ'"
using step_hyps1 step_hyps2
by argo
show ?thesis
unfolding step_hyps1(2) step_hyps2(1)
unfolding ‹ℱ2' = ℱ'› ..
next
case step_hyps2: (resolution_bot L2 D2 U⇩e⇩r2' Γ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_pos L2 D2 U⇩e⇩r2' Γ2' K2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_neg L2 D2 U⇩e⇩r2' Γ2' K2 C2)
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
qed
next
case step_hyps1: (resolution_bot Γ E L D U⇩e⇩r' U⇩e⇩r Γ' ℱ)
show ?thesis
using step2
unfolding step_hyps1(1)
proof (cases N "(U⇩e⇩r, ℱ, Γ, Some E)" z rule: ord_res_7.cases)
case step_hyps2: (decide_neg L2 A2 Γ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (skip_defined L2 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_neg L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos L2 D2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos_ultimate L2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (production L2 Γ2' 𝒞2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (factoring L2 ℱ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_bot L2 D2 U⇩e⇩r2' Γ2')
have "U⇩e⇩r2' = U⇩e⇩r'"
using step_hyps1 step_hyps2
by argo
have "Γ2' = Γ'"
using step_hyps1 step_hyps2
by argo
show ?thesis
unfolding step_hyps1(2) step_hyps2(1)
unfolding ‹U⇩e⇩r2' = U⇩e⇩r'› ‹Γ2' = Γ'› ..
next
case step_hyps2: (resolution_pos L2 D2 U⇩e⇩r2' Γ2' K2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of E, THEN Uniq_D] by metis
have "D2 = D"
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
by (metis option.inject)
have False
using step_hyps1 step_hyps2
unfolding ‹D2 = D›
by argo
then show ?thesis ..
next
case step_hyps2: (resolution_neg L2 D2 U⇩e⇩r2' Γ2' K2 C2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of E, THEN Uniq_D] by metis
have "D2 = D"
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
by (metis option.inject)
have False
using step_hyps1 step_hyps2
unfolding ‹D2 = D›
by argo
then show ?thesis ..
qed
next
case step_hyps1: (resolution_pos Γ E L D U⇩e⇩r' U⇩e⇩r Γ' K ℱ)
show ?thesis
using step2
unfolding step_hyps1(1)
proof (cases N "(U⇩e⇩r, ℱ, Γ, Some E)" z rule: ord_res_7.cases)
case step_hyps2: (decide_neg L2 A2 Γ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (skip_defined L2 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_neg L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos L2 D2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos_ultimate L2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (production L2 Γ2' 𝒞2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (factoring L2 ℱ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_bot L2 D2 U⇩e⇩r2' Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of E, THEN Uniq_D] by metis
have "D2 = D"
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
by (metis option.inject)
have False
using step_hyps1 step_hyps2
unfolding ‹D2 = D›
by argo
then show ?thesis ..
next
case step_hyps2: (resolution_pos L2 D2 U⇩e⇩r2' Γ2' K2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of E, THEN Uniq_D] by metis
have "D2 = D"
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
by (metis option.inject)
have "K2 = K"
using step_hyps1 step_hyps2
unfolding ‹D2 = D›
using linorder_lit.Uniq_is_maximal_in_mset[of "eres D E", THEN Uniq_D] by metis
have "U⇩e⇩r2' = U⇩e⇩r'"
using step_hyps1 step_hyps2
unfolding ‹D2 = D›
by argo
have "Γ2' = Γ'"
using step_hyps1 step_hyps2
unfolding ‹K2 = K›
by argo
show ?thesis
unfolding step_hyps1(2) step_hyps2(1)
unfolding ‹U⇩e⇩r2' = U⇩e⇩r'› ‹Γ2' = Γ'› ‹D2 = D› ..
next
case step_hyps2: (resolution_neg L2 D2 U⇩e⇩r2' Γ2' K2 C2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of E, THEN Uniq_D] by metis
have "D2 = D"
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
by (metis option.inject)
have "K2 = K"
using step_hyps1 step_hyps2
unfolding ‹D2 = D›
using linorder_lit.Uniq_is_maximal_in_mset[of "eres D E", THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹K2 = K›
by argo
then show ?thesis ..
qed
next
case step_hyps1: (resolution_neg Γ E L D U⇩e⇩r' U⇩e⇩r Γ' K C ℱ)
show ?thesis
using step2
unfolding step_hyps1(1)
proof (cases N "(U⇩e⇩r, ℱ, Γ, Some E)" z rule: ord_res_7.cases)
case step_hyps2: (decide_neg L2 A2 Γ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (skip_defined L2 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_neg L2 Γ2' 𝒞2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos L2 D2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (skip_undefined_pos_ultimate L2 Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹L2 = L› by argo
then show ?thesis ..
next
case step_hyps2: (production L2 Γ2' 𝒞2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (factoring L2 ℱ2')
have False
using step_hyps1 step_hyps2 by argo
then show ?thesis ..
next
case step_hyps2: (resolution_bot L2 D2 U⇩e⇩r2' Γ2')
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of E, THEN Uniq_D] by metis
have "D2 = D"
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
by (metis option.inject)
have False
using step_hyps1 step_hyps2
unfolding ‹D2 = D›
by argo
then show ?thesis ..
next
case step_hyps2: (resolution_pos L2 D2 U⇩e⇩r2' Γ2' K2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of E, THEN Uniq_D] by metis
have "D2 = D"
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
by (metis option.inject)
have "K2 = K"
using step_hyps1 step_hyps2
unfolding ‹D2 = D›
using linorder_lit.Uniq_is_maximal_in_mset[of "eres D E", THEN Uniq_D] by metis
have False
using step_hyps1 step_hyps2
unfolding ‹K2 = K›
by argo
then show ?thesis ..
next
case step_hyps2: (resolution_neg L2 D2 U⇩e⇩r2' Γ2' K2 C2)
have "L2 = L"
using step_hyps1 step_hyps2
using linorder_lit.Uniq_is_maximal_in_mset[of E, THEN Uniq_D] by metis
have "D2 = D"
using step_hyps1 step_hyps2
unfolding ‹L2 = L›
by (metis option.inject)
have "K2 = K"
using step_hyps1 step_hyps2
unfolding ‹D2 = D›
using linorder_lit.Uniq_is_maximal_in_mset[of "eres D E", THEN Uniq_D] by metis
have "U⇩e⇩r2' = U⇩e⇩r'"
using step_hyps1 step_hyps2
unfolding ‹D2 = D›
by argo
have "Γ2' = Γ'"
using step_hyps1 step_hyps2
unfolding ‹K2 = K›
by argo
have "C2 = C"
using step_hyps1 step_hyps2
unfolding ‹K2 = K›
by (metis option.inject)
show ?thesis
unfolding step_hyps1(2) step_hyps2(1)
unfolding ‹U⇩e⇩r2' = U⇩e⇩r'› ‹Γ2' = Γ'› ‹C2 = C› ..
qed
qed
qed
inductive ord_res_7_final where
model_found:
"ord_res_7_final (N, U⇩e⇩r, ℱ, Γ, None)" |
contradiction_found:
"ord_res_7_final (N, U⇩e⇩r, ℱ, Γ, Some {#})"
sublocale ord_res_7_semantics: semantics where
step = "constant_context ord_res_7" and
final = ord_res_7_final
proof unfold_locales
fix S :: "'f gclause fset ×'f gclause fset × 'f gclause fset ×
('f gterm literal × 'f gterm literal multiset option) list ×
'f gterm literal multiset option"
obtain
N U⇩e⇩r ℱ :: "'f gterm clause fset" and
Γ :: "('f gterm literal × 'f gterm literal multiset option) list" and
𝒞 :: "'f gclause option"
where
S_def: "S = (N, U⇩e⇩r, ℱ, Γ, 𝒞)"
by (metis prod.exhaust)
assume "ord_res_7_final S"
hence "∄x. ord_res_7 N (U⇩e⇩r, ℱ, Γ, 𝒞) x"
unfolding S_def
proof (cases "(N, U⇩e⇩r, ℱ, Γ, 𝒞)" rule: ord_res_7_final.cases)
case model_found
thus ?thesis
by (auto elim: ord_res_7.cases)
next
case contradiction_found
thus ?thesis
by (auto simp: linorder_lit.is_maximal_in_mset_iff elim: ord_res_7.cases)
qed
thus "finished (constant_context ord_res_7) S"
by (simp add: S_def finished_def constant_context.simps)
qed
inductive ord_res_7_invars for N where
"ord_res_7_invars N (U⇩e⇩r, ℱ, Γ, 𝒞)" if
"ℱ |⊆| N |∪| U⇩e⇩r" and
"(∀C. 𝒞 = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r))" and
"(∀D. 𝒞 = Some D ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀L⇩C. linorder_lit.is_maximal_in_mset C L⇩C ⟶
¬ trail_defined_lit Γ L⇩C ⟶ (trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))))" and
"(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. 𝒞 = Some D ⟶ C ≺⇩c D) ⟶ trail_true_cls Γ C)" and
"(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. 𝒞 = Some D ⟶ C ≺⇩c D) ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ)))" and
"sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
"linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
"(𝒞 = None ⟶ trail_atms Γ = atms_of_clss (N |∪| U⇩e⇩r))" and
"(∀C. 𝒞 = Some C ⟶
(∀A |∈| trail_atms Γ. ∃L. linorder_lit.is_maximal_in_mset C L ∧ A ≼⇩t atm_of L))" and
"(∀Ln ∈ set Γ. is_neg (fst Ln) ⟷ snd Ln = None)" and
"(∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C))" and
"(∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln))" and
"(∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r))" and
"(∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#})" and
"(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
lemma clause_almost_defined_if_lt_next_clause:
assumes "ord_res_7_invars N (U⇩e⇩r, ℱ, Γ, 𝒞)"
shows "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. 𝒞 = Some D ⟶ C ≺⇩c D) ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶ trail_defined_cls Γ {#L ∈# C. L ≠ K#})"
proof (intro ballI impI allI)
fix C :: "'f gclause" and K :: "'f gliteral"
assume
C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
C_lt: "∀D. 𝒞 = Some D ⟶ C ≺⇩c D" and
C_max_lit: "ord_res.is_maximal_lit K C"
show "trail_defined_cls Γ {#L ∈# C. L ≠ K#}"
using assms
proof (cases N "(U⇩e⇩r, ℱ, Γ, 𝒞)" rule: ord_res_7_invars.cases)
case invars: 1
have "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ)"
using invars C_in C_lt C_max_lit by metis
hence C_almost_almost_defined: "trail_defined_cls Γ {#L ∈# C. L ≠ K ∧ L ≠ - K#}"
using clause_almost_almost_definedI[OF C_in C_max_lit] by blast
show ?thesis
proof (cases "trail_defined_lit Γ K")
case True
hence "trail_defined_lit Γ (- K)"
unfolding trail_defined_lit_def uminus_of_uminus_id by argo
then show ?thesis
using C_almost_almost_defined
unfolding trail_defined_cls_def
by auto
next
case False
show ?thesis
proof (cases 𝒞)
case None
hence "trail_atms Γ = atms_of_clss (N |∪| U⇩e⇩r)"
using invars by argo
then show ?thesis
by (metis C_in C_max_lit False atm_of_in_atms_of_clssI linorder_lit.is_maximal_in_mset_iff
trail_defined_lit_iff_trail_defined_atm)
next
case (Some D)
hence "C ≺⇩c D"
using C_lt by simp
then show ?thesis
using invars
by (smt (verit, ccfv_SIG) C_almost_almost_defined C_in C_max_lit False Some
‹¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ)›
atm_of_in_atms_of_clssI atm_of_uminus filter_mset_cong0
linorder_lit.is_greatest_in_set_iff linorder_lit.is_maximal_in_mset_iff
linorder_lit.is_maximal_in_set_eq_is_greatest_in_set
linorder_lit.is_maximal_in_set_iff literal.collapse(1) literal.exhaust_sel
ord_res.less_lit_simps(4) trail_defined_lit_iff_trail_defined_atm)
qed
qed
qed
qed
lemma ord_res_7_invars_def:
"ord_res_7_invars N s ⟷
(∀U⇩e⇩r ℱ Γ 𝒞. s = (U⇩e⇩r, ℱ, Γ, 𝒞) ⟶
ℱ |⊆| N |∪| U⇩e⇩r ∧
(∀C. 𝒞 = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)) ∧
(∀D. 𝒞 = Some D ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀L⇩C. linorder_lit.is_maximal_in_mset C L⇩C ⟶
¬ trail_defined_lit Γ L⇩C ⟶ (trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C)))) ∧
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. 𝒞 = Some D ⟶ C ≺⇩c D) ⟶ trail_true_cls Γ C) ∧
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. 𝒞 = Some D ⟶ C ≺⇩c D) ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))) ∧
sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ ∧
linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r)) ∧
(𝒞 = None ⟶ trail_atms Γ = atms_of_clss (N |∪| U⇩e⇩r)) ∧
(∀C. 𝒞 = Some C ⟶
(∀A |∈| trail_atms Γ. ∃L. linorder_lit.is_maximal_in_mset C L ∧ A ≼⇩t atm_of L)) ∧
(∀Ln ∈ set Γ. is_neg (fst Ln) ⟷ snd Ln = None) ∧
(∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)) ∧
(∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)) ∧
(∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)) ∧
(∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}) ∧
(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C)))"
(is "?NICE N s ⟷ ?UGLY N s")
proof (rule iffI)
show "?NICE N s ⟹ ?UGLY N s"
apply (intro allI impI)
subgoal premises prems for U⇩e⇩r ℱ Γ 𝒞
using prems(1) unfolding prems(2)
by (cases N "(U⇩e⇩r, ℱ, Γ, 𝒞)" rule: ord_res_7_invars.cases) (simp only:)
done
next
assume "?UGLY N s"
obtain U⇩e⇩r ℱ Γ 𝒞 where s_def: "s = (U⇩e⇩r, ℱ, Γ, 𝒞)"
by (metis prod.exhaust)
show "?NICE N s"
using ‹?UGLY N s›[rule_format, OF s_def]
unfolding s_def
by (intro ord_res_7_invars.intros) simp_all
qed
lemma ord_res_7_invars_implies_trail_consistent:
assumes "ord_res_7_invars N (U⇩e⇩r, ℱ, Γ, 𝒞)"
shows "trail_consistent Γ"
using assms unfolding ord_res_7_invars_def
by (metis trail_consistent_if_sorted_wrt_atoms)
lemma ord_res_7_invars_implies_propagated_clause_almost_false:
assumes invars: "ord_res_7_invars N (U⇩e⇩r, ℱ, Γ, 𝒞)" and "(L, Some C) ∈ set Γ"
shows "trail_false_cls Γ {#K ∈# C. K ≠ L#}"
proof -
obtain Γ⇩1 Γ⇩0 where Γ_eq: "Γ = Γ⇩1 @ (L, Some C) # Γ⇩0"
using ‹(L, Some C) ∈ set Γ› by (metis split_list)
hence "trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
using invars by (simp_all add: ord_res_7_invars_def)
moreover have "suffix Γ⇩0 Γ"
using Γ_eq by (simp add: suffix_def)
ultimately show ?thesis
by (metis trail_false_cls_if_trail_false_suffix)
qed
lemma ord_res_7_preserves_invars:
assumes step: "ord_res_7 N s s'" and invar: "ord_res_7_invars N s"
shows "ord_res_7_invars N s'"
using step
proof (cases N s s' rule: ord_res_7.cases)
case step_hyps: (decide_neg Γ D L U⇩e⇩r A Γ' ℱ)
note D_max_lit = ‹ord_res.is_maximal_lit L D›
have
"A |∈| atms_of_clss (N |∪| U⇩e⇩r)" and
"A ≺⇩t atm_of L" and
"A |∉| trail_atms Γ"
using step_hyps unfolding atomize_conj linorder_trm.is_least_in_ffilter_iff by argo
have "suffix Γ Γ'"
using step_hyps unfolding suffix_def by simp
have
ℱ_subset: "ℱ |⊆| N |∪| U⇩e⇩r" and
D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
clauses_lt_D_seldomly_have_undef_max_lit:
"∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀L⇩C. linorder_lit.is_maximal_in_mset C L⇩C ⟶
¬ trail_defined_lit Γ L⇩C ⟶ (trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))" and
clauses_lt_D_true: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ C" and
no_undef_atm_lt_max_lit_if_lt_D: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))" and
Γ_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
Γ_lower: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
trail_atms_le0: "∀A |∈| trail_atms Γ. ∃L. ord_res.is_maximal_lit L D ∧ (A ≼⇩t atm_of L)" and
Γ_deci_iff_neg: "∀Ln ∈ set Γ. snd Ln = None ⟷ is_neg (fst Ln)" and
Γ_deci_ball_lt_true: "∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)" and
Γ_prop_in: "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
Γ_prop_greatest:
"∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)" and
Γ_prop_almost_false:
"∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}" and
Γ_prop_ball_lt_true: "(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
using invar by (simp_all add: ‹s = (U⇩e⇩r, ℱ, Γ, Some D)› ord_res_7_invars_def)
have trail_atms_le: "∀A |∈| trail_atms Γ. A ≼⇩t atm_of L"
using trail_atms_le0 ‹ord_res.is_maximal_lit L D›
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
have clauses_lt_D_almost_defined: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶ trail_defined_cls Γ {#L ∈# C. L ≠ K#})"
using invar[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, Some D)›] clause_almost_defined_if_lt_next_clause
by simp
have "ℱ |⊆| N |∪| U⇩e⇩r"
using ℱ_subset .
moreover have "∀C'. Some D = Some C' ⟶ C' |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using D_in by simp
moreover have "trail_true_cls Γ' {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
if "Some D = Some E" and
C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
C_lt: "C ≺⇩c E" and
C_max_lit: "linorder_lit.is_maximal_in_mset C L⇩C" and
L⇩C_undef: "¬ trail_defined_lit Γ' L⇩C"
for E C L⇩C
proof -
have "E = D"
using that by simp
hence "C ≺⇩c D"
using C_lt by argo
moreover have "¬ trail_defined_lit Γ L⇩C"
using L⇩C_undef ‹suffix Γ Γ'›
using trail_defined_lit_if_trail_defined_suffix by blast
ultimately have "trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
using clauses_lt_D_seldomly_have_undef_max_lit[rule_format, OF C_in _ C_max_lit] by metis
thus ?thesis
using ‹suffix Γ Γ'› trail_true_cls_if_trail_true_suffix by blast
qed
moreover have
"trail_true_cls Γ' C"
"⋀K. linorder_lit.is_maximal_in_mset C K ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ')"
if C_lt: "⋀D'. Some D = Some D' ⟹ C ≺⇩c D'" and "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" for C
proof -
have "C ≺⇩c D"
using C_lt by metis
hence "trail_true_cls Γ C"
using clauses_lt_D_true ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› by metis
thus "trail_true_cls Γ' C"
using ‹suffix Γ Γ'›
by (metis trail_true_cls_if_trail_true_suffix)
fix K
assume C_max_lit: "linorder_lit.is_maximal_in_mset C K"
have "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ)"
using no_undef_atm_lt_max_lit_if_lt_D
using ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹C ≺⇩c D› C_max_lit by metis
thus "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ')"
using step_hyps(6) by auto
qed
moreover have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
proof -
have "∀x |∈| trail_atms Γ. x ≺⇩t A"
using step_hyps(5)[unfolded linorder_trm.is_least_in_ffilter_iff, simplified]
by (metis Γ_lower linorder_trm.antisym_conv3 linorder_trm.is_lower_set_iff)
hence "∀x∈set Γ. atm_of (fst x) ≺⇩t A"
by (simp add: fset_trail_atms)
thus ?thesis
using Γ_sorted by (simp add: ‹Γ' = (Neg A, None) # Γ›)
qed
moreover have "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r))"
proof -
have "linorder_trm.is_lower_set (insert A (fset (trail_atms Γ)))
(fset (atms_of_clss (N |∪| U⇩e⇩r)))"
proof (rule linorder_trm.is_lower_set_insertI)
show "A |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using step_hyps(5)[unfolded linorder_trm.is_least_in_ffilter_iff, simplified]
by argo
next
show "∀w|∈|atms_of_clss (N |∪| U⇩e⇩r). w ≺⇩t A ⟶ w |∈| trail_atms Γ"
using step_hyps(5)[unfolded linorder_trm.is_least_in_ffilter_iff, simplified]
by fastforce
next
show "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
using Γ_lower .
qed
moreover have "trail_atms Γ' = finsert A (trail_atms Γ)"
by (simp add: ‹Γ' = (Neg A, None) # Γ›)
ultimately show ?thesis
by simp
qed
moreover have "∀A |∈| trail_atms Γ'. ∃L. ord_res.is_maximal_lit L D ∧ (A ≼⇩t atm_of L)"
proof (intro ballI exI conjI)
show "ord_res.is_maximal_lit L D"
using ‹ord_res.is_maximal_lit L D› .
next
fix x assume "x |∈| trail_atms Γ'"
hence "x = A ∨ x |∈| trail_atms Γ"
unfolding ‹Γ' = (Neg A, None) # Γ› by simp
thus "x ≼⇩t atm_of L"
proof (elim disjE)
assume "x = A"
thus "x ≼⇩t atm_of L"
using step_hyps(5) by (simp add: linorder_trm.is_least_in_ffilter_iff)
next
assume "x |∈| trail_atms Γ"
thus "x ≼⇩t atm_of L"
using trail_atms_le by metis
qed
qed
moreover have "∀Ln ∈ set Γ'. snd Ln = None ⟷ is_neg (fst Ln)"
unfolding ‹Γ' = (Neg A, None) # Γ›
using Γ_deci_iff_neg by simp
moreover have "trail_true_cls Γ' C"
if "Ln ∈ set Γ'" and "snd Ln = None" and "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "C ≺⇩c {#fst Ln#}"
for Ln C
proof -
have "Ln = (Neg A, None) ∨ Ln ∈ set Γ"
using ‹Ln ∈ set Γ'› unfolding ‹Γ' = (Neg A, None) # Γ› by simp
hence "trail_true_cls Γ C"
proof (elim disjE)
assume "Ln = (Neg A, None)"
hence "fst Ln ≺⇩l L"
by (metis ‹A ≺⇩t atm_of L› fst_conv literal.exhaust_sel ord_res.less_lit_simps(3)
ord_res.less_lit_simps(4))
moreover have "linorder_lit.is_maximal_in_mset {#fst Ln#} (fst Ln)"
unfolding linorder_lit.is_maximal_in_mset_iff by simp
ultimately have "{#fst Ln#} ≺⇩c D"
using D_max_lit
using linorder_lit.multp_if_maximal_less_that_maximal by metis
hence "C ≺⇩c D"
using ‹C ≺⇩c {#fst Ln#}› by order
thus "trail_true_cls Γ C"
using ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)›
using clauses_lt_D_true by blast
next
assume "Ln ∈ set Γ"
thus "trail_true_cls Γ C"
using Γ_deci_ball_lt_true ‹snd Ln = None› ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹C ≺⇩c {#fst Ln#}›
by metis
qed
thus "trail_true_cls Γ' C"
using ‹suffix Γ Γ'› by (metis trail_true_cls_if_trail_true_suffix)
qed
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
unfolding ‹Γ' = (Neg A, None) # Γ› using Γ_prop_in by simp
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)"
unfolding ‹Γ' = (Neg A, None) # Γ› using Γ_prop_greatest by simp
moreover have "∀Γ⇩1 L C Γ⇩0. Γ' = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
unfolding ‹Γ' = (Neg A, None) # Γ› using Γ_prop_almost_false
by (metis (no_types, lifting) append_eq_Cons_conv list.inject option.discI prod.inject)
moreover have "(∀Γ⇩1 L D Γ⇩0. Γ' = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
using Γ_prop_ball_lt_true
unfolding ‹Γ' = (Neg A, None) # Γ›
by (smt (verit, best) append_eq_Cons_conv list.inject option.discI snd_conv)
ultimately show ?thesis
by (auto simp add: ‹s' = (U⇩e⇩r, ℱ, Γ', Some D)› ord_res_7_invars_def)
next
case step_hyps: (skip_defined Γ D K U⇩e⇩r 𝒞' ℱ)
note D_max_lit = ‹ord_res.is_maximal_lit K D›
have
ℱ_subset: "ℱ |⊆| N |∪| U⇩e⇩r" and
D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
clauses_lt_D_seldomly_have_undef_max_lit:
"∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀L⇩C. linorder_lit.is_maximal_in_mset C L⇩C ⟶
¬ trail_defined_lit Γ L⇩C ⟶ (trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))" and
clauses_lt_D_true: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ C" and
no_undef_atm_lt_max_lit_if_lt_D: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))" and
Γ_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
Γ_lower: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
trail_atms_le0: "∀A |∈| trail_atms Γ. ∃L. ord_res.is_maximal_lit L D ∧ (A ≼⇩t atm_of L)" and
Γ_deci_iff_neg: "∀Ln ∈ set Γ. snd Ln = None ⟷ is_neg (fst Ln)" and
Γ_deci_ball_lt_true: "∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)" and
Γ_prop_in: "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
Γ_prop_greatest:
"∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)" and
Γ_prop_almost_false:
"∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}" and
Γ_prop_ball_lt_true: "(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
using invar by (simp_all add: ‹s = (U⇩e⇩r, ℱ, Γ, Some D)› ord_res_7_invars_def)
have clauses_lt_D_almost_defined: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶ trail_defined_cls Γ {#L ∈# C. L ≠ K#})"
using invar[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, Some D)›] clause_almost_defined_if_lt_next_clause
by simp
have Γ_consistent: "trail_consistent Γ"
using trail_consistent_if_sorted_wrt_atoms Γ_sorted by metis
have "K ∈# D" and lit_in_D_le_K: "⋀L. L ∈# D ⟹ L ≼⇩l K"
using ‹ord_res.is_maximal_lit K D›
unfolding atomize_imp atomize_all atomize_conj linorder_lit.is_maximal_in_mset_iff
using linorder_lit.leI by blast
hence "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using D_in atm_of_in_atms_of_clssI by metis
have trail_atms_le: "∀A |∈| trail_atms Γ. A ≼⇩t atm_of K"
using trail_atms_le0 ‹ord_res.is_maximal_lit K D›
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
have "trail_defined_cls Γ {#Ka ∈# D. Ka ≠ K#}"
using step_hyps(4,5,6) D_in by (metis clause_almost_definedI)
show ?thesis
unfolding ‹s' = (U⇩e⇩r, ℱ, Γ, 𝒞')›
proof (intro ord_res_7_invars.intros)
show "ℱ |⊆| N |∪| U⇩e⇩r"
using ℱ_subset .
show "∀C'. 𝒞' = Some C' ⟶ C' |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using step_hyps(7) by (metis linorder_cls.is_least_in_ffilter_iff Some_eq_The_optionalD)
have "trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
if "𝒞' = Some E" and
C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
C_lt: "C ≺⇩c E" and
C_max_lit: "linorder_lit.is_maximal_in_mset C L⇩C" and
L⇩C_undef: "¬ trail_defined_lit Γ L⇩C"
for E C L⇩C
proof -
have "linorder_cls.is_least_in_fset (ffilter ((≺⇩c) D) (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
using ‹𝒞' = Some E› step_hyps by (metis Some_eq_The_optionalD)
hence "C ≺⇩c D ∨ C = D"
unfolding linorder_cls.is_least_in_ffilter_iff
using C_lt by (metis C_in linorder_cls.not_less_iff_gr_or_eq)
thus ?thesis
proof (elim disjE)
assume "C ≺⇩c D"
thus ?thesis
using clauses_lt_D_seldomly_have_undef_max_lit[rule_format, OF C_in _ C_max_lit L⇩C_undef]
by argo
next
assume "C = D"
hence "L⇩C = K"
using C_max_lit D_max_lit
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
hence False
using L⇩C_undef ‹trail_defined_lit Γ K› by argo
thus ?thesis ..
qed
qed
thus "∀D. 𝒞' = Some D ⟶ (∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀L⇩C. ord_res.is_maximal_lit L⇩C C ⟶ ¬ trail_defined_lit Γ L⇩C ⟶
trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))"
by metis
have
"trail_true_cls Γ C"
"⋀K. linorder_lit.is_maximal_in_mset C K ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ)"
if C_lt: "⋀E. 𝒞' = Some E ⟹ C ≺⇩c E" and C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" for C
proof -
have "C ≼⇩c D"
using step_hyps that by (metis clause_le_if_lt_least_greater)
hence "C ≺⇩c D ∨ C = D"
by simp
thus "trail_true_cls Γ C"
proof (elim disjE)
assume "C ≺⇩c D"
thus "trail_true_cls Γ C"
using clauses_lt_D_true ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› by metis
next
assume "C = D"
have "trail_defined_cls Γ D"
using ‹trail_defined_lit Γ K› ‹trail_defined_cls Γ {#Ka ∈# D. Ka ≠ K#}›
unfolding trail_defined_cls_def by auto
hence "trail_true_cls Γ D"
using Γ_consistent ‹¬ trail_false_cls Γ D›
by (metis trail_true_or_false_cls_if_defined)
thus "trail_true_cls Γ C"
using ‹C = D› by simp
qed
fix K⇩c
assume C_max_lit: "linorder_lit.is_maximal_in_mset C K⇩c"
thus "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩c ∧ A |∉| trail_atms Γ)"
using ‹C ≺⇩c D ∨ C = D›
proof (elim disjE)
assume "C ≺⇩c D"
thus ?thesis
using no_undef_atm_lt_max_lit_if_lt_D ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› C_max_lit by metis
next
assume "C = D"
thus ?thesis
by (metis C_max_lit D_max_lit Uniq_D linorder_lit.Uniq_is_maximal_in_mset step_hyps(5))
qed
qed
thus
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. 𝒞' = Some D ⟶ C ≺⇩c D) ⟶ trail_true_cls Γ C"
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. 𝒞' = Some D ⟶ C ≺⇩c D) ⟶
(∀K. ord_res.is_maximal_lit K C ⟶
¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))"
unfolding atomize_conj by metis
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
show "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
using Γ_lower .
have "trail_atms Γ = atms_of_clss (N |∪| U⇩e⇩r)" if "𝒞' = None"
proof (intro fsubset_antisym)
show "trail_atms Γ |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
using Γ_lower unfolding linorder_trm.is_lower_set_iff by blast
next
have nbex_gt_D: "¬ (∃E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). D ≺⇩c E)"
using step_hyps ‹𝒞' = None›
by (metis clause_le_if_lt_least_greater linorder_cls.leD option.simps(3))
have "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). atm_of K ≺⇩t A)"
proof (intro notI , elim bexE)
fix A :: "'f gterm"
assume "A |∈| atms_of_clss (N |∪| U⇩e⇩r)" and "atm_of K ≺⇩t A"
hence "A |∈| atms_of_clss (iefac ℱ |`| (N |∪| U⇩e⇩r))"
by simp
then obtain E L where E_in: "E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "L ∈# E" and "A = atm_of L"
unfolding atms_of_clss_def atms_of_cls_def
by (smt (verit, del_insts) fimage_iff fmember_ffUnion_iff fset_fset_mset)
have "K ≺⇩l L"
using ‹atm_of K ≺⇩t A› ‹A = atm_of L›
by (cases K; cases L) simp_all
hence "D ≺⇩c E"
using D_max_lit ‹L ∈# E›
by (metis empty_iff linorder_lit.ex_maximal_in_mset linorder_lit.is_maximal_in_mset_iff
linorder_lit.less_linear linorder_lit.less_trans
linorder_lit.multp_if_maximal_less_that_maximal set_mset_empty)
thus False
using E_in nbex_gt_D by metis
qed
hence "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A |∉| trail_atms Γ)"
using step_hyps(5) step_hyps(6)
by (metis linorder_trm.linorder_cases
trail_defined_lit_iff_trail_defined_atm)
then show "atms_of_clss (N |∪| U⇩e⇩r) |⊆| trail_atms Γ"
by blast
qed
thus "𝒞' = None ⟶ trail_atms Γ = atms_of_clss (N |∪| U⇩e⇩r)"
by metis
show "∀D. 𝒞' = Some D ⟶ (∀A |∈| trail_atms Γ.
∃L. ord_res.is_maximal_lit L D ∧ A ≼⇩t atm_of L)"
proof (intro allI impI ballI)
fix E :: "'f gterm literal multiset" and A :: "'f gterm"
assume "𝒞' = Some E" and "A |∈| trail_atms Γ"
have "linorder_cls.is_least_in_fset (ffilter ((≺⇩c) D) (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
using step_hyps(7) ‹𝒞' = Some E› by (metis Some_eq_The_optionalD)
hence "D ≺⇩c E"
unfolding linorder_cls.is_least_in_ffilter_iff by argo
obtain L where "linorder_lit.is_maximal_in_mset E L"
by (metis ‹D ≺⇩c E› linorder_cls.leD linorder_lit.ex_maximal_in_mset mempty_lesseq_cls)
show "∃L. ord_res.is_maximal_lit L E ∧ A ≼⇩t atm_of L"
proof (intro exI conjI)
show "ord_res.is_maximal_lit L E"
using ‹ord_res.is_maximal_lit L E› .
next
have "K ≼⇩l L"
using step_hyps(4) ‹ord_res.is_maximal_lit L E›
by (metis ‹D ≺⇩c E› linorder_cls.less_asym linorder_lit.leI
linorder_lit.multp_if_maximal_less_that_maximal)
hence "atm_of K ≼⇩t atm_of L"
by (cases K; cases L) simp_all
moreover have "A ≼⇩t atm_of K"
using ‹A |∈| trail_atms Γ› trail_atms_le by blast
ultimately show "A ≼⇩t atm_of L"
by order
qed
qed
show "∀Ln∈set Γ. is_neg (fst Ln) = (snd Ln = None)"
using Γ_deci_iff_neg by metis
show "∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)"
using Γ_deci_ball_lt_true .
show "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using Γ_prop_in by simp
show "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)"
using Γ_prop_greatest by simp
show "∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
using Γ_prop_almost_false .
show "(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
using Γ_prop_ball_lt_true .
qed
next
case step_hyps: (skip_undefined_neg Γ D K U⇩e⇩r Γ' 𝒞' ℱ)
note D_max_lit = ‹ord_res.is_maximal_lit K D›
have "suffix Γ Γ'"
using step_hyps unfolding suffix_def by simp
have
ℱ_subset: "ℱ |⊆| N |∪| U⇩e⇩r" and
D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
clauses_lt_D_seldomly_have_undef_max_lit:
"∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀L⇩C. linorder_lit.is_maximal_in_mset C L⇩C ⟶
¬ trail_defined_lit Γ L⇩C ⟶ (trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))" and
clauses_lt_D_true: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ C" and
no_undef_atm_lt_max_lit_if_lt_D: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))" and
Γ_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
Γ_lower: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
trail_atms_le0: "∀A |∈| trail_atms Γ. ∃L. ord_res.is_maximal_lit L D ∧ (A ≼⇩t atm_of L)" and
Γ_deci_iff_neg: "∀Ln ∈ set Γ. snd Ln = None ⟷ is_neg (fst Ln)" and
Γ_deci_ball_lt_true: "∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)" and
Γ_prop_in: "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
Γ_prop_greatest:
"∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)" and
Γ_prop_almost_false:
"∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}" and
Γ_prop_ball_lt_true: "(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
using invar by (simp_all add: ‹s = (U⇩e⇩r, ℱ, Γ, Some D)› ord_res_7_invars_def)
have clauses_lt_D_almost_defined: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶ trail_defined_cls Γ {#L ∈# C. L ≠ K#})"
using invar[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, Some D)›] clause_almost_defined_if_lt_next_clause
by simp
have Γ_consistent: "trail_consistent Γ"
using trail_consistent_if_sorted_wrt_atoms Γ_sorted by metis
have "K ∈# D"
using ‹ord_res.is_maximal_lit K D›
unfolding linorder_lit.is_maximal_in_mset_iff by argo
hence "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using D_in atm_of_in_atms_of_clssI by metis
have trail_atms_le: "∀A |∈| trail_atms Γ. A ≼⇩t atm_of K"
using trail_atms_le0 ‹ord_res.is_maximal_lit K D›
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
have "ℱ |⊆| N |∪| U⇩e⇩r"
using ℱ_subset .
moreover have "∀C'. 𝒞' = Some C' ⟶ C' |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using step_hyps(9) by (metis linorder_cls.is_least_in_ffilter_iff Some_eq_The_optionalD)
moreover have "trail_true_cls Γ' {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
if "𝒞' = Some E" and
C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
C_lt: "C ≺⇩c E" and
C_max_lit: "linorder_lit.is_maximal_in_mset C L⇩C" and
L⇩C_undef: "¬ trail_defined_lit Γ' L⇩C"
for E C L⇩C
proof -
have "linorder_cls.is_least_in_fset (ffilter ((≺⇩c) D) (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
using ‹𝒞' = Some E› step_hyps by (metis Some_eq_The_optionalD)
hence "C ≺⇩c D ∨ C = D"
unfolding linorder_cls.is_least_in_ffilter_iff
using C_lt by (metis C_in linorder_cls.not_less_iff_gr_or_eq)
thus ?thesis
proof (elim disjE)
assume "C ≺⇩c D"
moreover have "¬ trail_defined_lit Γ L⇩C"
using L⇩C_undef ‹suffix Γ Γ'›
using trail_defined_lit_if_trail_defined_suffix by blast
ultimately have "trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
using clauses_lt_D_seldomly_have_undef_max_lit[rule_format, OF C_in _ C_max_lit] by metis
thus ?thesis
using ‹suffix Γ Γ'› trail_true_cls_if_trail_true_suffix by blast
next
assume "C = D"
hence "L⇩C = K"
using C_max_lit D_max_lit
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
moreover have "trail_defined_lit Γ' K"
by (simp add: step_hyps(8) trail_defined_lit_def)
ultimately have False
using L⇩C_undef by argo
thus ?thesis ..
qed
qed
moreover have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
proof -
have "atm_of K |∉| trail_atms Γ"
using ‹¬ trail_defined_lit Γ K›
by (simp add: trail_defined_lit_iff_trail_defined_atm)
have "x ≺⇩t atm_of K" if x_in: "x |∈| trail_atms Γ" for x
proof -
have "x ≼⇩t atm_of K"
using x_in trail_atms_le by metis
moreover have "x ≠ atm_of K"
using x_in ‹atm_of K |∉| trail_atms Γ› by metis
ultimately show ?thesis
by order
qed
hence "∀x∈set Γ. atm_of (fst x) ≺⇩t atm_of K"
by (simp add: fset_trail_atms)
thus ?thesis
using Γ_sorted ‹Γ' = (K, None) # Γ› by simp
qed
moreover have Γ'_lower: "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r))"
proof -
have "linorder_trm.is_lower_set (insert (atm_of K) (fset (trail_atms Γ)))
(fset (atms_of_clss (N |∪| U⇩e⇩r)))"
proof (rule linorder_trm.is_lower_set_insertI)
show "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using ‹atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)› .
next
show "∀w|∈|atms_of_clss (N |∪| U⇩e⇩r). w ≺⇩t (atm_of K) ⟶ w |∈| trail_atms Γ"
using step_hyps(5)[unfolded linorder_trm.is_least_in_ffilter_iff, simplified]
by fastforce
next
show "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
using Γ_lower .
qed
moreover have "trail_atms Γ' = finsert (atm_of K) (trail_atms Γ)"
by (simp add: ‹Γ' = (K, None) # Γ›)
ultimately show ?thesis
by simp
qed
moreover have "trail_atms Γ' = atms_of_clss (N |∪| U⇩e⇩r)" if "𝒞' = None"
proof (intro fsubset_antisym)
show "trail_atms Γ' |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
using Γ'_lower unfolding linorder_trm.is_lower_set_iff by blast
next
have nbex_gt_D: "¬ (∃E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). D ≺⇩c E)"
using step_hyps ‹𝒞' = None›
by (metis clause_le_if_lt_least_greater linorder_cls.leD option.simps(3))
have "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). atm_of K ≺⇩t A)"
proof (intro notI , elim bexE)
fix A :: "'f gterm"
assume "A |∈| atms_of_clss (N |∪| U⇩e⇩r)" and "atm_of K ≺⇩t A"
hence "A |∈| atms_of_clss (iefac ℱ |`| (N |∪| U⇩e⇩r))"
by simp
then obtain E L where E_in: "E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "L ∈# E" and "A = atm_of L"
unfolding atms_of_clss_def atms_of_cls_def
by (smt (verit, del_insts) fimage_iff fmember_ffUnion_iff fset_fset_mset)
have "K ≺⇩l L"
using ‹atm_of K ≺⇩t A› ‹A = atm_of L›
by (cases K; cases L) simp_all
hence "D ≺⇩c E"
using D_max_lit ‹L ∈# E›
by (metis empty_iff linorder_lit.ex_maximal_in_mset linorder_lit.is_maximal_in_mset_iff
linorder_lit.less_linear linorder_lit.less_trans
linorder_lit.multp_if_maximal_less_that_maximal set_mset_empty)
thus False
using E_in nbex_gt_D by metis
qed
hence "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A |∉| trail_atms Γ')"
using step_hyps
by (metis finsert_iff linorder_trm.antisym_conv3 prod.sel(1) trail_atms.simps(2))
then show "atms_of_clss (N |∪| U⇩e⇩r) |⊆| trail_atms Γ'"
by blast
qed
moreover have "∀D. 𝒞' = Some D ⟶ (∀A |∈| trail_atms Γ'.
∃L. ord_res.is_maximal_lit L D ∧ A ≼⇩t atm_of L)"
proof (intro allI impI ballI)
fix E :: "'f gterm literal multiset" and A :: "'f gterm"
assume "𝒞' = Some E" and "A |∈| trail_atms Γ'"
have "linorder_cls.is_least_in_fset (ffilter ((≺⇩c) D) (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
using step_hyps(9) ‹𝒞' = Some E› by (metis Some_eq_The_optionalD)
hence "D ≺⇩c E"
unfolding linorder_cls.is_least_in_ffilter_iff by argo
obtain L where "linorder_lit.is_maximal_in_mset E L"
by (metis ‹D ≺⇩c E› linorder_cls.leD linorder_lit.ex_maximal_in_mset mempty_lesseq_cls)
show "∃L. ord_res.is_maximal_lit L E ∧ A ≼⇩t atm_of L"
proof (intro exI conjI)
show "ord_res.is_maximal_lit L E"
using ‹ord_res.is_maximal_lit L E› .
next
have "K ≼⇩l L"
using step_hyps(4) ‹ord_res.is_maximal_lit L E›
by (metis ‹D ≺⇩c E› linorder_cls.less_asym linorder_lit.leI
linorder_lit.multp_if_maximal_less_that_maximal)
hence "atm_of K ≼⇩t atm_of L"
by (cases K; cases L) simp_all
moreover have "A ≼⇩t atm_of K"
proof -
have "A = atm_of K ∨ A |∈| trail_atms Γ"
using ‹A |∈| trail_atms Γ'›
unfolding ‹Γ' = (K, None) # Γ›
by (metis (mono_tags, lifting) finsertE prod.sel(1) trail_atms.simps(2))
thus "A ≼⇩t atm_of K"
using trail_atms_le by blast
qed
ultimately show "A ≼⇩t atm_of L"
by order
qed
qed
moreover have "∀Ln ∈ set Γ'. snd Ln = None ⟷ is_neg (fst Ln)"
unfolding ‹Γ' = (K, None) # Γ›
using Γ_deci_iff_neg ‹is_neg K› by simp
moreover have "trail_true_cls Γ' C"
if "Ln ∈ set Γ'" and "snd Ln = None" and "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "C ≺⇩c {#fst Ln#}"
for Ln C
proof -
have "Ln = (K, None) ∨ Ln ∈ set Γ"
using ‹Ln ∈ set Γ'› unfolding ‹Γ' = (K, None) # Γ› by simp
hence "trail_true_cls Γ C"
proof (elim disjE)
assume "Ln = (K, None)"
hence "∀x ∈# C. x ≺⇩l K"
using ‹C ≺⇩c {#fst Ln#}›
unfolding multp_singleton_right[OF linorder_lit.transp_on_less]
by simp
hence "C ≺⇩c D"
using D_max_lit
by (metis ‹K ∈# D› empty_iff ord_res.multp_if_all_left_smaller set_mset_empty)
thus "trail_true_cls Γ C"
using ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)›
using clauses_lt_D_true by blast
next
assume "Ln ∈ set Γ"
thus "trail_true_cls Γ C"
using Γ_deci_ball_lt_true ‹snd Ln = None› ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹C ≺⇩c {#fst Ln#}›
by metis
qed
thus "trail_true_cls Γ' C"
using ‹suffix Γ Γ'› by (metis trail_true_cls_if_trail_true_suffix)
qed
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using Γ_prop_in ‹Γ' = (K, None) # Γ› by simp
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)"
using Γ_prop_greatest ‹Γ' = (K, None) # Γ› by simp
moreover have "∀Γ⇩1 L C Γ⇩0. Γ' = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
unfolding ‹Γ' = (K, None) # Γ› using Γ_prop_almost_false
by (metis (no_types, lifting) append_eq_Cons_conv list.inject option.discI prod.inject)
moreover have "(∀Γ⇩1 L D Γ⇩0. Γ' = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
unfolding ‹Γ' = (K, None) # Γ› using Γ_prop_ball_lt_true
by (smt (verit, ccfv_SIG) append_eq_Cons_conv list.inject option.discI prod.inject)
ultimately show ?thesis
unfolding ‹s' = (U⇩e⇩r, ℱ, Γ', 𝒞')›
proof (intro ord_res_7_invars.intros)
have "trail_true_cls Γ' C"
"⋀K⇩C. linorder_lit.is_maximal_in_mset C K⇩C ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ')"
if C_lt: "⋀E. 𝒞' = Some E ⟶ C ≺⇩c E" and C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" for C
proof -
have "C ≼⇩c D"
using step_hyps that by (metis clause_le_if_lt_least_greater)
hence "C ≺⇩c D ∨ C = D"
by simp
thus "trail_true_cls Γ' C"
proof (elim disjE)
assume "C ≺⇩c D"
hence "trail_true_cls Γ C"
using clauses_lt_D_true ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› by metis
thus "trail_true_cls Γ' C"
using ‹suffix Γ Γ'› by (metis trail_true_cls_if_trail_true_suffix)
next
assume "C = D"
have "trail_true_lit Γ' K"
unfolding ‹Γ' = (K, None) # Γ› trail_true_lit_def by simp
thus "trail_true_cls Γ' C"
unfolding ‹C = D› trail_true_cls_def
using ‹K ∈# D› by metis
qed
fix K⇩C
assume C_max_lit: "linorder_lit.is_maximal_in_mset C K⇩C"
show "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ')"
using ‹C ≺⇩c D ∨ C = D›
proof (elim disjE)
assume "C ≺⇩c D"
hence "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ)"
using no_undef_atm_lt_max_lit_if_lt_D ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› C_max_lit by metis
thus "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ')"
by (metis finsert_iff step_hyps(8) trail_atms.simps(2))
next
assume "C = D"
thus "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ')"
by (metis (mono_tags, lifting) C_max_lit D_max_lit Uniq_D Γ'_lower finsert_iff
linorder_lit.Uniq_is_maximal_in_mset linorder_trm.not_in_lower_setI prod.sel(1)
step_hyps(8) trail_atms.simps(2))
qed
qed
thus
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. 𝒞' = Some D ⟶ C ≺⇩c D) ⟶ trail_true_cls Γ' C"
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. 𝒞' = Some D ⟶ C ≺⇩c D) ⟶
(∀K. ord_res.is_maximal_lit K C ⟶
¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ'))"
unfolding atomize_conj by metis
qed simp_all
next
case step_hyps: (skip_undefined_pos Γ D K U⇩e⇩r ℱ E)
note D_max_lit = ‹ord_res.is_maximal_lit K D›
note E_least = ‹linorder_cls.is_least_in_fset (ffilter ((≺⇩c) D) (iefac ℱ |`| (N |∪| U⇩e⇩r))) E›
have "D ≺⇩c E"
using E_least unfolding linorder_cls.is_least_in_ffilter_iff by argo
have
ℱ_subset: "ℱ |⊆| N |∪| U⇩e⇩r" and
D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
clauses_lt_D_seldomly_have_undef_max_lit:
"∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀L⇩C. linorder_lit.is_maximal_in_mset C L⇩C ⟶
¬ trail_defined_lit Γ L⇩C ⟶ (trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))" and
clauses_lt_D_true: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ C" and
no_undef_atm_lt_max_lit_if_lt_D: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))" and
Γ_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
Γ_lower: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
trail_atms_le0: "∀A |∈| trail_atms Γ. ∃L. ord_res.is_maximal_lit L D ∧ (A ≼⇩t atm_of L)" and
Γ_deci_iff_neg: "∀Ln ∈ set Γ. snd Ln = None ⟷ is_neg (fst Ln)" and
Γ_deci_ball_lt_true: "∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)" and
Γ_prop_in: "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
Γ_prop_greatest:
"∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)" and
Γ_prop_almost_false:
"∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}" and
Γ_prop_ball_lt_true: "(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
using invar by (simp_all add: ‹s = (U⇩e⇩r, ℱ, Γ, Some D)› ord_res_7_invars_def)
have clauses_lt_D_almost_defined: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶ trail_defined_cls Γ {#L ∈# C. L ≠ K#})"
using invar[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, Some D)›] clause_almost_defined_if_lt_next_clause
by simp
have Γ_consistent: "trail_consistent Γ"
using trail_consistent_if_sorted_wrt_atoms Γ_sorted by metis
have "K ∈# D"
using ‹ord_res.is_maximal_lit K D›
unfolding linorder_lit.is_maximal_in_mset_iff by argo
hence "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using D_in atm_of_in_atms_of_clssI by metis
have "trail_defined_cls Γ {#L ∈# D. L ≠ K ∧ L ≠ - K#}"
using clause_almost_almost_definedI[OF D_in step_hyps(4,5)] .
moreover have "- K ∉# D"
using ‹is_pos K› D_max_lit
by (metis (no_types, opaque_lifting) is_pos_def linorder_lit.antisym_conv3
linorder_lit.is_maximal_in_mset_iff linorder_trm.less_imp_not_eq ord_res.less_lit_simps(4)
uminus_Pos uminus_not_id)
ultimately have D_almost_defined: "trail_defined_cls Γ {#L ∈# D. L ≠ K#}"
unfolding trail_defined_cls_def by auto
hence "trail_true_cls Γ {#L ∈# D. L ≠ K#}"
using ‹¬ trail_false_cls Γ {#L ∈# D. L ≠ K#}›
using trail_true_or_false_cls_if_defined by metis
hence D_true: "trail_true_cls Γ D"
unfolding trail_true_cls_def by auto
have trail_atms_le: "∀A |∈| trail_atms Γ. A ≼⇩t atm_of K"
using trail_atms_le0 D_max_lit
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
obtain L where E_max_lit: "linorder_lit.is_maximal_in_mset E L"
by (metis ‹D ≺⇩c E› linorder_cls.leD linorder_lit.ex_maximal_in_mset mempty_lesseq_cls)
have "ℱ |⊆| N |∪| U⇩e⇩r"
using ℱ_subset .
moreover have "∀C'. Some E = Some C' ⟶ C' |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using step_hyps unfolding linorder_cls.is_least_in_ffilter_iff by simp
moreover have "trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
if "Some E = Some E'" and
C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
C_lt: "C ≺⇩c E'" and
C_max_lit: "linorder_lit.is_maximal_in_mset C L⇩C" and
L⇩C_undef: "¬ trail_defined_lit Γ L⇩C"
for E' C L⇩C
proof -
have "E' = E"
using that by simp
hence "linorder_cls.is_least_in_fset (ffilter ((≺⇩c) D) (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
using step_hyps by metis
hence "C ≺⇩c D ∨ C = D"
unfolding linorder_cls.is_least_in_ffilter_iff
using C_lt ‹E' = E› by (metis C_in linorder_cls.not_less_iff_gr_or_eq)
thus ?thesis
proof (elim disjE)
assume "C ≺⇩c D"
thus "trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
using clauses_lt_D_seldomly_have_undef_max_lit[rule_format, OF C_in _ C_max_lit L⇩C_undef]
by metis
next
assume "C = D"
hence "L⇩C = K"
using C_max_lit D_max_lit
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
thus ?thesis
using ‹C = D› ‹trail_true_cls Γ {#L ∈# D. L ≠ K#}› ‹is_pos K› by metis
qed
qed
moreover have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
moreover have "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
using Γ_lower .
moreover have "∀D. Some E = Some D ⟶ (∀A |∈| trail_atms Γ.
∃L. ord_res.is_maximal_lit L D ∧ A ≼⇩t atm_of L)"
proof -
have "∀A |∈| trail_atms Γ. ∃L. ord_res.is_maximal_lit L E ∧ A ≼⇩t atm_of L"
proof (intro ballI)
fix A :: "'f gterm"
assume "A |∈| trail_atms Γ"
show "∃L. ord_res.is_maximal_lit L E ∧ A ≼⇩t atm_of L"
proof (intro exI conjI)
show "ord_res.is_maximal_lit L E"
using E_max_lit .
next
have "K ≼⇩l L"
using D_max_lit E_max_lit
by (metis ‹D ≺⇩c E› linorder_cls.less_asym linorder_lit.leI
linorder_lit.multp_if_maximal_less_that_maximal)
hence "atm_of K ≼⇩t atm_of L"
by (cases K; cases L) simp_all
moreover have "A ≼⇩t atm_of K"
using ‹A |∈| trail_atms Γ› trail_atms_le by metis
ultimately show "A ≼⇩t atm_of L"
by order
qed
qed
thus ?thesis
by simp
qed
moreover have "∀Ln ∈ set Γ. snd Ln = None ⟷ is_neg (fst Ln)"
using Γ_deci_iff_neg .
moreover have "∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)"
using Γ_deci_ball_lt_true .
moreover have "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using Γ_prop_in .
moreover have "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)"
using Γ_prop_greatest .
moreover have "∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
using Γ_prop_almost_false .
moreover have "(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
using Γ_prop_ball_lt_true .
ultimately show ?thesis
unfolding ‹s' = (U⇩e⇩r, ℱ, Γ, Some E)›
proof (intro ord_res_7_invars.intros)
have "trail_true_cls Γ C"
"⋀K⇩C. linorder_lit.is_maximal_in_mset C K⇩C ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ)"
if C_lt: "⋀E'. Some E = Some E' ⟹ C ≺⇩c E'" and C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" for C
proof -
have "C ≺⇩c E"
using C_lt by simp
hence "C ≺⇩c D ∨ C = D"
using E_least C_in
by (metis linorder_cls.is_least_in_ffilter_iff linorder_cls.less_imp_triv
linorder_cls.linorder_cases)
thus "trail_true_cls Γ C"
proof (elim disjE)
assume "C ≺⇩c D"
thus "trail_true_cls Γ C"
using clauses_lt_D_true ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› by metis
next
assume "C = D"
thus "trail_true_cls Γ C"
using D_true by argo
qed
fix K⇩C
assume C_max_lit: "linorder_lit.is_maximal_in_mset C K⇩C"
show "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ)"
using ‹C ≺⇩c D ∨ C = D›
proof (elim disjE)
assume "C ≺⇩c D"
thus "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ)"
using no_undef_atm_lt_max_lit_if_lt_D ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› C_max_lit by metis
next
assume "C = D"
thus "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ)"
by (metis C_max_lit D_max_lit Uniq_D linorder_lit.Uniq_is_maximal_in_mset step_hyps(5))
qed
qed
thus
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. Some E = Some D ⟶ C ≺⇩c D) ⟶ trail_true_cls Γ C"
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. Some E = Some D ⟶ C ≺⇩c D) ⟶
(∀K. ord_res.is_maximal_lit K C ⟶
¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))"
unfolding atomize_conj by metis
qed simp_all
next
case step_hyps: (skip_undefined_pos_ultimate Γ D K U⇩e⇩r Γ' ℱ)
note D_max_lit = ‹ord_res.is_maximal_lit K D›
have "suffix Γ Γ'"
using ‹Γ' = (- K, None) # Γ› by (simp add: suffix_def)
have
ℱ_subset: "ℱ |⊆| N |∪| U⇩e⇩r" and
D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
clauses_lt_D_seldomly_have_undef_max_lit:
"∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀L⇩C. linorder_lit.is_maximal_in_mset C L⇩C ⟶
¬ trail_defined_lit Γ L⇩C ⟶ (trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))" and
clauses_lt_D_true: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ C" and
no_undef_atm_lt_max_lit_if_lt_D: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))" and
Γ_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
Γ_lower: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
trail_atms_le0: "∀A |∈| trail_atms Γ. ∃L. ord_res.is_maximal_lit L D ∧ (A ≼⇩t atm_of L)" and
Γ_deci_iff_neg: "∀Ln ∈ set Γ. snd Ln = None ⟷ is_neg (fst Ln)" and
Γ_deci_ball_lt_true: "∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)" and
Γ_prop_in: "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
Γ_prop_greatest:
"∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)" and
Γ_prop_almost_false:
"∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}" and
Γ_prop_ball_lt_true: "(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
using invar by (simp_all add: ‹s = (U⇩e⇩r, ℱ, Γ, Some D)› ord_res_7_invars_def)
have clauses_lt_D_almost_defined: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶ trail_defined_cls Γ {#L ∈# C. L ≠ K#})"
using invar[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, Some D)›] clause_almost_defined_if_lt_next_clause
by simp
have Γ_consistent: "trail_consistent Γ"
using trail_consistent_if_sorted_wrt_atoms Γ_sorted by metis
have "K ∈# D"
using ‹ord_res.is_maximal_lit K D›
unfolding linorder_lit.is_maximal_in_mset_iff by argo
hence "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using D_in atm_of_in_atms_of_clssI by metis
have "trail_defined_cls Γ {#L ∈# D. L ≠ K ∧ L ≠ - K#}"
using clause_almost_almost_definedI[OF D_in step_hyps(4,5)] .
moreover have "- K ∉# D"
using ‹is_pos K› D_max_lit
by (metis (no_types, opaque_lifting) is_pos_def linorder_lit.antisym_conv3
linorder_lit.is_maximal_in_mset_iff linorder_trm.less_imp_not_eq ord_res.less_lit_simps(4)
uminus_Pos uminus_not_id)
ultimately have D_almost_defined: "trail_defined_cls Γ {#L ∈# D. L ≠ K#}"
unfolding trail_defined_cls_def by auto
hence "trail_true_cls Γ {#L ∈# D. L ≠ K#}"
using ‹¬ trail_false_cls Γ {#L ∈# D. L ≠ K#}›
using trail_true_or_false_cls_if_defined by metis
hence D_true: "trail_true_cls Γ D"
unfolding trail_true_cls_def by auto
have trail_atms_le: "∀A |∈| trail_atms Γ. A ≼⇩t atm_of K"
using trail_atms_le0 D_max_lit
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
have "ℱ |⊆| N |∪| U⇩e⇩r"
using ℱ_subset .
moreover have "∀C'. None = Some C' ⟶ C' |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
by simp
moreover have "trail_true_cls Γ' {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
if "None = Some E'" and
C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
C_lt: "C ≺⇩c E'" and
C_max_lit: "linorder_lit.is_maximal_in_mset C L⇩C" and
L⇩C_undef: "¬ trail_defined_lit Γ' L⇩C"
for E' C L⇩C
using that by simp
moreover have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
proof -
have "∀x∈set Γ. atm_of (fst x) ≺⇩t atm_of K"
by (metis image_eqI linorder_trm.less_linear linorder_trm.not_le step_hyps(6) trail_atms_le
trail_defined_lit_def trail_defined_lit_iff_trail_defined_atm)
thus ?thesis
unfolding ‹Γ' = (- K, None) # Γ›
using Γ_sorted by simp
qed
moreover have Γ'_lower: "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r))"
proof -
have "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using ‹atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)› .
moreover have "∀w|∈|atms_of_clss (N |∪| U⇩e⇩r). w ≺⇩t atm_of K ⟶ w |∈| trail_atms Γ"
using step_hyps(5) by blast
ultimately show ?thesis
using Γ_lower by (simp add: ‹Γ' = (- K, None) # Γ› linorder_trm.is_lower_set_insertI)
qed
moreover have "trail_atms Γ' = atms_of_clss (N |∪| U⇩e⇩r)"
proof (intro fsubset_antisym)
show "trail_atms Γ' |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
using Γ'_lower unfolding linorder_trm.is_lower_set_iff by blast
next
have nbex_gt_D: "¬ (∃E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). D ≺⇩c E)"
using step_hyps by argo
have "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). atm_of K ≺⇩t A)"
proof (intro notI , elim bexE)
fix A :: "'f gterm"
assume "A |∈| atms_of_clss (N |∪| U⇩e⇩r)" and "atm_of K ≺⇩t A"
hence "A |∈| atms_of_clss (iefac ℱ |`| (N |∪| U⇩e⇩r))"
by simp
then obtain E L where E_in: "E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "L ∈# E" and "A = atm_of L"
unfolding atms_of_clss_def atms_of_cls_def
by (smt (verit, del_insts) fimage_iff fmember_ffUnion_iff fset_fset_mset)
have "K ≺⇩l L"
using ‹atm_of K ≺⇩t A› ‹A = atm_of L›
by (cases K; cases L) simp_all
hence "D ≺⇩c E"
using D_max_lit ‹L ∈# E›
by (metis empty_iff linorder_lit.ex_maximal_in_mset linorder_lit.is_maximal_in_mset_iff
linorder_lit.less_linear linorder_lit.less_trans
linorder_lit.multp_if_maximal_less_that_maximal set_mset_empty)
thus False
using E_in nbex_gt_D by metis
qed
hence "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A |∉| trail_atms Γ')"
using step_hyps
by (metis atm_of_uminus finsert_iff fst_conv linorder_trm.antisym_conv3 trail_atms.simps(2))
then show "atms_of_clss (N |∪| U⇩e⇩r) |⊆| trail_atms Γ'"
by blast
qed
moreover have "∀D. None = Some D ⟶ (∀A |∈| trail_atms Γ.
∃L. ord_res.is_maximal_lit L D ∧ A ≼⇩t atm_of L)"
by simp
moreover have "∀Ln ∈ set Γ'. snd Ln = None ⟷ is_neg (fst Ln)"
using Γ_deci_iff_neg ‹is_pos K›
by (simp add: ‹Γ' = (- K, None) # Γ› is_pos_neg_not_is_pos)
moreover have "trail_true_cls Γ' C"
if "Ln ∈ set Γ'" and "snd Ln = None" and "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "C ≺⇩c {#fst Ln#}"
for Ln C
proof -
have "Ln = (- K, None) ∨ Ln ∈ set Γ"
using ‹Ln ∈ set Γ'› unfolding ‹Γ' = (- K, None) # Γ› by simp
hence "trail_true_cls Γ C"
proof (elim disjE)
assume "Ln = (- K, None)"
hence "∀x ∈# C. x ≺⇩l - K"
using ‹C ≺⇩c {#fst Ln#}›
unfolding multp_singleton_right[OF linorder_lit.transp_on_less]
by simp
hence "C ≼⇩c D"
using D_max_lit step_hyps
using linorder_cls.leI that(3) by blast
thus "trail_true_cls Γ C"
using ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› D_true
using clauses_lt_D_true by blast
next
assume "Ln ∈ set Γ"
thus "trail_true_cls Γ C"
using Γ_deci_ball_lt_true ‹snd Ln = None› ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹C ≺⇩c {#fst Ln#}›
by metis
qed
thus "trail_true_cls Γ' C"
using ‹suffix Γ Γ'› by (metis trail_true_cls_if_trail_true_suffix)
qed
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using Γ_prop_in by (simp add: ‹Γ' = (- K, None) # Γ›)
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)"
using Γ_prop_greatest by (simp add: ‹Γ' = (- K, None) # Γ›)
moreover have "∀Γ⇩1 L C Γ⇩0. Γ' = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
using Γ_prop_almost_false
unfolding ‹Γ' = (- K, None) # Γ›
by (metis (no_types, lifting) append_eq_Cons_conv list.inject option.discI prod.inject)
moreover have "(∀Γ⇩1 L D Γ⇩0. Γ' = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
using Γ_prop_ball_lt_true
unfolding ‹Γ' = (- K, None) # Γ›
by (metis D_true clauses_lt_D_true linorder_cls.neq_iff list.inject step_hyps(10) suffix_Cons
suffix_def)
ultimately show ?thesis
unfolding ‹s' = (U⇩e⇩r, ℱ, Γ', None)›
proof (intro ord_res_7_invars.intros)
have "trail_true_cls Γ' C"
"⋀K⇩C. linorder_lit.is_maximal_in_mset C K⇩C ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ')"
if C_lt: "⋀E. None = Some E ⟹ C ≺⇩c E" and C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" for C
proof -
have "None = The_optional (linorder_cls.is_least_in_fset
(ffilter ((≺⇩c) D) (iefac ℱ |`| (N |∪| U⇩e⇩r))))"
using step_hyps
by (metis (no_types, opaque_lifting) Some_eq_The_optionalD
linorder_cls.is_least_in_ffilter_iff not_Some_eq)
hence "C ≼⇩c D"
using step_hyps that by (metis clause_le_if_lt_least_greater)
hence "C ≺⇩c D ∨ C = D"
by simp
hence "trail_true_cls Γ C"
proof (elim disjE)
assume "C ≺⇩c D"
thus "trail_true_cls Γ C"
using clauses_lt_D_true ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› by metis
next
assume "C = D"
thus "trail_true_cls Γ C"
using D_true by argo
qed
thus "trail_true_cls Γ' C"
using ‹suffix Γ Γ'› by (metis trail_true_cls_if_trail_true_suffix)
fix K⇩C
assume C_max_lit: "linorder_lit.is_maximal_in_mset C K⇩C"
thus "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ')"
using ‹C ≺⇩c D ∨ C = D›
proof (elim disjE)
assume "C ≺⇩c D"
hence "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ)"
using no_undef_atm_lt_max_lit_if_lt_D C_in C_max_lit by force
thus ?thesis
using step_hyps(9) by force
next
assume "C = D"
thus ?thesis
by (metis C_max_lit D_max_lit finsert_iff linorder_cls.order.irrefl
linorder_lit.antisym_conv3 linorder_lit.multp_if_maximal_less_that_maximal
step_hyps(5) step_hyps(9) trail_atms.simps(2))
qed
qed
thus
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. None = Some D ⟶ C ≺⇩c D) ⟶ trail_true_cls Γ' C"
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. None = Some D ⟶ C ≺⇩c D) ⟶
(∀K. ord_res.is_maximal_lit K C ⟶
¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ'))"
unfolding atomize_conj by metis
qed simp_all
next
case step_hyps: (production Γ D K U⇩e⇩r Γ' 𝒞' ℱ)
note D_max_lit = ‹ord_res.is_maximal_lit K D›
have "suffix Γ Γ'"
using step_hyps by (simp add: suffix_def)
have
ℱ_subset: "ℱ |⊆| N |∪| U⇩e⇩r" and
D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
clauses_lt_D_seldomly_have_undef_max_lit:
"∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀L⇩C. linorder_lit.is_maximal_in_mset C L⇩C ⟶
¬ trail_defined_lit Γ L⇩C ⟶ (trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))" and
clauses_lt_D_true: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ C" and
no_undef_atm_lt_max_lit_if_lt_D: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))" and
Γ_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
Γ_lower: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
trail_atms_le0: "∀A |∈| trail_atms Γ. ∃L. ord_res.is_maximal_lit L D ∧ (A ≼⇩t atm_of L)" and
Γ_deci_iff_neg: "∀Ln ∈ set Γ. snd Ln = None ⟷ is_neg (fst Ln)" and
Γ_deci_ball_lt_true: "∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)" and
Γ_prop_in: "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
Γ_prop_greatest:
"∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)" and
Γ_prop_almost_false:
"∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}" and
Γ_prop_ball_lt_true: "(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
using invar by (simp_all add: ‹s = (U⇩e⇩r, ℱ, Γ, Some D)› ord_res_7_invars_def)
have clauses_lt_D_almost_defined: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶ trail_defined_cls Γ {#L ∈# C. L ≠ K#})"
using invar[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, Some D)›] clause_almost_defined_if_lt_next_clause
by simp
have "K ∈# D"
using ‹ord_res.is_maximal_lit K D›
unfolding linorder_lit.is_maximal_in_mset_iff by argo
hence "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using D_in atm_of_in_atms_of_clssI by metis
have "atm_of K |∉| trail_atms Γ"
using ‹¬ trail_defined_lit Γ K›
by (metis trail_defined_lit_iff_trail_defined_atm)
hence trail_atms_lt: "∀A |∈| trail_atms Γ. A ≺⇩t atm_of K"
using trail_atms_le0 ‹ord_res.is_maximal_lit K D›
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset linorder_trm.antisym_conv1)
have "ℱ |⊆| N |∪| U⇩e⇩r"
using ℱ_subset .
moreover have "∀C'. 𝒞' = Some C' ⟶ C' |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using step_hyps(11) by (metis linorder_cls.is_least_in_ffilter_iff Some_eq_The_optionalD)
moreover have "trail_true_cls Γ' {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
if "𝒞' = Some E" and
C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
C_lt: "C ≺⇩c E" and
C_max_lit: "linorder_lit.is_maximal_in_mset C L⇩C" and
L⇩C_undef: "¬ trail_defined_lit Γ' L⇩C"
for E C L⇩C
proof -
have "linorder_cls.is_least_in_fset (ffilter ((≺⇩c) D) (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
using ‹𝒞' = Some E› step_hyps by (metis Some_eq_The_optionalD)
hence "C ≺⇩c D ∨ C = D"
unfolding linorder_cls.is_least_in_ffilter_iff
using C_lt by (metis C_in linorder_cls.not_less_iff_gr_or_eq)
thus ?thesis
proof (elim disjE)
assume "C ≺⇩c D"
moreover have "¬ trail_defined_lit Γ L⇩C"
using L⇩C_undef ‹suffix Γ Γ'›
using trail_defined_lit_if_trail_defined_suffix by blast
ultimately have "trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
using clauses_lt_D_seldomly_have_undef_max_lit[rule_format, OF C_in _ C_max_lit] by metis
thus ?thesis
using ‹suffix Γ Γ'› trail_true_cls_if_trail_true_suffix by blast
next
assume "C = D"
hence "L⇩C = K"
using C_max_lit D_max_lit
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
moreover have "trail_defined_lit Γ' K"
by (simp add: step_hyps trail_defined_lit_def)
ultimately have False
using L⇩C_undef by argo
thus ?thesis ..
qed
qed
moreover have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
proof -
have "x ≺⇩t atm_of K" if x_in: "x |∈| trail_atms Γ" for x
using x_in trail_atms_lt by metis
hence "∀x∈set Γ. atm_of (fst x) ≺⇩t atm_of K"
by (simp add: fset_trail_atms)
thus ?thesis
using Γ_sorted
by (simp add: ‹Γ' = (K, Some D) # Γ›)
qed
moreover have Γ'_lower: "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r))"
proof -
have "linorder_trm.is_lower_set (insert (atm_of K) (fset (trail_atms Γ)))
(fset (atms_of_clss (N |∪| U⇩e⇩r)))"
proof (rule linorder_trm.is_lower_set_insertI)
show "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using ‹atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)› .
next
show "∀w|∈|atms_of_clss (N |∪| U⇩e⇩r). w ≺⇩t (atm_of K) ⟶ w |∈| trail_atms Γ"
using step_hyps(5)[unfolded linorder_trm.is_least_in_ffilter_iff, simplified]
by fastforce
next
show "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
using Γ_lower .
qed
moreover have "trail_atms Γ' = finsert (atm_of K) (trail_atms Γ)"
by (simp add: ‹Γ' = (K, Some D) # Γ›)
ultimately show ?thesis
by simp
qed
moreover have "trail_atms Γ' = atms_of_clss (N |∪| U⇩e⇩r)" if "𝒞' = None"
proof (intro fsubset_antisym)
show "trail_atms Γ' |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
using Γ'_lower unfolding linorder_trm.is_lower_set_iff by blast
next
have nbex_gt_D: "¬ (∃E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). D ≺⇩c E)"
using step_hyps ‹𝒞' = None›
by (metis clause_le_if_lt_least_greater linorder_cls.leD option.simps(3))
have "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). atm_of K ≺⇩t A)"
proof (intro notI , elim bexE)
fix A :: "'f gterm"
assume "A |∈| atms_of_clss (N |∪| U⇩e⇩r)" and "atm_of K ≺⇩t A"
hence "A |∈| atms_of_clss (iefac ℱ |`| (N |∪| U⇩e⇩r))"
by simp
then obtain E L where E_in: "E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "L ∈# E" and "A = atm_of L"
unfolding atms_of_clss_def atms_of_cls_def
by (smt (verit, del_insts) fimage_iff fmember_ffUnion_iff fset_fset_mset)
have "K ≺⇩l L"
using ‹atm_of K ≺⇩t A› ‹A = atm_of L›
by (cases K; cases L) simp_all
hence "D ≺⇩c E"
using D_max_lit ‹L ∈# E›
by (metis empty_iff linorder_lit.ex_maximal_in_mset linorder_lit.is_maximal_in_mset_iff
linorder_lit.less_linear linorder_lit.less_trans
linorder_lit.multp_if_maximal_less_that_maximal set_mset_empty)
thus False
using E_in nbex_gt_D by metis
qed
hence "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A |∉| trail_atms Γ')"
using step_hyps
by (metis finsert_iff fst_conv linorder_trm.antisym_conv3 trail_atms.simps(2))
then show "atms_of_clss (N |∪| U⇩e⇩r) |⊆| trail_atms Γ'"
by blast
qed
moreover have "∀D. 𝒞' = Some D ⟶ (∀A |∈| trail_atms Γ'.
∃L. ord_res.is_maximal_lit L D ∧ A ≼⇩t atm_of L)"
proof (intro allI impI ballI)
fix E :: "'f gterm literal multiset" and A :: "'f gterm"
assume "𝒞' = Some E" and "A |∈| trail_atms Γ'"
have "linorder_cls.is_least_in_fset (ffilter ((≺⇩c) D) (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
using step_hyps(11) ‹𝒞' = Some E› by (metis Some_eq_The_optionalD)
hence "D ≺⇩c E"
unfolding linorder_cls.is_least_in_ffilter_iff by argo
obtain L where "linorder_lit.is_maximal_in_mset E L"
by (metis ‹D ≺⇩c E› linorder_cls.leD linorder_lit.ex_maximal_in_mset mempty_lesseq_cls)
show "∃L. ord_res.is_maximal_lit L E ∧ A ≼⇩t atm_of L"
proof (intro exI conjI)
show "ord_res.is_maximal_lit L E"
using ‹ord_res.is_maximal_lit L E› .
next
have "K ≼⇩l L"
using step_hyps(4) ‹ord_res.is_maximal_lit L E›
by (metis ‹D ≺⇩c E› linorder_cls.less_asym linorder_lit.leI
linorder_lit.multp_if_maximal_less_that_maximal)
hence "atm_of K ≼⇩t atm_of L"
by (cases K; cases L) simp_all
moreover have "A ≼⇩t atm_of K"
proof -
have "A = atm_of K ∨ A |∈| trail_atms Γ"
using ‹A |∈| trail_atms Γ'›
unfolding ‹Γ' = (K, Some D) # Γ›
by simp
thus "A ≼⇩t atm_of K"
using trail_atms_lt by blast
qed
ultimately show "A ≼⇩t atm_of L"
by order
qed
qed
moreover have "∀Ln ∈ set Γ'. snd Ln = None ⟷ is_neg (fst Ln)"
unfolding ‹Γ' = (K, Some D) # Γ›
using Γ_deci_iff_neg ‹is_pos K› by simp
moreover have "trail_true_cls Γ' C"
if "Ln ∈ set Γ'" and "snd Ln = None" and "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "C ≺⇩c {#fst Ln#}"
for Ln C
proof -
have "Ln = (K, Some D) ∨ Ln ∈ set Γ"
using ‹Ln ∈ set Γ'› unfolding ‹Γ' = (K, Some D) # Γ› by simp
hence "trail_true_cls Γ C"
proof (elim disjE)
assume "Ln = (K, Some D)"
hence False
using ‹snd Ln = None› by simp
thus ?thesis ..
next
assume "Ln ∈ set Γ"
thus "trail_true_cls Γ C"
using Γ_deci_ball_lt_true ‹snd Ln = None› ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹C ≺⇩c {#fst Ln#}›
by metis
qed
thus "trail_true_cls Γ' C"
using ‹suffix Γ Γ'› by (metis trail_true_cls_if_trail_true_suffix)
qed
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using Γ_prop_in step_hyps(10) ‹D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› by simp
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)"
using Γ_prop_greatest step_hyps(8,9,10) by simp
moreover have "∀Γ⇩1 L C Γ⇩0. Γ' = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
unfolding ‹Γ' = (K, Some D) # Γ›
using Γ_prop_almost_false ‹trail_false_cls Γ {#x ∈# D. x ≠ K#}›
by (metis (no_types, lifting) append_eq_Cons_conv list.inject option.inject prod.inject)
moreover have "(∀Γ⇩1 L D Γ⇩0. Γ' = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
proof -
have "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ C"
proof (intro ballI impI)
fix C :: "'f gterm literal multiset"
assume "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "C ≺⇩c D"
thus "trail_true_cls Γ C"
using clauses_lt_D_true by metis
qed
thus ?thesis
unfolding ‹Γ' = (K, Some D) # Γ›
by (smt (verit, ccfv_SIG) Γ_prop_ball_lt_true append_eq_Cons_conv list.inject option.inject
prod.inject)
qed
ultimately show ?thesis
unfolding ‹s' = (U⇩e⇩r, ℱ, Γ', 𝒞')›
proof (intro ord_res_7_invars.intros)
have "trail_true_cls Γ' C"
"⋀K⇩C. linorder_lit.is_maximal_in_mset C K⇩C ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ')"
if C_lt: "⋀E. 𝒞' = Some E ⟹ C ≺⇩c E" and C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" for C
proof -
have "C ≼⇩c D"
using step_hyps that by (metis clause_le_if_lt_least_greater)
hence "C ≺⇩c D ∨ C = D"
by simp
thus "trail_true_cls Γ' C"
proof (elim disjE)
assume "C ≺⇩c D"
hence "trail_true_cls Γ C"
using clauses_lt_D_true ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› by metis
thus "trail_true_cls Γ' C"
using ‹suffix Γ Γ'› by (metis trail_true_cls_if_trail_true_suffix)
next
assume "C = D"
have "trail_true_lit Γ' K"
using ‹Γ' = (K, Some D) # Γ› ‹is_pos K›
unfolding trail_true_lit_def by (cases K) simp_all
thus "trail_true_cls Γ' C"
unfolding ‹C = D› trail_true_cls_def
using ‹K ∈# D› by metis
qed
fix K⇩C
assume C_max_lit: "linorder_lit.is_maximal_in_mset C K⇩C"
show "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ')"
using ‹C ≺⇩c D ∨ C = D›
proof (elim disjE)
assume "C ≺⇩c D"
hence "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ)"
using no_undef_atm_lt_max_lit_if_lt_D C_in C_max_lit by force
thus ?thesis
using step_hyps by force
next
assume "C = D"
thus ?thesis
by (metis C_max_lit D_max_lit ‹suffix Γ Γ'› linorder_lit.Uniq_is_maximal_in_mset
literal.sel(2) step_hyps(5) the1_equality' trail_defined_lit_if_trail_defined_suffix
trail_defined_lit_iff_trail_defined_atm)
qed
qed
thus
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. 𝒞' = Some D ⟶ C ≺⇩c D) ⟶ trail_true_cls Γ' C"
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). (∀D. 𝒞' = Some D ⟶ C ≺⇩c D) ⟶
(∀K. ord_res.is_maximal_lit K C ⟶
¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ'))"
unfolding atomize_conj by metis
qed simp_all
next
case step_hyps: (factoring Γ D K U⇩e⇩r ℱ' ℱ)
note D_max_lit = ‹ord_res.is_maximal_lit K D›
have
ℱ_subset: "ℱ |⊆| N |∪| U⇩e⇩r" and
D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
clauses_lt_D_seldomly_have_undef_max_lit:
"∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀L⇩C. linorder_lit.is_maximal_in_mset C L⇩C ⟶
¬ trail_defined_lit Γ L⇩C ⟶ (trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))" and
clauses_lt_D_true: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ C" and
no_undef_atm_lt_max_lit_if_lt_D: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))" and
Γ_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
Γ_lower: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
trail_atms_le0: "∀A |∈| trail_atms Γ. ∃L. ord_res.is_maximal_lit L D ∧ (A ≼⇩t atm_of L)" and
Γ_deci_iff_neg: "∀Ln ∈ set Γ. snd Ln = None ⟷ is_neg (fst Ln)" and
Γ_deci_ball_lt_true: "∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)" and
Γ_prop_in: "∀Ln ∈ set Γ. ∀D. snd Ln = Some D ⟶ D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
Γ_prop_greatest:
"∀Ln ∈ set Γ. ∀D. snd Ln = Some D ⟶ linorder_lit.is_greatest_in_mset D (fst Ln)" and
Γ_prop_almost_false:
"∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}" and
Γ_prop_ball_lt_true: "(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
using invar by (simp_all add: ‹s = (U⇩e⇩r, ℱ, Γ, Some D)› ord_res_7_invars_def)
have clauses_lt_D_almost_defined: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶ trail_defined_cls Γ {#L ∈# C. L ≠ K#})"
using invar[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, Some D)›] clause_almost_defined_if_lt_next_clause
by simp
have "atm_of K |∉| trail_atms Γ"
using ‹¬ trail_defined_lit Γ K›
by (metis trail_defined_lit_iff_trail_defined_atm)
hence trail_atms_lt: "∀A |∈| trail_atms Γ. A ≺⇩t atm_of K"
using trail_atms_le0 ‹ord_res.is_maximal_lit K D›
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset linorder_trm.antisym_conv1)
have "efac D ≠ D"
using ‹¬ ord_res.is_strictly_maximal_lit K D› D_max_lit ‹is_pos K›
by (metis ex1_efac_eq_factoring_chain ex_ground_factoringI is_pos_def)
hence "efac D ≺⇩c D"
by (metis efac_properties_if_not_ident(1))
hence D_in_strong: "D |∈| N |∪| U⇩e⇩r" and "D |∉| ℱ"
using D_in ‹efac D ≠ D›
unfolding atomize_conj iefac_def
by (smt (verit) factorizable_if_neq_efac fimage_iff iefac_def ex1_efac_eq_factoring_chain)
have "ℱ' |⊆| N |∪| U⇩e⇩r"
unfolding ‹ℱ' = finsert D ℱ›
using ℱ_subset D_in_strong by simp
moreover have "∀C'. Some (efac D) = Some C' ⟶ C' |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
proof -
have "efac D |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
using D_in_strong by (simp add: iefac_def ‹ℱ' = finsert D ℱ›)
thus ?thesis
by simp
qed
moreover have "trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
if "Some (efac D) = Some E" and
C_in: "C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)" and
C_lt: "C ≺⇩c E" and
C_max_lit: "linorder_lit.is_maximal_in_mset C L⇩C" and
L⇩C_undef: "¬ trail_defined_lit Γ L⇩C"
for E C L⇩C
proof -
have "E = efac D"
using that by simp
hence "C ≺⇩c efac D"
using C_lt by order
hence "C ≠ efac D"
by order
hence "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using C_in iefac_def step_hyps(10) by auto
moreover have "C ≺⇩c D"
using ‹C ≺⇩c efac D› ‹efac D ≺⇩c D› by order
ultimately show "trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
using clauses_lt_D_seldomly_have_undef_max_lit C_max_lit L⇩C_undef by metis
qed
moreover have "trail_true_cls Γ C"
"⋀K⇩C. linorder_lit.is_maximal_in_mset C K⇩C ⟹ trail_defined_cls Γ {#L ∈# C. L ≠ K⇩C#}"
if C_lt: "⋀E. Some (efac D) = Some E ⟹ C ≺⇩c E" and C_in: "C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)" for C
proof -
have "C ≺⇩c efac D"
using C_lt by metis
hence "C ≠ efac D"
by order
hence "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using C_in by (auto simp: ‹ℱ' = finsert D ℱ› iefac_def)
moreover have "C ≺⇩c D"
using ‹C ≺⇩c efac D› ‹efac D ≺⇩c D› by order
ultimately show "trail_true_cls Γ C"
using clauses_lt_D_true by metis
fix K⇩C
assume C_max_lit: "linorder_lit.is_maximal_in_mset C K⇩C"
show "trail_defined_cls Γ {#L ∈# C. L ≠ K⇩C#}"
using clauses_lt_D_almost_defined ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹C ≺⇩c D› C_max_lit
by metis
qed
moreover have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
moreover have "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
using Γ_lower .
moreover have "∀D'. Some (efac D) = Some D' ⟶ (∀A |∈| trail_atms Γ.
∃L. ord_res.is_maximal_lit L D' ∧ A ≼⇩t atm_of L)"
proof -
have "∀A |∈| trail_atms Γ. ∃L. ord_res.is_maximal_lit L (efac D) ∧ A ≼⇩t atm_of L"
using trail_atms_lt
using ex1_efac_eq_factoring_chain step_hyps(4)
ord_res.ground_factorings_preserves_maximal_literal by blast
thus ?thesis
by simp
qed
moreover have "∀Ln ∈ set Γ. snd Ln = None ⟷ is_neg (fst Ln)"
using Γ_deci_iff_neg .
moreover have "trail_true_cls Γ C"
if "Ln ∈ set Γ" and "snd Ln = None" and "C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)" and "C ≺⇩c {#fst Ln#}"
for Ln C
proof -
have "C = efac D ∨ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using ‹C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)› by (auto simp: iefac_def ‹ℱ' = finsert D ℱ›)
thus "trail_true_cls Γ C"
proof (elim disjE)
assume "C = efac D"
hence "linorder_lit.is_greatest_in_mset C K"
using D_max_lit ‹is_pos K›
by (metis greatest_literal_in_efacI)
hence "K ≺⇩l fst Ln"
using ‹C ≺⇩c {#fst Ln#}›
by (simp add: linorder_lit.is_greatest_in_mset_iff)
hence "atm_of K ≼⇩t atm_of (fst Ln)"
by (cases K; cases "fst Ln") simp_all
moreover have "atm_of (fst Ln) |∈| trail_atms Γ"
using ‹Ln ∈ set Γ› by (simp add: fset_trail_atms)
moreover have "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)"
by (meson D_in D_max_lit atm_of_in_atms_of_clssI linorder_lit.is_maximal_in_mset_iff)
ultimately have "atm_of K |∈| trail_atms Γ"
using Γ_lower
unfolding linorder_trm.is_lower_set_iff
by fastforce
hence False
using ‹atm_of K |∉| trail_atms Γ› by contradiction
thus "trail_true_cls Γ C" ..
next
assume "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
thus "trail_true_cls Γ C"
using Γ_deci_ball_lt_true ‹Ln ∈ set Γ› ‹snd Ln = None› ‹C ≺⇩c {#fst Ln#}›
by metis
qed
qed
moreover have "C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)" if "Ln ∈ set Γ" and "snd Ln = Some C" for Ln C
proof -
have "atm_of (fst Ln) ≺⇩t atm_of K"
using trail_atms_lt[unfolded fset_trail_atms, simplified] ‹Ln ∈ set Γ› by metis
hence "atm_of (fst Ln) ≠ atm_of K"
by order
hence "fst Ln ≠ K"
by (cases "fst Ln"; cases K) simp_all
moreover have "ord_res.is_maximal_lit (fst Ln) C"
using Γ_prop_greatest ‹Ln ∈ set Γ› ‹snd Ln = Some C› by blast
ultimately have "C ≠ D"
using ‹ord_res.is_maximal_lit K D› by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
moreover have "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using Γ_prop_in ‹Ln ∈ set Γ› ‹snd Ln = Some C› by metis
ultimately show ?thesis
by (auto simp: ‹ℱ' = finsert D ℱ› iefac_def)
qed
moreover have "∀Ln ∈ set Γ. ∀D. snd Ln = Some D ⟶ linorder_lit.is_greatest_in_mset D (fst Ln)"
using Γ_prop_greatest by simp
moreover have "∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
using Γ_prop_almost_false .
moreover have "(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))"
proof (intro allI impI ballI)
fix
Γ⇩1 Γ⇩0 :: "('f gliteral × 'f gclause option) list" and
L :: "'f gliteral" and
C⇩0 C⇩1 :: "'f gclause"
assume
Γ_eq: "Γ = Γ⇩1 @ (L, Some C⇩1) # Γ⇩0" and
C⇩0_in: "C⇩0 |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)" and
"C⇩0 ≺⇩c C⇩1"
have "C⇩0 = efac D ∨ C⇩0 |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using C⇩0_in by (auto simp: iefac_def ‹ℱ' = finsert D ℱ›)
thus "trail_true_cls Γ⇩0 C⇩0"
proof (elim disjE)
assume "C⇩0 = efac D"
have "atm_of L |∈| trail_atms Γ"
using Γ_eq unfolding fset_trail_atms by simp
hence "atm_of L ≺⇩t atm_of K"
using trail_atms_lt by metis
hence "L ≺⇩l K"
by (cases L; cases K) simp_all
moreover have "linorder_lit.is_greatest_in_mset C⇩1 L"
using Γ_eq Γ_prop_greatest by simp
moreover have "linorder_lit.is_greatest_in_mset (efac D) K"
using ‹is_pos K› D_max_lit by (metis greatest_literal_in_efacI)
ultimately have "C⇩1 ≺⇩c efac D"
by (metis linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset
linorder_lit.multp_if_maximal_less_that_maximal)
hence False
using ‹C⇩0 = efac D› ‹C⇩0 ≺⇩c C⇩1› by order
thus ?thesis ..
next
assume "C⇩0 |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
thus ?thesis
using Γ_prop_ball_lt_true Γ_eq ‹C⇩0 ≺⇩c C⇩1› by metis
qed
qed
ultimately show ?thesis
unfolding ‹s' = (U⇩e⇩r, ℱ', Γ, Some (efac D))›
proof (intro ord_res_7_invars.intros)
have "trail_true_cls Γ C"
"⋀K⇩C. linorder_lit.is_maximal_in_mset C K⇩C ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ)"
if C_lt: "⋀E. Some (efac D) = Some E ⟹ C ≺⇩c E" and C_in: "C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
for C
proof -
have "C ≺⇩c efac D"
using C_lt by metis
hence "C ≠ efac D"
by order
hence "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using C_in by (auto simp: ‹ℱ' = finsert D ℱ› iefac_def)
moreover have "C ≺⇩c D"
using ‹C ≺⇩c efac D› ‹efac D ≺⇩c D› by order
ultimately show "trail_true_cls Γ C"
using clauses_lt_D_true by metis
fix K⇩C
assume C_max_lit: "linorder_lit.is_maximal_in_mset C K⇩C"
thus "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩C ∧ A |∉| trail_atms Γ)"
using no_undef_atm_lt_max_lit_if_lt_D ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹C ≺⇩c D› by metis
qed
thus
"∀C|∈|iefac ℱ' |`| (N |∪| U⇩e⇩r). (∀Da. Some (efac D) = Some Da ⟶ C ≺⇩c Da) ⟶
trail_true_cls Γ C"
"∀C|∈|iefac ℱ' |`| (N |∪| U⇩e⇩r). (∀Da. Some (efac D) = Some Da ⟶ C ≺⇩c Da) ⟶
(∀K. ord_res.is_maximal_lit K C ⟶
¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))"
unfolding atomize_conj by metis
qed simp_all
next
case step_hyps: (resolution_bot Γ E K D U⇩e⇩r' U⇩e⇩r Γ' ℱ)
have
ℱ_subset: "ℱ |⊆| N |∪| U⇩e⇩r" and
E_in: "E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
clauses_lt_E_seldomly_have_undef_max_lit:
"∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶
(∀L⇩C. linorder_lit.is_maximal_in_mset C L⇩C ⟶
¬ trail_defined_lit Γ L⇩C ⟶ (trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))" and
clauses_lt_E_true: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶ trail_true_cls Γ C" and
no_undef_atm_lt_max_lit_if_lt_E: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))" and
Γ_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
Γ_lower: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
trail_atms_le0: "∀A |∈| trail_atms Γ. ∃L. ord_res.is_maximal_lit L E ∧ (A ≼⇩t atm_of L)" and
Γ_deci_iff_neg: "∀Ln ∈ set Γ. snd Ln = None ⟷ is_neg (fst Ln)" and
Γ_deci_ball_lt_true: "∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)" and
Γ_prop_in: "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
Γ_prop_greatest:
"∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)" and
Γ_prop_almost_false:
"∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}" and
Γ_prop_ball_lt_true: "∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C)"
using invar by (simp_all add: ‹s = (U⇩e⇩r, ℱ, Γ, Some E)› ord_res_7_invars_def)
have clauses_lt_E_almost_defined: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶ trail_defined_cls Γ {#L ∈# C. L ≠ K#})"
using invar[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, Some E)›] clause_almost_defined_if_lt_next_clause
by simp
have "ℱ |⊆| N |∪| U⇩e⇩r'"
unfolding ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r›
using ℱ_subset by blast
moreover have "∀C'. Some {#} = Some C' ⟶ C' |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
by (simp add: ‹eres D E = {#}› ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r›)
moreover have "trail_true_cls Γ' {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
if "Some {#} = Some E" and
C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')" and
C_lt: "C ≺⇩c E" and
C_max_lit: "linorder_lit.is_maximal_in_mset C L⇩C" and
L⇩C_undef: "¬ trail_defined_lit Γ' L⇩C"
for E C L⇩C
proof -
have "E = {#}"
using that by simp
hence False
using C_lt linorder_cls.leD mempty_lesseq_cls by blast
thus ?thesis ..
qed
moreover have "trail_defined_cls Γ' {#L ∈# x. L ≠ K⇩x#}"
if "Some {#} = Some y" and x_in: "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')" and "x ≺⇩c y" and
x_max_lit: "linorder_lit.is_maximal_in_mset x K⇩x" for x y K⇩x
proof -
have False
using linorder_cls.leD mempty_lesseq_cls that(1) that(3) by blast
thus ?thesis ..
qed
moreover have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
unfolding ‹Γ' = []› by simp
moreover have "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r'))"
unfolding ‹Γ' = []›
by (simp add: linorder_trm.is_lower_set_iff)
moreover have "∀D. Some {#} = Some D ⟶ (∀A |∈| trail_atms Γ'.
∃L. ord_res.is_maximal_lit L D ∧ A ≼⇩t atm_of L)"
unfolding ‹Γ' = []› by simp
moreover have "∀Ln ∈ set Γ'. snd Ln = None ⟷ is_neg (fst Ln)"
unfolding ‹Γ' = []› by simp
moreover have "∀Ln ∈ set Γ'. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r'). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ' C)"
using ‹Γ' = []› by simp
moreover have "∀Ln ∈ set Γ'. snd Ln = None ⟶
¬(∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r'). linorder_lit.is_maximal_in_mset C (- (fst Ln)))"
using ‹Γ' = []› by simp
moreover have "∀Ln ∈ set Γ'. ∀D. snd Ln = Some D ⟶
¬(∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r'). C ≺⇩c D ∧ fst Ln ∈# C)"
using ‹Γ' = []› by simp
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
using ‹Γ' = []› by simp
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)"
using ‹Γ' = []› by simp
moreover have "∀Γ⇩1 L C Γ⇩0. Γ' = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
using ‹Γ' = []› by simp
moreover have "∀Γ⇩1 L D Γ⇩0. Γ' = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r'). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C)"
using ‹Γ' = []› by simp
ultimately show ?thesis
unfolding ‹s' = (U⇩e⇩r', ℱ, Γ', Some {#})›
proof (intro ord_res_7_invars.intros)
have "trail_true_cls Γ' x"
"⋀K⇩x. linorder_lit.is_maximal_in_mset x K⇩x ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r'). A ≺⇩t atm_of K⇩x ∧ A |∉| trail_atms Γ')"
if C_lt: "⋀E. Some {#} = Some E ⟹ x ≺⇩c E" and C_in: "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
for x
proof -
have "x ≺⇩c {#}"
using C_lt by metis
hence False
using linorder_cls.leD mempty_lesseq_cls by blast
thus
"trail_true_cls Γ' x"
"⋀K⇩x. linorder_lit.is_maximal_in_mset x K⇩x ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r'). A ≺⇩t atm_of K⇩x ∧ A |∉| trail_atms Γ')"
by argo+
qed
thus
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). (∀D. Some {#} = Some D ⟶ C ≺⇩c D) ⟶ trail_true_cls Γ' C"
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). (∀D. Some {#} = Some D ⟶ C ≺⇩c D) ⟶
(∀K. ord_res.is_maximal_lit K C ⟶
¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r'). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ'))"
unfolding atomize_conj by metis
qed simp_all
next
case step_hyps: (resolution_pos Γ E L D U⇩e⇩r' U⇩e⇩r Γ' K ℱ)
note E_max_lit = ‹ord_res.is_maximal_lit L E›
note eres_max_lit = ‹ord_res.is_maximal_lit K (eres D E)›
have
ℱ_subset: "ℱ |⊆| N |∪| U⇩e⇩r" and
E_in: "E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
clauses_lt_D_seldomly_have_undef_max_lit:
"∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶
(∀L⇩C. linorder_lit.is_maximal_in_mset C L⇩C ⟶
¬ trail_defined_lit Γ L⇩C ⟶ (trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))" and
clauses_lt_E_true: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶ trail_true_cls Γ C" and
no_undef_atm_lt_max_lit_if_lt_E: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))" and
Γ_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
Γ_lower: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
trail_atms_le0: "∀A |∈| trail_atms Γ. ∃L. ord_res.is_maximal_lit L E ∧ (A ≼⇩t atm_of L)" and
Γ_deci_iff_neg: "∀Ln ∈ set Γ. snd Ln = None ⟷ is_neg (fst Ln)" and
Γ_deci_ball_lt_true: "∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)" and
Γ_prop_in: "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
Γ_prop_greatest:
"∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)" and
Γ_prop_almost_false:
"∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}" and
Γ_prop_ball_lt_true: "∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C)"
using invar by (simp_all add: ‹s = (U⇩e⇩r, ℱ, Γ, Some E)› ord_res_7_invars_def)
have clauses_lt_E_almost_defined: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶ trail_defined_cls Γ {#L ∈# C. L ≠ K#})"
using invar[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, Some E)›] clause_almost_defined_if_lt_next_clause
by simp
have Γ_consistent: "trail_consistent Γ"
using trail_consistent_if_sorted_wrt_atoms Γ_sorted by metis
have trail_atms_le: "∀A |∈| trail_atms Γ. A ≼⇩t atm_of L"
using trail_atms_le0 E_max_lit
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
have "(- L, Some D) ∈ set Γ"
using ‹map_of Γ (- L) = Some (Some D)› by (metis map_of_SomeD)
hence D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using Γ_prop_in by simp
have D_max_lit: "linorder_lit.is_greatest_in_mset D (- L)"
using Γ_prop_greatest ‹(- L, Some D) ∈ set Γ› by fastforce
have "suffix Γ' Γ"
using step_hyps(9) suffix_dropWhile by metis
hence "atms_of_cls (eres D E) |⊆| atms_of_cls D |∪| atms_of_cls E"
using lit_in_one_of_resolvents_if_in_eres
unfolding atms_of_cls_def by fastforce
moreover have "atms_of_cls D |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
using ‹D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)›
by (metis atms_of_clss_fimage_iefac atms_of_clss_finsert finsert_absorb funion_upper1)
moreover have "atms_of_cls E |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
using ‹E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)›
by (metis atms_of_clss_fimage_iefac atms_of_clss_finsert finsert_absorb funion_upper1)
ultimately have "atms_of_clss (N |∪| U⇩e⇩r) = atms_of_clss (N |∪| U⇩e⇩r')"
unfolding ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r› atms_of_clss_def by auto
obtain A⇩L where L_def: "L = Neg A⇩L"
using ‹is_neg L› by (cases L) simp_all
have "D ≺⇩c E"
using clause_lt_clause_if_max_lit_comp
using E_max_lit ‹is_neg L› D_max_lit
by (metis linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset)
have "eres D E ≺⇩c E"
using eres_lt_if
using E_max_lit ‹is_neg L› D_max_lit by metis
hence "eres D E ≠ E"
by order
have "L ∈# E"
using E_max_lit unfolding linorder_lit.is_maximal_in_mset_iff by metis
hence "- L ∉# E"
using not_both_lit_and_comp_lit_in_false_clause_if_trail_consistent
using Γ_consistent ‹trail_false_cls Γ E› by metis
hence "∀K ∈# eres D E. atm_of K ≺⇩t atm_of L"
using lit_in_eres_lt_greatest_lit_in_grestest_resolvant[OF ‹eres D E ≠ E› E_max_lit] by metis
hence "∀K ∈# eres D E. K ≠ L ∧ K ≠ - L"
by fastforce
moreover have "∀L ∈# eres D E. L ∈# D ∨ L ∈# E"
using lit_in_one_of_resolvents_if_in_eres by metis
moreover have D_almost_false: "trail_false_cls Γ {#K ∈# D. K ≠ - L#}"
using ord_res_7_invars_implies_propagated_clause_almost_false
using ‹(- L, Some D) ∈ set Γ› invar[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, Some E)›]
by metis
ultimately have "trail_false_cls Γ (eres D E)"
using ‹trail_false_cls Γ E› unfolding trail_false_cls_def by fastforce
hence "trail_false_lit Γ K"
using eres_max_lit unfolding linorder_lit.is_maximal_in_mset_iff trail_false_cls_def by metis
have "eres D E |∉| N |∪| U⇩e⇩r"
using eres_not_in_known_clauses_if_trail_false_cls
using Γ_consistent clauses_lt_E_true ‹eres D E ≺⇩c E› ‹trail_false_cls Γ (eres D E)› by metis
hence "eres D E |∉| ℱ"
using ℱ_subset by blast
hence "iefac ℱ (eres D E) = eres D E"
by (simp add: iefac_def)
hence "iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))"
unfolding ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r› by simp
have "trail_false_lit Γ K"
by (meson ‹trail_false_cls Γ (eres D E)› linorder_lit.is_maximal_in_mset_iff step_hyps(10)
trail_false_cls_def)
have mem_set_Γ'_iff: "(Ln ∈ set Γ') = (¬ atm_of K ≼⇩t atm_of (fst Ln) ∧ Ln ∈ set Γ)" for Ln
unfolding ‹Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ›
proof (rule mem_set_dropWhile_conv_if_list_sorted_and_pred_monotone)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
next
show "monotone_on (set Γ) (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) (λx y. y ≤ x)
(λLn. atm_of K ≼⇩t atm_of (fst Ln))"
by (rule monotone_onI) auto
qed
hence atms_in_Γ'_lt_atm_K: "∀x |∈| trail_atms Γ'. x ≺⇩t atm_of K"
by (auto simp add: fset_trail_atms)
have "ℱ |⊆| N |∪| U⇩e⇩r'"
unfolding ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r›
using ℱ_subset by blast
moreover have "∀C'. Some (eres D E) = Some C' ⟶ C' |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
proof -
have "eres D E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
using ‹iefac ℱ (eres D E) = eres D E›
by (simp add: ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r›)
thus ?thesis
by simp
qed
moreover have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
using Γ_sorted step_hyps(9) by (metis sorted_wrt_dropWhile)
moreover have Γ'_lower: "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r'))"
proof -
have "linorder_trm.is_lower_fset (trail_atms Γ') (trail_atms Γ)"
unfolding linorder_trm.is_lower_set_iff
proof (intro conjI ballI impI)
show "fset (trail_atms Γ') ⊆ fset (trail_atms Γ)"
unfolding fset_trail_atms using ‹suffix Γ' Γ› by (metis image_mono set_mono_suffix)
next
obtain Γ'' where "Γ = Γ'' @ Γ'"
using ‹suffix Γ' Γ› unfolding suffix_def by metis
fix l x
assume "l |∈| trail_atms Γ'" and "x |∈| trail_atms Γ" and "x ≺⇩t l"
have "x |∈| trail_atms Γ'' ∨ x |∈| trail_atms Γ'"
using ‹x |∈| trail_atms Γ› unfolding ‹Γ = Γ'' @ Γ'› fset_trail_atms by auto
thus "x |∈| trail_atms Γ'"
proof (elim disjE)
assume "x |∈| trail_atms Γ''"
hence "l ≺⇩t x"
using Γ_sorted ‹l |∈| trail_atms Γ'›
unfolding ‹Γ = Γ'' @ Γ'› sorted_wrt_append fset_trail_atms by blast
hence False
using ‹x ≺⇩t l› by order
thus "x |∈| trail_atms Γ'" ..
next
assume "x |∈| trail_atms Γ'"
thus "x |∈| trail_atms Γ'" .
qed
qed
thus ?thesis
using Γ_lower
unfolding ‹atms_of_clss (N |∪| U⇩e⇩r) = atms_of_clss (N |∪| U⇩e⇩r')›
by order
qed
moreover have "∀DE. Some (eres D E) = Some DE ⟶ (∀A |∈| trail_atms Γ'.
∃L. ord_res.is_maximal_lit L DE ∧ A ≼⇩t atm_of L)"
using atms_in_Γ'_lt_atm_K eres_max_lit by blast
moreover have "∀Ln ∈ set Γ'. snd Ln = None ⟷ is_neg (fst Ln)"
using Γ_deci_iff_neg ‹suffix Γ' Γ›
by (metis (no_types, opaque_lifting) in_set_conv_decomp suffixE suffix_appendD)
moreover have "trail_true_cls Γ' C"
if "Ln ∈ set Γ'" and "snd Ln = None" and "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')" and "C ≺⇩c {#fst Ln#}"
for Ln C
proof -
have "Ln ∈ set Γ"
using ‹Ln ∈ set Γ'› ‹suffix Γ' Γ› set_mono_suffix by blast
have "C = eres D E ∨ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')›
unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
by simp
thus "trail_true_cls Γ' C"
proof (elim disjE)
assume "C = eres D E"
hence "K ≺⇩l fst Ln"
using ‹C ≺⇩c {#fst Ln#}› eres_max_lit
by (simp add: linorder_lit.is_maximal_in_mset_iff)
hence "atm_of K ≼⇩t atm_of (fst Ln)"
by (cases K; cases "fst Ln") simp_all
moreover have "atm_of (fst Ln) |∈| trail_atms Γ'"
using ‹Ln ∈ set Γ'› by (simp add: fset_trail_atms)
moreover have "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r')"
by (metis ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
atm_of_in_atms_of_clssI eres_max_lit finsert_iff linorder_lit.is_maximal_in_mset_iff)
ultimately have "atm_of K |∈| trail_atms Γ'"
using Γ'_lower
unfolding linorder_trm.is_lower_set_iff
by fastforce
moreover have "atm_of K |∉| trail_atms Γ'"
using atms_in_Γ'_lt_atm_K by blast
ultimately show "trail_true_cls Γ' C"
by contradiction
next
assume "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
hence "trail_true_cls Γ C"
using Γ_deci_ball_lt_true ‹Ln ∈ set Γ› ‹snd Ln = None› ‹C ≺⇩c {#fst Ln#}› by metis
then obtain L⇩C where "L⇩C ∈# C" and "trail_true_lit Γ L⇩C"
unfolding trail_true_cls_def by auto
hence "∀x ∈# C. x ≺⇩l fst Ln"
using ‹C ≺⇩c {#fst Ln#}›
unfolding multp_singleton_right[OF linorder_lit.transp_on_less]
by simp
hence "L⇩C ≺⇩l fst Ln"
using ‹L⇩C ∈# C› by metis
hence "atm_of L⇩C ≼⇩t atm_of (fst Ln)"
by (cases L⇩C; cases "fst Ln") simp_all
moreover have "atm_of (fst Ln) ≺⇩t atm_of K"
using atms_in_Γ'_lt_atm_K
by (simp add: fset_trail_atms that(1))
ultimately have "atm_of L⇩C ≺⇩t atm_of K"
by order
have "L⇩C ∈ fst ` set Γ"
using ‹trail_true_lit Γ L⇩C›
unfolding trail_true_lit_def .
hence "L⇩C ∈ fst ` set Γ'"
using mem_set_Γ'_iff
using ‹atm_of L⇩C ≺⇩t atm_of K› linorder_trm.not_le by auto
hence "trail_true_lit Γ' L⇩C"
unfolding trail_true_lit_def .
thus "trail_true_cls Γ' C"
using ‹L⇩C ∈# C›
unfolding trail_true_cls_def by auto
qed
qed
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
using Γ_prop_in ‹suffix Γ' Γ› set_mono_suffix ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r› by blast
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)"
using Γ_prop_greatest ‹suffix Γ' Γ› set_mono_suffix by blast
moreover have "∀Γ⇩1 L C Γ⇩0. Γ' = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
using Γ_prop_almost_false ‹suffix Γ' Γ›
by (metis (no_types, lifting) append.assoc suffix_def)
moreover have "∀Γ⇩1 L D Γ⇩0. Γ' = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r'). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C)"
proof (intro allI impI ballI)
fix
Γ⇩1 Γ⇩0 :: "('f gliteral × 'f gclause option) list" and
L :: "'f gliteral" and
C⇩0 C⇩1 :: "'f gclause"
assume
Γ'_eq: "Γ' = Γ⇩1 @ (L, Some C⇩1) # Γ⇩0" and
C⇩0_in: "C⇩0 |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')" and
"C⇩0 ≺⇩c C⇩1"
have "C⇩0 = eres D E ∨ C⇩0 |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using C⇩0_in
unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
by simp
thus "trail_true_cls Γ⇩0 C⇩0"
proof (elim disjE)
assume "C⇩0 = eres D E"
have "¬ atm_of K ≼⇩t atm_of (fst (L, Some C⇩1))" and "(L, Some C⇩1) ∈ set Γ"
unfolding atomize_conj
using Γ'_eq ‹Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ›
using mem_set_dropWhile_conv_if_list_sorted_and_pred_monotone[OF Γ_sorted mono_atms_lt]
by (metis in_set_conv_decomp)
then have "¬ atm_of K ≼⇩t atm_of L"
by simp
hence "atm_of L ≺⇩t atm_of K"
by order
moreover have "linorder_lit.is_greatest_in_mset C⇩1 L"
using Γ_prop_greatest ‹(L, Some C⇩1) ∈ set Γ› by fastforce
ultimately have False
using ‹C⇩0 ≺⇩c C⇩1›
by (metis Neg_atm_of_iff ‹C⇩0 = eres D E› asympD eres_max_lit
linorder_lit.is_greatest_in_mset_iff_is_maximal_and_count_eq_one
linorder_lit.multp_if_maximal_less_that_maximal literal.collapse(1)
ord_res.asymp_less_cls ord_res.less_lit_simps(1) ord_res.less_lit_simps(4)
step_hyps(11))
thus "trail_true_cls Γ⇩0 C⇩0" ..
next
assume "C⇩0 |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
thus "trail_true_cls Γ⇩0 C⇩0"
using Γ_prop_ball_lt_true Γ'_eq ‹C⇩0 ≺⇩c C⇩1›
by (metis (no_types, opaque_lifting) ‹suffix Γ' Γ› append_assoc suffixE)
qed
qed
ultimately show ?thesis
unfolding ‹s' = (U⇩e⇩r', ℱ, Γ', Some (eres D E))›
proof (intro ord_res_7_invars.intros)
have clause_true_in_Γ'_if: "trail_true_cls Γ' x" and
"⋀K⇩x. linorder_lit.is_maximal_in_mset x K⇩x ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r'). A ≺⇩t atm_of K⇩x ∧ A |∉| trail_atms Γ')"
if x_lt: "⋀DE. Some (eres D E) = Some DE ⟶ x ≺⇩c DE" and x_in: "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
for x
proof -
have "x ≺⇩c eres D E"
using x_lt by metis
hence "x ≠ eres D E"
by order
hence x_in': "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using x_in ‹iefac ℱ (eres D E) = eres D E›
by (simp add: ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r›)
have "x ≺⇩c E"
using ‹x ≺⇩c eres D E› ‹eres D E ≺⇩c E› by order
have x_true: "trail_true_cls Γ x"
using clauses_lt_E_true x_in' ‹x ≺⇩c E› by metis
have "(- K, None) ∈ set Γ"
using ‹trail_false_lit Γ K›
using ‹is_pos K›
using Γ_deci_iff_neg
by (metis is_pos_neg_not_is_pos map_of_SomeD map_of_eq_None_iff not_Some_eq prod.collapse
prod.inject trail_false_lit_def)
obtain L⇩x where "L⇩x ∈# x" and L⇩x_true: "trail_true_lit Γ L⇩x"
using x_true unfolding trail_true_cls_def by metis
moreover have "L⇩x ≠ K"
using Γ_consistent ‹trail_false_cls Γ (eres D E)› L⇩x_true eres_max_lit
by (metis linorder_lit.is_maximal_in_mset_iff not_trail_true_cls_and_trail_false_cls
trail_true_cls_def)
moreover have "L⇩x ≠ - K"
using eres_max_lit ‹x ≺⇩c eres D E› ‹L⇩x ≠ K› ‹L⇩x ∈# x›
by (smt (verit, del_insts) empty_iff linorder_cls.less_not_sym
linorder_lit.ex_maximal_in_mset linorder_lit.is_maximal_in_mset_iff
linorder_lit.less_trans linorder_lit.multp_if_maximal_less_that_maximal linorder_lit.neqE
linorder_trm.not_less_iff_gr_or_eq literal.collapse(1) ord_res.less_lit_simps(4)
set_mset_empty step_hyps(11) uminus_literal_def)
ultimately have "atm_of L⇩x ≠ atm_of K"
by (simp add: atm_of_eq_atm_of)
moreover have "L⇩x ≼⇩l K"
proof (rule linorder_lit.less_than_maximal_if_multp⇩H⇩O[OF eres_max_lit _ ‹L⇩x ∈# x›])
show "multp⇩H⇩O (≺⇩l) x (eres D E)"
using ‹x ≺⇩c eres D E›
by (simp add: multp_imp_multp⇩H⇩O)
qed
ultimately have "atm_of L⇩x ≺⇩t atm_of K"
by (cases L⇩x; cases K) simp_all
hence "trail_true_lit Γ' L⇩x"
unfolding ‹Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ›
using L⇩x_true
unfolding trail_true_lit_def
using mem_set_dropWhile_conv_if_list_sorted_and_pred_monotone[OF Γ_sorted mono_atms_lt]
by (metis (no_types, lifting) image_iff linorder_trm.not_le)
thus "trail_true_cls Γ' x"
using ‹L⇩x ∈# x› unfolding trail_true_cls_def by metis
fix K⇩x
assume x_max_lit: "ord_res.is_maximal_lit K⇩x x"
hence "K⇩x ≼⇩l K"
using ‹x ≺⇩c eres D E› eres_max_lit
using linorder_lit.multp_if_maximal_less_that_maximal by fastforce
hence "atm_of K⇩x ≼⇩t atm_of K"
by (cases K⇩x; cases K) simp_all
have "A |∈| trail_atms Γ'"
if A_lt: "A ≺⇩t atm_of K⇩x" and A_in: "A |∈| atms_of_clss (N |∪| U⇩e⇩r)" for A
unfolding ‹Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ›
proof (rule in_trail_atms_dropWhileI)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
next
show "monotone_on (set Γ) (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) (λx y. y ≤ x) (λx. atm_of K ≼⇩t atm_of (fst x))"
using mono_atms_lt .
next
show "¬ atm_of K ≼⇩t A"
using A_lt ‹atm_of K⇩x ≼⇩t atm_of K› by order
next
have "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩x ∧ A |∉| trail_atms Γ)"
using no_undef_atm_lt_max_lit_if_lt_E ‹x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹x ≺⇩c E› x_max_lit
by metis
thus "A |∈| trail_atms Γ"
using A_in A_lt by metis
qed
thus "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r'). A ≺⇩t atm_of K⇩x ∧ A |∉| trail_atms Γ')"
using ‹atms_of_clss (N |∪| U⇩e⇩r) = atms_of_clss (N |∪| U⇩e⇩r')› by metis
qed
thus
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). (∀DE. Some (eres D E) = Some DE ⟶ C ≺⇩c DE) ⟶
trail_true_cls Γ' C"
"∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). (∀DE. Some (eres D E) = Some DE ⟶ C ≺⇩c DE) ⟶
(∀K. ord_res.is_maximal_lit K C ⟶
¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r'). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ'))"
unfolding atomize_conj by metis
have "trail_true_cls Γ' {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
if "Some (eres D E) = Some DE" and
C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')" and
C_lt: "C ≺⇩c DE" and
C_max_lit: "linorder_lit.is_maximal_in_mset C L⇩C" and
L⇩C_undef: "¬ trail_defined_lit Γ' L⇩C"
for DE C L⇩C
proof -
have "DE = eres D E"
using that by simp
hence "C ≺⇩c eres D E"
using C_lt by order
hence "C ≠ eres D E"
by order
hence "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using C_in ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
by simp
moreover have "C ≺⇩c E"
using ‹C ≺⇩c eres D E› ‹eres D E ≺⇩c E› by order
have "L⇩C ≼⇩l K"
using ‹C ≺⇩c eres D E› C_max_lit eres_max_lit
by (meson linorder_cls.dual_order.asym linorder_lit.leI
linorder_lit.multp_if_maximal_less_that_maximal)
hence "L⇩C ≺⇩l K ∨ L⇩C = K"
by simp
thus ?thesis
proof (elim disjE)
assume "L⇩C ≺⇩l K"
hence "atm_of L⇩C ≺⇩t atm_of K"
using ‹is_pos K›
by (cases L⇩C; cases K) simp_all
have "trail_defined_lit Γ' L⇩C"
unfolding ‹Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ›
proof (intro trail_defined_lit_dropWhileI ballI)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
next
show "monotone_on (set Γ) (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) (λx y. y ≤ x)
(λx. atm_of K ≼⇩t atm_of (fst x))"
using mono_atms_lt .
next
have "¬ atm_of K ≼⇩t atm_of L⇩C"
using ‹atm_of L⇩C ≺⇩t atm_of K› by order
thus "¬ atm_of K ≼⇩t atm_of L⇩C ∧ ¬ atm_of K ≼⇩t atm_of (- L⇩C)"
by simp
next
have "trail_defined_lit Γ K"
using ‹trail_false_lit Γ K›
using trail_defined_lit_iff_true_or_false by blast
moreover have "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)"
by (metis ‹atms_of_clss (N |∪| U⇩e⇩r) = atms_of_clss (N |∪| U⇩e⇩r')›
‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
atm_of_in_atms_of_clssI eres_max_lit finsertI1 linorder_lit.is_maximal_in_mset_iff)
moreover have "atm_of L⇩C |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› C_max_lit atm_of_in_atms_of_clssI
unfolding linorder_lit.is_maximal_in_mset_iff
by metis
ultimately show "trail_defined_lit Γ L⇩C"
using ‹atm_of L⇩C ≺⇩t atm_of K› Γ_lower
unfolding trail_defined_lit_iff_trail_defined_atm
by (meson linorder_trm.is_lower_set_iff)
qed
hence False
using L⇩C_undef by contradiction
thus ?thesis ..
next
have "trail_true_cls Γ' C"
using clause_true_in_Γ'_if C_in ‹C ≺⇩c eres D E› by blast
hence "trail_true_cls Γ' {#K ∈# C. K ≠ L⇩C#}"
using L⇩C_undef
by (smt (verit, best) mem_Collect_eq set_mset_filter trail_defined_lit_iff_true_or_false
trail_true_cls_def)
moreover assume "L⇩C = K"
ultimately show "trail_true_cls Γ' {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C"
using ‹is_pos K› by metis
qed
qed
thus "∀Da. Some (eres D E) = Some Da ⟶
(∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). C ≺⇩c Da ⟶ (∀L⇩C. ord_res.is_maximal_lit L⇩C C ⟶
¬ trail_defined_lit Γ' L⇩C ⟶ trail_true_cls Γ' {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))"
by metis
qed simp_all
next
case step_hyps: (resolution_neg Γ E L D U⇩e⇩r' U⇩e⇩r Γ' K C ℱ)
note E_max_lit = ‹ord_res.is_maximal_lit L E›
note eres_max_lit = ‹ord_res.is_maximal_lit K (eres D E)›
have
ℱ_subset: "ℱ |⊆| N |∪| U⇩e⇩r" and
E_in: "E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
clauses_lt_D_seldomly_have_undef_max_lit:
"∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶
(∀L⇩C. linorder_lit.is_maximal_in_mset C L⇩C ⟶
¬ trail_defined_lit Γ L⇩C ⟶ (trail_true_cls Γ {#K ∈# C. K ≠ L⇩C#} ∧ is_pos L⇩C))" and
clauses_lt_E_true: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶ trail_true_cls Γ C" and
no_undef_atm_lt_max_lit_if_lt_E: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ))" and
Γ_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
Γ_lower: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
trail_atms_le0: "∀A |∈| trail_atms Γ. ∃L. ord_res.is_maximal_lit L E ∧ (A ≼⇩t atm_of L)" and
Γ_deci_iff_neg: "∀Ln ∈ set Γ. snd Ln = None ⟷ is_neg (fst Ln)" and
Γ_deci_ball_lt_true: "∀Ln ∈ set Γ. snd Ln = None ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c {#fst Ln#} ⟶ trail_true_cls Γ C)" and
Γ_prop_in: "∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
Γ_prop_greatest:
"∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)" and
Γ_prop_almost_false:
"∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}" and
Γ_prop_ball_lt_true: "(∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C))" and
Γ_prop_ball_lt_true: "∀Γ⇩1 L D Γ⇩0. Γ = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C)"
using invar by (simp_all add: ‹s = (U⇩e⇩r, ℱ, Γ, Some E)› ord_res_7_invars_def)
have clauses_lt_E_almost_defined: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶
(∀K. linorder_lit.is_maximal_in_mset C K ⟶ trail_defined_cls Γ {#L ∈# C. L ≠ K#})"
using invar[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, Some E)›] clause_almost_defined_if_lt_next_clause
by simp
have Γ_consistent: "trail_consistent Γ"
using trail_consistent_if_sorted_wrt_atoms Γ_sorted by metis
have trail_atms_le: "∀A |∈| trail_atms Γ. A ≼⇩t atm_of L"
using trail_atms_le0 E_max_lit
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
have "(- L, Some D) ∈ set Γ"
using ‹map_of Γ (- L) = Some (Some D)› by (metis map_of_SomeD)
hence D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using Γ_prop_in by simp
have D_max_lit: "linorder_lit.is_greatest_in_mset D (- L)"
using Γ_prop_greatest ‹(- L, Some D) ∈ set Γ› by fastforce
have "D ≺⇩c E"
using clause_lt_clause_if_max_lit_comp
using E_max_lit ‹is_neg L› D_max_lit
by (metis linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset)
have "eres D E ≺⇩c E"
using eres_lt_if
using E_max_lit ‹is_neg L› D_max_lit by metis
hence "eres D E ≠ E"
by order
have "(- K, Some C) ∈ set Γ"
using ‹map_of Γ (- K) = Some (Some C)› by (metis map_of_SomeD)
hence C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using Γ_prop_in by simp
have C_max_lit: "linorder_lit.is_greatest_in_mset C (- K)"
using Γ_prop_greatest ‹(- K, Some C) ∈ set Γ› by fastforce
hence "C ≺⇩c eres D E"
using ‹ord_res.is_maximal_lit K (eres D E)› ‹is_neg L›
by (metis Neg_atm_of_iff Pos_atm_of_iff linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset
linorder_lit.multp_if_maximal_less_that_maximal linorder_lit.not_less_iff_gr_or_eq
linorder_trm.less_irrefl ord_res.less_lit_simps(4) step_hyps(11) uminus_Neg)
have "suffix Γ' Γ"
using step_hyps(9) suffix_dropWhile by metis
hence "atms_of_cls (eres D E) |⊆| atms_of_cls D |∪| atms_of_cls E"
using lit_in_one_of_resolvents_if_in_eres
unfolding atms_of_cls_def by fastforce
moreover have "atms_of_cls D |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
using D_in
by (metis atms_of_clss_fimage_iefac atms_of_clss_finsert finsert_absorb funion_upper1)
moreover have "atms_of_cls E |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
using E_in
by (metis atms_of_clss_fimage_iefac atms_of_clss_finsert finsert_absorb funion_upper1)
ultimately have "atms_of_clss (N |∪| U⇩e⇩r) = atms_of_clss (N |∪| U⇩e⇩r')"
unfolding ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r› atms_of_clss_def by auto
have "L ∈# E"
using E_max_lit unfolding linorder_lit.is_maximal_in_mset_iff by metis
hence "- L ∉# E"
using not_both_lit_and_comp_lit_in_false_clause_if_trail_consistent
using Γ_consistent ‹trail_false_cls Γ E› by metis
hence "∀K ∈# eres D E. atm_of K ≺⇩t atm_of L"
using lit_in_eres_lt_greatest_lit_in_grestest_resolvant[OF ‹eres D E ≠ E› E_max_lit] by metis
hence "∀K ∈# eres D E. K ≠ L ∧ K ≠ - L"
by fastforce
moreover have "∀L ∈# eres D E. L ∈# D ∨ L ∈# E"
using lit_in_one_of_resolvents_if_in_eres by metis
moreover have D_almost_false: "trail_false_cls Γ {#K ∈# D. K ≠ - L#}"
using ord_res_7_invars_implies_propagated_clause_almost_false
using ‹(- L, Some D) ∈ set Γ› invar[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, Some E)›]
by metis
ultimately have "trail_false_cls Γ (eres D E)"
using ‹trail_false_cls Γ E› unfolding trail_false_cls_def by fastforce
have "eres D E |∉| N |∪| U⇩e⇩r"
using eres_not_in_known_clauses_if_trail_false_cls
using Γ_consistent clauses_lt_E_true ‹eres D E ≺⇩c E› ‹trail_false_cls Γ (eres D E)› by metis
hence "eres D E |∉| ℱ"
using ℱ_subset by blast
hence "iefac ℱ (eres D E) = eres D E"
by (simp add: iefac_def)
hence "iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))"
by (simp add: ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r›)
have mem_set_Γ'_iff: "(Ln ∈ set Γ') = (¬ atm_of K ≼⇩t atm_of (fst Ln) ∧ Ln ∈ set Γ)" for Ln
unfolding ‹Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ›
proof (rule mem_set_dropWhile_conv_if_list_sorted_and_pred_monotone)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
next
show "monotone_on (set Γ) (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) (λx y. y ≤ x)
(λLn. atm_of K ≼⇩t atm_of (fst Ln))"
by (rule monotone_onI) auto
qed
have atms_in_Γ'_lt_atm_K: "∀A |∈| trail_atms Γ'. A ≺⇩t atm_of K"
proof -
have "∃L. ord_res.is_maximal_lit L C ∧ x ≺⇩t atm_of L" if "x |∈| trail_atms Γ'" for x
proof (intro exI conjI)
show "ord_res.is_maximal_lit (- K) C"
using C_max_lit by blast
next
show "x ≺⇩t atm_of (- K)"
using ‹x |∈| trail_atms Γ'› mem_set_Γ'_iff unfolding fset_trail_atms by fastforce
qed
hence "∀A|∈|trail_atms Γ'. A ≺⇩t atm_of (- K)"
using C_max_lit
by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset
linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset)
thus ?thesis
by (metis atm_of_uminus)
qed
have "ℱ |⊆| N |∪| U⇩e⇩r'"
unfolding ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r›
using ℱ_subset by blast
moreover have "∀C'. Some C = Some C' ⟶ C' |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
using C_in by (simp add: ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r›)
moreover have
"⋀K⇩x. linorder_lit.is_maximal_in_mset x K⇩x ⟹ trail_defined_cls Γ' {#L ∈# x. L ≠ K⇩x#}" and
clause_true_in_Γ'_if: "trail_true_cls Γ' x"
if x_lt: "⋀y. Some C = Some y ⟹ x ≺⇩c y" and x_in: "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')" for x
proof -
have "x ≺⇩c C"
using x_lt by metis
hence "x ≺⇩c eres D E"
using ‹C ≺⇩c eres D E› by order
hence "x ≠ eres D E"
by order
have "x ≺⇩c E"
using ‹x ≺⇩c eres D E› ‹eres D E ≺⇩c E› by order
moreover have x_in': "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using x_in ‹x ≠ eres D E›
unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
by simp
ultimately have x_true: "trail_true_cls Γ x"
using clauses_lt_E_true by metis
then obtain L⇩x where "L⇩x ∈# x" and "trail_true_lit Γ L⇩x"
unfolding trail_true_cls_def by metis
have "L⇩x ≼⇩l - K"
using C_max_lit ‹x ≺⇩c C› ‹L⇩x ∈# x›
by (smt (verit, ccfv_threshold) asympD empty_not_add_mset ord_res.transp_less_lit insert_DiffM
linorder_lit.is_greatest_in_set_iff linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset
linorder_lit.is_maximal_in_mset_iff linorder_lit.is_maximal_in_set_eq_is_greatest_in_set
linorder_lit.is_maximal_in_set_iff linorder_lit.leI ord_res.asymp_less_cls
ord_res.multp_if_all_left_smaller transpE)
have mono_atms_lt: "monotone_on (set Γ) (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) (λx y. y ≤ x)
(λx. atm_of K ≼⇩t atm_of (fst x))"
proof (intro monotone_onI, unfold le_bool_def, intro impI)
fix x y
assume "atm_of (fst y) ≺⇩t atm_of (fst x)" and "atm_of K ≼⇩t atm_of (fst y)"
thus "atm_of K ≼⇩t atm_of (fst x)"
by order
qed
obtain Γ⇩1 Γ⇩0 where Γ_eq: "Γ = Γ⇩1 @ (- K, Some C) # Γ⇩0"
using ‹(- K, Some C) ∈ set Γ› by (metis split_list)
hence "trail_true_cls Γ⇩0 x"
using Γ_prop_ball_lt_true x_in' ‹x ≺⇩c C› by metis
then obtain L⇩x where "L⇩x ∈# x" and L⇩x_true: "trail_true_lit Γ⇩0 L⇩x"
unfolding trail_true_cls_def by auto
moreover have "Γ' = Γ⇩0"
proof -
have "Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) ((Γ⇩1 @ [(- K, Some C)]) @ Γ⇩0)"
unfolding ‹Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ› Γ_eq by simp
also have "… = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ⇩0"
proof (rule dropWhile_append2)
fix Ln :: "'f gterm literal × 'f gclause option"
assume "Ln ∈ set (Γ⇩1 @ [(- K, Some C)])"
moreover have "∀x∈set Γ⇩1. atm_of K ≺⇩t atm_of (fst x)"
using Γ_sorted by (simp add: Γ_eq sorted_wrt_append)
ultimately show "atm_of K ≼⇩t atm_of (fst Ln)"
using ‹is_neg K› by auto
qed
also have "… = Γ⇩0"
proof (cases Γ⇩0)
case Nil
thus ?thesis
by (simp add: dropWhile_eq_self_iff)
next
case (Cons Ln Γ⇩0')
hence "atm_of (fst Ln) ≺⇩t atm_of K"
using Γ_sorted by (simp add: Γ_eq sorted_wrt_append)
hence "¬ atm_of K ≼⇩t atm_of (fst Ln)"
by order
hence "¬ atm_of K ≼⇩t atm_of (fst (hd Γ⇩0))"
by (simp add: ‹Γ⇩0 = Ln # Γ⇩0'›)
thus ?thesis
by (simp add: dropWhile_eq_self_iff)
qed
finally show ?thesis .
qed
ultimately have "trail_true_lit Γ' L⇩x"
by argo
thus "trail_true_cls Γ' x"
using ‹L⇩x ∈# x› unfolding trail_true_cls_def by metis
fix K⇩x assume x_max_lit: "ord_res.is_maximal_lit K⇩x x"
show "trail_defined_cls Γ' {#L ∈# x. L ≠ K⇩x#}"
unfolding ‹Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ›
proof (intro trail_defined_cls_dropWhileI ballI)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
next
show "monotone_on (set Γ) (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) (λx y. y ≤ x)
(λx. atm_of K ≼⇩t atm_of (fst x))"
using mono_atms_lt .
next
fix L⇩x
assume "L⇩x ∈# {#L ∈# x. L ≠ K⇩x#}"
hence "L⇩x ∈# x" and "L⇩x ≠ K⇩x"
by simp_all
hence "L⇩x ≺⇩l K⇩x"
using x_max_lit ‹L⇩x ∈# x› ‹L⇩x ≠ K⇩x› unfolding linorder_lit.is_maximal_in_mset_iff
by fastforce
moreover have "K⇩x ≼⇩l K"
using ‹x ≺⇩c eres D E›
using linorder_lit.multp_if_maximal_less_that_maximal[OF eres_max_lit x_max_lit]
by fastforce
ultimately have "atm_of L⇩x ≺⇩t atm_of K"
using ‹is_neg K›
by (metis C_max_lit Pos_atm_of_iff ‹x ≺⇩c C› linorder_cls.dual_order.asym
linorder_lit.dual_order.strict_trans1
linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset linorder_lit.less_le_not_le
linorder_lit.multp_if_maximal_less_that_maximal linorder_trm.linorder_cases
literal.collapse(2) ord_res.less_lit_simps(3) ord_res.less_lit_simps(4) uminus_Neg
x_max_lit)
hence "¬ atm_of K ≼⇩t atm_of L⇩x"
by order
thus "¬ atm_of K ≼⇩t atm_of L⇩x ∧ ¬ atm_of K ≼⇩t atm_of (- L⇩x)"
unfolding atm_of_uminus conj_absorb .
next
show "trail_defined_cls Γ {#L ∈# x. L ≠ K⇩x#}"
using clauses_lt_E_almost_defined x_in' ‹x ≺⇩c E› x_max_lit by metis
qed
qed
moreover have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
using Γ_sorted step_hyps(9) by (metis sorted_wrt_dropWhile)
moreover have Γ'_lower: "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r'))"
proof -
have "linorder_trm.is_lower_fset (trail_atms Γ') (trail_atms Γ)"
unfolding linorder_trm.is_lower_set_iff
proof (intro conjI ballI impI)
show "fset (trail_atms Γ') ⊆ fset (trail_atms Γ)"
unfolding fset_trail_atms using ‹suffix Γ' Γ› by (metis image_mono set_mono_suffix)
next
obtain Γ'' where "Γ = Γ'' @ Γ'"
using ‹suffix Γ' Γ› unfolding suffix_def by metis
fix l x
assume "l |∈| trail_atms Γ'" and "x |∈| trail_atms Γ" and "x ≺⇩t l"
have "x |∈| trail_atms Γ'' ∨ x |∈| trail_atms Γ'"
using ‹x |∈| trail_atms Γ› unfolding ‹Γ = Γ'' @ Γ'› fset_trail_atms by auto
thus "x |∈| trail_atms Γ'"
proof (elim disjE)
assume "x |∈| trail_atms Γ''"
hence "l ≺⇩t x"
using Γ_sorted ‹l |∈| trail_atms Γ'›
unfolding ‹Γ = Γ'' @ Γ'› sorted_wrt_append fset_trail_atms by blast
hence False
using ‹x ≺⇩t l› by order
thus "x |∈| trail_atms Γ'" ..
next
assume "x |∈| trail_atms Γ'"
thus "x |∈| trail_atms Γ'" .
qed
qed
thus ?thesis
using Γ_lower
unfolding ‹atms_of_clss (N |∪| U⇩e⇩r) = atms_of_clss (N |∪| U⇩e⇩r')›
by order
qed
moreover have "∀DE. Some C = Some DE ⟶ (∀A |∈| trail_atms Γ'.
∃L. ord_res.is_maximal_lit L DE ∧ A ≼⇩t atm_of L)"
using atms_in_Γ'_lt_atm_K C_max_lit by fastforce
moreover have "∀Ln ∈ set Γ'. snd Ln = None ⟷ is_neg (fst Ln)"
using Γ_deci_iff_neg ‹suffix Γ' Γ›
by (metis (no_types, opaque_lifting) in_set_conv_decomp suffixE suffix_appendD)
moreover have "trail_true_cls Γ' C"
if "Ln ∈ set Γ'" and "snd Ln = None" and "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')" and "C ≺⇩c {#fst Ln#}"
for Ln C
proof -
have "Ln ∈ set Γ"
using ‹Ln ∈ set Γ'› ‹suffix Γ' Γ› set_mono_suffix by blast
have "C = eres D E ∨ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')›
unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
by simp
thus "trail_true_cls Γ' C"
proof (elim disjE)
assume "C = eres D E"
hence "K ≺⇩l fst Ln"
using ‹C ≺⇩c {#fst Ln#}› eres_max_lit
by (simp add: linorder_lit.is_maximal_in_mset_iff)
hence "atm_of K ≼⇩t atm_of (fst Ln)"
by (cases K; cases "fst Ln") simp_all
moreover have "atm_of (fst Ln) |∈| trail_atms Γ'"
using ‹Ln ∈ set Γ'› by (simp add: fset_trail_atms)
moreover have "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r')"
by (metis ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
atm_of_in_atms_of_clssI eres_max_lit finsert_iff linorder_lit.is_maximal_in_mset_iff)
ultimately have "atm_of K |∈| trail_atms Γ'"
using Γ'_lower
unfolding linorder_trm.is_lower_set_iff
by fastforce
moreover have "atm_of K |∉| trail_atms Γ'"
using atms_in_Γ'_lt_atm_K by blast
ultimately show "trail_true_cls Γ' C"
by contradiction
next
assume "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
hence "trail_true_cls Γ C"
using Γ_deci_ball_lt_true ‹Ln ∈ set Γ› ‹snd Ln = None› ‹C ≺⇩c {#fst Ln#}› by metis
then obtain L⇩C where "L⇩C ∈# C" and "trail_true_lit Γ L⇩C"
unfolding trail_true_cls_def by auto
hence "∀x ∈# C. x ≺⇩l fst Ln"
using ‹C ≺⇩c {#fst Ln#}›
unfolding multp_singleton_right[OF linorder_lit.transp_on_less]
by simp
hence "L⇩C ≺⇩l fst Ln"
using ‹L⇩C ∈# C› by metis
hence "atm_of L⇩C ≼⇩t atm_of (fst Ln)"
by (cases L⇩C; cases "fst Ln") simp_all
moreover have "atm_of (fst Ln) ≺⇩t atm_of K"
using atms_in_Γ'_lt_atm_K
by (simp add: fset_trail_atms that(1))
ultimately have "atm_of L⇩C ≺⇩t atm_of K"
by order
have "L⇩C ∈ fst ` set Γ"
using ‹trail_true_lit Γ L⇩C›
unfolding trail_true_lit_def .
hence "L⇩C ∈ fst ` set Γ'"
using mem_set_Γ'_iff
using ‹atm_of L⇩C ≺⇩t atm_of K› linorder_trm.not_le by auto
hence "trail_true_lit Γ' L⇩C"
unfolding trail_true_lit_def .
thus "trail_true_cls Γ' C"
using ‹L⇩C ∈# C›
unfolding trail_true_cls_def by auto
qed
qed
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
using Γ_prop_in ‹suffix Γ' Γ› set_mono_suffix ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r› by blast
moreover have "∀Ln ∈ set Γ'. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)"
using Γ_prop_greatest ‹suffix Γ' Γ› set_mono_suffix by blast
moreover have "∀Γ⇩1 L C Γ⇩0. Γ' = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
using Γ_prop_almost_false ‹suffix Γ' Γ›
by (metis (no_types, lifting) append.assoc suffix_def)
moreover have "∀Γ⇩1 L D Γ⇩0. Γ' = Γ⇩1 @ (L, Some D) # Γ⇩0 ⟶
(∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r'). C ≺⇩c D ⟶ trail_true_cls Γ⇩0 C)"
proof (intro allI impI ballI)
fix
Γ⇩1 Γ⇩0 :: "('f gliteral × 'f gclause option) list" and
L :: "'f gliteral" and
C⇩0 C⇩1 :: "'f gclause"
assume
Γ'_eq: "Γ' = Γ⇩1 @ (L, Some C⇩1) # Γ⇩0" and
C⇩0_in: "C⇩0 |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')" and
"C⇩0 ≺⇩c C⇩1"
have "C⇩0 = eres D E ∨ C⇩0 |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using C⇩0_in
unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
by simp
thus "trail_true_cls Γ⇩0 C⇩0"
proof (elim disjE)
assume "C⇩0 = eres D E"
have "¬ atm_of K ≼⇩t atm_of (fst (L, Some C⇩1))" and "(L, Some C⇩1) ∈ set Γ"
unfolding atomize_conj
using Γ'_eq ‹Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ›
using mem_set_dropWhile_conv_if_list_sorted_and_pred_monotone[OF Γ_sorted mono_atms_lt]
by (metis in_set_conv_decomp)
then have "¬ atm_of K ≼⇩t atm_of L"
by simp
hence "atm_of L ≺⇩t atm_of K"
by order
moreover have "linorder_lit.is_greatest_in_mset C⇩1 L"
using Γ_prop_greatest ‹(L, Some C⇩1) ∈ set Γ› by fastforce
ultimately have False
using ‹C⇩0 ≺⇩c C⇩1›
by (smt (verit) ‹C⇩0 = eres D E› eres_max_lit linorder_cls.dual_order.asym
linorder_lit.dual_order.strict_trans
linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset
linorder_lit.multp_if_maximal_less_that_maximal linorder_lit.not_less_iff_gr_or_eq
literal.collapse(1) literal.collapse(2) ord_res.less_lit_simps(1)
ord_res.less_lit_simps(4))
thus "trail_true_cls Γ⇩0 C⇩0" ..
next
assume "C⇩0 |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
thus "trail_true_cls Γ⇩0 C⇩0"
using Γ_prop_ball_lt_true Γ'_eq ‹C⇩0 ≺⇩c C⇩1›
by (metis (no_types, opaque_lifting) ‹suffix Γ' Γ› append_assoc suffixE)
qed
qed
ultimately show ?thesis
unfolding ‹s' = (U⇩e⇩r', ℱ, Γ', Some C)›
proof (intro ord_res_7_invars.intros)
have clause_true_in_Γ'_if: "trail_true_cls Γ' x" and
"⋀K⇩x. linorder_lit.is_maximal_in_mset x K⇩x ⟹
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r'). A ≺⇩t atm_of K⇩x ∧ A |∉| trail_atms Γ')"
if x_lt: "⋀DE. Some C = Some DE ⟶ x ≺⇩c DE" and x_in: "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
for x
proof -
have "x ≺⇩c C"
using x_lt by metis
hence "x ≺⇩c eres D E"
using ‹C ≺⇩c eres D E› by order
hence "x ≠ eres D E"
by order
have "x ≺⇩c E"
using ‹x ≺⇩c eres D E› ‹eres D E ≺⇩c E› by order
moreover have x_in': "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using x_in ‹x ≠ eres D E›
unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
by simp
ultimately have x_true: "trail_true_cls Γ x"
using clauses_lt_E_true by metis
then obtain L⇩x where "L⇩x ∈# x" and "trail_true_lit Γ L⇩x"
unfolding trail_true_cls_def by metis
have "L⇩x ≼⇩l - K"
using C_max_lit ‹x ≺⇩c C› ‹L⇩x ∈# x›
by (smt (verit, ccfv_threshold) asympD empty_not_add_mset ord_res.transp_less_lit insert_DiffM
linorder_lit.is_greatest_in_set_iff linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset
linorder_lit.is_maximal_in_mset_iff linorder_lit.is_maximal_in_set_eq_is_greatest_in_set
linorder_lit.is_maximal_in_set_iff linorder_lit.leI ord_res.asymp_less_cls
ord_res.multp_if_all_left_smaller transpE)
have mono_atms_lt: "monotone_on (set Γ) (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) (λx y. y ≤ x)
(λx. atm_of K ≼⇩t atm_of (fst x))"
proof (intro monotone_onI, unfold le_bool_def, intro impI)
fix x y
assume "atm_of (fst y) ≺⇩t atm_of (fst x)" and "atm_of K ≼⇩t atm_of (fst y)"
thus "atm_of K ≼⇩t atm_of (fst x)"
by order
qed
obtain Γ⇩1 Γ⇩0 where Γ_eq: "Γ = Γ⇩1 @ (- K, Some C) # Γ⇩0"
using ‹(- K, Some C) ∈ set Γ› by (metis split_list)
hence "trail_true_cls Γ⇩0 x"
using Γ_prop_ball_lt_true x_in' ‹x ≺⇩c C› by metis
then obtain L⇩x where "L⇩x ∈# x" and L⇩x_true: "trail_true_lit Γ⇩0 L⇩x"
unfolding trail_true_cls_def by auto
moreover have "Γ' = Γ⇩0"
proof -
have "Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) ((Γ⇩1 @ [(- K, Some C)]) @ Γ⇩0)"
unfolding ‹Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ› Γ_eq by simp
also have "… = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ⇩0"
proof (rule dropWhile_append2)
fix Ln :: "'f gterm literal × 'f gclause option"
assume "Ln ∈ set (Γ⇩1 @ [(- K, Some C)])"
moreover have "∀x∈set Γ⇩1. atm_of K ≺⇩t atm_of (fst x)"
using Γ_sorted by (simp add: Γ_eq sorted_wrt_append)
ultimately show "atm_of K ≼⇩t atm_of (fst Ln)"
using ‹is_neg K› by auto
qed
also have "… = Γ⇩0"
proof (cases Γ⇩0)
case Nil
thus ?thesis
by (simp add: dropWhile_eq_self_iff)
next
case (Cons Ln Γ⇩0')
hence "atm_of (fst Ln) ≺⇩t atm_of K"
using Γ_sorted by (simp add: Γ_eq sorted_wrt_append)
hence "¬ atm_of K ≼⇩t atm_of (fst Ln)"
by order
hence "¬ atm_of K ≼⇩t atm_of (fst (hd Γ⇩0))"
by (simp add: ‹Γ⇩0 = Ln # Γ⇩0'›)
thus ?thesis
by (simp add: dropWhile_eq_self_iff)
qed
finally show ?thesis .
qed
ultimately have "trail_true_lit Γ' L⇩x"
by argo
thus "trail_true_cls Γ' x"
using ‹L⇩x ∈# x› unfolding trail_true_cls_def by metis
fix K⇩x
assume x_max_lit: "ord_res.is_maximal_lit K⇩x x"
hence "K⇩x ≼⇩l K"
using ‹x ≺⇩c eres D E› eres_max_lit
using linorder_lit.multp_if_maximal_less_that_maximal by fastforce
hence "atm_of K⇩x ≼⇩t atm_of K"
by (cases K⇩x; cases K) simp_all
have "A |∈| trail_atms Γ'"
if A_lt: "A ≺⇩t atm_of K⇩x" and A_in: "A |∈| atms_of_clss (N |∪| U⇩e⇩r)" for A
unfolding ‹Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ›
proof (rule in_trail_atms_dropWhileI)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
next
show "monotone_on (set Γ) (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) (λx y. y ≤ x) (λx. atm_of K ≼⇩t atm_of (fst x))"
using mono_atms_lt .
next
show "¬ atm_of K ≼⇩t A"
using A_lt ‹atm_of K⇩x ≼⇩t atm_of K› by order
next
have "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K⇩x ∧ A |∉| trail_atms Γ)"
using no_undef_atm_lt_max_lit_if_lt_E ‹x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹x ≺⇩c E› x_max_lit
by metis
thus "A |∈| trail_atms Γ"
using A_in A_lt by metis
qed
thus "¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r'). A ≺⇩t atm_of K⇩x ∧ A |∉| trail_atms Γ')"
using ‹atms_of_clss (N |∪| U⇩e⇩r) = atms_of_clss (N |∪| U⇩e⇩r')› by metis
qed
thus
"∀x|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). (∀DE. Some C = Some DE ⟶ x ≺⇩c DE) ⟶
trail_true_cls Γ' x"
"∀x|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). (∀DE. Some C = Some DE ⟶ x ≺⇩c DE) ⟶
(∀K. ord_res.is_maximal_lit K x ⟶
¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r'). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ'))"
unfolding atomize_conj by metis
have "trail_true_cls Γ' {#K ∈# B. K ≠ L⇩B#} ∧ is_pos L⇩B"
if "Some C = Some C'" and
B_in: "B |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')" and
B_lt: "B ≺⇩c C'" and
B_max_lit: "linorder_lit.is_maximal_in_mset B L⇩B" and
L⇩B_undef: "¬ trail_defined_lit Γ' L⇩B"
for C' B L⇩B
proof -
have "C' = C"
using that by simp
hence "B ≺⇩c C"
using B_lt by order
hence "B ≺⇩c eres D E"
using ‹C ≺⇩c eres D E› by order
hence "B ≠ eres D E"
by order
hence "B |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using B_in ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
by simp
moreover have "B ≺⇩c E"
using ‹B ≺⇩c eres D E› ‹eres D E ≺⇩c E› by order
have "L⇩B ≼⇩l - K"
using ‹B ≺⇩c C› B_max_lit C_max_lit
by (metis asympD linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset linorder_lit.leI
linorder_lit.multp_if_maximal_less_that_maximal ord_res.asymp_less_cls)
hence "L⇩B ≺⇩l - K ∨ L⇩B = - K"
by simp
thus ?thesis
proof (elim disjE)
assume "L⇩B ≺⇩l - K"
hence "atm_of L⇩B ≺⇩t atm_of K"
using ‹is_neg K›
by (cases L⇩B; cases K) simp_all
have "trail_defined_lit Γ' L⇩B"
unfolding ‹Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ›
proof (intro trail_defined_lit_dropWhileI ballI)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
next
show "monotone_on (set Γ) (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) (λx y. y ≤ x)
(λx. atm_of K ≼⇩t atm_of (fst x))"
using mono_atms_lt .
next
have "¬ atm_of K ≼⇩t atm_of L⇩B"
using ‹atm_of L⇩B ≺⇩t atm_of K› by order
thus "¬ atm_of K ≼⇩t atm_of L⇩B ∧ ¬ atm_of K ≼⇩t atm_of (- L⇩B)"
by simp
next
have "trail_defined_lit Γ K"
by (metis map_of_eq_None_iff option.discI step_hyps(12) trail_defined_lit_def)
moreover have "atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)"
by (metis ‹atms_of_clss (N |∪| U⇩e⇩r) = atms_of_clss (N |∪| U⇩e⇩r')›
‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
atm_of_in_atms_of_clssI eres_max_lit finsertI1 linorder_lit.is_maximal_in_mset_iff)
moreover have "atm_of L⇩B |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using ‹B |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› B_max_lit atm_of_in_atms_of_clssI
unfolding linorder_lit.is_maximal_in_mset_iff
by metis
ultimately show "trail_defined_lit Γ L⇩B"
using ‹atm_of L⇩B ≺⇩t atm_of K› Γ_lower
unfolding trail_defined_lit_iff_trail_defined_atm
by (meson linorder_trm.is_lower_set_iff)
qed
hence False
using L⇩B_undef by contradiction
thus ?thesis ..
next
have "trail_true_cls Γ' B"
using clause_true_in_Γ'_if B_in ‹B ≺⇩c C› by blast
hence "trail_true_cls Γ' {#K ∈# B. K ≠ L⇩B#}"
using L⇩B_undef
by (smt (verit, best) mem_Collect_eq set_mset_filter trail_defined_lit_iff_true_or_false
trail_true_cls_def)
moreover assume "L⇩B = - K"
ultimately show "trail_true_cls Γ' {#K ∈# B. K ≠ L⇩B#} ∧ is_pos L⇩B"
using ‹is_neg K›
by (cases K) simp_all
qed
qed
thus "∀Da. Some C = Some Da ⟶
(∀x|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). x ≺⇩c Da ⟶ (∀L⇩C. ord_res.is_maximal_lit L⇩C x ⟶
¬ trail_defined_lit Γ' L⇩C ⟶ trail_true_cls Γ' {#K ∈# x. K ≠ L⇩C#} ∧ is_pos L⇩C))"
by metis
qed simp_all
qed
lemma rtranclp_ord_res_7_preserves_ord_res_7_invars:
assumes
step: "(ord_res_7 N)⇧*⇧* s s'" and
invars: "ord_res_7_invars N s"
shows "ord_res_7_invars N s'"
using step invars ord_res_7_preserves_invars
by (smt (verit, del_insts) rtranclp_induct)
lemma tranclp_ord_res_7_preserves_ord_res_7_invars:
assumes
step: "(ord_res_7 N)⇧+⇧+ s s'" and
invars: "ord_res_7_invars N s"
shows "ord_res_7_invars N s'"
using step invars ord_res_7_preserves_invars
by (smt (verit, del_insts) tranclp_induct)
lemma propagating_clause_almost_false:
assumes invars: "ord_res_7_invars N (U⇩e⇩r, ℱ, Γ, 𝒞)" and "(L, Some C) ∈ set Γ"
shows "trail_false_cls Γ {#K ∈# C. K ≠ L#}"
proof -
have "∀Γ⇩1 L C Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ⟶ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
using invars unfolding ord_res_7_invars_def by metis
hence "∃Γ⇩1 Γ⇩0. Γ = Γ⇩1 @ (L, Some C) # Γ⇩0 ∧ trail_false_cls Γ⇩0 {#K ∈# C. K ≠ L#}"
using ‹(L, Some C) ∈ set Γ› unfolding in_set_conv_decomp by metis
thus "trail_false_cls Γ {#K ∈# C. K ≠ L#}"
by (metis suffixI suffix_ConsD trail_false_cls_if_trail_false_suffix)
qed
lemma ex_ord_res_7_if_not_final:
assumes
not_final: "¬ ord_res_7_final (N, s)" and
invars: "ord_res_7_invars N s"
shows "∃s'. ord_res_7 N s s'"
proof -
obtain U⇩e⇩r ℱ Γ 𝒞 where "s = (U⇩e⇩r, ℱ, Γ, 𝒞)"
by (metis surj_pair)
note invars' = invars[unfolded ord_res_7_invars_def, rule_format, OF ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)›]
have Γ_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using invars' by argo
have Γ_consistent: "trail_consistent Γ"
using Γ_sorted trail_consistent_if_sorted_wrt_atoms by metis
have "distinct (map fst Γ)"
proof (rule distinct_if_sorted_wrt_asymp)
have "sorted_wrt (λx y. fst y ≺⇩l fst x) Γ"
proof (rule sorted_wrt_mono_rel)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
next
fix x y :: "'f gterm literal × 'f gterm literal multiset option"
assume "atm_of (fst y) ≺⇩t atm_of (fst x)"
thus "fst y ≺⇩l fst x"
by (cases "fst x"; cases "fst y") (simp_all only: literal.sel ord_res.less_lit_simps)
qed
thus "sorted_wrt (λx y. y ≺⇩l x) (map fst Γ)"
unfolding sorted_wrt_map .
next
show "asymp_on (set (map fst Γ)) (λx y. y ≺⇩l x)"
using linorder_lit.asymp_on_greater .
qed
hence map_of_Γ_eq_SomeI: "⋀x y. (x, y) ∈ set Γ ⟹ map_of Γ x = Some y"
by (metis map_of_is_SomeI)
have Γ_lower: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
using invars' by argo
obtain E where "𝒞 = Some E" and "E ≠ {#}"
using not_final[unfolded ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ord_res_7_final.simps, simplified]
by metis
have E_in: "E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using invars' ‹𝒞 = Some E› by metis
obtain L where E_max_lit: "ord_res.is_maximal_lit L E"
using ‹E ≠ {#}› linorder_lit.ex_maximal_in_mset by metis
show ?thesis
proof (cases "trail_false_cls Γ E")
case E_false: True
hence L_false: "trail_false_lit Γ L"
using E_max_lit unfolding linorder_lit.is_maximal_in_mset_iff trail_false_cls_def by metis
hence "∃opt. (- L, opt) ∈ set Γ"
by (auto simp: trail_false_lit_def)
have "¬ is_pos L"
proof (rule notI)
assume "is_pos L"
hence "is_neg (- L)"
by (metis ‹is_pos L› is_pos_neg_not_is_pos)
hence "(- L, None) ∈ set Γ"
using invars' ‹∃opt. (- L, opt) ∈ set Γ› by (metis prod.sel)
moreover have "E ≺⇩c {#- L#}"
using E_max_lit ‹is_pos L›
by (smt (verit, best) Neg_atm_of_iff add_mset_remove_trivial empty_iff
ord_res.less_lit_simps(4) linorder_cls.less_irrefl linorder_lit.is_greatest_in_mset_iff
linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset linorder_lit.less_linear
linorder_lit.multp_if_maximal_less_that_maximal literal.collapse(1)
ord_res.less_lit_simps(1) set_mset_empty uminus_literal_def union_single_eq_member)
ultimately have "trail_true_cls Γ E"
using invars' E_in by force
hence "¬ trail_false_cls Γ E"
by (metis Γ_consistent not_trail_true_cls_and_trail_false_cls)
thus False
using E_false by contradiction
qed
hence L_neg: "is_neg L"
by argo
then obtain D where "(- L, Some D) ∈ set Γ"
using invars' ‹is_neg L› ‹∃opt. (- L, opt) ∈ set Γ›
by (metis prod.sel is_pos_neg_not_is_pos not_Some_eq)
hence "map_of Γ (- L) = Some (Some D)"
using map_of_Γ_eq_SomeI by metis
have "∃Γ⇩1 Γ⇩0. Γ = Γ⇩1 @ (- L, Some D) # Γ⇩0 ∧ trail_false_cls Γ⇩0 {#K ∈# D. K ≠ - L#}"
using invars' ‹(- L, Some D) ∈ set Γ› propagating_clause_almost_false
unfolding in_set_conv_decomp by metis
have D_almost_false: "trail_false_cls Γ {#K ∈# D. K ≠ - L#}"
using invars ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹(- L, Some D) ∈ set Γ› propagating_clause_almost_false
by metis
show ?thesis
proof (cases "eres D E = {#}")
case True
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = Some E›
using E_false E_max_lit L_neg ‹map_of Γ (- L) = Some (Some D)›
using ord_res_7.resolution_bot by metis
next
case False
then obtain K where eres_max_lit: "ord_res.is_maximal_lit K (eres D E)"
using linorder_lit.ex_maximal_in_mset by metis
hence "K ∈# eres D E"
unfolding linorder_lit.is_maximal_in_mset_iff by argo
hence "K ∈# D ∧ K ≠ - L ∨ K ∈# E"
using strong_lit_in_one_of_resolvents_if_in_eres[OF E_max_lit] by metis
hence K_false: "trail_false_lit Γ K"
using D_almost_false E_false unfolding trail_false_cls_def by auto
hence "∃opt. (- K, opt) ∈ set Γ"
by (auto simp: trail_false_lit_def)
show ?thesis
proof (cases K)
case (Pos A⇩K)
hence "is_pos K"
by simp
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = Some E›
using E_false E_max_lit L_neg ‹map_of Γ (- L) = Some (Some D)› False eres_max_lit
using ord_res_7.resolution_pos by metis
next
case (Neg A⇩K)
hence "is_neg K"
by simp
then obtain C where "(- K, Some C) ∈ set Γ"
using invars' ‹is_neg L› ‹∃opt. (- K, opt) ∈ set Γ›
by (metis prod.sel is_pos_neg_not_is_pos not_Some_eq)
hence "map_of Γ (- K) = Some (Some C)"
using map_of_Γ_eq_SomeI by metis
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = Some E›
using E_false E_max_lit L_neg ‹map_of Γ (- L) = Some (Some D)› False eres_max_lit
‹is_neg K›
using ord_res_7.resolution_neg by metis
qed
qed
next
case E_not_false: False
show ?thesis
proof (cases "∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of L ∧ A |∉| trail_atms Γ")
case True
then obtain A where A_least: "linorder_trm.is_least_in_fset
{|A |∈| atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of L ∧ A |∉| trail_atms Γ|} A"
by (metis (no_types, lifting) bot_fset.rep_eq empty_iff ffmember_filter
linorder_trm.ex_least_in_fset)
show ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = Some E›
using ord_res_7.decide_neg[OF E_not_false E_max_lit A_least refl, of ℱ]
by metis
next
case nex_undef_atm_lt_L: False
show ?thesis
proof (cases "trail_defined_lit Γ L")
case True
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = Some E›
using ord_res_7.skip_defined[OF E_not_false E_max_lit nex_undef_atm_lt_L]
by metis
next
case L_undef: False
show ?thesis
proof (cases L)
case L_eq: (Pos A⇩L)
hence L_pos: "is_pos L"
by simp
show ?thesis
proof (cases "trail_false_cls Γ {#K ∈# E. K ≠ L#}")
case E_almost_false: True
show ?thesis
proof (cases "ord_res.is_strictly_maximal_lit L E")
case True
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = Some E›
using ord_res_7.production[OF E_not_false E_max_lit nex_undef_atm_lt_L L_undef L_pos
E_almost_false]
by metis
next
case False
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = Some E›
using ord_res_7.factoring[OF E_not_false E_max_lit nex_undef_atm_lt_L L_undef L_pos
E_almost_false]
by metis
qed
next
case E_not_almost_false: False
show ?thesis
proof (cases "∃D|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). E ≺⇩c D")
case True
then obtain F where "linorder_cls.is_least_in_fset
(ffilter ((≺⇩c) E) (iefac ℱ |`| (N |∪| U⇩e⇩r))) F"
by (metis bot_fset.rep_eq empty_iff ffmember_filter linorder_cls.ex1_least_in_fset)
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = Some E›
using ord_res_7.skip_undefined_pos[OF E_not_false E_max_lit nex_undef_atm_lt_L L_undef
L_pos E_not_almost_false]
by metis
next
case False
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = Some E›
using ord_res_7.skip_undefined_pos_ultimate[OF E_not_false E_max_lit
nex_undef_atm_lt_L L_undef L_pos E_not_almost_false]
by metis
qed
qed
next
case L_eq: (Neg A⇩L)
hence "is_neg L"
by simp
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = Some E›
using ord_res_7.skip_undefined_neg[OF E_not_false E_max_lit nex_undef_atm_lt_L L_undef]
by metis
qed
qed
qed
qed
qed
lemma ord_res_7_safe_state_if_invars:
fixes N :: "'f gclause fset" and s
assumes invars: "ord_res_7_invars N s"
shows "safe_state (constant_context ord_res_7) ord_res_7_final (N, s)"
using safe_state_constant_context_if_invars[where
ℛ = ord_res_7 and ℱ = ord_res_7_final and ℐ = ord_res_7_invars]
using ord_res_7_preserves_invars ex_ord_res_7_if_not_final invars by metis
end
end