Theory Saturation_Framework_Extensions.Standard_Redundancy_Criterion

(*  Title:       Counterexample-Reducing Inference Systems and the Standard Redundancy Criterion
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017, 2020
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
    Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
    Author:      Martin Desharnais <desharnais at mpi-inf.mpg.de>, 2021
*)

section ‹Counterexample-Reducing Inference Systems and the Standard Redundancy Criterion›

theory Standard_Redundancy_Criterion
  imports
    Saturation_Framework.Calculus
    "HOL-Library.Multiset_Order"
begin

text ‹
The standard redundancy criterion can be defined uniformly for all inference systems equipped with
a compact consequence relation. The essence of the refutational completeness argument can be carried
out abstractly for counterexample-reducing inference systems, which enjoy a ``smallest
counterexample'' property. This material is partly based on Section 4.2 of Bachmair and Ganzinger's
\emph{Handbook} chapter, but adapted to the saturation framework of Waldmann et al.
›

subsection ‹Counterexample-Reducing Inference Systems›

abbreviation main_prem_of :: "'f inference  'f" where
  "main_prem_of ι  last (prems_of ι)"

abbreviation side_prems_of :: "'f inference  'f list" where
  "side_prems_of ι  butlast (prems_of ι)"

lemma set_prems_of:
  "set (prems_of ι) = (if prems_of ι = [] then {} else {main_prem_of ι}  set (side_prems_of ι))"
  by clarsimp (metis Un_insert_right append_Nil2 append_butlast_last_id list.set(2) set_append)

locale counterex_reducing_inference_system = inference_system Inf + consequence_relation
  for Inf :: "'f inference set" +
  fixes
    I_of :: "'f set  'f set" and
    less :: "'f  'f  bool" (infix "" 50)
  assumes
    wfP_less: "wfP (≺)" and
    Inf_counterex_reducing:
      "N  Bot = {}  D  N  ¬ I_of N  {D} 
      (C. C  N  ¬ I_of N  {C}  D  C  D = C) 
      ι  Inf. prems_of ι  []  main_prem_of ι = D  set (side_prems_of ι)  N 
        I_of N  set (side_prems_of ι)  ¬ I_of N  {concl_of ι}  concl_of ι  D"

begin

lemma ex_min_counterex:
  fixes N :: "'f set"
  assumes "¬ I  N"
  shows "C  N. ¬ I  {C}  (D  N. D  C  I  {D})"
proof -
  obtain C where
    "C  N" and "¬ I  {C}"
    using assms all_formulas_entailed by blast
  then have c_in: "C  {C  N. ¬ I  {C}}"
    by blast
  show ?thesis
    using wfP_eq_minimal[THEN iffD1, rule_format, OF wfP_less c_in] by blast
qed

end

text ‹
Theorem 4.4 (generalizes Theorems 3.9 and 3.16):
›

locale counterex_reducing_inference_system_with_trivial_redundancy =
  counterex_reducing_inference_system _ _ Inf + calculus _ Inf _ "λ_. {}" "λ_. {}"
  for Inf :: "'f inference set" +
  assumes less_total: "C D. C  D  C  D  D  C"
begin

theorem saturated_model:
  assumes
    satur: "saturated N" and
    bot_ni_n: "N  Bot = {}"
  shows "I_of N  N"
proof (rule ccontr)
  assume "¬ I_of N  N"
  then obtain D :: 'f where
    d_in_n: "D  N" and
    d_cex: "¬ I_of N  {D}" and
    d_min: "C. C  N  C  D  I_of N  {C}"
    by (meson ex_min_counterex)
  then obtain ι :: "'f inference" where
    ι_inf: "ι  Inf" and
    concl_cex: "¬ I_of N  {concl_of ι}" and
    concl_lt_d: "concl_of ι  D"
    using Inf_counterex_reducing[OF bot_ni_n] less_total
    by force
  have "concl_of ι  N"
    using ι_inf Red_I_of_Inf_to_N by blast
  then show False
    using concl_cex concl_lt_d d_min by blast
qed

text ‹
An abstract version of Corollary 3.10 does not hold without some conditions, according to Nitpick:
›

corollary saturated_complete:
  assumes
    satur: "saturated N" and
    unsat: "N  Bot"
  shows "N  Bot  {}"
  oops

end


subsection ‹Compactness›

locale concl_compact_consequence_relation = consequence_relation +
  assumes
    entails_concl_compact: "finite EE  CC  EE  CC'  CC. finite CC'  CC'  EE"
begin

