author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 56467  8d7d6f17c6a7 
child 58842  22b87ab47d3b 
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 max_solutions: int Unsynchronized.ref 
43025
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

18 
val solve_direct: Proof.state > bool * (string * Proof.state) 
30980  19 
end; 
20 

40130  21 
structure Solve_Direct: SOLVE_DIRECT = 
30980  22 
struct 
23 

43025
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

24 
datatype mode = Auto_Try  Try  Normal 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

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 

52701
51dfdcd88e84
guard unify tracing via visible status of global theory;
wenzelm
parents:
52645
diff
changeset

32 

30980  33 
(* preferences *) 
34 

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 _ = 
52639  38 
ProofGeneral.preference_option ProofGeneral.category_tracing 
52645  39 
NONE 
56467  40 
@{system_option auto_solve_direct} 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52007
diff
changeset

41 
"autosolvedirect" 
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52007
diff
changeset

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

40129  44 

45 
(* solve_direct command *) 

46 

43025
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

47 
fun do_solve_direct mode state = 
30980  48 
let 
49 
val ctxt = Proof.context_of state; 

52701
51dfdcd88e84
guard unify tracing via visible status of global theory;
wenzelm
parents:
52645
diff
changeset

50 
val find_ctxt = if mode = Auto_Try then Context_Position.set_visible false ctxt else ctxt; 
30980  51 

33301  52 
val crits = [(true, Find_Theorems.Solves)]; 
40129  53 
fun find g = 
52701
51dfdcd88e84
guard unify tracing via visible status of global theory;
wenzelm
parents:
52645
diff
changeset

54 
snd (Find_Theorems.find_theorems find_ctxt (SOME g) (SOME (! max_solutions)) false crits); 
30980  55 

56 
fun prt_result (goal, results) = 

57 
let 

58 
val msg = 

43025
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

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

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

63 
in 

64 
Pretty.big_list 

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

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

69 
fun seek_against_goal () = 

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

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

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

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

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

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

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

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

85 
(someN, 
40129  86 
state > 
43025
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

87 
(if mode = Auto_Try then 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

88 
Proof.goal_message 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

89 
(fn () => 
52643
34c29356930e
more explicit Markup.information for messages produced by "auto" tools;
wenzelm
parents:
52641
diff
changeset

90 
Pretty.markup Markup.information (message results)) 
43025
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

91 
else 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

92 
tap (fn _ => 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

93 
Output.urgent_message (Pretty.string_of (Pretty.chunks (message results)))))) 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

94 
 SOME NONE => 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

95 
(if mode = Normal then Output.urgent_message "No proof found." 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

96 
else (); 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

97 
(noneN, state)) 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

98 
 NONE => 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

99 
(if mode = Normal then Output.urgent_message "An error occurred." 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

100 
else (); 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

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

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

103 
> `(fn (outcome_code, _) => outcome_code = someN); 
30980  104 

43025
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

105 
val solve_direct = do_solve_direct Normal 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

106 

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

107 
val _ = 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45666
diff
changeset

108 
Outer_Syntax.improper_command @{command_spec "solve_direct"} 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45666
diff
changeset

109 
"try to solve conjectures directly with existing theorems" 
51557
4e4b56b7a3a5
more robust access Toplevel.proof_of  prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
wenzelm
parents:
50201
diff
changeset

110 
(Scan.succeed (Toplevel.unknown_proof o 
4e4b56b7a3a5
more robust access Toplevel.proof_of  prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
wenzelm
parents:
50201
diff
changeset

111 
Toplevel.keep (ignore o solve_direct o Toplevel.proof_of))); 
40129  112 

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

113 

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

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

115 

43025
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

116 
fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try) 
5a0dec7bc099
handle nonauto try case gracefully in Solve Direct
blanchet
parents:
43024
diff
changeset

117 

56467  118 
val _ = Try.tool_setup (solve_directN, (10, @{system_option auto_solve_direct}, try_solve_direct)); 
30980  119 

120 
end; 