Theory Zipperposition_Loop

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

section ‹Zipperposition Loop with Ghost State›

text ‹The Zipperposition loop is a variant of the DISCOUNT loop that can cope
with inferences generating (countably) infinitely many conclusions. The version
formalized here has an additional ghost component @{text D} in its state tuple,
which is used in the refinement proof from the abstract procedure @{text LGC}.›

theory Zipperposition_Loop
  imports DISCOUNT_Loop
begin

context discount_loop
begin


subsection ‹Basic Definitions and Lemmas›

fun flat_inferences_of :: "'f inference llist multiset ⇒ 'f inference set" where
  "flat_inferences_of T = ⋃ {lset ι |ι. ι ∈# T}"

fun
  zl_state :: "'f inference llist multiset × 'f inference set × 'f set × 'f set × 'f set ⇒
    'f inference set × ('f × DL_label) set"
where
  "zl_state (T, D, P, Y, A) = (flat_inferences_of T - D, labeled_formulas_of (P, Y, A))"

lemma zl_state_alt_def:
  "zl_state (T, D, P, Y, A) =
   (flat_inferences_of T - D, (λC. (C, Passive)) ` P ∪ (λC. (C, YY)) ` Y ∪ (λC. (C, Active)) ` A)"
  by auto

inductive
  ZL :: "'f inference set × ('f × DL_label) set ⇒ 'f inference set × ('f × DL_label) set ⇒ bool"
  (infix ‹↝ZL› 50)
where
  compute_infer: "ι0 ∈ no_labels.Red_I (A ∪ {C}) ⟹
    zl_state (T + {#LCons ι0 ιs#}, D, P, {}, A) ↝ZL zl_state (T + {#ιs#}, D ∪ {ι0}, P ∪ {C}, {}, A)"
| choose_p: "zl_state (T, D, P ∪ {C}, {}, A) ↝ZL zl_state (T, D, P, {C}, A)"
| delete_fwd: "C ∈ no_labels.Red_F A ∨ (∃C' ∈ A. C' ≼⋅ C) ⟹
    zl_state (T, D, P, {C}, A) ↝ZL zl_state (T, D, P, {}, A)"
| simplify_fwd: "C ∈ no_labels.Red_F (A ∪ {C'}) ⟹
    zl_state (T, D, P, {C}, A) ↝ZL zl_state (T, D, P, {C'}, A)"
| delete_bwd: "C' ∈ no_labels.Red_F {C} ∨ C' ⋅≻ C ⟹
    zl_state (T, D, P, {C}, A ∪ {C'}) ↝ZL zl_state (T, D, P, {C}, A)"
| simplify_bwd: "C' ∈ no_labels.Red_F {C, C''} ⟹
    zl_state (T, D, P, {C}, A ∪ {C'}) ↝ZL zl_state (T, D, P ∪ {C''}, {C}, A)"
| schedule_infer: "flat_inferences_of T' = no_labels.Inf_between A {C} ⟹
    zl_state (T, D, P, {C}, A) ↝ZL zl_state (T + T', D - flat_inferences_of T', P, {}, A ∪ {C})"
| delete_orphan_infers: "lset ιs ∩ no_labels.Inf_from A = {} ⟹
    zl_state (T + {#ιs#}, D, P, Y, A) ↝ZL zl_state (T, D ∪ lset ιs, P, Y, A)"


subsection ‹Refinement›

lemma zl_compute_infer_in_lgc:
  assumes "ι0 ∈ no_labels.Red_I (A ∪ {C})"
  shows "zl_state (T + {#LCons ι0 ιs#}, D, P, {}, A) ↝LGC
    zl_state (T + {#ιs#}, D ∪ {ι0}, P ∪ {C}, {}, A)"
proof -
  show ?thesis
  proof (cases "ι0 ∈ D")
    case True
    hence infs: "flat_inferences_of (T + {#LCons ι0 ιs#}) - D =
      flat_inferences_of (T + {#ιs#}) - (D ∪ {ι0})"
      by fastforce
    show ?thesis
      unfolding zl_state.simps infs
      by (rule step.process[of _ "labeled_formulas_of (P, {}, A)" "{}" _ "{(C, Passive)}"])
        (auto simp: active_subset_def)
  next
    case i0_ni: False
    show ?thesis
      unfolding zl_state.simps
    proof (rule step.compute_infer[of _ _ ι0 _ _ "{(C, Passive)}"])
      show "flat_inferences_of (T + {#LCons ι0 ιs#}) - D =
        flat_inferences_of (T + {#ιs#}) - (D ∪ {ι0}) ∪ {ι0}"
        using i0_ni by fastforce
    next
      show "labeled_formulas_of (P ∪ {C}, {}, A) = labeled_formulas_of (P, {}, A) ∪ {(C, Passive)}"
        by auto
    next
      show "active_subset {(C, Passive)} = {}"
        by (auto simp: active_subset_def)
    next
      show "ι0 ∈ no_labels.Red_I_𝒢 (fst ` (labeled_formulas_of (P, {}, A) ∪ {(C, Passive)}))"
        by simp (metis (no_types) Un_commute Un_empty_right Un_insert_right Un_upper1 assms
            no_labels.empty_ord.Red_I_of_subset subset_iff)
    qed
  qed
