author  wenzelm 
Mon, 25 Oct 2010 16:41:23 +0200  
changeset 40129  0843888de43e 
parent 40116  9ed3711366c8 
child 40130  db6e84082695 
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 
32740  13 
val auto : bool Unsynchronized.ref 
39329  14 
val max_solutions : int Unsynchronized.ref 
15 
val setup : theory > theory 

30980  16 
end; 
17 

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

18 
structure Solve_Direct : SOLVE_DIRECT = 
30980  19 
struct 
20 

40129  21 
val solve_directN = "solve_direct"; 
22 

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

23 

30980  24 
(* preferences *) 
25 

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

28 

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

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

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

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

33 
("Auto " ^ solve_directN) 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

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

40129  36 

37 
(* solve_direct command *) 

38 

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

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

42 

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

30980  46 

47 
fun prt_result (goal, results) = 

48 
let 

49 
val msg = 

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

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

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

54 
in 

55 
Pretty.big_list 

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

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

60 
fun seek_against_goal () = 

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

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

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

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

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

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

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

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

78 
(if auto then 

79 
Proof.goal_message 

80 
(fn () => 

81 
Pretty.chunks 

82 
[Pretty.str "", 

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

84 
else 

85 
tap (fn _ => 

86 
priority (Pretty.string_of (Pretty.chunks (message results)))))) 

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

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

88 
end; 
30980  89 

40129  90 
val invoke_solve_direct = fst o solve_direct false; 
39329  91 

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

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

93 
Outer_Syntax.improper_command solve_directN 
40129  94 
"try to solve conjectures directly with existing theorems" Keyword.diag 
95 
(Scan.succeed (Toplevel.keep (K () o invoke_solve_direct o Toplevel.proof_of))); 

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 

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

100 
fun auto_solve_direct state = 
40129  101 
if not (! auto) then (false, state) else solve_direct true state; 
40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

102 

40129  103 
val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct); 
30980  104 

105 
end; 