author | wenzelm |
Mon, 27 Feb 2012 19:54:50 +0100 | |
changeset 46716 | c45a4427db39 |
parent 46713 | e6e1ec6d5c1c |
child 46717 | b09afce1e54f |
permissions | -rw-r--r-- |
30143 | 1 |
(* Title: Pure/Tools/find_theorems.ML |
26283 | 2 |
Author: Rafal Kolanski and Gerwin Klein, NICTA |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
3 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
4 |
Retrieve theorems from proof context. |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
5 |
*) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
6 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
7 |
signature FIND_THEOREMS = |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
8 |
sig |
16036 | 9 |
datatype 'term criterion = |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
10 |
Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term | |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
11 |
Pattern of 'term |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
12 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
13 |
datatype theorem = |
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
14 |
Internal of Facts.ref * thm | External of Facts.ref * term |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
15 |
|
43070 | 16 |
type 'term query = { |
17 |
goal: thm option, |
|
18 |
limit: int option, |
|
19 |
rem_dups: bool, |
|
20 |
criteria: (bool * 'term criterion) list |
|
21 |
} |
|
22 |
||
32738 | 23 |
val tac_limit: int Unsynchronized.ref |
24 |
val limit: int Unsynchronized.ref |
|
43067 | 25 |
|
26 |
val read_criterion: Proof.context -> string criterion -> term criterion |
|
43068
ac769b5edd1d
exported raw query parser; removed inconsistent clone
krauss
parents:
43067
diff
changeset
|
27 |
val query_parser: (bool * string criterion) list parser |
43067 | 28 |
|
43071 | 29 |
val xml_of_query: term query -> XML.tree |
30 |
val query_of_xml: XML.tree -> term query |
|
31 |
val xml_of_result: int option * theorem list -> XML.tree |
|
32 |
val result_of_xml: XML.tree -> int option * theorem list |
|
33 |
||
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
34 |
val find_theorems: Proof.context -> thm option -> int option -> bool -> |
43067 | 35 |
(bool * term criterion) list -> int option * (Facts.ref * thm) list |
36 |
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
|
37 |
(bool * string criterion) list -> int option * (Facts.ref * thm) list |
43070 | 38 |
|
39 |
val filter_theorems: Proof.context -> theorem list -> term query -> |
|
43067 | 40 |
int option * theorem list |
43070 | 41 |
val filter_theorems_cmd: Proof.context -> theorem list -> string query -> |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
42 |
int option * theorem list |
41841
c27b0b37041a
Refactor find_theorems to provide a more general filter_facts method
noschinl
parents:
41835
diff
changeset
|
43 |
|
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
44 |
val pretty_theorem: Proof.context -> theorem -> Pretty.T |
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
|
45 |
val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T |
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
46 |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
47 |
end; |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
48 |
|
33301 | 49 |
structure Find_Theorems: FIND_THEOREMS = |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
50 |
struct |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
51 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
52 |
(** search criteria **) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
53 |
|
16036 | 54 |
datatype 'term criterion = |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
55 |
Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term | |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
56 |
Pattern of 'term; |
16036 | 57 |
|
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
58 |
fun apply_dummies tm = |
33301 | 59 |
let |
60 |
val (xs, _) = Term.strip_abs tm; |
|
61 |
val tm' = Term.betapplys (tm, map (Term.dummy_pattern o #2) xs); |
|
62 |
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
|
63 |
|
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
64 |
fun parse_pattern ctxt nm = |
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
65 |
let |
42360 | 66 |
val consts = Proof_Context.consts_of ctxt; |
33301 | 67 |
val nm' = |
68 |
(case Syntax.parse_term ctxt nm of |
|
69 |
Const (c, _) => c |
|
70 |
| _ => Consts.intern consts nm); |
|
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
71 |
in |
33301 | 72 |
(case try (Consts.the_abbreviation consts) nm' of |
42360 | 73 |
SOME (_, rhs) => apply_dummies (Proof_Context.expand_abbrevs ctxt rhs) |
74 |
| NONE => Proof_Context.read_term_pattern ctxt nm) |
|
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
75 |
end; |
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
76 |
|
16036 | 77 |
fun read_criterion _ (Name name) = Name name |
78 |
| read_criterion _ Intro = Intro |
|
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
79 |
| read_criterion _ IntroIff = IntroIff |
16036 | 80 |
| read_criterion _ Elim = Elim |
81 |
| read_criterion _ Dest = Dest |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
82 |
| read_criterion _ Solves = Solves |
42360 | 83 |
| 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
|
84 |
| read_criterion ctxt (Pattern str) = Pattern (parse_pattern ctxt str); |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
85 |
|
16036 | 86 |
fun pretty_criterion ctxt (b, c) = |
87 |
let |
|
88 |
fun prfx s = if b then s else "-" ^ s; |
|
89 |
in |
|
90 |
(case c of |
|
91 |
Name name => Pretty.str (prfx "name: " ^ quote name) |
|
92 |
| Intro => Pretty.str (prfx "intro") |
|
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
93 |
| IntroIff => Pretty.str (prfx "introiff") |
16036 | 94 |
| Elim => Pretty.str (prfx "elim") |
95 |
| 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
|
96 |
| Solves => Pretty.str (prfx "solves") |
16088 | 97 |
| Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1, |
24920 | 98 |
Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))] |
16036 | 99 |
| Pattern pat => Pretty.enclose (prfx " \"") "\"" |
24920 | 100 |
[Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)]) |
16036 | 101 |
end; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
102 |
|
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
|
103 |
|
43620 | 104 |
|
43070 | 105 |
(** queries **) |
106 |
||
107 |
type 'term query = { |
|
108 |
goal: thm option, |
|
109 |
limit: int option, |
|
110 |
rem_dups: bool, |
|
111 |
criteria: (bool * 'term criterion) list |
|
112 |
}; |
|
113 |
||
114 |
fun map_criteria f {goal, limit, rem_dups, criteria} = |
|
115 |
{goal=goal, limit=limit, rem_dups=rem_dups, criteria=f criteria}; |
|
116 |
||
43071 | 117 |
fun xml_of_criterion (Name name) = XML.Elem (("Name", [("val", name)]), []) |
118 |
| xml_of_criterion Intro = XML.Elem (("Intro", []) , []) |
|
119 |
| xml_of_criterion IntroIff = XML.Elem (("IntroIff", []) , []) |
|
120 |
| xml_of_criterion Elim = XML.Elem (("Elim", []) , []) |
|
121 |
| xml_of_criterion Dest = XML.Elem (("Dest", []) , []) |
|
122 |
| xml_of_criterion Solves = XML.Elem (("Solves", []) , []) |
|
123 |
| xml_of_criterion (Simp pat) = XML.Elem (("Simp", []) , [XML_Syntax.xml_of_term pat]) |
|
124 |
| xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []) , [XML_Syntax.xml_of_term pat]); |
|
125 |
||
126 |
fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name |
|
127 |
| criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro |
|
128 |
| criterion_of_xml (XML.Elem (("IntroIff", []) , [])) = IntroIff |
|
129 |
| criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim |
|
130 |
| criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest |
|
131 |
| criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves |
|
132 |
| criterion_of_xml (XML.Elem (("Simp", []) , [tree])) = Simp (XML_Syntax.term_of_xml tree) |
|
133 |
| criterion_of_xml (XML.Elem (("Pattern", []) , [tree])) = Pattern (XML_Syntax.term_of_xml tree) |
|
134 |
| criterion_of_xml tree = raise XML_Syntax.XML ("criterion_of_xml: bad tree", tree); |
|
135 |
||
136 |
fun xml_of_query {goal=NONE, limit, rem_dups, criteria} = |
|
137 |
let |
|
138 |
val properties = [] |
|
139 |
|> (if rem_dups then cons ("rem_dups", "") else I) |
|
140 |
|> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I); |
|
141 |
in |
|
43767 | 142 |
XML.Elem (("Query", properties), XML.Encode.list |
143 |
(XML.Encode.pair XML.Encode.bool (single o xml_of_criterion)) criteria) |
|
43071 | 144 |
end |
145 |
| xml_of_query _ = raise Fail "cannot serialize goal"; |
|
146 |
||
147 |
fun query_of_xml (XML.Elem (("Query", properties), body)) = |
|
148 |
let |
|
149 |
val rem_dups = Properties.defined properties "rem_dups"; |
|
150 |
val limit = Properties.get properties "limit" |> Option.map Markup.parse_int; |
|
43724 | 151 |
val criteria = |
43767 | 152 |
XML.Decode.list (XML.Decode.pair XML.Decode.bool |
43724 | 153 |
(criterion_of_xml o the_single)) body; |
43071 | 154 |
in |
155 |
{goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria} |
|
156 |
end |
|
157 |
| query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree); |
|
43070 | 158 |
|
43620 | 159 |
|
160 |
||
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
161 |
(** theorems, either internal or external (without proof) **) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
162 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
163 |
datatype theorem = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
164 |
Internal of Facts.ref * thm | |
43071 | 165 |
External of Facts.ref * term; (* FIXME: Facts.ref not appropriate *) |
166 |
||
167 |
fun fact_ref_markup (Facts.Named ((name, pos), SOME [Facts.Single i])) = |
|
168 |
Position.markup pos o Markup.properties [("name", name), ("index", Markup.print_int i)] |
|
169 |
| fact_ref_markup (Facts.Named ((name, pos), NONE)) = |
|
170 |
Position.markup pos o Markup.properties [("name", name)] |
|
43620 | 171 |
| fact_ref_markup fact_ref = raise Fail "bad fact ref"; |
43071 | 172 |
|
173 |
fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal" |
|
174 |
| xml_of_theorem (External (fact_ref, prop)) = |
|
43620 | 175 |
XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop]); |
43071 | 176 |
|
177 |
fun theorem_of_xml (XML.Elem (("External", properties), [tree])) = |
|
43620 | 178 |
let |
179 |
val name = the (Properties.get properties "name"); |
|
180 |
val pos = Position.of_properties properties; |
|
181 |
val intvs_opt = Option.map (single o Facts.Single o Markup.parse_int) |
|
182 |
(Properties.get properties "index"); |
|
183 |
in |
|
184 |
External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree) |
|
185 |
end |
|
43071 | 186 |
| theorem_of_xml tree = raise XML_Syntax.XML ("theorem_of_xml: bad tree", tree); |
187 |
||
188 |
fun xml_of_result (opt_found, theorems) = |
|
189 |
let |
|
190 |
val properties = |
|
191 |
if is_some opt_found then [("found", Markup.print_int (the opt_found))] else []; |
|
192 |
in |
|
43767 | 193 |
XML.Elem (("Result", properties), XML.Encode.list (single o xml_of_theorem) theorems) |
43071 | 194 |
end; |
195 |
||
196 |
fun result_of_xml (XML.Elem (("Result", properties), body)) = |
|
197 |
(Properties.get properties "found" |> Option.map Markup.parse_int, |
|
43767 | 198 |
XML.Decode.list (theorem_of_xml o the_single) body) |
43071 | 199 |
| result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree); |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
200 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
201 |
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
|
202 |
| prop_of (External (_, prop)) = prop; |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
203 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
204 |
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
|
205 |
| nprems_of (External (_, prop)) = Logic.count_prems prop; |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
206 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
207 |
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
|
208 |
| major_prem_of (External (_, prop)) = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
209 |
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
|
210 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
211 |
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
|
212 |
| 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
|
213 |
|
43620 | 214 |
|
215 |
||
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
216 |
(** search criterion filters **) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
217 |
|
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
218 |
(*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
|
219 |
input: theorem |
17106 | 220 |
output: (p:int, s:int) option, where |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
221 |
NONE indicates no match |
17106 | 222 |
p is the primary sorting criterion |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
223 |
(eg. number of assumptions in the theorem) |
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
224 |
s is the secondary sorting criterion |
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
225 |
(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
|
226 |
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
|
227 |
(biggest p, sum of all s) |
17106 | 228 |
currently p and s only matter for intro, elim, dest and simp filters, |
229 |
otherwise the default ordering is used. |
|
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
230 |
*) |
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
231 |
|
16088 | 232 |
|
233 |
(* matching theorems *) |
|
17106 | 234 |
|
35625 | 235 |
fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy; |
16088 | 236 |
|
43620 | 237 |
(*educated guesses on HOL*) (* FIXME utterly broken *) |
32798 | 238 |
val boolT = Type ("bool", []); |
239 |
val iff_const = Const ("op =", boolT --> boolT --> boolT); |
|
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
240 |
|
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
241 |
(*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
|
242 |
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
|
243 |
trivial matches are ignored. |
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
244 |
returns: smallest substitution size*) |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
245 |
fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src = |
16088 | 246 |
let |
42360 | 247 |
val thy = Proof_Context.theory_of ctxt; |
16088 | 248 |
|
32798 | 249 |
fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat)); |
16486 | 250 |
fun matches pat = |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
251 |
let |
35625 | 252 |
val jpat = Object_Logic.drop_judgment thy pat; |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
253 |
val c = Term.head_of jpat; |
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
254 |
val pats = |
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
255 |
if Term.is_Const c |
32798 | 256 |
then |
257 |
if doiff andalso c = iff_const then |
|
35625 | 258 |
(pat :: map (Object_Logic.ensure_propT thy) (snd (strip_comb jpat))) |
32798 | 259 |
|> filter (is_nontrivial thy) |
260 |
else [pat] |
|
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
261 |
else []; |
32798 | 262 |
in filter check_match pats end; |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
263 |
|
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
264 |
fun substsize pat = |
18184 | 265 |
let val (_, subst) = |
266 |
Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty) |
|
17205 | 267 |
in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end; |
16088 | 268 |
|
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
269 |
fun bestmatch [] = NONE |
33029 | 270 |
| bestmatch xs = SOME (foldl1 Int.min xs); |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
271 |
|
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
272 |
val match_thm = matches o refine_term; |
16486 | 273 |
in |
32798 | 274 |
maps match_thm (extract_terms term_src) |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
275 |
|> map substsize |
26283 | 276 |
|> bestmatch |
16088 | 277 |
end; |
278 |
||
279 |
||
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
280 |
(* filter_name *) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
281 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
282 |
fun filter_name str_pat theorem = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
283 |
if match_string str_pat (Facts.name_of_ref (fact_ref_of theorem)) |
17205 | 284 |
then SOME (0, 0) else NONE; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
285 |
|
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
|
286 |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
287 |
(* filter intro/elim/dest/solves rules *) |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
288 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
289 |
fun filter_dest ctxt goal theorem = |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
290 |
let |
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
291 |
val extract_dest = |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
292 |
(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
|
293 |
hd o Logic.strip_imp_prems); |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
294 |
val prems = Logic.prems_of_goal goal 1; |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
295 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
296 |
fun try_subst prem = is_matching_thm false extract_dest ctxt true prem theorem; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19476
diff
changeset
|
297 |
val successful = prems |> map_filter try_subst; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
298 |
in |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
299 |
(*if possible, keep best substitution (one with smallest size)*) |
17106 | 300 |
(*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
|
301 |
assumption is as good as an intro rule with none*) |
17205 | 302 |
if not (null successful) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
303 |
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
|
304 |
end; |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
305 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
306 |
fun filter_intro doiff ctxt goal theorem = |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
307 |
let |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
308 |
val extract_intro = (single o prop_of, Logic.strip_imp_concl); |
16036 | 309 |
val concl = Logic.concl_of_goal goal 1; |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
310 |
val ss = is_matching_thm doiff extract_intro ctxt true concl theorem; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
311 |
in |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
312 |
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
|
313 |
end; |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
314 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
315 |
fun filter_elim ctxt goal theorem = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
316 |
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
|
317 |
let |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
318 |
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
|
319 |
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
|
320 |
val goal_concl = Logic.concl_of_goal goal 1; |
26283 | 321 |
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
|
322 |
val rule_concl = Logic.strip_imp_concl rule; |
26283 | 323 |
fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2); |
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
324 |
val rule_tree = combine rule_mp rule_concl; |
26283 | 325 |
fun goal_tree prem = combine prem goal_concl; |
17106 | 326 |
fun try_subst prem = |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
327 |
is_matching_thm false (single, I) ctxt true (goal_tree prem) rule_tree; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19476
diff
changeset
|
328 |
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
|
329 |
in |
32798 | 330 |
(*elim rules always have assumptions, so an elim with one |
331 |
assumption is as good as an intro rule with none*) |
|
42360 | 332 |
if is_nontrivial (Proof_Context.theory_of ctxt) (major_prem_of theorem) |
17205 | 333 |
andalso not (null successful) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
334 |
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
|
335 |
end |
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
336 |
else NONE |
16036 | 337 |
|
32738 | 338 |
val tac_limit = Unsynchronized.ref 5; |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
339 |
|
30143 | 340 |
fun filter_solves ctxt goal = |
341 |
let |
|
342 |
fun etacn thm i = Seq.take (! tac_limit) o etac thm i; |
|
343 |
fun try_thm thm = |
|
344 |
if Thm.no_prems thm then rtac thm 1 goal |
|
30318
3d03190d2864
replaced archaic use of rep_ss by Simplifier.mksimps;
wenzelm
parents:
30234
diff
changeset
|
345 |
else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal; |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
346 |
in |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
347 |
fn Internal (_, thm) => |
43620 | 348 |
if is_some (Seq.pull (try_thm thm)) |
349 |
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
|
350 |
| External _ => NONE |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
351 |
end; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
352 |
|
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
|
353 |
|
16074 | 354 |
(* filter_simp *) |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
355 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
356 |
fun filter_simp ctxt t (Internal (_, thm)) = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
357 |
let |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
358 |
val mksimps = Simplifier.mksimps (simpset_of ctxt); |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
359 |
val extract_simp = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
360 |
(map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
361 |
val ss = is_matching_thm false extract_simp ctxt false t thm; |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
362 |
in |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
363 |
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
|
364 |
end |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
365 |
| filter_simp _ _ (External _) = NONE; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
366 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
367 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
368 |
(* filter_pattern *) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
369 |
|
32798 | 370 |
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
|
371 |
|
30143 | 372 |
(*Including all constants and frees is only sound because |
373 |
matching uses higher-order patterns. If full matching |
|
374 |
were used, then constants that may be subject to |
|
375 |
beta-reduction after substitution of frees should |
|
376 |
not be included for LHS set because they could be |
|
377 |
thrown away by the substituted function. |
|
378 |
e.g. for (?F 1 2) do not include 1 or 2, if it were |
|
379 |
possible for ?F to be (% x y. 3) |
|
380 |
The largest possible set should always be included on |
|
381 |
the RHS.*) |
|
382 |
||
383 |
fun filter_pattern ctxt pat = |
|
384 |
let |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
385 |
val pat_consts = get_names pat; |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
386 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
387 |
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
|
388 |
| check (theorem, c as SOME thm_consts) = |
33038 | 389 |
(if subset (op =) (pat_consts, thm_consts) andalso |
42360 | 390 |
Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem) |
32798 | 391 |
then SOME (0, 0) else NONE, c); |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
392 |
in check end; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
393 |
|
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
|
394 |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
395 |
(* interpret criteria as filters *) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
396 |
|
16036 | 397 |
local |
398 |
||
399 |
fun err_no_goal c = |
|
400 |
error ("Current goal required for " ^ c ^ " search criterion"); |
|
401 |
||
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
402 |
val fix_goal = Thm.prop_of; |
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
403 |
|
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
404 |
fun filter_crit _ _ (Name name) = apfst (filter_name name) |
16036 | 405 |
| filter_crit _ NONE Intro = err_no_goal "intro" |
41835
9712fae15200
fix non-exhaustive pattern match in find_theorems
noschinl
parents:
39557
diff
changeset
|
406 |
| filter_crit _ NONE IntroIff = err_no_goal "introiff" |
16036 | 407 |
| filter_crit _ NONE Elim = err_no_goal "elim" |
408 |
| 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
|
409 |
| filter_crit _ NONE Solves = err_no_goal "solves" |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
410 |
| filter_crit ctxt (SOME goal) Intro = apfst (filter_intro false ctxt (fix_goal goal)) |
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
411 |
| filter_crit ctxt (SOME goal) IntroIff = apfst (filter_intro true ctxt (fix_goal goal)) |
30143 | 412 |
| filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal)) |
413 |
| filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal)) |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
414 |
| filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal) |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
415 |
| filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat) |
16088 | 416 |
| filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat; |
16036 | 417 |
|
19502 | 418 |
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
|
419 |
|
17756 | 420 |
fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int) |
26283 | 421 |
| opt_add _ _ = NONE; |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
422 |
|
30143 | 423 |
fun app_filters thm = |
424 |
let |
|
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
425 |
fun app (NONE, _, _) = NONE |
32798 | 426 |
| app (SOME v, _, []) = SOME (v, thm) |
30143 | 427 |
| app (r, consts, f :: fs) = |
428 |
let val (r', consts') = f (thm, consts) |
|
429 |
in app (opt_add r r', consts', fs) end; |
|
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
430 |
in app end; |
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
431 |
|
16036 | 432 |
in |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
433 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
434 |
fun filter_criterion ctxt opt_goal (b, c) = |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
435 |
(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
|
436 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
437 |
fun sorted_filter filters theorems = |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
438 |
let |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
439 |
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
|
440 |
|
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
441 |
(*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
|
442 |
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
|
443 |
then by the substitution size*) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
444 |
fun result_ord (((p0, s0), _), ((p1, s1), _)) = |
17205 | 445 |
prod_ord int_ord int_ord ((p1, s1), (p0, s0)); |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
446 |
in map_filter eval_filters theorems |> sort result_ord |> map #2 end; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
447 |
|
30822 | 448 |
fun lazy_filter filters = |
449 |
let |
|
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
450 |
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
|
451 |
|
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
452 |
and first_match [] = NONE |
30822 | 453 |
| first_match (thm :: thms) = |
454 |
(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
|
455 |
NONE => first_match thms |
30822 | 456 |
| SOME (_, t) => SOME (t, lazy_match thms)); |
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
457 |
in lazy_match end; |
30822 | 458 |
|
16036 | 459 |
end; |
460 |
||
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
461 |
|
22414 | 462 |
(* removing duplicates, preferring nicer names, roughly n log n *) |
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset
|
463 |
|
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
464 |
local |
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
465 |
|
27486 | 466 |
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
|
467 |
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
|
468 |
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
|
469 |
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
|
470 |
|
27486 | 471 |
fun nicer_name (x, i) (y, j) = |
472 |
(case hidden_ord (x, y) of EQUAL => |
|
473 |
(case index_ord (i, j) of EQUAL => |
|
474 |
(case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord) |
|
475 |
| ord => ord) |
|
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
476 |
| ord => ord) <> GREATER; |
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
477 |
|
29848 | 478 |
fun rem_cdups nicer xs = |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
479 |
let |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
480 |
fun rem_c rev_seen [] = rev rev_seen |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
481 |
| 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
|
482 |
| 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
|
483 |
if (prop_of t) aconv (prop_of t') |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
484 |
then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs) |
30822 | 485 |
else rem_c (x :: rev_seen) (y :: xs) |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
486 |
in rem_c [] xs end; |
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
487 |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
488 |
in |
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
489 |
|
30143 | 490 |
fun nicer_shortest ctxt = |
491 |
let |
|
30216
0300b7420b07
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm
parents:
30188
diff
changeset
|
492 |
(* FIXME global name space!? *) |
42360 | 493 |
val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt)); |
29848 | 494 |
|
30216
0300b7420b07
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm
parents:
30188
diff
changeset
|
495 |
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
|
496 |
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
|
497 |
(ctxt |
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42360
diff
changeset
|
498 |
|> Config.put Name_Space.names_long false |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42360
diff
changeset
|
499 |
|> Config.put Name_Space.names_short false |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42360
diff
changeset
|
500 |
|> Config.put Name_Space.names_unique false) space; |
29848 | 501 |
|
502 |
fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = |
|
503 |
nicer_name (shorten x, i) (shorten y, j) |
|
504 |
| nicer (Facts.Fact _) (Facts.Named _) = true |
|
505 |
| nicer (Facts.Named _) (Facts.Fact _) = false; |
|
506 |
in nicer end; |
|
507 |
||
508 |
fun rem_thm_dups nicer xs = |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
509 |
xs ~~ (1 upto length xs) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
510 |
|> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1)) |
29848 | 511 |
|> rem_cdups nicer |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
512 |
|> sort (int_ord o pairself #2) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
513 |
|> map #1; |
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset
|
514 |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
515 |
end; |
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset
|
516 |
|
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset
|
517 |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
518 |
(* print_theorems *) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
519 |
|
26283 | 520 |
fun all_facts_of ctxt = |
33381 | 521 |
let |
33382 | 522 |
fun visible_facts facts = |
523 |
Facts.dest_static [] facts |
|
524 |
|> filter_out (Facts.is_concealed facts o #1); |
|
33381 | 525 |
in |
526 |
maps Facts.selections |
|
42360 | 527 |
(visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)) @ |
528 |
visible_facts (Proof_Context.facts_of ctxt)) |
|
33381 | 529 |
end; |
17972 | 530 |
|
32738 | 531 |
val limit = Unsynchronized.ref 40; |
25992
928594f50893
renamed thms_containing_limit to FindTheorems.limit;
wenzelm
parents:
25226
diff
changeset
|
532 |
|
43070 | 533 |
fun filter_theorems ctxt theorems query = |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
534 |
let |
43070 | 535 |
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
|
536 |
val filters = map (filter_criterion ctxt opt_goal) criteria; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
537 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
538 |
fun find_all theorems = |
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
539 |
let |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
540 |
val raw_matches = sorted_filter filters theorems; |
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
541 |
|
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
542 |
val matches = |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
543 |
if rem_dups |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
544 |
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
|
545 |
else raw_matches; |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
546 |
|
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
547 |
val len = length matches; |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
548 |
val lim = the_default (! limit) opt_limit; |
34088 | 549 |
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
|
550 |
|
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
551 |
val find = |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
552 |
if rem_dups orelse is_none opt_limit |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
553 |
then find_all |
30822 | 554 |
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
|
555 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
556 |
in find theorems end; |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
557 |
|
43070 | 558 |
fun filter_theorems_cmd ctxt theorems raw_query = |
559 |
filter_theorems ctxt theorems (map_criteria |
|
560 |
(map (apsnd (read_criterion ctxt))) raw_query); |
|
43067 | 561 |
|
562 |
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
|
563 |
let |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
564 |
val assms = |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
565 |
Proof_Context.get_fact ctxt (Facts.named "local.assms") |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
566 |
handle ERROR _ => []; |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
567 |
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
|
568 |
val opt_goal' = Option.map add_prems opt_goal; |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
569 |
in |
43070 | 570 |
filter ctxt (map Internal (all_facts_of ctxt)) |
571 |
{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
|
572 |
|> apsnd (map (fn Internal f => f)) |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
573 |
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
|
574 |
|
43067 | 575 |
val find_theorems = gen_find_theorems filter_theorems; |
576 |
val find_theorems_cmd = gen_find_theorems filter_theorems_cmd; |
|
577 |
||
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
578 |
fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
579 |
[Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
580 |
Display.pretty_thm ctxt thm] |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
581 |
| pretty_theorem ctxt (External (thmref, prop)) = Pretty.block |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
582 |
[Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
583 |
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
|
584 |
|
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
585 |
fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm)); |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
586 |
|
43076
7b06cd71792c
parameterize print_theorems over actual search function
krauss
parents:
43071
diff
changeset
|
587 |
fun gen_print_theorems find ctxt opt_goal opt_limit rem_dups raw_criteria = |
30143 | 588 |
let |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
589 |
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; |
43076
7b06cd71792c
parameterize print_theorems over actual search function
krauss
parents:
43071
diff
changeset
|
590 |
val (foundo, theorems) = find |
43070 | 591 |
{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
|
592 |
val returned = length theorems; |
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
31042
diff
changeset
|
593 |
|
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
594 |
val tally_msg = |
30822 | 595 |
(case foundo of |
38335 | 596 |
NONE => "displaying " ^ string_of_int returned ^ " theorem(s)" |
30822 | 597 |
| SOME found => |
38335 | 598 |
"found " ^ string_of_int found ^ " theorem(s)" ^ |
30822 | 599 |
(if returned < found |
600 |
then " (" ^ string_of_int returned ^ " displayed)" |
|
601 |
else "")); |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
602 |
in |
38335 | 603 |
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: |
604 |
Pretty.str "" :: |
|
46716
c45a4427db39
discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
wenzelm
parents:
46713
diff
changeset
|
605 |
(if null theorems then [Pretty.str "nothing found"] |
38335 | 606 |
else |
46716
c45a4427db39
discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
wenzelm
parents:
46713
diff
changeset
|
607 |
[Pretty.str (tally_msg ^ ":"), Pretty.str ""] @ |
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
608 |
map (pretty_theorem ctxt) theorems) |
38335 | 609 |
end |> Pretty.chunks |> Pretty.writeln; |
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
610 |
|
43076
7b06cd71792c
parameterize print_theorems over actual search function
krauss
parents:
43071
diff
changeset
|
611 |
fun print_theorems ctxt = |
7b06cd71792c
parameterize print_theorems over actual search function
krauss
parents:
43071
diff
changeset
|
612 |
gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt; |
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
|
613 |
|
32798 | 614 |
|
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
|
615 |
(** command syntax **) |
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
616 |
|
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
617 |
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
|
618 |
|
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
619 |
val criterion = |
36950 | 620 |
Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || |
621 |
Parse.reserved "intro" >> K Intro || |
|
622 |
Parse.reserved "introiff" >> K IntroIff || |
|
623 |
Parse.reserved "elim" >> K Elim || |
|
624 |
Parse.reserved "dest" >> K Dest || |
|
625 |
Parse.reserved "solves" >> K Solves || |
|
626 |
Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp || |
|
627 |
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
|
628 |
|
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
629 |
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
|
630 |
Scan.optional |
36950 | 631 |
(Parse.$$$ "(" |-- |
632 |
Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true |
|
633 |
--| Parse.$$$ ")")) (NONE, true); |
|
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
|
634 |
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
|
635 |
|
43068
ac769b5edd1d
exported raw query parser; removed inconsistent clone
krauss
parents:
43067
diff
changeset
|
636 |
val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion)); |
ac769b5edd1d
exported raw query parser; removed inconsistent clone
krauss
parents:
43067
diff
changeset
|
637 |
|
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
|
638 |
val _ = |
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
639 |
Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria" |
36950 | 640 |
Keyword.diag |
43068
ac769b5edd1d
exported raw query parser; removed inconsistent clone
krauss
parents:
43067
diff
changeset
|
641 |
(options -- query_parser |
38334 | 642 |
>> (fn ((opt_lim, rem_dups), spec) => |
643 |
Toplevel.no_timing o |
|
644 |
Toplevel.keep (fn state => |
|
645 |
let |
|
646 |
val ctxt = Toplevel.context_of state; |
|
647 |
val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal; |
|
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
648 |
in print_theorems ctxt opt_goal opt_lim rem_dups spec end))); |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
649 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
650 |
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
|
651 |
|
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
652 |
end; |