author  wenzelm 
Wed, 28 Oct 2009 22:02:53 +0100  
changeset 33290  6dcb0a970783 
parent 32966  5b21661fe618 
child 33301  1fe9fc908ec3 
permissions  rwrr 
30980  1 
(* Title: Tools/auto_solve.ML 
2 
Author: Timothy Bourke and Gerwin Klein, NICTA 

3 

4 
Check whether a newly stated theorem can be solved directly by an 

5 
existing theorem. Duplicate lemmas can be detected in this way. 

6 

7 
The implementation is based in part on Berghofer and Haftmann's 

8 
quickcheck.ML. It relies critically on the FindTheorems solves 

9 
feature. 

10 
*) 

11 

12 
signature AUTO_SOLVE = 

13 
sig 

32740  14 
val auto : bool Unsynchronized.ref 
15 
val auto_time_limit : int Unsynchronized.ref 

16 
val limit : int Unsynchronized.ref 

30980  17 
end; 
18 

32860
a4ab5d0cccd1
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents:
32740
diff
changeset

19 
structure Auto_Solve : AUTO_SOLVE = 
30980  20 
struct 
21 

22 
(* preferences *) 

23 

32740  24 
val auto = Unsynchronized.ref false; 
25 
val auto_time_limit = Unsynchronized.ref 2500; 

26 
val limit = Unsynchronized.ref 5; 

30980  27 

28 
val _ = 

29 
ProofGeneralPgip.add_preference Preferences.category_tracing 

32966
5b21661fe618
indicate CRITICAL nature of various setmp combinators;
wenzelm
parents:
32860
diff
changeset

30 
(setmp_CRITICAL auto true (fn () => 
30980  31 
Preferences.bool_pref auto 
32 
"autosolve" 

33 
"Try to solve newly declared lemmas with existing theorems.") ()); 

34 

35 
val _ = 

36 
ProofGeneralPgip.add_preference Preferences.category_tracing 

37 
(Preferences.nat_pref auto_time_limit 

38 
"autosolvetimelimit" 

39 
"Time limit for seeking automatic solutions (in milliseconds)."); 

40 

41 

42 
(* hook *) 

43 

44 
val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state => 

45 
let 

46 
val ctxt = Proof.context_of state; 

47 

48 
val crits = [(true, FindTheorems.Solves)]; 

49 
fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits); 

50 

51 
fun prt_result (goal, results) = 

52 
let 

53 
val msg = 

54 
(case goal of 

55 
NONE => "The current goal" 

56 
 SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg)); 

57 
in 

58 
Pretty.big_list 

59 
(msg ^ " could be solved directly with:") 

60 
(map (FindTheorems.pretty_thm ctxt) results) 

61 
end; 

62 

63 
fun seek_against_goal () = 

33290  64 
(case try Proof.simple_goal state of 
30980  65 
NONE => NONE 
33290  66 
 SOME {goal = st, ...} => 
30980  67 
let 
32860
a4ab5d0cccd1
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents:
32740
diff
changeset

68 
val subgoals = Drule.strip_imp_prems (Thm.cprop_of st); 
30980  69 
val rs = 
70 
if length subgoals = 1 

32860
a4ab5d0cccd1
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents:
32740
diff
changeset

71 
then [(NONE, find st)] 
30980  72 
else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals; 
73 
val results = filter_out (null o snd) rs; 

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

75 

76 
fun go () = 

77 
let 

78 
val res = 

79 
TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit)) 

80 
(try seek_against_goal) (); 

81 
in 

82 
(case res of 

83 
SOME (SOME results) => 

84 
state > Proof.goal_message 

85 
(fn () => Pretty.chunks 

86 
[Pretty.str "", 

87 
Pretty.markup Markup.hilite 

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

89 
 _ => state) 

32860
a4ab5d0cccd1
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents:
32740
diff
changeset

90 
end handle TimeLimit.TimeOut => (warning "Auto solve: timeout"; state); 
30980  91 
in 
92 
if int andalso ! auto andalso not (! Toplevel.quiet) 

93 
then go () 

94 
else state 

95 
end)); 

96 

97 
end; 

98 

32860
a4ab5d0cccd1
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents:
32740
diff
changeset

99 
val auto_solve = Auto_Solve.auto; 
a4ab5d0cccd1
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents:
32740
diff
changeset

100 
val auto_solve_time_limit = Auto_Solve.auto_time_limit; 
30980  101 