Theory DISCOUNT_Loop

(* Title:        DISCOUNT Loop
   Authors:      Qi Qiu, 2021
                 Jasmin Blanchette <j.c.blanchette at vu.nl>, 2022-2023
   Maintainer:   Jasmin Blanchette <j.c.blanchette at vu.nl>
*)

section ‹DISCOUNT Loop›

text ‹The DISCOUNT loop is one of the two best-known given clause procedures. It
is formalized as an instance of the abstract procedure @{text LGC}.›

theory DISCOUNT_Loop
  imports
    Given_Clause_Loops_Util
    More_Given_Clause_Architectures
begin


subsection ‹Locale›

datatype DL_label =
  Passive | YY | Active

primrec nat_of_DL_label :: "DL_label ⇒ nat" where
  "nat_of_DL_label Passive = 2"
| "nat_of_DL_label YY = 1"
| "nat_of_DL_label Active = 0"

definition DL_Prec_L :: "DL_label ⇒ DL_label ⇒ bool" (infix "⊏L" 50) where
  "DL_Prec_L l l' ⟷ nat_of_DL_label l < nat_of_DL_label l'"

locale discount_loop = labeled_lifting_intersection Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q
  Red_F_q 𝒢_F_q 𝒢_I_q
  "{ι⇩F⇩L :: ('f × 'l) inference. Infer (map fst (prems_of ι⇩F⇩L)) (fst (concl_of ι⇩F⇩L)) ∈ Inf_F}"
  for
    Bot_F :: "'f set"
    and Inf_F :: "'f inference set"
    and Bot_G :: "'g set"
    and Q :: "'q set"
    and entails_q :: "'q ⇒ 'g set ⇒ 'g set ⇒ bool"
    and Inf_G_q :: ‹'q ⇒ 'g inference set›
    and Red_I_q :: "'q ⇒ 'g set ⇒ 'g inference set"
    and Red_F_q :: "'q ⇒ 'g set ⇒ 'g set"
    and 𝒢_F_q :: "'q ⇒ 'f ⇒ 'g set"
    and 𝒢_I_q :: "'q ⇒ 'f inference ⇒ 'g inference set option"
  + fixes
    Equiv_F :: "'f ⇒ 'f ⇒ bool" (infix "≐" 50) and
    Prec_F :: "'f ⇒ 'f ⇒ bool" (infix "≺⋅" 50)
  assumes
    equiv_equiv_F: "equivp (≐)" and
    wf_prec_F: "minimal_element (≺⋅) UNIV" and
    compat_equiv_prec: "C1 ≐ D1 ⟹ C2 ≐ D2 ⟹ C1 ≺⋅ C2 ⟹ D1 ≺⋅ D2" and
    equiv_F_grounding: "q ∈ Q ⟹ C1 ≐ C2 ⟹ 𝒢_F_q q C1 ⊆ 𝒢_F_q q C2" and
    prec_F_grounding: "q ∈ Q ⟹ C2 ≺⋅ C1 ⟹ 𝒢_F_q q C1 ⊆ 𝒢_F_q q C2" and
    static_ref_comp: "statically_complete_calculus Bot_F Inf_F (⊨∩𝒢)
      no_labels.Red_I_𝒢 no_labels.Red_F_𝒢_empty" and
    inf_have_prems: "ιF ∈ Inf_F ⟹ prems_of ιF ≠ []"
begin

lemma po_on_DL_Prec_L: "po_on (⊏L) UNIV"
  by (metis (mono_tags, lifting) DL_Prec_L_def irreflp_onI less_imp_neq order.strict_trans po_on_def
      transp_onI)

lemma wfp_on_DL_Prec_L: "wfp_on (⊏L) UNIV"
  unfolding wfp_on_UNIV DL_Prec_L_def by (simp add: wfP_app)

lemma Active_minimal: "l2 ≠ Active ⟹ Active ⊏L l2"
  by (cases l2) (auto simp: DL_Prec_L_def)

lemma at_least_two_labels: "∃l2. Active ⊏L l2"
  using Active_minimal by blast

