Theory Non_Redundancy
theory Non_Redundancy
imports
SCL_FOL
Trail_Induced_Ordering
Initial_Literals_Generalize_Learned_Literals
Multiset_Order_Extra
begin
context scl_fol_calculus begin
section ‹Reasonable Steps›
lemma reasonable_scl_sound_state:
"reasonable_scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
using scl_preserves_sound_state reasonable_scl_def by blast
lemma reasonable_run_sound_state:
"(reasonable_scl N β)⇧*⇧* S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
by (smt (verit, best) reasonable_scl_sound_state rtranclp_induct)
subsection ‹Invariants›
subsubsection ‹No Conflict After Decide›
inductive no_conflict_after_decide for N β U where
Nil[simp]: "no_conflict_after_decide N β U []" |
Cons: "(is_decision_lit Ln ⟶ (∄S'. conflict N β (Ln # Γ, U, None) S')) ⟹
no_conflict_after_decide N β U Γ ⟹ no_conflict_after_decide N β U (Ln # Γ)"
definition no_conflict_after_decide' where
"no_conflict_after_decide' N β S = no_conflict_after_decide N β (state_learned S) (state_trail S)"
lemma no_conflict_after_decide'_initial_state[simp]: "no_conflict_after_decide' N β initial_state"
by (simp add: no_conflict_after_decide'_def no_conflict_after_decide.Nil)
lemma propagate_preserves_no_conflict_after_decide':
assumes "propagate N β S S'" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms
by (auto simp: no_conflict_after_decide'_def propagate_lit_def is_decision_lit_def
elim!: propagate.cases intro!: no_conflict_after_decide.Cons)
lemma decide_preserves_no_conflict_after_decide':
assumes "decide N β S S'" and "∄S''. conflict N β S' S''" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms
by (auto simp: no_conflict_after_decide'_def decide_lit_def is_decision_lit_def
elim!: decide.cases intro!: no_conflict_after_decide.Cons)
lemma conflict_preserves_no_conflict_after_decide':
assumes "conflict N β S S'" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms
by (auto simp: no_conflict_after_decide'_def elim: conflict.cases)
lemma skip_preserves_no_conflict_after_decide':
assumes "skip N β S S'" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms
by (auto simp: no_conflict_after_decide'_def
elim!: skip.cases elim: no_conflict_after_decide.cases)
lemma factorize_preserves_no_conflict_after_decide':
assumes "factorize N β S S'" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms
by (auto simp: no_conflict_after_decide'_def elim: factorize.cases)
lemma resolve_preserves_no_conflict_after_decide':
assumes "resolve N β S S'" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms
by (auto simp: no_conflict_after_decide'_def elim: resolve.cases)
lemma learning_clause_without_conflict_preserves_nex_conflict:
fixes N :: "('f, 'v) Term.term clause fset"
assumes "∄γ. is_ground_cls (C ⋅ γ) ∧ trail_false_cls Γ (C ⋅ γ)"
shows "∄S'. conflict N β (Γ, U, None) S' ⟹ ∄S'. conflict N β (Γ, finsert C U, None) S'"
proof (elim contrapos_nn exE)
fix S'
assume "conflict N β (Γ, finsert C U, None :: ('f, 'v) closure option) S'"
then show "∃S'. conflict N β (Γ, U, None) S'"
proof (cases N β "(Γ, finsert C U, None :: ('f, 'v) closure option)" S' rule: conflict.cases)
case (conflictI D γ)
then show ?thesis
using assms conflict.intros by blast
qed
qed
lemma backtrack_preserves_no_conflict_after_decide':
assumes step: "backtrack N β S S'" and invar: "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using step
proof (cases N β S S' rule: backtrack.cases)
case (backtrackI Γ Γ' Γ'' K L σ D U)
have "no_conflict_after_decide N β U (Γ' @ Γ'')"
using invar
unfolding backtrackI(1,2,3) no_conflict_after_decide'_def
by (auto simp: decide_lit_def elim: no_conflict_after_decide.cases)
hence "no_conflict_after_decide N β U Γ''"
by (induction Γ') (auto elim: no_conflict_after_decide.cases)
hence "no_conflict_after_decide N β (finsert (add_mset L D) U) Γ''"
using backtrackI(5)
proof (induction Γ'')
case Nil
show ?case
by (auto intro: no_conflict_after_decide.Nil)
next
case (Cons Ln Γ'')
hence "∄γ. is_ground_cls (add_mset L D ⋅ γ) ∧ trail_false_cls (Ln # Γ'') (add_mset L D ⋅ γ)"
by metis
hence "∄γ. is_ground_cls (add_mset L D ⋅ γ) ∧ trail_false_cls Γ'' (add_mset L D ⋅ γ)"
by (metis (no_types, opaque_lifting) image_insert insert_iff list.set(2) trail_false_cls_def
trail_false_lit_def)
hence 1: "no_conflict_after_decide N β (finsert (add_mset L D) U) Γ''"
by (rule Cons.IH)
show ?case
proof (intro no_conflict_after_decide.Cons impI)
assume "is_decision_lit Ln"
with Cons.hyps have "∄S'. conflict N β (Ln # Γ'', U, None) S'"
by simp
then show "∄S'. conflict N β (Ln # Γ'', finsert (add_mset L D) U, None) S'"
using learning_clause_without_conflict_preserves_nex_conflict
using ‹∄γ. is_ground_cls (add_mset L D ⋅ γ) ∧ trail_false_cls (Ln # Γ'') (add_mset L D ⋅ γ)›
by blast
next
show "no_conflict_after_decide N β (finsert (add_mset L D) U) Γ''"
using 1 .
qed
qed
thus ?thesis
unfolding backtrackI(1,2) no_conflict_after_decide'_def by simp
qed
lemma reasonable_scl_preserves_no_conflict_after_decide':
assumes "reasonable_scl N β S S'" and "no_conflict_after_decide' N β S"
shows "no_conflict_after_decide' N β S'"
using assms unfolding reasonable_scl_def scl_def
using propagate_preserves_no_conflict_after_decide' decide_preserves_no_conflict_after_decide'
conflict_preserves_no_conflict_after_decide' skip_preserves_no_conflict_after_decide'
factorize_preserves_no_conflict_after_decide' resolve_preserves_no_conflict_after_decide'
backtrack_preserves_no_conflict_after_decide'
by metis
subsection ‹Miscellaneous Lemmas›
lemma before_reasonable_conflict:
assumes conf: "conflict N β S1 S2" and
invars: "learned_nonempty S1" "trail_propagated_or_decided' N β S1"
"no_conflict_after_decide' N β S1"
shows "{#} |∈| N ∨ (∃S0. propagate N β S0 S1)"
using before_conflict[OF conf invars(1,2)]
proof (elim disjE exE)
fix S0 assume "decide N β S0 S1"
hence False
proof (cases N β S0 S1 rule: decide.cases)
case (decideI L γ Γ U)
with invars(3) have "no_conflict_after_decide N β U (trail_decide Γ (L ⋅l γ))"
by (simp add: no_conflict_after_decide'_def)
hence "∄S'. conflict N β (trail_decide Γ (L ⋅l γ), U, None) S'"
by (rule no_conflict_after_decide.cases) (simp_all add: decide_lit_def is_decision_lit_def)
then show ?thesis
using conf unfolding decideI(1,2) by metis
qed
thus ?thesis ..
qed auto
section ‹Regular Steps›
lemma regular_scl_if_conflict[simp]: "conflict N β S S' ⟹ regular_scl N β S S'"
by (simp add: regular_scl_def)
lemma regular_scl_if_skip[simp]: "skip N β S S' ⟹ regular_scl N β S S'"
by (auto simp: regular_scl_def reasonable_scl_def scl_def elim: conflict.cases skip.cases)
lemma regular_scl_if_factorize[simp]: "factorize N β S S' ⟹ regular_scl N β S S'"
by (auto simp: regular_scl_def reasonable_scl_def scl_def elim: conflict.cases factorize.cases)
lemma regular_scl_if_resolve[simp]: "resolve N β S S' ⟹ regular_scl N β S S'"
by (auto simp: regular_scl_def reasonable_scl_def scl_def elim: conflict.cases resolve.cases)
lemma regular_scl_if_backtrack[simp]: "backtrack N β S S' ⟹ regular_scl N β S S'"
by (smt (verit) backtrack.cases decide_well_defined(6) option.discI regular_scl_def conflict.simps
reasonable_scl_def scl_def state_conflict_simp)
lemma regular_scl_sound_state: "regular_scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
by (rule reasonable_scl_sound_state[OF reasonable_if_regular])
lemma regular_run_sound_state:
"(regular_scl N β)⇧*⇧* S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
by (smt (verit, best) regular_scl_sound_state rtranclp_induct)
subsection ‹Invariants›
subsubsection ‹Almost No Conflict With Trail›
inductive no_conflict_with_trail for N β U where
Nil: "(∄S'. conflict N β ([], U, None) S') ⟹ no_conflict_with_trail N β U []" |
Cons: "(∄S'. conflict N β (Ln # Γ, U, None) S') ⟹
no_conflict_with_trail N β U Γ ⟹ no_conflict_with_trail N β U (Ln # Γ)"
lemma nex_conflict_if_no_conflict_with_trail:
assumes "no_conflict_with_trail N β U Γ"
shows "∄S'. conflict N β (Γ, U, None) S'"
using assms by (auto elim: no_conflict_with_trail.cases)
lemma nex_conflict_if_no_conflict_with_trail':
assumes "no_conflict_with_trail N β U Γ"
shows "∄S'. conflict N β ([], U, None) S'"
using assms
by (induction Γ rule: no_conflict_with_trail.induct) simp_all
lemma no_conflict_after_decide_if_no_conflict_with_trail:
"no_conflict_with_trail N β U Γ ⟹ no_conflict_after_decide N β U Γ"
by (induction Γ rule: no_conflict_with_trail.induct)
(simp_all add: no_conflict_after_decide.Cons)
lemma not_trail_false_cls_if_no_conflict_with_trail:
"no_conflict_with_trail N β U Γ ⟹ D |∈| N |∪| U ⟹ D ≠ {#} ⟹ is_ground_cls (D ⋅ γ) ⟹
¬ trail_false_cls Γ (D ⋅ γ)"
proof (induction Γ rule: no_conflict_with_trail.induct)
case Nil
thus ?case by simp
next
case (Cons Ln Γ)
hence "¬ trail_false_cls (Ln # Γ) (D ⋅ γ)"
by (metis fst_conv not_trail_false_ground_cls_if_no_conflict state_conflict_simp
state_learned_simp state_trail_def)
thus ?case
by simp
qed
definition almost_no_conflict_with_trail where
"almost_no_conflict_with_trail N β S ⟷
{#} |∈| N ∧ state_trail S = [] ∨
no_conflict_with_trail N β (state_learned S)
(case state_trail S of [] ⇒ [] | Ln # Γ ⇒ if is_decision_lit Ln then Ln # Γ else Γ)"
lemma nex_conflict_if_no_conflict_with_trail'':
assumes no_conf: "state_conflict S = None" and "{#} |∉| N" and "learned_nonempty S"
"no_conflict_with_trail N β (state_learned S) (state_trail S)"
shows "∄S'. conflict N β S S'"
proof -
from no_conf obtain Γ U where S_def: "S = (Γ, U, None)"
by (metis state_simp)
from ‹learned_nonempty S› have "{#} |∉| U"
by (simp add: S_def learned_nonempty_def)
show ?thesis
using assms(4)
unfolding S_def state_proj_simp
proof (cases N β U Γ rule: no_conflict_with_trail.cases)
case Nil
then show "∄S'. conflict N β (Γ, U, None) S'"
using ‹{#} |∉| N› ‹{#} |∉| U›
by (auto simp: trail_false_cls_def elim: conflict.cases)
next
case (Cons Ln Γ')
then show "∄S'. conflict N β (Γ, U, None) S'"
by (auto intro: no_conflict_tail_trail)
qed
qed
lemma no_conflict_with_trail_if_nex_conflict:
assumes no_conf: "∄S'. conflict N β S S'" "state_conflict S = None"
shows "no_conflict_with_trail N β (state_learned S) (state_trail S)"
proof -
from no_conf(2) obtain Γ U where S_def: "S = (Γ, U, None)"
by (metis state_simp)
show ?thesis
using no_conf(1)
unfolding S_def state_proj_simp
proof (induction Γ)
case Nil
thus ?case by (simp add: no_conflict_with_trail.Nil)
next
case (Cons Ln Γ)
have "∄a. conflict N β (Γ, U, None) a"
by (rule no_conflict_tail_trail[OF Cons.prems])
hence "no_conflict_with_trail N β U Γ"
by (rule Cons.IH)
then show ?case
using Cons.prems
by (auto intro: no_conflict_with_trail.Cons)
qed
qed
lemma almost_no_conflict_with_trail_if_no_conflict_with_trail:
"no_conflict_with_trail N β U Γ ⟹ almost_no_conflict_with_trail N β (Γ, U, Cl)"
by (cases Γ) (auto simp: almost_no_conflict_with_trail_def elim: no_conflict_with_trail.cases)
lemma almost_no_conflict_with_trail_initial_state[simp]:
"almost_no_conflict_with_trail N β initial_state"
by (cases "{#} |∈| N") (auto simp: almost_no_conflict_with_trail_def trail_false_cls_def
elim!: conflict.cases intro: no_conflict_with_trail.Nil)
lemma propagate_preserves_almost_no_conflict_with_trail:
assumes step: "propagate N β S S'" and reg_step: "regular_scl N β S S'"
shows "almost_no_conflict_with_trail N β S'"
using reg_step[unfolded regular_scl_def]
proof (elim disjE conjE)
assume "conflict N β S S'"
with step have False
using conflict_well_defined by blast
thus ?thesis ..
next
assume no_conf: "∄S'. conflict N β S S'" and "reasonable_scl N β S S'"
from step show ?thesis
proof (cases N β S S' rule: propagate.cases)
case step_hyps: (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)
have "no_conflict_with_trail N β U Γ"
by (rule no_conflict_with_trail_if_nex_conflict[OF no_conf,
unfolded step_hyps state_proj_simp, OF refl])
thus ?thesis
unfolding step_hyps(1,2)
by (simp add: almost_no_conflict_with_trail_def propagate_lit_def is_decision_lit_def)
qed
qed
lemma decide_preserves_almost_no_conflict_with_trail:
assumes step: "decide N β S S'" and reg_step: "regular_scl N β S S'"
shows "almost_no_conflict_with_trail N β S'"
proof -
from reg_step have res_step: "reasonable_scl N β S S'"
by (rule reasonable_if_regular)
from step obtain Γ U where S'_def: "S' = (Γ, U, None)"
by (auto elim: decide.cases)
have "no_conflict_with_trail N β (state_learned S') (state_trail S')"
proof (rule no_conflict_with_trail_if_nex_conflict)
show "∄S''. conflict N β S' S''"
using step res_step[unfolded reasonable_scl_def] by argo
next
show "state_conflict S' = None"
by (simp add: S'_def)
qed
thus ?thesis
unfolding S'_def
by (simp add: almost_no_conflict_with_trail_if_no_conflict_with_trail)
qed
lemma almost_no_conflict_with_trail_conflict_not_relevant:
"almost_no_conflict_with_trail N β (Γ, U, Cl1) ⟷
almost_no_conflict_with_trail N β (Γ, U, Cl2)"
by (simp add: almost_no_conflict_with_trail_def)
lemma conflict_preserves_almost_no_conflict_with_trail:
assumes step: "conflict N β S S'" and invar: "almost_no_conflict_with_trail N β S"
shows "almost_no_conflict_with_trail N β S'"
proof -
from step obtain Γ U Cl where "S = (Γ, U, None)" and "S' = (Γ, U, Some Cl)"
by (auto elim: conflict.cases)
with invar show ?thesis
using almost_no_conflict_with_trail_conflict_not_relevant by metis
qed
lemma skip_preserves_almost_no_conflict_with_trail:
assumes step: "skip N β S S'" and invar: "almost_no_conflict_with_trail N β S"
shows "almost_no_conflict_with_trail N β S'"
using step
proof (cases N β S S' rule: skip.cases)
case step_hyps: (skipI L D σ n Γ U)
have "no_conflict_with_trail N β U (if is_decision_lit (L, n) then (L, n) # Γ else Γ)"
using invar unfolding step_hyps(1,2) by (simp add: almost_no_conflict_with_trail_def)
hence "no_conflict_with_trail N β U Γ"
by (cases "is_decision_lit (L, n)") (auto elim: no_conflict_with_trail.cases)
then show ?thesis
unfolding step_hyps(1,2)
by (rule almost_no_conflict_with_trail_if_no_conflict_with_trail)
qed
lemma factorize_preserves_almost_no_conflict_with_trail:
assumes step: "factorize N β S S'" and invar: "almost_no_conflict_with_trail N β S"
shows "almost_no_conflict_with_trail N β S'"
proof -
from step obtain Γ U Cl1 Cl2 where "S = (Γ, U, Some Cl1)" and "S' = (Γ, U, Some Cl2)"
by (auto elim: factorize.cases)
with invar show ?thesis
using almost_no_conflict_with_trail_conflict_not_relevant by metis
qed
lemma resolve_preserves_almost_no_conflict_with_trail:
assumes step: "resolve N β S S'" and invar: "almost_no_conflict_with_trail N β S"
shows "almost_no_conflict_with_trail N β S'"
proof -
from step obtain Γ U Cl1 Cl2 where "S = (Γ, U, Some Cl1)" and "S' = (Γ, U, Some Cl2)"
by (auto elim: resolve.cases)
with invar show ?thesis
using almost_no_conflict_with_trail_conflict_not_relevant by metis
qed
lemma backtrack_preserves_almost_no_conflict_with_trail:
assumes step: "backtrack N β S S'" and invar: "almost_no_conflict_with_trail N β S"
shows "almost_no_conflict_with_trail N β S'"
using step
proof (cases N β S S' rule: backtrack.cases)
case step_hyps: (backtrackI Γ Γ' Γ'' K L σ D U)
from invar have "no_conflict_with_trail N β U ((- (L ⋅l σ), None) # Γ' @ Γ'')"
by (simp add: step_hyps almost_no_conflict_with_trail_def decide_lit_def is_decision_lit_def)
hence "no_conflict_with_trail N β U (Γ' @ Γ'')"
by (auto elim: no_conflict_with_trail.cases)
hence "no_conflict_with_trail N β U Γ''"
by (induction Γ') (auto elim: no_conflict_with_trail.cases)
then have "no_conflict_with_trail N β (finsert (add_mset L D) U) Γ''"
by (metis learning_clause_without_conflict_preserves_nex_conflict
nex_conflict_if_no_conflict_with_trail no_conflict_with_trail_if_nex_conflict
state_conflict_simp state_learned_simp state_trail_simp step_hyps(5))
thus ?thesis
unfolding step_hyps(1,2)
by (rule almost_no_conflict_with_trail_if_no_conflict_with_trail)
qed
lemma regular_scl_preserves_almost_no_conflict_with_trail:
assumes "regular_scl N β S S'" and "almost_no_conflict_with_trail N β S"
shows "almost_no_conflict_with_trail N β S'"
using assms
using propagate_preserves_almost_no_conflict_with_trail decide_preserves_almost_no_conflict_with_trail
conflict_preserves_almost_no_conflict_with_trail skip_preserves_almost_no_conflict_with_trail
factorize_preserves_almost_no_conflict_with_trail resolve_preserves_almost_no_conflict_with_trail
backtrack_preserves_almost_no_conflict_with_trail
by (metis scl_def reasonable_if_regular scl_if_reasonable)
subsubsection ‹Backtrack Follows Regular Conflict Resolution›
lemma before_conflict_in_regular_run:
assumes
reg_run: "(regular_scl N β)⇧*⇧* initial_state S1" and
conf: "conflict N β S1 S2" and
"{#} |∉| N"
shows "∃S0. (regular_scl N β)⇧*⇧* initial_state S0 ∧ regular_scl N β S0 S1 ∧ (propagate N β S0 S1)"
proof -
from reg_run conf show ?thesis
proof (induction S1 arbitrary: S2 rule: rtranclp_induct)
case base
with ‹{#} |∉| N› have False
by (meson fempty_iff funion_iff mempty_in_iff_ex_conflict)
thus ?case ..
next
case (step S0 S1)
from step.hyps(1) have "learned_nonempty S0"
by (induction S0 rule: rtranclp_induct)
(simp_all add: scl_preserves_learned_nonempty[OF scl_if_reasonable[OF
reasonable_if_regular]])
with step.hyps(2) have "learned_nonempty S1"
by (simp add: scl_preserves_learned_nonempty[OF scl_if_reasonable[OF reasonable_if_regular]])
from step.hyps(1) have "trail_propagated_or_decided' N β S0"
by (induction S0 rule: rtranclp_induct)
(simp_all add: scl_preserves_trail_propagated_or_decided[OF scl_if_reasonable[OF
reasonable_if_regular]])
with step.hyps(2) have "trail_propagated_or_decided' N β S1"
by (simp add: scl_preserves_trail_propagated_or_decided[OF scl_if_reasonable[OF
reasonable_if_regular]])
from step.hyps(1) have "almost_no_conflict_with_trail N β S0"
by (induction S0 rule: rtranclp_induct)
(simp_all add: regular_scl_preserves_almost_no_conflict_with_trail)
with step.hyps(2) have "almost_no_conflict_with_trail N β S1"
by (simp add: regular_scl_preserves_almost_no_conflict_with_trail)
show ?case
proof (intro exI conjI)
show "(regular_scl N β)⇧*⇧* initial_state S0"
using step.hyps by simp
next
show "regular_scl N β S0 S1"
using step.hyps by simp
next
from step.prems obtain Γ U C γ where
S1_def: "S1 = (Γ, U, None)" and
S2_def: "S2 = (Γ, U, Some (C, γ))" and
C_in: "C |∈| N |∪| U" and
ground_conf: "is_ground_cls (C ⋅ γ)" and
tr_false_conf: "trail_false_cls Γ (C ⋅ γ)"
unfolding conflict.simps by auto
with step.hyps have "¬ conflict N β S0 S1" and "reasonable_scl N β S0 S1"
unfolding regular_scl_def by (simp_all add: conflict.simps)
with step.prems have "scl N β S0 S1" and "¬ decide N β S0 S1"
unfolding reasonable_scl_def by blast+
moreover from step.prems have "¬ backtrack N β S0 S1"
proof (cases Γ)
case Nil
then show ?thesis
using ‹{#} |∉| N› ‹almost_no_conflict_with_trail N β S1› step.prems
by (auto simp: S1_def almost_no_conflict_with_trail_def elim: no_conflict_with_trail.cases)
next
case (Cons Ln Γ')
have "C ≠ {#}"
using ‹{#} |∉| N›
by (metis C_in S1_def ‹learned_nonempty S1› funionE learned_nonempty_def state_proj_simp(2))
from Cons have "¬ is_decision_lit Ln"
using ‹¬ decide N β S0 S1›[unfolded S1_def]
by (metis (mono_tags, lifting) S1_def ‹almost_no_conflict_with_trail N β S1›
almost_no_conflict_with_trail_def list.discI list.simps(5)
nex_conflict_if_no_conflict_with_trail state_learned_simp state_trail_simp step.prems)
with ‹{#} |∉| N› have "no_conflict_with_trail N β U Γ'"
using ‹almost_no_conflict_with_trail N β S1›
by (simp add: Cons S1_def almost_no_conflict_with_trail_def)
with Cons show ?thesis
unfolding S1_def
using ‹{#} |∉| N›
by (smt (verit) S2_def ‹almost_no_conflict_with_trail N β S0› ‹learned_nonempty S1›
almost_no_conflict_with_trail_def backtrack.simps conflict.cases finsert_iff funionE
funion_finsert_right learned_nonempty_def list.case(2) list.sel(3) list.simps(3)
no_conflict_with_trail.simps not_trail_false_cls_if_no_conflict_with_trail
state_learned_simp state_trail_simp step.prems suffixI decide_lit_def
trail_false_cls_if_trail_false_suffix)
qed
ultimately show "propagate N β S0 S1"
by (simp add: scl_def S1_def skip.simps conflict.simps factorize.simps resolve.simps)
qed
qed
qed
definition regular_conflict_resolution where
"regular_conflict_resolution N β S ⟷ {#} |∉| N ⟶
(case state_conflict S of
None ⇒ (regular_scl N β)⇧*⇧* initial_state S |
Some _ ⇒ (∃S0 S1 S2 S3. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ regular_scl N β S1 S2 ∧
(factorize N β)⇧*⇧* S2 S3 ∧ (regular_scl N β)⇧*⇧* S2 S3 ∧
(S3 = S ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S))))"
lemma regular_conflict_resolution_initial_state[simp]:
"regular_conflict_resolution N β initial_state"
by (simp add: regular_conflict_resolution_def)
lemma propagate_preserves_regular_conflict_resolution:
assumes step: "propagate N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step have "state_conflict S = None" and "state_conflict S' = None"
by (auto elim: propagate.cases)
show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = None›
unfolding option.case
proof (rule impI)
assume "{#} |∉| N"
with invar have "(regular_scl N β)⇧*⇧* initial_state S"
unfolding regular_conflict_resolution_def ‹state_conflict S = None› by simp
thus "(regular_scl N β)⇧*⇧* initial_state S'"
using reg_step by (rule rtranclp.rtrancl_into_rtrancl)
qed
qed
lemma decide_preserves_regular_conflict_resolution:
assumes step: "decide N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step have "state_conflict S = None" and "state_conflict S' = None"
by (auto elim: decide.cases)
show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = None›
unfolding option.case
proof (rule impI)
assume "{#} |∉| N"
with invar have "(regular_scl N β)⇧*⇧* initial_state S"
unfolding regular_conflict_resolution_def ‹state_conflict S = None› by simp
thus "(regular_scl N β)⇧*⇧* initial_state S'"
using reg_step by (rule rtranclp.rtrancl_into_rtrancl)
qed
qed
lemma conflict_preserves_regular_conflict_resolution:
assumes step: "conflict N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step obtain C γ where "state_conflict S = None" and "state_conflict S' = Some (C, γ)"
by (auto elim!: conflict.cases)
show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = Some (C, γ)›
unfolding option.cases
proof (rule impI)
assume "{#} |∉| N"
with invar have reg_run: "(regular_scl N β)⇧*⇧* initial_state S"
unfolding regular_conflict_resolution_def ‹state_conflict S = None› by simp
from ‹{#} |∉| N› obtain S0 where
"(regular_scl N β)⇧*⇧* initial_state S0" "propagate N β S0 S" "regular_scl N β S0 S"
using before_conflict_in_regular_run[OF reg_run step] by metis
with step show "∃S0 S1 S2 S3. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ regular_scl N β S1 S2 ∧
(factorize N β)⇧*⇧* S2 S3 ∧ (regular_scl N β)⇧*⇧* S2 S3 ∧
(S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S'))"
using regular_scl_if_conflict
by blast
qed
qed
lemma
assumes "almost_no_conflict_with_trail N β S" and "{#} |∉| N"
shows "no_conflict_after_decide' N β S"
proof -
obtain U Γ Cl where S_def: "S = (Γ, U, Cl)"
by (metis state_simp)
show ?thesis
proof (cases Γ)
case Nil
thus ?thesis
by (simp add: S_def no_conflict_after_decide'_def)
next
case (Cons Ln Γ')
with assms have no_conf_with_trail:
"no_conflict_with_trail N β U (if is_decision_lit Ln then Ln # Γ' else Γ')"
by (simp add: S_def almost_no_conflict_with_trail_def)
show ?thesis
using no_conf_with_trail
by (cases "is_decision_lit Ln")
(simp_all add: S_def Cons no_conflict_after_decide'_def no_conflict_after_decide.Cons
no_conflict_after_decide_if_no_conflict_with_trail)
qed
qed
lemma mempty_not_in_learned_if_almost_no_conflict_with_trail:
"almost_no_conflict_with_trail N β S ⟹ {#} |∉| N ⟹ {#} |∉| state_learned S"
unfolding almost_no_conflict_with_trail_def
using nex_conflict_if_no_conflict_with_trail'[folded mempty_in_iff_ex_conflict]
by simp
lemma skip_preserves_regular_conflict_resolution:
assumes step: "skip N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step obtain C γ where
"state_conflict S = Some (C, γ)" and "state_conflict S' = Some (C, γ)"
by (auto elim!: skip.cases)
show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = Some (C, γ)›
unfolding option.cases
proof (intro impI)
assume "{#} |∉| N"
with invar obtain S0 S1 S2 S3 where
reg_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
confl: "conflict N β S1 S2" "regular_scl N β S1 S2" and
facto: "(factorize N β)⇧*⇧* S2 S3" "(regular_scl N β)⇧*⇧* S2 S3" and
maybe_reso: "S3 = S ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S)"
unfolding regular_conflict_resolution_def ‹state_conflict S = Some (C, γ)›
unfolding option.cases
by metis
from reg_run have "(regular_scl N β)⇧*⇧* initial_state S1"
using ‹regular_scl N β S0 S1› by simp
hence "(regular_scl N β)⇧*⇧* initial_state S2"
using ‹regular_scl N β S1 S2› by simp
hence "(regular_scl N β)⇧*⇧* initial_state S3"
using ‹(regular_scl N β)⇧*⇧* S2 S3› by simp
from ‹(factorize N β)⇧*⇧* S2 S3› have "state_trail S3 = state_trail S2"
by (induction S3 rule: rtranclp_induct) (auto elim: factorize.cases)
also from ‹conflict N β S1 S2› have "… = state_trail S1"
by (auto elim: conflict.cases)
finally have "state_trail S3 = state_trail S1"
by assumption
from ‹(factorize N β)⇧*⇧* S2 S3› have "state_learned S3 = state_learned S2"
proof (induction S3 rule: rtranclp_induct)
case base
show ?case by simp
next
case (step y z)
thus ?case
by (elim factorize.cases) simp
qed
also from ‹conflict N β S1 S2› have "… = state_learned S1"
by (auto elim: conflict.cases)
finally have "state_learned S3 = state_learned S1"
by assumption
from ‹propagate N β S0 S1› have "state_learned S1 = state_learned S0"
by (auto elim: propagate.cases)
from ‹propagate N β S0 S1› obtain L C γ where
"state_trail S1 = trail_propagate (state_trail S0) L C γ"
by (auto elim: propagate.cases)
from ‹(regular_scl N β)⇧*⇧* initial_state S3› have "almost_no_conflict_with_trail N β S3"
using regular_scl_preserves_almost_no_conflict_with_trail
by (induction S3 rule: rtranclp_induct) simp_all
show "∃S0 S1 S2 S3. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ regular_scl N β S1 S2 ∧
(factorize N β)⇧*⇧* S2 S3 ∧ (regular_scl N β)⇧*⇧* S2 S3 ∧
(S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S'))"
using reg_run propa confl facto
proof (intro impI exI conjI)
show "S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S')"
using maybe_reso
proof (elim disjE exE conjE)
fix S4 assume "resolve N β S3 S4" and "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
with step have "∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S'"
by (meson rtranclp.rtrancl_into_rtrancl sup2CI)
thus ?thesis ..
next
assume "S3 = S"
with ‹almost_no_conflict_with_trail N β S3› ‹{#} |∉| N›
have no_conf_with_trail: "no_conflict_with_trail N β (state_learned S)
(case state_trail S of [] ⇒ [] | Ln # Γ ⇒ if is_decision_lit Ln then Ln # Γ else Γ)"
by (simp add: almost_no_conflict_with_trail_def)
hence "{#} |∉| state_learned S"
using nex_conflict_if_no_conflict_with_trail'[folded mempty_in_iff_ex_conflict]
by simp
from no_conf_with_trail
have no_conf_with_trail': "no_conflict_with_trail N β (state_learned S1) (state_trail S0)"
using ‹S3 = S› ‹state_trail S3 = state_trail S1›
‹state_learned S3 = state_learned S1›
‹state_trail S1 = trail_propagate (state_trail S0) L C γ›
by (simp add: propagate_lit_def is_decision_lit_def)
have "∃D γ⇩D. state_conflict S2 = Some (D, γ⇩D) ∧ - (L ⋅l γ) ∈# D ⋅ γ⇩D"
using ‹conflict N β S1 S2›
proof (cases N β S1 S2 rule: conflict.cases)
case (conflictI D U γ⇩D Γ)
hence "trail_false_cls (trail_propagate (state_trail S0) L C γ) (D ⋅ γ⇩D)"
using ‹state_trail S1 = trail_propagate (state_trail S0) L C γ›
by simp
moreover from no_conf_with_trail' have "¬ trail_false_cls (state_trail S0) (D ⋅ γ⇩D)"
unfolding ‹state_learned S1 = state_learned S0›
proof (rule not_trail_false_cls_if_no_conflict_with_trail)
show "D |∈| N |∪| state_learned S0"
using ‹state_learned S1 = state_learned S0› local.conflictI(1) local.conflictI(3)
by fastforce
next
have "{#} |∉| U"
using ‹{#} |∉| state_learned S› ‹S3 = S› ‹state_learned S3 = state_learned S1›
unfolding conflictI(1,2)
by simp
thus "D ≠ {#}"
using ‹{#} |∉| N› ‹D |∈| N |∪| U›
by auto
next
show "is_ground_cls (D ⋅ γ⇩D)"
by (rule ‹is_ground_cls (D ⋅ γ⇩D)›)
qed
ultimately have "- (L ⋅l γ) ∈# D ⋅ γ⇩D"
by (metis subtrail_falseI propagate_lit_def)
moreover have "state_conflict S2 = Some (D, γ⇩D)"
unfolding conflictI(1,2) by simp
ultimately show ?thesis
by metis
qed
then obtain D γ⇩D where "state_conflict S2 = Some (D, γ⇩D)" and "- (L ⋅l γ) ∈# D ⋅ γ⇩D"
by metis
with ‹(factorize N β)⇧*⇧* S2 S3›
have "∃D' γ⇩D'. state_conflict S3 = Some (D', γ⇩D') ∧ - (L ⋅l γ) ∈# D' ⋅ γ⇩D'"
proof (induction S3 arbitrary: rule: rtranclp_induct)
case base
thus ?case by simp
next
case (step y z)
then obtain D' γ⇩D' where "state_conflict y = Some (D', γ⇩D')" and "- (L ⋅l γ) ∈# D' ⋅ γ⇩D'"
by auto
then show ?case
using step.hyps(2)
by (metis conflict_set_after_factorization)
qed
with step have False
using ‹state_trail S3 = state_trail S1›
unfolding ‹S3 = S› ‹state_trail S1 = trail_propagate (state_trail S0) L C γ›
by (auto simp add: propagate_lit_def elim!: skip.cases)
thus ?thesis ..
qed
qed
qed
qed
lemma factorize_preserves_regular_conflict_resolution:
assumes step: "factorize N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step obtain C γ C' γ' where
"state_conflict S = Some (C, γ)" and "state_conflict S' = Some (C', γ')"
by (auto elim!: factorize.cases)
show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = Some (C', γ')›
unfolding option.cases
proof (intro impI)
assume "{#} |∉| N"
with invar obtain S0 S1 S2 S3 where
reg_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
confl: "conflict N β S1 S2" "regular_scl N β S1 S2" and
facto: "(factorize N β)⇧*⇧* S2 S3" "(regular_scl N β)⇧*⇧* S2 S3" and
maybe_reso: "S3 = S ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S)"
unfolding regular_conflict_resolution_def ‹state_conflict S = Some (C, γ)›
unfolding option.cases
by metis
show "∃S0 S1 S2 S3. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ regular_scl N β S1 S2 ∧
(factorize N β)⇧*⇧* S2 S3 ∧ (regular_scl N β)⇧*⇧* S2 S3 ∧
(S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S'))"
using maybe_reso
proof (elim disjE exE conjE)
assume "S3 = S"
show ?thesis
using reg_run propa confl
proof (intro exI conjI)
show "(factorize N β)⇧*⇧* S2 S'"
using ‹(factorize N β)⇧*⇧* S2 S3› step
by (simp add: ‹S3 = S›)
next
show "(regular_scl N β)⇧*⇧* S2 S'"
using ‹(regular_scl N β)⇧*⇧* S2 S3› reg_step
by (simp add: ‹S3 = S›)
next
show "S' = S' ∨ (∃S4. resolve N β S' S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S')"
by simp
qed
next
fix S4 assume hyps: "resolve N β S3 S4" "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
show ?thesis
using reg_run propa confl facto
proof (intro exI conjI)
show "S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S')"
using hyps step
by (meson rtranclp.rtrancl_into_rtrancl sup2CI)
qed
qed
qed
qed
lemma resolve_preserves_regular_conflict_resolution:
assumes step: "resolve N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step obtain C γ C' γ' where
"state_conflict S = Some (C, γ)" and "state_conflict S' = Some (C', γ')"
by (auto elim!: resolve.cases)
show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = Some (C', γ')›
unfolding option.cases
proof (intro impI)
from step have "state_conflict S ≠ None"
by (auto elim: resolve.cases)
assume "{#} |∉| N"
with invar obtain S0 S1 S2 S3 where
reg_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
"propagate N β S0 S1" "regular_scl N β S0 S1" and
"conflict N β S1 S2" "regular_scl N β S1 S2" and
"(factorize N β)⇧*⇧* S2 S3" "(regular_scl N β)⇧*⇧* S2 S3" and
maybe_reso: "S3 = S ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S)"
unfolding regular_conflict_resolution_def ‹state_conflict S = Some (C, γ)›
unfolding option.cases
by metis
then show "∃S0 S1 S2 S3. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ regular_scl N β S1 S2 ∧
(factorize N β)⇧*⇧* S2 S3 ∧ (regular_scl N β)⇧*⇧* S2 S3 ∧
(S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S'))"
proof (intro exI conjI)
show "S3 = S' ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S')"
using maybe_reso step
by (metis (no_types, opaque_lifting) rtranclp.rtrancl_into_rtrancl rtranclp.rtrancl_refl
sup2I2)
qed
qed
qed
lemma backtrack_preserves_regular_conflict_resolution:
assumes step: "backtrack N β S S'" and reg_step: "regular_scl N β S S'" and
invar: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
proof -
from step obtain C γ where
"state_conflict S = Some (C, γ)" and "state_conflict S' = None"
by (auto elim!: backtrack.cases)
show ?thesis
unfolding regular_conflict_resolution_def ‹state_conflict S' = None›
unfolding option.case
proof (rule impI)
assume "{#} |∉| N"
with invar obtain S0 S1 S2 S3 where
reg_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
confl: "conflict N β S1 S2" "regular_scl N β S1 S2" and
facto: "(factorize N β)⇧*⇧* S2 S3" "(regular_scl N β)⇧*⇧* S2 S3" and
maybe_reso: "S3 = S ∨ (∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S)"
unfolding regular_conflict_resolution_def ‹state_conflict S = Some (C, γ)›
unfolding option.cases
by metis
from reg_run propa(2) confl(2) facto(2) have reg_run_S3: "(regular_scl N β)⇧*⇧* initial_state S3"
by simp
show "(regular_scl N β)⇧*⇧* initial_state S'"
using maybe_reso
proof (elim disjE exE conjE)
show "S3 = S ⟹ (regular_scl N β)⇧*⇧* initial_state S'"
using reg_run_S3 reg_step by simp
next
fix S4 assume hyps: "resolve N β S3 S4" "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
have "(regular_scl N β)⇧*⇧* initial_state S4"
using reg_run_S3 regular_scl_if_resolve[OF hyps(1)]
by (rule rtranclp.rtrancl_into_rtrancl)
also have "(regular_scl N β)⇧*⇧* S4 S"
using hyps(2)
by (rule mono_rtranclp[rule_format, rotated]) auto
also have "(regular_scl N β)⇧*⇧* S S'"
using reg_step by simp
finally show "(regular_scl N β)⇧*⇧* initial_state S'"
by assumption
qed
qed
qed
lemma regular_scl_preserves_regular_conflict_resolution:
assumes reg_step: "regular_scl N β S S'" and
invars: "regular_conflict_resolution N β S"
shows "regular_conflict_resolution N β S'"
using assms
using propagate_preserves_regular_conflict_resolution decide_preserves_regular_conflict_resolution
conflict_preserves_regular_conflict_resolution skip_preserves_regular_conflict_resolution
factorize_preserves_regular_conflict_resolution resolve_preserves_regular_conflict_resolution
backtrack_preserves_regular_conflict_resolution
by (metis regular_scl_def reasonable_scl_def scl_def)
subsection ‹Miscellaneous Lemmas›
lemma mempty_not_in_initial_clauses_if_non_empty_regular_conflict:
assumes "state_conflict S = Some (C, γ)" and "C ≠ {#}" and
invars: "almost_no_conflict_with_trail N β S" "sound_state N β S" "ground_false_closures S"
shows "{#} |∉| N"
proof -
from assms(1) obtain Γ U where S_def: "S = (Γ, U, Some (C, γ))"
by (metis state_simp)
from assms(2) obtain L C' where C_def: "C = add_mset L C'"
using multi_nonempty_split by metis
from invars(3) have "trail_false_cls Γ (C ⋅ γ)"
by (simp add: S_def ground_false_closures_def)
then obtain Ln Γ' where "Γ = Ln # Γ'"
by (metis assms(2) neq_Nil_conv not_trail_false_Nil(2) subst_cls_empty_iff)
with invars(1) have "no_conflict_with_trail N β U (if is_decision_lit Ln then Ln # Γ' else Γ')"
by (simp add: S_def almost_no_conflict_with_trail_def)
hence "∄S'. conflict N β ([], U, None) S'"
by (rule nex_conflict_if_no_conflict_with_trail')
hence "{#} |∉| N |∪| U"
unfolding mempty_in_iff_ex_conflict[symmetric] by assumption
thus ?thesis
by simp
qed
lemma mempty_not_in_initial_clauses_if_regular_run_reaches_non_empty_conflict:
assumes "(regular_scl N β)⇧*⇧* initial_state S" and "state_conflict S = Some (C, γ)" and "C ≠ {#}"
shows "{#} |∉| N"
proof (rule notI)
from assms(2) have "initial_state ≠ S" by fastforce
then obtain S' where
reg_scl_init_S': "regular_scl N β initial_state S'" and "(regular_scl N β)⇧*⇧* S' S"
by (metis assms(1) converse_rtranclpE)
assume "{#} |∈| N"
hence "conflict N β initial_state ([], {||}, Some ({#}, Var))"
by (rule conflict_initial_state_if_mempty_in_intial_clauses)
hence conf_init: "regular_scl N β initial_state ([], {||}, Some ({#}, Var))"
using regular_scl_def by blast
then obtain γ where S'_def: "S' = ([], {||}, Some ({#}, γ))"
using reg_scl_init_S'
unfolding regular_scl_def
using ‹conflict N β initial_state ([], {||}, Some ({#}, Var))›
conflict_initial_state_only_with_mempty
by blast
have "∄S'. scl N β ([], {||}, Some ({#}, γ)) S'" for γ
using no_more_step_if_conflict_mempty by simp
hence "∄S'. regular_scl N β ([], {||}, Some ({#}, γ)) S'" for γ
using scl_if_reasonable[OF reasonable_if_regular] by blast
hence "S = S'"
using ‹(regular_scl N β)⇧*⇧* S' S›
unfolding S'_def
by (metis converse_rtranclpE)
with assms(2,3) show False by (simp add: S'_def)
qed
lemma before_regular_backtrack:
assumes
backt: "backtrack N β S S'" and
invars: "sound_state N β S" "almost_no_conflict_with_trail N β S"
"regular_conflict_resolution N β S" "ground_false_closures S"
shows "∃S0 S1 S2 S3 S4. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ (factorize N β)⇧*⇧* S2 S3 ∧ resolve N β S3 S4 ∧
(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
proof -
from backt obtain L C γ where conflict_S: "state_conflict S = Some (add_mset L C, γ)"
by (auto elim: backtrack.cases)
have "{#} |∉| N"
proof (rule mempty_not_in_initial_clauses_if_non_empty_regular_conflict)
show "state_conflict S = Some (add_mset L C, γ)"
by (rule ‹state_conflict S = Some (add_mset L C, γ)›)
next
show "add_mset L C ≠ {#}"
by simp
next
show "almost_no_conflict_with_trail N β S"
by (rule ‹almost_no_conflict_with_trail N β S›)
next
show "sound_state N β S"
by (rule ‹sound_state N β S›)
next
show "ground_false_closures S"
by (rule ‹ground_false_closures S›)
qed
then obtain S0 S1 S2 S3 where
reg_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
confl: "conflict N β S1 S2" and
fact: "(factorize N β)⇧*⇧* S2 S3" and
maybe_resolution: "S3 = S ∨
(∃S4. resolve N β S3 S4 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S)"
using ‹regular_conflict_resolution N β S› ‹state_conflict S = Some (add_mset L C, γ)›
unfolding regular_conflict_resolution_def conflict_S option.case
by metis
have "S3 ≠ S"
proof (rule notI)
from ‹(factorize N β)⇧*⇧* S2 S3› have "state_trail S3 = state_trail S2"
by (induction S3 rule: rtranclp_induct) (auto elim: factorize.cases)
also from ‹conflict N β S1 S2› have "… = state_trail S1"
by (auto elim: conflict.cases)
finally have "state_trail S3 = state_trail S1"
by assumption
from ‹propagate N β S0 S1› obtain L C γ where
"state_trail S1 = trail_propagate (state_trail S0) L C γ"
by (auto elim: propagate.cases)
from ‹(factorize N β)⇧*⇧* S2 S3› have "state_learned S3 = state_learned S2"
proof (induction S3 rule: rtranclp_induct)
case base
show ?case by simp
next
case (step y z)
thus ?case
by (elim factorize.cases) simp
qed
also from ‹conflict N β S1 S2› have "… = state_learned S1"
by (auto elim: conflict.cases)
finally have "state_learned S3 = state_learned S1"
by assumption
from ‹propagate N β S0 S1› have "state_learned S1 = state_learned S0"
by (auto elim: propagate.cases)
assume "S3 = S"
hence no_conf_with_trail: "no_conflict_with_trail N β (state_learned S0) (state_trail S0)"
using ‹almost_no_conflict_with_trail N β S› ‹{#} |∉| N›
‹state_trail S1 = trail_propagate (state_trail S0) L C γ› ‹state_trail S3 = state_trail S1›
‹state_learned S3 = state_learned S1› ‹state_learned S1 = state_learned S0›
by (simp add: almost_no_conflict_with_trail_def propagate_lit_def is_decision_lit_def)
hence "{#} |∉| state_learned S0"
using nex_conflict_if_no_conflict_with_trail'[folded mempty_in_iff_ex_conflict] by simp
have "∃D γ⇩D. state_conflict S2 = Some (D, γ⇩D) ∧ - (L ⋅l γ) ∈# D ⋅ γ⇩D"
using ‹conflict N β S1 S2›
proof (cases N β S1 S2 rule: conflict.cases)
case (conflictI D U γ⇩D Γ)
hence "trail_false_cls (trail_propagate (state_trail S0) L C γ) (D ⋅ γ⇩D)"
using ‹state_trail S1 = trail_propagate (state_trail S0) L C γ›
by simp
moreover from no_conf_with_trail have "¬ trail_false_cls (state_trail S0) (D ⋅ γ⇩D)"
proof (rule not_trail_false_cls_if_no_conflict_with_trail)
show "D |∈| N |∪| state_learned S0"
using ‹state_learned S1 = state_learned S0› local.conflictI(1) local.conflictI(3)
by fastforce
next
have "{#} |∉| U"
using ‹{#} |∉| state_learned S0› ‹S3 = S› ‹state_learned S3 = state_learned S1›
‹state_learned S1 = state_learned S0›
unfolding conflictI(1,2)
by simp
thus "D ≠ {#}"
using ‹{#} |∉| N› ‹D |∈| N |∪| U›
by auto
next
show "is_ground_cls (D ⋅ γ⇩D)"
by (rule ‹is_ground_cls (D ⋅ γ⇩D)›)
qed
ultimately have "- (L ⋅l γ) ∈# D ⋅ γ⇩D"
by (metis subtrail_falseI propagate_lit_def)
moreover have "state_conflict S2 = Some (D, γ⇩D)"
unfolding conflictI(1,2) by simp
ultimately show ?thesis
by metis
qed
then obtain D γ⇩D where "state_conflict S2 = Some (D, γ⇩D)" and "- (L ⋅l γ) ∈# D ⋅ γ⇩D"
by metis
with ‹(factorize N β)⇧*⇧* S2 S3›
have "∃D' γ⇩D'. state_conflict S3 = Some (D', γ⇩D') ∧ - (L ⋅l γ) ∈# D' ⋅ γ⇩D'"
proof (induction S3 arbitrary: rule: rtranclp_induct)
case base
thus ?case by simp
next
case (step y z)
then obtain D' γ⇩D' where "state_conflict y = Some (D', γ⇩D')" and "- (L ⋅l γ) ∈# D' ⋅ γ⇩D'"
by auto
then show ?case
using step.hyps(2)
by (metis conflict_set_after_factorization)
qed
with backt ‹S3 = S› show False
using ‹state_trail S3 = state_trail S1›
unfolding ‹S3 = S› ‹state_trail S1 = trail_propagate (state_trail S0) L C γ›
by (auto simp add: decide_lit_def propagate_lit_def elim!: backtrack.cases)
qed
with maybe_resolution obtain S4 where
"resolve N β S3 S4" and "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
by metis
show ?thesis
proof (intro exI conjI)
show "(regular_scl N β)⇧*⇧* initial_state S0"
by (rule ‹(regular_scl N β)⇧*⇧* initial_state S0›)
next
show "propagate N β S0 S1"
by (rule ‹propagate N β S0 S1›)
next
show "regular_scl N β S0 S1"
by (rule propa(2))
next
show "conflict N β S1 S2"
by (rule ‹conflict N β S1 S2›)
next
show "(factorize N β)⇧*⇧* S2 S3"
by (rule ‹(factorize N β)⇧*⇧* S2 S3›)
next
show "resolve N β S3 S4"
by (rule ‹resolve N β S3 S4›)
next
show "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
by (rule ‹(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S›)
qed
qed
section ‹Resolve in Regular Runs›
lemma resolve_if_conflict_follows_propagate:
assumes
no_conf: "∄S⇩1. conflict N β S⇩0 S⇩1" and
propa: "propagate N β S⇩0 S⇩1" and
conf: "conflict N β S⇩1 S⇩2"
shows "∃S⇩3. resolve N β S⇩2 S⇩3"
using propa
proof (cases N β S⇩0 S⇩1 rule: propagate.cases)
case (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)
hence S⇩0_def: "S⇩0 = (Γ, U, None)"
by simp
from conf obtain γ⇩D D where
S⇩2_def: "S⇩2 = (trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ, U, Some (D, γ⇩D))" and
D_in: "D |∈| N |∪| U" and
gr_D_γ⇩D: "is_ground_cls (D ⋅ γ⇩D)" and
tr_false_Γ_L_μ: "trail_false_cls (trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ) (D ⋅ γ⇩D)"
by (elim conflict.cases) (unfold propagateI(1,2), blast)
from no_conf have "¬ trail_false_cls Γ (D ⋅ γ⇩D)"
using gr_D_γ⇩D D_in not_trail_false_ground_cls_if_no_conflict[of N β _ D γ⇩D]
using S⇩0_def by force
with tr_false_Γ_L_μ have "- (L ⋅l μ ⋅l γ) ∈# D ⋅ γ⇩D"
unfolding propagate_lit_def by (metis subtrail_falseI)
then obtain D' L' where D_def: "D = add_mset L' D'" and 1: "L ⋅l μ ⋅l γ = - (L' ⋅l γ⇩D)"
by (metis Melem_subst_cls multi_member_split uminus_of_uminus_id)
define ρ where
"ρ = renaming_wrt {add_mset L C⇩0 ⋅ μ}"
have "is_renaming ρ"
by (metis ρ_def finite.emptyI finite.insertI is_renaming_renaming_wrt)
hence "∀x. is_Var (ρ x)" and "inj ρ"
by (simp_all add: is_renaming_iff)
have disjoint_vars: "⋀C. vars_cls (C ⋅ ρ) ∩ vars_cls (add_mset L C⇩0 ⋅ μ) = {}"
by (simp add: ρ_def vars_cls_subst_renaming_disj)
have "∃μ'. Unification.mgu (atm_of L' ⋅a ρ) (atm_of L ⋅a μ) = Some μ'"
proof (rule ex_mgu_if_subst_eq_subst_and_disj_vars)
have "vars_lit L' ⊆ subst_domain γ⇩D"
using gr_D_γ⇩D[unfolded D_def]
by (simp add: vars_lit_subset_subst_domain_if_grounding is_ground_cls_imp_is_ground_lit)
hence "atm_of L' ⋅a ρ ⋅a rename_subst_domain ρ γ⇩D = atm_of L' ⋅a γ⇩D"
by (rule renaming_cancels_rename_subst_domain[OF ‹∀x. is_Var (ρ x)› ‹inj ρ›])
then show "atm_of L' ⋅a ρ ⋅a rename_subst_domain ρ γ⇩D = atm_of L ⋅a μ ⋅a γ"
using 1 by (metis atm_of_subst_lit atm_of_uminus)
next
show "vars_term (atm_of L' ⋅a ρ) ∩ vars_term (atm_of L ⋅a μ) = {}"
using disjoint_vars[of "{#L'#}"] by auto
qed
then obtain μ' where imgu_μ': "is_imgu μ' {{atm_of L' ⋅a ρ, atm_of (L ⋅l μ)}}"
using is_imgu_if_mgu_eq_Some by auto
let ?Γprop = "trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ"
let ?γreso = "λx. if x ∈ vars_cls (add_mset L' D' ⋅ ρ) then rename_subst_domain ρ γ⇩D x else γ x"
have "resolve N β
(?Γprop, U, Some (add_mset L' D', γ⇩D))
(?Γprop, U, Some ((D' ⋅ ρ + C⇩0 ⋅ μ ⋅ Var) ⋅ μ', ?γreso))"
proof (rule resolveI[OF refl])
show "L ⋅l μ ⋅l γ = - (L' ⋅l γ⇩D)"
by (rule 1)
next
show "is_renaming ρ"
by (metis ρ_def finite.emptyI finite.insertI is_renaming_renaming_wrt)
next
show "vars_cls (add_mset L' D' ⋅ ρ) ∩ vars_cls (add_mset (L ⋅l μ) (C⇩0 ⋅ μ) ⋅ Var) = {}"
using disjoint_vars[of "add_mset L' D'"] by simp
next
show "is_imgu μ' {{atm_of L' ⋅a ρ, atm_of (L ⋅l μ) ⋅a Var}}"
using imgu_μ' by simp
next
show "is_grounding_merge ?γreso
(vars_cls (add_mset L' D' ⋅ ρ)) (rename_subst_domain ρ γ⇩D)
(vars_cls (add_mset (L ⋅l μ) (C⇩0 ⋅ μ) ⋅ Var)) (rename_subst_domain Var γ)"
using is_grounding_merge_if_mem_then_else
by (metis rename_subst_domain_Var_lhs)
qed simp_all
thus ?thesis
unfolding S⇩2_def D_def by metis
qed
lemma factorize_preserves_resolvability:
assumes reso: "resolve N β S⇩1 S⇩2" and fact: "factorize N β S⇩1 S⇩3" and
invar: "ground_closures S⇩1"
shows "∃S⇩4. resolve N β S⇩3 S⇩4"
using reso
proof (cases N β S⇩1 S⇩2 rule: resolve.cases)
case (resolveI Γ Γ' K D γ⇩D L γ⇩C ρ⇩C ρ⇩D C μ γ U)
from fact[unfolded resolveI(1,2)] obtain LL' LL CC μ⇩L where
S⇩1_def: "S⇩1 = (Γ, U, Some (add_mset LL' (add_mset LL CC), γ⇩C))" and
S⇩3_def: "S⇩3 = (Γ, U, Some (add_mset LL CC ⋅ μ⇩L, γ⇩C))" and
"LL ⋅l γ⇩C = LL' ⋅l γ⇩C" and
imgu_μ⇩L: "is_imgu μ⇩L {{atm_of LL, atm_of LL'}}"
by (auto simp: ‹S⇩1 = (Γ, U, Some (add_mset L C, γ⇩C))› elim: factorize.cases)
from invar have
ground_conf: "is_ground_cls (add_mset L C ⋅ γ⇩C)"
unfolding resolveI(1,2)
by (simp_all add: ground_closures_def)
have "add_mset L C = add_mset LL' (add_mset LL CC)"
using resolveI(1) S⇩1_def by simp
from imgu_μ⇩L have "μ⇩L ⊙ γ⇩C = γ⇩C"
using ‹LL ⋅l γ⇩C = LL' ⋅l γ⇩C›
by (auto simp: is_imgu_def is_unifiers_def is_unifier_alt intro!: subst_atm_of_eqI)
have "L ⋅l μ⇩L ∈# add_mset LL CC ⋅ μ⇩L"
proof (cases "L = LL ∨ L = LL'")
case True
moreover have "LL ⋅l μ⇩L = LL' ⋅l μ⇩L"
proof -
have "is_unifier μ⇩L {atm_of LL, atm_of LL'}"
using imgu_μ⇩L[unfolded is_imgu_def, THEN conjunct1, unfolded is_unifiers_def, simplified] .
hence "atm_of LL ⋅a μ⇩L = atm_of LL' ⋅a μ⇩L"
unfolding is_unifier_alt[of "{atm_of LL, atm_of LL'}", simplified] ..
hence "atm_of (LL ⋅l μ⇩L) = atm_of (LL' ⋅l μ⇩L)"
unfolding atm_of_subst_lit[symmetric] .
thus ?thesis
using ‹LL ⋅l γ⇩C = LL' ⋅l γ⇩C›
by (metis (no_types, opaque_lifting) literal.expand subst_lit_is_neg)
qed
ultimately have "L ⋅l μ⇩L = LL ⋅l μ⇩L"
by presburger
thus ?thesis
by simp
next
case False
hence "L ∈# CC"
using ‹add_mset L C = add_mset LL' (add_mset LL CC)›
by (metis insert_iff set_mset_add_mset_insert)
thus ?thesis
by auto
qed
then obtain CCC where "add_mset LL CC ⋅ μ⇩L = add_mset L CCC ⋅ μ⇩L"
by (smt (verit, best) Melem_subst_cls mset_add subst_cls_add_mset)
define ρρ where
"ρρ = renaming_wrt {add_mset K D}"
have ren_ρρ: "is_renaming ρρ"
by (metis ρρ_def finite.emptyI finite.insertI is_renaming_renaming_wrt)
have disjoint_vars: "⋀C. vars_cls (C ⋅ ρρ) ∩ vars_cls (add_mset K D) = {}"
by (simp add: ρρ_def vars_cls_subst_renaming_disj)
have "K ⋅l γ⇩D = - (L ⋅l μ⇩L ⋅l γ⇩C)"
proof -
have "L ⋅l μ⇩L ⋅l γ⇩C = L ⋅l γ⇩C"
using ‹μ⇩L ⊙ γ⇩C = γ⇩C›
by (metis subst_lit_comp_subst)
thus ?thesis
using resolveI by simp
qed
have "∃μ. Unification.mgu (atm_of L ⋅a μ⇩L ⋅a ρρ) (atm_of K) = Some μ"
proof (rule ex_mgu_if_subst_eq_subst_and_disj_vars)
show "vars_term (atm_of L ⋅a μ⇩L ⋅a ρρ) ∩ vars_lit K = {}"
using disjoint_vars[of "{#L ⋅l μ⇩L#}"] by auto
next
have "vars_term (atm_of L ⋅a μ⇩L) ⊆ subst_domain γ⇩C"
by (metis ‹μ⇩L ⊙ γ⇩C = γ⇩C› atm_of_subst_lit ground_conf is_ground_cls_add_mset
subst_cls_add_mset subst_lit_comp_subst vars_lit_subset_subst_domain_if_grounding)
hence "atm_of L ⋅a μ⇩L ⋅a ρρ ⋅a rename_subst_domain ρρ γ⇩C = atm_of L ⋅a μ⇩L ⋅a γ⇩C"
using ren_ρρ
by (simp add: is_renaming_iff renaming_cancels_rename_subst_domain)
thus "atm_of L ⋅a μ⇩L ⋅a ρρ ⋅a rename_subst_domain ρρ γ⇩C = atm_of K ⋅a γ⇩D"
using ‹K ⋅l γ⇩D = - (L ⋅l μ⇩L ⋅l γ⇩C)›
by (metis atm_of_subst_lit atm_of_uminus)
qed
then obtain μμ where imgu_μμ: "is_imgu μμ {{atm_of L ⋅a μ⇩L ⋅a ρρ, atm_of K}}"
using is_imgu_if_mgu_eq_Some by auto
show ?thesis
unfolding S⇩3_def ‹add_mset LL CC ⋅ μ⇩L = add_mset L CCC ⋅ μ⇩L›
using resolve.resolveI[OF ‹Γ = trail_propagate Γ' K D γ⇩D› ‹K ⋅l γ⇩D = - (L ⋅l μ⇩L ⋅l γ⇩C)› ren_ρρ
is_renaming_id_subst, unfolded subst_atm_id_subst subst_cls_id_subst atm_of_subst_lit,
OF disjoint_vars imgu_μμ is_grounding_merge_if_mem_then_else, of N β U "CCC ⋅ μ⇩L"]
by auto
qed
text ‹The following lemma corresponds to Lemma 7 in the paper.›
lemma no_backtrack_after_conflict_if:
assumes conf: "conflict N β S1 S2" and trail_S2: "state_trail S1 = trail_propagate Γ L C γ"
shows "∄S4. backtrack N β S2 S4"
proof -
from trail_S2 conf have "state_trail S2 = trail_propagate Γ L C γ"
unfolding conflict.simps by auto
then show ?thesis
unfolding backtrack.simps propagate_lit_def decide_lit_def
by auto
qed
lemma skip_state_trail: "skip N β S S' ⟹ suffix (state_trail S') (state_trail S)"
by (auto simp: suffix_def elim: skip.cases)
lemma factorize_state_trail: "factorize N β S S' ⟹ state_trail S' = state_trail S"
by (auto elim: factorize.cases)
lemma resolve_state_trail: "resolve N β S S' ⟹ state_trail S' = state_trail S"
by (auto elim: resolve.cases)
lemma mempty_not_in_initial_clauses_if_run_leads_to_trail:
assumes
reg_run: "(regular_scl N β)⇧*⇧* initial_state S1" and
trail_lit: "state_trail S1 = Lc # Γ"
shows "{#} |∉| N"
proof (rule notI)
assume "{#} |∈| N"
then obtain γ where "conflict N β initial_state ([], {||}, Some ({#}, γ))"
using conflict_initial_state_if_mempty_in_intial_clauses by auto
moreover hence "∄S'. local.scl N β ([], {||}, Some ({#}, γ)) S'" for γ
using no_more_step_if_conflict_mempty by simp
ultimately show False
using trail_lit
by (metis (no_types, opaque_lifting) conflict_initial_state_only_with_mempty converse_rtranclpE
list.discI prod.sel(1) reasonable_if_regular reg_run regular_scl_def scl_if_reasonable
state_trail_def)
qed
lemma conflict_with_literal_gets_resolved:
assumes
trail_lit: "state_trail S1 = Lc # Γ" and
conf: "conflict N β S1 S2" and
resolution: "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S2 Sn" and
backtrack: "∃Sn'. backtrack N β Sn Sn'" and
mempty_not_in_init_clss: "{#} |∉| N" and
invars: "learned_nonempty S1" "trail_propagated_or_decided' N β S1" "no_conflict_after_decide' N β S1"
shows "¬ is_decision_lit Lc ∧ strict_suffix (state_trail Sn) (state_trail S1)"
proof -
obtain S0 where propa: "propagate N β S0 S1"
using mempty_not_in_init_clss before_reasonable_conflict[OF conf ‹learned_nonempty S1›
‹trail_propagated_or_decided' N β S1› ‹no_conflict_after_decide' N β S1›] by metis
from trail_lit propa have "¬ is_decision_lit Lc"
by (auto simp: propagate_lit_def is_decision_lit_def elim!: propagate.cases)
show ?thesis
proof (rule conjI)
show "¬ is_decision_lit Lc"
by (rule ‹¬ is_decision_lit Lc›)
next
show "strict_suffix (state_trail Sn) (state_trail S1)"
unfolding strict_suffix_def
proof (rule conjI)
from conf have "state_trail S2 = state_trail S1"
by (auto elim: conflict.cases)
moreover from resolution have "suffix (state_trail Sn) (state_trail S2)"
proof (induction Sn rule: rtranclp_induct)
case base
thus ?case
by simp
next
case (step y z)
from step.hyps(2) have "suffix (state_trail z) (state_trail y)"
by (auto simp: suffix_def factorize_state_trail resolve_state_trail
dest: skip_state_trail)
with step.IH show ?case
by (auto simp: suffix_def)
qed
ultimately show "suffix (state_trail Sn) (state_trail S1)"
by simp
next
from backtrack ‹¬ is_decision_lit Lc› show "state_trail Sn ≠ state_trail S1"
unfolding trail_lit
by (auto simp: decide_lit_def is_decision_lit_def elim!: backtrack.cases)
qed
qed
qed
section ‹Clause Redundancy›
definition ground_redundant where
"ground_redundant lt N C ⟷ {D ∈ N. lt D C} ⊫e {C}"
definition redundant where
"redundant lt N C ⟷
(∀C' ∈ grounding_of_cls C. ground_redundant lt (grounding_of_clss N) C')"
lemma "redundant lt N C ⟷ (∀C'∈ grounding_of_cls C. {D' ∈ grounding_of_clss N. lt D' C'} ⊫e {C'})"
by (simp add: redundant_def ground_redundant_def)
lemma ground_redundant_iff:
"ground_redundant lt N C ⟷ (∃M ⊆ N. M ⊫e {C} ∧ (∀D ∈ M. lt D C))"
proof (rule iffI)
assume red: "ground_redundant lt N C"
show "∃M⊆N. M ⊫e {C} ∧ (∀D∈M. lt D C)"
proof (intro exI conjI)
show "{D ∈ N. lt D C} ⊆ N"
by simp
next
show "{D ∈ N. lt D C} ⊫e {C}"
using red by (simp add: ground_redundant_def)
next
show "∀D∈{D ∈ N. lt D C}. lt D C"
by simp
qed
next
assume "∃M⊆N. M ⊫e {C} ∧ (∀D∈M. lt D C)"
then show "ground_redundant lt N C"
unfolding ground_redundant_def
by (smt (verit, ccfv_SIG) mem_Collect_eq subset_iff true_clss_mono)
qed
lemma ground_redundant_is_ground_standard_redundancy:
fixes lt
defines "Red_F⇩𝒢 ≡ λN. {C. ground_redundant lt N C}"
shows "Red_F⇩𝒢 N = {C. ∃M ⊆ N. M ⊫e {C} ∧ (∀D ∈ M. lt D C)}"
by (auto simp: Red_F⇩𝒢_def ground_redundant_iff)
lemma redundant_is_standard_redundancy:
fixes lt 𝒢⇩F 𝒢⇩F⇩s Red_F⇩𝒢 Red_F
defines
"𝒢⇩F ≡ grounding_of_cls" and
"𝒢⇩F⇩s ≡ grounding_of_clss" and
"Red_F⇩𝒢 ≡ λN. {C. ground_redundant lt N C}" and
"Red_F ≡ λN. {C. redundant lt N C}"
shows "Red_F N = {C. ∀D ∈ 𝒢⇩F C. D ∈ Red_F⇩𝒢 (𝒢⇩F⇩s N)}"
using Red_F_def Red_F⇩𝒢_def 𝒢⇩F⇩s_def 𝒢⇩F_def redundant_def by auto
lemma ground_redundant_if_strict_subset:
assumes "D ∈ N" and "D ⊂# C"
shows "ground_redundant (multp⇩H⇩O R) N C"
using assms
unfolding ground_redundant_def
by (metis (mono_tags, lifting) CollectI strict_subset_implies_multp⇩H⇩O subset_mset.less_le
true_clss_def true_clss_singleton true_clss_subclause)
lemma redundant_if_strict_subset:
assumes "D ∈ N" and "D ⊂# C"
shows "redundant (multp⇩H⇩O R) N C"
unfolding redundant_def
proof (rule ballI)
fix C' assume "C' ∈ grounding_of_cls C"
then obtain γ where "C' = C ⋅ γ" and "is_ground_subst γ"
by (auto simp: grounding_of_cls_def)
show "ground_redundant (multp⇩H⇩O R) (grounding_of_clss N) C'"
proof (rule ground_redundant_if_strict_subset)
from ‹D ∈ N› show "D ⋅ γ ∈ grounding_of_clss N"
using ‹is_ground_subst γ›
by (auto simp: grounding_of_clss_def grounding_of_cls_def)
next
from ‹D ⊂# C› show "D ⋅ γ ⊂# C'"
by (simp add: ‹C' = C ⋅ γ› subst_subset_mono)
qed
qed
lemma redundant_if_strict_subsumes:
assumes "D ⋅ σ ⊂# C" and "D ∈ N"
shows "redundant (multp⇩H⇩O R) N C"
unfolding redundant_def
proof (rule ballI)
fix C' assume "C' ∈ grounding_of_cls C"
then obtain γ where "C' = C ⋅ γ" and "is_ground_subst γ"
by (auto simp: grounding_of_cls_def)
show "ground_redundant (multp⇩H⇩O R) (grounding_of_clss N) C'"
proof (rule ground_redundant_if_strict_subset)
from ‹D ∈ N› show "D ⋅ σ ⋅ γ ∈ grounding_of_clss N"
using ‹is_ground_subst γ›
by (metis (no_types, lifting) UN_iff ground_subst_ground_cls grounding_of_cls_ground
grounding_of_clss_def insert_subset subst_cls_comp_subst
subst_cls_eq_grounding_of_cls_subset_eq)
next
from ‹D ⋅ σ ⊂# C› show "D ⋅ σ ⋅ γ ⊂# C'"
by (simp add: ‹C' = C ⋅ γ› subst_subset_mono)
qed
qed
lemma ground_redundant_mono_strong:
"ground_redundant R N C ⟹ (⋀x. x ∈ N ⟹ R x C ⟹ S x C) ⟹ ground_redundant S N C"
unfolding ground_redundant_def
by (simp add: true_clss_def)
lemma redundant_mono_strong:
"redundant R N C ⟹
(⋀x y. x ∈ grounding_of_clss N ⟹ y ∈ grounding_of_cls C ⟹ R x y ⟹ S x y) ⟹
redundant S N C"
by (auto simp: redundant_def
intro: ground_redundant_mono_strong[of R "grounding_of_clss N" _ S])
lemma redundant_multp_if_redundant_strict_subset:
"redundant (⊂#) N C ⟹ redundant (multp⇩H⇩O R) N C"
by (auto intro: strict_subset_implies_multp⇩H⇩O elim!: redundant_mono_strong)
lemma redundant_multp_if_redundant_subset:
"redundant (⊂#) N C ⟹ redundant (multp (trail_less_ex lt Ls)) N C"
by (auto intro: subset_implies_multp elim!: redundant_mono_strong)
lemma not_bex_subset_mset_if_not_ground_redundant:
assumes "is_ground_cls C" and "is_ground_clss N"
shows "¬ ground_redundant (⊂#) N C ⟹ ¬ (∃D ∈ N. D ⊂# C)"
using assms unfolding ground_redundant_def
apply (simp add: true_cls_def true_clss_def)
apply (elim exE conjE)
apply (rule ballI)
subgoal premises prems for I D
using prems(3)[rule_format, of D] prems(1,2,4-)
apply simp
by (meson mset_subset_eqD subset_mset.nless_le)
done
section ‹Trail-Induced Ordering›
subsection ‹Miscellaneous Lemmas›
lemma pairwise_distinct_if_trail_consistent:
fixes Γ
defines "Ls ≡ (map fst Γ)"
shows "trail_consistent Γ ⟹
∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)"
unfolding Ls_def
proof (induction Γ rule: trail_consistent.induct)
case Nil
show ?case by simp
next
case (Cons Γ L u)
from Cons.hyps have L_distinct:
"∀x < length (map fst Γ). map fst Γ ! x ≠ L"
"∀x < length (map fst Γ). map fst Γ ! x ≠ - L"
unfolding trail_defined_lit_def de_Morgan_disj
unfolding image_set in_set_conv_nth not_ex de_Morgan_conj disj_not1
by simp_all
show ?case
unfolding list.map prod.sel
proof (intro allI impI)
fix i j :: nat
assume i_lt: "i < length (L # map fst Γ)" and j_lt: "j < length (L # map fst Γ)" and "i ≠ j"
show
"(L # map fst Γ) ! i ≠ (L # map fst Γ) ! j ∧
(L # map fst Γ) ! i ≠ - (L # map fst Γ) ! j"
proof (cases i)
case 0
thus ?thesis
using L_distinct ‹i ≠ j› ‹j < length (L # map fst Γ)›
using gr0_conv_Suc by auto
next
case (Suc k)
then show ?thesis
apply simp
using i_lt j_lt ‹i ≠ j› L_distinct Cons.IH[rule_format]
using less_Suc_eq_0_disj by force
qed
qed
qed
subsection ‹Strict Partial Order›
lemma irreflp_trail_less_if_trail_consistant:
"trail_consistent Γ ⟹ irreflp (trail_less (map fst Γ))"
using irreflp_trail_less[OF
Clausal_Logic.uminus_not_id'
Clausal_Logic.uminus_of_uminus_id
pairwise_distinct_if_trail_consistent]
by assumption
lemma transp_trail_less_if_trail_consistant:
"trail_consistent Γ ⟹ transp (trail_less (map fst Γ))"
using transp_trail_less[OF
Clausal_Logic.uminus_not_id'
Clausal_Logic.uminus_of_uminus_id
pairwise_distinct_if_trail_consistent]
by assumption
lemma asymp_trail_less_if_trail_consistant:
"trail_consistent Γ ⟹ asymp (trail_less (map fst Γ))"
using asymp_trail_less[OF
Clausal_Logic.uminus_not_id'
Clausal_Logic.uminus_of_uminus_id
pairwise_distinct_if_trail_consistent]
by assumption
subsection ‹Properties›
lemma trail_defined_lit_if_trail_term_less:
assumes "trail_term_less (map (atm_of o fst) Γ) (atm_of L) (atm_of K)"
shows "trail_defined_lit Γ L" "trail_defined_lit Γ K"
proof -
from assms have "atm_of L ∈ set (map (atm_of o fst) Γ)" and "atm_of K ∈ set (map (atm_of o fst) Γ)"
by (auto simp: trail_term_less_def)
hence "atm_of L ∈ atm_of ` fst ` set Γ" and "atm_of K ∈ atm_of ` fst ` set Γ"
by auto
hence "L ∈ fst ` set Γ ∨ - L ∈ fst ` set Γ" and "K ∈ fst ` set Γ ∨ - K ∈ fst ` set Γ"
by (simp_all add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set)
thus "trail_defined_lit Γ L" and "trail_defined_lit Γ K"
by (simp_all add: trail_defined_lit_def)
qed
lemma trail_defined_cls_if_lt_defined:
assumes consistent_Γ: "trail_consistent Γ" and
C_lt_D: "multp⇩H⇩O (lit_less (trail_term_less (map (atm_of o fst) Γ))) C D" and
tr_def_D: "trail_defined_cls Γ D" and
lit_less_preserves_term_order: "⋀R L1 L2. lit_less R L1 L2 ⟹ R⇧=⇧= (atm_of L1) (atm_of L2)"
shows "trail_defined_cls Γ C"
proof -
from multp⇩H⇩O_implies_one_step[OF C_lt_D]
obtain I J K where D_def: "D = I + J" and C_def: "C = I + K" and "J ≠ {#}" and
*: "∀k∈#K. ∃x∈#J. lit_less (trail_term_less (map (atm_of o fst) Γ)) k x"
by auto
show ?thesis
unfolding trail_defined_cls_def
proof (rule ballI)
fix L assume L_in: "L ∈# C"
show "trail_defined_lit Γ L"
proof (cases "L ∈# I")
case True
then show ?thesis
using tr_def_D D_def
by (simp add: trail_defined_cls_def)
next
case False
with C_def L_in have "L ∈# K" by fastforce
then obtain L' where L'_in: "L'∈#J" and "lit_less (trail_term_less (map (atm_of o fst) Γ)) L L'"
using * by blast
hence "(trail_term_less (map (atm_of o fst) Γ))⇧=⇧= (atm_of L) (atm_of L')"
using lit_less_preserves_term_order by metis
thus ?thesis
using trail_defined_lit_if_trail_term_less(1)
by (metis (mono_tags, lifting) D_def L'_in atm_of_eq_atm_of sup2E tr_def_D
trail_defined_cls_def trail_defined_lit_iff_defined_uminus union_iff)
qed
qed
qed
section ‹Dynamic Non-Redundancy›
lemma regular_run_if_skip_factorize_resolve_run:
assumes "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S S'"
shows "(regular_scl N β)⇧*⇧* S S'"
using assms
proof (induction S' rule: rtranclp_induct)
case base
show ?case by simp
next
case (step S' S'')
from step.hyps(2) have "scl N β S' S''"
unfolding scl_def by blast
with step.hyps(2) have "reasonable_scl N β S' S''"
using reasonable_scl_def decide_well_defined(4) decide_well_defined(5) skip_well_defined(2)
by fast
moreover from step.hyps(2) have "¬ Ex (conflict N β S')"
apply simp
by (smt (verit, best) conflict.cases factorize.simps option.distinct(1) resolve.simps skip.simps
state_conflict_simp)
ultimately have "regular_scl N β S' S''"
by (simp add: regular_scl_def)
with step.IH show ?case
by simp
qed
lemma not_trail_true_and_false_lit:
"trail_consistent Γ ⟹ ¬ (trail_true_lit Γ L ∧ trail_false_lit Γ L)"
apply (simp add: trail_true_lit_def trail_false_lit_def)
by (metis (no_types, lifting) in_set_conv_nth list.set_map pairwise_distinct_if_trail_consistent
uminus_not_id')
lemma not_trail_true_and_false_cls:
"trail_consistent Γ ⟹ ¬ (trail_true_cls Γ C ∧ trail_false_cls Γ C)"
using not_trail_true_and_false_lit
by (metis trail_false_cls_def trail_true_cls_def)
fun standard_lit_less where
"standard_lit_less R (Pos t1) (Pos t2) = R t1 t2" |
"standard_lit_less R (Pos t1) (Neg t2) = R⇧=⇧= t1 t2" |
"standard_lit_less R (Neg t1) (Pos t2) = R t1 t2" |
"standard_lit_less R (Neg t1) (Neg t2) = R t1 t2"
lemma standard_lit_less_preserves_term_less:
shows "standard_lit_less R L1 L2 ⟹ R⇧=⇧= (atm_of L1) (atm_of L2)"
by (cases L1; cases L2) simp_all
theorem learned_clauses_in_regular_runs_invars:
fixes Γ lit_less
assumes
sound_S0: "sound_state N β S0" and
invars: "learned_nonempty S0" "trail_propagated_or_decided' N β S0"
"no_conflict_after_decide' N β S0" "almost_no_conflict_with_trail N β S0"
"trail_lits_consistent S0" "trail_closures_false' S0" "ground_false_closures S0" and
conflict: "conflict N β S0 S1" and
resolution: "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧+⇧+ S1 Sn" and
backtrack: "backtrack N β Sn Sn'" and
lit_less_preserves_term_order: "⋀R L1 L2. lit_less R L1 L2 ⟹ R⇧=⇧= (atm_of L1) (atm_of L2)"
defines
"Γ ≡ state_trail S1" and
"U ≡ state_learned S1" and
"trail_ord ≡ multp⇩H⇩O (lit_less (trail_term_less (map (atm_of o fst) Γ)))"
shows "(∃C γ. state_conflict Sn = Some (C, γ) ∧
C ⋅ γ ∉ grounding_of_clss (fset N ∪ fset U) ∧
set_mset (C ⋅ γ) ∉ set_mset ` grounding_of_clss (fset N ∪ fset U) ∧
C ∉ (fset N ∪ fset U) ∧
¬ (∃D ∈ fset N ∪ fset U. ∃σ. D ⋅ σ = C) ∧
¬ redundant trail_ord (fset N ∪ fset U) C)"
proof -
from conflict have "almost_no_conflict_with_trail N β S1"
using ‹almost_no_conflict_with_trail N β S0›
by (rule conflict_preserves_almost_no_conflict_with_trail)
from conflict obtain C1 γ1 where conflict_S1: "state_conflict S1 = Some (C1, γ1)"
by (smt (verit, best) conflict.simps state_conflict_simp)
with backtrack obtain Cn γn where conflict_Sn: "state_conflict Sn = Some (Cn, γn)" and "Cn ≠ {#}"
by (auto elim: backtrack.cases)
with resolution conflict_S1 have "C1 ≠ {#}"
proof (induction Sn arbitrary: C1 γ1 Cn γn rule: tranclp_induct)
case (base y)
then show ?case
by (auto elim: skip.cases factorize.cases resolve.cases)
next
case (step y z)
from step.prems step.hyps obtain Cy γy where
conf_y: "state_conflict y = Some (Cy, γy)" and "Cy ≠ {#}"
by (auto elim: skip.cases factorize.cases resolve.cases)
show ?case
using step.IH[OF _ conf_y ‹Cy ≠ {#}›] step.prems
by simp
qed
from conflict have sound_S1: "sound_state N β S1" and "ground_false_closures S1"
using sound_S0 ‹ground_false_closures S0›
by (simp_all add: conflict_preserves_sound_state conflict_preserves_ground_false_closures)
with resolution have sound_Sn: "sound_state N β Sn" and "ground_false_closures Sn"
by (induction rule: tranclp_induct)
(auto intro:
skip_preserves_sound_state
skip_preserves_ground_false_closures
factorize_preserves_sound_state
factorize_preserves_ground_false_closures
resolve_preserves_sound_state
resolve_preserves_ground_false_closures)
from conflict ‹trail_closures_false' S0› have "trail_closures_false' S1"
by (simp add: conflict_preserves_trail_closures_false')
from conflict_Sn sound_Sn have "fset N ⊫𝒢e {Cn}"
by (auto simp add: sound_state_def)
from conflict_S1 ‹ground_false_closures S1› have trail_S1_false_C1_γ1:
"trail_false_cls (state_trail S1) (C1 ⋅ γ1)"
by (auto simp add: ground_false_closures_def)
from conflict_Sn ‹ground_false_closures Sn› have trail_Sn_false_Cn_γn:
"trail_false_cls (state_trail Sn) (Cn ⋅ γn)"
by (auto simp add: ground_false_closures_def)
from resolution have "suffix (state_trail Sn) (state_trail S1) ∧
(∃Cn γn. state_conflict Sn = Some (Cn, γn) ∧ trail_false_cls (state_trail S1) (Cn ⋅ γn))"
proof (induction Sn rule: tranclp_induct)
case (base S2)
thus ?case
proof (elim sup2E)
assume "skip N β S1 S2"
thus ?thesis
using conflict_S1 skip.simps suffix_ConsI trail_S1_false_C1_γ1 by fastforce
next
assume "factorize N β S1 S2"
moreover with ‹ground_false_closures S1› have "ground_false_closures S2"
by (auto intro: factorize_preserves_ground_false_closures)
ultimately show ?thesis
by (cases N β S1 S2 rule: factorize.cases) (simp add: ground_false_closures_def)
next
assume "resolve N β S1 S2"
moreover with ‹ground_false_closures S1› have "ground_false_closures S2"
by (auto intro: resolve_preserves_ground_false_closures)
ultimately show ?thesis
by (cases N β S1 S2 rule: resolve.cases) (simp add: ground_false_closures_def)
qed
next
case (step Sm Sm')
from step.hyps(2) have "suffix (state_trail Sm') (state_trail Sm)"
by (auto elim!: skip.cases factorize.cases resolve.cases intro: suffix_ConsI)
with step.IH have "suffix (state_trail Sm') (state_trail S1)"
by force
from step.hyps(1) sound_S1 have sound_Sm: "sound_state N β Sm"
by (induction rule: tranclp_induct)
(auto intro: skip_preserves_sound_state factorize_preserves_sound_state
resolve_preserves_sound_state)
from step.hyps(1) ‹trail_closures_false' S1› have "trail_closures_false' Sm"
by (induction rule: tranclp_induct)
(auto intro: skip_preserves_trail_closures_false' factorize_preserves_trail_closures_false'
resolve_preserves_trail_closures_false')
from step.hyps(1) ‹ground_false_closures S1› have "ground_false_closures Sm"
by (induction rule: tranclp_induct)
(auto intro: skip_preserves_ground_false_closures factorize_preserves_ground_false_closures
resolve_preserves_ground_false_closures)
from step.IH obtain Cm γm where
conflict_Sm: "state_conflict Sm = Some (Cm, γm)" and
trail_false_Cm_γm: "trail_false_cls (state_trail S1) (Cm ⋅ γm)"
using step.prems step.hyps(2) ‹suffix (state_trail Sm') (state_trail Sm)›
‹suffix (state_trail Sm') (state_trail S1)›
unfolding suffix_def
by auto
from step.hyps(2) show ?case
proof (elim sup2E)
assume "skip N β Sm Sm'"
thus ?thesis
using ‹suffix (state_trail Sm') (state_trail S1)›
using conflict_Sm skip.simps trail_false_Cm_γm by auto
next
assume "factorize N β Sm Sm'"
thus ?thesis
proof (cases N β Sm Sm' rule: factorize.cases)
case (factorizeI L γ L' μ Γ U D)
with conflict_Sm have Cm_def: "Cm = add_mset L' (add_mset L D)" and γm_def: "γm = γ"
by simp_all
have "trail_false_cls (state_trail S1) ((D + {#L#}) ⋅ μ ⋅ γ)"
proof (rule trail_false_cls_subst_mgu_before_grounding[of _ _ L L'])
show "trail_false_cls (state_trail S1) ((D + {#L, L'#}) ⋅ γ)"
by (metis Cm_def γm_def empty_neutral(1) trail_false_Cm_γm union_commute
union_mset_add_mset_right)
next
show "is_imgu μ {{atm_of L, atm_of L'}}"
using factorizeI(4) by fastforce
next
have "is_unifier γ {atm_of L, atm_of L'}"
unfolding is_unifier_alt[of "{atm_of L, atm_of L'}", simplified]
by (metis atm_of_subst_lit factorizeI(3))
thus "is_unifiers γ {{atm_of L, atm_of L'}}"
by (simp add: is_unifiers_def)
qed
with factorizeI(2) show ?thesis
using ‹suffix (state_trail Sm') (state_trail S1)›
by (metis add_mset_add_single state_conflict_simp)
qed
next
assume "resolve N β Sm Sm'"
thus ?thesis
proof (cases N β Sm Sm' rule: resolve.cases)
case (resolveI Γ Γ' K D γ⇩D L γ⇩C ρ⇩C ρ⇩D C μ γ U)
with conflict_Sm have Cm_def: "Cm = add_mset L C" and γm_def: "γm = γ⇩C"
by simp_all
hence tr_false_S1_conf: "trail_false_cls (state_trail S1) (add_mset L C ⋅ γ⇩C)"
using trail_false_Cm_γm by simp
from sound_Sm have "sound_trail N Γ"
unfolding resolveI(1,2) sound_state_def
by simp
from ‹ground_false_closures Sm› have
ground_conf: "is_ground_cls (add_mset L C ⋅ γ⇩C)" and
ground_prop: "is_ground_cls (add_mset K D ⋅ γ⇩D)"
unfolding resolveI(1,2) ‹Γ = trail_propagate Γ' K D γ⇩D›
by (simp_all add: ground_false_closures_def ground_closures_def propagate_lit_def)
hence
"∀L∈#add_mset L C. L ⋅l ρ⇩C ⋅l γ = L ⋅l γ⇩C"
"∀K∈#add_mset K D. K ⋅l ρ⇩D ⋅l γ = K ⋅l γ⇩D"
using resolveI merge_of_renamed_groundings by metis+
have "atm_of L ⋅a ρ⇩C ⋅a γ = atm_of K ⋅a ρ⇩D ⋅a γ"
using ‹K ⋅l γ⇩D = - (L ⋅l γ⇩C)›
‹∀L∈#add_mset L C. L ⋅l ρ⇩C ⋅l γ = L ⋅l γ⇩C›[rule_format, of L, simplified]
‹∀K∈#add_mset K D. K ⋅l ρ⇩D ⋅l γ = K ⋅l γ⇩D›[rule_format, of K, simplified]
by (metis atm_of_eq_uminus_if_lit_eq atm_of_subst_lit)
hence "is_unifiers γ {{atm_of L ⋅a ρ⇩C, atm_of K ⋅a ρ⇩D}}"
by (simp add: is_unifiers_def is_unifier_alt)
hence "μ ⊙ γ = γ"
using ‹is_imgu μ {{atm_of L ⋅a ρ⇩C, atm_of K ⋅a ρ⇩D}}›
by (auto simp: is_imgu_def)
hence "C ⋅ ρ⇩C ⋅ μ ⋅ γ = C ⋅ γ⇩C" and "D ⋅ ρ⇩D ⋅ μ ⋅ γ = D ⋅ γ⇩D"
using ‹∀L∈#add_mset L C. L ⋅l ρ⇩C ⋅l γ = L ⋅l γ⇩C› ‹∀K∈#add_mset K D. K ⋅l ρ⇩D ⋅l γ = K ⋅l γ⇩D›
by (metis insert_iff same_on_lits_clause set_mset_add_mset_insert subst_cls_comp_subst
subst_lit_comp_subst)+
hence "(C ⋅ ρ⇩C + D ⋅ ρ⇩D) ⋅ μ ⋅ γ = C ⋅ γ⇩C + D ⋅ γ⇩D"
by (metis subst_cls_comp_subst subst_cls_union)
moreover have "trail_false_cls (state_trail S1) (D ⋅ γ⇩D)"
proof (rule trail_false_cls_if_trail_false_suffix)
show "suffix Γ' (state_trail S1)"
using resolveI ‹suffix (state_trail Sm') (state_trail S1)›
by (metis (no_types, opaque_lifting) state_trail_simp suffix_order.trans
suffix_trail_propagate)
next
from ‹trail_closures_false' Sm› have "trail_closures_false Γ"
unfolding resolveI(1,2)
by (simp add: trail_closures_false'_def)
thus "trail_false_cls Γ' (D ⋅ γ⇩D)"
using resolveI(3-)
by (auto simp: propagate_lit_def elim: trail_closures_false.cases)
qed
ultimately have "trail_false_cls (state_trail S1) ((C ⋅ ρ⇩C + D ⋅ ρ⇩D) ⋅ μ ⋅ γ)"
using tr_false_S1_conf
by (metis add_mset_add_single subst_cls_union trail_false_cls_plus)
then show ?thesis
using ‹suffix (state_trail Sm') (state_trail S1)›
using resolveI(1,2) by simp
qed
qed
qed
with conflict_Sn have
"suffix (state_trail Sn) (state_trail S1)" and
tr_false_S1_Cn_γn: "trail_false_cls (state_trail S1) (Cn ⋅ γn)"
by auto
from ‹ground_false_closures Sn› conflict_Sn have Cn_γn_in: "Cn ⋅ γn ∈ grounding_of_cls Cn"
unfolding ground_false_closures_def ground_closures_def
using grounding_of_cls_ground grounding_of_subst_cls_subset
by fastforce
from sound_S1 have sound_trail_S1: "sound_trail N (state_trail S1)"
by (auto simp add: sound_state_def)
have tr_consistent_S1: "trail_consistent (state_trail S1)"
using conflict_preserves_trail_lits_consistent[OF conflict ‹trail_lits_consistent S0›]
by (simp add: trail_lits_consistent_def)
have "∀L∈#Cn ⋅ γn. trail_defined_lit (state_trail S1) L"
using tr_false_S1_Cn_γn trail_defined_lit_iff_true_or_false trail_false_cls_def by blast
hence "trail_interp (state_trail S1) ⊫ Cn ⋅ γn ⟷ trail_true_cls (state_trail S1) (Cn ⋅ γn)"
using tr_consistent_S1 trail_true_cls_iff_trail_interp_entails by auto
hence not_trail_S1_entails_Cn_γn: "¬ trail_interp (state_trail S1) ⊫s {Cn ⋅ γn}"
using tr_false_S1_Cn_γn not_trail_true_and_false_cls[OF tr_consistent_S1] by auto
have "trail_defined_cls (state_trail S1) (Cn ⋅ γn)"
using ‹∀L∈#Cn ⋅ γn. trail_defined_lit (state_trail S1) L› trail_defined_cls_def by blast
have "{#} |∉| N"
by (rule mempty_not_in_initial_clauses_if_non_empty_regular_conflict[OF conflict_S1 ‹C1 ≠ {#}›
‹almost_no_conflict_with_trail N β S1› sound_S1 ‹ground_false_closures S1›])
then obtain S where "propagate N β S S0"
using before_reasonable_conflict[OF conflict ‹learned_nonempty S0›
‹trail_propagated_or_decided' N β S0› ‹no_conflict_after_decide' N β S0›]
by auto
have "state_learned S = state_learned S0"
using ‹propagate N β S S0› by (auto simp add: propagate.simps)
also from conflict have "... = state_learned S1"
by (auto simp add: conflict.simps)
finally have "state_learned S = state_learned S1"
by assumption
have "state_conflict S = None"
using ‹propagate N β S S0› by (auto simp add: propagate.simps)
from conflict have "state_trail S1 = state_trail S0"
by (smt (verit) conflict.cases state_trail_simp)
obtain L C γ where trail_S0_eq: "state_trail S0 = trail_propagate (state_trail S) L C γ"
using ‹propagate N β S S0› unfolding propagate.simps by auto
with backtrack have "strict_suffix (state_trail Sn) (state_trail S0)"
using conflict_with_literal_gets_resolved[OF _ conflict resolution[THEN tranclp_into_rtranclp] _
‹{#} |∉| N› ‹learned_nonempty S0› ‹trail_propagated_or_decided' N β S0›
‹no_conflict_after_decide' N β S0›]
by (metis (no_types, lifting) propagate_lit_def)
hence "suffix (state_trail Sn) (state_trail S)"
unfolding trail_S0_eq propagate_lit_def
by (metis suffix_Cons suffix_order.le_less suffix_order.less_irrefl)
moreover have "¬ trail_defined_lit (state_trail S) (L ⋅l γ)"
proof -
have "trail_consistent (state_trail S0)"
using ‹state_trail S1 = state_trail S0› ‹trail_consistent (state_trail S1)› by simp
thus ?thesis
by (smt (verit, best) Pair_inject list.distinct(1) list.inject trail_S0_eq
trail_consistent.cases propagate_lit_def)
qed
ultimately have "¬ trail_defined_lit (state_trail Sn) (L ⋅l γ)"
using trail_defined_lit_if_trail_defined_suffix by metis
moreover have "trail_false_cls (state_trail Sn) (Cn ⋅ γn)"
using ‹ground_false_closures Sn› conflict_Sn by (auto simp add: ground_false_closures_def)
ultimately have "L ⋅l γ ∉# Cn ⋅ γn ∧ - (L ⋅l γ) ∉# Cn ⋅ γn"
unfolding trail_false_cls_def trail_false_lit_def trail_defined_lit_def
by (metis uminus_of_uminus_id)
have no_conf_at_S: "∄S'. conflict N β S S'"
proof (rule nex_conflict_if_no_conflict_with_trail'')
show "state_conflict S = None"
using ‹propagate N β S S0› by (auto elim: propagate.cases)
next
show "{#} |∉| N"
by (rule ‹{#} |∉| N›)
next
show "learned_nonempty S"
using ‹learned_nonempty S0› ‹state_learned S = state_learned S0›
by (simp add: learned_nonempty_def)
next
show "no_conflict_with_trail N β (state_learned S) (state_trail S)"
using ‹almost_no_conflict_with_trail N β S0›
using ‹propagate N β S S0›
by (auto simp: almost_no_conflict_with_trail_def ‹state_learned S = state_learned S0›
propagate_lit_def is_decision_lit_def elim!: propagate.cases)
qed
have conf_at_S_if: "∃S'. conflict N β S S'"
if D_in: "D ∈ grounding_of_clss (fset N ∪ fset U)" and
tr_false_D: "trail_false_cls (state_trail S) D"
for D
using ex_conflict_if_trail_false_cls[OF tr_false_D D_in]
unfolding U_def ‹state_learned S = state_learned S1›[symmetric]
‹state_conflict S = None›[symmetric]
by simp
have not_gr_red_Cn_γn:
"¬ ground_redundant trail_ord (grounding_of_clss (fset N ∪ fset U)) (Cn ⋅ γn)"
proof (rule notI)
define gnds_le_Cn_γn where
"gnds_le_Cn_γn = {D ∈ grounding_of_clss (fset N ∪ fset U). trail_ord D (Cn ⋅ γn)}"
assume "ground_redundant trail_ord (grounding_of_clss (fset N ∪ fset U)) (Cn ⋅ γn)"
hence "gnds_le_Cn_γn ⊫e {Cn ⋅ γn}"
unfolding ground_redundant_def gnds_le_Cn_γn_def by simp
hence "¬ trail_interp (state_trail S1) ⊫s gnds_le_Cn_γn"
using not_trail_S1_entails_Cn_γn by auto
then obtain D where D_in: "D ∈ gnds_le_Cn_γn" and "¬ trail_interp (state_trail S1) ⊫ D"
by (auto simp: true_clss_def)
from D_in have
D_in: "D ∈ grounding_of_clss (fset N ∪ fset U)" and
D_le_Cn_γn: "trail_ord D (Cn ⋅ γn)"
unfolding gnds_le_Cn_γn_def by simp_all
from D_le_Cn_γn have "trail_defined_cls (state_trail S1) D"
using ‹trail_defined_cls (state_trail S1) (Cn ⋅ γn)›
using trail_defined_cls_if_lt_defined
using Γ_def lit_less_preserves_term_order tr_consistent_S1 trail_ord_def
by metis
hence "trail_false_cls (state_trail S1) D"
using ‹¬ trail_interp (state_trail S1) ⊫ D›
using ‹trail_consistent (state_trail S1)› trail_interp_cls_if_trail_true
trail_true_or_false_cls_if_defined by blast
have "L ⋅l γ ∉# D ∧ - (L ⋅l γ) ∉# D"
proof -
from D_le_Cn_γn have D_lt_Cn_γn':
"multp⇩H⇩O (lit_less (trail_term_less (map (atm_of ∘ fst) (state_trail S1)))) D (Cn ⋅ γn)"
unfolding trail_ord_def Γ_def .
have "∀K∈#Cn ⋅ γn. - K ∈ fst ` set (state_trail S1)"
by (rule ‹trail_false_cls (state_trail S1) (Cn ⋅ γn)›[unfolded trail_false_cls_def
trail_false_lit_def])
hence "∀K∈#Cn ⋅ γn. - K ∈ insert (L ⋅l γ) (fst ` set (state_trail S))"
unfolding ‹state_trail S1 = state_trail S0›
‹state_trail S0 = trail_propagate (state_trail S) L C γ›
propagate_lit_def list.set image_insert prod.sel
by simp
hence *: "∀K∈#Cn ⋅ γn. - K ∈ fst ` set (state_trail S)"
by (metis ‹L ⋅l γ ∉# Cn ⋅ γn ∧ - (L ⋅l γ) ∉# Cn ⋅ γn› insert_iff uminus_lit_swap)
have **: "∀K ∈# Cn ⋅ γn. trail_term_less (map (atm_of o fst) (state_trail S1))
(atm_of K) (atm_of (L ⋅l γ))"
unfolding ‹state_trail S1 = state_trail S0›
‹state_trail S0 = trail_propagate (state_trail S) L C γ›
propagate_lit_def comp_def prod.sel list.map
proof (rule ballI)
fix K assume "K ∈# Cn ⋅ γn"
with * have "- K ∈ fst ` set (state_trail S)"
by metis
hence "atm_of K ∈ set (map (λx. atm_of (fst x)) (state_trail S))"
by (metis (no_types, lifting) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
comp_eq_dest_lhs image_comp image_cong list.set_map)
thus "trail_term_less (atm_of (L ⋅l γ) # map (λx. atm_of (fst x)) (state_trail S))
(atm_of K) (atm_of (L ⋅l γ))"
using trail_term_less_Cons_if_mem by metis
qed
have "¬ (L ⋅l γ ∈# D ∨ - (L ⋅l γ) ∈# D)"
proof (rule notI)
obtain I J K where
"Cn ⋅ γn = I + J" and D_def: "D = I + K" and "J ≠ {#}" and
"∀k∈#K. ∃x∈#J. lit_less (trail_term_less (map (atm_of ∘ fst) (state_trail S1))) k x"
using multp⇩H⇩O_implies_one_step[OF D_lt_Cn_γn']
by auto
assume "L ⋅l γ ∈# D ∨ - (L ⋅l γ) ∈# D"
then show False
unfolding D_def Multiset.union_iff
proof (elim disjE)
show "L ⋅l γ ∈# I ⟹ False"
using ‹L ⋅l γ ∉# Cn ⋅ γn ∧ - (L ⋅l γ) ∉# Cn ⋅ γn› ‹Cn ⋅ γn = I + J› by simp
next
show "- (L ⋅l γ) ∈# I ⟹ False"
using ‹L ⋅l γ ∉# Cn ⋅ γn ∧ - (L ⋅l γ) ∉# Cn ⋅ γn› ‹Cn ⋅ γn = I + J› by simp
next
show "L ⋅l γ ∈# K ⟹ False"
using ‹L ⋅l γ ∉# Cn ⋅ γn ∧ - (L ⋅l γ) ∉# Cn ⋅ γn›[THEN conjunct1]
**[unfolded ‹Cn ⋅ γn = I + J›] ‹∀k∈#K. ∃x∈#J. lit_less (trail_term_less (map (atm_of ∘ fst) (state_trail S1))) k x›
by (metis (no_types, lifting) D_def Un_insert_right
‹¬ trail_interp (state_trail S1) ⊫ D›
‹state_trail S0 = trail_propagate (state_trail S) L C γ›
‹state_trail S1 = state_trail S0› ‹trail_consistent (state_trail S1)› image_insert
insert_iff list.set(2) mk_disjoint_insert prod.sel(1) set_mset_union
trail_interp_cls_if_trail_true propagate_lit_def trail_true_cls_def
trail_true_lit_def)
next
assume "- (L ⋅l γ) ∈# K"
then obtain j where
j_in: "j ∈# J" and
uminus_L_γ_lt_j: "lit_less (trail_term_less (map (atm_of ∘ fst) (state_trail S1))) (- (L ⋅l γ)) j"
using ‹∀k∈#K. ∃x∈#J. lit_less (trail_term_less (map (atm_of ∘ fst) (state_trail S1))) k x›
by blast
from j_in have
"trail_term_less (map (atm_of ∘ fst) (state_trail S1)) (atm_of j) (atm_of (L ⋅l γ))"
using **
by (auto simp: ‹Cn ⋅ γn = I + J›)
moreover from uminus_L_γ_lt_j have "trail_term_less (map (atm_of ∘ fst) (state_trail S1)) (atm_of (L ⋅l γ)) (atm_of j)"
using calculation lit_less_preserves_term_order by fastforce
moreover from tr_consistent_S1 have "distinct (map (atm_of ∘ fst) (state_trail S1))"
using distinct_atm_of_trail_if_trail_consistent by metis
ultimately show "False"
using asymp_trail_term_less[THEN asympD]
by metis
qed
qed
thus ?thesis by simp
qed
hence "trail_false_cls (state_trail S) D"
using D_in ‹trail_false_cls (state_trail S1) D›
unfolding ‹state_trail S1 = state_trail S0›
‹state_trail S0 = trail_propagate (state_trail S) L C γ›
by (simp add: propagate_lit_def subtrail_falseI)
thus False
using no_conf_at_S conf_at_S_if[OF D_in] by metis
qed
hence "¬ redundant trail_ord (fset N ∪ fset U) Cn"
unfolding redundant_def
using Cn_γn_in by auto
moreover have "Cn ⋅ γn ∉ grounding_of_clss (fset N ∪ fset U)"
proof -
have "is_ground_cls (Cn ⋅ γn)"
using Cn_γn_in is_ground_cls_if_in_grounding_of_cls by blast
moreover have "is_ground_clss (grounding_of_clss (fset N ∪ fset U))"
by simp
ultimately have "¬ ({D ∈ grounding_of_clss (fset N ∪ fset U). trail_ord D (Cn ⋅ γn)} ⊫e {Cn ⋅ γn})"
using not_gr_red_Cn_γn
by (simp add: ground_redundant_def)
thus ?thesis
using ‹suffix (state_trail Sn) (state_trail S)› conf_at_S_if no_conf_at_S
trail_Sn_false_Cn_γn trail_false_cls_if_trail_false_suffix by blast
qed
moreover have "set_mset (Cn ⋅ γn) ∉ set_mset ` grounding_of_clss (fset N ∪ fset U)"
proof (rule notI)
assume "set_mset (Cn ⋅ γn) ∈ set_mset ` grounding_of_clss (fset N ∪ fset U)"
then obtain D where
D_in: "D ∈ grounding_of_clss (fset N ∪ fset U)" and
set_mset_eq_D_Cn_γn: "set_mset D = set_mset (Cn ⋅ γn)"
by (auto simp add: image_iff)
have "¬ trail_interp (state_trail S1) ⊫ D"
unfolding true_cls_iff_set_mset_eq[OF set_mset_eq_D_Cn_γn]
using not_trail_S1_entails_Cn_γn
by simp
have "trail_defined_cls (state_trail S1) D"
using ‹∀L∈#Cn ⋅ γn. trail_defined_lit (state_trail S1) L›
unfolding set_mset_eq_D_Cn_γn[symmetric]
by (simp add: trail_defined_cls_def)
hence "trail_false_cls (state_trail S1) D"
using ‹¬ trail_interp (state_trail S1) ⊫ D›
using tr_consistent_S1 trail_interp_cls_if_trail_true trail_true_or_false_cls_if_defined
by blast
have "L ⋅l γ ∉# D ∧ - (L ⋅l γ) ∉# D"
using ‹L ⋅l γ ∉# Cn ⋅ γn ∧ - (L ⋅l γ) ∉# Cn ⋅ γn›
unfolding set_mset_eq_D_Cn_γn[symmetric]
by assumption
hence "trail_false_cls (state_trail S) D"
using D_in ‹trail_false_cls (state_trail S1) D›
unfolding ‹state_trail S1 = state_trail S0›
‹state_trail S0 = trail_propagate (state_trail S) L C γ›
by (simp add: propagate_lit_def subtrail_falseI)
thus False
using no_conf_at_S conf_at_S_if[OF D_in] by metis
qed
moreover have "¬(∃D ∈ fset N ∪ fset U. ∃σ. D ⋅ σ = Cn)"
by (metis (no_types, lifting) Cn_γn_in Set.set_insert UnCI calculation(2)
grounding_of_clss_insert grounding_of_subst_cls_subset subsetD)
moreover hence "Cn ∉ fset N ∪ fset U"
using subst_cls_id_subst by blast
ultimately show ?thesis
using conflict_Sn by simp
qed
theorem dynamic_non_redundancy_regular_scl:
fixes Γ
assumes
regular_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
conflict: "conflict N β S0 S1" and
resolution: "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧+⇧+ S1 Sn" and
backtrack: "backtrack N β Sn Sn'" and
lit_less_preserves_term_order: "⋀R L1 L2. lit_less R L1 L2 ⟹ R⇧=⇧= (atm_of L1) (atm_of L2)"
defines
"Γ ≡ state_trail S1" and
"U ≡ state_learned S1" and
"trail_ord ≡ multp⇩H⇩O (lit_less (trail_term_less (map (atm_of o fst) Γ)))"
shows "(regular_scl N β)⇧*⇧* initial_state Sn' ∧
(∃C γ. state_conflict Sn = Some (C, γ) ∧
C ⋅ γ ∉ grounding_of_clss (fset N ∪ fset U) ∧
set_mset (C ⋅ γ) ∉ set_mset ` grounding_of_clss (fset N ∪ fset U) ∧
C ∉ fset N ∪ fset U ∧
¬ (∃D ∈ fset N ∪ fset U. ∃σ. D ⋅ σ = C) ∧
¬ redundant trail_ord (fset N ∪ fset U) C)"
proof -
have "sound_state N β initial_state"
by (rule sound_initial_state)
with regular_run have sound_S0: "sound_state N β S0"
by (rule regular_run_sound_state)
from regular_run have "learned_nonempty S0"
by (induction S0 rule: rtranclp_induct)
(auto intro: scl_preserves_learned_nonempty reasonable_if_regular scl_if_reasonable)
from regular_run have "trail_propagated_or_decided' N β S0"
by (induction S0 rule: rtranclp_induct)
(auto intro: scl_preserves_trail_propagated_or_decided
reasonable_if_regular scl_if_reasonable)
from regular_run have "no_conflict_after_decide' N β S0"
by (induction S0 rule: rtranclp_induct)
(auto intro: reasonable_scl_preserves_no_conflict_after_decide' reasonable_if_regular)
from regular_run have "almost_no_conflict_with_trail N β S0"
by (induction S0 rule: rtranclp_induct)
(simp_all add: regular_scl_preserves_almost_no_conflict_with_trail)
from regular_run have "trail_lits_consistent S0"
by (induction S0 rule: rtranclp_induct)
(auto intro: scl_preserves_trail_lits_consistent reasonable_if_regular scl_if_reasonable)
from regular_run have "trail_lits_consistent S0"
by (induction S0 rule: rtranclp_induct)
(auto intro: scl_preserves_trail_lits_consistent reasonable_if_regular scl_if_reasonable)
from regular_run have "trail_closures_false' S0"
by (induction S0 rule: rtranclp_induct)
(auto intro: scl_preserves_trail_closures_false' reasonable_if_regular scl_if_reasonable)
from regular_run have "ground_false_closures S0"
by (induction S0 rule: rtranclp_induct)
(auto intro: scl_preserves_ground_false_closures reasonable_if_regular scl_if_reasonable)
from regular_run conflict have "(regular_scl N β)⇧*⇧* initial_state S1"
by (meson regular_scl_def rtranclp.simps)
also from resolution have reg_run_S1_Sn: "(regular_scl N β)⇧*⇧* ... Sn"
using regular_run_if_skip_factorize_resolve_run tranclp_into_rtranclp by metis
also have "(regular_scl N β)⇧*⇧* ... Sn'"
proof (rule r_into_rtranclp)
from backtrack have "scl N β Sn Sn'"
by (simp add: scl_def)
with backtrack have "reasonable_scl N β Sn Sn'"
using reasonable_scl_def decide_well_defined(6) by blast
with backtrack show "regular_scl N β Sn Sn'"
unfolding regular_scl_def
by (smt (verit) conflict.simps option.simps(3) backtrack.cases state_conflict_simp)
qed
finally have "(regular_scl N β)⇧*⇧* initial_state Sn'" by assumption
thus ?thesis
using learned_clauses_in_regular_runs_invars[OF sound_S0 ‹learned_nonempty S0›
‹trail_propagated_or_decided' N β S0›
‹no_conflict_after_decide' N β S0› ‹almost_no_conflict_with_trail N β S0›
‹trail_lits_consistent S0› ‹trail_closures_false' S0› ‹ground_false_closures S0›
conflict resolution backtrack]
using lit_less_preserves_term_order
using U_def Γ_def trail_ord_def by presburger
qed
theorem dynamic_non_redundancy_projectable_strategy:
fixes
S1 :: "('f, 'v) state" and
lit_less :: "(('f, 'v) term ⇒ ('f, 'v) term ⇒ bool) ⇒
('f, 'v) term literal ⇒ ('f, 'v) term literal ⇒ bool" and
strategy and strategy_init and proj
defines
"Γ ≡ state_trail S1" and
"U ≡ state_learned S1"
defines
"trail_ord ≡ multp⇩H⇩O (lit_less (trail_term_less (map (atm_of o fst) Γ)))"
assumes
run: "strategy⇧*⇧* strategy_init S0" and
conflict: "conflict N β (proj S0) S1" and
resolution: "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧+⇧+ S1 Sn" and
backtrack: "backtrack N β Sn Sn'" and
strategy_restricts_regular_scl:
"⋀S S'. strategy⇧*⇧* strategy_init S ⟹ strategy S S' ⟹ regular_scl N β (proj S) (proj S')" and
initial_state: "proj strategy_init = initial_state" and
lit_less_preserves_term_order: "⋀R L1 L2. lit_less R L1 L2 ⟹ R⇧=⇧= (atm_of L1) (atm_of L2)"
shows "(∃C γ. state_conflict Sn = Some (C, γ) ∧
C ⋅ γ ∉ grounding_of_clss (fset N ∪ fset U) ∧
set_mset (C ⋅ γ) ∉ set_mset ` grounding_of_clss (fset N ∪ fset U) ∧
C ∉ fset N ∪ fset U ∧
¬ (∃D ∈ fset N ∪ fset U. ∃σ. D ⋅ σ = C) ∧
¬ redundant trail_ord (fset N ∪ fset U) C)"
proof -
from backtrack have backtrack': "backtrack N β Sn Sn'"
by (simp add: shortest_backtrack_strategy_def)
have "(∃C γ. state_conflict Sn = Some (C, γ) ∧
C ⋅ γ ∉ grounding_of_clss (fset N ∪ fset U) ∧
set_mset (C ⋅ γ) ∉ set_mset ` grounding_of_clss (fset N ∪ fset U) ∧
C ∉ fset N ∪ fset U ∧
¬ (∃D ∈ fset N ∪ fset U. ∃σ. D ⋅ σ = C) ∧
¬ redundant (multp⇩H⇩O (lit_less
(trail_term_less (map (atm_of ∘ fst) (state_trail S1)))))
(fset N ∪ fset U) C)"
unfolding U_def
proof (rule dynamic_non_redundancy_regular_scl[THEN conjunct2])
show "(regular_scl N β)⇧*⇧* initial_state (proj S0)"
using run
proof (induction S0 rule: rtranclp_induct)
case base
thus ?case
unfolding initial_state by simp
next
case (step y z)
thus ?case
using strategy_restricts_regular_scl
by (meson rtranclp.simps)
qed
next
from assms show "conflict N β (proj S0) S1"
by simp
next
from assms show "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧+⇧+ S1 Sn"
by simp
next
from assms show "backtrack N β Sn Sn'"
by (simp add: shortest_backtrack_strategy_def)
next
from assms show "⋀R L1 L2. lit_less R L1 L2 ⟹ R⇧=⇧= (atm_of L1) (atm_of L2)"
by simp
qed
thus ?thesis
by (auto simp add: trail_ord_def Γ_def)
qed
corollary dynamic_non_redundancy_strategy:
fixes Γ
assumes
run: "strategy⇧*⇧* initial_state S0" and
conflict: "conflict N β S0 S1" and
resolution: "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧+⇧+ S1 Sn" and
backtrack: "backtrack N β Sn Sn'" and
strategy_imp_regular_scl: "⋀S S'. strategy S S' ⟹ regular_scl N β S S'" and
lit_less_preserves_term_order: "⋀R L1 L2. lit_less R L1 L2 ⟹ R⇧=⇧= (atm_of L1) (atm_of L2)"
defines
"Γ ≡ state_trail S1" and
"U ≡ state_learned S1" and
"trail_ord ≡ multp⇩H⇩O (lit_less (trail_term_less (map (atm_of o fst) Γ)))"
shows "(∃C γ. state_conflict Sn = Some (C, γ) ∧
C ⋅ γ ∉ grounding_of_clss (fset N ∪ fset U) ∧
set_mset (C ⋅ γ) ∉ set_mset ` grounding_of_clss (fset N ∪ fset U) ∧
C ∉ fset N ∪ fset U ∧
¬ (∃D ∈ fset N ∪ fset U. ∃σ. D ⋅ σ = C) ∧
¬ redundant trail_ord (fset N ∪ fset U) C)"
using dynamic_non_redundancy_projectable_strategy[of strategy initial_state _ _ _ "λx. x"]
using assms by blast
section ‹Static Non-Redundancy›
lemma before_regular_backtrack':
assumes
run: "(regular_scl N β)⇧*⇧* initial_state S" and
step: "backtrack N β S S'"
shows "∃S0 S1 S2 S3 S4. (regular_scl N β)⇧*⇧* initial_state S0 ∧
propagate N β S0 S1 ∧ regular_scl N β S0 S1 ∧
conflict N β S1 S2 ∧ (factorize N β)⇧*⇧* S2 S3 ∧ resolve N β S3 S4 ∧
(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
proof -
from run have "sound_state N β S"
by (induction S rule: rtranclp_induct)
(simp_all add: scl_preserves_sound_state[OF scl_if_regular])
moreover from run have "almost_no_conflict_with_trail N β S"
by (induction S rule: rtranclp_induct)
(simp_all add: regular_scl_preserves_almost_no_conflict_with_trail)
moreover from run have "regular_conflict_resolution N β S"
by (induction S rule: rtranclp_induct)
(simp_all add: regular_scl_preserves_regular_conflict_resolution)
moreover from run have "ground_false_closures S"
by (induction S rule: rtranclp_induct)
(simp_all add: scl_preserves_ground_false_closures[OF scl_if_regular])
ultimately obtain S0 S1 S2 S3 S4 where
run_S0: "(regular_scl N β)⇧*⇧* initial_state S0" and
propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
confl: "conflict N β S1 S2" and
facto: "(factorize N β)⇧*⇧* S2 S3" and
resol: "resolve N β S3 S4" and
reg_res: "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
using before_regular_backtrack[OF step] by blast
thus ?thesis
by metis
qed
theorem static_non_subsumption_regular_scl:
assumes
run: "(regular_scl N β)⇧*⇧* initial_state S" and
step: "backtrack N β S S'"
defines
"U ≡ state_learned S"
shows "∃C γ. state_conflict S = Some (C, γ) ∧ ¬ (∃D |∈| N |∪| U. subsumes D C)"
proof -
from before_regular_backtrack'[OF run step] obtain S0 S1 S2 S3 S4 where
run_S0: "(regular_scl N β)⇧*⇧* initial_state S0" and
propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
confl: "conflict N β S1 S2" and
facto: "(factorize N β)⇧*⇧* S2 S3" and
resol: "resolve N β S3 S4" and
reg_res: "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
using before_regular_backtrack[OF step] by blast
have "(regular_scl N β)⇧*⇧* initial_state S1"
using run_S0 propa(2) by simp
moreover have reg_res': "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧+⇧+ S2 S"
proof -
have "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S2 S3"
using facto
by (rule mono_rtranclp[rule_format, rotated]) simp
also have "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧+⇧+ S3 S4"
using resol by auto
finally show ?thesis
using reg_res by simp
qed
ultimately obtain C γ lt where
reg_run: "(regular_scl N β)⇧*⇧* initial_state S'" and
conf: "state_conflict S = Some (C, γ)" and
not_gen: "¬ (∃D ∈ fset N ∪ fset (state_learned S2). ∃σ. D ⋅ σ = C)" and
not_red: "¬ redundant (multp⇩H⇩O (standard_lit_less
(trail_term_less (map (atm_of ∘ fst) (state_trail S2)))))
(fset N ∪ fset (state_learned S2)) C"
using dynamic_non_redundancy_regular_scl[OF _ confl _ step, of standard_lit_less]
using standard_lit_less_preserves_term_less
by metis+
from not_red have "¬ (∃D∈fset N ∪ fset (state_learned S2). ∃σ. D ⋅ σ ⊂# C)"
using redundant_if_strict_subsumes
by (metis union_fset)
with not_gen have "¬ (∃D∈fset N ∪ fset (state_learned S2). ∃σ. D ⋅ σ ⊆# C)"
using subset_mset.order_iff_strict by blast
hence not_sub: "¬ (∃D∈fset N ∪ fset (state_learned S2). subsumes D C)"
by (simp add: subsumes_def)
from reg_res' have learned_S2: "state_learned S2 = state_learned S"
proof (induction S)
case (base y)
thus ?case
by (auto elim: skip.cases factorize.cases resolve.cases)
next
case (step y z)
from step.hyps have "state_learned y = state_learned z"
by (auto elim: skip.cases factorize.cases resolve.cases)
with step.IH show ?case
by simp
qed
show ?thesis
unfolding U_def
using conf not_sub[unfolded learned_S2]
by simp
qed
corollary static_non_subsumption_projectable_strategy:
fixes strategy and strategy_init and proj
assumes
run: "strategy⇧*⇧* strategy_init S" and
step: "backtrack N β (proj S) S'" and
strategy_restricts_regular_scl:
"⋀S S'. strategy⇧*⇧* strategy_init S ⟹ strategy S S' ⟹ regular_scl N β (proj S) (proj S')" and
initial_state: "proj strategy_init = initial_state"
defines
"U ≡ state_learned (proj S)"
shows "∃C γ. state_conflict (proj S) = Some (C, γ) ∧ ¬ (∃D |∈| N |∪| U. subsumes D C)"
unfolding U_def
proof (rule static_non_subsumption_regular_scl)
show "(regular_scl N β)⇧*⇧* initial_state (proj S)"
using run
proof (induction S rule: rtranclp_induct)
case base
thus ?case
unfolding initial_state by simp
next
case (step y z)
thus ?case
using strategy_restricts_regular_scl
by (meson rtranclp.simps)
qed
next
from step show "backtrack N β (proj S) S'"
by simp
qed
corollary static_non_subsumption_strategy:
assumes
run: "strategy⇧*⇧* initial_state S" and
step: "backtrack N β S S'" and
strategy_imp_regular_scl: "⋀S S'. strategy S S' ⟹ regular_scl N β S S'"
defines
"U ≡ state_learned S"
shows "∃C γ. state_conflict S = Some (C, γ) ∧ ¬ (∃D |∈| N |∪| U. subsumes D C)"
unfolding U_def
using static_non_subsumption_projectable_strategy[of strategy initial_state _ _ _ "λx. x"]
using assms by blast
end
end