author  kleing 
Sat, 10 Aug 2013 12:00:34 +0200  
changeset 52955  797362ce0c14 
parent 52954  b8b77a148ada 
child 52982  8e78bd316a53 
permissions  rwrr 
30143  1 
(* Title: Pure/Tools/find_theorems.ML 
26283  2 
Author: Rafal Kolanski and Gerwin Klein, NICTA 
46718  3 
Author: Lars Noschinski and Alexander Krauss, TU Muenchen 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

4 

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

5 
Retrieve theorems from proof context. 
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 

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

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

9 
sig 
16036  10 
datatype 'term criterion = 
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset

11 
Name of string  Intro  Elim  Dest  Solves  Simp of 'term  Pattern of 'term 
43070  12 
type 'term query = { 
13 
goal: thm option, 

14 
limit: int option, 

15 
rem_dups: bool, 

16 
criteria: (bool * 'term criterion) list 

17 
} 

52925  18 
val read_query: Position.T > string > (bool * string criterion) list 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

19 
val find_theorems: Proof.context > thm option > int option > bool > 
43067  20 
(bool * term criterion) list > int option * (Facts.ref * thm) list 
21 
val find_theorems_cmd: Proof.context > thm option > int option > bool > 

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

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

23 
val pretty_thm: Proof.context > Facts.ref * thm > Pretty.T 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

25 

33301  26 
structure Find_Theorems: FIND_THEOREMS = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

28 

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

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

30 

16036  31 
datatype 'term criterion = 
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset

32 
Name of string  Intro  Elim  Dest  Solves  Simp of 'term  Pattern of 'term; 
16036  33 

33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

34 
fun apply_dummies tm = 
33301  35 
let 
36 
val (xs, _) = Term.strip_abs tm; 

37 
val tm' = Term.betapplys (tm, map (Term.dummy_pattern o #2) xs); 

38 
in #1 (Term.replace_dummy_patterns tm' 1) end; 

33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

39 

c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

40 
fun parse_pattern ctxt nm = 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

41 
let 
42360  42 
val consts = Proof_Context.consts_of ctxt; 
33301  43 
val nm' = 
44 
(case Syntax.parse_term ctxt nm of 

45 
Const (c, _) => c 

46 
 _ => Consts.intern consts nm); 

33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

47 
in 
33301  48 
(case try (Consts.the_abbreviation consts) nm' of 
42360  49 
SOME (_, rhs) => apply_dummies (Proof_Context.expand_abbrevs ctxt rhs) 
50 
 NONE => Proof_Context.read_term_pattern ctxt nm) 

33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

51 
end; 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

52 

16036  53 
fun read_criterion _ (Name name) = Name name 
54 
 read_criterion _ Intro = Intro 

55 
 read_criterion _ Elim = Elim 

56 
 read_criterion _ Dest = Dest 

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

57 
 read_criterion _ Solves = Solves 
42360  58 
 read_criterion ctxt (Simp str) = Simp (Proof_Context.read_term_pattern ctxt str) 
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

59 
 read_criterion ctxt (Pattern str) = Pattern (parse_pattern ctxt str); 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

60 

16036  61 
fun pretty_criterion ctxt (b, c) = 
62 
let 

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

64 
in 

65 
(case c of 

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

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

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

69 
 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

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

76 

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

77 

43620  78 

43070  79 
(** queries **) 
80 

81 
type 'term query = { 

82 
goal: thm option, 

83 
limit: int option, 

84 
rem_dups: bool, 

85 
criteria: (bool * 'term criterion) list 

86 
}; 

87 

88 
fun map_criteria f {goal, limit, rem_dups, criteria} = 

46718  89 
{goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria}; 
43070  90 

43620  91 

92 

41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset

93 
(** theorems, either internal or external (without proof) **) 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

94 

b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

95 
datatype theorem = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

96 
Internal of Facts.ref * thm  
43071  97 
External of Facts.ref * term; (* FIXME: Facts.ref not appropriate *) 
98 

99 
fun fact_ref_markup (Facts.Named ((name, pos), SOME [Facts.Single i])) = 

100 
Position.markup pos o Markup.properties [("name", name), ("index", Markup.print_int i)] 

101 
 fact_ref_markup (Facts.Named ((name, pos), NONE)) = 

102 
Position.markup pos o Markup.properties [("name", name)] 

43620  103 
 fact_ref_markup fact_ref = raise Fail "bad fact ref"; 
43071  104 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

105 
fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

106 
 prop_of (External (_, prop)) = prop; 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

107 

b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

108 
fun nprems_of (Internal (_, thm)) = Thm.nprems_of thm 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

109 
 nprems_of (External (_, prop)) = Logic.count_prems prop; 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

110 

b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

111 
fun major_prem_of (Internal (_, thm)) = Thm.major_prem_of thm 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

112 
 major_prem_of (External (_, prop)) = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

113 
Logic.strip_assums_concl (hd (Logic.strip_imp_prems prop)); 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

114 

b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

115 
fun fact_ref_of (Internal (fact_ref, _)) = fact_ref 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

116 
 fact_ref_of (External (fact_ref, _)) = fact_ref; 
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

117 

43620  118 

119 

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

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

121 

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

122 
(*generated filters are to be of the form 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

123 
input: theorem 
17106  124 
output: (p:int, s:int) option, where 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

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

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

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

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

130 
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

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

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

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

135 

16088  136 

137 
(* matching theorems *) 

17106  138 

35625  139 
fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy; 
16088  140 

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

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

142 
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

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

144 
returns: smallest substitution size*) 
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset

145 
fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src = 
16088  146 
let 
42360  147 
val thy = Proof_Context.theory_of ctxt; 
16088  148 

16486  149 
fun matches pat = 
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset

150 
is_nontrivial thy pat andalso 
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset

151 
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

152 

52940  153 
fun subst_size pat = 
18184  154 
let val (_, subst) = 
155 
Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty) 

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

52941  158 
fun best_match [] = NONE 
159 
 best_match xs = SOME (foldl1 Int.min xs); 

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

160 

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

161 
val match_thm = matches o refine_term; 
16486  162 
in 
52940  163 
map (subst_size o refine_term) (filter match_thm (extract_terms term_src)) 
52941  164 
> best_match 
16088  165 
end; 
166 

167 

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

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

169 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

170 
fun filter_name str_pat theorem = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

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

173 

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

174 

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

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

176 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

177 
fun filter_dest ctxt goal theorem = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

179 
val extract_dest = 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

180 
(fn theorem => if nprems_of theorem = 0 then [] else [prop_of theorem], 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

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

183 

46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset

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

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

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

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

189 
assumption is as good as an intro rule with none*) 
17205  190 
if not (null successful) 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

191 
then SOME (nprems_of theorem  1, foldl1 Int.min successful) else NONE 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

193 

46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset

194 
fun filter_intro ctxt goal theorem = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

195 
let 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

196 
val extract_intro = (single o prop_of, Logic.strip_imp_concl); 
16036  197 
val concl = Logic.concl_of_goal goal 1; 
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset

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

199 
in 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

200 
if is_some ss then SOME (nprems_of theorem, the ss) else NONE 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

202 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

203 
fun filter_elim ctxt goal theorem = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

204 
if nprems_of theorem > 0 then 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

205 
let 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

206 
val rule = prop_of theorem; 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

207 
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

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

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

212 
val rule_tree = combine rule_mp rule_concl; 
26283  213 
fun goal_tree prem = combine prem goal_concl; 
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset

214 
fun try_subst prem = 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

215 
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

216 
in 
32798  217 
(*elim rules always have assumptions, so an elim with one 
218 
assumption is as good as an intro rule with none*) 

42360  219 
if is_nontrivial (Proof_Context.theory_of ctxt) (major_prem_of theorem) 
17205  220 
andalso not (null successful) 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

221 
then SOME (nprems_of theorem  1, foldl1 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

222 
end 
46718  223 
else NONE; 
16036  224 

30143  225 
fun filter_solves ctxt goal = 
226 
let 

52704
b824497c8e86
modify background theory where it is actually required (cf. 51dfdcd88e84);
wenzelm
parents:
52703
diff
changeset

227 
val thy' = 
b824497c8e86
modify background theory where it is actually required (cf. 51dfdcd88e84);
wenzelm
parents:
52703
diff
changeset

228 
Proof_Context.theory_of ctxt 
52788  229 
> Context_Position.set_visible_global (Context_Position.is_visible ctxt); 
52704
b824497c8e86
modify background theory where it is actually required (cf. 51dfdcd88e84);
wenzelm
parents:
52703
diff
changeset

230 
val ctxt' = Proof_Context.transfer thy' ctxt; 
b824497c8e86
modify background theory where it is actually required (cf. 51dfdcd88e84);
wenzelm
parents:
52703
diff
changeset

231 
val goal' = Thm.transfer thy' goal; 
b824497c8e86
modify background theory where it is actually required (cf. 51dfdcd88e84);
wenzelm
parents:
52703
diff
changeset

232 

52941  233 
fun limited_etac thm i = 
52702  234 
Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i; 
30143  235 
fun try_thm thm = 
52704
b824497c8e86
modify background theory where it is actually required (cf. 51dfdcd88e84);
wenzelm
parents:
52703
diff
changeset

236 
if Thm.no_prems thm then rtac thm 1 goal' 
52941  237 
else (limited_etac 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

238 
in 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

239 
fn Internal (_, thm) => 
43620  240 
if is_some (Seq.pull (try_thm thm)) 
241 
then SOME (Thm.nprems_of thm, 0) else NONE 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

242 
 External _ => NONE 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

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

244 

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

245 

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

247 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

248 
fun filter_simp ctxt t (Internal (_, thm)) = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

249 
let 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

250 
val mksimps = Simplifier.mksimps ctxt; 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

251 
val extract_simp = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

252 
(map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); 
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset

253 
val ss = is_matching_thm extract_simp ctxt false t thm; 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

254 
in 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

255 
if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

256 
end 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

257 
 filter_simp _ _ (External _) = NONE; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

258 

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

259 

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

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

261 

32798  262 
fun get_names t = Term.add_const_names t (Term.add_free_names t []); 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

263 

52940  264 
(*Including all constants and frees is only sound because matching 
265 
uses higherorder patterns. If full matching were used, then 

266 
constants that may be subject to betareduction after substitution 

267 
of frees should not be included for LHS set because they could be 

268 
thrown away by the substituted function. E.g. for (?F 1 2) do not 

269 
include 1 or 2, if it were possible for ?F to be (%x y. 3). The 

270 
largest possible set should always be included on the RHS.*) 

30143  271 

272 
fun filter_pattern ctxt pat = 

273 
let 

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

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

275 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

276 
fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem))) 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

