31 val get_thms_closure: theory > thmref > thm list 
31 val get_thms_closure: theory > thmref > thm list 
32 val single_thm: string > thm list > thm 
32 val single_thm: string > thm list > thm 
33 val select_thm: thmref > thm list > thm list 
33 val select_thm: thmref > thm list > thm list 
34 val cond_extern_thm_sg: Sign.sg > string > xstring 
34 val cond_extern_thm_sg: Sign.sg > string > xstring 
35 val thms_containing: theory > string list * string list > (string * thm list) list 
35 val thms_containing: theory > string list * string list > (string * thm list) list 
36 val find_theorems: Sign.sg > (string * thm list) list > string list > (string * thm list) list 
36 val find_theorems: ('a * 'b list) list > ('a * 'b > bool) list > ('a * 'b list) list 
37 val thms_containing_consts: theory > string list > (string * thm) list 
37 val thms_containing_consts: theory > string list > (string * thm) list 
38 val find_matching_thms: (thm > thm list) * (term > term) 
38 val find_matching_thms: (thm > thm list) * (term > term) 
39 > theory > term > (string * thm) list 
39 > theory > term > (string * thm) list 

40 val is_matching_thm: (thm > thm list) * (term > term) 

41 > Sign.sg > term > (string * thm) > bool 
40 val find_intros: theory > term > (string * thm) list 
42 val find_intros: theory > term > (string * thm) list 
41 val find_intros_goal : theory > thm > int > (string * thm) list 
43 val find_intros_goal : theory > thm > int > (string * thm) list 
42 val find_elims : theory > term > (string * thm) list 
44 val find_elims : theory > term > (string * thm) list 
43 val hide_thms: bool > string list > theory > theory 
45 val hide_thms: bool > string list > theory > theory 
44 val store_thm: (bstring * thm) * theory attribute list > theory > theory * thm 
46 val store_thm: (bstring * thm) * theory attribute list > theory > theory * thm 
250 
252 
251 fun thms_containing_consts thy consts = 
253 fun thms_containing_consts thy consts = 
252 thms_containing thy (consts, []) > map #2 > List.concat 
254 thms_containing thy (consts, []) > map #2 > List.concat 
253 > map (fn th => (Thm.name_of_thm th, th)) 
255 > map (fn th => (Thm.name_of_thm th, th)) 
254 
256 
255 (* find_theorems  finding theorems by matching on a series of subterms *) 
257 (* Searching based on filters *) 
256 
258 (* a filter must only take a (name:string, theorem:Thm.thm) and return true 
257 (* Takes a string pattern, such as "(_::nat) + (_ + _)" and converts it into 
259 if it finds a match, false if it doesn't *) 
258 a term with all free variables made schematic *) 
260 
259 fun str_pattern_to_term sg str_pattern = 
261 (* given facts and filters, find all facts in which at least one theorem 

262 matches on ALL filters *) 

263 fun find_theorems facts filters = 
260 let 
264 let 
261 (* pattern as term with dummies as Consts *) 
265 (* break fact up into theorems, but associate them with the name of this 
262 val term_pattern = read_cterm sg (str_pattern, TypeInfer.logicT) 
266 fact, so that filters looking by name will only consider the fact's 
263 > Thm.term_of; 
267 name *) 
264 (* with dummies as Vars *) 
268 fun fact_to_names_thms (name, thms) = 
265 val v_pattern = #2 (Term.replace_dummy_patterns (1,term_pattern)); 
269 map (fn thm => (name, thm)) thms; 
266 in 
270 
267 (* with schematic vars *) 
271 (* all filters return true when applied to a named theorem *) 
268 #1 (Type.varify (v_pattern, [])) 
272 fun match_all_filters filters name_thm = 
269 end; 
273 List.all (fn filter => filter name_thm) filters; 
270 
274 
271 (* find all thms such that for each returned thm, all given 
275 (* at least one theorem in this fact which matches all filters *) 
272 propositions are subterms of it *) 
276 fun fact_matches_filters filters fact = 
273 fun thms_matching_patterns tsign (pat::pats) thms = 
277 List.exists (match_all_filters filters) (fact_to_names_thms fact); 
274 let 
278 
275 fun match_single pattern thm = 
279 fun matches x = (fact_matches_filters filters x) 
276 Pattern.matches_subterm tsign (pat, Thm.prop_of thm); 

277 in 

278 thms_matching_patterns tsign pats 

279 (List.filter (match_single pat) thms) 

280 end 

281  thms_matching_patterns _ _ thms = thms; 

282 

283 (* facts are pairs of theorem name and a list of its thms *) 

284 fun find_theorems sg facts str_patterns = 

285 let 

286 val typesg = Sign.tsig_of sg; 

287 

288 (* the patterns we will be looking for *) 

289 val patterns = map (str_pattern_to_term sg) str_patterns; 

290 

291 (* we are interested in theorems which have one or more thms for which 

292 all patterns are subterms *) 

293 fun matches (_, thms) = 

294 (not o null o (thms_matching_patterns typesg patterns)) thms 

295 in 
280 in 
296 List.filter matches facts 
281 List.filter matches facts 
297 end; 
282 end; 
298 
283 
299 (* intro/elim theorems *) 
284 (* intro/elim theorems *) 
344 else sels) 
329 else sels) 
345 end 
330 end 
346  select([],sels) = sels 
331  select([],sels) = sels 
347 
332 
348 in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end; 
333 in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end; 

334 

335 (* like find_matching_thms, but for one named theorem only *) 

336 fun is_matching_thm extract sg prop name_thm = 

337 (case top_const prop of NONE => false 

338  SOME c => 

339 not ([] = select_match(c,prop, sg,[name_thm],extract))); 

340 
349 
341 
350 fun find_matching_thms extract thy prop = 
342 fun find_matching_thms extract thy prop = 
351 (case top_const prop of NONE => [] 
343 (case top_const prop of NONE => [] 
352  SOME c => let val thms = thms_containing_consts thy [c] 
344  SOME c => let val thms = thms_containing_consts thy [c] 
353 in select_match(c,prop,Theory.sign_of thy,thms,extract) end) 
345 in select_match(c,prop,Theory.sign_of thy,thms,extract) end) 