Theory MLSSmf_to_MLSS_Correctness

theory MLSSmf_to_MLSS_Correctness
  imports MLSSmf_to_MLSS_Soundness MLSSmf_to_MLSS_Completeness
begin

fun reduce :: "('v, 'f) MLSSmf_clause ⇒ ('v, 'f) Composite pset_fm set set" where
  "reduce 𝒞 = normalized_MLSSmf_clause.reduced_dnf 𝒞"

fun interp_DNF :: "(('v, 'f) Composite ⇒ hf) ⇒ ('v, 'f) Composite pset_fm set set ⇒ bool" where
  "interp_DNF ℳ clauses ⟷ (∃clause ∈ clauses. ∀lt ∈ clause. interp I⇩s⇩a ℳ lt)"

corollary MLSSmf_to_MLSS_correct:
  assumes "norm_clause 𝒞"
    shows "(∃M⇩v M⇩f. I⇩c⇩l M⇩v M⇩f 𝒞) ⟷ (∃ℳ. interp_DNF ℳ (reduce 𝒞))"
proof
  from assms interpret normalized_MLSSmf_clause 𝒞 by unfold_locales
  assume "∃M⇩v M⇩f. I⇩c⇩l M⇩v M⇩f 𝒞"
  with MLSSmf_to_MLSS_soundness obtain ℳ where "is_model_for_reduced_dnf ℳ"
    using assms by blast
  then have "interp_DNF ℳ (reduce 𝒞)" unfolding is_model_for_reduced_dnf_def by simp
  then show "∃ℳ. interp_DNF ℳ (reduce 𝒞)" by blast
next
  from assms interpret normalized_MLSSmf_clause 𝒞 by unfold_locales
  assume "∃ℳ. interp_DNF ℳ (reduce 𝒞)"
  then obtain ℳ where "interp_DNF ℳ (reduce 𝒞)" by blast
  then have "is_model_for_reduced_dnf ℳ" unfolding is_model_for_reduced_dnf_def by simp
  with MLSSmf_to_MLSS_completeness show "∃M⇩v M⇩f. I⇩c⇩l M⇩v M⇩f 𝒞" by blast
qed

end