Theory Fair_DISCOUNT_Loop

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

section ‹Fair DISCOUNT Loop›

text ‹The fair DISCOUNT loop assumes that the passive queue is fair and
ensures (dynamic) refutational completeness under that assumption.›

theory Fair_DISCOUNT_Loop
  imports
    Given_Clause_Loops_Util
    DISCOUNT_Loop
    Prover_Queue
begin


subsection ‹Locale›

type_synonym ('p, 'f) DLf_state = "'p × 'f option × 'f fset"

datatype 'f passive_elem =
  is_passive_inference: Passive_Inference (passive_inference: "'f inference")
| is_passive_formula: Passive_Formula (passive_formula: 'f)

lemma passive_inference_filter:
  "passive_inference ` Set.filter is_passive_inference N = {ι. Passive_Inference ι ∈ N}"
  by force

lemma passive_formula_filter:
  "passive_formula ` Set.filter is_passive_formula N = {C. Passive_Formula C ∈ N}"
  by force

locale fair_discount_loop =
  discount_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 +
  fair_prover_queue empty select add remove felems
  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) and
    empty :: 'p and
    select :: "'p ⇒ 'f passive_elem" and
    add :: "'f passive_elem ⇒ 'p ⇒ 'p" and
    remove :: "'f passive_elem ⇒ 'p ⇒ 'p" and
    felems :: "'p ⇒ 'f passive_elem fset" +
  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

lemma trans_Prec_S: "trans {(x, y). x ≺S y}"
  using transp_Prec_S transp_trans by blast

lemma irreflp_Prec_S: "irreflp (≺S)"
  using minimal_element.wf wfp_imp_irreflp wf_Prec_S wfp_on_UNIV by blast

lemma irrefl_Prec_S: "irrefl {(x, y). x ≺S y}"
  by (metis CollectD case_prod_conv irrefl_def irreflp_Prec_S irreflp_def)


subsection ‹Basic Definitions and Lemmas›

abbreviation passive_of :: "('p, 'f) DLf_state ⇒ 'p" where
  "passive_of St ≡ fst St"
abbreviation yy_of :: "('p, 'f) DLf_state ⇒ 'f option" where
  "yy_of St ≡ fst (snd St)"
abbreviation active_of :: "('p, 'f) DLf_state ⇒ 'f fset" where
  "active_of St ≡ snd (snd St)"

definition passive_inferences_of :: "'p ⇒ 'f inference set" where
  "passive_inferences_of P = {ι. Passive_Inference ι ∈ elems P}"
definition passive_formulas_of :: "'p ⇒ 'f set" where
  "passive_formulas_of P = {C. Passive_Formula C ∈ elems P}"

lemma finite_passive_inferences_of: "finite (passive_inferences_of P)"
proof -
  have inj_pi: "inj Passive_Inference"
    unfolding inj_on_def by auto
  show ?thesis
    unfolding passive_inferences_of_def by (auto intro: finite_inverse_image[OF _ inj_pi])
qed

lemma finite_passive_formulas_of: "finite (passive_formulas_of P)"
proof -
  have inj_pi: "inj Passive_Formula"
    unfolding inj_on_def by auto
  show ?thesis
    unfolding passive_formulas_of_def by (auto intro: finite_inverse_image[OF _ inj_pi])
qed

abbreviation all_formulas_of :: "('p, 'f) DLf_state ⇒ 'f set" where
  "all_formulas_of St ≡ passive_formulas_of (passive_of St) ∪ set_option (yy_of St) ∪
     fset (active_of St)"

lemma passive_inferences_of_empty[simp]: "passive_inferences_of empty = {}"
  unfolding passive_inferences_of_def by simp

lemma passive_inferences_of_add_Passive_Inference[simp]:
  "passive_inferences_of (add (Passive_Inference ι) P) = {ι} ∪ passive_inferences_of P"
  unfolding passive_inferences_of_def by auto

lemma passive_inferences_of_add_Passive_Formula[simp]:
  "passive_inferences_of (add (Passive_Formula C) P) = passive_inferences_of P"
  unfolding passive_inferences_of_def by auto

lemma passive_inferences_of_fold_add_Passive_Inference[simp]:
  "passive_inferences_of (fold (add ∘ Passive_Inference) ιs P) = passive_inferences_of P ∪ set ιs"
  by (induct ιs arbitrary: P) auto

lemma passive_inferences_of_fold_add_Passive_Formula[simp]:
  "passive_inferences_of (fold (add ∘ Passive_Formula) Cs P) = passive_inferences_of P"
  by (induct Cs arbitrary: P) auto

lemma passive_inferences_of_remove_Passive_Inference[simp]:
  "passive_inferences_of (remove (Passive_Inference ι) P) = passive_inferences_of P - {ι}"
  unfolding passive_inferences_of_def by auto

lemma passive_inferences_of_remove_Passive_Formula[simp]:
  "passive_inferences_of (remove (Passive_Formula C) P) = passive_inferences_of P"
  unfolding passive_inferences_of_def by auto

lemma passive_inferences_of_fold_remove_Passive_Inference[simp]:
  "passive_inferences_of (fold (remove ∘ Passive_Inference) ιs P) = passive_inferences_of P - set ιs"
  by (induct ιs arbitrary: P) auto

lemma passive_inferences_of_fold_remove_Passive_Formula[simp]:
  "passive_inferences_of (fold (remove ∘ Passive_Formula) Cs P) = passive_inferences_of P"
  by (induct Cs arbitrary: P) auto