qed

lemma zl_choose_p_in_lgc: "zl_state (T, D, P ∪ {C}, {}, A) ↝LGC zl_state (T, D, P, {C}, A)"
proof -
  let ?𝒩 = "labeled_formulas_of (P, {}, A)"
  and ?𝒯 = "flat_inferences_of T - D"
  have "Passive ⊐L YY"
    by (simp add: DL_Prec_L_def)
  hence "(?𝒯, ?𝒩 ∪ {(C, Passive)}) ↝LGC (?𝒯, ?𝒩 ∪ {(C, YY)})"
    using relabel_inactive by blast
  hence "(?𝒯, labeled_formulas_of (P ∪ {C}, {}, A)) ↝LGC (?𝒯, labeled_formulas_of (P, {C}, A))"
     by (metis PYA_add_passive_formula P0A_add_y_formula)
  thus ?thesis
    by auto
qed

lemma zl_delete_fwd_in_lgc:
  assumes "C ∈ no_labels.Red_F A ∨ (∃C' ∈ A. C' ≼⋅ C)"
  shows "zl_state (T, D, P, {C}, A) ↝LGC zl_state (T, D, P, {}, A)"
  using assms
proof
  assume c_in: "C ∈ no_labels.Red_F A"
  hence "A ⊆ fst ` labeled_formulas_of (P, {}, A)"
    by simp
  hence "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)
  thus ?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
  hence "(C', Active) ∈ labeled_formulas_of (P, {}, A)"
    by auto
  moreover have "YY ⊐L Active"
    by (simp add: DL_Prec_L_def)
  ultimately show ?thesis
    by (metis P0A_add_y_formula remove_succ_L c'_in_and_c'_ls_c zl_state.simps)
qed

lemma zl_simplify_fwd_in_lgc:
  assumes "C ∈ no_labels.Red_F_𝒢 (A ∪ {C'})"
  shows "zl_state (T, D, P, {C}, A) ↝LGC zl_state (T, D, P, {C'}, A)"