277 
 check (theorem, c as SOME thm_consts) = 
33038  278 
(if subset (op =) (pat_consts, thm_consts) andalso 
42360  279 
Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem) 
32798  280 
then SOME (0, 0) else NONE, c); 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

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

282 

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

283 

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

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

285 

16036  286 
local 
287 

288 
fun err_no_goal c = 

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

290 

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

291 
fun filter_crit _ _ (Name name) = apfst (filter_name name) 
16036  292 
 filter_crit _ NONE Intro = err_no_goal "intro" 
293 
 filter_crit _ NONE Elim = err_no_goal "elim" 

294 
 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

295 
 filter_crit _ NONE Solves = err_no_goal "solves" 
52940  296 
 filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (Thm.prop_of goal)) 
297 
 filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (Thm.prop_of goal)) 

298 
 filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (Thm.prop_of goal)) 

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

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

300 
 filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat) 
16088  301 
 filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat; 
16036  302 

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

304 

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

307 

30143  308 
fun app_filters thm = 
309 
let 

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

310 
fun app (NONE, _, _) = NONE 
32798  311 
 app (SOME v, _, []) = SOME (v, thm) 
30143  312 
 app (r, consts, f :: fs) = 
313 
let val (r', consts') = f (thm, consts) 

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

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

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

