Theory Resolution

subsection‹Resolution›
theory Resolution
imports CNF "HOL-Library.While_Combinator"
begin

text‹Resolution is different from the other proof systems:
  its derivations do not represent proofs in the way the other systems do.
  Rather, they represent invariant additions (under satisfiability) to set of clauses.›
inductive Resolution :: "'a literal set set ⇒ 'a literal set ⇒ bool" (‹_ ⊢ _› [30] 28) where
Ass: "C ∈ S ⟹ S ⊢ C" |
R: "S ⊢ C ⟹ S ⊢ D ⟹ k⇧+ ∈ C ⟹ k¯ ∈ D ⟹ S ⊢ (C - {k⇧+}) ∪ (D - {k¯})"
text‹The problematic part of this formulation is that we can't talk about a "Resolution Refutation" in an inductive manner. 
  In the places where Gallier's proofs~\<^cite>‹"gallier2015logic"› do that, we have to work around that.›

lemma Resolution_weaken: "S ⊢ D ⟹ T ∪ S ⊢ D"
  by(induction rule: Resolution.induct; auto intro: Resolution.intros)

lemma Resolution_unnecessary:
  assumes sd: "∀C ∈ T. S ⊢ C"
  shows "T ∪ S ⊢ D ⟷ S ⊢ D" (is "?l ⟷ ?r")
proof
  assume ?l
  from ‹?l› sd show  ?r
  proof(induction "T ∪ S" D rule: Resolution.induct)
    case (Ass D)
    show ?case proof cases
      assume "D ∈ S" with Resolution.Ass show ?thesis .
    next
      assume "D ∉ S"
      with Ass.hyps have "D ∈ T" by simp
      with Ass.prems show ?thesis by blast
    qed
  next
    case (R D H k) thus ?case by (simp add: Resolution.R)
  qed
next
  assume ?r with Resolution_weaken show ?l by blast
qed

lemma Resolution_taint_assumptions: "S ∪ T ⊢ C ⟹ ∃R ⊆ D. ((∪) D ` S) ∪ T ⊢ R ∪ C"
(* No, we don't need to show this for an arbitrary clause D, but the proof doesn't get any more readable if you only allow a single atom. *)
proof(induction "S ∪ T" "C" rule: Resolution.induct)
 case (Ass C)
  show ?case proof(cases "C ∈ S")
    case True
    hence "D ∪ C ∈ (∪) D ` S ∪ T" by simp
    with Resolution.Ass have "((∪) D ` S) ∪ T ⊢ D ∪ C" .
    thus ?thesis by blast
  next
    case False
    with Ass have "C ∈ T" by simp
    hence "((∪) D ` S) ∪ T ⊢ C" by(simp add: Resolution.Ass)
    thus ?thesis by(intro exI[where x="{}"]) simp
  qed
next
  case (R C1 C2 k)
  let ?m = "((∪) D ` S) ∪ T"
  from R obtain R1 where IH1: "R1 ⊆ D" "?m ⊢ R1 ∪ C1" by blast
  from R obtain R2 where IH2: "R2 ⊆ D" "?m ⊢ R2 ∪ C2" by blast
  from R have "k⇧+ ∈ R1 ∪ C1" "k¯ ∈ R2 ∪ C2" by simp_all
  note Resolution.R[OF IH1(2) IH2(2) this]
  hence "?m ⊢ (R1 - {k⇧+}) ∪ (R2 - {k¯}) ∪ (C1 - {k⇧+} ∪ (C2 - {k¯}))"
    by (simp add: Un_Diff Un_left_commute sup.assoc)
  moreover have "(R1 - {k⇧+}) ∪ (R2 - {k¯}) ⊆ D" (* hah▹ gotcha. This is the reason that I should be doing this on sets▹ not multisets. - neh, actually, there are others. how is the rule even supposed to look? *)
    using IH1(1) IH2(1) by blast
  ultimately show ?case by blast
qed

text‹Resolution is ``strange'':
Given a set of clauses that is presumed to be satisfiable,
it derives new clauses that can be added while preserving the satisfiability of the set of clauses.
However, not every clause that could be added while keeping satisfiability can actually be added by resolution.
Especially, the above lemma ‹Resolution_taint_assumptions› gives us the derivability of a clause
@{term "R ∪ C"}, where @{term "R ⊆ D"}. What we might actually want is the derivability of 
@{term "D ∪ C"}. Any model that satisfies @{term "R ∪ C"} obviously satisfies @{term "D ∪ C"} 
(since they are disjunctions), but Resolution only allows to derive the former.
›
text‹Nevertheless, ‹Resolution_taint_assumptions›, can still be a quite useful lemma:
picking @{term D} to be a singleton set only leaves two possibilities for @{term R}.›

