Theory More_Given_Clause_Architectures

(* Title:        More Lemmas about Given Clause Architectures 
   Authors:      Qi Qiu, 2021
                 Jasmin Blanchette <j.c.blanchette at vu.nl>, 2022-2023
   Maintainer:   Jasmin Blanchette <j.c.blanchette at vu.nl>
*)

section ‹More Lemmas about Given Clause Architectures›

text ‹This section proves lemmas about Tourret's formalization of the abstract
given clause procedures @{text GC} and @{text LGC}.›

theory More_Given_Clause_Architectures
  imports Saturation_Framework.Given_Clause_Architectures
begin


subsection ‹Inference System›

context inference_system
begin

lemma Inf_from_empty: "Inf_from {} = {ι ∈ Inf. prems_of ι = []}"
  using Inf_from_def by auto

end


subsection ‹Given Clause Procedure Basis›

context given_clause_basis
begin

lemma no_labels_entails_mono_left: "M ⊆ N ⟹ M ⊨∩𝒢 P ⟹ N ⊨∩𝒢 P"
  using no_labels.entails_trans no_labels.subset_entailed by blast

lemma no_labels_Red_F_imp_Red_F:
  assumes "C ∈ no_labels.Red_F (fst ` 𝒩)"
  shows "(C, l) ∈ Red_F 𝒩 "
proof -
  let ?N = "fst ` 𝒩"
  have c_in_red_f_g_q: "∀q ∈ Q. C ∈ no_labels.Red_F_𝒢_q q ?N"
    using no_labels.Red_F_def assms by auto
  moreover have redfgq_eq_redfeq:
    "∀q ∈ Q. no_labels.Red_F_𝒢_q q ?N = no_labels.Red_F_𝒢_empty_q q ?N"
    using no_labels.Red_F_𝒢_empty_q_def no_labels.Red_F_𝒢_q_def by auto
  ultimately have "∀q ∈ Q. C ∈ no_labels.Red_F_𝒢_empty_q q ?N"
    by simp
  then have "∀q ∈ Q. 𝒢_F_q q C ⊆ Red_F_q q (no_labels.𝒢_Fset_q q ?N)"
    using redfgq_eq_redfeq no_labels.Red_F_𝒢_q_def by auto
  moreover have "∀q ∈ Q. 𝒢_F_L_q q (C, l) = 𝒢_F_q q C"
    by simp
  moreover have "∀q ∈ Q. no_labels.𝒢_Fset_q q ?N = 𝒢_Fset_q q 𝒩"
    by auto
  ultimately have "∀q ∈ Q. 𝒢_F_L_q q (C, l) ⊆ Red_F_q q (𝒢_Fset_L_q q 𝒩)"
    by auto
  then have "∀q ∈ Q. (C, l) ∈ Red_F_𝒢_q q 𝒩"
    using c_in_red_f_g_q Red_F_𝒢_q_def by force
  then show "(C, l) ∈ Red_F 𝒩"
    using Red_F_def by simp
qed

lemma succ_F_imp_Red_F:
  assumes
    "C' ∈ fst ` 𝒩" and
    "C' ≺⋅ C"
  shows "(C, l) ∈ Red_F 𝒩"
proof -
  have "∃l'. (C', l') ∈ 𝒩"
    using assms by auto
  then obtain l' where
    c'_l'_in: "(C', l') ∈ 𝒩"
    by auto
  then have c'_l'_ls_c_l: "(C', l') ⊏ (C, l)"
    using assms Prec_FL_def by simp
  moreover have g_f_q_included: "∀q ∈ Q. 𝒢_F_q q C ⊆  𝒢_F_q q C'"
    using assms prec_F_grounding by simp
  ultimately have "∀q ∈ Q. 𝒢_F_L_q q (C, l) ⊆ 𝒢_F_L_q q (C, l)"
    by auto
  then have "∀q ∈ Q. (C, l) ∈ Red_F_𝒢_q q 𝒩"
    using c'_l'_in c'_l'_ls_c_l g_f_q_included Red_F_𝒢_q_def by fastforce
  thus " (C, l) ∈ Red_F 𝒩 "
    using Red_F_def by auto
qed

lemma succ_L_imp_Red_F:
  assumes
    "(C', l') ∈ 𝒩" and
    "C' ≼⋅ C" and
    "l' ⊏L l"
  shows "(C, l) ∈ Red_F 𝒩"
