53 |
53 |
54 fun do_proof (Proof (fix, assms, steps)) = |
54 fun do_proof (Proof (fix, assms, steps)) = |
55 let val (refed, steps) = do_steps steps in |
55 let val (refed, steps) = do_steps steps in |
56 (refed, Proof (fix, assms, steps)) |
56 (refed, Proof (fix, assms, steps)) |
57 end |
57 end |
58 and do_steps steps = |
58 and do_steps [] = ([], []) |
59 let |
59 | do_steps steps = |
60 (* the last step is always implicitly referenced *) |
60 let |
61 val (steps, (refed, concl)) = |
61 (* the last step is always implicitly referenced *) |
62 split_last steps |
62 val (steps, (refed, concl)) = |
63 ||> do_refed_step |
63 split_last steps |
64 in |
64 ||> do_refed_step |
65 fold_rev do_step steps (refed, [concl]) |
65 in |
66 end |
66 fold_rev do_step steps (refed, [concl]) |
|
67 end |
67 and do_step step (refed, accu) = |
68 and do_step step (refed, accu) = |
68 case label_of_step step of |
69 (case label_of_step step of |
69 NONE => (refed, step :: accu) |
70 NONE => (refed, step :: accu) |
70 | SOME l => |
71 | SOME l => |
71 if Ord_List.member label_ord refed l then |
72 if Ord_List.member label_ord refed l then |
72 do_refed_step step |
73 do_refed_step step |
73 |>> Ord_List.union label_ord refed |
74 |>> Ord_List.union label_ord refed |
74 ||> (fn x => x :: accu) |
75 ||> (fn x => x :: accu) |
75 else |
76 else |
76 (refed, accu) |
77 (refed, accu)) |
77 and do_refed_step step = step |> postproc_step |> do_refed_step' |
78 and do_refed_step step = step |> postproc_step |> do_refed_step' |
78 and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar" |
79 and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar" |
79 | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) = |
80 | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) = |
80 let |
81 let |
81 val (refed, subproofs) = |
82 val (refed, subproofs) = |