1(* ========================================================================= *) 2(* INTERFACE TO THE LCF-STYLE LOGICAL KERNEL, PLUS SOME DERIVED RULES *) 3(* Copyright (c) 2001-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6structure mlibThm :> mlibThm = 7struct 8 9open mlibUseful mlibTerm mlibKernel mlibMatch; 10 11infixr ::> 12 13structure T = mlibTermnet; local open mlibTermnet in end; 14 15type subst = mlibSubst.subst; 16val |<>| = mlibSubst.|<>|; 17val op ::> = mlibSubst.::>; 18val term_subst = mlibSubst.term_subst; 19val formula_subst = mlibSubst.formula_subst; 20val pp_subst = mlibSubst.pp_subst; 21 22(* ------------------------------------------------------------------------- *) 23(* Chatting. *) 24(* ------------------------------------------------------------------------- *) 25 26val module = "mlibThm"; 27val () = add_trace {module = module, alignment = I} 28fun chatting l = tracing {module = module, level = l}; 29fun chat s = (trace s; true) 30 31fun chattrans n s a b pp = 32 if not (chatting n) then () 33 else (chat (s ^ ": " ^ pp a ^ " --> " ^ pp b ^ "\n"); ()); 34 35(* ------------------------------------------------------------------------- *) 36(* Annotated primitive inferences. *) 37(* ------------------------------------------------------------------------- *) 38 39datatype inference' = 40 Axiom' of formula list 41| Refl' of term 42| Assume' of formula 43| Inst' of subst * thm 44| Factor' of thm 45| Resolve' of formula * thm * thm 46| Equality' of formula * int list * term * bool * thm 47 48fun primitive_inference (Axiom' cl) = AXIOM cl 49 | primitive_inference (Refl' tm) = REFL tm 50 | primitive_inference (Assume' l) = ASSUME l 51 | primitive_inference (Inst' (s,th)) = INST s th 52 | primitive_inference (Factor' th) = FACTOR th 53 | primitive_inference (Resolve' (l,th1,th2)) = RESOLVE l th1 th2 54 | primitive_inference (Equality' (l,p,t,s,th)) = EQUALITY l p t s th; 55 56val clause = fst o dest_thm; 57 58fun dest_axiom th = 59 case dest_thm th of (lits,(Axiom,[])) => lits 60 | _ => raise Error "dest_axiom"; 61 62val is_axiom = can dest_axiom; 63 64(* ------------------------------------------------------------------------- *) 65(* Pretty-printing of theorems *) 66(* ------------------------------------------------------------------------- *) 67 68fun pp_thm th = 69 PP.block PP.INCONSISTENT 3 70 [PP.add_string "|- ", pp_formula (list_mk_disj (clause th))]; 71 72fun inference_to_string Axiom = "Axiom" 73 | inference_to_string Refl = "Refl" 74 | inference_to_string Assume = "Assume" 75 | inference_to_string Inst = "Inst" 76 | inference_to_string Factor = "Factor" 77 | inference_to_string Resolve = "Resolve" 78 | inference_to_string Equality = "Equality"; 79 80val pp_inference = pp_map inference_to_string pp_string; 81 82fun dest_inference' (Axiom' _) = Axiom 83 | dest_inference' (Refl' _) = Refl 84 | dest_inference' (Assume' _) = Assume 85 | dest_inference' (Factor' _) = Factor 86 | dest_inference' (Inst' _) = Inst 87 | dest_inference' (Resolve' _) = Resolve 88 | dest_inference' (Equality' _) = Equality; 89 90local 91 open PP; 92 93 fun pp_inf pp_ax pp_th inf = 94 let 95 fun pp_i (Axiom' a) = pp_ax a 96 | pp_i (Refl' a) = [add_break (1,0), pp_term a] 97 | pp_i (Assume' a) = [add_break (1,0), pp_formula a] 98 | pp_i (Factor' a) = [add_break (1,0), pp_th a] 99 | pp_i (Inst' (sub,thm)) = 100 [add_break (1,0), 101 block INCONSISTENT 1 [ 102 add_string "{", 103 pp_binop " =" pp_string pp_subst ("sub",sub), 104 add_string ",", add_break (1,0), 105 pp_binop " =" pp_string pp_th ("thm",thm), 106 add_string "}" 107 ] 108 ] 109 | pp_i (Resolve' (res,pos,neg)) = 110 [add_break (1,0), 111 block INCONSISTENT 1 [ 112 add_string "{", 113 pp_binop " =" pp_string pp_formula ("res",res), 114 add_string ",", add_break (1,0), 115 pp_binop " =" pp_string pp_th ("pos",pos), 116 add_string ",", add_break (1,0), 117 pp_binop " =" pp_string pp_th ("neg",neg), 118 add_string "}" 119 ] 120 ] 121 | pp_i (Equality' (lit,path,res,lr,thm)) = 122 [add_break (1,0), 123 block INCONSISTENT 1 [ 124 add_string "{", 125 pp_binop " =" pp_string pp_formula ("lit",lit), 126 add_string ",", add_break (1,0), 127 pp_binop " =" pp_string (pp_list pp_int) ("path",path), 128 add_string ",", add_break (1,0), 129 pp_binop " =" pp_string pp_term ("res",res), 130 add_string ",", add_break (1,0), 131 pp_binop " =" pp_string pp_bool ("lr",lr), 132 add_string ",", add_break (1,0), 133 pp_binop " =" pp_string pp_th ("thm",thm), 134 add_string "}" 135 ] 136 ] 137 in 138 block INCONSISTENT 0 ( 139 pp_inference (dest_inference' inf) :: 140 pp_i inf 141 ) 142 end; 143 144 fun pp_axiom fms = [add_break (1,0), pp_list pp_formula fms] 145in 146 val pp_inference' = pp_inf pp_axiom pp_thm; 147 148 fun pp_proof prf = 149 let 150 fun thm_string n = "(" ^ int_to_string n ^ ")" 151 val prf = enumerate 0 prf 152 fun pp_th th = 153 case List.find (fn (_,(t,_)) => t = th) prf of 154 NONE => add_string "(???)" 155 | SOME (n,_) => add_string (thm_string n) 156 fun pp_step (n,(th,i)) = 157 let 158 val s = thm_string n 159 in 160 [ 161 block CONSISTENT (1 + size s) [ 162 add_string (s ^ " "), 163 pp_thm th, 164 add_break (2,0), 165 pp_bracket "[" "]" (pp_inf (fn _ => []) pp_th) i 166 ], 167 NL 168 ] 169 end 170 in 171 block CONSISTENT 0 ( 172 [add_string "START OF PROOF", NL] @ 173 List.concat (map pp_step prf) @ 174 [add_string "END OF PROOF", NL] 175 ) 176 end; 177end; 178 179(* Purely functional pretty-printing *) 180 181fun thm_to_string' len = PP.pp_to_string len pp_thm; 182fun inference_to_string' len = PP.pp_to_string len pp_inference'; 183fun proof_to_string' len = PP.pp_to_string len pp_proof; 184 185(* Pretty-printing using !LINE_LENGTH *) 186 187fun thm_to_string th = thm_to_string' (!LINE_LENGTH) th; 188fun inference_to_string inf = inference_to_string' (!LINE_LENGTH) inf; 189fun proof_to_string p = proof_to_string' (!LINE_LENGTH) p; 190 191(* ------------------------------------------------------------------------- *) 192(* Theorem operations. *) 193(* ------------------------------------------------------------------------- *) 194 195local 196 fun cmp Axiom Axiom = EQUAL 197 | cmp Axiom _ = LESS 198 | cmp _ Axiom = GREATER 199 | cmp Refl Refl = EQUAL 200 | cmp Refl _ = LESS 201 | cmp _ Refl = GREATER 202 | cmp Assume Assume = EQUAL 203 | cmp Assume _ = LESS 204 | cmp _ Assume = GREATER 205 | cmp Inst Inst = EQUAL 206 | cmp Inst _ = LESS 207 | cmp _ Inst = GREATER 208 | cmp Factor Factor = EQUAL 209 | cmp Factor _ = LESS 210 | cmp _ Factor = GREATER 211 | cmp Resolve Resolve = EQUAL 212 | cmp Resolve Equality = LESS 213 | cmp Equality Resolve = GREATER 214 | cmp Equality Equality = EQUAL; 215 216 fun cm [] = EQUAL 217 | cm ((th1,th2) :: l) = 218 if th1 = th2 then cm l else 219 let 220 val (l1,(p1,ths1)) = dest_thm th1 221 val (l2,(p2,ths2)) = dest_thm th2 222 in 223 case lex_list_order formula_compare (l1,l2) of EQUAL 224 => (case cmp p1 p2 of EQUAL => cm (zip ths1 ths2 @ l) | x => x) 225 | x => x 226 end; 227in 228 fun thm_compare th1_th2 = cm [th1_th2]; 229end; 230 231local 232 val deps = snd o snd o dest_thm; 233 fun empty () = Binarymap.mkDict thm_compare; 234 fun peek th m = Binarymap.peek (m,th); 235 fun ins (th,a) m = Binarymap.insert (m,th,a); 236in 237 fun thm_map f = 238 let 239 fun g th m = 240 case peek th m of SOME a => (a,m) 241 | NONE => 242 let 243 val (al,m) = maps g (deps th) m 244 val a = f (th,al) 245 in 246 (a, ins (th,a) m) 247 end 248 in 249 fn th => fst (g th (empty ())) 250 end; 251end; 252 253local 254 val deps = snd o snd o dest_thm; 255 fun empty a = (Binaryset.empty thm_compare, a); 256 fun mem th (s,_) = Binaryset.member (s,th); 257 fun ins f th (s,a) = (Binaryset.add (s,th), f (th,a)) 258in 259 fun thm_foldr f = 260 let fun g (th,x) = if mem th x then x else ins f th (foldl g x (deps th)) 261 in fn a => fn th => snd (g (th, empty a)) 262 end; 263end; 264 265(* ------------------------------------------------------------------------- *) 266(* Reconstructing proofs. *) 267(* ------------------------------------------------------------------------- *) 268 269fun reconstruct_resolvant cl1 cl2 (cl1',cl2') = 270 case (subtract (setify cl1) cl1', subtract (setify cl2) cl2') of 271 (_ :: _ :: _, _) => NONE 272 | (_, _ :: _ :: _) => NONE 273 | ([l],[]) => SOME l 274 | ([],[l']) => SOME (negate l') 275 | ([l],[l']) => if negate l = l' then SOME l else NONE 276 | ([],[]) => SOME False; 277 278fun reconstruct_equality l r = 279 let 280 fun recon_fn p (f,args) (f',args') rest = 281 recon_tm 282 (if f <> f' orelse length args <> length args' then rest 283 else map (C cons p ## I) (enumerate 0 (zip args args')) @ rest) 284 and recon_tm [] = NONE 285 | recon_tm ((p,(tm,tm')) :: rest) = 286 if tm = l andalso tm' = r then SOME (rev p) 287 else 288 case (tm,tm') of (Fn a, Fn a') => recon_fn p a a' rest 289 | _ => recon_tm rest 290 291 fun recon_lit (Not a) (Not a') = recon_lit a a' 292 | recon_lit (Atom a) (Atom a') = 293 if l <> r andalso a = a' then NONE else recon_tm [([],(a,a'))] 294 | recon_lit _ _ = NONE 295 in 296 fn (lit,lit') => 297 case recon_lit lit lit' of SOME p => SOME (lit,p) | NONE => NONE 298 end; 299 300fun reconstruct (cl,(Axiom,[])) = Axiom' cl 301 | reconstruct ([lit],(Refl,[])) = Refl' (lhs lit) 302 | reconstruct ([fm, _], (Assume,[])) = Assume' fm 303 | reconstruct (cl, (Inst,[th])) = 304 Inst' (matchl_literals |<>| (zip (clause th) cl), th) 305 | reconstruct (_, (Factor,[th])) = Factor' th 306 | reconstruct (cl, (Resolve, [th1, th2])) = 307 let 308 val f = reconstruct_resolvant (clause th1) (clause th2) 309 val l = 310 case f (cl,cl) of SOME l => l 311 | NONE => 312 case first f (List.tabulate (length cl, divide cl)) of SOME l => l 313 | NONE => 314 raise Bug 315 ("inference: couldn't reconstruct resolvant" ^ 316 "\nth = " ^ thm_to_string (AXIOM cl) ^ 317 "\nth1 = " ^ thm_to_string th1 ^ 318 "\nth2 = " ^ thm_to_string th2) 319 in 320 Resolve' (l,th1,th2) 321 end 322 | reconstruct (Not eq :: cl, (Equality,[th])) = 323 if length (clause th) < length cl then 324 let 325 val (l,r) = dest_eq eq 326 val lit = hd cl 327 fun f (p |-> t) = 328 if t = l then SOME (p,false) 329 else if t = r then SOME (p,true) 330 else NONE 331 in 332 case first f (literal_subterms lit) of SOME (p,lr) => 333 let 334 val (l,r) = if lr then (l,r) else (r,l) 335 val lit = literal_rewrite (p |-> l) lit 336 in 337 Equality' (lit,p,r,lr,th) 338 end 339 | NONE => raise Bug "inference: couldn't reconstruct weak equality" 340 end 341 else 342 let 343 val line = zip (clause th) cl 344 fun sync l r = first (reconstruct_equality l r) line 345 val (l,r) = dest_eq eq 346 in 347 case sync l r of SOME (lit,p) => Equality' (lit,p,r,true,th) 348 | NONE => 349 case sync r l of SOME (lit,p) => Equality' (lit,p,l,false,th) 350 | NONE => raise Bug "inference: couldn't reconstruct equality step" 351 end 352 | reconstruct _ = raise Bug "inference: malformed inference"; 353 354fun inference th = 355 let 356 val i = reconstruct (dest_thm th) 357 val _ = 358 (primitive_inference i = th) orelse 359 raise Bug 360 ("inference: failed:\nth = " ^ thm_to_string th ^ "\ninf = " 361 ^ inference_to_string i ^ "\ninf_th = " 362 ^ thm_to_string (primitive_inference i)) 363 in 364 i 365 end; 366 367val proof = rev o thm_foldr (fn (th,l) => (th, inference th) :: l) []; 368 369(* ------------------------------------------------------------------------- *) 370(* Contradictions and units. *) 371(* ------------------------------------------------------------------------- *) 372 373val is_contradiction = null o clause; 374 375fun dest_unit th = 376 case clause th of [lit] => lit | _ => raise Error "dest_unit: not a unit"; 377 378val is_unit = can dest_unit; 379 380val dest_unit_eq = dest_eq o dest_unit; 381 382val is_unit_eq = can dest_unit_eq; 383 384(* ------------------------------------------------------------------------- *) 385(* Derived rules *) 386(* ------------------------------------------------------------------------- *) 387 388fun CONTR False th = th 389 | CONTR lit th = RESOLVE (negate lit) (ASSUME lit) th; 390 391fun WEAKEN lits th = foldl (uncurry CONTR) th (rev lits); 392 393fun FRESH_VARSL ths = 394 let 395 val fvs = FVL [] (List.concat (map clause ths)) 396 val vvs = new_vars (length fvs) 397 val sub = mlibSubst.from_maplets (zipwith (curry op |->) fvs vvs) 398 in 399 map (INST sub) ths 400 end 401 handle Error _ => raise Bug "FRESH_VARSL: shouldn't fail"; 402 403val FRESH_VARS = hd o FRESH_VARSL o sing; 404 405fun UNIT_SQUASH th = 406 case clause th of [] => raise Error "UNIT_SQUASH: contradiction" 407 | [_] => th 408 | _ :: _ :: _ => 409 let 410 fun squash env (x :: (xs as y :: _)) = squash (unify_literals env x y) xs 411 | squash env _ = env 412 in 413 FACTOR (INST (squash |<>| (clause th)) th) 414 end; 415 416val REFLEXIVITY = REFL (Var "x"); 417 418val SYMMETRY = 419 EQUALITY (mk_eq (Var "x", Var "x")) [0] (Var "y") true REFLEXIVITY; 420 421val TRANSITIVITY = 422 EQUALITY (mk_eq (Var "y", Var "z")) [0] (Var "x") false 423 (ASSUME (Not (mk_eq (Var "y", Var "z")))); 424 425fun FUN_CONGRUENCE (function,arity) = 426 let 427 val xs = List.tabulate (arity, fn i => Var ("x" ^ int_to_string i)) 428 val ys = List.tabulate (arity, fn i => Var ("y" ^ int_to_string i)) 429 fun f (i,th) = 430 EQUALITY (List.last (clause th)) [1,i] (List.nth (ys,i)) true th 431 val refl = INST (("x" |-> Fn (function,xs)) ::> |<>|) REFLEXIVITY 432 in 433 foldl f refl (rev (interval 0 arity)) 434 end; 435 436fun REL_CONGRUENCE (relation,arity) = 437 let 438 val xs = List.tabulate (arity, fn i => Var ("x" ^ int_to_string i)) 439 val ys = List.tabulate (arity, fn i => Var ("y" ^ int_to_string i)) 440 fun f (i,th) = 441 EQUALITY (List.last (clause th)) [i] (List.nth (ys,i)) true th 442 val refl = ASSUME (Not (Atom (Fn (relation,xs)))) 443 in 444 foldl f refl (rev (interval 0 arity)) 445 end; 446 447fun SYM lit th = 448 let 449 fun g x y = RESOLVE lit th (EQUALITY (refl x) [0] y true (REFL x)) 450 fun f (true,(x,y)) = g x y | f (false,(x,y)) = g y x 451 in 452 f ((I ## dest_eq) (dest_literal lit)) 453 end; 454 455local 456 fun psym lit = 457 let 458 val (s,(x,y)) = (I ## dest_eq) (dest_literal lit) 459 val () = assert (x <> y) (Error "psym: refl") 460 in 461 mk_literal (s, mk_eq (y,x)) 462 end; 463 464 fun syms [] th = th 465 | syms (l :: ls) th = 466 syms ls 467 (case total psym l of NONE => th 468 | SOME l' => if mem l' ls then SYM l th else th); 469in 470 val EQ_FACTOR = FACTOR o (W (syms o clause)) o FACTOR; 471end; 472 473fun REWR' (rw,r,lr) ((th,lit),tm) p = 474 let 475 val eq = if lr then mk_eq (tm,r) else mk_eq (r,tm) 476 val th' = RESOLVE eq rw (EQUALITY lit p r lr th) 477 val lit' = literal_rewrite (p |-> r) lit 478 val tm' = r 479 in 480 ((th',lit'),tm') 481 end; 482 483fun REWR (rw,lr) (th,lit,p) = 484 let val r = let val (x,y) = dest_unit_eq rw in if lr then y else x end 485 in fst (fst (REWR' (rw,r,lr) ((th,lit), literal_subterm p lit) p)) 486 end; 487 488fun DEPTH1 conv = 489 let 490 fun rewr_top (thl_tm as (_,tm)) p = 491 (case total conv tm of NONE => thl_tm 492 | SOME rw_r_lr => rewr_top (REWR' rw_r_lr thl_tm (rev p)) p) 493 494 fun rewr new thl tm_orig p = 495 let 496 val (thl,tm) = rewr_top (thl,tm_orig) p 497 val () = chattrans 2 "rewr" tm_orig tm term_to_string 498 in 499 if new orelse tm <> tm_orig then rewr_sub thl tm p else (thl,tm) 500 end 501 and rewr_sub thl tm_orig p = 502 let 503 val (thl,tm) = rewr_below thl tm_orig p 504 val () = chattrans 3 "rewr_sub" tm_orig tm term_to_string 505 in 506 if tm <> tm_orig then rewr false thl tm p else (thl,tm) 507 end 508 and rewr_below thl (tm as Var _) _ = (thl,tm) 509 | rewr_below thl (tm as Fn (name,xs)) p = 510 let 511 fun f ((n,x),(tl,ys)) = 512 let val (tl,y) = rewr true tl x (n :: p) in (tl, y :: ys) end 513 val (thl,ys) = (I ## rev) (foldl f (thl,[]) (enumerate 0 xs)) 514 in 515 (thl, if xs = ys then tm else Fn (name,ys)) 516 end 517 518 fun rewr_lit th lit = 519 fst (rewr_below (th,lit) (dest_atom (literal_atom lit)) []) 520 in 521 fn (th,lit) => 522 let 523 val () = assert (mem lit (clause th)) (Bug "DEPTH1: no such literal") 524 val (th',lit') = rewr_lit th lit 525 val () = chattrans 3 "DEPTH1 (thm)" th th' thm_to_string 526 val () = chattrans 2 "DEPTH1 (lit)" lit lit' formula_to_string 527 in 528 (th',lit') 529 end 530 handle Error _ => raise Bug "DEPTH1: shouldn't fail" 531 end; 532 533fun DEPTH conv = 534 let 535 fun rewr_lit (lit,th) = 536 if mem lit (clause th) then fst (DEPTH1 conv (th,lit)) 537 else (assert (is_eq (negate lit)) (Bug "DEPTH: vanished"); th) 538 in 539 fn th => 540 let 541 val th' = foldl rewr_lit th (clause th) 542 val () = chattrans 1 "DEPTH" th th' thm_to_string 543 in 544 th' 545 end 546 handle Error _ => raise Bug "DEPTH: shouldn't fail" 547 end; 548 549(* ------------------------------------------------------------------------- *) 550(* Converting to clauses *) 551(* ------------------------------------------------------------------------- *) 552 553val axiomatize = map AXIOM o mlibCanon.clausal; 554 555val eq_axioms = 556 let 557 val functions' = List.filter (fn (_,n) => 0 < n) o functions 558 val relations' = List.filter (non (equal eq_rel)) o relations 559 val eqs = [REFLEXIVITY, SYMMETRY, TRANSITIVITY] 560 val rels = map REL_CONGRUENCE o relations' 561 val funs = map FUN_CONGRUENCE o functions' 562 in 563 fn fm => eqs @ funs fm @ rels fm 564 end; 565 566local 567 fun eq_axs g = if eq_occurs g then eq_axioms g else []; 568 fun raw a b = (axiomatize a, axiomatize b); 569 fun semi g a b = (eq_axs g @ axiomatize a, axiomatize (Not b)); 570 fun full g = ([], eq_axs g @ axiomatize (Not g)); 571 fun is_raw a b = mlibCanon.is_cnf a andalso mlibCanon.is_cnf b; 572 fun is_semi a b = mlibCanon.is_cnf a andalso mlibCanon.is_clause b andalso b <> False; 573in 574 fun clauses g = 575 let 576 val g = generalize g 577 val (thms,hyps) = 578 case g of 579 Imp (a, Imp (b, False)) => if is_raw a b then raw a b else full g 580 | Imp (a,b) => if is_semi a b then semi g a b else full g 581 | _ => full g 582 in 583 {thms = thms, hyps = hyps} 584 end; 585end; 586 587end 588