Theory Ordered_Resolution_Prover.Herbrand_Interpretation

(*  Title:       Herbrand Interpretation
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
    Maintainer:  Jasmin Blanchette <j.c.blanchette at vu.nl>
*)

section ‹Herbrand Intepretation›

theory Herbrand_Interpretation
  imports Clausal_Logic
begin

text ‹
The material formalized here corresponds roughly to Sections 2.2 (``Herbrand
Interpretations'') of Bachmair and Ganzinger, excluding the formula and term
syntax.

A Herbrand interpretation is a set of ground atoms that are to be considered true.
›

type_synonym 'a interp = "'a set"

definition true_lit :: "'a interp  'a literal  bool" (infix "⊨l" 50) where
  "I ⊨l L  (if is_pos L then (λP. P) else Not) (atm_of L  I)"

lemma true_lit_simps[simp]:
  "I ⊨l Pos A  A  I"
  "I ⊨l Neg A  A  I"
  unfolding true_lit_def by auto

lemma true_lit_iff[iff]: "I ⊨l L  (A. L = Pos A  A  I  L = Neg A  A  I)"
  by (cases L) simp+

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

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

lemma true_cls_singleton[iff]: "I  {#L#}  I ⊨l L"
  unfolding true_cls_def by simp

lemma true_cls_add_mset[iff]: "I  add_mset C D  I ⊨l C  I  D"
  unfolding true_cls_def by auto

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

lemma true_cls_mono: "set_mset C  set_mset D  I  C  I  D"
  unfolding true_cls_def subset_eq by metis

lemma
  assumes "I  J"
  shows
    false_to_true_imp_ex_pos: "¬ I  C  J  C  A  J. Pos A ∈# C" and
    true_to_false_imp_ex_neg: "I  C  ¬ J  C  A  J. Neg A ∈# C"
  using assms unfolding subset_iff true_cls_def by (metis literal.collapse true_lit_simps)+

lemma true_cls_replicate_mset[iff]: "I  replicate_mset n L  n  0  I ⊨l L"
  by (simp add: true_cls_def)

lemma pos_literal_in_imp_true_cls[intro]: "Pos A ∈# C  A  I  I  C"
  using true_cls_def by blast

lemma neg_literal_notin_imp_true_cls[intro]: "Neg A ∈# C  A  I  I  C"
  using true_cls_def by blast

lemma pos_neg_in_imp_true: "Pos A ∈# C  Neg A ∈# C  I  C"
  using true_cls_def by blast

definition true_clss :: "'a interp  'a clause set  bool" (infix "⊨s" 50) where
  "I ⊨s CC  (C  CC. I  C)"

lemma true_clss_empty[iff]: "I ⊨s {}"
  by (simp add: true_clss_def)

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

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

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

lemma true_clss_Union[iff]: "I ⊨s  CCC  (CC  CCC. I ⊨s CC)"
  unfolding true_clss_def by simp

lemma true_clss_mono: "DD  CC  I ⊨s CC  I ⊨s DD"
  by (simp add: subsetD true_clss_def)

lemma true_clss_mono_strong: "(D  DD. C  CC. C ⊆# D)  I ⊨s CC  I ⊨s DD"
  unfolding true_clss_def true_cls_def true_lit_def by (meson mset_subset_eqD)

lemma true_clss_subclause: "C ⊆# D  I ⊨s {C}  I ⊨s {D}"
  by (rule true_clss_mono_strong[of _ "{C}"]) auto

abbreviation satisfiable :: "'a clause set  bool" where
  "satisfiable CC  I. I ⊨s CC"

lemma satisfiable_antimono: "CC  DD  satisfiable DD  satisfiable CC"
  using true_clss_mono by blast

lemma unsatisfiable_mono: "CC  DD  ¬ satisfiable CC  ¬ satisfiable DD"
  using satisfiable_antimono by blast

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

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

lemma true_cls_mset_singleton[iff]: "I ⊨m {#C#}  I  C"
  by (simp add: true_cls_mset_def)

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

lemma true_cls_mset_Union[iff]: "I ⊨m # CCC  (CC ∈# CCC. I ⊨m CC)"
  unfolding true_cls_mset_def by simp

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

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

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

lemma true_cls_mset_mono_strong: "(D ∈# DD. C ∈# CC. C ⊆# D)  I ⊨m CC  I ⊨m DD"
  unfolding true_cls_mset_def true_cls_def true_lit_def by (meson mset_subset_eqD)

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

lemma true_clss_mset_set[simp]: "finite CC  I ⊨m mset_set CC  I ⊨s CC"
  unfolding true_clss_def true_cls_mset_def by auto

lemma true_cls_mset_true_cls: "I ⊨m CC  C ∈# CC  I  C"
  using true_cls_mset_def by auto

end