diff --git a/thys/Saturation_Framework_Extensions/Clausal_Calculus.thy b/thys/Saturation_Framework_Extensions/Clausal_Calculus.thy --- a/thys/Saturation_Framework_Extensions/Clausal_Calculus.thy +++ b/thys/Saturation_Framework_Extensions/Clausal_Calculus.thy @@ -1,210 +1,192 @@ (* Title: Clausal Calculi Author: Jasmin Blanchette , 2020 *) section \Clausal Calculi\ theory Clausal_Calculus imports Ordered_Resolution_Prover.Unordered_Ground_Resolution - Consistency_Preservation + Soundness Standard_Redundancy_Criterion begin text \Various results about consequence relations, counterexample-reducing inference systems, and the standard redundancy criteria are specialized and customized for clauses as opposed to arbitrary formulas.\ subsection \Setup\ text \To avoid confusion, we use the symbol \\\ (with or without subscripts) for the ``models'' and entailment relations on clauses and \\\ for the abstract concept of consequence.\ abbreviation true_lit_thick :: "'a interp \ 'a literal \ bool" (infix "\l" 50) where "I \l L \ I \l L" abbreviation true_cls_thick :: "'a interp \ 'a clause \ bool" (infix "\" 50) where "I \ C \ I \ C" abbreviation true_clss_thick :: "'a interp \ 'a clause set \ bool" (infix "\s" 50) where "I \s \ \ I \s \" abbreviation true_cls_mset_thick :: "'a interp \ 'a clause multiset \ bool" (infix "\m" 50) where "I \m \ \ I \m \" no_notation true_lit (infix "\l" 50) no_notation true_cls (infix "\" 50) no_notation true_clss (infix "\s" 50) no_notation true_cls_mset (infix "\m" 50) subsection \Consequence Relation\ abbreviation entails_clss :: "'a clause set \ 'a clause set \ bool" (infix "\e" 50) where "N1 \e N2 \ \I. I \s N1 \ I \s N2" lemma entails_iff_unsatisfiable_single: "CC \e {E} \ \ satisfiable (CC \ {{#- L#} |L. L \# E})" (is "_ \ _ (_ \ ?NegD)") proof assume c_ent_e: "CC \e {E}" have "\ I \s CC \ ?NegD" for I using c_ent_e[rule_format, of I] unfolding true_clss_def true_cls_def true_lit_def if_distribR if_bool_eq_conj by (fastforce simp: ball_Un is_pos_neg_not_is_pos) then show "\ satisfiable (CC \ ?NegD)" by auto next assume "\ satisfiable (CC \ ?NegD)" then have "\ I \s CC \ ?NegD" for I by auto then show "CC \e {E}" unfolding true_clss_def true_cls_def true_lit_def if_distribR if_bool_eq_conj by (fastforce simp: ball_Un is_pos_neg_not_is_pos) qed lemma entails_iff_unsatisfiable: "CC \e EE \ (\E \ EE. \ satisfiable (CC \ {{#- L#} |L. L \# E}))" (is "?lhs = ?rhs") proof - have "?lhs \ (\E \ EE. CC \e {E})" unfolding true_clss_def by auto also have "... \ ?rhs" unfolding entails_iff_unsatisfiable_single by auto finally show ?thesis . qed interpretation consequence_relation "{{#}}" "(\e)" proof fix N2 N1 :: "'a clause set" assume "\C \ N2. N1 \e {C}" then show "N1 \e N2" unfolding true_clss_singleton by (simp add: true_clss_def) qed (auto intro: true_clss_mono) interpretation compact_consequence_relation "{{#}} :: ('a :: wellorder) clause set" "(\e)" by unfold_locales (use clausal_logic_compact in auto) interpretation concl_compact_consequence_relation "{{#}} :: ('a :: wellorder) clause set" "(\e)" proof fix CC EE :: "'a clause set" assume fin_e: "finite EE" and c_ent_e: "CC \e EE" have "\E \ EE. \ satisfiable (CC \ {{#- L#} |L. L \# E})" using c_ent_e[unfolded entails_iff_unsatisfiable] . then have "\E \ EE. \DD \ CC \ {{#- L#} |L. L \# E}. finite DD \ \ satisfiable DD" by (subst (asm) clausal_logic_compact) then obtain DD_of where d_of: "\E \ EE. DD_of E \ CC \ {{#- L#} |L. L \# E} \ finite (DD_of E) \ \ satisfiable (DD_of E)" by moura define CC' where "CC' = (\E \ EE. DD_of E - {{#- L#} |L. L \# E})" have "CC' \ CC" unfolding CC'_def using d_of by auto moreover have c'_fin: "finite CC'" unfolding CC'_def using d_of fin_e by blast moreover have "CC' \e EE" unfolding entails_iff_unsatisfiable proof fix E assume e_in: "E \ EE" have "DD_of E \ CC' \ {{#- L#} |L. L \# E}" using e_in d_of unfolding CC'_def by auto moreover have "\ satisfiable (DD_of E)" using e_in d_of by auto ultimately show "\ satisfiable (CC' \ {{#- L#} |L. L \# E})" by (rule unsatisfiable_mono[of "DD_of E"]) qed ultimately show "\CC' \ CC. finite CC' \ CC' \e EE" by blast qed subsection \Counterexample-Reducing Inference Systems\ definition clss_of_interp :: "'a set \ 'a literal multiset set" where "clss_of_interp I = {{#(if A \ I then Pos else Neg) A#} |A. True}" lemma true_clss_of_interp_iff_equal[simp]: "J \s clss_of_interp I \ J = I" unfolding clss_of_interp_def true_clss_def true_cls_def true_lit_def by force lemma entails_iff_models[simp]: "clss_of_interp I \e CC \ I \s CC" by simp locale clausal_counterex_reducing_inference_system = inference_system Inf for Inf :: "('a :: wellorder) clause inference set" + - fixes clausal_I_of :: "'a clause set \ 'a interp" + fixes J_of :: "'a clause set \ 'a interp" assumes clausal_Inf_counterex_reducing: - "{#} \ N \ D \ N \ \ clausal_I_of N \ D \ - (\C. C \ N \ \ clausal_I_of N \ C \ D \ C) \ - \Cs E. set Cs \ N \ clausal_I_of N \s set Cs \ Infer (Cs @ [D]) E \ Inf - \ \ clausal_I_of N \ E \ E < D" + "{#} \ N \ D \ N \ \ J_of N \ D \ (\C. C \ N \ \ J_of N \ C \ D \ C) \ + \\ \ Inf. prems_of \ \ [] \ main_prem_of \ = D \ set (side_prems_of \) \ N \ + J_of N \s set (side_prems_of \) \ \ J_of N \ concl_of \ \ concl_of \ < D" begin abbreviation I_of :: "'a clause set \ 'a clause set" where - "I_of N \ clss_of_interp (clausal_I_of N)" + "I_of N \ clss_of_interp (J_of N)" lemma Inf_counterex_reducing: assumes bot_ni_n: "N \ {{#}} = {}" and d_in_n: "D \ N" and n_ent_d: "\ I_of N \e {D}" and d_min: "\C. C \ N \ \ I_of N \e {C} \ D \ C" shows "\\ \ Inf. prems_of \ \ [] \ main_prem_of \ = D \ set (side_prems_of \) \ N - \ I_of N \e set (side_prems_of \) \ \ I_of N \e {concl_of \} \ concl_of \ < D" -proof - - have "{#} \ N" - using bot_ni_n by auto - moreover note d_in_n - moreover have "\ clausal_I_of N \ D" - using n_ent_d by simp - moreover have "C \ N \ \ clausal_I_of N \ C \ D \ C" for C - using d_min[of C] by simp - ultimately obtain Cs E where - "set Cs \ N" and - "clausal_I_of N \s set Cs" and - "Infer (Cs @ [D]) E \ Inf" and - "\ clausal_I_of N \ E" and - "E < D" - using clausal_Inf_counterex_reducing by metis - then show ?thesis - using snoc_eq_iff_butlast by fastforce -qed + \ I_of N \e set (side_prems_of \) \ \ I_of N \e {concl_of \} \ concl_of \ < D" + using bot_ni_n clausal_Inf_counterex_reducing d_in_n d_min n_ent_d by auto sublocale counterex_reducing_inference_system "{{#}}" "(\e)" Inf I_of by unfold_locales (fact Inf_counterex_reducing) end subsection \Counterexample-Reducing Calculi Equipped with a Standard Redundancy Criterion\ locale clausal_counterex_reducing_calculus_with_standard_redundancy = calculus_with_standard_redundancy Inf "{{#}}" "(\e)" + - clausal_counterex_reducing_inference_system Inf clausal_I_of + clausal_counterex_reducing_inference_system Inf J_of for Inf :: "('a :: wellorder) clause inference set" and - clausal_I_of :: "'a clause set \ 'a set" + J_of :: "'a clause set \ 'a set" begin sublocale counterex_reducing_calculus_with_standard_redundancy "{{#}}" "(\e)" I_of by unfold_locales sublocale refutationally_compact_calculus "{{#}}" Inf "(\e)" Red_I Red_F by unfold_locales -lemma clausal_saturated_model: "saturated N \ {#} \ N \ clausal_I_of N \s N" +lemma clausal_saturated_model: "saturated N \ {#} \ N \ J_of N \s N" by (simp add: saturated_model[simplified]) corollary clausal_saturated_complete: "saturated N \ (\I. \ I \s N) \ {#} \ N" using clausal_saturated_model by blast end end diff --git a/thys/Saturation_Framework_Extensions/Consistency_Preservation.thy b/thys/Saturation_Framework_Extensions/Consistency_Preservation.thy deleted file mode 100644 --- a/thys/Saturation_Framework_Extensions/Consistency_Preservation.thy +++ /dev/null @@ -1,177 +0,0 @@ -(* Title: Consistency Preservation - Author: Jasmin Blanchette , 2014, 2017, 2020 - Author: Dmitriy Traytel , 2014 - Author: Anders Schlichtkrull , 2017 -*) - -section \Consistency Preservation\ - -theory Consistency_Preservation - imports - Saturation_Framework.Calculus -begin - -text \ -Assuming compactness of the consequence relation, the limit of a derivation based on a redundancy -criterion is satisfiable if and only if the initial set is satisfiable. This material is partly -based on Section 4.1 of Bachmair and Ganzinger's \emph{Handbook} chapter, but adapted to the -saturation framework of Waldmann et al. -\ - -locale compact_consequence_relation = consequence_relation + - assumes - entails_compact: "CC \ Bot \ \CC' \ CC. finite CC' \ CC' \ Bot" -begin - -lemma chain_entails_derive_consist_preserving: - assumes - ent: "chain (\) Ns" and - n0_sat: "\ lhd Ns \ Bot" - shows "\ Sup_llist Ns \ Bot" -proof - - have bot_sat: "\ {} \ Bot" - using n0_sat by (meson empty_subsetI entails_trans subset_entailed) - - { - fix DD - assume fin: "finite DD" and sset_lun: "DD \ Sup_llist Ns" - then obtain k where - dd_sset: "DD \ Sup_upto_llist Ns (enat k)" - using finite_Sup_llist_imp_Sup_upto_llist by blast - have "\ Sup_upto_llist Ns (enat k) \ Bot" - proof (induct k) - case 0 - then show ?case - unfolding Sup_upto_llist_def - using lhd_conv_lnth[OF chain_not_lnull[OF ent], symmetric] n0_sat bot_sat by auto - next - case (Suc k) - show ?case - proof (cases "enat (Suc k) \ llength Ns") - case True - then have "Sup_upto_llist Ns (enat k) = Sup_upto_llist Ns (enat (Suc k))" - unfolding Sup_upto_llist_def using le_Suc_eq by auto - then show ?thesis - using Suc by simp - next - case False - then have entail_succ: "lnth Ns k \ lnth Ns (Suc k)" - using ent chain_lnth_rel by fastforce - from False have lt: "enat (Suc k) < llength Ns \ enat k < llength Ns" - by (meson Suc_ile_eq le_cases not_le) - have "{i. enat i < llength Ns \ i \ Suc k} = - {i. enat i < llength Ns \ i \ k} \ {i. enat i < llength Ns \ i = Suc k}" by auto - then have "Sup_upto_llist Ns (enat (Suc k)) = - Sup_upto_llist Ns (enat k) \ lnth Ns (Suc k)" - using lt unfolding Sup_upto_llist_def enat_ord_code(1) by blast - moreover have "Sup_upto_llist Ns k \ lnth Ns (Suc k)" - using entail_succ subset_entailed [of "lnth Ns k" "Sup_upto_llist Ns k"] lt - unfolding Sup_upto_llist_def by (simp add: entail_succ UN_upper entails_trans) - ultimately have "Sup_upto_llist Ns k \ Sup_upto_llist Ns (Suc k)" - using entail_union subset_entailed by fastforce - then show ?thesis using Suc.hyps using entails_trans by blast - qed - qed - then have "\ DD \ Bot" - using dd_sset entails_trans subset_entailed unfolding Sup_upto_llist_def by blast - } - then show ?thesis - using entails_compact by auto -qed - -end - -locale refutationally_compact_calculus = calculus + compact_consequence_relation -begin - -text \ -This corresponds to Lemma 4.2: -\ - -lemma - assumes chain_red: "chain (\Red) Ns" - shows - Red_F_Sup_subset_Red_F_Liminf: "Red_F (Sup_llist Ns) \ Red_F (Liminf_llist Ns)" and - Red_I_Sup_subset_Red_I_Liminf: "Red_I (Sup_llist Ns) \ Red_I (Liminf_llist Ns)" and - unsat_limit_iff: "chain (\) Ns \ Liminf_llist Ns \ Bot \ lhd Ns \ Bot" -proof - - { - fix C i j - assume - c_in: "C \ lnth Ns i" and - c_ni: "C \ Red_F (Sup_llist Ns)" and - j: "j \ i" and - j': "enat j < llength Ns" - from c_ni have c_ni': "\i. enat i < llength Ns \ C \ Red_F (lnth Ns i)" - using Red_F_of_subset lnth_subset_Sup_llist by (metis subsetD) - have "C \ lnth Ns j" - using j j' - proof (induct j) - case 0 - then show ?case - using c_in by blast - next - case (Suc k) - then show ?case - proof (cases "i < Suc k") - case True - have "i \ k" - using True by linarith - moreover have "enat k < llength Ns" - using Suc.prems(2) Suc_ile_eq by (blast intro: dual_order.strict_implies_order) - ultimately have "C \ lnth Ns k" - using Suc.hyps by blast - moreover have "lnth Ns k \Red lnth Ns (Suc k)" - using Suc.prems(2) chain_lnth_rel chain_red by blast - ultimately show ?thesis - by (meson DiffI Suc.prems(2) c_ni' derive.cases subset_eq) - qed (use Suc c_in in auto) - qed - } - then have lu_ll: "Sup_llist Ns - Red_F (Sup_llist Ns) \ Liminf_llist Ns" - unfolding Sup_llist_def Liminf_llist_def by blast - - have "Red_F (Sup_llist Ns - Red_F (Sup_llist Ns)) \ Red_F (Liminf_llist Ns)" - using lu_ll by (simp add: Red_F_of_subset) - then show "Red_F (Sup_llist Ns) \ Red_F (Liminf_llist Ns)" - using Red_F_of_Red_F_subset by auto - - have "Red_I (Sup_llist Ns - Red_F (Sup_llist Ns)) \ Red_I (Liminf_llist Ns)" - using lu_ll by (simp add: Red_I_of_subset) - then show "Red_I (Sup_llist Ns) \ Red_I (Liminf_llist Ns)" - using Red_I_without_red_F by auto - - { - assume ent: "chain (\) Ns" - show "Liminf_llist Ns \ Bot \ lhd Ns \ Bot" - proof - assume "Liminf_llist Ns \ Bot" - then have "Sup_llist Ns \ Bot" - using Liminf_llist_subset_Sup_llist by (metis entails_trans subset_entailed) - then show "lhd Ns \ Bot" - using ent chain_entails_derive_consist_preserving by blast - next - assume "lhd Ns \ Bot" - then have "Sup_llist Ns \ Bot" - by (meson ent chain_not_lnull entails_trans lhd_subset_Sup_llist subset_entailed) - then have "Sup_llist Ns - Red_F (Sup_llist Ns) \ Bot" - using Red_F_Bot entail_set_all_formulas by blast - then show "Liminf_llist Ns \ Bot" - using entails_trans lu_ll subset_entailed by blast - qed - } -qed - -lemma - assumes "chain (\Red) Ns" - shows - Red_F_limit_Sup: "Red_F (Liminf_llist Ns) = Red_F (Sup_llist Ns)" and - Red_I_limit_Sup: "Red_I (Liminf_llist Ns) = Red_I (Sup_llist Ns)" - by (metis assms Liminf_llist_subset_Sup_llist Red_F_of_Red_F_subset Red_F_of_subset Red_in_Sup - double_diff order_refl subset_antisym) - (metis assms Liminf_llist_subset_Sup_llist Red_I_of_Red_F_subset Red_I_of_subset Red_in_Sup - double_diff order_refl subset_antisym) - -end - -end diff --git a/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy b/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy --- a/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy +++ b/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy @@ -1,1135 +1,1151 @@ (* Title: Application of the Saturation Framework to Bachmair and Ganzinger's RP Author: Sophie Tourret , 2018-2020 Author: Jasmin Blanchette , 2020 *) section \Application of the Saturation Framework to Bachmair and Ganzinger's \textsf{RP}\ theory FO_Ordered_Resolution_Prover_Revisited imports Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover Saturation_Framework.Given_Clause_Architectures Clausal_Calculus Soundness begin text \The main results about Bachmair and Ganzinger's \textsf{RP} prover, as established in Section 4.3 of their \emph{Handbook} chapter and formalized by Schlichtkrull et al., are re-proved here using the saturation framework of Waldmann et al.\ subsection \Setup\ no_notation true_lit (infix "\l" 50) no_notation true_cls (infix "\" 50) no_notation true_clss (infix "\s" 50) no_notation true_cls_mset (infix "\m" 50) hide_type (open) Inference_System.inference hide_const (open) Inference_System.Infer Inference_System.main_prem_of Inference_System.side_prems_of Inference_System.prems_of Inference_System.concl_of Inference_System.concls_of Inference_System.infer_from type_synonym 'a old_inference = "'a Inference_System.inference" abbreviation "old_Infer \ Inference_System.Infer" abbreviation "old_side_prems_of \ Inference_System.side_prems_of" abbreviation "old_main_prem_of \ Inference_System.main_prem_of" abbreviation "old_concl_of \ Inference_System.concl_of" abbreviation "old_prems_of \ Inference_System.prems_of" abbreviation "old_concls_of \ Inference_System.concls_of" abbreviation "old_infer_from \ Inference_System.infer_from" lemmas old_infer_from_def = Inference_System.infer_from_def subsection \Library\ lemma set_zip_replicate_right[simp]: "set (zip xs (replicate (length xs) y)) = (\x. (x, y)) ` set xs" by (induct xs) auto subsection \Ground Layer\ context FO_resolution_prover begin interpretation gr: ground_resolution_with_selection "S_M S M" using selection_axioms by unfold_locales (fact S_M_selects_subseteq S_M_selects_neg_lits)+ definition G_Inf :: "'a clause set \ 'a clause inference set" where "G_Inf M = {Infer (CAs @ [DA]) E |CAs DA AAs As E. gr.ord_resolve M CAs DA AAs As E}" lemma G_Inf_have_prems: "\ \ G_Inf M \ prems_of \ \ []" unfolding G_Inf_def by auto lemma G_Inf_reductive: "\ \ G_Inf M \ concl_of \ < main_prem_of \" unfolding G_Inf_def by (auto dest: gr.ord_resolve_reductive) interpretation G: sound_inference_system "G_Inf M" "{{#}}" "(\e)" proof fix \ assume i_in: "\ \ G_Inf M" moreover { fix I assume I_ent_prems: "I \s set (prems_of \)" obtain CAs AAs As where the_inf: "gr.ord_resolve M CAs (main_prem_of \) AAs As (concl_of \)" and CAs: "CAs = side_prems_of \" using i_in unfolding G_Inf_def by auto then have "I \ concl_of \" using gr.ord_resolve_sound[of M CAs "main_prem_of \" AAs As "concl_of \" I] by (metis I_ent_prems G_Inf_have_prems i_in insert_is_Un set_mset_mset set_prems_of true_clss_insert true_clss_set_mset) } ultimately show "set (inference.prems_of \) \e {concl_of \}" by simp qed interpretation G: clausal_counterex_reducing_inference_system "G_Inf M" "gr.INTERP M" proof fix N D assume "{#} \ N" and "D \ N" and "\ gr.INTERP M N \ D" and "\C. C \ N \ \ gr.INTERP M N \ C \ D \ C" then obtain CAs AAs As E where - "set CAs \ N" and - "gr.INTERP M N \m mset CAs" and - "\CA. CA \ set CAs \ gr.production M N CA \ {}" and - "gr.ord_resolve M CAs D AAs As E" and - "\ gr.INTERP M N \ E" and - "E < D" + cas_in: "set CAs \ N" and + n_mod_cas: "gr.INTERP M N \m mset CAs" and + ca_prod: "\CA. CA \ set CAs \ gr.production M N CA \ {}" and + e_res: "gr.ord_resolve M CAs D AAs As E" and + n_nmod_e: "\ gr.INTERP M N \ E" and + e_lt_d: "E < D" using gr.ord_resolve_counterex_reducing by blast - then show "\Cs E. set Cs \ N \ gr.INTERP M N \s set Cs \ Infer (Cs @ [D]) E \ G_Inf M - \ \ gr.INTERP M N \ E \ E < D" - unfolding G_Inf_def - by (metis (mono_tags, lifting) gr.ex_min_counterex gr.productive_imp_INTERP mem_Collect_eq) + define \ where + "\ = Infer (CAs @ [D]) E" + + have "\ \ G_Inf M" + unfolding \_def G_Inf_def using e_res by auto + moreover have "prems_of \ \ []" + unfolding \_def by simp + moreover have "main_prem_of \ = D" + unfolding \_def by simp + moreover have "set (side_prems_of \) \ N" + unfolding \_def using cas_in by simp + moreover have "gr.INTERP M N \s set (side_prems_of \)" + unfolding \_def using n_mod_cas ca_prod by (simp add: gr.productive_imp_INTERP true_clss_def) + moreover have "\ gr.INTERP M N \ concl_of \" + unfolding \_def using n_nmod_e by simp + moreover have "concl_of \ < D" + unfolding \_def using e_lt_d by simp + ultimately show "\\ \ G_Inf M. prems_of \ \ [] \ main_prem_of \ = D \ set (side_prems_of \) \ N \ + gr.INTERP M N \s set (side_prems_of \) \ \ gr.INTERP M N \ concl_of \ \ concl_of \ < D" + by blast qed interpretation G: clausal_counterex_reducing_calculus_with_standard_redundancy "G_Inf M" "gr.INTERP M" by (unfold_locales, fact G_Inf_have_prems, fact G_Inf_reductive) interpretation G: statically_complete_calculus "{{#}}" "G_Inf M" "(\e)" "G.Red_I M" G.Red_F by unfold_locales (use G.clausal_saturated_complete in blast) subsection \First-Order Layer\ abbreviation \_F :: \'a clause \ 'a clause set\ where \\_F \ grounding_of_cls\ abbreviation \_Fs :: \'a clause set \ 'a clause set\ where \\_Fs \ grounding_of_clss\ lemmas \_F_def = grounding_of_cls_def lemmas \_Fs_def = grounding_of_clss_def definition \_Inf :: \'a clause set \ 'a clause inference \ 'a clause inference set\ where \\_Inf M \ = {Infer (prems_of \ \\cl \s) (concl_of \ \ \) |\ \s. is_ground_subst_list \s \ is_ground_subst \ \ Infer (prems_of \ \\cl \s) (concl_of \ \ \) \ G_Inf M}\ abbreviation \_Inf_opt :: \'a clause set \ 'a clause inference \ 'a clause inference set option\ where \\_Inf_opt M \ \ Some (\_Inf M \)\ definition F_Inf :: "'a clause inference set" where "F_Inf = {Infer (CAs @ [DA]) E | CAs DA AAs As \ E. ord_resolve_rename S CAs DA AAs As \ E}" lemma F_Inf_have_prems: "\ \ F_Inf \ prems_of \ \ []" unfolding F_Inf_def by force interpretation F: lifting_intersection F_Inf "{{#}}" UNIV G_Inf "\N. (\e)" G.Red_I "\N. G.Red_F" "{{#}}" "\N. \_F" \_Inf_opt "\D C C'. False" proof (unfold_locales; (intro ballI)?) show "UNIV \ {}" by (rule UNIV_not_empty) next show "consequence_relation {{#}} (\e)" by (fact consequence_relation_axioms) next show "\M. tiebreaker_lifting {{#}} F_Inf {{#}} (\e) (G_Inf M) (G.Red_I M) G.Red_F \_F (\_Inf_opt M) (\D C C'. False)" proof fix M \ assume \_in: "\ \ F_Inf" show "the (\_Inf_opt M \) \ G.Red_I M (\_F (concl_of \))" unfolding option.sel proof fix \' assume \'_in: "\' \ \_Inf M \" then obtain \ \s where \': "\' = Infer (prems_of \ \\cl \s) (concl_of \ \ \)" and \s_gr: "is_ground_subst_list \s" and \_gr: "is_ground_subst \" and \_infer: "Infer (prems_of \ \\cl \s) (concl_of \ \ \) \ G_Inf M" unfolding \_Inf_def by blast let ?DD1 = "{concl_of \ \ \}" show "\' \ G.Red_I M (\_F (concl_of \))" unfolding G.Red_I_def G.redundant_infer_def mem_Collect_eq using \' \_gr \_infer by (metis inference.sel(2) G_Inf_reductive empty_iff ground_subst_ground_cls grounding_of_cls_ground insert_iff subst_cls_eq_grounding_of_cls_subset_eq true_clss_union) qed qed (auto simp: \_F_def ex_ground_subst) qed notation F.entails_\ (infix "\\e" 50) lemma F_entails_\_iff: "N1 \\e N2 \ \ (\_F ` N1) \e \ (\_F ` N2)" unfolding F.entails_\_def by simp lemma true_Union_grounding_of_cls_iff_true_all_interps_ground_substs: "I \s (\C \ N. {C \ \ |\. is_ground_subst \}) \ (\\. is_ground_subst \ \ I \s N \cs \)" unfolding true_clss_def subst_clss_def by blast interpretation F: sound_inference_system F_Inf "{{#}}" "(\\e)" proof fix \ assume i_in: "\ \ F_Inf" moreover { fix I \ assume I_entails_prems: "\\. is_ground_subst \ \ I \s set (prems_of \) \cs \" and \_gr: "is_ground_subst \" obtain CAs AAs As \ where the_inf: "ord_resolve_rename S CAs (main_prem_of \) AAs As \ (concl_of \)" and CAs: "CAs = side_prems_of \" using i_in unfolding F_Inf_def by auto have prems: "mset (prems_of \) = mset (side_prems_of \) + {#main_prem_of \#}" by (metis (no_types) F_Inf_have_prems[OF i_in] add.right_neutral append_Cons append_Nil2 append_butlast_last_id mset.simps(2) mset_rev mset_single_iff_right rev_append rev_is_Nil_conv union_mset_add_mset_right) have "I \ concl_of \ \ \" using ord_resolve_rename_sound[OF the_inf, of I \, OF _ \_gr] unfolding CAs prems[symmetric] using I_entails_prems by (metis set_mset_mset set_mset_subst_cls_mset_subst_clss true_clss_set_mset) } ultimately show "set (inference.prems_of \) \\e {concl_of \}" unfolding F.entails_\_def \_F_def true_Union_grounding_of_cls_iff_true_all_interps_ground_substs by auto qed lemma G_Inf_overapproximates_F_Inf: "\\<^sub>0 \ G.Inf_from M (\ (\_F ` M)) \ \\. \ \ F.Inf_from M \ \\<^sub>0 \ \_Inf M \" proof - assume \\<^sub>0_in: "\\<^sub>0 \ G.Inf_from M (\ (\_F ` M))" have prems_\\<^sub>0_in: "set (prems_of \\<^sub>0) \ \ (\_F ` M)" using \\<^sub>0_in unfolding G.Inf_from_def by simp note \\<^sub>0_G_Inf = G.Inf_if_Inf_from[OF \\<^sub>0_in] then obtain CAs DA AAs As E where gr_res: \gr.ord_resolve M CAs DA AAs As E\ and \\<^sub>0_is: \\\<^sub>0 = Infer (CAs @ [DA]) E\ unfolding G_Inf_def by auto have CAs_in: \set CAs \ set (prems_of \\<^sub>0)\ by (simp add: \\<^sub>0_is subsetI) then have ground_CAs: \is_ground_cls_list CAs\ using prems_\\<^sub>0_in union_grounding_of_cls_ground is_ground_cls_list_def is_ground_clss_def by auto have DA_in: \DA \ set (prems_of \\<^sub>0)\ using \\<^sub>0_is by simp then have ground_DA: \is_ground_cls DA\ using prems_\\<^sub>0_in union_grounding_of_cls_ground is_ground_clss_def by auto obtain \ where grounded_res: \ord_resolve (S_M S M) CAs DA AAs As \ E\ using ground_ord_resolve_imp_ord_resolve[OF ground_DA ground_CAs gr.ground_resolution_with_selection_axioms gr_res] by auto have prems_ground: \{DA} \ set CAs \ \_Fs M\ using prems_\\<^sub>0_in CAs_in DA_in unfolding \_Fs_def by fast obtain \s \ \2 CAs0 DA0 AAs0 As0 E0 \ where ground_n: "is_ground_subst \" and ground_ns: "is_ground_subst_list \s" and ground_n2: "is_ground_subst \2" and ngr_res: "ord_resolve_rename S CAs0 DA0 AAs0 As0 \ E0" and CAs0_is: "CAs0 \\cl \s = CAs" and DA0_is: "DA0 \ \ = DA" and E0_is: "E0 \ \2 = E" and prems_in: "{DA0} \ set CAs0 \ M" and len_CAs0: "length CAs0 = length CAs" and len_ns: "length \s = length CAs" using ord_resolve_rename_lifting[OF _ grounded_res selection_axioms prems_ground] sel_stable by smt have "length CAs0 = length \s" using len_CAs0 len_ns by simp then have \\<^sub>0_is': "\\<^sub>0 = Infer ((CAs0 @ [DA0]) \\cl (\s @ [\])) (E0 \ \2)" unfolding \\<^sub>0_is by (auto simp: CAs0_is[symmetric] DA0_is[symmetric] E0_is[symmetric]) define \ :: "'a clause inference" where "\ = Infer (CAs0 @ [DA0]) E0" have i_F_Inf: \\ \ F_Inf\ unfolding \_def F_Inf_def using ngr_res by auto have "\\ \s. \\<^sub>0 = Infer ((CAs0 @ [DA0]) \\cl \s) (E0 \ \) \ is_ground_subst_list \s \ is_ground_subst \ \ Infer ((CAs0 @ [DA0]) \\cl \s) (E0 \ \) \ G_Inf M" by (rule exI[of _ \2], rule exI[of _ "\s @ [\]"], use ground_ns in \auto intro: ground_n ground_n2 \\<^sub>0_G_Inf[unfolded \\<^sub>0_is'] simp: \\<^sub>0_is' is_ground_subst_list_def\) then have \\\<^sub>0 \ \_Inf M \\ unfolding \_Inf_def \_def CAs0_is[symmetric] DA0_is[symmetric] E0_is[symmetric] by simp moreover have \\ \ F.Inf_from M\ using prems_in i_F_Inf unfolding F.Inf_from_def \_def by simp ultimately show ?thesis by blast qed interpretation F: statically_complete_calculus "{{#}}" F_Inf "(\\e)" F.Red_I_\ F.Red_F_\_empty proof (rule F.stat_ref_comp_to_non_ground_fam_inter; clarsimp; (intro exI)?) show "\M. statically_complete_calculus {{#}} (G_Inf M) (\e) (G.Red_I M) G.Red_F" by (fact G.statically_complete_calculus_axioms) next fix N assume "F.saturated N" show "F.ground.Inf_from_q N (\ (\_F ` N)) \ {\. \\' \ F.Inf_from N. \ \ \_Inf N \'} \ G.Red_I N (\ (\_F ` N))" using G_Inf_overapproximates_F_Inf unfolding F.ground.Inf_from_q_def \_Inf_def by fastforce qed subsection \Labeled First-Order Layer (or Given Clause Layer)\ datatype label = New | Processed | Old definition FL_Infer_of :: "'a clause inference \ ('a clause \ label) inference set" where "FL_Infer_of \ = {Infer Cls (D, New) |Cls D. \ = Infer (map fst Cls) D}" definition FL_Inf :: "('a clause \ label) inference set" where "FL_Inf = (\\ \ F_Inf. FL_Infer_of \)" abbreviation F_Equiv :: "'a clause \ 'a clause \ bool" (infix "\" 50) where "C \ D \ generalizes C D \ generalizes D C" abbreviation F_Prec :: "'a clause \ 'a clause \ bool" (infix "\\" 50) where "C \\ D \ strictly_generalizes C D" fun L_Prec :: "label \ label \ bool" (infix "\l" 50) where "Old \l l \ l \ Old" | "Processed \l l \ l = New" | "New \l l \ False" lemma irrefl_L_Prec: "\ l \l l" by (cases l) auto lemma trans_L_Prec: "l1 \l l2 \ l2 \l l3 \ l1 \l l3" by (cases l1; cases l2; cases l3) auto lemma wf_L_Prec: "wfP (\l)" by (metis L_Prec.elims(2) L_Prec.simps(3) not_accp_down wfP_accp_iff) interpretation FL: given_clause "{{#}}" F_Inf "{{#}}" UNIV "\N. (\e)" G_Inf G.Red_I "\N. G.Red_F" "\N. \_F" \_Inf_opt FL_Inf "(\)" "(\\)" "(\l)" Old proof (unfold_locales; (intro ballI)?) show "equivp (\)" unfolding equivp_def by (meson generalizes_refl generalizes_trans) next show "po_on (\\) UNIV" unfolding po_on_def irreflp_on_def transp_on_def using strictly_generalizes_irrefl strictly_generalizes_trans by auto next show "wfp_on (\\) UNIV" unfolding wfp_on_UNIV by (metis wf_strictly_generalizes) next show "po_on (\l) UNIV" unfolding po_on_def irreflp_on_def transp_on_def using irrefl_L_Prec trans_L_Prec by blast next show "wfp_on (\l) UNIV" unfolding wfp_on_UNIV by (rule wf_L_Prec) next fix C1 D1 C2 D2 assume "C1 \ D1" "C2 \ D2" "C1 \\ C2" then show "D1 \\ D2" by (smt antisym size_mset_mono size_subst strictly_generalizes_def generalizes_def generalizes_trans) next fix N C1 C2 assume "C1 \ C2" then show "\_F C1 \ \_F C2" unfolding generalizes_def \_F_def by clarsimp (metis is_ground_comp_subst subst_cls_comp_subst) next fix N C2 C1 assume "C2 \\ C1" then show "\_F C1 \ \_F C2" unfolding strictly_generalizes_def generalizes_def \_F_def by clarsimp (metis is_ground_comp_subst subst_cls_comp_subst) next show "\l. L_Prec Old l" using L_Prec.simps(1) by blast qed (auto simp: FL_Inf_def FL_Infer_of_def F_Inf_have_prems) notation FL.Prec_FL (infix "\" 50) notation FL.entails_\_L (infix "\\Le" 50) notation FL.derive (infix "\RedL" 50) notation FL.step (infix "\GC" 50) lemma FL_Red_F_eq: "FL.Red_F N = {C. \D \ \_F (fst C). D \ G.Red_F (\ (\_F ` fst ` N)) \ (\E \ N. E \ C \ D \ \_F (fst E))}" unfolding FL.Red_F_def FL.Red_F_\_q_def by auto lemma mem_FL_Red_F_because_G_Red_F: "(\D \ \_F (fst Cl). D \ G.Red_F (\ (\_F ` fst ` N))) \ Cl \ FL.Red_F N" unfolding FL_Red_F_eq by auto lemma mem_FL_Red_F_because_Prec_FL: "(\D \ \_F (fst Cl). \El \ N. El \ Cl \ D \ \_F (fst El)) \ Cl \ FL.Red_F N" unfolding FL_Red_F_eq by auto interpretation FL: compact_consequence_relation FL.Bot_FL "(\\Le)" proof fix CCl assume unsat: "CCl \\Le FL.Bot_FL" let ?bot = "({#}, undefined)" have "CCl \\Le {?bot}" using unsat by (metis (lifting) FL.entail_set_all_formulas UNIV_I insertI1 mem_Sigma_iff) then have "\ satisfiable (\CL \ CCl. \_F (fst CL))" unfolding FL.labeled_entailment_lifting F_entails_\_iff by auto then obtain DD where d_sub: "DD \ (\Cl \ CCl. \_F (fst Cl))" and d_fin: "finite DD" and d_unsat: "\I. \ I \s DD" unfolding clausal_logic_compact[of "\CL \ CCl. \_F (fst CL)"] by blast define CCl' :: "('a clause \ label) set" where "CCl' = {SOME Cl. Cl \ CCl \ D \ \_F (fst Cl) |D. D \ DD}" have ex_in_cl: "\Cl. Cl \ CCl \ D \ \_F (fst Cl)" if "D \ DD" for D using that d_sub by blast then have d_sub': "DD \ (\Cl \ CCl'. \_F (fst Cl))" using ex_in_cl unfolding CCl'_def by clarsimp (metis (lifting) eq_fst_iff ex_in_cl someI_ex) have "CCl' \ CCl" unfolding CCl'_def using someI_ex[OF ex_in_cl] by blast moreover have "finite CCl'" unfolding CCl'_def using d_fin by simp moreover have "CCl' \\Le FL.Bot_FL" unfolding CCl'_def using d_unsat ex_in_cl d_sub' CCl'_def by (metis (no_types, lifting) FL.entails_\_L_def subsetD true_clss_def) ultimately show "\CCl' \ CCl. finite CCl' \ CCl' \\Le FL.Bot_FL" by blast qed interpretation FL: refutationally_compact_calculus FL.Bot_FL FL_Inf "(\\Le)" FL.Red_I FL.Red_F .. subsection \\textsf{RP} Layer\ interpretation sq: selection "S_Q Sts" unfolding S_Q_def using S_M_selects_subseteq S_M_selects_neg_lits selection_axioms by unfold_locales auto interpretation gd: ground_resolution_with_selection "S_Q Sts" by unfold_locales interpretation src: standard_redundancy_criterion_reductive "gd.ord_\ Sts" by unfold_locales interpretation src: standard_redundancy_criterion_counterex_reducing "gd.ord_\ Sts" "ground_resolution_with_selection.INTERP (S_Q Sts)" by unfold_locales definition lclss_of_state :: "'a state \ ('a clause \ label) set" where "lclss_of_state St = (\C. (C, New)) ` N_of_state St \ (\C. (C, Processed)) ` P_of_state St \ (\C. (C, Old)) ` Q_of_state St" lemma image_hd_lclss_of_state[simp]: "fst ` lclss_of_state St = clss_of_state St" unfolding lclss_of_state_def by (auto simp: image_Un image_comp) lemma insert_lclss_of_state[simp]: "insert (C, New) (lclss_of_state (N, P, Q)) = lclss_of_state (N \ {C}, P, Q)" "insert (C, Processed) (lclss_of_state (N, P, Q)) = lclss_of_state (N, P \ {C}, Q)" "insert (C, Old) (lclss_of_state (N, P, Q)) = lclss_of_state (N, P, Q \ {C})" unfolding lclss_of_state_def image_def by auto lemma union_lclss_of_state[simp]: "lclss_of_state (N1, P1, Q1) \ lclss_of_state (N2, P2, Q2) = lclss_of_state (N1 \ N2, P1 \ P2, Q1 \ Q2)" unfolding lclss_of_state_def by auto lemma mem_lclss_of_state[simp]: "(C, New) \ lclss_of_state (N, P, Q) \ C \ N" "(C, Processed) \ lclss_of_state (N, P, Q) \ C \ P" "(C, Old) \ lclss_of_state (N, P, Q) \ C \ Q" unfolding lclss_of_state_def image_def by auto lemma lclss_Liminf_commute: "Liminf_llist (lmap lclss_of_state Sts) = lclss_of_state (Liminf_state Sts)" proof - have \Liminf_llist (lmap lclss_of_state Sts) = (\C. (C, New)) ` Liminf_llist (lmap N_of_state Sts) \ (\C. (C, Processed)) ` Liminf_llist (lmap P_of_state Sts) \ (\C. (C, Old)) ` Liminf_llist (lmap Q_of_state Sts)\ proof - have \inj_on (\C. (C, Old)) (Sup_llist (lmap Q_of_state Sts))\ by (meson Pair_inject inj_onI) moreover have \inj_on (\C. (C, Processed)) (Sup_llist (lmap P_of_state Sts))\ by (meson Pair_inject inj_onI) moreover have \inj_on (\C. (C, New)) (Sup_llist (lmap N_of_state Sts))\ by (meson Pair_inject inj_onI) moreover have \ \x\lset Sts. \Y\lset Sts. ((\C. (C, New)) ` N_of_state x \ (\C. (C, Processed)) ` P_of_state x) \ (\C. (C, Old)) ` Q_of_state Y = {}\ by auto moreover have \ \x\lset Sts. \Y\lset Sts. (\C. (C, New)) ` N_of_state x \ (\C. (C, Processed)) ` P_of_state Y = {}\ by auto ultimately show ?thesis unfolding lclss_of_state_def[abs_def] using Liminf_llist_lmap_union Liminf_llist_lmap_image by (smt llist.map_cong) qed then show ?thesis unfolding lclss_of_state_def Liminf_state_def by auto qed lemma GC_tautology_step: assumes tauto: "Neg A \# C" "Pos A \# C" shows "lclss_of_state (N \ {C}, P, Q) \GC lclss_of_state (N, P, Q)" proof - have c\_red: "C\ \ G.Red_F (\D \ N'. \_F (fst D))" if in_g: "C\ \ \_F C" for N' :: "('a clause \ label) set" and C\ proof - obtain \ where "C\ = C \ \" using in_g unfolding \_F_def by blast then have compl_lits: "Neg (A \a \) \# C\" "Pos (A \a \) \# C\" using tauto Neg_Melem_subst_atm_subst_cls Pos_Melem_subst_atm_subst_cls by auto then have "{} \e {C\}" unfolding true_clss_def true_cls_def true_lit_def if_distrib_fun by (metis literal.disc literal.sel singletonD) then show ?thesis unfolding G.Red_F_def by auto qed show ?thesis proof (rule FL.step.process[of _ "lclss_of_state (N, P, Q)" "{(C, New)}" _ "{}"]) show \lclss_of_state (N \ {C}, P, Q) = lclss_of_state (N, P, Q) \ {(C, New)}\ unfolding lclss_of_state_def by auto next show \lclss_of_state (N, P, Q) = lclss_of_state (N, P, Q) \ {}\ unfolding lclss_of_state_def by auto next show \{(C, New)} \ FL.Red_F_\ (lclss_of_state (N, P, Q) \ {})\ using mem_FL_Red_F_because_G_Red_F c\_red[of _ "lclss_of_state (N, P, Q)"] unfolding lclss_of_state_def by auto next show \FL.active_subset {} = {}\ unfolding FL.active_subset_def by auto qed qed lemma GC_subsumption_step: assumes d_in: "Dl \ N" and d_sub_c: "strictly_subsumes (fst Dl) (fst Cl) \ subsumes (fst Dl) (fst Cl) \ snd Dl \l snd Cl" shows "N \ {Cl} \GC N" proof - have d_sub'_c: "Cl \ FL.Red_F {Dl} \ Dl \ Cl" proof (cases "size (fst Dl) = size (fst Cl)") case True assume sizes_eq: \size (fst Dl) = size (fst Cl)\ have \size (fst Dl) = size (fst Cl) \ strictly_subsumes (fst Dl) (fst Cl) \ subsumes (fst Dl) (fst Cl) \ snd Dl \l snd Cl \ Dl \ Cl\ unfolding FL.Prec_FL_def unfolding generalizes_def strictly_generalizes_def strictly_subsumes_def subsumes_def by (metis size_subst subset_mset.order_refl subseteq_mset_size_eql) then have "Dl \ Cl" using sizes_eq d_sub_c by auto then show ?thesis by (rule disjI2) next case False then have d_ssub_c: "strictly_subsumes (fst Dl) (fst Cl)" using d_sub_c unfolding strictly_subsumes_def subsumes_def by (metis size_subst strict_subset_subst_strictly_subsumes strictly_subsumes_antisym subset_mset.antisym_conv2) have "Cl \ FL.Red_F {Dl}" proof (rule mem_FL_Red_F_because_G_Red_F) show \\D\\_F (fst Cl). D \ G.Red_F (\ (\_F ` fst ` {Dl}))\ using d_ssub_c unfolding G.Red_F_def strictly_subsumes_def subsumes_def \_F_def proof clarsimp fix \ \' assume fst_not_in: \\\. \ fst Cl \ \ \# fst Dl\ and fst_in: \fst Dl \ \ \# fst Cl\ and gr_sig: \is_ground_subst \'\ have \{fst Dl \ \ \ \'} \ {fst Dl \ \ |\. is_ground_subst \}\ using gr_sig by (metis (mono_tags, lifting) is_ground_comp_subst mem_Collect_eq singletonD subsetI subst_cls_comp_subst) moreover have \\I. I \s {fst Dl \ \ \ \'} \ I \ fst Cl \ \'\ using fst_in by (meson subst_cls_mono_mset true_clss_insert true_clss_subclause) moreover have \\D\{fst Dl \ \ \ \'}. D < fst Cl \ \'\ using fst_not_in fst_in gr_sig proof clarify show \\\. \ fst Cl \ \ \# fst Dl \ fst Dl \ \ \# fst Cl \ is_ground_subst \' \ fst Dl \ \ \ \' < fst Cl \ \'\ by (metis False size_subst subset_imp_less_mset subset_mset.le_less subst_subset_mono) qed ultimately show \\DD\{fst Dl \ \ |\. is_ground_subst \}. (\I. I \s DD \ I \ fst Cl \ \') \ (\D\DD. D < fst Cl \ \')\ by blast qed qed then show ?thesis by (rule disjI1) qed show ?thesis proof (rule FL.step.process[of _ N "{Cl}" _ "{}"], simp+) show \Cl \ FL.Red_F_\ N\ using d_sub'_c unfolding FL_Red_F_eq proof - have \\D. D \ \_F (fst Cl) \ \E\N. E \ Cl \ D \ \_F (fst E) \ \D\\_F (fst Cl). D \ G.Red_F (\_F (fst Dl)) \ Dl \ Cl \ D \ \_F (fst Dl) \ D \ G.Red_F (\a\N. \_F (fst a))\ by (metis (no_types, lifting) G.Red_F_of_subset SUP_upper d_in subset_iff) moreover have \\D. D \ \_F (fst Cl) \ \E\N. E \ Cl \ D \ \_F (fst E) \ Dl \ Cl \ D \ G.Red_F (\a\N. \_F (fst a))\ by (smt FL.Prec_FL_def FL.equiv_F_grounding FL.prec_F_grounding UNIV_witness d_in in_mono) ultimately show \Cl \ {C. \D\\_F (fst C). D \ G.Red_F (\ (\_F ` fst ` {Dl})) \ (\E\{Dl}. E \ C \ D \ \_F (fst E))} \ Dl \ Cl \ Cl \ {C. \D\\_F (fst C). D \ G.Red_F (\ (\_F ` fst ` N)) \ (\E\N. E \ C \ D \ \_F (fst E))}\ by auto qed next show \FL.active_subset {} = {}\ unfolding FL.active_subset_def by simp qed qed lemma GC_reduction_step: assumes young: "snd Dl \ Old" and d_sub_c: "fst Dl \# fst Cl" shows "N \ {Cl} \GC N \ {Dl}" proof (rule FL.step.process[of _ N "{Cl}" _ "{Dl}"]) have "Cl \ FL.Red_F {Dl}" proof (rule mem_FL_Red_F_because_G_Red_F) show \\D\\_F (fst Cl). D \ G.Red_F (\ (\_F ` fst ` {Dl}))\ using d_sub_c unfolding G.Red_F_def strictly_subsumes_def subsumes_def \_F_def proof clarsimp fix \ assume fst_not_in: \\ fst Cl \# fst Dl\ and fst_in: \fst Dl \# fst Cl\ and gr_sig: \is_ground_subst \\ have \{fst Dl \ \} \ {fst Dl \ \ |\. is_ground_subst \}\ using gr_sig by blast moreover have \fst Dl \ \ < fst Cl \ \\ using subst_subset_mono[OF d_sub_c, of \] gr_sig by (simp add: subset_imp_less_mset) moreover have \\I. I \ fst Dl \ \ \ I \ fst Cl \ \\ using subst_subset_mono[OF d_sub_c] true_clss_subclause by fast ultimately show \\DD\{fst Dl \ \ |\. is_ground_subst \}. (\I. I \s DD \ I \ fst Cl \ \) \ (\D\DD. D < fst Cl \ \)\ by blast qed qed then show "{Cl} \ FL.Red_F (N \ {Dl})" using FL.Red_F_of_subset by blast qed (auto simp: FL.active_subset_def young) lemma GC_processing_step: "N \ {(C, New)} \GC N \ {(C, Processed)}" proof (rule FL.step.process[of _ N "{(C, New)}" _ "{(C, Processed)}"]) have "(C, New) \ FL.Red_F {(C, Processed)}" by (rule mem_FL_Red_F_because_Prec_FL) (simp add: FL.Prec_FL_def generalizes_refl) then show "{(C, New)} \ FL.Red_F (N \ {(C, Processed)})" using FL.Red_F_of_subset by blast qed (auto simp: FL.active_subset_def) lemma old_inferences_between_eq_new_inferences_between: "old_concl_of ` inference_system.inferences_between (ord_FO_\ S) N C = concl_of ` F.Inf_from2 N {C}" (is "?rp = ?f") proof (intro set_eqI iffI) fix E assume e_in: "E \ old_concl_of ` inference_system.inferences_between (ord_FO_\ S) N C" obtain CAs DA AAs As \ where e_res: "ord_resolve_rename S CAs DA AAs As \ E" and cd_sub: "set CAs \ {DA} \ N \ {C}" and c_in: "C \ set CAs \ {DA}" using e_in unfolding inference_system.inferences_between_def infer_from_def ord_FO_\_def by auto show "E \ concl_of ` F.Inf_from2 N {C}" unfolding F.Inf_from2_alt F.Inf_from_def proof - have \Infer (CAs @ [DA]) E \ F_Inf \ set (prems_of (Infer (CAs @ [DA]) E)) \ insert C N \ C \ set (prems_of (Infer (CAs @ [DA]) E)) \ E = concl_of (Infer (CAs @ [DA]) E)\ using e_res cd_sub c_in F_Inf_def by auto then show \E \ concl_of ` {\ \ F_Inf. \ \ {\ \ F_Inf. set (prems_of \) \ N \ {C}} \ set (prems_of \) \ {C} \ {}}\ by (smt Un_insert_right boolean_algebra_cancel.sup0 disjoint_insert(2) mem_Collect_eq image_def) qed next fix E assume e_in: "E \ concl_of ` F.Inf_from2 N {C}" obtain CAs DA AAs As \ where e_res: "ord_resolve_rename S CAs DA AAs As \ E" and cd_sub: "set CAs \ {DA} \ N \ {C}" and c_in: "C \ set CAs \ {DA}" using e_in unfolding F.Inf_from2_alt F.Inf_from_def F_Inf_def inference_system.Inf_from2_alt inference_system.Inf_from_def by (auto simp: image_def Bex_def) show "E \ old_concl_of ` inference_system.inferences_between (ord_FO_\ S) N C" unfolding inference_system.inferences_between_def infer_from_def ord_FO_\_def using e_res cd_sub c_in by (clarsimp simp: image_def Bex_def, rule_tac x = "old_Infer (mset CAs) DA E" in exI, auto) qed lemma GC_inference_step: assumes young: "l \ Old" and no_active: "FL.active_subset M = {}" and m_sup: "fst ` M \ old_concl_of ` inference_system.inferences_between (ord_FO_\ S) (fst ` FL.active_subset N) C" shows "N \ {(C, l)} \GC N \ {(C, Old)} \ M" proof (rule FL.step.infer[of _ N C l _ M]) have m_sup': "fst ` M \ concl_of ` F.Inf_from2 (fst ` FL.active_subset N) {C}" using m_sup unfolding old_inferences_between_eq_new_inferences_between . show "F.Inf_from2 (fst ` FL.active_subset N) {C} \ F.Red_I (fst ` (N \ {(C, Old)} \ M))" proof fix \ assume \_in_if2: "\ \ F.Inf_from2 (fst ` FL.active_subset N) {C}" note \_in = F.Inf_if_Inf_from2[OF \_in_if2] have "concl_of \ \ fst ` M" using m_sup' \_in_if2 m_sup' by (auto simp: image_def Collect_mono_iff F.Inf_from2_alt) then have "concl_of \ \ fst ` (N \ {(C, Old)} \ M)" by auto then show "\ \ F.Red_I_\ (fst ` (N \ {(C, Old)} \ M))" by (rule F.Red_I_of_Inf_to_N[OF \_in]) qed qed (use young no_active in auto) lemma RP_step_imp_GC_step: "St \ St' \ lclss_of_state St \GC lclss_of_state St'" proof (induction rule: RP.induct) case (tautology_deletion A C N P Q) then show ?case by (rule GC_tautology_step) next case (forward_subsumption D P Q C N) note d_in = this(1) and d_sub_c = this(2) show ?case proof (cases "D \ P") case True then show ?thesis using GC_subsumption_step[of "(D, Processed)" "lclss_of_state (N, P, Q)" "(C, New)"] d_sub_c by auto next case False then have "D \ Q" using d_in by simp then show ?thesis using GC_subsumption_step[of "(D, Old)" "lclss_of_state (N, P, Q)" "(C, New)"] d_sub_c by auto qed next case (backward_subsumption_P D N C P Q) note d_in = this(1) and d_ssub_c = this(2) then show ?case using GC_subsumption_step[of "(D, New)" "lclss_of_state (N, P, Q)" "(C, Processed)"] d_ssub_c by auto next case (backward_subsumption_Q D N C P Q) note d_in = this(1) and d_ssub_c = this(2) then show ?case using GC_subsumption_step[of "(D, New)" "lclss_of_state (N, P, Q)" "(C, Old)"] d_ssub_c by auto next case (forward_reduction D L' P Q L \ C N) show ?case using GC_reduction_step[of "(C, New)" "(C + {#L#}, New)" "lclss_of_state (N, P, Q)"] by auto next case (backward_reduction_P D L' N L \ C P Q) show ?case using GC_reduction_step[of "(C, Processed)" "(C + {#L#}, Processed)" "lclss_of_state (N, P, Q)"] by auto next case (backward_reduction_Q D L' N L \ C P Q) show ?case using GC_reduction_step[of "(C, Processed)" "(C + {#L#}, Old)" "lclss_of_state (N, P, Q)"] by auto next case (clause_processing N C P Q) show ?case using GC_processing_step[of "lclss_of_state (N, P, Q)" C] by auto next case (inference_computation N Q C P) note n = this(1) show ?case proof - have \FL.active_subset (lclss_of_state (N, {}, {})) = {}\ unfolding n by (auto simp: FL.active_subset_def) moreover have \old_concls_of (inference_system.inferences_between (ord_FO_\ S) (fst ` FL.active_subset (lclss_of_state ({}, P, Q))) C) \ N\ unfolding n inference_system.inferences_between_def image_def mem_Collect_eq lclss_of_state_def infer_from_def by (auto simp: FL.active_subset_def) ultimately have \lclss_of_state ({}, insert C P, Q) \GC lclss_of_state (N, P, insert C Q)\ using GC_inference_step[of Processed "lclss_of_state (N, {}, {})" "lclss_of_state ({}, P, Q)" C, simplified] by blast then show ?case by (auto simp: FL.active_subset_def) qed qed lemma RP_derivation_imp_GC_derivation: "chain (\) Sts \ chain (\GC) (lmap lclss_of_state Sts)" using chain_lmap RP_step_imp_GC_step by blast lemma RP_step_imp_derive_step: "St \ St' \ lclss_of_state St \RedL lclss_of_state St'" by (rule FL.one_step_equiv) (rule RP_step_imp_GC_step) lemma RP_derivation_imp_derive_derivation: "chain (\) Sts \ chain (\RedL) (lmap lclss_of_state Sts)" using chain_lmap RP_step_imp_derive_step by blast theorem RP_sound_new_statement: assumes deriv: "chain (\) Sts" and bot_in: "{#} \ clss_of_state (Liminf_state Sts)" shows "clss_of_state (lhd Sts) \\e {{#}}" proof - have "clss_of_state (Liminf_state Sts) \\e {{#}}" using F.subset_entailed bot_in by auto then have "fst ` Liminf_llist (lmap lclss_of_state Sts) \\e {{#}}" by (metis image_hd_lclss_of_state lclss_Liminf_commute) then have "Liminf_llist (lmap lclss_of_state Sts) \\Le FL.Bot_FL" using FL.labeled_entailment_lifting by simp then have "lhd (lmap lclss_of_state Sts) \\Le FL.Bot_FL" proof - assume entails_lim: \FL.entails_\ (Liminf_llist (lmap lclss_of_state Sts)) ({{#}} \ UNIV)\ have \chain (\RedL) (lmap lclss_of_state Sts)\ using deriv RP_derivation_imp_derive_derivation by simp moreover have \chain FL.entails_\ (lmap lclss_of_state Sts)\ by (smt F_entails_\_iff FL.labeled_entailment_lifting RP_model chain_lmap deriv \_Fs_def image_hd_lclss_of_state) ultimately show \FL.entails_\ (lhd (lmap lclss_of_state Sts)) ({{#}} \ UNIV)\ using entails_lim FL.unsat_limit_iff by blast qed then have "lclss_of_state (lhd Sts) \\Le FL.Bot_FL" using chain_not_lnull deriv by fastforce then show ?thesis unfolding FL.entails_\_L_def F.entails_\_def lclss_of_state_def by auto qed theorem RP_saturated_if_fair_new_statement: assumes deriv: "chain (\) Sts" and init: "FL.active_subset (lclss_of_state (lhd Sts)) = {}" and final: "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}" shows "FL.saturated (Liminf_llist (lmap lclss_of_state Sts))" proof - note nnil = chain_not_lnull[OF deriv] have gc_deriv: "chain (\GC) (lmap lclss_of_state Sts)" by (rule RP_derivation_imp_GC_derivation[OF deriv]) show ?thesis using nnil init final FL.fair_implies_Liminf_saturated[OF FL.gc_to_red[OF gc_deriv] FL.gc_fair[OF gc_deriv]] by simp qed corollary RP_complete_if_fair_new_statement: assumes deriv: "chain (\) Sts" and init: "FL.active_subset (lclss_of_state (lhd Sts)) = {}" and final: "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}" and unsat: "grounding_of_state (lhd Sts) \e {{#}}" shows "{#} \ Q_of_state (Liminf_state Sts)" proof - note nnil = chain_not_lnull[OF deriv] note len = chain_length_pos[OF deriv] have gc_deriv: "chain (\GC) (lmap lclss_of_state Sts)" by (rule RP_derivation_imp_GC_derivation[OF deriv]) have hd_unsat: "fst ` lhd (lmap lclss_of_state Sts) \\e {{#}}" proof - have hd_lcls: "fst ` lhd (lmap lclss_of_state Sts) = lhd (lmap clss_of_state Sts)" using len zero_enat_def by auto show ?thesis unfolding hd_lcls F_entails_\_iff unfolding true_clss_def proof fix I show "Ball (\ (\_F ` lhd (lmap (\St. N_of_state St \ P_of_state St \ Q_of_state St) Sts))) ((\) I) \ Ball (\ (\_F ` {{#}})) ((\) I)" using unsat unfolding \_Fs_def by (metis (no_types, lifting) chain_length_pos gc_deriv gr.ex_min_counterex i0_less llength_eq_0 llength_lmap llength_lmap llist.map_sel(1) true_cls_empty true_clss_singleton) qed qed have "\BL \ {{#}} \ UNIV. BL \ Liminf_llist (lmap lclss_of_state Sts)" proof (rule FL.gc_complete_Liminf[OF gc_deriv,of "{#}"]) show \FL.active_subset (lhd (lmap lclss_of_state Sts)) = {}\ by (simp add: init nnil) next show \FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}\ using final by blast next show \{#} \ {{#}}\ by simp next show \fst ` lhd (lmap lclss_of_state Sts) \\e {{#}}\ using hd_unsat by blast qed then show ?thesis unfolding Liminf_state_def lclss_Liminf_commute using final[unfolded FL.passive_subset_def] Liminf_state_def lclss_Liminf_commute by fastforce qed subsection \Alternative Derivation of Previous \textsf{RP} Results\ lemma old_fair_imp_new_fair: assumes nnul: "\ lnull Sts" and fair: "fair_state_seq Sts" and empty_Q0: "Q_of_state (lhd Sts) = {}" shows "FL.active_subset (lclss_of_state (lhd Sts)) = {}" "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}" proof - show "FL.active_subset (lclss_of_state (lhd Sts)) = {}" using nnul empty_Q0 unfolding FL.active_subset_def by (cases Sts) auto next show "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}" using fair unfolding fair_state_seq_def FL.passive_subset_def proof assume \N_of_state (Liminf_state Sts) = {}\ and \P_of_state (Liminf_state Sts) = {}\ then show \{CL \ Liminf_llist (lmap lclss_of_state Sts). snd CL \ Old} = {}\ unfolding lclss_Liminf_commute lclss_of_state_def by auto qed qed lemma old_redundant_infer_iff: "src.redundant_infer N \ \ (\DD. DD \ N \ DD \ set_mset (old_side_prems_of \) \e {old_concl_of \} \ (\D \ DD. D < old_main_prem_of \))" (is "?lhs \ ?rhs") proof assume ?lhs then show ?rhs unfolding src.redundant_infer_def by auto next assume ?rhs then obtain DD0 where "DD0 \ N" and "DD0 \ set_mset (old_side_prems_of \) \e {old_concl_of \}" and "\D \ DD0. D < old_main_prem_of \" by blast then obtain DD where fin_dd: "finite DD" and dd_in: "DD \ N" and dd_un: "DD \ set_mset (old_side_prems_of \) \e {old_concl_of \}" and all_dd: "\D \ DD. D < old_main_prem_of \" using entails_concl_compact_union[of "{old_concl_of \}" DD0 "set_mset (old_side_prems_of \)"] by fast show ?lhs unfolding src.redundant_infer_def proof show \set_mset (mset_set DD) \ N \ (\I. I \m mset_set DD + old_side_prems_of \ \ I \ old_concl_of \) \ (\D. D \# mset_set DD \ D < old_main_prem_of \)\ using fin_dd dd_in dd_un all_dd by auto qed qed definition old_infer_of :: "'a clause inference \ 'a old_inference" where "old_infer_of \ = old_Infer (mset (side_prems_of \)) (main_prem_of \) (concl_of \)" lemma new_redundant_infer_imp_old_redundant_infer: "G.redundant_infer N \ \ src.redundant_infer N (old_infer_of \)" unfolding old_redundant_infer_iff G.redundant_infer_def old_infer_of_def by simp lemma saturated_imp_saturated_RP: assumes satur: "FL.saturated (Liminf_llist (lmap lclss_of_state Sts))" and no_passive: "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}" shows "src.saturated_upto Sts (grounding_of_state (Liminf_state Sts))" proof - define Q where "Q = Liminf_llist (lmap Q_of_state Sts)" define Ql where "Ql = (\C. (C, Old)) ` Q" define G where "G = \ (\_F ` Q)" have limuls_eq: "Liminf_llist (lmap lclss_of_state Sts) = Ql" unfolding Ql_def Q_def using no_passive[unfolded FL.passive_subset_def] proof (simp) (* Sledgehammer-generated *) assume a1: "\a b. (a, b) \ Liminf_llist (lmap lclss_of_state Sts) \ b = Old" obtain mm :: "'a literal multiset set \ 'a literal multiset" where f2: "\M. {} = M \ mm M \ M" by (metis (no_types) equals0I) have f3: "\ps. Liminf_llist (lmap lclss_of_state ps) = lclss_of_state (Liminf_llist (lmap N_of_state ps), Liminf_llist (lmap P_of_state ps), Liminf_llist (lmap Q_of_state ps))" using Liminf_state_def lclss_Liminf_commute by presburger then have f4: "Liminf_llist (lmap P_of_state Sts) = {}" using f2 a1 by (metis (no_types) label.simps(5) mem_lclss_of_state(2)) have "Liminf_llist (lmap N_of_state Sts) = {}" using f3 f2 a1 by (metis (no_types) label.simps(3) mem_lclss_of_state(1)) then show "Liminf_llist (lmap lclss_of_state Sts) = (\m. (m, Old)) ` Liminf_llist (lmap Q_of_state Sts)" using f4 f3 by (simp add: lclss_of_state_def) qed have clst_eq: "clss_of_state (Liminf_state Sts) = Q" proof - (* Sledgehammer-generated *) have f1: "Q_of_state (Liminf_state Sts) = Q" using Liminf_state_def Q_def Q_of_state.simps by presburger then have f2: "Ql \ ((\m. (m, New)) ` N_of_state (Liminf_state Sts) \ (\m. (m, Processed)) ` P_of_state (Liminf_state Sts)) = lclss_of_state (Liminf_state Sts)" by (simp add: Ql_def lclss_of_state_def sup_commute) have f3: "lclss_of_state ({}, {}, Q_of_state (Liminf_state Sts)) = {} \ Ql" using f1 by (simp add: Ql_def lclss_of_state_def) have "Ql = (\m. (m, New)) ` N_of_state (Liminf_state Sts) \ (\m. (m, Processed)) ` P_of_state (Liminf_state Sts) \ (Ql \ {})" using f1 lclss_Liminf_commute lclss_of_state_def limuls_eq by auto then have "clss_of_state (Liminf_state Sts) = fst ` lclss_of_state ({}, {}, Q_of_state (Liminf_state Sts))" using f3 f2 by (simp add: sup_commute) then show ?thesis unfolding Q_def by (simp add: Liminf_state_def) qed have gflimuls_eq: "(\Cl \ Ql. \_F (fst Cl)) = G" unfolding Ql_def G_def by auto have "gd.inferences_from Sts G \ src.Ri Sts G" proof fix \ assume \_inf: "\ \ gd.inferences_from Sts G" obtain \ where \_inff: "\ \ G.Inf_from Q G" and \: "\ = old_infer_of \" using \_inf unfolding gd.inferences_from_def old_infer_from_def G.Inf_from_def old_infer_of_def proof (atomize_elim, clarify) assume g_is: \\ \ gd.ord_\ Sts\ and prems_in: \set_mset (old_side_prems_of \ + {#old_main_prem_of \#}) \ G\ obtain CAs DA AAs As E where main_in: \DA \ G\ and side_in: \set CAs \ G\ and g_is2: \\ = old_Infer (mset CAs) DA E\ and ord_res: \gd.ord_resolve Sts CAs DA AAs As E\ using g_is prems_in unfolding gd.ord_\_def by auto define \_\ where "\_\ = Infer (CAs @ [DA]) E" then have \\_\ \ G_Inf Q\ using Q_of_state.simps g_is g_is2 ord_res Liminf_state_def S_Q_def unfolding gd.ord_\_def G_Inf_def Q_def by auto moreover have \set (prems_of \_\) \ G\ using g_is2 prems_in unfolding \_\_def by simp moreover have \\ = old_Infer (mset (side_prems_of \_\)) (main_prem_of \_\) (concl_of \_\)\ using g_is2 unfolding \_\_def by simp ultimately show \\\. \ \ {\ \ G_Inf Q. set (prems_of \) \ G} \ \ = old_Infer (mset (side_prems_of \)) (main_prem_of \) (concl_of \)\ by blast qed obtain \' where \'_inff: "\' \ F.Inf_from Q" and \_in_\': "\ \ \_Inf Q \'" using G_Inf_overapproximates_F_Inf \_inff unfolding G_def by blast note \'_inf = F.Inf_if_Inf_from[OF \'_inff] let ?olds = "replicate (length (prems_of \')) Old" obtain \'' and l0 where \'': "\'' = Infer (zip (prems_of \') ?olds) (concl_of \', l0)" and \''_inf: "\'' \ FL_Inf" using FL.Inf_F_to_Inf_FL[OF \'_inf, of ?olds, simplified] by blast have "set (prems_of \'') \ Ql" using \'_inff[unfolded F.Inf_from_def, simplified] unfolding \'' Ql_def by auto then have "\'' \ FL.Inf_from Ql" unfolding FL.Inf_from_def using \''_inf by simp moreover have "\' = FL.to_F \''" unfolding \'' unfolding FL.to_F_def by simp ultimately have "\ \ G.Red_I Q G" using \_in_\' FL.sat_inf_imp_ground_red_fam_inter[OF satur, unfolded limuls_eq gflimuls_eq, simplified] by blast then have "G.redundant_infer G \" unfolding G.Red_I_def by auto then have \_red: "src.redundant_infer G \" unfolding \ by (rule new_redundant_infer_imp_old_redundant_infer) moreover have "\ \ gd.ord_\ Sts" using \_inf gd.inferences_from_def by blast ultimately show "\ \ src.Ri Sts G" unfolding src.Ri_def by auto qed then show ?thesis unfolding G_def clst_eq src.saturated_upto_def by clarsimp (smt Diff_subset gd.inferences_from_mono subset_eq \_Fs_def) qed theorem RP_sound_old_statement: assumes deriv: "chain (\) Sts" and bot_in: "{#} \ clss_of_state (Liminf_state Sts)" shows "\ satisfiable (grounding_of_state (lhd Sts))" using RP_sound_new_statement[OF deriv bot_in] unfolding F_entails_\_iff \_Fs_def by simp text \The theorem below is stated differently than the original theorem in \textsf{RP}: The grounding of the limit might be a strict subset of the limit of the groundings. Because saturation is neither monotone nor antimonotone, the two results are incomparable. See also @{thm [source] grounding_of_state_Liminf_state_subseteq}.\ theorem RP_saturated_if_fair_old_statement_altered: assumes deriv: "chain (\) Sts" and fair: "fair_state_seq Sts" and empty_Q0: "Q_of_state (lhd Sts) = {}" shows "src.saturated_upto Sts (grounding_of_state (Liminf_state Sts))" proof - note fair' = old_fair_imp_new_fair[OF chain_not_lnull[OF deriv] fair empty_Q0] show ?thesis proof (rule saturated_imp_saturated_RP[OF _ fair'(2)], rule RP_saturated_if_fair_new_statement) show \chain (\) Sts\ by (rule deriv) qed (rule fair')+ qed corollary RP_complete_if_fair_old_statement: assumes deriv: "chain (\) Sts" and fair: "fair_state_seq Sts" and empty_Q0: "Q_of_state (lhd Sts) = {}" and unsat: "\ satisfiable (grounding_of_state (lhd Sts))" shows "{#} \ Q_of_state (Liminf_state Sts)" proof (rule RP_complete_if_fair_new_statement) show \chain (\) Sts\ by (rule deriv) next show \\_Fs (N_of_state (lhd Sts) \ P_of_state (lhd Sts) \ Q_of_state (lhd Sts)) \e {{#}}\ using unsat unfolding F_entails_\_iff by auto qed (rule old_fair_imp_new_fair[OF chain_not_lnull[OF deriv] fair empty_Q0])+ end end diff --git a/thys/Saturation_Framework_Extensions/Soundness.thy b/thys/Saturation_Framework_Extensions/Soundness.thy --- a/thys/Saturation_Framework_Extensions/Soundness.thy +++ b/thys/Saturation_Framework_Extensions/Soundness.thy @@ -1,35 +1,156 @@ (* Title: Soundness Author: Sophie Tourret , 2020 - Author: Jasmin Blanchette , 2020 + Author: Jasmin Blanchette , 2014, 2017, 2020 + Author: Dmitriy Traytel , 2014 + Author: Anders Schlichtkrull , 2017 *) section \Soundness\ theory Soundness - imports Consistency_Preservation + imports Saturation_Framework.Calculus begin text \ Although consistency-preservation usually suffices, soundness is a more precise concept and is sometimes useful. \ locale sound_inference_system = inference_system + consequence_relation + assumes sound: \\ \ Inf \ set (prems_of \) \ {concl_of \}\ begin lemma Inf_consist_preserving: assumes n_cons: "\ N \ Bot" shows "\ N \ concl_of ` Inf_from N \ Bot" proof - have "N \ concl_of ` Inf_from N" using sound unfolding Inf_from_def image_def Bex_def mem_Collect_eq by (smt all_formulas_entailed entails_trans mem_Collect_eq subset_entailed) then show ?thesis using n_cons entails_trans_strong by blast qed end +text \ +Assuming compactness of the consequence relation, the limit of a derivation based on a redundancy +criterion is satisfiable if and only if the initial set is satisfiable. This material is partly +based on Section 4.1 of Bachmair and Ganzinger's \emph{Handbook} chapter, but adapted to the +saturation framework of Waldmann et al. +\ + +locale compact_consequence_relation = consequence_relation + + assumes + entails_compact: "CC \ Bot \ \CC' \ CC. finite CC' \ CC' \ Bot" +begin + +lemma chain_entails_derive_consist_preserving: + assumes + ent: "chain (\) Ns" and + n0_sat: "\ lhd Ns \ Bot" + shows "\ Sup_llist Ns \ Bot" +proof - + have bot_sat: "\ {} \ Bot" + using n0_sat by (meson empty_subsetI entails_trans subset_entailed) + + { + fix DD + assume fin: "finite DD" and sset_lun: "DD \ Sup_llist Ns" + then obtain k where + dd_sset: "DD \ Sup_upto_llist Ns (enat k)" + using finite_Sup_llist_imp_Sup_upto_llist by blast + have "\ Sup_upto_llist Ns (enat k) \ Bot" + proof (induct k) + case 0 + then show ?case + unfolding Sup_upto_llist_def + using lhd_conv_lnth[OF chain_not_lnull[OF ent], symmetric] n0_sat bot_sat by auto + next + case (Suc k) + show ?case + proof (cases "enat (Suc k) \ llength Ns") + case True + then have "Sup_upto_llist Ns (enat k) = Sup_upto_llist Ns (enat (Suc k))" + unfolding Sup_upto_llist_def using le_Suc_eq by auto + then show ?thesis + using Suc by simp + next + case False + then have entail_succ: "lnth Ns k \ lnth Ns (Suc k)" + using ent chain_lnth_rel by fastforce + from False have lt: "enat (Suc k) < llength Ns \ enat k < llength Ns" + by (meson Suc_ile_eq le_cases not_le) + have "{i. enat i < llength Ns \ i \ Suc k} = + {i. enat i < llength Ns \ i \ k} \ {i. enat i < llength Ns \ i = Suc k}" by auto + then have "Sup_upto_llist Ns (enat (Suc k)) = + Sup_upto_llist Ns (enat k) \ lnth Ns (Suc k)" + using lt unfolding Sup_upto_llist_def enat_ord_code(1) by blast + moreover have "Sup_upto_llist Ns k \ lnth Ns (Suc k)" + using entail_succ subset_entailed [of "lnth Ns k" "Sup_upto_llist Ns k"] lt + unfolding Sup_upto_llist_def by (simp add: entail_succ UN_upper entails_trans) + ultimately have "Sup_upto_llist Ns k \ Sup_upto_llist Ns (Suc k)" + using entail_union subset_entailed by fastforce + then show ?thesis using Suc.hyps using entails_trans by blast + qed + qed + then have "\ DD \ Bot" + using dd_sset entails_trans subset_entailed unfolding Sup_upto_llist_def by blast + } + then show ?thesis + using entails_compact by auto +qed + end + +locale refutationally_compact_calculus = calculus + compact_consequence_relation +begin + +text \ +The next three lemmas correspond to Lemma 4.2: +\ + +lemma Red_F_Sup_subset_Red_F_Liminf: + "chain (\Red) Ns \ Red_F (Sup_llist Ns) \ Red_F (Liminf_llist Ns)" + by (metis Liminf_llist_subset_Sup_llist Red_in_Sup Un_absorb1 calculus.Red_F_of_Red_F_subset + calculus_axioms double_diff sup_ge2) + +lemma Red_I_Sup_subset_Red_I_Liminf: + "chain (\Red) Ns \ Red_I (Sup_llist Ns) \ Red_I (Liminf_llist Ns)" + by (metis Liminf_llist_subset_Sup_llist Red_I_of_Red_F_subset Red_in_Sup double_diff subset_refl) + +lemma unsat_limit_iff: + assumes + chain_red: "chain (\Red) Ns" and + chain_ent: "chain (\) Ns" + shows "Liminf_llist Ns \ Bot \ lhd Ns \ Bot" +proof + assume "Liminf_llist Ns \ Bot" + then have "Sup_llist Ns \ Bot" + using Liminf_llist_subset_Sup_llist by (metis entails_trans subset_entailed) + then show "lhd Ns \ Bot" + using chain_ent chain_entails_derive_consist_preserving by blast +next + assume "lhd Ns \ Bot" + then have "Sup_llist Ns \ Bot" + by (meson chain_ent chain_not_lnull entails_trans lhd_subset_Sup_llist subset_entailed) + then have "Sup_llist Ns - Red_F (Sup_llist Ns) \ Bot" + using Red_F_Bot entail_set_all_formulas by blast + then show "Liminf_llist Ns \ Bot" + using entails_trans subset_entailed by (smt Diff_iff Red_in_Sup chain_red subset_eq) +qed + +text \Some easy consequences:\ + +lemma Red_F_limit_Sup: "chain (\Red) Ns \ Red_F (Liminf_llist Ns) = Red_F (Sup_llist Ns)" + by (metis Liminf_llist_subset_Sup_llist Red_F_of_Red_F_subset Red_F_of_subset Red_in_Sup + double_diff order_refl subset_antisym) + +lemma Red_I_limit_Sup: "chain (\Red) Ns \ Red_I (Liminf_llist Ns) = Red_I (Sup_llist Ns)" + by (metis Liminf_llist_subset_Sup_llist Red_I_of_Red_F_subset Red_I_of_subset Red_in_Sup + double_diff order_refl subset_antisym) + +end + +end