lemma passive_formulas_of_empty[simp]: "passive_formulas_of empty = {}"
  unfolding passive_formulas_of_def by simp

lemma passive_formulas_of_add_Passive_Inference[simp]:
  "passive_formulas_of (add (Passive_Inference ι) P) = passive_formulas_of P"
  unfolding passive_formulas_of_def by auto

lemma passive_formulas_of_add_Passive_Formula[simp]:
  "passive_formulas_of (add (Passive_Formula C) P) = {C} ∪ passive_formulas_of P"
  unfolding passive_formulas_of_def by auto

lemma passive_formulas_of_fold_add_Passive_Inference[simp]:
  "passive_formulas_of (fold (add ∘ Passive_Inference) ιs P) = passive_formulas_of P"
  by (induct ιs arbitrary: P) auto

lemma passive_formulas_of_fold_add_Passive_Formula[simp]:
  "passive_formulas_of (fold (add ∘ Passive_Formula) Cs P) = passive_formulas_of P ∪ set Cs"
  by (induct Cs arbitrary: P) auto

lemma passive_formulas_of_remove_Passive_Inference[simp]:
  "passive_formulas_of (remove (Passive_Inference ι) P) = passive_formulas_of P"
  unfolding passive_formulas_of_def by auto

lemma passive_formulas_of_remove_Passive_Formula[simp]:
  "passive_formulas_of (remove (Passive_Formula C) P) = passive_formulas_of P - {C}"
  unfolding passive_formulas_of_def by auto

lemma passive_formulas_of_fold_remove_Passive_Inference[simp]:
  "passive_formulas_of (fold (remove ∘ Passive_Inference) ιs P) = passive_formulas_of P"
  by (induct ιs arbitrary: P) auto

lemma passive_formulas_of_fold_remove_Passive_Formula[simp]:
  "passive_formulas_of (fold (remove ∘ Passive_Formula) Cs P) = passive_formulas_of P - set Cs"
  by (induct Cs arbitrary: P) auto

fun fstate :: "('p, 'f) DLf_state ⇒ 'f inference set × ('f × DL_label) set" where
  "fstate (P, Y, A) = state (passive_inferences_of P, passive_formulas_of P, set_option Y, fset A)"

lemma fstate_alt_def:
  "fstate St = state (passive_inferences_of (fst St), passive_formulas_of (fst St),
     set_option (fst (snd St)), fset (snd (snd St)))"
  by (cases St) auto

definition Liminf_fstate :: "('p, 'f) DLf_state llist ⇒ 'f set × 'f set × 'f set" where
  "Liminf_fstate Sts =
   (Liminf_llist (lmap (passive_formulas_of ∘ passive_of) Sts),
    Liminf_llist (lmap (set_option ∘ yy_of) Sts),
    Liminf_llist (lmap (fset ∘ active_of) Sts))"

lemma Liminf_fstate_commute:
  "Liminf_llist (lmap (snd ∘ fstate) Sts) = labeled_formulas_of (Liminf_fstate Sts)"
