diff --git a/thys/Ordered_Resolution_Prover/Inference_System.thy b/thys/Ordered_Resolution_Prover/Inference_System.thy
--- a/thys/Ordered_Resolution_Prover/Inference_System.thy
+++ b/thys/Ordered_Resolution_Prover/Inference_System.thy
@@ -1,295 +1,291 @@
 (*  Title:       Refutational Inference Systems
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>Refutational Inference Systems\<close>
 
 theory Inference_System
   imports Herbrand_Interpretation
 begin
 
 text \<open>
 This theory gathers results from Section 2.4 (``Refutational Theorem Proving''), 3 (``Standard
 Resolution''), and 4.2 (``Counterexample-Reducing Inference Systems'') of Bachmair and Ganzinger's
 chapter.
 \<close>
 
 
 subsection \<open>Preliminaries\<close>
 
 text \<open>
 Inferences have one distinguished main premise, any number of side premises, and a conclusion.
 \<close>
 
 datatype 'a inference =
   Infer (side_prems_of: "'a clause multiset") (main_prem_of: "'a clause") (concl_of: "'a clause")
 
 abbreviation prems_of :: "'a inference \<Rightarrow> 'a clause multiset" where
   "prems_of \<gamma> \<equiv> side_prems_of \<gamma> + {#main_prem_of \<gamma>#}"
 
 abbreviation concls_of :: "'a inference set \<Rightarrow> 'a clause set" where
   "concls_of \<Gamma> \<equiv> concl_of ` \<Gamma>"
 
-(* FIXME: make an abbreviation *)
 definition infer_from :: "'a clause set \<Rightarrow> 'a inference \<Rightarrow> bool" where
   "infer_from CC \<gamma> \<longleftrightarrow> set_mset (prems_of \<gamma>) \<subseteq> CC"
 
 locale inference_system =
   fixes \<Gamma> :: "'a inference set"
 begin
 
 definition inferences_from :: "'a clause set \<Rightarrow> 'a inference set" where
   "inferences_from CC = {\<gamma>. \<gamma> \<in> \<Gamma> \<and> infer_from CC \<gamma>}"
 
 definition inferences_between :: "'a clause set \<Rightarrow> 'a clause \<Rightarrow> 'a inference set" where
   "inferences_between CC C = {\<gamma>. \<gamma> \<in> \<Gamma> \<and> infer_from (CC \<union> {C}) \<gamma> \<and> C \<in># prems_of \<gamma>}"
 
 lemma inferences_from_mono: "CC \<subseteq> DD \<Longrightarrow> inferences_from CC \<subseteq> inferences_from DD"
   unfolding inferences_from_def infer_from_def by fast
 
 definition saturated :: "'a clause set \<Rightarrow> bool" where
   "saturated N \<longleftrightarrow> concls_of (inferences_from N) \<subseteq> N"
 
 lemma saturatedD:
   assumes
     satur: "saturated N" and
     inf: "Infer CC D E \<in> \<Gamma>" and
     cc_subs_n: "set_mset CC \<subseteq> N" and
     d_in_n: "D \<in> N"
   shows "E \<in> N"
 proof -
   have "Infer CC D E \<in> inferences_from N"
     unfolding inferences_from_def infer_from_def using inf cc_subs_n d_in_n by simp
   then have "E \<in> concls_of (inferences_from N)"
     unfolding image_iff by (metis inference.sel(3))
   then show "E \<in> N"
     using satur unfolding saturated_def by blast
 qed
 
 end
 
 text \<open>
 Satisfiability preservation is a weaker requirement than soundness.
 \<close>
 
 locale sat_preserving_inference_system = inference_system +
   assumes \<Gamma>_sat_preserving: "satisfiable N \<Longrightarrow> satisfiable (N \<union> concls_of (inferences_from N))"
 
 locale sound_inference_system = inference_system +
   assumes \<Gamma>_sound: "Infer CC D E \<in> \<Gamma> \<Longrightarrow> I \<Turnstile>m CC \<Longrightarrow> I \<Turnstile> D \<Longrightarrow> I \<Turnstile> E"
 begin
 
 lemma \<Gamma>_sat_preserving:
   assumes sat_n: "satisfiable N"
   shows "satisfiable (N \<union> concls_of (inferences_from N))"
 proof -
   obtain I where i: "I \<Turnstile>s N"
     using sat_n by blast
   then have "\<And>CC D E. Infer CC D E \<in> \<Gamma> \<Longrightarrow> set_mset CC \<subseteq> N \<Longrightarrow> D \<in> N \<Longrightarrow> I \<Turnstile> E"
     using \<Gamma>_sound unfolding true_clss_def true_cls_mset_def by (simp add: subset_eq)
   then have "\<And>\<gamma>. \<gamma> \<in> \<Gamma> \<Longrightarrow> infer_from N \<gamma> \<Longrightarrow> I \<Turnstile> concl_of \<gamma>"
     unfolding infer_from_def by (case_tac \<gamma>) clarsimp
   then have "I \<Turnstile>s concls_of (inferences_from N)"
     unfolding inferences_from_def image_def true_clss_def infer_from_def by blast
   then have "I \<Turnstile>s N \<union> concls_of (inferences_from N)"
     using i by simp
   then show ?thesis
     by blast
 qed
 
 sublocale sat_preserving_inference_system
   by unfold_locales (erule \<Gamma>_sat_preserving)
 
 end
 
 locale reductive_inference_system = inference_system \<Gamma> for \<Gamma> :: "('a :: wellorder) inference set" +
   assumes \<Gamma>_reductive: "\<gamma> \<in> \<Gamma> \<Longrightarrow> concl_of \<gamma> < main_prem_of \<gamma>"
 
 
 subsection \<open>Refutational Completeness\<close>
 
 text \<open>
 Refutational completeness can be established once and for all for counterexample-reducing inference
 systems. The material formalized here draws from both the general framework of Section 4.2 and the
 concrete instances of Section 3.
 \<close>
 
 locale counterex_reducing_inference_system =
   inference_system \<Gamma> for \<Gamma> :: "('a :: wellorder) inference set" +
   fixes I_of :: "'a clause set \<Rightarrow> 'a interp"
   assumes \<Gamma>_counterex_reducing:
     "{#} \<notin> N \<Longrightarrow> D \<in> N \<Longrightarrow> \<not> I_of N \<Turnstile> D \<Longrightarrow> (\<And>C. C \<in> N \<Longrightarrow> \<not> I_of N \<Turnstile> C \<Longrightarrow> D \<le> C) \<Longrightarrow>
      \<exists>CC E. set_mset CC \<subseteq> N \<and> I_of N \<Turnstile>m CC \<and> Infer CC D E \<in> \<Gamma> \<and> \<not> I_of N \<Turnstile> E \<and> E < D"
 begin
 
 lemma ex_min_counterex:
   fixes N :: "('a :: wellorder) clause set"
   assumes "\<not> I \<Turnstile>s N"
   shows "\<exists>C \<in> N. \<not> I \<Turnstile> C \<and> (\<forall>D \<in> N. D < C \<longrightarrow> I \<Turnstile> D)"
 proof -
   obtain C where "C \<in> N" and "\<not> I \<Turnstile> C"
     using assms unfolding true_clss_def by auto
   then have c_in: "C \<in> {C \<in> N. \<not> I \<Turnstile> C}"
     by blast
   show ?thesis
     using wf_eq_minimal[THEN iffD1, rule_format, OF wf_less_multiset c_in] by blast
 qed
 
 (* Theorem 4.4 (generalizes Theorems 3.9 and 3.16) *)
 
 theorem saturated_model:
   assumes
     satur: "saturated N" and
     ec_ni_n: "{#} \<notin> N"
   shows "I_of N \<Turnstile>s N"
 proof -
-  have ec_ni_n: "{#} \<notin> N"
-    using ec_ni_n by auto
-
   {
     assume "\<not> I_of N \<Turnstile>s N"
     then obtain D where
       d_in_n: "D \<in> N" and
       d_cex: "\<not> I_of N \<Turnstile> D" and
       d_min: "\<And>C. C \<in> N \<Longrightarrow> C < D \<Longrightarrow> I_of N \<Turnstile> C"
       by (meson ex_min_counterex)
     then obtain CC E where
       cc_subs_n: "set_mset CC \<subseteq> N" and
       inf_e: "Infer CC D E \<in> \<Gamma>" and
       e_cex: "\<not> I_of N \<Turnstile> E" and
       e_lt_d: "E < D"
       using \<Gamma>_counterex_reducing[OF ec_ni_n] not_less by metis
     from cc_subs_n inf_e have "E \<in> N"
       using d_in_n satur by (blast dest: saturatedD)
     then have False
       using e_cex e_lt_d d_min not_less by blast
   }
   then show ?thesis
     by satx
 qed
 
 text \<open>
 Cf. Corollary 3.10:
 \<close>
 
 corollary saturated_complete: "saturated N \<Longrightarrow> \<not> satisfiable N \<Longrightarrow> {#} \<in> N"
   using saturated_model by blast
 
 end
 
 
 subsection \<open>Compactness\<close>
 
 text \<open>
 Bachmair and Ganzinger claim that compactness follows from refutational completeness but leave the
 proof to the readers' imagination. Our proof relies on an inductive definition of saturation in
 terms of a base set of clauses.
 \<close>
 
 context inference_system
 begin
 
 inductive_set saturate :: "'a clause set \<Rightarrow> 'a clause set" for CC :: "'a clause set" where
   base: "C \<in> CC \<Longrightarrow> C \<in> saturate CC"
 | step: "Infer CC' D E \<in> \<Gamma> \<Longrightarrow> (\<And>C'. C' \<in># CC' \<Longrightarrow> C' \<in> saturate CC) \<Longrightarrow> D \<in> saturate CC \<Longrightarrow>
     E \<in> saturate CC"
 
 lemma saturate_mono: "C \<in> saturate CC \<Longrightarrow> CC \<subseteq> DD \<Longrightarrow> C \<in> saturate DD"
   by (induct rule: saturate.induct) (auto intro: saturate.intros)
 
 lemma saturated_saturate[simp, intro]: "saturated (saturate N)"
   unfolding saturated_def inferences_from_def infer_from_def image_def
   by clarify (rename_tac x, case_tac x, auto elim!: saturate.step)
 
 lemma saturate_finite: "C \<in> saturate CC \<Longrightarrow> \<exists>DD. DD \<subseteq> CC \<and> finite DD \<and> C \<in> saturate DD"
 proof (induct rule: saturate.induct)
   case (base C)
   then have "{C} \<subseteq> CC" and "finite {C}" and "C \<in> saturate {C}"
     by (auto intro: saturate.intros)
   then show ?case
     by blast
 next
   case (step CC' D E)
   obtain DD_of where
     "\<And>C. C \<in># CC' \<Longrightarrow> DD_of C \<subseteq> CC \<and> finite (DD_of C) \<and> C \<in> saturate (DD_of C)"
     using step(3) by metis
   then have
     "(\<Union>C \<in> set_mset CC'. DD_of C) \<subseteq> CC"
     "finite (\<Union>C \<in> set_mset CC'. DD_of C) \<and> set_mset CC' \<subseteq> saturate (\<Union>C \<in> set_mset CC'. DD_of C)"
     by (auto intro: saturate_mono)
   then obtain DD where
     d_sub: "DD \<subseteq> CC" and d_fin: "finite DD" and in_sat_d: "set_mset CC' \<subseteq> saturate DD"
     by blast
   obtain EE where
     e_sub: "EE \<subseteq> CC" and e_fin: "finite EE" and in_sat_ee: "D \<in> saturate EE"
     using step(5) by blast
   have "DD \<union> EE \<subseteq> CC"
     using d_sub e_sub step(1) by fast
   moreover have "finite (DD \<union> EE)"
     using d_fin e_fin by fast
   moreover have "E \<in> saturate (DD \<union> EE)"
     using in_sat_d in_sat_ee step.hyps(1)
     by (blast intro: inference_system.saturate.step saturate_mono)
   ultimately show ?case
     by blast
 qed
 
 end
 
 context sound_inference_system
 begin
 
 theorem saturate_sound: "C \<in> saturate CC \<Longrightarrow> I \<Turnstile>s CC \<Longrightarrow> I \<Turnstile> C"
   by (induct rule: saturate.induct) (auto simp: true_cls_mset_def true_clss_def \<Gamma>_sound)
 
 end
 
 context sat_preserving_inference_system
 begin
 
 text \<open>
 This result surely holds, but we have yet to prove it. The challenge is: Every time a new clause is
 introduced, we also get a new interpretation (by the definition of
 \<open>sat_preserving_inference_system\<close>). But the interpretation we want here is then the one that
 exists "at the limit". Maybe we can use compactness to prove it.
 \<close>
 
 theorem saturate_sat_preserving: "satisfiable CC \<Longrightarrow> satisfiable (saturate CC)"
   oops
 
 end
 
 locale sound_counterex_reducing_inference_system =
   counterex_reducing_inference_system + sound_inference_system
 begin
 
 text \<open>
 Compactness of clausal logic is stated as Theorem 3.12 for the case of unordered ground resolution.
 The proof below is a generalization to any sound counterexample-reducing inference system. The
 actual theorem will become available once the locale has been instantiated with a concrete inference
 system.
 \<close>
 
 theorem clausal_logic_compact:
   fixes N :: "('a :: wellorder) clause set"
   shows "\<not> satisfiable N \<longleftrightarrow> (\<exists>DD \<subseteq> N. finite DD \<and> \<not> satisfiable DD)"
 proof
   assume "\<not> satisfiable N"
   then have "{#} \<in> saturate N"
     using saturated_complete saturated_saturate saturate.base unfolding true_clss_def by meson
   then have "\<exists>DD \<subseteq> N. finite DD \<and> {#} \<in> saturate DD"
     using saturate_finite by fastforce
   then show "\<exists>DD \<subseteq> N. finite DD \<and> \<not> satisfiable DD"
     using saturate_sound by auto
 next
   assume "\<exists>DD \<subseteq> N. finite DD \<and> \<not> satisfiable DD"
   then show "\<not> satisfiable N"
     by (blast intro: true_clss_mono)
 qed
 
 end
 
 end
diff --git a/thys/Ordered_Resolution_Prover/Standard_Redundancy.thy b/thys/Ordered_Resolution_Prover/Standard_Redundancy.thy
--- a/thys/Ordered_Resolution_Prover/Standard_Redundancy.thy
+++ b/thys/Ordered_Resolution_Prover/Standard_Redundancy.thy
@@ -1,339 +1,339 @@
 (*  Title:       The Standard Redundancy Criterion
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>The Standard Redundancy Criterion\<close>
 
 theory Standard_Redundancy
   imports Proving_Process
 begin
 
 text \<open>
 This material is based on Section 4.2.2 (``The Standard Redundancy Criterion'') of Bachmair and
 Ganzinger's chapter.
 \<close>
 
 locale standard_redundancy_criterion =
   inference_system \<Gamma> for \<Gamma> :: "('a :: wellorder) inference set"
 begin
 
 definition redundant_infer :: "'a clause set \<Rightarrow> 'a inference \<Rightarrow> bool" where
   "redundant_infer N \<gamma> \<longleftrightarrow>
    (\<exists>DD. set_mset DD \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD + side_prems_of \<gamma> \<longrightarrow> I \<Turnstile> concl_of \<gamma>)
       \<and> (\<forall>D. D \<in># DD \<longrightarrow> D < main_prem_of \<gamma>))"
 
 definition Rf :: "'a clause set \<Rightarrow> 'a clause set" where
   "Rf N = {C. \<exists>DD. set_mset DD \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD \<longrightarrow> I \<Turnstile> C) \<and> (\<forall>D. D \<in># DD \<longrightarrow> D < C)}"
 
 definition Ri :: "'a clause set \<Rightarrow> 'a inference set" where
   "Ri N = {\<gamma> \<in> \<Gamma>. redundant_infer N \<gamma>}"
 
 lemma tautology_Rf:
   assumes "Pos A \<in># C"
   assumes "Neg A \<in># C"
   shows "C \<in> Rf N"
 proof -
   have "set_mset {#} \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m {#} \<longrightarrow> I \<Turnstile> C) \<and> (\<forall>D. D \<in># {#} \<longrightarrow> D < C)"
     using assms by auto
   then show "C \<in> Rf N"
     unfolding Rf_def by blast
 qed
 
 lemma tautology_redundant_infer:
   assumes
     pos: "Pos A \<in># concl_of \<iota>" and
     neg: "Neg A \<in># concl_of \<iota>"
   shows "redundant_infer N \<iota>"
   by (metis empty_iff empty_subsetI neg pos pos_neg_in_imp_true redundant_infer_def set_mset_empty)
 
 lemma contradiction_Rf: "{#} \<in> N \<Longrightarrow> Rf N = UNIV - {{#}}"
   unfolding Rf_def by force
 
 text \<open>
 The following results correspond to Lemma 4.5. The lemma \<open>wlog_non_Rf\<close> generalizes the core of
 the argument.
 \<close>
 
 lemma Rf_mono: "N \<subseteq> N' \<Longrightarrow> Rf N \<subseteq> Rf N'"
   unfolding Rf_def by auto
 
 lemma wlog_non_Rf:
   assumes ex: "\<exists>DD. set_mset DD \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E) \<and> (\<forall>D'. D' \<in># DD \<longrightarrow> D' < D)"
   shows "\<exists>DD. set_mset DD \<subseteq> N - Rf N \<and> (\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E) \<and> (\<forall>D'. D' \<in># DD \<longrightarrow> D' < D)"
 proof -
   from ex obtain DD0 where
     dd0: "DD0 \<in> {DD. set_mset DD \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E) \<and> (\<forall>D'. D' \<in># DD \<longrightarrow> D' < D)}"
     by blast
   have "\<exists>DD. set_mset DD \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E) \<and> (\<forall>D'. D' \<in># DD \<longrightarrow> D' < D) \<and>
       (\<forall>DD'. set_mset DD' \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD' + CC \<longrightarrow> I \<Turnstile> E) \<and> (\<forall>D'. D' \<in># DD' \<longrightarrow> D' < D) \<longrightarrow>
     DD \<le> DD')"
     using wf_eq_minimal[THEN iffD1, rule_format, OF wf_less_multiset dd0]
     unfolding not_le[symmetric] by blast
   then obtain DD where
     dd_subs_n: "set_mset DD \<subseteq> N" and
     ddcc_imp_e: "\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E" and
     dd_lt_d: "\<forall>D'. D' \<in># DD \<longrightarrow> D' < D" and
     d_min: "\<forall>DD'. set_mset DD' \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD' + CC \<longrightarrow> I \<Turnstile> E) \<and> (\<forall>D'. D' \<in># DD' \<longrightarrow> D' < D) \<longrightarrow>
       DD \<le> DD'"
     by blast
 
   have "\<forall>Da. Da \<in># DD \<longrightarrow> Da \<notin> Rf N"
   proof clarify
     fix Da
     assume
       da_in_dd: "Da \<in># DD" and
       da_rf: "Da \<in> Rf N"
 
     from da_rf obtain DD' where
       dd'_subs_n: "set_mset DD' \<subseteq> N" and
       dd'_imp_da: "\<forall>I. I \<Turnstile>m DD' \<longrightarrow> I \<Turnstile> Da" and
       dd'_lt_da: "\<forall>D'. D' \<in># DD' \<longrightarrow> D' < Da"
       unfolding Rf_def by blast
 
     define DDa where
       "DDa = DD - {#Da#} + DD'"
 
     have "set_mset DDa \<subseteq> N"
       unfolding DDa_def using dd_subs_n dd'_subs_n
       by (meson contra_subsetD in_diffD subsetI union_iff)
     moreover have "\<forall>I. I \<Turnstile>m DDa + CC \<longrightarrow> I \<Turnstile> E"
       using dd'_imp_da ddcc_imp_e da_in_dd unfolding DDa_def true_cls_mset_def
       by (metis in_remove1_mset_neq union_iff)
     moreover have "\<forall>D'. D' \<in># DDa \<longrightarrow> D' < D"
       using dd_lt_d dd'_lt_da da_in_dd unfolding DDa_def
       by (metis insert_DiffM2 order.strict_trans union_iff)
     moreover have "DDa < DD"
       unfolding DDa_def
       by (meson da_in_dd dd'_lt_da mset_lt_single_right_iff single_subset_iff union_le_diff_plus)
     ultimately show False
       using d_min unfolding less_eq_multiset_def by (auto intro!: antisym)
   qed
   then show ?thesis
     using dd_subs_n ddcc_imp_e dd_lt_d by auto
 qed
 
 lemma Rf_imp_ex_non_Rf:
   assumes "C \<in> Rf N"
   shows "\<exists>CC. set_mset CC \<subseteq> N - Rf N \<and> (\<forall>I. I \<Turnstile>m CC \<longrightarrow> I \<Turnstile> C) \<and> (\<forall>C'. C' \<in># CC \<longrightarrow> C' < C)"
   using assms by (auto simp: Rf_def intro: wlog_non_Rf[of _ "{#}", simplified])
 
 lemma Rf_subs_Rf_diff_Rf: "Rf N \<subseteq> Rf (N - Rf N)"
 proof
   fix C
   assume c_rf: "C \<in> Rf N"
   then obtain CC where
     cc_subs: "set_mset CC \<subseteq> N - Rf N" and
     cc_imp_c: "\<forall>I. I \<Turnstile>m CC \<longrightarrow> I \<Turnstile> C" and
     cc_lt_c: "\<forall>C'. C' \<in># CC \<longrightarrow> C' < C"
     using Rf_imp_ex_non_Rf by blast
   have "\<forall>D. D \<in># CC \<longrightarrow> D \<notin> Rf N"
     using cc_subs by (simp add: subset_iff)
   then have cc_nr:
-    "\<And>C DD. C \<in># CC \<Longrightarrow> set_mset DD \<subseteq> N \<Longrightarrow> \<forall>I. I \<Turnstile>m DD \<longrightarrow> I \<Turnstile> C \<Longrightarrow> \<exists>D. D \<in># DD \<and> ~ D < C"
+    "\<And>C DD. C \<in># CC \<Longrightarrow> set_mset DD \<subseteq> N \<Longrightarrow> \<forall>I. I \<Turnstile>m DD \<longrightarrow> I \<Turnstile> C \<Longrightarrow> \<exists>D. D \<in># DD \<and> \<not> D < C"
       unfolding Rf_def by auto metis
   have "set_mset CC \<subseteq> N"
     using cc_subs by auto
   then have "set_mset CC \<subseteq>
     N - {C. \<exists>DD. set_mset DD \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD \<longrightarrow> I \<Turnstile> C) \<and> (\<forall>D. D \<in># DD \<longrightarrow> D < C)}"
     using cc_nr by auto
   then show "C \<in> Rf (N - Rf N)"
     using cc_imp_c cc_lt_c unfolding Rf_def by auto
 qed
 
 lemma Rf_eq_Rf_diff_Rf: "Rf N = Rf (N - Rf N)"
   by (metis Diff_subset Rf_mono Rf_subs_Rf_diff_Rf subset_antisym)
 
 text \<open>
 The following results correspond to Lemma 4.6.
 \<close>
 
 lemma Ri_mono: "N \<subseteq> N' \<Longrightarrow> Ri N \<subseteq> Ri N'"
   unfolding Ri_def redundant_infer_def by auto
 
 lemma Ri_subs_Ri_diff_Rf: "Ri N \<subseteq> Ri (N - Rf N)"
 proof
   fix \<gamma>
   assume \<gamma>_ri: "\<gamma> \<in> Ri N"
   then obtain CC D E where \<gamma>: "\<gamma> = Infer CC D E"
     by (cases \<gamma>)
   have cc: "CC = side_prems_of \<gamma>" and d: "D = main_prem_of \<gamma>" and e: "E = concl_of \<gamma>"
     unfolding \<gamma> by simp_all
   obtain DD where
     "set_mset DD \<subseteq> N" and "\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E" and "\<forall>C. C \<in># DD \<longrightarrow> C < D"
     using \<gamma>_ri unfolding Ri_def redundant_infer_def cc d e by blast
   then obtain DD' where
     "set_mset DD' \<subseteq> N - Rf N" and "\<forall>I. I \<Turnstile>m DD' + CC \<longrightarrow> I \<Turnstile> E" and "\<forall>D'. D' \<in># DD' \<longrightarrow> D' < D"
     using wlog_non_Rf by atomize_elim blast
   then show "\<gamma> \<in> Ri (N - Rf N)"
     using \<gamma>_ri unfolding Ri_def redundant_infer_def d cc e by blast
 qed
 
 lemma Ri_eq_Ri_diff_Rf: "Ri N = Ri (N - Rf N)"
   by (metis Diff_subset Ri_mono Ri_subs_Ri_diff_Rf subset_antisym)
 
 lemma Ri_subset_\<Gamma>: "Ri N \<subseteq> \<Gamma>"
   unfolding Ri_def by blast
 
 lemma Rf_indep: "N' \<subseteq> Rf N \<Longrightarrow> Rf N \<subseteq> Rf (N - N')"
   by (metis Diff_cancel Diff_eq_empty_iff Diff_mono Rf_eq_Rf_diff_Rf Rf_mono)
 
 lemma Ri_indep: "N' \<subseteq> Rf N \<Longrightarrow> Ri N \<subseteq> Ri (N - N')"
   by (metis Diff_mono Ri_eq_Ri_diff_Rf Ri_mono order_refl)
 
 lemma Rf_model:
   assumes "I \<Turnstile>s N - Rf N"
   shows "I \<Turnstile>s N"
 proof -
   have "I \<Turnstile>s Rf (N - Rf N)"
     unfolding true_clss_def
     by (subst Rf_def, simp add: true_cls_mset_def, metis assms subset_eq true_clss_def)
   then have "I \<Turnstile>s Rf N"
     using Rf_subs_Rf_diff_Rf true_clss_mono by blast
   then show ?thesis
     using assms by (metis Un_Diff_cancel true_clss_union)
 qed
 
 lemma Rf_sat: "satisfiable (N - Rf N) \<Longrightarrow> satisfiable N"
   by (metis Rf_model)
 
 text \<open>
 The following corresponds to Theorem 4.7:
 \<close>
 
 sublocale redundancy_criterion \<Gamma> Rf Ri
   by unfold_locales (rule Ri_subset_\<Gamma>, (elim Rf_mono Ri_mono Rf_indep Ri_indep Rf_sat)+)
 
 end
 
 locale standard_redundancy_criterion_reductive =
   standard_redundancy_criterion + reductive_inference_system
 begin
 
 text \<open>
 The following corresponds to Theorem 4.8:
 \<close>
 
 lemma Ri_effective:
   assumes
     in_\<gamma>: "\<gamma> \<in> \<Gamma>" and
     concl_of_in_n_un_rf_n: "concl_of \<gamma> \<in> N \<union> Rf N"
   shows "\<gamma> \<in> Ri N"
 proof -
   obtain CC D E where
     \<gamma>: "\<gamma> = Infer CC D E"
     by (cases \<gamma>)
   then have cc: "CC = side_prems_of \<gamma>" and d: "D = main_prem_of \<gamma>" and e: "E = concl_of \<gamma>"
     unfolding \<gamma> by simp_all
   note e_in_n_un_rf_n = concl_of_in_n_un_rf_n[folded e]
 
   {
     assume "E \<in> N"
     moreover have "E < D"
       using \<Gamma>_reductive e d in_\<gamma> by auto
     ultimately have
       "set_mset {#E#} \<subseteq> N" and "\<forall>I. I \<Turnstile>m {#E#} + CC \<longrightarrow> I \<Turnstile> E" and "\<forall>D'. D' \<in># {#E#} \<longrightarrow> D' < D"
       by simp_all
     then have "redundant_infer N \<gamma>"
       using redundant_infer_def cc d e by blast
   }
   moreover
   {
     assume "E \<in> Rf N"
     then obtain DD where
       dd_sset: "set_mset DD \<subseteq> N" and
       dd_imp_e: "\<forall>I. I \<Turnstile>m DD \<longrightarrow> I \<Turnstile> E" and
       dd_lt_e: "\<forall>C'. C' \<in># DD \<longrightarrow> C' < E"
       unfolding Rf_def by blast
     from dd_lt_e have "\<forall>Da. Da \<in># DD \<longrightarrow> Da < D"
       using d e in_\<gamma> \<Gamma>_reductive less_trans by blast
     then have "redundant_infer N \<gamma>"
       using redundant_infer_def dd_sset dd_imp_e cc d e by blast
   }
   ultimately show "\<gamma> \<in> Ri N"
     using in_\<gamma> e_in_n_un_rf_n unfolding Ri_def by blast
 qed
 
 sublocale effective_redundancy_criterion \<Gamma> Rf Ri
   unfolding effective_redundancy_criterion_def
   by (intro conjI redundancy_criterion_axioms, unfold_locales, rule Ri_effective)
 
 lemma contradiction_Rf: "{#} \<in> N \<Longrightarrow> Ri N = \<Gamma>"
   unfolding Ri_def redundant_infer_def using \<Gamma>_reductive le_multiset_empty_right
   by (force intro: exI[of _ "{#{#}#}"] le_multiset_empty_left)
 
 end
 
 locale standard_redundancy_criterion_counterex_reducing =
   standard_redundancy_criterion + counterex_reducing_inference_system
 begin
 
 text \<open>
 The following result corresponds to Theorem 4.9.
 \<close>
 
 lemma saturated_upto_complete_if:
   assumes
     satur: "saturated_upto N" and
     unsat: "\<not> satisfiable N"
   shows "{#} \<in> N"
 proof (rule ccontr)
   assume ec_ni_n: "{#} \<notin> N"
 
   define M where
     "M = N - Rf N"
 
   have ec_ni_m: "{#} \<notin> M"
     unfolding M_def using ec_ni_n by fast
 
   have "I_of M \<Turnstile>s M"
   proof (rule ccontr)
     assume "\<not> I_of M \<Turnstile>s M"
     then obtain D where
       d_in_m: "D \<in> M" and
       d_cex: "\<not> I_of M \<Turnstile> D" and
       d_min: "\<And>C. C \<in> M \<Longrightarrow> C < D \<Longrightarrow> I_of M \<Turnstile> C"
       using ex_min_counterex by meson
     then obtain \<gamma> CC E where
       \<gamma>: "\<gamma> = Infer CC D E" and
       cc_subs_m: "set_mset CC \<subseteq> M" and
       cc_true: "I_of M \<Turnstile>m CC" and
       \<gamma>_in: "\<gamma> \<in> \<Gamma>" and
       e_cex: "\<not> I_of M \<Turnstile> E" and
       e_lt_d: "E < D"
       using \<Gamma>_counterex_reducing[OF ec_ni_m] not_less by metis
     have cc: "CC = side_prems_of \<gamma>" and d: "D = main_prem_of \<gamma>" and e: "E = concl_of \<gamma>"
       unfolding \<gamma> by simp_all
     have "\<gamma> \<in> Ri N"
       by (rule subsetD[OF satur[unfolded saturated_upto_def inferences_from_def infer_from_def]])
         (simp add: \<gamma>_in d_in_m cc_subs_m cc[symmetric] d[symmetric] M_def[symmetric])
     then have "\<gamma> \<in> Ri M"
       unfolding M_def using Ri_indep by fast
     then obtain DD where
       dd_subs_m: "set_mset DD \<subseteq> M" and
       dd_cc_imp_d: "\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E" and
       dd_lt_d: "\<forall>C. C \<in># DD \<longrightarrow> C < D"
       unfolding Ri_def redundant_infer_def cc d e by blast
     from dd_subs_m dd_lt_d have "I_of M \<Turnstile>m DD"
       using d_min unfolding true_cls_mset_def by (metis contra_subsetD)
     then have "I_of M \<Turnstile> E"
       using dd_cc_imp_d cc_true by auto
     then show False
       using e_cex by auto
   qed
   then have "I_of M \<Turnstile>s N"
     using M_def Rf_model by blast
   then show False
     using unsat by blast
 qed
 
 theorem saturated_upto_complete:
   assumes "saturated_upto N"
   shows "\<not> satisfiable N \<longleftrightarrow> {#} \<in> N"
   using assms saturated_upto_complete_if true_clss_def by auto
 
 end
 
 end