author  blanchet 
Sat, 11 Sep 2010 12:32:31 +0200  
changeset 39329  0a85f960ac50 
parent 39138  53886463f559 
child 39616  8052101883c3 
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 

39329  7 
The implementation relies critically on the Find_Theorems solves 
30980  8 
feature. 
9 
*) 

10 

11 
signature AUTO_SOLVE = 

12 
sig 

32740  13 
val auto : bool Unsynchronized.ref 
39329  14 
val max_solutions : int Unsynchronized.ref 
15 
val setup : theory > theory 

30980  16 
end; 
17 

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

18 
structure Auto_Solve : AUTO_SOLVE = 
30980  19 
struct 
20 

21 
(* preferences *) 

22 

32740  23 
val auto = Unsynchronized.ref false; 
39329  24 
val max_solutions = Unsynchronized.ref 5; 
33889
4328de748fb2
some rearangement of load order to keep preferences adjacent  slightly fragile;
wenzelm
parents:
33301
diff
changeset

25 

4328de748fb2
some rearangement of load order to keep preferences adjacent  slightly fragile;
wenzelm
parents:
33301
diff
changeset

26 
val _ = 
4328de748fb2
some rearangement of load order to keep preferences adjacent  slightly fragile;
wenzelm
parents:
33301
diff
changeset

27 
ProofGeneralPgip.add_preference Preferences.category_tracing 
39138
53886463f559
use setmp_noncritical for sequential Pure bootstrap;
wenzelm
parents:
33889
diff
changeset

28 
(setmp_noncritical auto true (fn () => 
30980  29 
Preferences.bool_pref auto 
39329  30 
"autosolve" "Try to solve conjectures with existing theorems.") ()); 
30980  31 

32 

33 
(* hook *) 

34 

39329  35 
fun auto_solve state = 
30980  36 
let 
37 
val ctxt = Proof.context_of state; 

38 

33301  39 
val crits = [(true, Find_Theorems.Solves)]; 
39329  40 
fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits); 
30980  41 

42 
fun prt_result (goal, results) = 

43 
let 

44 
val msg = 

45 
(case goal of 

46 
NONE => "The current goal" 

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

48 
in 

49 
Pretty.big_list 

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

33301  51 
(map (Find_Theorems.pretty_thm ctxt) results) 
30980  52 
end; 
53 

54 
fun seek_against_goal () = 

33290  55 
(case try Proof.simple_goal state of 
30980  56 
NONE => NONE 
33290  57 
 SOME {goal = st, ...} => 
30980  58 
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

59 
val subgoals = Drule.strip_imp_prems (Thm.cprop_of st); 
30980  60 
val rs = 
61 
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

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

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

66 

67 
fun go () = 

39329  68 
(case try seek_against_goal () of 
69 
SOME (SOME results) => 

70 
(true, state > Proof.goal_message 

71 
(fn () => Pretty.chunks 

72 
[Pretty.str "", 

73 
Pretty.markup Markup.hilite 

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

75 
 _ => (false, state)); 

76 
in if not (!auto) then (false, state) else go () end; 

77 

78 
val setup = Auto_Tools.register_tool ("solve", auto_solve) 

30980  79 

80 
end; 