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_mono: "DD ⊆ CC ⟹ I ⊨s CC ⟹ I ⊨s DD"
by (simp add: subsetD true_clss_def)
abbreviation satisfiable :: "'a clause set ⇒ bool" where
"satisfiable CC ≡ ∃I. I ⊨s CC"
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_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_clss_set_mset[iff]: "I ⊨s set_mset CC ⟷ I ⊨m 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