author  blanchet 
Mon, 25 Oct 2010 10:30:46 +0200  
changeset 40116  9ed3711366c8 
parent 39616  src/Tools/auto_solve.ML@8052101883c3 
child 40129  0843888de43e 
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 

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

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

22 

30980  23 
(* preferences *) 
24 

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

27 

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

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

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

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

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

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

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

35 
fun solve_direct auto 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 = 

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

45 
(if auto then "Auto " else "") ^ solve_directN ^ ": " ^ 
30980  46 
(case goal of 
47 
NONE => "The current goal" 

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

49 
in 

50 
Pretty.big_list 

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

51 
(msg ^ " can be solved directly with") 
33301  52 
(map (Find_Theorems.pretty_thm ctxt) results) 
30980  53 
end; 
54 

55 
fun seek_against_goal () = 

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

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

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

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

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

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

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

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

70 
SOME (SOME results) => 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

71 
(true, state > (if auto then 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

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

73 
(fn () => Pretty.chunks 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

74 
[Pretty.str "", 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

75 
Pretty.markup Markup.hilite (message results)]) 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

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

77 
tap (fn _ => priority (Pretty.string_of 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

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

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

80 
end; 
30980  81 

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

82 
val invoke_solve_direct = fst o solve_direct false 
39329  83 

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

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

85 
Outer_Syntax.improper_command solve_directN 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

86 
"try to solve conjectures directly with existing theorems" Keyword.diag 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

87 
(Scan.succeed (Toplevel.keep (K () o invoke_solve_direct 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

88 
o Toplevel.proof_of))) 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

89 

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

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

91 

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

92 
fun auto_solve_direct state = 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

93 
if not (!auto) then (false, state) else solve_direct true state 
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
39616
diff
changeset

94 

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

95 
val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct) 
30980  96 

97 
end; 