Theory Proving_Process

(*  Title:       Theorem Proving Processes
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
    Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
    Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
*)

section ‹Theorem Proving Processes›

theory Proving_Process
  imports Unordered_Ground_Resolution Lazy_List_Chain
begin

text ‹
This material corresponds to Section 4.1 (``Theorem Proving Processes'') of Bachmair and Ganzinger's
chapter.

The locale assumptions below capture conditions R1 to R3 of Definition 4.1.
Rf› denotes $\mathcal{R}_{\mathcal{F}}$; Ri› denotes $\mathcal{R}_{\mathcal{I}}$.
›

locale redundancy_criterion = inference_system +
  fixes
    Rf :: "'a clause set  'a clause set" and
    Ri :: "'a clause set  'a inference set"
  assumes
    Ri_subset_Γ: "Ri N  Γ" and
    Rf_mono: "N  N'  Rf N  Rf N'" and
    Ri_mono: "N  N'  Ri N  Ri N'" and
    Rf_indep: "N'  Rf N  Rf N  Rf (N - N')" and
    Ri_indep: "N'  Rf N  Ri N  Ri (N - N')" and
    Rf_sat: "satisfiable (N - Rf N)  satisfiable N"
begin

definition saturated_upto :: "'a clause set  bool" where
  "saturated_upto N  inferences_from (N - Rf N)  Ri N"

inductive "derive" :: "'a clause set  'a clause set  bool" (infix "" 50) where
  deduction_deletion: "N - M  concls_of (inferences_from M)  M - N  Rf N  M  N"

lemma derive_subset: "M  N  N  M  concls_of (inferences_from M)"
  by (meson Diff_subset_conv derive.cases)

end

locale sat_preserving_redundancy_criterion =
  sat_preserving_inference_system "Γ :: ('a :: wellorder) inference set" + redundancy_criterion
begin

lemma deriv_sat_preserving:
  assumes
    deriv: "chain (▹) Ns" and
    sat_n0: "satisfiable (lhd Ns)"
  shows "satisfiable (Sup_llist Ns)"
proof -
  have len_ns: "llength Ns > 0"
    using deriv by (case_tac Ns) simp+
  {
    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 "satisfiable (Sup_upto_llist Ns k)"
    proof (induct k)
      case 0
      then show ?case
        using len_ns sat_n0
        unfolding Sup_upto_llist_def true_clss_def lhd_conv_lnth[OF chain_not_lnull[OF deriv]]
        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 "lnth Ns k  lnth Ns (Suc k)"
          using deriv by (auto simp: chain_lnth_rel)
        then have "lnth Ns (Suc k)  lnth Ns k  concls_of (inferences_from (lnth Ns k))"
          by (rule derive_subset)
        moreover have "lnth Ns k  Sup_upto_llist Ns k"
          unfolding Sup_upto_llist_def using False Suc_ile_eq linear by blast
        ultimately have "lnth Ns (Suc k)
           Sup_upto_llist Ns k  concls_of (inferences_from (Sup_upto_llist Ns k))"
          by clarsimp (metis UnCI UnE image_Un inferences_from_mono le_iff_sup)
        moreover have "Sup_upto_llist Ns (Suc k) = Sup_upto_llist Ns k  lnth Ns (Suc k)"
          unfolding Sup_upto_llist_def using False by (force elim: le_SucE)
        moreover have
          "satisfiable (Sup_upto_llist Ns k  concls_of (inferences_from (Sup_upto_llist Ns k)))"
          using Suc Γ_sat_preserving unfolding sat_preserving_inference_system_def by simp
        ultimately show ?thesis
          by (metis le_iff_sup true_clss_union)
      qed
    qed
    then have "satisfiable DD"
      using dd_sset unfolding Sup_upto_llist_def by (blast intro: true_clss_mono)
  }
  then show ?thesis
    using ground_resolution_without_selection.clausal_logic_compact[THEN iffD1] by metis
qed

text ‹
This corresponds to Lemma 4.2:
›

lemma
  assumes deriv: "chain (▹) Ns"
  shows
    Rf_Sup_subset_Rf_Liminf: "Rf (Sup_llist Ns)  Rf (Liminf_llist Ns)" and
    Ri_Sup_subset_Ri_Liminf: "Ri (Sup_llist Ns)  Ri (Liminf_llist Ns)" and
    sat_limit_iff: "satisfiable (Liminf_llist Ns)  satisfiable (lhd Ns)"