proof -
  have "Liminf_llist (lmap (snd ∘ fstate) Sts) =
    (λC. (C, Passive)) ` Liminf_llist (lmap (passive_formulas_of ∘ passive_of) Sts) ∪
    (λC. (C, YY)) ` Liminf_llist (lmap (set_option ∘ yy_of) Sts) ∪
    (λC. (C, Active)) ` Liminf_llist (lmap (fset ∘ active_of) Sts)"
    unfolding fstate_alt_def state_alt_def
    apply simp
    apply (subst Liminf_llist_lmap_union, fast)+
    apply (subst Liminf_llist_lmap_image, simp add: inj_on_convol_ident)+
    by auto
 thus ?thesis
   unfolding Liminf_fstate_def by fastforce
qed

fun formulas_union :: "'f set × 'f set × 'f set ⇒ 'f set" where
  "formulas_union (P, Y, A) = P ∪ Y ∪ A"

inductive fair_DL :: "('p, 'f) DLf_state ⇒ ('p, 'f) DLf_state ⇒ bool" (infix ‹↝DLf› 50) where
  compute_infer: "P ≠ empty ⟹ select P = Passive_Inference ι ⟹
    ι ∈ no_labels.Red_I (fset A ∪ {C}) ⟹
    (P, None, A) ↝DLf (remove (select P) P, Some C, A)"
| choose_p: "P ≠ empty ⟹ select P = Passive_Formula C ⟹
    (P, None, A) ↝DLf (remove (select P) P, Some C, A)"
| delete_fwd: "C ∈ no_labels.Red_F (fset A) ∨ (∃C' ∈ fset A. C' ≼⋅ C) ⟹
    (P, Some C, A) ↝DLf (P, None, A)"
| simplify_fwd: "C' ≺S C ⟹ C ∈ no_labels.Red_F (fset A ∪ {C'}) ⟹
    (P, Some C, A) ↝DLf (P, Some C', A)"
| delete_bwd: "C' |∉| A ⟹ C' ∈ no_labels.Red_F {C} ∨ C' ⋅≻ C ⟹
    (P, Some C, A |∪| {|C'|}) ↝DLf (P, Some C, A)"
| simplify_bwd: "C' |∉| A ⟹ C'' ≺S C' ⟹ C' ∈ no_labels.Red_F {C, C''} ⟹
    (P, Some C, A |∪| {|C'|}) ↝DLf (add (Passive_Formula C'') P, Some C, A)"
| schedule_infer: "set ιs = no_labels.Inf_between (fset A) {C} ⟹
    (P, Some C, A) ↝DLf (fold (add ∘ Passive_Inference) ιs P, None, A |∪| {|C|})"
| delete_orphan_infers: "ιs ≠ [] ⟹ set ιs ⊆ passive_inferences_of P ⟹
    set ιs ∩ no_labels.Inf_from (fset A) = {} ⟹
    (P, Y, A) ↝DLf (fold (remove ∘ Passive_Inference) ιs P, Y, A)"


subsection ‹Initial State and Invariant›

inductive is_initial_DLf_state :: "('p, 'f) DLf_state ⇒ bool" where
  "is_initial_DLf_state (empty, None, {||})"

inductive DLf_invariant :: "('p, 'f) DLf_state ⇒ bool" where
  "passive_inferences_of P ⊆ Inf_F ⟹ DLf_invariant (P, Y, A)"

lemma initial_DLf_invariant: "is_initial_DLf_state St ⟹ DLf_invariant St"
  unfolding is_initial_DLf_state.simps DLf_invariant.simps by auto

lemma step_DLf_invariant:
  assumes
    inv: "DLf_invariant St" and
    step: "St ↝DLf St'"
  shows "DLf_invariant St'"
  using step inv
proof cases
  case (schedule_infer ιs A C P)
  note defs = this(1,2) and ιs_inf_betw = this(3)
  have "set ιs ⊆ Inf_F"
    using ιs_inf_betw unfolding no_labels.Inf_between_def no_labels.Inf_from_def by auto
  thus ?thesis
    using inv unfolding defs
    by (auto simp: DLf_invariant.simps passive_inferences_of_def fold_map[symmetric])
qed (auto simp: DLf_invariant.simps passive_inferences_of_def fold_map[symmetric])

lemma chain_DLf_invariant_lnth:
  assumes
    chain: "chain (↝DLf) Sts" and
    fair_hd: "DLf_invariant (lhd Sts)" and
    i_lt: "enat i < llength Sts"
  shows "DLf_invariant (lnth Sts i)"
  using i_lt
proof (induct i)
  case 0
  thus ?case
    using fair_hd lhd_conv_lnth zero_enat_def by fastforce
next
  case (Suc i)
  note ih = this(1) and si_lt = this(2)

  have "enat i < llength Sts"
    using si_lt Suc_ile_eq nless_le by blast
  hence inv_i: "DLf_invariant (lnth Sts i)"
    by (rule ih)
  have step: "lnth Sts i ↝DLf lnth Sts (Suc i)"
    using chain chain_lnth_rel si_lt by blast

  show ?case
    by (rule step_DLf_invariant[OF inv_i step])
qed

lemma chain_DLf_invariant_llast:
  assumes
    chain: "chain (↝DLf) Sts" and
    fair_hd: "DLf_invariant (lhd Sts)" and
    fin: "lfinite Sts"
  shows "DLf_invariant (llast Sts)"
proof -
  obtain i :: nat where
    i: "llength Sts = enat i"
    using lfinite_llength_enat[OF fin] by blast

  have im1_lt: "enat (i - 1) < llength Sts"
    by (metis chain chain_length_pos diff_less enat_ord_simps(2) i zero_enat_def zero_less_one)

  show ?thesis
    using chain_DLf_invariant_lnth[OF chain fair_hd im1_lt]
    by (metis Suc_diff_1 chain chain_length_pos eSuc_enat enat_ord_simps(2) i llast_conv_lnth
        zero_enat_def)
qed


subsection ‹Final State›

inductive is_final_DLf_state :: "('p, 'f) DLf_state ⇒ bool" where
  "is_final_DLf_state (empty, None, A)"

lemma is_final_DLf_state_iff_no_DLf_step:
  assumes inv: "DLf_invariant St"
  shows "is_final_DLf_state St ⟷ (∀St'. ¬ St ↝DLf St')"
proof
  assume "is_final_DLf_state St"
  then obtain A :: "'f fset" where
    st: "St = (empty, None, A)"
    by (auto simp: is_final_DLf_state.simps)
  show "∀St'. ¬ St ↝DLf St'"
    unfolding st
  proof (intro allI notI)
    fix St'
    assume "(empty, None, A) ↝DLf St'"
    thus False
      by cases auto
  qed
next
  assume no_step: "∀St'. ¬ St ↝DLf St'"
  show "is_final_DLf_state St"
  proof (rule ccontr)
    assume not_fin: "¬ is_final_DLf_state St"

    obtain P :: 'p and Y :: "'f option" and A :: "'f fset" where
      st: "St = (P, Y, A)"
      by (cases St)

    have "P ≠ empty ∨ Y ≠ None"
      using not_fin unfolding st is_final_DLf_state.simps by auto
    moreover {
      assume
        p: "P ≠ empty" and
        y: "Y = None"

      have "∃St'. St ↝DLf St'"
      proof (cases "select P")
        case sel: (Passive_Inference ι)
        hence ι_inf: "ι ∈ Inf_F"
          using inv p unfolding st by (metis DLf_invariant.cases fst_conv mem_Collect_eq
              passive_inferences_of_def select_in_felems subset_iff)
        have ι_red: "ι ∈ no_labels.Red_I_𝒢 (fset A ∪ {concl_of ι})"
          using ι_inf no_labels.empty_ord.Red_I_of_Inf_to_N by auto
        show ?thesis
          using fair_DL.compute_infer[OF p sel ι_red] unfolding st p y by blast
      next
        case (Passive_Formula C)
        then show ?thesis
          using fair_DL.choose_p[OF p] unfolding st p y by fast
      qed
    } moreover {
      assume "Y ≠ None"
      then obtain C :: 'f where
        y: "Y = Some C"
        by blast

      have fin: "finite (no_labels.Inf_between (fset A) {C})"
        by (rule finite_Inf_between[of "fset A", simplified])
      obtain ιs :: "'f inference list" where
        ιs: "set ιs = no_labels.Inf_between (fset A) {C}"
        using finite_imp_set_eq[OF fin] by blast

      have "∃St'. St ↝DLf St'"
        using fair_DL.schedule_infer[OF ιs] unfolding st y by fast
    } ultimately show False
      using no_step by force
  qed
qed


subsection ‹Refinement›

lemma fair_DL_step_imp_DL_step:
  assumes dlf: "(P, Y, A) ↝DLf (P', Y', A')"
  shows "fstate (P, Y, A) ↝DL fstate (P', Y', A')"
  using dlf
proof cases
  case (compute_infer ι C)
  note defs = this(1-4) and p_nemp = this(5) and sel = this(6) and ι_red = this(7)

  have pas_min_ι_uni_ι: "passive_inferences_of P - {ι} ∪ {ι} = passive_inferences_of P"
    by (metis Un_insert_right insert_Diff_single insert_absorb mem_Collect_eq p_nemp
        passive_inferences_of_def sel select_in_felems sup_bot.right_neutral)

  show ?thesis
    unfolding defs fstate_alt_def
    using DL.compute_infer[OF ι_red,
        of "passive_inferences_of (remove (select P) P)" "passive_formulas_of P"]
    by (simp only: sel prod.sel option.set passive_inferences_of_remove_Passive_Inference
        passive_formulas_of_remove_Passive_Inference pas_min_ι_uni_ι)
next
  case (choose_p C)
  note defs = this(1-4) and p_nemp = this(5) and sel = this(6)

  have pas_min_c_uni_c: "passive_formulas_of P - {C} ∪ {C} = passive_formulas_of P"
    by (metis Un_insert_right insert_Diff mem_Collect_eq p_nemp passive_formulas_of_def sel
        select_in_felems sup_bot.right_neutral)

  show ?thesis
    unfolding defs fstate_alt_def
    using DL.choose_p[of "passive_inferences_of P" "passive_formulas_of (remove (select P) P)" C
        "fset A"]
    unfolding sel by (simp only: prod.sel option.set passive_formulas_of_remove_Passive_Formula
        passive_inferences_of_remove_Passive_Formula pas_min_c_uni_c)
next
  case (delete_fwd C)
  note defs = this(1-4) and c_red = this(5)
  show ?thesis
    unfolding defs fstate_alt_def using DL.delete_fwd[OF c_red] by simp
next
  case (simplify_fwd C' C)
  note defs = this(1-4) and c_red = this(6)
  show ?thesis
    unfolding defs fstate_alt_def using DL.simplify_fwd[OF c_red] by simp
next
  case (delete_bwd C' C)
  note defs = this(1-4) and c'_red = this(6)
  show ?thesis
    unfolding defs fstate_alt_def using DL.delete_bwd[OF c'_red] by simp
next
  case (simplify_bwd C'' C' C)
  note defs = this(1-4) and c''_red = this(7)
  show ?thesis
    unfolding defs fstate_alt_def using DL.simplify_bwd[OF c''_red] by simp
next
  case (schedule_infer ιs C)
  note defs = this(1-4) and ιs = this(5)
  show ?thesis
    unfolding defs fstate_alt_def
    using DL.schedule_infer[OF ιs, of "passive_inferences_of P" "passive_formulas_of P"] by simp
next
  case (delete_orphan_infers ιs)
  note defs = this(1-3) and ιs_ne = this(4) and ιs_pas = this(5) and inter = this(6)

  have pas_min_ιs_uni_ιs: "passive_inferences_of P - set ιs ∪ set ιs = passive_inferences_of P"
    by (simp add: ιs_pas set_eq_subset)

  show ?thesis
    unfolding defs fstate_alt_def
    using DL.delete_orphan_infers[OF inter,
        of "passive_inferences_of (fold (remove ∘ Passive_Inference) ιs P)"
        "passive_formulas_of P" "set_option Y"]
    by (simp only: prod.sel passive_inferences_of_fold_remove_Passive_Inference
        passive_formulas_of_fold_remove_Passive_Inference pas_min_ιs_uni_ιs)
qed

lemma fair_DL_step_imp_GC_step:
  "(P, Y, A) ↝DLf (P', Y', A') ⟹ fstate (P, Y, A) ↝LGC fstate (P', Y', A')"
  by (rule DL_step_imp_LGC_step[OF fair_DL_step_imp_DL_step])


subsection ‹Completeness›

fun mset_of_fstate :: "('p, 'f) DLf_state ⇒ 'f multiset" where
  "mset_of_fstate (P, Y, A) =
   image_mset concl_of (mset_set (passive_inferences_of P)) + mset_set (passive_formulas_of P) +
   mset_set (set_option Y) + mset_set (fset A)"

abbreviation Precprec_S :: "'f multiset ⇒ 'f multiset ⇒ bool" (infix ‹≺≺S› 50) where
  "(≺≺S) ≡ multp (≺S)"

lemma wfP_Precprec_S: "wfP (≺≺S)"
  using minimal_element_def wfp_multp wf_Prec_S wfp_on_UNIV by blast

definition Less_state :: "('p, 'f) DLf_state ⇒ ('p, 'f) DLf_state ⇒ bool" (infix ‹⊏› 50) where
  "St' ⊏ St ⟷
   (yy_of St' = None ∧ yy_of St ≠ None)
   ∨ ((yy_of St' = None ⟷ yy_of St = None) ∧ mset_of_fstate St' ≺≺S mset_of_fstate St)"

lemma wfP_Less_state: "wfP (⊏)"
proof -
  let ?boolset = "{(b', b :: bool). b' < b}"
  let ?msetset = "{(M', M). M' ≺≺S M}"
  let ?pair_of = "λSt. (yy_of St ≠ None, mset_of_fstate St)"

  have wf_boolset: "wf ?boolset"
    by (rule Wellfounded.wellorder_class.wf)
  have wf_msetset: "wf ?msetset"
    using wfP_Precprec_S wfp_def by auto
  have wf_lex_prod: "wf (?boolset <*lex*> ?msetset)"
    by (rule wf_lex_prod[OF wf_boolset wf_msetset])

  have Less_state_alt_def:
    "⋀St' St. St' ⊏ St ⟷ (?pair_of St', ?pair_of St) ∈ ?boolset <*lex*> ?msetset"
    unfolding Less_state_def by auto

  show ?thesis
    unfolding wfp_def Less_state_alt_def using wf_app[of _ ?pair_of] wf_lex_prod by blast
qed

lemma non_compute_infer_choose_p_DLf_step_imp_Less_state:
  assumes
    step: "St ↝DLf St'" and
    yy: "yy_of St ≠ None ∨ yy_of St' = None"
  shows "St' ⊏ St"
  using step
proof cases
  case (compute_infer P ι A C)
  note defs = this(1,2)
  have False
    using step yy unfolding defs by simp
  thus ?thesis
    by blast
next
  case (choose_p P C A)
  note defs = this(1,2)
  have False
    using step yy unfolding defs by simp
  thus ?thesis
    by blast
next
  case (delete_fwd C A P)
  note defs = this(1,2)
  show ?thesis
    unfolding defs Less_state_def by (auto intro!: subset_implies_multp)
next
  case (simplify_fwd C' C A P)
  note defs = this(1,2) and prec = this(3)

  let ?new_bef = "image_mset concl_of (mset_set (passive_inferences_of P)) +
    mset_set (passive_formulas_of P) + mset_set (fset A) + {#C#}"
  let ?new_aft = "image_mset concl_of (mset_set (passive_inferences_of P)) +
    mset_set (passive_formulas_of P) + mset_set (fset A) + {#C'#}"

  have lt_new: "?new_aft ≺≺S ?new_bef"
    unfolding multp_def
  proof (subst mult_cancelL[OF trans_Prec_S irrefl_Prec_S], fold multp_def)
    show "{#C'#} ≺≺S {#C#}"
      unfolding multp_def using prec by (auto intro: singletons_in_mult)
  qed
  thus ?thesis
    unfolding defs Less_state_def by simp
next
  case (delete_bwd C' A C P)
  note defs = this(1,2) and c_ni = this(3)
  show ?thesis
    unfolding defs Less_state_def using c_ni
    by (auto intro!: subset_implies_multp)
next
  case (simplify_bwd C' A C'' C P)
  note defs = this(1,2) and c'_ni = this(3) and prec = this(4)

  show ?thesis
  proof (cases "C'' ∈ passive_formulas_of P")
    case c''_in: True
    show ?thesis
      unfolding defs Less_state_def using c'_ni
      by (auto simp: insert_absorb[OF c''_in] intro!: subset_implies_multp)
  next
    case c''_ni: False

    have bef: "add_mset C (image_mset concl_of (mset_set (passive_inferences_of P)) +
        mset_set (passive_formulas_of P) + mset_set (insert C' (fset A))) =
      add_mset C
        (image_mset concl_of (mset_set (passive_inferences_of P)) +
         mset_set (passive_formulas_of P) + mset_set (fset A)) + {#C'#}" (is "?old_bef = ?new_bef")
      using c'_ni by auto
    have aft: "add_mset C
        (image_mset concl_of (mset_set (passive_inferences_of P)) +
         mset_set (insert C'' (passive_formulas_of P)) + mset_set (fset A)) =
      add_mset C
        (image_mset concl_of (mset_set (passive_inferences_of P)) +
         mset_set (passive_formulas_of P) + mset_set (fset A)) + {#C''#}" (is "?old_aft = ?new_aft")
      using c''_ni by (simp add: finite_passive_formulas_of)

    have lt_new: "?new_aft ≺≺S ?new_bef"
      unfolding multp_def
    proof (subst mult_cancelL[OF trans_Prec_S irrefl_Prec_S], fold multp_def)
      show "{#C''#} ≺≺S {#C'#}"
        unfolding multp_def using prec by (auto intro: singletons_in_mult)
    qed
    show ?thesis
      unfolding defs Less_state_def by simp (simp only: bef aft lt_new)
  qed
next
  case (schedule_infer ιs A C P)
  note defs = this(1,2)
  show ?thesis
    unfolding defs Less_state_def by auto
next
  case (delete_orphan_infers ιs P A Y)
  note defs = this(1,2) and ιs_nnil = this(3) and ιs_sub = this(4) and ιs_inter = this(5)
  have "image_mset concl_of (mset_set (passive_inferences_of P - set ιs)) ⊂#
    image_mset concl_of (mset_set (passive_inferences_of P))"
    by (metis Diff_empty Diff_subset ιs_nnil ιs_sub double_diff empty_subsetI
        finite_passive_inferences_of finite_subset image_mset_subset_mono mset_set_eq_iff set_empty
        subset_imp_msubset_mset_set subset_mset.nless_le)
  thus ?thesis
    unfolding defs Less_state_def by (auto intro!: subset_implies_multp)
qed

lemma yy_nonempty_DLf_step_imp_Less_state:
  assumes
    step: "St ↝DLf St'" and
    yy: "yy_of St ≠ None" and
    yy': "yy_of St' ≠ None"
  shows "St' ⊏ St"
proof -
  have "yy_of St ≠ None ∨ yy_of St' = None"
    using yy by blast
  thus ?thesis
    using non_compute_infer_choose_p_DLf_step_imp_Less_state[OF step] by blast
qed

lemma fair_DL_Liminf_yy_empty:
  assumes
    len: "llength Sts = ∞" and
    full: "full_chain (↝DLf) Sts" and
    inv: "DLf_invariant (lhd Sts)"
  shows "Liminf_llist (lmap (set_option ∘ yy_of) Sts) = {}"
proof (rule ccontr)
  assume lim_nemp: "Liminf_llist (lmap (set_option ∘ yy_of) Sts) ≠ {}"

  obtain i :: nat where
    i_lt: "enat i < llength Sts" and
    inter_nemp: "⋂ ((set_option ∘ yy_of ∘ lnth Sts) ` {j. i ≤ j ∧ enat j < llength Sts}) ≠ {}"
    using lim_nemp unfolding Liminf_llist_def by auto

  from inter_nemp obtain C :: 'f where
    c_in: "∀P ∈ lnth Sts ` {j. i ≤ j ∧ enat j < llength Sts}. C ∈ set_option (yy_of P)"
    by auto
  hence c_in': "∀j ≥ i. enat j < llength Sts ⟶ C ∈ set_option (yy_of (lnth Sts j))"
    by auto

  have si_lt: "enat (Suc i) < llength Sts"
    unfolding len by auto

  have yy_j: "yy_of (lnth Sts j) ≠ None" if j_ge: "j ≥ i" for j
    using c_in' len j_ge by auto
  hence yy_sj: "yy_of (lnth Sts (Suc j)) ≠ None" if j_ge: "j ≥ i" for j
    using le_Suc_eq that by presburger
  have step: "lnth Sts j ↝DLf lnth Sts (Suc j)" if j_ge: "j ≥ i" for j
    using full_chain_imp_chain[OF full] infinite_chain_lnth_rel len llength_eq_infty_conv_lfinite
    by blast

  have "lnth Sts (Suc j) ⊏ lnth Sts j" if j_ge: "j ≥ i" for j
    using yy_nonempty_DLf_step_imp_Less_state by (meson step j_ge yy_j yy_sj)
  hence "(⊏)¯¯ (lnth Sts j) (lnth Sts (Suc j))" if j_ge: "j ≥ i" for j
    using j_ge by blast
  hence inf_down_chain: "chain (⊏)¯¯ (ldropn i Sts)"
    by (simp add: chain_ldropnI si_lt)

  have inf_i: "¬ lfinite (ldropn i Sts)"
    using len by (simp add: llength_eq_infty_conv_lfinite)

  show False
    using inf_i inf_down_chain wfP_iff_no_infinite_down_chain_llist[of "(⊏)"] wfP_Less_state
    by metis