lemma entails_concl_compact_union:
  assumes
    fin_e: "finite EE" and
    cd_ent: "CC  DD  EE"
  shows "CC'  CC. finite CC'  CC'  DD  EE"
proof -
  obtain CCDD' where
    cd1_fin: "finite CCDD'" and
    cd1_sub: "CCDD'  CC  DD" and
    cd1_ent: "CCDD'  EE"
    using entails_concl_compact[OF fin_e cd_ent] by blast

  define CC' where
    "CC' = CCDD' - DD"
  have "CC'  CC"
    unfolding CC'_def using cd1_sub by blast
  moreover have "finite CC'"
    unfolding CC'_def using cd1_fin by blast
  moreover have "CC'  DD  EE"
    unfolding CC'_def using cd1_ent
    by (metis Un_Diff_cancel2 Un_upper1 entails_trans subset_entailed)
  ultimately show ?thesis
    by blast
qed

end


subsection ‹The Finitary Standard Redundancy Criterion›

locale finitary_standard_formula_redundancy =
  consequence_relation Bot "(⊨)"
  for
    Bot :: "'f set" and
    entails :: "'f set  'f set  bool" (infix "" 50) +
  fixes
    less :: "'f  'f  bool" (infix "" 50)
  assumes
    transp_less: "transp (≺)" and
    wfP_less: "wfP (≺)"
begin

definition Red_F :: "'f set  'f set" where
  "Red_F N = {C. DD  N. finite DD  DD  {C}  (D  DD. D  C)}"

text ‹
The following results correspond to Lemma 4.5. The lemma wlog_non_Red_F› generalizes the core of
the argument.
›

lemma Red_F_of_subset: "N  N'  Red_F N  Red_F N'"
  unfolding Red_F_def by fast

lemma wlog_non_Red_F:
  assumes
    dd0_fin: "finite DD0" and
    dd0_sub: "DD0  N" and
    dd0_ent: "DD0  CC  {E}" and
    dd0_lt: "D'  DD0. D'  D"
  shows "DD  N - Red_F N. finite DD  DD  CC  {E}  (D'  DD. D'  D)"
proof -
  have mset_DD0_in: "mset_set DD0 
    {DD. set_mset DD  N  set_mset DD  CC  {E}  (D'  set_mset DD. D'  D)}"
    using assms finite_set_mset_mset_set by simp
  obtain DD :: "'f multiset" where
    dd_subs_n: "set_mset DD  N" and
    ddcc_ent_e: "set_mset DD  CC  {E}" and
    dd_lt_d: "D' ∈# DD. D'  D" and
    d_min: "y. multp (≺) y DD 
      y  {DD. set_mset DD  N  set_mset DD  CC  {E}  (D'∈#DD. D'  D)}"
    using wfP_eq_minimal[THEN iffD1, rule_format, OF wfP_less[THEN wfP_multp] mset_DD0_in]
    by blast

  have "Da ∈# DD. Da  Red_F N"
  proof clarify
    fix Da :: 'f
    assume
      da_in_dd: "Da ∈# DD" and
      da_rf: "Da  Red_F N"

    obtain DDa0 :: "'f set" where
      dda0_subs_n: "DDa0  N" and
      dda0_fin: "finite DDa0" and
      dda0_ent_da: "DDa0  {Da}" and
      dda0_lt_da: "D  DDa0. D  Da"
      using da_rf unfolding Red_F_def mem_Collect_eq
      by blast

    define DDa :: "'f multiset" where
      "DDa = DD - {#Da#} + mset_set DDa0"

    have "set_mset DDa  N"
      unfolding DDa_def using dd_subs_n dda0_subs_n finite_set_mset_mset_set[OF dda0_fin]
      by (smt (verit, best) contra_subsetD in_diffD subsetI union_iff)
    moreover have "set_mset DDa  CC  {E}"
    proof (rule entails_trans_strong[of _ "{Da}"])
      show "set_mset DDa  CC  {Da}"
        unfolding DDa_def set_mset_union finite_set_mset_mset_set[OF dda0_fin]
        by (rule entails_trans[OF _ dda0_ent_da]) (auto intro: subset_entailed)
    next
      have H: "set_mset (DD - {#Da#} + mset_set DDa0)  CC  {Da} =
        set_mset (DD + mset_set DDa0)  CC"
        by (smt (verit) Un_insert_left Un_insert_right da_in_dd insert_DiffM
            set_mset_add_mset_insert set_mset_union sup_bot.right_neutral)
      show "set_mset DDa  CC  {Da}  {E}"
        unfolding DDa_def H
        by (rule entails_trans[OF _ ddcc_ent_e]) (auto intro: subset_entailed)
    qed
    moreover have "D' ∈# DDa. D'  D"
      using dd_lt_d dda0_lt_da da_in_dd unfolding DDa_def
      using transp_less[THEN transpD]
      using finite_set_mset_mset_set[OF dda0_fin]
      by (metis insert_DiffM2 union_iff)
    moreover have "multp (≺) DDa DD"
      unfolding DDa_def multp_eq_multpDM[OF wfP_imp_asymp[OF wfP_less] transp_less] multpDM_def
      using finite_set_mset_mset_set[OF dda0_fin]
      by (metis da_in_dd dda0_lt_da mset_subset_eq_single multi_self_add_other_not_self
          union_single_eq_member)
    ultimately show False
      using d_min by (auto intro!: antisym)
  qed
  then show ?thesis
    using dd_subs_n ddcc_ent_e dd_lt_d by blast
