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}" using imgu_μ⇩_{L}[unfolded is_imgu_def, THEN conjunct1, unfolded is_unifiers_def, simplified] using ‹LL ⋅l γ⇩_{C}= LL' ⋅l γ⇩_{C}› by (metis (no_types, opaque_lifting) atm_of_subst_lit finite.emptyI finite.insertI insertCI is_unifier_alt literal.expand subst_lit_is_neg) 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 (* after conflict, one can apply factorize arbitrarily often, but resolve must be applied at least once. Prove this lemma! conflict in reg run ⟹ ALL following runs have the following shape: factorize* then resolve then (skip or factorize or resolve)* *) 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