Theory Negation_Type_DNF

section‹Negation Type DNF›
theory Negation_Type_DNF
imports Negation_Type
begin


(*Just a draft. needed for packet_set*)

type_synonym 'a dnf = "(('a negation_type) list) list"

fun cnf_to_bool :: "('a ⇒ bool) ⇒ 'a negation_type list ⇒ bool" where
  "cnf_to_bool _ [] ⟷ True" |
  "cnf_to_bool f (Pos a#as) ⟷ (f a) ∧ cnf_to_bool f as" |
  "cnf_to_bool f (Neg a#as) ⟷ (¬ f a) ∧ cnf_to_bool f as"

fun dnf_to_bool :: "('a ⇒ bool) ⇒ 'a dnf ⇒ bool" where
  "dnf_to_bool _ [] ⟷ False" |
  "dnf_to_bool f (as#ass) ⟷ (cnf_to_bool f as) ∨ (dnf_to_bool f ass)"

text‹representing @{const True}›
definition dnf_True :: "'a dnf" where
  "dnf_True ≡ [[]]"
lemma dnf_True: "dnf_to_bool f dnf_True"
  unfolding dnf_True_def by(simp)

text‹representing @{const False}›
definition dnf_False :: "'a dnf" where
  "dnf_False ≡ []"
lemma dnf_False: "¬ dnf_to_bool f dnf_False"
  unfolding dnf_False_def by(simp)

lemma cnf_to_bool_append: "cnf_to_bool γ (a1 @ a2) ⟷ cnf_to_bool γ a1 ∧ cnf_to_bool γ a2"
  by(induction γ a1 rule: cnf_to_bool.induct) (simp_all)
lemma dnf_to_bool_append: "dnf_to_bool γ (a1 @ a2) ⟷ dnf_to_bool γ a1 ∨ dnf_to_bool γ a2"
  by(induction a1) (simp_all)

definition dnf_and :: "'a dnf ⇒ 'a dnf ⇒ 'a dnf" where
  "dnf_and cnf1 cnf2 = [andlist1 @ andlist2. andlist1 <- cnf1, andlist2 <- cnf2]"

value "dnf_and ([[a,b], [c,d]]) ([[v,w], [x,y]])"

lemma cnf_to_bool_set: "cnf_to_bool f cnf ⟷ (∀ c ∈ set cnf. (case c of Pos a ⇒ f a | Neg a ⇒ ¬ f a))"
  proof(induction cnf)
  case Nil thus ?case by simp
  next
  case Cons thus ?case by (simp split: negation_type.split)
  qed
lemma dnf_to_bool_set: "dnf_to_bool γ dnf ⟷ (∃ d ∈ set dnf. cnf_to_bool γ d)"
  proof(induction dnf)
  case Nil thus ?case by simp
  next
  case (Cons d d1) thus ?case by(simp)
  qed

lemma dnf_to_bool_seteq: "set ` set d1 = set ` set d2 ⟹ dnf_to_bool γ d1 ⟷ dnf_to_bool γ d2"
  proof -
    assume assm: "set ` set d1 = set ` set d2"
    have helper1: "⋀P d. (∃d∈set d. ∀c∈set d. P c) ⟷ (∃d∈set ` set d. ∀c∈d. P c)" by blast
    from assm show ?thesis
      apply(simp add: dnf_to_bool_set cnf_to_bool_set)
      apply(subst helper1)
      apply(subst helper1)
      apply(simp)
      done
  qed

lemma dnf_and_correct: "dnf_to_bool γ (dnf_and d1 d2) ⟷ dnf_to_bool γ d1 ∧ dnf_to_bool γ d2"
 apply(simp add: dnf_and_def)
 apply(induction d1)
  apply(simp)
 apply(simp add: dnf_to_bool_append)
 apply(simp add: dnf_to_bool_set cnf_to_bool_set)
 by (meson UnCI UnE)

lemma dnf_and_symmetric: "dnf_to_bool γ (dnf_and d1 d2) ⟷ dnf_to_bool γ (dnf_and d2 d1)"
  using dnf_and_correct by blast

 
