1(* ========================================================================= *) 2(* MAPPING BETWEEN HOL AND FIRST-ORDER LOGIC. *) 3(* Created by Joe Hurd, October 2001 *) 4(* ========================================================================= *) 5 6structure folMapping :> folMapping = 7struct 8 9open HolKernel Parse boolLib; 10 11infix THENR ## |->; 12 13type 'a pp = 'a mlibUseful.pp; 14type term1 = mlibTerm.term; 15type formula1 = mlibTerm.formula; 16type thm1 = mlibThm.thm; 17type vars = term list * hol_type list; 18 19val assert = mlibUseful.assert; 20val pinst = matchTools.pinst; 21val INST_TY = matchTools.INST_TY; 22val PINST = matchTools.PINST; 23 24(* ------------------------------------------------------------------------- *) 25(* Chatting and error handling. *) 26(* ------------------------------------------------------------------------- *) 27 28local 29 open mlibUseful; 30 val module = "folMapping"; 31in 32 val () = add_trace {module = module, alignment = I} 33 fun chatting l = tracing {module = module, level = l}; 34 fun chat s = (trace s; true) 35 val ERR = mk_HOL_ERR module; 36 fun BUG f m = Bug (f ^ ": " ^ m); 37end; 38 39(* ------------------------------------------------------------------------- *) 40(* Mapping parameters. *) 41(* ------------------------------------------------------------------------- *) 42 43type parameters = 44 {higher_order : bool, (* Application is a first-order function *) 45 with_types : bool}; (* First-order terms include HOL type info *) 46 47val defaults = 48 {higher_order = false, 49 with_types = false}; 50 51fun update_higher_order f (parm : parameters) : parameters = 52 let val {higher_order, with_types} = parm 53 in {higher_order = f higher_order, with_types = with_types} 54 end; 55 56fun update_with_types f (parm : parameters) : parameters = 57 let val {higher_order, with_types} = parm 58 in {higher_order = higher_order, with_types = f with_types} 59 end; 60 61(* ------------------------------------------------------------------------- *) 62(* Helper functions. *) 63(* ------------------------------------------------------------------------- *) 64 65fun uncurry3 f (x, y, z) = f x y z; 66 67fun zipwith f = 68 let 69 fun z l [] [] = l 70 | z l (x :: xs) (y :: ys) = z (f x y :: l) xs ys 71 | z _ _ _ = raise ERR "zipwith" "lists different lengths"; 72 in 73 fn xs => fn ys => rev (z [] xs ys) 74 end; 75 76fun possibly f x = case total f x of SOME y => y | NONE => x; 77 78fun dest_prefix p = 79 let 80 fun check s = assert (String.isPrefix p s) (ERR "dest_prefix" "") 81 val size_p = size p 82 in 83 fn s => (check s; String.extract (s, size_p, NONE)) 84 end; 85 86fun is_prefix p = can (dest_prefix p); 87 88fun mk_prefix p s = p ^ s; 89 90val dest_prime = dest_prefix "'"; 91val is_prime = is_prefix "'"; 92val mk_prime = mk_prefix "'"; 93 94fun dest_const_name s = 95 let val n = index (equal #".") (String.explode s) 96 in (String.extract (s, 0, SOME n), String.extract (s, n + 1, NONE)) 97 end; 98val is_const_name = can dest_const_name; 99fun mk_const_name (t, c) = t ^ "." ^ c; 100 101val type_vars_in_terms = foldl (fn (h, t) => union (type_vars_in_term h) t) []; 102 103fun list_mk_conj' [] = T | list_mk_conj' l = list_mk_conj l; 104fun list_mk_disj' [] = F | list_mk_disj' l = list_mk_disj l; 105 106fun change_vars (tmG, tyG) (tmV, tyV) = 107 let 108 fun tyF v = let val g = tyG v in (g, v |-> g) end 109 val (tyV', tyS) = unzip (map tyF tyV) 110 fun tmF v = let val v' = inst tyS v val g = tmG v' in (g, v' |-> g) end 111 val (tmV', tmS) = unzip (map tmF tmV) 112 in 113 ((tmV', tyV'), (tmS, tyS)) 114 end; 115 116fun gen_alpha c f (varV, a) = 117 let val (varW, sub) = c varV in (varW, f sub a) end; 118 119fun gen_vfree_vars varP c a = (matchTools.vfree_vars varP (c a), a); 120 121fun f THENR (g : rule) : rule = g o f; 122fun REPEATR f : rule = repeat f; 123 124fun terms_to_string tms = 125 String.concat (map (fn x => "\n" ^ Parse.term_to_string x) tms) ^ "\n"; 126 127fun remove_type (mlibTerm.Fn (":", [tm, _])) = tm | remove_type tm = tm; 128 129(* ------------------------------------------------------------------------- *) 130(* "new" variables can be instantiated; everything else is a local constant. *) 131(* ------------------------------------------------------------------------- *) 132 133val FOL_PREFIX = "XXfolXX"; 134 135local 136 val tag = mk_prefix FOL_PREFIX; 137 val untag = dest_prefix FOL_PREFIX; 138 val new_string = mlibUseful.int_to_string o mlibUseful.new_int; 139in 140 val fake_new_tyvar = mk_vartype o mk_prime o tag; 141 val new_tyvar = fake_new_tyvar o new_string; 142 val is_new_tyvar = can (untag o dest_prime o dest_vartype); 143 val fake_new_var = mk_var o (tag ## I); 144 val new_var = fake_new_var o (new_string ## I) o pair (); 145 val is_new_var = can (untag o fst o dest_var); 146end; 147 148val all_new_tyvars = 149 W (inst o map (fn v => v |-> new_tyvar ()) o type_vars_in_term); 150 151val to_gen = (genvar o type_of, (fn _ : hol_type => gen_tyvar ())); 152val to_new = (new_var o type_of, (fn _ : hol_type => new_tyvar ())); 153val to_fake_new = (fake_new_var o dest_var, 154 fake_new_tyvar o dest_prime o dest_vartype); 155 156fun new_free_vars x = gen_vfree_vars (is_new_var, is_new_tyvar) x; 157 158val fresh_tyvars = 159 let fun f ty = if is_new_tyvar ty then SOME (ty |-> new_tyvar ()) else NONE 160 in List.mapPartial f o type_vars_in_terms 161 end; 162 163fun freshen_tyvars tm = inst (fresh_tyvars [tm]) tm; 164fun freshenl_tyvars tms = map (inst (fresh_tyvars tms)) tms; 165 166val new_match_type = matchTools.vmatch_type is_new_tyvar; 167val new_unify_type = matchTools.vunify_type is_new_tyvar; 168val new_unifyl_type = matchTools.vunifyl_type is_new_tyvar; 169val new_match_ty = matchTools.vmatch (K false, is_new_tyvar); 170val new_unify_ty = matchTools.vunify (K false, is_new_tyvar); 171val new_unifyl_ty = matchTools.vunifyl (K false, is_new_tyvar); 172val new_match = matchTools.vmatch (is_new_var, is_new_tyvar); 173val new_match_uty = matchTools.vmatch_uty (is_new_var, is_new_tyvar); 174val new_unify = matchTools.vunify (is_new_var, is_new_tyvar); 175val new_unifyl = matchTools.vunifyl (is_new_var, is_new_tyvar); 176 177(* ------------------------------------------------------------------------- *) 178(* Operations on terms with floppy type variables. *) 179(* ------------------------------------------------------------------------- *) 180 181local 182 fun sync tyS _ [] = tyS 183 | sync tyS vars (tm :: work) = 184 (case dest_term tm of VAR (s, ty) => 185 if not (is_new_var tm) then sync tyS vars work else 186 (case assoc1 s vars of NONE => sync tyS ((s, ty) :: vars) work 187 | SOME (_, ty') => sync (new_unifyl_type tyS [(ty, ty')]) vars work) 188 | COMB (a, b) => sync tyS vars (a :: b :: work) 189 | CONST _ => sync tyS vars work 190 | LAMB _ => raise ERR "sync_vars" "lambda"); 191in 192 fun sync_vars tms = sync [] [] tms; 193end; 194 195local 196 fun app s (a, b) = new_unifyl_type s [(a, b --> new_tyvar ())]; 197 fun iapp b (a, s) = 198 let val s = app s (a, b) in (snd (dom_rng (type_subst s a)), s) end; 199in 200 fun prepare_mk_comb (a, b) = app (sync_vars [a, b]) (type_of a, type_of b) 201 fun prepare_list_mk_comb (f, a) = 202 snd (foldl (uncurry (iapp o type_of)) (type_of f, sync_vars (f :: a)) a); 203end; 204 205fun unify_mk_comb (a, b) = 206 let val i = inst (prepare_mk_comb (a, b)) in mk_comb (i a, i b) end; 207 208fun unify_list_mk_comb (f, a) = 209 let val i = inst (prepare_list_mk_comb (f, a)) 210 in list_mk_comb (i f, map i a) 211 end; 212 213local val eq_tm = prim_mk_const {Thy = "min", Name = "="}; 214in fun unify_mk_eq (a, b) = unify_list_mk_comb (all_new_tyvars eq_tm, [a, b]); 215end; 216 217val freshen_mk_comb = freshen_tyvars o unify_mk_comb; 218val freshen_list_mk_comb = freshen_tyvars o unify_list_mk_comb; 219 220fun cast_to ty tm = inst (new_match_type (type_of tm) ty) tm; 221 222(* Quick testing 223val a = mk_varconst "list.LENGTH"; type_of a; 224val b = mk_varconst "x"; type_of b; 225val c = unify_mk_comb (a, b); type_of c; 226try sync_vars [``LENGTH (x:'b list) <= 0``, ``x:'a``, ``HD x = 3``]; 227prepare_list_mk_comb (``LENGTH``, [``[3; 4]``]); 228try unify_list_mk_comb (``COND``, new_tyvars [``HD x``, ``CONS x``, ``I``]); 229*) 230 231(* ------------------------------------------------------------------------- *) 232(* Worker theorems for first-order proof translation. *) 233(* ------------------------------------------------------------------------- *) 234 235val HIDE_LITERAL = prove 236 (``!a. a ==> ~a ==> F``, 237 tautLib.TAUT_TAC); 238 239val SHOW_LITERAL = prove 240 (``!x. (~x ==> F) ==> x``, 241 tautLib.TAUT_TAC); 242 243val INITIALIZE_CLAUSE = prove 244 (``!a b. a \/ b ==> ~a ==> b``, 245 tautLib.TAUT_TAC); 246 247val FINALIZE_CLAUSE = prove 248 (``!a b. (~a ==> b) ==> (a \/ b)``, 249 tautLib.TAUT_TAC); 250 251val RESOLUTION = prove 252 (``!a. a /\ ~a ==> F``, 253 tautLib.TAUT_TAC); 254 255val EQUAL_STEP = prove 256 (``!a b c. ((a ==> (b = c)) /\ b) ==> ~a \/ c``, 257 tautLib.TAUT_TAC); 258 259val EXCLUDED_MIDDLE' = prove 260 (``!t. ~t \/ t``, 261 tautLib.TAUT_TAC); 262 263(* ------------------------------------------------------------------------- *) 264(* Operations on HOL literals and clauses. *) 265(* ------------------------------------------------------------------------- *) 266 267(* 268val negative_literal = is_neg; 269 270val positive_literal = not o negative_literal; 271 272fun negate_literal lit = 273 if positive_literal lit then mk_neg lit else dest_neg lit; 274 275fun literal_atom lit = if positive_literal lit then lit else negate_literal lit; 276*) 277 278val clause_literals = strip_disj o snd o strip_forall; 279 280(* 281local 282 fun atom ({higher_order, with_types} : parameters) p 283fun lit_subterm parm p lit = 284 if is_neg lit then (mk_neg o cast_to 285 let 286 val 287*) 288 289(* ------------------------------------------------------------------------- *) 290(* Operations for accessing literals, which are kept on the assumption list. *) 291(* ------------------------------------------------------------------------- *) 292 293fun hide_literal th = UNDISCH (MP (SPEC (concl th) HIDE_LITERAL) th); 294 295fun show_literal lit = 296 let val lit' = mk_neg lit 297 in DISCH lit' THENR MP (SPEC lit SHOW_LITERAL) 298 end; 299 300local 301 fun REMOVE_DISJ th = 302 let val (a,b) = dest_disj (concl th) 303 in UNDISCH (MP (SPECL [a,b] INITIALIZE_CLAUSE) th) 304 end; 305 306 val INIT = 307 CONV_RULE (REPEATC (REWR_CONV (GSYM DISJ_ASSOC))) 308 THENR REPEATR REMOVE_DISJ 309 THENR hide_literal; 310in 311 fun initialize_lits th = 312 if concl th = F then ([], th) else (strip_disj (concl th), INIT th); 313end; 314 315local 316 fun final_lit lit = 317 let val lit' = mk_neg lit 318 in fn th => MP (SPECL [lit, concl th] FINALIZE_CLAUSE) (DISCH lit' th) 319 end; 320in 321 fun finalize_lits (lits, th) = 322 case rev lits of [] => th 323 | lit :: rest => foldl (uncurry final_lit) (show_literal lit th) rest; 324end; 325 326(* Quick testing 327val t1 = initialize_hol_thm (([], []), ASSUME ``p \/ ~q \/ ~r \/ s``); 328val t2 = initialize_hol_thm (([], []), ASSUME ``((p \/ ~q) \/ ~r) \/ s``); 329try finalize_hol_thm t1; 330try finalize_hol_thm t2; 331*) 332 333(* ------------------------------------------------------------------------- *) 334(* varconsts lump together constants and locally constant variables. *) 335(* ------------------------------------------------------------------------- *) 336 337fun dest_varconst tm = 338 case dest_term tm of VAR (s, _) => s 339 | CONST {Thy, Name, Ty = _} => mk_const_name (Thy, Name) 340 | _ => raise ERR "dest_varconst" (term_to_string tm ^ " is neither"); 341 342val is_varconst = can dest_varconst; 343 344fun mk_varconst s = 345 all_new_tyvars 346 (if is_const_name s then 347 let val (t, n) = dest_const_name s 348 in prim_mk_const {Thy = t, Name = n} 349 end 350 else mk_var (s, alpha)); 351 352(* ------------------------------------------------------------------------- *) 353(* Prettify FOL representations of HOL terms---WILL BREAK PROOF TRANSLATION! *) 354(* ------------------------------------------------------------------------- *) 355 356val prettify_fol = ref false; 357 358val type_op_map = 359 [("fun", "->"), ("prod", "*"), ("sum", "+")]; 360 361val term_op_map = 362 [("min.=", "equality"), ("min.==>", "implication"), 363 ("bool.T", "truth"), ("bool.F", "falsity"), ("bool.~", "negation"), 364 ("bool./\\", "conjunction"), ("bool.\\/", "disjunction"), 365 ("bool.?", "existential"), ("bool.!", "universal"), 366 ("arithmetic.NUMERAL", "NUMERAL"), ("arithmetic.NUMERAL_BIT1", "BIT1"), 367 ("arithmetic.NUMERAL_BIT2", "BIT2"), ("arithmetic.ALT_ZERO", "ZERO")]; 368 369local 370 val pr_op = possibly (fn x => assoc x type_op_map); 371 fun Var' v = mlibTerm.Var (if is_prime v then "_" ^ dest_prime v else v); 372 fun Fn' (f, a) = mlibTerm.Fn (f, a); 373in 374 fun prettify_type (mlibTerm.Var v) = Var' v 375 | prettify_type (mlibTerm.Fn (f, a)) = Fn' (pr_op f, map prettify_type a); 376end; 377 378local 379 val dest = total (dest_prefix "%%genvar%%"); 380in 381 fun prettify_varname s = 382 case dest s of SOME s' => "vg" ^ s' 383 | NONE => if !mlibTerm.var_string s then s else "v_" ^ s; 384end; 385 386local 387 local val dest = total (dest_prefix "%%genvar%%"); 388 in fun pr_cname s = case dest s of SOME s' => "gv" ^ s' | NONE => s; 389 end; 390 391 fun pr_op s = 392 case assoc1 s term_op_map of SOME (_, s') => s' 393 | NONE => if is_const_name s then snd (dest_const_name s) else pr_cname s; 394 395 fun pr_fn s p a = (pr_op s, p a); 396 397 fun Var' v = mlibTerm.Var (prettify_varname v); 398 fun Fn' (f, a) = mlibTerm.Fn (f, a); 399in 400 fun prettify_term (mlibTerm.Var v) = Var' v 401 | prettify_term (mlibTerm.Fn (":", [tm, ty])) = 402 mlibTerm.Fn (":", [prettify_term tm, prettify_type ty]) 403 | prettify_term (mlibTerm.Fn (f, a)) = Fn' (pr_fn f (map prettify_term) a); 404end; 405 406val prettify_formula = 407 let 408 open mlibTerm 409 fun pr True = True 410 | pr False = False 411 | pr (Atom tm) = Atom (prettify_term tm) 412 | pr (Not f) = Not (pr f) 413 | pr (And (f, g)) = And (pr f, pr g) 414 | pr (Or (f, g)) = Or (pr f, pr g) 415 | pr (Imp (f, g)) = Imp (pr f, pr g) 416 | pr (Iff (f, g)) = Iff (pr f, pr g) 417 | pr (Forall (v, f)) = Forall (prettify_varname v, pr f) 418 | pr (Exists (v, f)) = Exists (prettify_varname v, pr f) 419 in 420 pr 421 end; 422 423(* 424val pp_term1 = mlibUseful.pp_map prettify_term mlibTerm.pp_term; 425val pp_formula1 = mlibUseful.pp_map prettify_formula mlibTerm.pp_formula; 426 427local 428 (* Don't make this visible: theorems deserve better protection *) 429 val prettify_thm = (mlibThm.AXIOM o map prettify_formula o mlibThm.clause); 430in 431 val pp_thm1 = mlibUseful.pp_map prettify_thm mlibThm.pp_thm; 432end; 433*) 434 435(* ------------------------------------------------------------------------- *) 436(* Translate a HOL type to FOL, and back again. *) 437(* ------------------------------------------------------------------------- *) 438 439local 440 fun dest_type ty = 441 let 442 val {Args, Thy, Tyop} = dest_thy_type ty 443 in 444 (Thy ^ "$" ^ Tyop, Args) 445 end 446 fun mk_type (nm, args) = 447 let 448 val (ss1, ss2) = Substring.position "$" (Substring.full nm) 449 val thy = Substring.string ss1 450 val nm = Substring.slice(ss2, 1, NONE) |> Substring.string 451 in 452 mk_thy_type {Tyop = nm, Thy = thy, Args = args} 453 end 454in 455 456fun hol_type_to_fol tyV = 457 let 458 fun ty_to_fol hol_ty = 459 if is_vartype hol_ty then 460 (if mem hol_ty tyV then mlibTerm.Var else (fn s => mlibTerm.Fn (s, []))) 461 (dest_vartype hol_ty) 462 else 463 let val (f, args) = dest_type hol_ty 464 in mlibTerm.Fn (f, map ty_to_fol args) 465 end 466 in 467 ty_to_fol 468 end; 469 470fun fol_type_to_hol (mlibTerm.Var v) = fake_new_tyvar (possibly dest_prime v) 471 | fol_type_to_hol (mlibTerm.Fn (f, a)) = 472 if not (is_prime f) then mk_type (f, map fol_type_to_hol a) 473 else (assert (null a) (ERR "fol_type_to_hol" "bad prime"); mk_vartype f); 474end (* local *) 475 476val fol_bool = hol_type_to_fol [] bool; 477 478(* Quick testing 479installPP pp_term; 480val t = try hol_type_to_fol [alpha] ``:'a list -> bool # (bool + 'b) list``; 481try fol_type_to_hol t; 482*) 483 484(* ------------------------------------------------------------------------- *) 485(* Translate a HOL literal to FOL. *) 486(* ------------------------------------------------------------------------- *) 487 488fun hol_term_to_fol (parm : parameters) (tmV, tyV) = 489 let 490 val {with_types, higher_order, ...} = parm 491 fun tmty2fol tm = 492 if not with_types then tm2fol tm 493 else mlibTerm.Fn (":", [tm2fol tm, hol_type_to_fol tyV (type_of tm)]) 494 and tm2fol tm = 495 if mem tm tmV then mlibTerm.Var (fst (dest_var tm)) 496 else if higher_order then 497 if is_comb tm then 498 let val (a, b) = dest_comb tm 499 in mlibTerm.Fn ("%", [tmty2fol a, tmty2fol b]) 500 end 501 else mlibTerm.Fn (dest_varconst tm, []) 502 else 503 let 504 val (f, args) = strip_comb tm 505 val () = assert (not (mem f tmV)) (ERR "hol_term_to_fol" "ho term") 506 in 507 mlibTerm.Fn (dest_varconst f, map tmty2fol args) 508 end 509 in 510 fn tm => (if !prettify_fol then prettify_term else I) (tmty2fol tm) 511 end; 512 513fun hol_atom_to_fol parm vs tm = 514 mlibTerm.Atom 515 (if is_eq tm then 516 let val (a, b) = dest_eq tm 517 in mlibTerm.Fn ("=", map (hol_term_to_fol parm vs) [a, b]) 518 end 519 else if #higher_order parm then mlibTerm.Fn ("$", [hol_term_to_fol parm vs tm]) 520 else remove_type (hol_term_to_fol parm vs tm)); 521 522fun hol_literal_to_fol parm vars lit = 523 if is_neg lit then mlibTerm.Not (hol_atom_to_fol parm vars (dest_neg lit)) 524 else hol_atom_to_fol parm vars lit; 525 526(* ------------------------------------------------------------------------- *) 527(* The HOL -> FOL user interface: *) 528(* translation of theorems and lists of literals. *) 529(* ------------------------------------------------------------------------- *) 530 531fun hol_literals_to_fol parm (vars, lits) = 532 map (hol_literal_to_fol parm vars) lits; 533 534fun hol_thm_to_fol parm (vars, th) = 535 mlibThm.AXIOM (hol_literals_to_fol parm (vars, fst (initialize_lits th))); 536 537(* Quick testing 538installPP pp_formula; 539try hol_literals_to_fol {higher_order = true, with_types = true} 540 (([``v_b : 'b``], [``:'a``]), 541 [``~P (c_a : 'a, v_b : 'b)``, ``0 <= LENGTH ([] : 'a list)``]); 542try hol_literals_to_fol {higher_order = true, with_types = false} 543 (([``v_b : 'b``], [``:'a``]), 544 [``~P (c_a : 'a, v_b : 'b)``, ``0 <= LENGTH ([] : 'a list)``]); 545try hol_literals_to_fol {higher_order = false, with_types = true} 546 (([``v_b : 'b``], [``:'a``]), 547 [``~P (c_a : 'a, v_b : 'b)``, ``0 <= LENGTH ([] : 'a list)``]); 548try hol_literals_to_fol {higher_order = false, with_types = false} 549 (([``v_b : 'b``], [``:'a``]), 550 [``~P (c_a : 'a, v_b : 'b)``, ``0 <= LENGTH ([] : 'a list)``]); 551*) 552 553(* ------------------------------------------------------------------------- *) 554(* Translate a FOL literal to HOL. *) 555(* ------------------------------------------------------------------------- *) 556 557fun fol_term_to_hol' ({higher_order, with_types = true, ...} : parameters) = 558 let 559 fun tmty_to_hol (mlibTerm.Fn (":",[tm,ty])) = tm_to_hol (fol_type_to_hol ty) tm 560 | tmty_to_hol _ = raise ERR "fol_term_to_hol" "missing type information" 561 and tm_to_hol ty (mlibTerm.Var v) = fake_new_var (v, ty) 562 | tm_to_hol ty (mlibTerm.Fn (fname, args)) = 563 if higher_order then 564 case (fname, args) of (_, []) => cast_to ty (mk_varconst fname) 565 | ("%", [f, a]) => mk_comb (tmty_to_hol f, tmty_to_hol a) 566 | _ => raise ERR "fol_term_to_hol" "(typed) weird higher-order term" 567 else 568 let 569 val hol_args = map tmty_to_hol args 570 val f_type = foldr (fn (h, t) => type_of h --> t) ty hol_args 571 in 572 list_mk_comb (cast_to f_type (mk_varconst fname), hol_args) 573 end 574 in 575 tmty_to_hol 576 end 577 | fol_term_to_hol' ({higher_order, with_types = false, ...} : parameters) = 578 let 579 fun tm_to_hol (mlibTerm.Var v) = fake_new_var (v, new_tyvar ()) 580 | tm_to_hol (mlibTerm.Fn (fname, args)) = 581 if higher_order then 582 case (fname, args) of (_, []) => mk_varconst fname 583 | ("%", [f, a]) => freshen_mk_comb (tm_to_hol f, tm_to_hol a) 584 | _ => raise ERR "fol_term_to_hol" "(typeless) weird higher-order term" 585 else freshen_list_mk_comb (mk_varconst fname, map tm_to_hol args) 586 in 587 tm_to_hol 588 end; 589 590fun fol_term_to_hol parm fol_tm = 591 if not (chatting 1) then fol_term_to_hol' parm fol_tm else 592 let 593 fun cmp (mlibTerm.Var v) (mlibTerm.Var w) = 594 possibly dest_prime v = dest_prefix FOL_PREFIX (possibly dest_prime w) 595 | cmp (mlibTerm.Fn (f, a)) (mlibTerm.Fn (g, b)) = 596 f = g andalso length a = length b andalso 597 List.all (uncurry cmp) (zip a b) 598 | cmp _ _ = false 599 val hol_tm = fol_term_to_hol' parm fol_tm 600 val fol_tm' = uncurry (hol_term_to_fol parm) (new_free_vars I hol_tm) 601 val () = assert (cmp fol_tm fol_tm') 602 (BUG "fol_term_to_hol" 603 ("not inverse:\n\noriginal fol =\n" ^ mlibTerm.term_to_string fol_tm ^ 604 "\n\nhol =\n" ^ term_to_string hol_tm ^ 605 "\n\nnew fol =\n" ^ mlibTerm.term_to_string fol_tm')) 606 in 607 hol_tm 608 end; 609 610fun fol_atom_to_hol parm (mlibTerm.Atom (mlibTerm.Fn ("=", [x, y]))) = 611 unify_mk_eq (fol_term_to_hol parm x, fol_term_to_hol parm y) 612 | fol_atom_to_hol parm fm = 613 (cast_to bool o fol_term_to_hol parm) 614 let 615 val {higher_order, with_types} = parm 616 in 617 case (higher_order, with_types, fm) of 618 (true, _, mlibTerm.Atom (mlibTerm.Fn ("$", [tm]))) => tm 619 | (false, true, mlibTerm.Atom tm) => mlibTerm.Fn (":", [tm, fol_bool]) 620 | (false, false, mlibTerm.Atom tm) => tm 621 | _ => raise BUG "fol_atom_to_fol" "malformed atom" 622 end; 623 624fun fol_literal_to_hol _ mlibTerm.True = T 625 | fol_literal_to_hol _ mlibTerm.False = F 626 | fol_literal_to_hol parm (mlibTerm.Not a) = mk_neg (fol_literal_to_hol parm a) 627 | fol_literal_to_hol parm (a as mlibTerm.Atom _) = fol_atom_to_hol parm a 628 | fol_literal_to_hol _ _ = raise ERR "fol_literal_to_hol" "not a literal"; 629 630(* Quick testing 631installPP pp_formula; 632val parm = {higher_order = false, with_types = true}; 633val lits = try hol_literals_to_fol parm 634 (([``v_b : 'b``], [``:'b``]), 635 [``~P (c_a : 'a list, v_b : 'b)``, ``0 <= LENGTH (c_a : 'a list)``]); 636val [lit1, lit2] = lits; 637try (fol_literal_to_hol parm) lit1; 638try (fol_literal_to_hol parm) lit2; 639*) 640 641(* ------------------------------------------------------------------------- *) 642(* Translate FOL paths to HOL. *) 643(* ------------------------------------------------------------------------- *) 644 645local 646 fun zeroes l [] = rev l 647 | zeroes l (0 :: h :: t) = zeroes (h :: l) t 648 | zeroes _ _ = raise BUG "fol_path_to_hol" "couldn't strip zeroes"; 649 650 fun hp r tm [] = (r, tm) 651 | hp r tm (0 :: p) = hp (r o RATOR_CONV) (rator tm) p 652 | hp r tm (1 :: p) = hp (r o RAND_CONV) (rand tm) p 653 | hp _ _ _ = raise BUG "fol_path_to_hol" "bad higher-order path"; 654 655 fun fp r tm [] = (r, tm) 656 | fp r tm (n :: p) = 657 let 658 val (_, l) = strip_comb tm 659 val m = (length l - 1) - n 660 val r = r o funpow m RATOR_CONV o RAND_CONV 661 val tm = rand (funpow m rator tm) 662 in 663 fp r tm p 664 end; 665 666 fun ap {higher_order, with_types} (r, tm) p = 667 uncurry3 (if higher_order then hp else fp) 668 ((fn (r', tm', p') => (r', tm', if with_types then zeroes [] p' else p')) 669 (if is_eq tm then 670 (case p of 0 :: p => (r o LAND_CONV, lhs tm, p) 671 | 1 :: p => (r o RAND_CONV, rhs tm, p) 672 | _ => raise BUG "fol_path_to_hol" "bad eq path") 673 else 674 (r, tm, 675 (if higher_order then 676 (case p of 0 :: p => p 677 | _ => raise BUG "fol_path_to_hol" "bad higher-order path") 678 else if with_types then 0 :: p 679 else p)))); 680in 681 fun fol_path_to_hol parm p tm = 682 ap parm (if is_neg tm then (RAND_CONV, dest_neg tm) else (I, tm)) p; 683end; 684 685(* Quick testing 686val parm = {higher_order = false, with_types = true}; 687mlibUseful.try (fol_path_to_hol parm) [0, 0, 1] ``~p a b c``; 688*) 689 690(* ------------------------------------------------------------------------- *) 691(* Translate a FOL theorem to HOL (the tricky bit). *) 692(* ------------------------------------------------------------------------- *) 693 694type Axioms = thm1 -> vars * thm; 695type Pattern = vars * term list; 696type Result = vars * thm list; 697 698fun proof_step parm prev = 699 let 700 open mlibTerm mlibMatch mlibThm 701 702 fun freshen (lits, th) = 703 if #with_types parm then (lits, th) 704 else 705 let val sub = fresh_tyvars lits 706 in (map (inst sub) lits, INST_TY sub th) 707 end 708 709 fun match_lits l l' = 710 (if #with_types parm then match_term else new_match_uty) 711 (list_mk_disj' l) (list_mk_disj' l') 712 713 fun step (fol_th, Axiom' _) = prev fol_th 714 | step (_, Assume' fol_lit) = 715 let 716 val th = if positive fol_lit then EXCLUDED_MIDDLE else EXCLUDED_MIDDLE' 717 val hol_atom = fol_literal_to_hol parm (literal_atom fol_lit) 718 in 719 initialize_lits (SPEC hol_atom th) 720 end 721 | step (fol_th, Inst' (_, fol_th1)) = 722 let 723 val (hol_lits1, hol_th1) = prev fol_th1 724 val hol_lits = map (fol_literal_to_hol parm) (clause fol_th) 725 val sub = match_lits hol_lits1 hol_lits 726 in 727 (map (pinst sub) hol_lits1, PINST sub hol_th1) 728 end 729 | step (_, Factor' fol_th) = 730 let 731 fun f uns lits [] = (new_unifyl_ty ([], []) uns, rev (map snd lits)) 732 | f uns lits ((fl, hl) :: rest) = 733 case List.find (equal fl o fst) lits of NONE 734 => f uns ((fl, hl) :: lits) rest 735 | SOME (_, hl') => f ((hl, hl') :: uns) lits rest 736 val (hol_lits, hol_th) = prev fol_th 737 val (sub, hol_lits') = f [] [] (zip (clause fol_th) hol_lits) 738 in 739 (map (pinst sub) hol_lits', PINST sub hol_th) 740 end 741 | step (_, Resolve' (False, fol_th1, fol_th2)) = 742 let 743 val (hol_lits1, hol_th1) = prev fol_th1 744 val (hol_lits2, _) = prev fol_th2 745 in 746 (hol_lits1 @ hol_lits2, hol_th1) 747 end 748 | step (_, Resolve' (fol_lit, fol_th1, fol_th2)) = 749 let 750 fun res0 fth fl = 751 let 752 val (hls, hth) = prev fth 753 val (a, b) = partition (equal fl o fst) (zip (clause fth) hls) 754 in 755 ((map snd a, map snd b), hth) 756 end 757 val (negate_lit, negate_lit') = 758 if positive fol_lit then (boolSyntax.mk_neg, boolSyntax.dest_neg) 759 else (boolSyntax.dest_neg, boolSyntax.mk_neg) 760 val hol_lit = fol_literal_to_hol parm fol_lit 761 val ((hol_ms1, hol_lits1), hol_th1) = res0 fol_th1 fol_lit 762 val ((hol_ms2, hol_lits2), hol_th2) = res0 fol_th2 (negate fol_lit) 763 val _ = chatting 2 andalso chat 764 ("resolve: hol_lits1 =\n" ^ terms_to_string hol_lits1 ^ 765 "resolve: hol_lits2 =\n" ^ terms_to_string hol_lits2 ^ 766 "resolve: hol_ms1 =\n" ^ terms_to_string hol_ms1 ^ 767 "resolve: hol_ms2 =\n" ^ terms_to_string hol_ms2) 768 val sub = new_unify_ty (hol_lit :: hol_ms1 @ map negate_lit' hol_ms2) 769 val hol_lit' = pinst sub hol_lit 770 val hol_nlit' = negate_lit hol_lit' 771 val hol_th1' = show_literal hol_lit' (PINST sub hol_th1) 772 val hol_th2' = show_literal hol_nlit' (PINST sub hol_th2) 773 in 774 (map (pinst sub) (hol_lits1 @ hol_lits2), 775 if positive fol_lit then 776 MP (SPEC hol_lit' RESOLUTION) (CONJ hol_th1' hol_th2') 777 else 778 MP (SPEC hol_nlit' RESOLUTION) (CONJ hol_th2' hol_th1')) 779 end 780 | step (_, Refl' fol_tm) = 781 initialize_lits (Thm.REFL (fol_term_to_hol parm fol_tm)) 782 | step (_, Equality' (fol_lit, fol_p, fol_r, lr, fol_th)) = 783 let 784 val (hol_lits, hol_th) = prev fol_th 785 val n = mlibUseful.index (equal fol_lit) (clause fol_th) 786 val hol_lit = 787 case n of NONE => fol_literal_to_hol parm fol_lit 788 | SOME n => List.nth (hol_lits, n) 789 val hol_r = fol_term_to_hol parm fol_r 790 val sub = sync_vars [hol_lit, hol_r] 791 val hol_lits = map (inst sub) hol_lits 792 val hol_th = INST_TY sub hol_th 793 val hol_lit = inst sub hol_lit 794 val hol_r = inst sub hol_r 795 val (PATH, hol_l) = fol_path_to_hol parm fol_p hol_lit 796 val sub = (new_unify_type o map type_of) [hol_l, hol_r] 797 val hol_lits = map (inst sub) hol_lits 798 val hol_th = INST_TY sub hol_th 799 val hol_lit = inst sub hol_lit 800 val hol_r = inst sub hol_r 801 val hol_l = inst sub hol_l 802 val eq = boolSyntax.mk_eq (if lr then (hol_l,hol_r) else (hol_r,hol_l)) 803 val hol_eq_th = (if lr then I else Thm.SYM) (Thm.ASSUME eq) 804 val hol_lit_th = (PATH (K hol_eq_th)) hol_lit 805 val hol_lit' = (boolSyntax.rhs o concl) hol_lit_th 806 val hol_lits' = 807 mk_neg eq :: 808 (case n of NONE => hol_lit' :: hol_lits 809 | SOME n => mlibUseful.update_nth (K hol_lit') n hol_lits) 810 val hol_lem = CONJ (DISCH eq hol_lit_th) (show_literal hol_lit hol_th) 811 val equal_step = SPECL [eq, hol_lit, hol_lit'] EQUAL_STEP 812 in 813 (hol_lits', snd (initialize_lits (MP equal_step hol_lem))) 814 end; 815 in 816 fn p => freshen (step p) 817 end; 818 819local 820 val initialize_axiom = 821 initialize_lits o snd o gen_alpha (change_vars to_fake_new) PINST; 822 823 fun previous a l x = 824 case assoc1 x l of SOME (_, y) => y | NONE => initialize_axiom (a x); 825 826 fun chat_proof th = 827 if not (chatting 1) then mlibThm.proof th else 828 let 829 val res = mlibThm.proof th 830 val _ = chat ("\n\nProof:\n" ^ mlibThm.proof_to_string res ^ "\n\n") 831 in 832 res 833 end; 834 835 fun chat_proof_step parm prev (p as (fol_th, inf)) = 836 if not (chatting 1) then proof_step parm prev p else 837 let 838 val _ = chat 839 ("_____________________________________________________\n" ^ 840 "\nfol: " ^ mlibThm.thm_to_string fol_th ^ "\n" ^ 841 "\ninf: " ^ mlibThm.inference_to_string inf ^ "\n") 842 val res = proof_step parm prev p 843 val _ = chat ("\nhol: " ^ thm_to_string (finalize_lits res) ^ "\n") 844 in 845 res 846 end; 847 848 fun translate parm prev = 849 let 850 fun f p [] = finalize_lits (snd (hd p)) 851 | f p (x :: l) = f ((fst x, chat_proof_step parm (prev p) x) :: p) l 852 in 853 f 854 end; 855 856 fun match_pattern pattern ths = 857 let 858 val pattern = gen_alpha (change_vars to_new) (map o pinst) pattern 859 val pattern = list_mk_conj' (snd pattern) 860 val ths_foot = list_mk_conj' (map concl ths) 861 in 862 map (PINST (new_match_uty pattern ths_foot)) ths 863 end; 864 865 val finalize_thms = 866 gen_alpha (change_vars to_gen) (map o PINST) o 867 new_free_vars (list_mk_conj' o map concl); 868in 869 fun fol_thms_to_hol parm axioms pattern ths = 870 (finalize_thms o match_pattern pattern o 871 map (translate parm (previous axioms) [] o chat_proof)) ths 872 handle HOL_ERR _ => raise ERR "fol_thms_to_hol" "proof translation error"; 873end; 874 875end 876