author  wenzelm 
Fri, 03 Apr 2015 18:36:19 +0200  
changeset 59916  f673ce6b1e2b 
parent 59888  27e4d0ab0948 
child 59934  b65c4370f831 
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 

34 
fun read_criterion _ (Name name) = Name name 

35 
 read_criterion _ Intro = Intro 

36 
 read_criterion _ Elim = Elim 

37 
 read_criterion _ Dest = Dest 

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

38 
 read_criterion _ Solves = Solves 
42360  39 
 read_criterion ctxt (Simp str) = Simp (Proof_Context.read_term_pattern ctxt str) 
59097
4b05ce4c84b0
revert "better" handling of abbreviation from c61fe520602b
haftmann
parents:
59096
diff
changeset

40 
 read_criterion ctxt (Pattern str) = Pattern (Proof_Context.read_term_pattern ctxt str); 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

41 

16036  42 
fun pretty_criterion ctxt (b, c) = 
43 
let 

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

45 
in 

46 
(case c of 

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

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

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

50 
 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

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

57 

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

58 

43620  59 

43070  60 
(** queries **) 
61 

62 
type 'term query = { 

63 
goal: thm option, 

64 
limit: int option, 

65 
rem_dups: bool, 

66 
criteria: (bool * 'term criterion) list 

67 
}; 

68 

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

46718  70 
{goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria}; 
43070  71 

43620  72 

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

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

74 

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

75 
(*generated filters are to be of the form 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

78 
NONE indicates no match 
17106  79 
p is the primary sorting criterion 
53632  80 
(eg. size of term) 
81 
s is the secondary sorting criterion 

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

82 
(eg. number of assumptions in the theorem) 
53632  83 
t is the tertiary sorting criterion 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

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

85 
when applying a set of filters to a thm, fold results in: 
53632  86 
(max p, max s, sum of all t) 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

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

88 

16088  89 

90 
(* matching theorems *) 

17106  91 

35625  92 
fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy; 
16088  93 

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

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

95 
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

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

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

98 
fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src = 
16088  99 
let 
42360  100 
val thy = Proof_Context.theory_of ctxt; 
16088  101 

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

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

104 
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

105 

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

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

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

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

113 

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

114 
val match_thm = matches o refine_term; 
16486  115 
in 
52940  116 
map (subst_size o refine_term) (filter match_thm (extract_terms term_src)) 
52941  117 
> best_match 
16088  118 
end; 
119 

120 

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

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

122 

55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

123 
fun filter_name str_pat (thmref, _) = 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

126 

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

127 

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

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

129 

55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

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

132 
val extract_dest = 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

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

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

136 

55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

137 
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

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

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

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

142 
assumption is as good as an intro rule with none*) 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

143 
if not (null successful) then 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

144 
SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm  1, foldl1 Int.min successful) 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

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

147 

55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

149 
let 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

150 
val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl); 
16036  151 
val concl = Logic.concl_of_goal goal 1; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

152 
in 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

153 
(case is_matching_thm extract_intro ctxt true concl thm of 
59096  154 
SOME k => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, k) 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

155 
 NONE => NONE) 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

157 

55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

158 
fun filter_elim ctxt goal (_, thm) = 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

160 
let 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

161 
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

162 
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

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

165 
val rule_concl = Logic.strip_imp_concl rule; 
57690  166 
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

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

169 
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

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

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

55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

174 
if is_nontrivial (Proof_Context.theory_of ctxt) (Thm.major_prem_of thm) 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

175 
andalso not (null successful) then 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

176 
SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm  1, foldl1 Int.min successful) 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

178 
end 
46718  179 
else NONE; 
16036  180 

30143  181 
fun filter_solves ctxt goal = 
182 
let 

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

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

184 
Proof_Context.theory_of ctxt 
52788  185 
> 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

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

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

188 

52941  189 
fun limited_etac thm i = 
58837  190 
Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59098
diff
changeset

191 
eresolve_tac ctxt' [thm] i; 
30143  192 
fun try_thm thm = 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59098
diff
changeset

193 
if Thm.no_prems thm then resolve_tac ctxt' [thm] 1 goal' 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53633
diff
changeset

