author  blanchet 
Fri, 27 May 2011 10:30:08 +0200  
changeset 43018  121aa59b4d17 
parent 40931  061b8257ab9f 
child 43020  abb5d1f907e4 
permissions  rwrr 
40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

1 
(* Title: Tools/solve_direct.ML 
30980  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 

40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

11 
signature SOLVE_DIRECT = 
30980  12 
sig 
40130  13 
val auto: bool Unsynchronized.ref 
14 
val max_solutions: int Unsynchronized.ref 

15 
val solve_direct: bool > Proof.state > bool * Proof.state 

16 
val setup: theory > theory 

30980  17 
end; 
18 

40130  19 
structure Solve_Direct: SOLVE_DIRECT = 
30980  20 
struct 
21 

40129  22 
val solve_directN = "solve_direct"; 
23 

40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

24 

30980  25 
(* preferences *) 
26 

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

29 

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

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

31 
ProofGeneralPgip.add_preference Preferences.category_tracing 
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39329
diff
changeset

32 
(Unsynchronized.setmp auto true (fn () => 
30980  33 
Preferences.bool_pref auto 
40130  34 
"autosolvedirect" 
40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

35 
("Run " ^ quote solve_directN ^ " automatically.")) ()); 
30980  36 

40129  37 

38 
(* solve_direct command *) 

39 

40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

40 
fun solve_direct auto state = 
30980  41 
let 
42 
val ctxt = Proof.context_of state; 

43 

33301  44 
val crits = [(true, Find_Theorems.Solves)]; 
40129  45 
fun find g = 
46 
snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits); 

30980  47 

48 
fun prt_result (goal, results) = 

49 
let 

50 
val msg = 

40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

51 
(if auto then "Auto " else "") ^ solve_directN ^ ": " ^ 
30980  52 
(case goal of 
53 
NONE => "The current goal" 

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

55 
in 

56 
Pretty.big_list 

40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

57 
(msg ^ " can be solved directly with") 
33301  58 
(map (Find_Theorems.pretty_thm ctxt) results) 
30980  59 
end; 
60 

61 
fun seek_against_goal () = 

33290  62 
(case try Proof.simple_goal state of 
30980  63 
NONE => NONE 
33290  64 
 SOME {goal = st, ...} => 
30980  65 
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

66 
val subgoals = Drule.strip_imp_prems (Thm.cprop_of st); 
30980  67 
val rs = 
68 
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

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

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

40129  73 
fun message results = separate (Pretty.brk 0) (map prt_result results); 
40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

74 
in 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

75 
(case try seek_against_goal () of 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

76 
SOME (SOME results) => 
40129  77 
(true, 
78 
state > 

79 
(if auto then 

80 
Proof.goal_message 

81 
(fn () => 

82 
Pretty.chunks 

83 
[Pretty.str "", 

84 
Pretty.markup Markup.hilite (message results)]) 

85 
else 

86 
tap (fn _ => 

40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40130
diff
changeset

87 
Output.urgent_message (Pretty.string_of (Pretty.chunks (message results)))))) 
40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

88 
 _ => (false, state)) 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

89 
end; 
30980  90 

40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

91 
val _ = 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

92 
Outer_Syntax.improper_command solve_directN 
40129  93 
"try to solve conjectures directly with existing theorems" Keyword.diag 
40130  94 
(Scan.succeed 
95 
(Toplevel.keep (fn state => ignore (solve_direct false (Toplevel.proof_of state))))); 

40129  96 

40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

97 

9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

98 
(* hook *) 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

99 

43018  100 
val auto_solve_direct = solve_direct true; 
40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

101 

43018  102 
val setup = Try.register_tool (auto, auto_solve_direct); 
30980  103 

104 
end; 