Theory Fair_Otter_Loop_Complete

(* Title:        Completeness of Fair Otter Loop
   Authors:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2022-2023
   Maintainer:   Jasmin Blanchette <j.c.blanchette at vu.nl>
*)

section ‹Completeness of Fair Otter Loop›

text ‹The Otter loop is a special case of the iProver loop, with fewer rules.
We can therefore reuse the fair iProver loop's completeness result to derive the
(dynamic) refutational completeness of the fair Otter loop.›

theory Fair_Otter_Loop_Complete
  imports Fair_iProver_Loop
begin


subsection ‹Completeness›

context fair_otter_loop
begin

theorem
  assumes
    full: "full_chain (↝OLf) Sts" and
    init: "is_initial_OLf_state (lhd Sts)"
  shows
    fair_OL_Liminf_saturated: "saturated (state (Liminf_fstate Sts))" and
    fair_OL_complete_Liminf: "B ∈ Bot_F ⟹ fset (new_of (lhd Sts)) ⊨∩𝒢 {B} ⟹
      ∃B' ∈ Bot_F. B' ∈ state_union (Liminf_fstate Sts)" and
    fair_OL_complete: "B ∈ Bot_F ⟹ fset (new_of (lhd Sts)) ⊨∩𝒢 {B} ⟹
      ∃i. enat i < llength Sts ∧ (∃B' ∈ Bot_F. B' ∈ all_formulas_of (lnth Sts i))"
proof -
  have ilf_chain: "chain (↝ILf) Sts"
    using Lazy_List_Chain.chain_mono fair_IL.ol full_chain_imp_chain full by blast
  hence ilf_full: "full_chain (↝ILf) Sts"
    by (metis chain_ILf_invariant_llast full_chain_iff_chain initial_OLf_invariant
        is_final_OLf_state_iff_no_ILf_step is_final_OLf_state_iff_no_OLf_step full init)

  show "saturated (state (Liminf_fstate Sts))"
    by (rule fair_IL_Liminf_saturated[OF ilf_full init])

  {
    assume
      bot: "B ∈ Bot_F" and
      unsat: "fset (new_of (lhd Sts)) ⊨∩𝒢 {B}"

    show "∃B' ∈ Bot_F. B' ∈ state_union (Liminf_fstate Sts)"
      by (rule fair_IL_complete_Liminf[OF ilf_full init bot unsat])
    show "∃i. enat i < llength Sts ∧ (∃B' ∈ Bot_F. B' ∈ all_formulas_of (lnth Sts i))"
      by (rule fair_IL_complete[OF ilf_full init bot unsat])
  }
qed

end


subsection ‹Specialization with FIFO Queue›

text ‹As a proof of concept, we specialize the passive set to use a FIFO queue,
thereby eliminating the locale assumptions about the passive set.›

locale fifo_otter_loop =
  otter_loop 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
  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" and
    Equiv_F :: "'f ⇒ 'f ⇒ bool" (infix ‹≐› 50) and
    Prec_F :: "'f ⇒ 'f ⇒ bool" (infix ‹≺⋅› 50) +
  fixes
    Prec_S :: "'f ⇒ 'f ⇒ bool" (infix ‹≺S› 50)
  assumes
    wf_Prec_S: "minimal_element (≺S) UNIV" and
    transp_Prec_S: "transp (≺S)" and
    finite_Inf_between: "finite A ⟹ finite (no_labels.Inf_between A {C})"
begin

sublocale fifo_prover_queue
  .

sublocale fair_otter_loop 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 "[]" hd "λy xs. if y ∈ set xs then xs else xs @ [y]" removeAll fset_of_list Prec_S
proof
  show "po_on (≺S) UNIV"
    using wf_Prec_S minimal_element.po by blast
next
  show "wfp_on (≺S) UNIV"
    using wf_Prec_S minimal_element.wf by blast
next
  show "transp (≺S)"
    by (rule transp_Prec_S)
next
  show "⋀A C. finite A ⟹ finite (no_labels.Inf_between A {C})"
    by (fact finite_Inf_between)
qed

end

end