1 (* Title: auto_solve.ML |
1 (* Title: Pure/Tools/auto_solve.ML |
2 Author: Timothy Bourke and Gerwin Klein, NICTA |
2 Author: Timothy Bourke and Gerwin Klein, NICTA |
3 |
3 |
4 Check whether a newly stated theorem can be solved directly |
4 Check whether a newly stated theorem can be solved directly by an |
5 by an existing theorem. Duplicate lemmas can be detected in |
5 existing theorem. Duplicate lemmas can be detected in this way. |
6 this way. |
|
7 |
6 |
8 The implemenation is based in part on Berghofer and |
7 The implemenation is based in part on Berghofer and Haftmann's |
9 Haftmann's Pure/codegen.ML. It relies critically on |
8 Pure/codegen.ML. It relies critically on the FindTheorems solves |
10 the FindTheorems solves feature. |
9 feature. |
11 *) |
10 *) |
12 |
11 |
13 signature AUTO_SOLVE = |
12 signature AUTO_SOLVE = |
14 sig |
13 sig |
15 val auto : bool ref; |
14 val auto : bool ref |
16 val auto_time_limit : int ref; |
15 val auto_time_limit : int ref |
17 |
16 |
18 val seek_solution : bool -> Proof.state -> Proof.state; |
17 val seek_solution : bool -> Proof.state -> Proof.state |
19 end; |
18 end; |
20 |
19 |
21 structure AutoSolve : AUTO_SOLVE = |
20 structure AutoSolve : AUTO_SOLVE = |
22 struct |
21 struct |
23 structure FT = FindTheorems; |
|
24 |
22 |
25 val auto = ref false; |
23 val auto = ref false; |
26 val auto_time_limit = ref 2500; |
24 val auto_time_limit = ref 2500; |
27 |
25 |
28 fun seek_solution int state = let |
26 fun seek_solution int state = |
29 val ctxt = Proof.context_of state; |
27 let |
|
28 val ctxt = Proof.context_of state; |
30 |
29 |
31 fun conj_to_list [] = [] |
30 fun conj_to_list [] = [] |
32 | conj_to_list (t::ts) = |
31 | conj_to_list (t::ts) = |
33 (Conjunction.dest_conjunction t |
32 (Conjunction.dest_conjunction t |
34 |> (fn (t1, t2) => conj_to_list (t1::t2::ts))) |
33 |> (fn (t1, t2) => conj_to_list (t1::t2::ts))) |
35 handle TERM _ => t::conj_to_list ts; |
34 handle TERM _ => t::conj_to_list ts; |
36 |
35 |
37 val crits = [(true, FT.Solves)]; |
36 val crits = [(true, FindTheorems.Solves)]; |
38 fun find g = (NONE, FT.find_theorems ctxt g true crits); |
37 fun find g = (NONE, FindTheorems.find_theorems ctxt g true crits); |
39 fun find_cterm g = (SOME g, FT.find_theorems ctxt |
38 fun find_cterm g = (SOME g, FindTheorems.find_theorems ctxt |
40 (SOME (Goal.init g)) true crits); |
39 (SOME (Goal.init g)) true crits); |
41 |
40 |
42 fun prt_result (goal, results) = let |
41 fun prt_result (goal, results) = |
43 val msg = case goal of |
42 let |
44 NONE => "The current goal" |
43 val msg = case goal of |
45 | SOME g => Syntax.string_of_term ctxt (term_of g); |
44 NONE => "The current goal" |
46 in |
45 | SOME g => Syntax.string_of_term ctxt (term_of g); |
47 Pretty.big_list (msg ^ " could be solved directly with:") |
46 in |
48 (map Display.pretty_fact results) |
47 Pretty.big_list (msg ^ " could be solved directly with:") |
49 end; |
48 (map Display.pretty_fact results) |
|
49 end; |
50 |
50 |
51 fun seek_against_goal () = let |
51 fun seek_against_goal () = |
52 val goal = try Proof.get_goal state |
52 let |
53 |> Option.map (#2 o #2); |
53 val goal = try Proof.get_goal state |
|
54 |> Option.map (#2 o #2); |
54 |
55 |
55 val goals = goal |
56 val goals = goal |
56 |> Option.map (fn g => cprem_of g 1) |
57 |> Option.map (fn g => cprem_of g 1) |
57 |> the_list |
58 |> the_list |
58 |> conj_to_list; |
59 |> conj_to_list; |
59 |
60 |
60 val rs = if length goals = 1 |
61 val rs = if length goals = 1 |
61 then [find goal] |
62 then [find goal] |
62 else map find_cterm goals; |
63 else map find_cterm goals; |
63 val frs = filter_out (null o snd) rs; |
64 val frs = filter_out (null o snd) rs; |
64 |
65 |
65 in if null frs then NONE else SOME frs end; |
66 in if null frs then NONE else SOME frs end; |
66 |
67 |
67 fun go () = let |
68 fun go () = |
68 val res = TimeLimit.timeLimit |
69 let |
69 (Time.fromMilliseconds (!auto_time_limit)) |
70 val res = TimeLimit.timeLimit |
70 (try seek_against_goal) (); |
71 (Time.fromMilliseconds (! auto_time_limit)) |
71 in |
72 (try seek_against_goal) (); |
72 case Option.join res of |
73 in |
73 NONE => state |
74 case Option.join res of |
74 | SOME results => (Proof.goal_message |
75 NONE => state |
75 (fn () => Pretty.chunks [Pretty.str "", |
76 | SOME results => (Proof.goal_message |
76 Pretty.markup Markup.hilite |
77 (fn () => Pretty.chunks [Pretty.str "", |
77 (Library.separate (Pretty.brk 0) |
78 Pretty.markup Markup.hilite |
78 (map prt_result results))]) |
79 (Library.separate (Pretty.brk 0) |
79 state) |
80 (map prt_result results))]) |
80 end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state); |
81 state) |
81 in |
82 end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state); |
82 if int andalso !auto andalso not (!Toplevel.quiet) |
83 in |
83 then go () |
84 if int andalso ! auto andalso not (! Toplevel.quiet) |
84 else state |
85 then go () |
85 end; |
86 else state |
86 |
87 end; |
|
88 |
87 end; |
89 end; |
88 |
90 |
89 val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution); |
91 val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution); |
90 |
92 |
91 val auto_solve = AutoSolve.auto; |
93 val auto_solve = AutoSolve.auto; |