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