author  wenzelm 
Thu, 01 Oct 2009 00:32:00 +0200  
changeset 32798  4b85b59a9f66 
parent 32738  15bb09ca0378 
child 32859  204f749f35a9 
permissions  rwrr 
30143  1 
(* Title: Pure/Tools/find_theorems.ML 
26283  2 
Author: Rafal Kolanski and Gerwin Klein, NICTA 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

3 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

4 
Retrieve theorems from proof context. 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

5 
*) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

6 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

7 
signature FIND_THEOREMS = 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

8 
sig 
16036  9 
datatype 'term criterion = 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

10 
Name of string  Intro  IntroIff  Elim  Dest  Solves  Simp of 'term  
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

11 
Pattern of 'term 
32738  12 
val tac_limit: int Unsynchronized.ref 
13 
val limit: int Unsynchronized.ref 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

14 
val find_theorems: Proof.context > thm option > int option > bool > 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

15 
(bool * string criterion) list > int option * (Facts.ref * thm) list 
30186
1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30143
diff
changeset

16 
val pretty_thm: Proof.context > Facts.ref * thm > Pretty.T 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

17 
val print_theorems: Proof.context > thm option > int option > bool > 
16036  18 
(bool * string criterion) list > unit 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

19 
end; 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

20 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

21 
structure FindTheorems: FIND_THEOREMS = 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

22 
struct 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

23 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

24 
(** search criteria **) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

25 

16036  26 
datatype 'term criterion = 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

27 
Name of string  Intro  IntroIff  Elim  Dest  Solves  Simp of 'term  
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

28 
Pattern of 'term; 
16036  29 

30 
fun read_criterion _ (Name name) = Name name 

31 
 read_criterion _ Intro = Intro 

31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

32 
 read_criterion _ IntroIff = IntroIff 
16036  33 
 read_criterion _ Elim = Elim 
34 
 read_criterion _ Dest = Dest 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

35 
 read_criterion _ Solves = Solves 
24683  36 
 read_criterion ctxt (Simp str) = Simp (ProofContext.read_term_pattern ctxt str) 
37 
 read_criterion ctxt (Pattern str) = Pattern (ProofContext.read_term_pattern ctxt str); 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

38 

16036  39 
fun pretty_criterion ctxt (b, c) = 
40 
let 

41 
fun prfx s = if b then s else "" ^ s; 

42 
in 

43 
(case c of 

44 
Name name => Pretty.str (prfx "name: " ^ quote name) 

45 
 Intro => Pretty.str (prfx "intro") 

31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

46 
 IntroIff => Pretty.str (prfx "introiff") 
16036  47 
 Elim => Pretty.str (prfx "elim") 
48 
 Dest => Pretty.str (prfx "dest") 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

49 
 Solves => Pretty.str (prfx "solves") 
16088  50 
 Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1, 
24920  51 
Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))] 
16036  52 
 Pattern pat => Pretty.enclose (prfx " \"") "\"" 
24920  53 
[Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)]) 
16036  54 
end; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

55 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

56 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

57 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

58 
(** search criterion filters **) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

59 

16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

60 
(*generated filters are to be of the form 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

61 
input: (Facts.ref * thm) 
17106  62 
output: (p:int, s:int) option, where 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

63 
NONE indicates no match 
17106  64 
p is the primary sorting criterion 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

65 
(eg. number of assumptions in the theorem) 
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

66 
s is the secondary sorting criterion 
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

67 
(eg. size of the substitution for intro, elim and dest) 
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

68 
when applying a set of filters to a thm, fold results in: 
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

69 
(biggest p, sum of all s) 
17106  70 
currently p and s only matter for intro, elim, dest and simp filters, 
71 
otherwise the default ordering is used. 

16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

72 
*) 
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

73 

16088  74 

75 
(* matching theorems *) 

17106  76 

17205  77 
fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy; 
16088  78 

32798  79 
(*educated guesses on HOL*) (* FIXME broken *) 
80 
val boolT = Type ("bool", []); 

81 
val iff_const = Const ("op =", boolT > boolT > boolT); 

31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

82 

16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

83 
(*extract terms from term_src, refine them to the parts that concern us, 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

84 
if po try match them against obj else vice versa. 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

85 
trivial matches are ignored. 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

86 
returns: smallest substitution size*) 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