316 

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

318 

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

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

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

321 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

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

323 
let 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

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

325 

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

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

327 
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

328 
then by the substitution size*) 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

329 
fun result_ord (((p0, s0), _), ((p1, s1), _)) = 
17205  330 
prod_ord int_ord int_ord ((p1, s1), (p0, s0)); 
46977  331 
in 
332 
grouped 100 Par_List.map eval_filters theorems 

333 
> map_filter I > sort result_ord > map #2 

334 
end; 

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

335 

30822  336 
fun lazy_filter filters = 
337 
let 

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

338 
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

339 
and first_match [] = NONE 
30822  340 
 first_match (thm :: thms) = 
341 
(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

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

344 
in lazy_match end; 
30822  345 

16036  346 
end; 
347 

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

348 

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

350 

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

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

352 

27486  353 
val index_ord = option_ord (K EQUAL); 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33039
diff
changeset

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

355 
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

356 
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

357 

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

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

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

362 
 ord => ord) 

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

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

364 

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

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

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

368 
 rem_c rev_seen [x] = rem_c (x :: rev_seen) [] 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

369 
 rem_c rev_seen ((x as (t, _)) :: (y as (t', _)) :: xs) = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

370 
if (prop_of t) aconv (prop_of t') 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

371 
then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs) 
30822  372 
else rem_c (x :: rev_seen) (y :: xs) 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

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

374 

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

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

376 

30143  377 
fun nicer_shortest ctxt = 
378 
let 

52954  379 
val space = Facts.space_of (Proof_Context.facts_of ctxt); 
29848  380 

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

381 
val shorten = 
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42012
diff
changeset

382 
Name_Space.extern 
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42012
diff
changeset

383 
(ctxt 
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42360
diff
changeset

384 
> Config.put Name_Space.names_long false 
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42360
diff
changeset

385 
> Config.put Name_Space.names_short false 
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42360
diff
changeset

386 
> Config.put Name_Space.names_unique false) space; 
29848  387 

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

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

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

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

392 
in nicer end; 

393 

394 
fun rem_thm_dups nicer xs = 

52940  395 
(xs ~~ (1 upto length xs)) 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

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

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

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

400 

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

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

402 

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

403 

52941  404 

405 
(** main operations **) 

406 

407 
(* filter_theorems *) 

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

408 

26283  409 
fun all_facts_of ctxt = 
33381  410 
let 
33382  411 
fun visible_facts facts = 
412 
Facts.dest_static [] facts 

413 
> filter_out (Facts.is_concealed facts o #1); 

33381  414 
in 
415 
maps Facts.selections 

52955  416 
(visible_facts (Proof_Context.facts_of ctxt) @ 
417 
visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt))) 

33381  418 
end; 
17972  419 

43070  420 
fun filter_theorems ctxt theorems query = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

421 
let 
46718  422 
val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query; 
43069
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset

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

424 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

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

426 
let 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

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

428 

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

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

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

431 
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

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

433 

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

434 
val len = length matches; 
52702  435 
val lim = the_default (Options.default_int @{option find_theorems_limit}) opt_limit; 
34088  436 
in (SOME len, drop (Int.max (len  lim, 0)) matches) end; 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

437 

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

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

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

440 
then find_all 
30822  441 
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

442 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

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

444 

46718  445 
fun filter_theorems_cmd ctxt theorems raw_query = 
52941  446 
filter_theorems ctxt theorems (map_criteria (map (apsnd (read_criterion ctxt))) raw_query); 
447 

448 

449 
(* find_theorems *) 

450 

451 
local 

43067  452 

453 
fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria = 

43069
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset

454 
let 
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset

455 
val assms = 
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset

456 
Proof_Context.get_fact ctxt (Facts.named "local.assms") 
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset

457 
handle ERROR _ => []; 
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset

458 
val add_prems = Seq.hd o TRY (Method.insert_tac assms 1); 
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset

459 
val opt_goal' = Option.map add_prems opt_goal; 
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset

460 
in 
46718  461 
filter ctxt (map Internal (all_facts_of ctxt)) 
462 
{goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria} 

43069
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset

463 
> apsnd (map (fn Internal f => f)) 
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset

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

465 

52941  466 
in 
467 

43067  468 
val find_theorems = gen_find_theorems filter_theorems; 
469 
val find_theorems_cmd = gen_find_theorems filter_theorems_cmd; 

470 

52941  471 
end; 
472 

473 

474 
(* pretty_theorems *) 

475 

476 
local 

477 

49888  478 
fun pretty_ref ctxt thmref = 
479 
let 

480 
val (name, sel) = 

481 
(case thmref of 

482 
Facts.Named ((name, _), sel) => (name, sel) 

483 
 Facts.Fact _ => raise Fail "Illegal literal fact"); 

484 
in 

485 
[Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name), 

486 
Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1] 

487 
end; 

488 

489 
fun pretty_theorem ctxt (Internal (thmref, thm)) = 

490 
Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]) 

