Exercise13

//1
type Prop =
    | A of string
    | Dis of Prop * Prop
    | Con of Prop * Prop
    | Neg of Prop

//2
let rec nnf p =
    let rec negate p =
        match p with
        | A a -> Neg (A a)
        | Dis (p1,p2) -> Con (negate p1, negate p2)
        | Con (p1,p2) -> Dis (negate p1, negate p2)
        | Neg p -> nnf p
    match p with
    | A a -> A a
    | Neg p -> negate p
    | Con (p1,p2) -> Con (negate p1, negate p2)
    | Dis (p1,p2) -> Dis (negate p1, negate p2)

//examples
let p = A "p"
let q = A "q"
let s1 = Neg p
let s2 = Neg (Neg p)
let s3 = Neg (Dis (p,q))
let s4 = Neg (Neg s3)

let rec dnf p =
    match p with
    | Con(A a, Dis(p1,p2)) -> Dis(Con(A a, p1), Con(A a, p2))
    | _ -> p