sublocale lgc?: lazy_given_clause Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q Red_F_q 𝒢_F_q 𝒢_I_q
  Equiv_F Prec_F DL_Prec_L Active
  apply unfold_locales
              apply simp
             apply simp
            apply (rule equiv_equiv_F)
          apply (simp add: minimal_element.po wf_prec_F)
          using minimal_element.wf wf_prec_F apply blast
         apply (rule po_on_DL_Prec_L)
        apply (rule wfp_on_DL_Prec_L)
       apply (fact compat_equiv_prec)
      apply (fact equiv_F_grounding)
     apply (fact prec_F_grounding)
    apply (fact Active_minimal)
   apply (rule at_least_two_labels)
  using static_ref_comp statically_complete_calculus.statically_complete apply fastforce
  done

notation lgc.step (infix "↝LGC" 50)


subsection ‹Basic Definitions and Lemmas›

abbreviation c_dot_succ :: "'f ⇒ 'f ⇒ bool " (infix "⋅≻" 50) where
  "C ⋅≻ C' ≡ C' ≺⋅ C"
abbreviation sqsupset :: "DL_label ⇒ DL_label ⇒ bool" (infix "⊐L" 50) where
  "l ⊐L l' ≡ l' ⊏L l"

fun labeled_formulas_of :: " 'f set × 'f set × 'f set ⇒ ('f × DL_label) set " where
  "labeled_formulas_of (P, Y, A) = {(C, Passive) | C. C ∈ P} ∪ {(C, YY) | C. C ∈ Y} ∪
     {(C, Active) | C. C ∈ A}"

lemma labeled_formulas_of_alt_def:
  "labeled_formulas_of (P, Y, A) =
   (λC. (C, Passive)) ` P ∪ (λC. (C, YY)) ` Y ∪ (λC. (C, Active)) ` A"
  by auto

fun
  state :: "'f inference set × 'f set × 'f set × 'f set ⇒ 'f inference set × ('f × DL_label) set"
where
  "state (T, P, Y, A) = (T, labeled_formulas_of (P, Y, A))"

lemma state_alt_def:
  "state (T, P, Y, A) = (T, (λC. (C, Passive)) ` P ∪ (λC. (C, YY)) ` Y ∪ (λC. (C, Active)) ` A)"
  by auto

inductive
  DL :: "'f inference set × ('f × DL_label) set ⇒ 'f inference set × ('f × DL_label) set ⇒ bool"
  (infix "↝DL" 50)
where
  compute_infer: "ι ∈ no_labels.Red_I (A ∪ {C}) ⟹
    state (T ∪ {ι}, P, {}, A) ↝DL state (T, P, {C}, A)"
| choose_p: "state (T, P ∪ {C}, {}, A) ↝DL state (T, P, {C}, A)"
| delete_fwd: "C ∈ no_labels.Red_F A ∨ (∃C' ∈ A. C' ≼⋅ C) ⟹
    state (T, P, {C}, A) ↝DL state (T, P, {}, A)"
