Theory Resolution_Compl_Consistency

theory Resolution_Compl_Consistency
imports Resolution Consistency CNF_Formulas CNF_Formulas_Sema
begin
 
lemma OrI2': "(¬P ⟹ Q) ⟹ P ∨ Q" by auto
    
lemma atomD: "Atom k ∈ S ⟹ {Pos k} ∈ ⋃(cnf ` S)" "Not (Atom k) ∈ S ⟹ {Neg k} ∈ ⋃(cnf ` S)" by force+
      
lemma pcp_disj: (* this is the same as for LSC ⇒ Res. but I don't want to make the proof of that too, so I'm keeping my code duplication *)
 "⟦F ❙∨ G ∈ Γ; (∀xa. (xa = F ∨ xa ∈ Γ) ⟶ is_cnf xa) ⟶ (cnf F ∪ (⋃x∈Γ. cnf x) ⊢ □); (∀xa. (xa = G ∨ xa ∈ Γ) ⟶ is_cnf xa) ⟶ (cnf G ∪ (⋃x∈Γ. cnf x) ⊢ □); ∀x∈Γ. is_cnf x⟧
    ⟹ (⋃x∈Γ. cnf x) ⊢ □"
proof goal_cases
  case 1
  from 1(1,4) have "is_cnf (F ❙∨ G)" by blast
  hence db: "is_disj F" "is_lit_plus F" "is_disj G" by(cases F; simp)+
  hence "is_cnf F ∧ is_cnf G" by(cases F; cases G; simp)
  with 1 have IH: "(⋃(cnf ` (F ▹ Γ))) ⊢ □" "(⋃(cnf ` (G ▹ Γ))) ⊢ □" by simp_all
  let ?Γ = "(⋃(cnf ` Γ))"
  from IH have IH_readable: "cnf F ∪ ?Γ ⊢ □" "cnf G ∪ ?Γ ⊢ □" by auto
  show ?case proof(cases "cnf F = {} ∨ cnf G = {}")
    case True
    hence "cnf (F ❙∨ G) = {}" by auto
    thus ?thesis using True IH by auto
  next
    case False
    then obtain S T where ST: "cnf F = {S}" "cnf G = {T}"
      using cnf_disj_ex db(1,3) (* try applying meson here. It's weird. and sledgehammer even suggests it. *) by metis
    (* hint: card S ≤ 1 *)
    hence R: "cnf (F ❙∨ G) = { S ∪ T }" by simp
    have "⟦S▹?Γ ⊢ □; T▹?Γ ⊢ □⟧ ⟹ S ∪ T▹ ?Γ ⊢ □" proof -
      assume s: "S▹?Γ ⊢ □" and t: "T▹?Γ ⊢ □"
      hence s_w: "S ▹ S ∪ T ▹ ?Γ ⊢ □" using Resolution_weaken by (metis insert_commute insert_is_Un)
      note Resolution_taint_assumptions[of "{T}" ?Γ "□" S] t
      then obtain R where R: "S ∪ T ▹ ?Γ ⊢ R" "R⊆S" by (auto simp: Un_commute)
      have literal_subset_sandwich: "R = □ ∨ R = S" if "is_lit_plus F" "cnf F = {S}" "R ⊆ S"
      using that by(cases F rule: is_lit_plus.cases; simp) blast+
      show ?thesis using literal_subset_sandwich[OF db(2) ST(1) R(2)] proof
        assume "R = □" thus ?thesis using R(1) by blast
      next
        from Resolution_unnecessary[where T="{_}", simplified] R(1)
        have "(R ▹ S ∪ T ▹ ?Γ ⊢ □) = (S ∪ T ▹ ?Γ ⊢ □)"  .
        moreover assume "R = S" 
        ultimately show ?thesis using s_w by simp
      qed
    qed
    thus ?thesis using IH ST R 1(1) by (metis UN_insert insert_absorb insert_is_Un)
  qed
qed

lemma R_consistent: "pcp {Γ|Γ. ¬((∀γ ∈ Γ. is_cnf γ) ⟶ ((⋃(cnf ` Γ)) ⊢ □))}"
  unfolding pcp_def
  unfolding Ball_def
  unfolding mem_Collect_eq
  apply(intro allI impI)
  apply(erule contrapos_pp)
  apply(unfold not_ex de_Morgan_conj de_Morgan_disj not_not not_all not_imp disj_not1)
  apply(intro impI allI)
  apply(elim disjE exE conjE; intro OrI2')
          apply(unfold not_ex de_Morgan_conj de_Morgan_disj not_not not_all not_imp disj_not1 Ball_def[symmetric])
          apply safe
          apply (metis Ass Pow_bottom Pow_empty UN_I cnf.simps(3))
         apply (metis Diff_insert_absorb Resolution.simps insert_absorb singletonI sup_bot.right_neutral atomD)
        apply (simp; metis (no_types, opaque_lifting) UN_insert cnf.simps(5) insert_absorb is_cnf.simps(1) sup_assoc)
       apply (auto intro: pcp_disj)
  done
    
theorem Resolution_complete:
  fixes F :: "'a :: countable formula"
  shows "⊨ F ⟹ cnf (nnf (❙¬F)) ⊢ □"
proof(erule contrapos_pp)
  assume c: "¬ (cnf (nnf (❙¬ F)) ⊢ □)"
  have "{cnf_form_of (nnf (❙¬F))} ∈ {Γ |Γ. ¬ ((∀γ∈Γ. is_cnf γ) ⟶ ⋃ (cnf ` Γ) ⊢ □)}"
    by(simp add: cnf_cnf[OF is_nnf_nnf] c cnf_form_of_is[OF is_nnf_nnf])
  from pcp_sat[OF R_consistent this] have "sat {cnf_form_of (nnf (❙¬ F))}" .
  thus "¬ ⊨ F" by(simp add: sat_def cnf_form_semantics[OF is_nnf_nnf] nnf_semantics)
qed

    
end