Theory MLSS_Decidable

theory MLSS_Decidable
  imports Place_Realisation Syntactic_Description
begin

theorem MLSS_decidable:
  "(∃𝒜. satisfiable_normalized_MLSS_clause 𝒞 𝒜) ⟷
   (∃PI at⇩p. adequate_place_framework 𝒞 PI at⇩p)"  
proof
  assume "∃𝒜. satisfiable_normalized_MLSS_clause 𝒞 𝒜"
  then obtain 𝒜 where "satisfiable_normalized_MLSS_clause 𝒞 𝒜" by blast
  with satisfiable_normalized_MLSS_clause.syntactic_description_is_adequate
  show "∃PI at⇩p. adequate_place_framework 𝒞 PI at⇩p" by blast
next
  assume "∃PI at⇩p. adequate_place_framework 𝒞 PI at⇩p"
  then obtain PI at⇩p where "adequate_place_framework 𝒞 PI at⇩p" by blast
  then have "finite PI"
    by (simp add: adequate_place_framework.finite_PI)
  with u_exists[of PI "card PI"] obtain u
    where "(∀x∈PI. ∀y∈PI. x ≠ y ⟶ u x ≠ u y) ∧ (∀x∈PI. card PI ≤ hcard (u x))"
    by presburger
  with ‹adequate_place_framework 𝒞 PI at⇩p›
  have "place_realization 𝒞 PI at⇩p u"
    unfolding place_realization_def place_realization_axioms_def by blast
  with place_realization.ℳ_sat_𝒞 obtain ℳ where ℳ: "∀lt∈𝒞. interp I⇩s⇩a ℳ lt"
    by blast
  have "satisfiable_normalized_MLSS_clause 𝒞 ℳ"
  proof -
    from ‹adequate_place_framework 𝒞 PI at⇩p› have "normalized_MLSS_clause 𝒞"
      unfolding adequate_place_framework_def by blast
    moreover
    from ‹normalized_MLSS_clause 𝒞› have "finite (⋃ (vars ` 𝒞))"
      unfolding normalized_MLSS_clause_def
      by (simp add: finite_vars_fm)
    then have "proper_Venn_regions (⋃ (vars ` 𝒞))"
      by unfold_locales blast
    ultimately
    show ?thesis
      unfolding satisfiable_normalized_MLSS_clause_def satisfiable_normalized_MLSS_clause_axioms_def
      using ℳ by blast
  qed
  then show "∃𝒜. satisfiable_normalized_MLSS_clause 𝒞 𝒜" by blast
qed

end