Theory Lightweight_Avatar

(* Title:        Applications of the Splitting Framework to other architectures
 *               (Splitting without Backtracking)
 * Authors:      Ghilain Bergeron <ghilain.bergeron at inria.fr>, 2023
 *               Sophie Tourret <sophie.tourret at inria.fr, 2024-2025 *)


theory Lightweight_Avatar
  imports
    Main
    Modular_Splitting_Calculus
    Saturation_Framework_Extensions.FO_Ordered_Resolution_Prover_Revisited 
begin



subsection ‹Ordered Resolution with a Disjunctive Consequence Relation›

locale FO_resolution_prover_disjunctive = FO_resolution_prover S subst_atm id_subst comp_subst 
  renaming_aparts atm_of_atms mgu less_atm 
  for
    S :: ‹('a :: wellorder) clause ⇒ 'a clause› and 
    subst_atm :: ‹'a ⇒ 's ⇒ 'a› and 
    id_subst :: ‹'s› and 
    comp_subst :: ‹'s ⇒ 's ⇒ 's› and 
    renaming_aparts :: ‹'a clause list ⇒ 's list› and 
    atm_of_atms :: ‹'a list ⇒ 'a› and 
    mgu :: ‹'a set set ⇒ 's option› and 
    less_atm :: ‹'a ⇒ 'a ⇒ bool›
begin

no_notation entails_clss (infix ‹⊫e› 50)
no_notation Sema.entailment (‹(_ ⊫/ _)› [53, 53] 53)
no_notation Linear_Temporal_Logic_on_Streams.HLD_nxt (infixr "⋅" 65)
(* These two cause ambiguities in a few places. *)
notation entails_clss (infix ‹⊫∩e› 50)

(* All this is taken from the file 🗏‹FO_Ordered_Resolution_Prover_Revisited.thy›.
 * I don't like it, but I don't have a choice as I need access to these interpretations. *)
interpretation gr: ground_resolution_with_selection "S_M S M"
  using selection_axioms by unfold_locales (fact S_M_selects_subseteq S_M_selects_neg_lits)+

interpretation G: Soundness.sound_inference_system "G_Inf M" "{{#}}" "(⊫∩e)"
proof
  fix ι
  assume i_in: "ι ∈ G_Inf M"
  moreover
  {
    fix I
    assume I_ent_prems: "I ⊫s set (prems_of ι)"
    obtain CAs AAs As where
      the_inf: "gr.ord_resolve M CAs (main_prem_of ι) AAs As (concl_of ι)" and
      CAs: "CAs = side_prems_of ι"
      using i_in unfolding G_Inf_def by auto
    then have "I ⊫ concl_of ι"
      using gr.ord_resolve_sound[of M CAs "main_prem_of ι" AAs As "concl_of ι" I]
      by (metis I_ent_prems G_Inf_have_prems i_in insert_is_Un set_mset_mset set_prems_of
          true_clss_insert true_clss_set_mset)
  }
  ultimately show "set (inference.prems_of ι) ⊫∩e {concl_of ι}"
    by simp
qed

interpretation G: clausal_counterex_reducing_inference_system "G_Inf M" "gr.INTERP M"
proof
  fix N D
  assume
    "{#} ∉ N" and
    "D ∈ N" and
    "¬ gr.INTERP M N ⊫ D" and
    "⋀C. C ∈ N ⟹ ¬ gr.INTERP M N ⊫ C ⟹ D ≤ C"
  then obtain CAs AAs As E where
    cas_in: "set CAs ⊆ N" and
    n_mod_cas: "gr.INTERP M N ⊫m mset CAs" and
    ca_prod: "⋀CA. CA ∈ set CAs ⟹ gr.production M N CA ≠ {}" and
    e_res: "gr.ord_resolve M CAs D AAs As E" and
    n_nmod_e: "¬ gr.INTERP M N ⊫ E" and
    e_lt_d: "E < D"
    using gr.ord_resolve_counterex_reducing by blast
  define ι where
    "ι = Infer (CAs @ [D]) E"

  have "ι ∈ G_Inf M"
    unfolding ι_def G_Inf_def using e_res by auto
  moreover have "prems_of ι ≠ []"
    unfolding ι_def by simp
  moreover have "main_prem_of ι = D"
    unfolding ι_def by simp
  moreover have "set (side_prems_of ι) ⊆ N"
    unfolding ι_def using cas_in by simp
  moreover have "gr.INTERP M N ⊫s set (side_prems_of ι)"
    unfolding ι_def using n_mod_cas ca_prod by (simp add: gr.productive_imp_INTERP true_clss_def)
  moreover have "¬ gr.INTERP M N ⊫ concl_of ι"
    unfolding ι_def using n_nmod_e by simp
  moreover have "concl_of ι < D"
    unfolding ι_def using e_lt_d by simp
  ultimately show "∃ι ∈ G_Inf M. prems_of ι ≠ [] ∧ main_prem_of ι = D ∧ set (side_prems_of ι) ⊆ N ∧
    gr.INTERP M N ⊫s set (side_prems_of ι) ∧ ¬ gr.INTERP M N ⊫ concl_of ι ∧ concl_of ι < D"
    by blast
qed

(*** This one is not a copy-pasta! *)
interpretation G: calculus_with_standard_redundancy ‹G_Inf M› ‹{{#}}› ‹(⊫∩e)›
  ‹(<) :: 'a clause ⇒ 'a clause ⇒ bool›
  using G_Inf_have_prems G_Inf_reductive
  by (unfold_locales) simp_all 

(*** This one has been modified too! *)
interpretation G: clausal_counterex_reducing_calculus_with_standard_redundancy "G_Inf M"
  "gr.INTERP M"
  by (unfold_locales)

interpretation G: Calculus.statically_complete_calculus "{{#}}" "G_Inf M" "(⊫∩e)" "G.Red_I M" G.Red_F
  by unfold_locales (use G.clausal_saturated_complete in blast)

sublocale F: lifting_intersection F_Inf "{{#}}" UNIV G_Inf "λN. (⊫∩e)" G.Red_I "λN. G.Red_F"
  "{{#}}" "λN. 𝒢_F" 𝒢_I_opt "λD C C'. False"
proof (unfold_locales; (intro ballI)?)
  show "UNIV ≠ {}"
    by (rule UNIV_not_empty)
next
  show "Calculus.consequence_relation {{#}} (⊫∩e)"
    by (fact consequence_relation_axioms)
next
  show "⋀M. tiebreaker_lifting {{#}} F_Inf {{#}} (⊫∩e) (G_Inf M) (G.Red_I M) G.Red_F 𝒢_F (𝒢_I_opt M)
    (λD C C'. False)"
  proof
    fix M ι
    show "the (𝒢_I_opt M ι) ⊆ G.Red_I M (𝒢_F (concl_of ι))"
      unfolding option.sel
    proof
      fix ι'
      assume "ι' ∈ 𝒢_I M ι"
      then obtain ρ ρs where
        ι': "ι' = Infer (prems_of ι ⋅⋅cl ρs) (concl_of ι ⋅ ρ)" and
        ρ_gr: "is_ground_subst ρ" and
        ρ_infer: "Infer (prems_of ι ⋅⋅cl ρs) (concl_of ι ⋅ ρ) ∈ G_Inf M"
        unfolding 𝒢_I_def by blast

      show "ι' ∈ G.Red_I M (𝒢_F (concl_of ι))"
        unfolding G.Red_I_def G.redundant_infer_def mem_Collect_eq using ι' ρ_gr ρ_infer
        by (metis Calculus.inference.sel(2) G_Inf_reductive empty_iff ground_subst_ground_cls
            grounding_of_cls_ground insert_iff subst_cls_eq_grounding_of_cls_subset_eq
            true_clss_union)
    qed
  qed (auto simp: 𝒢_F_def ex_ground_subst)
qed

notation F.entails_𝒢 (infix "⊫∩𝒢e" 50)

sublocale F: sound_inference_system F_Inf "{{#}}" "(⊫∩𝒢e)"
proof
  fix ι
  assume i_in: "ι ∈ F_Inf"
  moreover
  {
    fix I η
    assume
      I_entails_prems: "∀σ. is_ground_subst σ ⟶ I ⊫s set (prems_of ι) ⋅cs σ" and
      η_gr: "is_ground_subst η"
    obtain CAs AAs As σ where
      the_inf: "ord_resolve_rename S CAs (main_prem_of ι) AAs As σ (concl_of ι)" and
      CAs: "CAs = side_prems_of ι"
      using i_in unfolding F_Inf_def by auto
    have prems: "mset (prems_of ι) = mset (side_prems_of ι) + {#main_prem_of ι#}"
      by (metis (no_types) F_Inf_have_prems[OF i_in] add.right_neutral append_Cons append_Nil2
          append_butlast_last_id mset.simps(2) mset_rev mset_single_iff_right rev_append
          rev_is_Nil_conv union_mset_add_mset_right)
    have "I ⊫ concl_of ι ⋅ η"
      using ord_resolve_rename_sound[OF the_inf, of I η, OF _ η_gr]
      unfolding CAs prems[symmetric] using I_entails_prems
      by (metis set_mset_mset set_mset_subst_cls_mset_subst_clss true_clss_set_mset)
  }
  ultimately show "set (inference.prems_of ι) ⊫∩𝒢e {concl_of ι}"
    unfolding F.entails_𝒢_def 𝒢_F_def true_Union_grounding_of_cls_iff by auto
qed

lemma F_stat_comp_calc: ‹Calculus.statically_complete_calculus {{#}} F_Inf (⊫∩𝒢e) F.Red_I_𝒢
   F.Red_F_𝒢_empty›
proof (rule F.stat_ref_comp_to_non_ground_fam_inter)
  have "⋀M. Calculus.statically_complete_calculus {{#}} (G_Inf M) (⊫∩e) (G.Red_I M) G.Red_F"
    by (fact G.statically_complete_calculus_axioms)
  then show ‹∀q∈UNIV. Calculus.statically_complete_calculus {{#}} (G_Inf q) (⊫∩e) (G.Red_I q) G.Red_F›
    by clarsimp
next
  fix N
  assume "F.saturated N"
  have "F.ground.Inf_from_q N (⋃ (𝒢_F ` N)) ⊆ {ι. ∃ι' ∈ F.Inf_from N. ι ∈ 𝒢_I N ι'}
    ∪ G.Red_I N (⋃ (𝒢_F ` N))"
    using G_Inf_overapprox_F_Inf unfolding F.ground.Inf_from_q_def 𝒢_I_def by fastforce
  then show ‹∃q∈UNIV. F.ground.Inf_from_q q (⋃ (𝒢_F ` N))
    ⊆ {ι. ∃ι'∈F.Inf_from N. 𝒢_I_opt q ι' ≠ None ∧ ι ∈ the (𝒢_I_opt q ι')} ∪ G.Red_I q (⋃ (𝒢_F ` N))›
    by auto
qed

sublocale F: Calculus.statically_complete_calculus "{{#}}" F_Inf "(⊫∩𝒢e)" F.Red_I_𝒢
  F.Red_F_𝒢_empty
  using F_stat_comp_calc by blast

sublocale F': Calculus.statically_complete_calculus "{{#}}" F_Inf "(⊫∩𝒢e)" F.empty_ord.Red_Red_I
  F.Red_F_𝒢_empty
  using F.empty_ord.reduced_calc_is_calc F.empty_ord.stat_is_stat_red F_stat_comp_calc
  by blast

(********************************************************)
(****************** End of copy pasta *******************)
(********************************************************)

(*<*)
interpretation F': Calculus.dynamically_complete_calculus ‹{{#}}› F_Inf ‹(⊫∩𝒢e)› 
  F.empty_ord.Red_Red_I F.Red_F_𝒢_empty
  using F'.dynamically_complete_calculus_axioms .

lemma entails_bot_iff_unsatisfiable: ‹M ⊫∩e {{#}} ⟷ ¬ satisfiable M›
  by blast 

lemma entails_conj_compactness':
  ‹M ⊫∩e N ⟷ (∀ I. (∀ M' ⊆ M. finite M' ⟶ I ⊫s M') ⟶
    (∀ N' ⊆ N. finite N' ⟶ I ⊫s N'))›
  by (meson empty_subsetI finite.emptyI finite_insert insert_subset true_clss_def true_clss_mono
      true_clss_singleton) 

lemma entails_𝒢_conj_compactness': 
  ‹M ⊫∩𝒢e N ⟷ (∀ I. (∀ M' ⊆ 𝒢_Fset M. finite M' ⟶ I ⊫s M') ⟶
     (∀ N' ⊆ 𝒢_Fset N. finite N' ⟶ I ⊫s N'))›
  unfolding F.entails_𝒢_def 𝒢_F_def using entails_conj_compactness'[of ‹𝒢_Fset M› ‹𝒢_Fset N›]
  unfolding 𝒢_Fset_def 𝒢_F_def by (meson UNIV_I) 

lemma entails_𝒢_iff_unsatisfiable:
  ‹M ⊫∩𝒢e N ⟷ (∀ C ∈ 𝒢_Fset N. ¬ satisfiable (𝒢_Fset M ∪ {{# -L #} | L. L ∈# C}))›
  unfolding F.entails_𝒢_def 𝒢_Fset_def 𝒢_F_def
  using entails_iff_unsatisfiable
  by (smt (verit, ccfv_threshold) UNIV_I)

lemma list_all3_eq_map2:
  ‹length xs = length ys ⟹ length ys = length zs ⟹
    list_all3 (λ x y z. z = F x y) xs ys zs ⟷ map2 F xs ys = zs›
proof (intro iffI)
  assume ‹list_all3 (λ x y z. z = F x y) xs ys zs› (is ‹list_all3 ?P xs ys zs›)
  then show ‹map2 F xs ys = zs›
    by (induction ?P xs ys zs rule: list_all3.induct, auto)
next
  assume
    ‹length xs = length ys› and
    ‹length ys = length zs› and
    ‹map2 F xs ys = zs›
  then show ‹list_all3 (λ x y z. z = F x y) xs ys zs›
  proof (induction ‹zip xs ys› arbitrary: xs ys zs) 
    case Nil
    then show ?case
      by auto 
  next
    case (Cons a as)

    obtain x y where
      ‹a = (x, y)›
      by fastforce
    then obtain z zs' xs' ys' where
      zs_eq: ‹zs = z # zs'› and
      xs_eq: ‹xs = x # xs'› and
      ys_eq: ‹ys = y # ys'› and
      z_is: ‹z = F x y›
      (* /!\ Very slow /!\ *)
      by (smt (verit, ccfv_threshold) Cons.hyps(2) Cons.prems(2) Cons.prems(3) Pair_inject
          list.inject map_eq_Cons_conv old.prod.case zip_eq_ConsE)
    then have
      ‹as = zip xs' ys'› and
      ‹length xs' = length ys'› and
      ‹length ys' = length zs'›
      using Cons.prems(1, 2) Cons.hyps(2)
      by auto 
    then show ?case
      using Cons.hyps Cons.prems(3) z_is zs_eq xs_eq ys_eq
      by auto
  qed
qed

lemma ex_finite_subset_M_if_ex_finite_subset_𝒢_F_M:
  ‹Mσ ⊆ 𝒢_Fset M ⟹ finite Mσ ⟹ Mσ ⊫∩e {{#}} ⟹
    ∃ M' ⊆ M. finite M' ∧ 𝒢_Fset M' ⊫∩e {{#}}›
proof -
  assume
    Mσ_subset: ‹Mσ ⊆ 𝒢_Fset M› and
    finite_Mσ: ‹finite Mσ› and
    Mσ_entails_bot: ‹Mσ ⊫∩e {{#}}›

  have ‹Mσ ⊆ (⋃ C ∈ M. {C ⋅ σ | σ. is_ground_subst σ})›
    using Mσ_subset
    unfolding 𝒢_Fset_def 𝒢_F_def
    by blast      
  then have ‹∀ C ∈ Mσ. ∃ C' ∈ M. ∃ σ. is_ground_subst σ ∧ C = C' ⋅ σ›
    by blast
  moreover have ‹Mσ ≠ {}›
    using Mσ_entails_bot
    by blast 
  then obtain Mσ' where
    Mσ'_is: ‹set Mσ' = Mσ› and
    ‹Mσ' ≠ []› 
    using finite_Mσ finite_list
    by (meson sorted_list_of_set.set_sorted_key_list_of_set
        sorted_list_of_set.sorted_key_list_of_set_eq_Nil_iff) 
  ultimately have ‹list.list_all (λ C. ∃ C' ∈ M. ∃ σ. is_ground_subst σ ∧ C = C' ⋅ σ) Mσ'›
    by (simp add: list.pred_set) 
  then obtain Cs where
    Cs_in_M: ‹set Cs ⊆ M› and
    ‹list_all2 (λ C C'. ∃ σ. is_ground_subst σ ∧ C = C' ⋅ σ) Mσ' Cs›
    using list_all_bex_ex_list_all2_conv[of M _ Mσ']
    by blast 
  then obtain σs where
    sigs_is: ‹list_all3 (λ C C' σ. is_ground_subst σ ∧ C = C' ⋅ σ) Mσ' Cs σs›
    using list_all2_ex_to_ex_list_all3[of _ Mσ' Cs]
    by blast 
  then have 
    all_grounding_in_σs: ‹list.list_all is_ground_subst σs›
    proof -
      have "⋀p ms msa ss. ¬ list_all3 p ms msa ss ∨
        list_all2 (λm s. ∃ma. p (m::'a literal multiset) (ma::'a literal multiset) (s::'s)) ms ss"
        by (metis (no_types) list_all2_ex_to_ex_list_all3 list_all3_reorder)
      then have f1: "list_all2 (λm s. ∃ma. is_ground_subst s ∧ m = ma ⋅ s) Mσ' σs"
        using sigs_is by blast
      have "∀ss p. ∃n. (list.list_all p ss ∨ n < length ss) ∧ 
        (¬ p (ss ! n::'s) ∨ list.list_all p ss)"
        using list_all_length by blast
      then show ?thesis
        using f1 by (metis (lifting) list_all2_conv_all_nth)
    qed
    have
    ‹list_all3 (λ C C' σ. C = C' ⋅ σ) Mσ' Cs σs›
    using list_all3_conj_distrib[of _ _ Mσ' Cs σs] list_all3_conv_list_all_3 sigs_is
    by fastforce
  then have Mσ'_eq_map2: ‹map2 (⋅) Cs σs = Mσ'›
    using list_all3_reorder2[of _ Mσ' Cs σs] list_all3_eq_map2[of Cs σs Mσ']
          list_all3_length_eq1[of _ Mσ' Cs σs] list_all3_length_eq2[of _ Mσ' Cs σs]
    by fastforce
  then have ‹set Mσ' ⊆ 𝒢_Fset (set Cs)›
    unfolding 𝒢_Fset_def 𝒢_F_def
    using all_grounding_in_σs
    by auto (metis list.pred_set set_zip_leftD set_zip_rightD) 
  then have ‹𝒢_Fset (set Cs) ⊫∩e {{#}}›
    using Mσ_entails_bot Mσ'_is
    by (meson true_clss_mono) 
  then show ‹∃ M' ⊆ M. finite M' ∧ 𝒢_Fset M' ⊫∩e {{#}}›
    using Cs_in_M
    by blast 
qed

lemma unsat_𝒢_compact: ‹M ⊫∩𝒢e {{#}} ⟹ ∃ M' ⊆ M. finite M' ∧ M' ⊫∩𝒢e {{#}}› 
proof -
  assume M_entails_bot: ‹M ⊫∩𝒢e {{#}}›
  then have ‹𝒢_Fset M ⊫∩e {{#}}›
    using F_entails_𝒢_iff grounding_of_clss_def
    by fastforce
  then have ‹∃ M' ⊆ 𝒢_Fset M. finite M' ∧ M' ⊫∩e {{#}}›
    using Unordered_Ground_Resolution.clausal_logic_compact
    by auto
  then have ‹∃ M' ⊆ M. finite M' ∧ 𝒢_Fset M' ⊫∩e {{#}}›
    by (elim exE conjE, blast intro: ex_finite_subset_M_if_ex_finite_subset_𝒢_F_M)
  then show ‹∃ M' ⊆ M. finite M' ∧ M' ⊫∩𝒢e {{#}}›
    using F_entails_𝒢_iff grounding_of_clss_def
    by auto
qed

lemma sat_𝒢_compact: ‹¬ M ⊫∩𝒢e {{#}} ⟹ ∀ M' ⊆ M. finite M' ⟶ ¬ M' ⊫∩𝒢e {{#}}›
  using unsat_𝒢_compact F.entails_trans F.subset_entailed
  by blast

lemma neg_of_𝒢_F_lits_is_𝒢_F_of_neg_lits:
  ‹⋃ {{{# -L #} | L. L ∈# D' } | D'. D' ∈ 𝒢_F D} = ⋃ (𝒢_F ` {{# -L #} | L. L ∈# D})›
proof -
  have ‹⋃ {{{# -L #} | L. L ∈# D'} | D'. D' ∈ 𝒢_F D} =
    ⋃ {{{# -L #} | L. L ∈# D ⋅ σ} | σ. is_ground_subst σ}›
    unfolding 𝒢_F_def
    by blast 
  also have ‹... = ⋃ {{{# -(L ⋅l σ) #} | L. L ∈# D} | σ. is_ground_subst σ}›
    unfolding subst_cls_def
    by blast
  also have ‹... = ⋃ {{{# -L ⋅l σ #} | L. L ∈# D} | σ. is_ground_subst σ}›
    by simp 
  also have ‹... = ⋃ {{{# -L #} ⋅ σ | L. L ∈# D} | σ. is_ground_subst σ}›
    unfolding subst_cls_def
    by simp
  also have ‹... = (⋃ C ∈ {{# -L #} | L. L ∈# D}. {C ⋅ σ | σ. is_ground_subst σ})›
    by blast
  also have ‹... = ⋃ (𝒢_F ` {{# -L #} | L. L ∈# D})›
    unfolding 𝒢_F_def
    by blast 
  finally show ?thesis .  
qed 

lemma entails_bot_neg_if_entails_𝒢_single: ‹M ⊫∩𝒢e {D} ⟹ M ∪ {{# -L #} | L. L ∈# D} ⊫∩𝒢e {{#}}›
proof -
  assume ‹M ⊫∩𝒢e {D}›
  then have unsat: ‹∀ D' ∈ 𝒢_F D. ¬ satisfiable (𝒢_Fset M ∪ {{# -L #} | L. L ∈# D'})› 
    unfolding entails_𝒢_iff_unsatisfiable
    by (simp add: grounding_of_clss_def)
  then have ‹¬ satisfiable (𝒢_Fset M ∪ (⋃ D' ∈ 𝒢_F D. {{# -L #} | L. L ∈# D'}))›
    using ex_ground_subst substitution_ops.grounding_of_cls_def
    by fastforce
  then have ‹¬ satisfiable (𝒢_Fset M ∪ (⋃ {{{# -L #} | L. L ∈# D'} | D'. D' ∈ 𝒢_F D}))›
    by fast 
  then have ‹¬ satisfiable (𝒢_Fset M ∪ (⋃ (𝒢_F ` {{# -L #} | L. L ∈# D})))›
    using neg_of_𝒢_F_lits_is_𝒢_F_of_neg_lits
    by auto 
  then have ‹𝒢_Fset M ∪ (⋃ (𝒢_F ` {{# -L #} | L. L ∈# D})) ⊫∩e {{#}}›
    by presburger 
  then show ‹M ∪ {{# -L #} | L. L ∈# D} ⊫∩𝒢e {{#}}›
    unfolding F_entails_𝒢_iff 𝒢_F_def 𝒢_Fset_def
    by force
qed

lemma minus_𝒢_Fset_to_𝒢_Fset_minus: ‹C ∈ 𝒢_Fset M - 𝒢_Fset N ⟹ C ∈ 𝒢_Fset (M - N)›
  unfolding 𝒢_Fset_def 𝒢_F_def
  by blast

lemma unsat_equiv3: ‹¬ satisfiable (⋃ C ∈ M. {C ⋅ σ | σ. is_ground_subst σ}) ⟷ M ⊫∩𝒢e {{#}}›
  unfolding F.entails_𝒢_def 𝒢_F_def
  using grounding_of_cls_def grounding_of_cls_empty
  by force

(*>*)

text ‹
  @{const ‹F.entails_𝒢›} is a conjunctive entailment, meaning that for @{term ‹M ⊫∩𝒢e N›} to hold,
  each clause in ‹N› must be entailed by ‹M›.
  Unfortunately, this clashes with requirement (D3) @{thm consequence_relation.entails_subsets} of
  a splitting calculus.

  Therefore, we define a disjunctive version of this entailment by stating that ‹M ⊫∪𝒢e N› iff
  there is some ‹C ∈ N› such that ‹M ⊫∩𝒢e {C}›.
  This definition is not quite enough because it does not capture (D1)
  @{thm consequence_relation.bot_entails_empty}.
  More specifically, if ‹N› is empty, then there does not exist a ‹C ∈ N›! But we know that
  ‹M ⊨∪𝒢e {}› if ‹M› is unsatisfiable.
  Hence ‹M ⊫∪𝒢e N› if ‹M› is unsatisfiable, or there exists some ‹C ∈ N› such that ‹M ⊫∩𝒢e {C}›.
  In addition, it is necessary to modify this definition to capture (D5) the compactness property
  of disjunctive entailment.
›
definition entails_𝒢_disj :: ‹'a clause set ⇒ 'a clause set ⇒ bool› (infix ‹⊫∪𝒢e› 50) where
  ‹M ⊫∪𝒢e N ⟷ M ⊫∩𝒢e {{#}} ∨ (∃ M' ⊆ M. finite M' ∧ (∃ C ∈ N. M' ⊫∩𝒢e {C}))› 


(*<*)
lemma unsat_supsets: ‹M ⊫∩𝒢e {{#}} ⟹ M ∪ M' ⊫∩𝒢e {{#}}›
  using F.entails_trans F.subset_entailed
  by blast
(*>*)

(* Property (D3) *) 
lemma entails_𝒢_disj_subsets: ‹M' ⊆ M ⟹ N' ⊆ N ⟹ M' ⊫∪𝒢e N' ⟹ M ⊫∪𝒢e N›
  by (smt (verit, del_insts) F.entails_trans F.subset_entailed entails_𝒢_disj_def order_trans subsetD) 

(* Property (D5) *)
lemma entails_𝒢_disj_compactness:
  ‹M ⊫∪𝒢e N ⟹ ∃ M' N'. M' ⊆ M ∧ N' ⊆ N ∧ finite M' ∧ finite N' ∧
     M' ⊫∪𝒢e N'›
proof -
  assume ‹M ⊫∪𝒢e N›
  then consider
    (M_unsat) ‹M ⊫∩𝒢e {{#}}› |
    (b) ‹∃ M' ⊆ M. finite M' ∧ (∃ C ∈ N. M' ⊫∩𝒢e {C})›
    unfolding entails_𝒢_disj_def
    by blast 
  then show ?thesis
  proof cases
    case M_unsat
    then show ?thesis
      using unsat_𝒢_compact[of M]
      unfolding entails_𝒢_disj_def
      by blast 
  next
    case b
    then show ?thesis
      unfolding entails_𝒢_disj_def
      by (meson empty_subsetI finite.emptyI finite.insertI insert_subset subset_refl) 
  qed
qed

(* Property (D4) *) 
lemma entails_𝒢_disj_cut: ‹M ⊫∪𝒢e N ∪ {C} ⟹ M' ∪ {C} ⊫∪𝒢e N' ⟹ M ∪ M' ⊫∪𝒢e N ∪ N'›
proof -
  assume M_entails_N_u_C: ‹M ⊫∪𝒢e N ∪ {C}› and
         M'_u_C_entails_N': ‹M' ∪ {C} ⊫∪𝒢e N'›
  then obtain P P' where
    P_subset_M: ‹P ⊆ M› and
    finite_P: ‹finite P› and
    P_entails_N_u_C: ‹P ⊫∪𝒢e N ∪ {C}› and
    P'_subset_M'_u_C: ‹P' ⊆ M' ∪ {C}› and
    finite_P': ‹finite P'› and
    P'_entails_N': ‹P' ⊫∪𝒢e N'›
    using entails_𝒢_disj_compactness[OF M_entails_N_u_C]
          entails_𝒢_disj_compactness[OF M'_u_C_entails_N'] entails_𝒢_disj_subsets
    by blast 

  have P_subset_M_u_M': ‹P ⊆ M ∪ M'›
    using P_subset_M
    by blast 

  show ?thesis
  proof (cases ‹C ∈ P'›) 
    case C_in_P': True

    define P'' where
      ‹P'' = P' - {C}›

    have P''_subset_M': ‹P'' ⊆ M'›
      using P'_subset_M'_u_C P''_def
      by blast

    have finite_P'': ‹finite P''›
      using finite_P' P''_def
      by blast 

    consider
      (M_unsat) ‹P ⊫∩𝒢e {{#}}›
    | (M'_u_C_unsat) ‹P' ⊫∩𝒢e {{#}}›
    | (c) ‹(∃ C' ∈ N ∪ {C}. P ⊫∩𝒢e {C'}) ∧ (∃ C' ∈ N'. P' ⊫∩𝒢e {C'})›
      using P_entails_N_u_C P'_entails_N' finite_P finite_P'
      unfolding entails_𝒢_disj_def
      by (metis (no_types, lifting) F.entails_trans F.subset_entailed) 
    then show ?thesis
    proof cases 
      case M_unsat
      then have ‹P ⊫∪𝒢e N ∪ N'›
        using entails_𝒢_disj_def
        by blast 
      then show ?thesis
        using entails_𝒢_disj_subsets[of P ‹M ∪ M'› ‹N ∪ N'› ‹N ∪ N'›, OF P_subset_M_u_M']
        by blast 
    next
      case M'_u_C_unsat
      then show ?thesis 
        (* /!\ Slow /!\ *)
        by (smt (z3) F.subset_entailed F_entails_𝒢_iff M_entails_N_u_C P'_subset_M'_u_C UN_Un
            Un_insert_right entails_𝒢_disj_def entails_𝒢_disj_subsets insert_iff
            sup_bot.right_neutral sup_ge1 true_clss_union) 
    next
      case c
      then obtain C1 C2 where
        C1_in_N_u_C: ‹C1 ∈ N ∪ {C}› and
        P_entails_C1: ‹P ⊫∩𝒢e {C1}› and
        C2_in_N': ‹C2 ∈ N'› and
        P'_entails_C2: ‹P' ⊫∩𝒢e {C2}›
        by blast
      then show ?thesis
      proof (cases ‹C1 = C›) 
        case C1_is_C: True

        show ?thesis   
        proof (cases ‹C2 = C›)
          case True
          then have ‹N ∪ {C} ∪ N' = N ∪ N'›
            using C2_in_N'
            by blast 
          moreover have ‹P ⊫∪𝒢e N ∪ {C}›
            using P_entails_C1 C1_in_N_u_C finite_P
            unfolding entails_𝒢_disj_def
            by blast 
          ultimately show ?thesis
            using entails_𝒢_disj_subsets[OF P_subset_M_u_M', of ‹N ∪ {C}› ‹N ∪ N'›]
            by blast 
        next
          case C2_not_C: False
          then have ‹P ∪ P'' ⊫∩𝒢e {C2}›
            by (smt (verit, del_insts) C1_is_C F.entail_union F.entails_trans F.subset_entailed
                P''_def P'_entails_C2 P_entails_C1 Un_commute Un_insert_left insert_Diff_single
                sup_ge2) 
          then have ‹M ∪ M' ⊫∪𝒢e N'›
            using C2_in_N' P''_subset_M' P_subset_M finite_UnI[OF finite_P finite_P'']
            by (smt (verit, ccfv_SIG) P_subset_M_u_M' Un_subset_iff Un_upper2 entails_𝒢_disj_def
                order_trans)
          then show ?thesis
            by (meson entails_𝒢_disj_subsets equalityE sup_ge2)  
        qed
      next
        case False
        then have ‹C1 ∈ N›
          using C1_in_N_u_C
          by blast 
        then have ‹P ⊫∪𝒢e N›
          unfolding entails_𝒢_disj_def
          using P_entails_C1 finite_P
          by blast 
        then show ?thesis
          using entails_𝒢_disj_subsets[OF P_subset_M_u_M']
          by blast 
      qed
    qed
  next
    case False
    then have ‹P' ⊆ M'›
      using P'_subset_M'_u_C
      by blast 
    then have ‹M' ⊫∪𝒢e N'›
      using P'_entails_N' entails_𝒢_disj_subsets
      by blast 
    then show ?thesis
      using entails_𝒢_disj_subsets[of M' ‹M ∪ M'› N' ‹N ∪ N'›] 
      by blast 
  qed
qed

lemma entails_𝒢_disj_cons_rel_ext: ‹consequence_relation {#} (⊫∪𝒢e)›
proof (standard)
  show ‹{{#}} ⊫∪𝒢e {}›
    using F.subset_entailed entails_𝒢_disj_def
    by blast
  show ‹⋀ C. {C} ⊫∪𝒢e {C}›
    by (meson F.subset_entailed entails_𝒢_disj_def finite.emptyI finite.insertI singletonI
        subset_refl)
  show ‹⋀ M' M N' N. M' ⊆ M ⟹ N' ⊆ N ⟹ M' ⊫∪𝒢e N' ⟹ M ⊫∪𝒢e N›
    by (rule entails_𝒢_disj_subsets)
  show ‹⋀ M N C M' N'. M ⊫∪𝒢e N ∪ {C} ⟹ M' ∪ {C} ⊫∪𝒢e N' ⟹ M ∪ M' ⊫∪𝒢e N ∪ N'›
    by (rule entails_𝒢_disj_cut)
  show ‹⋀ M N. M ⊫∪𝒢e N ⟹ ∃ M' N'. M' ⊆ M ∧ N' ⊆ N ∧ finite M' ∧ finite N' ∧ M' ⊫∪𝒢e N'›
    by (rule entails_𝒢_disj_compactness)
qed

sublocale entails_𝒢_disj_cons_rel: consequence_relation ‹{#}› ‹(⊫∪𝒢e)›
  by (rule entails_𝒢_disj_cons_rel_ext)

notation entails_𝒢_disj_cons_rel.entails_neg (infix ‹⊫∪𝒢e⇩∼› 50)

lemma all_redundant_to_bottom: ‹𝒞 ≠ {#} ⟹ 𝒞 ∈ F.Red_F_𝒢_empty {{#}}›
  unfolding F.Red_F_𝒢_empty_def F.Red_F_𝒢_empty_q_def G.Red_F_def
proof -
  assume C_not_empty: ‹𝒞 ≠ {#}›
  have ‹D ∈ 𝒢_F 𝒞 ⟹ ∃DD⊆{{#}}. (∀I. I ⊫s DD ⟶ I ⊫ D) ∧ (∀Da∈DD. Da < D)› for D
  proof -
    fix D :: ‹'a clause›
  
    assume ‹D ∈ 𝒢_F 𝒞›
    then have ‹D ≠ {#}›
      using C_not_empty unfolding 𝒢_F_def by force 
    then have ‹{#} < D›
      by auto 
    moreover have ‹∀ I. I ⊫s {{#}} ⟶ I ⊫ D›
      by blast
    ultimately show ‹∃ E ⊆ {{#}}. (∀I. I ⊫s E ⟶ I ⊫ D) ∧ (∀ C ∈ E. C < D)›
      by blast
  qed
  then show ‹𝒞 ∈ (⋂q. {C. ∀D∈𝒢_F C. D ∈ {C. ∃DD⊆⋃ (𝒢_F ` {{#}}). DD ⊫∩e {C} ∧ (∀D∈DD. D < C)}})›
    by simp
qed 

lemma bottom_never_redundant: ‹{#} ∉ F.Red_F_𝒢_empty N›
  unfolding F.Red_F_𝒢_empty_def F.Red_F_𝒢_empty_q_def G.Red_F_def
  by auto

lemma ‹F.Inf_between UNIV (F.Red_F_𝒢_empty N) ⊆ F.empty_ord.Red_Red_I N›
  using F.empty_ord.inf_subs_reduced_red_inf .

end (* locale FO_resolution_prover_disjunctive *)


subsection ‹Lightweight Avatar without BinSplit›

text ‹ Since the set ‹ℙ› of nullary predicates is left unspecified, we cannot define ‹fml› nor ‹asn›.
 Therefore, we keep them abstract and leave it to anybody instantiating this locale
 to specify them. ›

locale LA_calculus = FO_resolution_prover_disjunctive S subst_atm id_subst comp_subst renaming_aparts
  atm_of_atms mgu less_atm
  for
    S :: ‹('a :: wellorder) clause ⇒ 'a clause› and 
    subst_atm :: ‹'a ⇒ 's ⇒ 'a› and 
    id_subst :: ‹'s› and 
    comp_subst :: ‹'s ⇒ 's ⇒ 's› and 
    renaming_aparts :: ‹'a clause list ⇒ 's list› and 
    atm_of_atms :: ‹'a list ⇒ 'a› and 
    mgu :: ‹'a set set ⇒ 's option› and 
    less_atm :: ‹'a ⇒ 'a ⇒ bool› 
  + fixes
    asn :: ‹'a clause sign ⇒ ('v :: countable) sign set› and
    fml :: ‹'v ⇒ 'a clause›
  assumes
    asn_not_empty: ‹asn C ≠ {}› and
    fml_entails_C: ‹a ∈ asn C ⟹ {map_sign fml a} ⊫∪𝒢e⇩∼ {C}› and
    C_entails_fml: ‹a ∈ asn C ⟹ {C} ⊫∪𝒢e⇩∼ {map_sign fml a}› 
begin

interpretation entails_𝒢_disj_sound_inf_system:
  Calculi_And_Annotations.sound_inference_system F_Inf ‹{#}› ‹(⊫∪𝒢e)›
proof standard
  have ‹⋀ ι. ι ∈ F_Inf ⟹ set (prems_of ι) ⊫∩𝒢e {concl_of ι}›
    using F.sound
    by blast
  then show ‹⋀ ι. ι ∈ F_Inf ⟹ set (prems_of ι) ⊫∪𝒢e {concl_of ι}›
    using entails_𝒢_disj_def by blast

qed

interpretation LA_is_calculus: calculus ‹{#}› F_Inf ‹(⊫∪𝒢e)› F.empty_ord.Red_Red_I F.Red_F_𝒢_empty
proof standard 
  show ‹⋀ N. F.empty_ord.Red_Red_I N ⊆ F_Inf›
    using F'.Red_I_to_Inf
    by blast
  show ‹⋀ N. N ⊫∪𝒢e {{#}} ⟹ N - F.Red_F_𝒢_empty N ⊫∪𝒢e {{#}}›
    using F.empty_ord.Red_F_Bot
    by (metis (no_types, lifting) entails_𝒢_disj_def sat_𝒢_compact singleton_iff)
  show ‹⋀ N N'. N ⊆ N' ⟹ F.Red_F_𝒢_empty N ⊆ F.Red_F_𝒢_empty N'›
    using F.empty_ord.Red_F_of_subset
    by presburger
  show ‹⋀ N N'. N ⊆ N' ⟹ F.empty_ord.Red_Red_I N ⊆ F.empty_ord.Red_Red_I N'› 
    using F'.Red_I_of_subset
    by presburger
  show ‹⋀ N' N. N' ⊆ F.Red_F_𝒢_empty N ⟹ F.Red_F_𝒢_empty N ⊆ F.Red_F_𝒢_empty (N - N')›
    using F.empty_ord.Red_F_of_Red_F_subset
    by blast
  show ‹⋀ N' N. N' ⊆ F.Red_F_𝒢_empty N ⟹ F.empty_ord.Red_Red_I N ⊆ F.empty_ord.Red_Red_I (N - N')›
    using F'.Red_I_of_Red_F_subset
    by presburger
  show ‹⋀ ι N. ι ∈ F_Inf ⟹ concl_of ι ∈ N ⟹ ι ∈ F.empty_ord.Red_Red_I N›
    using F'.Red_I_of_Inf_to_N
    by blast
qed


interpretation LA_is_sound_calculus: sound_calculus ‹{#}› F_Inf ‹(⊫∪𝒢e)› ‹(⊫∪𝒢e)›
  F.empty_ord.Red_Red_I F.Red_F_𝒢_empty 
  using LA_is_calculus.Red_I_to_Inf LA_is_calculus.Red_F_Bot  LA_is_calculus.Red_F_of_subset 
        LA_is_calculus.Red_I_of_subset  LA_is_calculus.Red_F_of_Red_F_subset
        LA_is_calculus.Red_I_of_Red_F_subset LA_is_calculus.Red_I_of_Inf_to_N
  by (unfold_locales, presburger+)

interpretation LA_is_AF_calculus: calculus_with_annotated_consrel ‹{#}› F_Inf ‹(⊫∪𝒢e)› ‹(⊫∪𝒢e)›
  F.empty_ord.Red_Red_I F.Red_F_𝒢_empty fml asn
proof standard
  show ‹⋀ C. ∀ a ∈ asn C. {map_sign fml a} ⊫∪𝒢e⇩∼ {C}›
    using fml_entails_C
    by blast
  show ‹⋀ C. ∀ a ∈ asn C. {C} ⊫∪𝒢e⇩∼ {map_sign fml a}›
    using C_entails_fml
    by blast
  show ‹⋀ C. asn C ≠ {}›
    by (rule asn_not_empty) 
qed

(*<*)
lemma empty_not_unsat: ‹¬ {} ⊫∩𝒢e {{#}}›
  using unsat_equiv3
  by blast
(*>*)

interpretation core_LA_calculus: splitting_calculus ‹{#}› F_Inf ‹(⊫∪𝒢e)› ‹(⊫∪𝒢e)›
  F.empty_ord.Red_Red_I F.Red_F_𝒢_empty fml asn 
proof standard
  show ‹¬ {} ⊫∪𝒢e {}›
    unfolding entails_𝒢_disj_def using empty_not_unsat by blast
  show ‹⋀ N. F.Inf_between UNIV (F.Red_F_𝒢_empty N) ⊆ F.empty_ord.Red_Red_I N›
    using F.empty_ord.inf_subs_reduced_red_inf by blast
  show ‹⋀ N. {#} ∉ F.Red_F_𝒢_empty N›
    using bottom_never_redundant by blast
  show ‹⋀ 𝒞. 𝒞 ≠ {#} ⟹ 𝒞 ∈ F.Red_F_𝒢_empty {{#}}›
    using all_redundant_to_bottom by blast
qed

notation LA_is_AF_calculus.AF_entails_sound (infix ‹⊫s∪𝒢e⇩A⇩F› 50)
notation LA_is_AF_calculus.AF_entails (infix ‹⊨∪𝒢e⇩A⇩F› 50)

interpretation AF_calculus_extended ‹to_AF {#}› 
  core_LA_calculus.core.SInf ‹(⊨∪𝒢e⇩A⇩F)› ‹(⊫s∪𝒢e⇩A⇩F)› core_LA_calculus.core.SRed⇩I 
  core_LA_calculus.core.SRed⇩F "{}" "{}"
  using core_LA_calculus.empty_simps.AF_calculus_extended_axioms .

subsection ‹Lightweight Avatar›

text ‹
  We now augment the earlier calculus into ‹LA› with the simplification rule \textsc{BinSplit}.
› 

interpretation with_BinSplit: AF_calculus_with_binsplit ‹to_AF {#}› core_LA_calculus.core.SInf
  LA_is_AF_calculus.AF_entails LA_is_AF_calculus.AF_entails_sound core_LA_calculus.core.SRed⇩I 
  core_LA_calculus.core.SRed⇩F ‹{}› ‹{}› core_LA_calculus.bin_splittable
  using core_LA_calculus.extend_simps_with_binsplit[OF 
      core_LA_calculus.empty_simps.AF_calculus_extended_axioms] .

sublocale LA: AF_calculus_extended ‹to_AF {#}› 
  core_LA_calculus.core.SInf LA_is_AF_calculus.AF_entails LA_is_AF_calculus.AF_entails_sound 
  core_LA_calculus.core.SRed⇩I core_LA_calculus.core.SRed⇩F with_BinSplit.Simps_with_BinSplit ‹{}›
  using with_BinSplit.AF_calc_ext.AF_calculus_extended_axioms .

text ‹
   By Theorem @{thm annotated_calculus.S_calculus_statically_complete}, we can show that ‹LA› is
  statically complete, and therefore dynamically complete by Theorem
  @{thm annotated_calculus.S_calculus_dynamically_complete}.
›


lemma F_disj_complete: ‹statically_complete_calculus {#} F_Inf (⊫∪𝒢e) F.empty_ord.Red_Red_I
  F.Red_F_𝒢_empty›
proof
  show ‹⋀ N. LA_is_calculus.saturated N ⟹ N ⊫∪𝒢e {{#}} ⟹ {#} ∈ N›
    unfolding LA_is_calculus.saturated_def using F'.saturated_def F'.statically_complete
    by (smt (verit, ccfv_SIG) entails_𝒢_disj_def insertI1 sat_𝒢_compact singletonD)
qed

(* Local static completeness (as other forms of completeness, global, dynamic...)
   follows from static completeness of the base calculus *)
theorem strong_static_comp: 
  ‹LA_is_AF_calculus.locally_saturated 𝒩 ⟹ 𝒩 ⊨∪𝒢e⇩A⇩F {to_AF {#}} ⟹ to_AF {#} ∈ 𝒩›
  using core_LA_calculus.core.S_calculus_strong_statically_complete[OF F_disj_complete] .

sublocale strong_statically_complete_annotated_calculus ‹{#}› F_Inf "(⊫∪𝒢e)" "(⊫∪𝒢e)" 
  F.empty_ord.Red_Red_I F.Red_F_𝒢_empty fml asn  core_LA_calculus.core.SInf 
  core_LA_calculus.core.SRed⇩I core_LA_calculus.core.SRed⇩F
  using strong_static_comp by (unfold_locales, blast)

theorem strong_dynamic_comp: ‹is_derivation core_LA_calculus.core.S_calculus.derive 𝒩i ⟹ 
  LA_is_AF_calculus.locally_fair 𝒩i ⟹ llhd 𝒩i ⊨∪𝒢e⇩A⇩F {to_AF {#}} ⟹ 
  (∃ i. to_AF {#} ∈ llnth 𝒩i i)›
  using core_LA_calculus.core.S_calculus_strong_dynamically_complete[OF F_disj_complete] .

sublocale strong_dynamically_complete_annotated_calculus ‹{#}› F_Inf "(⊫∪𝒢e)" "(⊫∪𝒢e)" 
  F.empty_ord.Red_Red_I F.Red_F_𝒢_empty fml asn  core_LA_calculus.core.SInf 
  core_LA_calculus.core.SRed⇩I core_LA_calculus.core.SRed⇩F
  using strong_dynamic_comp by (unfold_locales, blast)


end (* locale LA_calculus *)

end (* theory Modular Lightweight_Avatar *)