author  wenzelm 
Sun, 01 Mar 2009 14:45:23 +0100  
changeset 30186  1f836e949ac2 
parent 30143  98a986b02022 
child 30188  82144a95f9ec 
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 = 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

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

11 
Pattern of 'term 
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

12 
val tac_limit: int ref 
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

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

14 
val find_theorems: Proof.context > thm option > bool > 
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

15 
(bool * string criterion) list > (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 = 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

27 
Name of string  Intro  Elim  Dest  Solves  Simp of 'term  
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 

32 
 read_criterion _ Elim = Elim 

33 
 read_criterion _ Dest = Dest 

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

34 
 read_criterion _ Solves = Solves 
24683  35 
 read_criterion ctxt (Simp str) = Simp (ProofContext.read_term_pattern ctxt str) 
36 
 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

37 

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

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

41 
in 

42 
(case c of 

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

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

45 
 Elim => Pretty.str (prfx "elim") 

46 
 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

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

53 

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

54 

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

55 

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

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

57 

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

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

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

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

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

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

65 
(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

66 
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

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

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

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

71 

16088  72 

73 
(* matching theorems *) 

17106  74 

17205  75 
fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy; 
16088  76 

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

77 
(*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

78 
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

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

80 
returns: smallest substitution size*) 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

81 
fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src = 
16088  82 
let 
17106  83 
val thy = ProofContext.theory_of ctxt; 
16088  84 

16486  85 
fun matches pat = 
17106  86 
is_nontrivial thy pat andalso 
17205  87 
Pattern.matches thy (if po then (pat, obj) else (obj, pat)); 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

88 

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

89 
fun substsize pat = 
18184  90 
let val (_, subst) = 
91 
Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty) 

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

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

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

96 

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

97 
val match_thm = matches o refine_term; 
16486  98 
in 
26283  99 
map (substsize o refine_term) (filter match_thm (extract_terms term_src)) 
100 
> bestmatch 

16088  101 
end; 
102 

103 

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

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

105 

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

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

109 

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

110 

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

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

112 

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

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

115 
val extract_dest = 
17205  116 
(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

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

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

119 

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

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

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

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

123 
(*if possible, keep best substitution (one with smallest size)*) 
17106  124 
(*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

125 
assumption is as good as an intro rule with none*) 
17205  126 
if not (null successful) 
127 
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

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

129 

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

131 
let 
17205  132 
val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl); 
16036  133 
val concl = Logic.concl_of_goal goal 1; 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

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

135 
in 
18939  136 
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

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

138 

17205  139 
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

140 
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

141 
let 
17205  142 
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

143 
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

144 
val goal_concl = Logic.concl_of_goal goal 1; 
26283  145 
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

146 
val rule_concl = Logic.strip_imp_concl rule; 
26283  147 
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

148 
val rule_tree = combine rule_mp rule_concl; 
26283  149 
fun goal_tree prem = combine prem goal_concl; 
17106  150 
fun try_subst prem = 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

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

152 
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

153 
in 
17106  154 
(*elim rules always have assumptions, so an elim with one 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

155 
assumption is as good as an intro rule with none*) 
17106  156 
if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm) 
17205  157 
andalso not (null successful) 
158 
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

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

160 
else NONE 
16036  161 

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

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

163 

30143  164 
fun filter_solves ctxt goal = 
165 
let 

166 
val baregoal = Logic.get_goal (Thm.prop_of goal) 1; 

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

167 

30143  168 
fun etacn thm i = Seq.take (! tac_limit) o etac thm i; 
169 
fun try_thm thm = 

170 
if Thm.no_prems thm then rtac thm 1 goal 

171 
else (etacn thm THEN_ALL_NEW 

172 
(Goal.norm_hhf_tac THEN' 

173 
Method.assumption_tac ctxt)) 1 goal; 

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

174 
in 
30143  175 
fn (_, thm) => 
176 
if (is_some o Seq.pull o try_thm) thm 

177 
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

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

179 

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

180 

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

182 

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

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

185 
val (_, {mk_rews = {mk, ...}, ...}) = 
29302  186 
Simplifier.rep_ss (Simplifier.local_simpset_of ctxt); 
17106  187 
val extract_simp = 
17205  188 
(map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl); 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

189 
val ss = is_matching_thm extract_simp ctxt false t thm 
17106  190 
in 
18939  191 
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

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

193 

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

194 

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

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

196 

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

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

198 
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

199 

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

202 
were used, then constants that may be subject to 

203 
betareduction after substitution of frees should 

204 
not be included for LHS set because they could be 

205 
thrown away by the substituted function. 

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

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

208 
The largest possible set should always be included on 

209 
the RHS.*) 

210 

211 
fun filter_pattern ctxt pat = 

212 
let 

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

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

214 

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

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

216 
 check ((_, thm), c as SOME thm_consts) = 
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

217 
(if pat_consts subset_string thm_consts 
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

218 
andalso (Pattern.matches_subterm (ProofContext.theory_of ctxt) 
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

219 
(pat, Thm.full_prop_of thm)) 
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

220 
then SOME (0, 0) else NONE, c); 
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

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

222 

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

223 

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

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

225 

16036  226 
local 
227 

228 
fun err_no_goal c = 

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

230 

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

231 
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

