Theory Prop_Resolution

theory Prop_Resolution
imports Entailment_Definition.Partial_Herbrand_Interpretation
  Weidenbach_Book_Base.WB_List_More
  Weidenbach_Book_Base.Wellfounded_More

begin
chapter ‹Resolution-based techniques›

text ‹This chapter contains the formalisation of resolution and superposition.›


section ‹Resolution›

subsection ‹Simplification Rules›

inductive simplify :: "'v clause_set ⇒ 'v clause_set ⇒ bool" for N :: "'v clause set" where
tautology_deletion:
  "add_mset (Pos P) (add_mset (Neg P) A) ∈ N ⟹ simplify N (N - {add_mset (Pos P) (add_mset (Neg P) A)})"|
condensation:
  "add_mset L (add_mset L A) ∈ N ⟹ simplify N (N - {add_mset L (add_mset L A)} ∪ {add_mset L A})" |
subsumption:
  "A ∈ N ⟹ A ⊂# B ⟹ B ∈ N ⟹ simplify N (N - {B})"

lemma simplify_preserve_models':
  fixes N N' :: "'v clause_set"
  assumes "simplify N N'"
  and "total_over_m I N"
  shows "I ⊨s N' ⟶ I ⊨s N"
  using assms
proof (induct rule: simplify.induct)
  case (tautology_deletion P A)
  then have "I ⊨ add_mset (Pos P) (add_mset (Neg P) A)"
    by (fastforce dest: mk_disjoint_insert)
  then show ?case by (metis Un_Diff_cancel2 true_clss_singleton true_clss_union)
next
  case (condensation A P)
  then show ?case
    by (fastforce dest: mk_disjoint_insert)
next
  case (subsumption A B)
  have "A ≠ B" using subsumption.hyps(2) by auto
  then have "I ⊨s N - {B} ⟹ I ⊨ A" using ‹A ∈ N› by (simp add: true_clss_def)
  moreover have "I ⊨ A ⟹ I ⊨ B" using ‹A <# B› by auto
  ultimately show ?case by (metis insert_Diff_single true_clss_insert)
qed

lemma simplify_preserve_models:
  fixes N N' :: "'v clause_set"
  assumes "simplify N N'"
  and "total_over_m I N"
  shows "I ⊨s N ⟶ I ⊨s N'"
  using assms apply (induct rule: simplify.induct)
  using true_clss_def by fastforce+

lemma simplify_preserve_models'':
  fixes N N' :: "'v clause_set"
  assumes "simplify N N'"
  and "total_over_m I N'"
  shows "I ⊨s N ⟶ I ⊨s N'"
  using assms apply (induct rule: simplify.induct)
  using true_clss_def by fastforce+

lemma simplify_preserve_models_eq:
  fixes N N' :: "'v clause_set"
  assumes "simplify N N'"
  and "total_over_m I N"
  shows "I ⊨s N ⟷ I ⊨s N'"
  using simplify_preserve_models simplify_preserve_models' assms by blast

lemma simplify_preserves_finite:
 assumes "simplify ψ ψ'"
 shows "finite ψ ⟷ finite ψ'"
 using assms by (induct rule: simplify.induct, auto simp add: remove_def)

lemma rtranclp_simplify_preserves_finite:
 assumes "rtranclp simplify ψ ψ'"
 shows "finite ψ ⟷ finite ψ'"
 using assms by (induct rule: rtranclp_induct) (auto simp add: simplify_preserves_finite)

lemma simplify_atms_of_ms:
  assumes "simplify ψ ψ'"
  shows "atms_of_ms ψ' ⊆ atms_of_ms ψ"
  using assms unfolding atms_of_ms_def
proof (induct rule: simplify.induct)
  case (tautology_deletion A P)
  then show ?case by auto
next
  case (condensation P A)
  moreover have "A + {#P#} + {#P#} ∈ ψ ⟹ ∃x∈ψ. atm_of P ∈ atm_of ` set_mset x"
    by (metis Un_iff atms_of_def atms_of_plus atms_of_singleton insert_iff)
  ultimately show ?case by (auto simp add: atms_of_def)
next
  case (subsumption A P)
  then show ?case by auto
qed

lemma rtranclp_simplify_atms_of_ms:
  assumes "rtranclp simplify ψ ψ'"
  shows "atms_of_ms ψ' ⊆ atms_of_ms ψ"
  using assms apply (induct rule: rtranclp_induct)
   apply (fastforce intro: simplify_atms_of_ms)
  using simplify_atms_of_ms by blast

lemma factoring_imp_simplify:
  assumes "{#L, L#} + C ∈ N"
  shows "∃N'. simplify N N'"
proof -
  have "add_mset L (add_mset L C) ∈ N" using assms by (simp add: add.commute union_lcomm)
  from condensation[OF this] show ?thesis by blast
qed


subsection ‹Unconstrained Resolution›

type_synonym 'v uncon_state = "'v clause_set"

inductive uncon_res :: "'v uncon_state ⇒ 'v uncon_state ⇒ bool" where
resolution:
  "{#Pos p#} + C ∈ N ⟹ {#Neg p#} + D ∈ N ⟹ (add_mset (Pos p) C, add_mset (Neg P) D) ∉ already_used
    ⟹ uncon_res N (N ∪ {C + D})" |
factoring: "{#L#} + {#L#} + C ∈ N ⟹ uncon_res N (insert (add_mset L C) N)"

lemma uncon_res_increasing:
  assumes "uncon_res S S'" and "ψ ∈ S"
  shows "ψ ∈ S'"
  using assms by (induct rule: uncon_res.induct) auto

lemma rtranclp_uncon_inference_increasing:
  assumes "rtranclp uncon_res S S'" and "ψ ∈ S"
  shows "ψ ∈ S'"
  using assms by (induct rule: rtranclp_induct) (auto simp add: uncon_res_increasing)


subsubsection ‹Subsumption›