qed

lemma DLf_step_imp_queue_step:
  assumes "St ↝DLf St'"
  shows "queue_step (passive_of St) (passive_of St')"
  using assms
  by cases (auto simp: fold_map[symmetric] intro: queue_step_idleI queue_step_addI
      queue_step_removeI queue_step_fold_addI queue_step_fold_removeI)

lemma fair_DL_Liminf_passive_empty:
  assumes
    len: "llength Sts = ∞" and
    full: "full_chain (↝DLf) Sts" and
    init: "is_initial_DLf_state (lhd Sts)"
  shows "Liminf_llist (lmap (elems ∘ passive_of) Sts) = {}"
proof -
  have chain_step: "chain queue_step (lmap passive_of Sts)"
    using DLf_step_imp_queue_step chain_lmap full_chain_imp_chain[OF full]
    by (metis (no_types, lifting))

  have inf_oft: "infinitely_often select_queue_step (lmap passive_of Sts)"
  proof
    assume "finitely_often select_queue_step (lmap passive_of Sts)"
    then obtain i :: nat where
      no_sel:
        "∀j ≥ i. ¬ select_queue_step (passive_of (lnth Sts j)) (passive_of (lnth Sts (Suc j)))"
      by (metis (no_types, lifting) enat_ord_code(4) finitely_often_def len llength_lmap lnth_lmap)

    have si_lt: "enat (Suc i) < llength Sts"
      unfolding len by auto

    have step: "lnth Sts j ↝DLf lnth Sts (Suc j)" if j_ge: "j ≥ i" for j
      using full_chain_imp_chain[OF full] infinite_chain_lnth_rel len llength_eq_infty_conv_lfinite
      by blast

    have yy: "yy_of (lnth Sts j) ≠ None ∨ yy_of (lnth Sts (Suc j)) = None" if j_ge: "j ≥ i" for j
      using step[OF j_ge]
    proof cases
      case (compute_infer P ι A C)
      note defs = this(1,2) and p_ne = this(3)
      have False
        using no_sel defs p_ne select_queue_stepI that by fastforce
      thus ?thesis
        by blast
    next
      case (choose_p P C A)
      note defs = this(1,2) and p_ne = this(3)
      have False
        using no_sel defs p_ne select_queue_stepI that by fastforce
      thus ?thesis
        by blast
    qed auto

    have "lnth Sts (Suc j) ⊏ lnth Sts j" if j_ge: "j ≥ i" for j
      by (rule non_compute_infer_choose_p_DLf_step_imp_Less_state[OF step[OF j_ge] yy[OF j_ge]])
    hence "(⊏)¯¯ (lnth Sts j) (lnth Sts (Suc j))" if j_ge: "j ≥ i" for j
      using j_ge by blast
    hence inf_down_chain: "chain (⊏)¯¯ (ldropn i Sts)"
      using chain_ldropn_lmapI[OF _ si_lt, of _ id, simplified llist.map_id] by simp

    have inf_i: "¬ lfinite (ldropn i Sts)"
      using len lfinite_ldropn llength_eq_infty_conv_lfinite by blast

    show False
      using inf_i inf_down_chain wfP_iff_no_infinite_down_chain_llist[of "(⊏)"] wfP_Less_state
      by blast
  qed

  have hd_emp: "lhd (lmap passive_of Sts) = empty"
    using init full full_chain_not_lnull unfolding is_initial_DLf_state.simps by fastforce

  have "Liminf_llist (lmap elems (lmap passive_of Sts)) = {}"
    by (rule fair[of "lmap passive_of Sts", OF chain_step inf_oft hd_emp])
  thus ?thesis
    by (simp add: llist.map_comp)