491 
 pretty_theorem ctxt (External (thmref, prop)) = 

492 
Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]); 

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

493 

52941  494 
in 
495 

41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset

496 
fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm)); 
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset

497 

52941  498 
fun pretty_theorems state opt_limit rem_dups raw_criteria = 
30143  499 
let 
52941  500 
val ctxt = Proof.context_of state; 
501 
val opt_goal = try Proof.simple_goal state > Option.map #goal; 

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

502 
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; 
52941  503 

52940  504 
val (opt_found, theorems) = 
52855  505 
filter_theorems ctxt (map Internal (all_facts_of ctxt)) 
506 
{goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria}; 

41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset

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

508 

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

509 
val tally_msg = 
52940  510 
(case opt_found of 
38335  511 
NONE => "displaying " ^ string_of_int returned ^ " theorem(s)" 
30822  512 
 SOME found => 
38335  513 
"found " ^ string_of_int found ^ " theorem(s)" ^ 
30822  514 
(if returned < found 
515 
then " (" ^ string_of_int returned ^ " displayed)" 

516 
else "")); 

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

517 
in 
38335  518 
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: 
519 
Pretty.str "" :: 

46716
c45a4427db39
discontinued slightly odd builtin timing (cf. 53fd5cc685b4)  the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
wenzelm
parents:
46713
diff
changeset

