Theory Intersection_Calculus

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

section ‹Calculi Based on the Intersection of Redundancy Criteria›

text ‹In this section, section 2.3 of the report is covered, on calculi
  equipped with a family of redundancy criteria.›

theory Intersection_Calculus
  imports
    Calculus
    Ordered_Resolution_Prover.Lazy_List_Liminf
    Ordered_Resolution_Prover.Lazy_List_Chain
begin


subsection ‹Calculi with a Family of Redundancy Criteria›

locale intersection_calculus =
  inference_system Inf + consequence_relation_family Bot Q entails_q
  for
    Bot :: "'f set" and
    Inf :: ‹'f inference set› and
    Q :: "'q set" and
    entails_q :: "'q ⇒ 'f set ⇒ 'f set ⇒ bool"
  + fixes
    Red_I_q :: "'q ⇒ 'f set ⇒ 'f inference set" and
    Red_F_q :: "'q ⇒ 'f set ⇒ 'f set"
  assumes
    Q_nonempty: "Q ≠ {}" and
    all_red_crit: "∀q ∈ Q. calculus Bot Inf (entails_q q) (Red_I_q q) (Red_F_q q)"
begin

definition Red_I :: "'f set ⇒ 'f inference set" where
  "Red_I N = (⋂q ∈ Q. Red_I_q q N)"

definition Red_F :: "'f set ⇒ 'f set" where
  "Red_F N = (⋂q ∈ Q. Red_F_q q N)"

(* lem:intersection-of-red-crit *)
sublocale calculus Bot Inf entails Red_I Red_F
  unfolding calculus_def calculus_axioms_def
proof (intro conjI)
  show "consequence_relation Bot entails"
  using intersect_cons_rel_family .
next
  show "∀N. Red_I N ⊆ Inf"
    unfolding Red_I_def
  proof
    fix N
    show "(⋂q ∈ Q. Red_I_q q N) ⊆ Inf"
    proof (intro Inter_subset)
      fix Red_Is
      assume one_red_inf: "Red_Is ∈ (λq. Red_I_q q N) ` Q"
      show "Red_Is ⊆ Inf"
        using one_red_inf all_red_crit calculus.Red_I_to_Inf by blast
    next
      show "(λq. Red_I_q q N) ` Q ≠ {}"
        using Q_nonempty by blast
    qed
  qed
next
  show "∀B N. B ∈ Bot ⟶ N ⊨Q {B} ⟶ N - Red_F N ⊨Q {B}"
  proof (intro allI impI)
    fix B N
    assume
      B_in: "B ∈ Bot" and
      N_unsat: "N ⊨Q {B}"
    show "N - Red_F N ⊨Q {B}" unfolding entails_def Red_F_def
    proof
      fix qi
      assume qi_in: "qi ∈ Q"
      define entails_qi (infix ‹⊨qi› 50) where "entails_qi = entails_q qi"
      have cons_rel_qi: "consequence_relation Bot entails_qi"
        unfolding entails_qi_def using qi_in all_red_crit calculus.axioms(1) by blast
      define Red_F_qi where "Red_F_qi = Red_F_q qi"
      have red_qi_in: "Red_F N ⊆ Red_F_qi N"
        unfolding Red_F_def Red_F_qi_def using qi_in image_iff by blast
      then have "N - Red_F_qi N ⊆ N - Red_F N" by blast
      then have entails_1: "N - Red_F N ⊨qi N - Red_F_qi N"
        using qi_in all_red_crit
        unfolding calculus_def consequence_relation_def entails_qi_def by metis
      have N_unsat_qi: "N ⊨qi {B}" using qi_in N_unsat unfolding entails_qi_def entails_def
        by simp
      then have N_unsat_qi: "N - Red_F_qi N ⊨qi {B}"
        using qi_in all_red_crit Red_F_qi_def calculus.Red_F_Bot[OF _ B_in] entails_qi_def
        by fastforce
      show "N - (⋂q ∈ Q. Red_F_q q N) ⊨qi {B}"
        using consequence_relation.entails_trans[OF cons_rel_qi entails_1 N_unsat_qi]
        unfolding Red_F_def .
    qed
  qed
