Theory Partial_Herbrand_Interpretation

(* Title: Partial Clausal Logic
    Author: Mathias Fleury <mathias.fleury@mpi-inf.mpg.de>

This theory is based on Blanchette's and Traytel's Clausal logic
*)
section ‹Partial Herbrand Interpretation›

theory Partial_Herbrand_Interpretation
  imports
    Weidenbach_Book_Base.WB_List_More
    Ordered_Resolution_Prover.Clausal_Logic
begin

subsection ‹More Literals›

text ‹The following lemma is very useful when in the goal appears an axioms like @{term ‹-L = K›}:
  this lemma allows the simplifier to rewrite L.›
lemma in_image_uminus_uminus: ‹a ∈ uminus ` A ⟷ -a ∈ A› for a :: ‹'v literal›
  using uminus_lit_swap by auto

lemma uminus_lit_swap: "- a = b ⟷ (a::'a literal) = - b"
  by auto

lemma atm_of_notin_atms_of_iff: ‹atm_of L ∉ atms_of C' ⟷ L ∉# C' ∧ -L ∉# C'› for L C'
  by (cases L) (auto simp: atm_iff_pos_or_neg_lit)

lemma atm_of_notin_atms_of_iff_Pos_Neg:
   ‹L ∉ atms_of C' ⟷ Pos L ∉# C' ∧ Neg L ∉# C'› for L C'
  by (auto simp: atm_iff_pos_or_neg_lit)

lemma atms_of_uminus[simp]: ‹atms_of (uminus `# C) = atms_of C›
  by (auto simp: atms_of_def image_image)

