Theory LSC_Resolution

subsection‹Converting between Resolution and SC proofs›
theory LSC_Resolution
imports LSC Resolution
begin    

lemma literal_subset_sandwich:
  assumes "is_lit_plus F" "cnf F = {C}" "R ⊆ C"
  shows "R = □ ∨ R = C"
using assms by(cases F rule: is_lit_plus.cases; simp) blast+ (* proof somewhat strange internally… *)

text‹Proof following Gallier~\<^cite>‹"gallier2015logic"›.›
theorem CSC_Resolution_pre: "Γ ⇒⇩n ⟹ ∀γ ∈ set_mset Γ. is_cnf γ ⟹ (⋃(cnf ` set_mset Γ)) ⊢ □"
proof(induction rule: LSC.induct)
  case (Ax k Γ)
  let ?s = "⋃(cnf ` set_mset (❙¬ (Atom k), Atom k, Γ))"
  have "?s ⊢ {k⇧+}" "?s ⊢ {k¯}" using Resolution.Ass[where 'a='a] by simp_all
  from Resolution.R[OF this, of k]
  have "?s ⊢ □" by simp
  thus ?case by simp
next
  case (BotL Γ) thus ?case by(simp add: Ass)
next
  case (AndL F G Γ)
  hence "⋃(cnf ` set_mset (F, G, Γ)) ⊢ □" by simp
  thus ?case by(simp add: Un_left_commute sup.assoc)
next
  (* The idea for the whole trickery with F being a literal (is_disj has to only allows right deep formulas)
    and the sandwiching is from Gallier, but mentioned there only in one little sentence. *)
  case (OrL F Γ G)
  hence "is_cnf (F ❙∨ G)" by simp
  hence d: "is_disj (F ❙∨ G)" by simp
  hence db: "is_disj F" "is_lit_plus F" "is_disj G" by (-, cases F) simp_all
  hence "is_cnf F ∧ is_cnf G" by(cases F; cases G; simp)
  with OrL have IH: "(⋃(cnf ` set_mset (F, Γ))) ⊢ □" "(⋃(cnf ` set_mset (G, Γ))) ⊢ □" by simp_all
  let ?Γ = "(⋃(cnf ` set_mset Γ))"
  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 ▹ ⋃(cnf ` set_mset Γ) ⊢ R" "R⊆S" by (auto simp: Un_commute)
      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 by simp
  qed
  hence case_readable: "cnf (F ❙∨ G) ∪ ?Γ ⊢ □" by auto
qed auto

corollary LSC_Resolution:
  assumes "Γ ⇒⇩n"
  shows "(⋃(cnf ` nnf ` set_mset Γ)) ⊢ □"
proof -
  from assms
  have "image_mset nnf Γ ⇒⇩n" by (simp add: LSC_NNF)
  from LSC_cnf[OF this]
  have "image_mset (cnf_form_of ∘ nnf) Γ ⇒⇩n" by(simp add: image_mset.compositionality is_nnf_nnf)
  moreover have "∀γ ∈ set_mset (image_mset (cnf_form_of ∘ nnf) Γ). is_cnf γ" 
    using cnf_form_of_is[where 'a='a, OF is_nnf_nnf] by simp
  moreover note CSC_Resolution_pre
  ultimately have "⋃(cnf ` set_mset (image_mset (cnf_form_of ∘ nnf) Γ)) ⊢ □"  by blast
  hence "⋃((λF. cnf (cnf_form_of (nnf F))) ` set_mset Γ) ⊢ □" by simp
  thus ?thesis unfolding cnf_cnf[OF is_nnf_nnf] by simp
qed
  
corollary SC_Resolution:
  assumes "Γ ⇒ {#}"
  shows "(⋃(cnf ` nnf ` set_mset Γ)) ⊢ □"
proof -
  from assms have "image_mset nnf Γ ⇒⇩n" by (simp add: LSC_NNF SC_LSC)
  hence "⋃(cnf` nnf ` set_mset (image_mset nnf Γ)) ⊢ □" using LSC_Resolution by blast
  thus ?thesis using is_nnf_nnf_id[where 'a='a] is_nnf_nnf[where 'a='a] by auto
qed

