equal
deleted
inserted
replaced
612 val max_dependencies = 20 |
612 val max_dependencies = 20 |
613 |
613 |
614 val prover_dependency_default_max_facts = 50 |
614 val prover_dependency_default_max_facts = 50 |
615 |
615 |
616 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) |
616 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) |
617 val typedef_deps = [@{thm CollectI} |> nickname_of_thm] |
617 val typedef_dep = nickname_of_thm @{thm CollectI} |
|
618 (* Mysterious parts of the class machinery create lots of proofs that refer |
|
619 exclusively to "someI_e" (and to some internal constructions). *) |
|
620 val class_some_dep = nickname_of_thm @{thm someI_ex} |
618 |
621 |
619 (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) |
622 (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) |
620 val typedef_ths = |
623 val typedef_ths = |
621 @{thms type_definition.Abs_inverse type_definition.Rep_inverse |
624 @{thms type_definition.Abs_inverse type_definition.Rep_inverse |
622 type_definition.Rep type_definition.Rep_inject |
625 type_definition.Rep type_definition.Rep_inject |
634 | NONE => false) |
637 | NONE => false) |
635 | NONE => false) |
638 | NONE => false) |
636 | is_size_def _ _ = false |
639 | is_size_def _ _ = false |
637 |
640 |
638 fun trim_dependencies th deps = |
641 fun trim_dependencies th deps = |
639 if length deps > max_dependencies then |
642 if length deps > max_dependencies then NONE else SOME deps |
640 NONE |
643 |
641 else |
644 fun isar_dependencies_of name_tabs th = |
642 SOME (if deps = typedef_deps orelse |
645 let |
643 exists (member (op =) typedef_ths) deps orelse |
646 val deps = thms_in_proof (SOME name_tabs) th |
644 is_size_def deps th then |
647 in |
645 [] |
648 if deps = [typedef_dep] orelse deps = [class_some_dep] orelse |
646 else |
649 exists (member (op =) typedef_ths) deps orelse is_size_def deps th then |
647 deps) |
650 [] |
648 |
651 else |
649 val isar_dependencies_of = thms_in_proof o SOME |
652 deps |
|
653 end |
650 |
654 |
651 fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover |
655 fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover |
652 auto_level facts name_tabs th = |
656 auto_level facts name_tabs th = |
653 case isar_dependencies_of name_tabs th of |
657 case isar_dependencies_of name_tabs th of |
654 [] => (false, []) |
658 [] => (false, []) |