1(* ========================================================================= *)
2(* DEFINITIONAL CNF IN HOL.                                                  *)
3(* Created by Joe Hurd, February 2002.                                       *)
4(* ========================================================================= *)
5
6(*
7app load ["simpLib", "combinTheory", "boolSimps", "numLib", "normalForms",
8          "defCNFTheory"];
9guessing_tyvars := false;
10*)
11
12(*
13*)
14structure defCNF :> defCNF =
15struct
16
17open HolKernel Parse boolLib simpLib numLib normalForms defCNFTheory;
18
19(* ------------------------------------------------------------------------- *)
20(* Helper functions.                                                         *)
21(* ------------------------------------------------------------------------- *)
22
23fun ERR f s =
24  HOL_ERR {message = s, origin_function = f, origin_structure = "defCNF"};
25
26fun distinct [] = true
27  | distinct (x :: rest) = not (mem x rest) andalso distinct rest;
28
29val zero = numSyntax.zero_tm
30val suc = numSyntax.suc_tm
31
32val beq = mk_thy_const{Name = "=", Ty = bool --> bool --> bool, Thy = "min"}
33
34fun dest_beq tm =
35  let val (a, b, ty) = dest_eq_ty tm
36  in if ty = bool then (a, b) else raise ERR "dest_beq" "not a bool"
37  end;
38
39val is_beq = can dest_beq;
40
41val OKDEF = prim_mk_const{Thy = "defCNF", Name = "OKDEF"};
42
43(* ------------------------------------------------------------------------- *)
44(* Definitional Conjunctive Normal Form using variable vectors               *)
45(*                                                                           *)
46(* Example:                                                                  *)
47(*   (~(p = ~(q = r)) = ~(~(p = q) = r))                                     *)
48(*   =                                                                       *)
49(*   ?v.                                                                     *)
50(*     (v 0 = (q = r)) /\ (v 1 = (p = v 0)) /\ (v 2 = (p = ~q)) /\           *)
51(*     (v 3 = (v 2 = ~r)) /\ (v 4 = (v 1 = v 3)) /\ v 4                      *)
52(* ------------------------------------------------------------------------- *)
53
54
55fun sub_cnf f con defs (a, b) =
56    let
57      val (defs, a) = f defs a
58      val (defs, b) = f defs b
59      val tm = mk_comb (mk_comb (con, a), b)
60    in
61      (defs, tm)
62    end;
63
64fun def_step (defs as (vec, n, ds), tm) =
65  case List.find (fn (_, b) => b = tm) ds of NONE =>
66    let
67      val g = mk_comb (vec, n)
68      val n = rhs (concl (REDUCE_CONV (mk_comb (suc, n))))
69    in
70      ((vec, n, (g, tm) :: ds), g)
71    end
72  | SOME (v, _) => (defs, v);
73
74fun gen_cnf defs tm =
75  if is_conj tm then
76    def_step (sub_cnf gen_cnf conjunction defs (dest_conj tm))
77  else if is_disj tm then
78    def_step (sub_cnf gen_cnf disjunction defs (dest_disj tm))
79  else if is_beq tm then
80    def_step (sub_cnf gen_cnf beq defs (dest_beq tm))
81  else
82    (defs, tm);
83
84fun disj_cnf defs tm =
85  if is_disj tm then sub_cnf disj_cnf disjunction defs (dest_disj tm)
86  else gen_cnf defs tm;
87
88fun conj_cnf defs tm =
89  if is_conj tm then sub_cnf conj_cnf conjunction defs (dest_conj tm)
90  else disj_cnf defs tm;
91
92val DISCH_CONJ = CONV_RULE (REWR_CONV AND_IMP_INTRO) o uncurry DISCH;
93
94val UNIQUE_CONV = let
95  val v = mk_var("v", numSyntax.num --> bool)
96in
97  FIRST_CONV (map (REWR_CONV o GEN v o SYM) (CONJUNCTS UNIQUE_def))
98end
99
100val DEF_CONV = (REWR_CONV o GSYM o CONJUNCT2) DEF_def;
101
102val FINAL_DEF_CONV =
103  REWR_CONV FINAL_DEF THENC
104  RAND_CONV (RATOR_CONV (RAND_CONV REDUCE_CONV));
105
106fun TODEF_CONV tm =
107  ((if is_conj tm then RAND_CONV TODEF_CONV else FINAL_DEF_CONV) THENC
108   LAND_CONV UNIQUE_CONV THENC
109   RAND_CONV (RATOR_CONV (RAND_CONV num_CONV)) THENC
110   DEF_CONV) tm;
111
112val AND_TRUEL_CONV = REWR_CONV (CONJUNCT1 (SPEC_ALL AND_CLAUSES));
113
114local
115  val OKDEF1_CONV = REWR_CONV (CONJUNCT1 OKDEF_def);
116  val OKDEF2_CONV = REWR_CONV (CONJUNCT2 OKDEF_def);
117in
118  fun OKDEF_CONV tm =
119    (OKDEF1_CONV ORELSEC
120     (OKDEF2_CONV THENC
121      LAND_CONV (REWRITE_CONV [OK_def] THENC REDUCE_CONV) THENC
122      AND_TRUEL_CONV THENC
123      RATOR_CONV (RAND_CONV REDUCE_CONV) THENC
124      OKDEF_CONV)) tm;
125end;
126
127fun ELIM_DEFS tm =
128  let
129    val th1 = SYM (QUANT_CONV TODEF_CONV tm)
130    val l = rand (snd (dest_exists (lhs (concl th1))))
131    val th2 = OKDEF_CONV (mk_comb (mk_comb (OKDEF, zero), l))
132  in
133    EQ_MP th1 (MATCH_MP CONSISTENCY (EQT_ELIM th2))
134  end;
135
136val ELIM_DEFS_CONV = EQT_INTRO o ELIM_DEFS;
137
138val pure_def_cnf_cleanup =
139  CONV_RULE (LAND_CONV ((LAND_CONV ELIM_DEFS_CONV) THENC AND_TRUEL_CONV));
140
141val dcnfgv = ref (K (genvar (num --> bool)))
142val ndefs = ref T
143
144fun PURE_DEF_CNF_VECTOR_CONV tm =
145  let
146    (*val (defs, tm') = conj_cnf (genvar (num --> bool), zero, []) tm*)
147    val (defs, tm') = conj_cnf ((!dcnfgv)(), zero, []) tm
148    val (vec, n, ds) = defs
149    val _ = (ndefs:=n)
150    val eqs = map mk_eq ds
151    val th1 = SYM (REWRITE_CONV (map ASSUME eqs) tm')
152  in
153    case eqs of [] => th1
154    | eq :: rest =>
155    let
156      val th2 = GEN vec (foldl DISCH_CONJ (DISCH eq th1) rest)
157      val th3 = HO_MATCH_MP BIGSTEP th2
158    in
159      pure_def_cnf_cleanup th3
160    end
161  end;
162
163val DEF_CNF_VECTOR_CONV =
164  DEF_NNF_CONV THENC PURE_DEF_CNF_VECTOR_CONV THENC CLEANUP_DEF_CNF_CONV;
165
166(* Quick testing
167val Term = Parse.Term;
168val Type = Parse.Type;
169show_assums := true;
170Globals.guessing_tyvars := true;
171app load ["normalFormsTest", "numLib", "arithmeticTheory", "bossLib"];
172open normalFormsTest numLib arithmeticTheory bossLib;
173Parse.reveal "C";
174val DEF_CNF_CONV' =
175  time DEF_NNF_CONV THENC
176  time PURE_DEF_CNF_VECTOR_CONV THENC
177  time CLEANUP_DEF_CNF_CONV;
178
179val th = DEF_CNF_CONV' ``~(p = q) ==> q /\ r``;
180PRETTIFY_VARS_CONV (rhs (concl th));
181
182try DEF_NNF_CONV ``~(p = ~(q = r)) = ~(~(p = q) = r)``;
183try (DEF_CNF_CONV' THENC PRETTIFY_VARS_CONV)
184  ``~(p = ~(q = r)) = ~(~(p = q) = r)``;
185try DEF_CNF_CONV ``(p /\ (q \/ r /\ s)) /\ (~p \/ ~q \/ ~s)``;
186
187(* Large formulas *)
188
189val valid1 = time (mk_neg o Term) valid_1;
190
191val _ = time DEF_CNF_CONV' valid1;
192
193(* The pigeon-hole principle *)
194
195fun test n = (((time DEF_CNF_CONV') o time (mk_neg o var_pigeon)) n; n);
196
197test 8;
198test 9;
199test 10;
200test 11;
201test 12;
202test 13;
203test 14;
204test 15;
205test 16;
206test 17;
207test 18;
208test 19;
209test 20;
210
211*)
212
213end
214