Theory Soundness

(*  Title:       Soundness
    Author:      Sophie Tourret <stourret at>, 2020
    Author:      Jasmin Blanchette <j.c.blanchette at>, 2014, 2017, 2020
    Author:      Dmitriy Traytel <traytel at>, 2014
    Author:      Anders Schlichtkrull <andschl at>, 2017

section ‹Soundness›

theory Soundness
  imports Saturation_Framework.Calculus

text ‹
Although consistency-preservation usually suffices, soundness is a more precise concept and is
sometimes useful.

locale sound_inference_system = inference_system + consequence_relation +
    sound: ι  Inf  set (prems_of ι)  {concl_of ι}

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


text ‹
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.

context calculus

text ‹
The next three lemmas correspond to Lemma 4.2:

lemma Red_F_Sup_subset_Red_F_Liminf:
  "chain (⊳) 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 (⊳) 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)

text ‹
Proof idea due to Uwe Waldmann:

lemma unsat_limit_iff:
    chain_red: "chain (⊳) Ns" and
    chain_ent: "chain (⊨) Ns"
  shows "Liminf_llist Ns  Bot  lhd Ns  Bot"
  assume "Liminf_llist Ns  Bot"
  moreover have "Sup_llist Ns  Liminf_llist Ns"
    by (simp add: Liminf_llist_subset_Sup_llist subset_entailed)
  moreover have "lhd Ns  Sup_llist Ns"
  proof -
    have "lhd Ns  lnth Ns i" if "i < llength Ns" for i
      using that
    proof (induct i)
      case 0
      then show ?case
        using chain_ent chain_not_lnull lhd_conv_lnth subset_entailed by fastforce
      case (Suc i)
      then show ?case
        using Suc_ile_eq chain_ent chain_lnth_rel entails_trans less_le by blast
    thus ?thesis
      unfolding Sup_llist_def using entail_unions by fastforce
  ultimately show "lhd Ns  Bot"
    using entails_trans by blast
  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 have "Liminf_llist Ns - Red_F (Sup_llist Ns)  Bot"
    by (smt Diff_idemp Diff_mono Diff_subset Liminf_llist_subset_Sup_llist
        Red_F_Sup_subset_Red_F_Liminf Red_F_of_subset Red_in_Sup antisym_conv chain_red double_diff
        entail_set_all_formulas order_refl order_trans subset_antisym)
  then show "Liminf_llist Ns  Bot"
    by (meson Diff_subset entails_trans subset_entailed)

text ‹Some easy consequences:›

lemma Red_F_limit_Sup: "chain (⊳) 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 (⊳) 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)