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

subsection ‹Changing the Consequence Relation›

text ‹A calculus and its refutational completeness can be transported to another
  consequence relation that agrees on entailment of contradictions. No agreement
  on other conclusions is required. The inference system and redundancy criteria,
  and hence saturation and derivations, are preserved.›

context calculus
begin

lemma calculus_with_equivalent_entailment:
  assumes cons: "consequence_relation Bot entails'"
    and bot_iff: "⋀B N. B ∈ Bot ⟹ (entails' N {B} ⟷ entails N {B})"
  shows "calculus Bot Inf entails' Red_I Red_F"
proof -
  interpret new: consequence_relation Bot entails' by (rule cons)
  show ?thesis
  proof
    show "Red_I N ⊆ Inf" for N by (rule Red_I_to_Inf)
    show "B ∈ Bot ⟹ entails' N {B} ⟹ entails' (N - Red_F N) {B}" for B N
      using bot_iff Red_F_Bot by blast
    show "N ⊆ N' ⟹ Red_F N ⊆ Red_F N'" for N N' by (rule Red_F_of_subset)
    show "N ⊆ N' ⟹ Red_I N ⊆ Red_I N'" for N N' by (rule Red_I_of_subset)
    show "N' ⊆ Red_F N ⟹ Red_F N ⊆ Red_F (N - N')" for N N'
      by (rule Red_F_of_Red_F_subset)
    show "N' ⊆ Red_F N ⟹ Red_I N ⊆ Red_I (N - N')" for N N'
      by (rule Red_I_of_Red_F_subset)
    show "ι ∈ Inf ⟹ concl_of ι ∈ N ⟹ ι ∈ Red_I N" for ι N
      by (rule Red_I_of_Inf_to_N)
  qed
qed

end

context statically_complete_calculus
begin

lemma statically_complete_with_equivalent_entailment:
  assumes cons: "consequence_relation Bot entails'"
    and bot_iff: "⋀B N. B ∈ Bot ⟹ (entails' N {B} ⟷ entails N {B})"
  shows "statically_complete_calculus Bot Inf entails' Red_I Red_F"
proof -
  interpret new: calculus Bot Inf entails' Red_I Red_F
    by (rule calculus_with_equivalent_entailment[OF cons bot_iff])
  show ?thesis
    by unfold_locales (use statically_complete bot_iff in blast)
qed

end

context dynamically_complete_calculus
begin

lemma dynamically_complete_with_equivalent_entailment:
  assumes cons: "consequence_relation Bot entails'"
    and bot_iff: "⋀B N. B ∈ Bot ⟹ (entails' N {B} ⟷ entails N {B})"
  shows "dynamically_complete_calculus Bot Inf entails' Red_I Red_F"
proof -
  interpret new: statically_complete_calculus Bot Inf entails' Red_I Red_F
    by (rule statically_complete_with_equivalent_entailment[OF cons bot_iff])
  show ?thesis by (rule new.dynamically_complete_calculus_axioms)
qed

end

end