194 
else 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53633
diff
changeset

195 
(limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt')) 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53633
diff
changeset

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

197 
in 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

198 
fn (_, thm) => 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

199 
if is_some (Seq.pull (try_thm thm)) 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

200 
then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

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

203 

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

204 

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

206 

55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

207 
fun filter_simp ctxt t (_, thm) = 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

208 
let 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

209 
val mksimps = Simplifier.mksimps ctxt; 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

210 
val extract_simp = 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

211 
(map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

212 
in 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

213 
(case is_matching_thm extract_simp ctxt false t thm of 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

214 
SOME ss => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, ss) 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

215 
 NONE => NONE) 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

217 

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

218 

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

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

220 

59098
b6ba3adb48e3
etaexpand all search patterns using schematic place holders
haftmann
parents:
59097
diff
changeset

221 
fun expand_abs t = 
b6ba3adb48e3
etaexpand all search patterns using schematic place holders
haftmann
parents:
59097
diff
changeset

222 
let 
b6ba3adb48e3
etaexpand all search patterns using schematic place holders
haftmann
parents:
59097
diff
changeset

223 
val m = Term.maxidx_of_term t + 1; 
b6ba3adb48e3
etaexpand all search patterns using schematic place holders
haftmann
parents:
59097
diff
changeset

224 
val vs = strip_abs_vars t; 
b6ba3adb48e3
etaexpand all search patterns using schematic place holders
haftmann
parents:
59097
diff
changeset

225 
val ts = map_index (fn (k, (_, T)) => Var ((Name.aT, m + k), T)) vs; 
b6ba3adb48e3
etaexpand all search patterns using schematic place holders
haftmann
parents:
59097
diff
changeset

226 
in betapplys (t, ts) end; 
b6ba3adb48e3
etaexpand all search patterns using schematic place holders
haftmann
parents:
59097
diff
changeset

227 

32798  228 
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

229 

59095
3100a7b1c092
turn applicationspecific Pattern.matches_subterm into an applicationprivate function
haftmann
parents:
59083
diff
changeset

230 
(* Does pat match a subterm of obj? *) 
3100a7b1c092
turn applicationspecific Pattern.matches_subterm into an applicationprivate function
haftmann
parents:
59083
diff
changeset

231 
fun matches_subterm thy (pat, obj) = 
3100a7b1c092
turn applicationspecific Pattern.matches_subterm into an applicationprivate function
haftmann
parents:
59083
diff
changeset

232 
let 
3100a7b1c092
turn applicationspecific Pattern.matches_subterm into an applicationprivate function
haftmann
parents:
59083
diff
changeset

233 
fun msub bounds obj = Pattern.matches thy (pat, obj) orelse 
3100a7b1c092
turn applicationspecific Pattern.matches_subterm into an applicationprivate function
haftmann
parents:
59083
diff
changeset

234 
(case obj of 
59096  235 
Abs (_, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t))) 
59095
3100a7b1c092
turn applicationspecific Pattern.matches_subterm into an applicationprivate function
haftmann
parents:
59083
diff
changeset

236 
 t $ u => msub bounds t orelse msub bounds u 
3100a7b1c092
turn applicationspecific Pattern.matches_subterm into an applicationprivate function
haftmann
parents:
59083
diff
changeset

237 
 _ => false) 
3100a7b1c092
turn applicationspecific Pattern.matches_subterm into an applicationprivate function
haftmann
parents:
59083
diff
changeset

238 
in msub 0 obj end; 
3100a7b1c092
turn applicationspecific Pattern.matches_subterm into an applicationprivate function
haftmann
parents:
59083
diff
changeset

239 

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

242 
constants that may be subject to betareduction after substitution 

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

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

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

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

30143  247 

248 
fun filter_pattern ctxt pat = 

249 
let 

59098
b6ba3adb48e3
etaexpand all search patterns using schematic place holders
haftmann
parents:
59097
diff
changeset

250 
val pat' = (expand_abs o Envir.eta_contract) pat; 
b6ba3adb48e3
etaexpand all search patterns using schematic place holders
haftmann
parents:
59097
diff
changeset

