Theory Completeness

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 bex_rtransclp_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
          alethe_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