87 
fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src = 
16088  88 
let 
17106  89 
val thy = ProofContext.theory_of ctxt; 
16088  90 

32798  91 
fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat)); 
16486  92 
fun matches pat = 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

93 
let 
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

94 
val jpat = ObjectLogic.drop_judgment thy pat; 
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

95 
val c = Term.head_of jpat; 
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

96 
val pats = 
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

97 
if Term.is_Const c 
32798  98 
then 
99 
if doiff andalso c = iff_const then 

100 
(pat :: map (ObjectLogic.ensure_propT thy) (snd (strip_comb jpat))) 

101 
> filter (is_nontrivial thy) 

102 
else [pat] 

31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

103 
else []; 
32798  104 
in filter check_match pats end; 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

105 

df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

106 
fun substsize pat = 
18184  107 
let val (_, subst) = 
108 
Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty) 

17205  109 
in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end; 
16088  110 

16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

111 
fun bestmatch [] = NONE 
32798  112 
 bestmatch xs = SOME (foldr1 Int.min xs); 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

113 

16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

114 
val match_thm = matches o refine_term; 
16486  115 
in 
32798  116 
maps match_thm (extract_terms term_src) 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

117 
> map substsize 
26283  118 
> bestmatch 
16088  119 
end; 
120 

121 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

122 
(* filter_name *) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

123 

17106  124 
fun filter_name str_pat (thmref, _) = 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

125 
if match_string str_pat (Facts.name_of_ref thmref) 
17205  126 
then SOME (0, 0) else NONE; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

127 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

128 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

129 
(* filter intro/elim/dest/solves rules *) 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

130 

17205  131 
fun filter_dest ctxt goal (_, thm) = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

132 
let 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

133 
val extract_dest = 
17205  134 
(fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm], 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

135 
hd o Logic.strip_imp_prems); 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

136 
val prems = Logic.prems_of_goal goal 1; 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

137 

31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

138 
fun try_subst prem = is_matching_thm false extract_dest ctxt true prem thm; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19476
diff
changeset

139 
val successful = prems > map_filter try_subst; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

140 
in 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

141 
(*if possible, keep best substitution (one with smallest size)*) 
17106  142 
(*dest rules always have assumptions, so a dest with one 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

143 
assumption is as good as an intro rule with none*) 
17205  144 
if not (null successful) 
145 
then SOME (Thm.nprems_of thm  1, foldr1 Int.min successful) else NONE 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

146 
end; 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

147 

31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

148 
fun filter_intro doiff ctxt goal (_, thm) = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

149 
let 
17205  150 
val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl); 
16036  151 
val concl = Logic.concl_of_goal goal 1; 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

152 
val ss = is_matching_thm doiff extract_intro ctxt true concl thm; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

153 
in 
18939  154 
if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

155 
end; 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

156 

17205  157 
fun filter_elim ctxt goal (_, thm) = 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

158 
if not (Thm.no_prems thm) then 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

159 
let 
17205  160 
val rule = Thm.full_prop_of thm; 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

161 
val prems = Logic.prems_of_goal goal 1; 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

162 
val goal_concl = Logic.concl_of_goal goal 1; 
26283  163 
val rule_mp = hd (Logic.strip_imp_prems rule); 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

164 
val rule_concl = Logic.strip_imp_concl rule; 
26283  165 
fun combine t1 t2 = Const ("*combine*", dummyT > dummyT) $ (t1 $ t2); 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

166 
val rule_tree = combine rule_mp rule_concl; 
26283  167 
fun goal_tree prem = combine prem goal_concl; 
17106  168 
fun try_subst prem = 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

169 
is_matching_thm false (single, I) ctxt true (goal_tree prem) rule_tree; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19476
diff
changeset

170 
val successful = prems > map_filter try_subst; 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

171 
in 
32798  172 
(*elim rules always have assumptions, so an elim with one 
173 
assumption is as good as an intro rule with none*) 

17106  174 
if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm) 
17205  175 
andalso not (null successful) 
176 
then SOME (Thm.nprems_of thm  1, foldr1 Int.min successful) else NONE 

16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

177 
end 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

178 
else NONE 
16036  179 

32738  180 
val tac_limit = Unsynchronized.ref 5; 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

181 

30143  182 
fun filter_solves ctxt goal = 
183 
let 

