NAE

NAE.thy

theory hw 
  imports Main
begin

datatype variable = A | B | C | D | Z

(* a literal is a variable or its negation*)
datatype literal = Not variable | Id variable

(* given an assignment of variables to truth values, we can evaluate a literal to a truth value*)
fun evalLit :: "(variable ⇒ bool) ⇒ literal ⇒ bool" where 
  "evalLit f (Not x) = (¬ (f x)) "
| "evalLit f (Id x) = (f x)"

(* This is the truth table for NAE4 *)
fun nae4 :: "bool ⇒ bool ⇒ bool ⇒ bool ⇒ bool" where 
  "nae4 True True True True = False"
 |"nae4 False False False False = False"
 |"nae4 _ _ _ _ = True"

(* This is the truth table for NAE3 *)
fun nae3 :: "bool ⇒ bool ⇒ bool ⇒ bool" where 
  "nae3 True True True = False"
 |"nae3 False False False = False"
 |"nae3 _ _ _ = True"

(* Given an assignment of variables to truth values and 3 literals in a NAE3 clause,
determine if the clause is satisfied *)
fun naesat3 :: "(variable ⇒ bool) ⇒ literal ⇒ literal ⇒ literal ⇒ bool" where 
"naesat3 f l1 l2 l3 = (nae3 (evalLit f l1)  (evalLit f l2) (evalLit f l3))"


(* Given an assignment of variables to truth values and 4 literals in a NAE4 clause,
determine if the clause is satisfied *)
fun naesat4 :: "(variable ⇒ bool) ⇒ literal ⇒ literal ⇒ literal ⇒ literal ⇒ bool" where 
"naesat4 f l1 l2 l3 l4 = (nae4 (evalLit f l1)  (evalLit f l2)  (evalLit f l3) (evalLit f l4))"

(* I use Z here as a fresh variable (like alpha in the answer 3.a)
this predicate ensures that the other variables in the clause canot be variable Z 
*)
fun freshVar :: "variable ⇒ variable ⇒ variable ⇒ variable ⇒ bool" where 
"freshVar v1 v2 v3 v4 = ((v1 ≠ Z) ∧ (v2 ≠ Z) ∧ (v3 ≠ Z) ∧ (v4 ≠ Z))"

fun noZ :: "literal ⇒ bool" where 
  "noZ (Id x) = (x ≠ Z)"
| "noZ (Not x) = (x ≠ Z)"

(* I use Z here as a fresh variable (like alpha in the answer 3.a)
this predicate ensures that the other literals in the clause canot contain variable Z 
*)
fun fresh :: "literal ⇒ literal ⇒ literal ⇒ literal ⇒ bool" where 
"fresh l1 l2 l3 l4 = (noZ l1 ∧ noZ l2 ∧ noZ l3 ∧ noZ l4)"

(*a b c d are metavariables that can range over all possible literals containing variables A B C D 
(but not Z since we demand Z is a fresh variable)

This then check that whenever `f` is a satisfying assignment for an NAE4 clause,
  then there exists a satisfying assignment `g` to the conjunction of NAE3 clauses.

  That is to say,  NAE4 clause  (l1 l2 l3 l4) has a satisfying assignment
             iff   NAE3 formula (l1 l2 Z) /\ (l3 l4 (not Z)) has a satisfying assignment
 *)
lemma reduction_preserves_naesatisfiability: 
  assumes "fresh a b c d"
  shows "(∃ (f:: variable ⇒ bool). (naesat4 f a b c d) ⟷ 
         (∃ (g:: variable ⇒ bool).((naesat3 g a b (Id Z) ∧ naesat3 g c d (Not Z)))))"
  unfolding naesat4.simps naesat3.simps evalLit.simps fresh.simps noZ.simps
  using assms evalLit.elims(2) evalLit.elims(3) evalLit.simps(2) fresh.elims(2) freshVar.elims(3) 
        freshVar.simps literal.distinct(1) literal.inject(1) nae3.elims(3) nae3.simps(1) 
        nae3.simps(2) nae4.simps(1) nae4.simps(11) nae4.simps(13) nae4.simps(4) nae4.simps(6) 
        noZ.elims(1) variable.distinct(7)
  by (smt (verit))

end