Lines Matching defs:guess
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