lemma Resolution_useless_infinite:
assumes R: "S ⊢ R"
assumes "finite R"
shows "∃S' ⊆ S. Ball S' finite ∧ finite S' ∧ (S' ⊢ R)"
using assms proof(induction rule: Resolution.induct)
  case (Ass C S) thus ?case using Resolution.Ass by(intro exI[where x="{C}"]) auto
next
  case (R S C D k)
  from R.prems have "finite C" "finite D" by simp_all
  with R.IH obtain SC SD where IH:
    "SC⊆S" "(∀C∈SC. finite C)" "finite SC" "SC ⊢ C"
    "SD⊆S" "(∀D∈SD. finite D)" "finite SD" "SD ⊢ D"
    by blast
  hence IHw: "SC ∪ SD ⊢ C" "SC ∪ SD ⊢ D" using Resolution_weaken 
    by(simp_all add: sup_commute Resolution_weaken (* yes, using and simp set. whatever. *))
  with IH(1-3,5-7) show ?case
    by(blast intro!: exI[where x="SC ∪ SD"] Resolution.R[OF _ _ ‹k⇧+ ∈ C› ‹k¯ ∈ D›])
qed
(* situation would be different if we allowed to resolve an infinite amount of literals in one step instead of just one.
   And I think that's exactly the reason why one doesn't do that.
 *)

text‹Now we define and verify a toy resolution prover.
Function ‹res› computes the set of resolvents of a clause set:›
context begin

definition res :: "'a clause set ⇒ 'a clause set" where
"res S =
 (⋃C1 ∈ S. ⋃C2 ∈ S. ⋃L1 ∈ C1. ⋃L2 ∈ C2.
 (case (L1,L2) of (Pos i,Neg j) ⇒ if i=j then {(C1 - {Pos i}) ∪ (C2 - {Neg j})} else {}
  | _ ⇒ {}))"

private definition "ex1 ≡ {{Neg (0::int)}, {Pos 0, Pos 1, Neg 2}, {Pos 0, Pos 1, Pos 2}, {Pos 0, Neg 1}}"
value "res ex1"
  
(* now we want to iterate res. We've got two options. Either use the while combinator,
   which is not so beautiful to present but easy to understand, or use partial_function magic,
  which looks beautiful, but… magic. The ML kind. *)

definition Rwhile ::" 'a clause set ⇒ 'a clause set option" where
"Rwhile = while_option (λS. □ ∉ S ∧ ¬ res S ⊆ S) (λS. res S ∪ S)"

value [code] "Rwhile ex1"
lemma "□ ∈ the (Rwhile ex1)" by eval

lemma Rwhile_sound: assumes "Rwhile S = Some S'"
  shows "∀C ∈ S'. Resolution S C"
apply(rule while_option_rule[OF _ assms[unfolded Rwhile_def]])
apply (auto simp: Ass R res_def split: if_splits literal.splits)
done

definition "all_clauses S = {s. s ⊆ {Pos k|k. k ∈ atoms_of_cnf S} ∪ {Neg k|k. k ∈ atoms_of_cnf S}}"
lemma s_sub_all_clauses: "S ⊆ all_clauses S"
  unfolding all_clauses_def
  apply(rule)
  apply(simp)
  apply(rule)
  apply(simp add: atoms_of_cnf_alt lit_atoms_cases[abs_def])
  by (metis imageI literal.exhaust literal.simps(5) literal.simps(6))
lemma atoms_res: "atoms_of_cnf (res S) ⊆  atoms_of_cnf S"
  unfolding res_def atoms_of_cnf_alt
  apply (clarsimp simp: lit_atoms_cases [abs_def] split: literal.splits if_splits)
  apply (clarsimp simp add: image_iff)
  apply force
  done

lemma exlitE: "(⋀x. xe = Pos x ⟹ P x) ⟹ (⋀x. xe = Neg x ⟹ False) ⟹ ∃x. xe = Pos x ∧ P x"
  by(cases xe) auto
lemma res_in_all_clauses: "res S ⊆ all_clauses S"
  apply (clarsimp simp: res_def all_clauses_def atoms_of_cnf_alt lit_atoms_cases
    split: literal.splits if_splits)
  apply (clarsimp simp add: image_iff)
  apply (metis atoms_of_lit.simps(1) atoms_of_lit.simps(2) lit_atoms_cases literal.exhaust)
  done

lemma Res_in_all_clauses: "res S ∪ S ⊆ all_clauses S"
  by (simp add: res_in_all_clauses s_sub_all_clauses)  