definition subsumes :: "'a literal multiset ⇒ 'a literal multiset ⇒ bool" where
"subsumes χ χ' ⟷
  (∀I. total_over_m I {χ'} ⟶ total_over_m I {χ})
  ∧ (∀I. total_over_m I {χ} ⟶ I ⊨ χ ⟶ I ⊨ χ')"

lemma subsumes_refl[simp]:
  "subsumes χ χ"
  unfolding subsumes_def by auto


lemma subsumes_subsumption:
  assumes "subsumes D χ"
  and "C ⊂# D" and "¬tautology χ"
  shows "subsumes C χ" unfolding subsumes_def
  using assms subsumption_total_over_m subsumption_chained unfolding subsumes_def
  by (blast intro!: subset_mset.less_imp_le)

lemma subsumes_tautology:
  assumes "subsumes (add_mset (Pos P) (add_mset (Neg P) C)) χ"
  shows "tautology χ"
  using assms unfolding subsumes_def by (auto simp add: tautology_def)


subsection ‹Inference Rule›

type_synonym 'v state = "'v clause_set × ('v clause × 'v clause) set"

inductive inference_clause :: "'v state ⇒ 'v clause × ('v clause × 'v clause) set ⇒ bool"
  (infix "⇒⇩\<Res>" 100) where
resolution:
  "{#Pos p#} + C ∈ N ⟹ {#Neg p#} + D ∈ N ⟹ ({#Pos p#} + C, {#Neg p#} + D) ∉ already_used
  ⟹ inference_clause (N, already_used) (C + D, already_used ∪ {({#Pos p#} + C, {#Neg p#} + D)})" |
factoring: "{#L, L#} + C ∈ N ⟹ inference_clause (N, already_used) (C + {#L#}, already_used)"

inductive inference :: "'v state ⇒ 'v state ⇒ bool" where
inference_step: "inference_clause S (clause, already_used)
  ⟹ inference S (fst S ∪ {clause}, already_used)"


abbreviation already_used_inv
  :: "'a literal multiset set × ('a literal multiset × 'a literal multiset) set ⇒ bool" where
"already_used_inv state ≡
  (∀(A, B) ∈ snd state. ∃p. Pos p ∈# A ∧ Neg p ∈# B ∧
          ((∃χ ∈ fst state. subsumes χ ((A - {#Pos p#}) + (B - {#Neg p#})))
            ∨ tautology ((A - {#Pos p#}) + (B - {#Neg p#}))))"

lemma inference_clause_preserves_already_used_inv:
  assumes "inference_clause S S'"
  and "already_used_inv S"
  shows "already_used_inv (fst S ∪ {fst S'}, snd S')"
  using assms apply (induct rule: inference_clause.induct)
  by fastforce+

lemma inference_preserves_already_used_inv:
  assumes "inference S S'"
  and "already_used_inv S"
  shows "already_used_inv S'"
  using assms
proof (induct rule: inference.induct)
  case (inference_step S clause already_used)
  then show ?case
    using inference_clause_preserves_already_used_inv[of S "(clause, already_used)"] by simp
qed

lemma rtranclp_inference_preserves_already_used_inv:
  assumes "rtranclp inference S S'"
  and "already_used_inv S"
  shows "already_used_inv S'"
  using assms apply (induct rule: rtranclp_induct, simp)
  using inference_preserves_already_used_inv unfolding tautology_def by fast

lemma subsumes_condensation:
  assumes "subsumes (C + {#L#} + {#L#}) D"
  shows "subsumes (C + {#L#}) D"
  using assms unfolding subsumes_def by simp

lemma simplify_preserves_already_used_inv:
  assumes "simplify N N'"
  and "already_used_inv (N, already_used)"
  shows "already_used_inv (N', already_used)"
  using assms
proof (induct rule: simplify.induct)
  case (condensation C L)
  then show ?case
    using subsumes_condensation by simp fast
next
  {
     fix a:: 'a and A :: "'a set" and P
     have "(∃x ∈ Set.remove a A. P x) ⟷ (∃x ∈ A. x ≠ a ∧ P x)" by auto
  } note ex_member_remove = this
  {
    fix a a0 :: "'v clause" and A :: "'v clause_set" and y
    assume "a ∈ A" and "a0 ⊂# a"
    then have "(∃x ∈ A. subsumes x y) ⟷ (subsumes a y ∨ (∃x ∈ A. x ≠ a ∧ subsumes x y))"
      by auto
  } note tt2 = this
  case (subsumption A B) note A = this(1) and AB = this(2) and B = this(3) and inv = this(4)
  show ?case
    proof (standard, standard)
      fix x a b
      assume x: "x ∈ snd (N - {B}, already_used)" and [simp]: "x = (a, b)"
      obtain p where p: "Pos p ∈# a ∧ Neg p ∈# b" and
        q: "(∃χ∈N. subsumes χ (a - {#Pos p#} + (b - {#Neg p#})))
          ∨ tautology (a - {#Pos p#} + (b - {#Neg p#}))"
        using inv x by fastforce
      consider (taut) "tautology (a - {#Pos p#} + (b - {#Neg p#}))" |
        (χ) χ where "χ ∈ N" "subsumes χ (a - {#Pos p#} + (b - {#Neg p#}))"
          "¬tautology (a - {#Pos p#} + (b - {#Neg p#}))"
        using q by auto
      then show
        "∃p. Pos p ∈# a ∧ Neg p ∈# b
             ∧ ((∃χ∈fst (N - {B}, already_used). subsumes χ (a - {#Pos p#} + (b - {#Neg p#})))
                 ∨ tautology (a - {#Pos p#} + (b - {#Neg p#})))"
        proof cases
          case taut
          then show ?thesis using p by auto
        next
          case χ note H = this
          show ?thesis using p A AB B subsumes_subsumption[OF _ AB H(3)] H(1,2) by fastforce
        qed
    qed
next
  case (tautology_deletion P C)
  then show ?case
  proof clarify
    fix a b
    assume "add_mset (Pos P) (add_mset (Neg P) C) ∈ N"
    assume "already_used_inv (N, already_used)"
    and "(a, b) ∈ snd (N - {add_mset (Pos P) (add_mset (Neg P) C)}, already_used)"
    then obtain p where
      "Pos p ∈# a ∧ Neg p ∈# b ∧
        ((∃χ∈fst (N ∪ {add_mset (Pos P) (add_mset (Neg P) C)}, already_used).
              subsumes χ (a - {#Pos p#} + (b - {#Neg p#})))
          ∨ tautology (a - {#Pos p#} + (b - {#Neg p#})))"
      by fastforce
    moreover have "tautology (add_mset (Pos P) (add_mset (Neg P) C))" by auto
    ultimately show
      "∃p. Pos p ∈# a ∧ Neg p ∈# b ∧
      ((∃χ∈fst (N - {add_mset (Pos P) (add_mset (Neg P) C)}, already_used).
        subsumes χ (remove1_mset (Pos p) a + remove1_mset (Neg p) b)) ∨
        tautology (remove1_mset (Pos p) a + remove1_mset (Neg p) b))"
      by (metis (no_types) Diff_iff Un_insert_right empty_iff fst_conv insertE subsumes_tautology
        sup_bot.right_neutral)
  qed
qed


lemma
  factoring_satisfiable: "I ⊨ add_mset L (add_mset L C) ⟷ I ⊨ add_mset L C" and
  resolution_satisfiable:
    "consistent_interp I ⟹ I ⊨ add_mset (Pos p) C ⟹ I ⊨ add_mset (Neg p) D ⟹ I ⊨ C + D" and
    factoring_same_vars: "atms_of (add_mset L (add_mset L C)) = atms_of (add_mset L C)"
  unfolding true_cls_def consistent_interp_def by (fastforce split: if_split_asm)+

lemma inference_increasing:
  assumes "inference S S'" and "ψ ∈ fst S"
  shows "ψ ∈ fst S'"
  using assms by (induct rule: inference.induct, auto)

lemma rtranclp_inference_increasing:
  assumes "rtranclp inference S S'" and "ψ ∈ fst S"
  shows "ψ ∈ fst S'"
  using assms by (induct rule: rtranclp_induct, auto simp add: inference_increasing)

lemma inference_clause_already_used_increasing:
  assumes "inference_clause S S'"
  shows "snd S ⊆ snd S'"
  using assms by (induct rule:inference_clause.induct, auto)


lemma inference_already_used_increasing:
  assumes "inference S S'"
  shows "snd S ⊆ snd S'"
  using assms apply (induct rule:inference.induct)
  using inference_clause_already_used_increasing by fastforce

lemma inference_clause_preserve_models:
  fixes N N' :: "'v clause_set"
  assumes "inference_clause T T'"
  and "total_over_m I (fst T)"
  and consistent: "consistent_interp I"
  shows "I ⊨s fst T ⟷ I ⊨s fst T ∪ {fst T'}"
  using assms apply (induct rule: inference_clause.induct)
  unfolding consistent_interp_def true_clss_def by auto force+


lemma inference_preserve_models:
  fixes N N' :: "'v clause_set"
  assumes "inference T T'"
  and "total_over_m I (fst T)"
  and consistent: "consistent_interp I"
  shows "I ⊨s fst T ⟷ I ⊨s fst T'"
  using assms apply (induct rule: inference.induct)
  using inference_clause_preserve_models by fastforce

lemma inference_clause_preserves_atms_of_ms:
  assumes "inference_clause S S'"
  shows "atms_of_ms (fst (fst S ∪ {fst S'}, snd S')) ⊆ atms_of_ms (fst S)"
  using assms by (induct rule: inference_clause.induct) (auto dest!: atms_of_atms_of_ms_mono)

lemma inference_preserves_atms_of_ms:
  fixes N N' :: "'v clause_set"
  assumes "inference T T'"
  shows "atms_of_ms (fst T') ⊆ atms_of_ms (fst T)"
  using assms apply (induct rule: inference.induct)
  using inference_clause_preserves_atms_of_ms by fastforce

lemma inference_preserves_total:
  fixes N N' :: "'v clause_set"
  assumes "inference (N, already_used) (N', already_used')"
  shows "total_over_m I N ⟹ total_over_m I N'"
    using assms inference_preserves_atms_of_ms unfolding total_over_m_def total_over_set_def
    by fastforce


lemma rtranclp_inference_preserves_total:
  assumes "rtranclp inference T T'"
  shows "total_over_m I (fst T) ⟹ total_over_m I (fst T')"
  using assms by (induct rule: rtranclp_induct, auto simp add: inference_preserves_total)

lemma rtranclp_inference_preserve_models:
  assumes "rtranclp inference N N'"
  and "total_over_m I (fst N)"
  and consistent: "consistent_interp I"
  shows "I ⊨s fst N ⟷ I ⊨s fst N'"
  using assms apply (induct rule: rtranclp_induct)
  apply (simp add: inference_preserve_models)
  using inference_preserve_models rtranclp_inference_preserves_total by blast

lemma inference_preserves_finite:
  assumes "inference ψ ψ'" and "finite (fst ψ)"
  shows "finite (fst ψ')"
  using assms by (induct rule: inference.induct, auto simp add: simplify_preserves_finite)


lemma inference_clause_preserves_finite_snd:
  assumes "inference_clause ψ ψ'" and "finite (snd ψ)"
  shows "finite (snd ψ')"
  using assms by (induct rule: inference_clause.induct, auto)


lemma inference_preserves_finite_snd:
  assumes "inference ψ ψ'" and "finite (snd ψ)"
  shows "finite (snd ψ')"
  using assms inference_clause_preserves_finite_snd by (induct rule: inference.induct, fastforce)


lemma rtranclp_inference_preserves_finite:
  assumes "rtranclp inference ψ ψ'" and "finite (fst ψ)"
  shows "finite (fst ψ')"
  using assms by (induct rule: rtranclp_induct)
    (auto simp add: simplify_preserves_finite inference_preserves_finite)

lemma consistent_interp_insert:
  assumes "consistent_interp I"
  and "atm_of P ∉ atm_of ` I"
  shows "consistent_interp (insert P I)"
proof -
  have P: "insert P I = I ∪ {P}" by auto
  show ?thesis unfolding P
  apply (rule consistent_interp_disjoint)
  using assms by (auto simp: image_iff)
qed

lemma simplify_clause_preserves_sat:
  assumes simp: "simplify ψ ψ'"
  and "satisfiable ψ'"
  shows "satisfiable ψ"
  using assms
proof induction
  case (tautology_deletion P A) note AP = this(1) and sat = this(2)
  let ?A' = "add_mset (Pos P) (add_mset (Neg P) A)"
  let ?ψ' = "ψ - {?A'}"
  obtain I where
    I: "I ⊨s ?ψ'" and
    cons: "consistent_interp I" and
    tot: "total_over_m I ?ψ'"
    using sat unfolding satisfiable_def by auto
  { assume "Pos P ∈ I ∨ Neg P ∈ I"
    then have "I ⊨ ?A'" by auto
    then have "I ⊨s ψ" using I by (metis insert_Diff tautology_deletion.hyps true_clss_insert)
    then have "?case" using cons tot by auto
  }
  moreover {
    assume Pos: "Pos P ∉ I" and Neg: "Neg P ∉ I"
    then have "consistent_interp (I ∪ {Pos P})" using cons by simp
    moreover have I'A: "I ∪ {Pos P} ⊨ ?A'" by auto
    have "{Pos P} ∪ I ⊨s ψ - {?A'}"
      using ‹I ⊨s ψ - {?A'}› true_clss_union_increase' by blast
    then have "I ∪ {Pos P} ⊨s ψ"
      by (metis (no_types) Un_empty_right Un_insert_left Un_insert_right I'A insert_Diff
        sup_bot.left_neutral tautology_deletion.hyps true_clss_insert)
    ultimately have ?case using satisfiable_carac' by blast
  }
  ultimately show ?case by blast
next
  case (condensation L A) note AL = this(1) and sat = this(2)
  let ?A' = "add_mset L A"
  let ?A = "add_mset L (add_mset L A)"
  have f3: "simplify ψ (ψ - {?A} ∪ {?A'})"
    using AL simplify.condensation by blast
  obtain LL :: "'a literal set" where
    f4: "LL ⊨s ψ - {?A} ∪ {?A'}
      ∧ consistent_interp LL
      ∧ total_over_m LL (ψ - {?A} ∪ {?A'})"
    using sat by (meson satisfiable_def)
  have f5: "insert (A + {#L#} + {#L#}) (ψ - {A + {#L#} + {#L#}}) = ψ"
    using AL by fastforce
  have "atms_of (?A') = atms_of (?A)"
    by simp
  then show ?case
    using f5 f4 f3 by (metis Un_insert_right add_mset_add_single atms_of_ms_insert satisfiable_carac
        simplify_preserve_models' sup_bot.right_neutral total_over_m_def)
next
  case (subsumption A B) note A = this(1) and AB = this(2) and B = this(3) and sat = this(4)
  let ?ψ' = "ψ - {B}"
  obtain I where I: "I ⊨s ?ψ'" and cons: "consistent_interp I" and tot: "total_over_m I ?ψ'"
    using sat unfolding satisfiable_def by auto
  have "I ⊨ A" using A I by (metis AB Diff_iff subset_mset.less_irrefl singletonD true_clss_def)
  then have "I ⊨ B" using AB subset_mset.less_imp_le true_cls_mono_leD by blast
  then have "I ⊨s ψ" using I by (metis insert_Diff_single true_clss_insert)
  then show ?case using cons satisfiable_carac' by blast
qed

lemma simplify_preserves_unsat:
  assumes "inference ψ ψ'"
  shows "satisfiable (fst ψ') ⟶ satisfiable (fst ψ)"
  using assms apply (induct rule: inference.induct)
  using satisfiable_decreasing by (metis fst_conv)+

lemma inference_preserves_unsat:
  assumes "inference⇧*⇧* S S'"
  shows "satisfiable (fst S') ⟶  satisfiable (fst S)"
  using assms apply (induct rule: rtranclp_induct)
  apply simp_all
  using simplify_preserves_unsat by blast

datatype 'v sem_tree = Node "'v" "'v sem_tree" "'v sem_tree" | Leaf

fun sem_tree_size :: "'v sem_tree ⇒ nat" where
"sem_tree_size Leaf = 0" |
"sem_tree_size (Node _ ag ad) = 1 + sem_tree_size ag + sem_tree_size ad"

lemma sem_tree_size[case_names bigger]:
  "(⋀xs:: 'v sem_tree. (⋀ys:: 'v sem_tree. sem_tree_size ys < sem_tree_size xs ⟹ P ys) ⟹ P xs)
  ⟹ P xs"
  by (fact Nat.measure_induct_rule)


fun partial_interps :: "'v sem_tree ⇒ 'v partial_interp ⇒ 'v clause_set ⇒ bool" where
"partial_interps Leaf I ψ = (∃χ. ¬ I ⊨ χ ∧ χ ∈ ψ ∧ total_over_m I {χ})" |
"partial_interps (Node v ag ad) I ψ ⟷
  (partial_interps ag (I ∪ {Pos v}) ψ ∧ partial_interps ad (I∪ {Neg v}) ψ)"


lemma simplify_preserve_partial_leaf:
  "simplify N N' ⟹ partial_interps Leaf I N ⟹ partial_interps Leaf I N'"
  apply (induct rule: simplify.induct)
    using union_lcomm apply auto[1]
   apply (simp)
   apply (metis atms_of_remdups_mset remdups_mset_singleton_sum true_cls_add_mset union_single_eq_member)
  apply auto
  by (metis atms_of_ms_emtpy_set subsumption_total_over_m total_over_m_def total_over_m_insert
      total_over_set_empty true_cls_mono_leD)

lemma simplify_preserve_partial_tree:
  assumes "simplify N N'"
  and "partial_interps t I N"
  shows "partial_interps t I N'"
  using assms apply (induct t arbitrary: I, simp)
  using simplify_preserve_partial_leaf by metis


lemma inference_preserve_partial_tree:
  assumes "inference S S'"
  and "partial_interps t I (fst S)"
  shows "partial_interps t I (fst S')"
  using assms apply (induct t arbitrary: I, simp_all)
  by (meson inference_increasing)


lemma rtranclp_inference_preserve_partial_tree:
  assumes "rtranclp inference N N'"
  and "partial_interps t I (fst N)"
  shows "partial_interps t I (fst N')"
  using assms apply (induct rule: rtranclp_induct, auto)
  using inference_preserve_partial_tree by force


function build_sem_tree :: "'v :: linorder set ⇒ 'v clause_set ⇒ 'v sem_tree" where
"build_sem_tree atms ψ =
  (if atms = {} ∨ ¬ finite atms
  then Leaf
  else Node (Min atms) (build_sem_tree (Set.remove (Min atms) atms) ψ)
     (build_sem_tree (Set.remove (Min atms) atms) ψ))"
by auto
termination
  apply (relation "measure (λ(A, _).  card A)", simp_all)
  apply (metis Min_in card_Diff1_less remove_def)+
done
declare build_sem_tree.induct[case_names tree]

lemma unsatisfiable_empty[simp]:
  "¬unsatisfiable {}"
   unfolding satisfiable_def apply auto
  using consistent_interp_def unfolding total_over_m_def total_over_set_def atms_of_ms_def by blast

lemma partial_interps_build_sem_tree_atms_general:
  fixes ψ :: "'v :: linorder clause_set" and p :: "'v literal list"
  assumes unsat: "unsatisfiable ψ" and "finite ψ" and "consistent_interp I"
  and "finite atms"
  and "atms_of_ms ψ = atms ∪ atms_of_s I" and "atms ∩ atms_of_s I = {}"
  shows "partial_interps (build_sem_tree atms ψ) I ψ"
  using assms
proof (induct arbitrary: I rule: build_sem_tree.induct)
  case (1 atms ψ Ia) note IH1 = this(1) and IH2 = this(2) and unsat = this(3) and finite = this(4)
    and cons = this(5)  and f = this(6) and un = this(7) and disj = this(8)
  {
    assume atms: "atms = {}"
    then have atmsIa: "atms_of_ms ψ = atms_of_s Ia" using un by auto
    then have "total_over_m Ia ψ" unfolding total_over_m_def atmsIa by auto
    then have χ: "∃χ ∈ ψ. ¬ Ia ⊨ χ"
      using unsat cons unfolding true_clss_def satisfiable_def by auto
    then have "build_sem_tree atms ψ = Leaf" using atms by auto
    moreover
      have tot: "⋀χ. χ ∈ ψ ⟹ total_over_m Ia {χ}"
      unfolding total_over_m_def total_over_set_def atms_of_ms_def atms_of_s_def
      using atmsIa atms_of_ms_def by fastforce
    have "partial_interps Leaf Ia ψ"
      using χ tot by (auto simp add: total_over_m_def total_over_set_def atms_of_ms_def)

      ultimately have ?case by metis
  }
  moreover {
    assume atms: "atms ≠ {}"
    have "build_sem_tree atms ψ = Node (Min atms) (build_sem_tree (Set.remove (Min atms) atms) ψ)
       (build_sem_tree (Set.remove (Min atms) atms) ψ)"
      using build_sem_tree.simps[of "atms" ψ] f atms by metis

    have "consistent_interp (Ia ∪ {Pos (Min atms)})" unfolding consistent_interp_def
      by (metis Int_iff Min_in Un_iff atm_of_uminus atms cons consistent_interp_def disj empty_iff
        f in_atms_of_s_decomp insert_iff literal.distinct(1) literal.exhaust_sel literal.sel(2)
        uminus_Neg uminus_Pos)
    moreover have "atms_of_ms ψ = Set.remove (Min atms) atms ∪ atms_of_s (Ia ∪ {Pos (Min atms)})"
      using Min_in atms f un by fastforce
    moreover have disj': "Set.remove (Min atms) atms ∩ atms_of_s (Ia ∪ {Pos (Min atms)}) = {}"
      by simp (metis disj disjoint_iff_not_equal member_remove)
    moreover have "finite (Set.remove (Min atms) atms)" using f by (simp add: remove_def)
    ultimately have subtree1: "partial_interps (build_sem_tree (Set.remove (Min atms) atms) ψ)
        (Ia ∪ {Pos (Min atms)}) ψ"
      using IH1[of "Ia ∪ {Pos (Min (atms))}"] atms f unsat finite by metis

    have "consistent_interp (Ia ∪ {Neg (Min atms)})" unfolding consistent_interp_def
      by (metis Int_iff Min_in Un_iff atm_of_uminus atms cons consistent_interp_def disj empty_iff
        f in_atms_of_s_decomp insert_iff literal.distinct(1) literal.exhaust_sel literal.sel(2)
        uminus_Neg)
    moreover have "atms_of_ms ψ = Set.remove (Min atms) atms ∪ atms_of_s (Ia ∪ {Neg (Min atms)})"
      using ‹atms_of_ms ψ = Set.remove (Min atms) atms ∪ atms_of_s (Ia ∪ {Pos (Min atms)})› by blast

    moreover have disj': "Set.remove (Min atms) atms ∩ atms_of_s (Ia ∪ {Neg (Min atms)}) = {}"
      using disj by auto
    moreover have "finite (Set.remove (Min atms) atms)" using f by (simp add: remove_def)
    ultimately have subtree2: "partial_interps (build_sem_tree (Set.remove (Min atms) atms) ψ)
        (Ia ∪ {Neg (Min atms)}) ψ"
      using IH2[of "Ia ∪ {Neg (Min (atms))}"]  atms f unsat finite by metis

    then have ?case
      using IH1 subtree1 subtree2 f local.finite unsat atms by simp
  }
  ultimately show ?case by metis
qed


lemma partial_interps_build_sem_tree_atms:
  fixes ψ :: "'v :: linorder clause_set" and p :: "'v literal list"
  assumes unsat: "unsatisfiable ψ" and finite: "finite ψ"
  shows "partial_interps (build_sem_tree (atms_of_ms ψ) ψ) {} ψ"
proof -
  have "consistent_interp {}" unfolding consistent_interp_def by auto
  moreover have "atms_of_ms ψ = atms_of_ms ψ ∪ atms_of_s {}" unfolding atms_of_s_def by auto
  moreover have "atms_of_ms ψ ∩ atms_of_s {} = {} " unfolding atms_of_s_def by auto
  moreover have "finite (atms_of_ms ψ)" unfolding atms_of_ms_def using finite by simp
  ultimately show "partial_interps (build_sem_tree (atms_of_ms ψ) ψ) {} ψ"
    using partial_interps_build_sem_tree_atms_general[of "ψ" "{}" "atms_of_ms ψ"] assms by metis
qed

lemma can_decrease_count:
  fixes ψ'' :: "'v clause_set × ('v clause × 'v clause × 'v) set"
  assumes "count χ L = n"
  and "L ∈# χ" and "χ ∈ fst ψ"
  shows "∃ψ' χ'. inference⇧*⇧* ψ ψ' ∧ χ' ∈ fst ψ' ∧ (∀L. L ∈# χ ⟷ L ∈# χ')
                 ∧ count χ' L = 1
                 ∧ (∀φ. φ ∈ fst ψ ⟶ φ ∈ fst ψ')
                 ∧ (I ⊨ χ ⟷ I ⊨ χ')
                 ∧ (∀I'. total_over_m I' {χ} ⟶ total_over_m I' {χ'})"
  using assms
proof (induct n arbitrary: χ ψ)
  case 0
  then show ?case by (simp add: not_in_iff[symmetric])
next
   case (Suc n χ)
   note IH = this(1) and count = this(2) and L = this(3) and χ = this(4)
   {
     assume "n = 0"
     then have "inference⇧*⇧* ψ ψ"
     and "χ ∈ fst ψ"
     and "∀L. (L ∈# χ) ⟷ (L ∈# χ)"
     and "count χ L = (1::nat)"
     and "∀φ. φ ∈ fst ψ ⟶ φ ∈ fst ψ"
       by (auto simp add: count L χ)
     then have ?case by metis
   }
   moreover {
     assume "n > 0"
     then have "∃C. χ = C + {#L, L#}"
       by (metis Suc_inject union_mset_add_mset_right add_mset_add_single count_add_mset count_inI
           less_not_refl3 local.count mset_add zero_less_Suc)
     then obtain C where C: "χ = C + {#L, L#}" by metis
     let ?χ' = "C +{#L#}"
     let ?ψ' = "(fst ψ ∪ {?χ'}, snd ψ)"
     have φ: "∀φ ∈ fst ψ. (φ ∈ fst ψ ∨ φ ≠ ?χ') ⟷ φ ∈ fst ?ψ'" unfolding C by auto
     have inf: "inference ψ ?ψ'"
       using C factoring χ prod.collapse union_commute inference_step
       by (metis add_mset_add_single)
     moreover have count': "count ?χ' L = n" using C count by auto
     moreover have Lχ': "L ∈# ?χ'" by auto
     moreover have χ'ψ': "?χ' ∈ fst ?ψ'" by auto
     ultimately obtain ψ''  and χ''
     where
       "inference⇧*⇧* ?ψ' ψ''" and
       α: "χ'' ∈ fst ψ''" and
       "∀La. (La ∈# ?χ') ⟷ (La ∈# χ'')" and
       β: "count χ'' L = (1::nat)" and
       φ': "∀φ. φ ∈ fst ?ψ' ⟶ φ ∈ fst ψ''" and
       Iχ: "I ⊨ ?χ' ⟷ I ⊨ χ''" and
       tot: "∀I'. total_over_m I' {?χ'} ⟶ total_over_m I' {χ''}"
       using IH[of ?χ' ?ψ'] count' Lχ' χ'ψ' by blast

     then have "inference⇧*⇧* ψ ψ''"
     and "∀La. (La ∈# χ) ⟷ (La ∈# χ'')"
     using inf unfolding C by auto
     moreover have "∀φ. φ ∈ fst ψ ⟶ φ ∈ fst ψ''" using φ φ' by metis
     moreover have "I ⊨ χ ⟷ I ⊨ χ''" using Iχ unfolding true_cls_def C by auto
     moreover have "∀I'. total_over_m I' {χ} ⟶ total_over_m I' {χ''}"
       using tot unfolding C total_over_m_def by auto
     ultimately have ?case using φ φ' α β  by metis
  }
  ultimately show ?case by auto
qed

lemma can_decrease_tree_size:
  fixes ψ :: "'v state" and tree :: "'v sem_tree"
  assumes "finite (fst ψ)" and "already_used_inv ψ"
  and "partial_interps tree I (fst ψ)"
  shows "∃(tree':: 'v sem_tree) ψ'. inference⇧*⇧* ψ ψ' ∧ partial_interps tree' I (fst ψ')
             ∧ (sem_tree_size tree' < sem_tree_size tree ∨ sem_tree_size tree = 0)"
  using assms
proof (induct arbitrary: I rule: sem_tree_size)
  case (bigger xs I) note IH = this(1) and finite = this(2) and a_u_i = this(3) and part = this(4)

  {
    assume "sem_tree_size xs = 0"
    then have "?case" using part by blast
  }

  moreover {
    assume sn0: "sem_tree_size xs > 0"
    obtain ag ad v where xs: "xs = Node v ag ad" using sn0 by (cases xs, auto)
    {
      assume "sem_tree_size ag = 0" and "sem_tree_size ad = 0"
      then have ag: "ag = Leaf" and ad: "ad = Leaf" by (cases ag,  auto) (cases ad,  auto)

      then obtain χ χ' where
        χ: "¬ I ∪ {Pos v} ⊨ χ" and
        totχ: "total_over_m (I ∪ {Pos v}) {χ}" and
        χψ: "χ ∈ fst ψ" and
        χ': "¬ I ∪ {Neg v} ⊨ χ'" and
        totχ': "total_over_m (I ∪ {Neg v}) {χ'}" and
        χ'ψ: "χ' ∈ fst ψ"
        using part unfolding xs by auto
      have Posv: "Pos v ∉# χ" using χ unfolding true_cls_def true_lit_def by auto
      have Negv: "Neg v ∉# χ'" using χ' unfolding true_cls_def true_lit_def by auto
      {
        assume Negχ: "Neg v ∉# χ"
        have "¬ I ⊨ χ" using χ Posv unfolding true_cls_def true_lit_def by auto
        moreover have "total_over_m I {χ}"
          using Posv Negχ atm_imp_pos_or_neg_lit totχ unfolding total_over_m_def total_over_set_def
          by fastforce
        ultimately have "partial_interps Leaf I (fst ψ)"
        and "sem_tree_size Leaf < sem_tree_size xs"
        and "inference⇧*⇧* ψ ψ"
          unfolding xs by (auto simp add: χψ)
      }
      moreover {
        assume Posχ: "Pos v ∉# χ'"
        then have Iχ: "¬ I ⊨ χ'" using χ' Posv unfolding true_cls_def true_lit_def by auto
        moreover have "total_over_m I {χ'}"
          using Negv Posχ atm_imp_pos_or_neg_lit totχ'
          unfolding total_over_m_def total_over_set_def by fastforce
        ultimately have "partial_interps Leaf I (fst ψ)" and
          "sem_tree_size Leaf < sem_tree_size xs" and
          "inference⇧*⇧* ψ ψ"
          using χ'ψ Iχ unfolding xs by auto
      }
      moreover {
        assume neg: "Neg v ∈# χ" and pos: "Pos v ∈# χ'"
        then obtain ψ' χ2 where inf: "rtranclp inference ψ ψ'" and χ2incl: "χ2 ∈ fst ψ'"
          and χχ2_incl: "∀L. L ∈# χ ⟷ L ∈# χ2"
          and countχ2: "count χ2 (Neg v) = 1"
          and φ: "∀φ::'v literal multiset. φ ∈ fst ψ ⟶ φ ∈ fst ψ'"
          and Iχ: "I ⊨ χ ⟷ I ⊨ χ2"
          and tot_impχ: "∀I'. total_over_m I' {χ} ⟶ total_over_m I' {χ2}"
          using can_decrease_count[of χ "Neg v" "count χ (Neg v)" ψ I] χψ χ'ψ by auto

        have "χ' ∈ fst ψ'" by (simp add: χ'ψ φ)
        with pos
        obtain ψ'' χ2' where
        inf': "inference⇧*⇧* ψ' ψ''"
        and χ2'_incl: "χ2' ∈ fst ψ''"
        and χ'χ2_incl: "∀L::'v literal. (L ∈# χ') = (L ∈# χ2')"
        and countχ2': "count χ2' (Pos v) = (1::nat)"
        and φ': "∀φ::'v literal multiset. φ ∈ fst ψ' ⟶ φ ∈ fst ψ''"
        and Iχ': "I ⊨ χ' ⟷ I ⊨ χ2'"
        and tot_impχ': "∀I'. total_over_m I' {χ'} ⟶ total_over_m I' {χ2'}"
        using can_decrease_count[of χ' "Pos v" " count χ' (Pos v)" ψ' I] by auto

        define C where C: "C = χ2 - {#Neg v#}"

        then have χ2: "χ2 = C + {#Neg v#}" and negC: "Neg v ∉# C" and posC: "Pos v ∉# C"
            using χχ2_incl neg apply auto[]
           using C χχ2_incl neg countχ2 count_eq_zero_iff apply fastforce
          using C Posv χχ2_incl in_diffD by fastforce

        obtain C' where
          χ2': "χ2' = C' + {#Pos v#}" and
          posC': "Pos v ∉# C'" and
          negC': "Neg v ∉# C'"
          proof -
            assume a1: "⋀C'. ⟦χ2' = C' + {#Pos v#}; Pos v ∉# C'; Neg v ∉# C'⟧ ⟹ thesis"
            have f2: "⋀n. (n::nat) - n = 0"
              by simp
            have "Neg v ∉# χ2' - {#Pos v#}"
              using Negv χ'χ2_incl by (auto simp: not_in_iff)
            have "count {#Pos v#} (Pos v) = 1"
              by simp
            then show ?thesis
              by (metis χ'χ2_incl ‹Neg v ∉# χ2' - {#Pos v#}› a1 countχ2' count_diff f2
                insert_DiffM2 less_numeral_extra(3) mem_Collect_eq pos set_mset_def)
          qed

        have "already_used_inv ψ'"
          using rtranclp_inference_preserves_already_used_inv[of ψ ψ'] a_u_i inf by blast
        then have a_u_i_ψ'': "already_used_inv ψ''"
          using rtranclp_inference_preserves_already_used_inv a_u_i inf' unfolding tautology_def
          by simp

        have totC: "total_over_m I {C}"
          using tot_impχ totχ tot_over_m_remove[of I "Pos v" C] negC posC unfolding χ2
          by (metis total_over_m_sum uminus_Neg uminus_of_uminus_id)
        have totC': "total_over_m I {C'}"
          using tot_impχ' totχ' total_over_m_sum tot_over_m_remove[of I "Neg v" C'] negC' posC'
          unfolding χ2' by (metis total_over_m_sum uminus_Neg)
        have "¬ I ⊨ C + C'"
          using χ Iχ χ' Iχ' unfolding χ2 χ2' true_cls_def by auto
        then have part_I_ψ''': "partial_interps Leaf I (fst ψ'' ∪ {C + C'})"
          using totC totC' by simp
            (metis ‹¬ I ⊨ C + C'› atms_of_ms_singleton total_over_m_def total_over_m_sum)
        {
          assume "({#Pos v#} + C', {#Neg v#} + C) ∉ snd ψ''"
          then have inf'': " inference ψ'' (fst ψ'' ∪ {C + C'}, snd ψ'' ∪ {(χ2', χ2)})"
            using add.commute φ' χ2incl ‹χ2' ∈ fst ψ''›  unfolding χ2 χ2'
            by (metis prod.collapse inference_step resolution)
          have "inference⇧*⇧* ψ (fst ψ'' ∪ {C + C'}, snd ψ'' ∪ {(χ2', χ2)})"
            using inf inf' inf''  rtranclp_trans by auto
          moreover have "sem_tree_size Leaf < sem_tree_size xs" unfolding xs by auto
          ultimately have "?case" using part_I_ψ''' by (metis fst_conv)
        }
        moreover {
          assume a: "({#Pos v#} + C', {#Neg v#} + C) ∈ snd ψ''"
          then have "(∃χ ∈ fst ψ''. (∀I. total_over_m I {C+C'} ⟶ total_over_m I {χ})
                     ∧ (∀I. total_over_m I {χ} ⟶ I ⊨ χ ⟶ I ⊨ C' + C))
                 ∨ tautology (C' + C)"
            proof -
              obtain p where p: "Pos p ∈# ({#Pos v#} + C')" and
              n: "Neg p ∈# ({#Neg v#} + C)" and
              decomp: "((∃χ∈fst ψ''.
                         (∀I. total_over_m I {({#Pos v#} + C') - {#Pos p#}
                                 + (({#Neg v#} + C) - {#Neg p#})}
                            ⟶ total_over_m I {χ})
                         ∧ (∀I. total_over_m I {χ} ⟶ I ⊨ χ
                            ⟶ I ⊨ ({#Pos v#} + C') - {#Pos p#} + (({#Neg v#} + C) - {#Neg p#}))
                        )
                      ∨ tautology (({#Pos v#} + C') - {#Pos p#} + (({#Neg v#} + C) - {#Neg p#})))"
                using a by (blast intro: allE[OF a_u_i_ψ''[unfolded subsumes_def Ball_def],
                    of "({#Pos v#} + C', {#Neg v#} + C)"])
              { assume "p ≠ v"
                then have "Pos p ∈# C' ∧ Neg p ∈# C" using p n by force
                then have ?thesis unfolding Bex_def by auto
              }
              moreover {
                assume "p = v"
               then have "?thesis" using decomp by (metis add.commute add_diff_cancel_left')
              }
              ultimately show ?thesis by auto
            qed
          moreover {
            assume "∃χ ∈ fst ψ''. (∀I. total_over_m I {C+C'} ⟶ total_over_m I {χ})
              ∧ (∀I. total_over_m I {χ} ⟶ I ⊨ χ ⟶ I ⊨ C' + C)"
            then obtain θ where θ: "θ ∈ fst ψ''" and
              tot_θ_CC': "∀I. total_over_m I {C+C'} ⟶ total_over_m I {θ}" and
              θ_inv: "∀I. total_over_m I {θ} ⟶ I ⊨ θ ⟶ I ⊨ C' + C" by blast
            have "partial_interps Leaf I (fst ψ'')"
              using tot_θ_CC' θ θ_inv totC totC' ‹¬ I ⊨ C + C'› total_over_m_sum by fastforce
            moreover have "sem_tree_size Leaf < sem_tree_size xs" unfolding xs by auto
            ultimately have ?case by (metis inf inf' rtranclp_trans)
          }
          moreover {
            assume tautCC': "tautology (C' + C)"
            have "total_over_m I {C'+C}" using totC totC' total_over_m_sum by auto
            then have "¬tautology (C' + C)"
              using ‹¬ I ⊨ C + C'› unfolding add.commute[of C C'] total_over_m_def
              unfolding tautology_def by auto
            then have False using tautCC'  unfolding tautology_def by auto
          }
          ultimately have ?case by auto
        }
        ultimately have ?case by auto
      }
      ultimately have ?case using part by (metis (no_types) sem_tree_size.simps(1))
    }
    moreover {
      assume size_ag: "sem_tree_size ag > 0"
      have "sem_tree_size ag < sem_tree_size xs" unfolding xs by auto
      moreover have "partial_interps ag (I ∪ {Pos v}) (fst ψ)"
        and partad: "partial_interps ad (I ∪ {Neg v}) (fst ψ)"
        using part partial_interps.simps(2) unfolding xs by metis+
      moreover have "sem_tree_size ag < sem_tree_size xs ⟶ finite (fst ψ) ⟶ already_used_inv ψ
        ⟶ ( partial_interps ag (I ∪ {Pos v}) (fst ψ) ⟶
        (∃tree' ψ'. inference⇧*⇧* ψ ψ' ∧ partial_interps tree' (I ∪ {Pos v}) (fst ψ')
          ∧ (sem_tree_size tree' < sem_tree_size ag ∨ sem_tree_size ag = 0)))"
          using IH by auto
      ultimately obtain ψ' :: "'v state" and tree' :: "'v sem_tree" where
        inf: "inference⇧*⇧* ψ ψ'"
        and part: "partial_interps tree' (I ∪ {Pos v}) (fst ψ')"
        and size: "sem_tree_size tree' < sem_tree_size ag ∨ sem_tree_size ag = 0"
        using finite part rtranclp.rtrancl_refl a_u_i by blast

      have "partial_interps ad (I ∪ {Neg v}) (fst ψ')"
        using rtranclp_inference_preserve_partial_tree inf partad by metis
      then have "partial_interps (Node v tree' ad) I (fst ψ')" using part by auto
      then have ?case using inf size size_ag part unfolding xs by fastforce
    }
    moreover {
      assume size_ad: "sem_tree_size ad > 0"
      have "sem_tree_size ad < sem_tree_size xs" unfolding xs by auto
      moreover have partag: "partial_interps ag (I ∪ {Pos v}) (fst ψ)" and
        "partial_interps ad (I ∪ {Neg v}) (fst ψ)"
        using part partial_interps.simps(2) unfolding xs by metis+
      moreover have "sem_tree_size ad < sem_tree_size xs ⟶ finite (fst ψ) ⟶ already_used_inv ψ
        ⟶ ( partial_interps ad (I ∪ {Neg v}) (fst ψ)
        ⟶ (∃tree' ψ'. inference⇧*⇧* ψ ψ' ∧ partial_interps tree' (I ∪ {Neg v}) (fst ψ')
            ∧ (sem_tree_size tree' < sem_tree_size ad ∨ sem_tree_size ad = 0)))"
        using IH by auto
      ultimately obtain ψ' :: "'v state" and tree' :: "'v sem_tree" where
        inf: "inference⇧*⇧* ψ ψ'"
        and part: "partial_interps tree' (I ∪ {Neg v}) (fst ψ')"
        and size: "sem_tree_size tree' < sem_tree_size ad ∨ sem_tree_size ad = 0"
        using finite part rtranclp.rtrancl_refl a_u_i by blast

      have "partial_interps ag (I ∪ {Pos v}) (fst ψ')"
        using rtranclp_inference_preserve_partial_tree inf partag by metis
      then have "partial_interps (Node v ag tree') I (fst ψ')" using part by auto
      then have "?case" using inf size size_ad unfolding xs by fastforce
    }
    ultimately have ?case by auto
  }
  ultimately show ?case by auto
qed

lemma inference_completeness_inv:
  fixes ψ :: "'v ::linorder state"
  assumes
    unsat: "¬satisfiable (fst ψ)" and
    finite: "finite (fst ψ)" and
    a_u_v: "already_used_inv ψ"
  shows "∃ψ'. (inference⇧*⇧* ψ ψ' ∧ {#} ∈ fst ψ')"
proof -
  obtain tree where "partial_interps tree {} (fst ψ)"
    using partial_interps_build_sem_tree_atms assms by metis
  then show ?thesis
    using unsat finite a_u_v
    proof (induct tree arbitrary: ψ rule: sem_tree_size)
      case (bigger tree ψ) note H = this
      {
        fix χ
        assume tree: "tree = Leaf"
        obtain χ where χ: "¬ {} ⊨ χ" and totχ: "total_over_m {} {χ}" and χψ: "χ ∈ fst ψ"
          using H unfolding tree by auto
        moreover have "{#} = χ"
          using totχ unfolding total_over_m_def total_over_set_def by fastforce
        moreover have "inference⇧*⇧* ψ ψ" by auto
        ultimately have ?case by metis
      }
      moreover {
        fix v tree1 tree2
        assume tree: "tree = Node v tree1 tree2"
        obtain
          tree' ψ' where inf: "inference⇧*⇧* ψ ψ'" and
          part': "partial_interps tree' {} (fst ψ')" and
          decrease: "sem_tree_size tree' < sem_tree_size tree ∨ sem_tree_size tree = 0"
          using can_decrease_tree_size[of ψ] H(2,4,5)  unfolding tautology_def by meson
        have "sem_tree_size tree' < sem_tree_size tree" using decrease unfolding tree by auto
        moreover have "finite (fst ψ')" using rtranclp_inference_preserves_finite inf H(4) by metis
        moreover have "unsatisfiable (fst ψ')"
          using inference_preserves_unsat inf bigger.prems(2) by blast
        moreover have "already_used_inv ψ'"
          using H(5) inf rtranclp_inference_preserves_already_used_inv[of ψ ψ'] by auto
        ultimately have ?case using inf rtranclp_trans part' H(1) by fastforce
      }
      ultimately show ?case by (cases tree, auto)
   qed
qed

lemma inference_completeness:
  fixes ψ :: "'v ::linorder state"
  assumes unsat: "¬satisfiable (fst ψ)"
  and finite: "finite (fst ψ)"
  and "snd ψ = {}"
  shows "∃ψ'. (rtranclp inference ψ ψ' ∧ {#} ∈ fst ψ')"
proof -
  have "already_used_inv ψ" unfolding assms by auto
  then show ?thesis using assms inference_completeness_inv by blast
qed

lemma inference_soundness:
  fixes ψ :: "'v ::linorder state"
  assumes "rtranclp inference ψ ψ'" and "{#} ∈ fst ψ'"
  shows "unsatisfiable (fst ψ)"
  using assms by (meson rtranclp_inference_preserve_models satisfiable_def true_cls_empty
    true_clss_def)

lemma inference_soundness_and_completeness:
fixes ψ :: "'v ::linorder state"
assumes finite: "finite (fst ψ)"
and "snd ψ = {}"
shows "(∃ψ'. (inference⇧*⇧* ψ ψ' ∧ {#} ∈ fst ψ')) ⟷ unsatisfiable (fst ψ)"
  using assms inference_completeness inference_soundness by metis

subsection ‹Lemma about the Simplified State›

abbreviation "simplified ψ ≡ (no_step simplify ψ)"

lemma simplified_count:
  assumes simp: "simplified ψ" and χ: "χ ∈ ψ"
  shows "count χ L ≤ 1"
proof -
  {
    let ?χ' = "χ - {#L, L#}"
    assume "count χ L ≥ 2"
    then have f1: "count (χ - {#L, L#} + {#L, L#}) L = count χ L"
      by simp
    then have "L ∈# χ - {#L#}"
      by (metis (no_types) add.left_neutral add_diff_cancel_left' count_union diff_diff_add
        diff_single_trivial insert_DiffM mem_Collect_eq multi_member_this not_gr0 set_mset_def)
    then have χ': "{#L, L#} + ?χ' = χ"
      using f1 in_diffD insert_DiffM by fastforce

    have "∃ψ'. simplify ψ ψ'"
      by (metis (no_types, hide_lams) χ χ' factoring_imp_simplify)
    then have False using simp by auto
  }
  then show ?thesis by arith
qed

lemma simplified_no_both:
  assumes simp: "simplified ψ" and χ: "χ ∈ ψ"
  shows "¬ (L ∈# χ ∧ -L ∈# χ)"
proof (rule ccontr)
  assume "¬ ¬ (L ∈# χ ∧ - L ∈# χ)"
  then have "L ∈# χ ∧ - L ∈# χ" by metis
  then obtain χ' where "χ = add_mset (Pos (atm_of L)) (add_mset (Neg (atm_of L)) χ')"
    by (cases L) (auto dest!: multi_member_split simp: add_eq_conv_ex)
  then show False using χ simp tautology_deletion by fast
qed

lemma add_mset_Neg_Pos_commute[simp]:
  "add_mset (Neg P) (add_mset (Pos P) C) = add_mset (Pos P) (add_mset (Neg P) C)"
  by (rule add_mset_commute)

lemma simplified_not_tautology:
  assumes "simplified {ψ}"
  shows "~tautology ψ"
proof (rule ccontr)
  assume "~ ?thesis"
  then obtain p where "Pos p ∈# ψ ∧ Neg p ∈# ψ" using tautology_decomp by metis
  then obtain χ where "ψ = χ + {#Pos p#} + {#Neg p#}"
    by (auto dest!: multi_member_split simp: add_eq_conv_ex)
  then have "~ simplified {ψ}" by (auto intro: tautology_deletion)
  then show False using assms by auto
qed

lemma simplified_remove:
  assumes "simplified {ψ}"
  shows "simplified {ψ - {#l#}}"
proof (rule ccontr)
  assume ns: "¬ simplified {ψ - {#l#}}"
  {
    assume "l ∉# ψ"
    then have "ψ - {#l#} = ψ" by simp
    then have False using ns assms by auto
  }
  moreover {
    assume lψ: "l ∈# ψ"
    have A: "⋀A. A ∈ {ψ - {#l#}} ⟷ add_mset l A ∈ {ψ}" by (auto simp add: lψ)
    obtain l' where l': "simplify {ψ - {#l#}} l'" using ns by metis
    then have "∃l'. simplify {ψ} l'"
      proof (induction rule: simplify.induct)
        case (tautology_deletion P A)
        then have "{#Neg P#} + ({#Pos P#} + (A + {#l#})) ∈ {ψ}"
          using A by auto
        then show ?thesis
          using simplified_no_both by fastforce
      next
        case (condensation L A)
        have "add_mset l (add_mset L (add_mset L A)) ∈ {ψ}"
          using condensation.hyps unfolding A by blast
        then have "{#L, L#} + (A + {#l#}) ∈ {ψ}"
          by auto
        then show ?case
          using factoring_imp_simplify by blast
      next
        case (subsumption A B)
        then show ?case by blast
      qed
    then have False using assms(1) by blast
  }
  ultimately show False by auto
qed


lemma in_simplified_simplified:
  assumes simp: "simplified ψ" and incl: "ψ' ⊆ ψ"
  shows "simplified ψ'"
proof (rule ccontr)
  assume "¬ ?thesis"
  then obtain ψ'' where "simplify ψ' ψ''" by metis
    then have "∃l'. simplify ψ l'"
      proof (induction rule: simplify.induct)
        case (tautology_deletion A P)
        then show ?thesis using simplify.tautology_deletion[of "A" P "ψ"] incl by blast
      next
        case (condensation A L)
        then show ?case using simplify.condensation[of A L "ψ"] incl by blast
      next
        case (subsumption A B)
        then show ?case using simplify.subsumption[of A "ψ" B] incl by auto
      qed
  then show False using assms(1) by blast
qed

lemma simplified_in:
  assumes "simplified ψ"
  and "N ∈ ψ"
  shows "simplified {N}"
  using assms by (metis Set.set_insert empty_subsetI in_simplified_simplified insert_mono)

lemma subsumes_imp_formula:
  assumes "ψ ≤# φ"
  shows "{ψ} ⊨p φ"
  unfolding true_clss_cls_def apply auto
  using assms true_cls_mono_leD by blast

lemma simplified_imp_distinct_mset_tauto:
  assumes simp: "simplified ψ'"
  shows "distinct_mset_set ψ'" and "∀χ ∈ ψ'. ¬tautology χ"
proof -
  show "∀χ ∈ ψ'. ¬tautology χ"
    using simp by (auto simp add: simplified_in simplified_not_tautology)

  show "distinct_mset_set ψ'"
    proof (rule ccontr)
      assume "¬?thesis"
      then obtain χ where "χ ∈ ψ'" and "¬distinct_mset χ" unfolding distinct_mset_set_def by auto
      then obtain L where "count χ L ≥ 2"
        unfolding distinct_mset_def
        by (meson count_greater_eq_one_iff le_antisym simp simplified_count)
      then show False by (metis Suc_1 ‹χ ∈ ψ'› not_less_eq_eq simp simplified_count)
    qed
qed

lemma simplified_no_more_full1_simplified:
  assumes "simplified ψ"
  shows "¬full1 simplify ψ ψ'"
  using assms unfolding full1_def by (meson tranclpD)


subsection ‹Resolution and Invariants›

inductive resolution :: "'v state ⇒ 'v state ⇒ bool" where
full1_simp: "full1 simplify N N' ⟹ resolution (N, already_used) (N', already_used)" |
inferring: "inference (N, already_used) (N', already_used') ⟹ simplified N
  ⟹ full simplify N' N'' ⟹ resolution (N, already_used) (N'', already_used')"

subsubsection ‹Invariants›

lemma resolution_finite:
  assumes "resolution ψ ψ'" and "finite (fst ψ)"
  shows "finite (fst ψ')"
  using assms by (induct rule: resolution.induct)
    (auto simp add: full1_def full_def rtranclp_simplify_preserves_finite
      dest: tranclp_into_rtranclp inference_preserves_finite)

lemma rtranclp_resolution_finite:
  assumes "resolution⇧*⇧* ψ ψ'" and "finite (fst ψ)"
  shows "finite (fst ψ')"
  using assms by (induct rule: rtranclp_induct, auto simp add: resolution_finite)

lemma resolution_finite_snd:
  assumes "resolution ψ ψ'" and "finite (snd ψ)"
  shows "finite (snd ψ')"
  using assms apply (induct rule: resolution.induct, auto simp add: inference_preserves_finite_snd)
  using inference_preserves_finite_snd snd_conv by metis

lemma rtranclp_resolution_finite_snd:
  assumes "resolution⇧*⇧* ψ ψ'" and "finite (snd ψ)"
  shows "finite (snd ψ')"
  using assms by (induct rule: rtranclp_induct, auto simp add: resolution_finite_snd)

lemma resolution_always_simplified:
 assumes "resolution ψ ψ'"
 shows "simplified (fst ψ')"
 using assms by (induct rule: resolution.induct)
   (auto simp add: full1_def full_def)

lemma tranclp_resolution_always_simplified:
  assumes "tranclp resolution ψ ψ'"
  shows "simplified (fst ψ')"
  using assms by (induct rule: tranclp.induct, auto simp add: resolution_always_simplified)

lemma resolution_atms_of:
  assumes "resolution ψ ψ'" and "finite (fst ψ)"
  shows "atms_of_ms (fst ψ') ⊆ atms_of_ms (fst ψ)"
  using assms apply (induct rule: resolution.induct)
    apply(simp add: rtranclp_simplify_atms_of_ms tranclp_into_rtranclp full1_def )
  by (metis (no_types, lifting) contra_subsetD fst_conv full_def
    inference_preserves_atms_of_ms rtranclp_simplify_atms_of_ms subsetI)

lemma rtranclp_resolution_atms_of:
  assumes "resolution⇧*⇧* ψ ψ'" and "finite (fst ψ)"
  shows "atms_of_ms (fst ψ') ⊆ atms_of_ms (fst ψ)"
  using assms apply (induct rule: rtranclp_induct)
  using resolution_atms_of rtranclp_resolution_finite by blast+

lemma resolution_include:
  assumes res: "resolution ψ ψ'" and finite: "finite (fst ψ)"
  shows "fst ψ' ⊆ simple_clss (atms_of_ms (fst ψ))"
proof -
  have finite': "finite (fst ψ')" using local.finite res resolution_finite by blast
  have "simplified (fst ψ')" using res finite' resolution_always_simplified by blast
  then have "fst ψ' ⊆ simple_clss (atms_of_ms (fst ψ'))"
    using simplified_in_simple_clss finite' simplified_imp_distinct_mset_tauto[of "fst ψ'"] by auto
  moreover have "atms_of_ms (fst ψ') ⊆ atms_of_ms (fst ψ)"
    using res finite resolution_atms_of[of ψ ψ'] by auto
  ultimately show ?thesis by (meson atms_of_ms_finite local.finite order.trans rev_finite_subset
    simple_clss_mono)
qed

lemma rtranclp_resolution_include:
  assumes res: "tranclp resolution ψ ψ'" and finite: "finite (fst ψ)"
  shows "fst ψ' ⊆ simple_clss (atms_of_ms (fst ψ))"
  using assms apply (induct rule: tranclp.induct)
    apply (simp add: resolution_include)
  by (meson simple_clss_mono order_trans resolution_include
    rtranclp_resolution_atms_of rtranclp_resolution_finite tranclp_into_rtranclp)

abbreviation already_used_all_simple
  :: "('a literal multiset × 'a literal multiset) set ⇒ 'a set ⇒ bool" where
"already_used_all_simple already_used vars ≡
(∀ (A, B) ∈ already_used. simplified {A} ∧ simplified {B} ∧ atms_of A ⊆ vars ∧ atms_of B ⊆ vars)"

lemma already_used_all_simple_vars_incl:
  assumes "vars ⊆ vars'"
  shows "already_used_all_simple a vars ⟹ already_used_all_simple a vars'"
  using assms by fast

lemma inference_clause_preserves_already_used_all_simple:
  assumes "inference_clause S S'"
  and "already_used_all_simple (snd S) vars"
  and "simplified (fst S)"
  and "atms_of_ms (fst S) ⊆ vars"
  shows "already_used_all_simple (snd (fst S ∪ {fst S'}, snd S')) vars"
  using assms
proof (induct rule: inference_clause.induct)
  case (factoring L C N already_used)
  then show ?case by (simp add: simplified_in factoring_imp_simplify)
next
  case (resolution P C N D already_used) note H = this
  show ?case apply clarify
    proof -
      fix A B v
      assume "(A, B) ∈ snd (fst (N, already_used)
        ∪ {fst (C + D, already_used ∪ {({#Pos P#} + C, {#Neg P#} + D)})},
           snd (C + D, already_used ∪ {({#Pos P#} + C, {#Neg P#} + D)}))"
      then have "(A, B) ∈ already_used ∨ (A, B) = ({#Pos P#} + C, {#Neg P#} + D)" by auto
      moreover {
        assume "(A, B) ∈ already_used"
        then have "simplified {A} ∧ simplified {B} ∧ atms_of A ⊆ vars ∧ atms_of B ⊆ vars"
          using H(4) by auto
      }
      moreover {
        assume eq: "(A, B) = ({#Pos P#} + C, {#Neg P#} + D)"
        then have "simplified {A}" using simplified_in H(1,5) by auto
        moreover have "simplified {B}" using eq simplified_in H(2,5) by auto
        moreover have "atms_of A ⊆ atms_of_ms N"
          using eq H(1)
          using atms_of_atms_of_ms_mono[of A N] by auto
        moreover have "atms_of B ⊆ atms_of_ms N"
          using eq H(2) atms_of_atms_of_ms_mono[of B N] by auto
        ultimately have "simplified {A} ∧ simplified {B} ∧ atms_of A ⊆ vars ∧ atms_of B ⊆ vars"
          using H(6) by auto
      }
      ultimately show "simplified {A} ∧ simplified {B} ∧ atms_of A ⊆ vars ∧ atms_of B ⊆ vars"
        by fast
    qed
qed

lemma inference_preserves_already_used_all_simple:
  assumes "inference S S'"
  and "already_used_all_simple (snd S) vars"
  and "simplified (fst S)"
  and "atms_of_ms (fst S) ⊆ vars"
  shows "already_used_all_simple (snd S') vars"
  using assms
proof (induct rule: inference.induct)
  case (inference_step S clause already_used)
  then show ?case
    using inference_clause_preserves_already_used_all_simple[of S "(clause, already_used)" vars]
    by auto
qed

lemma already_used_all_simple_inv:
  assumes "resolution S S'"
  and "already_used_all_simple (snd S) vars"
  and "atms_of_ms (fst S) ⊆ vars"
  shows "already_used_all_simple (snd S') vars"
  using assms
proof (induct rule: resolution.induct)
  case (full1_simp N N')
  then show ?case by simp
next
  case (inferring N already_used N' already_used' N'')
  then show "already_used_all_simple (snd (N'', already_used')) vars"
    using inference_preserves_already_used_all_simple[of "(N, already_used)"] by simp
qed

lemma rtranclp_already_used_all_simple_inv:
  assumes "resolution⇧*⇧* S S'"
  and "already_used_all_simple (snd S) vars"
  and "atms_of_ms (fst S) ⊆ vars"
  and "finite (fst S)"
  shows "already_used_all_simple (snd S') vars"
  using assms
proof (induct rule: rtranclp_induct)
  case base
  then show ?case by simp
next
  case (step S' S'') note infstar = this(1) and IH = this(3) and res = this(2) and
    already = this(4) and atms = this(5) and finite = this(6)
  have "already_used_all_simple (snd S') vars" using IH already atms finite by simp
  moreover have "atms_of_ms (fst S') ⊆ atms_of_ms (fst S)"
    by (simp add: infstar local.finite rtranclp_resolution_atms_of)
  then have "atms_of_ms (fst S') ⊆ vars" using atms by auto
  ultimately show ?case
    using already_used_all_simple_inv[OF res] by simp
qed

lemma inference_clause_simplified_already_used_subset:
  assumes "inference_clause S S'"
  and "simplified (fst S)"
  shows "snd S ⊂ snd S'"
  using assms apply (induct rule: inference_clause.induct)
   using factoring_imp_simplify apply (simp; blast)
  using factoring_imp_simplify by force

lemma inference_simplified_already_used_subset:
  assumes "inference S S'"
  and "simplified (fst S)"
  shows "snd S ⊂ snd S'"
  using assms apply (induct rule: inference.induct)
  by (metis inference_clause_simplified_already_used_subset snd_conv)

lemma resolution_simplified_already_used_subset:
  assumes "resolution S S'"
  and "simplified (fst S)"
  shows "snd S ⊂ snd S'"
  using assms apply (induct rule: resolution.induct, simp_all add: full1_def)
  apply (meson tranclpD)
  by (metis inference_simplified_already_used_subset fst_conv snd_conv)

lemma tranclp_resolution_simplified_already_used_subset:
  assumes "tranclp resolution S S'"
  and "simplified (fst S)"
  shows "snd S ⊂ snd S'"
  using assms apply (induct rule: tranclp.induct)
  using resolution_simplified_already_used_subset apply metis
  by (meson tranclp_resolution_always_simplified resolution_simplified_already_used_subset
    less_trans)

abbreviation "already_used_top vars ≡ simple_clss vars × simple_clss vars"

lemma already_used_all_simple_in_already_used_top:
  assumes "already_used_all_simple s vars" and "finite vars"
  shows "s ⊆ already_used_top vars"
proof
  fix x
  assume x_s: "x ∈ s"
  obtain A B where x: "x = (A, B)" by (cases x, auto)
  then have "simplified {A}" and "atms_of A ⊆ vars" using assms(1) x_s by fastforce+
  then have A: "A ∈ simple_clss vars"
    using simple_clss_mono[of "atms_of A" vars] x assms(2)
    simplified_imp_distinct_mset_tauto[of "{A}"]
    distinct_mset_not_tautology_implies_in_simple_clss by fast
  moreover have "simplified {B}" and "atms_of B ⊆ vars" using assms(1) x_s x by fast+
  then have B: "B ∈ simple_clss vars"
    using simplified_imp_distinct_mset_tauto[of "{B}"]
    distinct_mset_not_tautology_implies_in_simple_clss
    simple_clss_mono[of "atms_of B" vars] x assms(2) by fast
  ultimately show "x ∈ simple_clss vars × simple_clss vars"
    unfolding x by auto
qed

lemma already_used_top_finite:
  assumes "finite vars"
  shows "finite (already_used_top vars)"
  using simple_clss_finite assms by auto

lemma already_used_top_increasing:
  assumes "var ⊆ var'" and "finite var'"
  shows "already_used_top var ⊆ already_used_top var'"
  using assms simple_clss_mono by auto

lemma already_used_all_simple_finite:
  fixes s :: "('a literal multiset × 'a literal multiset) set" and vars :: "'a set"
  assumes "already_used_all_simple s vars" and "finite vars"
  shows "finite s"
  using assms already_used_all_simple_in_already_used_top[OF assms(1)]
  rev_finite_subset[OF already_used_top_finite[of vars]] by auto

abbreviation "card_simple vars ψ ≡ card (already_used_top vars - ψ)"

lemma resolution_card_simple_decreasing:
  assumes res: "resolution ψ ψ'"
  and a_u_s: "already_used_all_simple (snd ψ) vars"
  and finite_v: "finite vars"
  and finite_fst: "finite (fst ψ)"
  and finite_snd: "finite (snd ψ)"
  and simp: "simplified (fst ψ)"
  and "atms_of_ms (fst ψ) ⊆ vars"
  shows "card_simple vars (snd ψ') < card_simple vars (snd ψ)"
proof -
  let ?vars = "vars"
  let ?top = "simple_clss ?vars × simple_clss ?vars"
  have 1: "card_simple vars (snd ψ) = card ?top - card (snd ψ)"
    using card_Diff_subset finite_snd already_used_all_simple_in_already_used_top[OF a_u_s]
    finite_v by metis
  have a_u_s': "already_used_all_simple (snd ψ') vars"
    using already_used_all_simple_inv res a_u_s assms(7) by blast
  have f: "finite (snd ψ')" using already_used_all_simple_finite a_u_s' finite_v by auto
  have 2: "card_simple vars (snd ψ') = card ?top - card (snd ψ')"
    using card_Diff_subset[OF f] already_used_all_simple_in_already_used_top[OF a_u_s' finite_v]
    by auto
  have "card (already_used_top vars) ≥ card (snd ψ')"
    using already_used_all_simple_in_already_used_top[OF a_u_s' finite_v]
    card_mono[of "already_used_top vars" "snd ψ'"] already_used_top_finite[OF finite_v] by metis
  then show ?thesis
    using psubset_card_mono[OF f resolution_simplified_already_used_subset[OF res simp]]
    unfolding 1 2 by linarith
qed


lemma tranclp_resolution_card_simple_decreasing:
  assumes "tranclp resolution ψ ψ'" and finite_fst: "finite (fst ψ)"
  and "already_used_all_simple (snd ψ) vars"
  and "atms_of_ms (fst ψ) ⊆ vars"
  and finite_v: "finite vars"
  and finite_snd: "finite (snd ψ)"
  and "simplified (fst ψ)"
  shows "card_simple vars (snd ψ') < card_simple vars (snd ψ)"
  using assms
proof (induct rule: tranclp_induct)
  case (base ψ')
  then show ?case by (simp add: resolution_card_simple_decreasing)
next
  case (step ψ' ψ'') note res = this(1) and res' = this(2) and a_u_s = this(5) and
    atms = this(6) and f_v = this(7) and f_fst = this(4) and H = this
  then have "card_simple vars (snd ψ') < card_simple vars (snd ψ)" by auto
  moreover have a_u_s': "already_used_all_simple (snd ψ') vars"
    using rtranclp_already_used_all_simple_inv[OF tranclp_into_rtranclp[OF res] a_u_s atms f_fst] .
  have "finite (fst ψ')"
    by (meson finite_fst res rtranclp_resolution_finite tranclp_into_rtranclp)
  moreover have "finite (snd ψ')" using already_used_all_simple_finite[OF a_u_s' f_v] .
  moreover have "simplified (fst ψ')" using res tranclp_resolution_always_simplified by blast
  moreover have "atms_of_ms (fst ψ') ⊆ vars"
    by (meson atms f_fst order.trans res rtranclp_resolution_atms_of tranclp_into_rtranclp)
  ultimately show ?case
    using resolution_card_simple_decreasing[OF res' a_u_s' f_v] f_v
    less_trans[of "card_simple vars (snd ψ'')" "card_simple vars (snd ψ')"
      "card_simple vars (snd ψ)"]
    by blast
qed


lemma tranclp_resolution_card_simple_decreasing_2:
  assumes "tranclp resolution ψ ψ'"
  and finite_fst: "finite (fst ψ)"
  and empty_snd: "snd ψ = {}"
  and "simplified (fst ψ)"
  shows "card_simple (atms_of_ms (fst ψ)) (snd ψ') < card_simple (atms_of_ms (fst ψ)) (snd ψ)"
proof -
  let ?vars = "atms_of_ms (fst ψ)"
  have "already_used_all_simple (snd ψ) ?vars" unfolding empty_snd by auto
  moreover have "atms_of_ms (fst ψ) ⊆ ?vars" by auto
  moreover have finite_v: "finite ?vars" using finite_fst by auto
  moreover have finite_snd: "finite (snd ψ)" unfolding empty_snd by auto
  ultimately show ?thesis
    using assms(1,2,4) tranclp_resolution_card_simple_decreasing[of ψ ψ'] by presburger
qed


subsubsection ‹Well-Foundness of the Relation›

lemma wf_simplified_resolution:
  assumes f_vars: "finite vars"
  shows "wf {(y:: 'v:: linorder state, x). (atms_of_ms (fst x) ⊆ vars ∧ simplified (fst x)
    ∧ finite (snd x) ∧ finite (fst x) ∧ already_used_all_simple (snd x) vars) ∧ resolution x y}"
proof -
  {
    fix a b :: "'v::linorder state"
    assume "(b, a) ∈ {(y, x). (atms_of_ms (fst x) ⊆ vars ∧ simplified (fst x) ∧ finite (snd x)
      ∧ finite (fst x) ∧ already_used_all_simple (snd x) vars) ∧ resolution x y}"
    then have
      "atms_of_ms (fst a) ⊆ vars" and
      simp: "simplified (fst a)" and
      "finite (snd a)" and
      "finite (fst a)" and
      a_u_v: "already_used_all_simple (snd a) vars" and
      res: "resolution a b" by auto
    have "finite (already_used_top vars)" using f_vars already_used_top_finite by blast
    moreover have "already_used_top vars ⊆ already_used_top vars" by auto
    moreover have "snd b ⊆ already_used_top vars"
      using already_used_all_simple_in_already_used_top[of "snd b" vars]
      a_u_v already_used_all_simple_inv[OF res] ‹finite (fst a)› ‹atms_of_ms (fst a) ⊆ vars› f_vars
      by presburger
    moreover have "snd a ⊂ snd b" using resolution_simplified_already_used_subset[OF res simp] .
    ultimately have "finite (already_used_top vars) ∧ already_used_top vars ⊆ already_used_top vars
      ∧ snd b ⊆ already_used_top vars ∧ snd a ⊂ snd b" by metis
  }
  then show ?thesis using wf_bounded_set[of "{(y:: 'v:: linorder state, x).
    (atms_of_ms (fst x) ⊆ vars
    ∧ simplified (fst x) ∧ finite (snd x) ∧ finite (fst x)∧ already_used_all_simple (snd x) vars)
    ∧ resolution x y}" "λ_. already_used_top vars" "snd"] by auto
qed

lemma wf_simplified_resolution':
  assumes f_vars: "finite vars"
  shows "wf {(y:: 'v:: linorder state, x). (atms_of_ms (fst x) ⊆ vars ∧ ¬simplified (fst x)
    ∧ finite (snd x) ∧ finite (fst x) ∧ already_used_all_simple (snd x) vars) ∧ resolution x y}"
  unfolding wf_def
   apply (simp add: resolution_always_simplified)
  by (metis (mono_tags, hide_lams) fst_conv resolution_always_simplified)

lemma wf_resolution:
  assumes f_vars: "finite vars"
  shows "wf ({(y:: 'v:: linorder state, x). (atms_of_ms (fst x) ⊆ vars ∧ simplified (fst x)
        ∧ finite (snd x) ∧ finite (fst x) ∧ already_used_all_simple (snd x) vars) ∧ resolution x y}
    ∪ {(y, x). (atms_of_ms (fst x) ⊆ vars ∧ ¬ simplified (fst x) ∧ finite (snd x) ∧ finite (fst x)
       ∧ already_used_all_simple (snd x) vars) ∧ resolution x y})" (is "wf (?R ∪ ?S)")
proof -
  have "Domain ?R Int Range ?S = {}" using resolution_always_simplified by auto blast
  then show "wf (?R ∪ ?S)"
    using wf_simplified_resolution[OF f_vars] wf_simplified_resolution'[OF f_vars] wf_Un[of ?R ?S]
    by fast
qed

lemma rtrancp_simplify_already_used_inv:
  assumes "simplify⇧*⇧* S S'"
  and "already_used_inv (S, N)"
  shows "already_used_inv (S', N)"
  using assms apply induction
  using simplify_preserves_already_used_inv by fast+

lemma full1_simplify_already_used_inv:
  assumes "full1 simplify S S'"
  and "already_used_inv (S, N)"
  shows "already_used_inv (S', N)"
  using assms tranclp_into_rtranclp[of simplify S S'] rtrancp_simplify_already_used_inv
  unfolding full1_def by fast

lemma full_simplify_already_used_inv:
  assumes "full simplify S S'"
  and "already_used_inv (S, N)"
  shows "already_used_inv (S', N)"
  using assms rtrancp_simplify_already_used_inv unfolding full_def by fast
lemma resolution_already_used_inv:
  assumes "resolution S S'"
  and "already_used_inv S"
  shows "already_used_inv S'"
  using assms
proof induction
  case (full1_simp N N' already_used)
  then show ?case using full1_simplify_already_used_inv by fast
next
  case (inferring N already_used N' already_used' N''') note inf = this(1) and full = this(3) and
    a_u_v = this(4)
  then show ?case
    using inference_preserves_already_used_inv[OF inf a_u_v] full_simplify_already_used_inv full
    by fast
qed

lemma rtranclp_resolution_already_used_inv:
  assumes "resolution⇧*⇧* S S'"
  and "already_used_inv S"
  shows "already_used_inv S'"
  using assms apply induction
  using resolution_already_used_inv by fast+

lemma rtanclp_simplify_preserves_unsat:
  assumes "simplify⇧*⇧* ψ ψ'"
  shows "satisfiable ψ' ⟶ satisfiable ψ"
  using assms apply induction
  using simplify_clause_preserves_sat by blast+

lemma full1_simplify_preserves_unsat:
  assumes "full1 simplify ψ ψ'"
  shows "satisfiable ψ' ⟶ satisfiable ψ"
  using assms rtanclp_simplify_preserves_unsat[of ψ ψ'] tranclp_into_rtranclp
  unfolding full1_def by metis

lemma full_simplify_preserves_unsat:
  assumes "full simplify ψ ψ'"
  shows "satisfiable ψ' ⟶ satisfiable ψ"
  using assms rtanclp_simplify_preserves_unsat[of ψ ψ'] unfolding full_def by metis

lemma resolution_preserves_unsat:
  assumes "resolution ψ ψ'"
  shows "satisfiable (fst ψ') ⟶ satisfiable (fst ψ)"
  using assms apply (induct rule: resolution.induct)
  using full1_simplify_preserves_unsat apply (metis fst_conv)
  using full_simplify_preserves_unsat simplify_preserves_unsat by fastforce

lemma rtranclp_resolution_preserves_unsat:
  assumes "resolution⇧*⇧* ψ ψ'"
  shows "satisfiable (fst ψ') ⟶ satisfiable (fst ψ)"
  using assms apply induction
  using resolution_preserves_unsat by fast+

lemma rtranclp_simplify_preserve_partial_tree:
  assumes "simplify⇧*⇧* N N'"
  and "partial_interps t I N"
  shows "partial_interps t I N'"
  using assms apply (induction, simp)
  using simplify_preserve_partial_tree by metis

lemma full1_simplify_preserve_partial_tree:
  assumes "full1 simplify N N'"
  and "partial_interps t I N"
  shows "partial_interps t I N'"
  using assms rtranclp_simplify_preserve_partial_tree[of N N' t I] tranclp_into_rtranclp
  unfolding full1_def by fast

lemma full_simplify_preserve_partial_tree:
  assumes "full simplify N N'"
  and "partial_interps t I N"
  shows "partial_interps t I N'"
  using assms rtranclp_simplify_preserve_partial_tree[of N N' t I] tranclp_into_rtranclp
  unfolding full_def by fast

lemma resolution_preserve_partial_tree:
  assumes "resolution S S'"
  and "partial_interps t I (fst S)"
  shows "partial_interps t I (fst S')"
  using assms apply induction
    using full1_simplify_preserve_partial_tree fst_conv apply metis
  using full_simplify_preserve_partial_tree inference_preserve_partial_tree by fastforce

lemma rtranclp_resolution_preserve_partial_tree:
  assumes "resolution⇧*⇧* S S'"
  and "partial_interps t I (fst S)"
  shows "partial_interps t I (fst S')"
  using assms apply induction
  using resolution_preserve_partial_tree by fast+
  thm nat_less_induct nat.induct

lemma nat_ge_induct[case_names 0 Suc]:
  assumes "P 0"
  and "⋀n. (⋀m. m<Suc n ⟹ P m) ⟹ P (Suc n)"
  shows "P n"
  using assms apply (induct rule: nat_less_induct)
  by (rename_tac n, case_tac n) auto

lemma wf_always_more_step_False:
  assumes "wf R"
  shows "(∀x. ∃z. (z, x)∈R) ⟹ False"
 using assms unfolding wf_def by (meson Domain.DomainI assms wfE_min)

lemma finite_finite_mset_element_of_mset[simp]:
  assumes "finite N"
  shows "finite {f φ L |φ L. φ ∈ N ∧ L ∈# φ ∧ P φ L}"
  using assms
proof (induction N rule: finite_induct)
  case empty
  show ?case by auto
next
  case (insert x N) note finite = this(1) and IH = this(3)
  have "{f φ L |φ L. (φ = x ∨ φ ∈ N) ∧ L ∈# φ ∧ P φ L} ⊆ {f x L | L. L ∈# x ∧ P x L}
    ∪ {f φ L |φ L. φ ∈ N ∧ L ∈# φ ∧ P φ L}" by auto
  moreover have "finite {f x L | L. L ∈# x}" by auto
  ultimately show ?case using IH finite_subset by fastforce
qed


definition sum_count_ge_2 :: "'a multiset set ⇒ nat" ("Ξ") where
"sum_count_ge_2 ≡ folding.F (λφ. (+)(sum_mset {#count φ L |L ∈# φ. 2 ≤ count φ L#})) 0"


interpretation sum_count_ge_2:
  folding "λφ. (+)(sum_mset {#count φ L |L ∈# φ. 2 ≤ count φ L#})" 0
rewrites
  "folding.F (λφ. (+)(sum_mset {#count φ L |L ∈# φ. 2 ≤ count φ L#})) 0 = sum_count_ge_2"
proof -
  show "folding (λφ. (+) (sum_mset (image_mset (count φ) {# L ∈# φ. 2 ≤ count φ L#})))"
    by standard auto
  then interpret sum_count_ge_2:
    folding "λφ. (+)(sum_mset {#count φ L |L ∈# φ. 2 ≤ count φ L#})" 0 .
  show "folding.F (λφ. (+) (sum_mset (image_mset (count φ) {# L ∈# φ. 2 ≤ count φ L#}))) 0
    = sum_count_ge_2" by (auto simp add: sum_count_ge_2_def)
qed

lemma finite_incl_le_setsum:
 "finite (B::'a multiset set) ⟹ A ⊆ B ⟹ Ξ A ≤ Ξ B"
proof (induction arbitrary:A rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert a F) note finite = this(1) and aF = this(2) and IH = this(3) and AF = this(4)
  show ?case
    proof (cases "a ∈ A")
      assume "a ∉ A"
      then have "A ⊆ F" using AF by auto
      then show ?case using IH[of A] by (simp add: aF local.finite)
    next
      assume aA: "a ∈ A"
      then have "A - {a} ⊆ F" using AF by auto
      then have "Ξ (A - {a}) ≤ Ξ F" using IH by blast
      then show ?case
         proof -
           obtain nn :: "nat ⇒ nat ⇒ nat" where
             "∀x0 x1. (∃v2. x0 = x1 + v2) = (x0 = x1 + nn x0 x1)"
             by moura
           then have "Ξ F = Ξ (A - {a}) + nn (Ξ F) (Ξ (A - {a}))"
             by (meson ‹Ξ (A - {a}) ≤ Ξ F› le_iff_add)
           then show ?thesis
             by (metis (no_types) le_iff_add aA aF add.assoc finite.insertI finite_subset
               insert.prems local.finite sum_count_ge_2.insert sum_count_ge_2.remove)
         qed
    qed
qed

lemma simplify_finite_measure_decrease:
  "simplify N N' ⟹ finite N ⟹ card N' + Ξ N' < card N + Ξ N"
proof (induction rule: simplify.induct)
  case (tautology_deletion P A) note an = this(1) and fin = this(2)
  let ?N' = "N - {add_mset (Pos P) (add_mset (Neg P) A)}"
  have "card ?N' < card N"
    by (meson card_Diff1_less tautology_deletion.hyps tautology_deletion.prems)
  moreover have "?N' ⊆ N" by auto
  then have "sum_count_ge_2 ?N' ≤ sum_count_ge_2 N" using finite_incl_le_setsum[OF fin] by blast
  ultimately show ?case by linarith
next
  case (condensation L A) note AN = this(1) and fin = this(2)
  let ?C' = "add_mset L A"
  let ?C = "add_mset L ?C'"
  let ?N' = "N - {?C} ∪ {?C'}"
  have "card ?N' ≤ card N"
    using AN by (metis (no_types, lifting) Diff_subset Un_empty_right Un_insert_right card.remove
      card_insert_if card_mono fin finite_Diff order_refl)
  moreover have "Ξ {?C'} < Ξ {?C}"
  proof -
    have mset_decomp:
      "{# La ∈# A. (L = La ⟶ La ∈# A) ∧ (L ≠ La ⟶ 2 ≤ count A La)#}
        =  {# La ∈# A. L ≠ La ∧ 2 ≤ count A La#} +
          {# La ∈# A. L = La ∧ Suc 0 ≤ count A L#}"
      by (auto simp: multiset_eq_iff ac_simps)
    have mset_decomp2: "{# La ∈# A. L ≠ La ⟶ 2 ≤ count A La#} =
        {# La ∈# A. L ≠ La ∧ 2 ≤ count A La#} + replicate_mset (count A L) L"
      by (auto simp: multiset_eq_iff)
    have *: "(∑x∈#B. if L = x then Suc (count A x) else count A x) ≤
        (∑x∈#B. if L = x then Suc (count (add_mset L A) x) else count (add_mset L A) x)"
      for B
      by (auto intro!: sum_mset_mono)
    show ?thesis
      using *[of "{#La ∈# A. L ≠ La ∧ 2 ≤ count A La#}"]
      by (auto simp: mset_decomp mset_decomp2 filter_mset_eq)
  qed
  have "Ξ ?N' < Ξ N"
    proof cases
      assume a1: "?C' ∈ N"
      then show ?thesis
        proof -
          have f2: "⋀m M. insert (m::'a literal multiset) (M - {m}) = M ∪ {} ∨ m ∉ M"
            using Un_empty_right insert_Diff by blast
          have f3: "⋀m M Ma. insert (m::'a literal multiset) M - insert m Ma = M - insert m Ma"
            by simp
          then have f4: "⋀M m. M - {m::'a literal multiset} = M ∪ {} ∨ m ∈ M"
            using Diff_insert_absorb Un_empty_right by fastforce
          have f5: "insert ?C N = N"
            using f3 f2 Un_empty_right condensation.hyps insert_iff by fastforce
          have "⋀m M. insert (m::'a literal multiset) M = M ∪ {} ∨ m ∉ M"
            using f3 f2 Un_empty_right add.right_neutral insert_iff by fastforce
          then have "Ξ (N - {?C}) < Ξ N"
            using f5 f4 by (metis Un_empty_right ‹Ξ {?C'} < Ξ {?C}›
              add.right_neutral add_diff_cancel_left' add_gr_0 diff_less fin finite.emptyI not_le
              sum_count_ge_2.empty sum_count_ge_2.insert_remove trans_le_add2)
          then show ?thesis
            using f3 f2 a1 by (metis (no_types) Un_empty_right Un_insert_right condensation.hyps
              insert_iff multi_self_add_other_not_self)
        qed
    next
      assume "?C' ∉ N"
      have mset_decomp:
        "{# La ∈# A. (L = La ⟶ Suc 0 ≤ count A La) ∧ (L ≠ La ⟶ 2 ≤ count A La)#}
        =  {# La ∈# A. L ≠ La ∧ 2 ≤ count A La#} +
          {# La ∈# A. L = La ∧ Suc 0 ≤ count A L#}"
           by (auto simp: multiset_eq_iff ac_simps)
      have mset_decomp2: "{# La ∈# A. L ≠ La ⟶ 2 ≤ count A La#} =
        {# La ∈# A. L ≠ La ∧ 2 ≤ count A La#} + replicate_mset (count A L) L"
        by (auto simp: multiset_eq_iff)

      show ?thesis
        using ‹Ξ {?C'} < Ξ {?C}› condensation.hyps fin
        sum_count_ge_2.remove[of _ ?C] ‹?C' ∉ N›
        by (auto simp: mset_decomp mset_decomp2 filter_mset_eq)
    qed
  ultimately show ?case by linarith
next
  case (subsumption A B) note AN = this(1) and AB = this(2) and BN = this(3) and fin = this(4)
  have "card (N - {B}) < card N" using BN by (meson card_Diff1_less subsumption.prems)
  moreover have "Ξ (N - {B}) ≤ Ξ N"
    by (simp add: Diff_subset finite_incl_le_setsum subsumption.prems)
  ultimately show ?case by linarith
qed

lemma simplify_terminates:
  "wf {(N', N). finite N ∧ simplify N N'}"
   apply (rule wfP_if_measure[of finite simplify "λN. card N + Ξ N"])
  using simplify_finite_measure_decrease by blast


lemma wf_terminates:
  assumes "wf r"
  shows "∃N'.(N', N)∈ r⇧*  ∧ (∀N''. (N'', N')∉ r)"
proof -
  let ?P = "λN. (∃N'.(N', N)∈ r⇧*  ∧ (∀N''. (N'', N')∉ r))"
  have "∀x. (∀y. (y, x) ∈ r ⟶ ?P y) ⟶ ?P x"
    proof clarify
      fix x
      assume H: "∀y. (y, x) ∈ r ⟶ ?P y"
      { assume "∃y. (y, x) ∈ r"
        then obtain y where y: "(y, x) ∈ r" by blast
        then have "?P y" using H by blast
        then have "?P x" using y by (meson rtrancl.rtrancl_into_rtrancl)
      }
      moreover {
        assume "¬(∃y. (y, x) ∈ r)"
        then have "?P x" by auto
      }
      ultimately show "?P x" by blast
    qed
  moreover have "(∀x. (∀y. (y, x) ∈ r ⟶ ?P y) ⟶ ?P x) ⟶ All ?P"
    using assms unfolding wf_def by (rule allE)
  ultimately have "All ?P" by blast
  then show "?P N" by blast
qed

lemma rtranclp_simplify_terminates:
  assumes fin: "finite N"
  shows "∃N'. simplify⇧*⇧* N N' ∧ simplified N'"
proof -
  have H: "{(N', N). finite N ∧ simplify N N'} = {(N', N). simplify N N' ∧ finite N}" by auto
  then have wf: "wf {(N', N). simplify N N' ∧ finite N}"
    using simplify_terminates by (simp add: H)
  obtain N' where N': "(N', N)∈ {(b, a). simplify a b ∧ finite a}⇧*" and
    more: "∀N''. (N'', N')∉ {(b, a). simplify a b ∧ finite a}"
    using Prop_Resolution.wf_terminates[OF wf, of N] by blast
  have 1: "simplify⇧*⇧* N N'"
    using N' by (induction rule: rtrancl.induct) auto
  then have "finite N'" using fin rtranclp_simplify_preserves_finite by blast
  then have 2: "∀N''. ¬simplify N' N''" using more by auto

  show ?thesis using 1 2 by blast
qed

lemma finite_simplified_full1_simp:
  assumes "finite N"
  shows "simplified N ∨ (∃N'. full1 simplify N N')"
  using rtranclp_simplify_terminates[OF assms] unfolding full1_def
  by (metis Nitpick.rtranclp_unfold)

lemma finite_simplified_full_simp:
  assumes "finite N"
  shows "∃N'. full simplify N N'"
  using rtranclp_simplify_terminates[OF assms] unfolding full_def by metis

lemma can_decrease_tree_size_resolution:
  fixes ψ :: "'v state" and tree :: "'v sem_tree"
  assumes "finite (fst ψ)" and "already_used_inv ψ"
  and "partial_interps tree I (fst ψ)"
  and "simplified (fst ψ)"
  shows "∃(tree':: 'v sem_tree) ψ'. resolution⇧*⇧* ψ ψ' ∧ partial_interps tree' I (fst ψ')
    ∧ (sem_tree_size tree' < sem_tree_size tree ∨ sem_tree_size tree = 0)"
  using assms
proof (induct arbitrary: I rule: sem_tree_size)
  case (bigger xs I) note IH = this(1) and finite = this(2) and a_u_i = this(3) and part = this(4)
    and simp = this(5)

  { assume "sem_tree_size xs = 0"
    then have ?case using part by blast
  }

  moreover {
    assume sn0: "sem_tree_size xs > 0"
    obtain ag ad v where xs: "xs = Node v ag ad" using sn0 by (cases xs, auto)
    {
       assume "sem_tree_size ag = 0 ∧ sem_tree_size ad = 0"
       then have ag: "ag = Leaf" and ad: "ad = Leaf" by (cases ag, auto, cases ad, auto)

       then obtain χ χ' where
         χ: "¬ I ∪ {Pos v} ⊨ χ" and
         totχ: "total_over_m (I ∪ {Pos v}) {χ}" and
         χψ: "χ ∈ fst ψ" and
         χ': "¬ I ∪ {Neg v} ⊨ χ'" and
         totχ': "total_over_m (I ∪ {Neg v}) {χ'}" and χ'ψ: "χ' ∈ fst ψ"
         using part unfolding xs by auto
       have Posv: "Pos v ∉# χ" using χ unfolding true_cls_def true_lit_def by auto
       have Negv: "Neg v ∉# χ'" using χ' unfolding true_cls_def true_lit_def by auto
       {
         assume Negχ: "Neg v ∉# χ"
         then have "¬ I ⊨ χ" using χ Posv unfolding true_cls_def true_lit_def by auto
         moreover have "total_over_m I {χ}"
           using Posv Negχ atm_imp_pos_or_neg_lit totχ unfolding total_over_m_def total_over_set_def
           by fastforce
         ultimately have "partial_interps Leaf I (fst ψ)"
           and "sem_tree_size Leaf < sem_tree_size xs"
           and "resolution⇧*⇧* ψ ψ"
           unfolding xs by (auto simp add: χψ)
       }
       moreover {
          assume Posχ: "Pos v ∉# χ'"
          then have Iχ: "¬ I ⊨ χ'" using χ' Posv unfolding true_cls_def true_lit_def by auto
          moreover have "total_over_m I {χ'}"
            using Negv Posχ atm_imp_pos_or_neg_lit totχ'
            unfolding total_over_m_def total_over_set_def by fastforce
          ultimately have "partial_interps Leaf I (fst ψ)"
            and "sem_tree_size Leaf < sem_tree_size xs"
            and "resolution⇧*⇧* ψ ψ"
            using χ'ψ Iχ unfolding xs by auto
       }
       moreover {
          assume neg: "Neg v ∈# χ" and pos: "Pos v ∈# χ'"
          have "count χ (Neg v) = 1"
            using simplified_count[OF simp χψ] neg
            by (simp add: dual_order.antisym)
          have "count χ' (Pos v) = 1"
            using simplified_count[OF simp χ'ψ] pos
            by (simp add: dual_order.antisym)

          obtain C where χC: "χ = add_mset (Neg v) C" and negC: "Neg v ∉# C" and posC: "Pos v ∉# C"
            by (metis (no_types, lifting) One_nat_def Posv ‹count χ (Neg v) = 1›
                ‹count χ' (Pos v) = 1› count_add_mset count_greater_eq_Suc_zero_iff insert_DiffM
                le_numeral_extra(2) nat.inject pos)

          obtain C' where
            χC': "χ' = add_mset (Pos v) C'" and
            posC': "Pos v ∉# C'" and
            negC': "Neg v ∉# C'"
            by (metis (no_types, lifting) Negv One_nat_def ‹count χ' (Pos v) = 1› count_add_mset
                count_eq_zero_iff mset_add nat.inject pos)

          have totC: "total_over_m I {C}"
            using totχ tot_over_m_remove[of I "Pos v" C] negC posC unfolding χC by auto
          have totC': "total_over_m I {C'}"
            using totχ' total_over_m_sum tot_over_m_remove[of I "Neg v" C'] negC' posC'
            unfolding χC' by auto
          have "¬ I ⊨ C + C'"
            using χ χ' χC χC' by auto
          then have part_I_ψ''': "partial_interps Leaf I (fst ψ ∪ {C + C'})"
            using totC totC' ‹¬ I ⊨ C + C'› by (metis Un_insert_right insertI1
              partial_interps.simps(1) total_over_m_sum)
          {
            assume "(add_mset (Pos v) C', add_mset (Neg v) C) ∉ snd ψ"
            then have inf'': "inference ψ (fst ψ ∪ {C + C'}, snd ψ ∪ {(χ', χ)})"
              by (metis χ'ψ χC χC' χψ add_mset_add_single inference_clause.resolution
                  inference_step prod.collapse union_commute)
            obtain N' where full: "full simplify (fst ψ ∪ {C + C'}) N'"
              by (metis finite_simplified_full_simp fst_conv inf'' inference_preserves_finite
                local.finite)
            have "resolution ψ (N', snd ψ ∪ {(χ', χ)})"
              using resolution.intros(2)[OF _ simp full, of "snd ψ" "snd ψ ∪ {(χ', χ)}"] inf''
              by (metis surjective_pairing)
            moreover have "partial_interps Leaf I N'"
              using full_simplify_preserve_partial_tree[OF full part_I_ψ'''] .
            moreover have "sem_tree_size Leaf < sem_tree_size xs" unfolding xs by auto
            ultimately have ?case
              by (metis (no_types) prod.sel(1) rtranclp.rtrancl_into_rtrancl rtranclp.rtrancl_refl)
          }
          moreover {
            assume a: "({#Pos v#} + C', {#Neg v#} + C) ∈ snd ψ"
            then have "(∃χ ∈ fst ψ. (∀I. total_over_m I {C+C'} ⟶ total_over_m I {χ})
                ∧ (∀I. total_over_m I {χ} ⟶ I ⊨ χ ⟶ I ⊨ C' + C)) ∨ tautology (C' + C)"
              proof -
                obtain p where p: "Pos p ∈# ({#Pos v#} + C') ∧ Neg p ∈# ({#Neg v#} + C)
                  ∧((∃χ∈fst ψ. (∀I. total_over_m I {({#Pos v#} + C') - {#Pos p#} + (({#Neg v#} + C) - {#Neg p#})} ⟶ total_over_m I {χ}) ∧ (∀I. total_over_m I {χ} ⟶ I ⊨ χ ⟶ I ⊨ ({#Pos v#} + C') - {#Pos p#} + (({#Neg v#} + C) - {#Neg p#}))) ∨ tautology (({#Pos v#} + C') - {#Pos p#} + (({#Neg v#} + C) - {#Neg p#})))"
                  using a by (blast intro: allE[OF a_u_i[unfolded subsumes_def Ball_def],
                      of " ({#Pos v#} + C', {#Neg v#} + C)"])
                { assume "p ≠ v"
                  then have "Pos p ∈# C' ∧ Neg p ∈# C" using p by force
                  then have ?thesis by auto
                }
                moreover {
                  assume "p = v"
                 then have "?thesis" using p by (metis add.commute add_diff_cancel_left')
                }
                ultimately show ?thesis by auto
              qed
            moreover {
              assume "∃χ ∈ fst ψ. (∀I. total_over_m I {C+C'} ⟶ total_over_m I {χ})
                ∧ (∀I. total_over_m I {χ} ⟶ I ⊨ χ ⟶ I ⊨ C' + C)"
              then obtain θ where
                θ: "θ ∈ fst ψ" and
                tot_θ_CC': "∀I. total_over_m I {C+C'} ⟶ total_over_m I {θ}" and
                θ_inv: "∀I. total_over_m I {θ} ⟶ I ⊨ θ ⟶ I ⊨ C' + C" by blast
              have "partial_interps Leaf I (fst ψ)"
                using tot_θ_CC' θ θ_inv totC totC' ‹¬ I ⊨ C + C'› total_over_m_sum by fastforce
              moreover have "sem_tree_size Leaf < sem_tree_size xs" unfolding xs by auto
              ultimately have ?case by blast
            }
            moreover {
              assume tautCC': "tautology (C' + C)"
              have "total_over_m I {C'+C}" using totC totC' total_over_m_sum by auto
              then have "¬tautology (C' + C)"
                using ‹¬ I ⊨ C + C'› unfolding add.commute[of C C'] total_over_m_def
                unfolding tautology_def by auto
              then have False using tautCC'  unfolding tautology_def by auto
            }
            ultimately have ?case by auto
          }
          ultimately have ?case by auto
       }
       ultimately have ?case using part by (metis (no_types) sem_tree_size.simps(1))
    }
    moreover {
      assume size_ag: "sem_tree_size ag > 0"
      have "sem_tree_size ag < sem_tree_size xs" unfolding xs by auto
      moreover have "partial_interps ag (I ∪ {Pos v}) (fst ψ)"
      and partad: "partial_interps ad (I ∪ {Neg v}) (fst ψ)"
        using part partial_interps.simps(2) unfolding xs by metis+
      moreover
        have "sem_tree_size ag < sem_tree_size xs ⟹ finite (fst ψ) ⟹ already_used_inv ψ
          ⟹ partial_interps ag (I ∪ {Pos v}) (fst ψ) ⟹ simplified (fst ψ)
          ⟹ ∃tree' ψ'. resolution⇧*⇧* ψ ψ' ∧ partial_interps tree' (I ∪ {Pos v}) (fst ψ')
              ∧ (sem_tree_size tree' < sem_tree_size ag ∨ sem_tree_size ag = 0)"
          using IH[of ag "I ∪ {Pos v}"]  by auto
      ultimately obtain ψ' :: "'v state" and tree' :: "'v sem_tree" where
        inf: "resolution⇧*⇧* ψ ψ'"
        and part: "partial_interps tree' (I ∪ {Pos v}) (fst ψ')"
        and size: "sem_tree_size tree' < sem_tree_size ag ∨ sem_tree_size ag = 0"
        using finite part rtranclp.rtrancl_refl a_u_i simp by blast

      have "partial_interps ad (I ∪ {Neg v}) (fst ψ')"
        using rtranclp_resolution_preserve_partial_tree inf partad by fast
      then have "partial_interps (Node v tree' ad) I (fst ψ')" using part by auto
      then have ?case using inf size size_ag part unfolding xs by fastforce
    }
    moreover {
      assume size_ad: "sem_tree_size ad > 0"
      have "sem_tree_size ad < sem_tree_size xs" unfolding xs by auto
      moreover
        have
          partag: "partial_interps ag (I ∪ {Pos v}) (fst ψ)" and
          "partial_interps ad (I ∪ {Neg v}) (fst ψ)"
          using part partial_interps.simps(2) unfolding xs by metis+
      moreover have "sem_tree_size ad < sem_tree_size xs ⟶ finite (fst ψ) ⟶ already_used_inv ψ
        ⟶ ( partial_interps ad (I ∪ {Neg v}) (fst ψ) ⟶ simplified (fst ψ)
        ⟶ (∃tree' ψ'. resolution⇧*⇧* ψ ψ' ∧ partial_interps tree' (I ∪ {Neg v}) (fst ψ')
              ∧ (sem_tree_size tree' < sem_tree_size ad ∨ sem_tree_size ad = 0)))"
        using IH by blast
      ultimately obtain ψ' :: "'v state" and tree' :: "'v sem_tree" where
        inf: "resolution⇧*⇧* ψ ψ'"
        and part: "partial_interps tree' (I ∪ {Neg v}) (fst ψ')"
        and size: "sem_tree_size tree' < sem_tree_size ad ∨ sem_tree_size ad = 0"
        using finite part rtranclp.rtrancl_refl a_u_i simp by blast

      have "partial_interps ag (I ∪ {Pos v}) (fst ψ')"
        using rtranclp_resolution_preserve_partial_tree inf partag by fast
      then have "partial_interps (Node v ag tree') I (fst ψ')" using part by auto
      then have "?case" using inf size size_ad unfolding xs by fastforce
    }
     ultimately have ?case by auto
  }
  ultimately show ?case by auto
qed

lemma resolution_completeness_inv:
  fixes ψ :: "'v ::linorder state"
  assumes
    unsat: "¬satisfiable (fst ψ)" and
    finite: "finite (fst ψ)" and
    a_u_v: "already_used_inv ψ"
  shows "∃ψ'. (resolution⇧*⇧* ψ ψ' ∧ {#} ∈ fst ψ')"
proof -
  obtain tree where "partial_interps tree {} (fst ψ)"
    using partial_interps_build_sem_tree_atms assms by metis
  then show ?thesis
    using unsat finite a_u_v
    proof (induct tree arbitrary: ψ rule: sem_tree_size)
      case (bigger tree ψ) note H = this
      {
        fix χ
        assume tree: "tree = Leaf"
        obtain χ where χ: "¬ {} ⊨ χ" and totχ: "total_over_m {} {χ}" and χψ: "χ ∈ fst ψ"
          using H unfolding tree by auto
        moreover have "{#} = χ"
          using H atms_empty_iff_empty totχ
          unfolding true_cls_def total_over_m_def total_over_set_def by fastforce
        moreover have "resolution⇧*⇧* ψ ψ" by auto
        ultimately have ?case by metis
      }
      moreover {
        fix v tree1 tree2
        assume tree: "tree = Node v tree1 tree2"
        obtain ψ⇩0 where ψ⇩0: "resolution⇧*⇧* ψ ψ⇩0" and simp: "simplified (fst ψ⇩0)"
          proof -
            { assume "simplified (fst ψ)"
              moreover have "resolution⇧*⇧* ψ ψ" by auto
              ultimately have "thesis" using that by blast
            }
            moreover {
              assume "¬simplified (fst ψ)"
              then have "∃ψ'.  full1 simplify (fst ψ) ψ'"
                by (metis Nitpick.rtranclp_unfold bigger.prems(3) full1_def
                  rtranclp_simplify_terminates)
              then obtain N where "full1 simplify (fst ψ) N" by metis
              then have "resolution ψ (N, snd ψ)"
                using resolution.intros(1)[of "fst ψ" N "snd ψ"] by auto
              moreover have "simplified N"
                using ‹full1 simplify (fst ψ) N› unfolding full1_def by blast
              ultimately have ?thesis using that by force
            }
            ultimately show ?thesis by auto
          qed


        have p: "partial_interps tree {} (fst ψ⇩0)"
        and uns: "unsatisfiable (fst ψ⇩0)"
        and f: "finite (fst ψ⇩0)"
        and a_u_v: "already_used_inv ψ⇩0"
             using ψ⇩0 bigger.prems(1) rtranclp_resolution_preserve_partial_tree apply blast
            using ψ⇩0 bigger.prems(2) rtranclp_resolution_preserves_unsat apply blast
           using ψ⇩0 bigger.prems(3) rtranclp_resolution_finite apply blast
          using rtranclp_resolution_already_used_inv[OF ψ⇩0 bigger.prems(4)] by blast
        obtain tree' ψ' where
          inf: "resolution⇧*⇧* ψ⇩0 ψ'" and
          part': "partial_interps tree' {} (fst ψ')" and
          decrease: "sem_tree_size tree' < sem_tree_size tree ∨ sem_tree_size tree = 0"
          using can_decrease_tree_size_resolution[OF f a_u_v p simp] unfolding tautology_def
          by meson
        have s: "sem_tree_size tree' < sem_tree_size tree" using decrease unfolding tree by auto
        have fin: "finite (fst ψ')"
          using f inf rtranclp_resolution_finite by blast
        have unsat: "unsatisfiable (fst ψ')"
          using rtranclp_resolution_preserves_unsat inf uns by metis
        have a_u_i': "already_used_inv ψ'"
          using a_u_v inf rtranclp_resolution_already_used_inv[of ψ⇩0 ψ'] by auto
        have ?case
          using inf rtranclp_trans[of resolution] H(1)[OF s part' unsat fin a_u_i'] ψ⇩0 by blast
      }
      ultimately show ?case by (cases tree, auto)
   qed
qed

lemma resolution_preserves_already_used_inv:
  assumes "resolution S S'"
  and "already_used_inv S"
  shows "already_used_inv S'"
  using assms
  apply (induct rule: resolution.induct)
   apply (rule full1_simplify_already_used_inv; simp)
  apply (rule full_simplify_already_used_inv, simp)
  apply (rule inference_preserves_already_used_inv, simp)
  apply blast
  done

lemma rtranclp_resolution_preserves_already_used_inv:
  assumes "resolution⇧*⇧* S S'"
  and "already_used_inv S"
  shows "already_used_inv S'"
  using assms
  apply (induct rule: rtranclp_induct)
   apply simp
  using resolution_preserves_already_used_inv by fast

lemma resolution_completeness:
  fixes ψ :: "'v ::linorder state"
  assumes unsat: "¬satisfiable (fst ψ)"
  and finite: "finite (fst ψ)"
  and "snd ψ = {}"
  shows "∃ψ'. (resolution⇧*⇧* ψ ψ' ∧ {#} ∈ fst ψ')"
proof -
  have "already_used_inv ψ" unfolding assms by auto
  then show ?thesis using assms resolution_completeness_inv by blast
qed

lemma rtranclp_preserves_sat:
  assumes "simplify⇧*⇧* S S'"
  and "satisfiable S"
  shows "satisfiable S'"
  using assms apply induction
   apply simp
  by (meson satisfiable_carac satisfiable_def simplify_preserve_models_eq)

lemma resolution_preserves_sat:
  assumes "resolution S S'"
  and "satisfiable (fst S)"
  shows "satisfiable (fst S')"
  using assms apply (induction rule: resolution.induct)
   using rtranclp_preserves_sat tranclp_into_rtranclp unfolding full1_def apply fastforce
  by (metis fst_conv full_def inference_preserve_models rtranclp_preserves_sat
    satisfiable_carac' satisfiable_def)

lemma rtranclp_resolution_preserves_sat:
  assumes "resolution⇧*⇧* S S'"
  and "satisfiable (fst S)"
  shows "satisfiable (fst S')"
  using assms apply (induction rule: rtranclp_induct)
   apply simp
  using resolution_preserves_sat by blast

lemma resolution_soundness:
  fixes ψ :: "'v ::linorder state"
  assumes "resolution⇧*⇧* ψ ψ'" and "{#} ∈ fst ψ'"
  shows "unsatisfiable (fst ψ)"
  using assms by (meson rtranclp_resolution_preserves_sat satisfiable_def true_cls_empty
    true_clss_def)

lemma resolution_soundness_and_completeness:
fixes ψ :: "'v ::linorder state"
assumes finite: "finite (fst ψ)"
and snd: "snd ψ = {}"
shows "(∃ψ'. (resolution⇧*⇧* ψ ψ' ∧ {#} ∈ fst ψ')) ⟷ unsatisfiable (fst ψ)"
  using assms resolution_completeness resolution_soundness by metis

lemma simplified_falsity:
  assumes simp: "simplified ψ"
  and "{#} ∈ ψ"
  shows "ψ = {{#}}"
proof (rule ccontr)
  assume H: "¬ ?thesis"
  then obtain χ where "χ ∈ ψ" and "χ ≠ {#}" using assms(2) by blast
  then have "{#} ⊂# χ" by (simp add: subset_mset.zero_less_iff_neq_zero)
  then have "simplify ψ (ψ - {χ})"
    using simplify.subsumption[OF assms(2) ‹{#} ⊂# χ› ‹χ ∈ ψ›] by blast
  then show False using simp by blast
qed


lemma simplify_falsity_in_preserved:
  assumes "simplify χs χs'"
  and "{#} ∈ χs"
  shows "{#} ∈ χs'"
  using assms
  by induction auto

lemma rtranclp_simplify_falsity_in_preserved:
  assumes "simplify⇧*⇧* χs χs'"
  and "{#} ∈ χs"
  shows "{#} ∈ χs'"
  using assms
  by induction (auto intro: simplify_falsity_in_preserved)

lemma resolution_falsity_get_falsity_alone:
  assumes "finite (fst ψ)"
  shows "(∃ψ'. (resolution⇧*⇧* ψ ψ' ∧ {#} ∈ fst ψ')) ⟷ (∃a_u_v. resolution⇧*⇧* ψ ({{#}}, a_u_v))"
    (is "?A ⟷ ?B")
proof
  assume ?B
  then show ?A by auto
next
  assume ?A
  then obtain χs a_u_v where χs: "resolution⇧*⇧* ψ (χs, a_u_v)" and F: "{#} ∈ χs" by auto
  { assume "simplified χs"
    then have ?B using simplified_falsity[OF _ F] χs by blast
  }
  moreover {
    assume "¬ simplified χs"
    then obtain χs' where "full1 simplify χs χs'"
       by (metis χs assms finite_simplified_full1_simp fst_conv rtranclp_resolution_finite)
    then have "{#} ∈ χs'"
      unfolding full1_def by (meson F rtranclp_simplify_falsity_in_preserved
        tranclp_into_rtranclp)
    then have ?B
      by (metis χs ‹full1 simplify χs χs'› fst_conv full1_simp resolution_always_simplified
        rtranclp.rtrancl_into_rtrancl simplified_falsity)
  }
  ultimately show ?B by blast
qed

theorem resolution_soundness_and_completeness':
  fixes ψ :: "'v ::linorder state"
  assumes
    finite: "finite (fst ψ)"and
    snd: "snd ψ = {}"
  shows "(∃a_u_v. (resolution⇧*⇧* ψ ({{#}}, a_u_v))) ⟷ unsatisfiable (fst ψ)"
  using assms resolution_completeness resolution_soundness resolution_falsity_get_falsity_alone
  by metis

end