lemma distinct_mset_atm_ofD:
  ‹distinct_mset (atm_of `# mset xc) ⟹ distinct xc›
  by (induction xc) auto

lemma atms_of_cong_set_mset:
  ‹set_mset D = set_mset D' ⟹ atms_of D = atms_of D'›
  by (auto simp: atms_of_def)

lemma lit_in_set_iff_atm:
  ‹NO_MATCH (Pos x) l ⟹ NO_MATCH (Neg x) l ⟹
    l ∈ M ⟷ (∃l'. (l = Pos l' ∧ Pos l' ∈ M) ∨ (l = Neg l' ∧ Neg l' ∈ M))›
  by (cases l) auto


text ‹We define here entailment by a set of literals. This is an Herbrand interpretation, but not
  the same as used for the resolution prover. Both has different properties.
  One key difference is that such a set can be inconsistent (i.e.\
  containing both @{term "L::'a literal"} and @{term "-L::'a literal"}).

  Satisfiability is defined by the existence of a total and consistent model.
›

lemma lit_eq_Neg_Pos_iff:
  ‹x ≠ Neg (atm_of x) ⟷ is_pos x›
  ‹x ≠ Pos (atm_of x) ⟷ is_neg x›
  ‹-x ≠ Neg (atm_of x) ⟷ is_neg x›
  ‹-x ≠ Pos (atm_of x) ⟷ is_pos x›
  ‹Neg (atm_of x) ≠ x ⟷ is_pos x›
  ‹Pos (atm_of x) ≠ x ⟷ is_neg x›
  ‹Neg (atm_of x) ≠ -x ⟷ is_neg x›
  ‹Pos (atm_of x) ≠ -x ⟷ is_pos x›
  by (cases x; auto; fail)+


subsection ‹Clauses›

text ‹
Clauses are set of literals or (finite) multisets of literals.
›
type_synonym 'v clause_set = "'v clause set"
type_synonym 'v clauses = "'v clause multiset"

lemma is_neg_neg_not_is_neg: "is_neg (- L) ⟷ ¬ is_neg L"
  by (cases L) auto


subsection ‹Partial Interpretations›

type_synonym 'a partial_interp = "'a literal set"

definition true_lit :: "'a partial_interp ⇒ 'a literal ⇒ bool" (infix "⊨l" 50) where
  "I ⊨l L ⟷ L ∈ I"

declare true_lit_def[simp]


subsubsection ‹Consistency›

definition consistent_interp :: "'a literal set ⇒ bool" where
"consistent_interp I ⟷ (∀L. ¬(L ∈ I ∧ - L ∈ I))"

lemma consistent_interp_empty[simp]:
  "consistent_interp {}" unfolding consistent_interp_def by auto

lemma consistent_interp_single[simp]:
  "consistent_interp {L}" unfolding consistent_interp_def by auto

lemma Ex_consistent_interp: ‹Ex consistent_interp›
  by (auto simp: consistent_interp_def)

lemma consistent_interp_subset:
  assumes
    "A ⊆ B" and
    "consistent_interp B"
  shows "consistent_interp A"
  using assms unfolding consistent_interp_def by auto

lemma consistent_interp_change_insert:
  "a ∉ A ⟹ -a ∉ A ⟹ consistent_interp (insert (-a) A) ⟷ consistent_interp (insert a A)"
  unfolding consistent_interp_def by fastforce

lemma consistent_interp_insert_pos[simp]:
  "a ∉ A ⟹ consistent_interp (insert a A) ⟷ consistent_interp A ∧ -a ∉ A"
  unfolding consistent_interp_def by auto

lemma consistent_interp_insert_not_in:
  "consistent_interp A ⟹ a ∉ A ⟹ -a ∉ A ⟹ consistent_interp (insert a A)"
  unfolding consistent_interp_def by auto

lemma consistent_interp_unionD: ‹consistent_interp (I ∪ I') ⟹ consistent_interp I'›
  unfolding consistent_interp_def by auto

lemma consistent_interp_insert_iff:
  ‹consistent_interp (insert L C) ⟷ consistent_interp C ∧ -L ∉ C›
  by (metis consistent_interp_def consistent_interp_insert_pos insert_absorb)


lemma (in -) distinct_consistent_distinct_atm:
  ‹distinct M ⟹ consistent_interp (set M) ⟹ distinct_mset (atm_of `# mset M)›
  by (induction M) (auto simp: atm_of_eq_atm_of)


subsubsection ‹Atoms›

text ‹We define here various lifting of @{term atm_of} (applied to a single literal) to set and
  multisets of literals.›
definition atms_of_ms :: "'a clause set ⇒ 'a set" where
"atms_of_ms ψs = ⋃(atms_of ` ψs)"

lemma atms_of_mmltiset[simp]:
  "atms_of (mset a) = atm_of ` set a"
  by (induct a) auto

lemma atms_of_ms_mset_unfold:
  "atms_of_ms (mset ` b) = (⋃x∈b. atm_of ` set x)"
  unfolding atms_of_ms_def by simp

definition atms_of_s :: "'a literal set ⇒ 'a set" where
  "atms_of_s C = atm_of ` C"

lemma atms_of_ms_emtpy_set[simp]:
  "atms_of_ms {} = {}"
  unfolding atms_of_ms_def by auto

lemma atms_of_ms_memtpy[simp]:
  "atms_of_ms {{#}} = {}"
  unfolding atms_of_ms_def by auto

lemma atms_of_ms_mono:
  "A ⊆ B ⟹ atms_of_ms A ⊆ atms_of_ms B"
  unfolding atms_of_ms_def by auto

lemma atms_of_ms_finite[simp]:
  "finite ψs ⟹ finite (atms_of_ms ψs)"
  unfolding atms_of_ms_def by auto

lemma atms_of_ms_union[simp]:
  "atms_of_ms (ψs ∪ χs) = atms_of_ms ψs ∪ atms_of_ms χs"
  unfolding atms_of_ms_def by auto

lemma atms_of_ms_insert[simp]:
  "atms_of_ms (insert ψs χs) = atms_of ψs ∪ atms_of_ms χs"
  unfolding atms_of_ms_def by auto

lemma atms_of_ms_singleton[simp]: "atms_of_ms {L} = atms_of L"
  unfolding atms_of_ms_def by auto

lemma atms_of_atms_of_ms_mono[simp]:
  "A ∈ ψ ⟹ atms_of A ⊆ atms_of_ms ψ"
  unfolding atms_of_ms_def by fastforce

lemma atms_of_ms_remove_incl:
  shows "atms_of_ms (Set.remove a ψ) ⊆ atms_of_ms ψ"
  unfolding atms_of_ms_def by auto

lemma atms_of_ms_remove_subset:
  "atms_of_ms (φ - ψ) ⊆ atms_of_ms φ"
  unfolding atms_of_ms_def by auto

lemma finite_atms_of_ms_remove_subset[simp]:
  "finite (atms_of_ms A) ⟹ finite (atms_of_ms (A - C))"
  using atms_of_ms_remove_subset[of A C] finite_subset by blast

lemma atms_of_ms_empty_iff:
  "atms_of_ms A = {} ⟷ A = {{#}} ∨ A = {}"
  apply (rule iffI)
   apply (metis (no_types, lifting) atms_empty_iff_empty atms_of_atms_of_ms_mono insert_absorb
    singleton_iff singleton_insert_inj_eq' subsetI subset_empty)
  apply (auto; fail)
  done

lemma in_implies_atm_of_on_atms_of_ms:
  assumes "L ∈# C" and "C ∈ N"
  shows "atm_of L ∈ atms_of_ms N"
  using atms_of_atms_of_ms_mono[of C N] assms by (simp add: atm_of_lit_in_atms_of subset_iff)

lemma in_plus_implies_atm_of_on_atms_of_ms:
  assumes "C+{#L#} ∈ N"
  shows "atm_of L ∈ atms_of_ms N"
  using in_implies_atm_of_on_atms_of_ms[of _ "C +{#L#}"] assms by auto

lemma in_m_in_literals:
  assumes "add_mset A D ∈ ψs"
  shows "atm_of A ∈ atms_of_ms ψs"
  using assms by (auto dest: atms_of_atms_of_ms_mono)

lemma atms_of_s_union[simp]:
  "atms_of_s (Ia ∪ Ib) = atms_of_s Ia ∪ atms_of_s Ib"
  unfolding atms_of_s_def by auto

lemma atms_of_s_single[simp]:
  "atms_of_s {L} = {atm_of L}"
  unfolding atms_of_s_def by auto

lemma atms_of_s_insert[simp]:
  "atms_of_s (insert L Ib) = {atm_of L} ∪ atms_of_s Ib"
  unfolding atms_of_s_def by auto

lemma in_atms_of_s_decomp[iff]:
  "P ∈ atms_of_s I ⟷ (Pos P ∈ I ∨ Neg P ∈ I)" (is "?P ⟷ ?Q")
proof
  assume ?P
  then show ?Q unfolding atms_of_s_def by (metis image_iff literal.exhaust_sel)
next
  assume ?Q
  then show ?P unfolding atms_of_s_def by force
qed

lemma atm_of_in_atm_of_set_in_uminus:
  "atm_of L' ∈ atm_of ` B ⟹ L' ∈ B ∨ - L' ∈ B"
  using atms_of_s_def by (cases L') fastforce+

lemma finite_atms_of_s[simp]:
  ‹finite M ⟹ finite (atms_of_s M)›
  by (auto simp: atms_of_s_def)

lemma
  atms_of_s_empty [simp]:
    ‹atms_of_s {} = {}› and
  atms_of_s_empty_iff[simp]:
    ‹atms_of_s x = {} ⟷ x = {}›
  by (auto simp: atms_of_s_def)


subsubsection ‹Totality›

definition total_over_set :: "'a partial_interp ⇒ 'a set ⇒ bool" where
"total_over_set I S = (∀l∈S. Pos l ∈ I ∨ Neg l ∈ I)"

definition total_over_m :: "'a literal set ⇒ 'a clause set ⇒ bool" where
"total_over_m I ψs = total_over_set I (atms_of_ms ψs)"

lemma total_over_set_empty[simp]:
  "total_over_set I {}"
  unfolding total_over_set_def by auto

lemma total_over_m_empty[simp]:
  "total_over_m I {}"
  unfolding total_over_m_def by auto

lemma total_over_set_single[iff]:
  "total_over_set I {L} ⟷ (Pos L ∈ I ∨ Neg L ∈ I)"
  unfolding total_over_set_def by auto

lemma total_over_set_insert[iff]:
  "total_over_set I (insert L Ls) ⟷ ((Pos L ∈ I ∨ Neg L ∈ I) ∧ total_over_set I Ls)"
  unfolding total_over_set_def by auto

lemma total_over_set_union[iff]:
  "total_over_set I (Ls ∪ Ls') ⟷ (total_over_set I Ls ∧ total_over_set I Ls')"
  unfolding total_over_set_def by auto

lemma total_over_m_subset:
  "A ⊆ B ⟹ total_over_m I B ⟹ total_over_m I A"
  using atms_of_ms_mono[of A] unfolding total_over_m_def total_over_set_def by auto

lemma total_over_m_sum[iff]:
  shows "total_over_m I {C + D} ⟷ (total_over_m I {C} ∧ total_over_m I {D})"
  unfolding total_over_m_def total_over_set_def by auto

lemma total_over_m_union[iff]:
  "total_over_m I (A ∪ B) ⟷ (total_over_m I A ∧ total_over_m I B)"
  unfolding total_over_m_def total_over_set_def by auto

lemma total_over_m_insert[iff]:
  "total_over_m I (insert a A) ⟷ (total_over_set I (atms_of a) ∧ total_over_m I A)"
  unfolding total_over_m_def total_over_set_def by fastforce

lemma total_over_m_extension:
  fixes I :: "'v literal set" and A :: "'v clause_set"
  assumes total: "total_over_m I A"
  shows "∃I'. total_over_m (I ∪ I') (A∪B)
    ∧ (∀x∈I'. atm_of x ∈ atms_of_ms B ∧ atm_of x ∉ atms_of_ms A)"
proof -
  let ?I' = "{Pos v |v. v∈ atms_of_ms B ∧ v ∉ atms_of_ms A}"
  have "∀x∈?I'. atm_of x ∈ atms_of_ms B ∧ atm_of x ∉ atms_of_ms A" by auto
  moreover have "total_over_m (I ∪ ?I') (A∪B)"
    using total unfolding total_over_m_def total_over_set_def by auto
  ultimately show ?thesis by blast
qed

lemma total_over_m_consistent_extension:
  fixes I :: "'v literal set" and A :: "'v clause_set"
  assumes
    total: "total_over_m I A" and
    cons: "consistent_interp I"
  shows "∃I'. total_over_m (I ∪ I') (A ∪ B)
    ∧ (∀x∈I'. atm_of x ∈ atms_of_ms B ∧ atm_of x ∉ atms_of_ms A) ∧ consistent_interp (I ∪ I')"
proof -
  let ?I' = "{Pos v |v. v∈ atms_of_ms B ∧ v ∉ atms_of_ms A ∧ Pos v ∉ I ∧ Neg v ∉ I}"
  have "∀x∈?I'. atm_of x ∈ atms_of_ms B ∧ atm_of x ∉ atms_of_ms A" by auto
  moreover have "total_over_m (I ∪ ?I') (A∪B)"
    using total unfolding total_over_m_def total_over_set_def by auto
  moreover have "consistent_interp (I ∪ ?I')"
    using cons unfolding consistent_interp_def by (intro allI) (rename_tac L, case_tac L, auto)
  ultimately show ?thesis by blast
qed

lemma total_over_set_atms_of_m[simp]:
  "total_over_set Ia (atms_of_s Ia)"
  unfolding total_over_set_def atms_of_s_def by (metis image_iff literal.exhaust_sel)

lemma total_over_set_literal_defined:
  assumes "add_mset A D ∈ ψs"
  and "total_over_set I (atms_of_ms ψs)"
  shows "A ∈ I ∨ -A ∈ I"
  using assms unfolding total_over_set_def by (metis (no_types) Neg_atm_of_iff in_m_in_literals
    literal.collapse(1) uminus_Neg uminus_Pos)

lemma tot_over_m_remove:
  assumes "total_over_m (I ∪ {L}) {ψ}"
  and L: "L ∉# ψ" "-L ∉# ψ"
  shows "total_over_m I {ψ}"
  unfolding total_over_m_def total_over_set_def
proof
  fix l
  assume l: "l ∈ atms_of_ms {ψ}"
  then have "Pos l ∈ I ∨ Neg l ∈ I ∨ l = atm_of L"
    using assms unfolding total_over_m_def total_over_set_def by auto
  moreover have "atm_of L ∉ atms_of_ms {ψ}"
    proof (rule ccontr)
      assume "¬ ?thesis"
      then have "atm_of L ∈ atms_of ψ" by auto
      then have "Pos (atm_of L) ∈# ψ ∨ Neg (atm_of L) ∈# ψ"
        using atm_imp_pos_or_neg_lit by metis
      then have "L ∈# ψ ∨ - L ∈# ψ" by (cases L) auto
      then show False using L by auto
    qed
  ultimately show "Pos l ∈ I ∨ Neg l ∈ I" using l by metis
qed

lemma total_union:
  assumes "total_over_m I ψ"
  shows "total_over_m (I ∪ I') ψ"
  using assms unfolding total_over_m_def total_over_set_def by auto

lemma total_union_2:
  assumes "total_over_m I ψ"
  and "total_over_m I' ψ'"
  shows "total_over_m (I ∪ I') (ψ ∪ ψ')"
  using assms unfolding total_over_m_def total_over_set_def by auto

lemma total_over_m_alt_def: ‹total_over_m I S ⟷ atms_of_ms S ⊆ atms_of_s I›
  by (auto simp: total_over_m_def total_over_set_def)

lemma total_over_set_alt_def: ‹total_over_set M A ⟷ A ⊆ atms_of_s M›
  by (auto simp: total_over_set_def)


subsubsection ‹Interpretations›

definition true_cls :: "'a partial_interp ⇒ 'a clause ⇒ bool" (infix "⊨" 50) where
  "I ⊨ C ⟷ (∃L ∈# C. I ⊨l L)"

lemma true_cls_empty[iff]: "¬ I ⊨ {#}"
  unfolding true_cls_def by auto

lemma true_cls_singleton[iff]: "I ⊨ {#L#} ⟷ I ⊨l L"
  unfolding true_cls_def by (auto split:if_split_asm)

lemma true_cls_add_mset[iff]: "I ⊨ add_mset a D ⟷ a ∈ I ∨ I ⊨ D"
  unfolding true_cls_def by auto

lemma true_cls_union[iff]: "I ⊨ C + D ⟷ I ⊨ C ∨ I ⊨ D"
  unfolding true_cls_def by auto

lemma true_cls_mono_set_mset: "set_mset C ⊆ set_mset D ⟹ I ⊨ C ⟹ I ⊨ D"
  unfolding true_cls_def subset_eq Bex_def by metis

lemma true_cls_mono_leD[dest]: "A ⊆# B ⟹ I ⊨ A ⟹ I ⊨ B"
  unfolding true_cls_def by auto

lemma
  assumes "I ⊨ ψ"
  shows
    true_cls_union_increase[simp]: "I ∪ I' ⊨ ψ" and
    true_cls_union_increase'[simp]: "I' ∪ I ⊨ ψ"
  using assms unfolding true_cls_def by auto

lemma true_cls_mono_set_mset_l:
  assumes "A ⊨ ψ"
  and "A ⊆ B"
  shows "B ⊨ ψ"
  using assms unfolding true_cls_def by auto

lemma true_cls_replicate_mset[iff]: "I ⊨ replicate_mset n L ⟷ n ≠ 0 ∧ I ⊨l L"
  by (induct n) auto

lemma true_cls_empty_entails[iff]: "¬ {} ⊨ N"
  by (auto simp add: true_cls_def)

lemma true_cls_not_in_remove:
  assumes "L ∉# χ" and "I ∪ {L} ⊨ χ"
  shows "I ⊨ χ"
  using assms unfolding true_cls_def by auto

definition true_clss :: "'a partial_interp ⇒ 'a clause_set ⇒ bool" (infix "⊨s" 50) where
  "I ⊨s CC ⟷ (∀C ∈ CC. I ⊨ C)"

lemma true_clss_empty[simp]: "I ⊨s {}"
  unfolding true_clss_def by blast

lemma true_clss_singleton[iff]: "I ⊨s {C} ⟷ I ⊨ C"
  unfolding true_clss_def by blast

lemma true_clss_empty_entails_empty[iff]: "{} ⊨s N ⟷ N = {}"
  unfolding true_clss_def by (auto simp add: true_cls_def)

lemma true_cls_insert_l [simp]:
  "M ⊨ A ⟹ insert L M ⊨ A"
  unfolding true_cls_def by auto

lemma true_clss_union[iff]: "I ⊨s CC ∪ DD ⟷ I ⊨s CC ∧ I ⊨s DD"
  unfolding true_clss_def by blast

lemma true_clss_insert[iff]: "I ⊨s insert C DD ⟷ I ⊨ C ∧ I ⊨s DD"
  unfolding true_clss_def by blast

lemma true_clss_mono: "DD ⊆ CC ⟹ I ⊨s CC ⟹ I ⊨s DD"
  unfolding true_clss_def by blast

lemma true_clss_union_increase[simp]:
 assumes "I ⊨s ψ"
 shows "I ∪ I' ⊨s ψ"
 using assms unfolding true_clss_def by auto

lemma true_clss_union_increase'[simp]:
 assumes "I' ⊨s ψ"
 shows "I ∪ I' ⊨s ψ"
 using assms by (auto simp add: true_clss_def)

lemma true_clss_commute_l:
  "(I ∪ I' ⊨s ψ) ⟷ (I' ∪ I ⊨s ψ)"
  by (simp add: Un_commute)

lemma model_remove[simp]: "I ⊨s N ⟹ I ⊨s Set.remove a N"
  by (simp add: true_clss_def)

lemma model_remove_minus[simp]: "I ⊨s N ⟹ I ⊨s N - A"
  by (simp add: true_clss_def)

lemma notin_vars_union_true_cls_true_cls:
  assumes "∀x∈I'. atm_of x ∉ atms_of_ms A"
  and "atms_of L ⊆ atms_of_ms A"
  and "I ∪ I' ⊨ L"
  shows "I ⊨ L"
  using assms unfolding true_cls_def true_lit_def Bex_def
  by (metis Un_iff atm_of_lit_in_atms_of contra_subsetD)

lemma notin_vars_union_true_clss_true_clss:
  assumes "∀x∈I'. atm_of x ∉ atms_of_ms A"
  and "atms_of_ms L ⊆ atms_of_ms A"
  and "I ∪ I' ⊨s L"
  shows "I ⊨s L"
  using assms unfolding true_clss_def true_lit_def Ball_def
  by (meson atms_of_atms_of_ms_mono notin_vars_union_true_cls_true_cls subset_trans)

lemma true_cls_def_set_mset_eq:
  ‹set_mset A = set_mset B ⟹ I ⊨ A ⟷ I ⊨ B›
  by (auto simp: true_cls_def)

lemma true_cls_add_mset_strict: ‹I ⊨ add_mset L C ⟷ L ∈ I ∨ I ⊨ (removeAll_mset L C)›
  using true_cls_mono_set_mset[of ‹removeAll_mset L C› C I]
  apply (cases ‹L ∈# C›)
  apply (auto dest: multi_member_split simp: removeAll_notin)
  apply (metis (mono_tags, lifting) in_multiset_minus_notin_snd in_replicate_mset true_cls_def true_lit_def)
  done


subsubsection ‹Satisfiability›

definition satisfiable :: "'a clause set ⇒ bool" where
  "satisfiable CC ⟷ (∃I. (I ⊨s CC ∧ consistent_interp I ∧ total_over_m I CC))"

lemma satisfiable_single[simp]:
  "satisfiable {{#L#}}"
  unfolding satisfiable_def by fastforce

lemma satisfiable_empty[simp]: ‹satisfiable {}›
  by (auto simp: satisfiable_def Ex_consistent_interp)

abbreviation unsatisfiable :: "'a clause set ⇒ bool" where
  "unsatisfiable CC ≡ ¬ satisfiable CC"

lemma satisfiable_decreasing:
  assumes "satisfiable (ψ ∪ ψ')"
  shows "satisfiable ψ"
  using assms total_over_m_union unfolding satisfiable_def by blast

lemma satisfiable_def_min:
  "satisfiable CC
    ⟷ (∃I. I ⊨s CC ∧ consistent_interp I ∧ total_over_m I CC ∧ atm_of`I = atms_of_ms CC)"
    (is "?sat ⟷ ?B")
proof
  assume ?B then show ?sat by (auto simp add: satisfiable_def)
next
  assume ?sat
  then obtain I where
    I_CC: "I ⊨s CC" and
    cons: "consistent_interp I" and
    tot: "total_over_m I CC"
    unfolding satisfiable_def by auto
  let ?I = "{P. P ∈ I ∧ atm_of P ∈ atms_of_ms CC}"

  have I_CC: "?I ⊨s CC"
    using I_CC in_implies_atm_of_on_atms_of_ms unfolding true_clss_def Ball_def true_cls_def
    Bex_def true_lit_def
    by blast

  moreover have cons: "consistent_interp ?I"
    using cons unfolding consistent_interp_def by auto
  moreover have "total_over_m ?I CC"
    using tot unfolding total_over_m_def total_over_set_def by auto
  moreover
    have atms_CC_incl: "atms_of_ms CC ⊆ atm_of`I"
      using tot unfolding total_over_m_def total_over_set_def atms_of_ms_def
      by (auto simp add: atms_of_def atms_of_s_def[symmetric])
    have "atm_of ` ?I = atms_of_ms CC"
      using atms_CC_incl unfolding atms_of_ms_def by force
  ultimately show ?B by auto
qed

lemma satisfiable_carac:
  "(∃I. consistent_interp I ∧ I ⊨s φ) ⟷ satisfiable φ" (is "(∃I. ?Q I) ⟷ ?S")
proof
  assume "?S"
  then show "∃I. ?Q I" unfolding satisfiable_def by auto
next
  assume "∃I. ?Q I"
  then obtain I where cons: "consistent_interp I" and I: "I ⊨s φ" by metis
  let ?I' = "{Pos v |v. v ∉ atms_of_s I ∧ v ∈ atms_of_ms φ}"
  have "consistent_interp (I ∪ ?I')"
    using cons unfolding consistent_interp_def by (intro allI) (rename_tac L, case_tac L, auto)
  moreover have "total_over_m (I ∪ ?I') φ"
    unfolding total_over_m_def total_over_set_def by auto
  moreover have "I ∪ ?I' ⊨s φ"
    using I unfolding Ball_def true_clss_def true_cls_def by auto
  ultimately show ?S unfolding satisfiable_def by blast
qed

lemma satisfiable_carac'[simp]: "consistent_interp I ⟹ I ⊨s φ ⟹ satisfiable φ"
  using satisfiable_carac by metis

lemma unsatisfiable_mono:
  ‹N ⊆ N' ⟹ unsatisfiable N ⟹ unsatisfiable N'›
  by (metis (full_types) satisfiable_decreasing subset_Un_eq)


subsubsection ‹Entailment for Multisets of Clauses›

definition true_cls_mset :: "'a partial_interp ⇒ 'a clause multiset ⇒ bool" (infix "⊨m" 50) where
  "I ⊨m CC ⟷ (∀C ∈# CC. I ⊨ C)"

lemma true_cls_mset_empty[simp]: "I ⊨m {#}"
  unfolding true_cls_mset_def by auto

lemma true_cls_mset_singleton[iff]: "I ⊨m {#C#} ⟷ I ⊨ C"
  unfolding true_cls_mset_def by (auto split: if_split_asm)

lemma true_cls_mset_union[iff]: "I ⊨m CC + DD ⟷ I ⊨m CC ∧ I ⊨m DD"
  unfolding true_cls_mset_def by fastforce

lemma true_cls_mset_add_mset[iff]: "I ⊨m add_mset C CC ⟷ I ⊨ C ∧ I ⊨m CC"
  unfolding true_cls_mset_def by auto

lemma true_cls_mset_image_mset[iff]: "I ⊨m image_mset f A ⟷ (∀x ∈# A. I ⊨ f x)"
  unfolding true_cls_mset_def by fastforce

lemma true_cls_mset_mono: "set_mset DD ⊆ set_mset CC ⟹ I ⊨m CC ⟹ I ⊨m DD"
  unfolding true_cls_mset_def subset_iff by auto

lemma true_clss_set_mset[iff]: "I ⊨s set_mset CC ⟷ I ⊨m CC"
  unfolding true_clss_def true_cls_mset_def by auto

lemma true_cls_mset_increasing_r[simp]:
  "I ⊨m CC ⟹ I ∪ J ⊨m CC"
  unfolding true_cls_mset_def by auto

theorem true_cls_remove_unused:
  assumes "I ⊨ ψ"
  shows "{v ∈ I. atm_of v ∈ atms_of ψ} ⊨ ψ"
  using assms unfolding true_cls_def atms_of_def by auto

theorem true_clss_remove_unused:
  assumes "I ⊨s ψ"
  shows "{v ∈ I. atm_of v ∈ atms_of_ms ψ} ⊨s ψ"
  unfolding true_clss_def atms_of_def Ball_def
proof (intro allI impI)
  fix x
  assume "x ∈ ψ"
  then have "I ⊨ x"
    using assms unfolding true_clss_def atms_of_def Ball_def by auto

  then have "{v ∈ I. atm_of v ∈ atms_of x} ⊨ x"
    by (simp only: true_cls_remove_unused[of I])
  moreover have "{v ∈ I. atm_of v ∈ atms_of x} ⊆ {v ∈ I. atm_of v ∈ atms_of_ms ψ}"
    using ‹x ∈ ψ› by (auto simp add: atms_of_ms_def)
  ultimately show "{v ∈ I. atm_of v ∈ atms_of_ms ψ} ⊨ x"
    using true_cls_mono_set_mset_l by blast
qed

text ‹A simple application of the previous theorem:›
lemma true_clss_union_decrease:
  assumes II': "I ∪ I' ⊨ ψ"
  and H: "∀v ∈ I'. atm_of v ∉ atms_of ψ"
  shows "I ⊨ ψ"
proof -
  let ?I = "{v ∈ I ∪ I'. atm_of v ∈ atms_of ψ}"
  have "?I ⊨ ψ" using true_cls_remove_unused II' by blast
  moreover have "?I ⊆ I" using H by auto
  ultimately show ?thesis using true_cls_mono_set_mset_l by blast
qed

lemma multiset_not_empty:
  assumes "M ≠ {#}"
  and "x ∈# M"
  shows "∃A. x = Pos A ∨ x = Neg A"
  using assms literal.exhaust_sel by blast

lemma atms_of_ms_empty:
  fixes ψ :: "'v clause_set"
  assumes "atms_of_ms ψ = {}"
  shows "ψ = {} ∨ ψ = {{#}}"
  using assms by (auto simp add: atms_of_ms_def)

lemma consistent_interp_disjoint:
 assumes consI: "consistent_interp I"
 and disj: "atms_of_s A ∩ atms_of_s I = {}"
 and consA: "consistent_interp A"
 shows "consistent_interp (A ∪ I)"
proof (rule ccontr)
  assume "¬ ?thesis"
  moreover have "⋀L. ¬ (L ∈ A ∧ -L ∈ I)"
    using disj unfolding atms_of_s_def by (auto simp add: rev_image_eqI)
  ultimately show False
    using consA consI unfolding consistent_interp_def by (metis (full_types) Un_iff
      literal.exhaust_sel uminus_Neg uminus_Pos)
qed

lemma total_remove_unused:
  assumes "total_over_m I ψ"
  shows "total_over_m {v ∈ I. atm_of v ∈ atms_of_ms ψ} ψ"
  using assms unfolding total_over_m_def total_over_set_def
  by (metis (lifting) literal.sel(1,2) mem_Collect_eq)

lemma true_cls_remove_hd_if_notin_vars:
  assumes "insert a M'⊨ D"
  and "atm_of a ∉ atms_of D"
  shows "M' ⊨ D"
  using assms by (auto simp add: atm_of_lit_in_atms_of true_cls_def)

lemma total_over_set_atm_of:
  fixes I :: "'v partial_interp" and K :: "'v set"
  shows "total_over_set I K ⟷ (∀l ∈ K. l ∈ (atm_of ` I))"
  unfolding total_over_set_def by (metis atms_of_s_def in_atms_of_s_decomp)

lemma true_cls_mset_true_clss_iff:
  ‹finite C ⟹ I ⊨m mset_set C ⟷ I ⊨s C›
  ‹I ⊨m D ⟷ I ⊨s set_mset D›
  by (auto simp: true_clss_def true_cls_mset_def Ball_def
    dest: multi_member_split)


subsubsection ‹Tautologies›

text ‹We define tautologies as clause entailed by every total model and show later that is
  equivalent to containing a literal and its negation.›
definition "tautology (ψ:: 'v clause) ≡ ∀I. total_over_set I (atms_of ψ) ⟶ I ⊨ ψ"

lemma tautology_Pos_Neg[intro]:
  assumes "Pos p ∈# A" and "Neg p ∈# A"
  shows "tautology A"
  using assms unfolding tautology_def total_over_set_def true_cls_def Bex_def
  by (meson atm_iff_pos_or_neg_lit true_lit_def)

lemma tautology_minus[simp]:
  assumes "L ∈# A" and "-L ∈# A"
  shows "tautology A"
  by (metis assms literal.exhaust tautology_Pos_Neg uminus_Neg uminus_Pos)

lemma tautology_exists_Pos_Neg:
  assumes "tautology ψ"
  shows "∃p. Pos p ∈# ψ ∧ Neg p ∈# ψ"
proof (rule ccontr)
  assume p: "¬ (∃p. Pos p ∈# ψ ∧ Neg p ∈# ψ)"
  let ?I = "{-L | L. L ∈# ψ}"
  have "total_over_set ?I (atms_of ψ)"
    unfolding total_over_set_def using atm_imp_pos_or_neg_lit by force
  moreover have "¬ ?I ⊨ ψ"
    unfolding true_cls_def true_lit_def Bex_def apply clarify
    using p by (rename_tac x L, case_tac L) fastforce+
  ultimately show False using assms unfolding tautology_def by auto
qed

lemma tautology_decomp:
  "tautology ψ ⟷ (∃p. Pos p ∈# ψ ∧ Neg p ∈# ψ)"
  using tautology_exists_Pos_Neg by auto

lemma tautology_union_add_iff[simp]:
  ‹tautology (A ∪# B) ⟷ tautology (A + B)›
  by (auto simp: tautology_decomp)
lemma tautology_add_mset_union_add_iff[simp]:
  ‹tautology (add_mset L (A ∪# B)) ⟷ tautology (add_mset L (A + B))›
  by (auto simp: tautology_decomp)

lemma not_tautology_minus:
  ‹¬tautology A ⟹ ¬tautology (A - B)›
  by (auto simp: tautology_decomp dest: in_diffD)

lemma tautology_false[simp]: "¬tautology {#}"
  unfolding tautology_def by auto

lemma tautology_add_mset:
  "tautology (add_mset a L) ⟷ tautology L ∨ -a ∈# L"
  unfolding tautology_decomp by (cases a) auto

lemma tautology_single[simp]: ‹¬tautology {#L#}›
  by (simp add: tautology_add_mset)

lemma tautology_union:
  ‹tautology (A + B) ⟷ tautology A ∨ tautology B ∨ (∃a. a ∈# A ∧ -a ∈# B)›
  by (metis tautology_decomp tautology_minus uminus_Neg uminus_Pos union_iff)

lemma
  tautology_poss[simp]: ‹¬tautology (poss A)› and
  tautology_negs[simp]: ‹¬tautology (negs A)›
  by (auto simp: tautology_decomp)

lemma tautology_uminus[simp]:
  ‹tautology (uminus `# w) ⟷ tautology w›
  by (auto 5 5 simp: tautology_decomp add_mset_eq_add_mset eq_commute[of ‹Pos _› ‹-_›]
     eq_commute[of ‹Neg _› ‹-_›]
    simp flip: uminus_lit_swap
    dest!: multi_member_split)

lemma minus_interp_tautology:
  assumes "{-L | L. L∈# χ} ⊨ χ"
  shows "tautology χ"
proof -
  obtain L where "L ∈# χ ∧ -L ∈# χ"
    using assms unfolding true_cls_def by auto
  then show ?thesis using tautology_decomp literal.exhaust uminus_Neg uminus_Pos by metis
qed

lemma remove_literal_in_model_tautology:
  assumes "I ∪ {Pos P} ⊨ φ"
  and "I ∪ {Neg P} ⊨ φ"
  shows "I ⊨ φ ∨ tautology φ"
  using assms unfolding true_cls_def by auto

lemma tautology_imp_tautology:
  fixes χ χ' :: "'v clause"
  assumes "∀I. total_over_m I {χ} ⟶ I ⊨ χ ⟶ I ⊨ χ'" and "tautology χ"
  shows "tautology χ'" unfolding tautology_def
proof (intro allI HOL.impI)
  fix I ::"'v literal set"
  assume totI: "total_over_set I (atms_of χ')"
  let ?I' = "{Pos v |v. v∈ atms_of χ ∧ v ∉ atms_of_s I}"
  have totI': "total_over_m (I ∪ ?I') {χ}" unfolding total_over_m_def total_over_set_def by auto
  then have χ: "I ∪ ?I' ⊨ χ" using assms(2) unfolding total_over_m_def tautology_def by simp
  then have "I ∪ (?I'- I) ⊨ χ'" using assms(1) totI' by auto
  moreover have "⋀L. L ∈# χ' ⟹ L ∉ ?I'"
    using totI unfolding total_over_set_def by (auto dest: pos_lit_in_atms_of)
  ultimately show "I ⊨ χ'" unfolding true_cls_def by auto
qed

lemma not_tautology_mono: ‹D' ⊆# D ⟹ ¬tautology D ⟹ ¬tautology D'›
  by (meson tautology_imp_tautology true_cls_add_mset true_cls_mono_leD)

lemma tautology_decomp':
  ‹tautology C ⟷ (∃L. L ∈# C ∧ - L ∈# C)›
  unfolding tautology_decomp
  apply auto
  apply (case_tac L)
   apply auto
  done

lemma consistent_interp_tautology:
  ‹consistent_interp (set M') ⟷ ¬tautology (mset M')›
  by (auto simp: consistent_interp_def tautology_decomp lit_in_set_iff_atm)

lemma consistent_interp_tuatology_mset_set:
  ‹finite x ⟹ consistent_interp x  ⟷ ¬tautology (mset_set x)›
  using ex_mset[of ‹mset_set x›]
  by (auto simp: consistent_interp_tautology eq_commute[of ‹mset _›] mset_set_eq_mset_iff
      mset_set_set)

lemma tautology_distinct_atm_iff:
  ‹distinct_mset C ⟹ tautology C ⟷ ¬distinct_mset (atm_of `# C)›
  by (induction C)
    (auto simp: tautology_add_mset atm_of_eq_atm_of
      dest: multi_member_split)

lemma not_tautology_minusD:
  ‹tautology (A - B) ⟹ tautology A›
  by (auto simp: tautology_decomp dest: in_diffD)

lemma tautology_length_ge2: ‹tautology C ⟹ size C ≥ 2›
  by (auto simp: tautology_decomp add_mset_eq_add_mset dest!: multi_member_split)

lemma tautology_add_subset: ‹A ⊆# Aa ⟹ tautology (A + Aa) ⟷ tautology Aa› for A Aa
  by (metis mset_subset_eqD subset_mset.add_diff_inverse tautology_minus tautology_union)



subsubsection ‹Entailment for clauses and propositions›

text ‹We also need entailment of clauses by other clauses.›
definition true_cls_cls :: "'a clause ⇒ 'a clause ⇒ bool" (infix "⊨f" 49) where
"ψ ⊨f χ ⟷ (∀I. total_over_m I ({ψ} ∪ {χ}) ⟶ consistent_interp I ⟶ I ⊨ ψ ⟶ I ⊨ χ)"

definition true_cls_clss :: "'a clause ⇒ 'a clause_set ⇒ bool" (infix "⊨fs" 49) where
"ψ ⊨fs χ ⟷ (∀I. total_over_m I ({ψ} ∪ χ) ⟶ consistent_interp I ⟶ I ⊨ ψ ⟶ I ⊨s χ)"

definition true_clss_cls :: "'a clause_set ⇒ 'a clause ⇒ bool" (infix "⊨p" 49) where
"N ⊨p χ ⟷ (∀I. total_over_m I (N ∪ {χ}) ⟶ consistent_interp I ⟶ I ⊨s N ⟶ I ⊨ χ)"

definition true_clss_clss :: "'a clause_set ⇒ 'a clause_set ⇒ bool" (infix "⊨ps" 49) where
"N ⊨ps N' ⟷ (∀I. total_over_m I (N ∪ N') ⟶ consistent_interp I ⟶ I ⊨s N ⟶ I ⊨s N')"

lemma true_cls_cls_refl[simp]:
  "A ⊨f A"
  unfolding true_cls_cls_def by auto

lemma true_clss_cls_empty_empty[iff]:
  ‹{} ⊨p {#} ⟷ False›
  unfolding true_clss_cls_def consistent_interp_def by auto

lemma true_cls_cls_insert_l[simp]:
  "a ⊨f C ⟹ insert a A ⊨p C"
  unfolding true_cls_cls_def true_clss_cls_def true_clss_def by fastforce

lemma true_cls_clss_empty[iff]:
  "N ⊨fs {}"
  unfolding true_cls_clss_def by auto

lemma true_prop_true_clause[iff]:
  "{φ} ⊨p ψ ⟷ φ ⊨f ψ"
  unfolding true_cls_cls_def true_clss_cls_def by auto

lemma true_clss_clss_true_clss_cls[iff]:
  "N ⊨ps {ψ} ⟷ N ⊨p ψ"
  unfolding true_clss_clss_def true_clss_cls_def by auto

lemma true_clss_clss_true_cls_clss[iff]:
  "{χ} ⊨ps ψ ⟷ χ ⊨fs ψ"
  unfolding true_clss_clss_def true_cls_clss_def by auto

lemma true_clss_clss_empty[simp]:
  "N ⊨ps {}"
  unfolding true_clss_clss_def by auto

lemma true_clss_cls_subset:
  "A ⊆ B ⟹ A ⊨p CC ⟹ B ⊨p CC"
  unfolding true_clss_cls_def total_over_m_union by (simp add: total_over_m_subset true_clss_mono)

text ‹This version of @{thm true_clss_cls_subset} is useful as intro rule.›
lemma (in -)true_clss_cls_subsetI: ‹I ⊨p A ⟹ I ⊆ I' ⟹ I' ⊨p A›
  by (simp add: true_clss_cls_subset)

lemma true_clss_cs_mono_l[simp]:
  "A ⊨p CC ⟹ A ∪ B ⊨p CC"
  by (auto intro: true_clss_cls_subset)

lemma true_clss_cs_mono_l2[simp]:
  "B ⊨p CC ⟹ A ∪ B ⊨p CC"
  by (auto intro: true_clss_cls_subset)

lemma true_clss_cls_mono_r[simp]:
  "A ⊨p CC ⟹ A ⊨p CC + CC'"
  unfolding true_clss_cls_def total_over_m_union total_over_m_sum by blast

lemma true_clss_cls_mono_r'[simp]:
  "A ⊨p CC' ⟹ A ⊨p CC + CC'"
  unfolding true_clss_cls_def total_over_m_union total_over_m_sum by blast

lemma true_clss_cls_mono_add_mset[simp]:
  "A ⊨p CC ⟹ A ⊨p add_mset L CC"
   using true_clss_cls_mono_r[of A CC "add_mset L {#}"] by simp

lemma true_clss_clss_union_l[simp]:
  "A ⊨ps CC ⟹ A ∪ B ⊨ps CC"
  unfolding true_clss_clss_def total_over_m_union by fastforce

lemma true_clss_clss_union_l_r[simp]:
  "B ⊨ps CC ⟹ A ∪ B ⊨ps CC"
  unfolding true_clss_clss_def total_over_m_union by fastforce

lemma true_clss_cls_in[simp]:
  "CC ∈ A ⟹ A ⊨p CC"
  unfolding true_clss_cls_def true_clss_def total_over_m_union by fastforce

lemma true_clss_cls_insert_l[simp]:
  "A ⊨p C ⟹ insert a A ⊨p C"
  unfolding true_clss_cls_def true_clss_def using total_over_m_union
  by (metis Un_iff insert_is_Un sup.commute)

lemma true_clss_clss_insert_l[simp]:
  "A ⊨ps C ⟹ insert a A ⊨ps C"
  unfolding true_clss_cls_def true_clss_clss_def true_clss_def by blast

lemma true_clss_clss_union_and[iff]:
  "A ⊨ps C ∪ D ⟷ (A ⊨ps C ∧ A ⊨ps D)"
proof
  {
    fix A C D :: "'a clause_set"
    assume A: "A ⊨ps C ∪ D"
    have "A ⊨ps C"
        unfolding true_clss_clss_def true_clss_cls_def insert_def total_over_m_insert
      proof (intro allI impI)
        fix I
        assume
          totAC: "total_over_m I (A ∪ C)" and
          cons: "consistent_interp I" and
          I: "I ⊨s A"
        then have tot: "total_over_m I A" and tot': "total_over_m I C" by auto
        obtain I' where
          tot': "total_over_m (I ∪ I') (A ∪ C ∪ D)" and
          cons': "consistent_interp (I ∪ I')" and
          H: "∀x∈I'. atm_of x ∈ atms_of_ms D ∧ atm_of x ∉ atms_of_ms (A ∪ C)"
          using total_over_m_consistent_extension[OF _ cons, of "A ∪ C"] tot tot' by blast
        moreover have "I ∪ I' ⊨s A" using I by simp
        ultimately have "I ∪ I' ⊨s C ∪ D" using A unfolding true_clss_clss_def by auto
        then have "I ∪ I' ⊨s C ∪ D" by auto
        then show "I ⊨s C" using notin_vars_union_true_clss_true_clss[of I'] H by auto
      qed
   } note H = this
  assume "A ⊨ps C ∪ D"
  then show "A ⊨ps C ∧ A ⊨ps D" using H[of A] Un_commute[of C D] by metis
next
  assume "A ⊨ps C ∧ A ⊨ps D"
  then show "A ⊨ps C ∪ D"
    unfolding true_clss_clss_def by auto
qed

lemma true_clss_clss_insert[iff]:
  "A ⊨ps insert L Ls ⟷ (A ⊨p L ∧ A ⊨ps Ls)"
  using true_clss_clss_union_and[of A "{L}" "Ls"] by auto

lemma true_clss_clss_subset:
  "A ⊆ B ⟹ A ⊨ps CC ⟹ B ⊨ps CC"
  by (metis subset_Un_eq true_clss_clss_union_l)

text ‹Better suited as intro rule:›
lemma true_clss_clss_subsetI:
  "A ⊨ps CC ⟹ A ⊆ B ⟹ B ⊨ps CC"
  by (metis subset_Un_eq true_clss_clss_union_l)

lemma union_trus_clss_clss[simp]: "A ∪ B ⊨ps B"
  unfolding true_clss_clss_def by auto

lemma true_clss_clss_remove[simp]:
  "A ⊨ps B ⟹ A ⊨ps B - C"
  by (metis Un_Diff_Int true_clss_clss_union_and)

lemma true_clss_clss_subsetE:
  "N ⊨ps B ⟹ A ⊆ B ⟹ N ⊨ps A"
  by (metis sup.orderE true_clss_clss_union_and)

lemma true_clss_clss_in_imp_true_clss_cls:
  assumes "N ⊨ps U"
  and "A ∈ U"
  shows "N ⊨p A"
  using assms mk_disjoint_insert by fastforce

lemma all_in_true_clss_clss: "∀x ∈ B. x ∈ A ⟹ A ⊨ps B"
  unfolding true_clss_clss_def true_clss_def by auto

lemma true_clss_clss_left_right:
  assumes "A ⊨ps B"
  and "A ∪ B ⊨ps M"
  shows "A ⊨ps M ∪ B"
  using assms unfolding true_clss_clss_def by auto

lemma true_clss_clss_generalise_true_clss_clss:
  "A ∪ C ⊨ps D ⟹ B ⊨ps C ⟹ A ∪ B ⊨ps D"
proof -
  assume a1: "A ∪ C ⊨ps D"
  assume "B ⊨ps C"
  then have f2: "⋀M. M ∪ B ⊨ps C"
    by (meson true_clss_clss_union_l_r)
  have "⋀M. C ∪ (M ∪ A) ⊨ps D"
    using a1 by (simp add: Un_commute sup_left_commute)
  then show ?thesis
    using f2 by (metis (no_types) Un_commute true_clss_clss_left_right true_clss_clss_union_and)
qed

lemma true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or:
  assumes D: "N ⊨p add_mset (-L) D"
  and C: "N ⊨p add_mset L C"
  shows "N ⊨p D + C"
  unfolding true_clss_cls_def
proof (intro allI impI)
  fix I
  assume
    tot: "total_over_m I (N ∪ {D + C})" and
    "consistent_interp I" and
    "I ⊨s N"
  {
    assume L: "L ∈ I ∨ -L ∈ I"
    then have "total_over_m I {D + {#- L#}}"
      using tot by (cases L) auto
    then have "I ⊨ D + {#- L#}" using D ‹I ⊨s N› tot ‹consistent_interp I›
      unfolding true_clss_cls_def by auto
    moreover
      have "total_over_m I {C + {#L#}}"
        using L tot by (cases L) auto
      then have "I ⊨ C + {#L#}"
        using C ‹I ⊨s N› tot ‹consistent_interp I› unfolding true_clss_cls_def by auto
    ultimately have "I ⊨ D + C" using ‹consistent_interp I› consistent_interp_def by fastforce
  }
  moreover {
    assume L: "L ∉ I ∧ -L ∉ I"
    let ?I' = "I ∪ {L}"
    have "consistent_interp ?I'" using L ‹consistent_interp I› by auto
    moreover have "total_over_m ?I' {add_mset (-L) D}"
      using tot unfolding total_over_m_def total_over_set_def by (auto simp add: atms_of_def)
    moreover have "total_over_m ?I' N" using tot using total_union by blast
    moreover have "?I' ⊨s N" using ‹I ⊨s N› using true_clss_union_increase by blast
    ultimately have "?I' ⊨ add_mset (-L) D"
      using D unfolding true_clss_cls_def by blast
    then have "?I' ⊨ D" using L by auto
    moreover
      have "total_over_set I (atms_of (D + C))" using tot by auto
      then have "L ∉# D ∧ -L ∉# D"
        using L unfolding total_over_set_def atms_of_def by (cases L) force+
    ultimately have "I ⊨ D + C" unfolding true_cls_def by auto
  }
  ultimately show "I ⊨ D + C" by blast
qed

lemma true_cls_union_mset[iff]: "I ⊨ C ∪# D ⟷ I ⊨ C ∨ I ⊨ D"
  unfolding true_cls_def by force

lemma true_clss_cls_sup_iff_add: "N ⊨p C ∪# D ⟷ N ⊨p C + D"
  by (auto simp: true_clss_cls_def)

lemma true_clss_cls_union_mset_true_clss_cls_or_not_true_clss_cls_or:
  assumes
    D: "N ⊨p add_mset (-L) D" and
    C: "N ⊨p add_mset L C"
  shows "N ⊨p D ∪# C"
  using true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[OF assms]
  by (subst true_clss_cls_sup_iff_add)


lemma true_clss_cls_tautology_iff:
  ‹{} ⊨p a ⟷ tautology a› (is ‹?A ⟷ ?B›)
proof
  assume ?A
  then have H: ‹total_over_set I (atms_of a) ⟹ consistent_interp I ⟹ I ⊨ a› for I
    by (auto simp: true_clss_cls_def tautology_decomp add_mset_eq_add_mset
      dest!: multi_member_split)
  show ?B
    unfolding tautology_def
  proof (intro allI impI)
    fix I
    assume tot: ‹total_over_set I (atms_of a)›
    let ?Iinter = ‹I ∩ uminus ` I›
    let ?I = ‹I - ?Iinter ∪ Pos ` atm_of ` ?Iinter›
    have ‹total_over_set ?I (atms_of a)›
      using tot by (force simp: total_over_set_def image_image Clausal_Logic.uminus_lit_swap
        simp: image_iff)
    moreover have ‹consistent_interp ?I›
      unfolding consistent_interp_def image_iff
      apply clarify
      subgoal for L
        apply (cases L)
        apply (auto simp: consistent_interp_def uminus_lit_swap image_iff)
	apply (case_tac xa; auto; fail)+
	done
      done
    ultimately have ‹?I ⊨ a›
      using H[of ?I] by fast
    moreover have ‹?I ⊆ I›
      apply (rule)
      subgoal for x by (cases x; auto; rename_tac xb; case_tac xb; auto)
      done
    ultimately show ‹I ⊨ a›
      by (blast intro: true_cls_mono_set_mset_l)
  qed
next
  assume ?B
  then show ‹?A›
    by (auto simp: true_clss_cls_def tautology_decomp add_mset_eq_add_mset
      dest!: multi_member_split)
qed

lemma true_cls_mset_empty_iff[simp]: ‹{} ⊨m C ⟷ C = {#}›
  by (cases C)  auto

lemma true_clss_mono_left:
  ‹I ⊨s A ⟹ I ⊆ J ⟹ J ⊨s A›
  by (metis sup.orderE true_clss_union_increase')

lemma true_cls_remove_alien:
  ‹I ⊨ N ⟷ {L. L ∈ I ∧ atm_of L ∈ atms_of N} ⊨ N›
  by (auto simp: true_cls_def dest: multi_member_split)

lemma true_clss_remove_alien:
  ‹I ⊨s N ⟷ {L. L ∈ I ∧ atm_of L ∈ atms_of_ms N} ⊨s N›
  by (auto simp: true_clss_def true_cls_def in_implies_atm_of_on_atms_of_ms
    dest: multi_member_split)

lemma true_clss_alt_def:
  ‹N ⊨p χ ⟷
    (∀I. atms_of_s I = atms_of_ms (N ∪ {χ}) ⟶ consistent_interp I ⟶ I ⊨s N ⟶ I ⊨ χ)›
  apply (rule iffI)
  subgoal
    unfolding total_over_set_alt_def true_clss_cls_def total_over_m_alt_def
    by auto
  subgoal
    unfolding total_over_set_alt_def true_clss_cls_def total_over_m_alt_def
    apply (intro conjI impI allI)
    subgoal for I
      using consistent_interp_subset[of ‹{L ∈ I. atm_of L ∈ atms_of_ms (N ∪ {χ})}› I]
      true_clss_mono_left[of  ‹{L ∈ I. atm_of L ∈ atms_of_ms N}› N
         ‹{L ∈ I. atm_of L ∈ atms_of_ms (N ∪ {χ})}›]
      true_clss_remove_alien[of I N]
    by (drule_tac x = ‹{L ∈ I. atm_of L ∈ atms_of_ms (N ∪ {χ})}› in spec)
      (auto dest: true_cls_mono_set_mset_l)
    done
  done

lemma true_clss_alt_def2:
  assumes ‹¬tautology χ›
  shows ‹N ⊨p χ ⟷ (∀I. atms_of_s I = atms_of_ms N ⟶ consistent_interp I ⟶ I ⊨s N ⟶ I ⊨ χ)› (is ‹?A ⟷ ?B›)
proof (rule iffI)
  assume ?A
  then have H:
      ‹⋀I. atms_of_ms (N ∪ {χ}) ⊆ atms_of_s I ⟶
	   consistent_interp I ⟶ I ⊨s N ⟶ I ⊨ χ›
    unfolding total_over_set_alt_def total_over_m_alt_def true_clss_cls_def by blast
  show ?B
    unfolding total_over_set_alt_def total_over_m_alt_def true_clss_cls_def
  proof (intro conjI impI allI)
    fix I :: ‹'a literal set›
    assume
      atms: ‹atms_of_s I = atms_of_ms N› and
      cons: ‹consistent_interp I› and
      ‹I ⊨s N›
    let ?I1 = ‹I ∪ uminus ` {L ∈ set_mset χ. atm_of L ∉ atms_of_s I}›
    have ‹atms_of_ms (N ∪ {χ}) ⊆ atms_of_s ?I1›
      by (auto simp add: atms in_image_uminus_uminus atm_iff_pos_or_neg_lit)
    moreover have ‹consistent_interp ?I1›
      using cons assms by (auto simp: consistent_interp_def)
        (rename_tac x; case_tac x; auto; fail)+
    moreover have ‹?I1 ⊨s N›
      using ‹I ⊨s N› by auto
    ultimately have ‹?I1 ⊨ χ›
      using H[of ?I1] by auto
    then show ‹I ⊨ χ›
      using assms by (auto simp: true_cls_def)
  qed
next
  assume ?B
  show ?A
    unfolding total_over_m_alt_def true_clss_alt_def
  proof (intro conjI impI allI)
    fix I :: ‹'a literal set›
    assume
      atms: ‹atms_of_s I = atms_of_ms (N ∪ {χ})› and
      cons: ‹consistent_interp I› and
      ‹I ⊨s N›
    let ?I1 = ‹{L ∈ I. atm_of L ∈ atms_of_ms N}›
    have ‹atms_of_s ?I1 = atms_of_ms N›
      using atms by (auto simp add: in_image_uminus_uminus atm_iff_pos_or_neg_lit)
    moreover have ‹consistent_interp ?I1›
      using cons assms by (auto simp: consistent_interp_def)
    moreover have ‹?I1 ⊨s N›
      using ‹I ⊨s N› by (subst (asm)true_clss_remove_alien)
    ultimately have ‹?I1 ⊨ χ›
      using ‹?B› by auto
    then show ‹I ⊨ χ›
      using assms by (auto simp: true_cls_def)
  qed
qed

lemma true_clss_restrict_iff:
  assumes ‹¬tautology χ›
  shows ‹N ⊨p χ ⟷ N ⊨p {#L ∈# χ. atm_of L ∈ atms_of_ms N#}› (is ‹?A ⟷ ?B›)
  apply (subst true_clss_alt_def2[OF assms])
  apply (subst true_clss_alt_def2)
  subgoal using not_tautology_mono[OF _ assms] by (auto dest: not_tautology_minus)
  apply (rule HOL.iff_allI)
  apply (auto 5 5 simp: true_cls_def atms_of_s_def dest!: multi_member_split)
  done


text ‹This is a slightly restrictive theorem, that encompasses most useful cases.
  The assumption \<^term>‹¬tautology C› can be removed if the model \<^term>‹I› is total
  over the clause.
›
lemma true_clss_cls_true_clss_true_cls:
  assumes ‹N ⊨p C›
    ‹I ⊨s N› and
    cons: ‹consistent_interp I› and
    tauto: ‹¬tautology C›
  shows ‹I ⊨ C›
proof -
  let ?I = ‹I ∪ uminus ` {L ∈ set_mset C. atm_of L ∉ atms_of_s I}›
  let ?I2 = ‹?I ∪ Pos ` {L ∈ atms_of_ms N. L ∉ atms_of_s ?I}›
  have ‹total_over_m ?I2 (N ∪ {C})›
    by (auto simp: total_over_m_alt_def atms_of_def in_image_uminus_uminus
      dest!: multi_member_split)
  moreover have ‹consistent_interp ?I2›
    using cons tauto unfolding consistent_interp_def
    apply (intro allI)
    apply (case_tac L)
    by (auto simp: uminus_lit_swap eq_commute[of ‹Pos _› ‹- _›]
      eq_commute[of ‹Neg _› ‹- _›])
  moreover have ‹?I2 ⊨s N›
    using ‹I ⊨s N› by auto
  ultimately have ‹?I2 ⊨ C›
    using assms(1) unfolding true_clss_cls_def by fast
  then show ?thesis
    using tauto
    by (subst (asm) true_cls_remove_alien)
      (auto simp: true_cls_def in_image_uminus_uminus)
qed


subsection ‹Subsumptions›

lemma subsumption_total_over_m:
  assumes "A ⊆# B"
  shows "total_over_m I {B} ⟹ total_over_m I {A}"
  using assms unfolding subset_mset_def total_over_m_def total_over_set_def
  by (auto simp add: mset_subset_eq_exists_conv)

lemma atms_of_replicate_mset_replicate_mset_uminus[simp]:
  "atms_of (D - replicate_mset (count D L) L - replicate_mset (count D (-L)) (-L))
 = atms_of D - {atm_of L}"
  by (auto simp: atm_of_eq_atm_of atms_of_def in_diff_count dest: in_diffD)

lemma subsumption_chained:
  assumes
    "∀I. total_over_m I {D} ⟶ I ⊨ D ⟶ I ⊨ φ" and
    "C ⊆# D"
  shows "(∀I. total_over_m I {C} ⟶ I ⊨ C ⟶ I ⊨ φ) ∨ tautology φ"
  using assms
proof (induct "card {Pos v | v. v ∈ atms_of D ∧ v ∉ atms_of C}" arbitrary: D
    rule: nat_less_induct_case)
  case 0 note n = this(1) and H = this(2) and incl = this(3)
  then have "atms_of D ⊆ atms_of C" by auto
  then have "∀I. total_over_m I {C} ⟶ total_over_m I {D}"
    unfolding total_over_m_def total_over_set_def by auto
  moreover have "∀I. I ⊨ C ⟶ I ⊨ D" using incl true_cls_mono_leD by blast
  ultimately show ?case using H by auto
next
  case (Suc n D) note IH = this(1) and card = this(2) and H = this(3) and incl = this(4)
  let ?atms = "{Pos v |v. v ∈ atms_of D ∧ v ∉ atms_of C}"
  have "finite ?atms" by auto
  then obtain L where L: "L ∈ ?atms"
    using card by (metis (no_types, lifting) Collect_empty_eq card_0_eq mem_Collect_eq
      nat.simps(3))
  let ?D' = "D - replicate_mset (count D L) L - replicate_mset (count D (-L)) (-L)"
  have atms_of_D: "atms_of_ms {D} ⊆ atms_of_ms {?D'} ∪ {atm_of L}"
    using atms_of_replicate_mset_replicate_mset_uminus by force

  {
    fix I
    assume "total_over_m I {?D'}"
    then have tot: "total_over_m (I ∪ {L}) {D}"
      unfolding total_over_m_def total_over_set_def using atms_of_D by auto

    assume IDL: "I ⊨ ?D'"
    then have "insert L I ⊨ D" unfolding true_cls_def by (fastforce dest: in_diffD)
    then have "insert L I ⊨ φ" using H tot by auto

    moreover
      have tot': "total_over_m (I ∪ {-L}) {D}"
        using tot unfolding total_over_m_def total_over_set_def by auto
      have "I ∪ {-L} ⊨ D" using IDL unfolding true_cls_def by (force dest: in_diffD)
      then have "I ∪ {-L} ⊨ φ" using H tot' by auto
    ultimately have "I ⊨ φ ∨ tautology φ"
      using L remove_literal_in_model_tautology by force
  } note H' = this

  have "L ∉# C " and "-L ∉# C" using L atm_iff_pos_or_neg_lit by force+
  then have C_in_D': "C ⊆# ?D'" using ‹C ⊆# D› by (auto simp: subseteq_mset_def not_in_iff)
  have "card {Pos v |v. v ∈ atms_of ?D' ∧ v ∉ atms_of C} <
    card {Pos v |v. v ∈ atms_of D ∧ v ∉ atms_of C}"
    using L unfolding atms_of_replicate_mset_replicate_mset_uminus[of D L]
    by (auto intro!: psubset_card_mono)
  then show ?case
    using IH C_in_D' H' unfolding card[symmetric] by blast
qed


subsection ‹Removing Duplicates›

lemma tautology_remdups_mset[iff]:
  "tautology (remdups_mset C) ⟷ tautology C"
  unfolding tautology_decomp by auto

lemma atms_of_remdups_mset[simp]: "atms_of (remdups_mset C) = atms_of C"
  unfolding atms_of_def by auto

lemma true_cls_remdups_mset[iff]: "I ⊨ remdups_mset C ⟷ I ⊨ C"
  unfolding true_cls_def by auto

lemma true_clss_cls_remdups_mset[iff]: "A ⊨p remdups_mset C ⟷ A ⊨p C"
  unfolding true_clss_cls_def total_over_m_def by auto


subsection ‹Set of all Simple Clauses›

text ‹A simple clause with respect to a set of atoms is such that
  ▸ its atoms are included in the considered set of atoms;
  ▸ it is not a tautology;
  ▸ it does not contains duplicate literals.

  It corresponds to the clauses that cannot be simplified away in a calculus without considering
  the other clauses.›
definition simple_clss :: "'v set ⇒ 'v clause set" where
"simple_clss atms = {C. atms_of C ⊆ atms ∧ ¬tautology C ∧ distinct_mset C}"

lemma simple_clss_empty[simp]:
  "simple_clss {} = {{#}}"
  unfolding simple_clss_def by auto

lemma simple_clss_insert:
  assumes "l ∉ atms"
  shows "simple_clss (insert l atms) =
    ((+) {#Pos l#}) ` (simple_clss atms)
    ∪ ((+) {#Neg l#}) ` (simple_clss atms)
    ∪ simple_clss atms"(is "?I = ?U")
proof (standard; standard)
  fix C
  assume "C ∈ ?I"
  then have
    atms: "atms_of C ⊆ insert l atms" and
    taut: "¬tautology C" and
    dist: "distinct_mset C"
    unfolding simple_clss_def by auto
  have H: "⋀x. x ∈# C ⟹ atm_of x ∈ insert l atms"
    using atm_of_lit_in_atms_of atms by blast
  consider
      (Add) L where "L ∈# C" and "L = Neg l ∨ L = Pos l"
    | (No) "Pos l ∉# C" "Neg l ∉# C"
    by auto
  then show "C ∈ ?U"
    proof cases
      case Add
      then have LCL: "L ∉# C - {#L#}"
        using dist unfolding distinct_mset_def by (auto simp: not_in_iff)
      have LC: "-L ∉# C"
        using taut Add by auto
      obtain aa :: 'a where
        f4: "(aa ∈ atms_of (remove1_mset L C) ⟶ aa ∈ atms) ⟶ atms_of (remove1_mset L C) ⊆ atms"
        by (meson subset_iff)
      obtain ll :: "'a literal" where
        "aa ∉ atm_of ` set_mset (remove1_mset L C) ∨ aa = atm_of ll ∧ ll ∈# remove1_mset L C"
        by blast
      then have "atms_of (C - {#L#}) ⊆ atms"
        using f4 Add LCL LC H unfolding atms_of_def by (metis H in_diffD insertE
          literal.exhaust_sel uminus_Neg uminus_Pos)
      moreover have "¬ tautology (C - {#L#})"
        using taut by (metis Add(1) insert_DiffM tautology_add_mset)
      moreover have "distinct_mset (C - {#L#})"
        using dist by auto
      ultimately have "(C - {#L#}) ∈ simple_clss atms"
        using Add unfolding simple_clss_def by auto
      moreover have "C = {#L#} + (C - {#L#})"
        using Add by (auto simp: multiset_eq_iff)
      ultimately show ?thesis using Add by blast
    next
      case No
      then have "C ∈ simple_clss atms"
        using taut atms dist unfolding simple_clss_def
        by (auto simp: atm_iff_pos_or_neg_lit split: if_split_asm dest!: H)
      then show ?thesis by blast
    qed
next
  fix C
  assume "C ∈ ?U"
  then consider
      (Add) L C' where "C = {#L#} + C'" and "C' ∈ simple_clss atms" and
        "L = Pos l ∨ L = Neg l"
    | (No) "C ∈ simple_clss atms"
    by auto
  then show "C ∈ ?I"
    proof cases
      case No
      then show ?thesis unfolding simple_clss_def by auto
    next
      case (Add L C') note C' = this(1) and C = this(2) and L = this(3)
      then have
        atms: "atms_of C' ⊆ atms" and
        taut: "¬tautology C'" and
        dist: "distinct_mset C'"
        unfolding simple_clss_def by auto
      have "atms_of C ⊆ insert l atms"
        using atms C' L by auto
      moreover have "¬ tautology C"
        using taut C' L assms atms by (metis union_mset_add_mset_left add.left_neutral
            neg_lit_in_atms_of pos_lit_in_atms_of subsetCE tautology_add_mset
            uminus_Neg uminus_Pos)
      moreover have "distinct_mset C"
        using dist C' L by (metis union_mset_add_mset_left add.left_neutral assms atms
            distinct_mset_add_mset neg_lit_in_atms_of pos_lit_in_atms_of subsetCE)
      ultimately show ?thesis unfolding simple_clss_def by blast
    qed
qed

lemma simple_clss_finite:
  fixes atms :: "'v set"
  assumes "finite atms"
  shows "finite (simple_clss atms)"
  using assms by (induction rule: finite_induct) (auto simp: simple_clss_insert)

lemma simple_clssE:
  assumes
    "x ∈ simple_clss atms"
  shows "atms_of x ⊆ atms ∧ ¬tautology x ∧ distinct_mset x"
  using assms unfolding simple_clss_def by auto

lemma cls_in_simple_clss:
  shows "{#} ∈ simple_clss s"
  unfolding simple_clss_def by auto

lemma simple_clss_card:
  fixes atms :: "'v set"
  assumes "finite atms"
  shows "card (simple_clss atms) ≤ (3::nat) ^ (card atms)"
  using assms
proof (induct atms rule: finite_induct)
  case empty
  then show ?case by auto
next
  case (insert l C) note fin = this(1) and l = this(2) and IH = this(3)
  have notin:
    "⋀C'. add_mset (Pos l) C' ∉ simple_clss C"
    "⋀C'. add_mset (Neg l) C' ∉ simple_clss C"
    using l unfolding simple_clss_def by auto
  have H: "⋀C' D. {#Pos l#} + C' = {#Neg l#} + D ⟹ D ∈ simple_clss C ⟹ False"
    proof -
      fix C' D
      assume C'D: "{#Pos l#} + C' = {#Neg l#} + D" and D: "D ∈ simple_clss C"
      then have "Pos l ∈# D"
        by (auto simp: add_mset_eq_add_mset_ne)
      then have "l ∈ atms_of D"
        by (simp add: atm_iff_pos_or_neg_lit)
      then show False using D l unfolding simple_clss_def by auto
    qed
  let ?P = "((+) {#Pos l#}) ` (simple_clss C)"
  let ?N = "((+) {#Neg l#}) ` (simple_clss C)"
  let ?O = "simple_clss C"
  have "card (?P ∪ ?N ∪ ?O) = card (?P ∪ ?N) + card ?O"
    apply (subst card_Un_disjoint)
    using l fin by (auto simp: simple_clss_finite notin)
  moreover have "card (?P ∪ ?N) = card ?P + card ?N"
    apply (subst card_Un_disjoint)
    using l fin H by (auto simp: simple_clss_finite notin)
  moreover
    have "card ?P = card ?O"
      using inj_on_iff_eq_card[of ?O "(+) {#Pos l#}"]
      by (auto simp: fin simple_clss_finite inj_on_def)
  moreover have "card ?N = card ?O"
      using inj_on_iff_eq_card[of ?O "(+) {#Neg l#}"]
      by (auto simp: fin simple_clss_finite inj_on_def)
  moreover have "(3::nat) ^ card (insert l C) = 3 ^ (card C) + 3 ^ (card C) + 3 ^ (card C)"
    using l by (simp add: fin mult_2_right numeral_3_eq_3)
  ultimately show ?case using IH l by (auto simp: simple_clss_insert)
qed

lemma simple_clss_mono:
  assumes incl: "atms ⊆ atms'"
  shows "simple_clss atms ⊆ simple_clss atms'"
  using assms unfolding simple_clss_def by auto

lemma distinct_mset_not_tautology_implies_in_simple_clss:
  assumes "distinct_mset χ" and "¬tautology χ"
  shows "χ ∈ simple_clss (atms_of χ)"
  using assms unfolding simple_clss_def by auto

lemma simplified_in_simple_clss:
  assumes "distinct_mset_set ψ" and "∀χ ∈ ψ. ¬tautology χ"
  shows "ψ ⊆ simple_clss (atms_of_ms ψ)"
  using assms unfolding simple_clss_def
  by (auto simp: distinct_mset_set_def atms_of_ms_def)

lemma simple_clss_element_mono:
  ‹x ∈ simple_clss A ⟹ y ⊆# x ⟹ y ∈ simple_clss A›
  by (auto simp: simple_clss_def atms_of_def intro: distinct_mset_mono
    dest: not_tautology_mono)


subsection ‹Experiment: Expressing the Entailments as Locales›
(* Maybe should become locales at some point of time ?
Shared prop of ⊨:
* I + I' ⊨ A ⟷ I' + I ⊨ A

Shared by the formula version of ⊨:
* N ⊆ N' ⟹ N' ⊨ ψ ⟹ N ⊨ ψ
* A ⊆ B ⟹ N ⊨ B ⟹ N ⊨ A

Shared by the other ⊨ symbols:
* I ⊨ A ⟹ I + I' ⊨ A
* I ⊨ A ⋆ B ⟹ I ⊨ B ⋆ A
* I ⊨ A ⟹ I ⊨ B ⟹ I ⊨ A ⋆ B

Shared by the first layer 'a ⇒ 'b set ⇒ bool:
* A ⊆ B ⟹ I ⊨ A ⟹ I ⊨ B
* I ⊨ A ⋆ B ⟷ I ⊨s A ∨ I ⊨s B

Shared by the second layer of type 'a ⇒ 'b set ⇒ bool:
* definition: I ⊨s A ⟷ ∀a ∈ A. I ⊨ a
* I ⊨s {A} ⟷ I ⊨ A
* I ⊨s A ⋆ B ⟷ I ⊨s A ∧ I ⊨s B
* A ⊆ B ⟹ I ⊨s B ⟹ I ⊨s A
* I ⊨s {}

*   true_lit  ⊨   'a partial_interp ⇒ 'a literal ⇒ bool
*   true_cls  ⊨l 'a partial_interp ⇒ 'a clause ⇒ bool
⟶ true_clss ⊨s 'a partial_interp ⇒ 'a clause_set ⇒ bool

*   true_annot ⊨a ann_lits ⇒ 'a clause ⇒ bool
⟶ true_annots ⊨as ann_lits ⇒ 'a clause_set ⇒ bool

Formula version :
*   true_cls_cls ⊨f 'a clause ⇒ 'a clause ⇒ bool
⟶ true_cls_clss ⊨fs 'a clause ⇒ 'a clause_set ⇒ bool

*   true_clss_cls ⊨p 'a clause_set ⇒ 'a clause ⇒ bool
⟶ true_clss_clss ⊨ps 'a clause_set ⇒ 'a clause_set ⇒ bool
*)
locale entail =
  fixes entail :: "'a set ⇒ 'b ⇒ bool" (infix "⊨e" 50)
  assumes entail_insert[simp]: "I ≠ {} ⟹ insert L I ⊨e x ⟷ {L} ⊨e x ∨ I ⊨e x"
  assumes entail_union[simp]: "I ⊨e A ⟹ I ∪ I' ⊨e A"
begin

definition entails :: "'a set ⇒ 'b set ⇒ bool" (infix "⊨es" 50) where
  "I ⊨es A ⟷ (∀a ∈ A. I ⊨e a)"

lemma entails_empty[simp]:
  "I ⊨es {}"
  unfolding entails_def by auto

lemma entails_single[iff]:
  "I ⊨es {a} ⟷ I ⊨e a"
  unfolding entails_def by auto

lemma entails_insert_l[simp]:
  "M ⊨es A ⟹ insert L M ⊨es A"
  unfolding entails_def by (metis Un_commute entail_union insert_is_Un)

lemma entails_union[iff]: "I ⊨es CC ∪ DD ⟷ I ⊨es CC ∧ I ⊨es DD"
  unfolding entails_def by blast

lemma entails_insert[iff]: "I ⊨es insert C DD ⟷ I ⊨e C ∧ I ⊨es DD"
  unfolding entails_def by blast

lemma entails_insert_mono: "DD ⊆ CC ⟹ I ⊨es CC ⟹ I ⊨es DD"
  unfolding entails_def by blast

lemma entails_union_increase[simp]:
 assumes "I ⊨es ψ"
 shows "I ∪ I' ⊨es ψ"
 using assms unfolding entails_def by auto

lemma true_clss_commute_l:
  "I ∪ I' ⊨es ψ ⟷ I' ∪ I ⊨es ψ"
  by (simp add: Un_commute)

lemma entails_remove[simp]: "I ⊨es N ⟹ I ⊨es Set.remove a N"
  by (simp add: entails_def)

lemma entails_remove_minus[simp]: "I ⊨es N ⟹ I ⊨es N - A"
  by (simp add: entails_def)

end

interpretation true_cls: entail true_cls
  by standard (auto simp add: true_cls_def)


subsection ‹Entailment to be extended›

text ‹In some cases we want a more general version of entailment to have for example
  @{term "{} ⊨ {#L, -L#}"}. This is useful when the model we are building might not be total (the
  literal @{term L} might have been definitely removed from the set of clauses), but we still want
  to have a property of entailment considering that theses removed literals are not important.

  We can given a model @{term I} consider all the natural extensions: @{term C} is entailed
  by an extended @{term I}, if for all total extension of @{term I}, this model entails @{term C}.
  ›
definition true_clss_ext :: "'a literal set ⇒ 'a clause set ⇒ bool" (infix "⊨sext" 49)
where
"I ⊨sext N ⟷ (∀J. I ⊆ J ⟶ consistent_interp J ⟶ total_over_m J N ⟶ J ⊨s N)"

lemma true_clss_imp_true_cls_ext:
  "I⊨s N ⟹ I ⊨sext N"
  unfolding true_clss_ext_def by (metis sup.orderE true_clss_union_increase')

lemma true_clss_ext_decrease_right_remove_r:
  assumes "I ⊨sext N"
  shows "I ⊨sext N - {C}"
  unfolding true_clss_ext_def
proof (intro allI impI)
  fix J
  assume
    "I ⊆ J" and
    cons: "consistent_interp J" and
    tot: "total_over_m J (N - {C})"
  let ?J = "J ∪ {Pos (atm_of P)|P. P ∈# C ∧ atm_of P ∉ atm_of ` J}"
  have "I ⊆ ?J" using ‹I ⊆ J› by auto
  moreover have "consistent_interp ?J"
    using cons unfolding consistent_interp_def apply (intro allI)
    by (rename_tac L, case_tac L) (fastforce simp add: image_iff)+
  moreover have "total_over_m ?J N"
    using tot unfolding total_over_m_def total_over_set_def atms_of_ms_def
    apply clarify
    apply (rename_tac l a, case_tac "a ∈ N - {C}")
      apply (auto; fail)
    using atms_of_s_def atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
    by (fastforce simp: atms_of_def)
  ultimately have "?J ⊨s N"
    using assms unfolding true_clss_ext_def by blast
  then have "?J ⊨s N - {C}" by auto
  have "{v ∈ ?J. atm_of v ∈ atms_of_ms (N - {C})} ⊆ J"
    using tot unfolding total_over_m_def total_over_set_def
    by (auto intro!: rev_image_eqI)
  then show "J ⊨s N - {C}"
    using true_clss_remove_unused[OF ‹?J ⊨s N - {C}›] unfolding true_clss_def
    by (meson true_cls_mono_set_mset_l)
qed

lemma consistent_true_clss_ext_satisfiable:
  assumes "consistent_interp I" and "I ⊨sext A"
  shows "satisfiable A"
  by (metis Un_empty_left assms satisfiable_carac subset_Un_eq sup.left_idem
    total_over_m_consistent_extension total_over_m_empty true_clss_ext_def)

lemma not_consistent_true_clss_ext:
  assumes "¬consistent_interp I"
  shows "I ⊨sext A"
  by (meson assms consistent_interp_subset true_clss_ext_def)


(*Move in the theories*)
lemma inj_on_Pos: ‹inj_on Pos A› and
  inj_on_Neg: ‹inj_on Neg A›
  by (auto simp: inj_on_def)

lemma inj_on_uminus_lit: ‹inj_on uminus A› for A :: ‹'a literal set›
  by (auto simp: inj_on_def)

end