author  blanchet 
Fri, 27 Apr 2012 15:24:37 +0200  
changeset 47790  2e1636e45770 
parent 47773  src/HOL/ex/sledgehammer_tactics.ML@7292038cad2a 
child 47794  4ad62c5f9f88 
permissions  rwrr 
47790  1 
(* Title: HOL/TPTP/sledgehammer_tactics.ML 
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

2 
Author: Jasmin Blanchette, TU Muenchen 
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
41959
diff
changeset

3 
Copyright 2010, 2011 
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

4 

6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

5 
Sledgehammer as a tactic. 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

6 
*) 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

7 

6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

8 
signature SLEDGEHAMMER_TACTICS = 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

9 
sig 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44429
diff
changeset

10 
type relevance_override = Sledgehammer_Filter.relevance_override 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44429
diff
changeset

11 

44429  12 
val sledgehammer_with_metis_tac : 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44429
diff
changeset

13 
Proof.context > (string * string) list > relevance_override > int 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44429
diff
changeset

14 
> tactic 
44429  15 
val sledgehammer_as_oracle_tac : 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44429
diff
changeset

16 
Proof.context > (string * string) list > relevance_override > int 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44429
diff
changeset

17 
> tactic 
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

18 
end; 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

19 

6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

20 
structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

21 
struct 
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
41959
diff
changeset

22 

44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44429
diff
changeset

23 
open Sledgehammer_Filter 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44429
diff
changeset

24 

47773  25 
fun run_prover override_params relevance_override i n ctxt goal = 
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

26 
let 
40921
a516fbdd9931
improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents:
40635
diff
changeset

27 
val chained_ths = [] (* a tactic has no chained ths *) 
45706  28 
val params as {provers, relevance_thresholds, max_relevant, slice, ...} = 
44429  29 
Sledgehammer_Isar.default_params ctxt override_params 
30 
val name = hd provers 

43021  31 
val prover = 
32 
Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name 

40921
a516fbdd9931
improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents:
40635
diff
changeset

33 
val default_max_relevant = 
45706  34 
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name 
40921
a516fbdd9931
improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents:
40635
diff
changeset

35 
val is_built_in_const = 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

36 
Sledgehammer_Provers.is_built_in_const_for_prover ctxt name 
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

37 
val relevance_fudge = 
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

38 
Sledgehammer_Provers.relevance_fudge_for_prover ctxt name 
43088  39 
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i 
44625  40 
val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers 
40921
a516fbdd9931
improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents:
40635
diff
changeset

41 
val facts = 
44625  42 
Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override 
44586  43 
chained_ths hyp_ts concl_t 
44625  44 
> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds 
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel)  this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43212
diff
changeset

45 
(the_default default_max_relevant max_relevant) is_built_in_const 
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel)  this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43212
diff
changeset

46 
relevance_fudge relevance_override chained_ths hyp_ts concl_t 
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

47 
val problem = 
41090  48 
{state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, 
47532  49 
facts = map Sledgehammer_Provers.Untranslated_Fact facts} 
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

50 
in 
45520  51 
(case prover params (K (K (K ""))) problem of 
40921
a516fbdd9931
improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents:
40635
diff
changeset

52 
{outcome = NONE, used_facts, ...} => used_facts > map fst > SOME 
a516fbdd9931
improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents:
40635
diff
changeset

53 
 _ => NONE) 
a516fbdd9931
improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents:
40635
diff
changeset

54 
handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) 
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

55 
end 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

56 

6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

57 
fun thms_of_name ctxt name = 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

58 
let 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

59 
val lex = Keyword.get_lexicons 
42361  60 
val get = maps (Proof_Context.get_fact ctxt o fst) 
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

61 
in 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

62 
Source.of_string name 
40635
47004929bc71
ported sledgehammer_tactic to current development version
bulwahn
parents:
40633
diff
changeset

63 
> Symbol.source 
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

64 
> Token.source {do_recover=SOME false} lex Position.start 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

65 
> Token.source_proper 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

66 
> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

67 
> Source.exhaust 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

68 
end 
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

69 

44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44429
diff
changeset

70 
fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th = 
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

71 
let 
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

72 
val override_params = 
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

73 
override_params @ 
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

74 
[("preplay_timeout", "0")] 
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

75 
in 
47773  76 
case run_prover override_params relevance_override i i ctxt th of 
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

77 
SOME facts => 
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

78 
Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt 
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

79 
(maps (thms_of_name ctxt) facts) i th 
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

80 
 NONE => Seq.empty 
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

81 
end 
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

82 

44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44429
diff
changeset

83 
fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th = 
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

84 
let 
42361  85 
val thy = Proof_Context.theory_of ctxt 
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

86 
val override_params = 
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

87 
override_params @ 
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

88 
[("preplay_timeout", "0"), 
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset

89 
("minimize", "false")] 
47773  90 
val xs = run_prover override_params relevance_override i i ctxt th 
41357
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41243
diff
changeset

91 
in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end 
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41243
diff
changeset

92 

40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for noninteractive use
bulwahn
parents:
diff
changeset

93 
end; 