Theory Partial_Clausal_Logic

(*  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 Clausal Logic›

theory Partial_Clausal_Logic
imports "../lib/Clausal_Logic" List_More
begin

text ‹We define here entailment by a set of literals. This is ∗‹not› an Herbrand interpretation and
  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.
  ›

subsection ‹Clauses›

text ‹
Clauses are (finite) multisets of literals.
›

type_synonym 'a clause = "'a literal multiset"
type_synonym 'v clauses = "'v clause set"

subsection ‹Partial Interpretations›

type_synonym 'a interp = "'a literal set"

definition true_lit :: "'a 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 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

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 literal multiset set ⇒ 'a set" where
"atms_of_ms ψs = ⋃(atms_of ` ψs)"

lemma atms_of_msultiset[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_single_set_mset_atns_of[simp]:
  "atms_of_ms (single ` set_mset B) = atms_of B"
  unfolding atms_of_ms_def atms_of_def by auto

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[]
  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 "{#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+

subsubsection ‹Totality›
definition total_over_set :: "'a 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})"
  using assms 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 clauses"
  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 clauses"
  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[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 "{#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

subsubsection ‹Interpretations›
definition true_cls :: "'a 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:split_if_asm)

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_mset_def by (metis mem_set_mset_iff)

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 interp ⇒ 'a clauses ⇒ 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_mset_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)

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

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_mset_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

subsubsection ‹Entailment for Multisets of Clauses›
definition true_cls_mset :: "'a 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: split_if_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_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 clauses"
  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 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)

subsubsection ‹Tautologies›
text ‹We define tautologies as clauses 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_mset_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_mset_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_false[simp]: "¬tautology {#}"
  unfolding tautology_def by auto

lemma tautology_add_single:
  "tautology ({#a#} + L) ⟷ tautology L ∨ -a ∈# L"
  unfolding tautology_decomp by (cases a) auto

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

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 clauses ⇒ bool" (infix "⊨fs" 49) where
"ψ ⊨fs χ ⟷ (∀I. total_over_m I ({ψ} ∪ χ) ⟶ consistent_interp I ⟶ I ⊨ ψ ⟶ I ⊨s χ)"

definition true_clss_cls :: "'a clauses ⇒ '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 clauses ⇒ 'a clauses ⇒ 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_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)

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_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 clauses"
    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)

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 D + {#- L#}"
  and C: "N ⊨p C + {#L#}"
  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' {D + {#- L#}}"
      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' ⊨ D + {#- L#}"
      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_union_mset_true_clss_cls_or_not_true_clss_cls_or:
  assumes D: "N ⊨p D + {#- L#}"
  and C: "N ⊨p C + {#L#}"
  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› unfolding consistent_interp_def
    by auto
  }
  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' {D + {#- L#}}"
      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' ⊨ D + {#- L#}"
      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

(* TODO Move upper *)
lemma satisfiable_carac[iff]:
  "(∃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


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_le_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 split: split_if_asm simp add: atm_of_eq_atm_of atms_of_def)

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}" by auto

  {
    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 "I ∪ {L} ⊨ D" unfolding true_cls_def by force
    then have "I ∪ {L} ⊨ φ" 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
      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 add: subseteq_mset_def)
  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 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) =
    (op + {#Pos l#}) ` (simple_clss atms)
    ∪ (op + {#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 "L ∉# C - {#L#}"
        using dist unfolding distinct_mset_def by auto
      moreover have "-L ∉# C"
        using taut Add by auto
      ultimately have "atms_of (C - {#L#}) ⊆ atms"
        using atms Add by (auto simp: atm_iff_pos_or_neg_lit split: split_if_asm dest!: H)

      moreover have "¬ tautology (C - {#L#})"
        using taut by (metis Add(1) insert_DiffM tautology_add_single)
      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 auto
    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: split_if_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 by (metis assms atm_of_lit_in_atms_of atms literal.sel(1,2) subset_eq
          tautology_add_single uminus_Neg uminus_Pos)
      moreover have "distinct_mset C"
        using dist C' L
        by (metis assms atm_of_lit_in_atms_of atms contra_subsetD distinct_mset_add_single
          literal.sel(1,2))
      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'. {#Pos l#} + C' ∉ simple_clss C"
    "⋀C'. {#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 (metis insert_noteq_member literal.distinct(1) union_commute)
      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 = "(op + {#Pos l#}) ` (simple_clss C)"
  let ?N = "(op + {#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 "op + {#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 "op + {#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)

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 interp ⇒ 'a literal ⇒ bool
*   true_cls      ⊨l  'a interp ⇒ 'a clause ⇒ bool
⟶ true_clss     ⊨s  'a interp ⇒ 'a clauses ⇒ bool

*   true_annot    ⊨a   ann_literals ⇒ 'a clause ⇒ bool
⟶ true_annots   ⊨as  ann_literals ⇒ 'a clauses ⇒ bool

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

*   true_clss_cls  ⊨p  'a clauses ⇒ 'a clause ⇒ bool
⟶ true_clss_clss ⊨ps 'a clauses ⇒ 'a clauses ⇒ 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 literal multiset 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[]
    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)
end