(* Gallier just goes "Any resolution refutation can be transformed to a derivation in SCNF'"
   But we don't know what a resolution refutation is, inductively speaking. *)
(* would have been a bit nicer with orderings on formula to convert mset → list *)
lemma Resolution_LSC_pre:
  assumes "S ⊢ R"
  assumes "finite R"
  assumes "finite S" "Ball S finite"
  shows "∃S' R'. ∀Γ. set R' = R ∧ set (map set S') = S ∧ 
    (disj_of_clause R', {#disj_of_clause c. c ∈# mset S'#} + Γ ⇒⇩n ⟶ {#disj_of_clause c. c ∈# mset S'#} + Γ ⇒⇩n)"
(* order of quantifiers is important here… *)
using assms proof(induction S R rule: Resolution.induct)
  case (Ass F S)
  (* Idea: we don't just obtain an S', we obtain an S' that contains R (and not just some reordering of it) *)
  define Sm where "Sm = S - {F}"
  hence Sm: "S = F▹Sm" "F ∉ Sm" using Ass by fast+ (* try doing this with obtain… *)
  with Ass have fsm: "finite Sm" "Ball Sm finite" by auto
  then obtain Sm' where "Sm = set (map set Sm')" by (metis (full_types) ex_map_conv finite_list)
  moreover obtain R' where [simp]: "F = set R'" using Ass finite_list by blast
  ultimately have S: "S = set (map set (R'#Sm'))" unfolding Sm by simp
  show ?case
    using LSC_Contract[where 'a='a]
    by(intro exI[where x="R'#Sm'"] exI[where x=R']) (simp add: S add_ac)
  (* this was the base case. ugh. *)
next
  case (R S F G k)
  from R.prems have fin: "finite F" "finite G" by simp_all
  from R.IH(1)[OF fin(1) R.prems(2,3)] obtain FR FS where IHF:
    "set FR = F" "set (map set FS) = S"
    "⋀Γ GS. (disj_of_clause FR, image_mset disj_of_clause (mset (FS@GS)) + Γ ⇒⇩n 
      ⟹ image_mset disj_of_clause (mset (FS@GS)) + Γ ⇒⇩n)"
      by simp (metis add.assoc)
  from R.IH(2)[OF fin(2) R.prems(2,3)] obtain GR GS where IHG:
    "set GR = G" "set (map set GS) = S"
    "⋀Γ HS. (disj_of_clause GR, image_mset disj_of_clause (mset (GS@HS)) + Γ ⇒⇩n 
      ⟹ image_mset disj_of_clause (mset (GS@HS)) + Γ ⇒⇩n)"
    by simp (metis add.assoc)
  have IH: "image_mset disj_of_clause (mset (FS @ GS)) + Γ ⇒⇩n"
    if "disj_of_clause FR, disj_of_clause GR, image_mset disj_of_clause (mset (FS @ GS)) + Γ ⇒⇩n"
    for Γ using IHF(3)[of GS Γ] IHG(3)[of FS "disj_of_clause FR, Γ"] that
    by(simp add: add_mset_commute add_ac)
  show ?case
    apply(intro exI[where x="FS @ GS"] exI[where x="removeAll (k⇧+) FR @ removeAll (k¯) GR"] allI impI conjI)
      apply(simp add: IHF IHG;fail)
     apply(insert IHF IHG; simp;fail)
    apply(intro IH)
    apply(auto dest!: LSC_Sim_resolution_la simp add: IHF IHG R.hyps)
  done
qed
  
lemma Resolution_LSC_pre_nodisj: (* I've tried showing this directly instead of Resolution_LSC_pre, but that is surprisingly painful. *)
  assumes "S ⊢ R"
  assumes "finite R"
  assumes "finite S" "Ball S finite"
  shows "∃S' R'. ∀Γ. is_nnf_mset Γ ⟶ is_disj R' ∧ is_nnf S' ∧ cnf R' = {R} ∧ cnf S' ⊆ S ∧ 
    (R', S', Γ ⇒⇩n ⟶ S', Γ ⇒⇩n)"
proof -
  have mehorder: "F, ❙⋀G, Γ = ❙⋀G, F, Γ" for F G Γ by(simp add: add_ac)
  from Resolution_LSC_pre[where 'a='a,OF assms]
  obtain S' R' where o: "⋀Γ. is_nnf_mset Γ ⟹ set R' = R ∧ set (map set S') = S ∧ 
  (disj_of_clause R', image_mset disj_of_clause (mset S') + Γ ⇒⇩n ⟶ image_mset disj_of_clause (mset S') + Γ ⇒⇩n)"
    by blast
  hence p: "is_nnf_mset Γ ⟹ (disj_of_clause R', image_mset disj_of_clause (mset S') + Γ ⇒⇩n ⟹ image_mset disj_of_clause (mset S') + Γ ⇒⇩n)" 
    for Γ by blast
  show ?thesis
    apply(rule exI[where x="❙⋀map disj_of_clause S'"])
    apply(rule exI[where x="disj_of_clause R'"])
    apply safe
         apply(intro disj_of_clause_is;fail)
        apply(simp add: cnf_disj o; fail)+
     subgoal using o by(fastforce simp add: cnf_BigAnd cnf_disj)
    subgoal for Γ
      apply(frule p)
       apply(unfold mehorder)
       apply(drule LSC_BigAndL_inv)
         apply(simp;fail)+
      by (simp add: LSC_BigAndL)     
    done
qed

corollary Resolution_LSC1:
  assumes "S ⊢ □"
  shows "∃F. is_nnf F ∧ cnf F ⊆ S ∧ {#F#} ⇒⇩n"
proof -
  have *: "{f ∪ g |f g. f ∈ F ∧ g ∈ G} = {□} ⟹ F = {□}" for F G
  proof (rule ccontr)
    assume m: "{f ∪ g |f g. f ∈ F ∧ g ∈ G} = {□}"
    assume "F ≠ {□}"
    hence "F = {} ∨ (∃E. E ∈ F ∧ E ≠ □)" by blast
    thus False proof
      assume "F = {}"
      with m show False by simp
    next
      assume "∃E. E ∈ F ∧ E ≠ □"
      then obtain E where E: "E ∈ F ∧ E ≠ □" ..
      show False proof cases
        assume "G = {}" with m show False by simp
      next
        assume "G ≠ {}"
        then obtain D where "D ∈ G" by blast
        with E have "E ∪ D ∈ {f ∪ g |f g. f ∈ F ∧ g ∈ G}" by blast
        with m E show False by simp
      qed
    qed
  qed
  have *: "F = {□} ∧ G = {□}" if "{f ∪ g |f g. f ∈ F ∧ g ∈ G} = {□}" for F G
  proof (intro conjI)
    show "G = {□}"
      apply(rule *[of G F])
      apply(subst that[symmetric])
    by blast
  qed (rule *[OF that])
  have *: "is_nnf F ⟹ is_nnf_mset Γ ⟹ cnf F = {□} ⟹ F,Γ ⇒⇩n" for F Γ
    apply(induction F rule: cnf.induct; simp)
      apply blast
     apply (metis LSC.LSC.AndL LSC_weaken add_mset_commute singleton_Un_iff)
    apply(drule *; simp add: LSC.LSC.OrL)
  done
  from Resolution_useless_infinite[OF assms]
  obtain S' where su: "S'⊆S" and fin: "finite S'" "Ball S' finite" and pr: "(S' ⊢ □)" by blast
  from Resolution_LSC_pre_nodisj[OF pr finite.emptyI fin]
  obtain S'' where "is_nnf S''" "cnf S'' ⊆ S'" "{# S'' #} ⇒⇩n" 
    using * [OF disj_is_nnf, of _ ‹{#}›]
    by (metis LSC_weaken add_mset_commute empty_iff set_mset_empty)
  with su show ?thesis by blast
qed

corollary Resolution_SC1:
  assumes "S ⊢ □"
  shows "∃F. cnf (nnf F) ⊆ S ∧ {#F#} ⇒ {#}"
  apply(insert Resolution_LSC1[OF assms])
  apply(elim ex_forward)
  apply(elim conjE; intro conjI)
   subgoal by(subst is_nnf_nnf_id; assumption)
  apply(unfold SC_LSC)
  subgoal by (simp;fail)
done
    
(* really, these proofs have to do with sets, multisets and lists.
If I'd introduce finite sets somehow, the chaos would be perfect.
I want out.
*)

end