251 
val pat_consts = get_names pat'; 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

252 
fun check ((x, thm), NONE) = check ((x, thm), SOME (get_names (Thm.full_prop_of thm))) 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

253 
 check ((_, thm), c as SOME thm_consts) = 
33038  254 
(if subset (op =) (pat_consts, thm_consts) andalso 
59098
b6ba3adb48e3
etaexpand all search patterns using schematic place holders
haftmann
parents:
59097
diff
changeset

255 
matches_subterm (Proof_Context.theory_of ctxt) (pat', Thm.full_prop_of thm) 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

256 
then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE, c); 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

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

258 

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

259 

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

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

261 

16036  262 
local 
263 

264 
fun err_no_goal c = 

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

266 

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

267 
fun filter_crit _ _ (Name name) = apfst (filter_name name) 
16036  268 
 filter_crit _ NONE Intro = err_no_goal "intro" 
269 
 filter_crit _ NONE Elim = err_no_goal "elim" 

270 
 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

271 
 filter_crit _ NONE Solves = err_no_goal "solves" 
52940  272 
 filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (Thm.prop_of goal)) 
273 
 filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (Thm.prop_of goal)) 

274 
 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

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

276 
 filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat) 
16088  277 
 filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat; 
16036  278 

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

280 

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

283 

30143  284 
fun app_filters thm = 
285 
let 

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

286 
fun app (NONE, _, _) = NONE 
32798  287 
 app (SOME v, _, []) = SOME (v, thm) 
30143  288 
 app (r, consts, f :: fs) = 
289 
let val (r', consts') = f (thm, consts) 

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

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

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

292 

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

294 

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

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

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

297 

55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

299 
let 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

301 

53632  302 
(*filters return: (thm size, number of assumptions, substitution size) option, so 
303 
sort according to size of thm first, then number of assumptions, 

304 
then by the substitution size, then by term order *) 

55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

305 
fun result_ord (((p0, s0, t0), (_, thm0)), ((p1, s1, t1), (_, thm1))) = 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

306 
prod_ord int_ord (prod_ord int_ord (prod_ord int_ord Term_Ord.term_ord)) 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

307 
((p1, (s1, (t1, Thm.full_prop_of thm1))), (p0, (s0, (t0, Thm.full_prop_of thm0)))); 
46977  308 
in 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

309 
grouped 100 Par_List.map eval_filters thms 
46977  310 
> map_filter I > sort result_ord > map #2 
311 
end; 

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

312 

30822  313 
fun lazy_filter filters = 
314 
let 

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

315 
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

316 
and first_match [] = NONE 
30822  317 
 first_match (thm :: thms) = 
53632  318 
(case app_filters thm (SOME (0, 0, 0), NONE, filters) of 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

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

321 
in lazy_match end; 
30822  322 

16036  323 
end; 
324 

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

325 

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

327 

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

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

329 

27486  330 
val index_ord = option_ord (K EQUAL); 
59916  331 
val hidden_ord = bool_ord o apply2 Long_Name.is_hidden; 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58928
diff
changeset

332 
val qual_ord = int_ord o apply2 Long_Name.qualification; 
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58928
diff
changeset

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

334 

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

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

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

339 
 ord => ord) 

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

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

341 

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

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

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

345 
 rem_c rev_seen [x] = rem_c (x :: rev_seen) [] 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

346 
 rem_c rev_seen ((x as ((n, thm), _)) :: (y as ((n', thm'), _)) :: rest) = 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