proof -
  {
    fix C i j
    assume
      c_in: "C  lnth Ns i" and
      c_ni: "C  Rf (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  Rf (lnth Ns i)"
      using Rf_mono lnth_subset_Sup_llist Sup_llist_def by (blast dest: contra_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_in_k: "C  lnth Ns k"
          using Suc.hyps by blast
        have rel: "lnth Ns k  lnth Ns (Suc k)"
          using Suc.prems deriv by (auto simp: chain_lnth_rel)
        then show ?thesis
          using c_in_k c_ni' Suc.prems(2) by cases auto
      next
        case False
        then show ?thesis
          using Suc c_in by auto
      qed
    qed
  }
  then have lu_ll: "Sup_llist Ns - Rf (Sup_llist Ns)  Liminf_llist Ns"
    unfolding Sup_llist_def Liminf_llist_def by blast
  have rf: "Rf (Sup_llist Ns - Rf (Sup_llist Ns))  Rf (Liminf_llist Ns)"
    using lu_ll Rf_mono by simp
  have ri: "Ri (Sup_llist Ns - Rf (Sup_llist Ns))  Ri (Liminf_llist Ns)"
    using lu_ll Ri_mono by simp
  show "Rf (Sup_llist Ns)  Rf (Liminf_llist Ns)"
    using rf Rf_indep by blast
  show "Ri (Sup_llist Ns)  Ri (Liminf_llist Ns)"
    using ri Ri_indep by blast

  show "satisfiable (Liminf_llist Ns)  satisfiable (lhd Ns)"
  proof
    assume "satisfiable (lhd Ns)"
    then have "satisfiable (Sup_llist Ns)"
      using deriv deriv_sat_preserving by simp
    then show "satisfiable (Liminf_llist Ns)"
      using true_clss_mono[OF Liminf_llist_subset_Sup_llist] by blast
  next
    assume "satisfiable (Liminf_llist Ns)"
    then have "satisfiable (Sup_llist Ns - Rf (Sup_llist Ns))"
      using true_clss_mono[OF lu_ll] by blast
    then have "satisfiable (Sup_llist Ns)"
      using Rf_sat by blast
    then show "satisfiable (lhd Ns)"
      using deriv true_clss_mono lhd_subset_Sup_llist chain_not_lnull by metis
  qed
qed

lemma
  assumes "chain (▹) Ns"
  shows
    Rf_limit_Sup: "Rf (Liminf_llist Ns) = Rf (Sup_llist Ns)" and
    Ri_limit_Sup: "Ri (Liminf_llist Ns) = Ri (Sup_llist Ns)"
  using assms
  by (auto simp: Rf_Sup_subset_Rf_Liminf Rf_mono Ri_Sup_subset_Ri_Liminf Ri_mono
      Liminf_llist_subset_Sup_llist subset_antisym)

end

text ‹
The assumption below corresponds to condition R4 of Definition 4.1.
›

locale effective_redundancy_criterion = redundancy_criterion +
  assumes Ri_effective: "γ  Γ  concl_of γ  N  Rf N  γ  Ri N"
begin

definition fair_clss_seq :: "'a clause set llist  bool" where
  "fair_clss_seq Ns  (let N' = Liminf_llist Ns - Rf (Liminf_llist Ns) in
     concls_of (inferences_from N' - Ri N')  Sup_llist Ns  Rf (Sup_llist Ns))"

end

locale sat_preserving_effective_redundancy_criterion =
  sat_preserving_inference_system "Γ :: ('a :: wellorder) inference set" +
  effective_redundancy_criterion
begin

sublocale sat_preserving_redundancy_criterion
  ..

text ‹
The result below corresponds to Theorem 4.3.
›

theorem fair_derive_saturated_upto:
  assumes
    deriv: "chain (▹) Ns" and
    fair: "fair_clss_seq Ns"
  shows "saturated_upto (Liminf_llist Ns)"
  unfolding saturated_upto_def
proof
  fix γ
  let ?N' = "Liminf_llist Ns - Rf (Liminf_llist Ns)"
  assume γ: "γ  inferences_from ?N'"
  show "γ  Ri (Liminf_llist Ns)"
  proof (cases "γ  Ri ?N'")
    case True
    then show ?thesis
      using Ri_mono by blast
  next
    case False
    have "concls_of (inferences_from ?N' - Ri ?N')  Sup_llist Ns  Rf (Sup_llist Ns)"
      using fair unfolding fair_clss_seq_def Let_def .
    then have "concl_of γ  Sup_llist Ns  Rf (Sup_llist Ns)"
      using False γ by auto
    moreover
    {
      assume "concl_of γ  Sup_llist Ns"
      then have "γ  Ri (Sup_llist Ns)"
        using γ Ri_effective inferences_from_def by blast
      then have "γ  Ri (Liminf_llist Ns)"
        using deriv Ri_Sup_subset_Ri_Liminf by fast
    }
    moreover
    {
      assume "concl_of γ  Rf (Sup_llist Ns)"
      then have "concl_of γ  Rf (Liminf_llist Ns)"
        using deriv Rf_Sup_subset_Rf_Liminf by blast
      then have "γ  Ri (Liminf_llist Ns)"
        using γ Ri_effective inferences_from_def by auto
    }
    ultimately show "γ  Ri (Liminf_llist Ns)"
      by blast
  qed