qed

lemma Red_F_imp_ex_non_Red_F:
  assumes c_in: "C  Red_F N"
  shows "CC  N - Red_F N. finite CC  CC  {C}  (C'  CC. C'  C)"
proof -
  obtain DD :: "'f set" where
    dd_fin: "finite DD" and
    dd_sub: "DD  N" and
    dd_ent: "DD  {C}" and
    dd_lt: "D  DD. D  C"
    using c_in[unfolded Red_F_def] by fast
  show ?thesis
    by (rule wlog_non_Red_F[of "DD" N "{}" C C, simplified, OF dd_fin dd_sub dd_ent dd_lt])
qed

lemma Red_F_subs_Red_F_diff_Red_F: "Red_F N  Red_F (N - Red_F N)"
proof
  fix C
  assume c_rf: "C  Red_F N"
  then obtain CC :: "'f set" where
    cc_subs: "CC  N - Red_F N" and
    cc_fin: "finite CC" and
    cc_ent_c: "CC  {C}" and
    cc_lt_c: "C'  CC. C'  C"
    using Red_F_imp_ex_non_Red_F[of C N] by blast
  have "D  CC. D  Red_F N"
    using cc_subs by fast
  then have cc_nr:
    "C  CC. DD  N. finite DD  DD  {C}  (D  DD. ¬ D  C)"
    unfolding Red_F_def by simp
  have "CC  N"
    using cc_subs by auto
  then have "CC  N - {C. DD  N. finite DD  DD  {C}  (D  DD. D  C)}"
    using cc_nr by blast
  then show "C  Red_F (N - Red_F N)"
    using cc_fin cc_ent_c cc_lt_c unfolding Red_F_def by blast
qed

lemma Red_F_eq_Red_F_diff_Red_F: "Red_F N = Red_F (N - Red_F N)"
  by (simp add: Red_F_of_subset Red_F_subs_Red_F_diff_Red_F set_eq_subset)

text ‹
The following results correspond to Lemma 4.6.
›

lemma Red_F_of_Red_F_subset: "N'  Red_F N  Red_F N  Red_F (N - N')"
  by (metis Diff_mono Red_F_eq_Red_F_diff_Red_F Red_F_of_subset order_refl)

lemma Red_F_model: "M  N - Red_F N  M  N"
  by (metis (no_types) DiffI Red_F_imp_ex_non_Red_F entail_set_all_formulas entails_trans
      subset_entailed)

lemma Red_F_Bot: "B  Bot  N  {B}  N - Red_F N  {B}"
  using Red_F_model entails_trans subset_entailed by blast

end

locale calculus_with_finitary_standard_redundancy =
  inference_system Inf + finitary_standard_formula_redundancy Bot "(⊨)" "(≺)"
  for
    Inf :: "'f inference set" and
    Bot :: "'f set" and
    entails :: "'f set  'f set  bool" (infix "" 50) and
    less :: "'f  'f  bool" (infix "" 50) +
  assumes
    Inf_has_prem: "ι  Inf  prems_of ι  []" and
    Inf_reductive: "ι  Inf  concl_of ι  main_prem_of ι"
begin

definition redundant_infer :: "'f set  'f inference  bool" where
  "redundant_infer N ι 
   (DD  N. finite DD  DD  set (side_prems_of ι)  {concl_of ι}  (D  DD. D  main_prem_of ι))"

definition Red_I :: "'f set  'f inference set" where
  "Red_I N = {ι  Inf. redundant_infer N ι}"

