225 fun thm_ord (((p0, s0), _), ((p1, s1), _)) = |
225 fun thm_ord (((p0, s0), _), ((p1, s1), _)) = |
226 prod_ord int_ord int_ord ((p1, s1), (p0, s0)); |
226 prod_ord int_ord int_ord ((p1, s1), (p0, s0)); |
227 in |
227 in |
228 map (`(eval_filters filters)) thms |
228 map (`(eval_filters filters)) thms |
229 |> map_filter (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE) |
229 |> map_filter (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE) |
230 |> sort thm_ord |> map #2 |
230 |> sort thm_ord |> map #2 |
231 end; |
231 end; |
232 |
232 |
233 end; |
233 end; |
234 |
234 |
235 |
235 |
236 (* removing duplicates, preferring nicer names *) |
236 (* removing duplicates, preferring nicer names *) |
237 |
237 |
238 fun rem_thm_dups xs = |
238 fun rem_thm_dups xs = |
239 let |
239 let |
240 fun nicer (Fact x) (Fact y) = size x <= size y |
240 fun nicer (Fact x) (Fact y) = size x <= size y |
241 | nicer (Fact _) _ = true |
241 | nicer (Fact _) _ = true |
242 | nicer (PureThy.Name x) (PureThy.Name y) = size x <= size y |
242 | nicer (PureThy.Name x) (PureThy.Name y) = size x <= size y |
243 | nicer (PureThy.Name _) (Fact _) = false |
243 | nicer (PureThy.Name _) (Fact _) = false |
244 | nicer (PureThy.Name _) _ = true |
244 | nicer (PureThy.Name _) _ = true |
245 | nicer (NameSelection (x,_)) (NameSelection (y,_)) = size x <= size y |
245 | nicer (NameSelection (x, _)) (NameSelection (y, _)) = size x <= size y |
246 | nicer (NameSelection _) _ = false; |
246 | nicer (NameSelection _) _ = false; |
247 |
247 |
248 fun is_in [] _ = NONE |
248 fun is_in [] _ = NONE |
249 | is_in ((n,t) :: xs) t' = if eq_thm (t, t') |
249 | is_in ((n, t) :: xs) t' = |
250 then SOME (n,t) |
250 if Thm.eq_thm (t, t') then SOME (n, t) else is_in xs t'; |
251 else is_in xs t'; |
251 |
252 |
252 fun eq ((_, t1), (_, t2)) = Thm.eq_thm (t1, t2); |
253 fun eq ((_,t1),(_,t2)) = eq_thm (t1,t2) |
253 |
254 |
254 fun rem_d (rev_seen, []) = rev rev_seen |
255 fun rem_d (rev_seen, []) = rev rev_seen |
255 | rem_d (rev_seen, (x as (n', t')) :: xs) = |
256 | rem_d (rev_seen, (x as (n',t')) :: xs) = |
256 (case is_in rev_seen t' of |
257 case is_in rev_seen t' of |
257 NONE => rem_d (x :: rev_seen, xs) |
258 NONE => rem_d (x::rev_seen, xs) |
258 | SOME (n, t) => |
259 | SOME (n,t) => if nicer n n' |
259 if nicer n n' |
260 then rem_d (rev_seen, xs) |
260 then rem_d (rev_seen, xs) |
261 else rem_d (x::remove eq (n,t) rev_seen,xs) |
261 else rem_d (x :: remove eq (n, t) rev_seen, xs)) |
262 |
262 in rem_d ([], xs) end; |
263 in rem_d ([], xs) end; |
|
264 |
|
265 |
263 |
266 |
264 |
267 (* print_theorems *) |
265 (* print_theorems *) |
268 |
266 |
269 fun find_thms ctxt spec = |
267 fun find_thms ctxt spec = |
270 (PureThy.thms_containing (ProofContext.theory_of ctxt) spec |
268 (PureThy.thms_containing (ProofContext.theory_of ctxt) spec |
271 |> maps PureThy.selections) @ |
269 |> maps PureThy.selections) @ |
272 (ProofContext.lthms_containing ctxt spec |
270 (ProofContext.lthms_containing ctxt spec |
273 |> maps PureThy.selections |
271 |> maps PureThy.selections |
274 |> distinct (fn ((r1, th1), (r2, th2)) => |
272 |> distinct (fn ((r1, th1), (r2, th2)) => |
275 r1 = r2 andalso Drule.eq_thm_prop (th1, th2))); |
273 r1 = r2 andalso Thm.eq_thm_prop (th1, th2))); |
276 |
274 |
277 fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = |
275 fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = |
278 let |
276 let |
279 val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; |
277 val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; |
280 val filters = map (filter_criterion ctxt opt_goal) criteria; |
278 val filters = map (filter_criterion ctxt opt_goal) criteria; |
281 |
279 |
282 val raw_matches = all_filters filters (find_thms ctxt ([], [])); |
280 val raw_matches = all_filters filters (find_thms ctxt ([], [])); |
283 val matches = if rem_dups andalso not (null filters) |
281 val matches = |
284 then rem_thm_dups raw_matches |
282 if rem_dups andalso not (null filters) |
285 else raw_matches; |
283 then rem_thm_dups raw_matches |
|
284 else raw_matches; |
286 |
285 |
287 val len = length matches; |
286 val len = length matches; |
288 val limit = the_default (! thms_containing_limit) opt_limit; |
287 val limit = the_default (! thms_containing_limit) opt_limit; |
289 val thms = Library.drop (len - limit, matches); |
288 val thms = Library.drop (len - limit, matches); |
290 |
289 |