proof -
  let ?𝒩 = "labeled_formulas_of (P, {}, A)"
  and ?ℳ = "{(C, YY)}"
  and ?ℳ'= "{(C', YY)}"
  have "A ∪ {C'} ⊆ fst ` (?𝒩 ∪ ?ℳ')"
    by auto
  hence "C ∈ no_labels.Red_F_𝒢 (fst` (?𝒩 ∪ ?ℳ'))"
    by (smt (verit, ccfv_SIG) assms no_labels.Red_F_of_subset subset_iff)
  hence "(C, YY) ∈ Red_F (?𝒩 ∪ ?ℳ')"
    using no_labels_Red_F_imp_Red_F by simp
  hence "?ℳ ⊆ Red_F_𝒢 (?𝒩 ∪ ?ℳ')"
    by simp
  moreover have "active_subset ?ℳ' = {}"
    using active_subset_def by auto
  ultimately have "(flat_inferences_of T - D, labeled_formulas_of (P, {}, A) ∪ {(C, YY)}) ↝LGC
    (flat_inferences_of T - D, labeled_formulas_of (P, {}, A) ∪ {(C', YY)})"
    using process[of _ _ "?ℳ" _ "?ℳ'"] by auto
  thus ?thesis
    by simp
qed

lemma zl_delete_bwd_in_lgc:
  assumes "C' ∈ no_labels.Red_F_𝒢 {C} ∨ C' ⋅≻ C"
  shows "zl_state (T, D, P, {C}, A ∪ {C'}) ↝LGC zl_state (T, D, 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
  hence "C' ∈ no_labels.Red_F_𝒢 (fst` ?𝒩)"
    by (metis (no_types, lifting) c'_in insert_Diff insert_subset no_labels.Red_F_of_subset)
  hence "(flat_inferences_of T - D, ?𝒩 ∪ {(C', Active)}) ↝LGC (flat_inferences_of T - D, ?𝒩)"
    using remove_redundant_no_label by auto

  moreover have "?𝒩 ∪ {(C', Active)} = labeled_formulas_of (P, {C}, A ∪ {C'})"
    using PYA_add_active_formula by blast
  ultimately have "(flat_inferences_of T - D, labeled_formulas_of (P, {C}, A ∪ {C'})) ↝LGC
    zl_state (T, D, P, {C}, A)"
    by simp
  thus ?thesis
    by auto
next
  assume "C' ⋅≻ C"
  moreover have "(C, YY) ∈ labeled_formulas_of (P, {C}, A)"
    by simp
  ultimately show ?thesis
    by (metis remove_succ_F PYA_add_active_formula zl_state.simps)
qed

lemma zl_simplify_bwd_in_lgc:
  assumes "C' ∈ no_labels.Red_F_𝒢 {C, C''}"
  shows "zl_state (T, D, P, {C}, A ∪ {C'}) ↝LGC zl_state (T, D, P ∪ {C''}, {C}, A)"
proof -
  let ?ℳ = "{(C', Active)}"
  and ?ℳ' = "{(C'', Passive)}"
  and ?𝒩 = "labeled_formulas_of (P, {C}, A)"
  have "{C, C''} ⊆ fst` (?𝒩 ∪ ?ℳ')"
    by simp
  hence "C' ∈ no_labels.Red_F_𝒢 (fst` (?𝒩 ∪ ?ℳ'))"
    by (smt (z3) DiffI Diff_eq_empty_iff assms empty_iff no_labels.Red_F_of_subset)
  hence ℳ_included: " ?ℳ ⊆ Red_F_𝒢 (?𝒩 ∪ ?ℳ')"
    using no_labels_Red_F_imp_Red_F by auto
  have "active_subset ?ℳ' = {}"
    using active_subset_def by auto
  hence "(flat_inferences_of T - D, ?𝒩 ∪ ?ℳ) ↝LGC (flat_inferences_of T - D, ?𝒩 ∪ ?ℳ')"
    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 zl_schedule_infer_in_lgc:
  assumes "flat_inferences_of T' = no_labels.Inf_between A {C}"
  shows "zl_state (T, D, P, {C}, A) ↝LGC
    zl_state (T + T', D - flat_inferences_of T', P, {}, A ∪ {C})"
proof -
  let ?𝒩 = "labeled_formulas_of (P, {}, A)"
  have "fst ` active_subset ?𝒩 = A"
    by (meson prj_active_subset_of_state)
  hence infs: "flat_inferences_of T' = no_labels.Inf_between (fst ` active_subset ?𝒩) {C}"
    using assms by simp

  have inf: "(flat_inferences_of T - D, ?𝒩 ∪ {(C, YY)}) ↝LGC
    ((flat_inferences_of T - D) ∪ flat_inferences_of T', ?𝒩 ∪ {(C, Active)})"
    by (rule step.schedule_infer[of _ _ "flat_inferences_of T'" _ ?𝒩 C YY]) (use infs in auto)

  have m_bef: "labeled_formulas_of (P, {C}, A) = ?𝒩 ∪ {(C, YY)}"
    by auto
  have t_aft: "flat_inferences_of (T + T') - (D - flat_inferences_of T') =
    (flat_inferences_of T - D) ∪ flat_inferences_of T'"
    by auto
  have m_aft: "labeled_formulas_of (P, {}, A ∪ {C}) = ?𝒩 ∪ {(C, Active)}"
    by auto
  show ?thesis
    unfolding zl_state.simps m_bef t_aft m_aft using inf .
qed

lemma zl_delete_orphan_infers_in_lgc:
  assumes inter: "lset ιs ∩ no_labels.Inf_from A = {}"
  shows "zl_state (T + {#ιs#}, D, P, Y, A) ↝LGC zl_state (T, D ∪ lset ιs, P, Y, A)"
proof -
  let ?𝒩 = "labeled_formulas_of (P, Y, A)"

  have inf: "(flat_inferences_of T ∪ lset ιs - D, ?𝒩)
    ↝LGC (flat_inferences_of T - (D ∪ lset ιs), ?𝒩)"
    by (rule step.delete_orphan_infers[of _ _ "lset ιs - D"])
      (use inter prj_active_subset_of_state in auto)

  have t_bef: "flat_inferences_of (T + {#ιs#}) - D = flat_inferences_of T ∪ lset ιs - D"
    by auto
  show ?thesis
    unfolding zl_state.simps t_bef using inf .
qed

theorem ZL_step_imp_LGC_step: "St ↝ZL St' ⟹ St ↝LGC St'"
proof (induction rule: ZL.induct)
  case (compute_infer ι0 A C T ιs D P)
  thus ?case
    using zl_compute_infer_in_lgc by auto
next
  case (choose_p T D P C A)
  thus ?case
    using zl_choose_p_in_lgc by auto
next
  case (delete_fwd C A T D P)
  thus ?case
    using zl_delete_fwd_in_lgc by auto
next
  case (simplify_fwd C A C' T D P)
  thus ?case
    using zl_simplify_fwd_in_lgc by blast
next
  case (delete_bwd C' C T D P A)
  thus ?case
    using zl_delete_bwd_in_lgc by blast
next
  case (simplify_bwd C' C C'' T D P A)
  thus ?case
    using zl_simplify_bwd_in_lgc by blast
next
  case (schedule_infer T' A C T D P)
  thus ?case
    using zl_schedule_infer_in_lgc by blast
next
  case (delete_orphan_infers ιs A T D P Y)
  thus ?case
    using zl_delete_orphan_infers_in_lgc by auto
qed


subsection ‹Completeness›

theorem
  assumes
    zl_chain: "chain (↝ZL) 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
    ZL_Liminf_saturated: "saturated (Liminf_llist (lmap snd Sts))" and
    ZL_complete_Liminf: "B ∈ Bot_F ⟹ fst ` snd (lhd Sts) ⊨∩𝒢 {B} ⟹
      ∃BL ∈ Bot_FL. BL ∈ Liminf_llist (lmap snd Sts)" and
    ZL_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 zl_chain ZL_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 ZL_complete_Liminf: "∃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])
    thus OL_complete: "∃i. enat i < llength Sts ∧ (∃BL ∈ Bot_FL. BL ∈ snd (lnth Sts i))"
      unfolding Liminf_llist_def by auto
  }
qed

end

end