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