1(* ========================================================================= *) 2(* HOL NORMALIZATION FUNCTIONS. *) 3(* Created by Joe Hurd, October 2001 *) 4(* ========================================================================= *) 5 6structure normalForms :> normalForms = 7struct 8 9open HolKernel Parse boolLib simpLib; 10 11(* Fix the grammar used by this file *) 12structure Parse = 13struct 14 open Parse 15 val (Type,Term) = parse_from_grammars combinTheory.combin_grammars 16end 17open Parse 18 19 20(* ------------------------------------------------------------------------- *) 21(* Tracing. *) 22(* ------------------------------------------------------------------------- *) 23 24val trace_level = ref 0; 25val () = register_trace ("normalForms", trace_level, 10); 26fun chatting l = l <= !trace_level; 27fun chat s = (Lib.say s; true); 28 29(* ------------------------------------------------------------------------- *) 30(* Helper functions. *) 31(* ------------------------------------------------------------------------- *) 32 33val ERR = mk_HOL_ERR "normalForms"; 34 35fun op_distinct cmp [] = true 36 | op_distinct cmp (x :: rest) = 37 not (op_mem cmp x rest) andalso op_distinct cmp rest 38 39val beq = ``$= : bool->bool->bool``; 40 41fun dest_beq tm = 42 let val (a, b, ty) = dest_eq_ty tm 43 in if ty = bool then (a, b) else raise ERR "dest_beq" "not a bool" 44 end; 45 46val is_beq = can dest_beq; 47 48fun JUNCTS_CONV p c = 49 let fun f t = (if p t then LAND_CONV c THENC RAND_CONV f else c) t in f end; 50 51val CONJUNCTS_CONV = JUNCTS_CONV is_conj; 52val DISJUNCTS_CONV = JUNCTS_CONV is_disj; 53 54fun FORALL_CONV c tm = 55 if is_forall tm then QUANT_CONV c tm 56 else raise ERR "FORALL_CONV" "not a forall"; 57 58fun EXISTS_CONV c tm = 59 if is_exists tm then QUANT_CONV c tm 60 else raise ERR "EXISTS_CONV" "not an exists"; 61 62fun STRIP_EXISTS_CONV c tm = 63 if is_exists tm then STRIP_QUANT_CONV c tm else c tm; 64 65fun STRIP_FORALL_CONV c tm = 66 if is_forall tm then STRIP_QUANT_CONV c tm else c tm; 67 68fun ANTI_ETA_CONV v tm = SYM (ETA_CONV (mk_abs (v, mk_comb (tm, v)))); 69 70fun ETA_EXPAND_CONV tm = 71 let val (ty,_) = dom_rng (type_of tm) in ANTI_ETA_CONV (genvar ty) tm end; 72 73fun ANTI_BETA_CONV vars tm = 74 let 75 val tm' = list_mk_comb (list_mk_abs (vars, tm), vars) 76 val c = funpow (length vars) (fn c => RATOR_CONV c THENC BETA_CONV) ALL_CONV 77 in 78 SYM (c tm') 79 end; 80 81fun AVOID_SPEC_TAC (tm, v) = 82 W (fn (_, g) => SPEC_TAC (tm, variant (free_vars g) v)); 83 84local 85 open tautLib; 86 val th = prove (``(a <=> b) /\ (c <=> d) ==> (a /\ c <=> b /\ d)``, TAUT_TAC); 87 val (a, b, c, d) = (``a:bool``, ``b:bool``, ``c:bool``, ``d:bool``); 88in 89 fun MK_CONJ_EQ th1 th2 = 90 let 91 val (A, B) = dest_eq (concl th1) 92 val (C, D) = dest_eq (concl th2) 93 in 94 MP (INST [a |-> A, b |-> B, c |-> C, d |-> D] th) (CONJ th1 th2) 95 end; 96end; 97 98local 99 val th = prove (``(a /\ b) /\ c <=> b /\ (a /\ c)``, tautLib.TAUT_TAC); 100 val (a, b, c) = (``a:bool``, ``b:bool``, ``c:bool``); 101in 102 fun CONJ_RASSOC_CONV tm = 103 let 104 val (t, C) = dest_conj tm 105 val (A, B) = dest_conj t 106 in 107 INST [a |-> A, b |-> B, c |-> C] th 108 end; 109end; 110 111local 112 val th = prove (``(a \/ b) \/ c <=> b \/ (a \/ c)``, tautLib.TAUT_TAC); 113 val (a, b, c) = (``a:bool``, ``b:bool``, ``c:bool``); 114in 115 fun DISJ_RASSOC_CONV tm = 116 let 117 val (t, C) = dest_disj tm 118 val (A, B) = dest_disj t 119 in 120 INST [a |-> A, b |-> B, c |-> C] th 121 end; 122end; 123 124(* ------------------------------------------------------------------------- *) 125(* Replace genvars with variants on `v`. *) 126(* *) 127(* Example: *) 128(* ?%%genvar%%20744 %%genvar%%20745 %%genvar%%20746. *) 129(* (%%genvar%%20744 \/ %%genvar%%20745 \/ ~%%genvar%%20746) /\ *) 130(* (%%genvar%%20746 \/ ~%%genvar%%20744) /\ *) 131(* (%%genvar%%20746 \/ ~%%genvar%%20745) /\ (~q \/ ~%%genvar%%20745) /\ *) 132(* (r \/ ~%%genvar%%20745) /\ (%%genvar%%20745 \/ q \/ ~r) /\ *) 133(* (q \/ ~p \/ ~%%genvar%%20744) /\ (p \/ ~q \/ ~%%genvar%%20744) /\ *) 134(* (%%genvar%%20744 \/ ~p \/ ~q) /\ (%%genvar%%20744 \/ p \/ q) /\ *) 135(* %%genvar%%20746 *) 136(* = *) 137(* ?v v1 v2. *) 138(* (v \/ v1 \/ ~v2) /\ (v2 \/ ~v) /\ (v2 \/ ~v1) /\ (q \/ ~v1) /\ *) 139(* (r \/ ~v1) /\ (v1 \/ ~q \/ ~r) /\ (q \/ ~p \/ ~v) /\ *) 140(* (p \/ ~q \/ ~v) /\ (v \/ ~p \/ ~q) /\ (v \/ p \/ q) /\ v2 *) 141(* ------------------------------------------------------------------------- *) 142 143local 144 datatype ('a, 'b) sum = INL of 'a | INR of 'b; 145 146 fun ren _ [tm] [] = tm 147 | ren avoid (b :: a :: dealt) (INL NONE :: rest) = 148 ren avoid (mk_comb (a, b) :: dealt) rest 149 | ren avoid (b :: dealt) (INL (SOME v) :: rest) = 150 ren avoid (mk_abs (v, b) :: dealt) rest 151 | ren avoid dealt (INR (sub, tm) :: rest) = 152 (case dest_term tm of 153 CONST _ => ren avoid (tm :: dealt) rest 154 | VAR _ => ren avoid (subst sub tm :: dealt) rest 155 | COMB (a, b) => 156 ren avoid dealt (INR (sub, a) :: INR (sub, b) :: INL NONE :: rest) 157 | LAMB (v, b) => 158 let 159 val (v', sub') = 160 if not (is_genvar v) then (v, sub) else 161 let val v' = numvariant avoid (mk_var ("v", type_of v)) 162 in (v', (v |-> v') :: sub) 163 end 164 in 165 ren (op_insert aconv v' avoid) dealt 166 (INR (sub', b) :: INL (SOME v') :: rest) 167 end) 168 | ren _ _ _ = raise ERR "prettify_vars" "BUG"; 169in 170 fun prettify_vars tm = ren (all_vars tm) [] [INR ([], tm)]; 171end; 172 173fun PRETTIFY_VARS_CONV tm = ALPHA tm (prettify_vars tm); 174 175(* ------------------------------------------------------------------------- *) 176(* Conversion to combinators {S,K,I}. *) 177(* *) 178(* Example: *) 179(* (?f. !y. f y = y + 1) *) 180(* = *) 181(* $? (S (K $!) (S (S (K S) (S (K (S (K $=))) I)) (K (S $+ (K 1))))) *) 182(* ------------------------------------------------------------------------- *) 183 184fun COMBIN_CONV ths = 185 let 186 val mk_combin = FIRST_CONV (map HO_REWR_CONV ths) 187 fun conv tm = 188 (case dest_term tm of 189 CONST _ => ALL_CONV 190 | VAR _ => ALL_CONV 191 | COMB _ => RATOR_CONV conv THENC RAND_CONV conv 192 | LAMB _ => ABS_CONV conv THENC mk_combin THENC conv) tm 193 in 194 conv 195 end; 196 197val MK_S = prove 198 (``!x y. (\v. (x v) (y v)) = S (x:'a->'b->'c) y``, 199 REPEAT STRIP_TAC THEN 200 CONV_TAC (FUN_EQ_CONV) THEN 201 SIMP_TAC boolSimps.bool_ss [combinTheory.S_DEF, combinTheory.K_DEF]); 202 203val MK_K = prove 204 (``!x. (\v. x) = (K:'a->'b->'a) x``, 205 REPEAT STRIP_TAC THEN 206 CONV_TAC (FUN_EQ_CONV) THEN 207 SIMP_TAC boolSimps.bool_ss [combinTheory.S_DEF, combinTheory.K_DEF]); 208 209val MK_I = prove 210 (``(\v. v) = (I:'a->'a)``, 211 REPEAT STRIP_TAC THEN 212 CONV_TAC (FUN_EQ_CONV) THEN 213 SIMP_TAC boolSimps.bool_ss 214 [combinTheory.S_DEF, combinTheory.K_DEF, combinTheory.I_THM]); 215 216val SKI_SS = 217 simpLib.SSFRAG 218 {name=SOME"SKI", 219 convs = [], rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []}; 220 221val SKI_ss = simpLib.++ (pureSimps.pure_ss, SKI_SS); 222 223val SKI_CONV = 224 COMBIN_CONV [MK_K, MK_I, MK_S] THENC 225 SIMP_CONV SKI_ss []; 226 227(* ------------------------------------------------------------------------- *) 228(* Conversion to combinators {S,K,I,C,o}. *) 229(* *) 230(* Example: *) 231(* (?f. !y. f y = y + 1) *) 232(* = *) 233(* $? ($! o C (S o $o $= o I) (C $+ 1)) *) 234(* ------------------------------------------------------------------------- *) 235 236val MK_C = prove 237 (``!x y. (\v. (x v) y) = combin$C (x:'a->'b->'c) y``, 238 REPEAT STRIP_TAC THEN 239 CONV_TAC (FUN_EQ_CONV) THEN 240 SIMP_TAC boolSimps.bool_ss 241 [combinTheory.S_DEF, combinTheory.K_DEF, combinTheory.C_DEF]); 242 243val MK_o = prove 244 (``!x y. (\v:'a. x (y v)) = (x:'b->'c) o y``, 245 REPEAT STRIP_TAC THEN 246 CONV_TAC (FUN_EQ_CONV) THEN 247 SIMP_TAC boolSimps.bool_ss 248 [combinTheory.S_DEF, combinTheory.K_DEF, combinTheory.o_DEF]); 249 250val SKICo_SS = 251 simpLib.SSFRAG 252 {name=SOME"SKICo", 253 convs = [], 254 rewrs = [ 255 (SOME{Thy = "combin", Name = "I_o_ID"}, combinTheory.I_o_ID) 256 ], congs = [], 257 filter = NONE, ac = [], dprocs = []}; 258 259val SKICo_ss = simpLib.++ (SKI_ss, SKICo_SS); 260 261val SKICo_CONV = 262 COMBIN_CONV [MK_K, MK_I, MK_C, MK_o, MK_S] THENC 263 SIMP_CONV SKICo_ss []; 264 265(* ------------------------------------------------------------------------- *) 266(* Beta reduction and simplifying boolean rewrites. *) 267(* *) 268(* Example: *) 269(* (!x y. P x \/ (P y /\ F)) ==> ?z. P z *) 270(* = *) 271(* (!x. P x) ==> ?z. P z *) 272(* ------------------------------------------------------------------------- *) 273 274val FUN_EQ = prove 275 (``!(f : 'a -> 'b) g. (!x. f x = g x) = (f = g)``, 276 CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN 277 REWRITE_TAC []); 278 279val SIMPLIFY_SS = 280 simpLib.SSFRAG 281 {name=SOME"SIMPLIFY", 282 convs = [{name = "extensionality simplification", trace = 2, 283 key = SOME([], Term`!x. (f:'a -> 'b) x = g x`), 284 conv = K (K (REWR_CONV FUN_EQ))}], 285 rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []}; 286 287val simplify_ss = 288 simpLib.++ (simpLib.++ (pureSimps.pure_ss, boolSimps.BOOL_ss), SIMPLIFY_SS); 289 290val SIMPLIFY_CONV = SIMP_CONV simplify_ss []; 291 292(* ------------------------------------------------------------------------- *) 293(* Negation normal form. *) 294(* *) 295(* Example: *) 296(* (!x. P x) ==> ((?y. Q y) = ?z. P z /\ Q z) *) 297(* = *) 298(* ((?y. Q y) /\ (?z. P z /\ Q z) \/ (!y. ~Q y) /\ !z. ~P z \/ ~Q z) \/ *) 299(* ?x. ~P x *) 300(* ------------------------------------------------------------------------- *) 301 302val NOT_TRUE = prove (``~T = F``, tautLib.TAUT_TAC); 303 304val NOT_FALSE = prove (``~F = T``, tautLib.TAUT_TAC); 305 306val IMP_DISJ_THM' = prove 307 (``!x y. x ==> y <=> y \/ ~x``, 308 tautLib.TAUT_TAC); 309 310val NIMP_CONJ_THM = prove 311 (``!x y. ~(x ==> y) <=> x /\ ~y``, 312 tautLib.TAUT_TAC); 313 314val EQ_EXPAND' = prove 315 (``!x y. (x <=> y) <=> (x \/ ~y) /\ (~x \/ y)``, 316 tautLib.TAUT_TAC); 317 318val NEQ_EXPAND = prove 319 (``!x y. ~(x <=> y) <=> (x \/ y) /\ (~x \/ ~y)``, 320 tautLib.TAUT_TAC); 321 322val COND_EXPAND' = prove 323 (``!c a b. (if c then a else b) <=> ((~c \/ a) /\ (c \/ b))``, 324 tautLib.TAUT_TAC); 325 326val NCOND_EXPAND = prove 327 (``!c a b. ~(if c then a else b) <=> ((~c \/ ~a) /\ (c \/ ~b))``, 328 tautLib.TAUT_TAC); 329 330val DE_MORGAN_THM1 = prove 331 (``!x y. ~(x /\ y) <=> (~x \/ ~y)``, 332 tautLib.TAUT_TAC); 333 334val DE_MORGAN_THM2 = prove 335 (``!x y. ~(x \/ y) <=> (~x /\ ~y)``, 336 tautLib.TAUT_TAC); 337 338val NNF_EXISTS_UNIQUE = prove 339 (``!p. $?! p <=> ((?(x : 'a). p x) /\ !x y. p x /\ p y ==> (x = y))``, 340 GEN_TAC THEN 341 (KNOW_TAC ``$?! p = ?!(x : 'a). p x`` THEN1 342 (CONV_TAC (DEPTH_CONV (ETA_CONV)) THEN REWRITE_TAC [])) THEN 343 DISCH_THEN (fn th => REWRITE_TAC [th]) THEN 344 REWRITE_TAC [EXISTS_UNIQUE_THM]); 345 346val NOT_EXISTS_UNIQUE = prove 347 (``!p. ~($?! p) <=> ((!(x : 'a). ~p x) \/ ?x y. p x /\ p y /\ ~(x = y))``, 348 REWRITE_TAC [NNF_EXISTS_UNIQUE, DE_MORGAN_THM1] THEN 349 CONV_TAC (TOP_DEPTH_CONV (NOT_EXISTS_CONV ORELSEC NOT_FORALL_CONV)) THEN 350 REWRITE_TAC [NOT_IMP, CONJ_ASSOC]); 351 352val RES_FORALL_THM = prove 353 (``!p m. RES_FORALL p m = !(x : 'a). x IN p ==> m x``, 354 REWRITE_TAC [RES_FORALL_DEF] THEN BETA_TAC THEN REWRITE_TAC []); 355 356val RES_EXISTS_THM = prove 357 (``!p m. RES_EXISTS p m = ?(x : 'a). x IN p /\ m x``, 358 REWRITE_TAC [RES_EXISTS_DEF] THEN BETA_TAC THEN REWRITE_TAC []); 359 360val NOT_RES_FORALL = prove 361 (``!p m. ~RES_FORALL p m = ?(x : 'a). x IN p /\ ~m x``, 362 REWRITE_TAC [RES_FORALL_THM] THEN 363 CONV_TAC (DEPTH_CONV NOT_FORALL_CONV) THEN 364 REWRITE_TAC [IMP_DISJ_THM, DE_MORGAN_THM2]); 365 366val NOT_RES_EXISTS = prove 367 (``!p m. ~RES_EXISTS p m = !(x : 'a). x IN p ==> ~m x``, 368 REWRITE_TAC [RES_EXISTS_THM] THEN 369 CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) THEN 370 REWRITE_TAC [IMP_DISJ_THM, DE_MORGAN_THM2, DE_MORGAN_THM1]); 371 372fun NNF_SUB_CONV c tm = 373 (if is_forall tm then QUANT_CONV c 374 else if is_exists tm then QUANT_CONV c 375 else if is_conj tm then LAND_CONV c THENC RAND_CONV c 376 else if is_disj tm then LAND_CONV c THENC RAND_CONV c 377 else NO_CONV) tm; 378 379local 380 fun NEG_CONV c tm = (if is_neg tm then RAND_CONV c else NO_CONV) tm; 381 val beta_neg = 382 REWR_CONV (CONJUNCT1 NOT_CLAUSES) ORELSEC 383 BETA_CONV ORELSEC NEG_CONV BETA_CONV; 384 val push_neg = FIRST_CONV 385 (map REWR_CONV 386 [NOT_TRUE, NOT_FALSE, IMP_DISJ_THM', NIMP_CONJ_THM, EQ_EXPAND', 387 NEQ_EXPAND, COND_EXPAND', NCOND_EXPAND, DE_MORGAN_THM1, DE_MORGAN_THM2, 388 NNF_EXISTS_UNIQUE, NOT_EXISTS_UNIQUE, 389 RES_FORALL_THM, RES_EXISTS_THM, NOT_RES_FORALL, NOT_RES_EXISTS] @ 390 [NOT_FORALL_CONV, NOT_EXISTS_CONV]); 391 val q_neg = REPEATC beta_neg THENC TRY_CONV push_neg; 392in 393 fun PARTIAL_NNF_CONV c tm = 394 (q_neg THENC 395 (NNF_SUB_CONV (PARTIAL_NNF_CONV c) ORELSEC TRY_CONV c)) tm; 396end; 397 398fun PURE_NNF_CONV' c tm = 399 PARTIAL_NNF_CONV (c THENC PURE_NNF_CONV' c) tm; 400val PURE_NNF_CONV = PURE_NNF_CONV' NO_CONV; 401 402fun NNF_CONV' c = SIMPLIFY_CONV THENC PURE_NNF_CONV' c; 403val NNF_CONV = NNF_CONV' NO_CONV; 404 405(* ------------------------------------------------------------------------- *) 406(* Skolemization. *) 407(* *) 408(* Example: *) 409(* (!x. (?y. Q y \/ !z. ~P z \/ ~Q z) \/ ~P x) *) 410(* = *) 411(* ?y. !x. (Q (y x) \/ !z. ~P z \/ ~Q z) \/ ~P x *) 412(* ------------------------------------------------------------------------- *) 413 414fun PULL_EXISTS_CONV tm = 415 ((OR_EXISTS_CONV ORELSEC LEFT_AND_EXISTS_CONV ORELSEC RIGHT_AND_EXISTS_CONV 416 ORELSEC LEFT_OR_EXISTS_CONV ORELSEC RIGHT_OR_EXISTS_CONV ORELSEC 417 CHANGED_CONV SKOLEM_CONV) THENC 418 TRY_CONV (RAND_CONV (ABS_CONV PULL_EXISTS_CONV))) tm; 419 420val SKOLEMIZE_CONV = DEPTH_CONV PULL_EXISTS_CONV; 421 422(* ------------------------------------------------------------------------- *) 423(* Prenex Normal Form. *) 424(* ------------------------------------------------------------------------- *) 425 426local 427 val r1 = HO_REWR_CONV (GSYM FORALL_AND_THM); 428 val r2 = HO_REWR_CONV LEFT_AND_FORALL_THM; 429 val r3 = HO_REWR_CONV RIGHT_AND_FORALL_THM; 430 val r4 = HO_REWR_CONV (GSYM LEFT_FORALL_OR_THM); 431 val r5 = HO_REWR_CONV (GSYM RIGHT_FORALL_OR_THM); 432 433 fun p tm = 434 ((r1 ORELSEC r2 ORELSEC r3 ORELSEC r4 ORELSEC r5) THENC 435 TRY_CONV (QUANT_CONV p)) tm; 436in 437 val PRENEX_CONV = DEPTH_CONV p; 438end; 439 440local 441 val r1 = HO_REWR_CONV (GSYM LEFT_AND_FORALL_THM); 442 val r2 = HO_REWR_CONV (GSYM RIGHT_AND_FORALL_THM); 443 val r3 = HO_REWR_CONV FORALL_AND_THM; 444 445 fun p tm = 446 ((r1 THENC TRY_CONV (LAND_CONV p)) ORELSEC 447 (r2 THENC TRY_CONV (RAND_CONV p)) ORELSEC 448 r3 THENC BINOP_CONV (TRY_CONV p)) tm; 449in 450 val ANTI_PRENEX_CONV = DEPTH_CONV p; 451end; 452 453(* ------------------------------------------------------------------------- *) 454(* A basic tautology prover and simplifier for clauses *) 455(* *) 456(* Examples: *) 457(* TAUTOLOGY_CONV: p \/ r \/ ~p \/ ~q <=> T *) 458(* CONTRACT_CONV: (p \/ r) \/ p \/ ~q <=> p \/ r \/ ~q *) 459(* ------------------------------------------------------------------------- *) 460 461val BOOL_CASES = prove 462 (``!a b. (a ==> b) /\ (~a ==> b) ==> b``, 463 tautLib.TAUT_TAC); 464 465val T_OR = prove 466 (``!t. T \/ t <=> T``, 467 tautLib.TAUT_TAC); 468 469val OR_T = prove 470 (``!t. t \/ T <=> T``, 471 tautLib.TAUT_TAC); 472 473val T_AND = prove 474 (``!t. T /\ t <=> t``, 475 tautLib.TAUT_TAC); 476 477val AND_T = prove 478 (``!t. t /\ T <=> t``, 479 tautLib.TAUT_TAC); 480 481val OR_F = prove 482 (``!t. t \/ F <=> t``, 483 tautLib.TAUT_TAC); 484 485val CONTRACT_DISJ = prove 486 (``!a b b'. (~a ==> (b <=> b')) ==> (~a ==> (a \/ b <=> b'))``, 487 tautLib.TAUT_TAC); 488 489val DISJ_CONGRUENCE = prove 490 (``!a b b'. (~a ==> (b <=> b')) ==> (a \/ b <=> a \/ b')``, 491 tautLib.TAUT_TAC); 492 493local 494 fun harvest res [] = res 495 | harvest res (tm :: rest) = 496 if is_disj tm then 497 let val (a, b) = dest_disj tm 498 in harvest res (a :: b :: rest) 499 end 500 else harvest (tm :: res) rest 501in 502 fun disjuncts tm = harvest [] [tm] 503end; 504 505local 506 fun prove_case _ [] = raise ERR "TAUTOLOGY_CONV" "argh" 507 | prove_case d ((tm, path) :: rest) = 508 if is_disj tm then 509 let 510 val (a, b) = dest_disj tm 511 in 512 prove_case d ((a, (false, b) :: path) :: (b, (true, a) :: path) :: rest) 513 end 514 else if aconv tm d then 515 foldl (fn ((true, a), th) => DISJ2 a th | ((false, b), th) => DISJ1 th b) 516 (ASSUME d) 517 path 518 else 519 prove_case d rest 520 521 fun cases_on d tm = 522 let 523 val d' = mk_neg d 524 val pos_th = prove_case d [(tm, [])] 525 val neg_th = prove_case d' [(tm, [])] 526 in 527 MATCH_MP BOOL_CASES (CONJ (DISCH d pos_th) (DISCH d' neg_th)) 528 end 529in 530 fun TAUTOLOGY_CONV tm = 531 let 532 val (neg, pos) = partition is_neg (disjuncts tm) 533 in 534 case op_intersect aconv (map dest_neg neg) pos of 535 [] => NO_CONV tm 536 | d :: _ => EQT_INTRO (cases_on d tm) 537 end 538end; 539 540local 541 val simplify_or_f = REWR_CONV OR_F 542 val complicate_or_f = REWR_CONV (GSYM OR_F) 543 544 fun contract asms tm = 545 (if is_disj tm then contract' asms 546 else complicate_or_f THENC contract' asms) tm 547 and contract' asms tm = 548 let 549 val (a, b) = dest_disj tm 550 val a' = mk_neg a 551 val b_th = DISCH a' (if aconv b F then REFL F else contract (a :: asms) b) 552 in 553 if op_mem aconv a asms then UNDISCH (MATCH_MP CONTRACT_DISJ b_th) 554 else CONV_RULE (TRY_CONV (RAND_CONV simplify_or_f)) 555 (MATCH_MP DISJ_CONGRUENCE b_th) 556 end 557in 558 val CONTRACT_CONV = W 559 (fn tm => 560 if op_distinct aconv (disjuncts tm) then NO_CONV 561 else DEPTH_CONV DISJ_RASSOC_CONV THENC contract []); 562end; 563 564(* ------------------------------------------------------------------------- *) 565(* Conjunctive Normal Form. *) 566(* *) 567(* Example: *) 568(* (!x. P x ==> ?y z. Q y \/ ~?z. P z \/ Q z) *) 569(* = *) 570(* ?y. (!x x'. Q (y x) \/ ~P x' \/ ~P x) /\ !x x'. Q (y x) \/ ~Q x' \/ ~P x *) 571(* ------------------------------------------------------------------------- *) 572 573val tautology_checking = ref true; 574 575val TSIMP_CONV = 576 REWR_CONV OR_T ORELSEC REWR_CONV T_OR ORELSEC 577 REWR_CONV AND_T ORELSEC REWR_CONV T_AND; 578 579local 580 val r1 = REWR_CONV LEFT_OR_OVER_AND; 581 val r2 = REWR_CONV RIGHT_OR_OVER_AND; 582 val p1 = r1 ORELSEC r2; 583 val p2 = TAUTOLOGY_CONV ORELSEC CONTRACT_CONV; 584 val ps = TRY_CONV TSIMP_CONV; 585in 586 fun PUSH_ORS_CONV tm = 587 (TSIMP_CONV ORELSEC 588 (p1 THENC BINOP_CONV (TRY_CONV PUSH_ORS_CONV) THENC ps) ORELSEC 589 (if !tautology_checking then p2 else NO_CONV)) tm; 590end; 591 592val CLEAN_CNF_CONV = 593 DEPTH_CONV (DISJ_RASSOC_CONV ORELSEC CONJ_RASSOC_CONV ORELSEC 594 REWR_CONV FORALL_SIMP ORELSEC REWR_CONV EXISTS_SIMP); 595 596val PURE_CNF_CONV = 597 STRIP_EXISTS_CONV (STRIP_FORALL_CONV (DEPTH_CONV PUSH_ORS_CONV)) THENC 598 CLEAN_CNF_CONV; 599 600fun CNF_CONV' c = 601 NNF_CONV' c THENC 602 SKOLEMIZE_CONV THENC 603 PRENEX_CONV THENC 604 PURE_CNF_CONV; 605 606val CNF_CONV = CNF_CONV' NO_CONV; 607 608(* ------------------------------------------------------------------------- *) 609(* Disjunctive Normal Form. *) 610(* *) 611(* Example: *) 612(* (!x. P x ==> ?y z. Q y \/ ~?z. P z \/ Q z) *) 613(* = *) 614(* !x z. (?y. Q y) \/ (?y. ~P (z y) /\ ~Q (z y)) \/ ~P x *) 615(* ------------------------------------------------------------------------- *) 616 617val DOUBLE_NEG_CONV = REWR_CONV (GSYM (CONJUNCT1 NOT_CLAUSES)); 618 619fun NEG_CONV c tm = 620 ((if is_neg tm then ALL_CONV else DOUBLE_NEG_CONV) THENC RAND_CONV c) tm; 621 622fun DNF_CONV' c = 623 DOUBLE_NEG_CONV THENC RAND_CONV (CNF_CONV' (NEG_CONV c)) THENC PURE_NNF_CONV; 624 625val DNF_CONV = DNF_CONV' NO_CONV; 626 627(* ------------------------------------------------------------------------- *) 628(* Definitional Negation Normal Form *) 629(* *) 630(* Example: *) 631(* (~(p = ~(q = r)) = ~(~(p = q) = r)) *) 632(* = *) 633(* ((p = (q = r)) = ((p = ~q) = ~r)) *) 634(* ------------------------------------------------------------------------- *) 635 636val NEG_EQ = prove 637 (``!a b. ~(a <=> b) <=> (a <=> ~b)``, 638 tautLib.TAUT_TAC); 639 640fun DEF_NNF_SUB_CONV c tm = 641 (if is_forall tm then QUANT_CONV c 642 else if is_exists tm then QUANT_CONV c 643 else if is_conj tm then LAND_CONV c THENC RAND_CONV c 644 else if is_disj tm then LAND_CONV c THENC RAND_CONV c 645 else if is_beq tm then LAND_CONV c THENC RAND_CONV c 646 else NO_CONV) tm; 647 648local 649 fun NEG_CONV c tm = (if is_neg tm then RAND_CONV c else NO_CONV) tm; 650 val beta_neg = 651 REWR_CONV (CONJUNCT1 NOT_CLAUSES) ORELSEC 652 BETA_CONV ORELSEC NEG_CONV BETA_CONV; 653 val push_neg = FIRST_CONV 654 (map REWR_CONV 655 [NOT_TRUE, NOT_FALSE, IMP_DISJ_THM', NIMP_CONJ_THM, NEG_EQ, 656 COND_EXPAND', NCOND_EXPAND, DE_MORGAN_THM1, DE_MORGAN_THM2, 657 NNF_EXISTS_UNIQUE, NOT_EXISTS_UNIQUE, 658 RES_FORALL_THM, RES_EXISTS_THM, NOT_RES_FORALL, NOT_RES_EXISTS] @ 659 [NOT_FORALL_CONV, NOT_EXISTS_CONV]); 660 val q_neg = REPEATC beta_neg THENC TRY_CONV push_neg; 661in 662 fun PARTIAL_DEF_NNF_CONV c tm = 663 (q_neg THENC 664 (DEF_NNF_SUB_CONV (PARTIAL_DEF_NNF_CONV c) ORELSEC TRY_CONV c)) tm; 665end; 666 667fun PURE_DEF_NNF_CONV' c tm = 668 PARTIAL_DEF_NNF_CONV (c THENC PURE_DEF_NNF_CONV' c) tm; 669val PURE_DEF_NNF_CONV = PURE_DEF_NNF_CONV' NO_CONV; 670 671fun DEF_NNF_CONV' c = SIMPLIFY_CONV THENC PURE_DEF_NNF_CONV' c; 672val DEF_NNF_CONV = DEF_NNF_CONV' NO_CONV; 673 674datatype nnf_pos = Formula_pos | Atom_pos | Inside_pos; 675 676fun find_nnf find_f = 677 let 678 val fp = Formula_pos 679 fun f [] = raise ERR "find_nnf" "" 680 | f (p_vs_tm :: tms) = if find_f p_vs_tm then p_vs_tm else g p_vs_tm tms 681 and g (Formula_pos,vs,tm) tms = 682 if is_conj tm then 683 let val (a,b) = dest_conj tm in f ((fp,vs,a)::(fp,vs,b)::tms) end 684 else if is_disj tm then 685 let val (a,b) = dest_disj tm in f ((fp,vs,a)::(fp,vs,b)::tms) end 686 else if is_beq tm then 687 let val (a,b) = dest_beq tm in f ((fp,vs,a)::(fp,vs,b)::tms) end 688 else if is_forall tm then 689 let val (v,b) = dest_forall tm in f ((fp, v :: vs, b) :: tms) end 690 else if is_exists tm then 691 let val (v,b) = dest_exists tm in f ((fp, v :: vs, b) :: tms) end 692 else if is_neg tm then 693 let val a = dest_neg tm in f ((fp, vs, a) :: tms) end 694 else f ((Atom_pos, vs, tm) :: tms) 695 | g (_,vs,tm) tms = 696 if not (is_comb tm) then f tms 697 else f ((Inside_pos, vs, rator tm) :: (Inside_pos, vs, rand tm) :: tms) 698 in 699 fn tm => f [(fp,[],tm)] 700 end; 701 702fun ATOM_CONV c tm = (if is_neg tm then RAND_CONV c else c) tm; 703 704(* ------------------------------------------------------------------------- *) 705(* Definitional Conjunctive Normal Form *) 706(* *) 707(* Example: *) 708(* (~(p = ~(q = r)) = ~(~(p = q) = r)) *) 709(* = *) 710(* ?v v1 v2 v3 v4. *) 711(* (v4 \/ v1 \/ v3) /\ (v4 \/ ~v1 \/ ~v3) /\ (v1 \/ ~v3 \/ ~v4) /\ *) 712(* (v3 \/ ~v1 \/ ~v4) /\ (v3 \/ v2 \/ ~r) /\ (v3 \/ ~v2 \/ r) /\ *) 713(* (v2 \/ r \/ ~v3) /\ (~r \/ ~v2 \/ ~v3) /\ (v2 \/ p \/ ~q) /\ *) 714(* (v2 \/ ~p \/ q) /\ (p \/ q \/ ~v2) /\ (~q \/ ~p \/ ~v2) /\ *) 715(* (v1 \/ p \/ v) /\ (v1 \/ ~p \/ ~v) /\ (p \/ ~v \/ ~v1) /\ *) 716(* (v \/ ~p \/ ~v1) /\ (v \/ q \/ r) /\ (v \/ ~q \/ ~r) /\ *) 717(* (q \/ ~r \/ ~v) /\ (r \/ ~q \/ ~v) /\ v4 *) 718(* ------------------------------------------------------------------------- *) 719 720val EQ_DEFCNF = prove 721 (``!x y z. 722 (x <=> (y <=> z)) <=> 723 (z \/ ~y \/ ~x) /\ (y \/ ~z \/ ~x) /\ (x \/ ~y \/ ~z) /\ (x \/ y \/ z)``, 724 CONV_TAC CNF_CONV); 725 726val AND_DEFCNF = prove 727 (``!x y z. (x <=> (y /\ z)) <=> (y \/ ~x) /\ (z \/ ~x) /\ (x \/ ~y \/ ~z)``, 728 CONV_TAC CNF_CONV); 729 730val OR_DEFCNF = prove 731 (``!x y z. (x <=> (y \/ z)) <=> (y \/ z \/ ~x) /\ (x \/ ~y) /\ (x \/ ~z)``, 732 CONV_TAC CNF_CONV); 733 734fun sub_cnf f con defs (a, b) = 735 let 736 val (defs, a) = f defs a 737 val (defs, b) = f defs b 738 val tm = mk_comb (mk_comb (con, a), b) 739 in 740 (defs, tm) 741 end; 742 743fun def_step (defs, tm) = 744 case List.find (fn (_, b) => aconv b tm) defs of 745 NONE => let val g = genvar bool in ((g, tm) :: defs, g) end 746 | SOME (v, _) => (defs, v); 747 748fun gen_cnf defs tm = 749 if is_conj tm then 750 def_step (sub_cnf gen_cnf conjunction defs (dest_conj tm)) 751 else if is_disj tm then 752 def_step (sub_cnf gen_cnf disjunction defs (dest_disj tm)) 753 else if is_beq tm then 754 def_step (sub_cnf gen_cnf beq defs (dest_beq tm)) 755 else 756 (defs, tm); 757 758fun disj_cnf defs tm = 759 if is_disj tm then sub_cnf disj_cnf disjunction defs (dest_disj tm) 760 else gen_cnf defs tm; 761 762fun conj_cnf defs tm = 763 if is_conj tm then sub_cnf conj_cnf conjunction defs (dest_conj tm) 764 else disj_cnf defs tm; 765 766(* Natural rule 767val ONE_POINT_CONV = HO_REWR_CONV UNWIND_THM2; 768*) 769 770(* An attempt to soup it up 771*) 772fun ONE_POINT_CONV tm = 773 let 774 val (v, t) = dest_exists tm 775 val (q, b) = dest_conj t 776 val (_, d) = dest_eq q 777 val th = SPEC d (ISPEC (mk_abs (v, b)) UNWIND_THM2) 778 in 779 CONV_RULE 780 (LAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV)) THENC RAND_CONV BETA_CONV) th 781 end; 782 783fun gen_def_cnf tm = 784 let 785 val (defs, tm) = conj_cnf [] tm 786 val (vs, eqs) = unzip (map (fn (v, d) => (v, mk_eq (v, d))) (rev defs)) 787 val tm = list_mk_exists (vs, foldl mk_conj tm eqs) 788 in 789 (defs, tm) 790 end; 791 792fun PURE_DEF_CNF_CONV tm = 793 let 794 val (defs, tm) = gen_def_cnf tm 795 fun push c = QUANT_CONV c THENC ONE_POINT_CONV 796 val th = QCONV (funpow (length defs) push ALL_CONV) tm 797 in 798 SYM th 799 end; 800 801val def_cnf = snd o gen_def_cnf; 802 803val CLEAN_DEF_CNF_CONV = 804 (REWR_CONV EQ_DEFCNF ORELSEC 805 REWR_CONV AND_DEFCNF ORELSEC 806 REWR_CONV OR_DEFCNF) 807 THENC REWRITE_CONV [CONJUNCT1 NOT_CLAUSES]; 808 809local 810 datatype btree = LEAF of term | BRANCH of btree * btree; 811 812 fun btree_fold b f (LEAF tm) = b tm 813 | btree_fold b f (BRANCH (s, t)) = f (btree_fold b f s) (btree_fold b f t); 814 815 fun btree_strip_conj tm = 816 if is_conj tm then 817 (BRANCH o (btree_strip_conj ## btree_strip_conj) o dest_conj) tm 818 else LEAF tm; 819 820 val rewr = QCONV (CLEAN_DEF_CNF_CONV ORELSEC DEPTH_CONV DISJ_RASSOC_CONV); 821 822 fun cleanup tm = 823 let 824 val b = btree_strip_conj tm 825 val th = btree_fold rewr MK_CONJ_EQ b 826 in 827 CONV_RULE (RAND_CONV (DEPTH_CONV CONJ_RASSOC_CONV)) th 828 end; 829in 830 val CLEANUP_DEF_CNF_CONV = STRIP_EXISTS_CONV cleanup; 831end; 832 833local 834 val without_proof = curry (mk_oracle_thm "Definitional_CNF") []; 835in 836 fun ORACLE_PURE_DEF_CNF_CONV tm = without_proof (mk_eq (tm, def_cnf tm)); 837end; 838 839val DEF_CNF_CONV = 840 DEF_NNF_CONV THENC PURE_DEF_CNF_CONV THENC CLEANUP_DEF_CNF_CONV; 841 842val ORACLE_DEF_CNF_CONV = 843 DEF_NNF_CONV THENC ORACLE_PURE_DEF_CNF_CONV THENC CLEANUP_DEF_CNF_CONV; 844 845(* ------------------------------------------------------------------------- *) 846(* Removes leading existential quantifiers from a theorem, by introducing a *) 847(* new skolem constant with an appropriate assumption. *) 848(* *) 849(* Examples: *) 850(* SKOLEM_CONST_RULE ``a`` |- ?x. P x y z *) 851(* ----> [a = @x. P x y z] |- P a y *) 852(* *) 853(* SKOLEM_CONST_RULE ``a y z`` |- ?x. P x y *) 854(* ----> [a = \y z. @x. P x y z] |- P (a y z) y *) 855(* *) 856(* NEW_SKOLEM_CONST generates an argument for SKOLEM_CONST_RULE, and *) 857(* NEW_SKOLEM_CONST_RULE puts the two functions together. *) 858(* CLEANUP_SKOLEM_CONSTS_RULE tries to eliminate as many 'skolem *) 859(* assumptions' as possible. *) 860(* ------------------------------------------------------------------------- *) 861 862local 863 fun comb_beta (x, eq_th) = 864 CONV_RULE (RAND_CONV BETA_CONV) (MK_COMB (eq_th, REFL x)) 865in 866 fun SKOLEM_CONST_RULE c_vars th = 867 let 868 val (c, vars) = strip_comb c_vars 869 val sel_th = 870 CONV_RULE (RATOR_CONV (REWR_CONV EXISTS_DEF) THENC BETA_CONV) th 871 val pred = rator (concl sel_th) 872 val def_tm = list_mk_abs (vars, rand (concl sel_th)) 873 val def_th = ASSUME (mk_eq (c, def_tm)) 874 val eq_th = MK_COMB (REFL pred, foldl comb_beta def_th vars) 875 in 876 CONV_RULE BETA_CONV (EQ_MP (SYM eq_th) sel_th) 877 end 878end; 879 880fun NEW_SKOLEM_CONST th = 881 let 882 val tm = concl th 883 val fvs = op_set_diff aconv (free_vars tm) (free_varsl (hyp th)) 884 val (v, _) = dest_exists tm 885 val c_type = foldl (fn (h, t) => type_of h --> t) (type_of v) fvs 886 val c_vars = list_mk_comb (genvar c_type, rev fvs) 887 in 888 c_vars 889 end; 890 891val NEW_SKOLEM_CONST_RULE = W (SKOLEM_CONST_RULE o NEW_SKOLEM_CONST); 892 893local 894 fun zap _ _ [] = raise ERR "zap" "fresh out of asms" 895 | zap th checked (asm :: rest) = 896 if is_eq asm then 897 let 898 val (v,def) = dest_eq asm 899 in 900 if is_var v andalso all (not o free_in v) (def :: checked @ rest) then 901 MP (SPEC def (GEN v (DISCH asm th))) (REFL def) 902 else zap th (asm :: checked) rest 903 end 904 else zap th (asm :: checked) rest; 905in 906 val CLEANUP_SKOLEM_CONSTS_RULE = repeat (fn th => zap th [concl th] (hyp th)); 907end; 908 909(* ------------------------------------------------------------------------- *) 910(* Eliminating lambdas to make terms "as first-order as possible". *) 911(* *) 912(* Example: ((\x. f x z) = g z) = !x. f x z = g z x *) 913(* ------------------------------------------------------------------------- *) 914 915val LAMB_EQ_ELIM = prove 916 (``!(s : 'a -> 'b) t. ((\x. s x) = t) = (!x. s x = t x)``, 917 CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN 918 SIMP_TAC boolSimps.bool_ss []); 919 920val EQ_LAMB_ELIM = prove 921 (``!(s : 'a -> 'b) t. (s = (\x. t x)) = (!x. s x = t x)``, 922 CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN 923 SIMP_TAC boolSimps.bool_ss []); 924 925val DELAMB_CONV = SIMP_CONV simplify_ss [EQ_LAMB_ELIM, LAMB_EQ_ELIM]; 926 927(* ------------------------------------------------------------------------- *) 928(* Eliminating Hilbert's epsilon operator. *) 929(* *) 930(* Example: *) 931(* *) 932(* ((?n. f n = 0) ==> (f n = 0)) ==> 3 < n *) 933(* --------------------------------------- SELECT_TAC *) 934(* 3 < @n. f n = 0 *) 935(* ------------------------------------------------------------------------- *) 936 937local 938 fun norm vars tm = 939 let 940 val (a,b) = dest_comb tm 941 val _ = same_const select a orelse raise ERR "norm" "not a select" 942 val conv = ANTI_BETA_CONV (op_intersect aconv (free_vars b) vars) 943 val conv = 944 if is_abs b then conv else 945 let 946 val (ty,_) = dom_rng (type_of b) 947 val v = variant (all_vars b) (mk_var ("v", ty)) 948 in 949 RAND_CONV (ANTI_ETA_CONV v) THENC conv 950 end 951 in 952 conv tm 953 end; 954 955 fun select_norm vars tm = 956 let val svars = (case dest_term tm of LAMB (v,_) => v :: vars | _ => vars) 957 in SUB_CONV (select_norm svars) THENC TRY_CONV (norm vars) 958 end tm; 959in 960 val SELECT_NORM_CONV = select_norm []; 961end; 962 963local 964 val rewr = RATOR_CONV (REWR_CONV boolTheory.EXISTS_DEF) 965 fun conv vars = 966 rewr THENC BETA_CONV THENC RAND_CONV (ANTI_BETA_CONV vars) THENC BETA_CONV 967in 968 fun MK_VSELECT_THM vsel = 969 let 970 val (vars, sel) = strip_abs vsel 971 val (v, body) = dest_select sel 972 val ex = mk_exists (v, body) 973 in 974 foldr (uncurry GEN) (DISCH ex (EQ_MP (conv vars ex) (ASSUME ex))) vars 975 end; 976end; 977 978fun SPEC_VSELECT_TAC vsel = 979 let 980 val (v, _) = dest_var (fst (dest_select (snd (strip_abs vsel)))) 981 in 982 MP_TAC (MK_VSELECT_THM vsel) THEN 983 AVOID_SPEC_TAC (vsel, mk_var (v, type_of vsel)) THEN 984 GEN_TAC 985 end; 986 987local 988 fun get vs tm = 989 case 990 (case dest_term tm of COMB (x, y) => 991 (case get vs x of s as SOME _ => s | NONE => get vs y) 992 | LAMB (v, b) => get (v :: vs) b 993 | _ => NONE) of s as SOME _ => s 994 | NONE => 995 if is_select (snd (strip_abs tm)) andalso 996 null (op_intersect aconv (free_vars tm) vs) 997 then SOME tm 998 else NONE; 999in 1000 val get_vselect = partial (ERR "get_vselect" "not found") (get []); 1001end; 1002 1003val SPEC_ONE_SELECT_TAC = W (fn (_, tm) => SPEC_VSELECT_TAC (get_vselect tm)); 1004 1005val SELECT_TAC = CONV_TAC SELECT_NORM_CONV THEN REPEAT SPEC_ONE_SELECT_TAC; 1006 1007(* ------------------------------------------------------------------------- *) 1008(* Remove all Abbrev terms from a goal by rewriting them away (Abbrev = I) *) 1009(* ------------------------------------------------------------------------- *) 1010 1011val REMOVE_ABBR_TAC = 1012 PURE_REWRITE_TAC [markerTheory.Abbrev_def] THEN 1013 RULE_ASSUM_TAC (PURE_REWRITE_RULE [markerTheory.Abbrev_def]); 1014 1015(* ------------------------------------------------------------------------- *) 1016(* Lifting conditionals through function applications. *) 1017(* *) 1018(* Example: f (if x then y else z) = (if x then f y else f z) *) 1019(* ------------------------------------------------------------------------- *) 1020 1021fun cond_lift_rand_CONV tm = 1022 let 1023 val (Rator,Rand) = Term.dest_comb tm 1024 val (f,_) = strip_comb Rator 1025 val proceed = 1026 let val {Name,Thy,...} = Term.dest_thy_const f 1027 in not (Name="COND" andalso Thy="bool") 1028 end handle HOL_ERR _ => true 1029 in 1030 (if proceed then REWR_CONV boolTheory.COND_RAND else NO_CONV) tm 1031 end; 1032 1033val cond_lift_SS = 1034 simpLib.SSFRAG 1035 {name=SOME"cond_lift", 1036 convs = 1037 [{name = "conditional lifting at rand", trace = 2, 1038 key = SOME([], Term`(f:'a -> 'b) (COND P Q R)`), 1039 conv = K (K cond_lift_rand_CONV)}], 1040 rewrs = [(SOME {Thy = "bool", Name = "COND_RATOR"}, boolTheory.COND_RATOR)], 1041 congs = [], 1042 filter = NONE, 1043 ac = [], 1044 dprocs = []}; 1045 1046val cond_lift_ss = simpLib.++ (pureSimps.pure_ss, cond_lift_SS); 1047 1048(* ------------------------------------------------------------------------- *) 1049(* Converting boolean connectives to conditionals. *) 1050(* *) 1051(* Example: x /\ ~(y ==> ~z) <=> (if x then (if y then z else F) else F) *) 1052(* ------------------------------------------------------------------------- *) 1053 1054val COND_SIMP = prove 1055 (``!a f g. (if a then f a else g a):'a = (if a then f T else g F)``, 1056 SIMP_TAC boolSimps.bool_ss []); 1057 1058val COND_NOT = prove 1059 (``!a. ~a <=> if a then F else T``, 1060 SIMP_TAC boolSimps.bool_ss []); 1061 1062val COND_AND = prove 1063 (``!a b. a /\ b <=> (if a then b else F)``, 1064 SIMP_TAC boolSimps.bool_ss []); 1065 1066val COND_OR = prove 1067 (``!a b. a \/ b <=> if a then T else b``, 1068 SIMP_TAC boolSimps.bool_ss []); 1069 1070val COND_IMP = prove 1071 (``!a b. a ==> b <=> if a then b else T``, 1072 SIMP_TAC boolSimps.bool_ss []); 1073 1074val COND_EQ = prove 1075 (``!a b. (a <=> b) <=> if a then b else ~b``, 1076 SIMP_TAC boolSimps.bool_ss [EQ_IMP_THM, COND_EXPAND] 1077 THEN tautLib.TAUT_TAC); 1078 1079val COND_COND = prove 1080 (``!a b c x y. 1081 (if (if a then b else c) then (x:'a) else y) = 1082 (if a then (if b then x else y) else (if c then x else y))``, 1083 STRIP_TAC 1084 THEN MP_TAC (SPEC ``a:bool`` EXCLUDED_MIDDLE) 1085 THEN STRIP_TAC 1086 THEN ASM_SIMP_TAC boolSimps.bool_ss []); 1087 1088val COND_ETA = prove 1089 (``!a. (if a then T else F) = a``, 1090 SIMP_TAC boolSimps.bool_ss []); 1091 1092val COND_SIMP_CONV = CHANGED_CONV (HO_REWR_CONV COND_SIMP); 1093 1094val condify_SS = 1095 SSFRAG 1096 {name=SOME"condify", 1097 convs = 1098 [{name = "COND_SIMP_CONV", trace = 2, 1099 key = SOME ([], (``if a then (b:'a) else c``)), 1100 conv = K (K COND_SIMP_CONV)}], 1101 rewrs = map (fn th => (NONE, th)) 1102 [COND_CLAUSES, COND_NOT, COND_AND, COND_OR, COND_IMP, COND_EQ, COND_COND, 1103 COND_ID, COND_ETA, FORALL_SIMP, EXISTS_SIMP], 1104 congs = [], 1105 filter = NONE, 1106 ac = [], 1107 dprocs = []}; 1108 1109val condify_ss = simpLib.++ (pureSimps.pure_ss, condify_SS); 1110 1111(* ------------------------------------------------------------------------- *) 1112(* Definitional CNF minimizing number of clauses. *) 1113(* *) 1114(* Example: *) 1115(* |- (p /\ q /\ r) \/ (s /\ t /\ u) *) 1116(* --> *) 1117(* ([``d``], *) 1118(* [[.] |- (d \/ s) /\ (d \/ t) /\ (d \/ u), *) 1119(* [.] |- (d \/ ~p \/ ~q \/ ~r) /\ (~d \/ p) /\ (~d \/ q) /\ (~d \/ r)]) *) 1120(* *) 1121(* where the assumption [.] in both theorems is d = (p /\ q /\ r). *) 1122(* ------------------------------------------------------------------------- *) 1123 1124val COND_BOOL = prove 1125 (``!c. (if c then T else F) = c``, 1126 tautLib.TAUT_TAC); 1127 1128local 1129 fun comb_beta (x,eq_th) = 1130 CONV_RULE (RAND_CONV BETA_CONV) (MK_COMB (eq_th, REFL x)); 1131 1132 fun mk_def defs vs tm = 1133 let 1134 val def_tm = list_mk_abs (vs,tm) 1135 in 1136 case List.find (aconv def_tm o fst) defs of 1137 SOME (_,(vs,tm,def)) => 1138 let 1139 val _ = chatting 2 andalso chat "min_cnf: reusing definition.\n" 1140 in 1141 (defs, vs, tm, def, NONE) 1142 end 1143 | NONE => 1144 let 1145 val c = genvar (type_of def_tm) 1146 val def0 = foldl comb_beta (ASSUME (mk_eq (c,def_tm))) vs 1147 val def = SYM def0 1148 val def_th = GENL vs def0 1149 val defs = (def_tm,(vs,tm,def)) :: defs 1150 in 1151 (defs, vs, tm, def, SOME def_th) 1152 end 1153 end; 1154 1155 fun check_sub vs {redex,residue} = 1156 op_mem aconv redex vs andalso (type_of redex <> bool orelse is_var residue); 1157 1158 fun match_convish vs tm def tm' = 1159 let 1160 val (tmS,tyS) = match_term tm tm' 1161 val _ = null tyS orelse raise ERR "rename" "type match" 1162 val _ = all (check_sub vs) tmS orelse raise ERR "rename" "term match" 1163 in 1164 INST tmS def 1165 end; 1166in 1167 fun rename defs vs tm = 1168 let 1169 val vs = filter (fn v => op_mem aconv v vs) (free_vars tm) 1170 val (defs,vs,tm,def,def_th) = mk_def defs vs tm 1171 val convish = match_convish vs tm def 1172 in 1173 (defs, CONV_RULE (TOP_DEPTH_CONV convish), def_th) 1174 end 1175 handle e as HOL_ERR _ 1176 => (chat "normalForms.rename should never fail"; Raise e); 1177end; 1178 1179(* 1180local 1181 fun is_a_bool (p,vs,tm) = 1182 p = Inside_pos andalso 1183 type_of tm = bool andalso 1184 tm <> T andalso tm <> F andalso 1185 not let val (t,ws) = strip_comb tm in is_var t andalso subset ws vs end; 1186in 1187 fun extract_bools (defs,th,acc) = 1188 let 1189 val (_,vs,tm) = find_nnf is_a_bool (concl th) 1190 val (defs,rule,vth) = rename defs vs tm 1191 val acc = case vth of SOME vt => vt :: acc | NONE => acc 1192 in 1193 (defs, rule th, acc) 1194 end; 1195end; 1196 1197fun extract_lambdas (defs,th,acc) = 1198 let 1199 val (_,vs,tm) = find_nnf (is_abs o #3) (concl th) 1200 val (defs,rule,vth) = rename defs vs tm 1201 val acc = case vth of SOME vt => vt :: acc | NONE => acc 1202 in 1203 (defs, rule th, acc) 1204 end; 1205*) 1206 1207local 1208 val condify_bool = REWR_CONV (GSYM COND_BOOL); 1209 1210 val let_conv = REWR_CONV LET_THM; 1211 1212 fun is_a_bool tm = 1213 type_of tm = bool andalso not (aconv tm T) andalso not (aconv tm F); 1214 1215 fun lift_cond tm = 1216 TRY_CONV 1217 (REPEATC let_conv 1218 THENC COMB_CONV lift_bool 1219 THENC (REWR_CONV COND_RATOR 1220 ORELSEC REWR_CONV COND_RAND 1221 ORELSEC ALL_CONV)) tm 1222 and lift_bool tm = 1223 (chatting 3 andalso chat ("lift_bool: tm = " ^ term_to_string tm ^ "\n"); 1224 (if is_cond tm then ALL_CONV 1225(* Can't do this without more proof support for booleans 1226 else if is_a_bool tm then condify_bool 1227*) 1228 else lift_cond) tm); 1229in 1230 val boolify_conv = ATOM_CONV (CHANGED_CONV lift_cond); 1231end; 1232 1233fun min_cnf_prep defs acc [] = (defs, rev acc) 1234 | min_cnf_prep defs acc (th :: ths) = 1235 let 1236 val th = CONV_RULE DELAMB_CONV th 1237 val th = CONV_RULE (DEF_NNF_CONV' boolify_conv) th 1238(* 1239 val (defs,th,bs) = repeat extract_bools (defs,th,[]) 1240 val (defs,th,ls) = repeat extract_lambdas (defs,th,[]) 1241*) 1242 in 1243 min_cnf_prep defs (th :: acc) ths 1244 end; 1245 1246local 1247 open Arbint (* hope that on Poly/ML we can eventually just make 1248 Arbint a reference to its built-in infinite int type *) 1249 1250in 1251 1252datatype formula = Formula of (int * int) * term list * term * skeleton 1253and skeleton = 1254 Conj of formula * formula 1255 | Disj of formula * formula 1256 | Beq of formula * formula 1257 | Lit; 1258 1259fun conj_count (ap,an) (bp,bn) = (ap + bp, an * bn); 1260fun disj_count (ap,an) (bp,bn) = (ap * bp, an + bn); 1261fun beq_count (ap,an) (bp,bn) = (ap * bn + an * bp, ap * bp + an * bn); 1262 1263fun count_cnf vs tm = 1264 if is_exists tm then 1265 let 1266 val (v,b) = dest_exists tm 1267 in 1268 count_cnf (v :: vs) b 1269 end 1270 else if is_forall tm then 1271 let 1272 val (v,b) = dest_forall tm 1273 in 1274 count_cnf (v :: vs) b 1275 end 1276 else if is_conj tm then 1277 let 1278 val (a,b) = dest_conj tm 1279 val af as Formula (ac,_,_,_) = count_cnf vs a 1280 val bf as Formula (bc,_,_,_) = count_cnf vs b 1281 in 1282 Formula (conj_count ac bc, vs, tm, Conj (af,bf)) 1283 end 1284 else if is_disj tm then 1285 let 1286 val (a,b) = dest_disj tm 1287 val af as Formula (ac,_,_,_) = count_cnf vs a 1288 val bf as Formula (bc,_,_,_) = count_cnf vs b 1289 in 1290 Formula (disj_count ac bc, vs, tm, Disj (af,bf)) 1291 end 1292 else if is_beq tm then 1293 let 1294 val (a,b) = dest_beq tm 1295 val af as Formula (ac,_,_,_) = count_cnf vs a 1296 val bf as Formula (bc,_,_,_) = count_cnf vs b 1297 in 1298 Formula (beq_count ac bc, vs, tm, Beq (af,bf)) 1299 end 1300 else Formula ((Arbint.one,Arbint.one),vs,tm,Lit); 1301 1302 1303local 1304 fun check best [] = best 1305 | check best ((f, form) :: rest) = 1306 let 1307 val (n,_,_) = best 1308 val Formula ((pos,neg), vs, tm, skel) = form 1309 val m = f (Arbint.one,Arbint.one) + pos + neg 1310 val best = if m < n then (m,vs,tm) else best 1311 in 1312 break best f skel rest 1313 end 1314 and break best f (Conj (a,b)) rest = 1315 let 1316 val Formula (ac,_,_,_) = a 1317 val Formula (bc,_,_,_) = b 1318 fun fa ac = f (conj_count ac bc) 1319 fun fb bc = f (conj_count ac bc) 1320 val rest = (fa,a) :: (fb,b) :: rest 1321 in 1322 check best rest 1323 end 1324 | break best f (Disj (a,b)) rest = 1325 let 1326 val Formula (ac,_,_,_) = a 1327 val Formula (bc,_,_,_) = b 1328 fun fa ac = f (disj_count ac bc) 1329 fun fb bc = f (disj_count ac bc) 1330 val rest = (fa,a) :: (fb,b) :: rest 1331 in 1332 check best rest 1333 end 1334 | break best f (Beq (a,b)) rest = 1335 let 1336 val Formula (ac,_,_,_) = a 1337 val Formula (bc,_,_,_) = b 1338 fun fa ac = f (beq_count ac bc) 1339 fun fb bc = f (beq_count ac bc) 1340 val rest = (fa,a) :: (fb,b) :: rest 1341 in 1342 check best rest 1343 end 1344 | break best _ Lit rest = check best rest; 1345in 1346 val min_cnf_search = check; 1347end; 1348 1349val simple_cnf_rule = CONV_RULE (CNF_CONV' (CHANGED_CONV SKICo_CONV)); 1350 1351fun min_cnf_norm defs acc [] = (defs, rev acc) 1352 | min_cnf_norm defs acc (th :: ths) = 1353 let 1354 val concl_th = concl th 1355 val form as Formula ((m,_),_,_,_) = count_cnf [] concl_th 1356 val (n,vs,tm) = min_cnf_search (m,[],concl_th) [(fst,form)] 1357 in 1358 if n < m then 1359 let 1360 val _ = 1361 chatting 1 andalso 1362 chat ("min_cnf: "^Arbint.toString m^" -> "^ 1363 Arbint.toString n^" clauses\n") 1364 val _ = 1365 chatting 2 andalso 1366 chat ("min_cnf: renaming\n" ^ term_to_string tm ^ "\n") 1367 val (defs,rule,dth) = rename defs vs tm 1368 val ths = case dth of SOME dt => dt :: ths | NONE => ths 1369 in 1370 min_cnf_norm defs acc (rule th :: ths) 1371 end 1372 else 1373 min_cnf_norm defs (simple_cnf_rule th :: acc) ths 1374 end; 1375end (* of local enclosing open Arbint *) 1376 1377fun MIN_CNF ths = 1378 let 1379 val ths = map GEN_ALL ths 1380 val defs = [] 1381 val (defs,ths) = min_cnf_prep defs [] ths 1382 val (defs,ths) = min_cnf_norm defs [] ths 1383 val cs = map (lhs o hd o hyp o #3 o snd) defs 1384 in 1385 (cs,ths) 1386 end; 1387 1388(* Quick testing 1389val Term = Parse.Term; 1390val Type = Parse.Type; 1391Globals.guessing_tyvars := true; (* OK *) 1392app load ["numLib", "arithmeticTheory", "pred_setTheory", "bossLib"]; 1393open numLib arithmeticTheory pred_setTheory bossLib; 1394 1395val tm = ``~(0 <= m ==> 1396 0 <= n ==> 1397 0 < m /\ 0 < n ==> 1398 ((~(n <= 1) \/ (m = 1)) /\ 1399 (n <= 1 \/ (m + 1 = 1 + n) \/ m <= 0 /\ 1 + n <= 1) \/ 1400 m <= 1 /\ n <= 1 + 0 <=> 1401 (m = n)))``; 1402PARTIAL_NNF_CONV (REWR_CONV NOT_NUM_EQ) tm; 1403PURE_NNF_CONV' (REWR_CONV NOT_NUM_EQ) tm; 1404 1405CNF_CONV ``(p /\ (q \/ r /\ s)) /\ (~p \/ ~q \/ ~s)``; 1406CNF_CONV ``(p /\ (q \/ r /\ s)) /\ (~p \/ ~q \/ ~s) /\ (p \/ ~p)``; 1407CNF_CONV ``~(~(x = y) = z) = ~(x = ~(y = z))``; 1408CNF_CONV ``((p = q) = r) = (p = (q = r))``; 1409CNF_CONV ``~(((p = q) = r) = (p = (q = r)))``; 1410CNF_CONV ``?y. x < y ==> (!u. ?v. x * u < y * v)``; 1411CNF_CONV ``!x. P(x) ==> (?y z. Q(y) \/ ~(?z. P(z) /\ Q(z)))``; 1412 1413val th = DNF_CONV' (REWR_CONV NOT_NUM_EQ) 1414 ``~(0 <= m ==> 1415 0 <= n ==> 1416 0 < m /\ 0 < n ==> 1417 ((~(n <= 1) \/ (m = 1)) /\ 1418 (n <= 1 \/ (m + 1 = 1 + n) \/ m <= 0 /\ 1 + n <= 1) \/ 1419 m <= 1 /\ n <= 1 + 0 = 1420 (m = n)))``; 1421val ds = length (strip_disj (rhs (concl th))); 1422 1423try DEF_NNF_CONV ``~(p = ~(q = r)) = ~(~(p = q) = r)``; 1424try (DEF_CNF_CONV THENC PRETTIFY_VARS_CONV) 1425``~(p = ~(q = r)) = ~(~(p = q) = r)``; 1426CLEANUP_DEF_CNF_CONV ``?v. (v 0 = (x /\ y) /\ (v 1 = (v 0 = x))) /\ v 0``; 1427try PURE_DEF_CNF_CONV ``(p /\ (q \/ r /\ s)) /\ (~p \/ ~q \/ ~s)``; 1428 1429SKOLEM_CONST_RULE ``a:'a`` (ASSUME ``?x. (P:'a->'b->'c->bool) x y z``); 1430SKOLEM_CONST_RULE ``(a:'b->'c->'a) y z`` 1431 (ASSUME ``?x. (P:'a->'b->'c->bool) x y z``); 1432NEW_SKOLEM_CONST_RULE (ASSUME ``?x. (P:'a->'b->'c->bool) x y z``); 1433CLEANUP_SKOLEM_CONSTS_RULE it; 1434 1435DELAMB_CONV ``(\x. f x z) = g z``; 1436 1437g `3 < @n. f n = 0`; 1438e SELECT_TAC; 1439drop (); 1440 1441g `!p. 0 = @x. (?y w. (@z. z + w = p + q + y + x) = 2) = (?a b. (@c. c + a = p + q + b + x) < 3)`; 1442e SELECT_TAC; 1443drop (); 1444 1445g `!p. 0 = @x. (?y v. (@(z,r). z + v + r = p + q + y + x) = (2,3)) = (?a b. (@c. c + a = p + q + b + x) < 3)`; 1446e SELECT_TAC; 1447drop (); 1448 1449g `(!x. x IN p ==> (f x = f' x)) ==> ((@x. x IN p /\ f x) = @x. x IN p /\ f' x)`; 1450e STRIP_TAC; 1451e SELECT_TAC; 1452drop (); 1453 1454g `($@ p) = 3`; 1455e SELECT_TAC; 1456drop (); 1457 1458try (SIMP_CONV cond_lift_ss []) ``f (if x then 7 else 1)``; 1459 1460try (SIMP_CONV condify_ss []) ``x /\ ~(y ==> ~z)``; 1461 1462(MIN_CNF o map ASSUME) 1463[``!b. ~(p (c:bool) (b:bool))``]; 1464 1465(MIN_CNF o map ASSUME) 1466[``!t. ~(p = f (if x then y else z) (if a then b else c) 1467 (\q. r (if s then t else u)))``]; 1468 1469(MIN_CNF o map ASSUME) 1470[``!x. p (\y. y + x)``, ``!z. q (\y. y + z)``]; 1471 1472(MIN_CNF o map ASSUME) [``!q. ~(p /\ f (q /\ r))``]; 1473 1474MIN_CNF [GSPECIFICATION, 1475 ASSUME ``!x. x IN {y + 1 | y < n \/ y < m} ==> x <= m + n``]; 1476 1477val p34 = mk_neg 1478 ``((?x. !y. (p : 'a -> bool) x = p y) = ((?x. q x) = !y. q y)) = 1479 ((?x. !y. q x = q y) = ((?x. p x) = !y. p y))``; 1480 1481CNF_CONV p34; 1482MIN_CNF [ASSUME p34]; 1483*) 1484 1485(* Expensive tests 1486val p28 = 1487 ``(!x. P(x) ==> (!x. Q(x))) /\ 1488 ((!x. Q(x) \/ R(x)) ==> (?x. Q(x) /\ R(x))) /\ 1489 ((?x. R(x)) ==> (!x. L(x) ==> M(x))) ==> 1490 (!x. P(x) /\ L(x) ==> M(x))``; 1491time CNF_CONV (mk_neg p28); 1492 1493val gilmore9 = Term 1494 `!x. ?y. !z. 1495 ((!u. ?v. F'(y, u, v) /\ G(y, u) /\ ~H(y, x)) ==> 1496 (!u. ?v. F'(x, u, v) /\ G(z, u) /\ ~H(x, z)) ==> 1497 (!u. ?v. F'(x, u, v) /\ G(y, u) /\ ~H(x, y))) /\ 1498 ((!u. ?v. F'(x, u, v) /\ G(y, u) /\ ~H(x, y)) ==> 1499 ~(!u. ?v. F'(x, u, v) /\ G(z, u) /\ ~H(x, z)) ==> 1500 (!u. ?v. F'(y, u, v) /\ G(y, u) /\ ~H(y, x)) /\ 1501 (!u. ?v. F'(z, u, v) /\ G(y, u) /\ ~H(z, y)))`; 1502time CNF_CONV (mk_neg gilmore9); 1503 1504val p34 = 1505 ``((?x. !y. P(x) = P(y)) = 1506 ((?x. Q(x)) = (!y. Q(y)))) = 1507 ((?x. !y. Q(x) = Q(y)) = 1508 ((?x. P(x)) = (!y. P(y))))``; 1509time CNF_CONV (mk_neg p34); 1510 1511(* Large formulas *) 1512 1513val DEF_CNF_CONV' = 1514 time DEF_NNF_CONV THENC 1515 time PURE_DEF_CNF_CONV THENC 1516 time CLEANUP_DEF_CNF_CONV; 1517 1518val _ = time CLEANUP_DEF_CNF_CONV tm2; 1519 1520val valid1 = time (mk_neg o Term) valid_1; 1521 1522val _ = time DEF_CNF_CONV' valid1; 1523 1524(* The pigeon-hole principle *) 1525 1526fun test n = ((time DEF_CNF_CONV' o time (mk_neg o var_pigeon)) n; n); 1527 1528test 8; 1529test 9; 1530test 10; 1531test 11; 1532test 12; 1533test 13; 1534test 14; 1535test 15; 1536 1537val _ = use "../metis/data/large-problem.sml"; 1538val large_problem = time Term large_problem_frag; 1539time CNF_CONV (mk_neg large_problem); 1540*) 1541 1542end 1543