next
  show "∀N1 N2. N1 ⊆ N2 ⟶ Red_F N1 ⊆ Red_F N2"
  proof (intro allI impI)
    fix N1 :: "'f set"
    and N2 :: "'f set"
    assume
      N1_in_N2: "N1 ⊆ N2"
    show "Red_F N1 ⊆ Red_F N2"
    proof
      fix C
      assume "C ∈ Red_F N1"
      then have "∀qi ∈ Q. C ∈ Red_F_q qi N1" unfolding Red_F_def by blast
      then have "∀qi ∈ Q. C ∈ Red_F_q qi N2"
        using N1_in_N2 all_red_crit calculus.axioms(2) calculus.Red_F_of_subset by blast
      then show "C ∈ Red_F N2" unfolding Red_F_def by blast
    qed
  qed
next
  show "∀N1 N2. N1 ⊆ N2 ⟶ Red_I N1 ⊆ Red_I N2"
  proof (intro allI impI)
    fix N1 :: "'f set"
    and N2 :: "'f set"
    assume
      N1_in_N2: "N1 ⊆ N2"
    show "Red_I N1 ⊆ Red_I N2"
    proof
      fix ι
      assume "ι ∈ Red_I N1"
      then have "∀qi ∈ Q. ι ∈ Red_I_q qi N1" unfolding Red_I_def by blast
      then have "∀qi ∈ Q. ι ∈ Red_I_q qi N2"
        using N1_in_N2 all_red_crit calculus.axioms(2) calculus.Red_I_of_subset by blast
      then show "ι ∈ Red_I N2" unfolding Red_I_def by blast
    qed
  qed
next
  show "∀N2 N1. N2 ⊆ Red_F N1 ⟶ Red_F N1 ⊆ Red_F (N1 - N2)"
  proof (intro allI impI)
    fix N2 N1
    assume N2_in_Red_N1: "N2 ⊆ Red_F N1"
    show "Red_F N1 ⊆ Red_F (N1 - N2)"
    proof
      fix C
      assume "C ∈ Red_F N1"
      then have "∀qi ∈ Q. C ∈ Red_F_q qi N1" unfolding Red_F_def by blast
      moreover have "∀qi ∈ Q. N2 ⊆ Red_F_q qi N1" using N2_in_Red_N1 unfolding Red_F_def by blast
      ultimately have "∀qi ∈ Q. C ∈ Red_F_q qi (N1 - N2)"
        using all_red_crit calculus.axioms(2) calculus.Red_F_of_Red_F_subset
        by blast
      then show "C ∈ Red_F (N1 - N2)" unfolding Red_F_def by blast
    qed
  qed
next
  show "∀N2 N1. N2 ⊆ Red_F N1 ⟶ Red_I N1 ⊆ Red_I (N1 - N2)"
  proof (intro allI impI)
    fix N2 N1
    assume N2_in_Red_N1: "N2 ⊆ Red_F N1"
    show "Red_I N1 ⊆ Red_I (N1 - N2)"
    proof
      fix ι
      assume "ι ∈ Red_I N1"
      then have "∀qi ∈ Q. ι ∈ Red_I_q qi N1" unfolding Red_I_def by blast
      moreover have "∀qi ∈ Q. N2 ⊆ Red_F_q qi N1" using N2_in_Red_N1 unfolding Red_F_def by blast
      ultimately have "∀qi ∈ Q. ι ∈ Red_I_q qi (N1 - N2)"
        using all_red_crit calculus.axioms(2) calculus.Red_I_of_Red_F_subset by blast
      then show "ι ∈ Red_I (N1 - N2)" unfolding Red_I_def by blast
    qed
  qed