lemma all_clauses_Res_inv: "all_clauses (res S ∪ S) = all_clauses S"
  unfolding all_clauses_def atoms_of_cnf_Un
  using atoms_res by fast
lemma all_clauses_finite: "finite S ∧ (∀C ∈ S. finite C) ⟹ finite (all_clauses S)"
  unfolding all_clauses_def atoms_of_cnf_def by simp
lemma finite_res: "∀C ∈ S. finite C ⟹ ∀C ∈ res S. finite C"
  unfolding res_def by(clarsimp split: literal.splits)

lemma "finite T ⟹ S ⊆ T ⟹ card S < Suc (card T)"
  by (simp add: card_mono le_imp_less_Suc)
    
lemma "finite S ∧ (∀C ∈ S. finite C) ⟹ ∃T. Rwhile S = Some T"
  apply(unfold Rwhile_def)
  apply(rule measure_while_option_Some[rotated, where f="λT. Suc (card (all_clauses S)) - card T"
        and P="λT. finite T ∧ (∀C ∈ T. finite C) ∧ all_clauses T = all_clauses S"])
   apply(simp;fail)
  apply(intro conjI)
     subgoal by (meson all_clauses_finite finite_UnI finite_subset res_in_all_clauses)
    subgoal using finite_res by blast
   subgoal using all_clauses_Res_inv by blast
  subgoal 
    apply(rule diff_less_mono2)
     subgoal by (metis Res_in_all_clauses all_clauses_finite card_seteq finite_subset not_le sup_commute sup_ge2)
    subgoal apply(intro card_mono le_imp_less_Suc)
      subgoal using all_clauses_finite by blast
      subgoal using s_sub_all_clauses by blast
    done
  done
done

partial_function(option) Res where
"Res S = (let R = res S ∪ S in if R = S then Some S else Res R)"
declare Res.simps[code]

value [code] "Res ex1"
lemma "□ ∈ the (Res ex1)" by code_simp

lemma res: "C ∈ res S ⟹ S ⊢ C"
  unfolding res_def by(auto split: literal.splits if_splits) (metis Resolution.simps literal.exhaust)    

lemma Res_sound: "Res S = Some S' ⟹ (∀C ∈ S'. S ⊢ C)"
proof (induction arbitrary: S S' rule: Res.fixp_induct)
  fix X S S'
  assume IH: "⋀S S'. X S = Some S' ⟹ (∀C∈S'. S ⊢ C)"
  assume prem: "(let R = res S ∪ S in if R = S then Some S else X R) = Some S'"
  thus "(∀C∈S'. S ⊢ C)"
  proof cases
    assume "res S ∪ S = S"
    with prem show ?thesis by (simp add: Resolution.Ass)
  next
    assume 1: "res S ∪ S ≠ S"
    with prem have "X (res S ∪ S) = Some S'" by simp
    with IH have "∀C∈S'. res S ∪ S ⊢ C" by blast
    thus ?thesis using Resolution_unnecessary res by blast (* this needs the generalized Resolution_unnecessary lemma. And I don't get why the option-variant didn't. *)
  qed
qed (fast intro!: option_admissible)+

lemma Res_terminates: "finite S ⟹ ∀C ∈ S. finite C ⟹ ∃T. Res S = Some T"
proof(induction "card (all_clauses S) - card S" arbitrary: S rule: less_induct) (* can be done by induction on "card (all_clauses S - S)", but I found that to be more annoying. *)
  case less
  let ?r = "res S ∪ S"
  show ?case proof(cases "?r = S")
    case False
    have b: "finite (res S ∪ S)" by (meson less Res_in_all_clauses all_clauses_finite infinite_super)
    have c: "Ball (res S ∪ S) finite" using less.prems(2) finite_res by auto
    have "card S < card ?r" by (metis False b psubsetI psubset_card_mono sup_ge2)
    moreover have "card ?r ≤ (card (all_clauses S))"
      by (meson less Res_in_all_clauses all_clauses_finite card_mono le_imp_less_Suc)
    ultimately have a: "(card (all_clauses ?r)) - card ?r < (card (all_clauses S)) - card S" 
      using all_clauses_Res_inv[of S] by simp
    from less(1)[OF a b c] show ?thesis by (subst Res.simps) (simp add: Let_def)
  qed (simp add: Res.simps)
qed
  
(* just to demonstrate, this would not work: *)
code_pred (*(modes: i ⇒ i ⇒ bool)*) Resolution . (* can't infer any modes. *)
print_theorems (* doesn't generate any theorems either. *)

end
end