184 
fun etacn thm i = Seq.take (! tac_limit) o etac thm i; 

185 
fun try_thm thm = 

186 
if Thm.no_prems thm then rtac thm 1 goal 

30318
3d03190d2864
replaced archaic use of rep_ss by Simplifier.mksimps;
wenzelm
parents:
30234
diff
changeset

187 
else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal; 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

188 
in 
30143  189 
fn (_, thm) => 
32798  190 
if is_some (Seq.pull (try_thm thm)) 
30143  191 
then SOME (Thm.nprems_of thm, 0) else NONE 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

192 
end; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

193 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

194 

16074  195 
(* filter_simp *) 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

196 

17205  197 
fun filter_simp ctxt t (_, thm) = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

198 
let 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

199 
val mksimps = Simplifier.mksimps (simpset_of ctxt); 
17106  200 
val extract_simp = 
30318
3d03190d2864
replaced archaic use of rep_ss by Simplifier.mksimps;
wenzelm
parents:
30234
diff
changeset

201 
(map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

202 
val ss = is_matching_thm false extract_simp ctxt false t thm; 
17106  203 
in 
18939  204 
if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

205 
end; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

206 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

207 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

208 
(* filter_pattern *) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

209 

32798  210 
fun get_names t = Term.add_const_names t (Term.add_free_names t []); 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

211 
fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm); 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

212 

30143  213 
(*Including all constants and frees is only sound because 
214 
matching uses higherorder patterns. If full matching 

215 
were used, then constants that may be subject to 

216 
betareduction after substitution of frees should 

217 
not be included for LHS set because they could be 

218 
thrown away by the substituted function. 

219 
e.g. for (?F 1 2) do not include 1 or 2, if it were 

220 
possible for ?F to be (% x y. 3) 

221 
The largest possible set should always be included on 

222 
the RHS.*) 

223 

224 
fun filter_pattern ctxt pat = 

225 
let 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

226 
val pat_consts = get_names pat; 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

227 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

228 
fun check (t, NONE) = check (t, SOME (get_thm_names t)) 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

229 
 check ((_, thm), c as SOME thm_consts) = 
32798  230 
(if pat_consts subset_string thm_consts andalso 
231 
Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm) 

232 
then SOME (0, 0) else NONE, c); 

28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

233 
in check end; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

234 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

235 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

236 
(* interpret criteria as filters *) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

237 

16036  238 
local 
239 

240 
fun err_no_goal c = 

241 
error ("Current goal required for " ^ c ^ " search criterion"); 

242 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

243 
val fix_goal = Thm.prop_of; 
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

244 

28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

245 
fun filter_crit _ _ (Name name) = apfst (filter_name name) 
16036  246 
 filter_crit _ NONE Intro = err_no_goal "intro" 
247 
 filter_crit _ NONE Elim = err_no_goal "elim" 

248 
 filter_crit _ NONE Dest = err_no_goal "dest" 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

249 
 filter_crit _ NONE Solves = err_no_goal "solves" 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

250 
 filter_crit ctxt (SOME goal) Intro = apfst (filter_intro false ctxt (fix_goal goal)) 
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

251 
 filter_crit ctxt (SOME goal) IntroIff = apfst (filter_intro true ctxt (fix_goal goal)) 
30143  252 
 filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal)) 
253 
 filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal)) 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

254 
 filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal) 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

255 
 filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat) 
16088  256 
 filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat; 
16036  257 

19502  258 
fun opt_not x = if is_some x then NONE else SOME (0, 0); 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

259 

17756  260 
fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int) 
26283  261 
 opt_add _ _ = NONE; 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

262 

30143  263 
fun app_filters thm = 
264 
let 

28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

265 
fun app (NONE, _, _) = NONE 
32798  266 
 app (SOME v, _, []) = SOME (v, thm) 
30143  267 
 app (r, consts, f :: fs) = 
268 
let val (r', consts') = f (thm, consts) 

269 
in app (opt_add r r', consts', fs) end; 

28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

270 
in app end; 
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

271 

31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
31042
diff
changeset

272 

16036  273 
in 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

274 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

275 
fun filter_criterion ctxt opt_goal (b, c) = 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

