Theory Entailment_Definition.Partial_Annotated_Herbrand_Interpretation

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

section ‹Partial Annotated Herbrand Interpretation›
text ‹We here define decided literals (that will be used in both DPLL and CDCL) and the entailment
  corresponding to it.›

theory Partial_Annotated_Herbrand_Interpretation
imports
   Partial_Herbrand_Interpretation
begin


subsection ‹Decided Literals›

subsubsection ‹Definition›

datatype ('v, 'w, 'mark) annotated_lit =
  is_decided: Decided (lit_dec: 'v) |
  is_proped: Propagated (lit_prop: 'w) (mark_of: 'mark)

type_synonym ('v, 'w, 'mark) annotated_lits = ‹('v, 'w, 'mark) annotated_lit list›
type_synonym ('v, 'mark) ann_lit = ‹('v literal, 'v literal, 'mark) annotated_lit›

lemma ann_lit_list_induct[case_names Nil Decided Propagated]:
  assumes
    ‹P []› and
    ‹⋀L xs. P xs ⟹ P (Decided L # xs)› and
    ‹⋀L m xs. P xs ⟹ P (Propagated L m # xs)›
  shows ‹P xs›
  using assms apply (induction xs, simp)
  by (rename_tac a xs, case_tac a) auto

lemma is_decided_ex_Decided:
  ‹is_decided L ⟹ (⋀K. L = Decided K ⟹ P) ⟹ P›
  by (cases L) auto

lemma is_propedE: ‹is_proped L ⟹ (⋀K C. L = Propagated K C ⟹ P) ⟹ P›
  by (cases L) auto

lemma is_decided_no_proped_iff: ‹is_decided L ⟷ ¬is_proped L›
  by (cases L) auto

lemma not_is_decidedE:
  ‹¬is_decided E ⟹ (⋀K C. E = Propagated K C ⟹ thesis) ⟹ thesis›
  by (cases E) auto

type_synonym ('v, 'm) ann_lits = ‹('v, 'm) ann_lit list›

fun lit_of :: ‹('a, 'a, 'mark) annotated_lit ⇒ 'a› where
  ‹lit_of (Decided L) = L› |
  ‹lit_of (Propagated L _) = L›

definition lits_of :: ‹('a, 'b) ann_lit set ⇒ 'a literal set› where
‹lits_of Ls = lit_of ` Ls›

abbreviation lits_of_l :: ‹('a, 'b) ann_lits ⇒ 'a literal set› where
‹lits_of_l Ls ≡ lits_of (set Ls)›

lemma lits_of_l_empty[simp]:
  ‹lits_of {} = {}›
  unfolding lits_of_def by auto

lemma lits_of_insert[simp]:
  ‹lits_of (insert L Ls) = insert (lit_of L) (lits_of Ls)›
  unfolding lits_of_def by auto

lemma lits_of_l_Un[simp]:
  ‹lits_of (l ∪ l') = lits_of l ∪ lits_of l'›
  unfolding lits_of_def by auto

lemma finite_lits_of_def[simp]:
  ‹finite (lits_of_l L)›
  unfolding lits_of_def by auto

abbreviation unmark where
  ‹unmark ≡ (λa. {#lit_of a#})›

abbreviation unmark_s where
  ‹unmark_s M ≡ unmark ` M›

abbreviation unmark_l where
  ‹unmark_l M ≡ unmark_s (set M)›

lemma atms_of_ms_lambda_lit_of_is_atm_of_lit_of[simp]:
  ‹atms_of_ms (unmark_l M') = atm_of ` lits_of_l M'›
  unfolding atms_of_ms_def lits_of_def by auto

lemma lits_of_l_empty_is_empty[iff]:
  ‹lits_of_l M = {} ⟷ M = []›
  by (induct M) (auto simp: lits_of_def)

lemma in_unmark_l_in_lits_of_l_iff: ‹{#L#} ∈ unmark_l M ⟷ L ∈ lits_of_l M›
  by (induction M) auto

lemma atm_lit_of_set_lits_of_l:
  "(λl. atm_of (lit_of l)) ` set xs = atm_of ` lits_of_l xs"
  unfolding lits_of_def by auto


subsubsection ‹Entailment›

definition true_annot :: ‹('a, 'm) ann_lits ⇒ 'a clause ⇒ bool› (infix "⊨a" 49) where
  ‹I ⊨a C ⟷ (lits_of_l I) ⊨ C›

definition true_annots :: ‹('a, 'm) ann_lits ⇒ 'a clause_set ⇒ bool› (infix "⊨as" 49) where
  ‹I ⊨as CC ⟷ (∀C ∈ CC. I ⊨a C)›

lemma true_annot_empty_model[simp]:
  ‹¬[] ⊨a ψ›
  unfolding true_annot_def true_cls_def by simp

lemma true_annot_empty[simp]:
  ‹¬I ⊨a {#}›
  unfolding true_annot_def true_cls_def by simp

lemma empty_true_annots_def[iff]:
  ‹[] ⊨as ψ ⟷ ψ = {}›
  unfolding true_annots_def by auto

lemma true_annots_empty[simp]:
  ‹I ⊨as {}›
  unfolding true_annots_def by auto

lemma true_annots_single_true_annot[iff]:
  ‹I ⊨as {C} ⟷ I ⊨a C›
  unfolding true_annots_def by auto

lemma true_annot_insert_l[simp]:
  ‹M ⊨a A ⟹ L # M ⊨a A›
  unfolding true_annot_def by auto

lemma true_annots_insert_l [simp]:
  ‹M ⊨as A ⟹ L # M ⊨as A›
  unfolding true_annots_def by auto

lemma true_annots_union[iff]:
  ‹M ⊨as A ∪ B ⟷ (M ⊨as A ∧ M ⊨as B)›
  unfolding true_annots_def by auto

lemma true_annots_insert[iff]:
  ‹M ⊨as insert a A ⟷ (M ⊨a a ∧ M ⊨as A)›
  unfolding true_annots_def by auto

lemma true_annot_append_l:
  ‹M ⊨a A ⟹ M' @ M ⊨a A›
  unfolding true_annot_def by auto

lemma true_annots_append_l:
  ‹M ⊨as A ⟹ M' @ M ⊨as A›
  unfolding true_annots_def by (auto simp: true_annot_append_l)

text ‹Link between ‹⊨as› and ‹⊨s›:›
lemma true_annots_true_cls:
  ‹I ⊨as CC ⟷ lits_of_l I ⊨s CC›
  unfolding true_annots_def Ball_def true_annot_def true_clss_def by auto

lemma in_lit_of_true_annot:
  ‹a ∈ lits_of_l M ⟷ M ⊨a {#a#}›
  unfolding true_annot_def lits_of_def by auto

lemma true_annot_lit_of_notin_skip:
  ‹L # M ⊨a A ⟹ lit_of L ∉# A ⟹ M ⊨a A›
  unfolding true_annot_def true_cls_def by auto

lemma true_clss_singleton_lit_of_implies_incl:
  ‹I ⊨s unmark_l MLs ⟹ lits_of_l MLs ⊆ I›
  unfolding true_clss_def lits_of_def by auto

lemma true_annot_true_clss_cls:
  ‹MLs ⊨a ψ ⟹ set (map unmark MLs) ⊨p ψ›
  unfolding true_annot_def true_clss_cls_def true_cls_def
  by (auto dest: true_clss_singleton_lit_of_implies_incl)

lemma true_annots_true_clss_cls:
  ‹MLs ⊨as ψ ⟹ set (map unmark MLs) ⊨ps ψ›
  by (auto
    dest: true_clss_singleton_lit_of_implies_incl
    simp add: true_clss_def true_annots_def true_annot_def lits_of_def true_cls_def
    true_clss_clss_def)

lemma true_annots_decided_true_cls[iff]:
  ‹map Decided M ⊨as N ⟷ set M ⊨s N›
proof -
  have *: ‹lit_of ` Decided ` set M = set M› unfolding lits_of_def by force
  show ?thesis by (simp add: true_annots_true_cls * lits_of_def)
qed

lemma true_annot_singleton[iff]: ‹M ⊨a {#L#} ⟷ L ∈ lits_of_l M›
  unfolding true_annot_def lits_of_def by auto

lemma true_annots_true_clss_clss:
  ‹A ⊨as Ψ ⟹ unmark_l A ⊨ps Ψ›
  unfolding true_clss_clss_def true_annots_def true_clss_def
  by (auto dest!: true_clss_singleton_lit_of_implies_incl
    simp: lits_of_def true_annot_def true_cls_def)

lemma true_annot_commute:
  ‹M @ M' ⊨a D ⟷ M' @ M ⊨a D›
  unfolding true_annot_def by (simp add: Un_commute)

lemma true_annots_commute:
  ‹M @ M' ⊨as D ⟷ M' @ M ⊨as D›
  unfolding true_annots_def by (auto simp: true_annot_commute)

lemma true_annot_mono[dest]:
  ‹set I ⊆ set I' ⟹ I ⊨a N ⟹ I' ⊨a N›
  using true_cls_mono_set_mset_l unfolding true_annot_def lits_of_def
  by (metis (no_types) Un_commute Un_upper1 image_Un sup.orderE)

lemma true_annots_mono:
  ‹set I ⊆ set I' ⟹ I ⊨as N ⟹ I' ⊨as N›
  unfolding true_annots_def by auto


subsubsection ‹Defined and Undefined Literals›

text ‹We introduce the functions @{term defined_lit} and @{term undefined_lit} to know whether a
  literal is defined with respect to a list of decided literals (aka a trail in most cases).

  Remark that @{term undefined} already exists and is a completely different Isabelle function.
  ›
definition defined_lit :: ‹('a literal, 'a literal, 'm) annotated_lits ⇒ 'a literal ⇒ bool›
  where
‹defined_lit I L ⟷ (Decided L ∈ set I) ∨ (∃P. Propagated L P ∈ set I)
  ∨ (Decided (-L) ∈ set I) ∨ (∃P. Propagated (-L) P ∈ set I)›

abbreviation undefined_lit :: ‹('a literal, 'a literal, 'm) annotated_lits ⇒ 'a literal ⇒ bool›
where ‹undefined_lit I L ≡ ¬defined_lit I L›

lemma defined_lit_rev[simp]:
  ‹defined_lit (rev M) L ⟷ defined_lit M L›
  unfolding defined_lit_def by auto

lemma atm_imp_decided_or_proped:
  assumes ‹x ∈ set I›
  shows
    ‹(Decided (- lit_of x) ∈ set I)
    ∨ (Decided (lit_of x) ∈ set I)
    ∨ (∃l. Propagated (- lit_of x) l ∈ set I)
    ∨ (∃l. Propagated (lit_of x) l ∈ set I)›
  using assms by (metis (full_types) lit_of.elims)

lemma literal_is_lit_of_decided:
  assumes ‹L = lit_of x›
  shows ‹(x = Decided L) ∨ (∃l'. x = Propagated L l')›
  using assms by (cases x) auto

lemma true_annot_iff_decided_or_true_lit:
  ‹defined_lit I L ⟷ (lits_of_l I ⊨l L ∨ lits_of_l I ⊨l -L)›
  unfolding defined_lit_def by (auto simp add: lits_of_def rev_image_eqI
    dest!: literal_is_lit_of_decided)

lemma consistent_inter_true_annots_satisfiable:
  ‹consistent_interp (lits_of_l I) ⟹ I ⊨as N ⟹ satisfiable N›
  by (simp add: true_annots_true_cls)

lemma defined_lit_map:
  ‹defined_lit Ls L ⟷ atm_of L ∈ (λl. atm_of (lit_of l)) ` set Ls›
 unfolding defined_lit_def apply (rule iffI)
   using image_iff apply fastforce
 by (fastforce simp add: atm_of_eq_atm_of dest: atm_imp_decided_or_proped)

lemma defined_lit_uminus[iff]:
  ‹defined_lit I (-L) ⟷ defined_lit I L›
  unfolding defined_lit_def by auto

lemma Decided_Propagated_in_iff_in_lits_of_l:
  ‹defined_lit I L ⟷ (L ∈ lits_of_l I ∨ -L ∈ lits_of_l I)›
  unfolding lits_of_def by (metis lits_of_def true_annot_iff_decided_or_true_lit true_lit_def)

lemma consistent_add_undefined_lit_consistent[simp]:
  assumes
    ‹consistent_interp (lits_of_l Ls)› and
    ‹undefined_lit Ls L›
  shows ‹consistent_interp (insert L (lits_of_l Ls))›
  using assms unfolding consistent_interp_def by (auto simp: Decided_Propagated_in_iff_in_lits_of_l)

lemma decided_empty[simp]:
  ‹¬defined_lit [] L›
  unfolding defined_lit_def by simp

lemma undefined_lit_single[iff]:
  ‹defined_lit [L] K ⟷ atm_of (lit_of L) = atm_of K›
  by (auto simp: defined_lit_map)

lemma undefined_lit_cons[iff]:
  ‹undefined_lit (L # M) K ⟷ atm_of (lit_of L) ≠ atm_of K ∧ undefined_lit M K›
  by (auto simp: defined_lit_map)

lemma undefined_lit_append[iff]:
  ‹undefined_lit (M @ M') K ⟷ undefined_lit M K ∧ undefined_lit M' K›
  by (auto simp: defined_lit_map)

lemma defined_lit_cons:
  ‹defined_lit (L # M) K ⟷ atm_of (lit_of L) = atm_of K ∨ defined_lit M K›
  by (auto simp: defined_lit_map)

lemma defined_lit_append:
  ‹defined_lit (M @ M') K ⟷ defined_lit M K ∨ defined_lit M' K›
  by (auto simp: defined_lit_map)

lemma in_lits_of_l_defined_litD: ‹L_max ∈ lits_of_l M ⟹ defined_lit M L_max›
  by (auto simp: Decided_Propagated_in_iff_in_lits_of_l)

lemma undefined_notin: ‹undefined_lit M (lit_of x) ⟹ x ∉ set M› for x M
  by (metis in_lits_of_l_defined_litD insert_iff lits_of_insert mk_disjoint_insert)

lemma uminus_lits_of_l_definedD:
  ‹-x ∈ lits_of_l M ⟹ defined_lit M x›
  by (simp add: Decided_Propagated_in_iff_in_lits_of_l)

lemma defined_lit_Neg_Pos_iff:
  ‹defined_lit M (Neg A) ⟷ defined_lit M (Pos A)›
  by (simp add: defined_lit_map)

lemma defined_lit_Pos_atm_iff[simp]:
  ‹defined_lit M1 (Pos (atm_of x)) ⟷ defined_lit M1 x›
  by (cases x) (auto simp: defined_lit_Neg_Pos_iff)

lemma defined_lit_mono:
  ‹defined_lit M2 L ⟹ set M2 ⊆ set M3 ⟹ defined_lit M3 L›
  by (auto simp: Decided_Propagated_in_iff_in_lits_of_l)

lemma defined_lit_nth:
  ‹n < length M2 ⟹ defined_lit M2 (lit_of (M2 ! n))›
  by (auto simp: Decided_Propagated_in_iff_in_lits_of_l lits_of_def)


subsection ‹Backtracking›

fun backtrack_split :: ‹('a, 'v, 'm) annotated_lits
  ⇒ ('a, 'v, 'm) annotated_lits × ('a, 'v, 'm) annotated_lits› where
‹backtrack_split [] = ([], [])› |
‹backtrack_split (Propagated L P # mlits) = apfst ((#) (Propagated L P)) (backtrack_split mlits)› |
‹backtrack_split (Decided L # mlits) = ([], Decided L # mlits)›

lemma backtrack_split_fst_not_decided: ‹a ∈ set (fst (backtrack_split l)) ⟹ ¬is_decided a›
  by (induct l rule: ann_lit_list_induct) auto

lemma backtrack_split_snd_hd_decided:
  ‹snd (backtrack_split l) ≠ [] ⟹ is_decided (hd (snd (backtrack_split l)))›
  by (induct l rule: ann_lit_list_induct) auto

lemma backtrack_split_list_eq[simp]:
  ‹fst (backtrack_split l) @ (snd (backtrack_split l)) = l›
  by (induct l rule: ann_lit_list_induct) auto

lemma backtrack_snd_empty_not_decided:
  ‹backtrack_split M = (M'', []) ⟹ ∀l∈set M. ¬ is_decided l›
  by (metis append_Nil2 backtrack_split_fst_not_decided backtrack_split_list_eq snd_conv)

lemma backtrack_split_some_is_decided_then_snd_has_hd:
  ‹∃l∈set M. is_decided l ⟹ ∃M' L' M''. backtrack_split M = (M'', L' # M')›
  by (metis backtrack_snd_empty_not_decided list.exhaust prod.collapse)

text ‹Another characterisation of the result of @{const backtrack_split}. This view allows some
  simpler proofs, since @{term takeWhile} and @{term dropWhile} are highly automated:›
lemma backtrack_split_takeWhile_dropWhile:
  ‹backtrack_split M = (takeWhile (Not o is_decided) M, dropWhile (Not o is_decided) M)›
  by (induction M rule: ann_lit_list_induct) auto

subsection ‹Decomposition with respect to the First Decided Literals›
text ‹In this section we define a function that returns a decomposition with the first decided
  literal. This function is useful to define the backtracking of DPLL.›
subsubsection ‹Definition›
(*TODO: replace apsnd by let? Try to find some better expression on this function.
Ideas:
  * swap the side of Decided
  * case on the form of dropWhile (Not o is_decided)

Split function in 2 + list.product
*)
text ‹The pattern @{term ‹get_all_ann_decomposition [] = [([], [])]›} is necessary otherwise, we
  can call the @{term hd} function in the other pattern. ›
fun get_all_ann_decomposition :: ‹('a, 'b, 'm) annotated_lits
  ⇒ (('a, 'b, 'm) annotated_lits × ('a, 'b, 'm) annotated_lits) list› where
‹get_all_ann_decomposition (Decided L # Ls) =
  (Decided L # Ls, []) # get_all_ann_decomposition Ls› |
‹get_all_ann_decomposition (Propagated L P# Ls) =
  (apsnd ((#) (Propagated L P)) (hd (get_all_ann_decomposition Ls)))
    # tl (get_all_ann_decomposition Ls)› |
‹get_all_ann_decomposition [] = [([], [])]›

value ‹get_all_ann_decomposition [Propagated A5 B5, Decided C4, Propagated A3 B3,
  Propagated A2 B2, Decided C1, Propagated A0 B0]›

(*

fun get_all_ann_decomp where
‹get_all_ann_decomp [] ls = [([], ls)]› |
‹get_all_ann_decomp (L # Ls) ls =
  (if is_decided L then (L # Ls, ls) # get_all_ann_decomp Ls []
   else get_all_ann_decomp Ls (L # ls)) ›

abbreviation get_all_ann_decomposition where
‹get_all_ann_decomposition l ≡ get_all_ann_decomp l []›

lemma get_all_ann_decomposition_never_empty[iff]:
  ‹get_all_ann_decomp M l = [] ⟷ False›
  by (induct M arbitrary: l, simp) (case_tac a, auto)
*)

text ‹Now we can prove several simple properties about the function.›

lemma get_all_ann_decomposition_never_empty[iff]:
  ‹get_all_ann_decomposition M = [] ⟷ False›
  by (induct M, simp) (rename_tac a xs, case_tac a, auto)

lemma get_all_ann_decomposition_never_empty_sym[iff]:
  ‹[] = get_all_ann_decomposition M ⟷ False›
  using get_all_ann_decomposition_never_empty[of M] by presburger

lemma get_all_ann_decomposition_decomp:
  ‹hd (get_all_ann_decomposition S) = (a, c) ⟹ S = c @ a›
proof (induct S arbitrary: a c)
  case Nil
  then show ?case by simp
next
  case (Cons x A)
  then show ?case by (cases x; cases ‹hd (get_all_ann_decomposition A)›) auto
qed

lemma get_all_ann_decomposition_backtrack_split:
  ‹backtrack_split S = (M, M') ⟷ hd (get_all_ann_decomposition S) = (M', M)›
proof (induction S arbitrary: M M')
  case Nil
  then show ?case by auto
next
  case (Cons a S)
  then show ?case using backtrack_split_takeWhile_dropWhile by (cases a) force+
qed

lemma get_all_ann_decomposition_Nil_backtrack_split_snd_Nil:
  ‹get_all_ann_decomposition S = [([], A)] ⟹ snd (backtrack_split S) = []›
  by (simp add: get_all_ann_decomposition_backtrack_split sndI)

text ‹This functions says that the first element is either empty or starts with a decided element
  of the list.›
lemma get_all_ann_decomposition_length_1_fst_empty_or_length_1:
  assumes ‹get_all_ann_decomposition M = (a, b) # []›
  shows ‹a = [] ∨ (length a = 1 ∧ is_decided (hd a) ∧ hd a ∈ set M)›
  using assms
proof (induct M arbitrary: a b rule: ann_lit_list_induct)
  case Nil then show ?case by simp
next
  case (Decided L mark)
  then show ?case by simp
next
  case (Propagated L mark M)
  then show ?case by (cases ‹get_all_ann_decomposition M›) force+
qed

lemma get_all_ann_decomposition_fst_empty_or_hd_in_M:
  assumes ‹get_all_ann_decomposition M = (a, b) # l›
  shows ‹a = [] ∨ (is_decided (hd a) ∧ hd a ∈ set M)›
  using assms
proof (induct M arbitrary: a b rule: ann_lit_list_induct)
  case Nil
  then show ?case by auto
next
  case (Decided L ann xs)
  then show ?case by auto
next
  case (Propagated L m xs) note IH = this(1) and d = this(2)
  then show ?case
    using IH[of ‹fst (hd (get_all_ann_decomposition xs))› ‹snd (hd(get_all_ann_decomposition xs))›]
    by (cases ‹get_all_ann_decomposition xs›; cases a) auto
qed

lemma get_all_ann_decomposition_snd_not_decided:
  assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
  and ‹L ∈ set b›
  shows ‹¬is_decided L›
  using assms apply (induct M arbitrary: a b rule: ann_lit_list_induct, simp)
  by (rename_tac L' xs a b, case_tac ‹get_all_ann_decomposition xs›; fastforce)+

lemma tl_get_all_ann_decomposition_skip_some:
  assumes ‹x ∈ set (tl (get_all_ann_decomposition M1))›
  shows ‹x ∈ set (tl (get_all_ann_decomposition (M0 @ M1)))›
  using assms
  by (induct M0 rule: ann_lit_list_induct)
     (auto simp add: list.set_sel(2))

lemma hd_get_all_ann_decomposition_skip_some:
  assumes ‹(x, y) = hd (get_all_ann_decomposition M1)›
  shows ‹(x, y) ∈ set (get_all_ann_decomposition (M0 @ Decided K # M1))›
  using assms
proof (induction M0 rule: ann_lit_list_induct)
  case Nil
  then show ?case by auto
next
  case (Decided L M0)
  then show ?case by auto
next
  case (Propagated L C M0) note xy = this(1)[OF this(2-)] and hd = this(2)
  then show ?case
    by (cases ‹get_all_ann_decomposition (M0 @ Decided K # M1)›)
       (auto dest!: get_all_ann_decomposition_decomp
          arg_cong[of ‹get_all_ann_decomposition _› _ hd])
qed

lemma in_get_all_ann_decomposition_in_get_all_ann_decomposition_prepend:
  ‹(a, b) ∈ set (get_all_ann_decomposition M') ⟹
    ∃b'. (a, b' @ b) ∈ set (get_all_ann_decomposition (M @ M'))›
  apply (induction M rule: ann_lit_list_induct)
    apply (metis append_Nil)
   apply auto[]
  by (rename_tac L' m xs, case_tac ‹get_all_ann_decomposition (xs @ M')›) auto

lemma in_get_all_ann_decomposition_decided_or_empty:
  assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
  shows ‹a = [] ∨ (is_decided (hd a))›
  using assms
proof (induct M arbitrary: a b rule: ann_lit_list_induct)
  case Nil then show ?case by simp
next
  case (Decided l M)
  then show ?case by auto
next
  case (Propagated l mark M)
  then show ?case by (cases ‹get_all_ann_decomposition M›) force+
qed

lemma get_all_ann_decomposition_remove_undecided_length:
  assumes ‹∀l ∈ set M'. ¬is_decided l›
  shows ‹length (get_all_ann_decomposition (M' @ M'')) = length (get_all_ann_decomposition M'')›
  using assms by (induct M' arbitrary: M'' rule: ann_lit_list_induct) auto

lemma get_all_ann_decomposition_not_is_decided_length:
  assumes ‹∀l ∈ set M'. ¬is_decided l›
  shows ‹1 + length (get_all_ann_decomposition (Propagated (-L) P # M))
 = length (get_all_ann_decomposition (M' @ Decided L # M))›
 using assms get_all_ann_decomposition_remove_undecided_length by fastforce

lemma get_all_ann_decomposition_last_choice:
  assumes ‹tl (get_all_ann_decomposition (M' @ Decided L # M)) ≠ []›
  and ‹∀l ∈ set M'. ¬is_decided l›
  and ‹hd (tl (get_all_ann_decomposition (M' @ Decided L # M))) = (M0', M0)›
  shows ‹hd (get_all_ann_decomposition (Propagated (-L) P # M)) = (M0', Propagated (-L) P # M0)›
  using assms by (induct M' rule: ann_lit_list_induct) auto

lemma get_all_ann_decomposition_except_last_choice_equal:
  assumes ‹∀l ∈ set M'. ¬is_decided l›
  shows ‹tl (get_all_ann_decomposition (Propagated (-L) P # M))
 = tl (tl (get_all_ann_decomposition (M' @ Decided L # M)))›
  using assms by (induct M' rule: ann_lit_list_induct) auto

lemma get_all_ann_decomposition_hd_hd:
  assumes ‹get_all_ann_decomposition Ls = (M, C) # (M0, M0') # l›
  shows ‹tl M = M0' @ M0 ∧ is_decided (hd M)›
  using assms
proof (induct Ls arbitrary: M C M0 M0' l)
  case Nil
  then show ?case by simp
next
  case (Cons a Ls M C M0 M0' l) note IH = this(1) and g = this(2)
  { fix L ann level
    assume a: ‹a = Decided L›
    have ‹Ls = M0' @ M0›
      using g a by (force intro: get_all_ann_decomposition_decomp)
    then have ‹tl M = M0' @ M0 ∧ is_decided (hd M)› using g a by auto
  }
  moreover {
    fix L P
    assume a: ‹a = Propagated L P›
    have ‹tl M = M0' @ M0 ∧ is_decided (hd M)›
      using IH Cons.prems unfolding a by (cases ‹get_all_ann_decomposition Ls›) auto
  }
  ultimately show ?case by (cases a) auto
qed

lemma get_all_ann_decomposition_exists_prepend[dest]:
  assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
  shows ‹∃c. M = c @ b @ a›
  using assms apply (induct M rule: ann_lit_list_induct)
    apply simp
  by (rename_tac L' xs, case_tac ‹get_all_ann_decomposition xs›;
    auto dest!: arg_cong[of ‹get_all_ann_decomposition _› _ hd]
      get_all_ann_decomposition_decomp)+

lemma get_all_ann_decomposition_incl:
  assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
  shows ‹set b ⊆ set M› and ‹set a ⊆ set M›
  using assms get_all_ann_decomposition_exists_prepend by fastforce+

lemma get_all_ann_decomposition_exists_prepend':
  assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
  obtains c where ‹M = c @ b @ a›
  using assms apply (induct M rule: ann_lit_list_induct)
    apply auto[1]
  by (rename_tac L' xs, case_tac ‹hd (get_all_ann_decomposition xs)›,
    auto dest!: get_all_ann_decomposition_decomp simp add: list.set_sel(2))+

lemma union_in_get_all_ann_decomposition_is_subset:
  assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
  shows ‹set a ∪ set b ⊆ set M›
  using assms by force

lemma Decided_cons_in_get_all_ann_decomposition_append_Decided_cons:
  ‹∃c''. (Decided K # c, c'') ∈ set (get_all_ann_decomposition (c' @ Decided K # c))›
  apply (induction c' rule: ann_lit_list_induct)
    apply auto[2]
  apply (rename_tac L xs,
      case_tac ‹hd (get_all_ann_decomposition (xs @ Decided K # c))›)
  apply (case_tac ‹get_all_ann_decomposition (xs @ Decided K # c)›)
  by auto

lemma fst_get_all_ann_decomposition_prepend_not_decided:
  assumes ‹∀m∈set MS. ¬ is_decided m›
  shows ‹set (map fst (get_all_ann_decomposition M))
    = set (map fst (get_all_ann_decomposition (MS @ M)))›
  using assms apply (induction MS rule: ann_lit_list_induct)
  apply auto[2]
  by (rename_tac L m xs; case_tac ‹get_all_ann_decomposition (xs @ M)›) simp_all

lemma no_decision_get_all_ann_decomposition:
  ‹∀l∈set M. ¬ is_decided l ⟹  get_all_ann_decomposition M = [([], M)]›
  by (induction M rule: ann_lit_list_induct) auto


subsubsection ‹Entailment of the Propagated by the Decided Literal›

lemma get_all_ann_decomposition_snd_union:
  ‹set M = ⋃(set ` snd ` set (get_all_ann_decomposition M)) ∪ {L |L. is_decided L ∧ L ∈ set M}›
  (is ‹?M M = ?U M ∪ ?Ls M›)
proof (induct M rule: ann_lit_list_induct)
  case Nil
  then show ?case by simp
next
  case (Decided L M) note IH = this(1)
  then have ‹Decided L ∈ ?Ls (Decided L # M)› by auto
  moreover have ‹?U (Decided L # M) = ?U M› by auto
  moreover have ‹?M M = ?U M ∪ ?Ls M› using IH by auto
  ultimately show ?case by auto
next
  case (Propagated L m M)
  then show ?case by (cases ‹(get_all_ann_decomposition M)›) auto
qed



definition all_decomposition_implies :: ‹'a clause set
  ⇒ (('a, 'm) ann_lits × ('a, 'm) ann_lits) list ⇒ bool› where
 ‹all_decomposition_implies N S ⟷ (∀(Ls, seen) ∈ set S. unmark_l Ls ∪ N ⊨ps unmark_l seen)›

lemma all_decomposition_implies_empty[iff]:
  ‹all_decomposition_implies N []› unfolding all_decomposition_implies_def by auto

lemma all_decomposition_implies_single[iff]:
  ‹all_decomposition_implies N [(Ls, seen)] ⟷ unmark_l Ls ∪ N ⊨ps unmark_l seen›
  unfolding all_decomposition_implies_def by auto

lemma all_decomposition_implies_append[iff]:
  ‹all_decomposition_implies N (S @ S')
    ⟷ (all_decomposition_implies N S ∧ all_decomposition_implies N S')›
  unfolding all_decomposition_implies_def by auto

lemma all_decomposition_implies_cons_pair[iff]:
  ‹all_decomposition_implies N ((Ls, seen) # S')
    ⟷ (all_decomposition_implies N [(Ls, seen)] ∧ all_decomposition_implies N S')›
  unfolding all_decomposition_implies_def by auto

lemma all_decomposition_implies_cons_single[iff]:
  ‹all_decomposition_implies N (l # S') ⟷
    (unmark_l (fst l) ∪ N ⊨ps unmark_l (snd l) ∧
      all_decomposition_implies N S')›
  unfolding all_decomposition_implies_def by auto

lemma all_decomposition_implies_trail_is_implied:
  assumes ‹all_decomposition_implies N (get_all_ann_decomposition M)›
  shows ‹N ∪ {unmark L |L. is_decided L ∧ L ∈ set M}
    ⊨ps unmark ` ⋃(set ` snd ` set (get_all_ann_decomposition M))›
using assms
proof (induct ‹length (get_all_ann_decomposition M)› arbitrary: M)
  case 0
  then show ?case by auto
next
  case (Suc n) note IH = this(1) and length = this(2) and decomp = this(3)
  consider
      (le1) ‹length (get_all_ann_decomposition M) ≤ 1›
    | (gt1) ‹length (get_all_ann_decomposition M) > 1›
    by arith
  then show ?case
    proof cases
      case le1
      then obtain a b where g: ‹get_all_ann_decomposition M = (a, b) # []›
        by (cases ‹get_all_ann_decomposition M›) auto
      moreover {
        assume ‹a = []›
        then have ?thesis using Suc.prems g by auto
      }
      moreover {
        assume l: ‹length a = 1› and m: ‹is_decided (hd a)› and hd: ‹hd a ∈ set M›
        then have ‹unmark (hd a) ∈ {unmark L |L. is_decided L ∧ L ∈ set M}› by auto
        then have H: ‹unmark_l a ∪ N ⊆ N ∪ {unmark L |L. is_decided L ∧ L ∈ set M}›
          using l by (cases a) auto
        have f1: ‹unmark_l a ∪ N ⊨ps unmark_l b›
          using decomp unfolding all_decomposition_implies_def g by simp
        have ?thesis
          apply (rule true_clss_clss_subset) using f1 H g by auto
      }
      ultimately show ?thesis
        using get_all_ann_decomposition_length_1_fst_empty_or_length_1 by blast
    next
      case gt1
      then obtain Ls0 seen0 M' where
        Ls0: ‹get_all_ann_decomposition M = (Ls0, seen0) # get_all_ann_decomposition M'› and
        length': ‹length (get_all_ann_decomposition M') = n› and
        M'_in_M: ‹set M' ⊆ set M›
        using length by (induct M rule: ann_lit_list_induct) (auto simp: subset_insertI2)
      let ?d = ‹⋃(set ` snd ` set (get_all_ann_decomposition M'))›
      let ?unM = ‹{unmark L |L. is_decided L ∧ L ∈ set M}›
      let ?unM' = ‹{unmark L |L. is_decided L ∧ L ∈ set M'}›
      {
        assume ‹n = 0›
        then have ‹get_all_ann_decomposition M' = []› using length' by auto
        then have ?thesis using Suc.prems unfolding all_decomposition_implies_def Ls0 by auto
      }
      moreover {
        assume n: ‹n > 0›
        then obtain Ls1 seen1 l where
          Ls1: ‹get_all_ann_decomposition M' = (Ls1, seen1) # l›
          using length' by (induct M' rule: ann_lit_list_induct) auto

        have ‹all_decomposition_implies N (get_all_ann_decomposition M')›
          using decomp unfolding Ls0 by auto
        then have N: ‹N ∪ ?unM' ⊨ps unmark_s ?d›
          using IH length' by auto
        have l: ‹N ∪ ?unM' ⊆ N ∪ ?unM›
          using M'_in_M by auto
        from true_clss_clss_subset[OF this N]
        have ΨN: ‹N ∪ ?unM ⊨ps unmark_s ?d› by auto
        have ‹is_decided (hd Ls0)› and LS: ‹tl Ls0 = seen1 @ Ls1›
          using get_all_ann_decomposition_hd_hd[of M] unfolding Ls0 Ls1 by auto

        have LSM: ‹seen1 @ Ls1 = M'› using get_all_ann_decomposition_decomp[of M'] Ls1 by auto
        have M': ‹set M' = ?d ∪ {L |L. is_decided L ∧ L ∈ set M'}›
          using get_all_ann_decomposition_snd_union by auto

        {
          assume ‹Ls0 ≠ []›
          then have ‹hd Ls0 ∈ set M›
            using get_all_ann_decomposition_fst_empty_or_hd_in_M Ls0 by blast
          then have ‹N ∪ ?unM ⊨p unmark (hd Ls0)›
            using ‹is_decided (hd Ls0)› by (metis (mono_tags, lifting) UnCI mem_Collect_eq
              true_clss_cls_in)
        } note hd_Ls0 = this

        have l: ‹unmark ` (?d ∪ {L |L. is_decided L ∧ L ∈ set M'}) = unmark_s ?d ∪ ?unM'›
          by auto
        have ‹N ∪ ?unM' ⊨ps unmark ` (?d ∪ {L |L. is_decided L ∧ L ∈ set M'})›
          unfolding l using N by (auto simp: all_in_true_clss_clss)
        then have t: ‹N ∪ ?unM' ⊨ps unmark_l (tl Ls0)›
          using M' unfolding LS LSM by auto
        then have ‹N ∪ ?unM ⊨ps unmark_l (tl Ls0)›
          using M'_in_M true_clss_clss_subset[OF _ t, of ‹N ∪ ?unM›] by auto
        then have ‹N ∪ ?unM ⊨ps unmark_l Ls0›
          using hd_Ls0 by (cases Ls0) auto

        moreover have ‹unmark_l Ls0 ∪ N ⊨ps unmark_l seen0›
          using decomp unfolding Ls0 by simp
        moreover have ‹⋀M Ma. (M::'a clause set) ∪ Ma ⊨ps M›
          by (simp add: all_in_true_clss_clss)
        ultimately have Ψ: ‹N ∪ ?unM ⊨ps unmark_l seen0›
          by (meson true_clss_clss_left_right true_clss_clss_union_and true_clss_clss_union_l_r)

        moreover have ‹unmark ` (set seen0 ∪ ?d) = unmark_l seen0 ∪ unmark_s ?d›
          by auto
        ultimately have ?thesis using ΨN unfolding Ls0 by simp
      }
      ultimately show ?thesis by auto
    qed
qed

lemma all_decomposition_implies_propagated_lits_are_implied:
  assumes ‹all_decomposition_implies N (get_all_ann_decomposition M)›
  shows ‹N ∪ {unmark L |L. is_decided L ∧ L ∈ set M} ⊨ps unmark_l M›
    (is ‹?I ⊨ps ?A›)
proof -
  have ‹?I ⊨ps unmark_s {L |L. is_decided L ∧ L ∈ set M}›
    by (auto intro: all_in_true_clss_clss)
  moreover have ‹?I ⊨ps unmark ` ⋃(set ` snd ` set (get_all_ann_decomposition M))›
    using all_decomposition_implies_trail_is_implied assms by blast
  ultimately have ‹N ∪ {unmark m |m. is_decided m ∧ m ∈ set M}
    ⊨ps unmark ` ⋃(set ` snd ` set (get_all_ann_decomposition M))
      ∪ unmark ` {m |m. is_decided m ∧ m ∈ set M}›
      by blast
  then show ?thesis
    by (metis (no_types) get_all_ann_decomposition_snd_union[of M] image_Un)
qed

lemma all_decomposition_implies_insert_single:
  ‹all_decomposition_implies N M ⟹ all_decomposition_implies (insert C N) M›
  unfolding all_decomposition_implies_def by auto

lemma all_decomposition_implies_union:
  ‹all_decomposition_implies N M ⟹ all_decomposition_implies (N ∪ N') M›
  unfolding all_decomposition_implies_def sup.assoc[symmetric] by (auto intro: true_clss_clss_union_l)

lemma all_decomposition_implies_mono:
  ‹N ⊆ N' ⟹ all_decomposition_implies N M ⟹ all_decomposition_implies N' M›
  by (metis all_decomposition_implies_union le_iff_sup)

lemma all_decomposition_implies_mono_right:
  ‹all_decomposition_implies I (get_all_ann_decomposition (M' @ M)) ⟹
    all_decomposition_implies I (get_all_ann_decomposition M)›
  apply (induction M' arbitrary: M rule: ann_lit_list_induct)
  subgoal by auto
  subgoal by auto
  subgoal for L C M' M
    by (cases ‹get_all_ann_decomposition (M' @ M)›) auto
  done


subsection ‹Negation of a Clause›

text ‹
  We define the negation of a @{typ ‹'a clause›}: it converts a single clause to a set of clauses,
  where each clause is a single literal (whose negation is in the original clause).›
definition CNot :: ‹'v clause ⇒ 'v clause_set› where
‹CNot ψ = { {#-L#} | L. L ∈# ψ }›

lemma finite_CNot[simp]: ‹finite (CNot C)›
  by (auto simp: CNot_def)

lemma in_CNot_uminus[iff]:
  shows ‹{#L#} ∈ CNot ψ ⟷ -L ∈# ψ›
  unfolding CNot_def by force

lemma
  shows
    CNot_add_mset[simp]: ‹CNot (add_mset L ψ) = insert {#-L#} (CNot ψ)› and
    CNot_empty[simp]: ‹CNot {#} = {}› and
    CNot_plus[simp]: ‹CNot (A + B) = CNot A ∪ CNot B›
  unfolding CNot_def by auto

lemma CNot_eq_empty[iff]:
  ‹CNot D = {} ⟷ D = {#}›
  unfolding CNot_def by (auto simp add: multiset_eqI)

lemma in_CNot_implies_uminus:
  assumes ‹L ∈# D› and ‹M ⊨as CNot D›
  shows ‹M ⊨a {#-L#}› and ‹-L ∈ lits_of_l M›
  using assms by (auto simp: true_annots_def true_annot_def CNot_def)

lemma CNot_remdups_mset[simp]:
  ‹CNot (remdups_mset A) = CNot A›
  unfolding CNot_def by auto

lemma Ball_CNot_Ball_mset[simp]:
  ‹(∀x∈CNot D. P x) ⟷ (∀L∈# D. P {#-L#})›
 unfolding CNot_def by auto

lemma consistent_CNot_not:
  assumes ‹consistent_interp I›
  shows ‹I ⊨s CNot φ ⟹ ¬I ⊨ φ›
  using assms unfolding consistent_interp_def true_clss_def true_cls_def by auto

lemma total_not_true_cls_true_clss_CNot:
  assumes ‹total_over_m I {φ}› and ‹¬I ⊨ φ›
  shows ‹I ⊨s CNot φ›
  using assms unfolding total_over_m_def total_over_set_def true_clss_def true_cls_def CNot_def
    apply clarify
  by (rename_tac x L, case_tac L) (force intro: pos_lit_in_atms_of neg_lit_in_atms_of)+

lemma total_not_CNot:
  assumes ‹total_over_m I {φ}› and ‹¬I ⊨s CNot φ›
  shows ‹I ⊨ φ›
  using assms total_not_true_cls_true_clss_CNot by auto

lemma atms_of_ms_CNot_atms_of[simp]:
  ‹atms_of_ms (CNot C) = atms_of C›
  unfolding atms_of_ms_def atms_of_def CNot_def by fastforce

lemma true_clss_clss_contradiction_true_clss_cls_false:
  ‹C ∈ D ⟹ D ⊨ps CNot C ⟹ D ⊨p {#}›
  unfolding true_clss_clss_def true_clss_cls_def total_over_m_def
  by (metis Un_commute atms_of_empty atms_of_ms_CNot_atms_of atms_of_ms_insert atms_of_ms_union
    consistent_CNot_not insert_absorb sup_bot.left_neutral true_clss_def)

lemma true_annots_CNot_all_atms_defined:
  assumes ‹M ⊨as CNot T› and a1: ‹L ∈# T›
  shows ‹atm_of L ∈ atm_of ` lits_of_l M›
  by (metis assms atm_of_uminus image_eqI in_CNot_implies_uminus(1) true_annot_singleton)

lemma true_annots_CNot_all_uminus_atms_defined:
  assumes ‹M ⊨as CNot T› and a1: ‹-L ∈# T›
  shows ‹atm_of L ∈ atm_of ` lits_of_l M›
  by (metis assms atm_of_uminus image_eqI in_CNot_implies_uminus(1) true_annot_singleton)

lemma true_clss_clss_false_left_right:
  assumes ‹{{#L#}} ∪ B ⊨p {#}›
  shows ‹B ⊨ps CNot {#L#}›
  unfolding true_clss_clss_def true_clss_cls_def
proof (intro allI impI)
  fix I
  assume
    tot: ‹total_over_m I (B ∪ CNot {#L#})› and
    cons: ‹consistent_interp I› and
    I: ‹I ⊨s B›
  have ‹total_over_m I ({{#L#}} ∪ B)› using tot by auto
  then have ‹¬I ⊨s insert {#L#} B›
    using assms cons unfolding true_clss_cls_def by simp
  then show ‹I ⊨s CNot {#L#}›
    using tot I by (cases L) auto
qed

lemma true_annots_true_cls_def_iff_negation_in_model:
  ‹M ⊨as CNot C ⟷ (∀L ∈# C. -L ∈ lits_of_l M)›
  unfolding CNot_def true_annots_true_cls true_clss_def by auto

lemma true_clss_def_iff_negation_in_model:
  ‹M ⊨s CNot C ⟷ (∀l ∈# C. -l ∈ M)›
  by (auto simp: CNot_def true_clss_def)

lemma true_annots_CNot_definedD:
  ‹M ⊨as CNot C ⟹ ∀L ∈# C. defined_lit M L›
  unfolding true_annots_true_cls_def_iff_negation_in_model
  by (auto simp: Decided_Propagated_in_iff_in_lits_of_l)

(* TODO Mark as [simp]? *)
lemma true_annot_CNot_diff:
  ‹I ⊨as CNot C ⟹ I ⊨as CNot (C - C')›
  by (auto simp: true_annots_true_cls_def_iff_negation_in_model dest: in_diffD)

lemma CNot_mset_replicate[simp]:
  ‹CNot (mset (replicate n L)) = (if n = 0 then {} else {{#-L#}})›
  by (induction n) auto

lemma consistent_CNot_not_tautology:
  ‹consistent_interp M ⟹ M ⊨s CNot D ⟹ ¬tautology D›
  by (metis atms_of_ms_CNot_atms_of consistent_CNot_not satisfiable_carac' satisfiable_def
    tautology_def total_over_m_def)

lemma atms_of_ms_CNot_atms_of_ms: ‹atms_of_ms (CNot CC) = atms_of_ms {CC}›
  by simp

lemma total_over_m_CNot_toal_over_m[simp]:
  ‹total_over_m I (CNot C) = total_over_set I (atms_of C)›
  unfolding total_over_m_def total_over_set_def by auto

lemma true_clss_cls_plus_CNot:
  assumes
    CC_L: ‹A ⊨p add_mset L CC› and
    CNot_CC: ‹A ⊨ps CNot CC›
  shows ‹A ⊨p {#L#}›
  unfolding true_clss_clss_def true_clss_cls_def CNot_def total_over_m_def
proof (intro allI impI)
  fix I
  assume
    tot: ‹total_over_set I (atms_of_ms (A ∪ {{#L#}}))› and
    cons: ‹consistent_interp I› and
    I: ‹I ⊨s A›
  let ?I = ‹I ∪ {Pos P|P. P ∈ atms_of CC ∧ P ∉ atm_of ` I}›
  have cons': ‹consistent_interp ?I›
    using cons unfolding consistent_interp_def
    by (auto simp: uminus_lit_swap atms_of_def rev_image_eqI)
  have I': ‹?I ⊨s A›
    using I true_clss_union_increase by blast
  have tot_CNot: ‹total_over_m ?I (A ∪ CNot CC)›
    using tot atms_of_s_def by (fastforce simp: total_over_m_def total_over_set_def)

  then have tot_I_A_CC_L: ‹total_over_m ?I (A ∪ {add_mset L CC})›
    using tot unfolding total_over_m_def total_over_set_atm_of by auto
  then have ‹?I ⊨ add_mset L CC› using CC_L cons' I' unfolding true_clss_cls_def by blast
  moreover
    have ‹?I ⊨s CNot CC› using CNot_CC cons' I' tot_CNot unfolding true_clss_clss_def by auto
    then have ‹¬A ⊨p CC›
      by (metis (no_types, lifting) I' atms_of_ms_CNot_atms_of_ms atms_of_ms_union cons'
        consistent_CNot_not tot_CNot total_over_m_def true_clss_cls_def)
    then have ‹¬?I ⊨ CC› using ‹?I ⊨s CNot CC› cons' consistent_CNot_not by blast
  ultimately have ‹?I ⊨ {#L#}› by blast
  then show ‹I ⊨ {#L#}›
    by (metis (no_types, lifting) atms_of_ms_union cons' consistent_CNot_not tot total_not_CNot
      total_over_m_def total_over_set_union true_clss_union_increase)
qed

lemma true_annots_CNot_lit_of_notin_skip:
  assumes LM: ‹L # M ⊨as CNot A› and LA: ‹lit_of L ∉# A› ‹-lit_of L ∉# A›
  shows ‹M ⊨as CNot A›
  using LM unfolding true_annots_def Ball_def
proof (intro allI impI)
  fix l
  assume H: ‹∀x. x ∈ CNot A ⟶ L # M ⊨a x › and l: ‹l ∈ CNot A›
  then have ‹L # M ⊨a l› by auto
  then show ‹M ⊨a l› using LA l by (cases L) (auto simp: CNot_def)
 qed

lemma true_clss_clss_union_false_true_clss_clss_cnot:
  ‹A ∪ {B} ⊨ps {{#}} ⟷ A ⊨ps CNot B›
  using total_not_CNot consistent_CNot_not unfolding total_over_m_def true_clss_clss_def
  by fastforce

lemma true_annot_remove_hd_if_notin_vars:
  assumes ‹a # M'⊨a D› and ‹atm_of (lit_of a) ∉ atms_of D›
  shows ‹M' ⊨a D›
  using assms true_cls_remove_hd_if_notin_vars unfolding true_annot_def by auto

lemma true_annot_remove_if_notin_vars:
  assumes ‹M @ M'⊨a D› and ‹∀x∈atms_of D. x ∉ atm_of ` lits_of_l M›
  shows ‹M' ⊨a D›
  using assms by (induct M) (auto dest: true_annot_remove_hd_if_notin_vars)

lemma true_annots_remove_if_notin_vars:
  assumes ‹M @ M'⊨as D› and ‹∀x∈atms_of_ms D. x ∉ atm_of ` lits_of_l M›
  shows ‹M' ⊨as D› unfolding true_annots_def
  using assms unfolding true_annots_def atms_of_ms_def
  by (force dest: true_annot_remove_if_notin_vars)

lemma all_variables_defined_not_imply_cnot:
  assumes
    ‹∀s ∈ atms_of_ms {B}. s ∈ atm_of ` lits_of_l A› and
    ‹¬ A ⊨a B›
  shows ‹A ⊨as CNot B›
  unfolding true_annot_def true_annots_def Ball_def CNot_def true_lit_def
proof (clarify, rule ccontr)
  fix L
  assume LB: ‹L ∈# B› and L_false: ‹¬ lits_of_l A ⊨ {#}› and L_A: ‹- L ∉ lits_of_l A›
  then have ‹atm_of L ∈ atm_of ` lits_of_l A›
    using assms(1) by (simp add: atm_of_lit_in_atms_of lits_of_def)
  then have ‹L ∈ lits_of_l A ∨ -L ∈ lits_of_l A›
    using atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set by metis
  then have ‹L ∈ lits_of_l A› using L_A by auto
  then show False
    using LB assms(2) unfolding true_annot_def true_lit_def true_cls_def Bex_def
    by blast
qed

lemma CNot_union_mset[simp]:
  ‹CNot (A ∪# B) = CNot A ∪ CNot B›
  unfolding CNot_def by auto

lemma true_clss_clss_true_clss_cls_true_clss_clss:
  assumes
    ‹A ⊨ps unmark_l M› and ‹M ⊨as D›
  shows ‹A ⊨ps D›
  by (meson assms total_over_m_union true_annots_true_cls true_annots_true_clss_clss
      true_clss_clss_def true_clss_clss_left_right true_clss_clss_union_and
      true_clss_clss_union_l_r)

lemma true_clss_clss_CNot_true_clss_cls_unsatisfiable:
  assumes ‹A ⊨ps CNot D› and ‹A ⊨p D›
  shows ‹unsatisfiable A›
  using assms(2) unfolding true_clss_clss_def true_clss_cls_def satisfiable_def
  by (metis (full_types) Un_absorb Un_empty_right assms(1) atms_of_empty
      atms_of_ms_emtpy_set total_over_m_def total_over_m_insert total_over_m_union
      true_cls_empty true_clss_cls_def true_clss_clss_generalise_true_clss_clss
      true_clss_clss_true_clss_cls true_clss_clss_union_false_true_clss_clss_cnot)

lemma true_clss_cls_neg:
  ‹N ⊨p I ⟷ N ∪ (λL. {#-L#}) ` set_mset I ⊨p {#}›
proof -
  have [simp]: ‹(λL. {#- L#}) ` set_mset I = CNot I› for I
    by (auto simp: CNot_def)
  have [iff]: ‹ total_over_m Ia ((λL. {#- L#}) ` set_mset I) ⟷
     total_over_set Ia (atms_of I)› for Ia
    by (auto simp: total_over_m_def
       total_over_set_def atms_of_ms_def atms_of_def)
  show ?thesis
    by (auto simp: true_clss_cls_def consistent_CNot_not
       total_not_CNot)
qed

lemma all_decomposition_implies_conflict_DECO_clause:
  assumes ‹all_decomposition_implies N (get_all_ann_decomposition M)› and
    ‹M ⊨as CNot C› and
    ‹C ∈ N›
  shows ‹N ⊨p (uminus o lit_of) `# (filter_mset is_decided (mset M))›
    (is ‹?I ⊨p ?A›)
proof -
  have ‹{unmark m |m. is_decided m ∧ m ∈ set M} =
       unmark_s {L ∈ set M. is_decided L}›
     by auto
  have ‹N ∪ unmark_s {L ∈ set M. is_decided L} ⊨p {#}›
    by (metis (mono_tags, lifting) UnCI
      ‹{unmark m |m. is_decided m ∧ m ∈ set M} = unmark_s {L ∈ set M. is_decided L}›
      all_decomposition_implies_propagated_lits_are_implied assms
      true_clss_clss_contradiction_true_clss_cls_false true_clss_clss_true_clss_cls_true_clss_clss)
  then show ?thesis
    apply (subst true_clss_cls_neg)
    by (auto simp: image_image)
qed


subsection ‹Other›

definition ‹no_dup L ≡ distinct (map (λl. atm_of (lit_of l)) L)›

lemma no_dup_nil[simp]:
  ‹no_dup []›
  by (auto simp: no_dup_def)

lemma no_dup_cons[simp]:
  ‹no_dup (L # M) ⟷ undefined_lit M (lit_of L) ∧ no_dup M›
  by (auto simp: no_dup_def defined_lit_map)

lemma no_dup_append_cons[iff]:
  ‹no_dup (M @ L # M') ⟷ undefined_lit (M @ M') (lit_of L) ∧ no_dup (M @ M')›
  by (auto simp: no_dup_def defined_lit_map)

lemma no_dup_append_append_cons[iff]:
  ‹no_dup (M0 @ M @ L # M') ⟷ undefined_lit (M0 @ M @ M') (lit_of L) ∧ no_dup (M0 @ M @ M')›
  by (auto simp: no_dup_def defined_lit_map)

lemma no_dup_rev[simp]:
  ‹no_dup (rev M) ⟷ no_dup M›
  by (auto simp: rev_map[symmetric] no_dup_def)

lemma no_dup_appendD:
  ‹no_dup (a @ b) ⟹ no_dup b›
  by (auto simp: no_dup_def)

lemma no_dup_appendD1:
  ‹no_dup (a @ b) ⟹ no_dup a›
  by (auto simp: no_dup_def)

lemma no_dup_length_eq_card_atm_of_lits_of_l:
  assumes ‹no_dup M›
  shows ‹length M = card (atm_of ` lits_of_l M)›
  using assms unfolding lits_of_def by (induct M) (auto simp add: image_image no_dup_def)

lemma distinct_consistent_interp:
  ‹no_dup M ⟹ consistent_interp (lits_of_l M)›
proof (induct M)
  case Nil
  show ?case by auto
next
  case (Cons L M)
  then have a1: ‹consistent_interp (lits_of_l M)› by auto
  have ‹undefined_lit M (lit_of L)›
      using Cons.prems by auto
  then show ?case
    using a1 by simp
qed

lemma same_mset_no_dup_iff:
  ‹mset M = mset M' ⟹ no_dup M ⟷ no_dup M'›
  by (auto simp: no_dup_def same_mset_distinct_iff)

lemma distinct_get_all_ann_decomposition_no_dup:
  assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
  and ‹no_dup M›
  shows ‹no_dup (a @ b)›
  using assms by (force simp: no_dup_def)

lemma true_annots_lit_of_notin_skip:
  assumes ‹L # M ⊨as CNot A›
  and ‹-lit_of L ∉# A›
  and ‹no_dup (L # M)›
  shows ‹M ⊨as CNot A›
proof -
  have ‹∀l ∈# A. -l ∈ lits_of_l (L # M)›
    using assms(1) in_CNot_implies_uminus(2) by blast
  moreover {
    have ‹undefined_lit M (lit_of L)›
      using assms(3) by force
    then have ‹- lit_of L ∉ lits_of_l M›
      by (simp add: Decided_Propagated_in_iff_in_lits_of_l) }
  ultimately have ‹∀ l ∈# A. -l ∈ lits_of_l M›
    using assms(2) by (metis insert_iff list.simps(15) lits_of_insert uminus_of_uminus_id)
  then show ?thesis by (auto simp add: true_annots_def)
qed

lemma no_dup_imp_distinct: ‹no_dup M ⟹ distinct M›
  by (induction M) (auto simp: defined_lit_map)

lemma no_dup_tlD: ‹no_dup a ⟹ no_dup (tl a)›
  unfolding no_dup_def by (cases a) auto

lemma defined_lit_no_dupD:
  ‹defined_lit M1 L ⟹ no_dup (M2 @ M1) ⟹ undefined_lit M2 L›
  ‹defined_lit M1 L ⟹ no_dup (M2' @ M2 @ M1) ⟹ undefined_lit M2' L›
  ‹defined_lit M1 L ⟹ no_dup (M2' @ M2 @ M1) ⟹ undefined_lit M2 L›
  by (auto simp: defined_lit_map no_dup_def)

lemma no_dup_consistentD:
  ‹no_dup M ⟹ L ∈ lits_of_l M ⟹ -L ∉ lits_of_l M›
  using consistent_interp_def distinct_consistent_interp by blast

lemma no_dup_not_tautology: ‹no_dup M ⟹ ¬tautology (image_mset lit_of (mset M))›
  by (induction M) (auto simp: tautology_add_mset uminus_lit_swap defined_lit_def
      dest: atm_imp_decided_or_proped)

lemma no_dup_distinct: ‹no_dup M ⟹ distinct_mset (image_mset lit_of (mset M))›
  by (induction M) (auto simp: uminus_lit_swap defined_lit_def
      dest: atm_imp_decided_or_proped)

lemma no_dup_not_tautology_uminus: ‹no_dup M ⟹ ¬tautology {#-lit_of L. L ∈# mset M#}›
  by (induction M) (auto simp: tautology_add_mset uminus_lit_swap defined_lit_def
      dest: atm_imp_decided_or_proped)

lemma no_dup_distinct_uminus: ‹no_dup M ⟹ distinct_mset {#-lit_of L. L ∈# mset M#}›
  by (induction M) (auto simp: uminus_lit_swap defined_lit_def
      dest: atm_imp_decided_or_proped)

lemma no_dup_map_lit_of: ‹no_dup M ⟹ distinct (map lit_of M)›
  apply (induction M)
   apply (auto simp: dest: no_dup_imp_distinct)
  by (meson distinct.simps(2) no_dup_cons no_dup_imp_distinct)

lemma no_dup_alt_def:
  ‹no_dup M ⟷ distinct_mset {#atm_of (lit_of x). x ∈# mset M#}›
  by (auto simp: no_dup_def simp flip: distinct_mset_mset_distinct)

lemma no_dup_append_in_atm_notin:
   assumes ‹no_dup (M @ M')› and ‹L ∈ lits_of_l M'›
     shows ‹undefined_lit M L›
  using assms by (auto simp add: atm_lit_of_set_lits_of_l no_dup_def
      defined_lit_map)

lemma no_dup_uminus_append_in_atm_notin:
   assumes ‹no_dup (M @ M')› and ‹-L ∈ lits_of_l M'›
     shows ‹undefined_lit M L›
  using Decided_Propagated_in_iff_in_lits_of_l assms defined_lit_no_dupD(1) by blast


subsection ‹Extending Entailments to multisets›

text ‹We have defined previous entailment with respect to sets, but we also need a multiset version
  depending on the context. The conversion is simple using the function @{term set_mset} (in this
  direction, there is no loss of information).›
abbreviation true_annots_mset (infix "⊨asm" 50) where
‹I ⊨asm C ≡ I ⊨as (set_mset C)›

abbreviation true_clss_clss_m :: ‹'v clause multiset ⇒ 'v clause multiset ⇒ bool› (infix "⊨psm" 50)
  where
‹I ⊨psm C ≡ set_mset I ⊨ps (set_mset C)›

text ‹Analog of theorem @{thm [source] true_clss_clss_subsetE}›
lemma true_clss_clssm_subsetE: ‹N ⊨psm B ⟹ A ⊆# B ⟹ N ⊨psm A›
  using set_mset_mono true_clss_clss_subsetE by blast

abbreviation true_clss_cls_m:: ‹'a clause multiset ⇒ 'a clause ⇒ bool› (infix "⊨pm" 50) where
‹I ⊨pm C ≡ set_mset I ⊨p C›

abbreviation distinct_mset_mset :: ‹'a multiset multiset ⇒ bool› where
‹distinct_mset_mset Σ ≡ distinct_mset_set (set_mset Σ)›

abbreviation all_decomposition_implies_m where
‹all_decomposition_implies_m A B ≡ all_decomposition_implies (set_mset A) B›

abbreviation atms_of_mm :: ‹'a clause multiset ⇒ 'a set› where
‹atms_of_mm U ≡ atms_of_ms (set_mset U)›

text ‹Other definition using @{term ‹Union_mset›}›
lemma atms_of_mm_alt_def: ‹atms_of_mm U = set_mset (∑⇩# (image_mset (image_mset atm_of) U))›
  unfolding atms_of_ms_def by (auto simp: atms_of_def)

abbreviation true_clss_m:: ‹'a partial_interp ⇒ 'a clause multiset ⇒ bool› (infix "⊨sm" 50) where
‹I ⊨sm C ≡ I ⊨s set_mset C›

abbreviation true_clss_ext_m (infix "⊨sextm" 49) where
‹I ⊨sextm C ≡ I ⊨sext set_mset C›

lemma true_clss_cls_cong_set_mset:
  ‹N ⊨pm D ⟹ set_mset D = set_mset D' ⟹ N ⊨pm D'›
  by (auto simp add: true_clss_cls_def true_cls_def atms_of_cong_set_mset[of D D'])


subsection ‹More Lemmas›

lemma no_dup_cannot_not_lit_and_uminus:
  ‹no_dup M ⟹ - lit_of xa = lit_of x ⟹ x ∈ set M ⟹ xa ∉ set M›
  by (metis atm_of_uminus distinct_map inj_on_eq_iff uminus_not_id' no_dup_def)

lemma atms_of_ms_single_atm_of[simp]:
  ‹atms_of_ms {unmark L |L. P L} = atm_of ` {lit_of L |L. P L}›
  unfolding atms_of_ms_def by force

lemma true_cls_mset_restrict:
  ‹{L ∈ I. atm_of L ∈ atms_of_mm N} ⊨m N ⟷ I ⊨m N›
  by (auto simp: true_cls_mset_def true_cls_def
    dest!: multi_member_split)

lemma true_clss_restrict:
  ‹{L ∈ I. atm_of L ∈ atms_of_mm N} ⊨sm N ⟷ I ⊨sm N›
  by (auto simp: true_clss_def true_cls_def
    dest!: multi_member_split)

lemma total_over_m_atms_incl:
  assumes ‹total_over_m M (set_mset N)›
  shows
    ‹x ∈ atms_of_mm N ⟹ x ∈ atms_of_s M›
  by (meson assms contra_subsetD total_over_m_alt_def)

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


subsection ‹Negation of annotated clauses›

definition negate_ann_lits :: ‹('v literal, 'v literal, 'mark) annotated_lits ⇒ 'v literal multiset› where
  ‹negate_ann_lits M = (λL. - lit_of L) `# mset M›

lemma negate_ann_lits_empty[simp]: ‹negate_ann_lits [] = {#}›
  by (auto simp: negate_ann_lits_def)

lemma entails_CNot_negate_ann_lits:
  ‹M ⊨as CNot D ⟷ set_mset D ⊆ set_mset (negate_ann_lits M)›
  by (auto simp: true_annots_true_cls_def_iff_negation_in_model
      negate_ann_lits_def lits_of_def uminus_lit_swap
    dest!: multi_member_split)

text ‹Pointwise negation of a clause:›
definition pNeg :: ‹'v clause ⇒ 'v clause› where
  ‹pNeg C = {#-D. D ∈# C#}›

lemma pNeg_simps:
  ‹pNeg (add_mset A C) = add_mset (-A) (pNeg C)›
  ‹pNeg (C + D) = pNeg C + pNeg D›
  by (auto simp: pNeg_def)

lemma atms_of_pNeg[simp]: ‹atms_of (pNeg C) = atms_of C›
  by (auto simp: pNeg_def atms_of_def image_image)

lemma negate_ann_lits_pNeg_lit_of: ‹negate_ann_lits = pNeg o image_mset lit_of o mset›
  by (intro ext) (auto simp: negate_ann_lits_def pNeg_def)

lemma negate_ann_lits_empty_iff: ‹negate_ann_lits M ≠ {#} ⟷ M ≠ []›
  by (auto simp: negate_ann_lits_def)

lemma atms_of_negate_ann_lits[simp]: ‹atms_of (negate_ann_lits M) = atm_of ` (lits_of_l M)›
  unfolding negate_ann_lits_def lits_of_def atms_of_def by (auto simp: image_image)

lemma tautology_pNeg[simp]:
  ‹tautology (pNeg C) ⟷ tautology C›
  by (auto 5 5 simp: tautology_decomp pNeg_def
      uminus_lit_swap add_mset_eq_add_mset eq_commute[of ‹Neg _› ‹- _›] eq_commute[of ‹Pos _› ‹- _›]
    dest!: multi_member_split)

lemma pNeg_convolution[simp]:
  ‹pNeg (pNeg C) = C›
  by (auto simp: pNeg_def)

lemma pNeg_minus[simp]: ‹pNeg (A - B) = pNeg A - pNeg B›
  unfolding pNeg_def
  by (subst image_mset_minus_inj_on) (auto simp: inj_on_def)

lemma pNeg_empty[simp]: ‹pNeg {#} = {#}›
  unfolding pNeg_def
  by (auto simp: inj_on_def)

lemma pNeg_replicate_mset[simp]: ‹pNeg (replicate_mset n L) = replicate_mset n (-L)›
  unfolding pNeg_def by auto

lemma distinct_mset_pNeg_iff[iff]: ‹distinct_mset (pNeg x) ⟷ distinct_mset x›
  unfolding pNeg_def
  by (rule distinct_image_mset_inj) (auto simp: inj_on_def)

lemma pNeg_simple_clss_iff[simp]:
  ‹pNeg M ∈ simple_clss N ⟷ M ∈ simple_clss N›
  by (auto simp: simple_clss_def)

lemma atms_of_ms_pNeg[simp]: ‹atms_of_ms (pNeg ` N) = atms_of_ms N›
  unfolding atms_of_ms_def pNeg_def by (auto simp: image_image atms_of_def)

definition DECO_clause :: ‹('v, 'a) ann_lits ⇒ 'v clause› where
  ‹DECO_clause M = (uminus o lit_of) `# (filter_mset is_decided (mset M))›

lemma
  DECO_clause_cons_Decide[simp]:
    ‹DECO_clause (Decided L # M) = add_mset (-L) (DECO_clause M)› and
  DECO_clause_cons_Proped[simp]:
    ‹DECO_clause (Propagated L C # M) = DECO_clause M›
  by (auto simp: DECO_clause_def)


lemma no_dup_distinct_mset[intro!]:
  assumes n_d: ‹no_dup M›
  shows ‹distinct_mset (negate_ann_lits M)›
  unfolding negate_ann_lits_def no_dup_def
proof (subst distinct_image_mset_inj)
  show ‹inj_on (λL. - lit_of L) (set_mset (mset M))›
    unfolding inj_on_def Ball_def
  proof (intro allI impI, rule ccontr)
    fix L L'
    assume
      L: ‹L ∈# mset M› and
      L': ‹L' ∈# mset M› and
      lit: ‹- lit_of L = - lit_of L'› and
      LL': ‹L ≠ L'›
    have ‹atm_of (lit_of L) = atm_of (lit_of L')›
      using lit by auto
    moreover have ‹atm_of (lit_of L) ∈# (λl. atm_of (lit_of l)) `# mset M›
      using L by auto
    moreover have ‹atm_of (lit_of L') ∈# (λl. atm_of (lit_of l)) `# mset M›
      using L' by auto
    ultimately show False
      using assms LL' L L' unfolding distinct_mset_mset_distinct[symmetric] mset_map no_dup_def
      apply - apply (rule distinct_image_mset_not_equal[of L L' ‹(λl. atm_of (lit_of l))›])
      by auto
  qed
next
  show ‹distinct_mset (mset M)›
    using no_dup_imp_distinct[OF n_d] by simp
qed

lemma in_negate_trial_iff: ‹L ∈# negate_ann_lits M ⟷ - L ∈ lits_of_l M›
  unfolding negate_ann_lits_def lits_of_def by (auto simp: uminus_lit_swap)

lemma negate_ann_lits_cons[simp]:
  ‹negate_ann_lits (L # M) = add_mset (- lit_of L) (negate_ann_lits M)›
  by (auto simp: negate_ann_lits_def)

lemma uminus_simple_clss_iff[simp]:
  ‹uminus `# M ∈ simple_clss N ⟷  M ∈ simple_clss N›
 by (metis pNeg_simple_clss_iff pNeg_def)

lemma pNeg_mono: ‹C ⊆# C' ⟹ pNeg C ⊆# pNeg C'›
  by (auto simp: image_mset_subseteq_mono pNeg_def)

end