310 interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth |
310 interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth |
311 ts |
311 ts |
312 |> forall is_lambda_free ts ? cons "no_lams" |
312 |> forall is_lambda_free ts ? cons "no_lams" |
313 |> forall (not o exists_Const is_exists) ts ? cons "no_skos" |
313 |> forall (not o exists_Const is_exists) ts ? cons "no_skos" |
314 |> scope <> Global ? cons "local" |
314 |> scope <> Global ? cons "local" |
315 |> (case status of |
315 |> (case string_of_status status of "" => I | s => cons s) |
316 General => I |
|
317 | Induction => cons "induction" |
|
318 | Intro => cons "intro" |
|
319 | Inductive => cons "inductive" |
|
320 | Elim => cons "elim" |
|
321 | Simp => cons "simp" |
|
322 | Def => cons "def") |
|
323 |
316 |
324 (* Too many dependencies is a sign that a decision procedure is at work. There |
317 (* Too many dependencies is a sign that a decision procedure is at work. There |
325 isn't much too learn from such proofs. *) |
318 isn't much too learn from such proofs. *) |
326 val max_dependencies = 10 |
319 val max_dependencies = 15 |
327 val atp_dependency_default_max_fact = 50 |
320 val atp_dependency_default_max_fact = 50 |
328 |
321 |
|
322 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) |
|
323 val typedef_sig = [@{thm CollectI} |> nickname_of] |
|
324 |
|
325 (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) |
|
326 val typedef_ths = |
|
327 @{thms type_definition.Abs_inverse type_definition.Rep_inverse |
|
328 type_definition.Rep type_definition.Rep_inject |
|
329 type_definition.Abs_inject type_definition.Rep_cases |
|
330 type_definition.Abs_cases type_definition.Rep_induct |
|
331 type_definition.Abs_induct type_definition.Rep_range |
|
332 type_definition.Abs_image} |
|
333 |> map nickname_of |
|
334 |
329 fun trim_dependencies deps = |
335 fun trim_dependencies deps = |
330 if length deps <= max_dependencies then SOME deps else NONE |
336 if length deps > max_dependencies orelse deps = typedef_sig orelse |
|
337 exists (member (op =) typedef_ths) deps then |
|
338 NONE |
|
339 else |
|
340 SOME deps |
331 |
341 |
332 fun isar_dependencies_of all_names = |
342 fun isar_dependencies_of all_names = |
333 thms_in_proof (SOME all_names) #> trim_dependencies |
343 thms_in_proof (SOME all_names) #> trim_dependencies |
334 |
344 |
335 fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover |
345 fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover |