Theory CNF_Formulas

text‹CNFs alone are nice, but now we want to relate between CNFs and formulas.›
theory CNF_Formulas
imports Formulas CNF
begin
  
context begin

(* attempts to eliminate ⊥ from formulas while converting to nnf have been made.
But that just gives you additional cases. So nnfs and cnfs will contain ⊥ *) 

function (sequential) nnf where
"nnf (Atom k) = (Atom k)" |
"nnf ⊥ = ⊥" |
"nnf (Not (And F G)) = Or (nnf (Not F)) (nnf (Not G))" |
"nnf (Not (Or F G)) = And (nnf (Not F)) (nnf (Not G))" |
"nnf (Not (Not F)) = nnf F" |
"nnf (Not (Imp F G)) = And (nnf F) (nnf (Not G))" |
"nnf (Not F) = (Not F)" |
"nnf (And F G) = And (nnf F) (nnf G)" |
"nnf (Or F G) = Or (nnf F) (nnf G)" |
"nnf (Imp F G) = Or (nnf (Not F)) (nnf G)"
  by(pat_completeness) auto

private fun nnf_cost where
"nnf_cost (Atom _) = 42" | 
"nnf_cost ⊥ = 42" |
"nnf_cost (Not F) = Suc (nnf_cost F)" |
"nnf_cost (And F G) = Suc (nnf_cost F + nnf_cost G)" |
"nnf_cost (Or F G) = Suc (nnf_cost F + nnf_cost G)" |
"nnf_cost (Imp F G) = Suc (Suc (nnf_cost F + nnf_cost G))" (* this is why *)

termination nnf by(relation "measure (λF. nnf_cost F)"; simp)

lemma "nnf ((Atom (k::nat)) ❙→ (Not ((Atom l) ❙∨ (Not (Atom m))))) = ❙¬ (Atom k) ❙∨ (❙¬ (Atom l) ❙∧ Atom m)"
  by code_simp

fun is_lit_plus where
"is_lit_plus ⊥ = True" |
"is_lit_plus (Not ⊥) = True" |
"is_lit_plus (Atom _) = True" |
"is_lit_plus (Not (Atom _)) = True" |
"is_lit_plus _ = False"
case_of_simps is_lit_plus_cases: is_lit_plus.simps
fun is_disj where
(* It is crucial for this to be a (right) deep tree for the proof of LSC ⟹ Res
  At some point, we obtain a subset A where A is in a disjunction from (A ∨ B). 
  Now, resolution is at a loss because you can't say anything about the subset.
  If, however, that subset is sandwiched between a literal and the empty clause,
  you can just cover all the cases. *)
"is_disj (Or F G) = (is_lit_plus F ∧ is_disj G)" |
"is_disj F = is_lit_plus F"
fun is_cnf where
(* here, we do want to allow arbitrary trees of ∧.
  If we do not do that, the proofs in LSC_Resolution won't work,
  since it relies on the ∧ case being just
  a simple split in LSC and union in Resolution.
  It is possible that that is fixable, but at what cost? *)
"is_cnf (And F G) = (is_cnf F ∧ is_cnf G)" |
"is_cnf H = is_disj H"
fun is_nnf where
"is_nnf (Imp F G) = False" |
"is_nnf (And F G) = (is_nnf F ∧ is_nnf G)" |
"is_nnf (Or F G) = (is_nnf F ∧ is_nnf G)" |
"is_nnf F = is_lit_plus F"

lemma is_nnf_nnf: "is_nnf (nnf F)"
  by(induction F rule: nnf.induct; simp)
lemma nnf_no_imp: "A ❙→ B ∉ set (subformulae (nnf F))"
  by(induction F rule: nnf.induct; simp)
lemma subformulae_nnf: "is_nnf F ⟹ G ∈ set (subformulae F) ⟹ is_nnf G" (* fun fact *)
  by(induction F rule: is_nnf.induct; simp add: is_lit_plus_cases split: formula.splits; elim disjE conjE; simp)
lemma is_nnf_NotD: "is_nnf (❙¬ F) ⟹ (∃k. F = Atom k) ∨ F = ⊥"
  by(cases F; simp)

fun cnf :: "'a formula ⇒ 'a clause set" where
"cnf (Atom k) = {{ k⇧+ }}" |
"cnf (Not (Atom k)) = {{ k¯ }}" |
"cnf ⊥ = {□}" |
"cnf (Not ⊥) = {}"  |
"cnf (And F G) = cnf F ∪ cnf G"  |
"cnf (Or F G) = {C ∪ D| C D. C ∈ (cnf F) ∧ D ∈ (cnf G)}"

lemma cnf_fin:
assumes "is_nnf F"
shows "finite (cnf F)" "C ∈ cnf F ⟹ finite C"
proof -
  have "finite (cnf F) ∧ (C ∈ cnf F ⟶ finite C)" using assms
    by(induction F arbitrary: C rule: cnf.induct;  clarsimp simp add: finite_image_set2)
  thus "finite (cnf F)" "C ∈ cnf F ⟹ finite C" by simp+
qed

(* Sets, as produced by @{const cnf} can be hard to handle.
   Less because of their infinity, more because of their lack of explicit order. *)
fun cnf_lists :: "'a formula ⇒ 'a literal list list" where
"cnf_lists (Atom k) = [[ k⇧+ ]]" |
"cnf_lists (Not (Atom k)) = [[ k¯ ]]" |
"cnf_lists ⊥ = [[]]" |
"cnf_lists (Not ⊥) = []"  |
"cnf_lists (And F G) = cnf_lists F @ cnf_lists G"  |
"cnf_lists (Or F G) = [f @ g. f ← (cnf_lists F), g ← (cnf_lists G)]"

