author  Timothy Bourke 
Mon, 30 Mar 2009 12:25:52 +1100  
changeset 30785  15f64e05e703 
parent 30242  aea5d7fa7ef5 
child 30822  8aac4b974280 
permissions  rwrr 
30147  1 
(* Title: Pure/Tools/auto_solve.ML 
29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

2 
Author: Timothy Bourke and Gerwin Klein, NICTA 
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

3 

30147  4 
Check whether a newly stated theorem can be solved directly by an 
5 
existing theorem. Duplicate lemmas can be detected in this way. 

29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

6 

30147  7 
The implemenation is based in part on Berghofer and Haftmann's 
8 
Pure/codegen.ML. It relies critically on the FindTheorems solves 

9 
feature. 

29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

10 
*) 
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

11 

c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

12 
signature AUTO_SOLVE = 
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

13 
sig 
30147  14 
val auto : bool ref 
15 
val auto_time_limit : int ref 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30242
diff
changeset

16 
val limit : int ref 
29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

17 

30147  18 
val seek_solution : bool > Proof.state > Proof.state 
29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

19 
end; 
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

20 

c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

21 
structure AutoSolve : AUTO_SOLVE = 
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

22 
struct 
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

23 

30147  24 
val auto = ref false; 
25 
val auto_time_limit = ref 2500; 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30242
diff
changeset

26 
val limit = ref 5; 
29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

27 

30147  28 
fun seek_solution int state = 
29 
let 

30 
val ctxt = Proof.context_of state; 

29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

31 

30147  32 
fun conj_to_list [] = [] 
33 
 conj_to_list (t::ts) = 

34 
(Conjunction.dest_conjunction t 

35 
> (fn (t1, t2) => conj_to_list (t1::t2::ts))) 

36 
handle TERM _ => t::conj_to_list ts; 

29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

37 

30147  38 
val crits = [(true, FindTheorems.Solves)]; 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30242
diff
changeset

39 
fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (!limit)) false crits)); 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30242
diff
changeset

40 
fun find_cterm g = (SOME g, snd (FindTheorems.find_theorems ctxt 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30242
diff
changeset

41 
(SOME (Goal.init g)) (SOME (!limit)) false crits)); 
29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

42 

30147  43 
fun prt_result (goal, results) = 
44 
let 

45 
val msg = case goal of 

46 
NONE => "The current goal" 

47 
 SOME g => Syntax.string_of_term ctxt (term_of g); 

48 
in 

49 
Pretty.big_list (msg ^ " could be solved directly with:") 

30186
1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30147
diff
changeset

50 
(map (FindTheorems.pretty_thm ctxt) results) 
30147  51 
end; 
29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

52 

30147  53 
fun seek_against_goal () = 
54 
let 

55 
val goal = try Proof.get_goal state 

56 
> Option.map (#2 o #2); 

29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

57 

30147  58 
val goals = goal 
59 
> Option.map (fn g => cprem_of g 1) 

60 
> the_list 

61 
> conj_to_list; 

29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

62 

30147  63 
val rs = if length goals = 1 
64 
then [find goal] 

65 
else map find_cterm goals; 

66 
val frs = filter_out (null o snd) rs; 

29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

67 

30147  68 
in if null frs then NONE else SOME frs end; 
29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

69 

30147  70 
fun go () = 
71 
let 

72 
val res = TimeLimit.timeLimit 

73 
(Time.fromMilliseconds (! auto_time_limit)) 

74 
(try seek_against_goal) (); 

75 
in 

76 
case Option.join res of 

77 
NONE => state 

78 
 SOME results => (Proof.goal_message 

79 
(fn () => Pretty.chunks [Pretty.str "", 

80 
Pretty.markup Markup.hilite 

81 
(Library.separate (Pretty.brk 0) 

82 
(map prt_result results))]) 

83 
state) 

84 
end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state); 

85 
in 

86 
if int andalso ! auto andalso not (! Toplevel.quiet) 

87 
then go () 

88 
else state 

89 
end; 

90 

29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

91 
end; 
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

92 

c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

93 
val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution); 
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

94 

c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

95 
val auto_solve = AutoSolve.auto; 
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

96 
val auto_solve_time_limit = AutoSolve.auto_time_limit; 
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

97 