232 
val fix_goalo = Option.map fix_goal; 
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

233 

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

234 
fun filter_crit _ _ (Name name) = apfst (filter_name name) 
16036  235 
 filter_crit _ NONE Intro = err_no_goal "intro" 
236 
 filter_crit _ NONE Elim = err_no_goal "elim" 

237 
 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

238 
 filter_crit _ NONE Solves = err_no_goal "solves" 
30143  239 
 filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal)) 
240 
 filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal)) 

241 
 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

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

243 
 filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat) 
16088  244 
 filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat; 
16036  245 

19502  246 
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

247 

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

250 

30143  251 
fun app_filters thm = 
252 
let 

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

253 
fun app (NONE, _, _) = NONE 
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

254 
 app (SOME v, consts, []) = SOME (v, thm) 
30143  255 
 app (r, consts, f :: fs) = 
256 
let val (r', consts') = f (thm, consts) 

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

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

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

259 

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

261 

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

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

263 
(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

264 

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

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

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

267 
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

268 

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

269 
(*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

270 
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

271 
then by the substitution size*) 
17205  272 
fun thm_ord (((p0, s0), _), ((p1, s1), _)) = 
273 
prod_ord int_ord int_ord ((p1, s1), (p0, s0)); 

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

274 
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

275 

16036  276 
end; 
277 

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

278 

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

280 

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

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

282 

27486  283 
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

284 
val hidden_ord = bool_ord o pairself NameSpace.is_hidden; 
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

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

286 
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

287 

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

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

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

292 
 ord => ord) 

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

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

294 

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

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

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

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

299 
 rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) = 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

300 
if Thm.eq_thm_prop (t, t') 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

301 
then rem_c rev_seen ((if nicer n n' then x else y) :: xs) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

302 
else rem_c (x :: rev_seen) (y :: xs) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

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

304 

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

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

306 

30143  307 
fun nicer_shortest ctxt = 
308 
let 

29848  309 
val ns = ProofContext.theory_of ctxt 
310 
> PureThy.facts_of 

311 
> Facts.space_of; 

312 

313 
val len_sort = sort (int_ord o (pairself size)); 

314 
fun shorten s = (case len_sort (NameSpace.get_accesses ns s) of 

315 
[] => s 

316 
 s'::_ => s'); 

317 

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

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

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

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

322 
in nicer end; 

323 

324 
fun rem_thm_dups nicer xs = 

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

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

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

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

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

330 

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

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

332 

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

333 

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

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

335 

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

337 
maps Facts.selections 
27173  338 
(Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @ 
339 
Facts.dest_static [] (ProofContext.facts_of ctxt)); 

17972  340 

25992
928594f50893
renamed thms_containing_limit to FindTheorems.limit;
wenzelm
parents:
25226
diff
changeset

341 
val limit = ref 40; 
928594f50893
renamed thms_containing_limit to FindTheorems.limit;
wenzelm
parents:
25226
diff
changeset

342 

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

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

344 
let 
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

345 
val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.prems_of ctxt) 1)); 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

346 
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

347 

16036  348 
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

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

350 

26283  351 
val raw_matches = all_filters filters (all_facts_of ctxt); 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

352 

22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22343
diff
changeset

353 
val matches = 
22414  354 
if rem_dups 
29848  355 
then rem_thm_dups (nicer_shortest ctxt) raw_matches 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22343
diff
changeset

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

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

358 

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

359 

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

360 
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

361 
[Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, 
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

362 
ProofContext.pretty_thm ctxt thm]; 
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

363 

30143  364 
fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = 
365 
let 

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

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

367 

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

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

369 
val matches = find_theorems ctxt opt_goal rem_dups raw_criteria; 
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset

370 

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

371 
val len = length matches; 
25992
928594f50893
renamed thms_containing_limit to FindTheorems.limit;
wenzelm
parents:
25226
diff
changeset

372 
val lim = the_default (! limit) opt_limit; 
928594f50893
renamed thms_containing_limit to FindTheorems.limit;
wenzelm
parents:
25226
diff
changeset

373 
val thms = Library.drop (len  lim, matches); 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

374 

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

375 
val end_msg = " in " ^ 
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

376 
(List.nth (String.tokens Char.isSpace (end_timing start), 3)) 
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

377 
^ " secs" 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

379 
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

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

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

382 
else 
16036  383 
[Pretty.str ("found " ^ string_of_int len ^ " theorems" ^ 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

384 
(if len <= lim then "" 
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

385 
else " (" ^ string_of_int lim ^ " displayed)") 
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

386 
^ 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

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

388 
> 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

389 
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

390 

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

391 

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

392 

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

393 
(** 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

394 

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

395 
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

396 
Toplevel.unknown_theory o Toplevel.keep (fn state => 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

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

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

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

400 
val opt_goal = try Proof.get_goal proof_state > Option.map (#2 o #2); 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

401 
in print_theorems ctxt opt_goal opt_lim rem_dups spec 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

402 

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

403 
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

404 

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

405 
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

406 

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

407 
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

408 
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

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

410 
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

411 
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

412 
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

413 
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

414 
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

415 

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

416 
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

417 
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

418 
(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

419 
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

420 
 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

421 
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

422 

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

423 
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

424 
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

425 
(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

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

427 

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

428 
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

429 

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 
end; 