Theory Saturation_Framework.Calculus

(*  Title:       Calculi Based on a Redundancy Criterion
 *  Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2018-2020 *)

section ‹Calculi Based on a Redundancy Criterion›

text ‹This section introduces the most basic notions upon which the framework is
  built: consequence relations and inference systems. It also defines the notion
  of a family of consequence relations and of redundancy criteria. This
  corresponds to sections 2.1 and 2.2 of the report.›

theory Calculus
  imports
    Ordered_Resolution_Prover.Lazy_List_Liminf
    Ordered_Resolution_Prover.Lazy_List_Chain
begin


subsection ‹Consequence Relations›

locale consequence_relation =
  fixes
    Bot :: "'f set" and
    entails :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨" 50)
  assumes
    bot_not_empty: "Bot ≠ {}" and
    bot_entails_all: "B ∈ Bot ⟹ {B} ⊨ N1" and
    subset_entailed: "N2 ⊆ N1 ⟹ N1 ⊨ N2" and
    all_formulas_entailed: "(∀C ∈ N2. N1 ⊨ {C}) ⟹ N1 ⊨ N2" and
    entails_trans[trans]: "N1 ⊨ N2 ⟹ N2 ⊨ N3 ⟹ N1 ⊨ N3"
begin

lemma entail_set_all_formulas: "N1 ⊨ N2 ⟷ (∀C ∈ N2. N1 ⊨ {C})"
  by (meson all_formulas_entailed empty_subsetI insert_subset subset_entailed entails_trans)

lemma entail_union: "N ⊨ N1 ∧ N ⊨ N2 ⟷ N ⊨ N1 ∪ N2"
  using entail_set_all_formulas[of N N1] entail_set_all_formulas[of N N2]
    entail_set_all_formulas[of N "N1 ∪ N2"] by blast

lemma entail_unions: "(∀i ∈ I. N ⊨ Ni i) ⟷ N ⊨ ⋃ (Ni ` I)"
  using entail_set_all_formulas[of N "⋃ (Ni ` I)"] entail_set_all_formulas[of N]
    Complete_Lattices.UN_ball_bex_simps(2)[of Ni I "λC. N ⊨ {C}", symmetric]
  by meson

lemma entail_all_bot: "(∃B ∈ Bot. N ⊨ {B}) ⟹ ∀B' ∈ Bot. N ⊨ {B'}"
  using bot_entails_all entails_trans by blast

lemma entails_trans_strong: "N1 ⊨ N2 ⟹ N1 ∪ N2 ⊨ N3 ⟹ N1 ⊨ N3"
  by (meson entail_union entails_trans order_refl subset_entailed)

end


subsection ‹Families of Consequence Relations›

locale consequence_relation_family =
  fixes
    Bot :: "'f set" and
    Q :: "'q set" and
    entails_q :: "'q ⇒ 'f set ⇒ 'f set ⇒ bool"
  assumes
    Q_nonempty: "Q ≠ {}" and
    q_cons_rel: "∀q ∈ Q. consequence_relation Bot (entails_q q)"
begin

lemma bot_not_empty: "Bot ≠ {}"
  using Q_nonempty consequence_relation.bot_not_empty consequence_relation_family.q_cons_rel
    consequence_relation_family_axioms by blast

definition entails :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨Q" 50) where
  "N1 ⊨Q N2 ⟷ (∀q ∈ Q. entails_q q N1 N2)"

(* lem:intersection-of-conseq-rel *)
lemma intersect_cons_rel_family: "consequence_relation Bot entails"
  unfolding consequence_relation_def entails_def
  by (intro conjI bot_not_empty) (metis consequence_relation_def q_cons_rel)+

end


subsection ‹Inference Systems›

datatype 'f inference =
  Infer (prems_of: "'f list") (concl_of: "'f")

locale inference_system =
  fixes
    Inf :: ‹'f inference set›
begin

definition Inf_from :: "'f set ⇒ 'f inference set" where
  "Inf_from N = {ι ∈ Inf. set (prems_of ι) ⊆ N}"

definition Inf_between :: "'f set ⇒ 'f set ⇒ 'f inference set" where
  "Inf_between N M = Inf_from (N ∪ M) - Inf_from (N - M)"

lemma Inf_if_Inf_from: "ι ∈ Inf_from N ⟹ ι ∈ Inf"
  unfolding Inf_from_def by simp

lemma Inf_if_Inf_between: "ι ∈ Inf_between N M ⟹ ι ∈ Inf"
  unfolding Inf_between_def Inf_from_def by simp