next
  show "∀ι N. ι ∈ Inf ⟶ concl_of ι ∈ N ⟶ ι ∈ Red_I N"
  proof (intro allI impI)
    fix ι N
    assume
      i_in: "ι ∈ Inf" and
      concl_in: "concl_of ι ∈ N"
    then have "∀qi ∈ Q. ι ∈ Red_I_q qi N"
      using all_red_crit calculus.axioms(2) calculus.Red_I_of_Inf_to_N by blast
    then show "ι ∈ Red_I N" unfolding Red_I_def by blast
  qed
qed

(* lem:satur-wrt-intersection-of-red *)
lemma sat_int_to_sat_q: "calculus.saturated Inf Red_I N ⟷
  (∀qi ∈ Q. calculus.saturated Inf (Red_I_q qi) N)" for N
proof
  fix N
  assume inter_sat: "calculus.saturated Inf Red_I N"
  show "∀qi ∈ Q. calculus.saturated Inf (Red_I_q qi) N"
  proof
    fix qi
    assume qi_in: "qi ∈ Q"
    then interpret one: calculus Bot Inf "entails_q qi" "Red_I_q qi" "Red_F_q qi"
      by (metis all_red_crit)
    show "one.saturated N"
      using qi_in inter_sat
      unfolding one.saturated_def saturated_def Red_I_def by blast
  qed
next
  fix N
  assume all_sat: "∀qi ∈ Q. calculus.saturated Inf (Red_I_q qi) N"
  show "saturated N"
    unfolding saturated_def Red_I_def
  proof
    fix ι
    assume ι_in: "ι ∈ Inf_from N"
    have "∀Red_I_qi ∈ Red_I_q ` Q. ι ∈ Red_I_qi N"
    proof
      fix Red_I_qi
      assume red_inf_in: "Red_I_qi ∈ Red_I_q ` Q"
      then obtain qi where
        qi_in: "qi ∈ Q" and
        red_inf_qi_def: "Red_I_qi = Red_I_q qi" by blast
      then interpret one: calculus Bot Inf "entails_q qi" "Red_I_q qi" "Red_F_q qi"
        by (metis all_red_crit)
      have "one.saturated N" using qi_in all_sat red_inf_qi_def by blast
      then show "ι ∈ Red_I_qi N" unfolding one.saturated_def using ι_in red_inf_qi_def by blast
    qed
    then show "ι ∈ (⋂q ∈ Q. Red_I_q q N)" by blast
  qed
qed

(* lem:checking-static-ref-compl-for-intersections *)
lemma stat_ref_comp_from_bot_in_sat:
  "(∀N. calculus.saturated Inf Red_I N ∧ (∀B ∈ Bot. B ∉ N) ⟶
      (∃B ∈ Bot. ∃qi ∈ Q. ¬ entails_q qi N {B})) ⟹
   statically_complete_calculus Bot Inf entails Red_I Red_F"
proof (rule ccontr)
  assume
    N_saturated: "∀N. (calculus.saturated Inf Red_I N ∧ (∀B ∈ Bot. B ∉ N)) ⟶
      (∃B ∈ Bot. ∃qi ∈ Q. ¬ entails_q qi N {B})" and
    no_stat_ref_comp: "¬ statically_complete_calculus Bot Inf (⊨Q) Red_I Red_F"
  obtain N1 B1 where B1_in:
    "B1 ∈ Bot" and N1_saturated: "calculus.saturated Inf Red_I N1" and
    N1_unsat: "N1 ⊨Q {B1}" and no_B_in_N1: "∀B ∈ Bot. B ∉ N1"
    using no_stat_ref_comp by (metis calculus_axioms statically_complete_calculus.intro
        statically_complete_calculus_axioms.intro)
  obtain B2 qi where
    qi_in: "qi ∈ Q" and
    no_qi: "¬ entails_q qi N1 {B2}"
    using N_saturated N1_saturated no_B_in_N1 by auto
  have "N1 ⊨Q {B2}" using N1_unsat B1_in intersect_cons_rel_family
    unfolding consequence_relation_def by metis
  then have "entails_q qi N1 {B2}" unfolding entails_def using qi_in by blast
  then show False using no_qi by simp
qed

end

end