1(*===================================================================== *) 2(* FILE : quantHeuristicsLibBase.sml *) 3(* DESCRIPTION : some code to find instantations for quantified *) 4(* variables *) 5(* *) 6(* AUTHORS : Thomas Tuerk *) 7(* DATE : December 2008 *) 8(* ===================================================================== *) 9 10 11structure quantHeuristicsLibBase :> quantHeuristicsLibBase = 12struct 13 14(* 15quietdec := true; 16loadPath := 17 (concat [Globals.HOLDIR, "/src/quantHeuristics"]):: 18 !loadPath; 19 20map load ["quantHeuristicsTheory"]; 21load "ConseqConv" 22show_assums := true; 23quietdec := true; 24*) 25 26open HolKernel Parse boolLib Drule ConseqConv simpLib 27 quantHeuristicsTheory quantHeuristicsTools pairTools 28 29 30(* 31quietdec := false; 32*) 33 34val std_ss = numLib.std_ss 35 36 37 38(******************************************************* 39 * Traces and other global parameters 40 *******************************************************) 41 42val QUANT_INSTANTIATE_HEURISTIC___max_rec_depth = ref 250; 43val _ = register_trace("QUANT_INST___REC_DEPTH", QUANT_INSTANTIATE_HEURISTIC___max_rec_depth, 20000); 44 45val QUANT_INSTANTIATE_HEURISTIC___debug = ref 0; 46val _ = register_trace("QUANT_INST_DEBUG", QUANT_INSTANTIATE_HEURISTIC___debug, 3); 47 48val QUANT_INSTANTIATE_HEURISTIC___debug_depth = ref 5; 49val _ = register_trace("QUANT_INST_DEBUG_DEPTH", QUANT_INSTANTIATE_HEURISTIC___debug_depth, 2000); 50 51val QUANT_INSTANTIATE_HEURISTIC___print_term_length = ref 2000; 52val _ = register_trace("QUANT_INST___print_term_length", QUANT_INSTANTIATE_HEURISTIC___print_term_length, 2000); 53 54 55(******************************************************* 56 * Some general auxiliary functions 57 *******************************************************) 58 59local 60 val my_type_subst = [alpha |-> gen_tyvar(), beta |-> gen_tyvar(), gamma |-> gen_tyvar(), delta |-> gen_tyvar(), 61 ``:'e`` |-> gen_tyvar(), ``:'f`` |-> gen_tyvar(), ``:'g`` |-> gen_tyvar(), ``:'h`` |-> gen_tyvar()] 62in 63 fun intro_fresh_ty_vars thm = INST_TYPE my_type_subst thm 64end 65 66fun mapPartialAcc f acc [] = acc 67 | mapPartialAcc f acc (x::xs) = 68 let 69 val r_opt = f x; 70 val acc' = if isSome r_opt then (valOf r_opt)::acc else acc; 71 in 72 mapPartialAcc f acc' xs 73 end; 74 75fun mapPartial f = mapPartialAcc f []; 76 77fun say_HOL_WARNING funname warning = 78 Feedback.HOL_WARNING "quantHeuristicsBasicLib" funname warning 79 80fun genvar_RULE thm = 81let 82 val fvL = free_vars (concl thm) 83 val s = map (fn v => (v |-> genvar (type_of v))) fvL 84 85 val type_vL = type_vars_in_term (concl thm) 86 val ts = map (fn v => (v |-> gen_tyvar ())) type_vL 87in 88 INST_TYPE ts (INST s thm) 89end; 90 91 92 93(******************************************************* 94 * Datatype for guesses and some general functions on 95 * these guesses 96 *******************************************************) 97 98 99(*Heuristics can come up with guessed instantiations 100 of a universal or existential quantifier for different reasons. 101 The datatype guess captures these guesses and the reason. 102 103 There are 6 types of guesses with corresponding arguments as 104 defined in quantHeuristicsScript. 105*) 106 107datatype guess_type = 108 gty_exists_point 109| gty_forall_point 110| gty_exists 111| gty_forall 112| gty_exists_gap 113| gty_forall_gap 114 115 116fun qh_mk_const n = 117 prim_mk_const {Name = n, Thy = "quantHeuristics"} 118 119val GUESS_FORALL_tm = qh_mk_const "GUESS_FORALL"; 120val GUESS_FORALL_GAP_tm = qh_mk_const "GUESS_FORALL_GAP"; 121val GUESS_FORALL_POINT_tm = qh_mk_const "GUESS_FORALL_POINT"; 122val GUESS_EXISTS_tm = qh_mk_const "GUESS_EXISTS"; 123val GUESS_EXISTS_POINT_tm = qh_mk_const "GUESS_EXISTS_POINT"; 124val GUESS_EXISTS_GAP_tm = qh_mk_const "GUESS_EXISTS_GAP"; 125 126fun guess_type2term gty_exists_point = GUESS_EXISTS_POINT_tm 127 | guess_type2term gty_forall_point = GUESS_FORALL_POINT_tm 128 | guess_type2term gty_exists = GUESS_EXISTS_tm 129 | guess_type2term gty_forall = GUESS_FORALL_tm 130 | guess_type2term gty_exists_gap = GUESS_EXISTS_GAP_tm 131 | guess_type2term gty_forall_gap = GUESS_FORALL_GAP_tm 132 133fun guess_type2string gty_exists_point = "guess_exists_point" 134 | guess_type2string gty_forall_point = "guess_forall_point" 135 | guess_type2string gty_exists = "guess_exists" 136 | guess_type2string gty_forall = "guess_forall" 137 | guess_type2string gty_exists_gap = "guess_exists_gap" 138 | guess_type2string gty_forall_gap = "guess_forall_gap"; 139 140fun guess_term2type gtm = 141 if (same_const gtm GUESS_EXISTS_POINT_tm) then gty_exists_point else 142 if (same_const gtm GUESS_FORALL_POINT_tm) then gty_forall_point else 143 if (same_const gtm GUESS_EXISTS_tm) then gty_exists else 144 if (same_const gtm GUESS_FORALL_tm) then gty_forall else 145 if (same_const gtm GUESS_EXISTS_GAP_tm) then gty_exists_gap else 146 if (same_const gtm GUESS_FORALL_GAP_tm) then gty_forall_gap else 147 Feedback.fail(); 148 149 150(* 151 All guesses consist of an instatiation and a list of free variables in this instatiation. There might also be 152 a justification that might have been proved. The justification of a guess consists of a guess-type accompanied by either a theorem 153 or a term. The term/theorem has to correspond to the ML-level information. 154 Depending on the guess-type, it has to be a single guess as defined in 155 quantHeuristicsScript (either GUESS_FORALL_POINT, GUESS_EXISTS_POINT, GUESS_EXISTS, GUESS_FORALL, GUESS_EXISTS_GAP or GUESS_FORALL_GAP). 156 The list of free variables is mainly used to record names. In the guess theorem/term, only a single variable is allowed. 157 A simple example is 158 159 guess_term 160 (gty_forall_point, 161 ``SUC (y :num) + (z :num)``, 162 [``(y :num)``, ``(z :num)``], 163 ``GUESS_EXISTS_POINT (\(x :num # num). SUC (FST x) + SND x) 164 (\(x :num). (P :num -> bool) x)``) 165 166 Look at the ML-function check_guess for a more formal description, please. 167*) 168 169datatype guess = 170 (* Oracle Guesses *) 171 guess_general of term * term list 172 | (* formally justified guesses *) 173 guess_thm of guess_type * term * term list * thm 174 | (* informally justified guesses *) 175 guess_term of guess_type * term * term list * term 176 177 178(* Some auxiliary functions to check type of guesses and destruct them. *) 179fun is_guess_general (guess_general _) = true 180 | is_guess_general _ = false; 181 182fun is_guess_thm gty (guess_thm (gty2, _, _, _)) = (gty = gty2) 183 | is_guess_thm gty _ = false; 184 185fun is_guess_term gty (guess_term (gty2, _, _, _)) = (gty = gty2) 186 | is_guess_term gty _ = false; 187 188fun is_guess gty (guess_term (gty2, _, _, _)) = (gty = gty2) 189 | is_guess gty (guess_thm (gty2, _, _, _)) = (gty = gty2) 190 | is_guess gty _ = false; 191 192fun guess_extract (guess_general (i,fvL)) = (i,fvL) 193 | guess_extract (guess_thm (_,i,fvL,_)) = (i,fvL) 194 | guess_extract (guess_term (_,i,fvL,_)) = (i,fvL) 195 196fun guess_extract_thm (guess_thm (ty,i,fvL,thm)) = (ty,i,fvL,thm,true) 197 | guess_extract_thm (guess_term (ty,i,fvL,tm)) = (ty,i,fvL,ASSUME tm, false) 198 | guess_extract_thm _ = Feedback.fail(); 199 200fun guess2term (guess_general (_,_)) = NONE 201 | guess2term (guess_thm (_,_,_,thm)) = SOME (concl thm) 202 | guess2term (guess_term (_,_,_,tm)) = SOME tm 203 204fun guess2thm (guess_thm (_,_,_,thm)) = (true, thm) 205 | guess2thm (guess_term (_,_,_,tm)) = (false, ASSUME tm) 206 | guess2thm _ = Feedback.fail(); 207 208fun guess2thm_opt (guess_thm (_,_,_,thm)) = SOME thm 209 | guess2thm_opt _ = NONE 210 211fun guess_extract_type (guess_general (i,fvL)) = NONE 212 | guess_extract_type (guess_thm (ty,i,fvL,_)) = SOME ty 213 | guess_extract_type (guess_term (ty,i,fvL,_)) = SOME ty 214 215fun guess_has_thm (guess_thm _) = true 216 | guess_has_thm _ = false; 217 218fun guess_has_no_free_vars guess = 219 null (#2 (guess_extract guess)); 220 221fun guess_has_thm_no_free_vars guess = 222 guess_has_thm guess andalso 223 guess_has_no_free_vars guess; 224 225fun guess_thm_to_guess thm_ok ifvL_opt thm = 226let 227 val (gtm, args) = strip_comb (concl thm); 228 val _ = if (length args = 2) then () else Feedback.fail(); 229 val gty = guess_term2type gtm; 230 val (i, fvL) = if isSome ifvL_opt then valOf ifvL_opt else 231 let 232 val qi_t = el 1 args 233 val (_, qi_t) = if is_abs qi_t then (NONE,qi_t) else 234 let 235 val fvTy = hd (snd (dest_type (type_of qi_t))); 236 val fv = genvar fvTy; 237 val qi_t' = mk_abs (fv, mk_comb(qi_t,fv)); 238 in 239 (SOME (GSYM (ETA_CONV qi_t')), qi_t') 240 end; 241 val (fv, i) = dest_abs qi_t; 242 in 243 (i, [fv]) 244 end; 245in 246 if thm_ok then 247 guess_thm (gty, i, fvL, thm) 248 else 249 guess_term (gty, i, fvL, concl thm) 250end; 251 252fun dest_guess_tm t = 253let 254 val (gtm, args) = strip_comb t; 255 val _ = if (length args = 2) then () else Feedback.fail(); 256 val gty = guess_term2type gtm; 257 val (v_t, t_t) = dest_abs (el 2 args) 258in 259 (gty, (el 1 args), v_t, t_t) 260end; 261 262val is_guess_tm = can dest_guess_tm 263 264 265(******************************************************* 266 * Creating guesses in various ways 267 *******************************************************) 268 269(* 270val v = ``x:num`` 271val t = ``(P (x:num)):bool`` 272val i = ``SUC y + z`` 273val fvL = [``y:num``, ``z:num``] 274val base = GUESS_EXISTS_POINT_tm 275val gty = gty_forall_point 276*) 277val unit_ty = Type `:unit`; 278 279fun make_guess_thm_term gty v t i fvL = 280let 281 val base = guess_type2term gty; 282 val vt = mk_abs (v, t); 283 val fvL = if null fvL then [genvar unit_ty] else fvL; 284 val ip = pairLib.mk_pabs (pairLib.list_mk_pair fvL, i); 285 val ip_thm = (pairTools.PABS_ELIM_CONV ip) handle UNCHANGED => REFL ip; 286in 287 list_mk_icomb (base, [rhs (concl ip_thm), vt]) 288end; 289 290 291(* This is the prefered way to generate a well-formed guess *) 292fun mk_guess gty v t i fvL = 293 guess_term (gty, i, fvL, make_guess_thm_term gty v t i fvL) 294 295fun mk_guess_opt NONE v t i fvL = guess_general(i, fvL) 296 | mk_guess_opt (SOME gty) v t i fvL = mk_guess gty v t i fvL 297 298 299(* Given a guess_term the function is applied to prove the term. *) 300fun make_set_guess_thm (guess_term(ty, i, fvL, tm)) proofConv = 301 guess_thm (ty, i, fvL, proofConv tm) 302 | make_set_guess_thm guess _ = guess 303 304fun guess_remove_thm v t (guess_thm(ty, i, fvL, thm)) = 305 mk_guess ty v t i fvL 306 | guess_remove_thm v t (guess_term(ty, i, fvL, tm)) = 307 mk_guess ty v t i fvL 308 | guess_remove_thm _ _ guess = guess; 309 310fun guess_thm2term (guess_thm(ty, i, fvL, thm)) = 311 guess_term (ty, i, fvL, concl thm) 312 | guess_thm2term guess = guess; 313 314 315(* A dummy version that just uses mk_thm. *) 316fun make_set_guess_thm___dummy guess = 317 ((say_HOL_WARNING "make_set_guess_thm_opt___dummy" 318 "mk_thm was used to create a guess"); 319 make_set_guess_thm guess (fn x => mk_thm ([], x))); 320 321fun make_guess___dummy gty v t i fvL = 322 make_set_guess_thm___dummy (mk_guess gty v t i fvL); 323 324(* A dummy version that just uses assume. *) 325fun make_set_guess_thm___assume guess = 326 make_set_guess_thm guess ASSUME; 327 328fun make_guess___assume gty v t i fvL = 329 make_set_guess_thm___assume (mk_guess gty v t i fvL) 330 331 332(* A simple version that uses the simplifier. Surprisingly, this is often sufficient. *) 333fun make_set_guess_thm___simple guess = 334 make_set_guess_thm guess (fn x => EQT_ELIM 335 (SIMP_CONV std_ss [GUESS_REWRITES] x)) 336 337fun make_guess___simple gty v t i fvL = 338 make_set_guess_thm___simple (mk_guess gty v t i fvL) 339 340 341(* A simple version that uses rewrites. *) 342fun GUESS_REWRITE_PROVE t = 343let 344 open metisLib 345 val thm = SIMP_CONV std_ss [GUESS_REWRITES] t handle UNCHANGED => REFL t; 346 val t2 = rhs (concl thm) 347 val thm2 = if t2 = T then TRUTH else METIS_PROVE [] t2; 348in 349 EQ_MP (GSYM thm) thm2 350end; 351 352 353fun make_guess___rewrite gty v t i fvL = 354 make_set_guess_thm (mk_guess gty v t i fvL) GUESS_REWRITE_PROVE 355 356 357(* Other stuff *) 358fun term_list_to_string [] = "" 359 | term_list_to_string [t] = (term_to_string t) 360 | term_list_to_string (t1::t2::ts) = 361 (term_to_string t1)^", "^(term_list_to_string (t2::ts)) 362 363fun guess_to_string show_thm (guess_general (i,fvL)) = 364 "guess_general (``"^(term_to_string i)^"``, ["^(term_list_to_string fvL)^"])" 365 | guess_to_string show_thm (guess_thm (gty, i,fvL,thm)) = 366 (guess_type2string gty) ^ " (``"^(term_to_string i)^"``, ["^(term_list_to_string fvL)^"], "^ 367 (if show_thm then thm_to_string thm else "X")^")" 368 | guess_to_string show_thm (guess_term (gty, i,fvL,tm)) = 369 (guess_type2string gty) ^ " (``"^(term_to_string i)^"``, ["^(term_list_to_string fvL)^"], ``"^ 370 (if show_thm then term_to_string tm else "-")^"``)"; 371 372 373(* Checking whether a guess is well-formed and if not try to correct it automatically. *) 374fun check_guess v t (guess_general _) = true 375 | check_guess v t guess = 376 let 377 val (i,fvL) = guess_extract guess; 378 val ty = valOf (guess_extract_type guess); 379 val thm_term2 = valOf (guess2term guess) 380 val fvL_t = free_vars t; 381 val fvL_i = free_vars i; 382 val thm_term = make_guess_thm_term ty v t i fvL 383 in 384 (type_of v = type_of i) andalso 385 (all (fn x => (mem x fvL_i)) fvL) andalso 386 (aconv thm_term thm_term2) 387 end handle HOL_ERR _ => false; 388 389 390fun correct_guess v t guess = 391 if (check_guess v t guess) then SOME guess else 392 let 393 val guess2 = guess_remove_thm v t guess handle HOL_ERR _ => guess; 394 val still_error = not (check_guess v t guess2); 395 396 val error_msg = if still_error then 397 ("Error in guess: "^(guess_to_string true guess)) else 398 ("Malformed theorem in guess:\n"^(guess_to_string true guess)^ 399 "\nTheorem should be of form ``"^ 400 (term_to_string (valOf (guess2term guess2))) ^"``.") 401 val _ = say_HOL_WARNING "correct_guess" error_msg 402 in 403 if still_error then NONE else SOME guess2 404 end; 405 406fun correct_guess_list v t = mapPartial (correct_guess v t) 407 408 409 410(******************************************************* 411 * Try to weaken guesses to get guess_exists or guess_forall 412 *******************************************************) 413 414local 415 416(* 417val t = ``(P (x:num)):bool`` 418val i = ``(XXX (y:num) (z:num)):num``; 419val fvL = [``y:num``,``z:num``] 420val v = ``x:num``; 421 422val guess = make_set_guess_thm_opt___dummy v t (guess_forall_gap (i, fvL, NONE)); 423val (_,_,thm_opt) = guess_extract guess; 424val thm = valOf thm_opt 425 426*) 427 428fun guess_type_weaken gty_exists_point = gty_exists 429 | guess_type_weaken gty_forall_point = gty_forall 430 | guess_type_weaken gty_exists_gap = gty_exists 431 | guess_type_weaken gty_forall_gap = gty_forall 432 | guess_type_weaken gty_exists = gty_exists 433 | guess_type_weaken gty_forall = gty_forall 434 435val [weaken_thm_forall_gap, weaken_thm_forall_point, 436 weaken_thm_exists_point, weaken_thm_exists_gap] = BODY_CONJUNCTS GUESSES_WEAKEN_THM 437 438fun guess_weaken_thm gty_exists_point = weaken_thm_exists_point 439 | guess_weaken_thm gty_forall_point = weaken_thm_forall_point 440 | guess_weaken_thm gty_exists_gap = weaken_thm_exists_gap 441 | guess_weaken_thm gty_forall_gap = weaken_thm_forall_gap 442 | guess_weaken_thm _ = Feedback.fail(); 443 444in 445 446fun guess_weaken (guess_general (i, fvL)) = guess_general (i,fvL) 447 | guess_weaken (guess_term (gty, i, fvL, tm)) = 448 if (gty = gty_exists) orelse (gty = gty_forall) then 449 (guess_term (gty, i, fvL, tm)) 450 else 451 let 452 val gty' = guess_type_weaken gty; 453 val b' = guess_type2term gty' 454 val (_, args) = strip_comb tm; 455 val tm' = list_mk_icomb (b', args); 456 in 457 (guess_term (gty', i, fvL, tm')) 458 end 459 | guess_weaken (guess_thm (gty, i, fvL, thm)) = 460 if (gty = gty_exists) orelse (gty = gty_forall) then 461 (guess_thm (gty, i, fvL, thm)) 462 else 463 let 464 val gty' = guess_type_weaken gty; 465 val thm' = HO_MATCH_MP (guess_weaken_thm gty) thm; 466 in 467 guess_thm(gty', i, fvL, thm') 468 end; 469 470end 471 472 473(******************************************************* 474 * Collections of guesses 475 * 476 * There are usually many guesses around. Therefore, they are 477 * collected in one datastructure, that separates them after their 478 * type. Moreover, this datastructures also records rewrite theorems 479 * that were used to come up with these guesses. These rewrites might 480 * then be used later for simplification. 481 ********************************************************) 482 483type guess_collection = 484 {rewrites : thm list, 485 general : guess list, 486 exists_point : guess list, 487 forall_point : guess list, 488 exists : guess list, 489 forall : guess list, 490 exists_gap : guess list, 491 forall_gap : guess list} 492 493fun guess_collection_guess_type gty_exists_point = (#exists_point:guess_collection -> guess list) 494 | guess_collection_guess_type gty_forall_point = #forall_point 495 | guess_collection_guess_type gty_exists = #exists 496 | guess_collection_guess_type gty_forall = #forall 497 | guess_collection_guess_type gty_exists_gap = #exists_gap 498 | guess_collection_guess_type gty_forall_gap = #forall_gap 499 500val empty_guess_collection = 501 {rewrites = [], 502 general = [], 503 exists_point = [], 504 forall_point = [], 505 exists = [], 506 forall = [], 507 exists_gap = [], 508 forall_gap = []}:guess_collection 509 510fun is_empty_guess_collection (gc:guess_collection) = 511 (null (#rewrites gc)) andalso 512 (null (#general gc)) andalso 513 (null (#exists_point gc)) andalso 514 (null (#forall_point gc)) andalso 515 (null (#exists gc)) andalso 516 (null (#forall gc)) andalso 517 (null (#exists_gap gc)) andalso 518 (null (#forall_gap gc)) 519 520 521fun guess_collection_append (c1:guess_collection) (c2:guess_collection) = 522 {rewrites = append (#rewrites c1) (#rewrites c2), 523 general = append (#general c1) (#general c2), 524 exists_point = append (#exists_point c1) (#exists_point c2), 525 forall_point = append (#forall_point c1) (#forall_point c2), 526 exists = append (#exists c1) (#exists c2), 527 forall = append (#forall c1) (#forall c2), 528 exists_gap = append (#exists_gap c1) (#exists_gap c2), 529 forall_gap = append (#forall_gap c1) (#forall_gap c2)}:guess_collection 530 531 532fun guess_collection_flatten [] = empty_guess_collection 533 | guess_collection_flatten (NONE::L) = guess_collection_flatten L 534 | guess_collection_flatten ((SOME gc)::L) = 535 guess_collection_append gc (guess_collection_flatten L); 536 537 538 539(* Create a guess-collection from a list of rewrites and a list of guesses by 540 sorting the guesses in the right bucket. *) 541local 542fun guess_list2collection___int gp [] = gp 543 | guess_list2collection___int (g1,g3,g4,g5,g6,g7,g8) (guess::gL) = 544 let 545 val g1 = if (is_guess_general guess) then guess::g1 else g1; 546 val g3 = if (is_guess gty_exists_point guess) then guess::g3 else g3; 547 val g4 = if (is_guess gty_forall_point guess) then guess::g4 else g4; 548 val g5 = if (is_guess gty_exists guess) then guess::g5 else g5; 549 val g6 = if (is_guess gty_forall guess) then guess::g6 else g6; 550 val g7 = if (is_guess gty_exists_gap guess) then guess::g7 else g7; 551 val g8 = if (is_guess gty_forall_gap guess) then guess::g8 else g8; 552 in 553 guess_list2collection___int (g1,g3,g4,g5,g6,g7,g8) gL 554 end; 555in 556 fun guess_list2collection (rewL, gL) = 557 let 558 val (g1,g3,g4,g5,g6,g7,g8) = guess_list2collection___int ([],[],[],[],[],[],[]) gL; 559 in 560 {rewrites = rewL, general = g1, exists_point = g3, forall_point = g4, exists = g5, 561 forall = g6, exists_gap = g7, forall_gap = g8}:guess_collection 562 end; 563 564end; 565 566 567fun guess_collection2list (gc:guess_collection) = 568 (#rewrites gc, 569 flatten [#general gc, #exists_point gc, #forall_point gc, #forall gc, 570 #exists gc, #forall_gap gc, #exists_gap gc]); 571 572 573(* 574val guess = hd (#exists gc) 575val gc_ref = ref [] 576val gc = hd (!gc_ref) 577*) 578 579fun correct_guess_collection v t (gc:guess_collection) = 580 if (!QUANT_INSTANTIATE_HEURISTIC___debug > 0) then 581 let 582 val gc = 583 {rewrites = #rewrites gc, 584 general = correct_guess_list v t (#general gc), 585 exists_point = correct_guess_list v t (#exists_point gc), 586 forall_point = correct_guess_list v t (#forall_point gc), 587 forall = correct_guess_list v t (#forall gc), 588 exists = correct_guess_list v t (#exists gc), 589 forall_gap = correct_guess_list v t (#forall_gap gc), 590 exists_gap = correct_guess_list v t (#exists_gap gc)}:guess_collection; 591 592 val _ = if (all (is_guess gty_exists_point) (#exists_point gc)) andalso 593 (all (is_guess gty_forall_point) (#forall_point gc)) andalso 594 (all is_guess_general (#general gc)) andalso 595 (all (is_guess gty_forall) (#forall gc)) andalso 596 (all (is_guess gty_exists) (#exists gc)) andalso 597 (all (is_guess gty_forall_gap) (#forall_gap gc)) andalso 598 (all (is_guess gty_exists_gap) (#exists_gap gc)) then () else 599 say_HOL_WARNING "correct_guess_collection" "Guess-collection-invariant violated!" 600 601 in 602 gc 603 end else gc; 604 605fun guess_collection___get_exists_weaken (c:guess_collection) = 606 append (#exists_point c) (append (#exists c) (#exists_gap c)); 607 608fun guess_collection___get_forall_weaken (c:guess_collection) = 609 append (#forall_point c) (append (#forall c) (#forall_gap c)); 610 611 612fun filter_guess inst_filterL v t guess = 613 let val (i, fvL) = guess_extract guess in 614 if (all (fn f => f (v:term) (t:term) i fvL) inst_filterL) then SOME guess else NONE 615 handle HOL_ERR _ => NONE 616 end; 617 618fun filter_guess_list inst_filterL v t = mapPartial (filter_guess inst_filterL v t) 619 620fun filter_guess_collection inst_filterL v t (gc:guess_collection) = 621 if (null inst_filterL) then gc else 622 {rewrites = #rewrites gc, 623 general = filter_guess_list inst_filterL v t (#general gc), 624 exists_point = filter_guess_list inst_filterL v t (#exists_point gc), 625 forall_point = filter_guess_list inst_filterL v t (#forall_point gc), 626 forall = filter_guess_list inst_filterL v t (#forall gc), 627 exists = filter_guess_list inst_filterL v t (#exists gc), 628 forall_gap = filter_guess_list inst_filterL v t (#forall_gap gc), 629 exists_gap = filter_guess_list inst_filterL v t (#exists_gap gc)}:guess_collection; 630 631 632(******************************************************* 633 * Cleaning a guess collecion, i.e. removing duplicate 634 * guesses or guesses that can be easily derived by weakening 635 * stronger ones. 636 *******************************************************) 637 638local 639 640fun elim_double_guesses_int r [] = r 641 | elim_double_guesses_int r ([]::gLL) = 642 elim_double_guesses_int r gLL 643 | elim_double_guesses_int r ((((i, fvL),g)::gL)::gLL) = 644let 645 val already_present = (fvL = [i]) orelse 646 exists (fn ((i', fvL'), _) => (i = i') andalso (fvL = fvL')) r 647 val r' = if already_present then r else ((i, fvL), g)::r 648in 649 elim_double_guesses_int r' (gL::gLL) 650end; 651 652fun elim_double_guesses gL = 653let 654 val gL' = map (fn g => (guess_extract g, g)) gL 655 val (gL1, gL2) = partition (fn ((_,_),g) => 656 guess_has_thm g) gL'; 657in 658 map snd (elim_double_guesses_int [] [gL1, gL2]) 659end; 660 661 662fun clean_guess (guess_thm (gty, i, fvL, thm)) = 663let 664 val i' = rand (rator (concl thm)); 665 val thm' = if is_abs i' then thm else 666 let 667 val ty = hd (snd (dest_type (type_of i'))) 668 val v = genvar ty 669 val xthm = ETA_CONV (mk_abs(v, mk_comb (i', v))); 670 in 671 (CONV_RULE (RATOR_CONV (RAND_CONV (K (GSYM xthm)))) thm) 672 end 673in 674 guess_thm (gty, i, fvL, thm') 675end 676| clean_guess (guess_term (gty, i, fvL, tm)) = 677 let 678 val (b, args) = strip_comb tm; 679 val i' = hd args; 680 val i' = if is_abs i' then i' else 681 let 682 val ty = hd (snd (dest_type (type_of i'))) 683 val v = genvar ty 684 in 685 mk_abs (v, mk_comb (i', v)) 686 end 687 val tm' = list_mk_comb (b, [i', el 2 args]) 688 in 689 guess_term (gty, i, fvL, tm') 690 end 691| clean_guess guess = guess; 692 693 694fun elim_clean_guesses gL = 695 map clean_guess (elim_double_guesses gL); 696 697in 698 699fun guess_collection_clean (c:guess_collection) = 700 {rewrites = #rewrites c, 701 general = #general c, 702 exists_point = elim_clean_guesses (#exists_point c), 703 forall_point = elim_clean_guesses (#forall_point c), 704 exists = elim_clean_guesses (map guess_weaken (guess_collection___get_exists_weaken c)), 705 forall = elim_clean_guesses (map guess_weaken (guess_collection___get_forall_weaken c)), 706 exists_gap = elim_clean_guesses (#exists_gap c), 707 forall_gap = elim_clean_guesses (#forall_gap c)}: guess_collection 708 709end; 710 711 712 713 714 715 716 717(******************************************************* 718 * 719 * Heuristics for the common boolean operations 720 * 721 *******************************************************) 722 723(* A basic quantifier heuristics gets two arguments v and t. 724 It then tries to find guesses for "\v. t". *) 725type quant_heuristic_base = term -> term -> guess_collection; 726 727(* Often quantifier heuristics need to get guesses for subterms. 728 Therefore, they get an additional argument that can be used 729 as a system callback to get guesses for subterms. *) 730type quant_heuristic = quant_heuristic_base -> quant_heuristic_base; 731 732(* If a heuristic does not find any guesses, this exception is 733 thrown *) 734exception QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 735 736 737(* Dummy system callbacks that are handy for debugging. 738 739fun dummy_term_sys v t = 740let 741 val i = mk_var ("i", type_of v); 742 val fvL = []; 743in 744 {rewrites = [], 745 general = [], 746 exists_point = [mk_guess gty_exists_point v t i fvL], 747 forall_point = [mk_guess gty_forall_point v t i fvL], 748 exists = [mk_guess gty_exists v t i fvL], 749 forall = [mk_guess gty_forall v t i fvL], 750 exists_gap = [mk_guess gty_exists_gap v t i fvL], 751 forall_gap = [mk_guess gty_forall_gap v t i fvL]} 752end; 753 754fun dummy_sys v t = 755let 756 val i = mk_var ("i", type_of v); 757 val fvL = []; 758in 759 {rewrites = [], 760 general = [], 761 exists_point = [make_guess___dummy gty_exists_point v t i fvL], 762 forall_point = [make_guess___dummy gty_forall_point v t i fvL], 763 exists = [make_guess___dummy gty_exists v t i fvL], 764 forall = [make_guess___dummy gty_forall v t i fvL], 765 exists_gap = [make_guess___dummy gty_exists_gap v t i fvL], 766 forall_gap = [make_guess___dummy gty_forall_gap v t i fvL]} 767end; 768 769*) 770 771 772(********************************* 773 * Simple heuristic for Booleans 774 *********************************) 775 776(* 777 val t = ``x:bool`` 778 val v = t 779*) 780 781fun QUANT_INSTANTIATE_HEURISTIC___BOOL sys v t = 782let 783 val _ = if (aconv v t) then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 784in 785 {rewrites = [], 786 general = [], 787 exists_point = [make_guess___simple gty_exists_point v t T []], 788 forall_point = [make_guess___simple gty_forall_point v t F []], 789 forall = [], 790 exists = [], 791 forall_gap = [make_guess___simple gty_forall_gap v t F []], 792 exists_gap = [make_guess___simple gty_exists_gap v t T []]} 793end; 794 795 796(********************************* 797 * Heuristic for equations 798 *********************************) 799 800(* 801val t = ``7 + y + z = (x:num)``; 802val t = ``x:'a = f y``; 803val t = ``f y = x:'a``; 804val t = ``x + y = x + z``; 805val v = ``x:'a`` 806val t = ``(f (y':'b)):'a = f y`` 807val v = ``y':'b`` 808val sys = dummy_sys 809*) 810 811 812fun QUANT_INSTANTIATE_HEURISTIC___EQUATION sys v t = 813let 814 val _ = if (is_eq t) then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 815 val (l,r) = dest_eq t; 816 817 val (turn,top,i,s) = if (l = v) then (false, true, r,r) else 818 if (r = v) then (true, true, l,l) else 819 (false, false, match_term_var v l r, r) handle HOL_ERR _ => 820 (true, false, match_term_var v r l, l) handle HOL_ERR _ => 821 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 822 823 val _ = if (free_in v i) then Feedback.fail () else (); 824 val u_genvar = genvar unit_ty; 825 826 val g_exists_pointL = let 827 val v_l = mk_abs (v, l); 828 val v_r = mk_abs (v, r); 829 val g_exists_point_thm = ISPECL [i, v_l, v_r] (intro_fresh_ty_vars GUESS_RULES_EQUATION_EXISTS_POINT) 830 val g_exists_point_thm2 = CONV_RULE ( 831 RATOR_CONV (RAND_CONV (BINOP_CONV BETA_CONV)) THENC 832 RAND_CONV (RAND_CONV (ALPHA_CONV v THENC (ABS_CONV ((BINOP_CONV BETA_CONV)))))) g_exists_point_thm 833 val pre = (lhs o fst o dest_imp o concl) g_exists_point_thm2; 834 val g_exists_point_thm3 = MP g_exists_point_thm2 (REFL pre) 835 val g_exists_point_thm4 = CONV_RULE (RATOR_CONV (RAND_CONV (ALPHA_CONV u_genvar))) g_exists_point_thm3 836 in 837 [guess_thm (gty_exists_point, i, [], g_exists_point_thm4)] 838 end 839 840 val g_exists_gapL = if not top then [] else let 841 val g_thm0 = ISPEC i GUESS_RULES_EQUATION_EXISTS_GAP; 842 val g_thm1 = if turn then CONV_RULE (RAND_CONV (ABS_CONV SYM_CONV)) g_thm0 else g_thm0 843 val g_thm2 = CONV_RULE (RAND_CONV (ALPHA_CONV v)) g_thm1 844 val g_thm3 = CONV_RULE (RATOR_CONV (RAND_CONV (ALPHA_CONV u_genvar))) g_thm2 845 in 846 [guess_thm (gty_exists_gap, i, [], g_thm3)] 847 end 848in 849 {rewrites = [], 850 general = [], 851 exists_point = g_exists_pointL, 852 forall_point = [], 853 forall = [], 854 exists = [], 855 forall_gap = [], 856 exists_gap = g_exists_gapL}:guess_collection 857end; 858 859 860(********************************************* 861 * Heuristic for monochotomies and dichotomies 862 *********************************************) 863 864fun prefix_free_vars (prefix, fvL, i) = 865let 866 val fvL' = map (fn x => let 867 val (x_name, x_ty) = dest_var x; 868 val x'_name = prefix ^ "_"^x_name; 869 in 870 (mk_var (x'_name, x_ty)) 871 end) fvL 872 val i' = subst (map (fn (x,x') => (x |-> x')) (zip fvL fvL')) i; 873in 874 (fvL', i') 875end; 876 877(* 878 val t = ``l:'a list = []``; 879 val v = ``l:'a list``; 880 val fv = []; 881 val sys = NONE; 882 val thm = TypeBase.nchotomy_of ``:'a list``; 883*) 884 885fun QUANT_INSTANTIATE_HEURISTIC___EQUATION_two_cases thm sys v t = 886let 887 val _ = if is_eq t then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 888 val (l,r) = dest_eq t; 889 890 val (i,turn) = if (l = v) then (r,false) else 891 if (r = v) then (l,true) else 892 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 893 894 val thm' = ISPEC v (intro_fresh_ty_vars thm); 895 val (eeq1,eeq2) = dest_disj (concl thm'); 896 val left_right_flag = if ((is_eq eeq1) andalso (lhs eeq1 = v) andalso (rhs eeq1 = i)) then false else 897 if ((is_eq eeq2) andalso (lhs eeq2 = v) andalso (rhs eeq2 = i)) then true else 898 Feedback.fail (); 899 val (eeq1,eeq2,thm2) = if left_right_flag then 900 (eeq2, eeq1, CONV_RULE (PART_MATCH lhs DISJ_COMM) thm') else 901 (eeq1, eeq2, thm') 902 903 val (fvL, eeq2b) = strip_exists eeq2; 904 val (v',ni) = dest_eq eeq2b; 905 val _ = if (v = v') then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 906 907 val v_name = (fst o dest_var) v 908 val (fvL', ni') = prefix_free_vars (v_name, fvL, ni); 909 910 val thm3 = GEN v (CONV_RULE (RAND_CONV (INTRO_TUPLED_QUANT_CONV THENC 911 RAND_CONV PABS_ELIM_CONV)) thm2) 912 val g_thm0 = HO_MATCH_MP GUESS_RULES_TWO_CASES thm3 913 val g_thm = if not turn then g_thm0 else 914 CONV_RULE (RAND_CONV (ABS_CONV SYM_CONV)) g_thm0 915 916 val guess = guess_thm(gty_forall_gap, ni', fvL', g_thm); 917in 918 {rewrites = [], 919 general = [], 920 exists_point = [], 921 forall_point = [], 922 forall = [], 923 exists = [], 924 forall_gap = [guess], 925 exists_gap = []}:guess_collection 926end handle UNCHANGED => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 927 | HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 928 929(* 930val v = ``X:('a # 'b)`` 931val t = ``(P (X:('a # 'b))):bool`` 932val thm = TypeBase.nchotomy_of (type_of v) 933val sys = dummy_sys 934val thm = GEN v thm0 935*) 936 937fun QUANT_INSTANTIATE_HEURISTIC___one_case thm sys v t = 938let 939 val (vars, v_eq_i) = (strip_exists o snd o dest_forall o concl) thm; 940 val (_,i) = dest_eq v_eq_i 941 942 val v_name = (fst o dest_var) v 943 val (vars', i') = prefix_free_vars (v_name, vars, i); 944 945 val thm2 = CONV_RULE (QUANT_CONV ((INTRO_TUPLED_QUANT_CONV THENC 946 RAND_CONV PABS_ELIM_CONV))) thm 947 948 val g_thm0 = ISPEC (mk_abs (v, t)) 949 (HO_MATCH_MP GUESS_RULES_ONE_CASE___FORALL_GAP thm2) 950 val g_thm1 = ISPEC (mk_abs (v, t)) 951 (HO_MATCH_MP GUESS_RULES_ONE_CASE___EXISTS_GAP thm2) 952 953 val g0 = guess_thm (gty_forall_gap, i',vars', g_thm0); 954 val g1 = guess_thm (gty_exists_gap, i',vars', g_thm1); 955 956in 957 {rewrites = [], 958 general = [], 959 exists_point = [], 960 forall_point = [], 961 forall = [], 962 exists = [], 963 forall_gap = [g0], 964 exists_gap = [g1]}:guess_collection 965end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 966 967 968local 969 fun QUANT_INSTANTIATE_HEURISTIC___FAIL sys v t = 970 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 971 972 fun dest_ex_eq tt = 973 let 974 val (vars, eq) = strip_exists tt; 975 val (l, r) = dest_eq eq; 976 in 977 (vars, l, r) 978 end; 979 980 fun is_sing_case_thm thm = 981 let 982 val (v, b) = dest_forall (concl thm); 983 val (_, l, _) = dest_ex_eq b; 984 val _ = (if (aconv v l) then () else Feedback.fail()) 985 in 986 true 987 end handle HOL_ERR _ => false; 988 989 fun is_double_case_thm thm = 990 let 991 val (v, b) = dest_forall (concl thm); 992 val (b1, b2) = dest_disj b; 993 val (_, l1, _) = dest_ex_eq b1; 994 val (_, l2, _) = dest_ex_eq b2; 995 val _ = (if (aconv v l1) then () else Feedback.fail()) 996 val _ = (if (aconv v l2) then () else Feedback.fail()) 997 in 998 true 999 end handle HOL_ERR _ => false; 1000 1001 fun is_disj_case_thm thm = 1002 let 1003 val (v, b) = dest_forall (concl thm); 1004 val (b1, b2) = dest_disj b; 1005 in 1006 not (is_double_case_thm thm) 1007 end handle HOL_ERR _ => false; 1008 1009in 1010 fun QUANT_INSTANTIATE_HEURISTIC___cases thm = 1011 let 1012 in 1013 if is_sing_case_thm thm then 1014 QUANT_INSTANTIATE_HEURISTIC___one_case thm 1015 else if is_double_case_thm thm then 1016 QUANT_INSTANTIATE_HEURISTIC___EQUATION_two_cases thm 1017 else 1018 QUANT_INSTANTIATE_HEURISTIC___FAIL 1019 end; 1020 1021 1022 fun QUANT_INSTANTIATE_HEURISTIC___cases_list thmL = 1023 let 1024 val thmL1 = filter is_sing_case_thm thmL 1025 val thmL2 = filter is_double_case_thm thmL 1026 val thmL3 = filter is_disj_case_thm thmL 1027 1028 val hL1 = map QUANT_INSTANTIATE_HEURISTIC___one_case thmL1; 1029 val hL2 = map QUANT_INSTANTIATE_HEURISTIC___EQUATION_two_cases thmL2; 1030 in 1031 (hL1, hL2, thmL3) 1032 end 1033end; 1034 1035 1036 1037fun QUANT_INSTANTIATE_HEURISTIC___TypeBase_cases sys v t = 1038if not (is_eq t) then raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp else 1039(let 1040 val thm = TypeBase.nchotomy_of (type_of v) 1041in 1042 QUANT_INSTANTIATE_HEURISTIC___cases thm sys v t 1043end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp); 1044 1045 1046(********************************* 1047 * Another Heuristic for dichotomies 1048 *********************************) 1049(* 1050 val t = ``n = x:num``; 1051 val t = ``x = n:num``; 1052 val v = ``x:num``; 1053 val fv = [``x_n``]; 1054 val sys = NONE; 1055 val thmL = [GSYM prim_recTheory.SUC_ID] 1056 1057 val t = ``[] = l:'a list``; 1058 val v = ``l:'a list`` 1059 val thmL = [rich_listTheory.NOT_CONS_NIL] 1060 1061 val t = ``0 = x`` 1062*) 1063fun QUANT_INSTANTIATE_HEURISTIC___EQUATION_distinct thmL sys v t = 1064let 1065 val _ = if is_eq t then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1066 val (l,r) = dest_eq t; 1067 1068 val (i,turn) = if (l = v) then (r,false) else 1069 if (r = v) then (l,true) else 1070 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1071 1072 val thmL' = flatten (map BODY_CONJUNCTS thmL) 1073 val thmL'' = append thmL' (map GSYM thmL'); 1074 1075 val ni_thm = tryfind (fn thm => PART_MATCH (rhs o dest_neg) thm i) thmL''; 1076 val ni = (lhs o dest_neg o concl) ni_thm; 1077 1078 1079 val fvL_set = HOLset.difference (FVL [ni] empty_tmset, FVL [i] empty_tmset) 1080 val fvL_org = HOLset.listItems fvL_set 1081 val v_name = (fst o dest_var) v 1082 val (fvL, ni) = prefix_free_vars (v_name, fvL_org, ni); 1083 val fvL_org = if null fvL_org then [genvar unit_ty] else fvL_org; 1084 val ni_thm2 = GENL fvL_org ni_thm 1085 val ni_thm3 = CONV_RULE (INTRO_TUPLED_QUANT_CONV THENC 1086 RAND_CONV PABS_ELIM_CONV) ni_thm2 1087 1088 1089 val g_thm = let 1090 val (i_v, i_b) = dest_forall (concl ni_thm3); 1091 val i = mk_abs (i_v, lhs (dest_neg i_b)) 1092 val (vl, vr) = (mk_abs(v,l), mk_abs(v,r)); 1093 val g_thm0 = ISPECL [i, if turn then vr else vl, if turn then vl else vr] (intro_fresh_ty_vars GUESS_RULES_EQUATION_FORALL_POINT) 1094 val g_thm1 = BETA_RULE g_thm0 1095 val g_thm2 = HO_MATCH_MP g_thm1 ni_thm3; 1096 val g_thm3 = CONV_RULE (RAND_CONV 1097 (ALPHA_CONV v THENC 1098 (if (turn) then 1099 (ABS_CONV SYM_CONV) 1100 else ALL_CONV))) g_thm2 1101 in 1102 g_thm3 1103 end 1104 val guess = guess_thm (gty_forall_point, ni, fvL, g_thm); 1105in 1106 {rewrites = [ni_thm], 1107 general = [], 1108 exists_point = [], 1109 forall_point = [guess], 1110 forall = [], 1111 exists = [], 1112 forall_gap = [], 1113 exists_gap = []}:guess_collection 1114end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1115 1116 1117fun QUANT_INSTANTIATE_HEURISTIC___EQUATION___TypeBase_distinct sys v t = 1118let 1119 val _ = if is_eq t then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1120 val thm = TypeBase.distinct_of (type_of v); 1121in 1122 QUANT_INSTANTIATE_HEURISTIC___EQUATION_distinct [thm] sys v t 1123end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1124 1125 1126 1127 1128 1129(********************************* 1130 * Inference Collection 1131 *********************************) 1132 1133(* Some of the heuristics are able to use general theorems to generate guesses. 1134 These theorems should be of the form 1135 1136 ``pre ==> GUESS_TYPE i P`` 1137 1138 For efficiency, it is convient to collect these inference theorems 1139 depending on the type of the conclusion. That is what an inference collection 1140 does. 1141*) 1142 1143type inference_collection = 1144 {exists_point : thm list, 1145 forall_point : thm list, 1146 exists : thm list, 1147 forall : thm list, 1148 exists_gap : thm list, 1149 forall_gap : thm list}; 1150 1151 1152val empty_inference_collection = 1153 {exists_point = [], 1154 forall_point = [], 1155 exists = [], 1156 forall = [], 1157 exists_gap = [], 1158 forall_gap = []}:inference_collection; 1159 1160 1161fun GUESS_THM_list2collection inference_thmL = 1162let 1163 val L0 = flatten (map BODY_CONJUNCTS inference_thmL) 1164 val L1 = map (SIMP_RULE std_ss [combinTheory.K_DEF]) L0; 1165 fun sort_fun (thm, (l1,l2,l3,l4,l5,l6)) = 1166 let 1167 val gtm = (fst o strip_comb o snd o dest_imp o concl) thm 1168 in 1169 if (same_const gtm GUESS_EXISTS_POINT_tm)then 1170 (thm::l1, l2, l3, l4, l5, l6) else 1171 if (same_const gtm GUESS_FORALL_POINT_tm) then 1172 (l1, thm::l2, l3, l4, l5, l6) else 1173 if (same_const gtm GUESS_EXISTS_tm) then 1174 (l1, l2, thm::l3, l4, l5, l6) else 1175 if (same_const gtm GUESS_FORALL_tm) then 1176 (l1, l2, l3, thm::l4, l5, l6) else 1177 if (same_const gtm GUESS_EXISTS_GAP_tm) then 1178 (l1, l2, l3, l4, thm::l5, l6) else 1179 if (same_const gtm GUESS_FORALL_GAP_tm) then 1180 (l1, l2, l3, l4, l5, thm::l6) else 1181 (l1, l2, l3, l4, l5, l6) 1182 end handle HOL_ERR _ => (l1,l2,l3,l4,l5,l6) 1183 1184 val (l1,l2,l3,l4,l5,l6) = foldl sort_fun ([],[],[],[],[],[]) L1; 1185in 1186 {exists_point = l1, 1187 forall_point = l2, 1188 exists = l3, 1189 forall = l4, 1190 exists_gap = l5, 1191 forall_gap = l6 }:inference_collection 1192end; 1193 1194 1195 1196(********************************* 1197 * Heuristics for Quantifiers 1198 *********************************) 1199 1200(* 1201val t = ``!x. P x /\ (y = 2 + x) /\ Q y`` 1202val t = ``?x. P x /\ (y = 2) /\ Q y`` 1203val v = ``y:num`` 1204 1205val t = ``?y:'b. x:'a = f y`` 1206val v = ``x:'a`` 1207val sys = dummy_sys 1208val sys = heuristic 1209*) 1210 1211 1212local 1213 fun col (L1,L2,L3) = 1214 (GUESS_THM_list2collection [L1], 1215 GUESS_THM_list2collection [L2], 1216 GUESS_THM_list2collection [L3]); 1217 1218 1219 val f_icL = col (GUESS_RULES_FORALL, GUESS_RULES_FORALL___NEW_FV, GUESS_RULES_FORALL___NEW_FV_1); 1220 val e_icL = col (GUESS_RULES_EXISTS, GUESS_RULES_EXISTS___NEW_FV, GUESS_RULES_EXISTS___NEW_FV_1); 1221 val u_icL = col (GUESS_RULES_EXISTS_UNIQUE, TRUTH, TRUTH); 1222in 1223 1224fun QUANT_INSTANTIATE_HEURISTIC___QUANT allow_new_fv sys (v:term) t = 1225let 1226 val ((ic, ic_fv, ic_fv_1), (v2, b)) = 1227 (f_icL, dest_forall t) handle HOL_ERR _ => 1228 (e_icL, dest_exists t) handle HOL_ERR _ => 1229 (u_icL, dest_exists1 t) handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1230 1231 val gc:guess_collection = sys v b 1232 1233 fun apply_inference inf guess = 1234 let 1235 val (_, i, fvL, gthm0, was_thm) = guess_extract_thm guess; 1236 val gthm = GEN_ASSUM v2 gthm0; 1237 val new_fv = free_in v2 i 1238 val _ = if new_fv andalso not allow_new_fv then Feedback.fail() else (); 1239 val use_ic = if new_fv then (if null fvL then ic_fv_1 else ic_fv) else ic; 1240 val inf_thm = hd (inf use_ic) handle Empty => Feedback.fail(); 1241 val xthm2 = HO_MATCH_MP inf_thm gthm 1242 in 1243 SOME (guess_thm_to_guess was_thm (SOME (i, if new_fv then v2::fvL else fvL)) xthm2) 1244 end handle HOL_ERR _ => NONE; 1245 1246 val results = flatten (map (fn (s1, s2) => mapPartial (apply_inference s2) (s1 gc)) [ 1247 (#exists_point, #exists_point), 1248 (#forall_point, #forall_point), 1249 (#exists, #exists), 1250 (#forall, #forall), 1251 (#exists_gap, #exists_gap), 1252 (#forall_gap, #forall_gap)]) 1253in 1254 guess_list2collection ([], results) 1255end; 1256 1257end 1258 1259 1260(******************************************************************************) 1261(* General heuristic for moving guesses over structure *) 1262(******************************************************************************) 1263 1264fun process_simple_guess_thm thm = 1265let 1266 val (pre, ant) = dest_imp (concl thm); 1267 val (gty, i, v, t) = dest_guess_tm ant; 1268 1269 val i_ok = is_var i orelse 1270 let 1271 val (i_v, i_b) = dest_abs i 1272 in (type_of i_v = unit_ty) andalso (is_var i_b) end 1273 val _ = if (i_ok) then () else Feedback.fail(); 1274 val (_, tL) = strip_comb t 1275 val tL_simple = all (fn tx => is_var tx orelse 1276 let val (tx_b, tx_v) = dest_comb tx 1277 in (tx_v = v) andalso (is_var tx_b) end) tL 1278 1279 val preL = strip_conj pre 1280 fun check_internal pre_tm = 1281 let 1282 val (gty', i', v', t') = dest_guess_tm pre_tm; 1283 val _ = if (aconv i i') andalso (v = v') then () else Feedback.fail(); 1284 val index_opt = SOME (index (fn t'' => aconv t' t'') tL) handle HOL_ERR _ => NONE; 1285 in 1286 (gty', index_opt) 1287 end; 1288 1289 val pre_checkL = map check_internal preL; 1290 val thm' = CONV_RULE AND_IMP_ELIM_CONV thm 1291 1292 val pre_checkL_opt = if not tL_simple then NONE else SOME (map (fn (ty, index_opt) => (ty, valOf index_opt)) pre_checkL) handle Option => NONE 1293 1294in 1295 SOME (thm', pre_checkL_opt, mk_abs (v, t), i, gty) 1296end handle HOL_ERR _ => NONE; 1297 1298fun process_simple_guess_thm_warn thm = 1299let 1300 val r_opt = process_simple_guess_thm thm; 1301 val _ = if isSome r_opt then () else 1302 say_HOL_WARNING "process_simple_guess_thm" 1303 ("Inference theorem not well formed:\n"^(thm_to_string thm)) 1304in 1305 r_opt 1306end; 1307 1308 1309fun mk_guess_net guesses_thmL = 1310let 1311 fun fresh_vars thm = 1312 SIMP_RULE std_ss [combinTheory.K_DEF] (genvar_RULE thm) 1313 1314 val thmL0 = flatten (map (BODY_CONJUNCTS o fresh_vars) guesses_thmL) 1315 val thmL1 = mapPartial process_simple_guess_thm_warn thmL0 1316 1317 val (sL, cL) = partition (fn (_, opt, _, _, _) => isSome opt) thmL1 1318 1319 (* make guess_net for complex theorems *) 1320 fun group_thmL L [] = L 1321 | group_thmL L ((thm, _, P_t, _, _)::thmPL) = 1322 let 1323 val ((P_t', thmL), L') = pluck (fn (P_t', thmL) => (P_t = P_t')) L handle HOL_ERR _ => 1324 ((P_t, []), L) 1325 in 1326 group_thmL ((P_t', thm::thmL)::L') thmPL 1327 end 1328 val guess_net_complex = 1329 foldr (fn ((P_t, thmL), n) => Ho_Net.enter ([],P_t, (P_t, thmL)) n) Ho_Net.empty 1330 (group_thmL [] cL) 1331 1332 1333 (* make guess_net for simple theorems *) 1334 fun free_var_process (thm, pre_checkL_opt, v_t, i, gty) = 1335 let 1336 val (v, t) = dest_abs v_t; 1337 val (b_op, tL) = strip_comb t; 1338 1339 val pre_checkL = valOf pre_checkL_opt 1340 fun remove_free_var (n, tx) = is_comb tx andalso 1341 all (fn (ty, n') => (not (n = n')) orelse ((ty = gty_forall) orelse (ty = gty_exists))) 1342 pre_checkL 1343 1344 val ntL = enumerate 0 tL; 1345 val remove_varsL = filter remove_free_var ntL; 1346 1347 fun remove_vars_combins [] = [[]] 1348 | remove_vars_combins (x::xs) = 1349 let 1350 val L = remove_vars_combins xs 1351 in 1352 (map (fn z1 => x::z1) L) @ L 1353 end; 1354 val combs = remove_vars_combins remove_varsL 1355 1356 fun apply_combs cL = 1357 let 1358 val pre_checkL' = filter (fn (_,n) => all (fn (n', _) => not (n = n')) cL) pre_checkL 1359 fun mk_tL (sub,tL') [] = (sub, rev tL') 1360 | mk_tL (sub,tL') ((n, tx)::ntL) = 1361 let 1362 val do_remove = exists (fn (n', _) => n = n') cL 1363 val (sub', tL'') = if not do_remove then (sub, tx::tL') else 1364 let 1365 val (tx_b, tx_v) = dest_comb tx; 1366 val tx' = genvar (type_of tx); 1367 1368 in 1369 ((tx_b |-> mk_abs(tx_v, tx'))::sub, tx'::tL') 1370 end; 1371 in 1372 mk_tL (sub', tL'') ntL 1373 end; 1374 val (sub, tL') = mk_tL ([], []) ntL; 1375 val tL'' = map (fn tx => (true, fst (dest_comb tx)) handle HOL_ERR _ => (false, tx)) tL' 1376 val _ = if exists fst tL'' then () else Feedback.fail(); 1377 1378 val xthm0 = SIMP_RULE std_ss [GUESS_RULES_CONSTANT_FORALL, GUESS_RULES_CONSTANT_EXISTS, ETA_THM] (INST sub thm) 1379 1380 val (i_f, i_v) = if is_abs i then (false, snd (dest_abs i)) else (true, i) 1381 1382 val xthm1 = GENL (i_v::(map snd tL'')) xthm0 1383 in 1384 SOME (b_op, (i_f, map fst tL'', pre_checkL', gty, xthm1)) 1385 end handle HOL_ERR _ => NONE; 1386 in 1387 mapPartial apply_combs combs 1388 end; 1389 fun group_simpleL L [] = L 1390 | group_simpleL L ((tm, x)::tmxs) = 1391 let 1392 val ((_, xL), L') = pluck (fn (tm', _) => (same_const tm tm')) L handle HOL_ERR _ => 1393 ((tm, []), L) 1394 in 1395 group_simpleL ((tm, x::xL)::L') tmxs 1396 end 1397 val guess_net_simple = group_simpleL [] (flatten (map free_var_process sL)) 1398in 1399 (guess_net_complex, guess_net_simple) 1400end; 1401 1402 1403 1404(* 1405 1406val guesses_thmL = inference_thmL; 1407val guesses_net = mk_guess_net guesses_thmL 1408val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp (SOME (ref (mk_quant_heuristic_cache()))) 1409val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE 1410val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE std_qp NONE 1411val sys = heuristic; 1412 1413 1414val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE list_qp NONE 1415val sys = heuristic; 1416 1417val sys = dummy_sys 1418 1419val v = ``x:num`` 1420val t = ``(x = 2) ==> P x`` 1421 1422sys v t 1423 1424 1425val v = ``x:'a list`` 1426val t = ``Q ==> (~((x:'a list) = []) /\ P x)`` 1427 1428sys v t 1429GUESS_RULES_IMP 1430 1431val t = ``(x + (y:num) = z) \/ Q y`` 1432 1433val t = ``!x. (x + (y:num) = z) \/ Q y`` 1434 1435 1436val t = ``~(uf (x:'a) = uf y) \/ (P y /\ Q y)`` 1437val v = ``x:'a`` 1438val fv = [v] 1439val t = b 1440 1441 1442QUANT_INSTANTIATE_HEURISTIC___debug := 1443 1444val t = ``~(uf (x:'a) = uf (SND s)) \/ (IS_SOME (e (FST s)) /\ 1445 s IN var_res_prop___PROP f (wpb,rpb) sfb)`` 1446 1447val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE 1448val sys = heuristic; 1449QUANT_INSTANTIATE_HEURISTIC___print_term_length := 2000 1450*) 1451 1452fun strip_comb_abs t = 1453 let 1454 val (t1, t2) = dest_comb t; 1455 val (_, t3) = dest_abs t1; 1456 in 1457 strip_comb_abs t3 1458 end handle HOL_ERR _ => t; 1459 1460 1461fun dest_comb_abs fv fb = 1462 let 1463 val (t1, t2) = dest_comb fb; 1464 val _ = if (t2 = fv) then () else Feedback.fail(); 1465 val t3 = strip_comb_abs t1 1466 val (fv', _) = dest_abs (t3); 1467 in 1468 fv' 1469 end 1470 1471fun get_org_name fv fb = 1472 dest_comb_abs fv (find_term (can (dest_comb_abs fv)) fb) handle HOL_ERR _ => fv; 1473 1474 1475 1476fun local_cache_sys sys = 1477 let 1478 val lc_ref = ref [] 1479 in fn v => fn t => 1480 let 1481 val gc_opt = assoc t (!lc_ref) 1482 in 1483 if (isSome gc_opt) then valOf gc_opt else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 1484 end handle HOL_ERR _ => 1485 let 1486 val gc_opt = SOME (sys v t) handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => NONE 1487 | HOL_ERR _ => NONE; 1488 val _ = lc_ref := (t,gc_opt)::(!lc_ref); 1489 in 1490 if (isSome gc_opt) then valOf gc_opt else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 1491 1492 end 1493end; 1494 1495 1496 1497local 1498 fun exists_forall_CONV t = 1499 HO_REWR_CONV GUESS_RULES_CONSTANT_FORALL t handle HOL_ERR _ => 1500 HO_REWR_CONV GUESS_RULES_CONSTANT_EXISTS t 1501 1502 fun guess_rule_elim_constant_RULE v xthm0 = 1503 let 1504 val (_, t') = dest_abs (rand (rhs (concl xthm0))); 1505 in 1506 if (free_in v t') then xthm0 else 1507 CONV_RULE (RHS_CONV exists_forall_CONV) xthm0 1508 end 1509 1510 fun RRAND_CONV c t = 1511 if is_comb t then RAND_CONV (RRAND_CONV c) t else 1512 c t 1513 1514 fun test_thmL v_t_type tvset v t (P_t, thmL) = 1515 let 1516 val ty_m = match_type (type_of P_t) v_t_type 1517 val P_t' = inst ty_m P_t; 1518 val (v'', t'') = dest_abs P_t'; 1519 val t''' = subst [v'' |-> v] t''; 1520 val (term_sub, ty_sub) = ho_match_term [] tvset t''' t 1521 val _ = map (fn xx => if (free_in v (#residue xx)) then Feedback.fail() else ()) 1522 (term_sub) 1523 1524 val P_t'' = subst term_sub (inst ty_sub P_t'); 1525 val eq_thm0 = ((ALPHA_CONV v) THENC (DEPTH_CONV BETA_CONV)) P_t''; 1526 val eq_thm1_opt = SOME ((DEPTH_CONV BETA_CONV) (mk_abs (v, t))) handle UNCHANGED => NONE 1527 1528 val eq_thm = if isSome eq_thm1_opt then 1529 TRANS eq_thm0 (GSYM (valOf eq_thm1_opt)) else eq_thm0 1530 1531 val ty_sub2 = ty_m @ ty_sub; 1532 fun process_thm thm0 = 1533 let 1534 val xthm0 = INST_TY_TERM (term_sub, ty_sub2) thm0; 1535 val xthm1 = CONV_RULE (RRAND_CONV (K eq_thm)) xthm0 1536 in 1537 SOME xthm1 1538 end handle HOL_ERR _ => NONE 1539 1540 val thmL' = mapPartial process_thm thmL 1541 in 1542 thmL' 1543 end handle HOL_ERR _ => []; 1544 1545(* val (thm,gthm,rthm) = el 1 resL *) 1546 1547 fun GUESS_MP thm gthm = 1548 let 1549 val i = (rand o rator o fst o dest_imp o concl) thm; 1550 val gi = (rand o rator o concl) gthm; 1551 in 1552 if is_var i then 1553 let 1554 val i_ty = (hd o snd o dest_type o type_of) i 1555 val gi_ty = (hd o snd o dest_type o type_of) gi 1556 val ty_sub = [i_ty |-> gi_ty]; 1557 val i' = inst ty_sub i; 1558 1559 val xthm0 = INST_TY_TERM ([i' |-> gi], ty_sub) thm 1560 val xthm1 = MP xthm0 gthm 1561 in 1562 xthm1 1563 end 1564 else if (is_var (snd (dest_abs i)) handle HOL_ERR _ => false) then 1565 let 1566 val (i_v, i_b) = dest_abs i; 1567 val (g_v, g_b) = dest_abs gi; 1568 val _ = if free_in g_v g_b then Feedback.fail() else (); 1569 1570 val ty_sub = [type_of i_v |-> type_of g_v]; 1571 1572 val xthm0 = INST_TY_TERM ([i_b |-> g_b], ty_sub) thm 1573 val xthm1 = MP xthm0 gthm 1574 in 1575 xthm1 1576 end 1577 else MP thm gthm 1578 end; 1579 1580 1581 fun try_guess ifv_opt thm_ok thm guess = 1582 let 1583 val (ty, i, fvL, gthm, was_thm) = guess_extract_thm guess; 1584 val (ifv_opt, nthm) = if isSome ifv_opt then 1585 (ifv_opt, GUESS_MP thm gthm) 1586 else (SOME (i, fvL), GUESS_MP thm gthm) 1587 in 1588 SOME (ifv_opt, thm_ok andalso was_thm, nthm) 1589 end handle HOL_ERR _ => NONE; 1590 1591 fun elim_precond sys v (ifv_opt,thm_ok,thm) = 1592 let 1593 val xthm0 = CONV_RULE (RATOR_CONV ( 1594 (RAND_CONV (RAND_CONV (ALPHA_CONV v) THENC DEPTH_CONV BETA_CONV)))) thm 1595 1596 val precond = (fst o dest_imp) (concl xthm0) 1597 val (gty, _, v', t') = dest_guess_tm precond; 1598 in 1599 if (free_in v' t') then 1600 let 1601 val gc:guess_collection = sys v' t'; 1602 val gL = (guess_collection_guess_type gty) gc; 1603 in 1604 mapPartial (try_guess ifv_opt thm_ok xthm0) gL 1605 end else 1606 [(ifv_opt, thm_ok, MP (CONV_RULE (RATOR_CONV (RAND_CONV exists_forall_CONV)) xthm0) TRUTH)] 1607 end handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => [] 1608 | HOL_ERR _ => []; 1609 1610 fun elim_preconds sys v doneL [] = doneL 1611 | elim_preconds sys v doneL (ithm::thmL) = 1612 if (is_imp_only (concl (#3 ithm))) then 1613 elim_preconds sys v doneL (append (elim_precond sys v ithm) thmL) 1614 else 1615 if (isSome (#1 ithm)) then 1616 elim_preconds sys v (ithm::doneL) thmL 1617 else 1618 elim_preconds sys v doneL thmL 1619 1620in 1621 1622fun QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL_COMPLEX guesses_net_complex sys v t = 1623let 1624 val v_t = mk_abs (v, t); 1625 val possible_thmL = Ho_Net.lookup v_t guesses_net_complex; 1626 val tvset = FVL [t] empty_tmset; 1627 val _ = if HOLset.member (tvset, v) then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1628 1629 val current_thmL = flatten (map (test_thmL (type_of v_t) tvset v t) possible_thmL); 1630 1631 val sys' = local_cache_sys sys; 1632 val results = elim_preconds sys' v [] (map (fn y => (NONE, true, y)) current_thmL) 1633in 1634 guess_list2collection ([], (map (fn (ifv_opt, ok, thm) => guess_thm_to_guess ok ifv_opt thm) results)) 1635end 1636 1637end; 1638 1639 1640 1641(* 1642 1643val guesses_thmL = inference_thmL; 1644val (guesses_net_complex, guesses_net_simple) = mk_guess_net guesses_thmL 1645 1646val (guesses_net_complex, guesses_net_simple) = mk_guess_net[] 1647 1648val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp (SOME (ref (mk_quant_heuristic_cache()))) 1649val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE 1650val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE std_qp NONE 1651val sys = heuristic; 1652 1653 1654val sys = dummy_sys 1655 1656val v = ``z:num`` 1657val t = ``(z = 2) ==> P z`` 1658 1659 1660val v = ``z:num`` 1661val t = ``(z = 2)`` 1662 1663sys v t 1664 1665 1666val v = ``x:'a list`` 1667val t = ``Q ==> (~((x:'a list) = []) /\ P x)`` 1668 1669sys v t 1670GUESS_RULES_IMP 1671 1672val t = ``(x + (y:num) = z) \/ Q y`` 1673 1674val t = ``!x. (x + (y:num) = z) \/ Q y`` 1675 1676 1677val t = ``~(uf (x:'a) = uf y) \/ (P y /\ Q y)`` 1678val v = ``x:'a`` 1679val fv = [v] 1680val t = b 1681val v = ``x:num`` 1682val t = ``if b x then ((x = 2) /\ Q x) else (Q2 x /\ (x = 2))`` 1683 1684QUANT_INSTANTIATE_HEURISTIC___debug := 1685 1686val t = ``~(uf (x:'a) = uf (SND s)) \/ (IS_SOME (e (FST s)) /\ 1687 s IN var_res_prop___PROP f (wpb,rpb) sfb)`` 1688 1689val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE [] 1690val sys = heuristic; 1691 1692sys v t 1693sys v b 1694 1695t b 1696 1697val t = ``Q2 2 /\ (x = 2)`` 1698sys v t 1699 1700QUANT_INSTANTIATE_HEURISTIC___print_term_length := 2000 1701*) 1702 1703local 1704 fun fL_BETA_CONV [] = ALL_CONV 1705 | fL_BETA_CONV (true::fL) = 1706 RAND_CONV BETA_CONV THENC 1707 RATOR_CONV (fL_BETA_CONV fL) 1708 | fL_BETA_CONV (false::fL) = 1709 RATOR_CONV (fL_BETA_CONV fL) 1710in 1711 1712fun QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL_SIMPLE guesses_net_simple sys v t = 1713let 1714 val (b_op, tL) = strip_comb t; 1715 val (_, infL) = first (fn (tm, _) => same_const b_op tm) guesses_net_simple; 1716 1717 val fL = map (free_in v) tL 1718 val infL' = filter (fn (_, fL', _, _, _) => fL = fL') infL 1719 val _ = if null infL' then raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp else (); 1720 1721 val gcL = map (fn t => sys v t handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => empty_guess_collection 1722 | HOL_ERR _ => empty_guess_collection) tL; 1723 1724 fun try_inf (i_f, _, pre_checkL, gty, inf_thm) = 1725 let 1726 val (gty1, arg_n1) = hd pre_checkL; 1727 val pre_checkL_tl = tl pre_checkL; 1728 val gL = (guess_collection_guess_type gty1) (el (arg_n1+1) gcL); 1729 1730 fun process_guess guess = 1731 (let 1732 val (i, fvL) = guess_extract guess; 1733 val _ = if not i_f andalso not (null fvL) then Feedback.fail() else (); 1734 1735 val gL' = map (fn (gty, n) => 1736 first (fn g => guess_extract g = (i, fvL)) ((guess_collection_guess_type gty) (el (n+1) gcL))) pre_checkL_tl; 1737 1738 val final_gL = guess::gL'; 1739 val do_proof = all guess_has_thm final_gL; 1740 in 1741 if (not do_proof) then SOME (mk_guess gty v t i fvL) else 1742 let 1743 val gthm1 = snd (guess2thm guess); 1744 val i_t = (rand o rator o concl) gthm1; 1745 val i_tv = if i_f then i_t else snd (dest_abs i_t); 1746 val t_vL = map (fn (fv, ttt) => if fv then mk_abs (v, ttt) else ttt) (zip fL tL) 1747 val inf_thm0 = ISPECL (i_tv::t_vL) (intro_fresh_ty_vars inf_thm) 1748 val inf_thm1 = LIST_MP (map (snd o guess2thm) final_gL) inf_thm0 1749 val inf_thm2 = CONV_RULE (RAND_CONV (ALPHA_CONV v THENC 1750 ABS_CONV (fL_BETA_CONV (rev fL)))) inf_thm1 1751 in 1752 SOME (guess_thm (gty, i, fvL, inf_thm2)) 1753 end end) handle HOL_ERR _ => NONE 1754 in 1755 mapPartial process_guess gL 1756 end; 1757 1758 val gL2 = flatten (map try_inf infL') 1759in 1760 guess_list2collection ([], gL2) 1761end handle HOL_ERR _ => empty_guess_collection; 1762 1763end; 1764 1765 1766(******************************************************************************) 1767(* Heuristics that apply conversions *) 1768(******************************************************************************) 1769 1770(* Applying a rewrite rule to a guess *) 1771(* 1772val tref = ref NONE 1773 1774val (v,t,thmL,guess) = valOf (!tref) 1775val fvL = [``x:num``, ``y:num``] 1776val rewrite_thm = GSYM (HO_PART_MATCH lhs (hd thmL) ((fst o dest_imp) (concl thm_org))) 1777val fv = [] 1778 1779val v = ``x:num`` 1780val t = ``!t. (P (x:num) /\ Z t):bool`` 1781val t' = ``!t. X t \/ (Q (x:num))`` 1782val i = ``(i (y:num) (z:num)):num`` 1783val fvL = [``y:num``, ``z:num``] 1784 1785val rew_thm = mk_thm ([], mk_eq(t,t')) 1786 1787val guess = make_set_guess_thm_opt___dummy v t' (guess_forall (i,fvL,NONE)); 1788correct_guess fv v t (guess_rewrite_thm_opt v t rew_thm guess) 1789*) 1790 1791fun guess_rewrite rew_thm (guess_general (i, fvL)) = guess_general (i,fvL) 1792 | guess_rewrite rew_thm (guess_thm (gty, i, fvL, thm)) = 1793 guess_thm (gty, i, fvL, 1794 CONV_RULE (RAND_CONV (ABS_CONV (K (GSYM rew_thm)))) thm) 1795 | guess_rewrite rew_thm (guess_term (gty, i, fvL, tm)) = 1796 guess_term (gty, i, fvL, 1797 (rhs o concl) (RAND_CONV (ABS_CONV (K (GSYM rew_thm))) tm)) 1798 1799 1800fun QUANT_INSTANTIATE_HEURISTIC___REWRITE sys (v:term) rew_thm = 1801let 1802 val (lt,rt) = dest_eq (concl rew_thm); 1803 val gc1:guess_collection = sys v rt 1804 1805 val f = guess_rewrite rew_thm; 1806 val gc2 = 1807 {rewrites = #rewrites gc1, 1808 general = [], 1809 exists_point = map f (#exists_point gc1), 1810 forall_point = map f (#forall_point gc1), 1811 forall = map f (#forall gc1), 1812 exists = map f (#exists gc1), 1813 forall_gap = map f (#forall_gap gc1), 1814 exists_gap = map f (#exists_gap gc1)}:guess_collection 1815in 1816 gc2 1817end handle UNCHANGED => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 1818 | HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1819 1820 1821 1822fun QUANT_INSTANTIATE_HEURISTIC___CONV conv sys v t = 1823let 1824 val thm_opt = SOME (QCHANGED_CONV (CHANGED_CONV conv) t) handle HOL_ERR _ => NONE 1825in 1826 if not (isSome thm_opt) then raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp else 1827 QUANT_INSTANTIATE_HEURISTIC___REWRITE sys v (valOf thm_opt) 1828end handle UNCHANGED => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 1829 | HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1830 1831 1832fun QUANT_INSTANTIATE_HEURISTIC___EQUATION___TypeBase_one_one sys v t = 1833let 1834 val (l,_) = dest_eq t; 1835 val thm = TOP_ONCE_REWRITE_CONV [TypeBase.one_one_of (type_of l)] t 1836in 1837 QUANT_INSTANTIATE_HEURISTIC___REWRITE sys v thm 1838end handle UNCHANGED => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 1839 | HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1840 1841 1842 1843(******************************************************************************) 1844(* Heuristic tho rewrite the current term using an implication *) 1845(******************************************************************************) 1846 1847(* Applying a rewrite rule to a guess *) 1848(* 1849val v = ``x:num`` 1850val ctx = [] 1851val t = ``(P (x:num)):bool`` 1852val t2 = ``(x:num) = 2`` 1853val thm = mk_thm ([], mk_imp(t, t2)) 1854val thm2 = mk_thm ([], mk_imp(t2, t)) 1855val thms = [thm, thm2] 1856val thms = [thm] 1857val ctx = thms 1858val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE [] 1859val sys = heuristic; 1860 1861*) 1862 1863local 1864(* 1865 val inf_thm = GUESS_RULES_WEAKEN_FORALL_POINT 1866 val pre_thm = thm1 1867 val gL = (#forall_point gc) 1868 val ithm = inf_thm3 1869 val g = hd gL 1870 val thm = hd thmL 1871*) 1872 fun process_guess ithm g = 1873 let 1874 val (gty, i, fvL, gthm, _) = guess_extract_thm g; 1875 val gthm' = MATCH_MP ithm gthm 1876 in 1877 guess_thm(gty, i, fvL, gthm') 1878 end; 1879 1880 fun process_guess_list pre_thm v t t' inf_thm gL = 1881 let 1882 val vt = mk_abs(v, t) 1883 val vt' = mk_abs(v, t') 1884 val inf_thm1 = ISPECL [vt', vt] (intro_fresh_ty_vars inf_thm) 1885 val inf_thm2 = CONV_RULE ((RATOR_CONV o RAND_CONV o QUANT_CONV o BINOP_CONV) BETA_CONV) inf_thm1 1886 val inf_thm3 = MP inf_thm2 pre_thm 1887 1888 val gL' = map (process_guess inf_thm3) gL 1889 in 1890 gL' 1891 end handle HOL_ERR _ => []; 1892 1893 1894 fun try_single_thm strengthen sys v t thm = 1895 let 1896 val _ = if (is_imp_only (concl thm)) then () else fail(); 1897 val thm0 = (if strengthen then (PART_MATCH (rand o rator) thm t) else 1898 (PART_MATCH rand thm t)); 1899 1900 val pre_thm = GEN v thm0 1901 val t' = if strengthen then (rand (concl thm0)) else (rand (rator (concl thm0))) 1902 1903 val gfun = process_guess_list pre_thm v t t' 1904 1905 val gc1:guess_collection = sys v t' handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => fail() 1906 1907 1908 val gc2 = {rewrites = #rewrites gc1, 1909 general = #general gc1, 1910 exists_point = gfun GUESS_RULES_STRENGTHEN_EXISTS_POINT (#exists_point gc1), 1911 forall_point = gfun GUESS_RULES_WEAKEN_FORALL_POINT (#forall_point gc1), 1912 forall = [], 1913 exists = [], 1914 exists_gap = gfun GUESS_RULES_WEAKEN_EXISTS_GAP (#exists_gap gc1), 1915 forall_gap = gfun GUESS_RULES_STRENGTHEN_FORALL_GAP (#forall_gap gc1)}:guess_collection 1916 in SOME gc2 end handle HOL_ERR _ => NONE 1917 | UNCHANGED => NONE 1918in 1919 1920fun QUANT_INSTANTIATE_HEURISTIC___STRENGTHEN_WEAKEN thms sys (v:term) t = 1921let 1922 val thmL = flatten (map BODY_CONJUNCTS thms); 1923 val gcL_s = mapfilter (try_single_thm true sys v t) thmL 1924 val gcL_w = mapfilter (try_single_thm false sys v t) thmL 1925 val gc = guess_collection_flatten (gcL_s @ gcL_w) 1926in 1927 gc 1928end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1929 1930end 1931 1932 1933(******************************************************************************) 1934(* Heuristic that uses the precondition for direct matching *) 1935(******************************************************************************) 1936 1937(* 1938val v = ``x:'a`` 1939 1940val t = ``(P (x:'a)):bool`` 1941val thm = ASSUME t 1942 1943val t = ``(P (x:'a)):bool`` 1944val thm = ASSUME (mk_neg t) 1945 1946val t = ``(P (x:'a)):bool`` 1947val thm = ASSUME t 1948val t = mk_neg t 1949 1950val thms = [thm]; 1951QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION thms () (v:term) t 1952 1953 val v' = genvar (type_of v); 1954 val t' = subst [v |-> v'] t; 1955 1956 1957val thms = [thm] 1958 1959val v = ``n:num`` 1960val t = ``n < SUC m`` 1961val thm = hd thms 1962val SOME (thms, v, t) = !xxx 1963 1964*) 1965 1966local 1967 fun get_implication_gc sys v t neg dneg i P thm = let 1968 val _ = if neg then () else fail(); 1969 val ithm1 = ISPECL [P, i, v] (intro_fresh_ty_vars IMP_NEG_CONTRA); 1970 1971 val c0 = RATOR_CONV o RAND_CONV 1972 val (c2, c1) = (RAND_CONV BETA_CONV, BETA_CONV) 1973 val ithm2 = CONV_RULE (c0 c2) ithm1; 1974 val ithm3 = if dneg then CONV_RULE (c0 NEG_NEG_ELIM_CONV) ithm2 else ithm2 1975 val ithm4 = MP ithm3 thm 1976 val ithm5 = CONV_RULE (c0 c1) ithm4; 1977 1978 val free_vars_lhs = let 1979 val bound_vars = FVL (hyp ithm5) empty_tmset 1980 val bound_vars' = FVL [(rand (rator (concl ithm5)))] bound_vars 1981 val rest_vars = FVL [rand (concl ithm5)] empty_tmset 1982 val free_vars = HOLset.difference (rest_vars, bound_vars') 1983 in 1984 HOLset.listItems free_vars 1985 end 1986 val ithm6 = List.foldl (fn (v, thm) => CONV_RULE FORALL_IMP_CONV (GEN v thm)) ithm5 free_vars_lhs 1987 val gc = QUANT_INSTANTIATE_HEURISTIC___STRENGTHEN_WEAKEN [ithm6] sys (v:term) t 1988 handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => empty_guess_collection; 1989 in gc end handle HOL_ERR _ => empty_guess_collection; 1990 1991 1992 fun get_direct_matches_gc neg dneg i P thm = let 1993 val gthm0 = if neg then GUESS_RULES_TRIVIAL_FORALL_POINT else GUESS_RULES_TRIVIAL_EXISTS_POINT 1994 val gthm1 = ISPECL [i, P] (intro_fresh_ty_vars gthm0) 1995 1996 val c0 = if neg then (RAND_CONV BETA_CONV) else BETA_CONV 1997 val c1 = if dneg then c0 THENC NEG_NEG_ELIM_CONV else c0 1998 val gthm2 = CONV_RULE (RATOR_CONV (RAND_CONV c1)) gthm1 1999 val gthm = MP gthm2 thm; 2000 val gc = {rewrites = [], 2001 general = [], 2002 exists_point = if neg then [] else [guess_thm (gty_exists_point, i, [], gthm)], 2003 forall_point = if neg then [guess_thm (gty_forall_point, i, [], gthm)] else [], 2004 forall = [], 2005 exists = [], 2006 exists_gap = [], 2007 forall_gap = []}:guess_collection 2008 in gc end; 2009 2010 fun try_single_thm try_imps sys vset v t v' t' thm = 2011 let 2012 val (vs, _) = strip_forall (concl thm); 2013 val vs' = map (fn v => genvar (type_of v)) vs 2014 val thm' = SPECL vs' thm 2015 2016 val consts = HOLset.listItems (FVL [concl thm] vset) 2017 val (s, neg, dneg) = (Unify.simp_unify_terms consts t' (concl thm'), false, false) handle HOL_ERR _ => 2018 (Unify.simp_unify_terms consts (mk_neg t') (concl thm'), true, false) handle HOL_ERR _ => 2019 (Unify.simp_unify_terms consts t' (mk_neg (concl thm')), true, true) handle HOL_ERR _ => 2020 fail(); 2021 val i = Unify.deref_tmenv s v'; 2022 val P = mk_abs (v, t) 2023 val thm'' = INST s thm'; 2024 val gc = get_direct_matches_gc neg dneg i P thm''; 2025 val gc' = if try_imps then let 2026 val gc'' = get_implication_gc sys v t neg dneg i P thm''; 2027 in 2028 guess_collection_append gc gc'' 2029 end else gc 2030 in SOME gc' end handle HOL_ERR _ => NONE; 2031in 2032 2033fun QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION try_imps thms sys (v:term) t = 2034let 2035 val v' = genvar (type_of v); 2036 val t' = subst [v |-> v'] t; 2037 val thmL = flatten (map CONJUNCTS thms); 2038 val vset = HOLset.delete (FVL [t] empty_tmset, v) handle HOLset.NotFound => 2039 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 2040 2041 val gc = guess_collection_flatten (map (try_single_thm try_imps sys vset v t v' t') thmL) 2042in 2043 gc 2044end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 2045 2046end 2047 2048(******************************************************************************) 2049(******************************************************************************) 2050(* *) 2051(* Put everything together *) 2052(* Combine Heuristics / Caching etc *) 2053(* *) 2054(******************************************************************************) 2055(******************************************************************************) 2056 2057 2058(******************************************************************************) 2059(* Quantifier Heuristics Parameters *) 2060(******************************************************************************) 2061 2062(* One needs to collect all the heuristics, theorems etc used during guess search. 2063 The following datastructures achieves this. *) 2064 2065type quant_param = 2066{distinct_thms : thm list, (* Dichotomy theorems showing distinctiness *) 2067 cases_thms : thm list, (* Dichotomy theorems showing case completeness *) 2068 rewrite_thms : thm list, (* Theorems used for rewrites *) 2069 instantiation_thms : thm list, (* Theorems used for direct instantiations *) 2070 imp_thms : thm list, (* Theorems used for weakening and strengthening *) 2071 context_thms : thm list, (* additional context *) 2072 inference_thms : thm list, (* Theorems used as inference rules to derive guesses from guesses for subterms. *) 2073 convs : conv list, (* Conversions used *) 2074 filter : (term -> term -> bool) list, (* Getting a free variable and a term, these ML functions decide, whether to try and find a guess *) 2075 inst_filter : (term -> term -> term -> term list -> bool) list, 2076 (* Getting a free variable v and a term t as well as an instantiation i for v in t and the list of free variables in i, these ML functions decide, whether this instantiation i should be used *) 2077 context_heuristics : (bool * (thm list -> quant_heuristic)) list, (* Heuristics that may use the context of the given theorems, together with a flag whether to apply only at top *) 2078 heuristics : (bool * quant_heuristic) list, (* Heuristics that should be applied for all subterms *) 2079 final_rewrite_thms : thm list (* Rewrites used for cleaning up after instantiations. *) }; 2080 2081 2082fun combine_qp 2083 ({distinct_thms = l11, 2084 rewrite_thms = l12, 2085 cases_thms = l13, 2086 convs = l14, 2087 heuristics = l15, 2088 filter = l19, 2089 inst_filter = l1E, 2090 context_heuristics = l1A, 2091 imp_thms = l1B, 2092 instantiation_thms = l1C, 2093 context_thms = l1D, 2094 inference_thms = l17, 2095 final_rewrite_thms = l16}:quant_param) 2096 ({distinct_thms = l21, 2097 rewrite_thms = l22, 2098 cases_thms = l23, 2099 convs = l24, 2100 heuristics = l25, 2101 filter = l29, 2102 inst_filter = l2E, 2103 context_heuristics = l2A, 2104 imp_thms = l2B, 2105 instantiation_thms = l2C, 2106 context_thms = l2D, 2107 inference_thms = l27, 2108 final_rewrite_thms = l26}:quant_param) = 2109 2110 ({distinct_thms = (append l11 l21), 2111 rewrite_thms = (append l12 l22), 2112 cases_thms = (append l13 l23), 2113 convs = (append l14 l24), 2114 filter = (append l19 l29), 2115 inst_filter = (append l1E l2E), 2116 context_heuristics = (append l1A l2A), 2117 imp_thms = (append l1B l2B), 2118 instantiation_thms = (append l1C l2C), 2119 context_thms = (append l1D l2D), 2120 heuristics = (append l15 l25), 2121 inference_thms = (append l17 l27), 2122 final_rewrite_thms = (append l16 l26)}:quant_param) 2123 2124 2125val empty_qp = 2126 ({distinct_thms = [], 2127 rewrite_thms = [], 2128 cases_thms = [], 2129 convs = [], 2130 heuristics = [], 2131 filter = [], 2132 inst_filter = [], 2133 context_heuristics = [] , 2134 imp_thms = [], 2135 instantiation_thms = [], 2136 context_thms = [], 2137 inference_thms = [], 2138 final_rewrite_thms = []}:quant_param) 2139 2140fun combine_qps L = 2141 foldl (fn (a1,a2) => combine_qp a1 a2) empty_qp L; 2142 2143fun distinct_qp thmL = 2144 {distinct_thms=thmL, 2145 rewrite_thms=[], 2146 cases_thms=[], 2147 filter=[], 2148 context_heuristics=[], 2149 inference_thms=[], 2150 imp_thms = [], 2151 inst_filter = [], 2152 instantiation_thms = [], 2153 context_thms = [], 2154 convs=[],heuristics=[], 2155 final_rewrite_thms=[]}:quant_param; 2156 2157fun rewrite_qp thmL = 2158 {distinct_thms=[], 2159 rewrite_thms=thmL, 2160 cases_thms=[], 2161 filter=[], 2162 inst_filter = [], 2163 context_heuristics=[], 2164 inference_thms=[], 2165 imp_thms = [], 2166 instantiation_thms = [], 2167 context_thms = [], 2168 convs=[],heuristics=[], 2169 final_rewrite_thms=[]}:quant_param; 2170 2171fun fixed_context_qp thmL = 2172 {distinct_thms=[], 2173 rewrite_thms=[], 2174 cases_thms=[], 2175 filter=[], 2176 inst_filter = [], 2177 context_heuristics=[], 2178 inference_thms=[], 2179 imp_thms = [], 2180 instantiation_thms = [], 2181 context_thms = thmL, 2182 convs=[],heuristics=[], 2183 final_rewrite_thms=[]}:quant_param; 2184 2185fun imp_qp thmL = 2186 {distinct_thms=[], 2187 rewrite_thms=[], 2188 cases_thms=[], 2189 filter=[], 2190 inst_filter = [], 2191 context_heuristics=[], 2192 inference_thms=[], 2193 imp_thms = thmL, 2194 instantiation_thms = [], 2195 context_thms = [], 2196 convs=[],heuristics=[], 2197 final_rewrite_thms=[]}:quant_param; 2198 2199fun instantiation_qp thmL = 2200 {distinct_thms=[], 2201 rewrite_thms=[], 2202 cases_thms=[], 2203 filter=[], 2204 inst_filter = [], 2205 context_heuristics=[], 2206 inference_thms=[], 2207 imp_thms = [], 2208 instantiation_thms = thmL, 2209 context_thms = [], 2210 convs=[],heuristics=[], 2211 final_rewrite_thms=[]}:quant_param; 2212 2213fun final_rewrite_qp thmL = 2214 {distinct_thms=[], 2215 rewrite_thms=[], 2216 cases_thms=[], 2217 filter=[], 2218 inst_filter = [], 2219 context_heuristics=[], 2220 inference_thms=[], 2221 imp_thms = [], 2222 instantiation_thms = [], 2223 context_thms = [], 2224 convs=[],heuristics=[], 2225 final_rewrite_thms=thmL}:quant_param; 2226 2227fun cases_qp thmL = 2228 {distinct_thms=[], 2229 rewrite_thms=[], 2230 cases_thms=thmL, 2231 filter=[], 2232 inst_filter = [], 2233 context_heuristics=[], 2234 inference_thms=[], 2235 convs=[],heuristics=[], 2236 imp_thms = [], 2237 instantiation_thms = [], 2238 context_thms = [], 2239 final_rewrite_thms=[]}:quant_param; 2240 2241fun inference_qp thmL = 2242 {distinct_thms=[], 2243 rewrite_thms=[], 2244 cases_thms=[], 2245 filter=[], 2246 inst_filter = [], 2247 context_heuristics=[], 2248 inference_thms=thmL, 2249 convs=[],heuristics=[], 2250 imp_thms = [], 2251 instantiation_thms = [], 2252 context_thms = [], 2253 final_rewrite_thms=[]}:quant_param; 2254 2255fun convs_qp cL = 2256 {distinct_thms=[], 2257 rewrite_thms=[], 2258 cases_thms=[], 2259 filter=[], 2260 inst_filter = [], 2261 context_heuristics=[], 2262 inference_thms=[], 2263 convs=cL,heuristics=[], 2264 imp_thms = [], 2265 instantiation_thms = [], 2266 context_thms = [], 2267 final_rewrite_thms=[]}:quant_param; 2268 2269fun heuristics_qp hL = 2270 {distinct_thms=[], 2271 rewrite_thms=[], 2272 cases_thms=[], 2273 filter=[], 2274 inst_filter = [], 2275 context_heuristics=[], 2276 inference_thms=[], 2277 convs=[],heuristics=map (fn h => (false, h)) hL, 2278 imp_thms = [], 2279 instantiation_thms = [], 2280 context_thms = [], 2281 final_rewrite_thms=[]}:quant_param; 2282 2283fun top_heuristics_qp hL = 2284 {distinct_thms=[], 2285 rewrite_thms=[], 2286 cases_thms=[], 2287 filter=[], 2288 inst_filter = [], 2289 context_heuristics=[], 2290 inference_thms=[], 2291 convs=[], 2292 heuristics=map (fn h => (true, h)) hL, 2293 imp_thms = [], 2294 instantiation_thms = [], 2295 context_thms = [], 2296 final_rewrite_thms=[]}:quant_param; 2297 2298fun context_heuristics_qp chL = 2299 {distinct_thms=[], 2300 rewrite_thms=[], 2301 cases_thms=[], 2302 filter=[], 2303 inst_filter = [], 2304 context_heuristics=map (fn h => (false, h)) chL, 2305 inference_thms=[], 2306 imp_thms = [], 2307 instantiation_thms = [], 2308 context_thms = [], 2309 convs=[],heuristics=[], 2310 final_rewrite_thms=[]}:quant_param; 2311 2312fun context_top_heuristics_qp chL = 2313 {distinct_thms=[], 2314 rewrite_thms=[], 2315 cases_thms=[], 2316 filter=[], 2317 inst_filter = [], 2318 context_heuristics=map (fn h => (true, h)) chL, 2319 inference_thms=[], 2320 imp_thms = [], 2321 instantiation_thms = [], 2322 context_thms = [], 2323 convs=[],heuristics=[], 2324 final_rewrite_thms=[]}:quant_param; 2325 2326fun filter_qp fL = 2327 {distinct_thms=[], 2328 rewrite_thms=[], 2329 cases_thms=[], 2330 filter=fL, 2331 inst_filter = [], 2332 context_heuristics=[], 2333 inference_thms=[], 2334 imp_thms = [], 2335 instantiation_thms = [], 2336 context_thms = [], 2337 convs=[],heuristics=[], 2338 final_rewrite_thms=[]}:quant_param; 2339 2340fun inst_filter_qp fL = 2341 {distinct_thms=[], 2342 rewrite_thms=[], 2343 cases_thms=[], 2344 filter=[], 2345 inst_filter = fL, 2346 context_heuristics=[], 2347 inference_thms=[], 2348 imp_thms = [], 2349 instantiation_thms = [], 2350 context_thms = [], 2351 convs=[],heuristics=[], 2352 final_rewrite_thms=[]}:quant_param; 2353 2354 2355 2356(******************************************************************************) 2357(* Combining multiple heuristics and other stuff into one big one that *) 2358(* calls itself recursively, uses caches and provides debugging information *) 2359(******************************************************************************) 2360 2361 2362(* Cache *) 2363 2364(* 2365 val heuristicL = [QUANT_INSTANTIATE_HEURISTIC___EQUATION]; 2366 val v = ``x:num`` 2367 val t = ``x:num = 9`` 2368*) 2369 2370type quant_heuristic_cache = (Term.term, (Term.term, guess_collection) Redblackmap.dict) Redblackmap.dict 2371fun mk_quant_heuristic_cache () = (Redblackmap.mkDict Term.compare):quant_heuristic_cache 2372 2373(* 2374val cache = mk_quant_heuristic_cache () 2375val t = T 2376val v = T 2377val fv = [T] 2378val gc = SOME empty_guess_collection 2379*) 2380 2381fun quant_heuristic_cache___insert (cache:quant_heuristic_cache) (v:term) (t:term) (gc:guess_collection) = 2382let 2383 val t_cache_opt = Redblackmap.peek (cache,t) 2384 val t_cache = if isSome t_cache_opt then valOf t_cache_opt else 2385 (Redblackmap.mkDict Term.compare); 2386 2387 val t_cache' = Redblackmap.insert (t_cache, v, gc) 2388 val cache' = Redblackmap.insert (cache, t, t_cache') 2389in 2390 cache':quant_heuristic_cache 2391end; 2392 2393 2394 2395fun quant_heuristic_cache___peek (cache:quant_heuristic_cache) (v:term) (t:term) = 2396let 2397 val t_cache = Redblackmap.find (cache,t) 2398 val gc = Redblackmap.find (t_cache,v); 2399in 2400 SOME gc 2401end handle Redblackmap.NotFound => NONE; 2402 2403 2404 2405 2406(* Auxiliary functions *) 2407 2408fun cut_term_to_string t = 2409 let 2410 val n = !QUANT_INSTANTIATE_HEURISTIC___print_term_length; 2411 val st = term_to_string t; 2412 val st' = if (String.size st > n) then 2413 (substring (st,0,n)^"...") else st 2414 in 2415 st' 2416 end; 2417 2418 2419fun COMBINE_HEURISTIC_FUNS L = 2420let 2421 val gcL = map (fn h => 2422 ((SOME (h ()) 2423 handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => NONE 2424 | HOL_ERR _ => NONE 2425 | UNCHANGED => NONE 2426 ))) L; 2427 val gc = guess_collection_flatten gcL; 2428in 2429 gc 2430end; 2431 2432fun prefix_string 0 = "" 2433 | prefix_string n = " "^(prefix_string (n-1)); 2434 2435 2436(* 2437 2438val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE 2439val sys = heuristic; 2440 2441 2442val heuristicL = 2443 [QUANT_INSTANTIATE_HEURISTIC___EQUATION, 2444 QUANT_INSTANTIATE_HEURISTIC___BOOL, 2445 QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL 2446 (mk_guess_net inference_thmL)] 2447 2448val t = ``(x = 7) \/ Q x`` 2449val v = ``x:num`` 2450 2451sys v t 2452QUANT_INSTANTIATE_HEURISTIC___EQUATION sys v t 2453val t = ``!x y. P x y (z:'a)`` 2454val v = ``z:'a`` 2455val fv = [v] 2456 2457val n = 0; 2458val cache_ref_opt = SOME (ref (mk_quant_heuristic_cache ())) 2459val heuristicL = hL 2460*) 2461 2462(* The main function with an explicit recursion depth argument, and a list of already visited arguments. The arguments are: 2463 2464 n - recurion depth 2465 tL - stack of terms for which instantiation is searched. Needed to detect cycles and abort. 2466 filterL - a list of ML-functions that say which variable / term combinations to skip 2467 top_heuristicL - a list of heuristics that should just be tried at top-level but not used for recursive calls 2468 heuristicL - the list of heuristics to combine 2469 ctx_top_heuristicL - context heuristics to combine and only be used at top-level 2470 ctx_heuristicL - context heuristics to combine. In contrast to heuristicL they get an extra context argument as input and their result is 2471 not cached, because it may depend on the context. 2472 cache_ref_opt - a reference to a cache, if NONE is passed, a new cache is created internally 2473 ctx - context theorems that might be used 2474 v - the variable 2475 t - the term 2476*) 2477 2478fun BOUNDED_QUANT_INSTANTIATE_HEURISTIC___COMBINE n tL 2479 filterL inst_filterL top_heuristicL heuristicL ctx_top_heuristicL ctx_heuristicL cache_ref_opt (ctx:thm list) (v:term) (t:term) = 2480if (n >= !QUANT_INSTANTIATE_HEURISTIC___max_rec_depth) then 2481 ((say_HOL_WARNING "BOUNDED_QUANT_INSTANTIATE_HEURISTIC___COMBINE" "Maximal recursion depth reached!"); 2482 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp) 2483else let 2484 val _ = if exists (aconv t) tL then raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp else (); 2485 val _ = if (all (fn filter => (filter v t)) filterL) andalso (free_in v t) then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 2486 val cache_ref = if isSome cache_ref_opt then valOf cache_ref_opt else 2487 (ref (mk_quant_heuristic_cache ())); 2488 val gc_opt = quant_heuristic_cache___peek (!cache_ref) v t 2489 val cache_found = isSome gc_opt; 2490 2491 val _ = if ((!QUANT_INSTANTIATE_HEURISTIC___debug > 0) andalso (n <= !QUANT_INSTANTIATE_HEURISTIC___debug_depth)) then 2492 say ((prefix_string n)^"searching guesses for ``"^ 2493 (term_to_string v)^"`` in ``"^(cut_term_to_string t)^"``\n") 2494 else (); 2495 2496 val sys = BOUNDED_QUANT_INSTANTIATE_HEURISTIC___COMBINE (n+1) (t :: tL) filterL inst_filterL [] heuristicL [] ctx_heuristicL (SOME cache_ref) ctx; 2497 val gc = if (isSome gc_opt) then valOf gc_opt else 2498 let 2499 val hL = map (fn h => (fn () => (h sys v t))) (top_heuristicL @ heuristicL); 2500 val gc = COMBINE_HEURISTIC_FUNS hL; 2501 val _ = let 2502 val c = quant_heuristic_cache___insert (!cache_ref) v t gc; 2503 val _ = cache_ref := c 2504 in 2505 () 2506 end; 2507 in 2508 gc 2509 end; 2510 2511 val gc_context = let 2512 val hLc = map (fn h => (fn () => (h ctx sys v t))) (ctx_top_heuristicL @ ctx_heuristicL); 2513 val gc = COMBINE_HEURISTIC_FUNS (hLc); 2514 in 2515 gc 2516 end; 2517 val gc = correct_guess_collection v t (guess_collection_clean (guess_collection_append gc gc_context)); 2518 val gc = filter_guess_collection inst_filterL v t gc; 2519 2520 val _ = if (!QUANT_INSTANTIATE_HEURISTIC___debug > 0) andalso (n <= !QUANT_INSTANTIATE_HEURISTIC___debug_depth) then 2521 let 2522 val gL = (snd (guess_collection2list gc)); 2523 val prefix = prefix_string n; 2524 val guesses_found_string = if null gL then "no" else Int.toString (length gL); 2525 val _ = say (prefix^guesses_found_string^" guesses found for ``"^ 2526 (term_to_string v)^"`` in ``"^(cut_term_to_string t)^"``\n") 2527 2528 val show_thm = (!QUANT_INSTANTIATE_HEURISTIC___debug > 1); 2529 fun say_guess guess = say (prefix^" - "^ 2530 (guess_to_string show_thm guess)^"\n") 2531 val _ = foldl (fn (guess,_) => say_guess guess) () (snd (guess_collection2list gc)) 2532 in 2533 () 2534 end 2535 else () 2536 val _ = if (is_empty_guess_collection gc) then raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp else (); 2537in 2538 gc 2539end; 2540 2541 2542 2543(* The finial top level function *) 2544val QUANT_INSTANTIATE_HEURISTIC___COMBINE = 2545 BOUNDED_QUANT_INSTANTIATE_HEURISTIC___COMBINE 0 []; 2546 2547 2548 2549 2550(****************************************************************** 2551 * creating heuristics from a quantifier parameter 2552 ******************************************************************) 2553 2554local 2555 val inference_thmL = [GUESS_RULES_DISJ, GUESS_RULES_CONJ, 2556 GUESS_RULES_IMP, GUESS_RULES_EQUIV, 2557 GUESS_RULES_COND, GUESS_RULES_NEG]; 2558 val (guesses_net_complex, guesses_net_simple) = mk_guess_net inference_thmL; 2559 2560 val BASIC_QUANT_INSTANTIATE_HEURISTICS = 2561 [QUANT_INSTANTIATE_HEURISTIC___EQUATION, 2562 QUANT_INSTANTIATE_HEURISTIC___BOOL, 2563 QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL_SIMPLE guesses_net_simple, 2564 QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL_COMPLEX guesses_net_complex, 2565 QUANT_INSTANTIATE_HEURISTIC___QUANT true, 2566 QUANT_INSTANTIATE_HEURISTIC___CONV (markerLib.DEST_LABEL_CONV), 2567 QUANT_INSTANTIATE_HEURISTIC___CONV (asm_marker_ELIM_CONV) 2568 ] 2569in 2570 2571 (* The most basic heuristics that should always be turned on *) 2572 val basic_qp = heuristics_qp BASIC_QUANT_INSTANTIATE_HEURISTICS 2573 val direct_context_qp = context_heuristics_qp[QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION false] 2574 val context_qp = context_heuristics_qp[QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION true, QUANT_INSTANTIATE_HEURISTIC___STRENGTHEN_WEAKEN] 2575end; 2576 2577fun qp_to_heuristic 2578 ({distinct_thms = distinct_thmL, 2579 cases_thms = cases_thmL, 2580 rewrite_thms = rewrite_thmL, 2581 inference_thms = inference_thmL2, 2582 inst_filter = inst_filterF, 2583 convs = convL, 2584 filter = filterF, 2585 context_heuristics=full_context_heuristicL, 2586 heuristics = full_heuristicL, 2587 imp_thms = imp_thmL, 2588 instantiation_thms = instantiation_thmL, 2589 context_thms = ctx_thmL, 2590 final_rewrite_thms = final_rewrite_thmL}:quant_param) = 2591 let 2592 fun split_fun (b:bool) L = map snd (filter (fn (f, _) => b = f) L) 2593 val heuristicL = split_fun false full_heuristicL 2594 val top_heuristicL = split_fun true full_heuristicL 2595 val context_heuristicL = split_fun false full_context_heuristicL 2596 val top_context_heuristicL = split_fun true full_context_heuristicL 2597 val (hcL1, hcL2, imp_case_thms) = QUANT_INSTANTIATE_HEURISTIC___cases_list cases_thmL; 2598 val (guesses_net_complex, guesses_net_simple) = mk_guess_net inference_thmL2; 2599 val extra_imp_thms = mapfilter (MATCH_MP DISJ_IMP_INTRO) imp_case_thms 2600 2601 val top_heuristicL = (hcL1 @ top_heuristicL); 2602 val heuristicL_1 = [QUANT_INSTANTIATE_HEURISTIC___EQUATION_distinct distinct_thmL, 2603 QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL_SIMPLE guesses_net_simple, 2604 QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL_COMPLEX guesses_net_complex, 2605 QUANT_INSTANTIATE_HEURISTIC___STRENGTHEN_WEAKEN (imp_thmL @ extra_imp_thms), 2606 QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION true instantiation_thmL] 2607 val heuristicL_2 = map QUANT_INSTANTIATE_HEURISTIC___CONV ((map (fn thm => TOP_ONCE_REWRITE_CONV [thm]) rewrite_thmL)@convL) 2608 val heuristicL_final = flatten [heuristicL_1, heuristicL_2, hcL2, heuristicL] 2609 in 2610 fn cache_ref_opt => fn ctx => 2611 (QUANT_INSTANTIATE_HEURISTIC___COMBINE filterF inst_filterF top_heuristicL heuristicL_final 2612 top_context_heuristicL context_heuristicL cache_ref_opt (append ctx ctx_thmL)) 2613 end; 2614 2615(* very simple system callback for debugging *) 2616val debug_sys = qp_to_heuristic empty_qp NONE [] 2617 2618(****************************************************************** 2619 * a stateful heuristic and quant_param 2620 ******************************************************************) 2621 2622val quant_param_ref = ref empty_qp; 2623fun clear_stateful_qp () = (quant_param_ref := empty_qp); 2624 2625 2626fun stateful_qp___add_combine_arguments args = 2627 (quant_param_ref := 2628 combine_qps ((!quant_param_ref)::args)); 2629 2630 2631val TypeBase_qp = heuristics_qp [ 2632 QUANT_INSTANTIATE_HEURISTIC___EQUATION___TypeBase_one_one, 2633 QUANT_INSTANTIATE_HEURISTIC___EQUATION___TypeBase_distinct, 2634 QUANT_INSTANTIATE_HEURISTIC___TypeBase_cases]; 2635 2636 2637fun pure_stateful_qp () = (!quant_param_ref) 2638 2639fun stateful_qp () = combine_qp TypeBase_qp (pure_stateful_qp ()); 2640 2641fun get_qp___for_types typeL = 2642 {distinct_thms = map TypeBase.distinct_of typeL, 2643 cases_thms = map TypeBase.nchotomy_of typeL, 2644 rewrite_thms = map TypeBase.one_one_of typeL, 2645 context_heuristics=[], filter=[], 2646 final_rewrite_thms = [], 2647 inference_thms = [], 2648 imp_thms = [], 2649 instantiation_thms = [], 2650 inst_filter = [], 2651 context_thms = [], 2652 convs=[],heuristics=[]}:quant_param; 2653 2654 2655 2656(****************************************************************** 2657 * The main stuff 2658 ******************************************************************) 2659 2660(* 2661val only_eq = false; 2662val try_eq = true; 2663val expand_eq = false; 2664val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE neg_heuL []; 2665val dir = CONSEQ_CONV_UNKNOWN_direction; 2666val t = ``!t:num. (t = 5) ==> X`` 2667val t = ``!z t q. ((t = z2) ==> X z) /\ (z = 8 + t)`` 2668*) 2669 2670 2671fun move_exists_to_end t = 2672let 2673 val thm1 = SWAP_EXISTS_CONV t; 2674 2675 val (top_var, r_term) = dest_exists (rhs (concl thm1)); 2676 val thm2 = move_exists_to_end r_term; 2677 val thm3 = EQ_EXISTS_INTRO (top_var, thm2); 2678in 2679 TRANS thm1 thm3 2680end handle HOL_ERR _ => REFL t; 2681 2682 2683(* 2684val BOOL_SIMP_CONV_cs = (computeLib.bool_compset()); 2685val _ = computeLib.add_conv (boolSyntax.universal,1,QCONV QUANT_SIMP_CONV) BOOL_SIMP_CONV_cs; 2686val _ = computeLib.add_conv (boolSyntax.existential,1,QCONV QUANT_SIMP_CONV) BOOL_SIMP_CONV_cs; 2687val BOOL_SIMP_CONV = WEAK_CBV_CONV BOOL_SIMP_CONV_cs; 2688*) 2689 2690fun BOOL_SIMP_CONV rwL (gc:guess_collection) = 2691let 2692 val conv = REWRITE_CONV (append rwL (#rewrites gc)); 2693in 2694 fn t => conv t handle UNCHANGED => REFL t 2695end; 2696 2697 2698(* 2699val t = ``?x. (x = 2) /\ P x``; 2700val t = ``?x. (x = 2) \/ P x``; 2701val t = ``?x. (7 + z = x) /\ P x``; 2702 2703val t = ``?x. !z. ~(~(7 = x) \/ P x z)``; 2704val t = ``?l. ~(l = [])`` 2705 2706val t = ``?x a b. P /\ (f x = f 2) /\ Q (f x)`` 2707val t = ``?p1 p2. (p1 = 7) /\ Q p1 p2`` 2708val t = ``?p1. (p1 = 7) /\ Q p1`` 2709val t = ``?x:'a. (!y2:'b y:'b y3:'b. (x = f y y2 y3)) /\ P x`` 2710val t = ``?x. ~(Q3 x \/ Q x \/ Q2 x \/ ~(x = 2))`` 2711 2712val only_eq = true; 2713val try_eq = true; 2714val expand_eq = false; 2715val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE 2716val sys = heuristic; 2717val dir = CONSEQ_CONV_UNKNOWN_direction 2718val min_var_occs = true; 2719val rwL = [] 2720 2721val t = mk_exists (v, t 2722val t = ``!x. x = []`` 2723 2724heuristic ``l:'a list`` ``l:'a list = []`` 2725*) 2726 2727 2728fun QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (only_eq,try_eq,expand_eq) min_var_occs heuristic rwL (ctx:thm list) dir t = 2729if (not (is_exists t)) andalso (not (is_forall t)) andalso (not (is_exists1 t)) then raise UNCHANGED else 2730let 2731 val (v,b) = dest_abs (rand t); 2732in 2733 (if not (free_in v b) then 2734 ((if is_exists t then EXISTS_SIMP_CONV else 2735 if is_forall t then FORALL_SIMP_CONV else 2736 (HO_PART_MATCH lhs UEXISTS_SIMP)) t) 2737 else 2738 if is_exists t then 2739 let 2740 val (v,qb) = dest_exists t; 2741 val (qvL, b0) = strip_exists qb; 2742 2743 val b_thm = if min_var_occs then 2744 min_var_occur_CONV v b0 handle UNCHANGED => REFL b0 2745 else REFL b0; 2746 val b = rhs (concl b_thm); 2747 2748 val guessC = correct_guess_collection v b 2749 (heuristic ctx v b) 2750 handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => raise UNCHANGED; 2751 2752 val exists_pointL = #exists_point guessC; 2753 val existsL = append (#exists guessC) 2754 (map guess_weaken (#exists_gap guessC)) 2755 2756 val guess = first guess_has_thm exists_pointL handle HOL_ERR _ => 2757 first guess_has_thm_no_free_vars existsL handle HOL_ERR _ => 2758 first guess_has_thm existsL handle HOL_ERR _ => 2759 first (K true) exists_pointL handle HOL_ERR _ => 2760 first (K true) existsL handle HOL_ERR _ => 2761 first (K true) (#general guessC) handle HOL_ERR _ => 2762 raise UNCHANGED; 2763 2764 val (i,fvL) = guess_extract guess; 2765 val proof_opt = guess2thm_opt guess; 2766 val need_eq = (only_eq orelse (dir = CONSEQ_CONV_WEAKEN_direction)); 2767 val try_proof_eq = isSome proof_opt andalso try_eq andalso need_eq; 2768 2769 val thm_opt = if not try_proof_eq then NONE else 2770 if (is_guess_thm gty_exists_point guess) then 2771 let 2772 val proof = valOf proof_opt; 2773 val xthm0 = MATCH_MP GUESS_EXISTS_POINT_THM proof 2774 in 2775 SOME xthm0 2776 end 2777 else (*exists*) 2778 let 2779 val proof = (valOf proof_opt); 2780 val i_t = rand (rator (concl proof)) 2781 val xthm0 = ISPEC i_t GUESS_EXISTS_THM 2782 val new_part = (rhs o rand o snd o dest_forall o concl) xthm0 2783 val new_part_CONV1 = if null fvL then ALL_CONV else 2784 TRY_CONV (SPLIT_QUANT_CONV (pairSyntax.list_mk_pair fvL)) 2785 val new_part_thm = (new_part_CONV1 THENC SIMP_CONV std_ss []) new_part; 2786 val xthm1 = CONV_RULE (QUANT_CONV (RAND_CONV (RHS_CONV (K new_part_thm)))) xthm0 2787 val xthm2 = MATCH_MP xthm1 proof 2788 val xthm3 = CONV_RULE (RHS_CONV (DEPTH_CONV BETA_CONV)) xthm2 2789 in 2790 SOME xthm3 2791 end; 2792 val thm = if isSome thm_opt then valOf thm_opt else 2793 if need_eq then 2794 if not expand_eq then raise UNCHANGED else 2795 let 2796 val thm0 = HO_PART_MATCH lhs (ISPEC i quantHeuristicsTheory.UNWIND_EXISTS_THM) (mk_exists (v,b)) 2797 2798 val thm1 = foldl (fn (fv,th) => 2799 let 2800 val thm2 = AP_TERM (inst [alpha |-> type_of fv] boolSyntax.existential) (ABS fv th); 2801 val thm3 = CONV_RULE (LHS_CONV QUANT_SIMP_CONV) thm2 2802 val thm4 = CONV_RULE (RHS_CONV (HO_PART_MATCH lhs quantHeuristicsTheory.MOVE_EXISTS_IMP_THM)) thm3 2803 in 2804 thm4 2805 end) thm0 fvL; 2806 in 2807 thm1 2808 end 2809 else 2810 let 2811 val vL = free_vars b; 2812 val (fvL', sub) = list_variant vL fvL; 2813 val i' = subst sub i; 2814 val ib = subst [v |-> i'] b; 2815 val ib_thm = ASSUME ib 2816 val thm0 = EXISTS ((mk_exists (v,b)),i') ib_thm 2817 val thm1 = foldr (fn (v,th) => SIMPLE_CHOOSE v th) 2818 thm0 fvL'; 2819 val thm2 = DISCH_ALL thm1 2820 in 2821 thm2 2822 end; 2823 2824 val b_thm_conv = QUANT_CONV (REWR_CONV (GSYM b_thm)) 2825 val thm2 = if is_eq (concl thm) then 2826 CONV_RULE (LHS_CONV b_thm_conv) thm 2827 else 2828 CONV_RULE (RAND_CONV b_thm_conv) thm 2829 2830 val thm3 = if (null qvL) then thm2 else 2831 let 2832 val EXISTS_INTRO_FUN = 2833 if is_eq (concl thm2) then 2834 EQ_EXISTS_INTRO else IMP_EXISTS_INTRO; 2835 val thm3 = foldr EXISTS_INTRO_FUN thm2 qvL; 2836 val ex_move_thm = move_exists_to_end t; 2837 in 2838 THEN_CONSEQ_CONV___combine ex_move_thm thm3 t 2839 end; 2840 2841 val thm4 = CONSEQ_CONV___APPLY_CONV_RULE thm3 t (BOOL_SIMP_CONV rwL guessC) 2842 in 2843 thm4 2844 end else if is_forall t then 2845 let 2846 val neg_t = let 2847 val (vL, body) = strip_forall t; 2848 val n_body = mk_neg body 2849 in 2850 list_mk_exists (vL, n_body) end 2851 2852 val thm = QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (only_eq,try_eq,expand_eq) min_var_occs heuristic rwL ctx (CONSEQ_CONV_DIRECTION_NEGATE dir) (neg_t) 2853 2854 val neg_t_thm = NOT_FORALL_LIST_CONV (mk_neg t) 2855 val new_conv = TRY_CONV NOT_EXISTS_LIST_CONV THENC (BOOL_SIMP_CONV rwL empty_guess_collection) 2856 2857 val thm2 = if is_eq (concl thm) then 2858 let 2859 val thm3 = TRANS neg_t_thm thm; 2860 val thm4 = AP_TERM boolSyntax.negation thm3; 2861 val thm5 = CONV_RULE (LHS_CONV NEG_NEG_ELIM_CONV) thm4 2862 val thm6 = CONV_RULE (RHS_CONV new_conv) thm5; 2863 in 2864 thm6 2865 end 2866 else if (rand (rator (concl thm))) = neg_t then 2867 let 2868 val thm3 = IMP_TRANS (fst (EQ_IMP_RULE neg_t_thm)) thm; 2869 val thm4 = CONTRAPOS thm3; 2870 val thm5 = CONV_RULE (RAND_CONV NEG_NEG_ELIM_CONV) thm4 2871 val thm6 = CONV_RULE (RATOR_CONV (RAND_CONV new_conv)) thm5 2872 in 2873 thm6 2874 end 2875 else if (rand (concl thm)) = neg_t then 2876 let 2877 val thm3 = IMP_TRANS thm (snd (EQ_IMP_RULE neg_t_thm)); 2878 val thm4 = CONTRAPOS thm3; 2879 val thm5 = CONV_RULE (RATOR_CONV (RAND_CONV NEG_NEG_ELIM_CONV)) thm4 2880 val thm6 = CONV_RULE (RAND_CONV new_conv) thm5 2881 in 2882 thm6 2883 end 2884 else raise UNCHANGED; 2885 in 2886 thm2 2887 end else if is_exists1 t then 2888 let 2889 val (v,qb) = dest_exists1 t; 2890 2891 val guessC = correct_guess_collection v qb 2892 (heuristic ctx v qb); 2893 2894 val guess = first guess_has_thm_no_free_vars (#exists_gap guessC) handle HOL_ERR _ => 2895 first guess_has_thm_no_free_vars (#exists_point guessC) handle HOL_ERR _ => 2896 first guess_has_thm_no_free_vars (#exists guessC) handle HOL_ERR _ => 2897 raise UNCHANGED; 2898 2899 val (_, proof) = guess2thm guess 2900 val thm = if is_guess_thm gty_exists_gap guess then 2901 HO_MATCH_MP GUESSES_UEXISTS_THM2 proof 2902 else if is_guess_thm gty_exists_point guess then 2903 HO_MATCH_MP GUESSES_UEXISTS_THM3 proof 2904 else if is_guess_thm gty_exists guess then 2905 HO_MATCH_MP GUESSES_UEXISTS_THM1 proof 2906 else Feedback.fail() 2907 val thm2 = CONV_RULE (RHS_CONV (BOOL_SIMP_CONV rwL guessC)) thm 2908 in 2909 thm2 2910 end else raise UNCHANGED) 2911 handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => 2912 raise UNCHANGED 2913end; 2914 2915 2916 2917fun HEURISTIC_QUANT_INSTANTIATE_CONV re min_occs heuristic expand_eq rwL ctx = 2918 (if re then REDEPTH_CONV else DEPTH_CONV) 2919(CHANGED_CONV (QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (true,true,expand_eq) min_occs heuristic rwL ctx CONSEQ_CONV_UNKNOWN_direction)) THENC 2920REWRITE_CONV rwL; 2921 2922 2923 2924 2925(********************************************************) 2926(* Provide High level interfaces *) 2927(********************************************************) 2928 2929(***************************************************** 2930 * One of the most basic conversions. 2931 * 2932 * It get's the following arguments: 2933 * 2934 * - cache_ref_opt 2935 * a possible reference to a cache which stores 2936 * previously found guesses. A new cache can be 2937 * created using mk_quant_heuristic_cache 2938 * 2939 * - re : bool 2940 * redescent into a term some intantiation has been found? 2941 * similar to DEPTH_CONV and REDEPTH_CONV 2942 * 2943 * - min_occs 2944 * should occurences of the variable be tried to be removed in 2945 * a preprocessing step? 2946 * 2947 * - expand_eq : bool 2948 * all build in heuristics provide proofs with all guesses 2949 * if no proof is provided by user defined heuristics this 2950 * argument can be set to true to do a case split instead 2951 * 2952 * - args 2953 * a list of quant_params 2954 *****************************************************) 2955 2956fun EXTENSIBLE_QUANT_INSTANTIATE_CONV cache_ref_opt re min_occs expand_eq ctx bqp args = 2957 let val arg = (combine_qps (bqp::args)) in 2958 HEURISTIC_QUANT_INSTANTIATE_CONV re min_occs (qp_to_heuristic arg cache_ref_opt) expand_eq (#final_rewrite_thms arg) ctx 2959 end 2960 2961(* 2962val hL = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE arg 2963 2964(el 9 hL) dummy_sys v t 2965 2966QUANT_INSTANTIATE_HEURISTIC___COMBINE hL NONE v t 2967 2968(QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE arg NONE) v t 2969 2970val (cache_ref_opt, re, filter, min_occs, expand_eq, args) = 2971 (NONE, true, (K true), true, false, [pair_default_qp]) 2972*) 2973 2974 2975 2976 2977(****************************************************************** 2978 * A simpler interface, here just the quant_params list is needed 2979 ******************************************************************) 2980val QUANT_INSTANTIATE_CONV = 2981 EXTENSIBLE_QUANT_INSTANTIATE_CONV NONE true true false [] basic_qp 2982 2983val NORE_QUANT_INSTANTIATE_CONV = 2984 EXTENSIBLE_QUANT_INSTANTIATE_CONV NONE false true false [] basic_qp 2985 2986val FAST_QUANT_INSTANTIATE_CONV = 2987 EXTENSIBLE_QUANT_INSTANTIATE_CONV NONE false false false [] basic_qp 2988 2989val EXPAND_QUANT_INSTANTIATE_CONV = 2990 EXTENSIBLE_QUANT_INSTANTIATE_CONV NONE true true true [] basic_qp 2991 2992val NORE_EXPAND_QUANT_INSTANTIATE_CONV = 2993 EXTENSIBLE_QUANT_INSTANTIATE_CONV NONE false true true [] basic_qp 2994 2995val FAST_EXPAND_QUANT_INSTANTIATE_CONV = 2996 EXTENSIBLE_QUANT_INSTANTIATE_CONV NONE false false true [] basic_qp 2997 2998 2999fun QUANT_INSTANTIATE_REDUCER cache_ref_opt re min_occs expand_eq bqp qpL = 3000 let exception FACTDB of thm list; 3001 fun get_db e = (raise e) handle FACTDB thms => thms 3002 in Traverse.REDUCER 3003 {name=SOME"QUANT_INSTANTIATE", 3004 initial = FACTDB [], 3005 apply=(fn r => fn t => 3006 let 3007 val thms = get_db (#context r); 3008 val res = EXTENSIBLE_QUANT_INSTANTIATE_CONV cache_ref_opt re min_occs expand_eq thms bqp qpL t; 3009 in 3010 res 3011 end handle UNCHANGED => fail()), 3012 addcontext=(fn (ctxt,thms) => (FACTDB (thms @ (get_db ctxt))))} 3013 end; 3014 3015fun EXTENSIBLE_QUANT_INST_ss cache_ref_opt re min_occs expand_eq bqp qpL = 3016 simpLib.dproc_ss (QUANT_INSTANTIATE_REDUCER cache_ref_opt re min_occs expand_eq bqp qpL) 3017 3018fun QUANT_INST_ss qpL = EXTENSIBLE_QUANT_INST_ss NONE false true false basic_qp qpL 3019fun EXPAND_QUANT_INST_ss qpL = EXTENSIBLE_QUANT_INST_ss NONE false true true basic_qp qpL 3020fun FAST_QUANT_INST_ss qpL = EXTENSIBLE_QUANT_INST_ss NONE false false false basic_qp qpL 3021 3022fun QUANT_INSTANTIATE_TAC L = CONV_TAC (QUANT_INSTANTIATE_CONV L); 3023fun FAST_QUANT_INSTANTIATE_TAC L = CONV_TAC (FAST_QUANT_INSTANTIATE_CONV L); 3024fun ASM_QUANT_INSTANTIATE_TAC L = DISCH_ASM_CONV_TAC (QUANT_INSTANTIATE_CONV L); 3025fun FAST_ASM_QUANT_INSTANTIATE_TAC L = DISCH_ASM_CONV_TAC (FAST_QUANT_INSTANTIATE_CONV L); 3026 3027 3028(****************************************************************** 3029 * Interfaces for consequence conversions 3030 ******************************************************************) 3031 3032fun HEURISTIC_QUANT_INSTANTIATE_CONSEQ_CONV re min_occs heuristic rwL dir = 3033THEN_CONSEQ_CONV 3034((if re then CONTEXT_REDEPTH_CONSEQ_CONV else CONTEXT_DEPTH_CONSEQ_CONV) CONSEQ_CONV_IMP_CONTEXT 3035 (QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (false,true,false) min_occs heuristic rwL) dir) 3036(REWRITE_CONV rwL); 3037 3038fun EXTENSIBLE_QUANT_INSTANTIATE_CONSEQ_CONV cache_ref_opt re min_occs bqp args = 3039 let val arg = (combine_qps (bqp::args)) in 3040 HEURISTIC_QUANT_INSTANTIATE_CONSEQ_CONV re min_occs (qp_to_heuristic 3041 arg cache_ref_opt) (#final_rewrite_thms arg) end; 3042 3043fun EXTENSIBLE_QUANT_INSTANTIATE_STEP_CONSEQ_CONV cache_ref_opt min_occs bqp args = 3044 let val arg = (combine_qps (bqp::args)) in 3045 (QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (false,true,false) min_occs 3046 (qp_to_heuristic arg cache_ref_opt) 3047 (#final_rewrite_thms arg) []) end; 3048 3049val NORE_QUANT_INSTANTIATE_CONSEQ_CONV = 3050 EXTENSIBLE_QUANT_INSTANTIATE_CONSEQ_CONV NONE false false basic_qp 3051 3052val QUANT_INSTANTIATE_CONSEQ_CONV = 3053 EXTENSIBLE_QUANT_INSTANTIATE_CONSEQ_CONV NONE true true basic_qp 3054 3055val FAST_QUANT_INSTANTIATE_CONSEQ_CONV = 3056 EXTENSIBLE_QUANT_INSTANTIATE_CONSEQ_CONV NONE false false basic_qp 3057 3058fun QUANT_INSTANTIATE_CONSEQ_TAC L = 3059 DISCH_ASM_CONSEQ_CONV_TAC (QUANT_INSTANTIATE_CONSEQ_CONV L); 3060 3061 3062(********************************************************************* 3063 * Oracle heuristic 3064 * 3065 * This heuristic produces unjustified guesses. If explicitly asked, 3066 * guesses are tried to be justified by METIS 3067 **********************************************************************) 3068fun QUANT_INSTANTIATE_HEURISTIC___ORACLE try_proof ml_callback ctx sys v t = 3069let 3070 val res_opt = ml_callback ctx v t; 3071 val (i, fvL) = if isSome res_opt then valOf res_opt else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 3072in 3073 if not try_proof then 3074 {rewrites = [], 3075 general = [guess_general (i,fvL)], 3076 exists_point = [], 3077 forall_point = [], 3078 forall = [], 3079 exists = [], 3080 forall_gap = [], 3081 exists_gap = []} 3082 else 3083 {rewrites = [], 3084 general = [], 3085 exists_point = [], 3086 forall_point = [], 3087 forall = [make_guess___rewrite gty_forall v t i fvL] handle HOL_ERR _ => [], 3088 exists = [make_guess___rewrite gty_exists v t i fvL] handle HOL_ERR _ => [], 3089 forall_gap = [], 3090 exists_gap = []} 3091end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 3092 3093fun oracle_qp ml_callback = top_heuristics_qp [ 3094 QUANT_INSTANTIATE_HEURISTIC___ORACLE false (fn _ => ml_callback) []] 3095 3096fun context_oracle_qp ml_callback = context_top_heuristics_qp [ 3097 QUANT_INSTANTIATE_HEURISTIC___ORACLE false ml_callback] 3098 3099(***************************************************************** 3100 * Predefined filters 3101 *****************************************************************) 3102 3103fun type_match_filter tyL v (t:term) = 3104 let 3105 val ty' = type_of v; 3106 val _ = tryfind (fn ty => match_type ty ty') tyL; 3107 in true end handle HOL_ERR _ => false; 3108 3109 3110fun type_filter tyL v (t:term) = 3111 let 3112 val ty' = type_of v; 3113 val _ = tryfind (fn ty => ty = ty') tyL; 3114 in true end handle HOL_ERR _ => false; 3115 3116fun subterm_match_filter tL (v:term) t = 3117 can (find_term (fn t' => exists (can (fn t'' => match_term t'' t')) tL)) t 3118 3119fun subterm_filter tL (v:term) t = 3120 can (find_term (fn t' => exists (aconv t') tL)) t 3121 3122fun neg_filter f (v:term) (t:term) = not (f v t) 3123 3124 3125(********************************************************************* 3126 * Instantiate quantifiers by explicitly given guesses 3127 * 3128 * QUANT_INST_TAC / QUANT_INST_CONV are able to 3129 * instantiate quantifiers at subpositions. 3130 * They get a list of trible consisting of 3131 * (name_of_var, instantiation, list of free variables instantiation). 3132 * They then try to (partially) instantiate the named variables 3133 * with the given instantiations. 3134 **********************************************************************) 3135 3136(* 3137val t = ``t = 0`` 3138val v = ``x:num`` 3139val ctxt = [] 3140val try_proof = false; 3141val L = [("x", `0`, []), ("t", `xxx n`:term frag list, ["n"])] 3142val L = [("pdata'", `idata_h::pdata22`:term frag list, [`pdata22`]), 3143 ("idata'", `idata_t`, [])] 3144*) 3145 3146 3147fun QUANT_INSTANTIATE_HEURISTIC___LIST_callback ctxt L _ v t = 3148let 3149 val (v_name, v_type) = dest_var v 3150 val (_,i_quot,free_vars_quot) = first (fn (p,_,_) => (p = v_name)) L; 3151 3152 val i_quot' = QUOTE "(" :: (i_quot @ [QUOTE "):", ANTIQUOTE(ty_antiq v_type), QUOTE ""]); 3153 3154 val ctxt = append (Term.free_vars t) ctxt; 3155 val i = Parse.parse_in_context ctxt i_quot'; 3156 val ctxt = append (Term.free_vars i) ctxt; 3157 3158 val fvL = map (fn s => Parse.parse_in_context ctxt s) free_vars_quot; 3159in 3160 SOME (i, fvL) 3161end; 3162 3163 3164fun QUANT_INSTANTIATE_HEURISTIC___LIST ctxt try_proof L v t = 3165 QUANT_INSTANTIATE_HEURISTIC___ORACLE try_proof (QUANT_INSTANTIATE_HEURISTIC___LIST_callback ctxt L) () [] v t 3166 3167fun QUANT_TAC L (asm,t) = 3168 let 3169 val ctxt = HOLset.listItems (FVL (t::asm) empty_tmset); 3170 in 3171 REDEPTH_CONSEQ_CONV_TAC 3172 (QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (false,false,false) 3173 false (K (QUANT_INSTANTIATE_HEURISTIC___LIST ctxt false L)) [] []) 3174 (asm,t) 3175 end; 3176 3177fun INST_QUANT_CONV L t = 3178 let 3179 val ctxt = HOLset.listItems (FVL [t] empty_tmset); 3180 in 3181 DEPTH_CONV 3182 (QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (true,true,false) 3183 false (K (QUANT_INSTANTIATE_HEURISTIC___LIST ctxt true L)) [] [] CONSEQ_CONV_UNKNOWN_direction) 3184 t 3185 end; 3186 3187end 3188