primrec form_of_lit where
"form_of_lit (Pos k) = Atom k" |
"form_of_lit (Neg k) = ❙¬(Atom k)"
case_of_simps form_of_lit_cases: form_of_lit.simps

definition "disj_of_clause c ≡ ❙⋁[form_of_lit l. l ← c]"
definition "form_of_cnf F ≡ ❙⋀[disj_of_clause c. c ← F]"
definition "cnf_form_of ≡ form_of_cnf ∘ cnf_lists"
lemmas cnf_form_of_defs = cnf_form_of_def form_of_cnf_def disj_of_clause_def

lemma disj_of_clause_simps[simp]:
  "disj_of_clause [] = ⊥"
  "disj_of_clause (F#FF) = form_of_lit F ❙∨ disj_of_clause FF"
by(simp_all add: disj_of_clause_def)

lemma is_cnf_BigAnd: "is_cnf (❙⋀ls) ⟷ (∀l ∈ set ls. is_cnf l)"
  by(induction ls; simp)

private lemma BigOr_is_not_cnf'': "is_cnf (❙⋁ls) ⟹ (∀l ∈ set ls. is_lit_plus l)" 
proof(induction ls)
  case (Cons l ls)
  from Cons.prems have "is_cnf (❙⋁ ls)" 
    by (metis BigOr.simps is_cnf.simps(3,5) is_disj.simps(1) list.exhaust)
  thus ?case using Cons by simp
qed simp
private lemma BigOr_is_not_cnf': "(∀l ∈ set ls. is_lit_plus l) ⟹ is_cnf (❙⋁ls)" 
  by(induction ls; simp) (metis BigOr.simps(1, 2) formula.distinct(25) is_cnf.elims(2) is_cnf.simps(3) list.exhaust)
  (* ugh *)
lemma BigOr_is_not_cnf: "is_cnf (❙⋁ls) ⟷ (∀l ∈ set ls. is_lit_plus l)"
  using BigOr_is_not_cnf' BigOr_is_not_cnf'' by blast

lemma is_nnf_BigAnd[simp]: "is_nnf (❙⋀ls) ⟷ (∀l ∈ set ls. is_nnf l)"
  by(induction ls; simp)
lemma is_nnf_BigOr[simp]: "is_nnf (❙⋁ls) ⟷ (∀l ∈ set ls. is_nnf l)"
  by(induction ls; simp)
lemma form_of_lit_is_nnf[simp,intro!]: "is_nnf (form_of_lit x)"
  by(cases x; simp)
lemma form_of_lit_is_lit[simp,intro!]: "is_lit_plus (form_of_lit x)"
  by(cases x; simp)
lemma disj_of_clause_is_nnf[simp,intro!]: "is_nnf (disj_of_clause F)"
  unfolding disj_of_clause_def by simp

lemma cnf_form_of_is: "is_nnf F ⟹ is_cnf (cnf_form_of F)"
  by(cases F) (auto simp: cnf_form_of_defs is_cnf_BigAnd BigOr_is_not_cnf)

lemma nnf_cnf_form: "is_nnf F ⟹ is_nnf (cnf_form_of F)"
  by(cases F) (auto simp add: cnf_form_of_defs)

lemma cnf_BigAnd: "cnf (❙⋀ls) = (⋃x ∈ set ls. cnf x)"
  by(induction ls; simp)

lemma cnf_BigOr: "cnf (❙⋁ (x @ y)) =  {f ∪ g |f g. f ∈ cnf (❙⋁x) ∧ g ∈ cnf (❙⋁y)}"
  by(induction x arbitrary: y; simp) (metis (no_types, opaque_lifting) sup.assoc)

lemma cnf_cnf: "is_nnf F ⟹ cnf (cnf_form_of F) = cnf F"
  by(induction F rule: cnf.induct; 
     fastforce simp add: cnf_form_of_defs cnf_BigAnd cnf_BigOr)
(* this is not an idempotency (is that a word?) lemma, since cnf_form_of is not idempotent. *)

lemma is_nnf_nnf_id: "is_nnf F ⟹ nnf F = F"
proof(induction rule: is_nnf.induct)
  fix v assume "is_nnf (❙¬ v)"
  thus "nnf (❙¬ v) = ❙¬ v" by(cases v rule: is_lit_plus.cases; simp)
qed simp_all
  
lemma disj_of_clause_is: "is_disj (disj_of_clause R)"
  by(induction R; simp)
    
lemma form_of_cnf_is_nnf: "is_nnf (form_of_cnf R)"
  unfolding form_of_cnf_def by simp
    
lemma cnf_disj: "cnf (disj_of_clause R) = {set R}"
  by(induction R; simp add: form_of_lit_cases split: literal.splits)
lemma cnf_disj_ex: "is_disj F ⟹ ∃R. cnf F = {R} ∨ cnf F = {}"
  by(induction F rule: is_disj.induct; clarsimp simp: is_lit_plus_cases split: formula.splits)
    
    
lemma cnf_form_of_cnf: "cnf (form_of_cnf S) = set (map set S)"
  unfolding form_of_cnf_def by (simp add: cnf_BigAnd cnf_disj) blast
    
lemma disj_is_nnf: "is_disj F ⟹ is_nnf F"
  by(induction F rule: is_disj.induct; simp add: is_lit_plus_cases split: formula.splits)
    
lemma nnf_BigAnd: "nnf (❙⋀F) = ❙⋀(map nnf F)"
  by(induction F; simp)

end

end