author  wenzelm 
Tue, 31 Mar 2009 22:23:33 +0200  
changeset 30825  14d24e1fe594 
parent 30822  8aac4b974280 
child 31007  7c871a9cf6f4 
permissions  rwrr 
30825  1 
(* Title: 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 
30825  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 

30825  7 
The implementation is based in part on Berghofer and Haftmann's 
8 
quickcheck.ML. It relies critically on the FindTheorems solves 

30147  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 
val crits = [(true, FindTheorems.Solves)]; 
30825  33 
fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits); 
29858
c8cee17d7e50
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff
changeset

34 

30147  35 
fun prt_result (goal, results) = 
36 
let 

30822  37 
val msg = 
38 
(case goal of 

39 
NONE => "The current goal" 

30825  40 
 SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg)); 
30147  41 
in 
30822  42 
Pretty.big_list 
43 
(msg ^ " could be solved directly with:") 

44 
(map (FindTheorems.pretty_thm ctxt) results) 

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

46 

30147  47 
fun seek_against_goal () = 
30825  48 
(case try Proof.get_goal state of 
49 
NONE => NONE 

50 
 SOME (_, (_, goal)) => 

51 
let 

52 
val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1); 

53 
val rs = 

54 
if length subgoals = 1 

55 
then [(NONE, find goal)] 

56 
else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals; 

57 
val results = filter_out (null o snd) rs; 

58 
in if null results then NONE else SOME results end); 

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

59 

30147  60 
fun go () = 
61 
let 

30822  62 
val res = 
63 
TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit)) 

64 
(try seek_against_goal) (); 

30147  65 
in 
30822  66 
(case res of 
67 
SOME (SOME results) => 

68 
state > Proof.goal_message 

69 
(fn () => Pretty.chunks 

70 
[Pretty.str "", 

71 
Pretty.markup Markup.hilite 

72 
(separate (Pretty.brk 0) (map prt_result results))]) 

30825  73 
 _ => state) 
30147  74 
end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state); 
75 
in 

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

77 
then go () 

78 
else state 

79 
end; 

80 

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

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

82 

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

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

84 

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

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

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

87 