Theory Resolution_Compl_SC_Full

theory Resolution_Compl_SC_Full
imports LSC_Resolution Resolution SC_Sema Compactness
begin

theorem Resolution_complete:
  fixes S :: "'a :: countable formula set"
  assumes val: "S ⊫ F"
  shows "⋃((cnf ∘ nnf) ` ({❙¬F} ∪ S)) ⊢ □"
  (* look: S may be infinite. *)
proof -
  let ?mun = "λs. ⋃((cnf ∘ nnf) ` s)"
  (* note: there's an alternate version of this proof with CSC_Resolution_pre and the CNF_Semantics *)
  from compact_entailment[OF val] obtain S'' where fin: "finite S''" and su: "S'' ⊆ S" and val': " S'' ⊫ F" by blast
  from fin obtain S' where S: "S'' = set_mset S'" using finite_set_mset_mset_set by blast
  have cnf: "∀F ∈ set_mset (image_mset (cnf_form_of ∘ nnf) (❙¬ F, S')). is_cnf F" by(simp add: cnf_form_of_is is_nnf_nnf)
  note entailment_def[simp]
  from val' have "S'' ⊫ ❙¬(❙¬F)" by simp
  hence "S' ⇒ {#❙¬(❙¬F)#}"
    unfolding SC_sound_complete sequent_intuitonistic_semantics S .
  hence "❙¬F, S' ⇒ {#}" by (simp add: NotR_inv)
  hence "image_mset nnf (❙¬F, S') ⇒ {#}" using LSC_NNF SC_LSC by blast
  hence "image_mset nnf (❙¬F, S') ⇒⇩n" by (simp add: SC_LSC is_nnf_nnf)
  with LSC_Resolution have "⋃(cnf ` nnf ` set_mset (image_mset nnf (❙¬ F, S'))) ⊢ □"  .
  hence "?mun ({❙¬ F} ∪ S'') ⊢ □" 
    unfolding set_image_mset image_comp comp_def S is_nnf_nnf_id[OF is_nnf_nnf] by simp
  from Resolution_weaken[OF this, of "?mun S"] show ?thesis using su by (metis UN_Un Un_left_commute sup.order_iff)
qed

end