318 isn't much too learn from such proofs. *) |
318 isn't much too learn from such proofs. *) |
319 val max_dependencies = 20 |
319 val max_dependencies = 20 |
320 val atp_dependency_default_max_fact = 50 |
320 val atp_dependency_default_max_fact = 50 |
321 |
321 |
322 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) |
322 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) |
323 val typedef_sig = [@{thm CollectI} |> nickname_of] |
323 val typedef_deps = [@{thm CollectI} |> nickname_of] |
324 |
324 |
325 (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) |
325 (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) |
326 val typedef_ths = |
326 val typedef_ths = |
327 @{thms type_definition.Abs_inverse type_definition.Rep_inverse |
327 @{thms type_definition.Abs_inverse type_definition.Rep_inverse |
328 type_definition.Rep type_definition.Rep_inject |
328 type_definition.Rep type_definition.Rep_inject |
330 type_definition.Abs_cases type_definition.Rep_induct |
330 type_definition.Abs_cases type_definition.Rep_induct |
331 type_definition.Abs_induct type_definition.Rep_range |
331 type_definition.Abs_induct type_definition.Rep_range |
332 type_definition.Abs_image} |
332 type_definition.Abs_image} |
333 |> map nickname_of |
333 |> map nickname_of |
334 |
334 |
335 fun trim_dependencies deps = |
335 fun is_size_def [dep] th = |
336 if length deps > max_dependencies orelse deps = typedef_sig orelse |
336 (case first_field ".recs" dep of |
337 exists (member (op =) typedef_ths) deps then |
337 SOME (pref, _) => |
|
338 (case first_field ".size" (nickname_of th) of |
|
339 SOME (pref', _) => pref = pref' |
|
340 | NONE => false) |
|
341 | NONE => false) |
|
342 | is_size_def _ _ = false |
|
343 |
|
344 fun trim_dependencies th deps = |
|
345 if length deps > max_dependencies orelse deps = typedef_deps orelse |
|
346 exists (member (op =) typedef_ths) deps orelse is_size_def deps th then |
338 NONE |
347 NONE |
339 else |
348 else |
340 SOME deps |
349 SOME deps |
341 |
350 |
342 fun isar_dependencies_of all_names = |
351 fun isar_dependencies_of all_names th = |
343 thms_in_proof (SOME all_names) #> trim_dependencies |
352 th |> thms_in_proof (SOME all_names) |> trim_dependencies th |
344 |
353 |
345 fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover |
354 fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover |
346 auto_level facts all_names th = |
355 auto_level facts all_names th = |
347 case isar_dependencies_of all_names th of |
356 case isar_dependencies_of all_names th of |
348 SOME [] => NONE |
357 SOME [] => NONE |