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 Teq t2 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 => tmem 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:term, fvL),g)::gL)::gLL) = 644let 645 val already_present = 646 tml_eq fvL [i] orelse 647 exists (fn ((i', fvL'), _) => i ~~ i' andalso tml_eq fvL fvL') r 648 val r' = if already_present then r else ((i, fvL), g)::r 649in 650 elim_double_guesses_int r' (gL::gLL) 651end; 652 653fun elim_double_guesses gL = 654let 655 val gL' = map (fn g => (guess_extract g, g)) gL 656 val (gL1, gL2) = partition (fn ((_,_),g) => 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 () 815 else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 816 val (l,r) = dest_eq t 817 818 val (turn,top,i,s) = 819 if (l ~~ v) then (false, true, r,r) 820 else if (r ~~ v) then (true, true, l,l) 821 else 822 (false, false, match_term_var v l r, r) 823 handle HOL_ERR _ => 824 (true, false, match_term_var v r l, l) 825 handle HOL_ERR _ => 826 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 827 828 val _ = if (free_in v i) then Feedback.fail () else (); 829 val u_genvar = genvar unit_ty; 830 831 val g_exists_pointL = let 832 val v_l = mk_abs (v, l); 833 val v_r = mk_abs (v, r); 834 val g_exists_point_thm = ISPECL [i, v_l, v_r] (intro_fresh_ty_vars GUESS_RULES_EQUATION_EXISTS_POINT) 835 val g_exists_point_thm2 = CONV_RULE ( 836 RATOR_CONV (RAND_CONV (BINOP_CONV BETA_CONV)) THENC 837 RAND_CONV (RAND_CONV (ALPHA_CONV v THENC (ABS_CONV ((BINOP_CONV BETA_CONV)))))) g_exists_point_thm 838 val pre = (lhs o fst o dest_imp o concl) g_exists_point_thm2; 839 val g_exists_point_thm3 = MP g_exists_point_thm2 (REFL pre) 840 val g_exists_point_thm4 = CONV_RULE (RATOR_CONV (RAND_CONV (ALPHA_CONV u_genvar))) g_exists_point_thm3 841 in 842 [guess_thm (gty_exists_point, i, [], g_exists_point_thm4)] 843 end 844 845 val g_exists_gapL = if not top then [] else let 846 val g_thm0 = ISPEC i GUESS_RULES_EQUATION_EXISTS_GAP; 847 val g_thm1 = if turn then CONV_RULE (RAND_CONV (ABS_CONV SYM_CONV)) g_thm0 else g_thm0 848 val g_thm2 = CONV_RULE (RAND_CONV (ALPHA_CONV v)) g_thm1 849 val g_thm3 = CONV_RULE (RATOR_CONV (RAND_CONV (ALPHA_CONV u_genvar))) g_thm2 850 in 851 [guess_thm (gty_exists_gap, i, [], g_thm3)] 852 end 853in 854 {rewrites = [], 855 general = [], 856 exists_point = g_exists_pointL, 857 forall_point = [], 858 forall = [], 859 exists = [], 860 forall_gap = [], 861 exists_gap = g_exists_gapL}:guess_collection 862end; 863 864 865(********************************************* 866 * Heuristic for monochotomies and dichotomies 867 *********************************************) 868 869fun prefix_free_vars (prefix, fvL, i) = 870let 871 val fvL' = map (fn x => let 872 val (x_name, x_ty) = dest_var x; 873 val x'_name = prefix ^ "_"^x_name; 874 in 875 (mk_var (x'_name, x_ty)) 876 end) fvL 877 val i' = subst (map (fn (x,x') => (x |-> x')) (zip fvL fvL')) i; 878in 879 (fvL', i') 880end; 881 882(* 883 val t = ``l:'a list = []``; 884 val v = ``l:'a list``; 885 val fv = []; 886 val sys = NONE; 887 val thm = TypeBase.nchotomy_of ``:'a list``; 888*) 889 890fun QUANT_INSTANTIATE_HEURISTIC___EQUATION_two_cases thm sys v t = 891let 892 val _ = if is_eq t then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 893 val (l,r) = dest_eq t; 894 895 val (i,turn) = if (l ~~ v) then (r,false) else 896 if (r ~~ v) then (l,true) else 897 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 898 899 val thm' = ISPEC v (intro_fresh_ty_vars thm); 900 val (eeq1,eeq2) = dest_disj (concl thm'); 901 val left_right_flag = 902 if is_eq eeq1 andalso lhs eeq1 ~~ v andalso rhs eeq1 ~~ i then false 903 else if is_eq eeq2 andalso lhs eeq2 ~~ v andalso rhs eeq2 ~~ i then true 904 else Feedback.fail () 905 val (eeq1,eeq2,thm2) = if left_right_flag then 906 (eeq2, eeq1, CONV_RULE (PART_MATCH lhs DISJ_COMM) thm') else 907 (eeq1, eeq2, thm') 908 909 val (fvL, eeq2b) = strip_exists eeq2; 910 val (v',ni) = dest_eq eeq2b; 911 val _ = if v ~~ v' then () 912 else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 913 914 val v_name = (fst o dest_var) v 915 val (fvL', ni') = prefix_free_vars (v_name, fvL, ni); 916 917 val thm3 = GEN v (CONV_RULE (RAND_CONV (INTRO_TUPLED_QUANT_CONV THENC 918 RAND_CONV PABS_ELIM_CONV)) thm2) 919 val g_thm0 = HO_MATCH_MP GUESS_RULES_TWO_CASES thm3 920 val g_thm = if not turn then g_thm0 else 921 CONV_RULE (RAND_CONV (ABS_CONV SYM_CONV)) g_thm0 922 923 val guess = guess_thm(gty_forall_gap, ni', fvL', g_thm); 924in 925 {rewrites = [], 926 general = [], 927 exists_point = [], 928 forall_point = [], 929 forall = [], 930 exists = [], 931 forall_gap = [guess], 932 exists_gap = []}:guess_collection 933end handle UNCHANGED => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 934 | HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 935 936(* 937val v = ``X:('a # 'b)`` 938val t = ``(P (X:('a # 'b))):bool`` 939val thm = TypeBase.nchotomy_of (type_of v) 940val sys = dummy_sys 941val thm = GEN v thm0 942*) 943 944fun QUANT_INSTANTIATE_HEURISTIC___one_case thm sys v t = 945let 946 val (vars, v_eq_i) = (strip_exists o snd o dest_forall o concl) thm; 947 val (_,i) = dest_eq v_eq_i 948 949 val v_name = (fst o dest_var) v 950 val (vars', i') = prefix_free_vars (v_name, vars, i); 951 952 val thm2 = CONV_RULE (QUANT_CONV ((INTRO_TUPLED_QUANT_CONV THENC 953 RAND_CONV PABS_ELIM_CONV))) thm 954 955 val g_thm0 = ISPEC (mk_abs (v, t)) 956 (HO_MATCH_MP GUESS_RULES_ONE_CASE___FORALL_GAP thm2) 957 val g_thm1 = ISPEC (mk_abs (v, t)) 958 (HO_MATCH_MP GUESS_RULES_ONE_CASE___EXISTS_GAP thm2) 959 960 val g0 = guess_thm (gty_forall_gap, i',vars', g_thm0); 961 val g1 = guess_thm (gty_exists_gap, i',vars', g_thm1); 962 963in 964 {rewrites = [], 965 general = [], 966 exists_point = [], 967 forall_point = [], 968 forall = [], 969 exists = [], 970 forall_gap = [g0], 971 exists_gap = [g1]}:guess_collection 972end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 973 974 975local 976 fun QUANT_INSTANTIATE_HEURISTIC___FAIL sys v t = 977 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 978 979 fun dest_ex_eq tt = 980 let 981 val (vars, eq) = strip_exists tt; 982 val (l, r) = dest_eq eq; 983 in 984 (vars, l, r) 985 end; 986 987 fun is_sing_case_thm thm = 988 let 989 val (v, b) = dest_forall (concl thm); 990 val (_, l, _) = dest_ex_eq b; 991 val _ = (if (aconv v l) then () else Feedback.fail()) 992 in 993 true 994 end handle HOL_ERR _ => false; 995 996 fun is_double_case_thm thm = 997 let 998 val (v, b) = dest_forall (concl thm); 999 val (b1, b2) = dest_disj b; 1000 val (_, l1, _) = dest_ex_eq b1; 1001 val (_, l2, _) = dest_ex_eq b2; 1002 val _ = (if (aconv v l1) then () else Feedback.fail()) 1003 val _ = (if (aconv v l2) then () else Feedback.fail()) 1004 in 1005 true 1006 end handle HOL_ERR _ => false; 1007 1008 fun is_disj_case_thm thm = 1009 let 1010 val (v, b) = dest_forall (concl thm); 1011 val (b1, b2) = dest_disj b; 1012 in 1013 not (is_double_case_thm thm) 1014 end handle HOL_ERR _ => false; 1015 1016in 1017 fun QUANT_INSTANTIATE_HEURISTIC___cases thm = 1018 let 1019 in 1020 if is_sing_case_thm thm then 1021 QUANT_INSTANTIATE_HEURISTIC___one_case thm 1022 else if is_double_case_thm thm then 1023 QUANT_INSTANTIATE_HEURISTIC___EQUATION_two_cases thm 1024 else 1025 QUANT_INSTANTIATE_HEURISTIC___FAIL 1026 end; 1027 1028 1029 fun QUANT_INSTANTIATE_HEURISTIC___cases_list thmL = 1030 let 1031 val thmL1 = filter is_sing_case_thm thmL 1032 val thmL2 = filter is_double_case_thm thmL 1033 val thmL3 = filter is_disj_case_thm thmL 1034 1035 val hL1 = map QUANT_INSTANTIATE_HEURISTIC___one_case thmL1; 1036 val hL2 = map QUANT_INSTANTIATE_HEURISTIC___EQUATION_two_cases thmL2; 1037 in 1038 (hL1, hL2, thmL3) 1039 end 1040end; 1041 1042 1043 1044fun QUANT_INSTANTIATE_HEURISTIC___TypeBase_cases sys v t = 1045if not (is_eq t) then raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp else 1046(let 1047 val thm = TypeBase.nchotomy_of (type_of v) 1048in 1049 QUANT_INSTANTIATE_HEURISTIC___cases thm sys v t 1050end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp); 1051 1052 1053(********************************* 1054 * Another Heuristic for dichotomies 1055 *********************************) 1056(* 1057 val t = ``n = x:num``; 1058 val t = ``x = n:num``; 1059 val v = ``x:num``; 1060 val fv = [``x_n``]; 1061 val sys = NONE; 1062 val thmL = [GSYM prim_recTheory.SUC_ID] 1063 1064 val t = ``[] = l:'a list``; 1065 val v = ``l:'a list`` 1066 val thmL = [rich_listTheory.NOT_CONS_NIL] 1067 1068 val t = ``0 = x`` 1069*) 1070fun QUANT_INSTANTIATE_HEURISTIC___EQUATION_distinct thmL sys v t = 1071let 1072 val _ = if is_eq t then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1073 val (l,r) = dest_eq t; 1074 1075 val (i,turn) = if (l ~~ v) then (r,false) else 1076 if (r ~~ v) then (l,true) else 1077 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1078 1079 val thmL' = flatten (map BODY_CONJUNCTS thmL) 1080 val thmL'' = append thmL' (map GSYM thmL'); 1081 1082 val ni_thm = tryfind (fn thm => PART_MATCH (rhs o dest_neg) thm i) thmL''; 1083 val ni = (lhs o dest_neg o concl) ni_thm; 1084 1085 1086 val fvL_set = HOLset.difference (FVL [ni] empty_tmset, FVL [i] empty_tmset) 1087 val fvL_org = HOLset.listItems fvL_set 1088 val v_name = (fst o dest_var) v 1089 val (fvL, ni) = prefix_free_vars (v_name, fvL_org, ni); 1090 val fvL_org = if null fvL_org then [genvar unit_ty] else fvL_org; 1091 val ni_thm2 = GENL fvL_org ni_thm 1092 val ni_thm3 = CONV_RULE (INTRO_TUPLED_QUANT_CONV THENC 1093 RAND_CONV PABS_ELIM_CONV) ni_thm2 1094 1095 1096 val g_thm = let 1097 val (i_v, i_b) = dest_forall (concl ni_thm3); 1098 val i = mk_abs (i_v, lhs (dest_neg i_b)) 1099 val (vl, vr) = (mk_abs(v,l), mk_abs(v,r)); 1100 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) 1101 val g_thm1 = BETA_RULE g_thm0 1102 val g_thm2 = HO_MATCH_MP g_thm1 ni_thm3; 1103 val g_thm3 = CONV_RULE (RAND_CONV 1104 (ALPHA_CONV v THENC 1105 (if (turn) then 1106 (ABS_CONV SYM_CONV) 1107 else ALL_CONV))) g_thm2 1108 in 1109 g_thm3 1110 end 1111 val guess = guess_thm (gty_forall_point, ni, fvL, g_thm); 1112in 1113 {rewrites = [ni_thm], 1114 general = [], 1115 exists_point = [], 1116 forall_point = [guess], 1117 forall = [], 1118 exists = [], 1119 forall_gap = [], 1120 exists_gap = []}:guess_collection 1121end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1122 1123 1124fun QUANT_INSTANTIATE_HEURISTIC___EQUATION___TypeBase_distinct sys v t = 1125let 1126 val _ = if is_eq t then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1127 val thm = TypeBase.distinct_of (type_of v); 1128in 1129 QUANT_INSTANTIATE_HEURISTIC___EQUATION_distinct [thm] sys v t 1130end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1131 1132 1133 1134 1135 1136(********************************* 1137 * Inference Collection 1138 *********************************) 1139 1140(* Some of the heuristics are able to use general theorems to generate guesses. 1141 These theorems should be of the form 1142 1143 ``pre ==> GUESS_TYPE i P`` 1144 1145 For efficiency, it is convient to collect these inference theorems 1146 depending on the type of the conclusion. That is what an inference collection 1147 does. 1148*) 1149 1150type inference_collection = 1151 {exists_point : thm list, 1152 forall_point : thm list, 1153 exists : thm list, 1154 forall : thm list, 1155 exists_gap : thm list, 1156 forall_gap : thm list}; 1157 1158 1159val empty_inference_collection = 1160 {exists_point = [], 1161 forall_point = [], 1162 exists = [], 1163 forall = [], 1164 exists_gap = [], 1165 forall_gap = []}:inference_collection; 1166 1167 1168fun GUESS_THM_list2collection inference_thmL = 1169let 1170 val L0 = flatten (map BODY_CONJUNCTS inference_thmL) 1171 val L1 = map (SIMP_RULE std_ss [combinTheory.K_DEF]) L0; 1172 fun sort_fun (thm, (l1,l2,l3,l4,l5,l6)) = 1173 let 1174 val gtm = (fst o strip_comb o snd o dest_imp o concl) thm 1175 in 1176 if (same_const gtm GUESS_EXISTS_POINT_tm)then 1177 (thm::l1, l2, l3, l4, l5, l6) else 1178 if (same_const gtm GUESS_FORALL_POINT_tm) then 1179 (l1, thm::l2, l3, l4, l5, l6) else 1180 if (same_const gtm GUESS_EXISTS_tm) then 1181 (l1, l2, thm::l3, l4, l5, l6) else 1182 if (same_const gtm GUESS_FORALL_tm) then 1183 (l1, l2, l3, thm::l4, l5, l6) else 1184 if (same_const gtm GUESS_EXISTS_GAP_tm) then 1185 (l1, l2, l3, l4, thm::l5, l6) else 1186 if (same_const gtm GUESS_FORALL_GAP_tm) then 1187 (l1, l2, l3, l4, l5, thm::l6) else 1188 (l1, l2, l3, l4, l5, l6) 1189 end handle HOL_ERR _ => (l1,l2,l3,l4,l5,l6) 1190 1191 val (l1,l2,l3,l4,l5,l6) = foldl sort_fun ([],[],[],[],[],[]) L1; 1192in 1193 {exists_point = l1, 1194 forall_point = l2, 1195 exists = l3, 1196 forall = l4, 1197 exists_gap = l5, 1198 forall_gap = l6 }:inference_collection 1199end; 1200 1201 1202 1203(********************************* 1204 * Heuristics for Quantifiers 1205 *********************************) 1206 1207(* 1208val t = ``!x. P x /\ (y = 2 + x) /\ Q y`` 1209val t = ``?x. P x /\ (y = 2) /\ Q y`` 1210val v = ``y:num`` 1211 1212val t = ``?y:'b. x:'a = f y`` 1213val v = ``x:'a`` 1214val sys = dummy_sys 1215val sys = heuristic 1216*) 1217 1218 1219local 1220 fun col (L1,L2,L3) = 1221 (GUESS_THM_list2collection [L1], 1222 GUESS_THM_list2collection [L2], 1223 GUESS_THM_list2collection [L3]); 1224 1225 1226 val f_icL = col (GUESS_RULES_FORALL, GUESS_RULES_FORALL___NEW_FV, GUESS_RULES_FORALL___NEW_FV_1); 1227 val e_icL = col (GUESS_RULES_EXISTS, GUESS_RULES_EXISTS___NEW_FV, GUESS_RULES_EXISTS___NEW_FV_1); 1228 val u_icL = col (GUESS_RULES_EXISTS_UNIQUE, TRUTH, TRUTH); 1229in 1230 1231fun QUANT_INSTANTIATE_HEURISTIC___QUANT allow_new_fv sys (v:term) t = 1232let 1233 val ((ic, ic_fv, ic_fv_1), (v2, b)) = 1234 (f_icL, dest_forall t) handle HOL_ERR _ => 1235 (e_icL, dest_exists t) handle HOL_ERR _ => 1236 (u_icL, dest_exists1 t) handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1237 1238 val gc:guess_collection = sys v b 1239 1240 fun apply_inference inf guess = 1241 let 1242 val (_, i, fvL, gthm0, was_thm) = guess_extract_thm guess; 1243 val gthm = GEN_ASSUM v2 gthm0; 1244 val new_fv = free_in v2 i 1245 val _ = if new_fv andalso not allow_new_fv then Feedback.fail() else (); 1246 val use_ic = if new_fv then (if null fvL then ic_fv_1 else ic_fv) else ic; 1247 val inf_thm = hd (inf use_ic) handle Empty => Feedback.fail(); 1248 val xthm2 = HO_MATCH_MP inf_thm gthm 1249 in 1250 SOME (guess_thm_to_guess was_thm (SOME (i, if new_fv then v2::fvL else fvL)) xthm2) 1251 end handle HOL_ERR _ => NONE; 1252 1253 val results = flatten (map (fn (s1, s2) => mapPartial (apply_inference s2) (s1 gc)) [ 1254 (#exists_point, #exists_point), 1255 (#forall_point, #forall_point), 1256 (#exists, #exists), 1257 (#forall, #forall), 1258 (#exists_gap, #exists_gap), 1259 (#forall_gap, #forall_gap)]) 1260in 1261 guess_list2collection ([], results) 1262end; 1263 1264end 1265 1266 1267(******************************************************************************) 1268(* General heuristic for moving guesses over structure *) 1269(******************************************************************************) 1270 1271fun process_simple_guess_thm thm = 1272let 1273 val (pre, ant) = dest_imp (concl thm); 1274 val (gty, i, v, t) = dest_guess_tm ant; 1275 1276 val i_ok = is_var i orelse 1277 let 1278 val (i_v, i_b) = dest_abs i 1279 in (type_of i_v = unit_ty) andalso (is_var i_b) end 1280 val _ = if (i_ok) then () else Feedback.fail(); 1281 val (_, tL) = strip_comb t 1282 val tL_simple = 1283 all (fn tx => is_var tx orelse 1284 let val (tx_b, tx_v) = dest_comb tx 1285 in 1286 tx_v ~~ v andalso is_var tx_b 1287 end) tL 1288 1289 val preL = strip_conj pre 1290 fun check_internal pre_tm = 1291 let 1292 val (gty', i', v', t') = dest_guess_tm pre_tm 1293 val _ = if i ~~ i' andalso v ~~ v' then () else Feedback.fail() 1294 val index_opt = 1295 SOME (index (fn t'' => t' ~~ t'') tL) handle HOL_ERR _ => NONE 1296 in 1297 (gty', index_opt) 1298 end; 1299 1300 val pre_checkL = map check_internal preL; 1301 val thm' = CONV_RULE AND_IMP_ELIM_CONV thm 1302 1303 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 1304 1305in 1306 SOME (thm', pre_checkL_opt, mk_abs (v, t), i, gty) 1307end handle HOL_ERR _ => NONE; 1308 1309fun process_simple_guess_thm_warn thm = 1310let 1311 val r_opt = process_simple_guess_thm thm; 1312 val _ = if isSome r_opt then () else 1313 say_HOL_WARNING "process_simple_guess_thm" 1314 ("Inference theorem not well formed:\n"^(thm_to_string thm)) 1315in 1316 r_opt 1317end; 1318 1319 1320fun mk_guess_net guesses_thmL = 1321let 1322 fun fresh_vars thm = 1323 SIMP_RULE std_ss [combinTheory.K_DEF] (genvar_RULE thm) 1324 1325 val thmL0 = flatten (map (BODY_CONJUNCTS o fresh_vars) guesses_thmL) 1326 val thmL1 = mapPartial process_simple_guess_thm_warn thmL0 1327 1328 val (sL, cL) = partition (fn (_, opt, _, _, _) => isSome opt) thmL1 1329 1330 (* make guess_net for complex theorems *) 1331 fun group_thmL L [] = L 1332 | group_thmL L ((thm, _, P_t, _, _)::thmPL) = 1333 let 1334 val ((P_t', thmL), L') = 1335 pluck (fn (P_t', thmL) => P_t ~~ P_t') L 1336 handle HOL_ERR _ => ((P_t, []), L) 1337 in 1338 group_thmL ((P_t', thm::thmL)::L') thmPL 1339 end 1340 val guess_net_complex = 1341 foldr (fn ((P_t, thmL), n) => Ho_Net.enter ([],P_t, (P_t, thmL)) n) Ho_Net.empty 1342 (group_thmL [] cL) 1343 1344 1345 (* make guess_net for simple theorems *) 1346 fun free_var_process (thm, pre_checkL_opt, v_t, i, gty) = 1347 let 1348 val (v, t) = dest_abs v_t; 1349 val (b_op, tL) = strip_comb t; 1350 1351 val pre_checkL = valOf pre_checkL_opt 1352 fun remove_free_var (n, tx) = is_comb tx andalso 1353 all (fn (ty, n') => (not (n = n')) orelse ((ty = gty_forall) orelse (ty = gty_exists))) 1354 pre_checkL 1355 1356 val ntL = enumerate 0 tL; 1357 val remove_varsL = filter remove_free_var ntL; 1358 1359 fun remove_vars_combins [] = [[]] 1360 | remove_vars_combins (x::xs) = 1361 let 1362 val L = remove_vars_combins xs 1363 in 1364 (map (fn z1 => x::z1) L) @ L 1365 end; 1366 val combs = remove_vars_combins remove_varsL 1367 1368 fun apply_combs cL = 1369 let 1370 val pre_checkL' = filter (fn (_,n) => all (fn (n', _) => not (n = n')) cL) pre_checkL 1371 fun mk_tL (sub,tL') [] = (sub, rev tL') 1372 | mk_tL (sub,tL') ((n, tx)::ntL) = 1373 let 1374 val do_remove = exists (fn (n', _) => n = n') cL 1375 val (sub', tL'') = if not do_remove then (sub, tx::tL') else 1376 let 1377 val (tx_b, tx_v) = dest_comb tx; 1378 val tx' = genvar (type_of tx); 1379 1380 in 1381 ((tx_b |-> mk_abs(tx_v, tx'))::sub, tx'::tL') 1382 end; 1383 in 1384 mk_tL (sub', tL'') ntL 1385 end; 1386 val (sub, tL') = mk_tL ([], []) ntL; 1387 val tL'' = map (fn tx => (true, fst (dest_comb tx)) handle HOL_ERR _ => (false, tx)) tL' 1388 val _ = if exists fst tL'' then () else Feedback.fail(); 1389 1390 val xthm0 = SIMP_RULE std_ss [GUESS_RULES_CONSTANT_FORALL, GUESS_RULES_CONSTANT_EXISTS, ETA_THM] (INST sub thm) 1391 1392 val (i_f, i_v) = if is_abs i then (false, snd (dest_abs i)) else (true, i) 1393 1394 val xthm1 = GENL (i_v::(map snd tL'')) xthm0 1395 in 1396 SOME (b_op, (i_f, map fst tL'', pre_checkL', gty, xthm1)) 1397 end handle HOL_ERR _ => NONE; 1398 in 1399 mapPartial apply_combs combs 1400 end; 1401 fun group_simpleL L [] = L 1402 | group_simpleL L ((tm, x)::tmxs) = 1403 let 1404 val ((_, xL), L') = pluck (fn (tm', _) => (same_const tm tm')) L handle HOL_ERR _ => 1405 ((tm, []), L) 1406 in 1407 group_simpleL ((tm, x::xL)::L') tmxs 1408 end 1409 val guess_net_simple = group_simpleL [] (flatten (map free_var_process sL)) 1410in 1411 (guess_net_complex, guess_net_simple) 1412end; 1413 1414 1415 1416(* 1417 1418val guesses_thmL = inference_thmL; 1419val guesses_net = mk_guess_net guesses_thmL 1420val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp (SOME (ref (mk_quant_heuristic_cache()))) 1421val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE 1422val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE std_qp NONE 1423val sys = heuristic; 1424 1425 1426val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE list_qp NONE 1427val sys = heuristic; 1428 1429val sys = dummy_sys 1430 1431val v = ``x:num`` 1432val t = ``(x = 2) ==> P x`` 1433 1434sys v t 1435 1436 1437val v = ``x:'a list`` 1438val t = ``Q ==> (~((x:'a list) = []) /\ P x)`` 1439 1440sys v t 1441GUESS_RULES_IMP 1442 1443val t = ``(x + (y:num) = z) \/ Q y`` 1444 1445val t = ``!x. (x + (y:num) = z) \/ Q y`` 1446 1447 1448val t = ``~(uf (x:'a) = uf y) \/ (P y /\ Q y)`` 1449val v = ``x:'a`` 1450val fv = [v] 1451val t = b 1452 1453 1454QUANT_INSTANTIATE_HEURISTIC___debug := 1455 1456val t = ``~(uf (x:'a) = uf (SND s)) \/ (IS_SOME (e (FST s)) /\ 1457 s IN var_res_prop___PROP f (wpb,rpb) sfb)`` 1458 1459val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE 1460val sys = heuristic; 1461QUANT_INSTANTIATE_HEURISTIC___print_term_length := 2000 1462*) 1463 1464fun strip_comb_abs t = 1465 let 1466 val (t1, t2) = dest_comb t; 1467 val (_, t3) = dest_abs t1; 1468 in 1469 strip_comb_abs t3 1470 end handle HOL_ERR _ => t; 1471 1472 1473fun dest_comb_abs fv fb = 1474 let 1475 val (t1, t2) = dest_comb fb 1476 val _ = if t2 ~~ fv then () else Feedback.fail() 1477 val t3 = strip_comb_abs t1 1478 val (fv', _) = dest_abs t3 1479 in 1480 fv' 1481 end 1482 1483fun get_org_name fv fb = 1484 dest_comb_abs fv (find_term (can (dest_comb_abs fv)) fb) handle HOL_ERR _ => fv; 1485 1486 1487 1488fun local_cache_sys sys = 1489 let 1490 val lc_ref = ref [] 1491 in fn v => fn t => 1492 let 1493 val gc_opt = tassoc t (!lc_ref) 1494 in 1495 if (isSome gc_opt) then valOf gc_opt 1496 else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 1497 end handle HOL_ERR _ => 1498 let 1499 val gc_opt = SOME (sys v t) handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => NONE 1500 | HOL_ERR _ => NONE; 1501 val _ = lc_ref := (t,gc_opt)::(!lc_ref); 1502 in 1503 if (isSome gc_opt) then valOf gc_opt 1504 else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 1505 1506 end 1507end; 1508 1509 1510 1511local 1512 fun exists_forall_CONV t = 1513 HO_REWR_CONV GUESS_RULES_CONSTANT_FORALL t handle HOL_ERR _ => 1514 HO_REWR_CONV GUESS_RULES_CONSTANT_EXISTS t 1515 1516 fun guess_rule_elim_constant_RULE v xthm0 = 1517 let 1518 val (_, t') = dest_abs (rand (rhs (concl xthm0))); 1519 in 1520 if (free_in v t') then xthm0 else 1521 CONV_RULE (RHS_CONV exists_forall_CONV) xthm0 1522 end 1523 1524 fun RRAND_CONV c t = 1525 if is_comb t then RAND_CONV (RRAND_CONV c) t else 1526 c t 1527 1528 fun test_thmL v_t_type tvset v t (P_t, thmL) = 1529 let 1530 val ty_m = match_type (type_of P_t) v_t_type 1531 val P_t' = inst ty_m P_t; 1532 val (v'', t'') = dest_abs P_t'; 1533 val t''' = subst [v'' |-> v] t''; 1534 val (term_sub, ty_sub) = ho_match_term [] tvset t''' t 1535 val _ = map (fn xx => if (free_in v (#residue xx)) then Feedback.fail() else ()) 1536 (term_sub) 1537 1538 val P_t'' = subst term_sub (inst ty_sub P_t'); 1539 val eq_thm0 = ((ALPHA_CONV v) THENC (DEPTH_CONV BETA_CONV)) P_t''; 1540 val eq_thm1_opt = SOME ((DEPTH_CONV BETA_CONV) (mk_abs (v, t))) handle UNCHANGED => NONE 1541 1542 val eq_thm = if isSome eq_thm1_opt then 1543 TRANS eq_thm0 (GSYM (valOf eq_thm1_opt)) else eq_thm0 1544 1545 val ty_sub2 = ty_m @ ty_sub; 1546 fun process_thm thm0 = 1547 let 1548 val xthm0 = INST_TY_TERM (term_sub, ty_sub2) thm0; 1549 val xthm1 = CONV_RULE (RRAND_CONV (K eq_thm)) xthm0 1550 in 1551 SOME xthm1 1552 end handle HOL_ERR _ => NONE 1553 1554 val thmL' = mapPartial process_thm thmL 1555 in 1556 thmL' 1557 end handle HOL_ERR _ => []; 1558 1559(* val (thm,gthm,rthm) = el 1 resL *) 1560 1561 fun GUESS_MP thm gthm = 1562 let 1563 val i = (rand o rator o fst o dest_imp o concl) thm; 1564 val gi = (rand o rator o concl) gthm; 1565 in 1566 if is_var i then 1567 let 1568 val i_ty = (hd o snd o dest_type o type_of) i 1569 val gi_ty = (hd o snd o dest_type o type_of) gi 1570 val ty_sub = [i_ty |-> gi_ty]; 1571 val i' = inst ty_sub i; 1572 1573 val xthm0 = INST_TY_TERM ([i' |-> gi], ty_sub) thm 1574 val xthm1 = MP xthm0 gthm 1575 in 1576 xthm1 1577 end 1578 else if (is_var (snd (dest_abs i)) handle HOL_ERR _ => false) then 1579 let 1580 val (i_v, i_b) = dest_abs i; 1581 val (g_v, g_b) = dest_abs gi; 1582 val _ = if free_in g_v g_b then Feedback.fail() else (); 1583 1584 val ty_sub = [type_of i_v |-> type_of g_v]; 1585 1586 val xthm0 = INST_TY_TERM ([i_b |-> g_b], ty_sub) thm 1587 val xthm1 = MP xthm0 gthm 1588 in 1589 xthm1 1590 end 1591 else MP thm gthm 1592 end; 1593 1594 1595 fun try_guess ifv_opt thm_ok thm guess = 1596 let 1597 val (ty, i, fvL, gthm, was_thm) = guess_extract_thm guess; 1598 val (ifv_opt, nthm) = if isSome ifv_opt then 1599 (ifv_opt, GUESS_MP thm gthm) 1600 else (SOME (i, fvL), GUESS_MP thm gthm) 1601 in 1602 SOME (ifv_opt, thm_ok andalso was_thm, nthm) 1603 end handle HOL_ERR _ => NONE; 1604 1605 fun elim_precond sys v (ifv_opt,thm_ok,thm) = 1606 let 1607 val xthm0 = CONV_RULE (RATOR_CONV ( 1608 (RAND_CONV (RAND_CONV (ALPHA_CONV v) THENC DEPTH_CONV BETA_CONV)))) thm 1609 1610 val precond = (fst o dest_imp) (concl xthm0) 1611 val (gty, _, v', t') = dest_guess_tm precond; 1612 in 1613 if (free_in v' t') then 1614 let 1615 val gc:guess_collection = sys v' t'; 1616 val gL = (guess_collection_guess_type gty) gc; 1617 in 1618 mapPartial (try_guess ifv_opt thm_ok xthm0) gL 1619 end else 1620 [(ifv_opt, thm_ok, MP (CONV_RULE (RATOR_CONV (RAND_CONV exists_forall_CONV)) xthm0) TRUTH)] 1621 end handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => [] 1622 | HOL_ERR _ => []; 1623 1624 fun elim_preconds sys v doneL [] = doneL 1625 | elim_preconds sys v doneL (ithm::thmL) = 1626 if (is_imp_only (concl (#3 ithm))) then 1627 elim_preconds sys v doneL (append (elim_precond sys v ithm) thmL) 1628 else 1629 if (isSome (#1 ithm)) then 1630 elim_preconds sys v (ithm::doneL) thmL 1631 else 1632 elim_preconds sys v doneL thmL 1633 1634in 1635 1636fun QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL_COMPLEX guesses_net_complex sys v t = 1637let 1638 val v_t = mk_abs (v, t) 1639 val possible_thmL = Ho_Net.lookup v_t guesses_net_complex 1640 val tvset = FVL [t] empty_tmset 1641 val _ = if v IN tvset then () 1642 else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 1643 1644 val current_thmL = flatten (map (test_thmL (type_of v_t) tvset v t) 1645 possible_thmL) 1646 1647 val sys' = local_cache_sys sys 1648 val results = elim_preconds sys' v [] 1649 (map (fn y => (NONE, true, y)) current_thmL) 1650in 1651 guess_list2collection 1652 ([], (map (fn (ifv_opt, ok, thm) => guess_thm_to_guess ok ifv_opt thm) 1653 results)) 1654end 1655 1656end; 1657 1658 1659 1660(* 1661 1662val guesses_thmL = inference_thmL; 1663val (guesses_net_complex, guesses_net_simple) = mk_guess_net guesses_thmL 1664 1665val (guesses_net_complex, guesses_net_simple) = mk_guess_net[] 1666 1667val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp (SOME (ref (mk_quant_heuristic_cache()))) 1668val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE 1669val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE std_qp NONE 1670val sys = heuristic; 1671 1672 1673val sys = dummy_sys 1674 1675val v = ``z:num`` 1676val t = ``(z = 2) ==> P z`` 1677 1678 1679val v = ``z:num`` 1680val t = ``(z = 2)`` 1681 1682sys v t 1683 1684 1685val v = ``x:'a list`` 1686val t = ``Q ==> (~((x:'a list) = []) /\ P x)`` 1687 1688sys v t 1689GUESS_RULES_IMP 1690 1691val t = ``(x + (y:num) = z) \/ Q y`` 1692 1693val t = ``!x. (x + (y:num) = z) \/ Q y`` 1694 1695 1696val t = ``~(uf (x:'a) = uf y) \/ (P y /\ Q y)`` 1697val v = ``x:'a`` 1698val fv = [v] 1699val t = b 1700val v = ``x:num`` 1701val t = ``if b x then ((x = 2) /\ Q x) else (Q2 x /\ (x = 2))`` 1702 1703QUANT_INSTANTIATE_HEURISTIC___debug := 1704 1705val t = ``~(uf (x:'a) = uf (SND s)) \/ (IS_SOME (e (FST s)) /\ 1706 s IN var_res_prop___PROP f (wpb,rpb) sfb)`` 1707 1708val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE [] 1709val sys = heuristic; 1710 1711sys v t 1712sys v b 1713 1714t b 1715 1716val t = ``Q2 2 /\ (x = 2)`` 1717sys v t 1718 1719QUANT_INSTANTIATE_HEURISTIC___print_term_length := 2000 1720*) 1721 1722local 1723 fun fL_BETA_CONV [] = ALL_CONV 1724 | fL_BETA_CONV (true::fL) = 1725 RAND_CONV BETA_CONV THENC 1726 RATOR_CONV (fL_BETA_CONV fL) 1727 | fL_BETA_CONV (false::fL) = 1728 RATOR_CONV (fL_BETA_CONV fL) 1729 fun tmtml_eq (tm1,tml1) (tm2,tml2) = tm1 ~~ tm2 andalso tml_eq tml1 tml2 1730in 1731 1732fun QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL_SIMPLE guesses_net_simple sys v t = 1733let 1734 val (b_op, tL) = strip_comb t; 1735 val (_, infL) = first (fn (tm, _) => same_const b_op tm) guesses_net_simple; 1736 1737 val fL = map (free_in v) tL 1738 val infL' = filter (fn (_, fL', _, _, _) => fL = fL') infL 1739 val _ = if null infL' then raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp else (); 1740 1741 val gcL = map (fn t => sys v t handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => empty_guess_collection 1742 | HOL_ERR _ => empty_guess_collection) tL; 1743 1744 fun try_inf (i_f, _, pre_checkL, gty, inf_thm) = 1745 let 1746 val (gty1, arg_n1) = hd pre_checkL; 1747 val pre_checkL_tl = tl pre_checkL; 1748 val gL = (guess_collection_guess_type gty1) (el (arg_n1+1) gcL); 1749 1750 fun process_guess guess = 1751 (let 1752 val (i, fvL) = guess_extract guess 1753 val _ = if not i_f andalso not (null fvL) then Feedback.fail() else () 1754 1755 val gL' = 1756 map (fn (gty, n) => 1757 first (fn g => tmtml_eq (guess_extract g) (i, fvL)) 1758 ((guess_collection_guess_type gty) (el (n+1) gcL))) 1759 pre_checkL_tl 1760 1761 val final_gL = guess::gL'; 1762 val do_proof = all guess_has_thm final_gL; 1763 in 1764 if (not do_proof) then SOME (mk_guess gty v t i fvL) else 1765 let 1766 val gthm1 = snd (guess2thm guess); 1767 val i_t = (rand o rator o concl) gthm1; 1768 val i_tv = if i_f then i_t else snd (dest_abs i_t); 1769 val t_vL = map (fn (fv, ttt) => if fv then mk_abs (v, ttt) else ttt) (zip fL tL) 1770 val inf_thm0 = ISPECL (i_tv::t_vL) (intro_fresh_ty_vars inf_thm) 1771 val inf_thm1 = LIST_MP (map (snd o guess2thm) final_gL) inf_thm0 1772 val inf_thm2 = CONV_RULE (RAND_CONV (ALPHA_CONV v THENC 1773 ABS_CONV (fL_BETA_CONV (rev fL)))) inf_thm1 1774 in 1775 SOME (guess_thm (gty, i, fvL, inf_thm2)) 1776 end end) handle HOL_ERR _ => NONE 1777 in 1778 mapPartial process_guess gL 1779 end; 1780 1781 val gL2 = flatten (map try_inf infL') 1782in 1783 guess_list2collection ([], gL2) 1784end handle HOL_ERR _ => empty_guess_collection; 1785 1786end; 1787 1788 1789(******************************************************************************) 1790(* Heuristics that apply conversions *) 1791(******************************************************************************) 1792 1793(* Applying a rewrite rule to a guess *) 1794(* 1795val tref = ref NONE 1796 1797val (v,t,thmL,guess) = valOf (!tref) 1798val fvL = [``x:num``, ``y:num``] 1799val rewrite_thm = GSYM (HO_PART_MATCH lhs (hd thmL) ((fst o dest_imp) (concl thm_org))) 1800val fv = [] 1801 1802val v = ``x:num`` 1803val t = ``!t. (P (x:num) /\ Z t):bool`` 1804val t' = ``!t. X t \/ (Q (x:num))`` 1805val i = ``(i (y:num) (z:num)):num`` 1806val fvL = [``y:num``, ``z:num``] 1807 1808val rew_thm = mk_thm ([], mk_eq(t,t')) 1809 1810val guess = make_set_guess_thm_opt___dummy v t' (guess_forall (i,fvL,NONE)); 1811correct_guess fv v t (guess_rewrite_thm_opt v t rew_thm guess) 1812*) 1813 1814fun guess_rewrite rew_thm (guess_general (i, fvL)) = guess_general (i,fvL) 1815 | guess_rewrite rew_thm (guess_thm (gty, i, fvL, thm)) = 1816 guess_thm (gty, i, fvL, 1817 CONV_RULE (RAND_CONV (ABS_CONV (K (GSYM rew_thm)))) thm) 1818 | guess_rewrite rew_thm (guess_term (gty, i, fvL, tm)) = 1819 guess_term (gty, i, fvL, 1820 (rhs o concl) (RAND_CONV (ABS_CONV (K (GSYM rew_thm))) tm)) 1821 1822 1823fun QUANT_INSTANTIATE_HEURISTIC___REWRITE sys (v:term) rew_thm = 1824let 1825 val (lt,rt) = dest_eq (concl rew_thm); 1826 val gc1:guess_collection = sys v rt 1827 1828 val f = guess_rewrite rew_thm; 1829 val gc2 = 1830 {rewrites = #rewrites gc1, 1831 general = [], 1832 exists_point = map f (#exists_point gc1), 1833 forall_point = map f (#forall_point gc1), 1834 forall = map f (#forall gc1), 1835 exists = map f (#exists gc1), 1836 forall_gap = map f (#forall_gap gc1), 1837 exists_gap = map f (#exists_gap gc1)}:guess_collection 1838in 1839 gc2 1840end handle UNCHANGED => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 1841 | HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1842 1843 1844 1845fun QUANT_INSTANTIATE_HEURISTIC___CONV conv sys v t = 1846let 1847 val thm_opt = SOME (QCHANGED_CONV (CHANGED_CONV conv) t) handle HOL_ERR _ => NONE 1848in 1849 if not (isSome thm_opt) then raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp else 1850 QUANT_INSTANTIATE_HEURISTIC___REWRITE sys v (valOf thm_opt) 1851end handle UNCHANGED => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 1852 | HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1853 1854 1855fun QUANT_INSTANTIATE_HEURISTIC___EQUATION___TypeBase_one_one sys v t = 1856let 1857 val (l,_) = dest_eq t; 1858 val thm = TOP_ONCE_REWRITE_CONV [TypeBase.one_one_of (type_of l)] t 1859in 1860 QUANT_INSTANTIATE_HEURISTIC___REWRITE sys v thm 1861end handle UNCHANGED => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 1862 | HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1863 1864 1865 1866(******************************************************************************) 1867(* Heuristic tho rewrite the current term using an implication *) 1868(******************************************************************************) 1869 1870(* Applying a rewrite rule to a guess *) 1871(* 1872val v = ``x:num`` 1873val ctx = [] 1874val t = ``(P (x:num)):bool`` 1875val t2 = ``(x:num) = 2`` 1876val thm = mk_thm ([], mk_imp(t, t2)) 1877val thm2 = mk_thm ([], mk_imp(t2, t)) 1878val thms = [thm, thm2] 1879val thms = [thm] 1880val ctx = thms 1881val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE [] 1882val sys = heuristic; 1883 1884*) 1885 1886local 1887(* 1888 val inf_thm = GUESS_RULES_WEAKEN_FORALL_POINT 1889 val pre_thm = thm1 1890 val gL = (#forall_point gc) 1891 val ithm = inf_thm3 1892 val g = hd gL 1893 val thm = hd thmL 1894*) 1895 fun process_guess ithm g = 1896 let 1897 val (gty, i, fvL, gthm, _) = guess_extract_thm g; 1898 val gthm' = MATCH_MP ithm gthm 1899 in 1900 guess_thm(gty, i, fvL, gthm') 1901 end; 1902 1903 fun process_guess_list pre_thm v t t' inf_thm gL = 1904 let 1905 val vt = mk_abs(v, t) 1906 val vt' = mk_abs(v, t') 1907 val inf_thm1 = ISPECL [vt', vt] (intro_fresh_ty_vars inf_thm) 1908 val inf_thm2 = CONV_RULE ((RATOR_CONV o RAND_CONV o QUANT_CONV o BINOP_CONV) BETA_CONV) inf_thm1 1909 val inf_thm3 = MP inf_thm2 pre_thm 1910 1911 val gL' = map (process_guess inf_thm3) gL 1912 in 1913 gL' 1914 end handle HOL_ERR _ => []; 1915 1916 1917 fun try_single_thm strengthen sys v t thm = 1918 let 1919 val _ = if (is_imp_only (concl thm)) then () else fail(); 1920 val thm0 = (if strengthen then (PART_MATCH (rand o rator) thm t) else 1921 (PART_MATCH rand thm t)); 1922 1923 val pre_thm = GEN v thm0 1924 val t' = if strengthen then (rand (concl thm0)) else (rand (rator (concl thm0))) 1925 1926 val gfun = process_guess_list pre_thm v t t' 1927 1928 val gc1:guess_collection = sys v t' handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => fail() 1929 1930 1931 val gc2 = {rewrites = #rewrites gc1, 1932 general = #general gc1, 1933 exists_point = gfun GUESS_RULES_STRENGTHEN_EXISTS_POINT (#exists_point gc1), 1934 forall_point = gfun GUESS_RULES_WEAKEN_FORALL_POINT (#forall_point gc1), 1935 forall = [], 1936 exists = [], 1937 exists_gap = gfun GUESS_RULES_WEAKEN_EXISTS_GAP (#exists_gap gc1), 1938 forall_gap = gfun GUESS_RULES_STRENGTHEN_FORALL_GAP (#forall_gap gc1)}:guess_collection 1939 in SOME gc2 end handle HOL_ERR _ => NONE 1940 | UNCHANGED => NONE 1941in 1942 1943fun QUANT_INSTANTIATE_HEURISTIC___STRENGTHEN_WEAKEN thms sys (v:term) t = 1944let 1945 val thmL = flatten (map BODY_CONJUNCTS thms); 1946 val gcL_s = mapfilter (try_single_thm true sys v t) thmL 1947 val gcL_w = mapfilter (try_single_thm false sys v t) thmL 1948 val gc = guess_collection_flatten (gcL_s @ gcL_w) 1949in 1950 gc 1951end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 1952 1953end 1954 1955 1956(******************************************************************************) 1957(* Heuristic that uses the precondition for direct matching *) 1958(******************************************************************************) 1959 1960(* 1961val v = ``x:'a`` 1962 1963val t = ``(P (x:'a)):bool`` 1964val thm = ASSUME t 1965 1966val t = ``(P (x:'a)):bool`` 1967val thm = ASSUME (mk_neg t) 1968 1969val t = ``(P (x:'a)):bool`` 1970val thm = ASSUME t 1971val t = mk_neg t 1972 1973val thms = [thm]; 1974QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION thms () (v:term) t 1975 1976 val v' = genvar (type_of v); 1977 val t' = subst [v |-> v'] t; 1978 1979 1980val thms = [thm] 1981 1982val v = ``n:num`` 1983val t = ``n < SUC m`` 1984val thm = hd thms 1985val SOME (thms, v, t) = !xxx 1986 1987*) 1988 1989local 1990 fun get_implication_gc sys v t neg dneg i P thm = let 1991 val _ = if neg then () else fail(); 1992 val ithm1 = ISPECL [P, i, v] (intro_fresh_ty_vars IMP_NEG_CONTRA); 1993 1994 val c0 = RATOR_CONV o RAND_CONV 1995 val (c2, c1) = (RAND_CONV BETA_CONV, BETA_CONV) 1996 val ithm2 = CONV_RULE (c0 c2) ithm1; 1997 val ithm3 = if dneg then CONV_RULE (c0 NEG_NEG_ELIM_CONV) ithm2 else ithm2 1998 val ithm4 = MP ithm3 thm 1999 val ithm5 = CONV_RULE (c0 c1) ithm4; 2000 2001 val free_vars_lhs = let 2002 val bound_vars = FVL (hyp ithm5) empty_tmset 2003 val bound_vars' = FVL [(rand (rator (concl ithm5)))] bound_vars 2004 val rest_vars = FVL [rand (concl ithm5)] empty_tmset 2005 val free_vars = HOLset.difference (rest_vars, bound_vars') 2006 in 2007 HOLset.listItems free_vars 2008 end 2009 val ithm6 = List.foldl (fn (v, thm) => CONV_RULE FORALL_IMP_CONV (GEN v thm)) ithm5 free_vars_lhs 2010 val gc = QUANT_INSTANTIATE_HEURISTIC___STRENGTHEN_WEAKEN [ithm6] sys (v:term) t 2011 handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => empty_guess_collection; 2012 in gc end handle HOL_ERR _ => empty_guess_collection; 2013 2014 2015 fun get_direct_matches_gc neg dneg i P thm = let 2016 val gthm0 = if neg then GUESS_RULES_TRIVIAL_FORALL_POINT else GUESS_RULES_TRIVIAL_EXISTS_POINT 2017 val gthm1 = ISPECL [i, P] (intro_fresh_ty_vars gthm0) 2018 2019 val c0 = if neg then (RAND_CONV BETA_CONV) else BETA_CONV 2020 val c1 = if dneg then c0 THENC NEG_NEG_ELIM_CONV else c0 2021 val gthm2 = CONV_RULE (RATOR_CONV (RAND_CONV c1)) gthm1 2022 val gthm = MP gthm2 thm; 2023 val gc = {rewrites = [], 2024 general = [], 2025 exists_point = if neg then [] else [guess_thm (gty_exists_point, i, [], gthm)], 2026 forall_point = if neg then [guess_thm (gty_forall_point, i, [], gthm)] else [], 2027 forall = [], 2028 exists = [], 2029 exists_gap = [], 2030 forall_gap = []}:guess_collection 2031 in gc end; 2032 2033 fun try_single_thm try_imps sys vset v t v' t' thm = 2034 let 2035 val (vs, _) = strip_forall (concl thm); 2036 val vs' = map (fn v => genvar (type_of v)) vs 2037 val thm' = SPECL vs' thm 2038 2039 val consts = HOLset.listItems (FVL [concl thm] vset) 2040 val (s, neg, dneg) = (Unify.simp_unify_terms consts t' (concl thm'), false, false) handle HOL_ERR _ => 2041 (Unify.simp_unify_terms consts (mk_neg t') (concl thm'), true, false) handle HOL_ERR _ => 2042 (Unify.simp_unify_terms consts t' (mk_neg (concl thm')), true, true) handle HOL_ERR _ => 2043 fail(); 2044 val i = Unify.deref_tmenv s v'; 2045 val P = mk_abs (v, t) 2046 val thm'' = INST s thm'; 2047 val gc = get_direct_matches_gc neg dneg i P thm''; 2048 val gc' = if try_imps then let 2049 val gc'' = get_implication_gc sys v t neg dneg i P thm''; 2050 in 2051 guess_collection_append gc gc'' 2052 end else gc 2053 in SOME gc' end handle HOL_ERR _ => NONE; 2054in 2055 2056fun QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION try_imps thms sys (v:term) t = 2057let 2058 val v' = genvar (type_of v); 2059 val t' = subst [v |-> v'] t; 2060 val thmL = flatten (map CONJUNCTS thms); 2061 val vset = HOLset.delete (FVL [t] empty_tmset, v) handle HOLset.NotFound => 2062 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 2063 2064 val gc = guess_collection_flatten (map (try_single_thm try_imps sys vset v t v' t') thmL) 2065in 2066 gc 2067end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 2068 2069end 2070 2071(******************************************************************************) 2072(******************************************************************************) 2073(* *) 2074(* Put everything together *) 2075(* Combine Heuristics / Caching etc *) 2076(* *) 2077(******************************************************************************) 2078(******************************************************************************) 2079 2080 2081(******************************************************************************) 2082(* Quantifier Heuristics Parameters *) 2083(******************************************************************************) 2084 2085(* One needs to collect all the heuristics, theorems etc used during guess search. 2086 The following datastructures achieves this. *) 2087 2088type quant_param = 2089{distinct_thms : thm list, (* Dichotomy theorems showing distinctiness *) 2090 cases_thms : thm list, (* Dichotomy theorems showing case completeness *) 2091 rewrite_thms : thm list, (* Theorems used for rewrites *) 2092 instantiation_thms : thm list, (* Theorems used for direct instantiations *) 2093 imp_thms : thm list, (* Theorems used for weakening and strengthening *) 2094 context_thms : thm list, (* additional context *) 2095 inference_thms : thm list, (* Theorems used as inference rules to derive guesses from guesses for subterms. *) 2096 convs : conv list, (* Conversions used *) 2097 filter : (term -> term -> bool) list, (* Getting a free variable and a term, these ML functions decide, whether to try and find a guess *) 2098 inst_filter : (term -> term -> term -> term list -> bool) list, 2099 (* 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 *) 2100 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 *) 2101 heuristics : (bool * quant_heuristic) list, (* Heuristics that should be applied for all subterms *) 2102 final_rewrite_thms : thm list (* Rewrites used for cleaning up after instantiations. *) }; 2103 2104 2105fun combine_qp 2106 ({distinct_thms = l11, 2107 rewrite_thms = l12, 2108 cases_thms = l13, 2109 convs = l14, 2110 heuristics = l15, 2111 filter = l19, 2112 inst_filter = l1E, 2113 context_heuristics = l1A, 2114 imp_thms = l1B, 2115 instantiation_thms = l1C, 2116 context_thms = l1D, 2117 inference_thms = l17, 2118 final_rewrite_thms = l16}:quant_param) 2119 ({distinct_thms = l21, 2120 rewrite_thms = l22, 2121 cases_thms = l23, 2122 convs = l24, 2123 heuristics = l25, 2124 filter = l29, 2125 inst_filter = l2E, 2126 context_heuristics = l2A, 2127 imp_thms = l2B, 2128 instantiation_thms = l2C, 2129 context_thms = l2D, 2130 inference_thms = l27, 2131 final_rewrite_thms = l26}:quant_param) = 2132 2133 ({distinct_thms = (append l11 l21), 2134 rewrite_thms = (append l12 l22), 2135 cases_thms = (append l13 l23), 2136 convs = (append l14 l24), 2137 filter = (append l19 l29), 2138 inst_filter = (append l1E l2E), 2139 context_heuristics = (append l1A l2A), 2140 imp_thms = (append l1B l2B), 2141 instantiation_thms = (append l1C l2C), 2142 context_thms = (append l1D l2D), 2143 heuristics = (append l15 l25), 2144 inference_thms = (append l17 l27), 2145 final_rewrite_thms = (append l16 l26)}:quant_param) 2146 2147 2148val empty_qp = 2149 ({distinct_thms = [], 2150 rewrite_thms = [], 2151 cases_thms = [], 2152 convs = [], 2153 heuristics = [], 2154 filter = [], 2155 inst_filter = [], 2156 context_heuristics = [] , 2157 imp_thms = [], 2158 instantiation_thms = [], 2159 context_thms = [], 2160 inference_thms = [], 2161 final_rewrite_thms = []}:quant_param) 2162 2163fun combine_qps L = 2164 foldl (fn (a1,a2) => combine_qp a1 a2) empty_qp L; 2165 2166fun distinct_qp thmL = 2167 {distinct_thms=thmL, 2168 rewrite_thms=[], 2169 cases_thms=[], 2170 filter=[], 2171 context_heuristics=[], 2172 inference_thms=[], 2173 imp_thms = [], 2174 inst_filter = [], 2175 instantiation_thms = [], 2176 context_thms = [], 2177 convs=[],heuristics=[], 2178 final_rewrite_thms=[]}:quant_param; 2179 2180fun rewrite_qp thmL = 2181 {distinct_thms=[], 2182 rewrite_thms=thmL, 2183 cases_thms=[], 2184 filter=[], 2185 inst_filter = [], 2186 context_heuristics=[], 2187 inference_thms=[], 2188 imp_thms = [], 2189 instantiation_thms = [], 2190 context_thms = [], 2191 convs=[],heuristics=[], 2192 final_rewrite_thms=[]}:quant_param; 2193 2194fun fixed_context_qp thmL = 2195 {distinct_thms=[], 2196 rewrite_thms=[], 2197 cases_thms=[], 2198 filter=[], 2199 inst_filter = [], 2200 context_heuristics=[], 2201 inference_thms=[], 2202 imp_thms = [], 2203 instantiation_thms = [], 2204 context_thms = thmL, 2205 convs=[],heuristics=[], 2206 final_rewrite_thms=[]}:quant_param; 2207 2208fun imp_qp thmL = 2209 {distinct_thms=[], 2210 rewrite_thms=[], 2211 cases_thms=[], 2212 filter=[], 2213 inst_filter = [], 2214 context_heuristics=[], 2215 inference_thms=[], 2216 imp_thms = thmL, 2217 instantiation_thms = [], 2218 context_thms = [], 2219 convs=[],heuristics=[], 2220 final_rewrite_thms=[]}:quant_param; 2221 2222fun instantiation_qp thmL = 2223 {distinct_thms=[], 2224 rewrite_thms=[], 2225 cases_thms=[], 2226 filter=[], 2227 inst_filter = [], 2228 context_heuristics=[], 2229 inference_thms=[], 2230 imp_thms = [], 2231 instantiation_thms = thmL, 2232 context_thms = [], 2233 convs=[],heuristics=[], 2234 final_rewrite_thms=[]}:quant_param; 2235 2236fun final_rewrite_qp thmL = 2237 {distinct_thms=[], 2238 rewrite_thms=[], 2239 cases_thms=[], 2240 filter=[], 2241 inst_filter = [], 2242 context_heuristics=[], 2243 inference_thms=[], 2244 imp_thms = [], 2245 instantiation_thms = [], 2246 context_thms = [], 2247 convs=[],heuristics=[], 2248 final_rewrite_thms=thmL}:quant_param; 2249 2250fun cases_qp thmL = 2251 {distinct_thms=[], 2252 rewrite_thms=[], 2253 cases_thms=thmL, 2254 filter=[], 2255 inst_filter = [], 2256 context_heuristics=[], 2257 inference_thms=[], 2258 convs=[],heuristics=[], 2259 imp_thms = [], 2260 instantiation_thms = [], 2261 context_thms = [], 2262 final_rewrite_thms=[]}:quant_param; 2263 2264fun inference_qp thmL = 2265 {distinct_thms=[], 2266 rewrite_thms=[], 2267 cases_thms=[], 2268 filter=[], 2269 inst_filter = [], 2270 context_heuristics=[], 2271 inference_thms=thmL, 2272 convs=[],heuristics=[], 2273 imp_thms = [], 2274 instantiation_thms = [], 2275 context_thms = [], 2276 final_rewrite_thms=[]}:quant_param; 2277 2278fun convs_qp cL = 2279 {distinct_thms=[], 2280 rewrite_thms=[], 2281 cases_thms=[], 2282 filter=[], 2283 inst_filter = [], 2284 context_heuristics=[], 2285 inference_thms=[], 2286 convs=cL,heuristics=[], 2287 imp_thms = [], 2288 instantiation_thms = [], 2289 context_thms = [], 2290 final_rewrite_thms=[]}:quant_param; 2291 2292fun heuristics_qp hL = 2293 {distinct_thms=[], 2294 rewrite_thms=[], 2295 cases_thms=[], 2296 filter=[], 2297 inst_filter = [], 2298 context_heuristics=[], 2299 inference_thms=[], 2300 convs=[],heuristics=map (fn h => (false, h)) hL, 2301 imp_thms = [], 2302 instantiation_thms = [], 2303 context_thms = [], 2304 final_rewrite_thms=[]}:quant_param; 2305 2306fun top_heuristics_qp hL = 2307 {distinct_thms=[], 2308 rewrite_thms=[], 2309 cases_thms=[], 2310 filter=[], 2311 inst_filter = [], 2312 context_heuristics=[], 2313 inference_thms=[], 2314 convs=[], 2315 heuristics=map (fn h => (true, h)) hL, 2316 imp_thms = [], 2317 instantiation_thms = [], 2318 context_thms = [], 2319 final_rewrite_thms=[]}:quant_param; 2320 2321fun context_heuristics_qp chL = 2322 {distinct_thms=[], 2323 rewrite_thms=[], 2324 cases_thms=[], 2325 filter=[], 2326 inst_filter = [], 2327 context_heuristics=map (fn h => (false, h)) chL, 2328 inference_thms=[], 2329 imp_thms = [], 2330 instantiation_thms = [], 2331 context_thms = [], 2332 convs=[],heuristics=[], 2333 final_rewrite_thms=[]}:quant_param; 2334 2335fun context_top_heuristics_qp chL = 2336 {distinct_thms=[], 2337 rewrite_thms=[], 2338 cases_thms=[], 2339 filter=[], 2340 inst_filter = [], 2341 context_heuristics=map (fn h => (true, h)) chL, 2342 inference_thms=[], 2343 imp_thms = [], 2344 instantiation_thms = [], 2345 context_thms = [], 2346 convs=[],heuristics=[], 2347 final_rewrite_thms=[]}:quant_param; 2348 2349fun filter_qp fL = 2350 {distinct_thms=[], 2351 rewrite_thms=[], 2352 cases_thms=[], 2353 filter=fL, 2354 inst_filter = [], 2355 context_heuristics=[], 2356 inference_thms=[], 2357 imp_thms = [], 2358 instantiation_thms = [], 2359 context_thms = [], 2360 convs=[],heuristics=[], 2361 final_rewrite_thms=[]}:quant_param; 2362 2363fun inst_filter_qp fL = 2364 {distinct_thms=[], 2365 rewrite_thms=[], 2366 cases_thms=[], 2367 filter=[], 2368 inst_filter = fL, 2369 context_heuristics=[], 2370 inference_thms=[], 2371 imp_thms = [], 2372 instantiation_thms = [], 2373 context_thms = [], 2374 convs=[],heuristics=[], 2375 final_rewrite_thms=[]}:quant_param; 2376 2377 2378 2379(******************************************************************************) 2380(* Combining multiple heuristics and other stuff into one big one that *) 2381(* calls itself recursively, uses caches and provides debugging information *) 2382(******************************************************************************) 2383 2384 2385(* Cache *) 2386 2387(* 2388 val heuristicL = [QUANT_INSTANTIATE_HEURISTIC___EQUATION]; 2389 val v = ``x:num`` 2390 val t = ``x:num = 9`` 2391*) 2392 2393type quant_heuristic_cache = (Term.term, (Term.term, guess_collection) Redblackmap.dict) Redblackmap.dict 2394fun mk_quant_heuristic_cache () = (Redblackmap.mkDict Term.compare):quant_heuristic_cache 2395 2396(* 2397val cache = mk_quant_heuristic_cache () 2398val t = T 2399val v = T 2400val fv = [T] 2401val gc = SOME empty_guess_collection 2402*) 2403 2404fun quant_heuristic_cache___insert (cache:quant_heuristic_cache) (v:term) (t:term) (gc:guess_collection) = 2405let 2406 val t_cache_opt = Redblackmap.peek (cache,t) 2407 val t_cache = if isSome t_cache_opt then valOf t_cache_opt else 2408 (Redblackmap.mkDict Term.compare); 2409 2410 val t_cache' = Redblackmap.insert (t_cache, v, gc) 2411 val cache' = Redblackmap.insert (cache, t, t_cache') 2412in 2413 cache':quant_heuristic_cache 2414end; 2415 2416 2417 2418fun quant_heuristic_cache___peek (cache:quant_heuristic_cache) (v:term) (t:term) = 2419let 2420 val t_cache = Redblackmap.find (cache,t) 2421 val gc = Redblackmap.find (t_cache,v); 2422in 2423 SOME gc 2424end handle Redblackmap.NotFound => NONE; 2425 2426 2427 2428 2429(* Auxiliary functions *) 2430 2431fun cut_term_to_string t = 2432 let 2433 val n = !QUANT_INSTANTIATE_HEURISTIC___print_term_length; 2434 val st = term_to_string t; 2435 val st' = if (String.size st > n) then 2436 (substring (st,0,n)^"...") else st 2437 in 2438 st' 2439 end; 2440 2441 2442fun COMBINE_HEURISTIC_FUNS L = 2443let 2444 val gcL = map (fn h => 2445 ((SOME (h ()) 2446 handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => NONE 2447 | HOL_ERR _ => NONE 2448 | UNCHANGED => NONE 2449 ))) L; 2450 val gc = guess_collection_flatten gcL; 2451in 2452 gc 2453end; 2454 2455fun prefix_string 0 = "" 2456 | prefix_string n = " "^(prefix_string (n-1)); 2457 2458 2459(* 2460 2461val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE 2462val sys = heuristic; 2463 2464 2465val heuristicL = 2466 [QUANT_INSTANTIATE_HEURISTIC___EQUATION, 2467 QUANT_INSTANTIATE_HEURISTIC___BOOL, 2468 QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL 2469 (mk_guess_net inference_thmL)] 2470 2471val t = ``(x = 7) \/ Q x`` 2472val v = ``x:num`` 2473 2474sys v t 2475QUANT_INSTANTIATE_HEURISTIC___EQUATION sys v t 2476val t = ``!x y. P x y (z:'a)`` 2477val v = ``z:'a`` 2478val fv = [v] 2479 2480val n = 0; 2481val cache_ref_opt = SOME (ref (mk_quant_heuristic_cache ())) 2482val heuristicL = hL 2483*) 2484 2485(* The main function with an explicit recursion depth argument, and a list of already visited arguments. The arguments are: 2486 2487 n - recurion depth 2488 tL - stack of terms for which instantiation is searched. Needed to detect cycles and abort. 2489 filterL - a list of ML-functions that say which variable / term combinations to skip 2490 top_heuristicL - a list of heuristics that should just be tried at top-level but not used for recursive calls 2491 heuristicL - the list of heuristics to combine 2492 ctx_top_heuristicL - context heuristics to combine and only be used at top-level 2493 ctx_heuristicL - context heuristics to combine. In contrast to heuristicL they get an extra context argument as input and their result is 2494 not cached, because it may depend on the context. 2495 cache_ref_opt - a reference to a cache, if NONE is passed, a new cache is created internally 2496 ctx - context theorems that might be used 2497 v - the variable 2498 t - the term 2499*) 2500 2501fun BOUNDED_QUANT_INSTANTIATE_HEURISTIC___COMBINE n tL 2502 filterL inst_filterL top_heuristicL heuristicL ctx_top_heuristicL ctx_heuristicL cache_ref_opt (ctx:thm list) (v:term) (t:term) = 2503if (n >= !QUANT_INSTANTIATE_HEURISTIC___max_rec_depth) then 2504 ((say_HOL_WARNING "BOUNDED_QUANT_INSTANTIATE_HEURISTIC___COMBINE" "Maximal recursion depth reached!"); 2505 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp) 2506else let 2507 val _ = if exists (aconv t) tL then raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp else (); 2508 val _ = if (all (fn filter => (filter v t)) filterL) andalso (free_in v t) then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 2509 val cache_ref = if isSome cache_ref_opt then valOf cache_ref_opt else 2510 (ref (mk_quant_heuristic_cache ())); 2511 val gc_opt = quant_heuristic_cache___peek (!cache_ref) v t 2512 val cache_found = isSome gc_opt; 2513 2514 val _ = if ((!QUANT_INSTANTIATE_HEURISTIC___debug > 0) andalso (n <= !QUANT_INSTANTIATE_HEURISTIC___debug_depth)) then 2515 say ((prefix_string n)^"searching guesses for ``"^ 2516 (term_to_string v)^"`` in ``"^(cut_term_to_string t)^"``\n") 2517 else (); 2518 2519 val sys = BOUNDED_QUANT_INSTANTIATE_HEURISTIC___COMBINE (n+1) (t :: tL) filterL inst_filterL [] heuristicL [] ctx_heuristicL (SOME cache_ref) ctx; 2520 val gc = if (isSome gc_opt) then valOf gc_opt else 2521 let 2522 val hL = map (fn h => (fn () => (h sys v t))) (top_heuristicL @ heuristicL); 2523 val gc = COMBINE_HEURISTIC_FUNS hL; 2524 val _ = let 2525 val c = quant_heuristic_cache___insert (!cache_ref) v t gc; 2526 val _ = cache_ref := c 2527 in 2528 () 2529 end; 2530 in 2531 gc 2532 end; 2533 2534 val gc_context = let 2535 val hLc = map (fn h => (fn () => (h ctx sys v t))) (ctx_top_heuristicL @ ctx_heuristicL); 2536 val gc = COMBINE_HEURISTIC_FUNS (hLc); 2537 in 2538 gc 2539 end; 2540 val gc = correct_guess_collection v t (guess_collection_clean (guess_collection_append gc gc_context)); 2541 val gc = filter_guess_collection inst_filterL v t gc; 2542 2543 val _ = if (!QUANT_INSTANTIATE_HEURISTIC___debug > 0) andalso (n <= !QUANT_INSTANTIATE_HEURISTIC___debug_depth) then 2544 let 2545 val gL = (snd (guess_collection2list gc)); 2546 val prefix = prefix_string n; 2547 val guesses_found_string = if null gL then "no" else Int.toString (length gL); 2548 val _ = say (prefix^guesses_found_string^" guesses found for ``"^ 2549 (term_to_string v)^"`` in ``"^(cut_term_to_string t)^"``\n") 2550 2551 val show_thm = (!QUANT_INSTANTIATE_HEURISTIC___debug > 1); 2552 fun say_guess guess = say (prefix^" - "^ 2553 (guess_to_string show_thm guess)^"\n") 2554 val _ = foldl (fn (guess,_) => say_guess guess) () (snd (guess_collection2list gc)) 2555 in 2556 () 2557 end 2558 else () 2559 val _ = if (is_empty_guess_collection gc) then raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp else (); 2560in 2561 gc 2562end; 2563 2564 2565 2566(* The finial top level function *) 2567val QUANT_INSTANTIATE_HEURISTIC___COMBINE = 2568 BOUNDED_QUANT_INSTANTIATE_HEURISTIC___COMBINE 0 []; 2569 2570 2571 2572 2573(****************************************************************** 2574 * creating heuristics from a quantifier parameter 2575 ******************************************************************) 2576 2577local 2578 val inference_thmL = [GUESS_RULES_DISJ, GUESS_RULES_CONJ, 2579 GUESS_RULES_IMP, GUESS_RULES_EQUIV, 2580 GUESS_RULES_COND, GUESS_RULES_NEG]; 2581 val (guesses_net_complex, guesses_net_simple) = mk_guess_net inference_thmL; 2582 2583 val BASIC_QUANT_INSTANTIATE_HEURISTICS = 2584 [QUANT_INSTANTIATE_HEURISTIC___EQUATION, 2585 QUANT_INSTANTIATE_HEURISTIC___BOOL, 2586 QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL_SIMPLE guesses_net_simple, 2587 QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL_COMPLEX guesses_net_complex, 2588 QUANT_INSTANTIATE_HEURISTIC___QUANT true, 2589 QUANT_INSTANTIATE_HEURISTIC___CONV (markerLib.DEST_LABEL_CONV), 2590 QUANT_INSTANTIATE_HEURISTIC___CONV (asm_marker_ELIM_CONV) 2591 ] 2592in 2593 2594 (* The most basic heuristics that should always be turned on *) 2595 val basic_qp = heuristics_qp BASIC_QUANT_INSTANTIATE_HEURISTICS 2596 val direct_context_qp = context_heuristics_qp[QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION false] 2597 val context_qp = context_heuristics_qp[QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION true, QUANT_INSTANTIATE_HEURISTIC___STRENGTHEN_WEAKEN] 2598end; 2599 2600fun qp_to_heuristic 2601 ({distinct_thms = distinct_thmL, 2602 cases_thms = cases_thmL, 2603 rewrite_thms = rewrite_thmL, 2604 inference_thms = inference_thmL2, 2605 inst_filter = inst_filterF, 2606 convs = convL, 2607 filter = filterF, 2608 context_heuristics=full_context_heuristicL, 2609 heuristics = full_heuristicL, 2610 imp_thms = imp_thmL, 2611 instantiation_thms = instantiation_thmL, 2612 context_thms = ctx_thmL, 2613 final_rewrite_thms = final_rewrite_thmL}:quant_param) = 2614 let 2615 fun split_fun (b:bool) L = map snd (filter (fn (f, _) => b = f) L) 2616 val heuristicL = split_fun false full_heuristicL 2617 val top_heuristicL = split_fun true full_heuristicL 2618 val context_heuristicL = split_fun false full_context_heuristicL 2619 val top_context_heuristicL = split_fun true full_context_heuristicL 2620 val (hcL1, hcL2, imp_case_thms) = QUANT_INSTANTIATE_HEURISTIC___cases_list cases_thmL; 2621 val (guesses_net_complex, guesses_net_simple) = mk_guess_net inference_thmL2; 2622 val extra_imp_thms = mapfilter (MATCH_MP DISJ_IMP_INTRO) imp_case_thms 2623 2624 val top_heuristicL = (hcL1 @ top_heuristicL); 2625 val heuristicL_1 = [QUANT_INSTANTIATE_HEURISTIC___EQUATION_distinct distinct_thmL, 2626 QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL_SIMPLE guesses_net_simple, 2627 QUANT_INSTANTIATE_HEURISTIC___THM_GENERAL_COMPLEX guesses_net_complex, 2628 QUANT_INSTANTIATE_HEURISTIC___STRENGTHEN_WEAKEN (imp_thmL @ extra_imp_thms), 2629 QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION true instantiation_thmL] 2630 val heuristicL_2 = map QUANT_INSTANTIATE_HEURISTIC___CONV ((map (fn thm => TOP_ONCE_REWRITE_CONV [thm]) rewrite_thmL)@convL) 2631 val heuristicL_final = flatten [heuristicL_1, heuristicL_2, hcL2, heuristicL] 2632 in 2633 fn cache_ref_opt => fn ctx => 2634 (QUANT_INSTANTIATE_HEURISTIC___COMBINE filterF inst_filterF top_heuristicL heuristicL_final 2635 top_context_heuristicL context_heuristicL cache_ref_opt (append ctx ctx_thmL)) 2636 end; 2637 2638(* very simple system callback for debugging *) 2639val debug_sys = qp_to_heuristic empty_qp NONE [] 2640 2641(****************************************************************** 2642 * a stateful heuristic and quant_param 2643 ******************************************************************) 2644 2645val quant_param_ref = ref empty_qp; 2646fun clear_stateful_qp () = (quant_param_ref := empty_qp); 2647 2648 2649fun stateful_qp___add_combine_arguments args = 2650 (quant_param_ref := 2651 combine_qps ((!quant_param_ref)::args)); 2652 2653 2654val TypeBase_qp = heuristics_qp [ 2655 QUANT_INSTANTIATE_HEURISTIC___EQUATION___TypeBase_one_one, 2656 QUANT_INSTANTIATE_HEURISTIC___EQUATION___TypeBase_distinct, 2657 QUANT_INSTANTIATE_HEURISTIC___TypeBase_cases]; 2658 2659 2660fun pure_stateful_qp () = (!quant_param_ref) 2661 2662fun stateful_qp () = combine_qp TypeBase_qp (pure_stateful_qp ()); 2663 2664fun get_qp___for_types typeL = 2665 {distinct_thms = map TypeBase.distinct_of typeL, 2666 cases_thms = map TypeBase.nchotomy_of typeL, 2667 rewrite_thms = map TypeBase.one_one_of typeL, 2668 context_heuristics=[], filter=[], 2669 final_rewrite_thms = [], 2670 inference_thms = [], 2671 imp_thms = [], 2672 instantiation_thms = [], 2673 inst_filter = [], 2674 context_thms = [], 2675 convs=[],heuristics=[]}:quant_param; 2676 2677 2678 2679(****************************************************************** 2680 * The main stuff 2681 ******************************************************************) 2682 2683(* 2684val only_eq = false; 2685val try_eq = true; 2686val expand_eq = false; 2687val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE neg_heuL []; 2688val dir = CONSEQ_CONV_UNKNOWN_direction; 2689val t = ``!t:num. (t = 5) ==> X`` 2690val t = ``!z t q. ((t = z2) ==> X z) /\ (z = 8 + t)`` 2691*) 2692 2693 2694fun move_exists_to_end t = 2695let 2696 val thm1 = SWAP_EXISTS_CONV t; 2697 2698 val (top_var, r_term) = dest_exists (rhs (concl thm1)); 2699 val thm2 = move_exists_to_end r_term; 2700 val thm3 = EQ_EXISTS_INTRO (top_var, thm2); 2701in 2702 TRANS thm1 thm3 2703end handle HOL_ERR _ => REFL t; 2704 2705 2706(* 2707val BOOL_SIMP_CONV_cs = (computeLib.bool_compset()); 2708val _ = computeLib.add_conv (boolSyntax.universal,1,QCONV QUANT_SIMP_CONV) BOOL_SIMP_CONV_cs; 2709val _ = computeLib.add_conv (boolSyntax.existential,1,QCONV QUANT_SIMP_CONV) BOOL_SIMP_CONV_cs; 2710val BOOL_SIMP_CONV = WEAK_CBV_CONV BOOL_SIMP_CONV_cs; 2711*) 2712 2713fun BOOL_SIMP_CONV rwL (gc:guess_collection) = 2714let 2715 val conv = REWRITE_CONV (append rwL (#rewrites gc)); 2716in 2717 fn t => conv t handle UNCHANGED => REFL t 2718end; 2719 2720 2721(* 2722val t = ``?x. (x = 2) /\ P x``; 2723val t = ``?x. (x = 2) \/ P x``; 2724val t = ``?x. (7 + z = x) /\ P x``; 2725 2726val t = ``?x. !z. ~(~(7 = x) \/ P x z)``; 2727val t = ``?l. ~(l = [])`` 2728 2729val t = ``?x a b. P /\ (f x = f 2) /\ Q (f x)`` 2730val t = ``?p1 p2. (p1 = 7) /\ Q p1 p2`` 2731val t = ``?p1. (p1 = 7) /\ Q p1`` 2732val t = ``?x:'a. (!y2:'b y:'b y3:'b. (x = f y y2 y3)) /\ P x`` 2733val t = ``?x. ~(Q3 x \/ Q x \/ Q2 x \/ ~(x = 2))`` 2734 2735val only_eq = true; 2736val try_eq = true; 2737val expand_eq = false; 2738val heuristic = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE empty_qp NONE 2739val sys = heuristic; 2740val dir = CONSEQ_CONV_UNKNOWN_direction 2741val min_var_occs = true; 2742val rwL = [] 2743 2744val t = mk_exists (v, t 2745val t = ``!x. x = []`` 2746 2747heuristic ``l:'a list`` ``l:'a list = []`` 2748*) 2749 2750 2751fun QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (only_eq,try_eq,expand_eq) min_var_occs heuristic rwL (ctx:thm list) dir t = 2752if (not (is_exists t)) andalso (not (is_forall t)) andalso (not (is_exists1 t)) then raise UNCHANGED else 2753let 2754 val (v,b) = dest_abs (rand t); 2755in 2756 (if not (free_in v b) then 2757 ((if is_exists t then EXISTS_SIMP_CONV else 2758 if is_forall t then FORALL_SIMP_CONV else 2759 (HO_PART_MATCH lhs UEXISTS_SIMP)) t) 2760 else 2761 if is_exists t then 2762 let 2763 val (v,qb) = dest_exists t; 2764 val (qvL, b0) = strip_exists qb; 2765 2766 val b_thm = if min_var_occs then 2767 min_var_occur_CONV v b0 handle UNCHANGED => REFL b0 2768 else REFL b0; 2769 val b = rhs (concl b_thm); 2770 2771 val guessC = correct_guess_collection v b 2772 (heuristic ctx v b) 2773 handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => raise UNCHANGED; 2774 2775 val exists_pointL = #exists_point guessC; 2776 val existsL = append (#exists guessC) 2777 (map guess_weaken (#exists_gap guessC)) 2778 2779 val guess = first guess_has_thm exists_pointL handle HOL_ERR _ => 2780 first guess_has_thm_no_free_vars existsL handle HOL_ERR _ => 2781 first guess_has_thm existsL handle HOL_ERR _ => 2782 first (K true) exists_pointL handle HOL_ERR _ => 2783 first (K true) existsL handle HOL_ERR _ => 2784 first (K true) (#general guessC) handle HOL_ERR _ => 2785 raise UNCHANGED; 2786 2787 val (i,fvL) = guess_extract guess; 2788 val proof_opt = guess2thm_opt guess; 2789 val need_eq = (only_eq orelse (dir = CONSEQ_CONV_WEAKEN_direction)); 2790 val try_proof_eq = isSome proof_opt andalso try_eq andalso need_eq; 2791 2792 val thm_opt = if not try_proof_eq then NONE else 2793 if (is_guess_thm gty_exists_point guess) then 2794 let 2795 val proof = valOf proof_opt; 2796 val xthm0 = MATCH_MP GUESS_EXISTS_POINT_THM proof 2797 in 2798 SOME xthm0 2799 end 2800 else (*exists*) 2801 let 2802 val proof = (valOf proof_opt); 2803 val i_t = rand (rator (concl proof)) 2804 val xthm0 = ISPEC i_t GUESS_EXISTS_THM 2805 val new_part = (rhs o rand o snd o dest_forall o concl) xthm0 2806 val new_part_CONV1 = if null fvL then ALL_CONV else 2807 TRY_CONV (SPLIT_QUANT_CONV (pairSyntax.list_mk_pair fvL)) 2808 val new_part_thm = (new_part_CONV1 THENC SIMP_CONV std_ss []) new_part; 2809 val xthm1 = CONV_RULE (QUANT_CONV (RAND_CONV (RHS_CONV (K new_part_thm)))) xthm0 2810 val xthm2 = MATCH_MP xthm1 proof 2811 val xthm3 = CONV_RULE (RHS_CONV (DEPTH_CONV BETA_CONV)) xthm2 2812 in 2813 SOME xthm3 2814 end; 2815 val thm = if isSome thm_opt then valOf thm_opt else 2816 if need_eq then 2817 if not expand_eq then raise UNCHANGED else 2818 let 2819 val thm0 = HO_PART_MATCH lhs (ISPEC i quantHeuristicsTheory.UNWIND_EXISTS_THM) (mk_exists (v,b)) 2820 2821 val thm1 = foldl (fn (fv,th) => 2822 let 2823 val thm2 = AP_TERM (inst [alpha |-> type_of fv] boolSyntax.existential) (ABS fv th); 2824 val thm3 = CONV_RULE (LHS_CONV QUANT_SIMP_CONV) thm2 2825 val thm4 = CONV_RULE (RHS_CONV (HO_PART_MATCH lhs quantHeuristicsTheory.MOVE_EXISTS_IMP_THM)) thm3 2826 in 2827 thm4 2828 end) thm0 fvL; 2829 in 2830 thm1 2831 end 2832 else 2833 let 2834 val vL = free_vars b; 2835 val (fvL', sub) = list_variant vL fvL; 2836 val i' = subst sub i; 2837 val ib = subst [v |-> i'] b; 2838 val ib_thm = ASSUME ib 2839 val thm0 = EXISTS ((mk_exists (v,b)),i') ib_thm 2840 val thm1 = foldr (fn (v,th) => SIMPLE_CHOOSE v th) 2841 thm0 fvL'; 2842 val thm2 = DISCH_ALL thm1 2843 in 2844 thm2 2845 end; 2846 2847 val b_thm_conv = QUANT_CONV (REWR_CONV (GSYM b_thm)) 2848 val thm2 = if is_eq (concl thm) then 2849 CONV_RULE (LHS_CONV b_thm_conv) thm 2850 else 2851 CONV_RULE (RAND_CONV b_thm_conv) thm 2852 2853 val thm3 = if (null qvL) then thm2 else 2854 let 2855 val EXISTS_INTRO_FUN = 2856 if is_eq (concl thm2) then 2857 EQ_EXISTS_INTRO else IMP_EXISTS_INTRO; 2858 val thm3 = foldr EXISTS_INTRO_FUN thm2 qvL; 2859 val ex_move_thm = move_exists_to_end t; 2860 in 2861 THEN_CONSEQ_CONV___combine ex_move_thm thm3 t 2862 end; 2863 2864 val thm4 = CONSEQ_CONV___APPLY_CONV_RULE thm3 t (BOOL_SIMP_CONV rwL guessC) 2865 in 2866 thm4 2867 end else if is_forall t then 2868 let 2869 val neg_t = let 2870 val (vL, body) = strip_forall t; 2871 val n_body = mk_neg body 2872 in 2873 list_mk_exists (vL, n_body) end 2874 2875 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) 2876 2877 val neg_t_thm = NOT_FORALL_LIST_CONV (mk_neg t) 2878 val new_conv = TRY_CONV NOT_EXISTS_LIST_CONV THENC (BOOL_SIMP_CONV rwL empty_guess_collection) 2879 2880 val thm2 = if is_eq (concl thm) then 2881 let 2882 val thm3 = TRANS neg_t_thm thm; 2883 val thm4 = AP_TERM boolSyntax.negation thm3; 2884 val thm5 = CONV_RULE (LHS_CONV NEG_NEG_ELIM_CONV) thm4 2885 val thm6 = CONV_RULE (RHS_CONV new_conv) thm5; 2886 in 2887 thm6 2888 end 2889 else if rand (rator (concl thm)) ~~ neg_t then 2890 let 2891 val thm3 = IMP_TRANS (fst (EQ_IMP_RULE neg_t_thm)) thm; 2892 val thm4 = CONTRAPOS thm3; 2893 val thm5 = CONV_RULE (RAND_CONV NEG_NEG_ELIM_CONV) thm4 2894 val thm6 = CONV_RULE (RATOR_CONV (RAND_CONV new_conv)) thm5 2895 in 2896 thm6 2897 end 2898 else if rand (concl thm) ~~ neg_t then 2899 let 2900 val thm3 = IMP_TRANS thm (snd (EQ_IMP_RULE neg_t_thm)); 2901 val thm4 = CONTRAPOS thm3; 2902 val thm5 = CONV_RULE (RATOR_CONV (RAND_CONV NEG_NEG_ELIM_CONV)) thm4 2903 val thm6 = CONV_RULE (RAND_CONV new_conv) thm5 2904 in 2905 thm6 2906 end 2907 else raise UNCHANGED; 2908 in 2909 thm2 2910 end else if is_exists1 t then 2911 let 2912 val (v,qb) = dest_exists1 t; 2913 2914 val guessC = correct_guess_collection v qb 2915 (heuristic ctx v qb); 2916 2917 val guess = first guess_has_thm_no_free_vars (#exists_gap guessC) handle HOL_ERR _ => 2918 first guess_has_thm_no_free_vars (#exists_point guessC) handle HOL_ERR _ => 2919 first guess_has_thm_no_free_vars (#exists guessC) handle HOL_ERR _ => 2920 raise UNCHANGED; 2921 2922 val (_, proof) = guess2thm guess 2923 val thm = if is_guess_thm gty_exists_gap guess then 2924 HO_MATCH_MP GUESSES_UEXISTS_THM2 proof 2925 else if is_guess_thm gty_exists_point guess then 2926 HO_MATCH_MP GUESSES_UEXISTS_THM3 proof 2927 else if is_guess_thm gty_exists guess then 2928 HO_MATCH_MP GUESSES_UEXISTS_THM1 proof 2929 else Feedback.fail() 2930 val thm2 = CONV_RULE (RHS_CONV (BOOL_SIMP_CONV rwL guessC)) thm 2931 in 2932 thm2 2933 end else raise UNCHANGED) 2934 handle QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => 2935 raise UNCHANGED 2936end; 2937 2938 2939 2940fun HEURISTIC_QUANT_INSTANTIATE_CONV re min_occs heuristic expand_eq rwL ctx = 2941 (if re then REDEPTH_CONV else DEPTH_CONV) 2942(CHANGED_CONV (QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (true,true,expand_eq) min_occs heuristic rwL ctx CONSEQ_CONV_UNKNOWN_direction)) THENC 2943REWRITE_CONV rwL; 2944 2945 2946 2947 2948(********************************************************) 2949(* Provide High level interfaces *) 2950(********************************************************) 2951 2952(***************************************************** 2953 * One of the most basic conversions. 2954 * 2955 * It get's the following arguments: 2956 * 2957 * - cache_ref_opt 2958 * a possible reference to a cache which stores 2959 * previously found guesses. A new cache can be 2960 * created using mk_quant_heuristic_cache 2961 * 2962 * - re : bool 2963 * redescent into a term some intantiation has been found? 2964 * similar to DEPTH_CONV and REDEPTH_CONV 2965 * 2966 * - min_occs 2967 * should occurences of the variable be tried to be removed in 2968 * a preprocessing step? 2969 * 2970 * - expand_eq : bool 2971 * all build in heuristics provide proofs with all guesses 2972 * if no proof is provided by user defined heuristics this 2973 * argument can be set to true to do a case split instead 2974 * 2975 * - args 2976 * a list of quant_params 2977 *****************************************************) 2978 2979fun EXTENSIBLE_QUANT_INSTANTIATE_CONV cache_ref_opt re min_occs expand_eq ctx bqp args = 2980 let val arg = (combine_qps (bqp::args)) in 2981 HEURISTIC_QUANT_INSTANTIATE_CONV re min_occs (qp_to_heuristic arg cache_ref_opt) expand_eq (#final_rewrite_thms arg) ctx 2982 end 2983 2984(* 2985val hL = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE arg 2986 2987(el 9 hL) dummy_sys v t 2988 2989QUANT_INSTANTIATE_HEURISTIC___COMBINE hL NONE v t 2990 2991(QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE arg NONE) v t 2992 2993val (cache_ref_opt, re, filter, min_occs, expand_eq, args) = 2994 (NONE, true, (K true), true, false, [pair_default_qp]) 2995*) 2996 2997 2998 2999 3000(****************************************************************** 3001 * A simpler interface, here just the quant_params list is needed 3002 ******************************************************************) 3003val QUANT_INSTANTIATE_CONV = 3004 EXTENSIBLE_QUANT_INSTANTIATE_CONV NONE true true false [] basic_qp 3005 3006val NORE_QUANT_INSTANTIATE_CONV = 3007 EXTENSIBLE_QUANT_INSTANTIATE_CONV NONE false true false [] basic_qp 3008 3009val FAST_QUANT_INSTANTIATE_CONV = 3010 EXTENSIBLE_QUANT_INSTANTIATE_CONV NONE false false false [] basic_qp 3011 3012val EXPAND_QUANT_INSTANTIATE_CONV = 3013 EXTENSIBLE_QUANT_INSTANTIATE_CONV NONE true true true [] basic_qp 3014 3015val NORE_EXPAND_QUANT_INSTANTIATE_CONV = 3016 EXTENSIBLE_QUANT_INSTANTIATE_CONV NONE false true true [] basic_qp 3017 3018val FAST_EXPAND_QUANT_INSTANTIATE_CONV = 3019 EXTENSIBLE_QUANT_INSTANTIATE_CONV NONE false false true [] basic_qp 3020 3021 3022fun QUANT_INSTANTIATE_REDUCER cache_ref_opt re min_occs expand_eq bqp qpL = 3023 let exception FACTDB of thm list; 3024 fun get_db e = (raise e) handle FACTDB thms => thms 3025 in Traverse.REDUCER 3026 {name=SOME"QUANT_INSTANTIATE", 3027 initial = FACTDB [], 3028 apply=(fn r => fn t => 3029 let 3030 val thms = get_db (#context r); 3031 val res = EXTENSIBLE_QUANT_INSTANTIATE_CONV cache_ref_opt re min_occs expand_eq thms bqp qpL t; 3032 in 3033 res 3034 end handle UNCHANGED => fail()), 3035 addcontext=(fn (ctxt,thms) => (FACTDB (thms @ (get_db ctxt))))} 3036 end; 3037 3038fun EXTENSIBLE_QUANT_INST_ss cache_ref_opt re min_occs expand_eq bqp qpL = 3039 simpLib.dproc_ss (QUANT_INSTANTIATE_REDUCER cache_ref_opt re min_occs expand_eq bqp qpL) 3040 3041fun QUANT_INST_ss qpL = EXTENSIBLE_QUANT_INST_ss NONE false true false basic_qp qpL 3042fun EXPAND_QUANT_INST_ss qpL = EXTENSIBLE_QUANT_INST_ss NONE false true true basic_qp qpL 3043fun FAST_QUANT_INST_ss qpL = EXTENSIBLE_QUANT_INST_ss NONE false false false basic_qp qpL 3044 3045fun QUANT_INSTANTIATE_TAC L = CONV_TAC (QUANT_INSTANTIATE_CONV L); 3046fun FAST_QUANT_INSTANTIATE_TAC L = CONV_TAC (FAST_QUANT_INSTANTIATE_CONV L); 3047fun ASM_QUANT_INSTANTIATE_TAC L = DISCH_ASM_CONV_TAC (QUANT_INSTANTIATE_CONV L); 3048fun FAST_ASM_QUANT_INSTANTIATE_TAC L = DISCH_ASM_CONV_TAC (FAST_QUANT_INSTANTIATE_CONV L); 3049 3050 3051(****************************************************************** 3052 * Interfaces for consequence conversions 3053 ******************************************************************) 3054 3055fun HEURISTIC_QUANT_INSTANTIATE_CONSEQ_CONV re min_occs heuristic rwL dir = 3056THEN_CONSEQ_CONV 3057((if re then CONTEXT_REDEPTH_CONSEQ_CONV else CONTEXT_DEPTH_CONSEQ_CONV) CONSEQ_CONV_IMP_CONTEXT 3058 (QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (false,true,false) min_occs heuristic rwL) dir) 3059(REWRITE_CONV rwL); 3060 3061fun EXTENSIBLE_QUANT_INSTANTIATE_CONSEQ_CONV cache_ref_opt re min_occs bqp args = 3062 let val arg = (combine_qps (bqp::args)) in 3063 HEURISTIC_QUANT_INSTANTIATE_CONSEQ_CONV re min_occs (qp_to_heuristic 3064 arg cache_ref_opt) (#final_rewrite_thms arg) end; 3065 3066fun EXTENSIBLE_QUANT_INSTANTIATE_STEP_CONSEQ_CONV cache_ref_opt min_occs bqp args = 3067 let val arg = (combine_qps (bqp::args)) in 3068 (QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (false,true,false) min_occs 3069 (qp_to_heuristic arg cache_ref_opt) 3070 (#final_rewrite_thms arg) []) end; 3071 3072val NORE_QUANT_INSTANTIATE_CONSEQ_CONV = 3073 EXTENSIBLE_QUANT_INSTANTIATE_CONSEQ_CONV NONE false false basic_qp 3074 3075val QUANT_INSTANTIATE_CONSEQ_CONV = 3076 EXTENSIBLE_QUANT_INSTANTIATE_CONSEQ_CONV NONE true true basic_qp 3077 3078val FAST_QUANT_INSTANTIATE_CONSEQ_CONV = 3079 EXTENSIBLE_QUANT_INSTANTIATE_CONSEQ_CONV NONE false false basic_qp 3080 3081fun QUANT_INSTANTIATE_CONSEQ_TAC L = 3082 DISCH_ASM_CONSEQ_CONV_TAC (QUANT_INSTANTIATE_CONSEQ_CONV L); 3083 3084 3085(********************************************************************* 3086 * Oracle heuristic 3087 * 3088 * This heuristic produces unjustified guesses. If explicitly asked, 3089 * guesses are tried to be justified by METIS 3090 **********************************************************************) 3091fun QUANT_INSTANTIATE_HEURISTIC___ORACLE try_proof ml_callback ctx sys v t = 3092let 3093 val res_opt = ml_callback ctx v t; 3094 val (i, fvL) = if isSome res_opt then valOf res_opt else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 3095in 3096 if not try_proof then 3097 {rewrites = [], 3098 general = [guess_general (i,fvL)], 3099 exists_point = [], 3100 forall_point = [], 3101 forall = [], 3102 exists = [], 3103 forall_gap = [], 3104 exists_gap = []} 3105 else 3106 {rewrites = [], 3107 general = [], 3108 exists_point = [], 3109 forall_point = [], 3110 forall = [make_guess___rewrite gty_forall v t i fvL] handle HOL_ERR _ => [], 3111 exists = [make_guess___rewrite gty_exists v t i fvL] handle HOL_ERR _ => [], 3112 forall_gap = [], 3113 exists_gap = []} 3114end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 3115 3116fun oracle_qp ml_callback = top_heuristics_qp [ 3117 QUANT_INSTANTIATE_HEURISTIC___ORACLE false (fn _ => ml_callback) []] 3118 3119fun context_oracle_qp ml_callback = context_top_heuristics_qp [ 3120 QUANT_INSTANTIATE_HEURISTIC___ORACLE false ml_callback] 3121 3122(***************************************************************** 3123 * Predefined filters 3124 *****************************************************************) 3125 3126fun type_match_filter tyL v (t:term) = 3127 let 3128 val ty' = type_of v; 3129 val _ = tryfind (fn ty => match_type ty ty') tyL; 3130 in true end handle HOL_ERR _ => false; 3131 3132 3133fun type_filter tyL v (t:term) = 3134 let 3135 val ty' = type_of v; 3136 val _ = tryfind (fn ty => ty = ty') tyL; 3137 in true end handle HOL_ERR _ => false; 3138 3139fun subterm_match_filter tL (v:term) t = 3140 can (find_term (fn t' => exists (can (fn t'' => match_term t'' t')) tL)) t 3141 3142fun subterm_filter tL (v:term) t = 3143 can (find_term (fn t' => exists (aconv t') tL)) t 3144 3145fun neg_filter f (v:term) (t:term) = not (f v t) 3146 3147 3148(********************************************************************* 3149 * Instantiate quantifiers by explicitly given guesses 3150 * 3151 * QUANT_INST_TAC / QUANT_INST_CONV are able to 3152 * instantiate quantifiers at subpositions. 3153 * They get a list of trible consisting of 3154 * (name_of_var, instantiation, list of free variables instantiation). 3155 * They then try to (partially) instantiate the named variables 3156 * with the given instantiations. 3157 **********************************************************************) 3158 3159(* 3160val t = ``t = 0`` 3161val v = ``x:num`` 3162val ctxt = [] 3163val try_proof = false; 3164val L = [("x", `0`, []), ("t", `xxx n`:term frag list, ["n"])] 3165val L = [("pdata'", `idata_h::pdata22`:term frag list, [`pdata22`]), 3166 ("idata'", `idata_t`, [])] 3167*) 3168 3169 3170fun QUANT_INSTANTIATE_HEURISTIC___LIST_callback ctxt L _ v t = 3171let 3172 val (v_name, v_type) = dest_var v 3173 val (_,i_quot,free_vars_quot) = first (fn (p,_,_) => (p = v_name)) L; 3174 3175 val i_quot' = QUOTE "(" :: (i_quot @ [QUOTE "):", ANTIQUOTE(ty_antiq v_type), QUOTE ""]); 3176 3177 val ctxt = append (Term.free_vars t) ctxt; 3178 val i = Parse.parse_in_context ctxt i_quot'; 3179 val ctxt = append (Term.free_vars i) ctxt; 3180 3181 val fvL = map (fn s => Parse.parse_in_context ctxt s) free_vars_quot; 3182in 3183 SOME (i, fvL) 3184end; 3185 3186 3187fun QUANT_INSTANTIATE_HEURISTIC___LIST ctxt try_proof L v t = 3188 QUANT_INSTANTIATE_HEURISTIC___ORACLE try_proof (QUANT_INSTANTIATE_HEURISTIC___LIST_callback ctxt L) () [] v t 3189 3190fun QUANT_TAC L (asm,t) = 3191 let 3192 val ctxt = HOLset.listItems (FVL (t::asm) empty_tmset); 3193 in 3194 REDEPTH_CONSEQ_CONV_TAC 3195 (QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (false,false,false) 3196 false (K (QUANT_INSTANTIATE_HEURISTIC___LIST ctxt false L)) [] []) 3197 (asm,t) 3198 end; 3199 3200fun INST_QUANT_CONV L t = 3201 let 3202 val ctxt = HOLset.listItems (FVL [t] empty_tmset); 3203 in 3204 DEPTH_CONV 3205 (QUANT_INSTANTIATE_HEURISTIC_STEP_CONSEQ_CONV (true,true,false) 3206 false (K (QUANT_INSTANTIATE_HEURISTIC___LIST ctxt true L)) [] [] CONSEQ_CONV_UNKNOWN_direction) 3207 t 3208 end; 3209 3210end 3211