proof -
  have c'_l'_ls_c_l: "(C', l') ⊏ (C, l)"
    using Prec_FL_def assms by auto
  have c'_le_c: "C' ≼⋅ C"
    using assms by simp
  then show "(C, l) ∈ Red_F 𝒩"
  proof
    assume c'_ls_c: " C' ≺⋅ C "
    have "C' ∈ fst ` 𝒩"
      by (metis assms(1) eq_fst_iff rev_image_eqI)
     then show ?thesis
      using c'_ls_c succ_F_imp_Red_F by blast
  next
    assume c'_eq_c: " C' ≐ C "
    have c_eq_c': "C ≐ C'"
      using c'_eq_c equiv_equiv_F equivp_symp by force
    have "∀q ∈ Q. 𝒢_F_q q C' = 𝒢_F_q q C"
      using c'_eq_c c_eq_c' equiv_F_grounding subset_antisym by auto
    then have "∀q ∈ Q. 𝒢_F_L_q q (C, l) = 𝒢_F_L_q q (C', l')" by auto
    then have "∀q ∈ Q. (C, l) ∈ Red_F_𝒢_q q 𝒩"
      using assms(1) c'_l'_ls_c_l Red_F_𝒢_q_def by auto
    then show ?thesis
      using Red_F_def by auto
  qed
qed

lemma prj_fl_set_to_f_set_distr_union [simp]: "fst ` (ℳ ∪ 𝒩) = fst ` ℳ ∪ fst ` 𝒩"
  by (rule Set.image_Un)

lemma prj_labeledN_eq_N [simp]: "fst ` {(C, l) | C. C ∈ N} = N"
proof -
  let ?𝒩 = "{(C, l) | C. C ∈ N}"
  have "fst` ?𝒩 = N"
    proof
      show "fst` ?𝒩 ⊆ N"
        by fastforce
    next
      show "fst` ?𝒩 ⊇ N"
      proof
        fix x
        assume "x ∈ N"
        then have "(x, l) ∈ ?𝒩"
          by auto
        then show "x ∈ fst` ?𝒩"
          by force
      qed
    qed
    then show "fst` ?𝒩 = N"
      by simp
qed

end


subsection ‹Given Clause Procedure›

context given_clause
begin

lemma remove_redundant:
  assumes "(C, l) ∈ Red_F 𝒩"
  shows "𝒩 ∪ {(C, l)} ↝GC 𝒩"
proof -
  have "{(C, l)} ⊆ Red_F (𝒩 ∪ {})"
    using assms by simp
  moreover have "active_subset {} = {}"
    using active_subset_def by simp
  ultimately show "𝒩 ∪ {(C, l)} ↝GC 𝒩"
    by (metis process sup_bot_right)
qed

lemma remove_redundant_no_label:
  assumes " C ∈ no_labels.Red_F (fst ` 𝒩)"
  shows "𝒩 ∪ {(C, l)} ↝GC 𝒩"
proof -
  have "(C, l) ∈ Red_F 𝒩"
    using no_labels_Red_F_imp_Red_F assms by simp
  then show ?thesis
    using remove_redundant by auto
qed

lemma add_inactive:
  assumes "l ≠ active"
  shows "𝒩 ↝GC 𝒩 ∪ {(C, l)}"
proof -
  have active_subset_C_l: "active_subset {(C, l)} = {}"
    using active_subset_def assms by simp
  also have "{} ⊆ Red_F (𝒩 ∪ {(C, l)})"
    by simp
  finally show "𝒩 ↝GC 𝒩 ∪ {(C, l)}"
    by (metis active_subset_C_l process sup_bot.right_neutral)
qed

lemma remove_succ_F:
  assumes
    "(C', l') ∈ 𝒩" and
    "C' ≺⋅ C"
  shows "𝒩 ∪ {(C, l)} ↝GC 𝒩"
proof -
  have "C' ∈ fst ` 𝒩"
    by (metis assms(1) fst_conv rev_image_eqI)
  then have "{(C, l)} ⊆ Red_F (𝒩)"
    using assms succ_F_imp_Red_F by auto
  then show ?thesis
    using remove_redundant by simp
qed

lemma remove_succ_L:
  assumes
    "(C', l') ∈ 𝒩" and
    "C' ≼⋅ C" and
    "l' ⊏L l"
  shows "𝒩 ∪ {(C, l)} ↝GC 𝒩"
proof -
  have "(C, l) ∈ Red_F 𝒩"
    using assms succ_L_imp_Red_F by auto
  then show "𝒩 ∪ {(C, l)} ↝GC 𝒩"
    using remove_redundant by auto
qed

lemma relabel_inactive:
  assumes
    "l' ⊏L l" and
    "l' ≠ active"
  shows "𝒩 ∪ {(C, l)} ↝GC 𝒩 ∪ {(C, l')}"
