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