Theory iProver_Loop

(* Title:        iProver 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 ‹iProver Loop›

text ‹The iProver loop is a variant of the Otter loop that supports the
elimination of clauses that are made redundant by their own children.›

theory iProver_Loop
  imports Otter_Loop
begin

context otter_loop
begin


subsection ‹Definition›

inductive IL :: "('f × OL_label) set ⇒ ('f × OL_label) set ⇒ bool" (infix ‹↝IL› 50)
where
  ol: "St ↝OL St' ⟹ St ↝IL St'"
| red_by_children: "C ∈ no_labels.Red_F (A ∪ M) ∨ (M = {C'} ∧ C' ≺⋅ C) ⟹
    state ({}, {}, P, {C}, A) ↝IL state (M, {}, P, {}, A)"


subsection ‹Refinement›

lemma red_by_children_in_GC:
  assumes "C ∈ no_labels.Red_F (A ∪ M) ∨ (M = {C'} ∧ C' ≺⋅ C)"
  shows "state ({}, {}, P, {C}, A) ↝GC state (M, {}, P, {}, A)"
proof -
  let ?𝒩 = "state ({}, {}, P, {}, A)"
  and ?St = "{(C, YY)}"
  and ?St' = "{(x, New) |x. x ∈ M}"

  have "(C, YY) ∈ Red_F (?𝒩 ∪ ?St')"
    using assms
  proof
    assume c_in: "C ∈ no_labels.Red_F (A ∪ M)"
    have "A ∪ M ⊆ A ∪ M ∪ P" by auto
    also have "fst ` (?𝒩 ∪ ?St') = A ∪ M ∪ P"
      by auto
    then have "C ∈ no_labels.Red_F (fst ` (?𝒩 ∪ ?St'))"
      by (metis (no_types, lifting) c_in calculation in_mono no_labels.Red_F_of_subset)
    then show "(C, YY) ∈ Red_F (?𝒩 ∪ ?St')"
      using no_labels_Red_F_imp_Red_F by blast
  next
    assume assm: "M = {C'} ∧ C' ≺⋅ C"
    then have "C' ∈ fst ` (?𝒩 ∪ ?St')"
      by simp
    then show "(C, YY) ∈ Red_F (?𝒩 ∪ ?St')"
      by (metis (mono_tags) assm succ_F_imp_Red_F)
  qed
  then have St_included_in: "?St ⊆ Red_F (?𝒩 ∪ ?St')"
    by auto

  have prj_of_active_subset_of_St': "fst ` (active_subset ?St') = {}"
    by (simp add: active_subset_def)

  have "?𝒩 ∪ ?St ↝GC ?𝒩 ∪ ?St'"
    using process[of _ "?𝒩" "?St" _ "?St'"] St_included_in prj_of_active_subset_of_St' by auto
  moreover have "?𝒩 ∪ ?St = state ({}, {}, P, {C}, A)"
    by simp
  moreover have "?𝒩 ∪ ?St' = state (M, {}, P, {}, A)"
    by auto
  ultimately show "state ({}, {}, P, {C}, A) ↝GC state (M, {}, P, {}, A)"
    by simp
qed

theorem IL_step_imp_GC_step: "M ↝IL M' ⟹ M ↝GC M'"
proof (induction rule: IL.induct)
  case (ol St St')
  then show ?case
    by (simp add: OL_step_imp_GC_step)
next
  case (red_by_children C A M C' P)
  then show ?case using red_by_children_in_GC
    by auto
qed


subsection ‹Completeness›

theorem
  assumes
    il_chain: "chain (↝IL) Sts" and
    act: "active_subset (lhd Sts) = {}" and
    pas: "passive_subset (Liminf_llist Sts) = {}"
  shows
    IL_Liminf_saturated: "saturated (Liminf_llist Sts)" and
    IL_complete_Liminf: "B ∈ Bot_F ⟹ fst ` lhd Sts ⊨∩𝒢 {B} ⟹
      ∃BL ∈ Bot_FL. BL ∈ Liminf_llist Sts" and
    IL_complete: "B ∈ Bot_F ⟹ fst ` lhd Sts ⊨∩𝒢 {B} ⟹
      ∃i. enat i < llength Sts ∧ (∃BL ∈ Bot_FL. BL ∈ lnth Sts i)"
proof -
  have gc_chain: "chain (↝GC) Sts"
    using il_chain IL_step_imp_GC_step chain_mono by blast

  show "saturated (Liminf_llist Sts)"
    using gc.fair_implies_Liminf_saturated gc_chain gc_fair gc_to_red act pas by blast

  {
    assume
      bot: "B ∈ Bot_F" and
      unsat: "fst ` lhd Sts ⊨∩𝒢 {B}"
  
    show "∃BL ∈ Bot_FL. BL ∈ Liminf_llist Sts"
      by (rule gc_complete_Liminf[OF gc_chain act pas bot unsat])
    then show "∃i. enat i < llength Sts ∧ (∃BL ∈ Bot_FL. BL ∈ lnth Sts i)"
      unfolding Liminf_llist_def by auto
  }
qed

end

end