text ‹
The following results correspond to Lemma 4.6. It also uses @{thm [source] wlog_non_Red_F}.
›

lemma Red_I_of_subset: "N  N'  Red_I N  Red_I N'"
  unfolding Red_I_def redundant_infer_def by auto

lemma Red_I_subs_Red_I_diff_Red_F: "Red_I N  Red_I (N - Red_F N)"
proof
  fix ι
  assume ι_ri: "ι  Red_I N"
  define CC :: "'f set" where
    "CC = set (side_prems_of ι)"
  define D :: 'f where
    "D = main_prem_of ι"
  define E :: 'f where
    "E = concl_of ι"
  obtain DD :: "'f set" where
    dd_fin: "finite DD" and
    dd_sub: "DD  N" and
    dd_ent: "DD  CC  {E}" and
    dd_lt_d: "C  DD. C  D"
    using ι_ri unfolding Red_I_def redundant_infer_def CC_def D_def E_def by blast
  obtain DDa :: "'f set" where
    "DDa  N - Red_F N" and "finite DDa" and "DDa  CC  {E}" and "D'  DDa. D'  D"
    using wlog_non_Red_F[OF dd_fin dd_sub dd_ent dd_lt_d] by blast
  then show "ι  Red_I (N - Red_F N)"
    using ι_ri unfolding Red_I_def redundant_infer_def CC_def D_def E_def by blast
qed

lemma Red_I_eq_Red_I_diff_Red_F: "Red_I N = Red_I (N - Red_F N)"
  by (metis Diff_subset Red_I_of_subset Red_I_subs_Red_I_diff_Red_F subset_antisym)

lemma Red_I_to_Inf: "Red_I N  Inf"
  unfolding Red_I_def by blast

lemma Red_I_of_Red_F_subset: "N'  Red_F N  Red_I N  Red_I (N - N')"
  by (metis Diff_mono Red_I_eq_Red_I_diff_Red_F Red_I_of_subset order_refl)

lemma Red_I_of_Inf_to_N:
  assumes
    in_ι: "ι  Inf" and
    concl_in: "concl_of ι  N"
  shows "ι  Red_I N"
proof -
  have "redundant_infer N ι"
    unfolding redundant_infer_def
    by (rule exI[where x = "{concl_of ι}"])
      (simp add: Inf_reductive[OF in_ι] subset_entailed concl_in)
  then show "ι  Red_I N"
    by (simp add: Red_I_def in_ι)
qed

text ‹
The following corresponds to Theorems 4.7 and 4.8:
›

sublocale calculus Bot Inf "(⊨)" Red_I Red_F
  by (unfold_locales, fact Red_I_to_Inf, fact Red_F_Bot, fact Red_F_of_subset,
      fact Red_I_of_subset, fact Red_F_of_Red_F_subset, fact Red_I_of_Red_F_subset,
      fact Red_I_of_Inf_to_N)

end


subsection ‹The Standard Redundancy Criterion›

locale standard_formula_redundancy =
  concl_compact_consequence_relation Bot "(⊨)"
  for
    Bot :: "'f set" and
    entails :: "'f set  'f set  bool" (infix "" 50) +
  fixes
    less :: "'f  'f  bool" (infix "" 50)
  assumes
    transp_less: "transp (≺)" and
    wfP_less: "wfP (≺)"
begin

definition Red_F :: "'f set  'f set" where
  "Red_F N = {C. DD  N. DD  {C}  (D  DD. D  C)}"

text ‹
Compactness of @{term "(⊨)"} implies that @{const Red_F} is equivalent to its finitary
  counterpart.
›

interpretation fin_std_red_F: finitary_standard_formula_redundancy Bot "(⊨)" "(≺)"
  using transp_less asymp_on_less wfP_less by unfold_locales

lemma Red_F_conv: "Red_F = fin_std_red_F.Red_F"
proof (intro ext)
  fix N
  show "Red_F N = fin_std_red_F.Red_F N"
    unfolding Red_F_def fin_std_red_F.Red_F_def
    using entails_concl_compact
    by (smt (verit, best) Collect_cong finite.emptyI finite_insert subset_eq)
qed

text ‹
The results from @{locale finitary_standard_formula_redundancy} can now be lifted.

The following results correspond to Lemma 4.5.
›

lemma Red_F_of_subset: "N  N'  Red_F N  Red_F N'"
  unfolding Red_F_conv
  by (rule fin_std_red_F.Red_F_of_subset)

