theory Completeness imports Correct_Termination Termination "Functional_Ordered_Resolution_Prover.IsaFoR_Term" begin lemma (in scl_fol_calculus) regular_scl_run_derives_contradiction_if_unsat: fixes N β gnd_N defines "gnd_N ≡ grounding_of_clss (fset N)" and "gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼⇩_{B}β}" assumes unsat: "¬ satisfiable gnd_N_lt_β" and run: "(regular_scl N β)⇧^{*}⇧^{*}initial_state S" and no_more_step: "∄S'. regular_scl N β S S'" shows "∃γ. state_conflict S = Some ({#}, γ)" using unsat correct_termination_regular_scl_run[OF run no_more_step] by (simp add: gnd_N_lt_β_def gnd_N_def) theorem (in scl_fol_calculus) fixes N β gnd_N defines "gnd_N ≡ grounding_of_clss (fset N)" and "gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼⇩_{B}β}" assumes unsat: "¬ satisfiable gnd_N_lt_β" shows "∃S. (regular_scl N β)⇧^{*}⇧^{*}initial_state S ∧ (∄S'. regular_scl N β S S') ∧ (∃γ. state_conflict S = Some ({#}, γ))" proof - obtain S where run: "(regular_scl N β)⇧^{*}⇧^{*}initial_state S" and no_more_step: "(∄S'. regular_scl N β S S')" using termination_regular_scl[THEN ex_trans_min_element_if_wfp_on, of initial_state] by (metis (no_types, opaque_lifting) conversep_iff mem_Collect_eq rtranclp.rtrancl_into_rtrancl rtranclp.rtrancl_refl) moreover have "∃γ. state_conflict S = Some ({#}, γ)" using unsat correct_termination_regular_scl_run[OF run no_more_step] by (simp add: gnd_N_lt_β_def gnd_N_def) ultimately show ?thesis by metis qed lemma (in scl_fol_calculus) no_infinite_down_chain: "∄Ss. ¬ lfinite Ss ∧ Lazy_List_Chain.chain (λS S'. regular_scl N β S S') (LCons initial_state Ss)" using termination_regular_scl wfp_on_rtranclp_conversep_iff_no_infinite_down_chain_llist by metis theorem (in scl_fol_calculus) completeness_wrt_bound: fixes N β gnd_N defines "gnd_N ≡ grounding_of_clss (fset N)" and "gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼⇩_{B}β}" assumes unsat: "¬ satisfiable gnd_N_lt_β" shows "∄Ss. ¬ lfinite Ss ∧ Lazy_List_Chain.chain (λS S'. regular_scl N β S S') (LCons initial_state Ss)" and "∀S. (regular_scl N β)⇧^{*}⇧^{*}initial_state S ⟶ (∄S'. regular_scl N β S S') ⟶ (∃γ. state_conflict S = Some ({#}, γ))" using assms regular_scl_run_derives_contradiction_if_unsat no_infinite_down_chain by simp_all locale compact_scl = scl_fol_calculus renaming_vars "(<) :: ('f :: weighted, 'v) term ⇒ ('f, 'v) term ⇒ bool" for renaming_vars :: "'v set ⇒ 'v ⇒ 'v" begin theorem ex_bound_if_unsat: fixes N :: "('f, 'v) term clause fset" defines "gnd_N ≡ grounding_of_clss (fset N)" assumes unsat: "¬ satisfiable gnd_N" shows "∃β. ¬ satisfiable {C ∈ gnd_N. ∀L ∈# C. atm_of L ≤ β}" proof - from unsat obtain gnd_N' where "gnd_N' ⊆ gnd_N" and "finite gnd_N'" and unsat': "¬ satisfiable gnd_N'" using clausal_logic_compact[of gnd_N] by metis have "gnd_N' ≠ {}" using ‹¬ satisfiable gnd_N'› by force obtain C where C_in: "C ∈ gnd_N'" and C_min: "∀x∈gnd_N'. x ≤ C" using finite_has_maximal[OF ‹finite gnd_N'› ‹gnd_N' ≠ {}›] by force show ?thesis proof (cases C) case empty let ?S = "([], {||}, Some ({#}, Var))" show ?thesis proof (rule exI) have "{#} |∈| N" using C_in ‹gnd_N' ⊆ gnd_N› unfolding empty gnd_N_def by (smt (verit, del_insts) SCL_FOL.grounding_of_clss_def SCL_FOL.subst_cls_empty_iff UN_E mem_Collect_eq subset_iff substitution_ops.grounding_of_cls_def) hence "{#} ∈ gnd_N" using C_in ‹gnd_N' ⊆ gnd_N› local.empty by blast hence "{#} ∈ {C ∈ gnd_N. ∀L∈#C. atm_of L < undefined}" by force thus "¬ satisfiable {C ∈ gnd_N. ∀L∈#C. atm_of L ≤ undefined}" using unsat' by (smt (verit, best) C_min le_multiset_empty_right local.empty mem_Collect_eq nless_le subset_entailed subset_iff) qed next case (add x C') then obtain L where "L ∈# C" and L_min: "∀x∈#C. x ≤ L" using Multiset.bex_greatest_element[of C] by (metis empty_not_add_mset finite_set_mset infinite_growing linorder_le_less_linear set_mset_eq_empty_iff) from L_min C_min have "∀D∈gnd_N'. ∀K∈#D. atm_of K ≤ atm_of L" by (meson dual_order.trans ex_gt_imp_less_multiset leq_imp_less_eq_atm_of verit_comp_simplify1(3)) hence "gnd_N' ⊆ {D ∈ gnd_N. ∀K ∈# D. (atm_of K) ≤ (atm_of L)}" using ‹gnd_N' ⊆ gnd_N› subset_Collect_iff by auto hence "¬ satisfiable {D ∈ gnd_N. ∀K ∈# D. (atm_of K) ≤ (atm_of L)}" using ‹¬ satisfiable gnd_N'› by (meson satisfiable_antimono) thus ?thesis by auto qed qed end end