347 
if Thm.eq_thm_prop (thm, thm') 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

348 
then rem_c rev_seen ((if nicer n n' then x else y) :: rest) 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

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

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

351 

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

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

353 

30143  354 
fun nicer_shortest ctxt = 
355 
let 

56143
ed2b660a52a1
more accurate resolution of hybrid facts, which actually changes the sort order of results;
wenzelm
parents:
56141
diff
changeset

356 
fun extern_shortest name = 
ed2b660a52a1
more accurate resolution of hybrid facts, which actually changes the sort order of results;
wenzelm
parents:
56141
diff
changeset

357 
Name_Space.extern_shortest ctxt 
ed2b660a52a1
more accurate resolution of hybrid facts, which actually changes the sort order of results;
wenzelm
parents:
56141
diff
changeset

358 
(Facts.space_of (Proof_Context.facts_of_fact ctxt name)) name; 
29848  359 

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

55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55671
diff
changeset

361 
nicer_name (extern_shortest x, i) (extern_shortest y, j) 
29848  362 
 nicer (Facts.Fact _) (Facts.Named _) = true 
55670  363 
 nicer (Facts.Named _) (Facts.Fact _) = false 
364 
 nicer (Facts.Fact _) (Facts.Fact _) = true; 

29848  365 
in nicer end; 
366 

367 
fun rem_thm_dups nicer xs = 

52940  368 
(xs ~~ (1 upto length xs)) 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58928
diff
changeset

369 
> sort (Term_Ord.fast_term_ord o apply2 (Thm.full_prop_of o #2 o #1)) 
29848  370 
> rem_cdups nicer 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58928
diff
changeset

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

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

373 

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

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

375 

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

376 

52941  377 

378 
(** main operations **) 

379 

380 
(* filter_theorems *) 

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

381 

26283  382 
fun all_facts_of ctxt = 
33381  383 
let 
56158
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56143
diff
changeset

384 
val local_facts = Proof_Context.facts_of ctxt; 
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56143
diff
changeset

385 
val global_facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt); 
56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

386 
in 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

387 
maps Facts.selections 
56159  388 
(Facts.dest_static false [global_facts] local_facts @ 
56158
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56143
diff
changeset

389 
Facts.dest_static false [] global_facts) 
56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

390 
end; 
17972  391 

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

393 
let 
46718  394 
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

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

396 

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

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

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

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

400 

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

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

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

403 
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

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

405 

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

406 
val len = length matches; 
56467  407 
val lim = the_default (Options.default_int @{system_option find_theorems_limit}) opt_limit; 
34088  408 
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

409 

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

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

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

412 
then find_all 
30822  413 
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

414 

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

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

416 

46718  417 
fun filter_theorems_cmd ctxt theorems raw_query = 
52941  418 
filter_theorems ctxt theorems (map_criteria (map (apsnd (read_criterion ctxt))) raw_query); 
419 

420 

421 
(* find_theorems *) 

422 

423 
local 

43067  424 

425 
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

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

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

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

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

430 
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

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

432 
in 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

433 
filter ctxt (all_facts_of ctxt) 
46718  434 
{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

435 
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

436 

52941  437 
in 
438 

43067  439 
val find_theorems = gen_find_theorems filter_theorems; 
440 
val find_theorems_cmd = gen_find_theorems filter_theorems_cmd; 

441 

52941  442 
end; 
443 

444 

445 
(* pretty_theorems *) 

446 

447 
local 

448 

49888  449 
fun pretty_ref ctxt thmref = 
450 
let 

451 
val (name, sel) = 

452 
(case thmref of 

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

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

455 
in 

56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

456 
[Pretty.mark (#1 (Proof_Context.markup_extern_fact ctxt name)) (Pretty.str name), 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

457 
Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1] 
49888  458 
end; 
459 

52941  460 
in 
461 

55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

462 
fun pretty_thm ctxt (thmref, thm) = 
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

463 
Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]); 
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset

464 

52941  465 
fun pretty_theorems state opt_limit rem_dups raw_criteria = 
30143  466 
let 
52941  467 
val ctxt = Proof.context_of state; 
468 
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

469 
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; 
52941  470 

52940  471 
val (opt_found, theorems) = 
55671
aeca05e62fef
removed remains of old experiment (see b933142e02d0);
wenzelm
parents:
55670
diff
changeset

472 
filter_theorems ctxt (all_facts_of ctxt) 
52855  473 
{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

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

475 

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

476 
val tally_msg = 
52940  477 
(case opt_found of 
38335  478 
NONE => "displaying " ^ string_of_int returned ^ " theorem(s)" 
30822  479 
 SOME found => 
38335  480 
"found " ^ string_of_int found ^ " theorem(s)" ^ 
30822  481 
(if returned < found 
482 
then " (" ^ string_of_int returned ^ " displayed)" 

483 
else "")); 

56912
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset

484 
val position_markup = Position.markup (Position.thread_data ()) Markup.position; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

485 
in 
56891
48899c43b07d
tuned message  more context for detached window etc.;
wenzelm
parents:
56621
diff
changeset

486 
Pretty.block 
56912
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset

487 
(Pretty.fbreaks 
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset

488 
(Pretty.mark position_markup (Pretty.keyword1 "find_theorems") :: 
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset

489 
map (pretty_criterion ctxt) criteria)) :: 
38335  490 
Pretty.str "" :: 
56908
734f7e6151c9
tuned message: more compact, imitate actual command line;
wenzelm
parents:
56891
diff
changeset

491 
(if null theorems then [Pretty.str "found nothing"] 
38335  492 
else 
56908
734f7e6151c9
tuned message: more compact, imitate actual command line;
wenzelm
parents:
56891
diff
changeset

493 
Pretty.str (tally_msg ^ ":") :: 
734f7e6151c9
tuned message: more compact, imitate actual command line;
wenzelm
parents:
56891
diff
changeset

494 
grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems)) 
52855  495 
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

496 

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

498 

32798  499 

46718  500 

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

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

502 

52941  503 
fun proof_state st = 
504 
(case try Toplevel.proof_of st of 

505 
SOME state => state 

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

507 

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

508 
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

509 

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

510 
val criterion = 
36950  511 
Parse.reserved "name"  Parse.!!! (Parse.$$$ ":"  Parse.xname) >> Name  
512 
Parse.reserved "intro" >> K Intro  

513 
Parse.reserved "elim" >> K Elim  

514 
Parse.reserved "dest" >> K Dest  

515 
Parse.reserved "solves" >> K Solves  

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

517 
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

518 

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

519 
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

520 
Scan.optional 
36950  521 
(Parse.$$$ "("  
522 
Parse.!!! (Scan.option Parse.nat  Scan.optional (Parse.reserved "with_dups" >> K false) true 

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

52855  524 

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

58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58920
diff
changeset

527 
val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords; 
58905  528 

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

529 
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

530 

52925  531 
fun read_query pos str = 
59083  532 
Token.explode query_keywords pos str 
52855  533 
> filter Token.is_proper 
52925  534 
> Scan.error (Scan.finite Token.stopper (Parse.!!! (query  Scan.ahead Parse.eof))) 
535 
> #1; 

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

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 
val _ = 
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58837
diff
changeset

538 
Outer_Syntax.command @{command_spec "find_theorems"} 
50214  539 
"find theorems meeting specified criteria" 
52925  540 
(options  query >> (fn ((opt_lim, rem_dups), spec) => 
52941  541 
Toplevel.keep (fn st => 
542 
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

543 

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

544 
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

545 

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

546 

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

547 

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

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

549 

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

550 
val _ = 
52982
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52955
diff
changeset

551 
Query_Operation.register "find_theorems" (fn {state = st, args, output_result} => 
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52955
diff
changeset

552 
if can Toplevel.context_of st then 
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52955
diff
changeset

553 
let 
56621
798ba1c2da12
removed odd context argument: Thy_Info.get_theory does not fit into PIDE document model;
wenzelm
parents:
56613
diff
changeset

554 
val [limit_arg, allow_dups_arg, query_arg] = args; 
798ba1c2da12
removed odd context argument: Thy_Info.get_theory does not fit into PIDE document model;
wenzelm
parents:
56613
diff
changeset

555 
val state = proof_state st; 
52982
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52955
diff
changeset

556 
val opt_limit = Int.fromString limit_arg; 
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52955
diff
changeset

557 
val rem_dups = allow_dups_arg = "false"; 
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52955
diff
changeset

558 
val criteria = read_query Position.none query_arg; 
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52955
diff
changeset

559 
in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end 
8e78bd316a53
clarified Query_Operation.register: avoid hardwired parallel policy;
wenzelm
parents:
52955
diff
changeset

560 
else error "Unknown context"); 
52851
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52788
diff
changeset

561 

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

562 
end; 
59096  563 