lemma Red_F_imp_ex_non_Red_F: "C  Red_F N  CC  N - Red_F N. CC  {C}  (C'  CC. C'  C)"
  unfolding Red_F_conv
  using fin_std_red_F.Red_F_imp_ex_non_Red_F by meson

lemma Red_F_subs_Red_F_diff_Red_F: "Red_F N  Red_F (N - Red_F N)"
  unfolding Red_F_conv
  by (rule fin_std_red_F.Red_F_subs_Red_F_diff_Red_F)

lemma Red_F_eq_Red_F_diff_Red_F: "Red_F N = Red_F (N - Red_F N)"
  unfolding Red_F_conv
  by (rule fin_std_red_F.Red_F_eq_Red_F_diff_Red_F)

text ‹
The following results correspond to Lemma 4.6.
›

lemma Red_F_of_Red_F_subset: "N'  Red_F N  Red_F N  Red_F (N - N')"
  unfolding Red_F_conv
  by (rule fin_std_red_F.Red_F_of_Red_F_subset)

lemma Red_F_model: "M  N - Red_F N  M  N"
  unfolding Red_F_conv
  by (rule fin_std_red_F.Red_F_model)

lemma Red_F_Bot: "B  Bot  N  {B}  N - Red_F N  {B}"
  unfolding Red_F_conv
  by (rule fin_std_red_F.Red_F_Bot)

end

locale calculus_with_standard_redundancy =
  inference_system Inf + standard_formula_redundancy Bot "(⊨)" "(≺)"
  for
    Inf :: "'f inference set" and
    Bot :: "'f set" and
    entails :: "'f set  'f set  bool" (infix "" 50) and
    less :: "'f  'f  bool" (infix "" 50) +
  assumes
    Inf_has_prem: "ι  Inf  prems_of ι  []" and
    Inf_reductive: "ι  Inf  concl_of ι  main_prem_of ι"
begin

definition redundant_infer :: "'f set  'f inference  bool" where
  "redundant_infer N ι 
   (DD  N. DD  set (side_prems_of ι)  {concl_of ι}  (D  DD. D  main_prem_of ι))"

definition Red_I :: "'f set  'f inference set" where
  "Red_I N = {ι  Inf. redundant_infer N ι}"

text ‹
Compactness of @{term "(⊨)"} implies that @{const Red_I} is equivalent to its finitary counterpart.
›

interpretation fin_std_red: calculus_with_finitary_standard_redundancy Inf Bot "(⊨)"
  using transp_less asymp_on_less wfP_less Inf_has_prem Inf_reductive by unfold_locales

lemma redundant_infer_conv: "redundant_infer = fin_std_red.redundant_infer"
proof (intro ext)
  fix N ι
  show "redundant_infer N ι  fin_std_red.redundant_infer N ι"
    unfolding redundant_infer_def fin_std_red.redundant_infer_def
    using entails_concl_compact_union
    by (smt (verit, ccfv_threshold) finite.emptyI finite_insert subset_eq)
qed

lemma Red_I_conv: "Red_I = fin_std_red.Red_I"
  unfolding Red_I_def fin_std_red.Red_I_def
  unfolding redundant_infer_conv
  by (rule refl)

text ‹
The results from @{locale calculus_with_finitary_standard_redundancy} can now be lifted.

The following results correspond to Lemma 4.6.
›

lemma Red_I_of_subset: "N  N'  Red_I N  Red_I N'"
  unfolding Red_I_conv
  by (rule fin_std_red.Red_I_of_subset)

lemma Red_I_subs_Red_I_diff_Red_F: "Red_I N  Red_I (N - Red_F N)"
  unfolding Red_F_conv Red_I_conv
  by (rule fin_std_red.Red_I_subs_Red_I_diff_Red_F)

lemma Red_I_eq_Red_I_diff_Red_F: "Red_I N = Red_I (N - Red_F N)"
  unfolding Red_F_conv Red_I_conv
  by (rule fin_std_red.Red_I_eq_Red_I_diff_Red_F)

lemma Red_I_to_Inf: "Red_I N  Inf"
  unfolding Red_I_conv
  by (rule fin_std_red.Red_I_to_Inf)

lemma Red_I_of_Red_F_subset: "N'  Red_F N  Red_I N  Red_I (N - N')"
  unfolding Red_F_conv Red_I_conv
  by (rule fin_std_red.Red_I_of_Red_F_subset)

lemma Red_I_of_Inf_to_N:
  "ι  Inf  concl_of ι  N  ι  Red_I N"
  unfolding Red_I_conv
  by (rule fin_std_red.Red_I_of_Inf_to_N)