lemma Inf_between_alt:
  "Inf_between N M = {ι ∈ Inf. ι ∈ Inf_from (N ∪ M) ∧ set (prems_of ι) ∩ M ≠ {}}"
  unfolding Inf_from_def Inf_between_def by auto

lemma Inf_from_mono: "N ⊆ N' ⟹ Inf_from N ⊆ Inf_from N'"
  unfolding Inf_from_def by auto

lemma Inf_between_mono: "N ⊆ N' ⟹ M ⊆ M' ⟹ Inf_between N M ⊆ Inf_between N' M'"
  unfolding Inf_between_alt using Inf_from_mono[of "N ∪ M" "N' ∪ M'"] by auto

end


subsection ‹Families of Inference Systems›

locale inference_system_family =
  fixes
    Q :: "'q set" and
    Inf_q :: "'q ⇒ 'f inference set"
  assumes
    Q_nonempty: "Q ≠ {}"
begin

definition Inf_from_q :: "'q ⇒ 'f set ⇒ 'f inference set" where
  "Inf_from_q q = inference_system.Inf_from (Inf_q q)"

definition Inf_between_q :: "'q ⇒ 'f set ⇒ 'f set ⇒ 'f inference set" where
  "Inf_between_q q = inference_system.Inf_between (Inf_q q)"

lemma Inf_between_q_alt:
  "Inf_between_q q N M = {ι ∈ Inf_q q. ι ∈ Inf_from_q q (N ∪ M) ∧ set (prems_of ι) ∩ M ≠ {}}"
  unfolding Inf_from_q_def Inf_between_q_def inference_system.Inf_between_alt by auto

end


subsection ‹Calculi Based on a Single Redundancy Criterion›

locale calculus = inference_system Inf + consequence_relation Bot entails
  for
    Bot :: "'f set" and
    Inf :: ‹'f inference set› and
    entails :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨" 50)
  + fixes
    Red_I :: "'f set ⇒ 'f inference set" and
    Red_F :: "'f set ⇒ 'f set"
  assumes
    Red_I_to_Inf: "Red_I N ⊆ Inf" and
    Red_F_Bot: "B ∈ Bot ⟹ N ⊨ {B} ⟹ N - Red_F N ⊨ {B}" and
    Red_F_of_subset: "N ⊆ N' ⟹ Red_F N ⊆ Red_F N'" and
    Red_I_of_subset: "N ⊆ N' ⟹ Red_I N ⊆ Red_I N'" and
    Red_F_of_Red_F_subset: "N' ⊆ Red_F N ⟹ Red_F N ⊆ Red_F (N - N')" and
    Red_I_of_Red_F_subset: "N' ⊆ Red_F N ⟹ Red_I N ⊆ Red_I (N - N')" and
    Red_I_of_Inf_to_N: "ι ∈ Inf ⟹ concl_of ι ∈ N ⟹ ι ∈ Red_I N"
begin

lemma Red_I_of_Inf_to_N_subset: "{ι ∈ Inf. concl_of ι ∈ N} ⊆ Red_I N"
  using Red_I_of_Inf_to_N by blast

(* lem:red-concl-implies-red-inf *)
lemma red_concl_to_red_inf:
  assumes
    i_in: "ι ∈ Inf" and
    concl: "concl_of ι ∈ Red_F N"
  shows "ι ∈ Red_I N"
proof -
  have "ι ∈ Red_I (Red_F N)" by (simp add: Red_I_of_Inf_to_N i_in concl)
  then have i_in_Red: "ι ∈ Red_I (N ∪ Red_F N)" by (simp add: Red_I_of_Inf_to_N concl i_in)
  have red_n_subs: "Red_F N ⊆ Red_F (N ∪ Red_F N)" by (simp add: Red_F_of_subset)
  then have "ι ∈ Red_I ((N ∪ Red_F N) - (Red_F N - N))" using Red_I_of_Red_F_subset i_in_Red
    by (meson Diff_subset subsetCE subset_trans)
  then show ?thesis by (metis Diff_cancel Diff_subset Un_Diff Un_Diff_cancel contra_subsetD
    calculus.Red_I_of_subset calculus_axioms sup_bot.right_neutral)
qed

definition saturated :: "'f set ⇒ bool" where
  "saturated N ⟷ Inf_from N ⊆ Red_I N"

definition reduc_saturated :: "'f set ⇒ bool" where
  "reduc_saturated N ⟷ Inf_from (N - Red_F N) ⊆ Red_I N"

