1(* ========================================================================= *)
2(* PROBLEMS TO TEST THE HOL NORMALIZATION FUNCTIONS.                         *)
3(* Created by Joe Hurd, October 2001                                         *)
4(* ========================================================================= *)
5
6(*
7app load ["numLib"];
8*)
9
10(*
11*)
12structure normalFormsTest :> normalFormsTest =
13struct
14
15open HolKernel Parse boolLib numLib;
16
17infixr -->;
18
19(* ------------------------------------------------------------------------- *)
20(* The pigeon-hole principle, courtesy of Konrad Slind.                      *)
21(* ------------------------------------------------------------------------- *)
22
23val num = mk_type ("num", []);
24
25fun upto b t = if b >= t then [] else b :: upto (b + 1) t;
26
27fun number i [] = []
28  | number i (h :: t) = i :: number (i + 1) t;
29
30fun num_of_int i = mk_numeral (Arbnum.fromInt i)
31
32fun ith_var ty i = mk_var ("v" ^ int_to_string i, ty);
33
34val P = mk_var ("P", num --> num --> bool);
35
36fun mkP i j = list_mk_comb (P, [num_of_int i, num_of_int j]);
37
38fun row i j = list_mk_disj (map (mkP i) (upto 0 j));
39
40fun pigeon k =
41 let
42   fun shares Pi plist =
43     let
44       fun row j =
45         mk_conj
46         (mk_comb (Pi, num_of_int j), list_mk_disj (map (C mkP j) plist))
47      in
48        list_mk_disj(map row (upto 0 k))
49      end
50     fun sharesl _ [] = []
51       | sharesl i alist =
52       shares (mk_comb (P, num_of_int i)) alist :: sharesl (i + 1) (tl alist)
53   val in_holes = list_mk_conj (map (C row k) (upto 0 (k + 1)))
54   val Sharing = list_mk_disj (sharesl 0 (tl (upto 0 (k+1))))
55 in
56   mk_disj (mk_neg in_holes, Sharing)
57 end;
58
59fun dest_term tm = SOME
60  (dest_conj tm handle HOL_ERR _ =>
61   dest_disj tm handle HOL_ERR _ =>
62   dest_imp tm) handle HOL_ERR _ => NONE;
63
64fun atoms_of tm =
65 let
66   fun traverse tm s =
67     case dest_term tm of NONE => Binaryset.add (s,tm)
68     | SOME (x, y) => traverse x (traverse y s)
69   val set = traverse tm (Binaryset.empty Term.compare)
70 in
71   Binaryset.listItems set
72 end;
73
74fun varify tm =
75 let
76   val atoms = atoms_of tm
77   val theta = map2 (curry op|->) atoms (map (ith_var bool) (number 0 atoms))
78 in
79   subst theta tm
80 end;
81
82val var_pigeon = varify o pigeon;
83
84(* ------------------------------------------------------------------------- *)
85(* Large formulas.                                                           *)
86(* ------------------------------------------------------------------------- *)
87
88(* An example from Mike, originally called add4. *)
89
90val valid_1 =
91 `(N3 = A_0_) /\
92  (N4 = A_2_) /\
93  (N5 = A_4_) /\
94  (N6 = A_5_) /\
95  (N7 = A_6_) /\
96  (N8 = A_8_) /\
97  (N9 = A_3_) /\
98  (N10 = A_7_) /\
99  (N11 = A_9_) /\
100  (N12 = A_11_) /\
101  (N13 = A_1_) /\
102  (N14 = A_10_) /\
103  (N15 = ANDA) /\
104  (N16 = EXORA) /\
105  (N17 = B_3_) /\
106  (N18 = B_4_) /\
107  (N19 = B_6_) /\
108  (N20 = B_1_) /\
109  (N21 = B_7_) /\
110  (N22 = B_9_) /\
111  (N23 = B_2_) /\
112  (N24 = B_5_) /\
113  (N25 = B_8_) /\
114  (N26 = B_10_) /\
115  (N27 = B_11_) /\
116  (N28 = B_0_) /\
117  (N29 = ANDB) /\
118  (N30 = EXORB) /\
119  (N31 = CARRYIN) /\
120  (N98 = ~N29) /\
121  (N104 = ~N30) /\
122  (N97 = ~N15) /\
123  (N103 = ~N16) /\
124  (N102 = ~N31) /\
125  (N105 = ~N102) /\
126  (N243 = ~N14 \/ ~N97) /\
127  (N235 = ~N103) /\
128  (N244 = ~N26 \/ ~N98) /\
129  (N236 = ~N104) /\
130  (N224 = ~N22 \/ ~N98) /\
131  (N232 = ~N104) /\
132  (N223 = ~N11 \/ ~N97) /\
133  (N231 = ~N103) /\
134  (N217 = ~N8 \/ ~N97) /\
135  (N209 = ~N103) /\
136  (N218 = ~N25 \/ ~N98) /\
137  (N210 = ~N104) /\
138  (N197 = ~N21 \/ ~N98) /\
139  (N206 = ~N104) /\
140  (N196 = ~N10 \/ ~N97) /\
141  (N205 = ~N103) /\
142  (N190 = ~N19 \/ ~N98) /\
143  (N182 = ~N104) /\
144  (N189 = ~N7 \/ ~N97) /\
145  (N181 = ~N103) /\
146  (N251 = ~N27 \/ ~N98) /\
147  (N259 = ~N104) /\
148  (N250 = ~N12 \/ ~N97) /\
149  (N258 = ~N103) /\
150  (N163 = ~N18 \/ ~N98) /\
151  (N155 = ~N104) /\
152  (N162 = ~N5 \/ ~N97) /\
153  (N154 = ~N103) /\
154  (N170 = ~N24 \/ ~N98) /\
155  (N178 = ~N104) /\
156  (N169 = ~N6 \/ ~N97) /\
157  (N177 = ~N103) /\
158  (N136 = ~N23 \/ ~N98) /\
159  (N128 = ~N104) /\
160  (N135 = ~N4 \/ ~N97) /\
161  (N127 = ~N103) /\
162  (N116 = ~N20 \/ ~N98) /\
163  (N124 = ~N104) /\
164  (N115 = ~N13 \/ ~N97) /\
165  (N123 = ~N103) /\
166  (N110 = ~N28 \/ ~N98) /\
167  (N100 = ~N104) /\
168  (N109 = ~N3 \/ ~N97) /\
169  (N99 = ~N103) /\
170  (N142 = ~N17 \/ ~N98) /\
171  (N150 = ~N104) /\
172  (N141 = ~N9 \/ ~N97) /\
173  (N149 = ~N103) /\
174  (N87 = ~N243) /\
175  (N89 = ~N244) /\
176  (N83 = ~N224) /\
177  (N85 = ~N223) /\
178  (N79 = ~N217) /\
179  (N81 = ~N218) /\
180  (N75 = ~N197) /\
181  (N77 = ~N196) /\
182  (N73 = ~N190) /\
183  (N71 = ~N189) /\
184  (N91 = ~N251) /\
185  (N93 = ~N250) /\
186  (N65 = ~N163) /\
187  (N63 = ~N162) /\
188  (N67 = ~N170) /\
189  (N69 = ~N169) /\
190  (N57 = ~N136) /\
191  (N55 = ~N135) /\
192  (N51 = ~N116) /\
193  (N53 = ~N115) /\
194  (N49 = ~N110) /\
195  (N47 = ~N109) /\
196  (N59 = ~N142) /\
197  (N61 = ~N141) /\
198  (N241 = N87 /\ N103 \/ ~N87 /\ ~N103) /\
199  (N242 = N89 /\ N104 \/ ~N89 /\ ~N104) /\
200  (N227 = N83 /\ N104 \/ ~N83 /\ ~N104) /\
201  (N226 = N85 /\ N103 \/ ~N85 /\ ~N103) /\
202  (N215 = N79 /\ N103 \/ ~N79 /\ ~N103) /\
203  (N216 = N81 /\ N104 \/ ~N81 /\ ~N104) /\
204  (N200 = N75 /\ N104 \/ ~N75 /\ ~N104) /\
205  (N199 = N77 /\ N103 \/ ~N77 /\ ~N103) /\
206  (N188 = N73 /\ N104 \/ ~N73 /\ ~N104) /\
207  (N187 = N71 /\ N103 \/ ~N71 /\ ~N103) /\
208  (N254 = N91 /\ N104 \/ ~N91 /\ ~N104) /\
209  (N253 = N93 /\ N103 \/ ~N93 /\ ~N103) /\
210  (N160 = N65 /\ N104 \/ ~N65 /\ ~N104) /\
211  (N159 = N63 /\ N103 \/ ~N63 /\ ~N103) /\
212  (N173 = N67 /\ N104 \/ ~N67 /\ ~N104) /\
213  (N172 = N69 /\ N103 \/ ~N69 /\ ~N103) /\
214  (N134 = N57 /\ N104 \/ ~N57 /\ ~N104) /\
215  (N133 = N55 /\ N103 \/ ~N55 /\ ~N103) /\
216  (N119 = N51 /\ N104 \/ ~N51 /\ ~N104) /\
217  (N118 = N53 /\ N103 \/ ~N53 /\ ~N103) /\
218  (N108 = N49 /\ N104 \/ ~N49 /\ ~N104) /\
219  (N107 = N47 /\ N103 \/ ~N47 /\ ~N103) /\
220  (N145 = N59 /\ N104 \/ ~N59 /\ ~N104) /\
221  (N144 = N61 /\ N103 \/ ~N61 /\ ~N103) /\
222  (N88 = ~N241) /\
223  (N90 = ~N242) /\
224  (N84 = ~N227) /\
225  (N86 = ~N226) /\
226  (N80 = ~N215) /\
227  (N82 = ~N216) /\
228  (N76 = ~N200) /\
229  (N78 = ~N199) /\
230  (N74 = ~N188) /\
231  (N72 = ~N187) /\
232  (N92 = ~N254) /\
233  (N94 = ~N253) /\
234  (N66 = ~N160) /\
235  (N64 = ~N159) /\
236  (N68 = ~N173) /\
237  (N70 = ~N172) /\
238  (N58 = ~N134) /\
239  (N56 = ~N133) /\
240  (N52 = ~N119) /\
241  (N54 = ~N118) /\
242  (N50 = ~N108) /\
243  (N48 = ~N107) /\
244  (N60 = ~N145) /\
245  (N62 = ~N144) /\
246  (N234 = ~N88) /\
247  (N230 = ~N86) /\
248  (N208 = ~N80) /\
249  (N204 = ~N78) /\
250  (N180 = ~N72) /\
251  (N257 = ~N94) /\
252  (N152 = ~N64) /\
253  (N176 = ~N70) /\
254  (N126 = ~N56) /\
255  (N122 = ~N54) /\
256  (N96 = ~N48) /\
257  (N148 = ~N62) /\
258  (N237 = N90 /\ N88 \/ ~N90 /\ ~N88) /\
259  (N229 = N84 /\ N86 \/ ~N84 /\ ~N86) /\
260  (N211 = N82 /\ N80 \/ ~N82 /\ ~N80) /\
261  (N203 = N76 /\ N78 \/ ~N76 /\ ~N78) /\
262  (N183 = N74 /\ N72 \/ ~N74 /\ ~N72) /\
263  (N256 = N92 /\ N94 \/ ~N92 /\ ~N94) /\
264  (N156 = N66 /\ N64 \/ ~N66 /\ ~N64) /\
265  (N175 = N68 /\ N70 \/ ~N68 /\ ~N70) /\
266  (N129 = N58 /\ N56 \/ ~N58 /\ ~N56) /\
267  (N121 = N52 /\ N54 \/ ~N52 /\ ~N54) /\
268  (N101 = N50 /\ N48 \/ ~N50 /\ ~N48) /\
269  (N147 = N60 /\ N62 \/ ~N60 /\ ~N62) /\
270  (N233 = ~N237) /\
271  (N221 = ~N229) /\
272  (N207 = ~N211) /\
273  (N193 = ~N203) /\
274  (N179 = ~N183) /\
275  (N248 = ~N256) /\
276  (N151 = ~N156) /\
277  (N166 = ~N175) /\
278  (N125 = ~N129) /\
279  (N113 = ~N121) /\
280  (N95 = ~N101) /\
281  (N139 = ~N147) /\
282  (N245 = ~N233) /\
283  (N228 = ~N221) /\
284  (N219 = ~N207) /\
285  (N167 = ~N166 \/ ~N151 \/ ~N179 \/ ~N193) /\
286  (N202 = ~N193) /\
287  (N191 = ~N179) /\
288  (N255 = ~N248) /\
289  (N164 = ~N151) /\
290  (N174 = ~N166) /\
291  (N137 = ~N125) /\
292  (N120 = ~N113) /\
293  (N111 = ~N95) /\
294  (N146 = ~N139) /\
295  (N106 = N105 /\ ~N95 \/ ~N105 /\ N95) /\
296  (N161 = ~N167) /\
297  (N112 = ~N95 /\ ~N48 \/ ~N111 /\ ~N102) /\
298  (N114 = ~N112) /\
299  (N39 = ~N106) /\
300  (N130 = ~N120 /\ ~N112 \/ ~N122 /\ ~N113) /\
301  (N117 = N114 /\ N113 \/ ~N114 /\ ~N113) /\
302  (N131 = ~N130) /\
303  (N138 = ~N125 /\ ~N56 \/ ~N137 /\ ~N130) /\
304  (N32 = ~N117) /\
305  (N132 = N131 /\ ~N125 \/ ~N131 /\ N125) /\
306  (N153 = ~N146 /\ ~N138 \/ ~N148 /\ ~N139) /\
307  (N140 = ~N138) /\
308  (N37 = ~N132) /\
309  (N157 = ~N153) /\
310  (N165 = ~N151 /\ ~N64 \/ ~N164 /\ ~N153) /\
311  (N143 = N140 /\ N139 \/ ~N140 /\ ~N139) /\
312  (N158 = N157 /\ ~N151 \/ ~N157 /\ N151) /\
313  (N184 = ~N174 /\ ~N165 \/ ~N176 /\ ~N166) /\
314  (N168 = ~N165) /\
315  (N33 = ~N143) /\
316  (N43 = ~N158) /\
317  (N185 = ~N184) /\
318  (N192 = ~N179 /\ ~N72 \/ ~N191 /\ ~N184) /\
319  (N171 = N168 /\ N166 \/ ~N168 /\ ~N166) /\
320  (N195 = ~N192) /\
321  (N186 = N185 /\ ~N179 \/ ~N185 /\ N179) /\
322  (N201 = ~N202 /\ ~N192 \/ ~N204 /\ ~N193) /\
323  (N34 = ~N171) /\
324  (N198 = N195 /\ N193 \/ ~N195 /\ ~N193) /\
325  (N35 = ~N186) /\
326  (N194 = ~N167 /\ ~N153 \/ ~N161 /\ ~N201) /\
327  (N36 = ~N198) /\
328  (N212 = ~N194) /\
329  (N213 = ~N212) /\
330  (N220 = ~N207 /\ ~N80 \/ ~N219 /\ ~N212) /\
331  (N214 = N213 /\ ~N207 \/ ~N213 /\ N207) /\
332  (N222 = ~N220) /\
333  (N238 = ~N228 /\ ~N220 \/ ~N230 /\ ~N221) /\
334  (N38 = ~N214) /\
335  (N225 = N222 /\ N221 \/ ~N222 /\ ~N221) /\
336  (N239 = ~N238) /\
337  (N246 = ~N233 /\ ~N88 \/ ~N245 /\ ~N238) /\
338  (N40 = ~N225) /\
339  (N240 = N239 /\ ~N233 \/ ~N239 /\ N233) /\
340  (N261 = ~N255 /\ ~N246 \/ ~N257 /\ ~N248) /\
341  (N249 = ~N246) /\
342  (N262 = N261 /\ N246 \/ ~N261 /\ ~N246) /\
343  (N41 = ~N240) /\
344  (N44 = ~N261) /\
345  (N252 = N249 /\ N248 \/ ~N249 /\ ~N248) /\
346  (N45 = ~N262) /\
347  (N42 = ~N252) /\
348  (N46 = ~N42) /\
349  (O_4_ = N43) /\
350  (O_11_ = N42) /\
351  (O_10_ = N41) /\
352  (O_9_ = N40) /\
353  (O_0_ = N39) /\
354  (O_8_ = N38) /\
355  (O_2_ = N37) /\
356  (O_7_ = N36) /\
357  (O_6_ = N35) /\
358  (O_5_ = N34) /\
359  (O_3_ = N33) /\
360  (O_1_ = N32) /\
361  (AFTBUF1 = ~ANDA) /\
362  (AFTBUF2 = ~ANDB) /\
363  (AFTBUF3 = ~EXORA) /\
364  (AFTBUF4 = ~EXORB) /\
365  (AFTBUF5 = ~CARRYIN) /\
366  (N1_0_ = AFTBUF1 /\ A_0_) /\
367  (N1_1_ = AFTBUF1 /\ A_1_) /\
368  (N1_2_ = AFTBUF1 /\ A_2_) /\
369  (N1_3_ = AFTBUF1 /\ A_3_) /\
370  (N1_4_ = AFTBUF1 /\ A_4_) /\
371  (N1_5_ = AFTBUF1 /\ A_5_) /\
372  (N1_6_ = AFTBUF1 /\ A_6_) /\
373  (N1_7_ = AFTBUF1 /\ A_7_) /\
374  (N1_8_ = AFTBUF1 /\ A_8_) /\
375  (N1_9_ = AFTBUF1 /\ A_9_) /\
376  (N1_10_ = AFTBUF1 /\ A_10_) /\
377  (N1_11_ = AFTBUF1 /\ A_11_) /\
378  (N3_0_ = AFTBUF2 /\ B_0_) /\
379  (N3_1_ = AFTBUF2 /\ B_1_) /\
380  (N3_2_ = AFTBUF2 /\ B_2_) /\
381  (N3_3_ = AFTBUF2 /\ B_3_) /\
382  (N3_4_ = AFTBUF2 /\ B_4_) /\
383  (N3_5_ = AFTBUF2 /\ B_5_) /\
384  (N3_6_ = AFTBUF2 /\ B_6_) /\
385  (N3_7_ = AFTBUF2 /\ B_7_) /\
386  (N3_8_ = AFTBUF2 /\ B_8_) /\
387  (N3_9_ = AFTBUF2 /\ B_9_) /\
388  (N3_10_ = AFTBUF2 /\ B_10_) /\
389  (N3_11_ = AFTBUF2 /\ B_11_) /\
390  (N2_0_ = AFTBUF3 /\ ~N1_0_ \/ ~AFTBUF3 /\ N1_0_) /\
391  (N2_1_ = AFTBUF3 /\ ~N1_1_ \/ ~AFTBUF3 /\ N1_1_) /\
392  (N2_2_ = AFTBUF3 /\ ~N1_2_ \/ ~AFTBUF3 /\ N1_2_) /\
393  (N2_3_ = AFTBUF3 /\ ~N1_3_ \/ ~AFTBUF3 /\ N1_3_) /\
394  (N2_4_ = AFTBUF3 /\ ~N1_4_ \/ ~AFTBUF3 /\ N1_4_) /\
395  (N2_5_ = AFTBUF3 /\ ~N1_5_ \/ ~AFTBUF3 /\ N1_5_) /\
396  (N2_6_ = AFTBUF3 /\ ~N1_6_ \/ ~AFTBUF3 /\ N1_6_) /\
397  (N2_7_ = AFTBUF3 /\ ~N1_7_ \/ ~AFTBUF3 /\ N1_7_) /\
398  (N2_8_ = AFTBUF3 /\ ~N1_8_ \/ ~AFTBUF3 /\ N1_8_) /\
399  (N2_9_ = AFTBUF3 /\ ~N1_9_ \/ ~AFTBUF3 /\ N1_9_) /\
400  (N2_10_ = AFTBUF3 /\ ~N1_10_ \/ ~AFTBUF3 /\ N1_10_) /\
401  (N2_11_ = AFTBUF3 /\ ~N1_11_ \/ ~AFTBUF3 /\ N1_11_) /\
402  (N4_0_ = AFTBUF4 /\ ~N3_0_ \/ ~AFTBUF4 /\ N3_0_) /\
403  (N4_1_ = AFTBUF4 /\ ~N3_1_ \/ ~AFTBUF4 /\ N3_1_) /\
404  (N4_2_ = AFTBUF4 /\ ~N3_2_ \/ ~AFTBUF4 /\ N3_2_) /\
405  (N4_3_ = AFTBUF4 /\ ~N3_3_ \/ ~AFTBUF4 /\ N3_3_) /\
406  (N4_4_ = AFTBUF4 /\ ~N3_4_ \/ ~AFTBUF4 /\ N3_4_) /\
407  (N4_5_ = AFTBUF4 /\ ~N3_5_ \/ ~AFTBUF4 /\ N3_5_) /\
408  (N4_6_ = AFTBUF4 /\ ~N3_6_ \/ ~AFTBUF4 /\ N3_6_) /\
409  (N4_7_ = AFTBUF4 /\ ~N3_7_ \/ ~AFTBUF4 /\ N3_7_) /\
410  (N4_8_ = AFTBUF4 /\ ~N3_8_ \/ ~AFTBUF4 /\ N3_8_) /\
411  (N4_9_ = AFTBUF4 /\ ~N3_9_ \/ ~AFTBUF4 /\ N3_9_) /\
412  (N4_10_ = AFTBUF4 /\ ~N3_10_ \/ ~AFTBUF4 /\ N3_10_) /\
413  (N4_11_ = AFTBUF4 /\ ~N3_11_ \/ ~AFTBUF4 /\ N3_11_) /\
414  (COUT1 = AFTBUF5 /\ N4_0_ \/ AFTBUF5 /\ N2_0_ \/ N4_0_ /\ N2_0_) /\
415  (COUT2 = COUT1 /\ N4_1_ \/ COUT1 /\ N2_1_ \/ N4_1_ /\ N2_1_) /\
416  (COUT3 = COUT2 /\ N4_2_ \/ COUT2 /\ N2_2_ \/ N4_2_ /\ N2_2_) /\
417  (COUT4 = COUT3 /\ N4_3_ \/ COUT3 /\ N2_3_ \/ N4_3_ /\ N2_3_) /\
418  (COUT5 = COUT4 /\ N4_4_ \/ COUT4 /\ N2_4_ \/ N4_4_ /\ N2_4_) /\
419  (COUT6 = COUT5 /\ N4_5_ \/ COUT5 /\ N2_5_ \/ N4_5_ /\ N2_5_) /\
420  (COUT7 = COUT6 /\ N4_6_ \/ COUT6 /\ N2_6_ \/ N4_6_ /\ N2_6_) /\
421  (COUT8 = COUT7 /\ N4_7_ \/ COUT7 /\ N2_7_ \/ N4_7_ /\ N2_7_) /\
422  (COUT9 = COUT8 /\ N4_8_ \/ COUT8 /\ N2_8_ \/ N4_8_ /\ N2_8_) /\
423  (COUT10 = COUT9 /\ N4_9_ \/ COUT9 /\ N2_9_ \/ N4_9_ /\ N2_9_) /\
424  (COUT11 = COUT10 /\ N4_10_ \/ COUT10 /\ N2_10_ \/ N4_10_ /\ N2_10_) /\
425  (HULP0 = ~(N2_0_ = ~(N4_0_ = AFTBUF5))) /\
426  (HULP1 = ~(N2_1_ = ~(N4_1_ = COUT1))) /\
427  (HULP2 = ~(N2_2_ = ~(N4_2_ = COUT2))) /\
428  (HULP3 = ~(N2_3_ = ~(N4_3_ = COUT3))) /\
429  (HULP4 = ~(N2_4_ = ~(N4_4_ = COUT4))) /\
430  (HULP5 = ~(N2_5_ = ~(N4_5_ = COUT5))) /\
431  (HULP6 = ~(N2_6_ = ~(N4_6_ = COUT6))) /\
432  (HULP7 = ~(N2_7_ = ~(N4_7_ = COUT7))) /\
433  (HULP8 = ~(N2_8_ = ~(N4_8_ = COUT8))) /\
434  (HULP9 = ~(N2_9_ = ~(N4_9_ = COUT9))) /\
435  (HULP10 = ~(N2_10_ = ~(N4_10_ = COUT10))) /\
436  (HULP11 = ~(N2_11_ = ~(N4_11_ = COUT11))) /\
437  (HULP12 = COUT11 /\ N4_11_ \/ COUT11 /\ N2_11_ \/  N4_11_ /\ N2_11_)
438  ==> (O_0_ = HULP0) /\
439      (O_1_ = HULP1) /\
440      (O_2_ = HULP2) /\
441      (O_3_ = HULP3) /\
442      (O_4_ = HULP4) /\
443      (O_5_ = HULP5) /\
444      (O_6_ = HULP6) /\
445      (O_7_ = HULP7) /\
446      (O_8_ = HULP8) /\
447      (O_9_ = HULP9) /\
448      (O_10_ = HULP10) /\
449      (O_11_ =  HULP11)`;
450
451(* Quick testing
452app load ["normalForms", "HolSatLib"];
453open canonTools;
454
455val N = mk_neg;
456
457val DN_valid1 = time DEF_CNF_CONV (N valid1);
458val DNS_valid1 = time (snd o strip_exists o rhs o concl) DN_valid1;
459val DNS_SAT_valid1 = time (HolSatLib.satOracle HolSatLib.zchaff) DNS_valid1;
460(* Parsing:     runtime: 7.810s,   gctime: 3.450s,   systime: 0.000s. *)
461(* Normalizing: runtime: 897.030s, gctime: 446.330s, systime: 1.270s. *)
462(* Stripping:   runtime: 48.160s,  gctime: 26.200s,  systime: 0.020s. *)
463(* SAT solving: runtime: 7.480s,   gctime: 0.090s,   systime: 0.020s. *)
464
465(* These generate propositional encodings of the pigeon-hole principle. *)
466val pigeon1 = time var_pigeon 1;   (* runtime: 0.000s,     gctime: 0.000s  *)
467val pigeon2 = time var_pigeon 2;   (* runtime: 0.020s,     gctime: 0.010s  *)
468val pigeon3 = time var_pigeon 3;   (* runtime: 0.020s,     gctime: 0.000s  *)
469val pigeon4 = time var_pigeon 4;   (* runtime: 0.060s,     gctime: 0.000s  *)
470val pigeon5 = time var_pigeon 5;   (* runtime: 0.120s,     gctime: 0.000s  *)
471val pigeon6 = time var_pigeon 6;   (* runtime: 0.250s,     gctime: 0.010s  *)
472val pigeon7 = time var_pigeon 7;   (* runtime: 0.450s,     gctime: 0.000s  *)
473val pigeon8 = time var_pigeon 8;   (* runtime: 0.810s,     gctime: 0.020s  *)
474val pigeon9 = time var_pigeon 9;   (* runtime: 1.320s,     gctime: 0.010s  *)
475val pigeon10 = time var_pigeon 10; (* runtime: 2.050s,     gctime: 0.030s  *)
476val pigeon20 = time var_pigeon 20; (* runtime: 49.340s,    gctime: 0.510s  *)
477
478(* These result in a large CNF formula that is unsatisfiable. *)
479time CNF_CONV (N pigeon1);         (* runtime: 0.010s,     gctime: 0.000s  *)
480time CNF_CONV (N pigeon2);         (* runtime: 0.050s,     gctime: 0.020s  *)
481time CNF_CONV (N pigeon3);         (* runtime: 0.140s,     gctime: 0.010s  *)
482time CNF_CONV (N pigeon4);         (* runtime: 0.300s,     gctime: 0.050s  *)
483time CNF_CONV (N pigeon10);        (* runtime: 4.960s,     gctime: 0.320s  *)
484time CNF_CONV (N pigeon20);        (* runtime: 111.780s,   gctime: 4.750s  *)
485
486(* Without tautology checking, so result in (very) large CNF formulas. *)
487tautology_checking := false;
488time CNF_CONV pigeon1;             (* runtime: 0.010s,     gctime: 0.000s  *)
489time CNF_CONV pigeon2;             (* runtime: 0.780s,     gctime: 0.060s  *)
490(* time CNF_CONV pigeon3;             runtime: 23623.570s, gctime: 1739.000s *)
491
492(* These reduce the formulas to T, thus proving them. *)
493tautology_checking := true;
494time CNF_CONV pigeon1;             (* runtime: 0.010s,     gctime: 0.010s  *)
495time CNF_CONV pigeon2;             (* runtime: 0.370s,     gctime: 0.030s  *)
496time CNF_CONV pigeon3;             (* runtime: 104.530s,   gctime: 7.640s  *)
497(* time CNF_CONV pigeon4;  didn't finish after >7 hours                    *)
498
499(* Putting formulas in definitional CNF results in only a linear expansion *)
500time DEF_CNF_CONV (N pigeon1);     (* runtime: 0.070s,     gctime: 0.000s  *)
501time DEF_CNF_CONV (N pigeon2);     (* runtime: 0.460s,     gctime: 0.100s  *)
502time DEF_CNF_CONV (N pigeon3);     (* runtime: 1.460s,     gctime: 0.210s  *)
503time DEF_CNF_CONV (N pigeon4);     (* runtime: 3.770s,     gctime: 0.770s  *)
504time DEF_CNF_CONV (N pigeon5);     (* runtime: 8.590s,     gctime: 1.990s  *)
505time DEF_CNF_CONV (N pigeon6);     (* runtime: 17.360s,    gctime: 3.880s  *)
506time DEF_CNF_CONV (N pigeon7);     (* runtime: 33.990s,    gctime: 7.700s  *)
507time DEF_CNF_CONV (N pigeon8);     (* runtime: 63.180s,    gctime: 15.400s *)
508time DEF_CNF_CONV (N pigeon9);     (* runtime: 111.540s,   gctime: 27.510s *)
509time DEF_CNF_CONV (N pigeon10);    (* runtime: 187.620s,   gctime: 47.150s *)
510
511time DEF_CNF_CONV pigeon1;         (* runtime: 0.080s,     gctime: 0.000s  *)
512time DEF_CNF_CONV pigeon2;         (* runtime: 0.470s,     gctime: 0.070s  *)
513time DEF_CNF_CONV pigeon3;         (* runtime: 1.480s,     gctime: 0.310s  *)
514time DEF_CNF_CONV pigeon4;         (* runtime: 3.600s,     gctime: 0.580s  *)
515time DEF_CNF_CONV pigeon5;         (* runtime: 8.000s,     gctime: 1.550s  *)
516time DEF_CNF_CONV pigeon6;         (* runtime: 16.370s,    gctime: 3.240s  *)
517time DEF_CNF_CONV pigeon7;         (* runtime: 32.280s,    gctime: 7.100s  *)
518time DEF_CNF_CONV pigeon8;         (* runtime: 59.860s,    gctime: 14.120s *)
519time DEF_CNF_CONV pigeon9;         (* runtime: 105.650s,   gctime: 25.410s *)
520time DEF_CNF_CONV pigeon10;        (* runtime: 179.030s,   gctime: 42.820s *)
521*)
522
523end
524