276 
(if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c; 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

277 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

278 
fun sorted_filter filters thms = 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

279 
let 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

280 
fun eval_filters thm = app_filters thm (SOME (0, 0), NONE, filters); 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

281 

16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

282 
(*filters return: (number of assumptions, substitution size) option, so 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

283 
sort (desc. in both cases) according to number of assumptions first, 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

284 
then by the substitution size*) 
17205  285 
fun thm_ord (((p0, s0), _), ((p1, s1), _)) = 
286 
prod_ord int_ord int_ord ((p1, s1), (p0, s0)); 

28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

287 
in map_filter eval_filters thms > sort thm_ord > map #2 end; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

288 

30822  289 
fun lazy_filter filters = 
290 
let 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

291 
fun lazy_match thms = Seq.make (fn () => first_match thms) 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

292 

15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

293 
and first_match [] = NONE 
30822  294 
 first_match (thm :: thms) = 
295 
(case app_filters thm (SOME (0, 0), NONE, filters) of 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

296 
NONE => first_match thms 
30822  297 
 SOME (_, t) => SOME (t, lazy_match thms)); 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

298 
in lazy_match end; 
30822  299 

16036  300 
end; 
301 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

302 

22414  303 
(* removing duplicates, preferring nicer names, roughly n log n *) 
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset

304 

25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

305 
local 
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

306 

27486  307 
val index_ord = option_ord (K EQUAL); 
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

308 
val hidden_ord = bool_ord o pairself NameSpace.is_hidden; 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30318
diff
changeset

309 
val qual_ord = int_ord o pairself (length o Long_Name.explode); 
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

310 
val txt_ord = int_ord o pairself size; 
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

311 

27486  312 
fun nicer_name (x, i) (y, j) = 
313 
(case hidden_ord (x, y) of EQUAL => 

314 
(case index_ord (i, j) of EQUAL => 

315 
(case qual_ord (x, y) of EQUAL => txt_ord (x, y)  ord => ord) 

316 
 ord => ord) 

25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

317 
 ord => ord) <> GREATER; 
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

318 

29848  319 
fun rem_cdups nicer xs = 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

320 
let 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

321 
fun rem_c rev_seen [] = rev rev_seen 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

322 
 rem_c rev_seen [x] = rem_c (x :: rev_seen) [] 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

323 
 rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) = 