lemma Red_I_without_red_F:
  "Red_I (N - Red_F N) = Red_I N"
  using Red_I_of_subset [of "N - Red_F N" N]
    and Red_I_of_Red_F_subset [of "Red_F N" N] by blast

lemma saturated_without_red_F:
  assumes saturated: "saturated N"
  shows "saturated (N - Red_F N)"
proof -
  have "Inf_from (N - Red_F N) ⊆ Inf_from N" unfolding Inf_from_def by auto
  also have "Inf_from N ⊆ Red_I N" using saturated unfolding saturated_def by auto
  also have "Red_I N ⊆ Red_I (N - Red_F N)" using Red_I_of_Red_F_subset by auto
  finally have "Inf_from (N - Red_F N) ⊆ Red_I (N - Red_F N)" by auto
  then show ?thesis unfolding saturated_def by auto
qed

definition fair :: "'f set llist ⇒ bool" where
  "fair Ns ⟷ Inf_from (Liminf_llist Ns) ⊆ Sup_llist (lmap Red_I Ns)"

inductive "derive" :: "'f set ⇒ 'f set ⇒ bool" (infix "⊳" 50) where
  derive: "M - N ⊆ Red_F N ⟹ M ⊳ N"

lemma gt_Max_notin: ‹finite A ⟹ A ≠ {} ⟹ x > Max A ⟹ x ∉ A› by auto

lemma equiv_Sup_Liminf:
  assumes
    in_Sup: "C ∈ Sup_llist Ns" and
    not_in_Liminf: "C ∉ Liminf_llist Ns"
  shows
    "∃i ∈ {i. enat (Suc i) < llength Ns}. C ∈ lnth Ns i - lnth Ns (Suc i)"
proof -
  obtain i where C_D_i: "C ∈ Sup_upto_llist Ns (enat i)" and "enat i < llength Ns"
    using elem_Sup_llist_imp_Sup_upto_llist in_Sup by fast
  then obtain j where j: "j ≥ i ∧ enat j < llength Ns ∧ C ∉ lnth Ns j"
    using not_in_Liminf unfolding Sup_upto_llist_def chain_def Liminf_llist_def by auto
  obtain k where k: "C ∈ lnth Ns k" "enat k < llength Ns" "k ≤ i" using C_D_i
    unfolding Sup_upto_llist_def by auto
  let ?S = "{i. i < j ∧ i ≥ k ∧ C ∈ lnth Ns i}"
  define l where "l = Max ?S"
  have ‹k ∈ {i. i < j ∧ k ≤ i ∧ C ∈ lnth Ns i}› using k j by (auto simp: order.order_iff_strict)
  then have nempty: "{i. i < j ∧ k ≤ i ∧ C ∈ lnth Ns i} ≠ {}" by auto
  then have l_prop: "l < j ∧ l ≥ k ∧ C ∈ lnth Ns l" using Max_in[of ?S, OF _ nempty]
    unfolding l_def by auto
  then have "C ∈ lnth Ns l - lnth Ns (Suc l)" using j gt_Max_notin[OF _ nempty, of "Suc l"]
    unfolding l_def[symmetric] by (auto intro: Suc_lessI)
  then show ?thesis
  proof (rule bexI[of _ l])
    show "l ∈ {i. enat (Suc i) < llength Ns}"
      using l_prop j
      by (clarify, metis Suc_leI dual_order.order_iff_strict enat_ord_simps(2) less_trans)
  qed
qed

(* lem:nonpersistent-is-redundant *)
lemma Red_in_Sup:
  assumes deriv: "chain (⊳) Ns"
  shows "Sup_llist Ns - Liminf_llist Ns ⊆ Red_F (Sup_llist Ns)"
proof
  fix C
  assume C_in_subset: "C ∈ Sup_llist Ns - Liminf_llist Ns"
  {
    fix C i
    assume
      in_ith_elem: "C ∈ lnth Ns i - lnth Ns (Suc i)" and
      i: "enat (Suc i) < llength Ns"
    have "lnth Ns i ⊳ lnth Ns (Suc i)" using i deriv in_ith_elem chain_lnth_rel by auto
    then have "C ∈ Red_F (lnth Ns (Suc i))" using in_ith_elem derive.cases by blast
    then have "C ∈ Red_F (Sup_llist Ns)" using Red_F_of_subset
      by (meson contra_subsetD i lnth_subset_Sup_llist)
  }
  then show "C ∈ Red_F (Sup_llist Ns)" using equiv_Sup_Liminf[of C] C_in_subset by fast
qed

(* lem:redundant-remains-redundant-during-run 1/2 *)
lemma Red_I_subset_Liminf:
  assumes deriv: ‹chain (⊳) Ns› and
    i: ‹enat i < llength Ns›
  shows ‹Red_I (lnth Ns i) ⊆ Red_I (Liminf_llist Ns)›
proof -
  have Sup_in_diff: ‹Red_I (Sup_llist Ns) ⊆ Red_I (Sup_llist Ns - (Sup_llist Ns - Liminf_llist Ns))›
    using Red_I_of_Red_F_subset[OF Red_in_Sup] deriv by auto
  also have ‹Sup_llist Ns - (Sup_llist Ns - Liminf_llist Ns) = Liminf_llist Ns›
    by (simp add: Liminf_llist_subset_Sup_llist double_diff)
  then have Red_I_Sup_in_Liminf: ‹Red_I (Sup_llist Ns) ⊆ Red_I (Liminf_llist Ns)›
    using Sup_in_diff by auto
  have ‹lnth Ns i ⊆ Sup_llist Ns› unfolding Sup_llist_def using i by blast
  then have "Red_I (lnth Ns i) ⊆ Red_I (Sup_llist Ns)" using Red_I_of_subset
    unfolding Sup_llist_def by auto
  then show ?thesis using Red_I_Sup_in_Liminf by auto
qed

(* lem:redundant-remains-redundant-during-run 2/2 *)
lemma Red_F_subset_Liminf:
  assumes deriv: ‹chain (⊳) Ns› and
    i: ‹enat i < llength Ns›
  shows ‹Red_F (lnth Ns i) ⊆ Red_F (Liminf_llist Ns)›
proof -
  have Sup_in_diff: ‹Red_F (Sup_llist Ns) ⊆ Red_F (Sup_llist Ns - (Sup_llist Ns - Liminf_llist Ns))›
    using Red_F_of_Red_F_subset[OF Red_in_Sup] deriv by auto
  also have ‹Sup_llist Ns - (Sup_llist Ns - Liminf_llist Ns) = Liminf_llist Ns›
    by (simp add: Liminf_llist_subset_Sup_llist double_diff)
  then have Red_F_Sup_in_Liminf: ‹Red_F (Sup_llist Ns) ⊆ Red_F (Liminf_llist Ns)›
    using Sup_in_diff by auto
  have ‹lnth Ns i ⊆ Sup_llist Ns› unfolding Sup_llist_def using i by blast
  then have "Red_F (lnth Ns i) ⊆ Red_F (Sup_llist Ns)" using Red_F_of_subset
    unfolding Sup_llist_def by auto
  then show ?thesis using Red_F_Sup_in_Liminf by auto
qed

(* lem:N-i-is-persistent-or-redundant *)
lemma i_in_Liminf_or_Red_F:
  assumes
    deriv: ‹chain (⊳) Ns› and
    i: ‹enat i < llength Ns›
  shows ‹lnth Ns i ⊆ Red_F (Liminf_llist Ns) ∪ Liminf_llist Ns›
proof (rule,rule)
  fix C
  assume C: ‹C ∈ lnth Ns i›
  and C_not_Liminf: ‹C ∉ Liminf_llist Ns›
  have ‹C ∈ Sup_llist Ns› unfolding Sup_llist_def using C i by auto
  then obtain j where j: ‹C ∈ lnth Ns j - lnth Ns (Suc j)› ‹enat (Suc j) < llength Ns›
    using equiv_Sup_Liminf[of C Ns] C_not_Liminf by auto
  then have ‹C ∈ Red_F (lnth Ns (Suc j))›
    using deriv by (meson chain_lnth_rel contra_subsetD derive.cases)
  then show ‹C ∈ Red_F (Liminf_llist Ns)› using Red_F_subset_Liminf[of Ns "Suc j"] deriv j(2) by blast
qed

(* lem:fairness-implies-saturation *)
lemma fair_implies_Liminf_saturated:
  assumes
    deriv: ‹chain (⊳) Ns› and
    fair: ‹fair Ns›
  shows ‹saturated (Liminf_llist Ns)›
  unfolding saturated_def
proof
  fix ι
  assume ι: ‹ι ∈ Inf_from (Liminf_llist Ns)›
  have ‹ι ∈ Sup_llist (lmap Red_I Ns)› using fair ι unfolding fair_def by auto
  then obtain i where i: ‹enat i < llength Ns› ‹ι ∈ Red_I (lnth Ns i)›
    unfolding Sup_llist_def by auto
  then show ‹ι ∈ Red_I (Liminf_llist Ns)›
    using deriv i_in_Liminf_or_Red_F[of Ns i] Red_I_subset_Liminf by blast
