1(* ========================================================================= *)
2(* DEFINITIONAL CNF IN HOL.                                                  *)
3(* Created by Joe Hurd, February 2002.                                       *)
4(* ========================================================================= *)
5
6signature defCNF =
7sig
8
9include Abbrev
10
11(* ------------------------------------------------------------------------- *)
12(* Definitional Negation Normal Form                                         *)
13(*                                                                           *)
14(* Example:                                                                  *)
15(*   (~(p = ~(q = r)) = ~(~(p = q) = r))                                     *)
16(*   =                                                                       *)
17(*   ((p = (q = r)) = ((p = ~q) = ~r))                                       *)
18(* ------------------------------------------------------------------------- *)
19
20val DEF_NNF_CONV : conv
21
22(* ------------------------------------------------------------------------- *)
23(* Definitional Conjunctive Normal Form                                      *)
24(*                                                                           *)
25(* Example:                                                                  *)
26(*   (~(p = ~(q = r)) = ~(~(p = q) = r))                                     *)
27(*   =                                                                       *)
28(*   ?v v1 v2 v3 v4.                                                         *)
29(*     (v4 \/ v1 \/ v3) /\ (v4 \/ ~v1 \/ ~v3) /\ (v1 \/ ~v3 \/ ~v4) /\       *)
30(*     (v3 \/ ~v1 \/ ~v4) /\ (v3 \/ v2 \/ ~r) /\ (v3 \/ ~v2 \/ r) /\         *)
31(*     (v2 \/ r \/ ~v3) /\ (~r \/ ~v2 \/ ~v3) /\ (v2 \/ p \/ ~q) /\          *)
32(*     (v2 \/ ~p \/ q) /\ (p \/ q \/ ~v2) /\ (~q \/ ~p \/ ~v2) /\            *)
33(*     (v1 \/ p \/ v) /\ (v1 \/ ~p \/ ~v) /\ (p \/ ~v \/ ~v1) /\             *)
34(*     (v \/ ~p \/ ~v1) /\ (v \/ q \/ r) /\ (v \/ ~q \/ ~r) /\               *)
35(*     (q \/ ~r \/ ~v) /\ (r \/ ~q \/ ~v) /\ v4                              *)
36(* ------------------------------------------------------------------------- *)
37
38val PURE_DEF_CNF_CONV    : conv         (* Introduces definitions *)
39val CLEANUP_DEF_CNF_CONV : conv         (* Converts defns to CNF *)
40val DEF_CNF_CONV         : conv         (* NNF + PURE + CLEANUP *)
41
42(* ------------------------------------------------------------------------- *)
43(* Definitional Conjunctive Normal Form using variable vectors               *)
44(*                                                                           *)
45(* Example:                                                                  *)
46(*   (~(p = ~(q = r)) = ~(~(p = q) = r))                                     *)
47(*   =                                                                       *)
48(*   ?v.                                                                     *)
49(*     (v 4 \/ v 1 \/ v 3) /\ (v 4 \/ ~v 1 \/ ~v 3) /\                       *)
50(*     (v 1 \/ ~v 3 \/ ~v 4) /\ (v 3 \/ ~v 1 \/ ~v 4) /\                     *)
51(*     (~r \/ ~v 2 \/ ~v 3) /\ (v 2 \/ r \/ ~v 3) /\ (v 3 \/ ~v 2 \/ r) /\   *)
52(*     (v 3 \/ v 2 \/ ~r) /\ (~q \/ ~p \/ ~v 2) /\ (p \/ q \/ ~v 2) /\       *)
53(*     (v 2 \/ ~p \/ q) /\ (v 2 \/ p \/ ~q) /\ (v 0 \/ ~p \/ ~v 1) /\        *)
54(*     (p \/ ~v 0 \/ ~v 1) /\ (v 1 \/ ~p \/ ~v 0) /\ (v 1 \/ p \/ v 0) /\    *)
55(*     (r \/ ~q \/ ~v 0) /\ (q \/ ~r \/ ~v 0) /\ (v 0 \/ ~q \/ ~r) /\        *)
56(*     (v 0 \/ q \/ r) /\ v 4                                                *)
57(* ------------------------------------------------------------------------- *)
58
59val PURE_DEF_CNF_VECTOR_CONV : conv
60val DEF_CNF_VECTOR_CONV      : conv     (* NNF + PURE + CLEANUP *)
61
62val dcnfgv : (unit -> Term.term) ref
63  val ndefs : Term.term ref
64end
65