Theory CNF_Semantics_Supplement
theory CNF_Semantics_Supplement
imports "Propositional_Proof_Systems.CNF_Formulas_Sema" "CNF_Supplement"
begin
lemma not_model_if_exists_unmodeled_singleton_clause:
assumes "is_cnf F"
and "{L} ∈ cnf F"
and "¬lit_semantics ν L"
shows "¬ν ⊨ F"
proof (rule ccontr)
assume "¬¬ν ⊨ F"
then have a: "ν ⊨ F"
by blast
moreover have "is_nnf F"
using is_nnf_cnf[OF assms(1)]
by simp
moreover {
let ?C = "{L}"
have "¬(∃L'. L' ∈ ?C ∧ lit_semantics ν L')"
using assms(3)
by fast
then have "¬(∀C ∈ cnf F. ∃L. L ∈ C ∧ lit_semantics ν L)"
using assms(2)
by blast
hence "¬cnf_semantics ν (cnf F)"
unfolding cnf_semantics_def clause_semantics_def
by fast
}
ultimately have "¬ ν ⊨ F"
using cnf_semantics
by blast
thus False
using a
by blast
qed
corollary model_then_all_singleton_clauses_modelled:
assumes "is_cnf F"
and "{L} ∈ cnf F"
and "ν ⊨ F"
shows "lit_semantics ν L"
using not_model_if_exists_unmodeled_singleton_clause[OF assms(1, 2)] assms(3)
by blast
lemma model_for_cnf_is_model_of_all_subsets:
assumes "cnf_semantics ν ℱ"
and "ℱ' ⊆ ℱ"
shows "cnf_semantics ν ℱ'"
proof -
{
fix C
assume "C ∈ ℱ'"
then have "C ∈ ℱ"
using assms(2)
by blast
then have "clause_semantics ν C"
using assms(1)
unfolding cnf_semantics_def
by blast
}
thus ?thesis
unfolding cnf_semantics_def
by blast
qed
lemma cnf_semantics_monotonous_in_cnf_subsets_if:
assumes "𝒜 ⊨ Φ"
and "is_cnf Φ"
and "cnf Φ' ⊆ cnf Φ"
shows "cnf_semantics 𝒜 (cnf Φ')"
proof -
{
have "is_nnf Φ"
using is_nnf_cnf[OF assms(2)].
hence "cnf_semantics 𝒜 (cnf Φ)"
using cnf_semantics assms(1)
by blast
}
thus ?thesis
using model_for_cnf_is_model_of_all_subsets[OF _ assms(3)]
by simp
qed
corollary modelling_relation_monotonous_in_cnf_subsets_if:
assumes "𝒜 ⊨ Φ"
and "is_cnf Φ"
and "is_cnf Φ'"
and "cnf Φ' ⊆ cnf Φ"
shows "𝒜 ⊨ Φ'"
proof -
have "cnf_semantics 𝒜 (cnf Φ')"
using cnf_semantics_monotonous_in_cnf_subsets_if[OF assms(1, 2, 4)].
thus ?thesis
using cnf_semantics is_nnf_cnf[OF assms(3)]
by blast
qed
lemma lit_semantics_reducible_to_subset_if:
assumes "C' ⊆ C"
and "∀L ∈ C'. ¬lit_semantics 𝒜 L"
shows "clause_semantics 𝒜 C = clause_semantics 𝒜 (C - C')"
unfolding clause_semantics_def
using assms
by fast
end