qed

end

text ‹
This corresponds to the trivial redundancy criterion defined on page 36 of
Section 4.1.
›

locale trivial_redundancy_criterion = inference_system
begin

definition Rf :: "'a clause set  'a clause set" where
  "Rf _ = {}"

definition Ri :: "'a clause set  'a inference set" where
  "Ri N = {γ. γ  Γ  concl_of γ  N}"

sublocale effective_redundancy_criterion Γ Rf Ri
  by unfold_locales (auto simp: Rf_def Ri_def)

lemma saturated_upto_iff: "saturated_upto N  concls_of (inferences_from N)  N"
  unfolding saturated_upto_def inferences_from_def Rf_def Ri_def by auto

end

text ‹
The following lemmas corresponds to the standard extension of a redundancy criterion defined on
page 38 of Section 4.1.
›

lemma redundancy_criterion_standard_extension:
  assumes "Γ  Γ'" and "redundancy_criterion Γ Rf Ri"
  shows "redundancy_criterion Γ' Rf (λN. Ri N  (Γ' - Γ))"
  using assms unfolding redundancy_criterion_def by (intro conjI) ((auto simp: rev_subsetD)[5], sat)

lemma redundancy_criterion_standard_extension_saturated_upto_iff:
  assumes "Γ  Γ'" and "redundancy_criterion Γ Rf Ri"
  shows "redundancy_criterion.saturated_upto Γ Rf Ri M 
    redundancy_criterion.saturated_upto Γ' Rf (λN. Ri N  (Γ' - Γ)) M"
  using assms redundancy_criterion.saturated_upto_def redundancy_criterion.saturated_upto_def
    redundancy_criterion_standard_extension
  unfolding inference_system.inferences_from_def by blast

lemma redundancy_criterion_standard_extension_effective:
  assumes "Γ  Γ'" and "effective_redundancy_criterion Γ Rf Ri"
  shows "effective_redundancy_criterion Γ' Rf (λN. Ri N  (Γ' - Γ))"
  using assms redundancy_criterion_standard_extension[of Γ]
  unfolding effective_redundancy_criterion_def effective_redundancy_criterion_axioms_def by auto

lemma redundancy_criterion_standard_extension_fair_iff:
  assumes "Γ  Γ'" and "effective_redundancy_criterion Γ Rf Ri"
  shows "effective_redundancy_criterion.fair_clss_seq Γ' Rf (λN. Ri N  (Γ' - Γ)) Ns 
    effective_redundancy_criterion.fair_clss_seq Γ Rf Ri Ns"
  using assms redundancy_criterion_standard_extension_effective[of Γ Γ' Rf Ri]
    effective_redundancy_criterion.fair_clss_seq_def[of Γ Rf Ri Ns]
    effective_redundancy_criterion.fair_clss_seq_def[of Γ' Rf "(λN. Ri N  (Γ' - Γ))" Ns]
  unfolding inference_system.inferences_from_def Let_def by auto

theorem redundancy_criterion_standard_extension_fair_derive_saturated_upto:
  assumes
    subs: "Γ  Γ'" and
    red: "redundancy_criterion Γ Rf Ri" and
    red': "sat_preserving_effective_redundancy_criterion Γ' Rf (λN. Ri N  (Γ' - Γ))" and
    deriv: "chain (redundancy_criterion.derive Γ' Rf) Ns" and
    fair: "effective_redundancy_criterion.fair_clss_seq Γ' Rf (λN. Ri N  (Γ' - Γ)) Ns"
  shows "redundancy_criterion.saturated_upto Γ Rf Ri (Liminf_llist Ns)"
proof -
  have "redundancy_criterion.saturated_upto Γ' Rf (λN. Ri N  (Γ' - Γ)) (Liminf_llist Ns)"
    by (rule sat_preserving_effective_redundancy_criterion.fair_derive_saturated_upto
        [OF red' deriv fair])
  then show ?thesis
    by (rule redundancy_criterion_standard_extension_saturated_upto_iff[THEN iffD2, OF subs red])
qed

end