Theory Saturation_Framework_Extensions.Standard_Redundancy_Criterion
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_multp⇩D⇩M[OF wfp_imp_asymp[OF wfp_less] transp_less] multp⇩D⇩M_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 ⟹
(∃DD⊆N. DD ∪ set (side_prems_of ι) ⊨ {concl_of ι} ∧ (∀C∈DD. 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