qed

end

locale statically_complete_calculus = calculus +
  assumes statically_complete: "B ∈ Bot ⟹ saturated N ⟹ N ⊨ {B} ⟹ ∃B'∈Bot. B' ∈ N"
begin

lemma dynamically_complete_Liminf:
  fixes B Ns
  assumes
    bot_elem: ‹B ∈ Bot› and
    deriv: ‹chain (⊳) Ns› and
    fair: ‹fair Ns› and
    unsat: ‹lhd Ns ⊨ {B}›
  shows ‹∃B'∈Bot. B' ∈ Liminf_llist Ns›
proof -
  note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]]
  have non_empty: ‹¬ lnull Ns› using chain_not_lnull[OF deriv] .
  have subs: ‹lhd Ns ⊆ Sup_llist Ns›
    using lhd_subset_Sup_llist[of Ns] non_empty by (simp add: lhd_conv_lnth)
  have ‹Sup_llist Ns ⊨ {B}›
    using unsat subset_entailed[OF subs] entails_trans[of "Sup_llist Ns" "lhd Ns"] by auto
  then have Sup_no_Red: ‹Sup_llist Ns - Red_F (Sup_llist Ns) ⊨ {B}›
    using bot_elem Red_F_Bot by auto
  have Sup_no_Red_in_Liminf: ‹Sup_llist Ns - Red_F (Sup_llist Ns) ⊆ Liminf_llist Ns›
    using deriv Red_in_Sup by auto
  have Liminf_entails_Bot: ‹Liminf_llist Ns ⊨ {B}›
    using Sup_no_Red subset_entailed[OF Sup_no_Red_in_Liminf] entails_trans by blast
  have ‹saturated (Liminf_llist Ns)›
    using deriv fair fair_implies_Liminf_saturated unfolding saturated_def by auto
  then show ?thesis
    using bot_elem statically_complete Liminf_entails_Bot by auto
qed

end

locale dynamically_complete_calculus = calculus +
  assumes
    dynamically_complete: "B ∈ Bot ⟹ chain (⊳) Ns ⟹ fair Ns ⟹ lhd Ns ⊨ {B} ⟹
      ∃i ∈ {i. enat i < llength Ns}. ∃B'∈Bot. B' ∈ lnth Ns i"
begin

(* lem:dynamic-ref-compl-implies-static *)
sublocale statically_complete_calculus
proof
  fix B N
  assume
    bot_elem: ‹B ∈ Bot› and
    saturated_N: "saturated N" and
    refut_N: "N ⊨ {B}"
  define Ns where "Ns = LCons N LNil"
  have[simp]: ‹¬ lnull Ns› by (auto simp: Ns_def)
  have deriv_Ns: ‹chain (⊳) Ns› by (simp add: chain.chain_singleton Ns_def)
  have liminf_is_N: "Liminf_llist Ns = N" by (simp add: Ns_def Liminf_llist_LCons)
  have head_Ns: "N = lhd Ns" by (simp add: Ns_def)
  have "Sup_llist (lmap Red_I Ns) = Red_I N" by (simp add: Ns_def)
  then have fair_Ns: "fair Ns" using saturated_N by (simp add: fair_def saturated_def liminf_is_N)
  obtain i B' where B'_is_bot: ‹B' ∈ Bot› and B'_in: "B' ∈ lnth Ns i" and ‹i < llength Ns›
    using dynamically_complete[of B Ns] bot_elem fair_Ns head_Ns saturated_N deriv_Ns refut_N
    by auto
  then have "i = 0"
    by (auto simp: Ns_def enat_0_iff)
  show ‹∃B'∈Bot. B' ∈ N›
    using B'_is_bot B'_in unfolding ‹i = 0› head_Ns[symmetric] Ns_def by auto
qed

end

(* lem:static-ref-compl-implies-dynamic *)
sublocale statically_complete_calculus ⊆ dynamically_complete_calculus
proof
  fix B Ns
  assume
    ‹B ∈ Bot› and
    ‹chain (⊳) Ns› and
    ‹fair Ns› and
    ‹lhd Ns ⊨ {B}›
  then have ‹∃B'∈Bot. B' ∈ Liminf_llist Ns›
    by (rule dynamically_complete_Liminf)
  then show ‹∃i∈{i. enat i < llength Ns}. ∃B'∈Bot. B' ∈ lnth Ns i›
    unfolding Liminf_llist_def by auto
qed

end