Theory ORD_RES_10
theory ORD_RES_10
imports ORD_RES_8
begin
section ‹ORD-RES-10 (propagate iff a conflict is produced)›
type_synonym 'f ord_res_10_state =
"'f gclause fset ×'f gclause fset × 'f gclause fset × ('f gliteral × 'f gclause option) list"
context simulation_SCLFOL_ground_ordered_resolution begin
inductive ord_res_10 where
decide_neg: "
¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C) ⟹
linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A ⟹
¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)) ⟹
Γ' = (Neg A, None) # Γ ⟹
ord_res_10 N (U⇩e⇩r, ℱ, Γ) (U⇩e⇩r, ℱ, Γ')" |
decide_pos: "
¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C) ⟹
linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A ⟹
linorder_cls.is_least_in_fset {|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r).
clause_could_propagate Γ C (Pos A)|} C ⟹
Γ' = (Pos A, None) # Γ ⟹
¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ' C) ⟹
ℱ' = (if linorder_lit.is_greatest_in_mset C (Pos A) then ℱ else finsert C ℱ) ⟹
ord_res_10 N (U⇩e⇩r, ℱ, Γ) (U⇩e⇩r, ℱ', Γ')" |
propagate: "
¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C) ⟹
linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A ⟹
linorder_cls.is_least_in_fset {|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r).
clause_could_propagate Γ C (Pos A)|} C ⟹
Γ' = (Pos A, Some (efac C)) # Γ ⟹
(∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ' C) ⟹
ℱ' = (if linorder_lit.is_greatest_in_mset C (Pos A) then ℱ else finsert C ℱ) ⟹
ord_res_10 N (U⇩e⇩r, ℱ, Γ) (U⇩e⇩r, ℱ', Γ')" |
resolution: "
linorder_cls.is_least_in_fset {|D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ D|} D ⟹
linorder_lit.is_maximal_in_mset D (Neg A) ⟹
map_of Γ (Pos A) = Some (Some C) ⟹
U⇩e⇩r' = finsert (eres C D) U⇩e⇩r ⟹
Γ' = dropWhile (λLn. ∀K.
linorder_lit.is_maximal_in_mset (eres C D) K ⟶ atm_of K ≼⇩t atm_of (fst Ln)) Γ ⟹
ord_res_10 N (U⇩e⇩r, ℱ, Γ) (U⇩e⇩r', ℱ, Γ')"
lemma right_unique_ord_res_10:
fixes N :: "'f gclause fset"
shows "right_unique (ord_res_10 N)"
proof (rule right_uniqueI)
fix x y z
assume step1: "ord_res_10 N x y" and step2: "ord_res_10 N x z"
show "y = z"
using step1
proof (cases N x y rule: ord_res_10.cases)
case hyps1: (decide_neg ℱ U⇩e⇩r Γ A1 Γ1')
show ?thesis
using step2 unfolding ‹x = (U⇩e⇩r, ℱ, Γ)›
proof (cases N "(U⇩e⇩r, ℱ, Γ)" z rule: ord_res_10.cases)
case (decide_neg A Γ')
with hyps1 show ?thesis
by (metis (no_types, lifting) linorder_trm.dual_order.asym
linorder_trm.is_least_in_ffilter_iff)
next
case (decide_pos A C Γ' ℱ')
with hyps1 have False
by (metis (no_types, lifting) linorder_cls.is_least_in_ffilter_iff
linorder_trm.dual_order.asym linorder_trm.is_least_in_ffilter_iff)
thus ?thesis ..
next
case (propagate A C Γ' ℱ')
with hyps1 have False
by (metis (no_types, lifting) linorder_cls.is_least_in_ffilter_iff
linorder_trm.dual_order.asym linorder_trm.is_least_in_ffilter_iff)
thus ?thesis ..
next
case (resolution D A C U⇩e⇩r' Γ')
with hyps1 have False
by (metis (no_types, opaque_lifting) linorder_cls.is_least_in_ffilter_iff)
thus ?thesis ..
qed
next
case hyps1: (decide_pos ℱ U⇩e⇩r Γ A1 C1 Γ1' ℱ1')
show ?thesis
using step2 unfolding ‹x = (U⇩e⇩r, ℱ, Γ)›
proof (cases N "(U⇩e⇩r, ℱ, Γ)" z rule: ord_res_10.cases)
case (decide_neg A Γ')
with hyps1 have False
by (metis (no_types, lifting) linorder_cls.is_least_in_ffilter_iff
linorder_trm.dual_order.asym linorder_trm.is_least_in_ffilter_iff)
thus ?thesis ..
next
case (decide_pos A C Γ' ℱ')
with hyps1 show ?thesis
by (metis (no_types, lifting) linorder_cls.Uniq_is_least_in_fset
linorder_trm.Uniq_is_least_in_fset the1_equality')
next
case hyps2: (propagate A C Γ' ℱ')
have "A1 = A"
using hyps1 hyps2
by (metis (no_types, lifting) linorder_trm.dual_order.asym
linorder_trm.is_least_in_ffilter_iff)
hence "trail_false_cls Γ1' = trail_false_cls Γ'"
using hyps1 hyps2
unfolding trail_false_cls_def trail_false_lit_def
by simp
hence False
using hyps1 hyps2 by argo
thus ?thesis ..
next
case (resolution D A C U⇩e⇩r' Γ')
with hyps1 have False
by (meson linorder_cls.is_least_in_ffilter_iff)
thus ?thesis ..
qed
next
case hyps1: (propagate ℱ U⇩e⇩r Γ A1 C1 Γ1' ℱ1')
show ?thesis
using step2 unfolding ‹x = (U⇩e⇩r, ℱ, Γ)›
proof (cases N "(U⇩e⇩r, ℱ, Γ)" z rule: ord_res_10.cases)
case (decide_neg A Γ')
with hyps1 have False
by (metis (no_types, lifting) linorder_cls.is_least_in_ffilter_iff
linorder_trm.dual_order.asym linorder_trm.is_least_in_ffilter_iff)
thus ?thesis ..
next
case hyps2: (decide_pos A C Γ' ℱ')
have "A1 = A"
using hyps1 hyps2
by (metis (no_types, lifting) linorder_trm.dual_order.asym
linorder_trm.is_least_in_ffilter_iff)
hence "trail_false_cls Γ1' = trail_false_cls Γ'"
using hyps1 hyps2
unfolding trail_false_cls_def trail_false_lit_def
by simp
hence False
using hyps1 hyps2 by argo
thus ?thesis ..
next
case (propagate A C Γ' ℱ')
with hyps1 show ?thesis
by (metis (no_types, lifting) linorder_cls.Uniq_is_least_in_fset
linorder_trm.Uniq_is_least_in_fset the1_equality')
next
case (resolution D A C U⇩e⇩r' Γ')
with hyps1 have False
by (meson linorder_cls.is_least_in_ffilter_iff)
thus ?thesis ..
qed
next
case hyps1: (resolution Γ ℱ U⇩e⇩r D1 A1 C1 U⇩e⇩r1' Γ1')
show ?thesis
using step2 unfolding ‹x = (U⇩e⇩r, ℱ, Γ)›
proof (cases N "(U⇩e⇩r, ℱ, Γ)" z rule: ord_res_10.cases)
case (decide_neg A Γ')
with hyps1 have False
by (meson linorder_cls.is_least_in_ffilter_iff)
thus ?thesis ..
next
case (decide_pos A C Γ' ℱ')
with hyps1 have False
by (meson linorder_cls.is_least_in_ffilter_iff)
thus ?thesis ..
next
case (propagate A C Γ' ℱ')
with hyps1 have False
by (meson linorder_cls.is_least_in_ffilter_iff)
thus ?thesis ..
next
case hyps2: (resolution D A C U⇩e⇩r' Γ')
have "D1 = D"
using hyps1 hyps2
by (metis (no_types, opaque_lifting) linorder_cls.Uniq_is_least_in_fset Uniq_D)
have "A1 = A"
using hyps1 hyps2
unfolding ‹D1 = D›
by (metis (mono_tags, opaque_lifting) Uniq_D linorder_lit.Uniq_is_maximal_in_mset
literal.sel(2))
have "C1 = C"
using hyps1 hyps2
unfolding ‹A1 = A›
by simp
show ?thesis
using hyps1 hyps2
unfolding ‹D1 = D› ‹A1 = A› ‹C1 = C›
by argo
qed
qed
qed
sublocale ord_res_10_semantics: semantics where
step = "constant_context ord_res_10" and
final = ord_res_8_final
proof unfold_locales
fix S :: "'f ord_res_10_state"
obtain
N U⇩e⇩r ℱ :: "'f gclause fset" and
Γ :: "('f gliteral × 'f gclause option) list" where
S_def: "S = (N, U⇩e⇩r, ℱ, Γ)"
by (metis prod.exhaust)
assume "ord_res_8_final S"
hence "∄x. ord_res_10 N (U⇩e⇩r, ℱ, Γ) x"
unfolding S_def
proof (cases "(N, U⇩e⇩r, ℱ, Γ)" rule: ord_res_8_final.cases)
case model_found
have "∄A. linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A"
using ‹¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A |∉| trail_atms Γ)›
using linorder_trm.is_least_in_ffilter_iff by fastforce
moreover have "∄C. linorder_cls.is_least_in_fset
(ffilter (trail_false_cls Γ) (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
using ‹¬ fBex (iefac ℱ |`| (N |∪| U⇩e⇩r)) (trail_false_cls Γ)›
by (metis linorder_cls.is_least_in_ffilter_iff)
ultimately show ?thesis
unfolding ord_res_10.simps by blast
next
case contradiction_found
hence "∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C"
using trail_false_cls_mempty by metis
moreover have "∄D A. linorder_cls.is_least_in_fset (ffilter (trail_false_cls Γ)
(iefac ℱ |`| (N |∪| U⇩e⇩r))) D ∧ ord_res.is_maximal_lit (Neg A) D"
by (metis empty_iff linorder_cls.is_least_in_ffilter_iff linorder_cls.leD
linorder_lit.is_maximal_in_mset_iff local.contradiction_found(1) mempty_lesseq_cls
set_mset_empty trail_false_cls_mempty)
ultimately show ?thesis
unfolding ord_res_10.simps by blast
qed
thus "finished (constant_context ord_res_10) S"
by (simp add: S_def finished_def constant_context.simps)
qed
inductive ord_res_10_invars for N where
"ord_res_10_invars N (U⇩e⇩r, ℱ, Γ)" if
"sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
"∀Ln ∈ set Γ. ∀C. snd Ln = Some C ⟶ linorder_lit.is_greatest_in_mset C (fst Ln)" and
"linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
"∀Ln Γ'. Γ = Ln # Γ' ⟶
(snd Ln ≠ None ⟷ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C)) ∧
(snd Ln ≠ None ⟶ is_pos (fst Ln)) ∧
(∀C. snd Ln = Some C ⟶ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)) ∧
(∀C. snd Ln = Some C ⟶ clause_could_propagate Γ' C (fst Ln)) ∧
(∀x ∈ set Γ'. snd x = None)" and
"∀Γ⇩1 Ln Γ⇩0. Γ = Γ⇩1 @ Ln # Γ⇩0 ⟶
snd Ln = None ⟶ ¬(∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls (Ln # Γ⇩0) C)"
lemma ord_res_10_preserves_invars:
assumes
step: "ord_res_10 N s s'" and
invars: "ord_res_10_invars N s"
shows "ord_res_10_invars N s'"
using invars
proof (cases N s rule: ord_res_10_invars.cases)
case invars: (1 Γ U⇩e⇩r ℱ)
note Γ_sorted = ‹sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ›
note Γ_lower = ‹linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))›
have "trail_consistent Γ"
using Γ_sorted trail_consistent_if_sorted_wrt_atoms by metis
show ?thesis
using step unfolding ‹s = (U⇩e⇩r, ℱ, Γ)›
proof (cases N "(U⇩e⇩r, ℱ, Γ)" s' rule: ord_res_10.cases)
case step_hyps: (decide_neg A Γ')
have
A_in: "A |∈| atms_of_clss (N |∪| U⇩e⇩r)" and
A_gt: "∀A⇩1|∈|trail_atms Γ. A⇩1 ≺⇩t A" and
A_lt: "∀y|∈|atms_of_clss (N |∪| U⇩e⇩r).
y ≠ A ⟶ (∀A⇩1|∈|trail_atms Γ. A⇩1 ≺⇩t y) ⟶ A ≺⇩t y"
using ‹linorder_trm.is_least_in_fset _ A›
unfolding atomize_conj linorder_trm.is_least_in_ffilter_iff
by argo
have "trail_atms Γ' = finsert A (trail_atms Γ)"
unfolding ‹Γ' = (Neg A, _) # Γ› by simp
show ?thesis
unfolding ‹s' = (_, _, _)›
proof (intro ord_res_10_invars.intros allI impI conjI)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
unfolding ‹Γ' = (Neg A, None) # Γ› sorted_wrt.simps
proof (intro conjI ballI)
fix Ln :: "'f gliteral × 'f gclause option"
assume "Ln ∈ set Γ"
hence "atm_of (fst Ln) |∈| trail_atms Γ"
by (simp add: fset_trail_atms)
thus "atm_of (fst Ln) ≺⇩t atm_of (fst (Neg A, None))"
unfolding prod.sel literal.sel
using A_gt by metis
next
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
qed
show "∀Ln∈set Γ'. ∀C. snd Ln = Some C ⟶ ord_res.is_strictly_maximal_lit (fst Ln) C"
unfolding ‹Γ' = (_, None) # Γ›
using invars by simp
show "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r))"
unfolding ‹trail_atms Γ' = finsert A (trail_atms Γ)› finsert.rep_eq
proof (intro linorder_trm.is_lower_set_insertI ballI impI)
show "A |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using A_in .
next
fix w :: "'f gterm"
assume "w |∈| atms_of_clss (N |∪| U⇩e⇩r)" and "w ≺⇩t A"
thus "w |∈| trail_atms Γ"
by (metis A_lt Γ_lower linorder_trm.dual_order.asym linorder_trm.neq_iff
linorder_trm.not_in_lower_setI)
next
show "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
using Γ_lower .
qed
{
fix
Ln :: "'f gliteral × 'f gclause option" and
Γ'' :: "('f gliteral × 'f gclause option) list"
assume "Γ' = Ln # Γ''"
have "snd Ln = None"
using ‹Γ' = Ln # Γ''› step_hyps by auto
moreover have "¬ (∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls ((Neg A, None) # Γ) C)"
proof (rule notI , elim bexE)
fix C :: "'f gclause"
assume
C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
C_false: "trail_false_cls ((Neg A, None) # Γ) C"
have "clause_could_propagate Γ C (Pos A)"
unfolding clause_could_propagate_def
proof (intro conjI)
show "¬ trail_defined_lit Γ (Pos A)"
unfolding trail_defined_lit_iff_trail_defined_atm literal.sel
by (metis A_gt linorder_trm.less_irrefl)
next
show "ord_res.is_maximal_lit (Pos A) C"
unfolding linorder_lit.is_maximal_in_mset_iff
proof (intro conjI ballI impI)
have "¬ trail_false_cls Γ C"
using step_hyps C_in by metis
thus "Pos A ∈# C"
using C_false by (metis subtrail_falseI uminus_Neg)
next
fix L :: "'f gliteral"
assume L_in: "L ∈# C" and L_neq: "L ≠ Pos A"
have "trail_false_lit ((Neg A, None) # Γ) L"
using C_false L_in unfolding trail_false_cls_def by metis
hence "- L ∈ fst ` set Γ"
unfolding trail_false_lit_def
using L_neq
by (cases L) simp_all
hence "trail_defined_lit Γ L"
unfolding trail_defined_lit_def by argo
hence "atm_of L |∈| trail_atms Γ"
unfolding trail_defined_lit_iff_trail_defined_atm .
moreover have "∀A⇩1|∈|trail_atms Γ. A⇩1 ≺⇩t A"
using step_hyps unfolding linorder_trm.is_least_in_ffilter_iff by argo
ultimately have "atm_of L ≺⇩t A"
by metis
hence "L ≼⇩l Pos A"
by (cases L) simp_all
thus "¬ Pos A ≺⇩l L"
by order
qed
next
show "trail_false_cls Γ {#K ∈# C. K ≠ Pos A#}"
using C_false
unfolding trail_false_cls_def trail_false_lit_def
by (smt (verit, ccfv_SIG) mem_Collect_eq set_mset_filter subtrail_falseI
trail_false_cls_def trail_false_lit_def uminus_Neg)
qed
moreover have "¬ clause_could_propagate Γ C (Pos A)"
using C_in step_hyps by metis
ultimately show False
by contradiction
qed
ultimately show "(snd Ln ≠ None) = (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ' C)"
unfolding ‹Γ' = (Neg A, None) # Γ› by argo
show "snd Ln ≠ None ⟹ is_pos (fst Ln)"
using ‹snd Ln = None› by argo
have "¬ fBex (iefac ℱ |`| (N |∪| U⇩e⇩r)) (trail_false_cls Γ)"
using step_hyps by argo
hence "∀x∈set Γ. snd x = None"
using invars by (metis list.set_cases)
thus "∀x ∈ set Γ''. snd x = None"
using ‹Γ' = Ln # Γ''› ‹Γ' = (Neg A, None) # Γ› by simp
show "⋀C. snd Ln = Some C ⟹ clause_could_propagate Γ'' C (fst Ln)"
using ‹Γ' = Ln # Γ''› ‹Γ' = (Neg A, None) # Γ› by force
show "⋀D. snd Ln = Some D ⟹ D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using ‹Γ' = Ln # Γ''› ‹Γ' = (Neg A, None) # Γ› by force
}
have "¬ (∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls ((Neg A, None) # Γ) C)"
proof (intro notI , elim bexE)
fix C :: "'f gclause"
assume
C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
C_false: "trail_false_cls ((Neg A, None) # Γ) C"
have "clause_could_propagate Γ C (Pos A)"
unfolding clause_could_propagate_def
proof (intro conjI)
show "¬ trail_defined_lit Γ (Pos A)"
unfolding trail_defined_lit_iff_trail_defined_atm
by (metis A_gt linorder_trm.less_irrefl literal.sel(1))
next
have "¬ trail_false_cls Γ C"
using C_in step_hyps by metis
thus "trail_false_cls Γ {#K ∈# C. K ≠ Pos A#}"
by (smt (verit) C_false mem_Collect_eq set_mset_filter subtrail_falseI
trail_false_cls_def uminus_Neg)
show "ord_res.is_maximal_lit (Pos A) C"
unfolding linorder_lit.is_maximal_in_mset_iff
proof (intro conjI ballI impI)
show "Pos A ∈# C"
by (metis C_false ‹¬ trail_false_cls Γ C› subtrail_falseI uminus_Neg)
next
fix L
assume "L ∈# C" and "L ≠ Pos A"
hence "atm_of L |∈| trail_atms Γ"
using ‹trail_false_cls Γ {#K ∈# C. K ≠ Pos A#}›
using trail_defined_lit_iff_trail_defined_atm trail_defined_lit_iff_true_or_false
trail_false_cls_filter_mset_iff by blast
hence "atm_of L ≺⇩t A"
using A_gt by metis
hence "L ≺⇩l Pos A"
by (cases L) simp_all
thus "¬ Pos A ≺⇩l L"
by order
qed
qed
moreover have "¬ clause_could_propagate Γ C (Pos A)"
using C_in step_hyps by metis
ultimately show False
by contradiction
qed
thus "⋀Γ⇩1 Ln Γ⇩0. Γ' = Γ⇩1 @ Ln # Γ⇩0 ⟹ snd Ln = None ⟹
¬ (∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls (Ln # Γ⇩0) C)"
unfolding ‹Γ' = (_, None) # Γ›
by (metis suffixI trail_false_cls_if_trail_false_suffix)
qed
next
case step_hyps: (decide_pos A C Γ' ℱ')
have
A_in: "A |∈| atms_of_clss (N |∪| U⇩e⇩r)" and
A_gt: "∀A⇩1|∈|trail_atms Γ. A⇩1 ≺⇩t A" and
A_lt: "∀y|∈|atms_of_clss (N |∪| U⇩e⇩r).
y ≠ A ⟶ (∀A⇩1|∈|trail_atms Γ. A⇩1 ≺⇩t y) ⟶ A ≺⇩t y"
using ‹linorder_trm.is_least_in_fset _ A›
unfolding atomize_conj linorder_trm.is_least_in_ffilter_iff
by argo
have "trail_atms Γ' = finsert A (trail_atms Γ)"
unfolding ‹Γ' = (Pos A, _) # Γ› by simp
show ?thesis
unfolding ‹s' = (_, _, _)›
proof (intro ord_res_10_invars.intros allI impI conjI)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
unfolding ‹Γ' = (Pos A, None) # Γ› sorted_wrt.simps
proof (intro conjI ballI)
fix Ln :: "'f gliteral × 'f gclause option"
assume "Ln ∈ set Γ"
hence "atm_of (fst Ln) |∈| trail_atms Γ"
by (simp add: fset_trail_atms)
thus "atm_of (fst Ln) ≺⇩t atm_of (fst (Pos A, None))"
unfolding prod.sel literal.sel
using A_gt by metis
next
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
qed
show "∀Ln∈set Γ'. ∀C. snd Ln = Some C ⟶ ord_res.is_strictly_maximal_lit (fst Ln) C"
unfolding ‹Γ' = (_, None) # Γ›
using invars by simp
show "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r))"
unfolding ‹trail_atms Γ' = finsert A (trail_atms Γ)› finsert.rep_eq
proof (intro linorder_trm.is_lower_set_insertI ballI impI)
show "A |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using A_in .
next
fix w :: "'f gterm"
assume "w |∈| atms_of_clss (N |∪| U⇩e⇩r)" and "w ≺⇩t A"
thus "w |∈| trail_atms Γ"
by (metis A_lt Γ_lower linorder_trm.dual_order.asym linorder_trm.neq_iff
linorder_trm.not_in_lower_setI)
next
show "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
using Γ_lower .
qed
{
fix Ln and Γ''
assume "Γ' = Ln # Γ''"
have "snd Ln = None"
using ‹Γ' = Ln # Γ''› step_hyps by auto
moreover have "¬ (∃C|∈|iefac ℱ' |`| (N |∪| U⇩e⇩r). trail_false_cls ((Pos A, None) # Γ) C)"
proof (rule notI , elim bexE)
fix D :: "'f gclause"
assume D_in: "D |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
hence "D = efac C ∨ D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
unfolding ‹ℱ' = (if ord_res.is_strictly_maximal_lit (Pos A) C then ℱ else finsert C ℱ)›
by (smt (z3) fimage_iff finsert_iff iefac_def)
hence "¬ trail_false_cls Γ' D"
proof (elim disjE)
assume "D = efac C"
hence "trail_false_cls Γ' D ⟷ trail_false_cls Γ' C"
by (simp add: trail_false_cls_def)
moreover have "¬ trail_false_cls Γ' C"
using step_hyps unfolding linorder_cls.is_least_in_ffilter_iff by metis
ultimately show "¬ trail_false_cls Γ' D"
by argo
next
assume "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
thus "¬ trail_false_cls Γ' D"
using step_hyps by metis
qed
moreover assume "trail_false_cls ((Pos A, None) # Γ) D"
ultimately show False
unfolding ‹Γ' = (Pos A, None) # Γ›
by contradiction
qed
ultimately show "snd Ln ≠ None ⟷
(∃C|∈|iefac ℱ' |`| (N |∪| U⇩e⇩r). trail_false_cls Γ' C)"
unfolding ‹Γ' = (Pos A, None) # Γ› by argo
show "snd Ln ≠ None ⟹ is_pos (fst Ln)"
using ‹snd Ln = None› by argo
have "¬ fBex (iefac ℱ |`| (N |∪| U⇩e⇩r)) (trail_false_cls Γ)"
using step_hyps by argo
hence "∀x∈set Γ. snd x = None"
using invars by (metis list.set_cases)
thus "∀x∈set Γ''. snd x = None"
using ‹Γ' = Ln # Γ''› ‹Γ' = (Pos A, None) # Γ› by simp
show "⋀C. snd Ln = Some C ⟹ clause_could_propagate Γ'' C (fst Ln)"
using ‹Γ' = Ln # Γ''› ‹Γ' = (Pos A, None) # Γ› by force
show "⋀D. snd Ln = Some D ⟹ D |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
using ‹Γ' = Ln # Γ''› ‹Γ' = (Pos A, None) # Γ› by force
}
show "⋀Γ⇩1 Ln Γ⇩0. Γ' = Γ⇩1 @ Ln # Γ⇩0 ⟹ snd Ln = None ⟹
¬ (∃C|∈|iefac ℱ' |`| (N |∪| U⇩e⇩r). trail_false_cls (Ln # Γ⇩0) C)"
using step_hyps
unfolding bex_trail_false_cls_simp
by (meson suffixI trail_false_cls_if_trail_false_suffix)
qed
next
case step_hyps: (propagate A C Γ' ℱ')
have
A_in: "A |∈| atms_of_clss (N |∪| U⇩e⇩r)" and
A_gt: "∀A⇩1|∈|trail_atms Γ. A⇩1 ≺⇩t A" and
A_lt: "∀y|∈|atms_of_clss (N |∪| U⇩e⇩r).
y ≠ A ⟶ (∀A⇩1|∈|trail_atms Γ. A⇩1 ≺⇩t y) ⟶ A ≺⇩t y"
using ‹linorder_trm.is_least_in_fset _ A›
unfolding atomize_conj linorder_trm.is_least_in_ffilter_iff
by argo
have
C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
C_prop: "clause_could_propagate Γ C (Pos A)" and
C_lt: "∀D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r).
D ≠ C ⟶ clause_could_propagate Γ D (Pos A) ⟶ C ≺⇩c D"
using ‹linorder_cls.is_least_in_fset _ C›
unfolding atomize_conj linorder_cls.is_least_in_ffilter_iff by argo
have "trail_atms Γ' = finsert A (trail_atms Γ)"
unfolding ‹Γ' = (Pos A, _) # Γ› by simp
show ?thesis
unfolding ‹s' = (_, _, _)›
proof (intro ord_res_10_invars.intros allI impI conjI)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
unfolding ‹Γ' = (Pos A, _) # Γ› sorted_wrt.simps
proof (intro conjI ballI)
fix Ln :: "'f gliteral × 'f gclause option"
assume "Ln ∈ set Γ"
hence "atm_of (fst Ln) |∈| trail_atms Γ"
by (simp add: fset_trail_atms)
thus "atm_of (fst Ln) ≺⇩t atm_of (fst (Pos A, Some (efac C)))"
unfolding prod.sel literal.sel
using A_gt by metis
next
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
using Γ_sorted .
qed
show "∀Ln∈set Γ'. ∀C. snd Ln = Some C ⟶ ord_res.is_strictly_maximal_lit (fst Ln) C"
unfolding ‹Γ' = (Pos A, Some (efac C)) # Γ›
using invars step_hyps
by (simp add: clause_could_propagate_def greatest_literal_in_efacI
linorder_cls.is_least_in_ffilter_iff)
show "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r))"
unfolding ‹trail_atms Γ' = finsert A (trail_atms Γ)› finsert.rep_eq
proof (intro linorder_trm.is_lower_set_insertI ballI impI)
show "A |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using A_in .
next
fix w :: "'f gterm"
assume "w |∈| atms_of_clss (N |∪| U⇩e⇩r)" and "w ≺⇩t A"
thus "w |∈| trail_atms Γ"
by (metis A_lt Γ_lower linorder_trm.dual_order.asym linorder_trm.neq_iff
linorder_trm.not_in_lower_setI)
next
show "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
using Γ_lower .
qed
{
fix Ln and Γ''
assume "Γ' = Ln # Γ''"
hence "Ln = (Pos A, Some (efac C))" and "Γ'' = Γ"
using ‹Γ' = (Pos A, Some (efac C)) # Γ› by simp_all
obtain D where D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and D_false: "trail_false_cls Γ' D"
using step_hyps by metis
have "(∃C|∈|iefac ℱ' |`| (N |∪| U⇩e⇩r). trail_false_cls Γ' C)"
proof (rule bexI)
show "trail_false_cls Γ' D"
using D_false .
next
have "¬ trail_false_cls Γ' C"
by (metis clause_could_propagate_def linorder_cls.is_least_in_ffilter_iff
linorder_lit.is_maximal_in_mset_iff ord_res.less_lit_simps(2) reflclp_iff
step_hyps(2,4,5) subtrail_falseI uminus_Pos uminus_not_id')
hence "D ≠ C"
using D_false by metis
thus "D |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
unfolding ‹ℱ' = (if ord_res.is_strictly_maximal_lit (Pos A) C then ℱ else finsert C ℱ)›
using D_in iefac_def by auto
qed
moreover have "snd Ln ≠ None"
using ‹Γ' = Ln # Γ''› step_hyps by auto
ultimately show "snd Ln ≠ None ⟷
(∃C|∈|iefac ℱ' |`| (N |∪| U⇩e⇩r). trail_false_cls Γ' C)"
by argo
show "snd Ln ≠ None ⟹ is_pos (fst Ln)"
using ‹Ln = (Pos A, Some (efac C))› by auto
show "∀x∈set Γ''. snd x = None"
unfolding ‹Γ'' = Γ›
using invars by (meson list.set_cases step_hyps(2))
have "clause_could_propagate Γ (efac C) (Pos A)"
using C_prop clause_could_propagate_efac by metis
thus "⋀C. snd Ln = Some C ⟹ clause_could_propagate Γ'' C (fst Ln)"
using ‹Γ' = Ln # Γ''› ‹Γ' = (Pos A, Some (efac C)) # Γ›
by force
have "efac C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
proof (cases "ord_res.is_strictly_maximal_lit (Pos A) C")
case True
thus ?thesis
unfolding ‹ℱ' = _›
using C_in
by (metis (mono_tags, opaque_lifting) literal.discI(1)
nex_strictly_maximal_pos_lit_if_neq_efac)
next
case False
then show ?thesis
unfolding ‹ℱ' = _›
using C_in
by (smt (z3) fimage_iff finsert_iff iefac_def nex_strictly_maximal_pos_lit_if_neq_efac
obtains_positive_greatest_lit_if_efac_not_ident)
qed
thus "⋀D. snd Ln = Some D ⟹ D |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
using ‹Γ' = Ln # Γ''› ‹Γ' = (Pos A, Some (efac C)) # Γ› by force
}
show "⋀Γ⇩1 Ln Γ⇩0. Γ' = Γ⇩1 @ Ln # Γ⇩0 ⟹ snd Ln = None ⟹
¬ (∃C|∈|iefac ℱ' |`| (N |∪| U⇩e⇩r). trail_false_cls (Ln # Γ⇩0) C)"
unfolding ‹Γ' = (_, Some _) # Γ›
using invars
unfolding bex_trail_false_cls_simp
by (metis list.inject not_None_eq split_pairs suffix_Cons suffix_def)
qed
next
case step_hyps: (resolution D A C U⇩e⇩r' Γ')
note D_max_lit = ‹ord_res.is_maximal_lit (Neg A) D›
have C_max_lit: ‹ord_res.is_strictly_maximal_lit (Pos A) C›
using invars by (metis map_of_SomeD split_pairs step_hyps(4))
have
D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
D_false: "trail_false_cls Γ D" and
D_lt: "∀E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). E ≠ D ⟶ trail_false_cls Γ E ⟶ D ≺⇩c E"
using ‹linorder_cls.is_least_in_fset _ D›
unfolding atomize_conj linorder_cls.is_least_in_ffilter_iff by argo
have "A |∈| atms_of_clss (N |∪| U⇩e⇩r)"
using D_in D_max_lit
by (metis atm_of_in_atms_of_clssI linorder_lit.is_maximal_in_mset_iff literal.sel(2))
have "ord_res.ground_resolution D C ((D - {#Neg A#}) + (C - {#Pos A#}))"
proof (rule ord_res.ground_resolutionI)
show "D = add_mset (Neg A) (D - {#Neg A#})"
using D_max_lit unfolding linorder_lit.is_maximal_in_mset_iff by simp
next
show "C = add_mset (Pos A) (C - {#Pos A#})"
using C_max_lit unfolding linorder_lit.is_greatest_in_mset_iff by simp
next
show "C ≺⇩c D"
using C_max_lit D_max_lit
by (simp add: clause_lt_clause_if_max_lit_comp
linorder_lit.is_greatest_in_mset_iff_is_maximal_and_count_eq_one)
next
show "{#} = {#} ∧ ord_res.is_maximal_lit (Neg A) D ∨ Neg A ∈# {#}"
using D_max_lit by argo
next
show "{#} = {#}"
by argo
next
show "ord_res.is_strictly_maximal_lit (Pos A) C"
using C_max_lit .
next
show "remove1_mset (Neg A) D + remove1_mset (Pos A) C = (D - {#Neg A#}) + (C - {#Pos A#})"
..
qed
hence "eres C D ≠ D"
unfolding eres_ident_iff not_not ground_resolution_def by metis
obtain Γ⇩b where "Γ = (Pos A, Some C) # Γ⇩b"
using ‹map_of Γ (Pos A) = Some (Some C)› invars
by (metis list.set_cases map_of_SomeD not_Some_eq snd_conv)
have "A |∈| trail_atms Γ"
unfolding ‹Γ = (Pos A, Some C) # Γ⇩b› trail_atms_def by simp
moreover have "A |∉| trail_atms Γ'"
proof (cases "eres C D = {#}")
case True
hence "∄K. ord_res.is_maximal_lit K (eres C D)"
unfolding linorder_lit.is_maximal_in_mset_iff by simp
hence "Γ' = dropWhile (λLn. True) Γ"
using step_hyps(6) by simp
also have "… = []"
by simp
finally show ?thesis
using ‹Γ = (Pos A, Some C) # Γ⇩b› by simp
next
case False
then obtain K where eres_max_lit: "ord_res.is_maximal_lit K (eres C D)"
using linorder_lit.ex_maximal_in_mset by presburger
have "atm_of K ≺⇩t atm_of (Neg A)"
proof (rule lit_in_eres_lt_greatest_lit_in_grestest_resolvant [of C D])
show "eres C D ≠ D"
using ‹eres C D ≠ D› .
next
show "ord_res.is_maximal_lit (Neg A) D"
using D_max_lit .
next
show "- Neg A ∉# D"
using D_false ‹trail_consistent Γ›
by (meson D_max_lit linorder_lit.is_maximal_in_mset_iff
not_both_lit_and_comp_lit_in_false_clause_if_trail_consistent)
next
show "K ∈# eres C D"
using eres_max_lit unfolding linorder_lit.is_maximal_in_mset_iff by argo
qed
hence "atm_of K ≺⇩t A"
unfolding literal.sel .
hence "atm_of K ≼⇩t A"
by order
have "Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ"
using step_hyps(6) eres_max_lit
by (smt (verit, ccfv_threshold) Uniq_D dropWhile_cong linorder_lit.Uniq_is_maximal_in_mset)
also have "… = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ⇩b"
unfolding ‹Γ = (Pos A, Some C) # Γ⇩b›
unfolding dropWhile.simps prod.sel literal.sel
using ‹atm_of K ≼⇩t A› by simp
finally have "Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ⇩b" .
hence "trail_atms Γ' |⊆| trail_atms Γ⇩b"
by (simp only: suffix_dropWhile trail_atms_subset_if_suffix)
moreover have "A |∉| trail_atms Γ⇩b"
proof (rule notI)
assume "A |∈| trail_atms Γ⇩b"
then obtain Ln where "Ln ∈ set Γ⇩b" and "atm_of (fst Ln) = A"
unfolding fset_trail_atms by blast
moreover have "∀y∈set Γ⇩b. atm_of (fst y) ≺⇩t A"
using Γ_sorted[unfolded ‹Γ = (Pos A, Some C) # Γ⇩b›] by simp
ultimately have "A ≺⇩t A"
by metis
thus False
by order
qed
moreover have "trail_atms Γ⇩b |⊆| trail_atms Γ"
proof (rule trail_atms_subset_if_suffix)
show "suffix Γ⇩b Γ"
by (simp only: ‹Γ = (Pos A, Some C) # Γ⇩b› suffix_ConsI)
qed
ultimately show ?thesis
by fast
qed
ultimately have "Γ' ≠ Γ"
by metis
have C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using invars
by (meson ‹Γ = (Pos A, Some C) # Γ⇩b› snd_conv)
define P :: "'f gliteral × 'f gclause option ⇒ bool" where
"P ≡ λLn. ∀K. ord_res.is_maximal_lit K (eres C D) ⟶ atm_of K ≼⇩t atm_of (fst Ln)"
have "Γ = takeWhile P Γ @ Γ'"
unfolding takeWhile_dropWhile_id
unfolding P_def ‹Γ' = dropWhile _ Γ› by simp
hence "suffix Γ' Γ"
unfolding suffix_def by metis
show ?thesis
unfolding ‹s' = (_, _, _)›
proof (intro ord_res_10_invars.intros allI impI conjI)
show Γ'_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
by (metis (no_types, lifting) Γ_sorted ‹suffix Γ' Γ› sorted_wrt_append suffix_def)
show "∀Ln∈set Γ'. ∀C. snd Ln = Some C ⟶ ord_res.is_strictly_maximal_lit (fst Ln) C"
using ‹suffix Γ' Γ› invars(3) set_mono_suffix by blast
have "⋀xs. fset (trail_atms xs) = atm_of ` fst ` set xs"
unfolding fset_trail_atms ..
also have "⋀xs. atm_of ` fst ` set xs = set (map (atm_of o fst) xs)"
by (simp add: image_comp)
finally have "⋀xs. fset (trail_atms xs) = set (map (atm_of o fst) xs)" .
have "atms_of_clss (N |∪| U⇩e⇩r') = atms_of_cls (eres C D) |∪| atms_of_clss (N |∪| U⇩e⇩r)"
unfolding ‹U⇩e⇩r' = finsert (eres C D) U⇩e⇩r› by simp
also have "… = atms_of_clss (N |∪| U⇩e⇩r)"
proof -
have "atms_of_cls (eres C D) |⊆| atms_of_cls C |∪| atms_of_cls D"
by (smt (verit, best) atms_of_cls_def fimage_iff fset_fset_mset fsubsetI funionCI
lit_in_one_of_resolvents_if_in_eres)
moreover have "atms_of_cls C |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
using C_in
by (metis atms_of_clss_fimage_iefac atms_of_clss_finsert finsert_absorb fsubset_funion_eq)
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 fsubset_funion_eq)
ultimately show ?thesis
by blast
qed
finally have "atms_of_clss (N |∪| U⇩e⇩r') = atms_of_clss (N |∪| U⇩e⇩r)" .
show Γ'_lower: "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r'))"
unfolding ‹fset (trail_atms Γ') = set (map (atm_of o fst) Γ')›
proof (rule linorder_trm.sorted_and_lower_set_appendD_right(2))
have "sorted_wrt (λx y. y ≺⇩t x) (map (atm_of ∘ fst) Γ)"
using Γ_sorted by (simp add: sorted_wrt_map)
thus "sorted_wrt (λx y. y ≺⇩t x) (map (atm_of ∘ fst) (takeWhile P Γ) @ map (atm_of ∘ fst) Γ')"
using ‹Γ = takeWhile P Γ @ Γ'›
by (metis map_append)
next
show "linorder_trm.is_lower_set
(set (map (atm_of ∘ fst) (takeWhile P Γ) @ map (atm_of ∘ fst) Γ'))
(fset (atms_of_clss (N |∪| U⇩e⇩r')))"
unfolding map_append[symmetric]
unfolding ‹Γ = takeWhile P Γ @ Γ'›[symmetric]
using Γ_lower
unfolding ‹fset (trail_atms Γ) = set (map (atm_of o fst) Γ)›
unfolding ‹atms_of_clss (N |∪| U⇩e⇩r') = atms_of_clss (N |∪| U⇩e⇩r)›
.
qed
have no_false_cls_in_Γ': "¬ (∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). trail_false_cls Γ' C)"
if eres_max_lit: "ord_res.is_maximal_lit K (eres C D)"
for K
proof -
have FOO: "⋀Ln.
(∀K. ord_res.is_maximal_lit K (eres C D) ⟶ atm_of K ≼⇩t atm_of (fst Ln)) ⟷
atm_of K ≼⇩t atm_of (fst Ln)"
using eres_max_lit
by (metis linorder_lit.Uniq_is_maximal_in_mset the1_equality')
have "∀x ∈ set Γ'. atm_of (fst x) ≺⇩t atm_of K"
using ‹Γ' = dropWhile _ Γ›[unfolded FOO] Γ_sorted
by (metis linorder_trm.not_le mem_set_dropWhile_conv_if_list_sorted_and_pred_monotone
mono_atms_lt)
hence "∀x ∈ set Γ'. atm_of (fst x) ≠ atm_of K"
by fastforce
hence "atm_of K |∉| trail_atms Γ'"
unfolding fset_trail_atms by auto
hence "¬ trail_defined_lit Γ' K"
unfolding trail_defined_lit_iff_trail_defined_atm .
hence "¬ trail_false_lit Γ' K"
by (metis trail_defined_lit_iff_true_or_false)
hence "¬ trail_false_cls Γ' (eres C D)"
using eres_max_lit
unfolding linorder_lit.is_maximal_in_mset_iff trail_false_cls_def
by metis
show "¬ (∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). trail_false_cls Γ' C)"
unfolding ‹U⇩e⇩r' = finsert (eres C D) U⇩e⇩r›
proof (rule notI , elim bexE)
fix E :: "'f gclause"
assume
E_in: "E |∈| iefac ℱ |`| (N |∪| finsert (eres C D) U⇩e⇩r)" and
E_false: "trail_false_cls Γ' E"
have "E = iefac ℱ (eres C D) ∨ E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using E_in by simp
thus False
proof (elim disjE)
assume "E = iefac ℱ (eres C D)"
hence "trail_false_cls Γ' (eres C D)"
using E_false
by (simp add: iefac_def trail_false_cls_def)
thus False
using ‹¬ trail_false_cls Γ' (eres C D)› by contradiction
next
assume "E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
moreover have "trail_false_cls Γ E"
using E_false ‹suffix Γ' Γ› by (metis trail_false_cls_if_trail_false_suffix)
ultimately have "D ≼⇩c E"
using D_lt E_false by fast
then obtain L where "L ∈# E" and "Neg A ≼⇩l L"
using D_max_lit
by (metis empty_iff linorder_cls.leD linorder_lit.is_maximal_in_mset_iff
linorder_lit.leI ord_res.multp_if_all_left_smaller set_mset_empty)
hence "A ≼⇩t atm_of L"
by (cases L) simp_all
moreover have "A |∈| atms_of_clss (N |∪| U⇩e⇩r')"
using ‹A |∈| atms_of_clss (N |∪| U⇩e⇩r)›
using ‹atms_of_clss (N |∪| U⇩e⇩r') = atms_of_clss (N |∪| U⇩e⇩r)›
by (simp only:)
ultimately have "atm_of L |∉| trail_atms Γ'"
using linorder_trm.not_in_lower_setI[OF Γ'_lower] ‹A |∉| trail_atms Γ'› by blast
hence "¬ trail_defined_lit Γ' L"
unfolding trail_defined_lit_iff_trail_defined_atm .
hence "¬ trail_false_lit Γ' L"
by (metis trail_defined_lit_iff_true_or_false)
moreover have "trail_false_lit Γ' L"
using E_false ‹L ∈# E› unfolding trail_false_cls_def by metis
ultimately show False
by contradiction
qed
qed
qed
have ex_max_lit_in_eres_if: "∃K. ord_res.is_maximal_lit K (eres C D)"
if "Γ' = Γ⇩1 @ Ln # Γ⇩0" for Ln and Γ⇩1 Γ⇩0
proof -
have "∃x xs. Γ' = x # xs"
using that neq_Nil_conv by blast
hence "∃x. ¬ (∀K. ord_res.is_maximal_lit K (eres C D) ⟶ atm_of K ≼⇩t atm_of (fst x))"
unfolding step_hyps(6) dropWhile_eq_Cons_conv by auto
thus ?thesis
by metis
qed
{
fix Ln and Γ''
assume "Γ' = Ln # Γ''"
then obtain K where
eres_max_lit: "ord_res.is_maximal_lit K (eres C D)"
using ex_max_lit_in_eres_if[of "[]", simplified] by metis
have "¬ (∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). trail_false_cls Γ' C)"
using no_false_cls_in_Γ' eres_max_lit by metis
moreover have "snd Ln = None"
using invars ‹Γ' ≠ Γ› ‹suffix Γ' Γ›
by (metis ‹Γ = (Pos A, Some C) # Γ⇩b› ‹Γ' = Ln # Γ''› in_set_conv_decomp suffix_Cons
suffix_def)
ultimately show "snd Ln ≠ None ⟷ (∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). trail_false_cls Γ' C)"
by argo
show "snd Ln ≠ None ⟹ is_pos (fst Ln)"
using ‹snd Ln = None› by argo
show "∀x∈set Γ''. snd x = None"
using invars ‹Γ' ≠ Γ› ‹suffix Γ' Γ›
by (metis ‹Γ = (Pos A, Some C) # Γ⇩b› ‹Γ' = Ln # Γ''› set_mono_suffix subsetD suffix_ConsD2)
show "⋀C. snd Ln = Some C ⟹ clause_could_propagate Γ'' C (fst Ln)"
by (simp add: ‹snd Ln = None›)
show "⋀E. snd Ln = Some E ⟹ E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
by (simp add: ‹snd Ln = None›)
}
show "⋀Γ⇩1 Ln Γ⇩0. Γ' = Γ⇩1 @ Ln # Γ⇩0 ⟹ snd Ln = None ⟹
¬ (∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r'). trail_false_cls (Ln # Γ⇩0) C)"
using ex_max_lit_in_eres_if no_false_cls_in_Γ'
by (metis suffixI trail_false_cls_if_trail_false_suffix)
qed
qed
qed
lemma rtranclp_ord_res_10_preserves_invars:
assumes
step: "(ord_res_10 N)⇧*⇧* s s'" and
invars: "ord_res_10_invars N s"
shows "ord_res_10_invars N s'"
using step invars ord_res_10_preserves_invars
by (smt (verit, del_insts) rtranclp_induct)
lemma ex_ord_res_10_if_not_final:
assumes
not_final: "¬ ord_res_8_final (N, s)" and
invars: "ord_res_10_invars N s"
shows "∃s'. ord_res_10 N s s'"
using invars
proof (cases N s rule: ord_res_10_invars.cases)
case invars': (1 Γ U⇩e⇩r ℱ)
have
undef_atm_or_false_cls: "
(∃x |∈| atms_of_clss (N |∪| U⇩e⇩r). x |∉| trail_atms Γ) ∧
¬ (∃x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x)∨
(∃x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x)" and
"{#} |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)"
unfolding atomize_conj
using not_final[unfolded ord_res_8_final.simps] ‹s = (U⇩e⇩r, ℱ, Γ)› by metis
show ?thesis
using undef_atm_or_false_cls
proof (elim disjE conjE)
assume
ex_undef_atm: "∃x |∈| atms_of_clss (N |∪| U⇩e⇩r). x |∉| trail_atms Γ" and
no_conflict: "¬ (∃x|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x)"
moreover have "{|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r). ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} ≠ {||}"
proof -
obtain A⇩2 :: "'f gterm" where
A⇩2_in: "A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r)" and
A⇩2_undef: "A⇩2 |∉| trail_atms Γ"
using ex_undef_atm by metis
have "A⇩1 ≺⇩t A⇩2" if A⇩1_in: "A⇩1 |∈| trail_atms Γ" for A⇩1 :: "'f gterm"
proof -
have "A⇩1 ≠ A⇩2"
using A⇩1_in A⇩2_undef by metis
moreover have "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
using invars'[unfolded trail_is_lower_set_def, simplified] by argo
ultimately show ?thesis
by (meson A⇩2_in A⇩2_undef linorder_trm.is_lower_set_iff linorder_trm.linorder_cases that)
qed
thus ?thesis
using A⇩2_in
by (smt (verit, ccfv_threshold) femptyE ffmember_filter)
qed
ultimately obtain A :: "'f gterm" where
A_least: "linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A"
using ex_undef_atm linorder_trm.ex_least_in_fset by presburger
show "∃s'. ord_res_10 N s s'"
proof (cases "∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)")
case True
hence "{|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)|} ≠ {||}"
by force
then obtain C where
C_least: "linorder_cls.is_least_in_fset
{|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)|} C"
using linorder_cls.ex1_least_in_fset by meson
show ?thesis
proof (cases "∃D|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls ((Pos A, Some (efac C)) # Γ) D")
case True
then show ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ)›
using ord_res_10.propagate[OF no_conflict A_least C_least]
by metis
next
case False
hence "¬ (∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls ((Pos A, None) # Γ) C)"
by (simp add: trail_false_cls_def trail_false_lit_def)
then show ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ)›
using ord_res_10.decide_pos[OF no_conflict A_least C_least]
by metis
qed
next
case False
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ)›
using ord_res_10.decide_neg[OF no_conflict A_least]
by metis
qed
next
assume "∃x|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x"
then obtain D :: "'f gclause" where
D_least: "linorder_cls.is_least_in_fset
(ffilter (trail_false_cls Γ) (iefac ℱ |`| (N |∪| U⇩e⇩r))) D"
by (metis femptyE ffmember_filter linorder_cls.ex_least_in_fset)
hence D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and D_false: "trail_false_cls Γ D"
unfolding atomize_conj linorder_cls.is_least_in_ffilter_iff by argo
have "D ≠ {#}"
using D_in ‹{#} |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)› by metis
hence "Γ ≠ []"
using D_false
by (auto simp add: trail_false_cls_def trail_false_lit_def)
then obtain Ln Γ' where "Γ = Ln # Γ'"
using neq_Nil_conv by metis
hence "snd Ln ≠ None"
using invars' ‹∃x|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x› by presburger
have "∀x∈set Γ'. snd x = None"
using invars' ‹Γ = Ln # Γ'› by metis
have "¬(∃x|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ' x)"
proof (cases Γ')
case Nil
thus ?thesis
using ‹{#} |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)›
by (simp add: trail_false_cls_def trail_false_lit_def)
next
case (Cons x xs)
hence "snd x = None"
using ‹∀x∈set Γ'. snd x = None› by simp
then show ?thesis
using ‹∀Γ⇩1 Ln Γ⇩0. Γ = Γ⇩1 @ Ln # Γ⇩0 ⟶ snd Ln = None ⟶
¬ (∃C |∈| _. trail_false_cls (Ln # Γ⇩0) C)›[rule_format, of "[Ln]" x xs, simplified]
using Cons ‹Γ = Ln # Γ'› by blast
qed
hence "¬ trail_false_cls Γ' D"
using D_in by metis
hence "- fst Ln ∈# D"
using D_false ‹Γ = Ln # Γ'› by (metis eq_fst_iff subtrail_falseI)
moreover have "is_pos (fst Ln)"
using invars' ‹Γ = Ln # Γ'› ‹snd Ln ≠ None› by metis
moreover have "∀L ∈# D. atm_of L |∈| trail_atms Γ"
using D_false
unfolding trail_false_cls_def
using trail_defined_lit_iff_true_or_false[of Γ]
using trail_defined_lit_iff_trail_defined_atm[of Γ]
by metis
moreover have "∀x |∈| trail_atms Γ'. x ≺⇩t atm_of (fst Ln)"
using ‹sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ›[
unfolded ‹Γ = Ln # Γ'› sorted_wrt.simps]
by (simp add: fset_trail_atms)
ultimately have "linorder_lit.is_maximal_in_mset D (- fst Ln)"
unfolding linorder_lit.is_maximal_in_mset_iff
by (smt (verit, best) ‹Γ = Ln # Γ'› finsertE ord_res.less_lit_simps(4)
linorder_lit.not_less_iff_gr_or_eq literal.exhaust_sel ord_res.less_lit_simps(3)
trail_atms.simps(2) uminus_literal_def)
moreover obtain A where "fst Ln = Pos A"
using ‹is_pos (fst Ln)› by (cases "fst Ln") simp_all
ultimately have eres_max_lit: "ord_res.is_maximal_lit (Neg A) D"
by simp
obtain C :: "'f gclause" where
"map_of Γ (Pos A) = Some (Some C)"
unfolding ‹Γ = Ln # Γ'›
using ‹fst Ln = Pos A› ‹snd Ln ≠ None› by force
thus "∃s'. ord_res_10 N s s'"
unfolding ‹s = (U⇩e⇩r, ℱ, Γ)›
using ord_res_10.resolution[OF D_least eres_max_lit] by blast
qed
qed
lemma ord_res_10_safe_state_if_invars:
fixes N s
assumes invars: "ord_res_10_invars N s"
shows "safe_state (constant_context ord_res_10) ord_res_8_final (N, s)"
using safe_state_constant_context_if_invars[where
ℛ = ord_res_10 and ℱ = ord_res_8_final and ℐ = ord_res_10_invars]
using ord_res_10_preserves_invars ex_ord_res_10_if_not_final invars by metis
end
end