text ‹
The following corresponds to Theorems 4.7 and 4.8:
›

sublocale calculus Bot Inf "(⊨)" Red_I Red_F
  by (unfold_locales, fact Red_I_to_Inf, fact Red_F_Bot, fact Red_F_of_subset,
      fact Red_I_of_subset, fact Red_F_of_Red_F_subset, fact Red_I_of_Red_F_subset,
      fact Red_I_of_Inf_to_N)

end


subsection ‹Refutational Completeness›

locale calculus_with_standard_inference_redundancy = calculus Bot Inf "(⊨)" Red_I Red_F
  for Bot :: "'f set" and Inf and entails (infix "" 50) and Red_I and Red_F +
  fixes
    less :: "'f  'f  bool" (infix "" 50)
  assumes
    Inf_has_prem: "ι  Inf  prems_of ι  []" and
    Red_I_imp_redundant_infer: "ι  Red_I N 
      (DDN. DD  set (side_prems_of ι)  {concl_of ι}  (CDD. C  main_prem_of ι))"

sublocale calculus_with_finitary_standard_redundancy 
  calculus_with_standard_inference_redundancy Bot Inf "(⊨)" Red_I Red_F
  using Inf_has_prem
  by (unfold_locales) (auto simp: Red_I_def redundant_infer_def)

sublocale calculus_with_standard_redundancy 
  calculus_with_standard_inference_redundancy Bot Inf "(⊨)" Red_I Red_F
  using Inf_has_prem
  by (unfold_locales) (simp_all add: Red_I_def redundant_infer_def)

locale counterex_reducing_calculus_with_standard_inferance_redundancy =
  calculus_with_standard_inference_redundancy Bot Inf "(⊨)" Red_I Red_F "(≺)" +
  counterex_reducing_inference_system Bot "(⊨)" Inf I_of "(≺)"
  for
    Bot :: "'f set" and
    Inf :: "'f inference set" and
    entails :: "'f set  'f set  bool" (infix "" 50) and
    Red_I :: "'f set  'f inference set" and
    Red_F :: "'f set  'f set" and
    I_of :: "'f set  'f set" and
    less :: "'f  'f  bool" (infix "" 50) +
  assumes less_total: "C D. C  D  C  D  D  C"
begin

text ‹
The following result loosely corresponds to Theorem 4.9.
›

lemma saturated_model:
  assumes
    satur: "saturated N" and
    bot_ni_n: "N  Bot = {}"
  shows "I_of N  N"
proof (rule ccontr)
  assume "¬ I_of N  N"
  then obtain D :: 'f where
    d_in_n: "D  N" and
    d_cex: "¬ I_of N  {D}" and
    d_min: "C. C  N  C  D  I_of N  {C}"
    using ex_min_counterex by blast
  then obtain ι :: "'f inference" where
    ι_in: "ι  Inf" and
    ι_mprem: "D = main_prem_of ι" and
    sprem_subs_n: "set (side_prems_of ι)  N" and
    sprem_true: "I_of N  set (side_prems_of ι)" and
    concl_cex: "¬ I_of N  {concl_of ι}" and
    concl_lt_d: "concl_of ι  D"
    using Inf_counterex_reducing[OF bot_ni_n] less_total by metis
  have "ι  Red_I N"
    by (rule subsetD[OF satur[unfolded saturated_def Inf_from_def]],
        simp add: ι_in set_prems_of Inf_has_prem)
      (use ι_mprem d_in_n sprem_subs_n  in blast)
  then have "ι  Red_I N"
    using Red_I_without_red_F by blast
  then obtain DD :: "'f set" where
    dd_subs_n: "DD  N" and
    dd_cc_ent_d: "DD  set (side_prems_of ι)  {concl_of ι}" and
    dd_lt_d: "C  DD. C  D"
    unfolding ι_mprem using Red_I_imp_redundant_infer by meson
  from dd_subs_n dd_lt_d have "I_of N  DD"
    using d_min by (meson ex_min_counterex subset_iff)
  then have "I_of N  {concl_of ι}"
    using entails_trans dd_cc_ent_d entail_union sprem_true by blast
  then show False
    using concl_cex by auto
qed

text ‹
A more faithful abstract version of Theorem 4.9 does not hold without some conditions, according to
Nitpick:
›

corollary saturated_complete:
  assumes
    satur: "saturated N" and
    unsat: "N  Bot"
  shows "N  Bot  {}"
  oops

end

end