| simplify_fwd: "C ∈ no_labels.Red_F (A ∪ {C'}) ⟹
    state (T, P, {C}, A) ↝DL state (T, P, {C'}, A)"
| delete_bwd: "C' ∈ no_labels.Red_F {C} ∨ C' ⋅≻ C ⟹
    state (T, P, {C}, A ∪ {C'}) ↝DL state (T, P, {C}, A)"
| simplify_bwd: "C' ∈ no_labels.Red_F {C, C''} ⟹
    state (T, P, {C}, A ∪ {C'}) ↝DL state (T, P ∪ {C''}, {C}, A)"
| schedule_infer: "T' = no_labels.Inf_between A {C} ⟹
    state (T, P, {C}, A) ↝DL state (T ∪ T', P, {}, A ∪ {C})"
| delete_orphan_infers: "T' ∩ no_labels.Inf_from A = {} ⟹
    state (T ∪ T', P, Y, A) ↝DL state (T, P, Y, A)"

lemma If_f_in_A_then_fl_in_PYA: "C' ∈ A ⟹ (C', Active) ∈ labeled_formulas_of (P, Y, A)"
  by auto

lemma PYA_add_passive_formula[simp]:
  "labeled_formulas_of (P, Y, A) ∪ {(C, Passive)} = labeled_formulas_of (P ∪ {C}, Y, A)"
  by auto

lemma P0A_add_y_formula[simp]:
  "labeled_formulas_of (P, {}, A) ∪ {(C, YY)} = labeled_formulas_of (P, {C}, A)"
  by auto

lemma PYA_add_active_formula[simp]:
  "labeled_formulas_of (P, Y, A) ∪ {(C', Active)} = labeled_formulas_of (P, Y, A ∪ {C'})"
  by auto

lemma prj_active_subset_of_state: "fst ` active_subset (labeled_formulas_of (P, Y, A)) = A"
proof -
  have "active_subset {(C, YY) | C. C ∈ Y} = {}" and
       "active_subset {(C, Passive) | C. C ∈ P} = {}"
    using active_subset_def by auto
  moreover have "active_subset {(C, Active) | C. C ∈ A} = {(C, Active) | C. C ∈ A}"
    using active_subset_def by fastforce
  ultimately have "fst ` active_subset (labeled_formulas_of (P, Y, A)) =
    fst ` ({(C, Active) | C. C ∈ A})"
    by simp
  then show ?thesis
    by simp
qed

lemma active_subset_of_setOfFormulasWithLabelDiffActive:
  "l ≠ Active ⟹ active_subset {(C', l)} = {}"
  using active_subset_def by auto


subsection ‹Refinement›

lemma dl_compute_infer_in_lgc:
  assumes "ι ∈ no_labels.Red_I_𝒢 (A ∪ {C})"
  shows "state (T ∪ {ι}, P, {}, A) ↝LGC state (T, P, {C}, A)"
proof -
  let ?𝒩 = "labeled_formulas_of (P, {}, A)"
  and ?ℳ = "{(C, YY)}"
  have "A ∪ {C} ⊆ fst` (labeled_formulas_of (P, {}, A) ∪ {(C, YY)})"
    by auto
  then have "ι ∈ no_labels.Red_I_𝒢 (fst` (?𝒩 ∪ ?ℳ))"
    by (meson assms no_labels.empty_ord.Red_I_of_subset subsetD)
  also have "active_subset ?ℳ = {}"
    using active_subset_of_setOfFormulasWithLabelDiffActive by auto
  then have "(T ∪ {ι}, ?𝒩) ↝LGC (T, ?𝒩 ∪ ?ℳ)"
    using calculation lgc.step.compute_infer by blast
  moreover have "?𝒩 ∪ ?ℳ = labeled_formulas_of (P, {C}, A)"
    by simp
  ultimately show ?thesis
    by auto
qed

lemma dl_choose_p_in_lgc: "state (T, P ∪ {C}, {}, A) ↝LGC state (T, P, {C}, A)"
proof -
  let ?𝒩 = "labeled_formulas_of (P, {}, A)"
  have "Passive ⊐L YY"
    by (simp add: DL_Prec_L_def)
  then have "(T, ?𝒩 ∪ {(C, Passive)}) ↝LGC (T, ?𝒩 ∪ {(C, YY)})"
    using relabel_inactive by blast
  then have "(T, labeled_formulas_of (P ∪ {C}, {}, A)) ↝LGC (T, labeled_formulas_of (P, {C}, A))"
     by (metis PYA_add_passive_formula P0A_add_y_formula)
  then show ?thesis
    by auto
qed

lemma dl_delete_fwd_in_lgc:
  assumes " (C ∈ no_labels.Red_F A) ∨ (∃C'∈A. C' ≼⋅ C)"
  shows "state (T, P, {C}, A) ↝LGC state (T, P, {}, A)"
  using assms
proof
  assume c_in: "C ∈ no_labels.Red_F A"
  then have "A ⊆ fst ` (labeled_formulas_of (P, {}, A))"
    by simp
  then have "C ∈ no_labels.Red_F (fst ` (labeled_formulas_of (P, {}, A)))"
    by (metis (no_types, lifting) c_in in_mono no_labels.Red_F_of_subset)
  then show ?thesis
    using remove_redundant_no_label by auto
next
  assume "∃C'∈A. C' ≼⋅ C"
  then obtain C' where c'_in_and_c'_ls_c: "C' ∈ A ∧ C' ≼⋅ C"
    by auto
  then have "(C', Active) ∈ labeled_formulas_of (P, {}, A)"
    by auto
  then have "YY ⊐L Active"
    by (simp add: DL_Prec_L_def)
  then show ?thesis
    by (metis c'_in_and_c'_ls_c remove_succ_L state.simps P0A_add_y_formula
        If_f_in_A_then_fl_in_PYA)
qed

lemma dl_simplify_fwd_in_lgc:
  assumes "C ∈ no_labels.Red_F_𝒢 (A ∪ {C'})"
  shows "state (T, P, {C}, A) ↝LGC state (T, P, {C'}, A)"
proof -
  let ?𝒩 = "labeled_formulas_of (P, {}, A)"
  and ?ℳ = "{(C, YY)}"
  and ?ℳ'= "{(C', YY)}"
  have "A ∪ {C'} ⊆ fst` (?𝒩 ∪ ?ℳ')"
    by auto
  then have "C ∈ no_labels.Red_F_𝒢 (fst` (?𝒩 ∪ ?ℳ'))"
    by (smt (verit, ccfv_threshold) assms no_labels.Red_F_of_subset subset_iff)
  then have "(C, YY) ∈ Red_F (?𝒩 ∪ ?ℳ')"
    using no_labels_Red_F_imp_Red_F by simp
  then have "?ℳ ⊆ Red_F_𝒢 (?𝒩 ∪ ?ℳ')"
    by simp
  moreover have "active_subset ?ℳ' = {}"
    using active_subset_of_setOfFormulasWithLabelDiffActive by blast
  ultimately have "(T, labeled_formulas_of (P, {}, A) ∪ {(C, YY)}) ↝LGC
    (T, labeled_formulas_of (P, {}, A) ∪ {(C', YY)})"
    using process[of _ _ "?ℳ" _ "?ℳ'"] by auto
  then show ?thesis
    by simp
qed

lemma dl_delete_bwd_in_lgc:
  assumes "C' ∈ no_labels.Red_F_𝒢 {C} ∨ C' ⋅≻ C"
  shows "state (T, P, {C}, A ∪ {C'}) ↝LGC state (T, P, {C}, A)"
  using assms
proof
  let ?𝒩 = "labeled_formulas_of (P, {C}, A)"
  assume c'_in: "C' ∈ no_labels.Red_F_𝒢 {C}"
  have "{C} ⊆ fst ` ?𝒩"
    by simp
  then have "C' ∈ no_labels.Red_F_𝒢 (fst` ?𝒩)"
    by (metis (no_types, lifting) c'_in insert_Diff insert_subset no_labels.Red_F_of_subset)
  then have "(T, ?𝒩 ∪ {(C', Active)}) ↝LGC (T, ?𝒩)"
    using remove_redundant_no_label by auto
  then show ?thesis
    by (metis state.simps PYA_add_active_formula)
next
  assume "C' ⋅≻ C"
  moreover have "(C, YY) ∈ labeled_formulas_of (P, {C}, A)"
    by simp
  ultimately show ?thesis
    by (metis remove_succ_F state.simps PYA_add_active_formula)
qed

lemma dl_simplify_bwd_in_lgc:
  assumes "C' ∈ no_labels.Red_F_𝒢 {C, C''}"
  shows "state (T, P, {C}, A ∪ {C'}) ↝LGC state (T, P ∪ {C''}, {C}, A)"
proof -
  let ?ℳ = "{(C', Active)}"
  and ?ℳ' = "{(C'', Passive)}"
  and ?𝒩 = "labeled_formulas_of (P, {C}, A)"

  have "{C, C''} ⊆ fst` (?𝒩 ∪ ?ℳ')"
    by simp
  then have "C' ∈ no_labels.Red_F_𝒢 (fst` (?𝒩 ∪ ?ℳ'))"
    by (smt (z3) DiffI Diff_eq_empty_iff assms empty_iff no_labels.Red_F_of_subset)
  then have ℳ_included: "?ℳ ⊆ Red_F_𝒢 (?𝒩 ∪ ?ℳ')"
    using no_labels_Red_F_imp_Red_F by auto
  then have "active_subset ?ℳ' = {}"
    using active_subset_def by auto
  then have "(T, ?𝒩 ∪ ?ℳ) ↝LGC (T, ?𝒩 ∪ ?ℳ')"
    using ℳ_included process[of _ _ "?ℳ" _ "?ℳ'"] by auto
  moreover have "?𝒩 ∪ ?ℳ = labeled_formulas_of(P, {C}, A ∪ {C'})"
  and "?𝒩 ∪ ?ℳ' = labeled_formulas_of(P ∪ {C''}, {C}, A)"
    by auto
  ultimately show ?thesis
    by auto
qed

lemma dl_schedule_infer_in_lgc:
  assumes "T' = no_labels.Inf_between A {C}"
  shows "state (T, P, {C}, A) ↝LGC state (T ∪ T', P, {}, A ∪ {C})"
proof -
  let ?𝒩 = "labeled_formulas_of (P, {}, A)"
  have "fst ` (active_subset ?𝒩) = A"
    using prj_active_subset_of_state by blast
  then have "T' = no_labels.Inf_between (fst ` (active_subset ?𝒩)) {C}"
    using assms by auto
  then have "(T, labeled_formulas_of (P, {}, A) ∪ {(C, YY)}) ↝LGC
    (T ∪ T', labeled_formulas_of (P, {}, A) ∪ {(C, Active)})"
    using lgc.step.schedule_infer by blast
  then show ?thesis
    by (metis state.simps P0A_add_y_formula PYA_add_active_formula)
qed

lemma dl_delete_orphan_infers_in_lgc:
  assumes "T' ∩ no_labels.Inf_from A = {}"
  shows "state (T ∪ T', P, Y, A) ↝LGC state (T, P, Y, A)"
proof -
  let ?𝒩 = "labeled_formulas_of (P, Y, A)"
  have "fst ` (active_subset ?𝒩) = A"
    using prj_active_subset_of_state by blast
  then have "T' ∩ no_labels.Inf_from (fst ` (active_subset ?𝒩)) = {}"
    using assms by simp
  then have "(T ∪ T', ?𝒩) ↝LGC (T, ?𝒩)"
    using lgc.step.delete_orphan_infers by blast
  then show ?thesis
    by simp
qed

theorem DL_step_imp_LGC_step: "Tℳ ↝DL Tℳ' ⟹ Tℳ ↝LGC Tℳ'"
proof (induction rule: DL.induct)
  case (compute_infer ι A C T P)
  then show ?case
    using dl_compute_infer_in_lgc by blast
next
  case (choose_p T P C A)
  then show ?case
    using dl_choose_p_in_lgc by auto
next
  case (delete_fwd C A T P)
  then show ?case
    using dl_delete_fwd_in_lgc by auto
next
  case (simplify_fwd C A C' T P)
  then show ?case
    using dl_simplify_fwd_in_lgc by blast
next
  case (delete_bwd C' C T P A)
  then show ?case
    using dl_delete_bwd_in_lgc by blast
next
  case (simplify_bwd C' C C'' T P A)
  then show ?case
    using dl_simplify_bwd_in_lgc by blast
next
  case (schedule_infer T' A C T P)
  then show ?case
    using dl_schedule_infer_in_lgc by blast
next
  case (delete_orphan_infers T' A T P Y)
  then show ?case
    using dl_delete_orphan_infers_in_lgc by blast
qed


subsection ‹Completeness›

theorem
  assumes
    dl_chain: "chain (↝DL) Sts" and
    act: "active_subset (snd (lhd Sts)) = {}" and
    pas: "passive_subset (Liminf_llist (lmap snd Sts)) = {}" and
    no_prems_init: "∀ι ∈ Inf_F. prems_of ι = [] ⟶ ι ∈ fst (lhd Sts)" and
    final_sched: "Liminf_llist (lmap fst Sts) = {}"
  shows
    DL_Liminf_saturated: "saturated (Liminf_llist (lmap snd Sts))" and
    DL_complete_Liminf: "B ∈ Bot_F ⟹ fst ` snd (lhd Sts) ⊨∩𝒢 {B} ⟹
      ∃BL ∈ Bot_FL. BL ∈ Liminf_llist (lmap snd Sts)" and
    DL_complete: "B ∈ Bot_F ⟹ fst ` snd (lhd Sts) ⊨∩𝒢 {B} ⟹
      ∃i. enat i < llength Sts ∧ (∃BL ∈ Bot_FL. BL ∈ snd (lnth Sts i))"
proof -
  have lgc_chain: "chain (↝LGC) Sts"
    using dl_chain DL_step_imp_LGC_step chain_mono by blast

  show "saturated (Liminf_llist (lmap snd Sts))"
    using act final_sched lgc.fair_implies_Liminf_saturated lgc_chain lgc_fair lgc_to_red
      no_prems_init pas by blast
  {
    assume
      bot: "B ∈ Bot_F" and
      unsat: "fst ` snd (lhd Sts) ⊨∩𝒢 {B}"

    show "∃BL ∈ Bot_FL. BL ∈ Liminf_llist (lmap snd Sts)"
      by (rule lgc_complete_Liminf[OF lgc_chain act pas no_prems_init final_sched bot unsat])
    then show "∃i. enat i < llength Sts ∧ (∃BL ∈ Bot_FL. BL ∈ snd (lnth Sts i))"
      unfolding Liminf_llist_def by auto
  }
qed

end

end