Theory CNF_Semantics_Supplement

(*
  Author: Fred Kurz
*)
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

― ‹ NOTE This follows by contraposition from the previous lemma 
‹not_model_if_exists_unmodeled_singleton_clause›. ›
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

― ‹ NOTE This is essentially the ‹⇒› direction of the compactness theorem when treating CNFs as sets
of formulas (sets of disjunctions in this case). ›
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

― ‹ NOTE Show that any clause ‹C› containing a subset ‹C› for which all literals
  ‹L› evaluate to ‹False› for the given valuation ‹𝒜›, then the clause
  semantics evaluation can be reduced to the set ‹C - C'› where all literals of 
  ‹C'› have been removed. ›
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