1(*--------------------------------------------------------------------------- 2 A type of propositions and a few algorithms on it. 3 ---------------------------------------------------------------------------*) 4 5app load ["bossLib"]; open bossLib; 6 7 8Hol_datatype `prop = VAR of 'a 9 | NOT of prop 10 | AND of prop => prop 11 | OR of prop => prop`; 12 13 14(*--------------------------------------------------------------------------- 15 Wang's algorithm (implements the sequent calculus). 16 ---------------------------------------------------------------------------*) 17 18val Pr_def = 19 Hol_defn "Pr" 20 `(Pr vl [] (VAR v::r) vr = Pr vl [] r (v::vr)) 21 /\ (Pr vl [] (NOT x::r) vr = Pr vl [x] r vr) 22 /\ (Pr vl [] (OR x y::r) vr = Pr vl [] (x::y::r) vr) 23 /\ (Pr vl [] (AND x y::r) vr = Pr vl [] (x::r) vr /\ Pr vl [] (y::r) vr) 24 25 /\ (Pr vl (VAR v::l) r vr = Pr (v::vl) l r vr) 26 /\ (Pr vl (NOT x::l) r vr = Pr vl l (x::r) vr) 27 /\ (Pr vl (AND x y::l) r vr = Pr vl (x::y::l) r vr) 28 /\ (Pr vl (OR x y::l) r vr = Pr vl (x::l) r vr /\ Pr vl (y::l) r vr) 29 /\ (Pr vl [] [] vr = EXISTS (\y. MEM y vl) vr)`; 30 31 32val Wang_def = Define `Wang P = Pr [] [] [P] []`; 33 34set_fixity "OR" (Infixr 300); 35set_fixity "AND" (Infixr 400); 36 37(*--------------------------------------------------------------------------- 38 Termination of Pr. We need a subsidiary measure function on 39 propositions which makes a 2-argument proposition bigger than a 40 list of 2 propositions. 41 ---------------------------------------------------------------------------*) 42 43val Meas_def = 44 Define 45 `(Meas (VAR v) = 0) 46 /\ (Meas (NOT x) = SUC (Meas x)) 47 /\ (Meas (x AND y) = Meas x + Meas y + 2) 48 /\ (Meas (x OR y) = Meas x + Meas y + 2)`; 49 50(*---------------------------------------------------------------------------* 51 * Termination of Pr. * 52 *---------------------------------------------------------------------------*) 53 54val (Pr_eqns, Pr_ind) = 55 Defn.tprove (Pr_def, 56 WF_REL_TAC 57 `measure \(w:'a list, x:'a prop list, y:'a prop list, z:'a list). 58 list_size Meas x + list_size Meas y` 59 THEN RW_TAC arith_ss [Meas_def,listTheory.list_size_def]); 60 61(*--------------------------------------------------------------------------- 62 Examples. 63 ---------------------------------------------------------------------------*) 64 65val x = Term`VAR x`; val y = Term`VAR y`; val z = Term`VAR z`; 66val p = Term`VAR p`; val q = Term`VAR q`; val r = Term`VAR r`; 67val s = Term`VAR s`; 68 69fun imp x y = Term`(NOT ^x) OR ^y`; 70fun iff x y = Term`^(imp x y) AND ^(imp y x)`; 71 72val BOOL_CASES = Term `^x OR (NOT ^x)`; 73val NOT_BCASES = Term `^x OR (NOT ^y)`; 74val IMP_REFL = Term `(NOT ^x) OR ^x`; 75val DISTRIB = iff (Term`^x AND (^y OR ^z)`) 76 (Term`(^x AND ^y) OR (^x AND ^z)`); 77val PEIRCE = imp (imp (imp p q) p) p; 78val ANDREWS = imp (Term`^(imp p (Term`^q AND (^r OR ^s)`)) 79 AND ((NOT ^q) OR (NOT ^r))`) 80 (imp p s); 81val CLASSIC = imp (imp (Term`^p AND ^q`) r) 82 (Term `^(imp p r) OR ^(imp q r)`); 83 84(*--------------------------------------------------------------------------- 85 The following are adapted from jrh's tautology collection 86 in the examples directory. 87 ---------------------------------------------------------------------------*) 88 89val v0 = Term`VAR v0`; val v1 = Term`VAR v1`; val v2 = Term`VAR v2`; 90val v3 = Term`VAR v3`; val v4 = Term`VAR v4`; val v5 = Term`VAR v5`; 91val v6 = Term`VAR v6`; val v7 = Term`VAR v7`; val v8 = Term`VAR v8`; 92val v9 = Term`VAR v9`; 93 94val syn323_1 = Term 95 `NOT((^v0 OR ^v1) AND 96 (NOT ^v0 OR ^v1) AND 97 (NOT ^v1 OR ^v0) AND 98 (NOT ^v0 OR NOT ^v1))`; 99 100 101val syn029_1 = Term 102 `NOT((NOT ^v2 OR NOT ^v1) AND 103 ^v0 AND 104 (NOT ^v0 OR NOT ^v1 OR ^v2) AND 105 (NOT ^v2 OR ^v1) AND (^v1 OR ^v2))`; 106 107 108val syn052_1 = Term 109 `NOT((NOT ^v1 OR ^v0) AND 110 (NOT ^v0 OR ^v1) AND 111 (^v1 OR ^v0) AND 112 (NOT ^v1 OR ^v1) AND 113 (NOT ^v0 OR NOT ^v1))`; 114 115val syn051_1 = Term 116 `NOT(( ^v1 OR ^v0) AND 117 (^v1 OR ^v2) AND 118 (NOT ^v0 OR NOT ^v1) AND 119 (NOT ^v2 OR NOT ^v1) AND 120 (NOT ^v0 OR ^v1) AND 121 (NOT ^v1 OR ^v2))`; 122 123val syn044_1 = Term 124 `NOT((^v0 OR ^v1) AND 125 (NOT ^v0 OR NOT ^v1) AND 126 (NOT ^v0 OR ^v1 OR ^v2) AND 127 (NOT ^v2 OR ^v1) AND 128 (NOT ^v2 OR ^v0) AND 129 (NOT ^v1 OR ^v2))`; 130 131val syn011_1 = Term 132 `NOT(^v6 AND 133 (NOT ^v0 OR NOT ^v2) AND 134 (^v0 OR ^v1 OR ^v5) AND 135 (NOT ^v2 OR NOT ^v1) AND 136 (NOT ^v4 OR ^v2) AND 137 (NOT ^v3 OR ^v2) AND 138 (^v3 OR ^v4 OR ^v5) AND 139 (NOT ^v5 OR NOT ^v6))`; 140 141val syn032_1 = Term 142 `NOT((NOT ^v5 OR NOT ^v1) AND 143 (NOT ^v4 OR NOT ^v0) AND 144 (NOT ^v4 OR ^v0) AND 145 (NOT ^v5 OR ^v1) AND 146 (NOT ^v2 OR ^v4 OR ^v3) AND 147 (^v4 OR ^v2 OR ^v3) AND 148 (NOT ^v3 OR ^v4 OR ^v5))`; 149 150val syn030_1 = Term 151 `NOT((NOT ^v4 OR NOT ^v0 OR NOT ^v1) AND 152 (NOT ^v3 OR NOT ^v4 OR ^v0) AND 153 (NOT ^v1 OR ^v0) AND 154 (^v0 OR ^v1) AND 155 (NOT ^v0 OR ^v1) AND 156 (NOT ^v1 OR NOT ^v0 OR ^v2) AND 157 (NOT ^v2 OR ^v1) AND 158 (NOT ^v1 OR ^v3) AND 159 (NOT ^v2 OR NOT ^v3 OR ^v4))`; 160 161val syn054_1 = Term 162 `NOT((NOT ^v1 OR NOT ^v7) AND 163 (NOT ^v2 OR NOT ^v0) AND 164 (NOT ^v3 OR ^v7 OR ^v4) AND 165 (NOT ^v6 OR ^v0 OR ^v5) AND 166 (NOT ^v7 OR ^v1) AND 167 (NOT ^v0 OR ^v2) AND 168 (NOT ^v4 OR ^v1) AND 169 (NOT ^v5 OR ^v2) AND 170 (NOT ^v3 OR NOT ^v4) AND 171 (NOT ^v6 OR NOT ^v5) AND 172 (^v6 OR ^v7))`; 173 174val gra001_1 = Term 175 `NOT((NOT ^v1 OR ^v0) AND 176 (NOT ^v0 OR ^v1) AND 177 (NOT ^v4 OR NOT ^v2 OR NOT ^v0) AND 178 (NOT ^v4 OR ^v2 OR ^v0) AND 179 (NOT ^v2 OR ^v4 OR ^v0) AND 180 (NOT ^v0 OR ^v4 OR ^v2) AND 181 (NOT ^v3 OR NOT ^v2 OR NOT ^v1) AND 182 (NOT ^v3 OR ^v2 OR ^v1) AND 183 (NOT ^v2 OR ^v3 OR ^v1) AND 184 (NOT ^v1 OR ^v3 OR ^v2) AND 185 (NOT ^v3 OR NOT ^v4) AND 186 (^v3 OR ^v4))`; 187 188 189val syn321_1 = Term 190 `NOT((NOT ^v0 OR ^v9) AND 191 (NOT ^v0 OR ^v6) AND 192 (NOT ^v0 OR ^v7) AND 193 (NOT ^v8 OR ^v9) AND 194 (NOT ^v8 OR ^v6) AND 195 (NOT ^v8 OR ^v7) AND 196 (NOT ^v1 OR ^v9) AND 197 (NOT ^v1 OR ^v6) AND 198 (NOT ^v1 OR ^v7) AND 199 (NOT ^v2 OR ^v3) AND 200 (NOT ^v4 OR ^v5) AND 201 (NOT ^v7 OR ^v8) AND 202 (^v8 OR ^v9) AND 203 (^v8 OR ^v6) AND 204 (^v8 OR ^v7) AND 205 (NOT ^v8 OR NOT ^v9))`; 206 207 208val Eval = Count.apply (EVAL o Term); 209 210Eval `Wang ^BOOL_CASES`; 211Eval `Wang ^NOT_BCASES`; 212Eval `Wang ^IMP_REFL`; 213Eval `Wang ^DISTRIB`; 214Eval `Wang ^PEIRCE`; 215Eval `Wang ^ANDREWS`; 216Eval `Wang ^CLASSIC`; 217Eval `Wang ^syn323_1`; 218Eval `Wang ^syn029_1`; 219Eval `Wang ^syn052_1`; 220Eval `Wang ^syn051_1`; 221Eval `Wang ^syn044_1`; 222Eval `Wang ^syn011_1`; 223Eval `Wang ^syn032_1`; 224Eval `Wang ^syn030_1`; 225Eval `Wang ^syn054_1`; 226Eval `Wang ^gra001_1`; (* 45,395,214 inference steps (takes a long time) *) 227Eval `Wang ^syn321_1`; (* Takes longer, but not that much: 57,451,380 steps *) 228 229 230 231(*--------------------------------------------------------------------------- 232 Negation normal form (from Paulson's ML book). First a naive 233 version, which has a slightly complicated termination proof, 234 and then a faster mutually recursive version, which has an 235 easy termination proof. 236 ---------------------------------------------------------------------------*) 237 238val nnf_defn0 = 239 Hol_defn "nnf0" 240 `(nnf (VAR x) = VAR x) 241 /\ (nnf (NOT (VAR x)) = NOT(VAR x)) 242 /\ (nnf (NOT(NOT p)) = nnf p) 243 /\ (nnf (NOT(p AND q)) = nnf ((NOT p) OR (NOT q))) 244 /\ (nnf (NOT(p OR q)) = nnf ((NOT p) AND (NOT q))) 245 /\ (nnf (p AND q) = (nnf p) AND (nnf q)) 246 /\ (nnf (p OR q) = (nnf p) OR (nnf q))`; 247 248(*--------------------------------------------------------------------------- 249 The size of the largest NOT expression in a proposition. 250 ---------------------------------------------------------------------------*) 251 252val prop_size_def = fetch "-" "prop_size_def"; 253 254val MAX_def = Define `MAX x y = if x<y then y else x`; 255 256val NOT_SIZE_def = 257 Define 258 `(NOT_SIZE (VAR x) = 0) 259 /\ (NOT_SIZE (NOT p) = prop_size (\v.0) p) 260 /\ (NOT_SIZE ($AND p q) = MAX (NOT_SIZE p) (NOT_SIZE q)) 261 /\ (NOT_SIZE ($OR p q) = MAX (NOT_SIZE p) (NOT_SIZE q))`; 262 263 264val NOT_SIZE_LESS = Q.prove 265(`!p. NOT_SIZE p < prop_size (\v.0) p + 1`, 266 Induct 267 THEN RW_TAC arith_ss [NOT_SIZE_def, MAX_def, prop_size_def]); 268 269(*--------------------------------------------------------------------------- 270 Termination of nnf, using NOT_SIZE_LESS 271 ---------------------------------------------------------------------------*) 272 273val (nnf0_eqns, nnf0_ind) = 274Defn.tprove 275 (nnf_defn0, 276 WF_REL_TAC nnf_defn0 277 `inv_image ($< LEX $<) (\x. (NOT_SIZE x, prop_size (\v.0) x))` 278 THEN RW_TAC arith_ss [NOT_SIZE_def, MAX_def, 279 prop_size_def, NOT_SIZE_LESS]); 280 281 282(*--------------------------------------------------------------------------- 283 Mutually recursive algorithm. Termination is easy to prove, 284 and automatic. 285 ---------------------------------------------------------------------------*) 286 287val nnf_mutrec_eqns = 288 xDefine "nnf1" 289 `(nnfpos (VAR x) = VAR x) 290 /\ (nnfpos (NOT p) = nnfneg p) 291 /\ (nnfpos (p AND q) = (nnfpos p) AND (nnfpos q)) 292 /\ (nnfpos (p OR q) = (nnfpos p) OR (nnfpos q)) 293 294 /\ (nnfneg (VAR x) = NOT (VAR x)) 295 /\ (nnfneg (NOT p) = nnfpos p) 296 /\ (nnfneg (p AND q) = (nnfneg p) OR (nnfneg q)) 297 /\ (nnfneg (p OR q) = (nnfneg p) AND (nnfneg q))`; 298 299 300(*--------------------------------------------------------------------------- 301 Equivalence of nnf and nnfpos is straightforward. 302 ---------------------------------------------------------------------------*) 303 304val nnf_eq_nnfpos = Q.prove 305(`!p. nnf p = nnfpos p`, 306 recInduct nnf0_ind 307 THEN RW_TAC std_ss [nnf0_eqns,nnf_mutrec_eqns]); 308 309 310(*--------------------------------------------------------------------------- 311 Evaluation with nnfpos. First tell computeLib about nnf_mutrec_eqns. 312 ---------------------------------------------------------------------------*) 313 314val _ = computeLib.add_thms [nnf_mutrec_eqns] compset; 315 316Eval `nnfpos ^syn052_1`; 317Eval `nnfpos ^syn051_1`; 318Eval `nnfpos ^syn044_1`; 319Eval `nnfpos ^syn011_1`; 320Eval `nnfpos ^syn032_1`; 321Eval `nnfpos ^syn030_1`; 322Eval `nnfpos ^syn054_1`; 323Eval `nnfpos ^gra001_1`; 324Eval `nnfpos ^syn321_1`; 325 326 327 328(*--------------------------------------------------------------------------- 329 Conjunctive normal form (also from Paulson's ML book). 330 ---------------------------------------------------------------------------*) 331 332val distrib_def = 333 Define 334 `(distrib p (q AND r) = distrib p q AND distrib p r) 335 /\ (distrib (q AND r) p = distrib q p AND distrib r p) 336 /\ (distrib p q = p OR q)`; 337 338 339val cnf_def = 340 Define 341 `(cnf (p AND q) = cnf p AND cnf q) 342 /\ (cnf (p OR q) = distrib (cnf p) (cnf q)) 343 /\ (cnf p = p)`; 344 345 346val Value_def = 347 Define 348 `(Value P (VAR x) = P x) 349 /\ (Value P (NOT p) = ~Value P p) 350 /\ (Value P (p AND q) = Value P p /\ Value P q) 351 /\ (Value P (p OR q) = Value P p \/ Value P q)`; 352 353 354val Value_distrib_disj = Q.prove 355(`!p q P. Value P (distrib p q) = Value P p \/ Value P q`, 356 recInduct (fetch "-" "distrib_ind") 357 THEN RW_TAC std_ss [distrib_def, Value_def] 358 THEN PROVE_TAC []); 359 360 361val Value_cnf_stable = Q.prove 362(`!p Q. Value Q (cnf p) = Value Q p`, 363 Induct 364 THEN RW_TAC std_ss [cnf_def, Value_def, Value_distrib_disj]); 365 366 367val Value_nnf_stable = Q.prove 368(`!p Q. Value Q (nnf p) = Value Q p`, 369 recInduct nnf0_ind 370 THEN RW_TAC std_ss [nnf0_eqns,Value_def]); 371 372 373(*--------------------------------------------------------------------------- 374 An SML version of Wang's algorithm. 375 376fun mem x [] = false 377 | mem x (h::t) = (x=h) orelse mem x t; 378 379datatype 'a prop = VAR of 'a 380 | NOT of 'a prop 381 | AND of 'a prop * 'a prop 382 | OR of 'a prop * 'a prop; 383 384fun Prv vl [] (VAR v::r) vr = Prv vl [] r (v::vr) 385 | Prv vl [] (NOT x::r) vr = Prv vl [x] r vr 386 | Prv vl [] (OR(x,y)::r) vr = Prv vl [] (x::y::r) vr 387 | Prv vl [] (AND(x,y)::r) vr = Prv vl [] (x::r) vr 388 andalso 389 Prv vl [] (y::r) vr 390 | Prv vl (VAR v::l) r vr = Prv (v::vl) l r vr 391 | Prv vl (NOT x::l) r vr = Prv vl l (x::r) vr 392 | Prv vl (AND(x,y)::l) r vr = Prv vl (x::y::l) r vr 393 | Prv vl (OR(x,y)::l) r vr = Prv vl (x::l) r vr 394 andalso 395 Prv vl (y::l) r vr 396 397 | Prv vl [] [] vr = List.exists (fn y => mem y vl) vr; 398 399infixr 5 AND; 400infixr 4 OR; 401 402fun Wang M = Prv [] [] [M] []; 403 404 405 ************************* Examples ***************************** 406 407val x = VAR "x"; val y = VAR "y"; val z = VAR "z"; val p = VAR "p"; 408val q = VAR "q"; val r = VAR "r"; val s = VAR "s"; 409 410val v0 = VAR "v0"; val v1 = VAR "v1"; val v2 = VAR "v2"; val v3 = VAR "v3"; 411val v4 = VAR "v4"; val v5 = VAR "v5"; val v6 = VAR "v6"; val v7 = VAR "v7"; 412val v8 = VAR "v8"; val v9 = VAR "v9"; 413 414fun imp x y = NOT x OR y; 415fun iff x y = (imp x y) AND (imp y x); 416 417val BOOL_CASES = time Wang (x OR (NOT x)); 418val NOT_BCASES = time Wang (x OR (NOT y)); 419val IMP_REFL = time Wang (imp x x); 420val DISTRIB = time Wang (iff (x AND (y OR z)) 421 ((x AND y) OR (x AND z))); 422 423val PEIRCE = time Wang (imp (imp (imp p q) p) p); 424 425val ANDREWS = time Wang 426 (imp ((imp p (q AND (r OR s))) AND ((NOT q) OR (NOT r))) 427 (imp p s)); 428 429val syn323_1 = time Wang 430 (NOT((v0 OR v1) AND 431 (NOT v0 OR v1) AND 432 (NOT v1 OR v0) AND 433 (NOT v0 OR NOT v1))); 434 435val syn029_1 = 436time Wang 437 (NOT((NOT v2 OR NOT v1) AND 438 v0 AND 439 (NOT v0 OR NOT v1 OR v2) AND 440 (NOT v2 OR v1) AND (v1 OR v2))); 441 442 443val syn052_1 = 444time Wang 445 (NOT((NOT v1 OR v0) AND 446 (NOT v0 OR v1) AND 447 (v1 OR v0) AND (NOT v1 OR v1) AND (NOT v0 OR NOT v1))); 448 449val syn051_1 = 450time Wang 451 (NOT((v1 OR v0) AND 452 (v1 OR v2) AND 453 (NOT v0 OR NOT v1) AND 454 (NOT v2 OR NOT v1) AND 455 (NOT v0 OR v1) AND 456 (NOT v1 OR v2))); 457 458val syn044_1 = 459time Wang 460 (NOT((v0 OR v1) AND 461 (NOT v0 OR NOT v1) AND 462 (NOT v0 OR v1 OR v2) AND 463 (NOT v2 OR v1) AND 464 (NOT v2 OR v0) AND 465 (NOT v1 OR v2))); 466 467val syn011_1 = 468time Wang 469 (NOT(v6 AND 470 (NOT v0 OR NOT v2) AND 471 (v0 OR v1 OR v5) AND 472 (NOT v2 OR NOT v1) AND 473 (NOT v4 OR v2) AND 474 (NOT v3 OR v2) AND 475 (v3 OR v4 OR v5) AND 476 (NOT v5 OR NOT v6))); 477 478val syn032_1 = 479time Wang 480 (NOT((NOT v5 OR NOT v1) AND 481 (NOT v4 OR NOT v0) AND 482 (NOT v4 OR v0) AND 483 (NOT v5 OR v1) AND 484 (NOT v2 OR v4 OR v3) AND 485 (v4 OR v2 OR v3) AND 486 (NOT v3 OR v4 OR v5))); 487 488val syn030_1 = 489time Wang 490 (NOT((NOT v4 OR NOT v0 OR NOT v1) AND 491 (NOT v3 OR NOT v4 OR v0) AND 492 (NOT v1 OR v0) AND 493 (v0 OR v1) AND 494 (NOT v0 OR v1) AND 495 (NOT v1 OR NOT v0 OR v2) AND 496 (NOT v2 OR v1) AND 497 (NOT v1 OR v3) AND 498 (NOT v2 OR NOT v3 OR v4))); 499 500val syn054_1 = 501time Wang 502 (NOT((NOT v1 OR NOT v7) AND 503 (NOT v2 OR NOT v0) AND 504 (NOT v3 OR v7 OR v4) AND 505 (NOT v6 OR v0 OR v5) AND 506 (NOT v7 OR v1) AND 507 (NOT v0 OR v2) AND 508 (NOT v4 OR v1) AND 509 (NOT v5 OR v2) AND 510 (NOT v3 OR NOT v4) AND 511 (NOT v6 OR NOT v5) AND 512 (v6 OR v7))); 513 514 515val gra001_1 = 516time Wang 517 (NOT((NOT v1 OR v0) AND 518 (NOT v0 OR v1) AND 519 (NOT v4 OR NOT v2 OR NOT v0) AND 520 (NOT v4 OR v2 OR v0) AND 521 (NOT v2 OR v4 OR v0) AND 522 (NOT v0 OR v4 OR v2) AND 523 (NOT v3 OR NOT v2 OR NOT v1) AND 524 (NOT v3 OR v2 OR v1) AND 525 (NOT v2 OR v3 OR v1) AND 526 (NOT v1 OR v3 OR v2) AND 527 (NOT v3 OR NOT v4) AND 528 (v3 OR v4))); 529 530val syn321_1 = 531time Wang 532 (NOT((NOT v0 OR v9) AND 533 (NOT v0 OR v6) AND 534 (NOT v0 OR v7) AND 535 (NOT v8 OR v9) AND 536 (NOT v8 OR v6) AND 537 (NOT v8 OR v7) AND 538 (NOT v1 OR v9) AND 539 (NOT v1 OR v6) AND 540 (NOT v1 OR v7) AND 541 (NOT v2 OR v3) AND 542 (NOT v4 OR v5) AND 543 (NOT v7 OR v8) AND 544 (v8 OR v9) AND 545 (v8 OR v6) AND 546 (v8 OR v7) AND 547 (NOT v8 OR NOT v9))) ; 548 549 550 End of SML version. 551 ---------------------------------------------------------------------------*) 552