# Theory Ternary

```section‹Ternary Logic›
theory Ternary
imports Main
begin

text‹Kleene logic›

datatype ternaryvalue = TernaryTrue | TernaryFalse | TernaryUnknown
datatype ternaryformula = TernaryAnd ternaryformula ternaryformula
| TernaryOr ternaryformula ternaryformula
| TernaryNot ternaryformula
| TernaryValue ternaryvalue

fun ternary_to_bool :: "ternaryvalue ⇒ bool option" where
"ternary_to_bool TernaryTrue = Some True" |
"ternary_to_bool TernaryFalse = Some False" |
"ternary_to_bool TernaryUnknown = None"

fun bool_to_ternary :: "bool ⇒ ternaryvalue" where
"bool_to_ternary True = TernaryTrue" |
"bool_to_ternary False = TernaryFalse"

lemma "the ∘ ternary_to_bool ∘ bool_to_ternary = id"
by(simp add: fun_eq_iff, clarify, case_tac x, simp_all)
lemma ternary_to_bool_bool_to_ternary: "ternary_to_bool (bool_to_ternary X) = Some X"
by(cases X, simp_all)
lemma ternary_to_bool_None: "ternary_to_bool t = None ⟷ t = TernaryUnknown"
by(cases t, simp_all)
lemma ternary_to_bool_SomeE: "ternary_to_bool t = Some X ⟹
(t = TernaryTrue ⟹ X = True ⟹ P) ⟹ (t = TernaryFalse ⟹ X = False ⟹ P)  ⟹ P"
by(cases t)(simp)+
lemma ternary_to_bool_Some: "ternary_to_bool t = Some X ⟷
(t = TernaryTrue ∧ X = True) ∨ (t = TernaryFalse ∧ X = False)"
by(cases t, simp_all)
lemma bool_to_ternary_Unknown: "bool_to_ternary t = TernaryUnknown ⟷ False"
by(cases t, simp_all)

fun eval_ternary_And :: "ternaryvalue ⇒ ternaryvalue ⇒ ternaryvalue" where
"eval_ternary_And TernaryTrue TernaryTrue = TernaryTrue" |
"eval_ternary_And TernaryTrue TernaryFalse = TernaryFalse" |
"eval_ternary_And TernaryFalse TernaryTrue = TernaryFalse" |
"eval_ternary_And TernaryFalse TernaryFalse = TernaryFalse" |
"eval_ternary_And TernaryFalse TernaryUnknown = TernaryFalse" |
"eval_ternary_And TernaryTrue TernaryUnknown = TernaryUnknown" |
"eval_ternary_And TernaryUnknown TernaryFalse = TernaryFalse" |
"eval_ternary_And TernaryUnknown TernaryTrue = TernaryUnknown"  |
"eval_ternary_And TernaryUnknown TernaryUnknown = TernaryUnknown"

lemma eval_ternary_And_comm: "eval_ternary_And t1 t2 = eval_ternary_And t2 t1"
by (cases t1 t2 rule: ternaryvalue.exhaust[case_product ternaryvalue.exhaust]) auto

fun eval_ternary_Or :: "ternaryvalue ⇒ ternaryvalue ⇒ ternaryvalue" where
"eval_ternary_Or TernaryTrue TernaryTrue = TernaryTrue" |
"eval_ternary_Or TernaryTrue TernaryFalse = TernaryTrue" |
"eval_ternary_Or TernaryFalse TernaryTrue = TernaryTrue" |
"eval_ternary_Or TernaryFalse TernaryFalse = TernaryFalse" |
"eval_ternary_Or TernaryTrue TernaryUnknown = TernaryTrue" |
"eval_ternary_Or TernaryFalse TernaryUnknown = TernaryUnknown" |
"eval_ternary_Or TernaryUnknown TernaryTrue = TernaryTrue" |
"eval_ternary_Or TernaryUnknown TernaryFalse = TernaryUnknown" |
"eval_ternary_Or TernaryUnknown TernaryUnknown = TernaryUnknown"

fun eval_ternary_Not :: "ternaryvalue ⇒  ternaryvalue" where
"eval_ternary_Not TernaryTrue = TernaryFalse" |
"eval_ternary_Not TernaryFalse = TernaryTrue" |
"eval_ternary_Not TernaryUnknown = TernaryUnknown"

text‹Just to hint that we did not make a typo, we add the truth table for
the implication and show that it is compliant with @{term "a ⟶ b ⟷ ¬a ∨ b"}›
fun eval_ternary_Imp :: "ternaryvalue ⇒ ternaryvalue ⇒ ternaryvalue" where
"eval_ternary_Imp TernaryTrue TernaryTrue = TernaryTrue" |
"eval_ternary_Imp TernaryTrue TernaryFalse = TernaryFalse" |
"eval_ternary_Imp TernaryFalse TernaryTrue = TernaryTrue" |
"eval_ternary_Imp TernaryFalse TernaryFalse = TernaryTrue" |
"eval_ternary_Imp TernaryTrue TernaryUnknown = TernaryUnknown" |
"eval_ternary_Imp TernaryFalse TernaryUnknown = TernaryTrue" |
"eval_ternary_Imp TernaryUnknown TernaryTrue = TernaryTrue" |
"eval_ternary_Imp TernaryUnknown TernaryFalse = TernaryUnknown" |
"eval_ternary_Imp TernaryUnknown TernaryUnknown = TernaryUnknown"
lemma "eval_ternary_Imp a b = eval_ternary_Or (eval_ternary_Not a) b"
apply(cases a)
apply(case_tac [!] b)
apply(simp_all)
done

lemma eval_ternary_Not_UnknownD: "eval_ternary_Not t = TernaryUnknown ⟹ t = TernaryUnknown"
by (cases t) auto

lemma eval_ternary_DeMorgan:
"eval_ternary_Not (eval_ternary_And a b) = eval_ternary_Or (eval_ternary_Not a) (eval_ternary_Not b)"
"eval_ternary_Not (eval_ternary_Or a b) = eval_ternary_And (eval_ternary_Not a) (eval_ternary_Not b)"
by (cases a b rule: ternaryvalue.exhaust[case_product ternaryvalue.exhaust],auto)+

lemma eval_ternary_idempotence_Not: "eval_ternary_Not (eval_ternary_Not a) = a"
by (cases a) simp_all

lemma eval_ternary_simps_simple:
"eval_ternary_And TernaryTrue x = x"
"eval_ternary_And x TernaryTrue = x"
"eval_ternary_And TernaryFalse x = TernaryFalse"
"eval_ternary_And x TernaryFalse = TernaryFalse"
by(case_tac [!] x)(simp_all)

context
begin
private lemma bool_to_ternary_simp1: "bool_to_ternary X = TernaryTrue ⟷ X"
by (metis bool_to_ternary.elims ternaryvalue.distinct(1))
private lemma bool_to_ternary_simp2:  "bool_to_ternary Y = TernaryFalse ⟷ ¬ Y"
by (metis bool_to_ternary.elims ternaryvalue.distinct(1))
private lemma bool_to_ternary_simp3: "eval_ternary_Not (bool_to_ternary X) = TernaryTrue ⟷ ¬ X"
by (metis (full_types) bool_to_ternary_simp2 eval_ternary_Not.simps(1) eval_ternary_idempotence_Not)
private lemma bool_to_ternary_simp4: "eval_ternary_Not (bool_to_ternary X) = TernaryFalse ⟷ X"
by (metis bool_to_ternary_simp1 eval_ternary_Not.simps(1) eval_ternary_idempotence_Not)
private lemma bool_to_ternary_simp5: "¬ (eval_ternary_Not (bool_to_ternary X) = TernaryUnknown)"
by (metis bool_to_ternary_Unknown eval_ternary_Not_UnknownD)

private lemma bool_to_ternary_simp6: "bool_to_ternary X ≠ TernaryUnknown"
by (metis (full_types) bool_to_ternary.simps(1) bool_to_ternary.simps(2) ternaryvalue.distinct(3) ternaryvalue.distinct(5))

lemmas bool_to_ternary_simps = bool_to_ternary_simp1 bool_to_ternary_simp2
bool_to_ternary_simp3 bool_to_ternary_simp4
bool_to_ternary_simp5 bool_to_ternary_simp6
end

context
begin
private lemma bool_to_ternary_pullup1:
"eval_ternary_Not (bool_to_ternary X) = bool_to_ternary (¬ X)"
by(cases X)(simp_all)

private lemma bool_to_ternary_pullup2:
"eval_ternary_And (bool_to_ternary X1) (bool_to_ternary X2) = bool_to_ternary (X1 ∧ X2)"
by (metis bool_to_ternary_simps(1) bool_to_ternary_simps(2) eval_ternary_simps_simple(2) eval_ternary_simps_simple(4))

private lemma bool_to_ternary_pullup3:
"eval_ternary_Imp (bool_to_ternary X1) (bool_to_ternary X2) = bool_to_ternary (X1 ⟶ X2)"
by (metis bool_to_ternary_simps(1) bool_to_ternary_simps(2) eval_ternary_Imp.simps(1)
eval_ternary_Imp.simps(2) eval_ternary_Imp.simps(3) eval_ternary_Imp.simps(4))

private lemma bool_to_ternary_pullup4:
"eval_ternary_Or (bool_to_ternary X1) (bool_to_ternary X2) = bool_to_ternary (X1 ∨ X2)"
by (metis (full_types) bool_to_ternary.simps(1) bool_to_ternary.simps(2) eval_ternary_Or.simps(1) eval_ternary_Or.simps(2) eval_ternary_Or.simps(3) eval_ternary_Or.simps(4))

lemmas bool_to_ternary_pullup = bool_to_ternary_pullup1 bool_to_ternary_pullup2
bool_to_ternary_pullup3 bool_to_ternary_pullup4
end

fun ternary_ternary_eval :: "ternaryformula ⇒ ternaryvalue" where
"ternary_ternary_eval (TernaryAnd t1 t2) = eval_ternary_And (ternary_ternary_eval t1) (ternary_ternary_eval t2)" |
"ternary_ternary_eval (TernaryOr t1 t2) = eval_ternary_Or (ternary_ternary_eval t1) (ternary_ternary_eval t2)" |
"ternary_ternary_eval (TernaryNot t) = eval_ternary_Not (ternary_ternary_eval t)" |
"ternary_ternary_eval (TernaryValue t) = t"

lemma ternary_ternary_eval_DeMorgan: "ternary_ternary_eval (TernaryNot (TernaryAnd a b)) =
ternary_ternary_eval (TernaryOr (TernaryNot a) (TernaryNot b))"

lemma ternary_ternary_eval_idempotence_Not:
"ternary_ternary_eval (TernaryNot (TernaryNot a)) = ternary_ternary_eval a"

lemma ternary_ternary_eval_TernaryAnd_comm:
"ternary_ternary_eval (TernaryAnd t1 t2) = ternary_ternary_eval (TernaryAnd t2 t1)"

lemma "eval_ternary_Not (ternary_ternary_eval t) = (ternary_ternary_eval (TernaryNot t))" by simp

context
begin
private lemma eval_ternary_simps_2:
"eval_ternary_And (bool_to_ternary P) T = TernaryTrue ⟷ P ∧ T = TernaryTrue"
"eval_ternary_And T (bool_to_ternary P) = TernaryTrue ⟷ P ∧ T = TernaryTrue"
apply(case_tac [!] P)
done

private lemma eval_ternary_simps_3:
"eval_ternary_And (ternary_ternary_eval x) T = TernaryTrue ⟷
ternary_ternary_eval x = TernaryTrue ∧ T = TernaryTrue"
"eval_ternary_And T (ternary_ternary_eval x) = TernaryTrue ⟷
ternary_ternary_eval x = TernaryTrue ∧ T = TernaryTrue"
apply(case_tac [!] T)
apply(case_tac [!] "(ternary_ternary_eval x)")
apply(simp_all)
done

lemmas eval_ternary_simps = eval_ternary_simps_simple eval_ternary_simps_2 eval_ternary_simps_3
end

definition ternary_eval :: "ternaryformula ⇒ bool option" where
"ternary_eval t = ternary_to_bool (ternary_ternary_eval t)"

subsection‹Negation Normal Form›

text‹A formula is in Negation Normal Form (NNF) if negations only occur at the atoms (not before and/or)›
inductive NegationNormalForm :: "ternaryformula ⇒ bool" where
"NegationNormalForm (TernaryValue v)" |
"NegationNormalForm (TernaryNot (TernaryValue v))" |
"NegationNormalForm φ ⟹ NegationNormalForm ψ ⟹ NegationNormalForm (TernaryAnd φ ψ)"|
"NegationNormalForm φ ⟹ NegationNormalForm ψ ⟹ NegationNormalForm (TernaryOr φ ψ)"

text‹Convert a @{typ ternaryformula} to a  @{typ ternaryformula} in NNF.›
fun NNF_ternary :: "ternaryformula ⇒ ternaryformula" where
"NNF_ternary (TernaryValue v) = TernaryValue v" |
"NNF_ternary (TernaryAnd t1 t2) = TernaryAnd (NNF_ternary t1) (NNF_ternary t2)" |
"NNF_ternary (TernaryOr t1 t2) = TernaryOr (NNF_ternary t1) (NNF_ternary t2)" |
"NNF_ternary (TernaryNot (TernaryNot t)) = NNF_ternary t" |
"NNF_ternary (TernaryNot (TernaryValue v)) = TernaryValue (eval_ternary_Not v)" |
"NNF_ternary (TernaryNot (TernaryAnd t1 t2)) = TernaryOr (NNF_ternary (TernaryNot t1)) (NNF_ternary (TernaryNot t2))" |
"NNF_ternary (TernaryNot (TernaryOr t1 t2)) = TernaryAnd (NNF_ternary (TernaryNot t1)) (NNF_ternary (TernaryNot t2))"

lemma NNF_ternary_correct: "ternary_ternary_eval (NNF_ternary t) = ternary_ternary_eval t"
proof(induction t rule: NNF_ternary.induct)

lemma NNF_ternary_NegationNormalForm: "NegationNormalForm (NNF_ternary t)"
proof(induction t rule: NNF_ternary.induct)
qed(auto simp add: eval_ternary_DeMorgan eval_ternary_idempotence_Not intro: NegationNormalForm.intros)

context
begin
private lemma ternary_lift1: "eval_ternary_Not tv ≠ TernaryFalse ⟷ tv = TernaryFalse ∨ tv = TernaryUnknown"
using eval_ternary_Not.elims by blast
private lemma ternary_lift2: "eval_ternary_Not tv ≠ TernaryTrue ⟷ tv = TernaryTrue ∨ tv = TernaryUnknown"
using eval_ternary_Not.elims by blast
private lemma ternary_lift3: "eval_ternary_Not tv = TernaryFalse ⟷ tv = TernaryTrue"
by (metis eval_ternary_Not.simps(1) eval_ternary_idempotence_Not)
private lemma ternary_lift4: "eval_ternary_Not tv = TernaryTrue ⟷ tv = TernaryFalse"
by (metis eval_ternary_Not.simps(1) eval_ternary_idempotence_Not)
private lemma ternary_lift5: "eval_ternary_Not tv = TernaryUnknown ⟷ tv = TernaryUnknown"
by (metis eval_ternary_Not.simps(3) eval_ternary_idempotence_Not)

private lemma ternary_lift6: "eval_ternary_And t1 t2 = TernaryFalse ⟷ t1 = TernaryFalse ∨ t2 = TernaryFalse"
using eval_ternary_And.elims by blast
private lemma ternary_lift7: "eval_ternary_And t1 t2 = TernaryTrue ⟷ t1 = TernaryTrue ∧ t2 = TernaryTrue"
using eval_ternary_And.elims by blast

lemmas ternary_lift = ternary_lift1 ternary_lift2 ternary_lift3 ternary_lift4 ternary_lift5 ternary_lift6 ternary_lift7
end

context
begin
private lemma l1: "eval_ternary_Not tv = TernaryTrue ⟹ tv = TernaryFalse"
by (metis eval_ternary_Not.simps(1) eval_ternary_idempotence_Not)
private lemma l2: "eval_ternary_And t1 t2 = TernaryFalse ⟹ t1 = TernaryFalse ∨ t2 = TernaryFalse"
using eval_ternary_And.elims by blast

lemmas eval_ternaryD = l1 l2
end

end
```