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