src/quantHeuristics/quantHeuristicsLibBase.sml

101   The datatype guess captures these guesses and the reason.
152   a justification that might have been proved. The justification of a guess consists of a guess-type accompanied by either a theorem
154   Depending on the guess-type, it has to be a single guess as defined in
156   The list of free variables is mainly used to record names. In the guess theorem/term, only a single variable is allowed.
169 datatype guess =
218 fun guess_has_no_free_vars guess =
219     null (#2 (guess_extract guess));
221 fun guess_has_thm_no_free_vars guess =
222     guess_has_thm guess andalso
223     guess_has_no_free_vars guess;
291 (* This is the prefered way to generate a well-formed guess *)
302   | make_set_guess_thm guess _ =  guess
308   | guess_remove_thm _ _ guess =  guess;
312   | guess_thm2term guess =  guess;
316 fun make_set_guess_thm___dummy guess =
318                     "mk_thm was used to create a guess");
319     make_set_guess_thm guess (fn x => mk_thm ([], x)));
325 fun make_set_guess_thm___assume guess =
326     make_set_guess_thm guess ASSUME;
333 fun make_set_guess_thm___simple guess =
334      make_set_guess_thm guess (fn x => EQT_ELIM
373 (* Checking whether a guess is well-formed and if not try to correct it automatically. *)
375   | check_guess v t guess =
377       val (i,fvL) = guess_extract guess;
378       val ty = valOf (guess_extract_type guess);
379       val thm_term2 = valOf (guess2term guess)
390 fun correct_guess v t guess =
391    if (check_guess v t guess) then SOME guess else
393       val guess2 = guess_remove_thm v t guess handle HOL_ERR _ => guess;
397                          ("Error in guess: "^(guess_to_string true guess)) else
398                          ("Malformed theorem in guess:\n"^(guess_to_string true guess)^
422 val guess = make_set_guess_thm_opt___dummy v t (guess_forall_gap (i, fvL, NONE));
423 val (_,_,thm_opt) = guess_extract guess;
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}
493 fun guess_collection_guess_type gty_exists_point = (#exists_point:guess_collection -> guess list)
539 (* Create a guess-collection from a list of rewrites and a list of guesses by
543   | guess_list2collection___int (g1,g3,g4,g5,g6,g7,g8) (guess::gL) =
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;
574 val guess = hd (#exists gc)
612 fun 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
633  * Cleaning a guess collecion, i.e. removing duplicate
691 | clean_guess guess = guess;
916    val guess = guess_thm(gty_forall_gap, ni', fvL', g_thm);
924    forall_gap   = [guess],
1104    val guess = guess_thm (gty_forall_point, ni, fvL, g_thm);
1109    forall_point = [guess],
1233    fun apply_inference inf guess =
1235        val (_, i, fvL, gthm0, was_thm) = guess_extract_thm guess;
1581    fun try_guess ifv_opt thm_ok thm guess =
1583        val (ty, i, fvL, gthm, was_thm) = guess_extract_thm guess;
1730       fun process_guess guess =
1732          val (i, fvL) = guess_extract guess;
1738          val final_gL = guess::gL';
1743          val gthm1 = snd (guess2thm guess);
1770 (* Applying a rewrite rule to a guess *)
1774 val (v,t,thmL,guess) = valOf (!tref)
1787 val guess = make_set_guess_thm_opt___dummy v t' (guess_forall (i,fvL,NONE));
1788 correct_guess fv v t (guess_rewrite_thm_opt v t rew_thm guess)
1847 (* Applying a rewrite rule to a guess *)
2062 (* One needs to collect all the heuristics, theorems etc used during guess search.
2074  filter             : (term -> term -> bool) list, (* Getting a free variable and a term, these ML functions decide, whether to try and find a guess *)
2529                   fun say_guess guess = say (prefix^" - "^
2530                    (guess_to_string show_thm guess)^"\n")
2531                   val _ = foldl (fn (guess,_) => say_guess guess) () (snd (guess_collection2list gc))
2756       val guess = first guess_has_thm exists_pointL handle HOL_ERR _ =>
2764       val (i,fvL) = guess_extract guess;
2765       val proof_opt = guess2thm_opt guess;
2770           if (is_guess_thm gty_exists_point guess) then
2894       val guess = first guess_has_thm_no_free_vars (#exists_gap guessC) handle HOL_ERR _ =>
2899       val (_, proof) = guess2thm guess
2900       val thm = if is_guess_thm gty_exists_gap guess then
2902                 else if is_guess_thm gty_exists_point guess then
2904                 else if is_guess_thm gty_exists guess then