Theory Ordered_Resolution_Prover.Clausal_Logic

(* Title:        Clausal Logic
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
    Author:      Mathias Fleury <mathias.fleury at mpi-inf.mpg.de>, 2014
    Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

section ‹Clausal Logic›

theory Clausal_Logic
  imports Nested_Multisets_Ordinals.Multiset_More
begin

text ‹
Resolution operates of clauses, which are disjunctions of literals. The material formalized here
corresponds roughly to Sections 2.1 (``Formulas and Clauses'') of Bachmair and Ganzinger, excluding
the formula and term syntax.
›


subsection ‹Literals›

text ‹
Literals consist of a polarity (positive or negative) and an atom, of type @{typ 'a}.
›

datatype 'a literal =
  is_pos: Pos (atm_of: 'a)
| Neg (atm_of: 'a)

abbreviation is_neg :: "'a literal  bool" where
  "is_neg L  ¬ is_pos L"

lemma Pos_atm_of_iff[simp]: "Pos (atm_of L) = L  is_pos L"
  by (cases L) simp+

lemma Neg_atm_of_iff[simp]: "Neg (atm_of L) = L  is_neg L"
  by (cases L) simp+

lemma set_literal_atm_of: "set_literal L = {atm_of L}"
  by (cases L) simp+

lemma ex_lit_cases: "(L. P L)  (A. P (Pos A)  P (Neg A))"
  by (metis literal.exhaust)

instantiation literal :: (type) uminus
begin

definition uminus_literal :: "'a literal  'a literal" where
  "uminus L = (if is_pos L then Neg else Pos) (atm_of L)"

instance ..

end

lemma
  uminus_Pos[simp]: "- Pos A = Neg A" and
  uminus_Neg[simp]: "- Neg A = Pos A"
  unfolding uminus_literal_def by simp_all

lemma atm_of_uminus[simp]: "atm_of (-L) = atm_of L"
  by (case_tac L, auto)

lemma uminus_of_uminus_id[simp]: "- (- (x :: 'v literal)) = x"
  by (simp add: uminus_literal_def)

lemma uminus_not_id[simp]: "x  - (x:: 'v literal)"
  by (case_tac x) auto

lemma uminus_not_id'[simp]: "- x  (x:: 'v literal)"
  by (case_tac x, auto)

lemma uminus_eq_inj[iff]: "- (a::'v literal) = - b  a = b"
  by (case_tac a; case_tac b) auto+

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

lemma is_pos_neg_not_is_pos: "is_pos (- L)  ¬ is_pos L"
  by (cases L) auto

instantiation literal :: (preorder) preorder
begin

definition less_literal :: "'a literal  'a literal  bool" where
  "less_literal L M  atm_of L < atm_of M  atm_of L  atm_of M  is_neg L < is_neg M"

definition less_eq_literal :: "'a literal  'a literal  bool" where
  "less_eq_literal L M  atm_of L < atm_of M  atm_of L  atm_of M  is_neg L  is_neg M"

instance
  apply intro_classes
  unfolding less_literal_def less_eq_literal_def by (auto intro: order_trans simp: less_le_not_le)

end

instantiation literal :: (order) order
begin

instance
  by intro_classes (auto simp: less_eq_literal_def intro: literal.expand)

end

lemma pos_less_neg[simp]: "Pos A < Neg A"
  unfolding less_literal_def by simp

lemma pos_less_pos_iff[simp]: "Pos A < Pos B  A < B"
  unfolding less_literal_def by simp

lemma pos_less_neg_iff[simp]: "Pos A < Neg B  A  B"
  unfolding less_literal_def by (auto simp: less_le_not_le)

lemma neg_less_pos_iff[simp]: "Neg A < Pos B  A < B"
  unfolding less_literal_def by simp

lemma neg_less_neg_iff[simp]: "Neg A < Neg B  A < B"
  unfolding less_literal_def by simp

lemma pos_le_neg[simp]: "Pos A  Neg A"
  unfolding less_eq_literal_def by simp

lemma pos_le_pos_iff[simp]: "Pos A  Pos B  A  B"
  unfolding less_eq_literal_def by (auto simp: less_le_not_le)

lemma pos_le_neg_iff[simp]: "Pos A  Neg B  A  B"
  unfolding less_eq_literal_def by (auto simp: less_imp_le)

lemma neg_le_pos_iff[simp]: "Neg A  Pos B  A < B"
  unfolding less_eq_literal_def by simp

lemma neg_le_neg_iff[simp]: "Neg A  Neg B  A  B"
  unfolding less_eq_literal_def by (auto simp: less_imp_le)

lemma leq_imp_less_eq_atm_of: "L  M  atm_of L  atm_of M"
  unfolding less_eq_literal_def using less_imp_le by blast

instantiation literal :: (linorder) linorder
begin

instance
  apply intro_classes
  unfolding less_eq_literal_def less_literal_def by auto

end

instantiation literal :: (wellorder) wellorder
begin

instance
proof intro_classes
  fix P :: "'a literal  bool" and L :: "'a literal"
  assume ih: "L. (M. M < L  P M)  P L"
  have "x. (y. y < x  P (Pos y)  P (Neg y))  P (Pos x)  P (Neg x)"
    by (rule conjI[OF ih ih])
      (auto simp: less_literal_def atm_of_def split: literal.splits intro: ih)
  then have "A. P (Pos A)  P (Neg A)"
    by (rule less_induct) blast
  then show "P L"
    by (cases L) simp+
qed

end


subsection ‹Clauses›

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

type_synonym 'a clause = "'a literal multiset"

abbreviation map_clause :: "('a  'b)  'a clause  'b clause" where
  "map_clause f  image_mset (map_literal f)"

abbreviation rel_clause :: "('a  'b  bool)  'a clause  'b clause  bool" where
  "rel_clause R  rel_mset (rel_literal R)"

abbreviation poss :: "'a multiset  'a clause" where "poss AA  {#Pos A. A ∈# AA#}"
abbreviation negs :: "'a multiset  'a clause" where "negs AA  {#Neg A. A ∈# AA#}"

lemma Max_in_lits: "C  {#}  Max_mset C ∈# C"
  by simp

lemma Max_atm_of_set_mset_commute: "C  {#}  Max (atm_of ` set_mset C) = atm_of (Max_mset C)"
  by (rule mono_Max_commute[symmetric]) (auto simp: mono_def less_eq_literal_def)

lemma Max_pos_neg_less_multiset:
  assumes max: "Max_mset C = Pos A" and neg: "Neg A ∈# D"
  shows "C < D"
proof -
  have "Max_mset C < Neg A"
    using max by simp
  then show ?thesis
    using neg by (metis (no_types) Max_less_iff empty_iff ex_gt_imp_less_multiset finite_set_mset)
qed

lemma pos_Max_imp_neg_notin: "Max_mset C = Pos A  Neg A ∉# C"
  using Max_pos_neg_less_multiset by blast

lemma less_eq_Max_lit: "C  {#}  C  D  Max_mset C  Max_mset D"
proof (unfold less_eq_multisetHO)
  assume
    ne: "C  {#}" and
    ex_gt: "x. count D x < count C x  (y > x. count C y < count D y)"
  from ne have "Max_mset C ∈# C"
    by (fast intro: Max_in_lits)
  then have "l. l ∈# D  ¬ l < Max_mset C"
    using ex_gt by (metis count_greater_zero_iff count_inI less_not_sym)
  then have "¬ Max_mset D < Max_mset C"
    by (metis Max.coboundedI[OF finite_set_mset] le_less_trans)
  then show ?thesis
    by simp
qed

definition atms_of :: "'a clause  'a set" where
  "atms_of C = atm_of ` set_mset C"

lemma atms_of_empty[simp]: "atms_of {#} = {}"
  unfolding atms_of_def by simp

lemma atms_of_singleton[simp]: "atms_of {#L#} = {atm_of L}"
  unfolding atms_of_def by auto

lemma atms_of_add_mset[simp]: "atms_of (add_mset a A) = insert (atm_of a) (atms_of A)"
  unfolding atms_of_def by auto

lemma atms_of_union_mset[simp]: "atms_of (A ∪# B) = atms_of A  atms_of B"
  unfolding atms_of_def by auto

lemma finite_atms_of[iff]: "finite (atms_of C)"
  by (simp add: atms_of_def)

lemma atm_of_lit_in_atms_of: "L ∈# C  atm_of L  atms_of C"
  by (simp add: atms_of_def)

lemma atms_of_plus[simp]: "atms_of (C + D) = atms_of C  atms_of D"
  unfolding atms_of_def by auto

lemma in_atms_of_minusD: "x  atms_of (A - B)  x  atms_of A"
  by (auto simp: atms_of_def dest: in_diffD)

lemma pos_lit_in_atms_of: "Pos A ∈# C  A  atms_of C"
  unfolding atms_of_def by force

lemma neg_lit_in_atms_of: "Neg A ∈# C  A  atms_of C"
  unfolding atms_of_def by force

lemma atm_imp_pos_or_neg_lit: "A  atms_of C  Pos A ∈# C  Neg A ∈# C"
  unfolding atms_of_def image_def mem_Collect_eq by (metis Neg_atm_of_iff Pos_atm_of_iff)

lemma atm_iff_pos_or_neg_lit: "A  atms_of L  Pos A ∈# L  Neg A ∈# L"
  by (auto intro: pos_lit_in_atms_of neg_lit_in_atms_of dest: atm_imp_pos_or_neg_lit)

lemma atm_of_eq_atm_of: "atm_of L = atm_of L'  (L = L'  L = -L')"
  by (cases L; cases L') auto

lemma atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set: "atm_of L  atm_of ` I  (L  I  -L  I)"
  by (auto intro: rev_image_eqI simp: atm_of_eq_atm_of)

lemma lits_subseteq_imp_atms_subseteq: "set_mset C  set_mset D  atms_of C  atms_of D"
  unfolding atms_of_def by blast

lemma atms_empty_iff_empty[iff]: "atms_of C = {}  C = {#}"
  unfolding atms_of_def image_def Collect_empty_eq by auto

lemma
  atms_of_poss[simp]: "atms_of (poss AA) = set_mset AA" and
  atms_of_negs[simp]: "atms_of (negs AA) = set_mset AA"
  unfolding atms_of_def image_def by auto

lemma less_eq_Max_atms_of: "C  {#}  C  D  Max (atms_of C)  Max (atms_of D)"
  unfolding atms_of_def
  by (metis Max_atm_of_set_mset_commute leq_imp_less_eq_atm_of less_eq_Max_lit
      less_eq_multiset_empty_right)

lemma le_multiset_Max_in_imp_Max:
  "Max (atms_of D) = A  C  D  A  atms_of C  Max (atms_of C) = A"
  by (metis Max.coboundedI[OF finite_atms_of] atms_of_def empty_iff eq_iff image_subsetI
      less_eq_Max_atms_of set_mset_empty subset_Compl_self_eq)

lemma atm_of_Max_lit[simp]: "C  {#}  atm_of (Max_mset C) = Max (atms_of C)"
  unfolding atms_of_def Max_atm_of_set_mset_commute ..

lemma Max_lit_eq_pos_or_neg_Max_atm:
  "C  {#}  Max_mset C = Pos (Max (atms_of C))  Max_mset C = Neg (Max (atms_of C))"
  by (metis Neg_atm_of_iff Pos_atm_of_iff atm_of_Max_lit)

lemma atms_less_imp_lit_less_pos: "(B. B  atms_of C  B < A)  L ∈# C  L < Pos A"
  unfolding atms_of_def less_literal_def by force

lemma atms_less_eq_imp_lit_less_eq_neg: "(B. B  atms_of C  B  A)  L ∈# C  L  Neg A"
  unfolding less_eq_literal_def by (simp add: atm_of_lit_in_atms_of)

end