subsubsection‹inverting a DNF›
  text‹Example›
  lemma "(¬ ((a1 ∧ a2) ∨ b ∨ c)) = ((¬a1 ∧ ¬ b ∧ ¬ c) ∨ (¬a2 ∧ ¬ b ∧ ¬ c))" by blast
  lemma "(¬ ((a1 ∧ a2) ∨ (b1 ∧ b2) ∨ c)) = ((¬a1 ∧ ¬ b1 ∧ ¬ c) ∨ (¬a2 ∧ ¬ b1 ∧ ¬ c) ∨ (¬a1 ∧ ¬ b2 ∧ ¬ c) ∨ (¬a2 ∧ ¬ b2 ∧ ¬ c))" by blast
  
  fun listprepend :: "'a list ⇒ 'a list list ⇒ 'a list list" where
    "listprepend [] ns = []" |
    "listprepend (a#as) ns = (map (λxs. a#xs) ns) @ (listprepend as ns)"
  
  lemma "listprepend [a,b] [as, bs] = [a#as, a#bs, b#as, b#bs]" by simp
  
  lemma map_a_and: "dnf_to_bool γ (map ((#) a) ds) ⟷ dnf_to_bool γ [[a]] ∧ dnf_to_bool γ ds"
    apply(induction ds)
     apply(simp_all)
    apply(case_tac a)
     apply(simp_all)
     apply blast+
    done
  
  text‹this is how @{const listprepend} works:›
  lemma "¬ dnf_to_bool γ (listprepend [] ds)" by(simp)
  lemma "dnf_to_bool γ (listprepend [a] ds) ⟷ dnf_to_bool γ [[a]] ∧ dnf_to_bool γ ds" by(simp add: map_a_and)
  lemma "dnf_to_bool γ (listprepend [a, b] ds) ⟷ (dnf_to_bool γ [[a]] ∧ dnf_to_bool γ ds) ∨ (dnf_to_bool γ [[b]] ∧ dnf_to_bool γ ds)" 
    by(simp add: map_a_and dnf_to_bool_append)
  
  
  text‹We use ‹∃› to model the big ‹∨› operation›
  lemma listprepend_correct: "dnf_to_bool γ (listprepend as ds) ⟷ (∃a∈ set as. dnf_to_bool γ [[a]] ∧ dnf_to_bool γ ds)"
    apply(induction as)
     apply(simp)
    apply(simp)
    apply(rename_tac a as)
    apply(simp add: map_a_and cnf_to_bool_append dnf_to_bool_append)
    by blast
  lemma listprepend_correct': "dnf_to_bool γ (listprepend as ds) ⟷ (dnf_to_bool γ (map (λa. [a]) as) ∧ dnf_to_bool γ ds)"
    apply(induction as)
     apply(simp)
    apply(simp)
    apply(rename_tac a as)
    apply(simp add: map_a_and cnf_to_bool_append dnf_to_bool_append)
    by blast
  
  lemma cnf_invert_singelton: "cnf_to_bool γ [invert a] ⟷ ¬ cnf_to_bool γ [a]" by(cases a, simp_all)
  
  lemma cnf_singleton_false: "(∃a'∈set as. ¬ cnf_to_bool γ [a']) ⟷ ¬ cnf_to_bool γ as"
    by(induction γ as rule: cnf_to_bool.induct) (simp_all)
  
  fun dnf_not :: "'a dnf ⇒ 'a dnf" where
    "dnf_not [] = [[]]" | (*False goes to True*)
    "dnf_not (ns#nss) = listprepend (map invert ns) (dnf_not nss)"
  
  lemma dnf_not: "dnf_to_bool γ (dnf_not d) ⟷ ¬ dnf_to_bool γ d"
    apply(induction d)
     apply(simp_all)
    apply(simp add: listprepend_correct)
    apply(simp add: cnf_invert_singelton cnf_singleton_false)
    done

subsubsection‹Optimizing›
  (*there is probably a way better way to represent the set in the Collection framework
    A list of lists can be quite inefficient
    A better datastructure can help as we actually only use a set of sets*)
  definition optimize_dfn :: "'a dnf ⇒ 'a dnf" where
    "optimize_dfn dnf = map remdups (remdups dnf)"

  lemma "dnf_to_bool f (optimize_dfn dnf) = dnf_to_bool f dnf"
    unfolding optimize_dfn_def
    apply(rule dnf_to_bool_seteq)
    apply(simp)
    by (metis image_cong image_image set_remdups)

end