520 
(if null theorems then [Pretty.str "nothing found"] 
38335  521 
else 
46716
c45a4427db39
discontinued slightly odd builtin timing (cf. 53fd5cc685b4)  the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
wenzelm
parents:
46713
diff
changeset

522 
[Pretty.str (tally_msg ^ ":"), Pretty.str ""] @ 
52927  523 
grouped 10 Par_List.map (Pretty.item o single o pretty_theorem ctxt) theorems) 
52855  524 
end > Pretty.fbreaks > curry Pretty.blk 0; 
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

525 

52941  526 
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

527 

32798  528 

46718  529 

52865
02a7e7180ee5
slightly more general support for oneshot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
52863
diff
changeset

530 
(** Isar command syntax **) 
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

531 

52941  532 
fun proof_state st = 
533 
(case try Toplevel.proof_of st of 

534 
SOME state => state 

535 
 NONE => Proof.init (Toplevel.context_of st)); 

536 

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

537 
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

538 

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

539 
val criterion = 
36950  540 
Parse.reserved "name"  Parse.!!! (Parse.$$$ ":"  Parse.xname) >> Name  
541 
Parse.reserved "intro" >> K Intro  

542 
Parse.reserved "elim" >> K Elim  

543 
Parse.reserved "dest" >> K Dest  

544 
Parse.reserved "solves" >> K Solves  

545 
Parse.reserved "simp"  Parse.!!! (Parse.$$$ ":"  Parse.term) >> Simp  

546 
Parse.term >> Pattern; 

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

547 

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

548 
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

549 
Scan.optional 
36950  550 
(Parse.$$$ "("  
551 
Parse.!!! (Scan.option Parse.nat  Scan.optional (Parse.reserved "with_dups" >> K false) true 

552 
 Parse.$$$ ")")) (NONE, true); 

52855  553 

52925  554 
val query = Scan.repeat ((Scan.option Parse.minus >> is_none)  criterion); 
52855  555 

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

556 
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

557 

52925  558 
fun read_query pos str = 
559 
Outer_Syntax.scan pos str 

52855  560 
> filter Token.is_proper 
52925  561 
> Scan.error (Scan.finite Token.stopper (Parse.!!! (query  Scan.ahead Parse.eof))) 
562 
> #1; 

43068
ac769b5edd1d
exported raw query parser; removed inconsistent clone
krauss
parents:
43067
diff
changeset

563 

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

564 
val _ = 
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
46977
diff
changeset

565 
Outer_Syntax.improper_command @{command_spec "find_theorems"} 
50214  566 
"find theorems meeting specified criteria" 
52925  567 
(options  query >> (fn ((opt_lim, rem_dups), spec) => 
52941  568 
Toplevel.keep (fn st => 
569 
Pretty.writeln (pretty_theorems (proof_state st) opt_lim rem_dups spec)))); 

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

570 

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

571 
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

572 

52851
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52788
diff
changeset

573 

e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52788
diff
changeset

574 

52865
02a7e7180ee5
slightly more general support for oneshot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
52863
diff
changeset

575 
(** PIDE query operation **) 
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset

576 

52865
02a7e7180ee5
slightly more general support for oneshot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
52863
diff
changeset

577 
val _ = 
52943  578 
Query_Operation.register "find_theorems" 
579 
(fn st => fn [limit_arg, allow_dups_arg, context_arg, query_arg] => 

580 
if can Toplevel.context_of st then 

581 
let 

582 
val state = 

583 
if context_arg = "" then proof_state st 

584 
else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg)); 

585 
val opt_limit = Int.fromString limit_arg; 

586 
val rem_dups = allow_dups_arg = "false"; 

587 
val criteria = read_query Position.none query_arg; 

588 
in Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria) end 

589 
else error "Unknown context"); 

52851
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52788
diff
changeset

590 

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

591 
end; 