Theory CNF_Formulas_Sema

theory CNF_Formulas_Sema
imports CNF_Sema CNF_Formulas Sema
begin

lemma nnf_semantics: "𝒜 ⊨ nnf F ⟷ 𝒜 ⊨ F"
  by(induction F rule: nnf.induct; simp)
  
lemma cnf_semantics: "is_nnf F ⟹ cnf_semantics 𝒜 (cnf F) ⟷ 𝒜 ⊨ F"
  by(induction F rule: cnf.induct; simp add: cnf_semantics_def clause_semantics_def ball_Un; metis Un_iff)
  (* surprisingly, the solvers are smarter if this one is done on mutlisets.*)

lemma cnf_form_semantics: 
  fixes F :: "'a formula"
  assumes nnf: "is_nnf F"
  shows "𝒜 ⊨ cnf_form_of F ⟷ 𝒜 ⊨ F"
proof -
  define cnf_semantics_list
    where "cnf_semantics_list 𝒜 S ⟷ (∀s ∈ set S. ∃l ∈ set s. lit_semantics 𝒜 (l :: 'a literal))"
    for 𝒜 S
  have tcn: "cnf F = set (map set (cnf_lists F))" using nnf
    by(induction F rule: cnf.induct) (auto simp add: image_UN image_comp comp_def )
  have "𝒜 ⊨ F ⟷ cnf_semantics 𝒜 (cnf F)" using cnf_semantics[OF nnf] by simp
  also have "… = cnf_semantics 𝒜 (set (map set (cnf_lists F)))" unfolding tcn ..
  also have "… = cnf_semantics_list 𝒜 (cnf_lists F)"
    unfolding cnf_semantics_def clause_semantics_def cnf_semantics_list_def by fastforce
  also have "… = 𝒜 ⊨ (cnf_form_of F)" using nnf
    by(induction F rule: cnf_lists.induct;
       simp add: cnf_semantics_list_def cnf_form_of_defs  ball_Un bex_Un)
  finally show ?thesis by simp
qed
  
corollary "∃G. 𝒜 ⊨ F ⟷ 𝒜 ⊨ G ∧ is_cnf G"
  using cnf_form_of_is cnf_form_semantics is_nnf_nnf nnf_semantics by blast

end