52 List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls; |
52 List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls; |
53 |
53 |
54 (*Attack subgoals using safe inferences*) |
54 (*Attack subgoals using safe inferences*) |
55 fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt, |
55 fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt, |
56 int_uniq_mp_tac ctxt, |
56 int_uniq_mp_tac ctxt, |
57 biresolve_tac safe0_brls, |
57 biresolve_tac ctxt safe0_brls, |
58 hyp_subst_tac, |
58 hyp_subst_tac, |
59 biresolve_tac safep_brls] ; |
59 biresolve_tac ctxt safep_brls] ; |
60 |
60 |
61 (*Repeatedly attack subgoals using safe inferences*) |
61 (*Repeatedly attack subgoals using safe inferences*) |
62 fun safe_tac ctxt = DETERM (REPEAT_FIRST (safe_step_tac ctxt)); |
62 fun safe_tac ctxt = DETERM (REPEAT_FIRST (safe_step_tac ctxt)); |
63 |
63 |
64 (*These steps could instantiate variables and are therefore unsafe.*) |
64 (*These steps could instantiate variables and are therefore unsafe.*) |
65 fun inst_step_tac ctxt = assume_tac ctxt APPEND' mp_tac ctxt; |
65 fun inst_step_tac ctxt = assume_tac ctxt APPEND' mp_tac ctxt; |
66 |
66 |
67 (*One safe or unsafe step. *) |
67 (*One safe or unsafe step. *) |
68 fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac haz_brls i]; |
68 fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac ctxt haz_brls i]; |
69 |
69 |
70 (*Dumb but fast*) |
70 (*Dumb but fast*) |
71 fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); |
71 fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); |
72 |
72 |
73 (*Slower but smarter than fast_tac*) |
73 (*Slower but smarter than fast_tac*) |