qed

lemma fair_DL_Liminf_passive_formulas_empty:
  assumes
    len: "llength Sts = ∞" and
    full: "full_chain (↝DLf) Sts" and
    init: "is_initial_DLf_state (lhd Sts)"
  shows "Liminf_llist (lmap (passive_formulas_of ∘ passive_of) Sts) = {}"
proof -
  have lim_filt: "Liminf_llist (lmap (Set.filter is_passive_formula ∘ elems ∘ passive_of) Sts) = {}"
    using fair_DL_Liminf_passive_empty Liminf_llist_subset
    by (metis (no_types) empty_iff full init len llength_lmap llist.map_comp lnth_lmap member_filter
        subsetI subset_antisym)

  let ?g = "Set.filter is_passive_formula ∘ elems ∘ passive_of"

  have "inj_on passive_formula (Set.filter is_passive_formula (UNIV :: 'f passive_elem set))"
    unfolding inj_on_def by (metis member_filter passive_elem.collapse(2))
  moreover have "Sup_llist (lmap ?g Sts) ⊆ Set.filter is_passive_formula UNIV"
    unfolding Sup_llist_def by auto
  ultimately have inj_pi: "inj_on passive_formula (Sup_llist (lmap ?g Sts))"
    using inj_on_subset by blast

  have lim_pass: "Liminf_llist (lmap (λx. passive_formula `
    (Set.filter is_passive_formula ∘ elems ∘ passive_of) x) Sts) = {}"
    using Liminf_llist_lmap_image[OF inj_pi] lim_filt by simp

  have "Liminf_llist (lmap (λSt. {C. Passive_Formula C ∈ elems (passive_of St)}) Sts) = {}"
    using lim_pass passive_formula_filter by (smt (verit) Collect_cong comp_apply llist.map_cong)
  thus ?thesis
    unfolding passive_formulas_of_def comp_apply .
