author  blanchet 
Fri, 27 May 2011 10:30:08 +0200  
changeset 43020  abb5d1f907e4 
parent 43018  121aa59b4d17 
child 43024  58150aa44941 
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 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

13 
val solve_directN: string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

14 
val someN: string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

15 
val noneN: string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

16 
val unknownN: string 
40130  17 
val auto: bool Unsynchronized.ref 
18 
val max_solutions: int Unsynchronized.ref 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

19 
val solve_direct: bool > Proof.state > bool * (string * Proof.state) 
40130  20 
val setup: theory > theory 
30980  21 
end; 
22 

40130  23 
structure Solve_Direct: SOLVE_DIRECT = 
30980  24 
struct 
25 

40129  26 
val solve_directN = "solve_direct"; 
27 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

28 
val someN = "some"; 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

29 
val noneN = "none"; 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

30 
val unknownN = "none"; 
40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

31 

30980  32 
(* preferences *) 
33 

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

36 

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

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

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

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

42 
("Run " ^ quote solve_directN ^ " automatically.")) ()); 
30980  43 

40129  44 

45 
(* solve_direct command *) 

46 

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

47 
fun solve_direct auto state = 
30980  48 
let 
49 
val ctxt = Proof.context_of state; 

50 

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

30980  54 

55 
fun prt_result (goal, results) = 

56 
let 

57 
val msg = 

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

58 
(if auto then "Auto " else "") ^ solve_directN ^ ": " ^ 
30980  59 
(case goal of 
60 
NONE => "The current goal" 

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

62 
in 

63 
Pretty.big_list 

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

64 
(msg ^ " can be solved directly with") 
33301  65 
(map (Find_Theorems.pretty_thm ctxt) results) 
30980  66 
end; 
67 

68 
fun seek_against_goal () = 

33290  69 
(case try Proof.simple_goal state of 
30980  70 
NONE => NONE 
33290  71 
 SOME {goal = st, ...} => 
30980  72 
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

73 
val subgoals = Drule.strip_imp_prems (Thm.cprop_of st); 
30980  74 
val rs = 
75 
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

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

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

40129  80 
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

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

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

83 
SOME (SOME results) => 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

84 
(someN, 
40129  85 
state > 
86 
(if auto then 

87 
Proof.goal_message 

88 
(fn () => 

89 
Pretty.chunks 

90 
[Pretty.str "", 

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

92 
else 

93 
tap (fn _ => 

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

94 
Output.urgent_message (Pretty.string_of (Pretty.chunks (message results)))))) 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

95 
 SOME NONE => (noneN, state) 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

96 
 NONE => (unknownN, state)) 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

97 
end 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

98 
> `(fn (outcome_code, _) => outcome_code = someN); 
30980  99 

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

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

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

40129  105 

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

106 

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

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

108 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

109 
val setup = Try.register_tool (solve_directN, (auto, solve_direct)); 
30980  110 

111 
end; 