proof -
  have active_subset_c_l': "active_subset {(C, l')} = {}"
    using active_subset_def assms by auto

  have "C ≐ C "
    by (simp add: equiv_equiv_F equivp_reflp)
  moreover have "(C, l') ∈ 𝒩 ∪ {(C, l')} "
    by auto
  ultimately have "(C, l) ∈ Red_F (𝒩 ∪ {(C, l')})"
    using assms succ_L_imp_Red_F[of _ _ "𝒩 ∪ {(C, l')}"] by auto
  then have "{(C, l)} ⊆ Red_F (𝒩 ∪ {(C, l')})"
    by auto

  then show "𝒩 ∪ {(C, l)} ↝GC 𝒩 ∪ {(C, l')}"
    using active_subset_c_l' process[of _ _ "{(C, l)}" _ "{(C, l')}"] by auto
qed

end


subsection ‹Lazy Given Clause Procedure›

context lazy_given_clause
begin

lemma remove_redundant:
  assumes "(C, l) ∈ Red_F 𝒩"
  shows "(T, 𝒩 ∪ {(C, l)}) ↝LGC (T, 𝒩)"
proof -
  have "{(C, l)} ⊆ Red_F 𝒩"
    using assms by simp
  moreover have "active_subset {} = {}"
    using active_subset_def by simp
  ultimately show "(T, 𝒩 ∪ {(C, l)}) ↝LGC (T, 𝒩)"
    by (metis process sup_bot_right)
qed

lemma remove_redundant_no_label:
  assumes "C ∈ no_labels.Red_F (fst ` 𝒩)"
  shows "(T, 𝒩 ∪ {(C, l)}) ↝LGC (T, 𝒩)"
proof -
  have "(C, l) ∈ Red_F 𝒩"
    using no_labels_Red_F_imp_Red_F assms by simp
  then show "(T, 𝒩 ∪ {(C, l)}) ↝LGC (T, 𝒩)"
    using remove_redundant by auto
qed

lemma add_inactive:
  assumes "l ≠ active"
  shows "(T, 𝒩) ↝LGC (T, 𝒩 ∪ {(C, l)})"
proof -
  have active_subset_C_l: "active_subset {(C, l)} = {}"
    using active_subset_def assms by simp
  also have "{} ⊆ Red_F (𝒩 ∪ {(C, l)})"
    by simp
  finally show "(T, 𝒩) ↝LGC (T, 𝒩 ∪ {(C, l)})"
    by (metis active_subset_C_l process sup_bot.right_neutral)
qed

lemma remove_succ_F:
  assumes
    "(C', l') ∈ 𝒩" and
    "C' ≺⋅ C"
  shows "(T, 𝒩 ∪ {(C, l)}) ↝LGC (T, 𝒩)"
proof -
  have "C' ∈ fst ` 𝒩"
    by (metis assms(1) fst_conv rev_image_eqI)
  then have "{(C, l)} ⊆ Red_F (𝒩)"
    using assms succ_F_imp_Red_F by auto
  then show ?thesis
    using remove_redundant by simp
qed

lemma remove_succ_L:
  assumes
    "(C', l') ∈ 𝒩" and
    "C' ≼⋅ C" and
    "l' ⊏L l"
  shows "(T, 𝒩 ∪ {(C, l)}) ↝LGC (T, 𝒩)"
proof -
  have "(C, l) ∈ Red_F 𝒩"
    using assms succ_L_imp_Red_F by auto
  then show "(T, 𝒩 ∪ {(C, l)}) ↝LGC (T, 𝒩)"
    using remove_redundant by auto
qed

lemma relabel_inactive:
  assumes
    "l' ⊏L l" and
    "l' ≠ active"
  shows "(T, 𝒩 ∪ {(C, l)}) ↝LGC (T, 𝒩 ∪ {(C, l')})"
proof -
  have active_subset_c_l': "active_subset {(C, l')} = {}"
    using active_subset_def assms by auto

  have "C ≐ C "
    by (simp add: equiv_equiv_F equivp_reflp)
  moreover have "(C, l') ∈ 𝒩 ∪ {(C, l')} "
    by auto
  ultimately have "(C, l) ∈ Red_F (𝒩 ∪ {(C, l')})"
    using assms succ_L_imp_Red_F[of _ _ "𝒩 ∪ {(C, l')}"] by auto
  then have "{(C, l)} ⊆ Red_F (𝒩 ∪ {(C, l')})"
    by auto

  then show "(T, 𝒩 ∪ {(C, l)}) ↝LGC (T, 𝒩 ∪ {(C, l')})"
    using active_subset_c_l' process[of _ _ "{(C, l)}" _ "{(C, l')}"] by auto
qed

end

end