qed

lemma fair_DL_Liminf_passive_inferences_empty:
  assumes
    len: "llength Sts = ∞" and
    full: "full_chain (↝DLf) Sts" and
    init: "is_initial_DLf_state (lhd Sts)"
  shows "Liminf_llist (lmap (passive_inferences_of ∘ passive_of) Sts) = {}"
proof -
  have lim_filt: "Liminf_llist (lmap (Set.filter is_passive_inference ∘ elems ∘ passive_of) Sts) = {}"
    using fair_DL_Liminf_passive_empty Liminf_llist_subset
    by (metis (no_types) empty_iff full init len llength_lmap llist.map_comp lnth_lmap member_filter
        subsetI subset_antisym)

  let ?g = "Set.filter is_passive_inference ∘ elems ∘ passive_of"

  have "inj_on passive_inference (Set.filter is_passive_inference (UNIV :: 'f passive_elem set))"
    unfolding inj_on_def by (metis member_filter passive_elem.collapse(1))
  moreover have "Sup_llist (lmap ?g Sts) ⊆ Set.filter is_passive_inference UNIV"
    unfolding Sup_llist_def by auto
  ultimately have inj_pi: "inj_on passive_inference (Sup_llist (lmap ?g Sts))"
    using inj_on_subset by blast

  have lim_pass: "Liminf_llist (lmap (λx. passive_inference `
    (Set.filter is_passive_inference ∘ elems ∘ passive_of) x) Sts) = {}"
    using Liminf_llist_lmap_image[OF inj_pi] lim_filt by simp

  have "Liminf_llist (lmap (λSt. {ι. Passive_Inference ι ∈ elems (passive_of St)}) Sts) = {}"
    using lim_pass passive_inference_filter by (smt (verit) Collect_cong comp_apply llist.map_cong)
  thus ?thesis
    unfolding passive_inferences_of_def comp_apply .
