# Theory Completeness

```theory Completeness
imports
Correct_Termination
Termination
"Functional_Ordered_Resolution_Prover.IsaFoR_Term"
begin

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]

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]

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 ({#}, γ))"
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
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```