Theory ORD_RES_11
theory ORD_RES_11
imports ORD_RES_10
begin
section ‹ORD-RES-11 (SCL strategy)›
type_synonym 'f ord_res_11_state =
"'f gclause fset ×'f gclause fset × 'f gclause fset × ('f gliteral × 'f gclause option) list ×
'f gclause option"
context simulation_SCLFOL_ground_ordered_resolution begin
lemma
fixes N U⇩e⇩r ℱ Γ A
assumes
no_false_cls: "¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C)" and
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" and
C_least: "linorder_cls.is_least_in_fset {|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r).
clause_could_propagate Γ C (Pos A)|} C"
defines
"Γ' ≡ (Pos A, None) # Γ" and
"ℱ' ≡ (if linorder_lit.is_greatest_in_mset C (Pos A) then ℱ else finsert C ℱ)"
shows "
(∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ' C) ⟷
(∃C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r). trail_false_cls Γ' C)"
by (meson bex_trail_false_cls_simp)
inductive ord_res_11 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_11 N (U⇩e⇩r, ℱ, Γ, None) (U⇩e⇩r, ℱ, Γ', None)" |
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_11 N (U⇩e⇩r, ℱ, Γ, None) (U⇩e⇩r, ℱ', Γ', None)" |
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_11 N (U⇩e⇩r, ℱ, Γ, None) (U⇩e⇩r, ℱ', Γ', None)" |
conflict: "
linorder_cls.is_least_in_fset {|D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ D|} D ⟹
ord_res_11 N (U⇩e⇩r, ℱ, Γ, None) (U⇩e⇩r, ℱ, Γ, Some D)" |
skip: "- L ∉# C ⟹
ord_res_11 N (U⇩e⇩r, ℱ, (L, n) # Γ, Some C) (U⇩e⇩r, ℱ, Γ, Some C)" |
resolution: "
Γ = (L, Some D) # Γ' ⟹ - L ∈# C ⟹
ord_res_11 N (U⇩e⇩r, ℱ, Γ, Some C) (U⇩e⇩r, ℱ, Γ, Some ((C - {#- L#}) + (D - {#L#})))" |
backtrack: "
Γ = (L, None) # Γ' ⟹ - L ∈# C ⟹
ord_res_11 N (U⇩e⇩r, ℱ, Γ, Some C) (finsert C U⇩e⇩r, ℱ, Γ', None)"
lemma right_unique_ord_res_11:
fixes N :: "'f gclause fset"
shows "right_unique (ord_res_11 N)"
proof (rule right_uniqueI)
fix x y z
assume step1: "ord_res_11 N x y" and step2: "ord_res_11 N x z"
show "y = z"
using step1
proof (cases N x y rule: ord_res_11.cases)
case hyps1: (decide_neg ℱ U⇩e⇩r Γ A1 Γ1')
show ?thesis
using step2 unfolding ‹x = _›
proof (cases N "(U⇩e⇩r, ℱ, Γ, None :: 'f gclause option)" z rule: ord_res_11.cases)
case (decide_neg A Γ')
with hyps1 show ?thesis
by (metis (no_types, lifting) linorder_trm.dual_order.asym
linorder_trm.is_least_in_fset_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 (conflict D)
with hyps1 have False
by (metis (no_types) 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 = _›
proof (cases N "(U⇩e⇩r, ℱ, Γ, None :: 'f gclause option)" z rule: ord_res_11.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 ‹linorder_trm.is_least_in_fset _ A1› ‹linorder_trm.is_least_in_fset _ A›
by (metis (no_types) linorder_trm.Uniq_is_least_in_fset Uniq_D)
hence "trail_false_cls Γ1' = trail_false_cls Γ'"
unfolding ‹Γ1' = _ # Γ› ‹Γ' = _ # Γ›
unfolding trail_false_cls_def trail_false_lit_def
by simp
hence False
using hyps1 hyps2 by argo
thus ?thesis ..
next
case (conflict D)
with hyps1 have False
by (metis (no_types) 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 = _›
proof (cases N "(U⇩e⇩r, ℱ, Γ, None :: 'f gclause option)" z rule: ord_res_11.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 ‹linorder_trm.is_least_in_fset _ A1› ‹linorder_trm.is_least_in_fset _ A›
by (metis (no_types) linorder_trm.Uniq_is_least_in_fset Uniq_D)
hence "trail_false_cls Γ1' = trail_false_cls Γ'"
unfolding ‹Γ1' = _ # Γ› ‹Γ' = _ # Γ›
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 (conflict D)
with hyps1 have False
by (metis (no_types) linorder_cls.is_least_in_ffilter_iff)
thus ?thesis ..
qed
next
case hyps1: (conflict Γ ℱ U⇩e⇩r D1)
show ?thesis
using step2 unfolding ‹x = _›
proof (cases N "(U⇩e⇩r, ℱ, Γ, None :: 'f gclause option)" z rule: ord_res_11.cases)
case (decide_neg A Γ')
with hyps1 have False
by (metis (no_types) linorder_cls.is_least_in_ffilter_iff)
thus ?thesis ..
next
case (decide_pos A C Γ' ℱ')
with hyps1 have False
by (metis (no_types) linorder_cls.is_least_in_ffilter_iff)
thus ?thesis ..
next
case (propagate A C Γ' ℱ')
with hyps1 have False
by (metis (no_types) linorder_cls.is_least_in_ffilter_iff)
thus ?thesis ..
next
case (conflict D)
with hyps1 show ?thesis
by (metis (no_types) linorder_cls.Uniq_is_least_in_fset Uniq_D)
qed
next
case hyps1: (skip L C U⇩e⇩r ℱ n Γ)
show ?thesis
using step2 unfolding ‹x = _›
proof (cases N "(U⇩e⇩r, ℱ, (L, n) # Γ, Some C)" z rule: ord_res_11.cases)
case skip
with hyps1 show ?thesis
by argo
next
case (resolution L' D' Γ')
with hyps1 have False
by simp
thus ?thesis ..
next
case (backtrack K Γ')
with hyps1 have False
by simp
thus ?thesis ..
qed
next
case hyps1: (resolution Γ L1 D1 Γ1' C U⇩e⇩r ℱ)
show ?thesis
using step2 unfolding ‹x = _›
proof (cases N "(U⇩e⇩r, ℱ, Γ, Some C)" z rule: ord_res_11.cases)
case (skip L n Γ)
with hyps1 have False
by simp
thus ?thesis ..
next
case (resolution L D Γ')
with hyps1 show ?thesis
by simp
next
case (backtrack K Γ')
with hyps1 have False
by simp
thus ?thesis ..
qed
next
case hyps1: (backtrack Γ L Γ' C U⇩e⇩r ℱ)
show ?thesis
using step2 unfolding ‹x = _›
proof (cases N "(U⇩e⇩r, ℱ, Γ, Some C)" z rule: ord_res_11.cases)
case (skip L n Γ)
with hyps1 have False
by simp
thus ?thesis ..
next
case (resolution L D Γ')
with hyps1 have False
by simp
thus ?thesis ..
next
case (backtrack K Γ')
with hyps1 show ?thesis
by simp
qed
qed
qed
inductive ord_res_11_final :: "'f ord_res_11_state ⇒ bool" where
model_found: "
¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A |∉| trail_atms Γ) ⟹
¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C) ⟹
ord_res_11_final (N, U⇩e⇩r, ℱ, Γ, None)" |
contradiction_found: "
ord_res_11_final (N, U⇩e⇩r, ℱ, [], Some {#})"
sublocale ord_res_11_semantics: semantics where
step = "constant_context ord_res_11" and
final = ord_res_11_final
proof unfold_locales
fix S :: "'f ord_res_11_state"
assume "ord_res_11_final S"
thus "finished (constant_context ord_res_11) S"
proof (cases S rule: ord_res_11_final.cases)
case (model_found N U⇩e⇩r Γ ℱ)
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 Γ)›
unfolding linorder_trm.is_least_in_ffilter_iff
by blast
moreover have "∄D. linorder_cls.is_least_in_fset
(ffilter (trail_false_cls Γ) (iefac ℱ |`| (N |∪| U⇩e⇩r))) D"
using ‹¬ (∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C)›
unfolding linorder_cls.is_least_in_ffilter_iff
by metis
ultimately have "∄x. ord_res_11 N (U⇩e⇩r, ℱ, Γ, None) x"
by (auto elim: ord_res_11.cases)
thus ?thesis
by (simp add: ‹S = _› finished_def constant_context.simps)
next
case (contradiction_found N U⇩e⇩r ℱ)
hence "∄x. ord_res_11 N (U⇩e⇩r, ℱ, [], Some {#}) x"
by (auto elim: ord_res_11.cases)
thus ?thesis
by (simp add: ‹S = _› finished_def constant_context.simps)
qed
qed
inductive ord_res_11_invars where
"ord_res_11_invars N (U⇩e⇩r, ℱ, Γ, 𝒞)" if
"ord_res_10_invars N (U⇩e⇩r, ℱ, Γ)" and
"{#} |∈| N |∪| U⇩e⇩r ⟶ Γ = []" and
"∀C. 𝒞 = Some C ⟶ atms_of_cls C |⊆| atms_of_clss (N |∪| U⇩e⇩r)" and
"∀C. 𝒞 = Some C ⟶ trail_false_cls Γ C" and
"atms_of_clss U⇩e⇩r |⊆| atms_of_clss N" and
"∀C |∈| ℱ. ∃L. is_pos L ∧ linorder_lit.is_maximal_in_mset C L"
lemma ord_res_11_invars_initial_state: "ord_res_11_invars N ({||}, {||}, [], None)"
by (intro ord_res_11_invars.intros ord_res_10_invars.intros) simp_all
lemma mempty_in_fimage_iefac[simp]: "{#} |∈| iefac ℱ |`| N ⟷ {#} |∈| N"
using iefac_def by auto
lemma ord_res_11_preserves_invars:
assumes
step: "ord_res_11 N s s'" and
invars: "ord_res_11_invars N s"
shows "ord_res_11_invars N s'"
using invars
proof (cases N s rule: ord_res_11_invars.cases)
case more_invars: (1 U⇩e⇩r ℱ Γ 𝒞)
show ?thesis
using ‹ord_res_10_invars N (U⇩e⇩r, ℱ, Γ)›
proof (cases N "(U⇩e⇩r, ℱ, Γ)" rule: ord_res_10_invars.cases)
case invars: 1
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_11.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_11_invars.intros 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)
show "{#} |∈| N |∪| U⇩e⇩r ⟹ Γ' = []"
using bex_trail_false_cls_simp more_invars(3) step_hyps(3) trail_false_cls_mempty by blast
next
show "⋀C. None = Some C ⟹ atms_of_cls C |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
by simp
next
show "⋀C. None = Some C ⟹ trail_false_cls Γ' C"
by simp
next
show "atms_of_clss U⇩e⇩r |⊆| atms_of_clss N"
using more_invars by argo
next
show "∀C|∈|ℱ. ∃L. is_pos L ∧ ord_res.is_maximal_lit L C"
using more_invars by argo
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_11_invars.intros 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)
show "{#} |∈| N |∪| U⇩e⇩r ⟹ Γ' = []"
by (meson bex_trail_false_cls_simp step_hyps(3) trail_false_cls_mempty)
next
show "⋀C. None = Some C ⟹ atms_of_cls C |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
by simp
next
show "⋀C. None = Some C ⟹ trail_false_cls Γ' C"
by simp
next
show "atms_of_clss U⇩e⇩r |⊆| atms_of_clss N"
using more_invars by argo
next
have "∃L. is_pos L ∧ ord_res.is_maximal_lit L C"
using step_hyps
by (metis (no_types, lifting) clause_could_propagate_def
linorder_cls.is_least_in_ffilter_iff literal.discI(1))
thus "∀C|∈|ℱ'. ∃L. is_pos L ∧ ord_res.is_maximal_lit L C"
using more_invars ‹ℱ' = (if _ then ℱ else finsert C ℱ)› by simp
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_11_invars.intros 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_lit Γ' (Pos A)"
by (metis C_prop map_of_Cons_code(2) map_of_eq_None_iff clause_could_propagate_def
step_hyps(6) trail_defined_lit_def trail_false_lit_def uminus_not_id)
moreover have "Pos A ∈# C"
using C_prop
unfolding clause_could_propagate_def linorder_lit.is_maximal_in_mset_iff
by argo
ultimately have "¬ trail_false_cls Γ' C"
unfolding trail_false_cls_def by metis
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)
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)
show "{#} |∈| N |∪| U⇩e⇩r ⟹ Γ' = []"
by (meson bex_trail_false_cls_simp step_hyps(3) trail_false_cls_mempty)
next
show "⋀C. None = Some C ⟹ atms_of_cls C |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
by simp
next
show "⋀C. None = Some C ⟹ trail_false_cls Γ' C"
by simp
next
show "atms_of_clss U⇩e⇩r |⊆| atms_of_clss N"
using more_invars by argo
next
have "∃L. is_pos L ∧ ord_res.is_maximal_lit L C"
using step_hyps
by (metis (no_types, lifting) clause_could_propagate_def
linorder_cls.is_least_in_ffilter_iff literal.discI(1))
thus "∀C|∈|ℱ'. ∃L. is_pos L ∧ ord_res.is_maximal_lit L C"
using more_invars ‹ℱ' = (if _ then ℱ else finsert C ℱ)› by simp
qed
next
case step_hyps: (conflict D)
show ?thesis
unfolding ‹s' = _›
proof (intro ord_res_11_invars.intros allI impI)
show "ord_res_10_invars N (U⇩e⇩r, ℱ, Γ)"
using more_invars by argo
next
show "{#} |∈| N |∪| U⇩e⇩r ⟹ Γ = []"
using more_invars by argo
next
show "⋀C. Some D = Some C ⟹ atms_of_cls C |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
by (metis atm_of_in_atms_of_clssI atms_of_cls_def fimage_fsubsetI fset_fset_mset
linorder_cls.is_least_in_ffilter_iff option.inject step_hyps(3))
next
show "⋀C. Some D = Some C ⟹ trail_false_cls Γ C"
using ‹linorder_cls.is_least_in_fset _ D›
unfolding linorder_cls.is_least_in_ffilter_iff
by simp
next
show "atms_of_clss U⇩e⇩r |⊆| atms_of_clss N"
using more_invars by argo
next
show "∀C|∈|ℱ. ∃L. is_pos L ∧ ord_res.is_maximal_lit L C"
using more_invars by argo
qed
next
case step_hyps: (skip L C n Γ')
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)" .
show ?thesis
unfolding ‹s' = (U⇩e⇩r, ℱ, Γ', Some C)›
proof (intro ord_res_11_invars.intros ord_res_10_invars.intros ballI allI impI conjI)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
using invars unfolding ‹Γ = (L, n) # Γ'› by simp
next
fix Ln :: "'f gliteral × 'f gclause option" and C :: "'f gclause"
assume "Ln ∈ set Γ'" and "snd Ln = Some C"
then show "ord_res.is_strictly_maximal_lit (fst Ln) C"
using invars unfolding ‹Γ = (L, n) # Γ'› by simp
next
show "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) ([atm_of L] @ map (atm_of ∘ fst) Γ')"
unfolding ‹Γ = _ # Γ'› by simp
next
have "set ([atm_of L] @ map (atm_of ∘ fst) Γ') = fset (trail_atms Γ)"
unfolding append_Cons append_Nil list.set
unfolding ‹fset (trail_atms Γ') = set (map (atm_of o fst) Γ')›[symmetric]
unfolding ‹Γ = _ # Γ'› trail_atms.simps prod.sel
by simp
thus "linorder_trm.is_lower_set (set ([atm_of L] @ map (atm_of ∘ fst) Γ'))
(fset (atms_of_clss (N |∪| U⇩e⇩r)))"
using Γ_lower
by (simp only:)
qed
next
fix
Ln :: "'f gliteral × 'f gclause option" and
Γ'' :: "('f gliteral × 'f gclause option) list"
assume "Γ' = Ln # Γ''"
have "snd Ln = None"
by (metis ‹Γ' = Ln # Γ''› in_set_conv_decomp invars(4) step_hyps(1) suffixE suffix_Cons)
show "(snd Ln ≠ None) = (∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ' C)"
using ‹snd Ln = None›
by (metis ‹Γ' = Ln # Γ''› invars(5) step_hyps(1) suffixE suffix_Cons)
show "snd Ln ≠ None ⟹ is_pos (fst Ln)"
using ‹snd Ln = None› by simp
show "⋀C. snd Ln = Some C ⟹ clause_could_propagate Γ'' C (fst Ln)"
using ‹snd Ln = None› by simp
show "⋀C. snd Ln = Some C ⟹ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using ‹snd Ln = None› by simp
show "⋀x. x ∈ set Γ'' ⟹ snd x = None"
by (simp add: ‹Γ' = Ln # Γ''› invars(4) step_hyps(1))
next
fix
Ln :: "'f gliteral × 'f gclause option" and
Γ⇩1 Γ⇩0 :: "('f gliteral × 'f gclause option) list"
assume "Γ' = Γ⇩1 @ Ln # Γ⇩0" and "snd Ln = None"
thus "¬ (∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls (Ln # Γ⇩0) C)"
by (metis append_Cons invars(5) step_hyps(1))
next
show "{#} |∈| N |∪| U⇩e⇩r ⟹ Γ' = []"
using step_hyps(1) more_invars(3) by fastforce
next
show "⋀D. Some C = Some D ⟹ atms_of_cls D |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
using more_invars(4) step_hyps(2) by presburger
next
show "⋀D. Some C = Some D ⟹ trail_false_cls Γ' D"
using more_invars ‹𝒞 = Some C› ‹Γ = (L, n) # Γ'› ‹- L ∉# C›
using subtrail_falseI by auto
next
show "atms_of_clss U⇩e⇩r |⊆| atms_of_clss N"
using more_invars by argo
next
show "⋀C. C |∈| ℱ ⟹ ∃L. is_pos L ∧ ord_res.is_maximal_lit L C"
using more_invars by metis
qed
next
case step_hyps: (resolution L D Γ' C)
have D_max_lit: "ord_res.is_strictly_maximal_lit L D"
using invars ‹Γ = (L, Some D) # Γ'› by simp
show ?thesis
unfolding ‹s' = _›
proof (intro ord_res_11_invars.intros allI impI)
show "ord_res_10_invars N (U⇩e⇩r, ℱ, Γ)"
using more_invars by argo
next
show "{#} |∈| N |∪| U⇩e⇩r ⟹ Γ = []"
using more_invars by argo
next
have "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
using invars ‹Γ = (L, Some D) # Γ'›
by (metis snd_conv)
hence "atms_of_cls D |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
by (metis atms_of_clss_fimage_iefac atms_of_clss_finsert finsert_absorb funion_upper1)
moreover have "atms_of_cls C |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
by (smt (verit) add_single_right_eq_add_mset atms_of_cls_def dual_order.trans fimage_fsubsetI
fimage_iff fset_fset_mset more_invars(4) step_hyps(1) union_iff)
ultimately show "⋀E. Some (remove1_mset (- L) C + remove1_mset L D) = Some E ⟹
atms_of_cls E |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
by (smt (verit, ccfv_threshold) add_single_right_eq_add_mset atms_of_cls_def diff_single_trivial
fimage_iff fset_fset_mset fsubsetI fsubset_funion_eq funionI1 insert_DiffM
option.inject union_iff)
next
fix E :: "'f gclause"
assume "Some (remove1_mset (- L) C + remove1_mset L D) = Some E"
hence "E = remove1_mset (- L) C + remove1_mset L D"
by simp
show "trail_false_cls Γ E"
unfolding trail_false_cls_def
proof (intro ballI)
fix K :: "'f gliteral"
assume "K ∈# E"
hence "K ∈# remove1_mset (- L) C ∨ K ∈# remove1_mset L D"
unfolding ‹E = _› by simp
thus "trail_false_lit Γ K"
proof (elim disjE)
assume "K ∈# remove1_mset (- L) C"
moreover have "trail_false_cls Γ C"
using more_invars ‹𝒞 = Some C› by metis
ultimately show "trail_false_lit Γ K"
unfolding trail_false_cls_def
by (metis in_diffD)
next
assume K_in: "K ∈# remove1_mset L D"
have "clause_could_propagate Γ' D L"
using invars ‹Γ = (L, Some D) # Γ'› by simp
hence "trail_false_cls Γ' {#K ∈# D. K ≠ L#}"
by (simp only: clause_could_propagate_def)
hence "trail_false_cls Γ {#K ∈# D. K ≠ L#}"
unfolding ‹Γ = (L, Some D) # Γ'›
by (simp add: trail_false_cls_def trail_false_lit_def)
moreover have "K ∈# {#K ∈# D. K ≠ L#}"
using D_max_lit K_in in_diffD linorder_lit.is_greatest_in_mset_iff by fastforce
ultimately show "trail_false_lit Γ K"
unfolding trail_false_cls_def by metis
qed
qed
next
show "atms_of_clss U⇩e⇩r |⊆| atms_of_clss N"
using more_invars by argo
next
show "∀C |∈| ℱ. ∃L. is_pos L ∧ ord_res.is_maximal_lit L C"
using more_invars by metis
qed
next
case step_hyps: (backtrack L Γ' C)
have "{#} |∉| N |∪| U⇩e⇩r"
using more_invars step_hyps(3) by fastforce
hence "{#} |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)"
unfolding mempty_in_fimage_iefac .
hence "¬(∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C)"
using invars ‹Γ = _ # Γ'›
by (metis (no_types, opaque_lifting) split_pairs)
hence "¬(∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ' C)"
by (metis append.simps(1) step_hyps(3) suffix_ConsD suffix_def
trail_false_cls_if_trail_false_suffix)
moreover have "¬ trail_false_cls Γ' C"
by (metis ‹trail_consistent Γ› fst_conv list.distinct(1) list.inject step_hyps(3,4)
trail_consistent.simps trail_defined_lit_def trail_false_cls_def trail_false_lit_def
uminus_lit_swap)
ultimately have "¬(∃C|∈|iefac ℱ |`| (N |∪| finsert C U⇩e⇩r). trail_false_cls Γ' C)"
by (simp add: iefac_def trail_false_cls_def)
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_cls C |⊆| atms_of_clss (N |∪| U⇩e⇩r)"
using more_invars ‹𝒞 = Some C› by metis
hence "atms_of_clss (N |∪| finsert C U⇩e⇩r) = atms_of_clss (N |∪| U⇩e⇩r)"
by auto
show ?thesis
unfolding ‹s' = (finsert C U⇩e⇩r, ℱ, Γ', None)›
proof (intro ord_res_11_invars.intros ord_res_10_invars.intros ballI allI impI conjI)
show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
using invars unfolding ‹Γ = _ # Γ'› by simp
next
fix Ln :: "'f gliteral × 'f gclause option" and C :: "'f gclause"
assume "Ln ∈ set Γ'" and "snd Ln = Some C"
then show "ord_res.is_strictly_maximal_lit (fst Ln) C"
using invars unfolding ‹Γ = _ # Γ'› by simp
next
show "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| finsert C U⇩e⇩r))"
unfolding ‹fset (trail_atms Γ') = set (map (atm_of o fst) Γ')›
unfolding ‹atms_of_clss (N |∪| finsert C U⇩e⇩r) = atms_of_clss (N |∪| U⇩e⇩r)›
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) ([atm_of L] @ map (atm_of ∘ fst) Γ')"
unfolding ‹Γ = _ # Γ'› by simp
next
have "set ([atm_of L] @ map (atm_of ∘ fst) Γ') = fset (trail_atms Γ)"
unfolding append_Cons append_Nil list.set
unfolding ‹fset (trail_atms Γ') = set (map (atm_of o fst) Γ')›[symmetric]
unfolding ‹Γ = _ # Γ'› trail_atms.simps prod.sel
by simp
thus "linorder_trm.is_lower_set (set ([atm_of L] @ map (atm_of ∘ fst) Γ'))
(fset (atms_of_clss (N |∪| U⇩e⇩r)))"
using Γ_lower
by (simp only:)
qed
next
fix
Ln :: "'f gliteral × 'f gclause option" and
Γ'' :: "('f gliteral × 'f gclause option) list"
assume "Γ' = Ln # Γ''"
have "snd Ln = None"
by (simp add: ‹Γ' = Ln # Γ''› invars(4) step_hyps(3))
thus "(snd Ln ≠ None) ⟷ (∃C|∈|iefac ℱ |`| (N |∪| finsert C U⇩e⇩r). trail_false_cls Γ' C)"
using ‹¬(∃C|∈|iefac ℱ |`| (N |∪| finsert C U⇩e⇩r). trail_false_cls Γ' C)›
by argo
show "snd Ln ≠ None ⟹ is_pos (fst Ln)"
using ‹snd Ln = None› by simp
show "⋀C. snd Ln = Some C ⟹ clause_could_propagate Γ'' C (fst Ln)"
using ‹snd Ln = None› by simp
show "⋀D. snd Ln = Some D ⟹ D |∈| iefac ℱ |`| (N |∪| finsert C U⇩e⇩r)"
using ‹snd Ln = None› by simp
show "⋀x. x ∈ set Γ'' ⟹ snd x = None"
by (simp add: ‹Γ' = Ln # Γ''› invars(4) step_hyps(3))
next
fix
Ln :: "'f gliteral × 'f gclause option" and
Γ⇩1 Γ⇩0 :: "('f gliteral × 'f gclause option) list"
assume "Γ' = Γ⇩1 @ Ln # Γ⇩0" and "snd Ln = None"
thus "¬ (∃C|∈|iefac ℱ |`| (N |∪| finsert C U⇩e⇩r). trail_false_cls (Ln # Γ⇩0) C)"
using ‹¬(∃C|∈|iefac ℱ |`| (N |∪| finsert C U⇩e⇩r). trail_false_cls Γ' C)›
by (metis suffixI trail_false_cls_if_trail_false_suffix)
next
have "C ≠ {#}"
using ‹- L ∈# C› by force
hence "{#} |∉| N |∪| finsert C U⇩e⇩r"
using ‹{#} |∉| N |∪| U⇩e⇩r› by simp
thus "{#} |∈| N |∪| finsert C U⇩e⇩r ⟹ Γ' = []"
by contradiction
next
show "⋀D. None = Some D ⟹ atms_of_cls D |⊆| atms_of_clss (N |∪| finsert C U⇩e⇩r)"
by simp
next
show "⋀C. None = Some C ⟹ trail_false_cls Γ' C"
by simp
next
have "atms_of_cls C |⊆| atms_of_clss N"
by (smt (verit, ccfv_threshold) ‹atms_of_cls C |⊆| atms_of_clss (N |∪| U⇩e⇩r)›
atms_of_clss_def fin_mono fmember_ffUnion_iff fsubsetI funion_iff more_invars(6))
thus "atms_of_clss (finsert C U⇩e⇩r) |⊆| atms_of_clss N"
using ‹atms_of_clss U⇩e⇩r |⊆| atms_of_clss N› by simp
next
show "⋀C. C |∈| ℱ ⟹ ∃L. is_pos L ∧ ord_res.is_maximal_lit L C"
using more_invars by metis
qed
qed
qed
qed
lemma rtranclp_ord_res_11_preserves_invars:
assumes
step: "(ord_res_11 N)⇧*⇧* s s'" and
invars: "ord_res_11_invars N s"
shows "ord_res_11_invars N s'"
using step invars ord_res_11_preserves_invars
by (smt (verit, del_insts) rtranclp_induct)
lemma tranclp_ord_res_11_preserves_invars:
assumes
step: "(ord_res_11 N)⇧+⇧+ s s'" and
invars: "ord_res_11_invars N s"
shows "ord_res_11_invars N s'"
using step invars ord_res_11_preserves_invars
by (smt (verit, del_insts) tranclp_induct)
lemma ex_ord_res_11_if_not_final:
assumes
not_final: "¬ ord_res_11_final (N, s)" and
invars: "ord_res_11_invars N s"
shows "∃s'. ord_res_11 N s s'"
using invars
proof (cases N s rule: ord_res_11_invars.cases)
case more_invars: (1 U⇩e⇩r ℱ Γ 𝒞)
show ?thesis
using ‹ord_res_10_invars N (U⇩e⇩r, ℱ, Γ)›
proof (cases N "(U⇩e⇩r, ℱ, Γ)" rule: ord_res_10_invars.cases)
case invars: 1
show ?thesis
proof (cases 𝒞)
case None
show ?thesis
proof (cases "∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C")
case True
then obtain C where
"linorder_cls.is_least_in_fset (ffilter (trail_false_cls Γ) (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
using linorder_cls.ex_is_least_in_ffilter_iff by metis
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = None›
using ord_res_11.conflict by metis
next
case no_false_cls: False
hence "∃A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r). ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2"
using not_final
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = None›
by (smt (verit) invars(3) linorder_trm.antisym_conv3 linorder_trm.not_in_lower_setI
ord_res_11_final.model_found)
then obtain A 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 linorder_trm.ex_is_least_in_ffilter_iff by presburger
show ?thesis
proof (cases "∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)")
case True
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.ex_is_least_in_ffilter_iff by presburger
show ?thesis
proof (cases "∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls ((Pos A, None) # Γ) C")
case True
moreover have "trail_false_cls ((Pos A, None) # Γ) =
trail_false_cls ((Pos A, Some (efac C)) # Γ)"
unfolding trail_false_cls_def trail_false_lit_def by simp
ultimately show ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = None›
using ord_res_11.propagate[OF no_false_cls A_least C_least]
by metis
next
case False
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = None›
using ord_res_11.decide_pos[OF no_false_cls A_least C_least]
by metis
qed
next
case False
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = None›
using ord_res_11.decide_neg[OF no_false_cls A_least] by metis
qed
qed
next
case (Some D)
hence D_false: "trail_false_cls Γ D"
using more_invars by metis
show ?thesis
proof (cases "D = {#}")
case True
hence "Γ ≠ []"
using not_final
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = Some D›
unfolding ord_res_11_final.simps by metis
then obtain L n Γ' where "Γ = (L, n) # Γ'"
by (metis list.exhaust prod.exhaust)
moreover have "- L ∉# D"
unfolding ‹D = {#}› by simp
ultimately show ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹𝒞 = Some D›
using ord_res_11.skip by metis
next
case False
then obtain L n Γ' where "Γ = (L, n) # Γ'"
using D_false[unfolded trail_false_cls_def trail_false_lit_def]
by (metis eq_fst_iff image_iff list.set_cases multiset_nonemptyE)
show ?thesis
proof (cases "- L ∈# D")
case True
show ?thesis
proof (cases n)
case None
show ?thesis
proof (cases "- L ∈# D")
case True
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹Γ = (L, n) # Γ'› ‹n = None› ‹𝒞 = Some D›
using ord_res_11.backtrack by metis
next
case False
thus ?thesis
using ord_res_11.skip
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹Γ = (L, n) # Γ'› ‹n = None› ‹𝒞 = Some D› by metis
qed
next
case (Some C)
thus ?thesis
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹Γ = (L, n) # Γ'› ‹n = Some C› ‹𝒞 = Some D›
using ord_res_11.resolution[OF _ ‹- L ∈# D›] by metis
qed
next
case False
thus ?thesis
using ord_res_11.skip
unfolding ‹s = (U⇩e⇩r, ℱ, Γ, 𝒞)› ‹Γ = (L, n) # Γ'› ‹𝒞 = Some D› by metis
qed
qed
qed
qed
qed
lemma ord_res_11_safe_state_if_invars:
fixes N s
assumes invars: "ord_res_11_invars N s"
shows "safe_state (constant_context ord_res_11) ord_res_11_final (N, s)"
using safe_state_constant_context_if_invars[where
ℛ = ord_res_11 and ℱ = ord_res_11_final and ℐ = ord_res_11_invars]
using ord_res_11_preserves_invars ex_ord_res_11_if_not_final invars by metis
lemma rtrancl_ord_res_11_all_resolution_steps:
assumes C_max_lit: "ord_res.is_strictly_maximal_lit K C"
shows "(ord_res_11 N)⇧*⇧* (U, ℱ, (K, Some C) # Γ, Some D) (U, ℱ, (K, Some C) # Γ, Some (eres C D))"
proof -
obtain CD where "eres C D = CD" and run: "full_run (ground_resolution C) D CD"
using ex1_eres_eq_full_run_ground_resolution by metis
have "(ord_res_11 N)⇧*⇧* (U, ℱ, (K, Some C) # Γ, Some D) (U, ℱ, (K, Some C) # Γ, Some CD)"
proof (rule full_run_preserves_invariant[OF run])
show "(ord_res_11 N)⇧*⇧* (U, ℱ, (K, Some C) # Γ, Some D) (U, ℱ, (K, Some C) # Γ, Some D)"
by simp
next
fix x y
assume "ground_resolution C x y"
hence "ord_res_11 N (U, ℱ, (K, Some C) # Γ, Some x) (U, ℱ, (K, Some C) # Γ, Some y)"
unfolding ground_resolution_def
proof (cases x C y rule: ord_res.ground_resolution.cases)
case res_hyps: (ground_resolutionI A P⇩1' P⇩2')
have "K = - Neg A"
using C_max_lit
by (metis ord_res.Uniq_striclty_maximal_lit_in_ground_cls res_hyps(6) the1_equality'
uminus_Neg)
hence "- K ∈# x"
by (simp add: ‹x = add_mset (Neg A) P⇩1'›)
moreover have "y = remove1_mset (- K) x + remove1_mset K C"
using res_hyps ‹K = - Neg A› by force
ultimately show ?thesis
using ord_res_11.resolution[OF refl, of K x N U ℱ C Γ]
by metis
qed
moreover assume "(ord_res_11 N)⇧*⇧*
(U, ℱ, (K, Some C) # Γ, Some D)
(U, ℱ, (K, Some C) # Γ, Some x)"
ultimately show "(ord_res_11 N)⇧*⇧*
(U, ℱ, (K, Some C) # Γ, Some D)
(U, ℱ, (K, Some C) # Γ, Some y)"
by simp
qed
then show ?thesis
unfolding ‹eres C D = CD›
by argo
qed
lemma rtrancl_ord_res_11_all_skip_steps:
"(ord_res_11 N)⇧*⇧* (U, ℱ, Γ, Some C) (U, ℱ, dropWhile (λLn. - fst Ln ∉# C) Γ, Some C)"
proof (induction Γ)
case Nil
show ?case by simp
next
case (Cons Ln Γ)
show ?case
proof (cases "- fst Ln ∈# C")
case True
hence "dropWhile (λLn. - fst Ln ∉# C) (Ln # Γ) = Ln # Γ"
by simp
thus ?thesis
by simp
next
case False
hence *: "dropWhile (λLn. - fst Ln ∉# C) (Ln # Γ) = dropWhile (λLn. - fst Ln ∉# C) Γ"
by simp
obtain L 𝒞 where "Ln = (L, 𝒞)"
by (metis prod.exhaust)
have "ord_res_11 N (U, ℱ, Ln # Γ, Some C) (U, ℱ, Γ, Some C)"
unfolding ‹Ln = (L, 𝒞)›
proof (rule ord_res_11.skip)
show "- L ∉# C"
using False unfolding ‹Ln = (L, 𝒞)› by simp
qed
thus ?thesis
unfolding *
using Cons.IH
by simp
qed
qed
end
end