30822  324 
if Thm.eq_thm_prop (t, t') 
325 
then rem_c rev_seen ((if nicer n n' then x else y) :: xs) 

326 
else rem_c (x :: rev_seen) (y :: xs) 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

327 
in rem_c [] xs end; 
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

328 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

329 
in 
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

330 

30143  331 
fun nicer_shortest ctxt = 
332 
let 

30216
0300b7420b07
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm
parents:
30188
diff
changeset

333 
(* FIXME global name space!? *) 
0300b7420b07
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm
parents:
30188
diff
changeset

334 
val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt)); 
29848  335 

30216
0300b7420b07
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm
parents:
30188
diff
changeset

336 
val shorten = 
0300b7420b07
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm
parents:
30188
diff
changeset

337 
NameSpace.extern_flags {long_names = false, short_names = false, unique_names = false} space; 
29848  338 

339 
fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = 

340 
nicer_name (shorten x, i) (shorten y, j) 

341 
 nicer (Facts.Fact _) (Facts.Named _) = true 

342 
 nicer (Facts.Named _) (Facts.Fact _) = false; 

343 
in nicer end; 

344 

345 
fun rem_thm_dups nicer xs = 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

346 
xs ~~ (1 upto length xs) 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28900
diff
changeset

347 
> sort (TermOrd.fast_term_ord o pairself (Thm.prop_of o #2 o #1)) 
29848  348 
> rem_cdups nicer 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

349 
> sort (int_ord o pairself #2) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

350 
> map #1; 
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset

351 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

352 
end; 
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset

353 

275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset

354 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

355 
(* print_theorems *) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

356 

26283  357 
fun all_facts_of ctxt = 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

358 
maps Facts.selections 
27173  359 
(Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @ 
360 
Facts.dest_static [] (ProofContext.facts_of ctxt)); 

17972  361 

32738  362 
val limit = Unsynchronized.ref 40; 
25992
928594f50893
renamed thms_containing_limit to FindTheorems.limit;
wenzelm
parents:
25226
diff
changeset

363 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

364 
fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

365 
let 
30822  366 
val assms = 
367 
ProofContext.get_fact ctxt (Facts.named "local.assms") 

368 
handle ERROR _ => []; 

369 
val add_prems = Seq.hd o TRY (Method.insert_tac assms 1); 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

370 
val opt_goal' = Option.map add_prems opt_goal; 
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

371 

16036  372 
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

373 
val filters = map (filter_criterion ctxt opt_goal') criteria; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

374 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

375 
fun find_all facts = 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

376 
let 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

377 
val raw_matches = sorted_filter filters facts; 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

378 

15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

379 
val matches = 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

380 
if rem_dups 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

381 
then rem_thm_dups (nicer_shortest ctxt) raw_matches 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

382 
else raw_matches; 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

383 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

384 
val len = length matches; 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

385 
val lim = the_default (! limit) opt_limit; 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

386 
in (SOME len, Library.drop (len  lim, matches)) end; 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

387 

15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

388 
val find = 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

389 
if rem_dups orelse is_none opt_limit 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

390 
then find_all 
30822  391 
else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters; 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

392 

15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

393 
in find (all_facts_of ctxt) end; 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

394 

30186
1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30143
diff
changeset

395 

1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30143
diff
changeset

396 
fun pretty_thm ctxt (thmref, thm) = Pretty.block 
1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30143
diff
changeset

397 
[Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31687
diff
changeset

398 
Display.pretty_thm ctxt thm]; 
30186
1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30143
diff
changeset

399 

30143  400 
fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = 
401 
let 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

402 
val start = start_timing (); 
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

403 

2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

404 
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

405 
val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria; 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

406 
val returned = length thms; 
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
31042
diff
changeset

407 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

408 
val tally_msg = 
30822  409 
(case foundo of 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

410 
NONE => "displaying " ^ string_of_int returned ^ " theorems" 
30822  411 
 SOME found => 
412 
"found " ^ string_of_int found ^ " theorems" ^ 

413 
(if returned < found 

414 
then " (" ^ string_of_int returned ^ " displayed)" 

415 
else "")); 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

416 

31687  417 
val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs"; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

418 
in 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

419 
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

420 
:: Pretty.str "" :: 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

421 
(if null thms then [Pretty.str ("nothing found" ^ end_msg)] 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

422 
else 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

423 
[Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @ 
30186
1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30143
diff
changeset

424 
map (pretty_thm ctxt) thms) 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

425 
> Pretty.chunks > Pretty.writeln 
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

426 
end; 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

427 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

428 

32798  429 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

430 
(** command syntax **) 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

431 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

432 
fun find_theorems_cmd ((opt_lim, rem_dups), spec) = 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

433 
Toplevel.unknown_theory o Toplevel.keep (fn state => 
30822  434 
let 
435 
val proof_state = Toplevel.enter_proof_body state; 

436 
val ctxt = Proof.context_of proof_state; 

437 
val opt_goal = try Proof.get_goal proof_state > Option.map (#2 o #2); 

438 
in print_theorems ctxt opt_goal opt_lim rem_dups spec end); 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

439 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

440 
local 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

441 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

442 
structure P = OuterParse and K = OuterKeyword; 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

443 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

444 
val criterion = 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

445 
P.reserved "name"  P.!!! (P.$$$ ":"  P.xname) >> Name  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

446 
P.reserved "intro" >> K Intro  
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

447 
P.reserved "introiff" >> K IntroIff  
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

448 
P.reserved "elim" >> K Elim  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

449 
P.reserved "dest" >> K Dest  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

450 
P.reserved "solves" >> K Solves  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

451 
P.reserved "simp"  P.!!! (P.$$$ ":"  P.term) >> Simp  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

452 
P.term >> Pattern; 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

453 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

454 
val options = 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

455 
Scan.optional 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

456 
(P.$$$ "("  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

457 
P.!!! (Scan.option P.nat  Scan.optional (P.reserved "with_dups" >> K false) true 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

458 
 P.$$$ ")")) (NONE, true); 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

459 
in 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

460 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

461 
val _ = 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

462 
OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

463 
(options  Scan.repeat (((Scan.option P.minus >> is_none)  criterion)) 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

464 
>> (Toplevel.no_timing oo find_theorems_cmd)); 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

465 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

466 
end; 
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

467 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

468 
end; 