Theory FO_Ordered_Resolution_Prover_Revisited
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
no_notation RP (infix ‹↝› 50)
notation RP (infix ‹↝RP› 50)
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
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
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"
using G_Inf_have_prems G_Inf_reductive
by (unfold_locales) simp_all
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 𝒢_Fset :: ‹'a clause set ⇒ 'a clause set› where
‹𝒢_Fset ≡ grounding_of_clss›
lemmas 𝒢_F_def = grounding_of_cls_def
lemmas 𝒢_Fset_def = grounding_of_clss_def
definition 𝒢_I :: ‹'a clause set ⇒ 'a clause inference ⇒ 'a clause inference set› where
‹𝒢_I 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
𝒢_I_opt :: ‹'a clause set ⇒ 'a clause inference ⇒ 'a clause inference set option›
where
‹𝒢_I_opt M ι ≡ Some (𝒢_I 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" 𝒢_I_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 (𝒢_I_opt M)
(λD C C'. False)"
proof
fix M ι
show "the (𝒢_I_opt M ι) ⊆ G.Red_I M (𝒢_F (concl_of ι))"
unfolding option.sel
proof
fix ι'
assume "ι' ∈ 𝒢_I M ι"
then obtain ρ ρs where
ι': "ι' = Infer (prems_of ι ⋅⋅cl ρs) (concl_of ι ⋅ ρ)" and
ρ_gr: "is_ground_subst ρ" and
ρ_infer: "Infer (prems_of ι ⋅⋅cl ρs) (concl_of ι ⋅ ρ) ∈ G_Inf M"
unfolding 𝒢_I_def by blast
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:
"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 by auto
qed
lemma G_Inf_overapprox_F_Inf: "ι⇩0 ∈ G.Inf_from M (⋃ (𝒢_F ` M)) ⟹ ∃ι ∈ F.Inf_from M. ι⇩0 ∈ 𝒢_I M ι"
proof -
assume ι⇩0_in: "ι⇩0 ∈ G.Inf_from M (⋃ (𝒢_F ` M))"
have prems_ι⇩0_in: "set (prems_of ι⇩0) ⊆ ⋃ (𝒢_F ` M)"
using ι⇩0_in unfolding G.Inf_from_def by simp
note ι⇩0_G_Inf = G.Inf_if_Inf_from[OF ι⇩0_in]
then obtain CAs DA AAs As E where
gr_res: ‹gr.ord_resolve M CAs DA AAs As E› and
ι⇩0_is: ‹ι⇩0 = Infer (CAs @ [DA]) E›
unfolding G_Inf_def by auto
have CAs_in: ‹set CAs ⊆ set (prems_of ι⇩0)›
by (simp add: ι⇩0_is subsetI)
then have ground_CAs: ‹is_ground_cls_list CAs›
using prems_ι⇩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 ι⇩0)›
using ι⇩0_is by simp
then have ground_DA: ‹is_ground_cls DA›
using prems_ι⇩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 ⊆ 𝒢_Fset M›
using prems_ι⇩0_in CAs_in DA_in unfolding 𝒢_Fset_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 ι⇩0_is': "ι⇩0 = Infer ((CAs0 @ [DA0]) ⋅⋅cl (ηs @ [η])) (E0 ⋅ η2)"
unfolding ι⇩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. ι⇩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 ι⇩0_G_Inf[unfolded ι⇩0_is']
simp: ι⇩0_is' is_ground_subst_list_def›)
then have ‹ι⇩0 ∈ 𝒢_I M ι›
unfolding 𝒢_I_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. ι ∈ 𝒢_I N ι'}
∪ G.Red_I N (⋃ (𝒢_F ` N))"
using G_Inf_overapprox_F_Inf unfolding F.ground.Inf_from_q_def 𝒢_I_def by fastforce
qed
subsection ‹Labeled First-Order or Given Clause Layer›
datatype label = New | Processed | Old
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_iff_accp)
interpretation FL: given_clause "{{#}}" F_Inf "{{#}}" UNIV "λN. (⊫e)" G_Inf G.Red_I
"λN. G.Red_F" "λN. 𝒢_F" 𝒢_I_opt "(≐)" "(≺⋅)" "(⊏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: F_Inf_have_prems)
notation FL.Prec_FL (infix ‹⊏› 50)
notation FL.entails_𝒢_L (infix ‹⊫𝒢Le› 50)
notation FL.derive (infix ‹⊳L› 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
subsection ‹Resolution Prover 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_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)›
unfolding lclss_of_state_def using Liminf_llist_lmap_union Liminf_llist_lmap_image
by (smt Pair_inject Un_iff disjoint_iff_not_equal imageE inj_onI label.simps(1,3,5)
llist.map_cong)
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 "Neg (A ⋅a θ) ∈# Cθ" and "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 ‹{(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
qed (auto simp: lclss_of_state_def FL.active_subset_def)
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
qed (simp add: FL.active_subset_def)
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 ‹is_ground_subst σ›
then have ‹{fst Dl ⋅ σ} ⊆ {fst Dl ⋅ σ |σ. is_ground_subst σ}›
by blast
moreover have ‹fst Dl ⋅ σ < fst Cl ⋅ σ›
using subst_subset_mono[OF d_sub_c, of σ] 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_between 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_between N {C}"
unfolding F.Inf_between_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 mem_Collect_eq image_def)
qed
next
fix E
assume e_in: "E ∈ concl_of ` F.Inf_between 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_between_alt F.Inf_from_def F_Inf_def inference_system.Inf_between_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_between (fst ` FL.active_subset N) {C}"
using m_sup unfolding old_inferences_between_eq_new_inferences_between .
show "F.Inf_between (fst ` FL.active_subset N) {C} ⊆ F.Red_I (fst ` (N ∪ {(C, Old)} ∪ M))"
proof
fix ι
assume ι_in_if2: "ι ∈ F.Inf_between (fst ` FL.active_subset N) {C}"
note ι_in = F.Inf_if_Inf_between[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_between_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 ↝RP 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 (↝RP) 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 ↝RP St' ⟹ lclss_of_state St ⊳L lclss_of_state St'"
by (rule FL.one_step_equiv) (rule RP_step_imp_GC_step)
lemma RP_derivation_imp_derive_derivation:
"chain (↝RP) Sts ⟹ chain (⊳L) (lmap lclss_of_state Sts)"
using chain_lmap RP_step_imp_derive_step by blast
theorem RP_sound_new_statement:
assumes
deriv: "chain (↝RP) 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 ‹FL.entails_𝒢 (Liminf_llist (lmap lclss_of_state Sts)) ({{#}} × UNIV)›
moreover have ‹chain (⊳L) (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 𝒢_Fset_def
image_hd_lclss_of_state)
ultimately show ‹FL.entails_𝒢 (lhd (lmap lclss_of_state Sts)) ({{#}} × UNIV)›
using 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 (↝RP) 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 (↝RP) 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_lcls: "fst ` lhd (lmap lclss_of_state Sts) = lhd (lmap clss_of_state Sts)"
using len zero_enat_def by auto
have hd_unsat: "fst ` lhd (lmap lclss_of_state Sts) ⊫𝒢e {{#}}"
unfolding hd_lcls F_entails_𝒢_iff unfolding true_clss_def using unsat unfolding 𝒢_Fset_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)
have "∃BL ∈ {{#}} × UNIV. BL ∈ Liminf_llist (lmap lclss_of_state Sts)"
by (rule FL.gc_complete_Liminf[OF gc_deriv,of "{#}"])
(use final hd_unsat in ‹auto simp: init nnil›)
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)) = {}" and
"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 lclss_Liminf_commute lclss_of_state_def
by auto
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 ?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 using fin_dd dd_in dd_un all_dd
by simp (metis finite_set_mset_mset_set true_clss_set_mset)
qed (auto simp: src.redundant_infer_def)
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 n_empty: "N_of_state (Liminf_state Sts) = {}" and
p_empty: "P_of_state (Liminf_state Sts) = {}"
using no_passive[unfolded FL.passive_subset_def] Liminf_state_def lclss_Liminf_commute
by fastforce+
then have limuls_eq: "Liminf_llist (lmap lclss_of_state Sts) = Ql"
unfolding Ql_def Q_def using Liminf_state_def lclss_Liminf_commute lclss_of_state_def by auto
have clst_eq: "clss_of_state (Liminf_state Sts) = Q"
unfolding n_empty p_empty Q_def by (auto simp: Liminf_state_def)
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_ι': "ι ∈ 𝒢_I Q ι'"
using G_Inf_overapprox_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_FL"
using FL.Inf_F_to_Inf_FL[OF ι'_inf, of ?olds, simplified] by simp
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 𝒢_Fset_def)
qed
theorem RP_sound_old_statement:
assumes
deriv: "chain (↝RP) 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 𝒢_Fset_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 (↝RP) 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
by (rule saturated_imp_saturated_RP[OF _ fair'(2)], rule RP_saturated_if_fair_new_statement)
(rule deriv fair')+
qed
corollary RP_complete_if_fair_old_statement:
assumes
deriv: "chain (↝RP) 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 ‹𝒢_Fset (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 deriv old_fair_imp_new_fair[OF chain_not_lnull[OF deriv] fair empty_Q0])+
end
end