qed

theorem
  assumes
    full: "full_chain (↝DLf) Sts" and
    init: "is_initial_DLf_state (lhd Sts)"
  shows
    fair_DL_Liminf_saturated: "saturated (labeled_formulas_of (Liminf_fstate Sts))" and
    fair_DL_complete_Liminf: "B ∈ Bot_F ⟹ passive_formulas_of (passive_of (lhd Sts)) ⊨∩𝒢 {B} ⟹
      ∃B' ∈ Bot_F. B' ∈ formulas_union (Liminf_fstate Sts)" and
    fair_DL_complete: "B ∈ Bot_F ⟹ passive_formulas_of (passive_of (lhd Sts)) ⊨∩𝒢 {B} ⟹
      ∃i. enat i < llength Sts ∧ (∃B' ∈ Bot_F. B' ∈ all_formulas_of (lnth Sts i))"
proof -
  have chain: "chain (↝DLf) Sts"
    by (rule full_chain_imp_chain[OF full])
  hence dl_chain: "chain (↝DL) (lmap fstate Sts)"
    by (smt (verit, del_insts) chain_lmap fair_DL_step_imp_DL_step mset_of_fstate.cases)

  have inv: "DLf_invariant (lhd Sts)"
    using init initial_DLf_invariant by auto

  have nnul: "¬ lnull Sts"
    using chain chain_not_lnull by blast
  hence lhd_lmap: "⋀f. lhd (lmap f Sts) = f (lhd Sts)"
    by (rule llist.map_sel(1))

  have "active_of (lhd Sts) = {||}"
    by (metis is_initial_DLf_state.cases init snd_conv)
  hence act: "active_subset (snd (lhd (lmap fstate Sts))) = {}"
    unfolding active_subset_def lhd_lmap by (cases "lhd Sts") auto

  have pas_fml_and_t_inf: "passive_subset (Liminf_llist (lmap (snd ∘ fstate) Sts)) = {} ∧
    Liminf_llist (lmap (fst ∘ fstate) Sts) = {}" (is "?pas_fml ∧ ?t_inf")
  proof (cases "lfinite Sts")
    case fin: True

    have lim_fst: "Liminf_llist (lmap (fst ∘ fstate) Sts) = fst (fstate (llast Sts))" and
      lim_snd: "Liminf_llist (lmap (snd ∘ fstate) Sts) = snd (fstate (llast Sts))"
      using lfinite_Liminf_llist fin nnul
      by (metis comp_eq_dest_lhs lfinite_lmap llast_lmap llist.map_disc_iff)+

    have last_inv: "DLf_invariant (llast Sts)"
      by (rule chain_DLf_invariant_llast[OF chain inv fin])

    have "∀St'. ¬ llast Sts ↝DLf St'"
      using full_chain_lnth_not_rel[OF full] by (metis fin full_chain_iff_chain full)
    hence "is_final_DLf_state (llast Sts)"
      unfolding is_final_DLf_state_iff_no_DLf_step[OF last_inv] .
    then obtain A :: "'f fset" where
      at_l: "llast Sts = (empty, None, A)"
      unfolding is_final_DLf_state.simps by blast

    have ?pas_fml
      unfolding passive_subset_def lim_snd at_l by auto
    moreover have ?t_inf
      unfolding lim_fst at_l by simp
    ultimately show ?thesis
      by blast
  next
    case False
    hence len: "llength Sts = ∞"
      by (simp add: not_lfinite_llength)

    have ?pas_fml
      unfolding Liminf_fstate_commute passive_subset_def Liminf_fstate_def
      using fair_DL_Liminf_passive_formulas_empty[OF len full init]
        fair_DL_Liminf_yy_empty[OF len full inv]
      by simp
    moreover have ?t_inf
      unfolding fstate_alt_def using fair_DL_Liminf_passive_inferences_empty[OF len full init]
      by simp
    ultimately show ?thesis
      by blast
  qed
  note pas_fml = pas_fml_and_t_inf[THEN conjunct1] and
    t_inf = pas_fml_and_t_inf[THEN conjunct2]

  have pas_fml': "passive_subset (Liminf_llist (lmap snd (lmap fstate Sts))) = {}"
    using pas_fml by (simp add: llist.map_comp)
  have t_inf': "Liminf_llist (lmap fst (lmap fstate Sts)) = {}"
    using t_inf by (simp add: llist.map_comp)

  have no_prems_init: "∀ι ∈ Inf_F. prems_of ι = [] ⟶ ι ∈ fst (lhd (lmap fstate Sts))"
    using inf_have_prems by blast

  show "saturated (labeled_formulas_of (Liminf_fstate Sts))"
    using DL_Liminf_saturated[OF dl_chain act pas_fml' no_prems_init t_inf']
    unfolding Liminf_fstate_commute[folded llist.map_comp] .

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

    have unsat': "fst ` snd (lhd (lmap fstate Sts)) ⊨∩𝒢 {B}"
      using unsat unfolding lhd_lmap by (cases "lhd Sts") (auto intro: no_labels_entails_mono_left)

    show "∃B' ∈ Bot_F. B' ∈ formulas_union (Liminf_fstate Sts)"
      using DL_complete_Liminf[OF dl_chain act pas_fml' no_prems_init t_inf' bot unsat']
      unfolding Liminf_fstate_commute[folded llist.map_comp]
      by (cases "Liminf_fstate Sts") auto
    thus "∃i. enat i < llength Sts ∧ (∃B' ∈ Bot_F. B' ∈ all_formulas_of (lnth Sts i))"
      unfolding Liminf_fstate_def Liminf_llist_def by auto
  }
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_discount_loop =
  discount_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_discount_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